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

changeset 873:27bab3f65064

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 Fri, 16 Sep 2022 23:06:10 +0900
parents a639a0d92659
children 852bdf4a2df3
files src/zorn.agda
diffstat 1 files changed, 32 insertions(+), 0 deletions(-) [+]
line wrap: on
line diff
--- a/src/zorn.agda	Fri Sep 16 20:12:10 2022 +0900
+++ b/src/zorn.agda	Fri Sep 16 23:06:10 2022 +0900
@@ -816,6 +816,33 @@
                  pchainp : HOD
                  pchainp = UnionCF A f mf ay supf1  x
 
+                 zc10 :  {z : Ordinal} → OD.def (od pchain) z → OD.def (od pchainp) z
+                 zc10 {z} ⟪ az , ch-init fc ⟫ = ⟪ az , ch-init fc ⟫ 
+                 zc10 {z} ⟪ az , ch-is-sup u1 u1<x u1-is-sup fc ⟫ = ⟪ az , ch-is-sup u1 (ordtrans u1<x (pxo<x op)) ?  ?  ⟫
+
+                 zc11 :  {z : Ordinal} → z o< px  → OD.def (od pchainp) z → OD.def (od pchain) z
+                 zc11 {z} z<px ⟪ az , ch-init fc ⟫ = ⟪ az , ch-init fc ⟫ 
+                 zc11 {z} z<px ⟪ az , ch-is-sup u1 u1<x u1-is-sup fc ⟫ = ⟪ az , ch-is-sup u1 (ordtrans u1<x ?) ?  ?  ⟫
+
+                 zc12 :  {z : Ordinal} → OD.def (od pchainp) z → OD.def (od pchainpx) z
+                 zc12 {z} ⟪ az , ch-init fc ⟫ = case1 ⟪ az , ch-init fc ⟫ 
+                 zc12 {z} ⟪ az , ch-is-sup u1 u1<x u1-is-sup fc ⟫ = ?
+
+                 zc13 :  {z : Ordinal} → OD.def (od pchainpx) z → OD.def (od pchainp) z
+                 zc13 {z} (case1 ⟪ az , ch-init fc ⟫ ) = ⟪ az , ch-init fc ⟫ 
+                 zc13 {z} (case1 ⟪ az , ch-is-sup u1 u1<x u1-is-sup fc ⟫ ) = ⟪ az , ch-is-sup u1 (ordtrans u1<x (pxo<x op)) ?  ?  ⟫
+                 zc13 {z} (case2 fc) = ⟪ ? , ch-is-sup ? ? ?  ?  ⟫
+
+                 record STMP {z : Ordinal} (z≤x : z o≤ x ) : Set (Level.suc n) where
+                     field
+                         tsup : SUP A (UnionCF A f mf ay supf1 z)
+                         tsup=sup : supf1 z ≡ & (SUP.sup tsup ) 
+
+                 sup : {z : Ordinal} → (z≤x : z o≤ x ) → STMP z≤x
+                 sup {z} z≤x with trio< z px 
+                 ... | tri< a ¬b ¬c = record { tsup = ? ; tsup=sup = ? }
+                 ... | tri≈ ¬a b ¬c = record { tsup = ?  ; tsup=sup = ? }
+                 ... | tri> ¬a ¬b px<z = record { tsup = ? ; tsup=sup = ? }
 
           ... | case2 px<spfx = record { supf = supf0 ;  asupf = ZChain.asupf zc ; sup = λ lt → STMP.tsup (sup lt ) ; supf-mono = supf-mono 
               ; supf-< = ? ; sup=u = sup=u ; supf-is-sup = λ lt → STMP.tsup=sup (sup lt) }  where
@@ -832,6 +859,11 @@
                  zc10 :  {z : Ordinal} → OD.def (od pchain) z → OD.def (od pchain1) z
                  zc10 {z} ⟪ az , ch-init fc ⟫ = ⟪ az , ch-init fc ⟫ 
                  zc10 {z} ⟪ az , ch-is-sup u1 u1<x u1-is-sup fc ⟫ = ⟪ az , ch-is-sup u1 (ordtrans u1<x (pxo<x op)) ?  ?  ⟫
+
+                 zc111 : {z : Ordinal} → z o< px → OD.def (od pchain1) z → OD.def (od pchain) z 
+                 zc111 {z} z<px ⟪ az , ch-init fc ⟫ = ⟪ az , ch-init fc ⟫ 
+                 zc111 {z} z<px ⟪ az , ch-is-sup u1 u1<x u1-is-sup fc ⟫ = ⟪ az , ch-is-sup u1 (ordtrans u1<x ?) ?  ?  ⟫
+
                  zc11 : (¬ xSUP (UnionCF A f mf ay supf0 px) x ) ∨  (HasPrev A pchain x f )
                         → {z : Ordinal} → OD.def (od pchain1) z → OD.def (od pchain) z ∨ ( (supf0 px ≡ px) ∧ FClosure A f px z )
                  zc11 P {z} ⟪ az , ch-init fc ⟫ = case1 ⟪ az , ch-init fc ⟫