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

changeset 776:13d50db96684

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 20:09:43 +0900
parents 4d9f7d8beedf
children fa765e37d7f9
files src/zorn.agda
diffstat 1 files changed, 13 insertions(+), 13 deletions(-) [+]
line wrap: on
line diff
--- a/src/zorn.agda	Tue Jul 26 18:24:04 2022 +0900
+++ b/src/zorn.agda	Tue Jul 26 20:09:43 2022 +0900
@@ -714,7 +714,7 @@
           --
           no-extension : ZChain A f mf ay x
           no-extension = record { supf = supf0
-               ; initial = pinit ; chain∋init = pcy  ; csupf = csupf ; sup=u = ? ; order = ? ; fcy<sup = ? ; supf-mono = ZChain.supf-mono zc
+               ; initial = pinit ; chain∋init = pcy  ; csupf = csupf ; sup=u = {!!} ; order = {!!} ; fcy<sup = {!!} ; supf-mono = ZChain.supf-mono zc
               ;  chain⊆A = pchain⊆A ;  f-next = pnext ;  f-total = ptotal } 
 
           zc4 : ZChain A f mf ay x 
@@ -725,8 +725,8 @@
           ... | case1 pr = no-extension -- 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 ) apx )
           ... | case1 is-sup = -- x is a sup of zc 
-                record {  supf = psupf1 ; chain⊆A = ? ; f-next = ? ; f-total = ? ; csupf = ? ; sup=u = ? ; order = ? ; fcy<sup = ? 
-                   ; supf-mono = ? ; initial = ? ; chain∋init  = ? }  where
+                record {  supf = psupf1 ; chain⊆A = {!!} ; f-next = {!!} ; f-total = {!!} ; csupf = {!!} ; sup=u = {!!} ; order = {!!} ; fcy<sup = {!!} 
+                   ; supf-mono = {!!} ; initial = {!!} ; chain∋init  = {!!} }  where
              psupf1 : Ordinal → Ordinal
              psupf1 z with trio< z x 
              ... | tri< a ¬b ¬c = ZChain.supf zc z
@@ -761,7 +761,7 @@
           psupf : Ordinal → Ordinal
           psupf z with trio< z x 
           ... | tri< a ¬b ¬c = ZChain.supf (pzc (osuc z) (ob<x lim a)) z
-          ... | tri≈ ¬a b ¬c = spu              -- ^^ this z dependcy have to removed
+          ... | tri≈ ¬a b ¬c = spu              -- ^^ this z dependcy have to be removed
           ... | tri> ¬a ¬b c = spu   ----  ∀ z o< x , max (supf (pzc (osuc z) (ob<x lim a)))
 
           psupf<z : {z : Ordinal } → ( a : z o< x ) → psupf z ≡ ZChain.supf (pzc (osuc z) (ob<x lim a)) z
@@ -797,14 +797,14 @@
                         zc25 : psupf z ≡ ZChain.supf ozc z 
                         zc25 = psupf<z z<x
                         s<x : s o< x
-                        s<x = ?
+                        s<x = {!!}
                         zc26 : psupf s ≡ ZChain.supf (pzc (osuc s) (ob<x lim s<x))  s 
                         zc26 = psupf<z s<x
                         zc23 : ZChain.supf ozc s o< ZChain.supf ozc z
-                        zc23 = ?
+                        zc23 = {!!}
                         zc24 : FClosure A f (ZChain.supf ozc s) z1
                         zc24 with trio< s x
-                        ... | t = ?
+                        ... | t = {!!}
                         zc22 : (z1 ≡ psupf z) ∨ (z1 << psupf z)
                         zc22 with ZChain.order ozc <-osuc zc23 zc24 
                         ... | case1 eq = case1 (trans eq (sym eq1) )
@@ -813,9 +813,9 @@
                       cp1 = record {  fcy<sup = zc20   ; order = zc21 }
 
                      ---  u = supf u = supf z 
-          ... | tri≈ ¬a b ¬c | record { eq = eq1 } = ⟪ sa , ch-is-sup ? ? ? ⟫ where
+          ... | tri≈ ¬a b ¬c | record { eq = eq1 } = ⟪ sa , ch-is-sup {!!} {!!} {!!} ⟫ where
                 sa = SUP.A∋maximal usup
-          ... | tri> ¬a ¬b c | record { eq = eq1 } = ?
+          ... | tri> ¬a ¬b c | record { eq = eq1 } = {!!}
 
           pchain : HOD
           pchain = UnionCF A f mf ay psupf x
@@ -849,8 +849,8 @@
                           (sym (HasPrev.x=fy has-prev)) ( ch-is-sup u (ChainP-next A f mf ay _ is-sup) (fsuc _ fc))  ⟫ 
 
           no-extension : ZChain A f mf ay x
-          no-extension  = record { initial = pinit ; chain∋init = pcy  ; supf = psupf  ; csupf = csupf ; sup=u = ? ; order = ? ; fcy<sup = ?
-              ; supf-mono = ? ;  chain⊆A = pchain⊆A ;  f-next = pnext ;  f-total = ptotal }
+          no-extension  = record { initial = pinit ; chain∋init = pcy  ; supf = psupf  ; csupf = csupf ; sup=u = {!!} ; order = {!!} ; fcy<sup = {!!}
+              ; supf-mono = {!!} ;  chain⊆A = pchain⊆A ;  f-next = pnext ;  f-total = ptotal }
           zc5 : ZChain A f mf ay x 
           zc5 with ODC.∋-p O A (* x)
           ... | no noax = no-extension -- ¬ A ∋ p, just skip
@@ -858,8 +858,8 @@
                -- we have to check adding x preserve is-max ZChain A y f mf x
           ... | case1 pr = no-extension  
           ... | case2 ¬fy<x with ODC.p∨¬p O (IsSup A pchain ax )
-          ... | case1 is-sup = record { initial = {!!} ; chain∋init = {!!}  ; supf = psupf1  ; csupf = ? ; sup=u = ? ; order = ? ; fcy<sup = ?
-              ; supf-mono = ? ;  chain⊆A = {!!} ;  f-next = {!!} ;  f-total = ? } where -- x is a sup of (zc ?) 
+          ... | case1 is-sup = record { initial = {!!} ; chain∋init = {!!}  ; supf = psupf1  ; csupf = {!!} ; sup=u = {!!} ; order = {!!} ; fcy<sup = {!!}
+              ; supf-mono = {!!} ;  chain⊆A = {!!} ;  f-next = {!!} ;  f-total = {!!} } where -- x is a sup of (zc ?) 
              psupf1 : Ordinal → Ordinal
              psupf1 z with trio< z x 
              ... | tri< a ¬b ¬c = ZChain.supf (pzc z a) z