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

changeset 876:23dcb59d1231

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
csupf cannot be proved in ZChain itself
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 17 Sep 2022 15:11:13 +0900
parents 7f03e1d24961
children eaa863c4ebe8
files src/zorn.agda
diffstat 1 files changed, 20 insertions(+), 5 deletions(-) [+]
line wrap: on
line diff
--- a/src/zorn.agda	Sat Sep 17 12:53:51 2022 +0900
+++ b/src/zorn.agda	Sat Sep 17 15:11:13 2022 +0900
@@ -410,8 +410,14 @@
    supf-idem : {x : Ordinal } → supf (supf x) ≡ supf x
    supf-idem = ?
 
-   x≤supfx : (x : Ordinal ) → x o≤ supf x
-   x≤supfx = ?
+   x≤supfx : {x : Ordinal } → x o≤ supf x
+   x≤supfx {x} with trio< x (supf x)
+   ... | tri< a ¬b ¬c = o<→≤ a
+   ... | tri≈ ¬a b ¬c = o≤-refl0 b
+   ... | tri> ¬a ¬b c = ? --   supf x o< x
+   -- with osuc-≡< (supf-mono (o<→≤ c) )
+   -- ... | case1 eq = ?
+   -- ... | case2 lt = ⊥-elim ( o<¬≡ supf-idem lt)
 
    supf∈A : {b : Ordinal} → b o≤ z → odef A (supf b)
    supf∈A {b} b≤z = subst (λ k → odef A k ) (sym (supf-is-sup b≤z)) ( SUP.as ( sup b≤z ) )
@@ -423,11 +429,20 @@
    ... | case2 lt = case2 (subst (λ k → * w < k ) (subst (λ k → k ≡ _ ) *iso (cong (*) (sym (supf-is-sup u≤z ))) ) lt )
 
    csupf1 : {b : Ordinal } → supf b o< z → odef (UnionCF A f mf ay supf z) (supf b) 
-   csupf1 {b} sb<z = ⟪ asb , ch-is-sup (supf b) sb<z record { fcy<sup = fcy<sup ? ; order = ? ; supu=u = ? }  (init (subst (λ k → odef A k) ? asb)  (supf-idem) ) ⟫ where
+   csupf1 {b} sb<z = ⟪ asb , ch-is-sup (supf b) sb<z record { fcy<sup = fcy<sup (o<→≤ sb<z) ; order = order ; supu=u = supf-idem }  (init (subst (λ k → odef A k) (sym supf-idem) asb)  supf-idem ) ⟫ where
         b<z : b o< z
-        b<z = supf-inject0 supf-mono ( ordtrans<-≤ sb<z (x≤supfx z) )
+        b<z = supf-inject0 supf-mono ( ordtrans<-≤ sb<z x≤supfx  )
         asb : odef A (supf b)
         asb = supf∈A (o<→≤ b<z)
+        supb : SUP A (UnionCF A f mf ay supf (supf b))
+        supb = sup (o<→≤ sb<z)
+        supb-is-b : supf (supf b) ≡ & (SUP.sup supb)
+        supb-is-b = supf-is-sup (o<→≤ sb<z)
+        order : {s z1 : Ordinal} → supf s o< supf (supf b) →
+            FClosure A f (supf s) z1 → (z1 ≡ supf (supf b)) ∨ (z1 << supf (supf b))
+        order {s} {z1} ss<ssb fs with SUP.x<sup supb ?
+        ... | case1 eq = ?
+        ... | case2 lt = ?
 
    -- ordering is not proved here but in ZChain1 
 
@@ -766,7 +781,7 @@
           --           supf0 px ≡ supf0 x 
 
           no-extension : ( (¬ xSUP (UnionCF A f mf ay supf0 px) x ) ∨  HasPrev A pchain x f) → ZChain A f mf ay x
-          no-extension P with osuc-≡< (ZChain.x≤supfx zc px)
+          no-extension P with osuc-≡< (ZChain.x≤supfx zc )
           ... | case1 sfpx=px = ? where
                  pchainpx : HOD
                  pchainpx = record { od = record { def = λ z →  (odef A z ∧ UChain A f mf ay supf0 px z ) ∨ FClosure A f px z  } ; odmax = & A ; <odmax = zc00 } where