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

changeset 768:67c7d4b43844

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 22:53:11 +0900
parents 6c87cb98abf2
children 34678c0ad278
files src/zorn.agda
diffstat 1 files changed, 6 insertions(+), 15 deletions(-) [+]
line wrap: on
line diff
--- a/src/zorn.agda	Mon Jul 25 22:27:15 2022 +0900
+++ b/src/zorn.agda	Mon Jul 25 22:53:11 2022 +0900
@@ -645,10 +645,7 @@
       ; 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 with trio< z spi
-          ... | tri< a ¬b ¬c = y
-          ... | tri≈ ¬a b ¬c = spi
-          ... | tri> ¬a ¬b c = spi
+          isupf z = spi
           sp = ysup f mf ay
           asi = SUP.A∋maximal sp
           cy : odef (UnionCF A f mf ay isupf o∅) y
@@ -658,7 +655,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 = ?
+          ... | 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 )
           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 )  ⟫
@@ -669,9 +666,8 @@
                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} = uz00 where
-          -- = ? where -- ⟪ asi , ch-is-sup spi uz02 (init asi) ⟫ where
-               uz03 : {z : Ordinal } →  FClosure A f y z → (z ≡ spi) ∨ (z << spi)
+          csupf {z} = ⟪ asi , ch-is-sup spi uz02 (init asi) ⟫ where
+               uz03 : {z : Ordinal } →  FClosure A f y z → (z ≡ isupf spi) ∨ (z << isupf 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  ⟩
@@ -680,13 +676,8 @@
                ... | 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 = ?
+               uz02 :  ChainP A f mf ay isupf spi (isupf z)
+               uz02 = record { csupz = init asi ; supfu=u = refl ; fcy<sup = uz03 ; order = ? }
 
 
      --