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

changeset 778:6aafa22c951a

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 10:01:43 +0900
parents fa765e37d7f9
children 9e34893d9a03
files src/zorn.agda
diffstat 1 files changed, 44 insertions(+), 28 deletions(-) [+]
line wrap: on
line diff
--- a/src/zorn.agda	Thu Jul 28 09:10:36 2022 +0900
+++ b/src/zorn.agda	Thu Jul 28 10:01:43 2022 +0900
@@ -758,40 +758,56 @@
           usup = supP pchain0 (λ lt → proj1 lt) ptotal0
           spu = & (SUP.sup usup)
 
+          record Usupf ( w : Ordinal ) : Set n where
+             field
+                supf : Ordinal → Ordinal
+                uniq-supf : {z w1 : Ordinal } → z o< w1 → (w<x : w o< x) → (w1<w : w1 o< w) 
+                    →  supf z ≡ ZChain.supf (prev w1 (ordtrans w1<w 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 with Oprev-p x
+              ... | yes op = record { supf = ? ; uniq-supf = ? } where
+                  px = Oprev.oprev op
+                  zc : ZChain A f mf ay (Oprev.oprev op)
+                  zc = prev px (subst (λ k → px o< k) (Oprev.oprev=x op) <-osuc ) 
+                  supf : Ordinal → Ordinal 
+                  supf z with trio< z w
+                  ... | tri< a ¬b ¬c = ZChain.supf (prev _ ?) z
+                  ... | tri≈ ¬a b ¬c = ZChain.supf zc z
+                  ... | tri> ¬a ¬b c = ZChain.supf zc z
+                  us : {z : Ordinal } → z o< w → (w<x : w o< x) → supf z ≡ ZChain.supf (prev _ w<x) z
+                  us {z} z<w w<x with trio< z w
+                  ... | tri< a ¬b ¬c = u01 where
+                      u02 :  ? ≡ Usupf.supf (uprev z a) z
+                      u02 = ?
+                      u01 : ZChain.supf (prev ? ?) z ≡ ZChain.supf (prev w w<x) z
+                      u01 = ? -- subst (λ k → k ≡ _ ) ? ( Usupf.uniq-supf (uprev _ ?) ? ? )
+                  ... | tri≈ ¬a b ¬c = ?
+                  ... | tri> ¬a ¬b c = ?
+              ... | no wlim = record { supf = supf ; uniq-supf = ? } where
+                  supf : Ordinal → Ordinal 
+                  supf z with trio< (osuc z) w
+                  ... | tri< a ¬b ¬c = Usupf.supf ( uprev (osuc z) a ) z
+                  ... | tri≈ ¬a b ¬c = spu
+                  ... | tri> ¬a ¬b c = spu
+                  us : {z : Ordinal} {w2 : Ordinal} → z o< w2 
+                     → (w<x : w o< x) (w2<w : w2 o< w) → supf z ≡ ZChain.supf (prev w2 (ordtrans w2<w w<x)) z
+                  us {z} {w2} z<w2 w<x w2<w with trio< (osuc z) w
+                  ... | tri< a ¬b ¬c = ? where
+                      u00 =  Usupf.uniq-supf (uprev (osuc z) ?)  ? ? ? 
+                      u01 =  Usupf.uniq-supf (uprev w2 ?)  ? ? ?
+                  ... | tri≈ ¬a b ¬c = ?
+                  ... | tri> ¬a ¬b c = ?
+
+
           psupf : Ordinal → Ordinal
           psupf z with trio< z x 
           ... | tri< a ¬b ¬c = ZChain.supf (pzc (osuc z) (ob<x lim a)) z
           ... | 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 _ _ )