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

changeset 1084:7ec55b1bdfc2

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Zorn done
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 18 Dec 2022 02:04:45 +0900
parents 424af168622f
children a92aacd3d83a
files src/zorn.agda
diffstat 1 files changed, 1 insertions(+), 5 deletions(-) [+]
line wrap: on
line diff
--- a/src/zorn.agda	Sat Dec 17 21:20:49 2022 +0900
+++ b/src/zorn.agda	Sun Dec 18 02:04:45 2022 +0900
@@ -1349,11 +1349,7 @@
           IC⊆ : {a b : Ordinal } (ia : IChain ay supfz a ) (ib : IChain ay supfz b )
               → IChain-i ia o< IChain-i ib → odef (ZChain.chain (pzc (pic<x ib))) a
           IC⊆ {a} {b} (ic-init fc ) ib ia<ib = ⟪ A∋fc _ f mf fc , ch-init fc ⟫
-          IC⊆ {a} {b} (ic-isup i i<x sa<x fc ) (ic-init fcb ) ia<ib = ⊥-elim ( o<> ia<ib ic01 ) where
-               ic02 : o∅ o< supfz i<x
-               ic02 = ?
-               ic01 : o∅ o< i
-               ic01 = ordtrans<-≤ ic02 sa<x
+          IC⊆ {a} {b} (ic-isup i i<x sa<x fc ) (ic-init fcb ) ia<ib = ⊥-elim ( ¬x<0 ia<ib  )
           IC⊆ {a} {b} (ic-isup i i<x sa<x fc ) (ic-isup j j<x sb<x fcb ) ia<ib
               = ZChain.cfcs (pzc (ob<x lim j<x) ) (o<→≤ ia<ib) o≤-refl (OrdTrans (ZChain.supf-mono (pzc (ob<x lim j<x)) (o<→≤ ia<ib)) sb<x)
                   (subst (λ k → FClosure A f k a) (zeq _ _ (osucc (o<→≤ ia<ib)) (o<→≤ <-osuc)) fc )