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

changeset 898:37ddab37e189

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, 06 Oct 2022 18:59:44 +0900
parents f52c610cca06
children 37a09244cebd
files src/zorn.agda
diffstat 1 files changed, 4 insertions(+), 0 deletions(-) [+]
line wrap: on
line diff
--- a/src/zorn.agda	Thu Oct 06 18:44:18 2022 +0900
+++ b/src/zorn.agda	Thu Oct 06 18:59:44 2022 +0900
@@ -676,6 +676,10 @@
               ... | case2 lt = lt
               ... | case1 eq = ⊥-elim ( <-irr (case1 (sym m11)) m12 ) where 
                     ---    supf b ≡ supf x     * ( supf x ) ≤ * a < * b , * (supf x) ≡ * (supf b) ≡ * b
+                    ---    xchain = UnionCF A f mf ay supf x
+                    ---       {y : Ordinal} → odef xchain y → (y ≡ b ) ∨ (y < * b )
+                    ---     supf x ∈ xchian → ok
+                    ---   ¬ supf x ∈ xchian → ⊥ 
                     m10 : {a : Ordinal} → odef  (UnionCF A f mf ay supf x) a  → * ( supf x ) ≤ * a
                     m10 {a} ⟪ ua , ch-init fc ⟫ = ?
                     m10 {a} ⟪ ua , ch-is-sup u u<x is-sup fc ⟫ = ?