Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 985:0d8dafbecb0d
zc10 : supf c ≡ supf (& A) → {x : Ordinal } → odef A x → ¬ ( c << x ) ?
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sat, 12 Nov 2022 01:49:25 +0900 |
| parents | 94357ced682d |
| children | 557f8145d3c1 |
| files | src/zorn.agda |
| diffstat | 1 files changed, 14 insertions(+), 350 deletions(-) [+] |
line wrap: on
line diff
--- a/src/zorn.agda Wed Nov 09 03:14:40 2022 +0900 +++ b/src/zorn.agda Sat Nov 12 01:49:25 2022 +0900 @@ -418,7 +418,7 @@ minsup : {x : Ordinal } → x o≤ z → MinSUP A (UnionCF A f mf ay supf x) supf-is-minsup : {x : Ordinal } → (x≤z : x o≤ z) → supf x ≡ MinSUP.sup ( minsup x≤z ) - csupf : {b : Ordinal } → supf b o< z → odef (UnionCF A f mf ay supf z) (supf b) -- supf z is not an element of this chain + csupf : {b : Ordinal } → supf b o< supf z → odef (UnionCF A f mf ay supf z) (supf b) -- supf z is not an element of this chain chain : HOD chain = UnionCF A f mf ay supf z @@ -666,7 +666,7 @@ s<z : s o< & A s<z = ordtrans s<b b<z zc04 : odef (UnionCF A f mf ay supf (& A)) (supf s) - zc04 = ZChain.csupf zc (z09 (ZChain.asupf zc)) + zc04 = ZChain.csupf zc ? -- (z09 (ZChain.asupf zc)) zc05 : odef (UnionCF A f mf ay supf b) (supf s) zc05 with zc04 ... | ⟪ as , ch-init fc ⟫ = ⟪ as , ch-init fc ⟫ @@ -995,152 +995,6 @@ ... | 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 u<x)) ) - ... | 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 u<x ) - 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 u<x ) - 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 u<x1 cp1 fc1 ⟫ where - u<x0 : u o< x - u<x0 = supf-inject0 supf1-mono u<x -- 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)) su<sx) (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 (subst (λ k → supf1 k o< supf1 x) b s1u<s1x) 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 zc18 - 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) @@ -1177,59 +1031,11 @@ 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)))) + (ZChain.csupf zc ? ))) -- (subst (λ k → k o< px) (sf1=sf0 z≤px) s0z<px)))) -- px o< z1 , px o≤ supf1 z1 --> px o≤ sp1 o< x -- sp1 ≡ px--> odef (UnionCF A f mf ay supf1 x) sp1 - csupf1 : {z1 : Ordinal } → supf1 z1 o< x → odef (UnionCF A f mf ay supf1 x) (supf1 z1) - csupf1 {z1} sz1<x = csupf2 where - -- z1 o< px → supf1 z1 ≡ supf0 z1 - -- z1 ≡ px , supf0 px o< px .. px o< z1, x o≤ z1 ... supf1 z1 ≡ sp1 - -- z1 ≡ px , supf0 px ≡ px - 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 3cases - ... | case2 (case2 p) with trio< z1 px | inspect supf1 z1 - ... | tri< a ¬b ¬c | record { eq = eq1 } with osuc-≡< psz1≤px - ... | case2 lt = zc12 (proj1 p) (proj2 p) (case1 cs03) where - cs03 : odef (UnionCF A f mf ay supf0 px) (supf0 z1) - cs03 = ZChain.csupf zc (subst (λ k → k o< px) (sf1=sf0 (o<→≤ a)) lt ) - ... | case1 sfz=px with osuc-≡< ( supf1-mono (o<→≤ a) ) - ... | case1 sfz=sfpx = zc12 (proj1 p) (proj2 p) (case2 (init (ZChain.asupf zc) cs04 )) where - cs04 : supf0 px ≡ supf0 z1 - cs04 = begin - supf0 px ≡⟨ sym (sf1=sf0 o≤-refl) ⟩ - supf1 px ≡⟨ sym sfz=sfpx ⟩ - supf1 z1 ≡⟨ sf1=sf0 (o<→≤ a) ⟩ - supf0 z1 ∎ where open ≡-Reasoning - ... | case2 sfz<sfpx = ⊥-elim ( ¬p<x<op ⟪ cs05 , cs06 ⟫ ) where - --- supf1 z1 ≡ px , z1 o< px , px ≡ supf0 z1 o< supf0 px o< x - cs05 : px o< supf0 px - cs05 = subst₂ ( λ j k → j o< k ) sfz=px (sf1=sf0 o≤-refl ) sfz<sfpx - cs06 : supf0 px o< osuc px - cs06 = subst₂ (λ j k → j o< k ) (sym (proj1 p)) (sym opx=x) px<x - csupf2 | case2 (case2 p) | tri≈ ¬a b ¬c | record { eq = eq1 } = zc12 (proj1 p) (proj2 p) - (case2 (init (ZChain.asupf zc) (cong supf0 (sym b)))) - csupf2 | case2 (case2 p) | tri> ¬a ¬b px<z1 | record { eq = eq1 } = ⊥-elim ( ¬p<x<op ⟪ cs08 , cs09 ⟫ ) where - cs08 : px o< sp1 - cs08 = subst (λ k → k o< sp1 ) (proj1 p) (proj2 p ) - cs09 : sp1 o< osuc px - cs09 = subst ( λ k → sp1 o< k ) (sym (Oprev.oprev=x op)) sz1<x - csupf2 | case2 (case1 p) with trio< (supf0 px) sp1 -- ¬ (supf0 px o< sp1 -- sp1 o≤ supf px) - ... | tri< a ¬b ¬c = ⊥-elim (p a) - ... | tri≈ ¬a b ¬c = ? - ... | tri> ¬a ¬b c = ⊥-elim ( o≤> sfpx≤sp1 c ) - csupf2 | case1 p with trio< (supf0 px) px -- ¬ (supf0 px ≡ px ) - ... | tri< sf0px<px ¬b ¬c = ? where - cs10 : odef (UnionCF A f mf ay supf0 px) (supf0 px) - cs10 = ZChain.csupf zc sf0px<px - ... | tri≈ ¬a b ¬c = ⊥-elim (p b) - ... | tri> ¬a ¬b px<sf0px = ? where - cs11 : px o< z1 → odef (UnionCF A f mf ay supf1 x) (supf1 z1) - cs11 px<z1 = ⊥-elim ( ¬p<x<op ⟪ px<sf0px , subst₂ (λ j k → j o< k ) refl (sym (Oprev.oprev=x op)) - (ordtrans≤-< (subst (λ k → supf0 px o< k) (cong osuc (sym (sf1=sp1 px<z1 ))) sfpx≤sp1 ) sz1<x) ⟫ ) - cs12 : z1 o≤ px → odef (UnionCF A f mf ay supf1 x) (supf1 z1) - cs12 = ? + csupf1 : {z1 : Ordinal } → supf1 z1 o< supf1 x → odef (UnionCF A f mf ay supf1 x) (supf1 z1) + csupf1 {z1} sz<sx = ⟪ ? , ch-is-sup (supf1 z1) ? ? (init ? ? ) ⟫ zc41 | (case1 x<sp ) = record { supf = supf0 ; sup=u = ? ; asupf = ? ; supf-mono = ? ; supf-< = ? @@ -1594,15 +1400,11 @@ msp1 = msp0 (cf nmx) (cf-is-≤-monotonic nmx) as0 zc c : Ordinal c = MinSUP.sup msp1 - mc = c - mc<A : mc o< & A - mc<A = ∈∧P→o< ⟪ MinSUP.asm msp1 , lift true ⟫ - c=mc : c ≡ mc - c=mc = refl - z20 : mc << cf nmx mc - z20 = proj1 (cf-is-<-monotonic nmx mc (MinSUP.asm msp1) ) - asc : odef A (supf mc) + c<A : c o< & A + c<A = ∈∧P→o< ⟪ MinSUP.asm msp1 , lift true ⟫ + asc : odef A (supf c) asc = ZChain.asupf zc + spd : MinSUP A (uchain (cf nmx) (cf-is-≤-monotonic nmx) asc ) spd = ysup (cf nmx) (cf-is-≤-monotonic nmx) asc d = MinSUP.sup spd @@ -1636,152 +1438,14 @@ ... | case1 eq1 = case1 (cong (*) (trans (cong (cf nmx) (sym eq)) eq1) ) ... | case2 lt = case2 (subst (λ k → * k < * d1 ) (cong (cf nmx) eq) lt) - fsc<<d : {mc z : Ordinal } → (asc : odef A (supf mc)) → (spd : MinSUP A (uchain (cf nmx) (cf-is-≤-monotonic nmx) asc )) - → (fc : FClosure A (cf nmx) (supf mc) z) → z << MinSUP.sup spd - fsc<<d {mc} {z} asc spd fc = z25 where - d1 : Ordinal - d1 = MinSUP.sup spd -- supf d1 ≡ d - z24 : (z ≡ d1) ∨ ( z << d1 ) - z24 = MinSUP.x≤sup spd fc - -- - -- f ( f .. ( supf mc ) <= d1 - -- f d1 <= d1 - -- - z25 : z << d1 - z25 with z24 - ... | case2 lt = lt - ... | case1 eq = ⊥-elim ( <-irr z29 (proj1 (cf-is-<-monotonic nmx d1 (MinSUP.asm spd)) ) ) where - -- supf mc ≡ d1 - z32 : ((cf nmx z) ≡ d1) ∨ ( (cf nmx z) << d1 ) - z32 = MinSUP.x≤sup spd (fsuc _ fc) - z29 : (* (cf nmx d1) ≡ * d1) ∨ (* (cf nmx d1) < * d1) - z29 with z32 - ... | case1 eq1 = case1 (cong (*) (trans (cong (cf nmx) (sym eq)) eq1) ) - ... | case2 lt = case2 (subst (λ k → * k < * d1 ) (cong (cf nmx) eq) lt) - - smc<<d : supf mc << d - smc<<d = sc<<d asc spd - - sz<<c : {z : Ordinal } → z o< & A → supf z <= mc - sz<<c z<A = MinSUP.x≤sup msp1 (ZChain.csupf zc (z09 (ZChain.asupf zc) )) - - sc=c : supf mc ≡ mc - sc=c = ZChain.sup=u zc (MinSUP.asm msp1) (o<→≤ (∈∧P→o< ⟪ MinSUP.asm msp1 , lift true ⟫ )) ⟪ is-sup , not-hasprev ⟫ where - not-hasprev : ¬ HasPrev A (UnionCF A (cf nmx) (cf-is-≤-monotonic nmx) as0 (ZChain.supf zc) mc) (cf nmx) mc - not-hasprev record { ax = ax ; y = y ; ay = ⟪ ua1 , ch-init fc ⟫ ; x=fy = x=fy } = ⊥-elim ( <-irr z31 z30 ) where - z30 : * mc < * (cf nmx mc) - z30 = proj1 (cf-is-<-monotonic nmx mc (MinSUP.asm msp1)) - z31 : ( * (cf nmx mc) ≡ * mc ) ∨ ( * (cf nmx mc) < * mc ) - z31 = <=to≤ ( MinSUP.x≤sup msp1 (subst (λ k → odef (ZChain.chain zc) (cf nmx k)) (sym x=fy) - ⟪ proj2 (cf-is-≤-monotonic nmx _ (proj2 (cf-is-≤-monotonic nmx _ ua1 ) )) , ch-init (fsuc _ (fsuc _ fc)) ⟫ )) - not-hasprev record { ax = ax ; y = y ; ay = ⟪ ua1 , ch-is-sup u u<x is-sup1 fc ⟫; x=fy = x=fy } = ⊥-elim ( <-irr z48 z32 ) where - z30 : * mc < * (cf nmx mc) - z30 = proj1 (cf-is-<-monotonic nmx mc (MinSUP.asm msp1)) - z31 : ( supf mc ≡ mc ) ∨ ( * (supf mc) < * mc ) - z31 = MinSUP.x≤sup msp1 (ZChain.csupf zc (z09 (ZChain.asupf zc) )) - z32 : * (supf mc) < * (cf nmx (cf nmx y)) - z32 = ftrans<=-< z31 (subst (λ k → * mc < * k ) (cong (cf nmx) x=fy) z30 ) - z48 : ( * (cf nmx (cf nmx y)) ≡ * (supf mc)) ∨ (* (cf nmx (cf nmx y)) < * (supf mc) ) - z48 = <=to≤ (ZChain1.order (SZ1 (cf nmx) (cf-is-≤-monotonic nmx) as0 zc (& A)) mc<A u<x (fsuc _ ( fsuc _ fc ))) - is-sup : IsSUP A (UnionCF A (cf nmx) (cf-is-≤-monotonic nmx) as0 (ZChain.supf zc) mc) (MinSUP.asm msp1) - is-sup = record { x≤sup = λ zy → MinSUP.x≤sup msp1 (chain-mono (cf nmx) (cf-is-≤-monotonic nmx) as0 supf (ZChain.supf-mono zc) (o<→≤ mc<A) zy ) } - + z11 : odef (ZChain.chain zc) d + z11 = ZChain1.is-max (SZ1 (cf nmx) (cf-is-≤-monotonic nmx) as0 zc (& A)) {& s} ? ? ? ? ? where - not-hasprev : ¬ HasPrev A (UnionCF A (cf nmx) (cf-is-≤-monotonic nmx) as0 supf d) (cf nmx) d - not-hasprev record { ax = ax ; y = y ; ay = ⟪ ua1 , ch-init fc ⟫ ; x=fy = x=fy } = ⊥-elim ( <-irr z31 z30 ) where - z30 : * d < * (cf nmx d) - z30 = proj1 (cf-is-<-monotonic nmx d (MinSUP.asm spd)) - z32 : ( cf nmx (cf nmx y) ≡ supf mc ) ∨ ( * (cf nmx (cf nmx y)) < * (supf mc) ) - z32 = ZChain.fcy<sup zc (o<→≤ mc<A) (fsuc _ (fsuc _ fc)) - z31 : ( * (cf nmx d) ≡ * d ) ∨ ( * (cf nmx d) < * d ) - z31 = case2 ( subst (λ k → * (cf nmx k) < * d ) (sym x=fy) ( ftrans<=-< z32 ( sc<<d {mc} asc spd ) )) - not-hasprev record { ax = ax ; y = y ; ay = ⟪ ua1 , ch-is-sup u u<x is-sup1 fc ⟫; x=fy = x=fy } = ⊥-elim ( <-irr z46 z30 ) where - z45 : (* (cf nmx (cf nmx y)) ≡ * d) ∨ (* (cf nmx (cf nmx y)) < * d) → (* (cf nmx d) ≡ * d) ∨ (* (cf nmx d) < * d) - 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 (ZChain.supf-mono zc (o<→≤ d<A) ) - 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 z53 is-sup1 (init (ZChain.asupf zc) (ChainP.supu=u is-sup1)) ⟫ - z51 : supf u o≤ supf mc - z51 = or z52 (λ le → o≤-refl0 (z56 le) ) z57 where - z56 : u ≡ mc → supf u ≡ supf mc - z56 eq = cong supf eq - z57 : u << mc → supf u o≤ supf mc - z57 lt = ZChain.supf-<= zc (case2 z58) where - z58 : supf u << supf mc -- supf u o< supf d -- supf u << supf d - z58 = subst₂ ( λ j k → j << k ) (sym (ChainP.supu=u is-sup1)) (sym sc=c) lt - z49 : supf u o< supf mc → (cf nmx (cf nmx y) ≡ supf mc) ∨ (* (cf nmx (cf nmx y)) < * (supf mc) ) - z49 su<smc = ZChain1.order (SZ1 (cf nmx) (cf-is-≤-monotonic nmx) as0 zc (& A)) mc<A su<smc (fsuc _ ( fsuc _ fc )) - z50 : (cf nmx (cf nmx y) ≡ supf d) ∨ (* (cf nmx (cf nmx y)) < * (supf d) ) - z50 = ZChain1.order (SZ1 (cf nmx) (cf-is-≤-monotonic nmx) as0 zc (& A)) d<A u<x (fsuc _ ( fsuc _ fc )) - z47 : {mc d1 : Ordinal } {asc : odef A (supf mc)} (spd : MinSUP A (uchain (cf nmx) (cf-is-≤-monotonic nmx) asc )) - → (cf nmx (cf nmx y) ≡ supf mc) ∨ (* (cf nmx (cf nmx y)) < * (supf mc) ) → supf mc << d1 - → * (cf nmx (cf nmx y)) < * d1 - z47 {mc} {d1} {asc} spd (case1 eq) smc<d = subst (λ k → k < * d1 ) (sym (cong (*) eq)) smc<d - z47 {mc} {d1} {asc} spd (case2 lt) smc<d = IsStrictPartialOrder.trans PO lt smc<d - z30 : * d < * (cf nmx d) - z30 = proj1 (cf-is-<-monotonic nmx d (MinSUP.asm spd)) - z46 : (* (cf nmx d) ≡ * d) ∨ (* (cf nmx d) < * d) - z46 = or (osuc-≡< z51) z55 z54 where - z55 : supf u ≡ supf mc → (* (cf nmx d) ≡ * d) ∨ (* (cf nmx d) < * d) - z55 eq = <=to≤ (MinSUP.x≤sup spd ( subst₂ (λ j k → FClosure A (cf nmx) j (cf nmx k) ) eq (sym x=fy ) (fsuc _ (fsuc _ fc)) ) ) - z54 : supf u o< supf mc → (* (cf nmx d) ≡ * d) ∨ (* (cf nmx d) < * d) - z54 lt = z45 (case2 (z47 {mc} {d} {asc} spd (z49 lt) z48 )) - -- z46 with osuc-≡< z51 - -- ... | case1 eq = MinSUP.x≤sup spd ( subst₂ (λ j k → FClosure A (cf nmx) j k ) (trans (ChainP.supu=u is-sup1) eq) refl fc ) - -- ... | case2 lt = z45 (case2 (z47 {mc} {d} {asc} spd (z49 lt) z48 )) - - is-sup : IsSUP A (UnionCF A (cf nmx) (cf-is-≤-monotonic nmx) as0 (ZChain.supf zc) d) (MinSUP.asm spd) - is-sup = record { x≤sup = z22 } where - z23 : {z : Ordinal } → odef (uchain (cf nmx) (cf-is-≤-monotonic nmx) asc) z → (z ≡ MinSUP.sup spd) ∨ (z << MinSUP.sup spd) - z23 lt = MinSUP.x≤sup spd lt - z22 : {y : Ordinal} → odef (UnionCF A (cf nmx) (cf-is-≤-monotonic nmx) as0 (ZChain.supf zc) d) y → - (y ≡ MinSUP.sup spd) ∨ (y << MinSUP.sup spd) - z22 {a} ⟪ aa , ch-init fc ⟫ = case2 ( ( ftrans<=-< z32 ( sc<<d {mc} asc spd ) )) where - z32 : ( a ≡ supf mc ) ∨ ( * a < * (supf mc) ) - z32 = ZChain.fcy<sup zc (o<→≤ mc<A) fc - z22 {a} ⟪ aa , ch-is-sup u u<x is-sup1 fc ⟫ = tri u (supf mc) - z60 z61 ( λ sc<u → ⊥-elim ( o≤> ( subst (λ k → k o≤ supf mc) (ChainP.supu=u is-sup1) z51) sc<u )) where - z53 : supf u o< supf (& A) - z53 = ordtrans<-≤ u<x (ZChain.supf-mono zc (o<→≤ d<A) ) - 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 z53 is-sup1 (init (ZChain.asupf zc) (ChainP.supu=u is-sup1)) ⟫ - z56 : u ≡ mc → supf u ≡ supf mc - z56 eq = cong supf eq - z57 : u << mc → supf u o≤ supf mc - z57 lt = ZChain.supf-<= zc (case2 z58) where - z58 : supf u << supf mc -- supf u o< supf d -- supf u << supf d - z58 = subst₂ ( λ j k → j << k ) (sym (ChainP.supu=u is-sup1)) (sym sc=c) lt - z51 : supf u o≤ supf mc - z51 = or z52 (λ le → o≤-refl0 (z56 le) ) z57 - z60 : u o< supf mc → (a ≡ d ) ∨ ( * a < * d ) - z60 u<smc = case2 ( ftrans<=-< (ZChain1.order (SZ1 (cf nmx) (cf-is-≤-monotonic nmx) as0 zc (& A)) mc<A - (subst (λ k → k o< supf mc) (sym (ChainP.supu=u is-sup1)) u<smc) fc ) smc<<d ) - z61 : u ≡ supf mc → (a ≡ d ) ∨ ( * a < * d ) - z61 u=sc = case2 (fsc<<d {mc} asc spd (subst (λ k → FClosure A (cf nmx) k a) (trans (ChainP.supu=u is-sup1) u=sc) fc ) ) - -- u<x : ZChain.supf zc u o< ZChain.supf zc d - -- supf u o< supf c → order - - sd=d : supf d ≡ d - sd=d = ZChain.sup=u zc (MinSUP.asm spd) (o<→≤ d<A) ⟪ is-sup , not-hasprev ⟫ - - sc<sd : {mc d : Ordinal } → supf mc << supf d → supf mc o< supf d - sc<sd {mc} {d} sc<<sd with osuc-≡< ( ZChain.supf-<= zc (case2 sc<<sd ) ) - ... | case1 eq = ⊥-elim ( <-irr (case1 (cong (*) (sym eq) )) sc<<sd ) - ... | case2 lt = lt - - sms<sa : supf mc o< supf (& A) - sms<sa with osuc-≡< ( ZChain.supf-mono zc (o<→≤ ( ∈∧P→o< ⟪ MinSUP.asm msp1 , lift true ⟫) )) - ... | case2 lt = lt - ... | case1 eq = ⊥-elim ( o<¬≡ eq ( ordtrans<-≤ (sc<sd (subst (λ k → supf mc << k ) (sym sd=d) (sc<<d {mc} asc spd)) ) - ( ZChain.supf-mono zc (o<→≤ d<A )))) + z10 : supf d o≤ supf (& A) + z10 = ? ss<sa : supf c o< supf (& A) - ss<sa = subst (λ k → supf k o< supf (& A)) (sym c=mc) sms<sa + ss<sa = ? zorn00 : Maximal A zorn00 with is-o∅ ( & HasMaximal ) -- we have no Level (suc n) LEM