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

changeset 915:8695050933a7

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 Wed, 12 Oct 2022 20:49:21 +0900
parents 3105feb3c4e1
children f0b98f57ec65
files src/zorn.agda
diffstat 1 files changed, 8 insertions(+), 0 deletions(-) [+]
line wrap: on
line diff
--- a/src/zorn.agda	Wed Oct 12 11:11:42 2022 +0900
+++ b/src/zorn.agda	Wed Oct 12 20:49:21 2022 +0900
@@ -456,6 +456,14 @@
 
    -- ordering is not proved here but in ZChain1 
 
+   csupf< : {a b : Ordinal } → a o≤ b → odef (UnionCF A f mf ay supf z) (supf b) → odef (UnionCF A f mf ay supf z) (supf a) 
+   csupf< {a} {b} a≤b ⟪ as , ch-init fc ⟫ = ⟪ ? , ch-init ?  ⟫ 
+   csupf< {a} {b} a≤b ⟪ as , ch-is-sup u u<x is-sup fc ⟫ = ⟪ ? , ch-is-sup (supf a) uz01 ? ? ⟫ where
+       a≤u : ?
+       a≤u = ?
+       uz01 : supf a o< z
+       uz01 = ordtrans≤-< (subst (λ k → supf a o< k) (cong osuc (ChainP.supu=u is-sup)) (supf-mono a≤u )) u<x
+
 record ZChain1 ( A : HOD )    ( f : Ordinal → Ordinal )  (mf : ≤-monotonic-f A f) 
         {y : Ordinal} (ay : odef A y)  (zc : ZChain A f mf ay (& A)) ( z : Ordinal ) : Set (Level.suc n) where
    supf = ZChain.supf zc