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

changeset 767:6c87cb98abf2

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
spi <= u
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 25 Jul 2022 22:27:15 +0900
parents e1c6c32efe01
children 67c7d4b43844
files src/zorn.agda
diffstat 1 files changed, 27 insertions(+), 4 deletions(-) [+]
line wrap: on
line diff
--- a/src/zorn.agda	Mon Jul 25 21:21:29 2022 +0900
+++ b/src/zorn.agda	Mon Jul 25 22:27:15 2022 +0900
@@ -640,12 +640,17 @@
      ysup f mf {y} ay = supP (uchain f mf ay) (λ lt → A∋fc y f mf lt)  (utotal f mf ay) 
 
      inititalChain : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) {y : Ordinal} (ay : odef A y) → ZChain A f mf ay o∅
-     inititalChain f mf {y} ay = record { supf = isupf ; chain⊆A = λ lt → proj1 lt ; chain∋init = cy ; csupf = csupf ; fcy<sup = ? 
+     inititalChain f mf {y} ay = record { supf = isupf ; chain⊆A = λ lt → proj1 lt ; chain∋init = cy 
+      ; csupf = λ {z} → csupf {z} ; fcy<sup = λ u<0 → ⊥-elim ( ¬x<0 u<0 )
       ; initial = isy ; f-next = inext ; f-total = itotal ; sup=u = λ _ b<0 → ⊥-elim (¬x<0 b<0) ; order = λ b<0 → ⊥-elim (¬x<0 b<0) } where
           spi =  & (SUP.sup (ysup f mf ay))
           isupf : Ordinal → Ordinal
-          isupf z = spi
+          isupf z with trio< z spi
+          ... | tri< a ¬b ¬c = y
+          ... | tri≈ ¬a b ¬c = spi
+          ... | tri> ¬a ¬b c = spi
           sp = ysup f mf ay
+          asi = SUP.A∋maximal sp
           cy : odef (UnionCF A f mf ay isupf o∅) y
           cy = ⟪ ay , ch-init (init ay)  ⟫
           y<sup : * y ≤ SUP.sup (ysup f mf ay)
@@ -653,7 +658,7 @@
           isy : {z : Ordinal } → odef (UnionCF A f mf ay isupf o∅) z → * y ≤ * z
           isy {z} ⟪ az , uz ⟫ with uz 
           ... | ch-init fc = s≤fc y f mf fc 
-          ... | ch-is-sup u is-sup fc = ≤-ftrans (subst (λ k → * y ≤ k) (sym *iso) y<sup)  (s≤fc (& (SUP.sup (ysup f mf ay))) f mf fc )
+          ... | ch-is-sup u is-sup fc = ?
           inext : {a : Ordinal} → odef (UnionCF A f mf ay isupf o∅) a → odef (UnionCF A f mf ay isupf o∅) (f a)
           inext {a} ua with (proj2 ua)
           ... | ch-init fc = ⟪ proj2 (mf _ (proj1 ua))  , ch-init (fsuc _ fc )  ⟫
@@ -664,7 +669,25 @@
                uz01 = chain-total A f mf ay isupf (proj2 ca) (proj2 cb)  
 
           csupf : {z : Ordinal} → odef (UnionCF A f mf ay isupf o∅) (isupf z)
-          csupf {z} = ?
+          csupf {z} = uz00 where
+          -- = ? where -- ⟪ asi , ch-is-sup spi uz02 (init asi) ⟫ where
+               uz03 : {z : Ordinal } →  FClosure A f y z → (z ≡ spi) ∨ (z << spi)
+               uz03 {z} fc with SUP.x<sup sp (subst (λ k → FClosure A f y k ) (sym &iso) fc )
+               ... | case1 eq = case1 ( begin
+                  z ≡⟨ sym &iso  ⟩
+                  & (* z) ≡⟨ cong (&) eq  ⟩
+                  spi  ∎ ) where open ≡-Reasoning
+               ... | case2 lt = case2 (subst (λ k → * z < k ) (sym *iso) lt )
+               uz04 : {sup1 z1 : Ordinal} → sup1 o< spi → FClosure A f (isupf sup1) z1 → (z1 ≡ isupf spi) ∨ (z1 << isupf spi)
+               uz04 {s} {z} s<spi fcz = ?
+               -- uz02 :  ChainP A f mf ay isupf spi spi
+               -- uz02 = record { csupz = init asi ; supfu=u = refl ; fcy<sup = uz03 ; order = ? }
+               uz00 : odef (UnionCF A f mf ay isupf o∅) (isupf z)
+               uz00 with trio< z spi
+               ... | tri< a ¬b ¬c = ?
+               ... | tri≈ ¬a b ¬c = ?
+               ... | tri> ¬a ¬b c = ?
+
 
      --
      -- create all ZChains under o< x