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

changeset 780:10a036aeb688

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
sup=SUP is no good order and csupf has circular dependency
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 31 Jul 2022 17:57:15 +0900
parents 9e34893d9a03
children 460df9965d63
files src/zorn.agda
diffstat 1 files changed, 18 insertions(+), 20 deletions(-) [+]
line wrap: on
line diff
--- a/src/zorn.agda	Fri Jul 29 02:38:37 2022 +0900
+++ b/src/zorn.agda	Sun Jul 31 17:57:15 2022 +0900
@@ -283,6 +283,10 @@
 -- Union of supf z which o< x
 --
 
+--     data DChain  ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f)  {y : Ordinal} (ay : odef A y) : (z : Ordinal) → Set n where
+--        dinit :  DChain f mf ay (& (SUP.sup (ysup f mf ay)))
+--        dsuc  : {u : Ordinal } → (au : odef A u) → DChain  f mf ay u → DChain f mf ay ( & (SUP.sup (ysup f mf au)) )
+
 data UChain  ( A : HOD )    ( f : Ordinal → Ordinal )  (mf : ≤-monotonic-f A f) {y : Ordinal } (ay : odef A y )
        (supf : Ordinal → Ordinal) (x : Ordinal) : (z : Ordinal) → Set n where 
     ch-init : {z : Ordinal } (fc : FClosure A f y z) → UChain A f mf ay supf x z
@@ -310,6 +314,9 @@
       f-next : {a : Ordinal } → odef chain a → odef chain (f a)
       f-total : IsTotalOrderSet chain
 
+      sup : SUP A chain
+      supf=sup : supf z ≡ & (SUP.sup sup)
+
       supf-mono : { a b : Ordinal } → a o< b → supf a o≤ supf b
       csupf : (z : Ordinal ) → odef chain (supf z) 
       sup=u : {b : Ordinal} → (ab : odef A b) → b o< z  → IsSup A (UnionCF A f mf ay supf (osuc b)) ab → supf b ≡ b 
@@ -680,25 +687,6 @@
      -- create all ZChains under o< x
      --
 
-     record FChain (A : HOD ) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f)  {y : Ordinal} (ay : odef A y) (x : Ordinal) : Set n where
-        field
-            supf     : Ordinal → Ordinal
-            fcy<sup : { z : Ordinal ) → FClosure A f y z → z <= supf x
-            is-sup : ( z : Ordinal ) → (z<x : z o< x ) → { z1 : Ordinal } → FClosure A f (supf z) z1 → z1 <= supf x
-            is-minsup : ( x1 : Ordinal ) → 
-                (( z : Ordinal ) → (z<x : z o< x ) → { z1 : Ordinal } → FClosure A f (supf z) z1 → z1 <= x1 ) → supf x <= x1
-        order : {b s z1 : Ordinal} → b o< z → supf s o< supf b → FClosure A f (supf s) z1 → (z1 ≡ supf b) ∨ (z1 << supf b)
-        order = ?
-
-
-     fsupf : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) {y : Ordinal} (ay : odef A y) → (x : Ordinal ) → FChain A f mf ay x
-     fsupf f mf {y} ay x = TransFinite0 find x where
-          find : (x : Ordinal ) →  (( z : Ordinal ) → z o< x → FChain A f mf ay z ) → FChain A f mf ay x 
-          find x prev with trio< o∅ x
-          ... | tri< a ¬b ¬c = ?
-          ... | tri≈ ¬a b ¬c = ?
-          ... | tri> ¬a ¬b c = ?
-
      ind : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) {y : Ordinal} (ay : odef A y) → (x : Ordinal) 
          → ((z : Ordinal) → z o< x → ZChain A f mf ay z) → ZChain A f mf ay x
      ind f mf {y} ay x prev with Oprev-p x
@@ -811,7 +799,17 @@
           order :  {b sup1 z1 : Ordinal} → b o< x →
             psupf sup1 o< psupf b →
             FClosure A f (psupf sup1) z1 → (z1 ≡ psupf b) ∨ (z1 << psupf b)
-          order {b} {s} {z1}  b<x ps<pb fc = ?
+          order {b} {s} {z1}  b<x ps<pb fc = ? where
+                bzc = pzc (osuc b) (ob<x lim b<x)
+                Sb : SUP A ?
+                Sb = ZChain.sup bzc
+                sb = & (SUP.sup (ZChain.sup bzc))
+                zc21 : ZChain.supf bzc (osuc b) ≡ sb
+                zc21 = ZChain.supf=sup bzc
+                zc22 :  {z : HOD} → UnionCF A f mf ay (ZChain.supf bzc) (osuc b) ∋ z 
+                    → (z ≡ SUP.sup (ZChain.sup bzc)) ∨ (z < SUP.sup (ZChain.sup bzc))
+                zc22 = SUP.x<sup (ZChain.sup bzc)
+                zc23 = SUP.min-sup (ZChain.sup bzc)
 
           csupf : (z : Ordinal) → odef (UnionCF A f mf ay psupf x) (psupf z)
           csupf z with trio< z x | inspect psupf z