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

changeset 862:269467244745

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 Sep 2022 08:19:50 +0900
parents 4e60b42b83a3
children f5fc3f5f618f
files src/zorn.agda
diffstat 1 files changed, 16 insertions(+), 7 deletions(-) [+]
line wrap: on
line diff
--- a/src/zorn.agda	Thu Sep 08 14:33:08 2022 +0900
+++ b/src/zorn.agda	Fri Sep 09 08:19:50 2022 +0900
@@ -882,22 +882,22 @@
           ... | case1 pr = no-extension (case2 pr) -- we have previous A ∋ z < x , f z ≡ x, so chain ∋ f z ≡ x because of f-next
           ... | case2 ¬fy<x with ODC.p∨¬p O (IsSup A (ZChain.chain zc ) ax )
           ... | case1 is-sup = -- x is a sup of zc 
-                record {  supf = supf1 
+                record {  supf = supf1 ; supf-max = ?
                    ; csupf = {!!} ; sup=u = {!!} ; supf-mono = {!!}
                    ; sup = {!!} ; supf-is-sup = {!!}   }  where
              supf1 : Ordinal → Ordinal
              supf1 z with trio< z px 
-             ... | tri< a ¬b ¬c = ZChain.supf zc z
-             ... | tri≈ ¬a b ¬c = ZChain.supf zc z
-             ... | tri> ¬a ¬b c = x
+             ... | tri< a ¬b ¬c = ZChain.supf zc z 
+             ... | tri≈ ¬a b ¬c = ZChain.supf zc z 
+             ... | tri> ¬a ¬b c = x --- SUP A (UnionCF A f mf ay supf0 px) ≡ SUP A (UnionCF A f mf ay supf1 px) 
 
              pchainx : HOD
              pchainx = UnionCF A f mf ay supf1 x
 
-             supf0px=x : supf0 px ≡ x
-             supf0px=x = ? where
+             supf0px=x : (ax : odef A x) → IsSup A (ZChain.chain zc ) ax → x ≡  & (SUP.sup (ZChain.sup zc o≤-refl ) )
+             supf0px=x is-sup = ? where
                  zc50 : supf0 px ≡ & (SUP.sup (ZChain.sup zc o≤-refl ) )
-                 zc50 = ZChain.spuf-is-sup zc ?
+                 zc50 = ZChain.supf-is-sup zc ?
 
              supf-monox : {a b : Ordinal } → a o≤ b → supf1 a o≤ supf1 b
              supf-monox {i} {j} i≤j with trio< i px | trio< j px
@@ -921,6 +921,15 @@
              ... | tri≈ ¬a b ¬c = ⊥-elim ( o≤> x≤z (subst (λ k → k o< x ) (sym b) (pxo<x op)))
              ... | tri> ¬a ¬b c = refl
             
+             pchain0=x : UnionCF A f mf ay supf0 px ≡ UnionCF A f mf ay supf1 px 
+             pchain0=x =  ==→o≡ record { eq→ = zc10 ; eq← = zc11 } where
+                     zc10 :  {z : Ordinal} → OD.def (od pchain) z → odef (UnionCF A f mf ay supf1 px) z
+                     zc10 {z} ⟪ az , ch-init fc ⟫ = ⟪ az , ch-init fc ⟫
+                     zc10 {z} ⟪ az , ch-is-sup u1 u1≤x u1-is-sup fc ⟫ = ⟪ az , ch-is-sup u1 ? ? ?  ⟫
+                     zc11 : {z : Ordinal} → odef (UnionCF A f mf ay supf1 px) z → OD.def (od pchain) z
+                     zc11 {z} ⟪ az , ch-init fc ⟫ = ⟪ az , ch-init fc ⟫ 
+                     zc11 {z} ⟪ az , ch-is-sup u1 u1≤x u1-is-sup fc ⟫ = ?
+
              csupf :  {b : Ordinal} → b o≤ x → odef (UnionCF A f mf ay supf1 (supf1 b)) (supf1 b)
              csupf {b} b≤x with zc04 b≤x 
              ... | case2 b=x = ⟪ ? , ch-is-sup x ? ? (init ? ? ) ⟫