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

changeset 1036:23a8e4d558e0

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Fri, 02 Dec 2022 15:49:50 +0900
parents 2144ef00cab9
children 23e185ef2737
files src/zorn.agda
diffstat 1 files changed, 56 insertions(+), 3 deletions(-) [+]
line wrap: on
line diff
--- a/src/zorn.agda	Fri Dec 02 11:07:51 2022 +0900
+++ b/src/zorn.agda	Fri Dec 02 15:49:50 2022 +0900
@@ -1028,12 +1028,65 @@
                     ... | 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 ) = ?
+                    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 = ZChain.is-minsup zc (zc-b<x z<x)
-                 ... | case2 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 ⟪ ? , ch-is-sup px px<z z27 (fcpu fc ?) ⟫ where
+                            z27 : supf1 px ≡ px    --- sp1 o≤ x
+                            z27 = ?
+                        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