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

changeset 1022:1b87669d9b11

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, 25 Nov 2022 12:22:22 +0900
parents 1407fed90475
children 52272b5c9d58
files src/zorn.agda
diffstat 1 files changed, 24 insertions(+), 8 deletions(-) [+]
line wrap: on
line diff
--- a/src/zorn.agda	Fri Nov 25 10:45:05 2022 +0900
+++ b/src/zorn.agda	Fri Nov 25 12:22:22 2022 +0900
@@ -1288,23 +1288,39 @@
                  cfcs mf< {a} {b} {w} a<b b≤x sa<b fc with trio< b px 
                  ... | tri< a ¬b ¬c = ZChain.cfcs zc mf< a<b (o<→≤ a) sa<b fc
                  ... | tri≈ ¬a refl ¬c = ZChain.cfcs zc mf< a<b o≤-refl sa<b fc 
-                 ... | tri> ¬a ¬b px<b = ? where
+                 ... | tri> ¬a ¬b px<b = cfcs1 where
                      x=b : x ≡ b
-                     x=b = ?
+                     x=b with trio< x b
+                     ... | tri< a ¬b ¬c = ⊥-elim ( o≤> b≤x a )
+                     ... | tri≈ ¬a b ¬c = b
+                     ... | tri> ¬a ¬b c = ⊥-elim (  ¬p<x<op ⟪ px<b , zc-b<x _ c ⟫  )  -- px o< b o< x
                      --  a o< x, supf a o< x
                      --      a o< px , supf a o< px → odef U w
                      --      a ≡ px         -- supf0 px o< x → odef U w
-                     --                     -- x o≤ supf0 px o< x → ⊥
                      --      supf a ≡ px    -- a o< px → odef U w
                      --                        a ≡ px → supf px ≡ px → odef U w
 
+                     cfcs0 : a ≡ px → odef (UnionCF A f mf ay supf0 b) w
+                     cfcs0 a=px = ⟪  A∋fc {A} _ f mf fc , ch-is-sup (supf0 px) spx<b ? ? ⟫ where
+                         spx<b : supf0 px o< b
+                         spx<b = ?
+
                      cfcs1 : odef (UnionCF A f mf ay supf0 b) w
                      cfcs1 with trio< a px
-                     ... | tri< a<px ¬b ¬c = chain-mono f mf ay (ZChain.supf zc) (ZChain.supf-mono zc) (o<→≤ px<b) 
-                             ( ZChain.cfcs zc mf< a<px o≤-refl ? fc ) 
-                     ... | tri> ¬a ¬b c = ⊥-elim ( o≤> ? c )
-                     ... | tri≈ ¬a refl ¬c = ? --  supf0 px o< x  → odef (UnionCF A f mf ay supf0 x) (supf0 px)
-                                           --  x o≤ supf0 px o≤ sp  →
+                     ... | tri< a<px ¬b ¬c = cfcs2 where
+                         sa<x : supf0 a o< x
+                         sa<x = ordtrans<-≤ sa<b b≤x
+                         cfcs2 : odef (UnionCF A f mf ay supf0 b) w
+                         cfcs2 with trio< (supf0 a) px
+                         ... | tri< sa<x ¬b ¬c = chain-mono f mf ay (ZChain.supf zc) (ZChain.supf-mono zc) (o<→≤ px<b) 
+                             ( ZChain.cfcs zc mf< a<px o≤-refl sa<x fc ) 
+                         ... | tri> ¬a ¬b c = ⊥-elim ( ¬p<x<op ⟪ c , (zc-b<x _ sa<x)  ⟫ )
+                         ... | tri≈ ¬a sa=px ¬c with trio< a px
+                         ... | tri< a<px ¬b ¬c = ⟪  A∋fc {A} _ f mf fc , ch-is-sup (supf0 a) sa<b ? ? ⟫ 
+                         ... | tri≈ ¬a a=px ¬c = cfcs0 a=px
+                         ... | tri> ¬a ¬b c = ⊥-elim ( ¬p<x<op ⟪ c , (zc-b<x _ (ordtrans<-≤ a<b b≤x) )  ⟫ )
+                     ... | tri≈ ¬a a=px ¬c = cfcs0 a=px
+                     ... | tri> ¬a ¬b c = ⊥-elim ( o≤> (zc-b<x _ (ordtrans<-≤ a<b b≤x)) c )
 
                  zc17 : {z : Ordinal } → supf0 z o≤ supf0 px
                  zc17 {z} with trio< z px