Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 965:1c1c6a6ed4fa
removing ch-init is no good because of initialization
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sat, 05 Nov 2022 10:23:57 +0900 |
| parents | 0bee632db679 |
| children | 39c680188738 |
| files | src/zorn.agda |
| diffstat | 1 files changed, 18 insertions(+), 84 deletions(-) [+] |
line wrap: on
line diff
--- a/src/zorn.agda Fri Nov 04 20:48:00 2022 +0900 +++ b/src/zorn.agda Sat Nov 05 10:23:57 2022 +0900 @@ -272,7 +272,6 @@ data UChain ( A : HOD ) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f) {y : Ordinal } (ay : odef A y ) (supf : Ordinal → Ordinal) (x : Ordinal) : (z : Ordinal) → Set n where - ch-init : {z : Ordinal } (fc : FClosure A f y z) → UChain A f mf ay supf x z ch-is-sup : (u : Ordinal) {z : Ordinal } (u<x : supf u o< supf x) ( is-sup : ChainP A f mf ay supf u ) ( fc : FClosure A f (supf u) z ) → UChain A f mf ay supf x z @@ -288,37 +287,6 @@ {s s1 a b : Ordinal } ( ca : UChain A f mf ay supf s a ) ( cb : UChain A f mf ay supf s1 b ) → Tri (* a < * b) (* a ≡ * b) (* b < * a ) chain-total A f mf {y} ay supf {xa} {xb} {a} {b} ca cb = ct-ind xa xb ca cb where ct-ind : (xa xb : Ordinal) → {a b : Ordinal} → UChain A f mf ay supf xa a → UChain A f mf ay supf xb b → Tri (* a < * b) (* a ≡ * b) (* b < * a) - ct-ind xa xb {a} {b} (ch-init fca) (ch-init fcb) = fcn-cmp y f mf fca fcb - ct-ind xa xb {a} {b} (ch-init fca) (ch-is-sup ub u<x supb fcb) with ChainP.fcy<sup supb fca - ... | case1 eq with s≤fc (supf ub) f mf fcb - ... | case1 eq1 = tri≈ (λ lt → ⊥-elim (<-irr (case1 (sym ct00)) lt)) ct00 (λ lt → ⊥-elim (<-irr (case1 ct00) lt)) where - ct00 : * a ≡ * b - ct00 = trans (cong (*) eq) eq1 - ... | case2 lt = tri< ct01 (λ eq → <-irr (case1 (sym eq)) ct01) (λ lt → <-irr (case2 ct01) lt) where - ct01 : * a < * b - ct01 = subst (λ k → * k < * b ) (sym eq) lt - ct-ind xa xb {a} {b} (ch-init fca) (ch-is-sup ub u<x supb fcb) | case2 lt = tri< ct01 (λ eq → <-irr (case1 (sym eq)) ct01) (λ lt → <-irr (case2 ct01) lt) where - ct00 : * a < * (supf ub) - ct00 = lt - ct01 : * a < * b - ct01 with s≤fc (supf ub) f mf fcb - ... | case1 eq = subst (λ k → * a < k ) eq ct00 - ... | case2 lt = IsStrictPartialOrder.trans POO ct00 lt - ct-ind xa xb {a} {b} (ch-is-sup ua u<x supa fca) (ch-init fcb) with ChainP.fcy<sup supa fcb - ... | case1 eq with s≤fc (supf ua) f mf fca - ... | case1 eq1 = tri≈ (λ lt → ⊥-elim (<-irr (case1 (sym ct00)) lt)) ct00 (λ lt → ⊥-elim (<-irr (case1 ct00) lt)) where - ct00 : * a ≡ * b - ct00 = sym (trans (cong (*) eq) eq1 ) - ... | case2 lt = tri> (λ lt → <-irr (case2 ct01) lt) (λ eq → <-irr (case1 eq) ct01) ct01 where - ct01 : * b < * a - ct01 = subst (λ k → * k < * a ) (sym eq) lt - ct-ind xa xb {a} {b} (ch-is-sup ua u<x supa fca) (ch-init fcb) | case2 lt = tri> (λ lt → <-irr (case2 ct01) lt) (λ eq → <-irr (case1 eq) ct01) ct01 where - ct00 : * b < * (supf ua) - ct00 = lt - ct01 : * b < * a - ct01 with s≤fc (supf ua) f mf fca - ... | case1 eq = subst (λ k → * b < k ) eq ct00 - ... | case2 lt = IsStrictPartialOrder.trans POO ct00 lt ct-ind xa xb {a} {b} (ch-is-sup ua ua<x supa fca) (ch-is-sup ub ub<x supb fcb) with trio< ua ub ... | tri< a₁ ¬b ¬c with ChainP.order supb (subst₂ (λ j k → j o< k ) (sym (ChainP.supu=u supa )) (sym (ChainP.supu=u supb )) a₁) fca ... | case1 eq with s≤fc (supf ub) f mf fcb @@ -399,8 +367,6 @@ chain-mono : {A : HOD} ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) {y : Ordinal} (ay : odef A y) (supf : Ordinal → Ordinal ) (supf-mono : {x y : Ordinal } → x o≤ y → supf x o≤ supf y ) {a b c : Ordinal} → a o≤ b → 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 (supf-mono a≤b ) ) is-sup fc ⟫ @@ -415,6 +381,7 @@ supf-mono : {x y : Ordinal } → x o≤ y → supf x o≤ supf y supf-< : {x y : Ordinal } → supf x o< supf y → supf x << supf y supfmax : {x : Ordinal } → z o< x → supf x ≡ supf z + chain∋init : odef (UnionCF A f mf ay supf z) y 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 ) @@ -431,14 +398,10 @@ s=ms : {x : Ordinal } → (x≤z : x o≤ z ) → & (SUP.sup (sup x≤z)) ≡ MinSUP.sup (minsup x≤z) s=ms {x} x≤z = &iso - chain∋init : odef chain y - chain∋init = ⟪ ay , ch-init (init ay refl) ⟫ f-next : {a z : Ordinal} → odef (UnionCF A f mf ay supf z) a → odef (UnionCF A f mf ay supf z) (f a) - f-next {a} ⟪ aa , ch-init fc ⟫ = ⟪ proj2 (mf a aa) , ch-init (fsuc _ fc) ⟫ f-next {a} ⟪ aa , ch-is-sup u u<x is-sup fc ⟫ = ⟪ proj2 (mf a aa) , ch-is-sup u u<x is-sup (fsuc _ fc ) ⟫ initial : {z : Ordinal } → odef chain z → * y ≤ * z initial {a} ⟪ aa , ua ⟫ with ua - ... | ch-init fc = s≤fc y f mf fc ... | ch-is-sup u u<x is-sup fc = ≤-ftrans (<=to≤ zc7) (s≤fc _ f mf fc) where zc7 : y <= supf u zc7 = ChainP.fcy<sup is-sup (init ay refl) @@ -463,10 +426,13 @@ ... | case2 lt = ⊥-elim ( o<> sx<sy lt ) fcy<sup : {u w : Ordinal } → u o≤ z → FClosure A f y w → (w ≡ supf u ) ∨ ( w << supf u ) -- different from order because y o< supf - fcy<sup {u} {w} u≤z fc with MinSUP.x≤sup (minsup u≤z) ⟪ subst (λ k → odef A k ) (sym &iso) (A∋fc {A} y f mf fc) - , ch-init (subst (λ k → FClosure A f y k) (sym &iso) fc ) ⟫ - ... | case1 eq = case1 (subst (λ k → k ≡ supf u ) &iso (trans eq (sym (supf-is-minsup u≤z ) ) )) - ... | case2 lt = case2 (subst₂ (λ j k → j << k ) &iso (sym (supf-is-minsup u≤z )) lt ) + fcy<sup {u} {w} u≤z fc with chain∋init + ... | ⟪ ay1 , ch-is-sup uy uy<x is-sup fcy ⟫ = <=-trans (ChainP.fcy<sup is-sup fc) ? + + -- with MinSUP.x≤sup (minsup u≤z) ⟪ subst (λ k → odef A k ) (sym &iso) (A∋fc {A} y f mf fc) + -- , ? ⟫ --ch-init (subst (λ k → FClosure A f y k) (sym &iso) fc ) ⟫ + -- ... | case1 eq = case1 (subst (λ k → k ≡ supf u ) &iso (trans eq (sym (supf-is-minsup u≤z ) ) )) + -- ... | case2 lt = case2 (subst₂ (λ j k → j << k ) &iso (sym (supf-is-minsup u≤z )) lt ) -- ordering is not proved here but in ZChain1 @@ -498,10 +464,6 @@ as : A ∋ maximal ¬maximal<x : {x : HOD} → A ∋ x → ¬ maximal < x -- A is Partial, use negative -init-uchain : (A : HOD) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f) {y : Ordinal } → (ay : odef A y ) - { supf : Ordinal → Ordinal } { x : Ordinal } → odef (UnionCF A f mf ay supf x) y -init-uchain A f mf ay = ⟪ ay , ch-init (init ay refl) ⟫ - Zorn-lemma : { A : HOD } → o∅ o< & A → ( ( B : HOD) → (B⊆A : B ⊆' A) → IsTotalOrderSet B → SUP A B ) -- SUP condition @@ -616,7 +578,6 @@ → HasPrev A (UnionCF A f mf ay (ZChain.supf zc) x) f b → * a < * b → odef (UnionCF A f mf ay (ZChain.supf zc) x) b is-max-hp x {a} {b} ua ab has-prev a<b with HasPrev.ay has-prev - ... | ⟪ ab0 , ch-init fc ⟫ = ⟪ ab , ch-init ( subst (λ k → FClosure A f y k) (sym (HasPrev.x=fy has-prev)) (fsuc _ fc )) ⟫ ... | ⟪ ab0 , ch-is-sup u u<x is-sup fc ⟫ = ⟪ ab , subst (λ k → UChain A f mf ay (ZChain.supf zc) x k ) (sym (HasPrev.x=fy has-prev)) ( ch-is-sup u u<x is-sup (fsuc _ fc)) ⟫ @@ -632,7 +593,6 @@ 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 ⟫ ... | ⟪ as , ch-is-sup u u<x is-sup fc ⟫ = ⟪ as , ch-is-sup u zc08 is-sup fc ⟫ where zc07 : FClosure A f (supf u) (supf s) -- supf u ≤ supf s → supf u o≤ supf s zc07 = fc @@ -643,7 +603,6 @@ csupf-fc {b} {s} {z1} b<z ss≤sb (fsuc x fc) = subst (λ k → odef (UnionCF A f mf ay supf b) k ) (sym &iso) zc04 where zc04 : odef (UnionCF A f mf ay supf b) (f x) zc04 with subst (λ k → odef (UnionCF A f mf ay supf b) k ) &iso (csupf-fc b<z ss≤sb fc ) - ... | ⟪ as , ch-init fc ⟫ = ⟪ proj2 (mf _ as) , ch-init (fsuc _ fc) ⟫ ... | ⟪ as , ch-is-sup u u<x is-sup fc ⟫ = ⟪ proj2 (mf _ as) , ch-is-sup u u<x is-sup (fsuc _ fc) ⟫ order : {b s z1 : Ordinal} → b o< & A → supf s o< supf b → FClosure A f (supf s) z1 → (z1 ≡ supf b) ∨ (z1 << supf b) order {b} {s} {z1} b<z ss<sb fc = zc04 where @@ -692,9 +651,8 @@ * a < * b → odef (UnionCF A f mf ay supf x) b is-max {a} {b} ua sb<sx ab P a<b with ODC.or-exclude O P 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 sb<sx m06 (subst (λ k → FClosure A f k b) (sym m05) (init ab refl)) ⟫ where + is-max {a} {b} ua sb<sx ab P a<b | case2 is-sup + = ⟪ ab , ch-is-sup b sb<sx 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 @@ -727,6 +685,12 @@ → MinSUP A (uchain f mf ay) ysup f mf {y} ay = minsupP (uchain f mf ay) (λ lt → A∋fc y f mf lt) (utotal f mf ay) + UChainPreserve : {x z : Ordinal } { f : Ordinal → Ordinal } → {mf : ≤-monotonic-f A f } {y : Ordinal} {ay : odef A y} + → { supf0 supf1 : Ordinal → Ordinal } + → ( ( z : Ordinal ) → z o< x → supf0 z ≡ supf1 z) + → UnionCF A f mf ay supf0 x ≡ UnionCF A f mf ay supf1 x + UChainPreserve {x} {f} {mf} {y} {ay} {supf0} {supf1} <x→eq = ? + SUP⊆ : { B C : HOD } → B ⊆' C → SUP A C → SUP A B SUP⊆ {B} {C} B⊆C sup = record { sup = SUP.sup sup ; as = SUP.as sup ; x≤sup = λ lt → SUP.x≤sup sup (B⊆C lt) } @@ -888,7 +852,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 @@ -896,7 +859,6 @@ 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 @@ -917,7 +879,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 ⟫ ) zc12 : {z : Ordinal} → odef pchainpx z → odef (UnionCF A f mf ay supf1 x) z - zc12 {z} (case1 ⟪ az , ch-init fc ⟫ ) = ⟪ az , ch-init fc ⟫ zc12 {z} (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 @@ -929,7 +890,6 @@ 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 @@ -966,11 +926,11 @@ s≤px = o<→≤ (supf-inject0 supf1-mono ss<spx) ... | tri> ¬a ¬b c | _ = ⊥-elim ( ¬p<x<op ⟪ c , u≤px ⟫ ) zc12 {z} (case2 fc) = zc21 fc where + --- supf0 px o< sp1 zc20 : (supf0 px ≡ px ) ∨ ( supf0 px o< px ) zc20 = ? 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 ) with zc20 ... | case1 sfpx=px = ⟪ asp , ch-is-sup px zc18 @@ -1000,7 +960,6 @@ csupf17 (fsuc x fc) = ZChain.f-next zc (csupf17 fc) ... | case2 sfp<px with ZChain.csupf zc sfp<px -- odef (UnionCF A f mf ay supf0 px) (supf0 px) - ... | ⟪ ua1 , ch-init fc₁ ⟫ = ⟪ ua1 , ch-init fc₁ ⟫ ... | ⟪ ua1 , ch-is-sup u u<x is-sup fc₁ ⟫ = ⟪ ua1 , ch-is-sup u zc18 record { fcy<sup = z10 ; order = z11 ; supu=u = z12 } (fcpu fc₁ ? ) ⟫ where z10 : {z : Ordinal } → FClosure A f y z → (z ≡ supf1 u) ∨ ( z << supf1 u ) @@ -1125,16 +1084,13 @@ pchain1 = UnionCF A f mf ay supf1 x zc10 : {z : Ordinal} → OD.def (od pchain) z → OD.def (od pchain1) z - zc10 {z} ⟪ az , ch-init fc ⟫ = ⟪ az , ch-init fc ⟫ zc10 {z} ⟪ az , ch-is-sup u1 u1<x u1-is-sup fc ⟫ = ⟪ az , ch-is-sup u1 ? ? ? ⟫ zc111 : {z : Ordinal} → z o< px → OD.def (od pchain1) z → OD.def (od pchain) z - zc111 {z} z<px ⟪ az , ch-init fc ⟫ = ⟪ az , ch-init fc ⟫ zc111 {z} z<px ⟪ az , ch-is-sup u1 u1<x u1-is-sup fc ⟫ = ⟪ az , ch-is-sup u1 ? ? ? ⟫ zc11 : (¬ xSUP (UnionCF A f mf ay supf0 px) f x ) ∨ (HasPrev A pchain f x ) → {z : Ordinal} → OD.def (od pchain1) z → OD.def (od pchain) z ∨ ( (supf0 px ≡ px) ∧ FClosure A f px z ) - zc11 P {z} ⟪ az , ch-init fc ⟫ = case1 ⟪ az , ch-init fc ⟫ zc11 P {z} ⟪ az , ch-is-sup u1 u1<x u1-is-sup fc ⟫ with trio< u1 px ... | tri< u1<px ¬b ¬c = case1 ⟪ az , ch-is-sup u1 ? ? fc ⟫ ... | tri≈ ¬a eq ¬c = case2 ⟪ subst (λ k → supf0 k ≡ k) eq s1u=u , subst (λ k → FClosure A f k z) zc12 ? ⟫ where @@ -1153,7 +1109,6 @@ zc13 : osuc px o< osuc u1 zc13 = o≤-refl0 ( trans (Oprev.oprev=x op) (sym eq ) ) x≤sup : {w : Ordinal} → odef (UnionCF A f mf ay supf0 px) w → (w ≡ x) ∨ (w << x) - x≤sup {w} ⟪ az , ch-init {w} fc ⟫ = subst (λ k → (w ≡ k) ∨ (w << k)) s1u=x ? x≤sup {w} ⟪ az , ch-is-sup u u<x is-sup fc ⟫ with osuc-≡< ( supf-mono (ordtrans (o<→≤ u<x) ? )) ... | case1 eq1 = ⊥-elim ( o<¬≡ zc14 ? ) where zc14 : u ≡ osuc px @@ -1277,7 +1232,6 @@ HasPrev A (UnionCF A f mf ay supf x) f b → * a < * b → odef (UnionCF A f mf ay supf x) b is-max-hp supf x {a} {b} ua b<x ab has-prev a<b with HasPrev.ay has-prev - ... | ⟪ ab0 , ch-init fc ⟫ = ⟪ ab , ch-init ( subst (λ k → FClosure A f y k) (sym (HasPrev.x=fy has-prev)) (fsuc _ fc )) ⟫ ... | ⟪ ab0 , ch-is-sup u u<x is-sup fc ⟫ = ? -- ⟪ ab , -- subst (λ k → UChain A f mf ay supf x k ) -- (sym (HasPrev.x=fy has-prev)) ( ch-is-sup u u<x is-sup (fsuc _ fc)) ⟫ @@ -1293,19 +1247,15 @@ pchain0=1 : pchain ≡ pchain1 pchain0=1 = ==→o≡ record { eq→ = zc10 ; eq← = zc11 } where zc10 : {z : Ordinal} → OD.def (od pchain) z → OD.def (od pchain1) z - zc10 {z} ⟪ az , ch-init fc ⟫ = ⟪ az , ch-init fc ⟫ zc10 {z} ⟪ az , ch-is-sup u u<x is-sup fc ⟫ = zc12 fc where zc12 : {z : Ordinal} → FClosure A f (supf0 u) z → odef pchain1 z zc12 (fsuc x fc) with zc12 fc - ... | ⟪ ua1 , ch-init fc₁ ⟫ = ⟪ proj2 ( mf _ ua1) , ch-init (fsuc _ fc₁) ⟫ ... | ⟪ ua1 , ch-is-sup u u<x is-sup fc₁ ⟫ = ⟪ proj2 ( mf _ ua1) , ch-is-sup u u<x is-sup (fsuc _ fc₁) ⟫ zc12 (init asu su=z ) = ⟪ subst (λ k → odef A k) su=z asu , ch-is-sup u ? ? (init ? ? ) ⟫ zc11 : {z : Ordinal} → OD.def (od pchain1) z → OD.def (od pchain) z - zc11 {z} ⟪ az , ch-init fc ⟫ = ⟪ az , ch-init fc ⟫ zc11 {z} ⟪ az , ch-is-sup u u<x is-sup fc ⟫ = zc13 fc where zc13 : {z : Ordinal} → FClosure A f (supf1 u) z → odef pchain z zc13 (fsuc x fc) with zc13 fc - ... | ⟪ ua1 , ch-init fc₁ ⟫ = ⟪ proj2 ( mf _ ua1) , ch-init (fsuc _ fc₁) ⟫ ... | ⟪ ua1 , ch-is-sup u u<x is-sup fc₁ ⟫ = ⟪ proj2 ( mf _ ua1) , ch-is-sup u u<x is-sup (fsuc _ fc₁) ⟫ zc13 (init asu su=z ) with trio< u x ... | tri< a ¬b ¬c = ⟪ ? , ch-is-sup u ? ? (init ? ? ) ⟫ @@ -1419,7 +1369,7 @@ z04 : (nmx : ¬ Maximal A ) → (zc : ZChain A (cf nmx) (cf-is-≤-monotonic nmx) as0 (& A)) → ⊥ z04 nmx zc = <-irr0 {* (cf nmx c)} {* c} (subst (λ k → odef A k ) (sym &iso) (proj1 (is-cf nmx (MinSUP.asm msp1 )))) - (subst (λ k → odef A k) ? (MinSUP.asm msp1) ) + (subst (λ k → odef A k) (sym &iso) (MinSUP.asm msp1) ) (case1 ( cong (*)( fixpoint (cf nmx) (cf-is-≤-monotonic nmx ) zc msp1 ss<sa ))) -- x ≡ f x ̄ (proj1 (cf-is-<-monotonic nmx c (MinSUP.asm msp1 ))) where -- x < f x @@ -1502,12 +1452,6 @@ 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)) @@ -1522,13 +1466,6 @@ 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 @@ -1574,9 +1511,6 @@ 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)