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

comparison src/zorn.agda @ 747:c35a5001a0f8

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
initial chain separation
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Thu, 21 Jul 2022 13:20:04 +0900
parents 4a3ba4ad59d4
children 6c8ba542d11b
comparison
equal deleted inserted replaced
746:4a3ba4ad59d4 747:c35a5001a0f8
672 ; initial = pinit ; chain∋init = pcy ; sup=u = sup=u 672 ; initial = pinit ; chain∋init = pcy ; sup=u = sup=u
673 ; chain⊆A = pchain⊆A ; f-next = pnext ; f-total = ptotal ; order = order } where 673 ; chain⊆A = pchain⊆A ; f-next = pnext ; f-total = ptotal ; order = order } where
674 sup=u : {b : Ordinal} {ab : odef A b} → b o< x 674 sup=u : {b : Ordinal} {ab : odef A b} → b o< x
675 → IsSup A (UnionCF A f mf ay supf0 x) ab 675 → IsSup A (UnionCF A f mf ay supf0 x) ab
676 → supf0 b ≡ b 676 → supf0 b ≡ b
677 sup=u {b} b<x is-sup with trio< b px 677 sup=u {b} {ab} b<x is-sup with trio< b px
678 ... | tri< a ¬b ¬c = ZChain.sup=u zc a ? 678 ... | tri< a ¬b ¬c = ZChain.sup=u zc {b} {ab} a record { x<sup = pc20 } where
679 pc20 : {z : Ordinal} → odef (UnionCF A f mf ay (ZChain.supf zc) (Oprev.oprev op)) z → (z ≡ b) ∨ (z << b)
680 pc20 {z} ⟪ az , record { u = u0 ; u<x = u<x ; uchain = ch-init _ fc } ⟫ =
681 IsSup.x<sup is-sup ⟪ az , record { u = u0 ; u<x = case2 refl ; uchain = ch-init _ fc } ⟫
682 pc20 {z} ⟪ az , record { u = u0 ; u<x = u<x ; uchain = ch-is-sup is-sup-c fc } ⟫ with u<x
683 ... | case2 u=0 = ?
684 ... | case1 u<px = IsSup.x<sup is-sup ⟪ az , record { u = u0
685 ; u<x = case1 (subst (λ k → u0 o< k) (Oprev.oprev=x op) (ordtrans u<px <-osuc))
686 ; uchain = ch-is-sup is-sup-c fc } ⟫
679 ... | tri≈ ¬a refl ¬c = ? 687 ... | tri≈ ¬a refl ¬c = ?
680 ... | tri> ¬a ¬b c = ⊥-elim ( ¬p<x<op ⟪ c , subst (λ k → b o< k ) (sym (Oprev.oprev=x op)) b<x ⟫ ) 688 ... | tri> ¬a ¬b c = ⊥-elim ( ¬p<x<op ⟪ c , subst (λ k → b o< k ) (sym (Oprev.oprev=x op)) b<x ⟫ )
681 order : {b sup1 z1 : Ordinal} → b o< x → sup1 o< b → FClosure A f (supf0 sup1) z1 → z1 << supf0 b 689 order : {b sup1 z1 : Ordinal} → b o< x → sup1 o< b → FClosure A f (supf0 sup1) z1 → z1 << supf0 b
682 order {b} {s} {z1} b<x s<b fc with trio< b px 690 order {b} {s} {z1} b<x s<b fc with trio< b px
683 ... | tri< a ¬b ¬c = ZChain.order zc a s<b fc 691 ... | tri< a ¬b ¬c = ZChain.order zc a s<b fc