Members/kono/Proof/ZF-in-agda: src/zorn.agda comparison

comparison src/zorn.agda @ 1042:912ca4abe806

pxhainx conditon is requied?

author	Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date	Sun, 04 Dec 2022 09:15:12 +0900
parents	f12a9b4066a0
children	fd26e0c4e648

comparison

equal deleted inserted replaced

-:f12a9b4066a0
+:912ca4abe806
 open import Relation.Nullary
 open import Data.Empty
 import BAlgbra
 open import Data.Nat hiding ( _<_ ; _≤_ )
 open import Data.Nat.Properties
 open import nat
 open inOrdinal O
 open OD O
 ftrans≤-< {x} {y} {z} (case1 eq) y<z = subst (λ k → k < * z) (sym (cong (*) eq))  y<z
 ftrans≤-< {x} {y} {z} (case2 lt) y<z = IsStrictPartialOrder.trans PO lt y<z
 ftrans<-≤ : {x y z : Ordinal } →  x <<  y →  y ≤ z →  x <<  z
 ftrans<-≤ {x} {y} {z} x<y (case1 eq) = subst (λ k → * x < k ) ((cong (*) eq)) x<y
 ftrans<-≤ {x} {y} {z} x<y (case2 lt) = IsStrictPartialOrder.trans PO x<y lt
 <-irr : {a b : HOD} → (a ≡ b ) ∨ (a < b ) → b < a → ⊥
 <-irr {a} {b} (case1 a=b) b<a = IsStrictPartialOrder.irrefl PO   (sym a=b) b<a
 <-irr {a} {b} (case2 a<b) b<a = IsStrictPartialOrder.irrefl PO   refl
 (IsStrictPartialOrder.trans PO     b<a a<b)
 fc04 = fc00 i j (cong pred i=j) cx1 cy (cong pred i=x1) (cong pred j=y)
 ... | case2 x<fx | case1 y=fy = subst (λ k → * (f x) ≡ * k ) y=fy (fc03 y cy j=y) where
 fc03 : (y1 : Ordinal) → (cy1 : FClosure A f s y1 ) →  suc j ≡ fcn s mf cy1 → * (f x)  ≡ * y1
 fc03 y1 (init x₁ x₂) x = ⊥-elim (fc06 x₂ x)
 fc03 .(f y1) (fsuc y1 cy1) j=y1 with proj1 (mf y1 (A∋fc s f mf cy1 ) )
 ... | case1 eq = trans ( fc03  y1 cy1 j=y1 ) (cong (*) eq)
 ... | case2 lt = subst₂ (λ j k → * (f j) ≡ * (f k )) &iso &iso ( cong (λ k → * ( f (& k ))) fc05) where
 fc05 : * x ≡ * y1
 fc05 = fc00 i j (cong pred i=j) cx cy1 (cong pred i=x) (cong pred j=y1)
 ... | case2 x₁ | case2 x₂ = subst₂ (λ j k → * (f j) ≡ * (f k) ) &iso &iso (cong (λ k → * (f (& k))) (fc00 i j (cong pred i=j) cx cy (cong pred i=x) (cong pred j=y)))
 --
 --    if sup z1 ≡ sup z2, the chain is stopped at sup z1, then f (sup z1) ≡ sup z1
 --    this means sup z1 is the Maximal, so f is <-monotonic if we have no Maximal.
 --
 fc-stop : ( A : HOD )    ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f) { a b : Ordinal }
 → (aa : odef A a ) →(  {y : Ordinal} → FClosure A f a y → (y ≡ b ) ∨ (y << b )) → a ≡ b → f a ≡ a
 fc-stop A f mf {a} {b} aa x≤sup a=b with x≤sup (fsuc a (init aa refl ))
 ... | case1 eq = trans eq (sym a=b)
 ... | case2 lt = ⊥-elim (<-irr (case1 (cong (λ k → * (f k) ) (sym a=b))) (ftrans<-≤ lt fc00 ) ) where
 fc00 :   b ≤  (f b)
 fc00 = proj1 (mf _ (subst (λ k → odef A k) a=b aa ))
 ∈∧P→o< :  {A : HOD } {y : Ordinal} → {P : Set n} → odef A y ∧ P → y o< & A
 ∈∧P→o< {A } {y} p = subst (λ k → k o< & A) &iso ( c<→o< (subst (λ k → odef A k ) (sym &iso ) (proj1 p )))
 -- Union of supf z and FClosure A f y
 data UChain  { A : HOD } { f : Ordinal → Ordinal }  {supf : Ordinal → Ordinal} {y : Ordinal } (ay : odef A y )
 (x : Ordinal) : (z : Ordinal) → Set n where
 ch-init : {z : Ordinal } (fc : FClosure A f y z) → UChain ay x z
 ch-is-sup  : (u : Ordinal) {z : Ordinal }  (u<x : u o< x) (supu=u : supf u ≡ u) ( fc : FClosure A f (supf u) z ) → UChain ay x z
 UnionCF : ( A : HOD )    ( f : Ordinal → Ordinal ) {y : Ordinal } (ay : odef A y ) ( supf : Ordinal → Ordinal ) ( x : Ordinal ) → HOD
 UnionCF A f ay supf x
 = record { od = record { def = λ z → odef A z ∧ UChain {A} {f} {supf} ay x z } ;
 odmax = & A ; <odmax = λ {y} sy → ∈∧P→o< sy }
 supf-inject0 : {x y : Ordinal } {supf : Ordinal → Ordinal } → (supf-mono : {x y : Ordinal } →  x o≤  y  → supf x o≤ supf y )
 → supf x o< supf y → x o<  y
 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 ay supf a) c → odef (UnionCF A f 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 ⟪ ua , ch-is-sup u u<x supu=u fc ⟫ = ⟪ ua , ch-is-sup u (ordtrans<-≤ u<x a≤b) supu=u 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
 field
 supf :  Ordinal → Ordinal
 asupf :  {x : Ordinal } → odef A (supf x)
 supf-mono : {x y : Ordinal } → x o≤  y → supf x o≤ supf y
 supfmax : {x : Ordinal } → z o< x → supf x ≡ supf z
 is-minsup : {x : Ordinal } → (x≤z : x o≤ z) → IsMinSUP A (UnionCF A f ay supf x) (supf x)
 sup=u : {b : Ordinal} → (ab : odef A b) → b o≤ z
 → IsSUP A (UnionCF A f ay supf b) b ∧ (¬ HasPrev A (UnionCF A f ay supf b) f b ) → supf b ≡ b
 chain : HOD
 chain = UnionCF A f ay supf z
 chain⊆A = λ lt → proj1 lt
 chain∋init : {x : Ordinal } → x o≤ z → odef (UnionCF A f ay supf x) y
 chain∋init {x} x≤z = ⟪ ay , ch-init (init ay refl)  ⟫
 mf : ≤-monotonic-f A f
 mf x ax = ⟪ case2 mf00 , proj2 (mf< x ax ) ⟫ where
 mf00 : * x < * (f x)
 mf00 = proj1 ( mf< x ax )
 f-next : {a z : Ordinal} → odef (UnionCF A f ay supf z) a → odef (UnionCF A f ay supf z) (f a)
 f-next {a} ⟪ ua , ch-init fc ⟫ = ⟪ proj2 ( mf _ ua)  , ch-init (fsuc _ fc) ⟫
 f-next {a} ⟪ ua , ch-is-sup u su<x su=u fc ⟫ = ⟪ proj2 ( mf _ ua)  , ch-is-sup u su<x su=u (fsuc _ fc) ⟫
 supf-inject : {x y : Ordinal } → supf x o< supf y → x o<  y
 supf-inject {x} {y} sx<sy with trio< x y
 ... | tri< a ¬b ¬c = a
 ... | tri≈ ¬a refl ¬c = ⊥-elim ( o<¬≡ (cong supf refl) sx<sy )
 supf-is-minsup : {x : Ordinal } → (x≤z : x o≤ z) → supf x ≡ MinSUP.sup (minsup x≤z)
 supf-is-minsup _ = refl
 -- different from order because y o< supf
 fcy<sup  : {u w : Ordinal } → u o≤ z  → FClosure A f y w → (w ≡ supf u ) ∨ ( w << supf u )
 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 )
 initial : {x : Ordinal } → x o≤ z → odef (UnionCF A f ay supf x) x →  y ≤ x
 initial {x} x≤z ⟪ aa , ch-init fc ⟫ = s≤fc y f mf fc
 initial {x} x≤z ⟪ aa , ch-is-sup u u<x is-sup fc ⟫ = ≤-ftrans (fcy<sup (ordtrans u<x x≤z) (init ay refl)) (s≤fc _ f mf fc)
 f-total : IsTotalOrderSet chain
 f-total {a} {b} ⟪ uaa , ch-is-sup ua sua<x sua=ua fca ⟫ ⟪ uab , ch-is-sup ub sub<x sub=ub fcb ⟫ =
 subst₂ (λ j k → Tri (j < k) (j ≡ k) (k < j)) *iso *iso fc-total where
 fc-total : Tri (* (& a) < * (& b)) (* (& a) ≡ * (& b)) (* (& b) < * (& a) )
 fc-total with trio< ua ub
 ... | tri< a₁ ¬b ¬c with ≤-ftrans  (order (o<→≤ sub<x) a₁ fca ) (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 = cong (*) eq1
 ... | case2 a<b =  tri< a<b (λ eq → <-irr (case1 (sym eq)) a<b ) (λ lt → <-irr (case2 a<b ) lt)
 fc-total | tri≈ _ refl _ = fcn-cmp _ f mf fca fcb
 fc-total | tri> ¬a ¬b c with ≤-ftrans  (order (o<→≤ sua<x) c fcb ) (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 = cong (*) (sym eq1)
 ... | case2 b<a =  tri> (λ lt → <-irr (case2 b<a ) lt)  (λ eq → <-irr (case1 eq) b<a )  b<a
 f-total {a} {b} ⟪ uaa , ch-init fca ⟫ ⟪ uab , ch-is-sup ub sub<x sub=ub fcb ⟫ = ft00 where
 ft01 : (& a) ≤ (& b) → Tri ( a <  b) ( a ≡  b) ( b <  a )
 ft01 (case1 eq) = tri≈ (λ lt → ⊥-elim (<-irr (case1 (sym a=b)) lt)) a=b  (λ lt → ⊥-elim (<-irr (case1 a=b) lt))  where
 a=b : a ≡ b
 a=b = subst₂ (λ j k → j ≡ k ) *iso *iso (cong (*) eq)
 ft01 (case2 lt) = tri< a<b (λ eq → <-irr (case1 (sym eq)) a<b ) (λ lt → <-irr (case2 a<b ) lt)  where
 a<b : a < b
 a<b = subst₂ (λ j k → j < k ) *iso *iso lt
 ft00 :   Tri ( a <  b) ( a ≡  b) ( b <  a )
 ft00 = ft01 (≤-ftrans (fcy<sup (o<→≤ sub<x) fca) (s≤fc {A} _ f mf fcb))
 f-total {a} {b} ⟪ uaa , ch-is-sup ua sua<x sua=ua fca ⟫ ⟪ uab , ch-init fcb ⟫ = ft00 where
 ft01 : (& b) ≤ (& a) → Tri ( a <  b) ( a ≡  b) ( b <  a )
 ft01 (case1 eq) = tri≈ (λ lt → ⊥-elim (<-irr (case1 (sym a=b)) lt)) a=b  (λ lt → ⊥-elim (<-irr (case1 a=b) lt))  where
 a=b : a ≡ b
 a=b = subst₂ (λ j k → j ≡ k ) *iso *iso (cong (*) (sym eq))
 ft01 (case2 lt) = tri> (λ lt → <-irr (case2 b<a ) lt) (λ eq → <-irr (case1 eq) b<a ) b<a where
 b<a : b < a
 b<a = subst₂ (λ j k → j < k ) *iso *iso lt
 ft00 :   Tri ( a <  b) ( a ≡  b) ( b <  a )
 ft00 = ft01 (≤-ftrans (fcy<sup (o<→≤ sua<x) fcb) (s≤fc {A} _ f mf fca))
 f-total {a} {b} ⟪ uaa , ch-init fca ⟫ ⟪ uab , ch-init fcb ⟫ =
 subst₂ (λ j k → Tri (j < k) (j ≡ k) (k < j)) *iso *iso  (fcn-cmp y f mf fca fcb )
 IsMinSUP→NotHasPrev : {x sp : Ordinal } → odef A sp
 → ({y : Ordinal} → odef (UnionCF A f ay supf x) y → (y ≡ sp ) ∨ (y << sp ))
 → ( {a : Ordinal } → odef A a → a << f a )
 im00 : f (f pr) ≤ sp
 im00 = is-sup ( f-next (f-next (HasPrev.ay hp)))
 fsp≤sp : f sp ≤  sp
 fsp≤sp = subst (λ k → f k ≤ sp ) (sym (HasPrev.x=fy hp)) im00
 supf-¬hp : {x  : Ordinal } → x o≤ z
 → ( {a : Ordinal } → odef A a → a << f a )
 → ¬ ( HasPrev A (UnionCF A f ay supf x) f (supf x) )
 supf-¬hp {x} x≤z <-mono hp = IsMinSUP→NotHasPrev asupf (λ {w} uw →
 (subst (λ k → w ≤ k) (sym (supf-is-minsup x≤z)) ( MinSUP.x≤sup (minsup x≤z) uw) )) <-mono hp
 supf-idem : {b : Ordinal } → b o≤ z → supf b o≤ z  → supf (supf b) ≡ supf b
 supf-idem {b} b≤z sfb≤x = z52 where
 z54 :  {w : Ordinal} → odef (UnionCF A f ay supf (supf b)) w → (w ≡ supf b) ∨ (w << supf b)
 z54 {w} ⟪ aw , ch-init fc ⟫ = fcy<sup b≤z fc
 z54 {w} ⟪ aw , ch-is-sup u u<x su=u fc ⟫ = order b≤z su<b fc where
 su<b : u o< b
 su<b = supf-inject (subst (λ k → k o< supf b ) (sym (su=u)) u<x )
 z52 : supf (supf b) ≡ supf b
 z52 = sup=u asupf sfb≤x ⟪ record { ax = asupf  ; x≤sup = z54  } , IsMinSUP→NotHasPrev asupf z54 ( λ ax → proj1 (mf< _ ax)) ⟫
 -- cp : (mf< : <-monotonic-f A f) {b : Ordinal } → b o≤ z → supf b o≤ z  → ChainP A f supf (supf b)
 --    the condition of cfcs is satisfied, this is obvious
 record ZChain1 ( A : HOD )    ( f : Ordinal → Ordinal )  (mf< : <-monotonic-f A f)
 as : A ∋ maximal
 ¬maximal<x : {x : HOD} → A ∋ x  → ¬ maximal < x       -- A is Partial, use negative
 record IChain  (A : HOD)  ( f : Ordinal → Ordinal ) {x : Ordinal } (supfz : {z : Ordinal } → z o< x → Ordinal) (z : Ordinal ) : Set n where
 field
 i : Ordinal
 i<x : i o< x
 fc : FClosure A f (supfz i<x) z
 --
 -- supf in TransFinite indution may differ each other, but it is the same because of the minimul sup
 --
 supf-unique :  ( A : HOD )    ( f : Ordinal → Ordinal )  (mf< : <-monotonic-f A f)
 {y xa xb : Ordinal} → (ay : odef A y) →  (xa o≤ xb ) → (za : ZChain A f mf< ay xa ) (zb : ZChain A f mf< ay xb )
 → {z : Ordinal } → z o≤ xa → ZChain.supf za z ≡ ZChain.supf zb z
 supf-unique A f mf< {y} {xa} {xb} ay xa≤xb za zb {z} z≤xa = TransFinite0 {λ z → z o≤ xa → ZChain.supf za z ≡ ZChain.supf zb z } ind z z≤xa  where
 supfa = ZChain.supf za
 supfb = ZChain.supf zb
 ind : (x : Ordinal) → ((w : Ordinal) → w o< x → w o≤ xa → supfa w ≡ supfb w) → x o≤ xa → supfa x ≡ supfb x
 ind x prev x≤xa = sxa=sxb where
 ma = ZChain.minsup za x≤xa
 mb = ZChain.minsup zb (OrdTrans x≤xa xa≤xb )
 spa = MinSUP.sup ma
 spb = MinSUP.sup mb
 sax=spa : supfa x ≡ spa
 sax=spa = ZChain.supf-is-minsup za x≤xa
 sbx=spb : supfb x ≡ spb
 sbx=spb = ZChain.supf-is-minsup zb (OrdTrans x≤xa xa≤xb )
 sxa=sxb : supfa x ≡ supfb x
 sxa=sxb with trio< (supfa x) (supfb x)
 ... | tri≈ ¬a b ¬c = b
 ... | tri< a ¬b ¬c = ⊥-elim ( o≤> (
 begin
 supfb x  ≡⟨ sbx=spb ⟩
 spb  ≤⟨ MinSUP.minsup mb (MinSUP.as ma) (λ {z} uzb → MinSUP.x≤sup ma (z53 uzb)) ⟩
 spa ≡⟨ sym sax=spa ⟩
 supfa x ∎ ) a ) where
 open o≤-Reasoning O
 z53 : {z : Ordinal } →  odef (UnionCF A f ay (ZChain.supf zb) x) z →  odef (UnionCF A f ay (ZChain.supf za) x) z
 z53 ⟪ as , ch-init fc ⟫ = ⟪ as , ch-init fc ⟫
 z53 {z} ⟪ as , ch-is-sup u u<x su=u fc ⟫ = ⟪ as , ch-is-sup u u<x (trans ua=ub su=u) z55 ⟫ where
 ua=ub : supfa u ≡ supfb u
 ua=ub = prev u u<x (ordtrans u<x x≤xa )
 z55 : FClosure A f (ZChain.supf za u) z
 z55 = subst (λ k → FClosure A f k z ) (sym ua=ub) fc
 ... | tri> ¬a ¬b c = ⊥-elim ( o≤> (
 begin
 supfa x  ≡⟨ sax=spa ⟩
 spa  ≤⟨ MinSUP.minsup ma (MinSUP.as mb) (λ uza → MinSUP.x≤sup mb (z53 uza)) ⟩
 spb  ≡⟨ sym sbx=spb ⟩
 supfb x ∎ ) c ) where
 open o≤-Reasoning O
 z53 : {z : Ordinal } →  odef (UnionCF A f ay (ZChain.supf za) x) z →  odef (UnionCF A f ay (ZChain.supf zb) x) z
 z53 ⟪ as , ch-init fc ⟫ = ⟪ as , ch-init fc ⟫
 z53 {z} ⟪ as , ch-is-sup u u<x su=u fc ⟫ =  ⟪ as , ch-is-sup u u<x (trans ub=ua su=u) z55  ⟫ where
 ub=ua : supfb u ≡ supfa u
 ub=ua = sym ( prev u u<x (ordtrans u<x x≤xa ))
 z55 : FClosure A f (ZChain.supf zb u) z
 z55 = subst (λ k → FClosure A f k z ) (sym ub=ua) fc
 m03 not = ⊥-elim ( not s1 (z09 (SUP.ax S)) ⟪ SUP.ax S , m05 ⟫ ) where
 S : SUP A B
 S = supP B  B⊆A total
 s1 = & (SUP.sup S)
 m05 : {w : Ordinal } → odef B w → (w ≡ s1 ) ∨ (w << s1 )
 m05 {w} bw with SUP.x≤sup S bw
 ... | case1 eq = case1 ( subst₂ (λ j k → j ≡ k ) &iso refl (trans &iso eq))
 ... | case2 lt = case2 lt
 m02 : MinSUP A B
 m02 = dont-or (m00 (& A)) m03
 -- Uncountable ascending chain by axiom of choice
 cf : ¬ Maximal A → Ordinal → Ordinal
 supf = ZChain.supf zc
 zc1 :  (x : Ordinal ) → x o≤ & A →   ZChain1 A f mf< ay zc x
 zc1 x x≤A with Oprev-p x
 ... | yes op = record { is-max = is-max } where
 px = Oprev.oprev op
 is-max :  {a : Ordinal} {b : Ordinal} → odef (UnionCF A f ay supf x) a →
 b o< x → (ab : odef A b) →
 HasPrev A (UnionCF A f ay supf x) f b  ∨ IsSUP A (UnionCF A f ay supf b) b →
 m10 : odef (UnionCF A f ay supf x) b
 m10 = ZChain.cfcs zc b<x x≤A (subst (λ k → k o< x) (sym m05) b<x) (init (ZChain.asupf zc) m05)
 ... | case1 sb=sx = ⊥-elim (<-irr (case1 (cong (*) m10)) (proj1 (mf< (supf b) (ZChain.asupf zc)))) where
 m17 : MinSUP A (UnionCF A f ay supf x) -- supf z o< supf ( supf x )
 m17 = ZChain.minsup zc x≤A
 m18 : supf x ≡ MinSUP.sup m17
 m18 = ZChain.supf-is-minsup zc x≤A
 m10 : f (supf b) ≡ supf b
 m10 = fc-stop A f mf (ZChain.asupf zc) m11 sb=sx where
 m11 : {z : Ordinal} → FClosure A f (supf b) z → (z ≡ ZChain.supf zc x) ∨ (z << ZChain.supf zc x)
 m11 {z} fc = subst (λ k → (z ≡ k) ∨ (z << k)) (sym m18) ( MinSUP.x≤sup m17 m13 ) where
 m10 : odef (UnionCF A f ay supf x) b
 m10 = ZChain.cfcs zc b<x x≤A (subst (λ k → k o< x) (sym m05) b<x) (init (ZChain.asupf zc) m05)
 ... | case1 sb=sx = ⊥-elim (<-irr (case1 (cong (*) m10)) (proj1 (mf< (supf b) (ZChain.asupf zc)))) where
 m17 : MinSUP A (UnionCF A f ay supf x) -- supf z o< supf ( supf x )
 m17 = ZChain.minsup zc x≤A
 m18 : supf x ≡ MinSUP.sup m17
 m18 = ZChain.supf-is-minsup zc x≤A
 m10 : f (supf b) ≡ supf b
 m10 = fc-stop A f mf (ZChain.asupf zc) m11 sb=sx where
 m11 : {z : Ordinal} → FClosure A f (supf b) z → (z ≡ ZChain.supf zc x) ∨ (z << ZChain.supf zc x)
 m11 {z} fc = subst (λ k → (z ≡ k) ∨ (z << k)) (sym m18) ( MinSUP.x≤sup m17 m13 ) where
 ... | tri≈ ¬a b ¬c = case1 (o≤-refl0 b)
 ... | tri> ¬a ¬b px<b with osuc-≡< b≤x
 ... | case1 eq = case2 eq
 ... | case2 b<x = ⊥-elim ( ¬p<x<op ⟪ px<b , subst (λ k → b o< k ) (sym (Oprev.oprev=x op)) b<x  ⟫ )
 mf : ≤-monotonic-f A f
 mf x ax = ⟪ case2 mf00 , proj2 (mf< x ax ) ⟫ where
 mf00 : * x < * (f x)
 mf00 = proj1 ( mf< x ax )
 --
 sf≤ :  { z : Ordinal } → x o≤ z → supf0 x o≤ supf1 z
 sf≤ {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 c = subst₂ (λ j k → j o≤ k ) (trans (sf1=sf0 o≤-refl ) (sym (ZChain.supfmax zc px<x))) (sf1=sp1 c)
 (supf1-mono (o<→≤ c ))
 --  px o<z → supf x ≡ supf0 px ≡ supf1 px o≤ supf1 z
 fcup : {u z : Ordinal } → FClosure A f (supf1 u) z → u o≤ px → FClosure A f (supf0 u) z
 fcup {u} {z} fc u≤px = subst (λ k → FClosure A f k z ) (sf1=sf0 u≤px) fc
 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
 sfpx<x : sp1 o≤ x → supf0 px o< x
 sfpx<x sp1≤x with trio< (supf0 px) x
 ... | tri< a ¬b ¬c = a
 ... | tri≈ ¬a spx=x ¬c = ⊥-elim (<-irr (case1 (cong (*) m10)) (proj1 (mf< (supf0 px) (ZChain.asupf zc)))) where
 -- supf px ≡ x then the chain is stopped, which cannot happen when <-monotonic case
 m12 : supf0 px ≡ sp1
 m12 with osuc-≡< m13
 ... | case1 eq = eq
 ... | case2 lt = ⊥-elim ( o≤> sp1≤x (subst (λ k → k o< sp1) spx=x lt ))
 m10 : f (supf0 px) ≡ supf0 px
 m10 = fc-stop A f mf (ZChain.asupf zc) m11 m12 where
 m11 : {z : Ordinal} → FClosure A f (supf0 px) z → (z ≡ sp1) ∨ (z << sp1)
 m11 {z} fc = MinSUP.x≤sup sup1 (case2 fc)
 ... | tri> ¬a ¬b c = ⊥-elim ( o<¬≡ refl (ordtrans<-≤ c (OrdTrans m13 sp1≤x )))   -- x o< supf0 px o≤ sp1 ≤ x
 -- this is a kind of maximality, so we cannot prove this without <-monotonicity
 --
 cfcs : {a b w : Ordinal }
 → a o< b → b o≤ x → supf1 a o< b  → FClosure A f (supf1 a) w → odef (UnionCF A f ay supf1 b) w
 cfcs {a} {b} {w} a<b b≤x sa<b fc with zc43 (supf0 a) px
 ... | case2 px≤sa = z50 where
 a<x : a o< x
 a<x = ordtrans<-≤ a<b b≤x
 ... | case1 px=sa = ⟪ A∋fc {A} _ f mf fc , cp  ⟫ where
 sa≤px : supf0 a o≤ px
 sa≤px = subst₂ (λ j k → j o< k) px=sa (sym (Oprev.oprev=x op)) px<x
 spx=sa : supf0 px ≡ supf0 a
 spx=sa = begin
 supf0 px ≡⟨ cong supf0 px=sa  ⟩
 supf0 (supf0 a) ≡⟨ ZChain.supf-idem zc a≤px sa≤px  ⟩
 supf0 a ∎  where open ≡-Reasoning
 z51 : supf0 px o< b
 z51 = subst (λ k → k o< b ) (sym ( begin supf0 px ≡⟨ spx=sa ⟩
 supf0 a ≡⟨ sym (sf1=sf0 a≤px) ⟩
 supf1 a ∎ )) sa<b where open ≡-Reasoning
 z52 : supf1 a ≡ supf1 (supf0 px)
 z52 = begin supf1 a ≡⟨ sf1=sf0 a≤px ⟩
 supf0 a ≡⟨ sym (ZChain.supf-idem zc a≤px sa≤px ) ⟩
 supf0 (supf0 a) ≡⟨ sym (sf1=sf0 sa≤px)  ⟩
 supf1 (supf0 a) ≡⟨ cong supf1 (sym spx=sa) ⟩
 supf1 (supf0 px) ∎ where open ≡-Reasoning
 z53 : supf1 (supf0 px) ≡ supf0 px
 z53 = begin
 supf1 (supf0 px)  ≡⟨ cong supf1 spx=sa ⟩
 supf1 (supf0 a)  ≡⟨ sf1=sf0 sa≤px ⟩
 supf0 (supf0 a)  ≡⟨ sym ( cong supf0 px=sa ) ⟩
 supf0 px  ∎  where open ≡-Reasoning
 cp : UChain ay b w
 cp = ch-is-sup (supf0 px) z51 z53 (subst (λ k → FClosure A f k w) z52 fc)
 ... | case2 px<sa = ⊥-elim ( ¬p<x<op ⟪ px<sa , subst₂ (λ j k → j o< k ) (sf1=sf0 a≤px) (sym (Oprev.oprev=x op)) z53 ⟫  ) where
 z53  : supf1 a o< x
 z53  = ordtrans<-≤ sa<b b≤x
 ... | case1 sa<px with trio< a px
 ... | tri< a<px ¬b ¬c = z50 where
 z50 : odef (UnionCF A f ay supf1 b) w
 z50 with osuc-≡< b≤x
 ... | case2 lt with ZChain.cfcs zc a<b (subst (λ k → b o< k) (sym (Oprev.oprev=x op)) lt) sa<b fc
 ... | ⟪ az , ch-init fc ⟫ = ⟪ az , ch-init fc ⟫
 ... | ⟪ az , ch-is-sup u u<b su=u fc ⟫ = ⟪ az , ch-is-sup u u<b (trans (sym (sf=eq u<x)) su=u) (fcpu fc u≤px )  ⟫ where
 u≤px : u o≤ px
 u≤px = subst (λ k → u o< k) (sym (Oprev.oprev=x op))  (ordtrans<-≤ u<b b≤x )
 u<x : u o< x
 u<x = ordtrans<-≤ u<b b≤x
 z50 | case1 eq with ZChain.cfcs zc a<px o≤-refl sa<px fc
 ... | ⟪ az , ch-init fc ⟫ = ⟪ az , ch-init fc ⟫
 ... | ⟪ az , ch-is-sup u u<px su=u fc ⟫ = ⟪ az , ch-is-sup u u<b (trans (sym (sf=eq u<x)) su=u) (fcpu fc (o<→≤ u<px)) ⟫  where -- u o< px → u o< b ?
 u<b : u o< b
 u<b = subst (λ k → u o< k ) (trans (Oprev.oprev=x op) (sym eq) ) (ordtrans u<px <-osuc )
 u<x : u o< x
 u<x = subst (λ k → u o< k ) (Oprev.oprev=x op) ( ordtrans u<px <-osuc )
 ... | tri≈ ¬a a=px ¬c = csupf1 where
 -- a ≡ px , b ≡ x, sp o≤ x
 px<b : px o< b
 px<b = subst₂ (λ j k → j o< k) a=px refl a<b
 b=x : b ≡ x
 b=x with trio< b x
 ... | tri< a ¬b ¬c = ⊥-elim ( ¬p<x<op ⟪ px<b , subst (λ k → b o< k ) (sym (Oprev.oprev=x op)) a ⟫ ) --  px o< b o< x
 z51 : FClosure A f (supf1 px) w
 z51 = subst (λ k → FClosure A f k w) (sym (trans (cong supf1 (sym a=px)) (sf1=sf0 (o≤-refl0 a=px) ))) fc
 z53 : odef A w
 z53 = A∋fc {A} _ f mf fc
 csupf1 : odef (UnionCF A f ay supf1 b) w
-csupf1 = ⟪ z53 , ch-is-sup spx (subst (λ k → spx o< k) (sym b=x) (sfpx<x ?)) z52 fc1 ⟫  where
+csupf1 with zc43 px (supf0 px)
-spx = supf0 px
+... | case2 spx≤px = ⟪ z53 , ch-is-sup (supf0 px) z54 z52 fc1 ⟫  where
-spx≤px : supf0 px o≤ px
+z54 : supf0 px o< b
-spx≤px = zc-b<x _ (sfpx<x ?)
+z54 = subst (λ k → supf0 px o< k ) (trans (Oprev.oprev=x op) (sym b=x) ) spx≤px
 z52 : supf1 (supf0 px) ≡ supf0 px
-z52 = trans (sf1=sf0 (zc-b<x _ (sfpx<x ?))) ( ZChain.supf-idem zc o≤-refl (zc-b<x _ (sfpx<x ?) ) )
+z52 = trans (sf1=sf0 spx≤px ) ( ZChain.supf-idem zc o≤-refl spx≤px  )
-fc1 : FClosure A f (supf1 spx) w
+fc1 : FClosure A f (supf1 (supf0 px)) w
 fc1 = subst (λ k → FClosure A f k w ) (trans (cong supf0 a=px) (sym z52) ) fc
+... | case1 px<spx = ⊥-elim (¬p<x<op ⟪ px<spx , z54  ⟫ ) where  -- supf1 px o≤ spuf1 x → supf1 px ≡ x o< x
+z54 : supf0 px o≤ px
+z54 = subst₂ (λ j k → supf0 j o< k ) a=px (trans b=x (sym (Oprev.oprev=x op))) sa<b
 ... | tri> ¬a ¬b c = ⊥-elim ( ¬p<x<op ⟪ c , subst (λ k → a o< k ) (sym (Oprev.oprev=x op)) ( ordtrans<-≤ a<b b≤x) ⟫ ) --  px o< a o< b o≤ x
 zc11 : {z : Ordinal} → odef (UnionCF A f 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 u<x su=u fc ⟫ = zc21 fc where
 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 su=u fc₁   ⟫ = case1 ⟪ proj2 ( mf _ ua1)  ,  ch-is-sup u u<x su=u (fsuc _ fc₁) ⟫
 ... | case2 fc = case2 (fsuc _ fc)
 zc21 (init asp refl ) with trio< (supf0 u) (supf0 px)
 ... | tri< a ¬b ¬c = case1 ⟪ asp , ch-is-sup u u<px (trans (sym (sf1=sf0 (o<→≤ u<px))) su=u )(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
 ... | tri≈ ¬a b ¬c = case2 (init (subst (λ k → odef A k) b (ZChain.asupf zc) )
 (sym (trans (sf1=sf0 (zc-b<x _ u<x))  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  ⟫ )
 is-minsup :  {z : Ordinal} → z o≤ x → IsMinSUP A (UnionCF A f ay supf1 z) (supf1 z)
 is-minsup {z} z≤x with osuc-≡< z≤x
 ... | case1 z=x = record { as = zc22 ; x≤sup = z23 ; minsup = z24  }  where
 px<z : px o< z
 px<z = subst (λ k → px o< k) (sym z=x) px<x
 zc22 : odef A (supf1 z)
 zc22 = subst (λ k → odef A k ) (sym (sf1=sp1 px<z ))  ( MinSUP.as sup1 )
 z26 : supf1 px ≤ supf1 x
 z26 = subst₂ (λ j k → j ≤ k ) (sym (sf1=sf0 o≤-refl )) (sym (sf1=sp1 px<x )) sfpx≤sp1
 z23 : {w : Ordinal } → odef ( UnionCF A f ay supf1 z ) w → w ≤ supf1 z
 z23 {w} uz with zc11 (subst (λ k → odef (UnionCF A f ay supf1 k) w) z=x uz )
 ... | case1 uz = ≤-ftrans z25 (subst₂ (λ j k → j  ≤ supf1 k) (sf1=sf0 o≤-refl) (sym z=x) z26 ) where
 z25 : w ≤ supf0 px
 z25 = IsMinSUP.x≤sup (ZChain.is-minsup zc o≤-refl ) uz
 ... | case2 fc = subst (λ k → w ≤ k ) (sym (sf1=sp1 px<z)) ( MinSUP.x≤sup sup1 (case2 fc) )
 z24 : {s : Ordinal } → odef A s → ( {w : Ordinal } → odef ( UnionCF A f ay supf1 z ) w → w ≤ s )
 → supf1 z o≤ s
 z24 {s} as sup = subst (λ k → k o≤ s ) (sym (sf1=sp1 px<z)) ( MinSUP.minsup sup1 as z25 ) where
 z25 : {w : Ordinal } → odef pchainpx w → w ≤ s
 z25 {w} (case2 fc) = sup ⟪ A∋fc _ f mf fc , ch-is-sup (supf0 px) z28 z27 fc1 ⟫ where
-z28 : supf0 px o< z --    supf0 px ≡ supf1 px o≤ supf1 x o≤
+-- z=x , supf0 px o< x
+z28 : supf0 px o< z --    supf0 px ≡ supf1 px o≤ supf1 x ≡ sp1 o≤ x ≡ z
 z28 = subst (λ k → supf0 px o< k) (sym z=x) (sfpx<x ?)
 z29 : supf0 px o≤ px
 z29 = zc-b<x _ (sfpx<x ?)
 z27 : supf1 (supf0 px) ≡ supf0 px
 z27 = trans (sf1=sf0 z29) ( ZChain.supf-idem zc o≤-refl z29 )
 fc1 : FClosure A f (supf1 (supf0 px)) w
 fc1 = subst (λ k → FClosure A f k w) (sym z27) fc
+-- x o≤ supf0 px o≤ supf0 z ≡ supf0 x ≡ sp1
+--   x o≤ supf0 px o≤ supf0 x ≡ sp1
+--       fc : FClosure A f (supf0 px) w  --   ¬ ( supf0 px o< x ) → ¬ odef ( UnionCF A f ay supf1 z ) w
 z25 {w} (case1 ⟪ ua , ch-init fc ⟫) = sup ⟪ ua , ch-init fc ⟫
 z25 {w} (case1 ⟪ ua , ch-is-sup u u<x su=u fc  ⟫) = sup ⟪ ua , ch-is-sup u u<z
 (trans (sf1=sf0 u≤px)  su=u)  (fcpu fc u≤px)  ⟫ where
 u≤px : u o< osuc px
 u≤px = ordtrans u<x <-osuc
 u<z : u o< z
 u<z = ordtrans u<x (subst (λ k → px o< k ) (sym z=x) px<x )
 ... | case2 z<x = record { as = zc22 ; x≤sup = z23 ; minsup = z24  } where
 z≤px = zc-b<x _ z<x
 m =  ZChain.is-minsup zc z≤px
 zc22 : odef A (supf1 z)
 zc22 = subst (λ k → odef A k ) (sym (sf1=sf0 z≤px))  ( IsMinSUP.as m )
 z23 : {w : Ordinal } → odef ( UnionCF A f ay supf1 z ) w → w ≤ supf1 z
 z23 {w} ⟪ ua , ch-init fc ⟫ = subst (λ k → w ≤ k ) (sym (sf1=sf0 z≤px)) ( ZChain.fcy<sup zc z≤px fc )
 z23 {w} ⟪ ua ,  ch-is-sup u u<x su=u fc  ⟫ = subst (λ k → w ≤ k ) (sym (sf1=sf0 z≤px))
 (IsMinSUP.x≤sup m ⟪ ua ,  ch-is-sup u u<x (trans (sym (sf1=sf0 u≤px )) su=u)  (fcup fc u≤px )  ⟫ ) where
 u≤px : u o≤ px
 u≤px = ordtrans u<x z≤px
 z24 : {s : Ordinal } → odef A s → ( {w : Ordinal } → odef ( UnionCF A f ay supf1 z ) w → w ≤ s )
 → supf1 z o≤ s
 z24 {s} as sup = subst (λ k → k o≤ s ) (sym (sf1=sf0 z≤px)) ( IsMinSUP.minsup m as z25 ) where
 z25 : {w : Ordinal } → odef ( UnionCF A f ay supf0 z ) w → w ≤ s
 z25 {w} ⟪ ua , ch-init fc ⟫ = sup ⟪ ua , ch-init fc ⟫
 z25 {w} ⟪ ua , ch-is-sup u u<x su=u fc  ⟫ = sup ⟪ ua , ch-is-sup u u<x
 (trans (sf1=sf0 u≤px)  su=u)  (fcpu fc u≤px)  ⟫ where
 u≤px : u o≤ px
 u≤px = ordtrans u<x z≤px
 order : {a b : Ordinal} {w : Ordinal} →
 b o≤ x → a o< b → FClosure A f (supf1 a) w → w ≤ supf1 b
 order {a} {b} {w} b≤x a<b fc with trio< b px
 ... | tri< b<px ¬b ¬c = ZChain.order zc (o<→≤ b<px) a<b (fcup fc (o<→≤ (ordtrans a<b b<px) ))
 ... | tri≈ ¬a b=px ¬c = ZChain.order zc (o≤-refl0 b=px) a<b (fcup fc (o<→≤ (subst (λ k → a o< k) b=px a<b )))
 ... | tri> ¬a ¬b px<b with trio< a px
 ... | tri< a<px ¬b ¬c = ≤-ftrans (ZChain.order zc o≤-refl a<px fc) sfpx≤sp1  --   supf1 a ≡ supf0 a
 ... | tri≈ ¬a a=px ¬c = MinSUP.x≤sup sup1 (case2 (subst (λ k → FClosure A f (supf0 k) w) a=px fc ))
 ... | tri> ¬a ¬b px<a = ⊥-elim (¬p<x<op ⟪ px<a , zc22 ⟫ ) where  --   supf1 a ≡ sp1
 zc22 : a o< osuc px
 zc22 = subst (λ k → a o< k ) (sym (Oprev.oprev=x op)) (ordtrans<-≤ a<b b≤x)
 sup=u : {b : Ordinal} (ab : odef A b) →
 zc30 : x ≡ b
 zc30 with osuc-≡< b≤x
 ... | case1 eq = sym (eq)
 ... | case2 b<x = ⊥-elim (¬p<x<op ⟪ px<b , subst (λ k → b o< k ) (sym (Oprev.oprev=x op)) b<x ⟫ )
 zc31 : sp1 o≤ b
 zc31 = MinSUP.minsup sup1 ab zc32 where
 zc32 : {w : Ordinal } → odef pchainpx w → (w ≡ b) ∨ (w << b)
 zc32 = ?
 ... | no lim with trio< x o∅
 ... | tri< a ¬b ¬c = ⊥-elim ( ¬x<0 a )
 ... | tri≈ ¬a b ¬c = record { supf = ? ; sup=u = ? ; asupf = ? ; supf-mono = ? ; order = ?
 ; supfmax = ? ; is-minsup = ? ; cfcs = ?    }
 ... | tri> ¬a ¬b 0<x = record { supf = supf1 ; sup=u = ? ; asupf = ? ; supf-mono = supf-mono ; order = ?
 ; supfmax = ? ; is-minsup = ? ; cfcs = cfcs    }  where
 -- mf : ≤-monotonic-f A f
 -- mf x ax = ? -- ⟪ case2 ( proj1 (mf< x ax)) , proj2 (mf< x ax ) ⟫  will result memory exhaust
 mf : ≤-monotonic-f A f
 mf x ax = ⟪ case2 mf00 , proj2 (mf< x ax ) ⟫ where
 mf00 : * x < * (f x)
 mf00 = proj1 ( mf< x ax )
 pzc : {z : Ordinal} → z o< x → ZChain A f mf< ay z
 zc00 {z} ic = z09 ( A∋fc (supfz (IChain.i<x ic)) f mf (IChain.fc ic) )
 aic : {z : Ordinal } → IChain A f supfz z → odef A z
 aic {z} ic =  A∋fc _ f mf (IChain.fc ic )
 zeq : {xa xb z : Ordinal }
 → (xa<x : xa o< x) → (xb<x : xb o< x) → xa o≤ xb → z o≤ xa
 → ZChain.supf (pzc  xa<x) z ≡  ZChain.supf (pzc  xb<x) z
 zeq {xa} {xb} {z} xa<x xb<x xa≤xb z≤xa =  supf-unique A f mf< ay xa≤xb
 (pzc xa<x)  (pzc xb<x)  z≤xa
 iceq : {ix iy : Ordinal } → ix ≡ iy → {i<x : ix o< x } {i<y : iy o< x } → supfz i<x ≡ supfz i<y
 iceq refl = cong supfz  o<-irr
 ifc≤ : {za zb : Ordinal } ( ia : IChain A f supfz za ) ( ib : IChain A f supfz zb ) → (ia≤ib : IChain.i ia o≤ IChain.i ib )
 → FClosure A f (ZChain.supf (pzc (ob<x lim (IChain.i<x ib))) (IChain.i ia)) za
 ifc≤ {za} {zb} ia ib ia≤ib = subst (λ k → FClosure A f k _ ) (zeq _ _ (osucc ia≤ib) (o<→≤ <-osuc) )   (IChain.fc ia)
 ptotalx : IsTotalOrderSet pchainx
 ptotalx {a} {b} ia ib = subst₂ (λ j k → Tri (j < k) (j ≡ k) (k < j)) *iso *iso uz01 where
 uz01 : Tri (* (& a) < * (& b)) (* (& a) ≡ * (& b)) (* (& b) < * (& a) )
 uz01 with trio< (IChain.i ia)  (IChain.i ib)
 ... | tri< ia<ib ¬b ¬c with
 ≤-ftrans (ZChain.order (pzc (ob<x lim (IChain.i<x ib))) ? ia<ib (ifc≤ ia ib (o<→≤ ia<ib))) (s≤fc _ f mf (IChain.fc ib))
 ... | case1 eq1 = tri≈ (λ lt → ⊥-elim (<-irr (case1 (sym ct00)) lt)) ct00  (λ lt → ⊥-elim (<-irr (case1 ct00) lt)) where
 ct00 : * (& a) ≡ * (& b)
 ct00 = cong (*) eq1
 ... | case2 lt = tri< lt  (λ eq → <-irr (case1 (sym eq)) lt) (λ lt1 → <-irr (case2 lt) lt1)
 uz01 | tri≈ ¬a ia=ib ¬c = fcn-cmp _ f mf (IChain.fc ia) (subst (λ k → FClosure A f k (& b)) (sym (iceq ia=ib)) (IChain.fc ib))
 uz01 | tri> ¬a ¬b ib<ia  with
 ≤-ftrans (ZChain.order (pzc (ob<x lim (IChain.i<x ia))) ? ib<ia (ifc≤ ib ia (o<→≤ ib<ia))) (s≤fc _ f mf (IChain.fc ia))
 ... | case1 eq1 = tri≈ (λ lt → ⊥-elim (<-irr (case1 (sym ct00)) lt)) ct00  (λ lt → ⊥-elim (<-irr (case1 ct00) lt)) where
 ct00 : * (& a) ≡ * (& b)
 ct00 = sym (cong (*) eq1)
 usup = minsupP pchainx (λ ic → A∋fc _ f mf (IChain.fc ic ) ) ptotalx
 spu = MinSUP.sup usup
 supf1 : Ordinal → Ordinal
 supf1 z with trio< z x
 ... | tri< a ¬b ¬c = ZChain.supf (pzc  (ob<x lim a)) z
 ... | tri≈ ¬a b ¬c = spu
 ... | tri> ¬a ¬b c = spu
 pchain : HOD
 pchain = UnionCF A f ay supf1 x
 ptotal : IsTotalOrderSet pchain
 ptotal {a} {b} ca cb = subst₂ (λ j k → Tri (j < k) (j ≡ k) (k < j)) *iso *iso uz01 where
 uz01 : Tri (* (& a) < * (& b)) (* (& a) ≡ * (& b)) (* (& b) < * (& a) )
 uz01 = ? --  chain-total A f mf ay supf1 ( (proj2 ca)) ( (proj2 cb))
 sf1=sf : {z : Ordinal } → (a : z o< x ) → supf1 z ≡ ZChain.supf (pzc  (ob<x lim a)) z
 sf1=sf {z} z<x with trio< z x
 ... | tri< a ¬b ¬c = cong ( λ k → ZChain.supf (pzc (ob<x lim k)) z) o<-irr
 ... | tri≈ ¬a b ¬c = ⊥-elim (¬a z<x)
 ... | tri> ¬a ¬b c = ⊥-elim (¬a z<x)
 is-minsup :  {z : Ordinal} → z o≤ x → IsMinSUP A (UnionCF A f ay supf1 z) (supf1 z)
 is-minsup = ?
 cfcs :  {a b w : Ordinal } → a o< b → b o≤ x →  supf1 a o< b → FClosure A f (supf1 a) w → odef (UnionCF A f ay supf1 b) w
 cfcs {a} {b} {w} a<b b≤x sa<b fc with osuc-≡< b≤x
 ... | case1 b=x with trio< a x
 ... | tri< a<x ¬b ¬c = zc40 where
 sa = ZChain.supf (pzc  (ob<x lim a<x)) a
 m =  omax a sa     -- x is limit ordinal, so we have sa o< m o< x
 m<x : m o< x
 m<x with trio< a sa | inspect (omax a) sa
 osuc ( omax a sa ) ≡⟨ cong (λ k → osuc (omax a k)) (sym a=sa) ⟩
 osuc ( omax a a ) ≡⟨ cong osuc (omxx _) ⟩
 osuc ( osuc  a ) ≤⟨ o<→≤ (ob<x lim (ob<x lim a<x))  ⟩
 x ∎ ) where open o≤-Reasoning O
 ... | tri> ¬a ¬b c | record { eq = eq } = ob<x lim a<x
 sam = ZChain.supf (pzc (ob<x lim m<x)) a
 zc42 : osuc a o≤ osuc m
 zc42 = osucc (o<→≤ ( omax-x _ _ ) )
 sam<m : sam o< m
 sam<m = subst (λ k → k o< m ) (supf-unique A f mf< ay zc42 (pzc (ob<x lim a<x)) (pzc (ob<x lim m<x)) (o<→≤ <-osuc)) ( omax-y _ _ )
 fcm : FClosure A f (ZChain.supf (pzc (ob<x lim m<x)) a) w
 fcm = subst (λ k → FClosure A f k w ) (zeq (ob<x lim a<x) (ob<x lim m<x) zc42 (o<→≤ <-osuc) ) fc
 zcm : odef (UnionCF A f ay (ZChain.supf (pzc  (ob<x lim m<x))) (osuc (omax a sa))) w
 zcm = ZChain.cfcs (pzc  (ob<x lim m<x)) (o<→≤ (omax-x _ _)) o≤-refl (o<→≤ sam<m) fcm
 zc40 : odef (UnionCF A f ay supf1 b) w
 zc40 with ZChain.cfcs (pzc  (ob<x lim m<x)) (o<→≤ (omax-x _ _)) o≤-refl (o<→≤ sam<m) fcm
 ... | ⟪ az , cp ⟫ = ⟪ az , ? ⟫
 ... | tri≈ ¬a b ¬c = ⊥-elim ( ¬a (ordtrans<-≤ a<b b≤x))
 ... | tri> ¬a ¬b c = ⊥-elim ( ¬a (ordtrans<-≤ a<b b≤x))
 cfcs {a} {b} {w} a<b b≤x sa<b fc | case2 b<x = zc40 where
 supfb =  ZChain.supf (pzc (ob<x lim b<x))
 sb=sa : {a : Ordinal } → a o< b → supf1 a ≡ ZChain.supf (pzc (ob<x lim b<x)) a
 sb=sa {a} a<b = trans (sf1=sf (ordtrans<-≤ a<b b≤x)) (zeq _ _ (o<→≤ (osucc a<b)) (o<→≤ <-osuc) )
 fcb : FClosure A f (supfb a) w
 fcb = subst (λ k → FClosure A f k w) (sb=sa a<b) fc
 --  supfb a o< b assures it is in Union b
 zcb : odef (UnionCF A f ay supfb b) w
 zcb = ZChain.cfcs (pzc (ob<x lim b<x)) a<b (o<→≤ <-osuc) (subst (λ k → k o< b) (sb=sa a<b) sa<b) fcb
 zc40 : odef (UnionCF A f ay supf1 b) w
 zc40 with zcb
 ... | ⟪ az , cp  ⟫ = ⟪ az , ? ⟫
 sup=u : {b : Ordinal} (ab : odef A b) →
 b o≤ x → IsMinSUP A (UnionCF A f ay supf1 b) b ∧ (¬ HasPrev A (UnionCF A f ay supf1 b) f b ) → supf1 b ≡ b
 sup=u {b} ab b≤x is-sup with osuc-≡< b≤x
 ... | case1 b=x = ? where
 zc31 : spu o≤ b
 zc31 = MinSUP.minsup usup ab zc32 where
 zc32 : {w : Ordinal } → odef pchainx w → (w ≡ b) ∨ (w << b)
 zc32 = ?
 ... | case2 b<x = trans (sf1=sf ?) (ZChain.sup=u (pzc (ob<x lim b<x)) ab ? ? )
 ---
 --- the maximum chain  has fix point of any ≤-monotonic function
 ---

Mercurial > hg > Members > kono > Proof > ZF-in-agda

comparison src/zorn.agda @ 1042:912ca4abe806