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

changeset 762:eb68d0870cc6

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 Mon, 25 Jul 2022 14:56:49 +0900
parents 9307f895891c
children 9aa0fc917100
files src/zorn.agda
diffstat 1 files changed, 16 insertions(+), 3 deletions(-) [+]
line wrap: on
line diff
--- a/src/zorn.agda	Mon Jul 25 08:29:15 2022 +0900
+++ b/src/zorn.agda	Mon Jul 25 14:56:49 2022 +0900
@@ -476,6 +476,7 @@
                     ... | tri< a ¬b ¬c    = ⟪ proj1 ua , ch-is-sup u (o<→≤ a) is-sup-a fc ⟫ -- u o< osuc x
                     ... | tri≈ ¬a u=px ¬c = ⟪ proj1 ua , ch-is-sup u (o≤-refl0 u=px) is-sup-a fc ⟫
                     ... | tri> ¬a ¬b c = ⊥-elim (<-irr u≤a (ptrans a<b b<u) ) where
+                         --  a and b is a sup of chain, order forces minimulity of sup
                          su=u : ZChain.supf zc u ≡ u
                          su=u = ChainP.supfu=u is-sup-a 
                          u<A : u o< & A
@@ -493,11 +494,23 @@
                     m04 = ZChain1.is-max (prev px px<x) m03 b<px ab 
                          (case2 record {x<sup = λ {z} lt → IsSup.x<sup is-sup (chain-mono2 x ( o<→≤  (subst (λ k → px o< k) (Oprev.oprev=x op) <-osuc ))  o≤-refl lt)  } ) a<b
                  ... | tri≈ ¬a b=px ¬c = ⟪ ab , ch-is-sup b (o<→≤ b<x) m06 (subst (λ k → FClosure A f k b) m05 (init ab)) ⟫   where
-                    m06 : ChainP A f mf ay (ZChain.supf zc) b b
-                    m06 = ?
                     m05 : b ≡ ZChain.supf zc b
                     m05 = sym ( ZChain.sup=u zc ab (z09 ab) 
                       record { x<sup = λ {z} uz → IsSup.x<sup is-sup (chain-mono2 x (osucc b<x) o≤-refl uz )  }  )
+                    m04 : {z : Ordinal} → FClosure A f y z → z << ZChain.supf zc b
+                    m04 {z} fcz with IsSup.x<sup is-sup ⟪ A∋fc y f mf fcz , ch-init fcz ⟫
+                    ... | case1 z=b = ?
+                    ... | case2 z<b = subst (λ k → z << k) m05 z<b
+                    m07 : {sup1 z1 : Ordinal} → sup1 o< b → FClosure A f (ZChain.supf zc sup1) z1 → z1 << ZChain.supf zc b
+                    m07 {sup1} s<b (init ay) with IsSup.x<sup is-sup ⟪ A∋fc y f mf (init ay) , ch-is-sup  ⟫
+                    ... | case1 z=b = ?
+                    ... | case2 z<b = subst (λ k → z << k) m05 z<b
+                    m07 {sup1} s<b (fsuc is-sup-z fcz) with IsSup.x<sup is-sup ⟪ A∋fc y f mf fcz , ch-is-sup  ⟫
+                    ... | case1 z=b = ?
+                    ... | case2 z<b = subst (λ k → z << k) m05 z<b
+                    m06 : ChainP A f mf ay (ZChain.supf zc) b b
+                    m06 = record { csupz = subst (λ k → FClosure A f k b) m05 (init ab) ; supfu=u = sym m05 
+                      ; fcy<sup = m04  ; order = ? }
         ... | no lim = record { is-max = is-max }  where
            is-max :  {a : Ordinal} {b : Ordinal} → odef (UnionCF A f mf ay (ZChain.supf zc) x) a →
               b o< x → (ab : odef A b) →
@@ -779,7 +792,7 @@
           pinit {a} ⟪ aa , ua ⟫  with  ua
           ... | ch-init fc = s≤fc y f mf fc
           ... | ch-is-sup u u≤x is-sup fc = ≤-ftrans (case2 zc7) (s≤fc _ f mf fc)  where
-               zc7 : y << psupf ?
+               zc7 : y << psupf _
                zc7 = ChainP.fcy<sup is-sup (init ay)
           pcy : odef pchain y
           pcy = ⟪ ay , ch-init (init ay)    ⟫