Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 1078:2624f8a9f6ed
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Fri, 16 Dec 2022 12:25:17 +0900 |
| parents | faa512b2425c |
| children | c2546206c891 |
| files | src/zorn.agda |
| diffstat | 1 files changed, 120 insertions(+), 104 deletions(-) [+] |
line wrap: on
line diff
--- a/src/zorn.agda Fri Dec 16 10:08:05 2022 +0900 +++ b/src/zorn.agda Fri Dec 16 12:25:17 2022 +0900 @@ -283,13 +283,13 @@ -- Union of chain lower than x -data IChain {A : HOD} { f : Ordinal → Ordinal } {y : Ordinal } (ay : odef A y ) +data IChain {A : HOD} { f : Ordinal → Ordinal } {y : Ordinal } (ay : odef A y ) {x : Ordinal } (supfz : {z : Ordinal } → z o< x → Ordinal) : (z : Ordinal ) → Set n where ic-init : {z : Ordinal } (fc : FClosure A f y z) → IChain ay supfz z ic-isup : {z : Ordinal} (i : Ordinal) (i<x : i o< x) (s<x : supfz i<x o≤ i ) (fc : FClosure A f (supfz i<x) z) → IChain ay supfz z UnionIC : ( A : HOD ) ( f : Ordinal → Ordinal ) { x : Ordinal } {y : Ordinal } (ay : odef A y ) (supfz : {z : Ordinal } → z o< x → Ordinal) → HOD -UnionIC A f ay supfz +UnionIC A f ay supfz = record { od = record { def = λ z → odef A z ∧ IChain {A} {f} ay supfz z } ; odmax = & A ; <odmax = λ {y} sy → ∈∧P→o< sy } @@ -440,30 +440,30 @@ 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 ) - supf-mono< : {a b : Ordinal } → b o≤ z → supf a o< supf b → supf a << supf b + supf-mono< : {a b : Ordinal } → b o≤ z → supf a o< supf b → supf a << supf b supf-mono< {a} {b} b≤z sa<sb with order {a} {b} b≤z sa<sb (init asupf refl) ... | case2 lt = lt - ... | case1 eq = ⊥-elim ( o<¬≡ eq sa<sb ) + ... | case1 eq = ⊥-elim ( o<¬≡ eq sa<sb ) - supfeq : {a b : Ordinal } → a o≤ z → b o≤ z → UnionCF A f ay supf a ≡ UnionCF A f ay supf b → supf a ≡ supf b + supfeq : {a b : Ordinal } → a o≤ z → b o≤ z → UnionCF A f ay supf a ≡ UnionCF A f ay supf b → supf a ≡ supf b supfeq {a} {b} a≤z b≤z ua=ub with trio< (supf a) (supf b) ... | tri< sa<sb ¬b ¬c = ⊥-elim ( o≤> ( - IsMinSUP.minsup (is-minsup b≤z) asupf (λ {z} uzb → IsMinSUP.x≤sup (is-minsup a≤z) (subst (λ k → odef k z) (sym ua=ub) uzb)) ) sa<sb ) + IsMinSUP.minsup (is-minsup b≤z) asupf (λ {z} uzb → IsMinSUP.x≤sup (is-minsup a≤z) (subst (λ k → odef k z) (sym ua=ub) uzb)) ) sa<sb ) ... | tri≈ ¬a b ¬c = b ... | tri> ¬a ¬b sb<sa = ⊥-elim ( o≤> ( - IsMinSUP.minsup (is-minsup a≤z) asupf (λ {z} uza → IsMinSUP.x≤sup (is-minsup b≤z) (subst (λ k → odef k z) ua=ub uza)) ) sb<sa ) + IsMinSUP.minsup (is-minsup a≤z) asupf (λ {z} uza → IsMinSUP.x≤sup (is-minsup b≤z) (subst (λ k → odef k z) ua=ub uza)) ) sb<sa ) - union-max : {a b : Ordinal } → z o≤ supf a → b o≤ z → supf a o< supf b → UnionCF A f ay supf a ≡ UnionCF A f ay supf b + union-max : {a b : Ordinal } → z o≤ supf a → b o≤ z → supf a o< supf b → UnionCF A f ay supf a ≡ UnionCF A f ay supf b union-max {a} {b} z≤sa b≤z sa<sb = ==→o≡ record { eq→ = z47 ; eq← = z48 } where z47 : {w : Ordinal } → odef (UnionCF A f ay supf a ) w → odef ( UnionCF A f ay supf b ) w - z47 {w} ⟪ aw , ch-init fc ⟫ = ⟪ aw , ch-init fc ⟫ + z47 {w} ⟪ aw , ch-init fc ⟫ = ⟪ aw , ch-init fc ⟫ z47 {w} ⟪ aw , ch-is-sup u u<a su=u fc ⟫ = ⟪ aw , ch-is-sup u u<b su=u fc ⟫ where - u<b : u o< b + u<b : u o< b u<b = ordtrans u<a (supf-inject sa<sb ) z48 : {w : Ordinal } → odef (UnionCF A f ay supf b ) w → odef ( UnionCF A f ay supf a ) w - z48 {w} ⟪ aw , ch-init fc ⟫ = ⟪ aw , ch-init fc ⟫ + z48 {w} ⟪ aw , ch-init fc ⟫ = ⟪ aw , ch-init fc ⟫ z48 {w} ⟪ aw , ch-is-sup u u<b su=u fc ⟫ = ⟪ aw , ch-is-sup u u<a su=u fc ⟫ where - u<a : u o< a + u<a : u o< a u<a = supf-inject ( osucprev (begin osuc (supf u) ≡⟨ cong osuc su=u ⟩ osuc u ≤⟨ osucc (ordtrans<-≤ u<b b≤z ) ⟩ @@ -481,7 +481,7 @@ z47 : b o≤ supf b z47 = zo≤sz b≤z ... | tri≈ ¬a b ¬c = b - ... | tri> ¬a ¬b b<sb = ⊥-elim ( o≤> z48 b<sb ) + ... | tri> ¬a ¬b b<sb = ⊥-elim ( o≤> z48 b<sb ) 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 @@ -491,20 +491,20 @@ u<b : u o< b u<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 } + z52 = sup=u asupf sfb≤x record { ax = asupf ; x≤sup = z54 } - x≤supfx : {x : Ordinal } → x o≤ z → supf x o≤ z → x o≤ supf x + x≤supfx : {x : Ordinal } → x o≤ z → supf x o≤ z → x o≤ supf x x≤supfx {x} x≤z sx≤z with x<y∨y≤x (supf x) x ... | case2 le = le - ... | case1 spx<px = ⊥-elim ( <<-irr z45 (proj1 ( mf< (supf x) asupf ))) where + ... | case1 spx<px = ⊥-elim ( <<-irr z45 (proj1 ( mf< (supf x) asupf ))) where z46 : odef (UnionCF A f ay supf x) (f (supf x)) z46 = ⟪ proj2 ( mf (supf x) asupf ) , ch-is-sup (supf x) spx<px z47 (fsuc _ (init asupf z47 )) ⟫ where z47 : supf (supf x) ≡ supf x z47 = supf-idem x≤z sx≤z z45 : f (supf x) ≤ supf x - z45 = IsMinSUP.x≤sup (is-minsup x≤z ) z46 + z45 = IsMinSUP.x≤sup (is-minsup x≤z ) z46 - order0 : {a b w : Ordinal } → b o≤ z → supf a o< supf b → supf a o≤ z → FClosure A f (supf a) w → w ≤ supf b + order0 : {a b w : Ordinal } → b o≤ z → supf a o< supf b → supf a o≤ z → FClosure A f (supf a) w → w ≤ supf b order0 {a} {b} {w} b≤z sa<sb sa≤z fc = IsMinSUP.x≤sup (is-minsup b≤z) (cfcs (supf-inject sa<sb) b≤z sa<b fc) where sa<b : supf a o< b sa<b with x<y∨y≤x (supf a) b @@ -717,7 +717,7 @@ b<A : b o< & A b<A = z09 ab m05 : ZChain.supf zc b ≡ b - m05 = ZChain.sup=u zc ab (o<→≤ (z09 ab) ) record { ax = ab ; x≤sup = λ {z} uz → IsSUP.x≤sup (proj2 is-sup) uz } + m05 = ZChain.sup=u zc ab (o<→≤ (z09 ab) ) record { ax = ab ; x≤sup = λ {z} uz → IsSUP.x≤sup (proj2 is-sup) uz } 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 @@ -733,7 +733,7 @@ m04 nhp = proj1 is-sup ( record { ax = HasPrev.ax nhp ; y = HasPrev.y nhp ; ay = chain-mono1 (o<→≤ b<x) (HasPrev.ay nhp) ; x=fy = HasPrev.x=fy nhp } ) m05 : ZChain.supf zc b ≡ b - m05 = ZChain.sup=u zc ab (o<→≤ (z09 ab) ) record { ax = ab ; x≤sup = λ {z} uz → IsSUP.x≤sup (proj2 is-sup) uz } + m05 = ZChain.sup=u zc ab (o<→≤ (z09 ab) ) record { ax = ab ; x≤sup = λ {z} uz → IsSUP.x≤sup (proj2 is-sup) uz } m14 : ZChain.supf zc b o< x m14 = subst (λ k → k o< x ) (sym m05) b<x m13 : odef (UnionCF A f ay supf x) z @@ -753,7 +753,7 @@ m09 : b o< & A m09 = subst (λ k → k o< & A) &iso ( c<→o< (subst (λ k → odef A k ) (sym &iso ) ab)) m05 : ZChain.supf zc b ≡ b - m05 = ZChain.sup=u zc ab (o<→≤ m09) record { ax = ab ; x≤sup = λ lt → IsSUP.x≤sup (proj2 is-sup) lt } + m05 = ZChain.sup=u zc ab (o<→≤ m09) record { ax = ab ; x≤sup = λ lt → IsSUP.x≤sup (proj2 is-sup) lt } 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 @@ -765,7 +765,7 @@ 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 - m05 = ZChain.sup=u zc ab (o<→≤ (z09 ab) ) record { ax = ab ; x≤sup = λ {z} uz → IsSUP.x≤sup (proj2 is-sup) uz } + m05 = ZChain.sup=u zc ab (o<→≤ (z09 ab) ) record { ax = ab ; x≤sup = λ {z} uz → IsSUP.x≤sup (proj2 is-sup) uz } m14 : ZChain.supf zc b o< x m14 = subst (λ k → k o< x ) (sym m05) b<x m13 : odef (UnionCF A f ay supf x) z @@ -895,8 +895,8 @@ m14 {z} uz = MinSUP.x≤sup sup1 (case1 uz) zc41 : ZChain A f mf< ay x - zc41 = record { supf = supf1 ; asupf = asupf1 ; supf-mono = supf1-mono ; order = order - ; 0<supfz = 0<supfz + zc41 = record { supf = supf1 ; asupf = asupf1 ; supf-mono = supf1-mono ; order = order + ; 0<supfz = 0<supfz ; zo≤sz = zo≤sz ; is-minsup = is-minsup ; cfcs = cfcs } where supf1 : Ordinal → Ordinal @@ -1080,7 +1080,7 @@ zc22 = subst (λ k → odef A k ) (sym (sf1=sp1 px<z )) ( MinSUP.as sup1 ) z23 : {w : Ordinal } → odef ( UnionCF A f ay supf1 z ) w → w ≤ supf1 z z23 {w} uz = subst (λ k → w ≤ k ) (sym (sf1=sp1 px<z)) ( MinSUP.x≤sup sup1 ( - zc11 (subst (λ k → odef (UnionCF A f ay supf1 k) w) z=x uz ))) + zc11 (subst (λ k → odef (UnionCF A f ay supf1 k) w) z=x uz ))) 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 @@ -1123,25 +1123,25 @@ u≤px : u o≤ px u≤px = ordtrans u<x z≤px - supfeq1 : {a b : Ordinal } → a o≤ x → b o≤ x → UnionCF A f ay supf1 a ≡ UnionCF A f ay supf1 b → supf1 a ≡ supf1 b + supfeq1 : {a b : Ordinal } → a o≤ x → b o≤ x → UnionCF A f ay supf1 a ≡ UnionCF A f ay supf1 b → supf1 a ≡ supf1 b supfeq1 {a} {b} a≤z b≤z ua=ub with trio< (supf1 a) (supf1 b) ... | tri< sa<sb ¬b ¬c = ⊥-elim ( o≤> ( - IsMinSUP.minsup (is-minsup b≤z) asupf1 (λ {z} uzb → IsMinSUP.x≤sup (is-minsup a≤z) (subst (λ k → odef k z) (sym ua=ub) uzb)) ) sa<sb ) + IsMinSUP.minsup (is-minsup b≤z) asupf1 (λ {z} uzb → IsMinSUP.x≤sup (is-minsup a≤z) (subst (λ k → odef k z) (sym ua=ub) uzb)) ) sa<sb ) ... | tri≈ ¬a b ¬c = b ... | tri> ¬a ¬b sb<sa = ⊥-elim ( o≤> ( - IsMinSUP.minsup (is-minsup a≤z) asupf1 (λ {z} uza → IsMinSUP.x≤sup (is-minsup b≤z) (subst (λ k → odef k z) ua=ub uza)) ) sb<sa ) + IsMinSUP.minsup (is-minsup a≤z) asupf1 (λ {z} uza → IsMinSUP.x≤sup (is-minsup b≤z) (subst (λ k → odef k z) ua=ub uza)) ) sb<sa ) - union-max1 : {a b : Ordinal } → x o≤ supf1 a → b o≤ x → supf1 a o< supf1 b → UnionCF A f ay supf1 a ≡ UnionCF A f ay supf1 b + union-max1 : {a b : Ordinal } → x o≤ supf1 a → b o≤ x → supf1 a o< supf1 b → UnionCF A f ay supf1 a ≡ UnionCF A f ay supf1 b union-max1 {a} {b} z≤sa b≤z sa<sb = ==→o≡ record { eq→ = z47 ; eq← = z48 } where z47 : {w : Ordinal } → odef (UnionCF A f ay supf1 a ) w → odef ( UnionCF A f ay supf1 b ) w - z47 {w} ⟪ aw , ch-init fc ⟫ = ⟪ aw , ch-init fc ⟫ + z47 {w} ⟪ aw , ch-init fc ⟫ = ⟪ aw , ch-init fc ⟫ z47 {w} ⟪ aw , ch-is-sup u u<a su=u fc ⟫ = ⟪ aw , ch-is-sup u u<b su=u fc ⟫ where - u<b : u o< b + u<b : u o< b u<b = ordtrans u<a (supf-inject0 supf1-mono sa<sb ) z48 : {w : Ordinal } → odef (UnionCF A f ay supf1 b ) w → odef ( UnionCF A f ay supf1 a ) w - z48 {w} ⟪ aw , ch-init fc ⟫ = ⟪ aw , ch-init fc ⟫ + z48 {w} ⟪ aw , ch-init fc ⟫ = ⟪ aw , ch-init fc ⟫ z48 {w} ⟪ aw , ch-is-sup u u<b su=u fc ⟫ = ⟪ aw , ch-is-sup u u<a su=u fc ⟫ where - u<a : u o< a + u<a : u o< a u<a = supf-inject0 supf1-mono ( osucprev (begin osuc (supf1 u) ≡⟨ cong osuc su=u ⟩ osuc u ≤⟨ osucc (ordtrans<-≤ u<b b≤z ) ⟩ @@ -1153,18 +1153,18 @@ zo≤sz {z} z≤x with osuc-≡< z≤x ... | case2 z<x = subst (λ k → z o≤ k) (sym (sf1=sf0 (zc-b<x _ z<x ))) (ZChain.zo≤sz zc (zc-b<x _ z<x )) ... | case1 refl with osuc-≡< (supf1-mono (o<→≤ (px<x))) -- px o≤ supf1 px o≤ supf1 x ≡ sp1 → x o≤ sp1 - ... | case2 lt = begin - x ≡⟨ sym (Oprev.oprev=x op) ⟩ - osuc px ≤⟨ osucc (ZChain.zo≤sz zc o≤-refl) ⟩ - osuc (supf0 px) ≡⟨ sym (cong osuc (sf1=sf0 o≤-refl )) ⟩ - osuc (supf1 px) ≤⟨ osucc lt ⟩ + ... | case2 lt = begin + x ≡⟨ sym (Oprev.oprev=x op) ⟩ + osuc px ≤⟨ osucc (ZChain.zo≤sz zc o≤-refl) ⟩ + osuc (supf0 px) ≡⟨ sym (cong osuc (sf1=sf0 o≤-refl )) ⟩ + osuc (supf1 px) ≤⟨ osucc lt ⟩ supf1 x ∎ where open o≤-Reasoning O ... | case1 spx=sx with osuc-≡< ( ZChain.zo≤sz zc o≤-refl ) ... | case2 lt = begin - x ≡⟨ sym (Oprev.oprev=x op) ⟩ - osuc px ≤⟨ osucc lt ⟩ - supf0 px ≡⟨ sym (sf1=sf0 o≤-refl) ⟩ - supf1 px ≤⟨ supf1-mono (o<→≤ px<x) ⟩ + x ≡⟨ sym (Oprev.oprev=x op) ⟩ + osuc px ≤⟨ osucc lt ⟩ + supf0 px ≡⟨ sym (sf1=sf0 o≤-refl) ⟩ + supf1 px ≤⟨ supf1-mono (o<→≤ px<x) ⟩ supf1 x ∎ where open o≤-Reasoning O ... | case1 px=spx = ⊥-elim ( <<-irr zc40 (proj1 ( mf< (supf0 px) (ZChain.asupf zc))) ) where zc37 : supf0 px ≡ px @@ -1175,8 +1175,8 @@ supf1 px ≡⟨ spx=sx ⟩ supf1 x ≡⟨ sf1=sp1 px<x ⟩ sp1 ∎ where open ≡-Reasoning - zc40 : f (supf0 px) ≤ supf0 px - zc40 = subst (λ k → f (supf0 px) ≤ k ) (sym zc39) + zc40 : f (supf0 px) ≤ supf0 px + zc40 = subst (λ k → f (supf0 px) ≤ k ) (sym zc39) ( MinSUP.x≤sup sup1 (case2 ⟪ fsuc _ (init (ZChain.asupf zc) refl) , subst (λ k → k o< x) (sym zc37) px<x ⟫ )) order : {a b : Ordinal} {w : Ordinal} → @@ -1188,22 +1188,22 @@ a≤px with trio< a px ... | tri< a ¬b ¬c = o<→≤ a ... | tri≈ ¬a b ¬c = o≤-refl0 b - ... | tri> ¬a ¬b c = ⊥-elim ( ¬p<x<op ⟪ c , subst (λ k → a o< k) (sym (Oprev.oprev=x op)) + ... | 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 z20 : w ≤ supf1 b z20 with trio< b px - ... | tri< b<px ¬b ¬c = ZChain.order zc (o<→≤ b<px) (subst (λ k → k o< supf0 b) (sf1=sf0 (o<→≤ (ordtrans a<b b<px))) sa<sb) - (fcup fc (o<→≤ (ordtrans a<b b<px))) - ... | tri≈ ¬a b=px ¬c = IsMinSUP.x≤sup (ZChain.is-minsup zc (o≤-refl0 b=px)) z26 where + ... | tri< b<px ¬b ¬c = ZChain.order zc (o<→≤ b<px) (subst (λ k → k o< supf0 b) (sf1=sf0 (o<→≤ (ordtrans a<b b<px))) sa<sb) + (fcup fc (o<→≤ (ordtrans a<b b<px))) + ... | tri≈ ¬a b=px ¬c = IsMinSUP.x≤sup (ZChain.is-minsup zc (o≤-refl0 b=px)) z26 where a≤x : a o≤ x a≤x = o<→≤ (ordtrans ( subst (λ k → a o< k ) b=px a<b ) px<x ) - z26 : odef ( UnionCF A f ay supf0 b ) w + z26 : odef ( UnionCF A f ay supf0 b ) w z26 with x<y∨y≤x (supf1 a) b ... | case2 b≤sa = z27 where z27 : odef (UnionCF A f ay supf0 b) w z27 with osuc-≡< b≤sa - ... | case2 b<sa = ⊥-elim ( o<¬≡ ( supfeq1 a≤x b≤x - ( union-max1 x≤sa b≤x (subst (λ k → supf1 a o< k) (sym (sf1=sf0 (o≤-refl0 b=px))) sa<sb) )) + ... | case2 b<sa = ⊥-elim ( o<¬≡ ( supfeq1 a≤x b≤x + ( union-max1 x≤sa b≤x (subst (λ k → supf1 a o< k) (sym (sf1=sf0 (o≤-refl0 b=px))) sa<sb) )) (ordtrans<-≤ sa<sb (o≤-refl0 (sym (sf1=sf0 (o≤-refl0 b=px))) ))) where x≤sa : x o≤ supf1 a x≤sa = subst (λ k → k o≤ supf1 a ) (trans (cong osuc b=px) (Oprev.oprev=x op)) (osucc b<sa ) @@ -1215,13 +1215,13 @@ supf0 (supf0 a) ≡⟨ cong supf0 (sym (sf1=sf0 a≤px )) ⟩ supf0 (supf1 a) ≡⟨ cong supf0 (sym b=sa) ⟩ supf0 b ∎ where open ≡-Reasoning - ... | case1 sa<b with cfcs a<b b≤x sa<b fc - ... | ⟪ ua , ch-init fc ⟫ = ⟪ ua , ch-init fc ⟫ + ... | case1 sa<b with cfcs a<b b≤x sa<b fc + ... | ⟪ ua , ch-init fc ⟫ = ⟪ ua , ch-init fc ⟫ ... | ⟪ ua , ch-is-sup u u<x su=u fc ⟫ = ⟪ 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 : u o≤ px u≤px = o<→≤ ( subst (λ k → u o< k ) b=px u<x ) ... | tri> ¬a ¬b px<b with x<y∨y≤x (supf1 a) b - ... | case1 sa<b = MinSUP.x≤sup sup1 (zc11 ( chain-mono f mf ay supf1 supf1-mono b≤x (cfcs a<b b≤x sa<b fc))) + ... | case1 sa<b = MinSUP.x≤sup sup1 (zc11 ( chain-mono f mf ay supf1 supf1-mono b≤x (cfcs a<b b≤x sa<b fc))) ... | case2 b≤sa = ⊥-elim ( o<¬≡ z27 sa<sb ) where -- x=b x o≤ sa UnionCF a ≡ UnionCF b → supf1 a ≡ supfb b → ⊥ b=x : b ≡ x b=x with trio< b x @@ -1231,14 +1231,14 @@ a≤x : a o≤ x a≤x = o<→≤ ( subst (λ k → a o< k ) b=x a<b ) sf1b=sp1 : supf1 b ≡ sp1 - sf1b=sp1 = sf1=sp1 (subst (λ k → px o< k) (trans (Oprev.oprev=x op) (sym b=x)) <-osuc) + sf1b=sp1 = sf1=sp1 (subst (λ k → px o< k) (trans (Oprev.oprev=x op) (sym b=x)) <-osuc) z27 : supf1 a ≡ sp1 - z27 = trans ( supfeq1 a≤x b≤x ( union-max1 (subst (λ k → k o≤ supf1 a) b=x b≤sa) + z27 = trans ( supfeq1 a≤x b≤x ( union-max1 (subst (λ k → k o≤ supf1 a) b=x b≤sa) b≤x (subst (λ k → supf1 a o< k ) (sym sf1b=sp1) sa<sb ) ) ) sf1b=sp1 ... | no lim with trio< x o∅ ... | tri< a ¬b ¬c = ⊥-elim ( ¬x<0 a ) - ... | tri≈ ¬a b ¬c = record { supf = λ _ → MinSUP.sup (ysup f mf ay) ; asupf = MinSUP.as (ysup f mf ay) ; 0<supfz = ? + ... | tri≈ ¬a b ¬c = record { supf = λ _ → MinSUP.sup (ysup f mf ay) ; asupf = MinSUP.as (ysup f mf ay) ; 0<supfz = ? ; supf-mono = λ _ → o≤-refl ; order = λ _ s<s → ⊥-elim ( o<¬≡ refl s<s ) ; zo≤sz = ? ; is-minsup = ? ; cfcs = ? } where mf : ≤-monotonic-f A f @@ -1262,7 +1262,7 @@ supfz {z} z<x = ZChain.supf (pzc (ob<x lim z<x)) z pchainU : HOD - pchainU = UnionIC A f ay supfz + pchainU = UnionIC A f ay supfz zeq : {xa xb z : Ordinal } → (xa<x : xa o< x) → (xb<x : xb o< x) → xa o≤ xb → z o≤ xa @@ -1279,7 +1279,7 @@ pic<x : {z : Ordinal } → (ic : IChain ay supfz z ) → osuc (IChain-i ic) o< x pic<x {z} (ic-init fc) = ob<x lim 0<x -- 0<x ∧ lim x → osuc o∅ o< x - pic<x {z} (ic-isup ia ia<x sa<x fca) = ob<x lim ia<x + pic<x {z} (ic-isup ia ia<x sa<x fca) = ob<x lim ia<x pchainU⊆chain : {z : Ordinal } → (pz : odef pchainU z) → odef (ZChain.chain (pzc (pic<x (proj2 pz)))) z pchainU⊆chain {z} ⟪ aw , ic-init fc ⟫ = ⟪ aw , ch-init fc ⟫ @@ -1289,33 +1289,33 @@ uz03 : ZChain.supf (pzc (ob<x lim ia<x)) ia o≤ ia uz03 = sa<x - chain⊆pchainU : {z w : Ordinal } → (oz<x : osuc z o< x) → odef (ZChain.chain (pzc oz<x)) w → odef pchainU w + chain⊆pchainU : {z w : Ordinal } → (oz<x : osuc z o< x) → odef (ZChain.chain (pzc oz<x)) w → odef pchainU w chain⊆pchainU {z} {w} oz<x ⟪ aw , ch-init fc ⟫ = ⟪ aw , ic-init fc ⟫ - chain⊆pchainU {z} {w} oz<x ⟪ aw , ch-is-sup u u<oz su=u fc ⟫ + chain⊆pchainU {z} {w} oz<x ⟪ aw , ch-is-sup u u<oz su=u fc ⟫ = ⟪ aw , ic-isup u u<x (o≤-refl0 su≡u) (subst (λ k → FClosure A f k w ) su=su fc) ⟫ where u<x : u o< x u<x = ordtrans u<oz oz<x su=su : ZChain.supf (pzc oz<x) u ≡ supfz u<x su=su = sym ( zeq _ _ (osucc u<oz) (o<→≤ <-osuc) ) su≡u : supfz u<x ≡ u - su≡u = begin + su≡u = begin ZChain.supf (pzc (ob<x lim u<x )) u ≡⟨ sym su=su ⟩ ZChain.supf (pzc oz<x) u ≡⟨ su=u ⟩ - u ∎ where open ≡-Reasoning + u ∎ where open ≡-Reasoning - chain⊆pchainU1 : {z w : Ordinal } → (z<x : z o< x) → odef (UnionCF A f ay (ZChain.supf (pzc (ob<x lim z<x))) z) w → odef pchainU w + chain⊆pchainU1 : {z w : Ordinal } → (z<x : z o< x) → odef (UnionCF A f ay (ZChain.supf (pzc (ob<x lim z<x))) z) w → odef pchainU w chain⊆pchainU1 {z} {w} z<x ⟪ aw , ch-init fc ⟫ = ⟪ aw , ic-init fc ⟫ - chain⊆pchainU1 {z} {w} z<x ⟪ aw , ch-is-sup u u<oz su=u fc ⟫ + chain⊆pchainU1 {z} {w} z<x ⟪ aw , ch-is-sup u u<oz su=u fc ⟫ = ⟪ aw , ic-isup u u<x (o≤-refl0 su≡u) (subst (λ k → FClosure A f k w ) su=su fc) ⟫ where u<x : u o< x u<x = ordtrans u<oz z<x su=su : ZChain.supf (pzc (ob<x lim z<x)) u ≡ supfz u<x su=su = sym ( zeq _ _ (o<→≤ (osucc u<oz)) (o<→≤ <-osuc) ) su≡u : supfz u<x ≡ u - su≡u = begin + su≡u = begin ZChain.supf (pzc (ob<x lim u<x )) u ≡⟨ sym su=su ⟩ ZChain.supf (pzc (ob<x lim z<x)) u ≡⟨ su=u ⟩ - u ∎ where open ≡-Reasoning + u ∎ where open ≡-Reasoning ichain-inject : {a b : Ordinal } {ia : IChain ay supfz a } {ib : IChain ay supfz b } → ZChain.supf (pzc (pic<x ia)) (IChain-i ia) o< ZChain.supf (pzc (pic<x ib)) (IChain-i ib) @@ -1324,29 +1324,29 @@ uz11 : IChain-i ia o< IChain-i ib uz11 with trio< (IChain-i ia ) (IChain-i ib) ... | tri< a ¬b ¬c = a - ... | tri≈ ¬a b ¬c = ⊥-elim ( o<¬≡ (trans (zeq _ _ (o≤-refl0 (cong osuc b)) (o<→≤ <-osuc) ) + ... | tri≈ ¬a b ¬c = ⊥-elim ( o<¬≡ (trans (zeq _ _ (o≤-refl0 (cong osuc b)) (o<→≤ <-osuc) ) ( cong (ZChain.supf (pzc (pic<x ib))) b )) sa<sb ) ... | tri> ¬a ¬b c = ⊥-elim ( o≤> ( begin - ZChain.supf (pzc (pic<x ib)) (IChain-i ib) ≡⟨ zeq _ _ (o<→≤ (osucc c)) (o<→≤ <-osuc) ⟩ - ZChain.supf (pzc (pic<x ia)) (IChain-i ib) ≤⟨ ZChain.supf-mono (pzc (pic<x ia)) (o<→≤ c) ⟩ + ZChain.supf (pzc (pic<x ib)) (IChain-i ib) ≡⟨ zeq _ _ (o<→≤ (osucc c)) (o<→≤ <-osuc) ⟩ + ZChain.supf (pzc (pic<x ia)) (IChain-i ib) ≤⟨ ZChain.supf-mono (pzc (pic<x ia)) (o<→≤ c) ⟩ ZChain.supf (pzc (pic<x ia)) (IChain-i ia) ∎ ) sa<sb ) where open o≤-Reasoning O IC⊆ : {a b : Ordinal } (ia : IChain ay supfz a ) (ib : IChain ay supfz b ) → IChain-i ia o≤ IChain-i ib → odef (ZChain.chain (pzc (pic<x ib))) a IC⊆ {a} {b} (ic-init fc ) ib ia≤ib = ⟪ A∋fc _ f mf fc , ch-init fc ⟫ IC⊆ {a} {b} (ic-isup i i<x sa<x fc ) (ic-init fcb ) ia≤ib = ⊥-elim ( o≤> ia≤ib ic01 ) where - ic02 : o∅ o< supfz i<x - ic02 = ZChain.0<supfz (pzc (ob<x lim i<x)) + ic02 : o∅ o< supfz i<x + ic02 = ZChain.0<supfz (pzc (ob<x lim i<x)) ic01 : o∅ o< i ic01 = ordtrans<-≤ ic02 sa<x - IC⊆ {a} {b} (ic-isup i i<x sa<x fc ) (ic-isup j j<x sb<x fcb ) ia≤ib + IC⊆ {a} {b} (ic-isup i i<x sa<x fc ) (ic-isup j j<x sb<x fcb ) ia≤ib = ZChain.cfcs (pzc (ob<x lim j<x) ) ia≤ib o≤-refl (OrdTrans (ZChain.supf-mono (pzc (ob<x lim j<x)) ia≤ib) sb<x) (subst (λ k → FClosure A f k a) (zeq _ _ (osucc ia≤ib) (o<→≤ <-osuc)) fc ) ptotalU : IsTotalOrderSet pchainU ptotalU {a} {b} ia ib with trio< (IChain-i (proj2 ia)) (IChain-i (proj2 ib)) - ... | tri< ia<ib ¬b ¬c = ZChain.f-total (pzc (pic<x (proj2 ib))) (IC⊆ (proj2 ia) (proj2 ib) (o<→≤ ia<ib)) (pchainU⊆chain ib) - ... | tri≈ ¬a ia=ib ¬c = ZChain.f-total (pzc (pic<x (proj2 ib))) (IC⊆ (proj2 ia) (proj2 ib) (o≤-refl0 ia=ib)) (pchainU⊆chain ib) + ... | tri< ia<ib ¬b ¬c = ZChain.f-total (pzc (pic<x (proj2 ib))) (IC⊆ (proj2 ia) (proj2 ib) (o<→≤ ia<ib)) (pchainU⊆chain ib) + ... | tri≈ ¬a ia=ib ¬c = ZChain.f-total (pzc (pic<x (proj2 ib))) (IC⊆ (proj2 ia) (proj2 ib) (o≤-refl0 ia=ib)) (pchainU⊆chain ib) ... | tri> ¬a ¬b ib<ia = ZChain.f-total (pzc (pic<x (proj2 ia))) (pchainU⊆chain ia) (IC⊆ (proj2 ib) (proj2 ia) (o<→≤ ib<ia)) usup : MinSUP A pchainU @@ -1400,7 +1400,7 @@ supf1 z with trio< z x ... | tri< a ¬b ¬c = ZChain.supf (pzc (ob<x lim a)) z -- each sup o< x ... | tri≈ ¬a b ¬c = spu -- sup of all sup o< x - ... | tri> ¬a ¬b c = sps -- sup of spu which o< x + ... | tri> ¬a ¬b c = sps -- sup of spu which o< x -- if x o< spu, spu is not included in UnionCF x -- the chain @@ -1417,9 +1417,9 @@ sf1=spu : {z : Ordinal } → x ≡ z → supf1 z ≡ spu sf1=spu {z} eq with trio< z x - ... | tri< a ¬b ¬c = ⊥-elim (¬b (sym eq)) + ... | tri< a ¬b ¬c = ⊥-elim (¬b (sym eq)) ... | tri≈ ¬a b ¬c = refl - ... | tri> ¬a ¬b c = ⊥-elim (¬b (sym eq)) + ... | tri> ¬a ¬b c = ⊥-elim (¬b (sym eq)) sf1=sps : {z : Ordinal } → (a : x o< z ) → supf1 z ≡ sps sf1=sps {z} x<z with trio< z x @@ -1444,7 +1444,7 @@ asupf : {z : Ordinal } → odef A (supf1 z) asupf {z} with trio< z x - ... | tri< a ¬b ¬c = ZChain.asupf (pzc (ob<x lim a)) + ... | tri< a ¬b ¬c = ZChain.asupf (pzc (ob<x lim a)) ... | tri≈ ¬a b ¬c = MinSUP.as usup ... | tri> ¬a ¬b c = MinSUP.as ssup @@ -1457,18 +1457,18 @@ supf1 z ≡⟨ sf1=sf (ordtrans≤-< z≤y y<x) ⟩ ZChain.supf (pzc (ob<x lim (ordtrans≤-< z≤y y<x))) z ≡⟨ zeq _ _ (osucc z≤y) (o<→≤ <-osuc) ⟩ ZChain.supf (pzc (ob<x lim y<x)) z ≤⟨ ZChain.supf-mono (pzc (ob<x lim y<x)) z≤y ⟩ - ZChain.supf (pzc (ob<x lim y<x)) y ∎ + ZChain.supf (pzc (ob<x lim y<x)) y ∎ ... | tri≈ ¬a b ¬c = zc01 where -- supf1 z o≤ spu open o≤-Reasoning O zc01 : supf1 z o≤ spu zc01 with osuc-≡< (subst (λ k → z o≤ k) b z≤y) ... | case1 z=x = o≤-refl0 (sf1=spu (sym z=x)) - ... | case2 z<x = subst (λ k → k o≤ spu ) (sym (sf1=sf z<x)) ( IsMinSUP.minsup (ZChain.is-minsup (pzc (ob<x lim z<x)) (o<→≤ <-osuc) ) + ... | case2 z<x = subst (λ k → k o≤ spu ) (sym (sf1=sf z<x)) ( IsMinSUP.minsup (ZChain.is-minsup (pzc (ob<x lim z<x)) (o<→≤ <-osuc) ) (MinSUP.as usup) (λ uw → MinSUP.x≤sup usup (chain⊆pchainU1 z<x uw)) ) ... | tri> ¬a ¬b c = zc01 where -- supf1 z o≤ sps zc01 : supf1 z o≤ sps zc01 with trio< z x - ... | tri< z<x ¬b ¬c = IsMinSUP.minsup (ZChain.is-minsup (pzc (ob<x lim z<x)) (o<→≤ <-osuc) ) + ... | tri< z<x ¬b ¬c = IsMinSUP.minsup (ZChain.is-minsup (pzc (ob<x lim z<x)) (o<→≤ <-osuc) ) (MinSUP.as ssup) (λ uw → MinSUP.x≤sup ssup (case1 (chain⊆pchainU1 z<x uw)) ) ... | tri≈ ¬a z=x ¬c = MinSUP.minsup usup (MinSUP.as ssup) (λ uw → MinSUP.x≤sup ssup (case1 uw) ) ... | tri> ¬a ¬b c = o≤-refl -- (sf1=sps c) @@ -1479,23 +1479,23 @@ 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 = asupf ; x≤sup = zm00 ; minsup = zm01 } where - zm00 : {w : Ordinal } → odef (UnionCF A f ay supf1 z) w → w ≤ supf1 z - zm00 {w} ⟪ az , ch-init fc ⟫ = subst (λ k → w ≤ k ) (sym (sf1=spu (sym z=x))) ( MinSUP.x≤sup usup ⟪ az , ic-init fc ⟫ ) - zm00 {w} ⟪ az , ch-is-sup u u<b su=u fc ⟫ = subst (λ k → w ≤ k ) (sym (sf1=spu (sym z=x))) + zm00 : {w : Ordinal } → odef (UnionCF A f ay supf1 z) w → w ≤ supf1 z + zm00 {w} ⟪ az , ch-init fc ⟫ = subst (λ k → w ≤ k ) (sym (sf1=spu (sym z=x))) ( MinSUP.x≤sup usup ⟪ az , ic-init fc ⟫ ) + zm00 {w} ⟪ az , ch-is-sup u u<b su=u fc ⟫ = subst (λ k → w ≤ k ) (sym (sf1=spu (sym z=x))) ( MinSUP.x≤sup usup ⟪ az , ic-isup u u<x (o≤-refl0 zm05) (subst (λ k → FClosure A f k w) (sym zm06) fc) ⟫ ) where u<x : u o< x u<x = subst (λ k → u o< k) z=x u<b zm06 : supfz (subst (λ k → u o< k) z=x u<b) ≡ supf1 u zm06 = trans (zeq _ _ o≤-refl (o<→≤ <-osuc) ) (sym (sf1=sf u<x )) - zm05 : supfz (subst (λ k → u o< k) z=x u<b) ≡ u + zm05 : supfz (subst (λ k → u o< k) z=x u<b) ≡ u zm05 = trans zm06 su=u zm01 : { s : Ordinal } → odef A s → ( {x : Ordinal } → odef (UnionCF A f ay supf1 z) x → x ≤ s ) → supf1 z o≤ s - zm01 {s} as sup = subst (λ k → k o≤ s ) (sym (sf1=spu (sym z=x))) ( MinSUP.minsup usup as zm02 ) where + zm01 {s} as sup = subst (λ k → k o≤ s ) (sym (sf1=spu (sym z=x))) ( MinSUP.minsup usup as zm02 ) where zm02 : {w : Ordinal } → odef pchainU w → w ≤ s zm02 {w} uw with pchainU⊆chain uw - ... | ⟪ az , ch-init fc ⟫ = sup ⟪ az , ch-init fc ⟫ + ... | ⟪ az , ch-init fc ⟫ = sup ⟪ az , ch-init fc ⟫ ... | ⟪ az , ch-is-sup u1 u<b su=u fc ⟫ = sup ⟪ az , ch-is-sup u1 (ordtrans u<b zm05) (trans zm03 su=u) zm04 ⟫ where - zm05 : osuc (IChain-i (proj2 uw)) o< z + zm05 : osuc (IChain-i (proj2 uw)) o< z zm05 = subst (λ k → osuc (IChain-i (proj2 uw)) o< k) (sym z=x) ( pic<x (proj2 uw) ) u<x : u1 o< x u<x = subst (λ k → u1 o< k) z=x ( ordtrans u<b zm05 ) @@ -1504,21 +1504,21 @@ zm04 : FClosure A f (supf1 u1) w zm04 = subst (λ k → FClosure A f k w) (sym zm03) fc ... | case2 z<x = record { as = asupf ; x≤sup = zm00 ; minsup = zm01 } where - supf0 = ZChain.supf (pzc (ob<x lim z<x)) + supf0 = ZChain.supf (pzc (ob<x lim z<x)) msup : IsMinSUP A (UnionCF A f ay supf0 z) (supf0 z) msup = ZChain.is-minsup (pzc (ob<x lim z<x)) (o<→≤ <-osuc) s1=0 : {u : Ordinal } → u o< z → supf1 u ≡ supf0 u - s1=0 {u} u<z = trans (sf1=sf (ordtrans u<z z<x)) (zeq _ _ (o<→≤ (osucc u<z)) (o<→≤ <-osuc) ) - zm00 : {w : Ordinal } → odef (UnionCF A f ay supf1 z) w → w ≤ supf1 z - zm00 {w} ⟪ az , ch-init fc ⟫ = subst (λ k → w ≤ k ) (sym (sf1=sf z<x)) ( IsMinSUP.x≤sup msup ⟪ az , ch-init fc ⟫ ) - zm00 {w} ⟪ az , ch-is-sup u u<b su=u fc ⟫ = subst (λ k → w ≤ k ) (sym (sf1=sf z<x)) + s1=0 {u} u<z = trans (sf1=sf (ordtrans u<z z<x)) (zeq _ _ (o<→≤ (osucc u<z)) (o<→≤ <-osuc) ) + zm00 : {w : Ordinal } → odef (UnionCF A f ay supf1 z) w → w ≤ supf1 z + zm00 {w} ⟪ az , ch-init fc ⟫ = subst (λ k → w ≤ k ) (sym (sf1=sf z<x)) ( IsMinSUP.x≤sup msup ⟪ az , ch-init fc ⟫ ) + zm00 {w} ⟪ az , ch-is-sup u u<b su=u fc ⟫ = subst (λ k → w ≤ k ) (sym (sf1=sf z<x)) ( IsMinSUP.x≤sup msup ⟪ az , ch-is-sup u u<b (trans (sym (s1=0 u<b)) su=u) (subst (λ k → FClosure A f k w) (s1=0 u<b) fc) ⟫ ) zm01 : { s : Ordinal } → odef A s → ( {x : Ordinal } → odef (UnionCF A f ay supf1 z) x → x ≤ s ) → supf1 z o≤ s - zm01 {s} as sup = subst (λ k → k o≤ s ) (sym (sf1=sf z<x)) ( IsMinSUP.minsup msup as zm02 ) where + zm01 {s} as sup = subst (λ k → k o≤ s ) (sym (sf1=sf z<x)) ( IsMinSUP.minsup msup as zm02 ) where zm02 : {w : Ordinal } → odef (UnionCF A f ay supf0 z) w → w ≤ s zm02 {w} ⟪ az , ch-init fc ⟫ = sup ⟪ az , ch-init fc ⟫ - zm02 {w} ⟪ az , ch-is-sup u u<b su=u fc ⟫ = sup - ⟪ az , ch-is-sup u u<b (trans (s1=0 u<b) su=u) (subst (λ k → FClosure A f k w) (sym (s1=0 u<b)) fc) ⟫ + zm02 {w} ⟪ az , ch-is-sup u u<b su=u fc ⟫ = sup + ⟪ az , ch-is-sup u u<b (trans (s1=0 u<b) su=u) (subst (λ k → FClosure A f k w) (sym (s1=0 u<b)) fc) ⟫ @@ -1558,11 +1558,11 @@ osuc m ≤⟨ osucc m<x ⟩ x ≡⟨ sym b=x ⟩ b ∎ ) where open o≤-Reasoning O - zc45 : supf1 u ≡ ZChain.supf (pzc (ob<x lim m<x)) u + zc45 : supf1 u ≡ ZChain.supf (pzc (ob<x lim m<x)) u zc45 = begin supf1 u ≡⟨ sf1=sf (subst (λ k → u o< k) b=x u<b ) ⟩ ZChain.supf (pzc (ob<x lim (subst (λ k → u o< k) b=x u<b ))) u ≡⟨ zeq _ _ (osucc u<x) (o<→≤ <-osuc) ⟩ - ZChain.supf (pzc (ob<x lim m<x)) u ∎ where open ≡-Reasoning + ZChain.supf (pzc (ob<x lim m<x)) u ∎ where open ≡-Reasoning zc44 : FClosure A f (supf1 u) w zc44 = subst (λ k → FClosure A f k w ) (sym zc45) fc ... | tri≈ ¬a b ¬c = ⊥-elim ( ¬a (ordtrans<-≤ a<b b≤x)) @@ -1580,17 +1580,33 @@ zc40 with zcb ... | ⟪ az , ch-init fc ⟫ = ⟪ az , ch-init fc ⟫ ... | ⟪ az , ch-is-sup u u<x su=u fc ⟫ = ⟪ az , ch-is-sup u u<x (trans zc45 su=u) zc44 ⟫ where - zc45 : supf1 u ≡ ZChain.supf (pzc (ob<x lim b<x)) u + zc45 : supf1 u ≡ ZChain.supf (pzc (ob<x lim b<x)) u zc45 = begin supf1 u ≡⟨ sf1=sf (ordtrans u<x b<x) ⟩ ZChain.supf (pzc (ob<x lim (ordtrans u<x b<x) )) u ≡⟨ zeq _ _ (o<→≤ (osucc u<x)) (o<→≤ <-osuc) ⟩ - ZChain.supf (pzc (ob<x lim b<x )) u ∎ where open ≡-Reasoning + ZChain.supf (pzc (ob<x lim b<x )) u ∎ where open ≡-Reasoning zc44 : FClosure A f (supf1 u) w zc44 = subst (λ k → FClosure A f k w ) (sym zc45) fc order : {a b w : Ordinal } → b o≤ x → supf1 a o< supf1 b → FClosure A f (supf1 a) w → w ≤ supf1 b - order = ? - + order {a} {b} {w} b≤x sa<sb fc with osuc-≡< b≤x + ... | case2 b<x = subst (λ k → w ≤ k ) (sym (trans (sf1=sf b<x) (sym (zeq _ _ (o<→≤ <-osuc) o≤-refl )))) ( + ZChain.order (pzc b<x) o≤-refl + (subst₂ (λ j k → j o< k ) (trans (sf1=sf a<x) (zeq _ _ (osucc a<b) (o<→≤ <-osuc))) + (trans (sf1=sf b<x) (sym (zeq _ _ (o<→≤ <-osuc) o≤-refl))) sa<sb) + (subst (λ k → FClosure A f k w) (trans (sf1=sf a<x) (zeq _ _ (osucc a<b) (o<→≤ <-osuc)) ) fc ) ) where + a<b : a o< b + a<b = supf-inject0 supf-mono sa<sb + a<x : a o< x + a<x = ordtrans<-≤ a<b b≤x + ... | case1 refl = zc40 (subst₂ (λ j k → j o< k) (sf1=sf a<x) (sf1=spu refl) sa<sb) + (subst (λ k → FClosure A f k w) (sf1=sf a<x) fc ) where + a<x : a o< x + a<x = supf-inject0 supf-mono sa<sb + zc40 : ZChain.supf (pzc (ob<x lim a<x )) a o< spu → FClosure A f (ZChain.supf (pzc (ob<x lim a<x )) a) w → w ≤ spu + zc40 sa<sp fc = MinSUP.x≤sup usup ⟪ A∋fc _ f mf fc , ic-isup a a<x zc44 fc ⟫ where + zc44 : supfz a<x o≤ a + zc44 = ? --- --- the maximum chain has fix point of any ≤-monotonic function