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

changeset 777:fa765e37d7f9

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, 28 Jul 2022 09:10:36 +0900
parents 13d50db96684
children 6aafa22c951a
files src/zorn.agda
diffstat 1 files changed, 28 insertions(+), 0 deletions(-) [+]
line wrap: on
line diff
--- a/src/zorn.agda	Tue Jul 26 20:09:43 2022 +0900
+++ b/src/zorn.agda	Thu Jul 28 09:10:36 2022 +0900
@@ -764,6 +764,34 @@
           ... | tri≈ ¬a b ¬c = spu              -- ^^ this z dependcy have to be removed
           ... | tri> ¬a ¬b c = spu   ----  ∀ z o< x , max (supf (pzc (osuc z) (ob<x lim a)))
 
+          record Usupf ( w : Ordinal ) : Set n where
+             field
+                uniq-supf : {z : Ordinal } → (z<w : z o< w) → (w<x : w o< x) 
+                  →    ZChain.supf (pzc (osuc z) (ob<x lim (ordtrans z<w w<x))) z
+                     ≡ ZChain.supf (pzc (osuc w) (ob<x lim w<x)) z
+         
+          US : (w1 : Ordinal) → w1 o< x → Usupf w1
+          US w1 w1<x = TransFinite0 uind w1 where
+            uind :  (w : Ordinal) → ((z : Ordinal) → z o< w → Usupf z ) → Usupf w
+            uind w uprev = record { uniq-supf = u00 } where
+              u01 : {z w : Ordinal } → (z<w : z o< w) → (w<x : w o< x) 
+                  →    ZChain.supf (pzc w ?) z
+                     ≡ ZChain.supf (pzc (osuc w) (ob<x lim w<x)) z
+              u01 = ?
+              u00 : {z : Ordinal } → (z<w : z o< w) → (w<x : w o< x) 
+                  →    ZChain.supf (pzc (osuc z) (ob<x lim (ordtrans z<w w<x))) z
+                     ≡ ZChain.supf (pzc (osuc w) (ob<x lim w<x)) z
+              u00 {z} z<w w<x with Oprev-p w
+              ... | yes op with osuc-≡< ( subst (λ k → z o< k ) (sym (Oprev.oprev=x op)) z<w )
+              ... | case1 z=pw = ?
+              ... | case2 z<pw = ?
+              u00 {z} z<w w<x | no lim = ? where -- trans (Usupf.uniq-supf (uprev _ ?) ? ? ) (u01 ? ?) where
+                  us : {z : Ordinal } → z o< w → (w<x : w o< x) → ?
+                  us {z} z<w w<x with trio< z w
+                  ... | tri< a ¬b ¬c = ?
+                  ... | tri≈ ¬a b ¬c = ?
+                  ... | tri> ¬a ¬b c = ?
+
           psupf<z : {z : Ordinal } → ( a : z o< x ) → psupf z ≡ ZChain.supf (pzc (osuc z) (ob<x lim a)) z
           psupf<z {z} z<x with trio< z x
           ... | tri< a ¬b ¬c = cong (λ k → ZChain.supf (pzc (osuc z) (ob<x lim k)) z) ( o<-irr _ _ )