Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 981:6b67e43733ca
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Thu, 10 Nov 2022 09:07:07 +0900 |
| parents | 49cf50d451e1 |
| children | 6d29911a9d00 |
| files | src/zorn.agda |
| diffstat | 1 files changed, 8 insertions(+), 263 deletions(-) [+] |
line wrap: on
line diff
--- a/src/zorn.agda Wed Nov 09 11:10:11 2022 +0900 +++ b/src/zorn.agda Thu Nov 10 09:07:07 2022 +0900 @@ -401,8 +401,8 @@ → odef (UnionCF A f mf ay supf a) c → odef (UnionCF A f mf ay supf b) c chain-mono f mf ay supf supf-mono {a} {b} {c} a≤b ⟪ ua , ch-init fc ⟫ = ⟪ ua , ch-init fc ⟫ -chain-mono f mf ay supf supf-mono {a} {b} {c} a≤b ⟪ uaa , ch-is-sup ua ua<x is-sup fc ⟫ = - ⟪ uaa , ch-is-sup ua (ordtrans<-≤ ua<x ? ) is-sup fc ⟫ +chain-mono f mf ay supf supf-mono {a} {b} {c} a≤b ⟪ uaa , ch-is-sup ua ua≤x is-sup fc ⟫ = + ⟪ uaa , ch-is-sup ua (OrdTrans ua≤x (supf-mono a≤b) ) is-sup fc ⟫ record ZChain ( A : HOD ) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f) {y : Ordinal} (ay : odef A y) ( z : Ordinal ) : Set (Level.suc n) where @@ -483,43 +483,6 @@ fsp≤sp : f sp <= sp fsp≤sp = subst (λ k → f k <= sp ) (sym (HasPrev.x=fy hp)) im00 -UChain⊆ : ( A : HOD ) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f) - {z y : Ordinal} (ay : odef A y) { supf supf1 : Ordinal → Ordinal } - → (supf-mono : {x y : Ordinal } → x o≤ y → supf x o≤ supf y ) - → ( { x : Ordinal } → x o< z → supf x ≡ supf1 x) - → ( { x : Ordinal } → z o≤ x → supf z o≤ supf1 x) - → UnionCF A f mf ay supf z ⊆' UnionCF A f mf ay supf1 z -UChain⊆ A f mf {z} {y} ay {supf} {supf1} supf-mono eq<x lex ⟪ az , ch-init fc ⟫ = ⟪ az , ch-init fc ⟫ -UChain⊆ A f mf {z} {y} ay {supf} {supf1} supf-mono eq<x lex ⟪ az , ch-is-sup u {x} u≤x is-sup fc ⟫ = ⟪ az , ch-is-sup u ? cp1 fc1 ⟫ where - u≤x0 : u o< z - u≤x0 = supf-inject0 supf-mono ? - u≤x1 : supf1 u o< supf1 z - u≤x1 = subst (λ k → k o< supf1 z ) (eq<x u≤x0) (ordtrans<-≤ u≤x ? ) -- (lex o≤-refl ) ) - fc1 : FClosure A f (supf1 u) x - fc1 = subst (λ k → FClosure A f k x ) (eq<x u≤x0) fc - uc01 : {s : Ordinal } → supf1 s o< supf1 u → s o< z - uc01 {s} s<u with trio< s z - ... | tri< a ¬b ¬c = a - ... | tri≈ ¬a b ¬c = ⊥-elim ( o≤> uc02 s<u ) where -- (supf-mono (o<→≤ u≤x0)) - uc02 : supf1 u o≤ supf1 s - uc02 = begin - supf1 u <⟨ u≤x1 ⟩ - supf1 z ≡⟨ cong supf1 (sym b) ⟩ - supf1 s ∎ where open o≤-Reasoning O - ... | tri> ¬a ¬b c = ⊥-elim ( o≤> uc03 s<u ) where - uc03 : supf1 u o≤ supf1 s - uc03 = begin - supf1 u ≡⟨ sym (eq<x u≤x0) ⟩ - supf u <⟨ ? ⟩ - supf z ≤⟨ lex (o<→≤ c) ⟩ - supf1 s ∎ where open o≤-Reasoning O - cp1 : ChainP A f mf ay supf1 u - cp1 = record { fcy<sup = λ {z} fc → subst (λ k → (z ≡ k) ∨ ( z << k ) ) (eq<x u≤x0) (ChainP.fcy<sup is-sup fc ) - ; order = λ {s} {z} s<u fc → subst (λ k → (z ≡ k) ∨ ( z << k ) ) (eq<x u≤x0) - (ChainP.order is-sup (subst₂ (λ j k → j o< k ) (sym (eq<x (uc01 s<u) )) (sym (eq<x u≤x0)) s<u) - (subst (λ k → FClosure A f k z ) (sym (eq<x (uc01 s<u) )) fc )) - ; supu=u = trans (sym (eq<x u≤x0)) (ChainP.supu=u is-sup) } - record ZChain1 ( A : HOD ) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f) {y : Ordinal} (ay : odef A y) (zc : ZChain A f mf ay (& A)) ( z : Ordinal ) : Set (Level.suc n) where supf = ZChain.supf zc @@ -670,7 +633,7 @@ zc05 : odef (UnionCF A f mf ay supf b) (supf s) zc05 with zc04 ... | ⟪ as , ch-init fc ⟫ = ⟪ as , ch-init fc ⟫ - ... | ⟪ as , ch-is-sup u u≤x is-sup fc ⟫ = ⟪ as , ch-is-sup u ? is-sup fc ⟫ where + ... | ⟪ as , ch-is-sup u u≤x is-sup fc ⟫ = ⟪ as , ch-is-sup u (o<→≤ zc08) is-sup fc ⟫ where zc07 : FClosure A f (supf u) (supf s) -- supf u ≤ supf s → supf u o≤ supf s zc07 = fc zc06 : supf u ≡ u @@ -705,7 +668,7 @@ is-max {a} {b} ua b<x ab P a<b with ODC.or-exclude O P is-max {a} {b} ua b<x ab P a<b | case1 has-prev = is-max-hp x {a} {b} ua ab has-prev a<b is-max {a} {b} ua sb<sx ab P a<b | case2 is-sup - = ⟪ ab , ch-is-sup b ? m06 (subst (λ k → FClosure A f k b) (sym m05) (init ab refl)) ⟫ where + = ⟪ ab , ch-is-sup b (ZChain.supf-mono zc (o<→≤ b<x)) m06 (subst (λ k → FClosure A f k b) (sym m05) (init ab refl)) ⟫ where b<A : b o< & A b<A = z09 ab b<x : b o< x @@ -731,7 +694,7 @@ is-max {a} {b} ua sb<sx ab P a<b | case1 has-prev = is-max-hp x {a} {b} ua ab has-prev a<b is-max {a} {b} ua sb<sx ab P a<b | case2 is-sup with IsSUP.x≤sup (proj2 is-sup) (init-uchain A f mf ay ) ... | case1 b=y = ⟪ subst (λ k → odef A k ) b=y ay , ch-init (subst (λ k → FClosure A f y k ) b=y (init ay refl )) ⟫ - ... | case2 y<b = ⟪ ab , ch-is-sup b ? m06 (subst (λ k → FClosure A f k b) (sym m05) (init ab refl)) ⟫ where + ... | case2 y<b = ⟪ ab , ch-is-sup b (ZChain.supf-mono zc (o<→≤ b<x)) m06 (subst (λ k → FClosure A f k b) (sym m05) (init ab refl)) ⟫ where m09 : b o< & A m09 = subst (λ k → k o< & A) &iso ( c<→o< (subst (λ k → odef A k ) (sym &iso ) ab)) b<x : b o< x @@ -965,182 +928,6 @@ fcpu : {u z : Ordinal } → FClosure A f (supf0 u) z → u o≤ px → FClosure A f (supf1 u) z fcpu {u} {z} fc u≤px = subst (λ k → FClosure A f k z ) (sym (sf1=sf0 u≤px)) fc - zc11 : {z : Ordinal} → odef (UnionCF A f mf ay supf1 x) z → odef pchainpx z - zc11 {z} ⟪ az , ch-init fc ⟫ = case1 ⟪ az , ch-init fc ⟫ - zc11 {z} ⟪ az , ch-is-sup u su<sx is-sup fc ⟫ = zc21 fc where - u≤x : u o< x - u≤x = supf-inject0 supf1-mono ? -- su<sx - u≤px : u o≤ px - u≤px = zc-b<x _ u≤x - zc21 : {z1 : Ordinal } → FClosure A f (supf1 u) z1 → odef pchainpx z1 - zc21 {z1} (fsuc z2 fc ) with zc21 fc - ... | case1 ⟪ ua1 , ch-init fc₁ ⟫ = case1 ⟪ proj2 ( mf _ ua1) , ch-init (fsuc _ fc₁) ⟫ - ... | case1 ⟪ ua1 , ch-is-sup u u≤x u1-is-sup fc₁ ⟫ = case1 ⟪ proj2 ( mf _ ua1) , ch-is-sup u u≤x u1-is-sup (fsuc _ fc₁) ⟫ - ... | case2 fc = case2 (fsuc _ fc) - zc21 (init asp refl ) with trio< (supf0 u) (supf0 px) | inspect supf1 u - ... | tri< a ¬b ¬c | _ = case1 ⟪ asp , ch-is-sup u ? record {fcy<sup = zc13 ; order = zc17 - ; supu=u = trans (sym (sf1=sf0 (o<→≤ u<px))) (ChainP.supu=u is-sup) } (init asp0 (sym (sf1=sf0 (o<→≤ u<px))) ) ⟫ where - u<px : u o< px - u<px = ZChain.supf-inject zc a - asp0 : odef A (supf0 u) - asp0 = ZChain.asupf zc - zc17 : {s : Ordinal} {z1 : Ordinal} → supf0 s o< supf0 u → - FClosure A f (supf0 s) z1 → (z1 ≡ supf0 u) ∨ (z1 << supf0 u) - zc17 {s} {z1} ss<spx fc = subst (λ k → (z1 ≡ k) ∨ (z1 << k)) ((sf1=sf0 u≤px)) ( ChainP.order is-sup - (subst₂ (λ j k → j o< k ) (sym (sf1=sf0 zc18)) (sym (sf1=sf0 u≤px)) ss<spx) (fcpu fc zc18) ) where - zc18 : s o≤ px - zc18 = ordtrans (ZChain.supf-inject zc ss<spx) u≤px - zc13 : {z : Ordinal } → FClosure A f y z → (z ≡ supf0 u) ∨ ( z << supf0 u ) - zc13 {z} fc = subst (λ k → (z ≡ k) ∨ ( z << k )) (sf1=sf0 (o<→≤ u<px)) ( ChainP.fcy<sup is-sup fc ) - ... | tri≈ ¬a b ¬c | _ = case2 (init (subst (λ k → odef A k) b (ZChain.asupf zc) ) (sym (trans (sf1=sf0 u≤px) b ))) - ... | tri> ¬a ¬b c | _ = ⊥-elim ( ¬p<x<op ⟪ ZChain.supf-inject zc c , subst (λ k → u o< k ) (sym (Oprev.oprev=x op)) u≤x ⟫ ) - - zc35 : {z : Ordinal} → ¬ (supf0 px ≡ px) → odef (UnionCF A f mf ay supf1 x) z → odef (UnionCF A f mf ay supf0 x) z - zc35 {z} ne ⟪ ua1 , ch-init fc ⟫ = ⟪ ua1 , ch-init fc ⟫ - zc35 {z} ne ⟪ ua1 , ch-is-sup u u≤x is-sup fc ⟫ with osuc-≡< ( ZChain.supf-mono zc (o<→≤ (supf-inject0 supf1-mono ?)) ) - ... | case1 eq = zc34 where - u≤x0 : u o≤ px - u≤x0 = subst (λ k → u o< k ) (sym (Oprev.oprev=x op)) (supf-inject0 supf1-mono ? ) - zc34 : odef (UnionCF A f mf ay supf0 x) z - zc34 with trio< (supf0 px) px - ... | tri< sf0px<px ¬b ¬c = cp3 ( subst ( λ k → FClosure A f k z) - (trans (trans (sf1=sf0 u≤x0) eq) (ZChain.supfmax zc px<x) ) fc) where - cp3 : {z : Ordinal } → FClosure A f (supf0 px) z → odef (UnionCF A f mf ay supf0 x) z - cp3 (init uz refl) = chain-mono f mf ay supf0 (ZChain.supf-mono zc) (o<→≤ px<x) (ZChain.csupf zc sf0px<px) - cp3 (fsuc uz fc) = ZChain.f-next zc (cp3 fc) - ... | tri≈ ¬a b ¬c = ⊥-elim (ne b) - ... | tri> ¬a ¬b px<sf0px = ⊥-elim (¬p<x<op ⟪ cp5 , cp4 ⟫ ) where - cp4 : u o< osuc px - cp4 = subst (λ k → u o< k ) (sym (Oprev.oprev=x op)) ( supf-inject0 supf1-mono ? ) - cp5 : px o< u - cp5 = subst (λ k → px o< k ) ( begin - supf0 px ≡⟨ sym (ZChain.supfmax zc px<x) ⟩ - supf0 x ≡⟨ sym eq ⟩ - supf0 u ≡⟨ sym (sf1=sf0 u≤x0) ⟩ - supf1 u ≡⟨ ChainP.supu=u is-sup ⟩ - u ∎ ) px<sf0px where open ≡-Reasoning - ... | case2 u≤x1 = ⟪ ua1 , ch-is-sup u ? cp1 fc1 ⟫ where - u≤x0 : u o< x - u≤x0 = supf-inject0 supf1-mono ? -- supf0 u o≤ px ≡ supf0 px → supf0 u ≡ supf0 px ∨ u o< px - sf0u=sf1u : supf0 u ≡ supf1 u - sf0u=sf1u = sym (sf1=sf0 (subst (λ k → u o< k ) (sym (Oprev.oprev=x op)) u≤x0 )) - cp2 : {s : Ordinal } → supf0 s o< supf0 u → supf0 s ≡ supf1 s - cp2 {s} ss<su = sym ( sf1=sf0 ( begin - s <⟨ ZChain.supf-inject zc ss<su ⟩ - u ≤⟨ subst (λ k → u o< k ) (sym (Oprev.oprev=x op)) u≤x0 ⟩ - px ∎ )) where open o≤-Reasoning O - fc1 : FClosure A f (supf0 u) z - fc1 = subst (λ k → FClosure A f k z ) (sym sf0u=sf1u) fc - cp1 : ChainP A f mf ay supf0 u - cp1 = record { fcy<sup = λ {z} fc → subst (λ k → (z ≡ k) ∨ ( z << k ) ) (sym sf0u=sf1u) (ChainP.fcy<sup is-sup fc ) - ; order = λ {s} {z} s<u fc → subst (λ k → (z ≡ k) ∨ ( z << k ) ) (sym sf0u=sf1u) - (ChainP.order is-sup (subst₂ (λ j k → j o< k ) (cp2 s<u) sf0u=sf1u s<u) - (subst (λ k → FClosure A f k z ) (cp2 s<u) fc )) - ; supu=u = trans (sym (sf1=sf0 (subst (λ k → u o< k ) (sym (Oprev.oprev=x op)) u≤x0 ))) (ChainP.supu=u is-sup) } - - zc33 : {z : Ordinal} → ¬ (supf0 px o< sp1) → odef (UnionCF A f mf ay supf1 x) z → odef (UnionCF A f mf ay supf0 x) z - zc33 {z} lt = UChain⊆ A f mf ay supf1-mono (λ lt → sym (sf=eq lt)) sf≤0 where - sf≤0 : { z : Ordinal } → x o≤ z → supf1 x o≤ supf0 z - sf≤0 {z} x≤z with trio< z px - ... | tri< a ¬b ¬c = ⊥-elim ( o<> (osucc a) (subst (λ k → k o≤ z) (sym (Oprev.oprev=x op)) x≤z ) ) - ... | tri≈ ¬a b ¬c = ⊥-elim ( o≤> x≤z (subst (λ k → k o< x ) (sym b) px<x )) - ... | tri> ¬a ¬b px<z with trio< sp1 (supf0 x) -- = ? --- sp1 o≤ supf0 x - ... | tri< a ¬b ¬c = subst₂ ( λ j k → j o≤ k) (sym (sf1=sp1 px<x)) - (trans (ZChain.supfmax zc px<x) (sym (ZChain.supfmax zc px<z))) ( o<→≤ a ) - ... | tri≈ ¬a b ¬c = subst₂ ( λ j k → j o≤ k) (sym (sf1=sp1 px<x)) - (trans (ZChain.supfmax zc px<x) (sym (ZChain.supfmax zc px<z))) (o≤-refl0 b) - ... | tri> ¬a ¬b sf0<sp1 = ⊥-elim ( lt ( ordtrans≤-< (ZChain.supf-mono zc (o<→≤ px<x)) sf0<sp1 )) - - 3cases : (¬ (supf0 px ≡ px)) ∨ ( ¬ (supf0 px o< sp1 )) ∨ ( (supf0 px ≡ px) ∧ (supf0 px o< sp1 )) - 3cases with o≡? (supf0 px) px - ... | no ne = case1 ne - ... | yes eq with trio< (supf0 px) sp1 - ... | tri< a ¬b ¬c = case2 (case2 ⟪ eq , a ⟫ ) - ... | tri≈ ¬a b ¬c = case2 (case1 ¬a ) - ... | tri> ¬a ¬b c = case2 (case1 ¬a ) - - zc12 : {z : Ordinal} → supf0 px ≡ px → supf0 px o< sp1 → odef pchainpx z → odef (UnionCF A f mf ay supf1 x) z - zc12 {z} sfpx=px sfpx<sp (case1 ⟪ az , ch-init fc ⟫ ) = ⟪ az , ch-init fc ⟫ - zc12 {z} sfpx=px sfpx<sp (case1 ⟪ az , ch-is-sup u su<sx is-sup fc ⟫ ) = zc21 fc where - u<px : u o< px - u<px = ZChain.supf-inject zc ? -- su<sx - u≤x : u o< x - u≤x = ordtrans u<px px<x - u≤px : u o≤ px - u≤px = o<→≤ u<px - s1u<s1x : supf1 u o< supf1 x - s1u<s1x = ordtrans<-≤ (subst₂ (λ j k → j o< k ) (sym (sf1=sf0 u≤px )) (sym (sf1=sf0 o≤-refl)) ?) (supf1-mono (o<→≤ px<x) ) - zc21 : {z1 : Ordinal } → FClosure A f (supf0 u) z1 → odef (UnionCF A f mf ay supf1 x) z1 - zc21 {z1} (fsuc z2 fc ) with zc21 fc - ... | ⟪ ua1 , ch-init fc₁ ⟫ = ⟪ proj2 ( mf _ ua1) , ch-init (fsuc _ fc₁) ⟫ - ... | ⟪ ua1 , ch-is-sup u u≤x u1-is-sup fc₁ ⟫ = ⟪ proj2 ( mf _ ua1) , ch-is-sup u u≤x u1-is-sup (fsuc _ fc₁) ⟫ - zc21 (init asp refl ) with trio< u px | inspect supf1 u - ... | tri< a ¬b ¬c | _ = ⟪ asp , ch-is-sup u - ? -- s1u<s1x - record {fcy<sup = zc13 ; order = zc17 ; supu=u = trans (sf1=sf0 u≤px ) (ChainP.supu=u is-sup) } zc14 ⟫ where - zc17 : {s : Ordinal} {z1 : Ordinal} → supf1 s o< supf1 u → - FClosure A f (supf1 s) z1 → (z1 ≡ supf1 u) ∨ (z1 << supf1 u) - zc17 {s} {z1} ss<su fc = subst (λ k → (z1 ≡ k) ∨ (z1 << k)) (sym (sf1=sf0 (o<→≤ u<px))) ( ChainP.order is-sup - (subst₂ (λ j k → j o< k ) (sf1=sf0 s≤px) (sf1=sf0 (o<→≤ u<px)) ss<su) (fcup fc s≤px) ) where - s≤px : s o≤ px -- ss<su : supf1 s o< supf1 u - s≤px = ordtrans ( supf-inject0 supf1-mono ss<su ) (o<→≤ u<px) - zc14 : FClosure A f (supf1 u) (supf0 u) - zc14 = init (subst (λ k → odef A k ) (sym (sf1=sf0 u≤px)) asp) (sf1=sf0 u≤px) - zc13 : {z : Ordinal } → FClosure A f y z → (z ≡ supf1 u) ∨ ( z << supf1 u ) - zc13 {z} fc = subst (λ k → (z ≡ k) ∨ ( z << k )) (sym (sf1=sf0 u≤px )) ( ChainP.fcy<sup is-sup fc ) - ... | tri≈ ¬a b ¬c | _ = ⟪ asp , ch-is-sup px ? record { fcy<sup = zc13 - ; order = zc17 ; supu=u = zc18 } (init asupf1 (trans (sf1=sf0 o≤-refl ) (cong supf0 (sym b))) ) ⟫ where - zc13 : {z : Ordinal } → FClosure A f y z → (z ≡ supf1 px) ∨ ( z << supf1 px ) - zc13 {z} fc = subst (λ k → (z ≡ k) ∨ (z << k)) (trans (cong supf0 b) (sym (sf1=sf0 o≤-refl))) (ChainP.fcy<sup is-sup fc ) - zc18 : supf1 px ≡ px - zc18 = begin - supf1 px ≡⟨ sf1=sf0 o≤-refl ⟩ - supf0 px ≡⟨ cong supf0 (sym b) ⟩ - supf0 u ≡⟨ ChainP.supu=u is-sup ⟩ - u ≡⟨ b ⟩ - px ∎ where open ≡-Reasoning - zc17 : {s : Ordinal} {z1 : Ordinal} → supf1 s o< supf1 px → - FClosure A f (supf1 s) z1 → (z1 ≡ supf1 px) ∨ (z1 << supf1 px) - zc17 {s} {z1} ss<spx fc = subst (λ k → (z1 ≡ k) ∨ (z1 << k)) (trans (cong supf0 b) (sym (sf1=sf0 o≤-refl))) - ( ChainP.order is-sup (subst₂ (λ j k → j o< k) (sf1=sf0 s≤px) zc19 ss<spx) (fcup fc s≤px) ) where - zc19 : supf1 px ≡ supf0 u - zc19 = trans (sf1=sf0 o≤-refl) (cong supf0 (sym b)) - s≤px : s o≤ px - s≤px = o<→≤ (supf-inject0 supf1-mono ss<spx) - ... | tri> ¬a ¬b c | _ = ⊥-elim ( ¬p<x<op ⟪ c , u≤px ⟫ ) - zc12 {z} sfpx=px sfpx<sp (case2 fc) = zc21 fc where - --- supf0 px o< sp1 - zc21 : {z1 : Ordinal } → FClosure A f (supf0 px) z1 → odef (UnionCF A f mf ay supf1 x) z1 - zc21 {z1} (fsuc z2 fc ) with zc21 fc - ... | ⟪ ua1 , ch-init fc₁ ⟫ = ⟪ proj2 ( mf _ ua1) , ch-init (fsuc _ fc₁) ⟫ - ... | ⟪ ua1 , ch-is-sup u u≤x u1-is-sup fc₁ ⟫ = ⟪ proj2 ( mf _ ua1) , ch-is-sup u u≤x u1-is-sup (fsuc _ fc₁) ⟫ - zc21 (init asp refl ) = ⟪ asp , ch-is-sup px ? - record {fcy<sup = zc13 ; order = zc17 ; supu=u = zc15 } zc14 ⟫ where - zc15 : supf1 px ≡ px - zc15 = trans (sf1=sf0 o≤-refl ) (sfpx=px) - zc18 : supf1 px o< supf1 x - zc18 = subst₂ ( λ j k → j o< k ) (sym (sf1=sf0 o≤-refl)) (sym (sf1=sp1 px<x)) sfpx<sp - zc14 : FClosure A f (supf1 px) (supf0 px) - zc14 = init (subst (λ k → odef A k) (sym (sf1=sf0 o≤-refl)) asp) (sf1=sf0 o≤-refl) - zc13 : {z : Ordinal } → FClosure A f y z → (z ≡ supf1 px ) ∨ ( z << supf1 px ) - zc13 {z} fc = subst (λ k → (z ≡ k) ∨ ( z << k )) (sym (sf1=sf0 o≤-refl)) ( ZChain.fcy<sup zc o≤-refl fc ) - zc17 : {s : Ordinal} {z1 : Ordinal} → supf1 s o< supf1 px → - FClosure A f (supf1 s) z1 → (z1 ≡ supf1 px) ∨ (z1 << supf1 px) - zc17 {s} {z1} ss<spx fc = subst (λ k → (z1 ≡ k) ∨ (z1 << k )) mins-is-spx - (MinSUP.x≤sup mins (zc25 (fcup fc (o<→≤ s<px) )) ) where - mins : MinSUP A (UnionCF A f mf ay supf0 px) - mins = ZChain.minsup zc o≤-refl - mins-is-spx : MinSUP.sup mins ≡ supf1 px - mins-is-spx = trans (sym ( ZChain.supf-is-minsup zc o≤-refl ) ) (sym (sf1=sf0 o≤-refl )) - s<px : s o< px - s<px = supf-inject0 supf1-mono ss<spx - sf<px : supf0 s o< px - sf<px = subst₂ (λ j k → j o< k ) (sf1=sf0 (o<→≤ s<px)) (trans (sf1=sf0 o≤-refl) (sfpx=px)) ss<spx - zc25 : {z1 : Ordinal } → FClosure A f (supf0 s) z1 → odef (UnionCF A f mf ay supf0 px) z1 - zc25 (init as refl ) = ZChain.csupf zc sf<px - zc25 (fsuc x fc) = ZChain.f-next zc (zc25 fc) - - record STMP {z : Ordinal} (z≤x : z o≤ x ) : Set (Level.suc n) where field tsup : MinSUP A (UnionCF A f mf ay supf1 z) @@ -1173,50 +960,8 @@ odef (UnionCF A f mf ay supf1 z) x → (x ≡ sup2) ∨ (x << sup2)) → MinSUP.sup m o≤ sup2 ms01 {sup2} us P = MinSUP.minsup m ? ? - csupf0 : {z1 : Ordinal } → supf1 z1 o< px → z1 o≤ px → odef (UnionCF A f mf ay supf1 x) (supf1 z1) - csupf0 {z1} s0z<px z≤px = subst (λ k → odef (UnionCF A f mf ay supf1 x) k ) (sym (sf1=sf0 z≤px)) ( - UChain⊆ A f mf {x} {y} ay {supf0} {supf1} (ZChain.supf-mono zc) sf=eq sf≤ - (chain-mono f mf ay supf0 (ZChain.supf-mono zc) (o<→≤ px<x) - (ZChain.csupf zc (subst (λ k → k o< px) (sf1=sf0 z≤px) s0z<px)))) - -- px o< z1 , supf1 z1 o< x -> sp1 o≤ z1 -- sp1 o≤ supf1 x - -- px o≤ supf1 z1 , supf1 z1 o< x -> supf1 z1 ≡ px --> z1 o≤ px → supf0 z1 ≡ px - --> px o< x1 → sp1 ≡ px - csupf1 : {z1 : Ordinal } → supf1 z1 o< x → odef (UnionCF A f mf ay supf1 x) (supf1 z1) - csupf1 {z1} sz1<x = csupf2 where - psz1≤px : supf1 z1 o≤ px - psz1≤px = subst (λ k → supf1 z1 o< k ) (sym opx=x) sz1<x - csupf2 : odef (UnionCF A f mf ay supf1 x) (supf1 z1) - csupf2 with osuc-≡< psz1≤px - ... | case2 lt with trio< z1 px | inspect supf1 z1 - ... | tri< a ¬b ¬c | record { eq = eq } = - subst (λ k → odef (UnionCF A f mf ay supf1 x) k ) eq ( csupf0 (subst (λ k → k o< px) (sym eq) lt) (o<→≤ a )) - ... | tri≈ ¬a b ¬c | record { eq = eq } = - subst (λ k → odef (UnionCF A f mf ay supf1 x) k ) eq ( csupf0 (subst (λ k → k o< px) (sym eq) lt) (o≤-refl0 b )) - ... | tri> ¬a ¬b px<z1 | record { eq = eq } = ⟪ MinSUP.asm sup1 , ch-is-sup sp1 cs00 ? (init asupf1 ssp1=sp1 ) ⟫ where - ssp1=sp1 : supf1 sp1 ≡ sp1 - ssp1=sp1 = ? - cs00 : supf1 sp1 o≤ supf1 x - cs00 = ? - csupf2 | case1 psz1=px with trio< z1 px | inspect supf1 z1 - ... | tri< a ¬b ¬c | record { eq = eq } = ⟪ ZChain.asupf zc , ch-is-sup px cs00 ? (init asupf1 cs01 ) ⟫ where - -- spuf1 z1 == px o< x , z1 o< px, - cs03 : supf0 z1 o< px - cs03 = ? - cs02 : odef (UnionCF A f mf ay supf0 px) (supf0 z1) - cs02 = ZChain.csupf zc cs03 - cs01 : supf1 px ≡ supf0 z1 - cs01 = ? - cs00 : supf1 px o≤ supf1 x - cs00 = supf1-mono (o<→≤ px<x) - ... | tri≈ ¬a b ¬c | record { eq = eq } = ⟪ ZChain.asupf zc , ch-is-sup px cs00 ? (init asupf1 cs01 ) ⟫ where - cs01 : supf1 px ≡ supf0 z1 - cs01 = trans (sf1=sf0 o≤-refl) (cong supf0 (sym b) ) - cs00 : supf1 px o≤ supf1 x - cs00 = supf1-mono (o<→≤ px<x) - ... | tri> ¬a ¬b c | record { eq = eq } = ⟪ MinSUP.asm sup1 , ch-is-sup x o≤-refl ? (init asupf1 cs01 ) ⟫ where - cs01 : supf1 x ≡ sp1 - cs01 = sf1=sp1 px<x + csupf1 {z1} sz1<x = ? zc41 | (case1 x<sp ) = record { supf = supf0 ; sup=u = ? ; asupf = ? ; supf-mono = ? ; supf-< = ? ; supfmax = ? ; minsup = ? ; supf-is-minsup = ? ; csupf = ? } where @@ -1686,8 +1431,8 @@ z45 p = subst (λ k → (* (cf nmx k) ≡ * d) ∨ (* (cf nmx k) < * d)) (sym x=fy) p z48 : supf mc << d z48 = sc<<d {mc} asc spd - z53 : supf u o< supf (& A) - z53 = ordtrans<-≤ u≤x ? + z53 : supf u o≤ supf (& A) + z53 = OrdTrans u≤x ? z52 : ( u ≡ mc ) ∨ ( u << mc ) z52 = MinSUP.x≤sup msp1 ⟪ subst (λ k → odef A k ) (ChainP.supu=u is-sup1) (A∋fcs _ _ (cf-is-≤-monotonic nmx) fc) , ch-is-sup u ? is-sup1 (init (ZChain.asupf zc) (ChainP.supu=u is-sup1)) ⟫