Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 1053:a281ad683577
order connected
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Fri, 09 Dec 2022 20:53:59 +0900 |
| parents | 0b6cee971cba |
| children | 38148b08d85c |
| files | src/zorn.agda |
| diffstat | 1 files changed, 58 insertions(+), 9 deletions(-) [+] |
line wrap: on
line diff
--- a/src/zorn.agda Fri Dec 09 11:38:13 2022 +0900 +++ b/src/zorn.agda Fri Dec 09 20:53:59 2022 +0900 @@ -475,14 +475,30 @@ ... | case2 lt = lt ... | case1 eq = ⊥-elim ( o<¬≡ eq sa<sb ) - supfeq : {a b : Ordinal } → UnionCF A f ay supf a ≡ UnionCF A f ay supf b → supf a ≡ supf b - supfeq = ? + 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 ) + ... | 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 ) - unioneq : {a b : Ordinal } → z o≤ supf a → supf a o≤ supf b → UnionCF A f ay supf a ≡ UnionCF A f ay supf b - unioneq = ? - - -- 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 + 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-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-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-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-inject ( osucprev (begin + osuc (supf u) ≡⟨ cong osuc su=u ⟩ + osuc u ≤⟨ osucc (ordtrans<-≤ u<b b≤z ) ⟩ + z ≤⟨ z≤sa ⟩ + supf a ∎ )) where open o≤-Reasoning O 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 @@ -1184,6 +1200,31 @@ 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 ⟫ )) + 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 + 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 @@ -1202,13 +1243,21 @@ ... | tri≈ ¬a b=px ¬c = IsMinSUP.x≤sup (ZChain.is-minsup zc (o≤-refl0 b=px)) z26 where z26 : odef ( UnionCF A f ay supf0 b ) w z26 with x<y∨y≤x (supf1 a) b - ... | case2 b≤sa = ? + ... | case2 b≤sa = ⊥-elim ( o<¬≡ ( supfeq1 ? ? ( union-max1 ? ? (subst (λ k → supf1 a o< k) ? sa<sb) )) + (ordtrans<-≤ sa<sb (o≤-refl0 (sym (sf1=sf0 ?)) ))) ... | 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 ? ? ? ⟫ ... | 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 = ? -- x=b x o≤ sa UnionCF a ≡ UnionCF b → supf1 a ≡ supfb b → ⊥ + ... | case2 b≤sa = ⊥-elim ( o<¬≡ ? 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 + z27 : supf1 a ≡ supf1 b + z27 = supfeq1 ? ? ( union-max1 ? ? sa<sb ) ... | no lim with trio< x o∅ ... | tri< a ¬b ¬c = ⊥-elim ( ¬x<0 a )