Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 1088:125605b5bf47
supf-idem is not so easy
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sun, 18 Dec 2022 16:56:17 +0900 |
| parents | 2fa98e3c0fa3 |
| children | |
| files | src/zorn.agda |
| diffstat | 1 files changed, 219 insertions(+), 63 deletions(-) [+] |
line wrap: on
line diff
--- a/src/zorn.agda Sun Dec 18 10:32:29 2022 +0900 +++ b/src/zorn.agda Sun Dec 18 16:56:17 2022 +0900 @@ -342,13 +342,15 @@ {y : Ordinal} (ay : odef A y) ( z : Ordinal ) : Set (Level.suc n) where field supf : Ordinal → Ordinal + + cfcs : {a b w : Ordinal } → a o< b → b o≤ z → supf a o< b → FClosure A f (supf a) w → odef (UnionCF A f ay supf b) w + order : {a b w : Ordinal } → b o≤ z → supf a o< supf b → FClosure A f (supf a) w → w ≤ supf b + asupf : {x : Ordinal } → odef A (supf x) - supf-mono : {x y : Ordinal } → x o≤ y → supf x o≤ supf y zo≤sz : {x : Ordinal } → x o≤ z → x o≤ supf x + is-minsup : {x : Ordinal } → (x≤z : x o≤ z) → IsMinSUP A (UnionCF A f ay supf x) (supf x) - cfcs : {a b w : Ordinal } → a o< b → b o≤ z → supf a o< b → FClosure A f (supf a) w → odef (UnionCF A f ay supf b) w - supf-idem : {b : Ordinal } → b o≤ z → supf b o≤ z → supf (supf b) ≡ supf b chain : HOD chain = UnionCF A f ay supf z @@ -398,6 +400,50 @@ 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) (subst₂ (λ j k → j o< k) (sym sua=ua) (sym sub=ub) 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) (subst₂ (λ j k → j o< k) (sym sub=ub) (sym sua=ua) 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 ) + + 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 ) + 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≤> ( @@ -436,6 +482,16 @@ ... | tri≈ ¬a b ¬c = b ... | 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 + 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 (subst (λ k → k o< supf b) (sym su=u) u<x) fc where + 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 } + 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 @@ -447,64 +503,23 @@ z45 : f (supf x) ≤ supf x z45 = IsMinSUP.x≤sup (is-minsup x≤z ) z46 - order : {a b w : Ordinal } → b o≤ z → supf a o< supf b → FClosure A f (supf a) w → w ≤ supf b - order {a} {b} {w} b≤z sa<sb fc with x<y∨y≤x (supf a) z - ... | case2 z≤sa = ⊥-elim ( o<¬≡ z27 sa<sb ) where - z27 : supf a ≡ supf b - z27 = supfeq (OrdTrans (o<→≤ (supf-inject sa<sb)) b≤z) b≤z ( union-max z≤sa b≤z sa<sb) - ... | case1 sa<z = 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 - ... | case1 lt = lt - ... | case2 b≤sa = ⊥-elim ( o≤> b≤sa ( supf-inject ( osucprev ( begin - osuc (supf (supf a)) ≡⟨ cong osuc (supf-idem (ordtrans (supf-inject sa<sb) b≤z) (o<→≤ sa<z)) ⟩ - osuc (supf a) ≤⟨ osucc sa<sb ⟩ + -- order may proved is-minsup and supf-idem, but supf-idem uses order + -- Is proving supf-idem is easier than order? + -- + order0 : {a b w : Ordinal } → b o≤ z → supf a o< supf b → FClosure A f (supf a) w → w ≤ supf b + order0 {a} {b} {w} b≤z sa<sb fc with x<y∨y≤x (supf a) z + ... | case2 z≤sa = ⊥-elim ( o<¬≡ z27 sa<sb ) where + z27 : supf a ≡ supf b + z27 = supfeq (OrdTrans (o<→≤ (supf-inject sa<sb)) b≤z) b≤z ( union-max z≤sa b≤z sa<sb) + ... | case1 sa<z = 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 + ... | case1 lt = lt + ... | case2 b≤sa = ⊥-elim ( o≤> b≤sa ( supf-inject ( osucprev ( begin + osuc (supf (supf a)) ≡⟨ cong osuc (supf-idem (ordtrans (supf-inject sa<sb) b≤z) (o<→≤ sa<z)) ⟩ + osuc (supf a) ≤⟨ osucc sa<sb ⟩ supf b ∎ )))) where open o≤-Reasoning O - 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 ) - - 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) (subst₂ (λ j k → j o< k) (sym sua=ua) (sym sub=ub) 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) (subst₂ (λ j k → j o< k) (sym sub=ub) (sym sua=ua) 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 ) - record ZChain1 ( A : HOD ) ( f : Ordinal → Ordinal ) (mf< : <-monotonic-f A f) {y : Ordinal} (ay : odef A y) (zc : ZChain A f mf< ay (& A)) ( z : Ordinal ) : Set (Level.suc n) where supf = ZChain.supf zc @@ -1110,6 +1125,32 @@ 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} 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 ) + ... | 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 ) + + 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-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 = 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-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 = supf-inject0 supf1-mono ( osucprev (begin + osuc (supf1 u) ≡⟨ cong osuc su=u ⟩ + osuc u ≤⟨ osucc (ordtrans<-≤ u<b b≤z ) ⟩ + x ≤⟨ z≤sa ⟩ + supf1 a ∎ )) where open o≤-Reasoning O + + zo≤sz : {z : Ordinal} → z o≤ x → z o≤ supf1 z 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 )) @@ -1140,10 +1181,67 @@ 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} → + b o≤ x → supf1 a o< supf1 b → FClosure A f (supf1 a) w → w ≤ supf1 b + order {a} {b} {w} b≤x sa<sb fc = z20 where + a<b : a o< b + a<b = supf-inject0 supf1-mono sa<sb + a≤px : a o≤ px + 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)) + ( 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 + 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 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) )) + (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 ) + ... | case1 b=sa = ⊥-elim (o<¬≡ sa=sb sa<sb) where + sa=sb : supf1 a ≡ supf0 b + sa=sb = begin + supf1 a ≡⟨ sf1=sf0 a≤px ⟩ + supf0 a ≡⟨ sym (ZChain.supf-idem zc a≤px (o≤-refl0 (sym (trans (sym b=px) (trans b=sa (sf1=sf0 a≤px) ))))) ⟩ + 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 ⟫ + ... | ⟪ 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 = 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))) + ... | 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 + ... | tri< a ¬b ¬c = ⊥-elim ( ¬p<x<op ⟪ px<b , zc-b<x _ a ⟫ ) -- px o< b o< x + ... | tri≈ ¬a b ¬c = b + ... | tri> ¬a ¬b c = ⊥-elim ( o≤> b≤x c ) -- x o< b ≤ x + 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) + z27 : supf1 a ≡ sp1 + 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 x=0 ¬c = record { supf = λ _ → MinSUP.sup (ysup f mf ay) ; asupf = MinSUP.as (ysup f mf ay) - ; supf-mono = λ _ → o≤-refl + ... | tri≈ ¬a x=0 ¬c = record { supf = λ _ → MinSUP.sup (ysup f mf ay) ; asupf = MinSUP.as (ysup f mf ay) + ; supf-mono = λ _ → o≤-refl ; order = λ _ s<s → ⊥-elim ( o<¬≡ refl s<s ) ; zo≤sz = zo≤sz ; is-minsup = is-minsup ; cfcs = λ a<b b≤0 → ⊥-elim ( ¬x<0 (subst (λ k → _ o< k ) x=0 (ordtrans<-≤ a<b b≤0))) } where mf : ≤-monotonic-f A f mf x ax = ⟪ case2 mf00 , proj2 (mf< x ax ) ⟫ where @@ -1153,7 +1251,7 @@ zo≤sz : {z : Ordinal} → z o≤ x → z o≤ MinSUP.sup (ysup f mf ay) zo≤sz {z} z≤x with osuc-≡< z≤x - ... | case1 refl = subst (λ k → k o≤ _) (sym x=0) o∅≤z + ... | case1 refl = subst (λ k → k o≤ _) (sym x=0) o∅≤z ... | case2 lt = ⊥-elim ( ¬x<0 (subst (λ k → z o< k ) x=0 lt ) ) is-minsup : {z : Ordinal} → z o≤ x → @@ -1169,7 +1267,7 @@ is02 : {w : Ordinal } → odef (uchain f mf ay) w → (w ≡ s) ∨ (w << s) is02 fc = sup ⟪ A∋fc _ f mf fc , ch-init fc ⟫ ... | case2 lt = ⊥-elim ( ¬x<0 (subst (λ k → z o< k ) x=0 lt ) ) - ... | tri> ¬a ¬b 0<x = record { supf = supf1 ; asupf = asupf ; supf-mono = supf-mono ; order = order + ... | tri> ¬a ¬b 0<x = record { supf = supf1 ; asupf = asupf ; supf-mono = supf-mono ; order = order ; zo≤sz = zo≤sz ; is-minsup = is-minsup ; cfcs = cfcs } where mf : ≤-monotonic-f A f @@ -1554,6 +1652,64 @@ z48 = ⟪ proj2 (mf _ (MinSUP.as usup) ) , ic-isup _ (subst (λ k → k o< x) refl spu<x) z50 (fsuc _ (init (ZChain.asupf (pzc (ob<x lim spu<x))) z49)) ⟫ + 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) 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 ) + + 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-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 = ordtrans u<a (supf-inject0 supf-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-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 = supf-inject0 supf-mono ( osucprev (begin + osuc (supf1 u) ≡⟨ cong osuc su=u ⟩ + osuc u ≤⟨ osucc (ordtrans<-≤ u<b b≤z ) ⟩ + x ≤⟨ z≤sa ⟩ + supf1 a ∎ )) where open o≤-Reasoning O + + order : {a b w : Ordinal } → b o≤ x → supf1 a o< supf1 b → FClosure A f (supf1 a) w → w ≤ supf1 b + 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 = subst (λ k → w ≤ k ) (sym (sf1=spu 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 with x<y∨y≤x (supfz a<x) x + ... | case1 sa<x = z29 where + z28 : odef (UnionCF A f ay supf1 b) w + z28 = cfcs a<x o≤-refl (subst (λ k → k o< x) (sym (sf1=sf a<x)) sa<x) (subst (λ k → FClosure A f k w ) (sym (sf1=sf a<x)) fc ) + z29 : w ≤ spu + z29 with z28 + ... | ⟪ aw , ch-init fc ⟫ = MinSUP.x≤sup usup ⟪ aw , ic-init fc ⟫ + ... | ⟪ aw , ch-is-sup u u<b su=u fc ⟫ = MinSUP.x≤sup usup ⟪ aw , ic-isup u u<b z30 + (subst (λ k → FClosure A f k w) (sf1=sf u<b) fc) ⟫ where + z30 : supfz u<b o≤ u + z30 = o≤-refl0 ( trans (sym (sf1=sf u<b)) su=u ) + ... | case2 x≤sa = ⊥-elim ( o<¬≡ z27 sa<sb ) where + z27 : supf1 a ≡ supf1 b + z27 = begin + supf1 a ≡⟨ ( supfeq1 (o<→≤ a<x) o≤-refl ( union-max1 (subst (λ k → x o≤ k ) (sym (sf1=sf a<x)) x≤sa ) b≤x sa<sb) ) ⟩ + supf1 x ∎ where open ≡-Reasoning + --- --- the maximum chain has fix point of any ≤-monotonic function ---