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

changeset 1054:38148b08d85c

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, 09 Dec 2022 22:59:10 +0900
parents a281ad683577
children 60211e5b1fe5
files src/zorn.agda
diffstat 1 files changed, 29 insertions(+), 6 deletions(-) [+]
line wrap: on
line diff
--- a/src/zorn.agda	Fri Dec 09 20:53:59 2022 +0900
+++ b/src/zorn.agda	Fri Dec 09 22:59:10 2022 +0900
@@ -1241,23 +1241,46 @@
                      ... | 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 = ⊥-elim ( o<¬≡ ( supfeq1  ? ? ( union-max1 ? ? (subst (λ k → supf1 a o< k) ? sa<sb) )) 
-                               (ordtrans<-≤ sa<sb (o≤-refl0 (sym (sf1=sf0 ?)) ))) 
+                          ... | 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 = z28 where
+                                  a<x : a o< x
+                                  a<x = ?
+                                  z28 : odef (UnionCF A f ay supf0 b) w
+                                  z28 with cfcs a<x ? ? fc  
+                                  ... | ⟪ ua , ch-init fc ⟫ = ⟪ ua , ch-init fc ⟫ 
+                                  ... | ⟪ ua , ch-is-sup u u<x su=u fc ⟫ = ⟪ ua , ch-is-sup u ? ? (fcup fc ?)  ⟫ 
+                                  -- px ≡ supf1 a
                           ... | 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 ? ? ? ⟫ 
+                          ... | ⟪ 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<¬≡ ? sa<sb ) where -- x=b  x o≤ sa   UnionCF a ≡ UnionCF b → supf1 a ≡ supfb b → ⊥
+                     ... | 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
-                          z27 : supf1 a ≡ supf1 b
-                          z27 = supfeq1  ? ? ( union-max1 ? ? sa<sb ) 
+                          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 )