Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 873:27bab3f65064
...
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 ⟫