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

changeset 774:c32e85b55e19

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 Tue, 26 Jul 2022 15:14:35 +0900
parents 6a48f8eb8b53
children 4d9f7d8beedf
files src/zorn.agda
diffstat 1 files changed, 19 insertions(+), 6 deletions(-) [+]
line wrap: on
line diff
--- a/src/zorn.agda	Tue Jul 26 14:31:53 2022 +0900
+++ b/src/zorn.agda	Tue Jul 26 15:14:35 2022 +0900
@@ -766,11 +766,11 @@
           ... | tri≈ ¬a b ¬c = spu
           ... | tri> ¬a ¬b c = spu
 
-          psupf>z : {z : Ordinal } → x o< z → spu ≡ psupf z
-          psupf>z {z} x<z with trio< z x
-          ... | tri< a ¬b ¬c = ⊥-elim ( ¬c x<z)
-          ... | tri≈ ¬a b ¬c = ⊥-elim ( ¬c x<z)
-          ... | tri> ¬a ¬b c = refl
+          psupf<z : {z : Ordinal } → ( a : z o< x ) → psupf z ≡ ZChain.supf (pzc (osuc z) (ob<x lim a)) z
+          psupf<z {z} z<x with trio< z x
+          ... | tri< a ¬b ¬c = cong (λ k → ZChain.supf (pzc (osuc z) (ob<x lim k)) z) ( o<-irr _ _ )
+          ... | tri≈ ¬a b ¬c = ⊥-elim ( ¬a z<x)
+          ... | tri> ¬a ¬b c = ⊥-elim ( ¬a z<x)
 
           psupf=x : spu ≡ psupf x
           psupf=x = zc20 refl where
@@ -795,7 +795,20 @@
                       ... | case1 eq = case1 (trans eq (sym eq1) )
                       ... | case2 lt = case2 (subst ( λ k → z1 << k ) (sym eq1) lt)
                       zc21 :  {sup1 z1 : Ordinal} → psupf sup1 o< psupf z → FClosure A f (psupf sup1) z1 → (z1 ≡ psupf z) ∨ (z1 << psupf z)
-                      zc21 = ?
+                      zc21 {s} {z1} s<z fc = zc22 where
+                        zc23 : ZChain.supf ozc s o< ZChain.supf ozc z
+                        zc23 with trio< s x
+                        ... | tri< a ¬b ¬c = subst₂ (λ j k → j o< k ) 
+                            (cong (λ k → ZChain.supf (pzc (osuc z) (ob<x lim k)) _ ) o<-irr) (psupf<z z<x)  s<z
+                        ... | tri≈ ¬a b ¬c = ?
+                        ... | tri> ¬a ¬b c = ?
+                        zc24 : FClosure A f (ZChain.supf ozc s) z1
+                        zc24 with trio< s x
+                        ... | t = ?
+                        zc22 : (z1 ≡ psupf z) ∨ (z1 << psupf z)
+                        zc22 with ZChain.order ozc <-osuc zc23 zc24 
+                        ... | case1 eq = case1 (trans eq (sym eq1) )
+                        ... | case2 lt = case2 (subst ( λ k → z1 << k ) (sym eq1) lt)
                       cp1 : ChainP A f mf ay psupf z (ZChain.supf ozc z)
                       cp1 = record { csupz =  (subst (λ k → FClosure A f k _) (sym eq1) (init az) ) 
                            ; fcy<sup = zc20   ; order = zc21 }