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

changeset 837:8ceaf3455601

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 Thu, 25 Aug 2022 08:19:09 +0900
parents d72bcf8552bb
children 1a5bb940fceb
files src/zorn.agda
diffstat 1 files changed, 32 insertions(+), 2 deletions(-) [+]
line wrap: on
line diff
--- a/src/zorn.agda	Tue Aug 23 15:47:50 2022 +0900
+++ b/src/zorn.agda	Thu Aug 25 08:19:09 2022 +0900
@@ -350,6 +350,36 @@
           → HasPrev A (UnionCF A f mf ay (ZChain.supf zc) z) b f ∨  IsSup A (UnionCF A f mf ay (ZChain.supf zc) z) ab  
           → * a < * b  → odef ((UnionCF A f mf ay (ZChain.supf zc) z)) b
 
+initial-segment : ( A : HOD )    ( f : Ordinal → Ordinal )  (mf : ≤-monotonic-f A f) 
+        {a b y : Ordinal} (ay : odef A y)  (za : ZChain A f mf ay a ) (zb : ZChain A f mf ay b ) 
+        →  {z : Ordinal } → a o≤ b → z o≤ a
+        → ZChain.supf za z ≡ ZChain.supf zb z
+initial-segment A f mf {a} {b} {y} ay za zb {z} a≤b z≤a = TransFinite0 { λ x → x o≤ a → ZChain.supf za x ≡ ZChain.supf zb x } ind z z≤a where
+      ind :  (x : Ordinal) → ((z : Ordinal) → z o< x → z o≤ a → ZChain.supf za z ≡ ZChain.supf zb z ) →
+            x o≤ a → ZChain.supf za x ≡ ZChain.supf zb x
+      ind x prev x≤a = ? where
+          supfa = ZChain.supf za 
+          supfb = ZChain.supf zb 
+          zc10 : {w : Ordinal } → w o< z → UnionCF A f mf ay supfa w ≡ UnionCF A f mf ay supfb w 
+          zc10 = ?
+            -- w o< z → supfa w ≡ supfb w
+          supa : SUP A (UnionCF A f mf ay supfa x)
+          supa = ZChain.sup za x≤a
+          supb : SUP A (UnionCF A f mf ay supfb x)
+          supb = ZChain.sup zb (OrdTrans x≤a a≤b)
+          zc13 : UnionCF A f mf ay supfa x ≡ UnionCF A f mf ay supfb x 
+          zc13 = ? --
+             -- if x is sup of UCF px (or Union o< x ) , then supfa x ≡ x supfb x
+             -- if x is not sup of UCF px (or Union o< x ) or HasPrev, UCF x ≡ UCF px (or Union o< x)
+          zc15 : {B : HOD} → (a b : SUP A B) → SUP.sup a ≡ SUP.sup b
+          zc15 = ?
+          zc14 : supfa x ≡ supfb x
+          zc14 = begin 
+             supfa x ≡⟨ ? ⟩
+             & (SUP.sup supa) ≡⟨ ? ⟩
+             & (SUP.sup supb) ≡⟨ ? ⟩
+             supfb x ∎ where open ≡-Reasoning
+
 record Maximal ( A : HOD )  : Set (Level.suc n) where
    field
       maximal : HOD
@@ -789,9 +819,9 @@
 
           ysp =  & (SUP.sup (ysup f mf ay))
 
-          initial-segment : {a b z : Ordinal } → (a<x : a o< x) ( b<x : b o< x)  → a o< b  → z o≤ a 
+          initial-segment0 : {a b z : Ordinal } → (a<x : a o< x) ( b<x : b o< x)  → a o< b  → z o≤ a 
              → ZChain.supf (pzc (osuc a) (ob<x lim a<x )) z ≡ ZChain.supf (pzc (osuc b) (ob<x lim b<x )) z
-          initial-segment = ?
+          initial-segment0 = ?
 
           supf0 : Ordinal → Ordinal
           supf0 z with trio< z x