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

comparison src/zorn.agda @ 716:b0cad3ec7da0

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 Fri, 15 Jul 2022 21:39:32 +0900
parents e4587714c376
children d76047a8a89b 6c9fed204440
comparison
equal deleted inserted replaced
715:e4587714c376 716:b0cad3ec7da0
495 HasPrev A (UnionCF A f mf ay isupf o∅) ab f ∨ IsSup A (UnionCF A f mf ay isupf o∅) ab → 495 HasPrev A (UnionCF A f mf ay isupf o∅) ab f ∨ IsSup A (UnionCF A f mf ay isupf o∅) ab →
496 * a < * b → odef (UnionCF A f mf ay isupf o∅) b 496 * a < * b → odef (UnionCF A f mf ay isupf o∅) b
497 imax {a} {b} ua b<x ab (case1 hasp) a<b = subst (λ k → odef (UnionCF A f mf ay isupf o∅) k ) (sym (HasPrev.x=fy hasp)) ( inext (HasPrev.ay hasp) ) 497 imax {a} {b} ua b<x ab (case1 hasp) a<b = subst (λ k → odef (UnionCF A f mf ay isupf o∅) k ) (sym (HasPrev.x=fy hasp)) ( inext (HasPrev.ay hasp) )
498 imax {a} {b} ua b<x ab (case2 sup) a<b = ⊥-elim ( ¬x<0 b<x ) 498 imax {a} {b} ua b<x ab (case2 sup) a<b = ⊥-elim ( ¬x<0 b<x )
499 499
500 -- exor-sup : (B : HOD)
501 -- → ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) {y : Ordinal} (ay : odef A y) →
502 -- → {x : Ordinal } (xa : odef A x) → HasPrev A B xa → IsSup A B xa → ⊥
503 -- exor-sup B f mf {y} ay {x} xa hasp is-sup with trio<
504
500 -- 505 --
501 -- create all ZChains under o< x 506 -- create all ZChains under o< x
502 -- 507 --
503 508
504 ind : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) {y : Ordinal} (ay : odef A y) → (x : Ordinal) 509 ind : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) {y : Ordinal} (ay : odef A y) → (x : Ordinal)
617 ... | tri< a ¬b ¬c = ⟪ az , record { u = u ; u<x = case1 a ; uchain = ch-init z fc } ⟫ 622 ... | tri< a ¬b ¬c = ⟪ az , record { u = u ; u<x = case1 a ; uchain = ch-init z fc } ⟫
618 ... | tri≈ ¬a b ¬c = ⟪ az , record { u = u ; u<x = case2 refl ; uchain = ch-init z fc } ⟫ 623 ... | tri≈ ¬a b ¬c = ⟪ az , record { u = u ; u<x = case2 refl ; uchain = ch-init z fc } ⟫
619 ... | tri> ¬a ¬b c = ⊥-elim ( ¬x<0 c ) 624 ... | tri> ¬a ¬b c = ⊥-elim ( ¬x<0 c )
620 zc10 {z} ⟪ az , record { u = u ; u<x = case1 u<x ; uchain = ch-is-sup is-sup fc } ⟫ with trio< u px 625 zc10 {z} ⟪ az , record { u = u ; u<x = case1 u<x ; uchain = ch-is-sup is-sup fc } ⟫ with trio< u px
621 ... | tri< a ¬b ¬c = ⟪ az , record { u = u ; u<x = case1 a ; uchain = ch-is-sup is-sup fc } ⟫ 626 ... | tri< a ¬b ¬c = ⟪ az , record { u = u ; u<x = case1 a ; uchain = ch-is-sup is-sup fc } ⟫
622 ... | tri≈ ¬a b ¬c = ? -- ⊥-elim ( noapx ( subst (λ k → odef A k ) (trans b (sym &iso) ) (ChainP.au is-sup ) ))
623 ... | tri> ¬a ¬b c = ⊥-elim ( ¬p<x<op ⟪ c , subst (λ k → u o< k ) (sym (Oprev.oprev=x op)) u<x ⟫ ) 627 ... | tri> ¬a ¬b c = ⊥-elim ( ¬p<x<op ⟪ c , subst (λ k → u o< k ) (sym (Oprev.oprev=x op)) u<x ⟫ )
628 ... | tri≈ ¬a b ¬c = ? where
629 zc13 : odef (UnionCF A f mf ay (ZChain.supf zc) (Oprev.oprev op)) (HasPrev.y pr)
630 zc13 = HasPrev.ay pr
631 zc12 : ?
632 zc12 with proj1 (mf _ (A∋fcs _ f mf fc ) ) | zc13 -- u is sup and has prev
633 ... | case1 x | ⟪ apz , ach ⟫ = ?
634 ... | case2 x | ⟪ apz , ach ⟫ = ?
624 ... | tri> ¬a ¬b c = ⊥-elim ( ¬p<x<op ⟪ c , subst (λ k → b o< k ) (sym (Oprev.oprev=x op)) b<x ⟫ ) 635 ... | tri> ¬a ¬b c = ⊥-elim ( ¬p<x<op ⟪ c , subst (λ k → b o< k ) (sym (Oprev.oprev=x op)) b<x ⟫ )
625 ... | tri≈ ¬a b=px ¬c = zc15 where 636 ... | tri≈ ¬a b=px ¬c = zc15 where
626 zc14 : f (HasPrev.y pr) ≡ b 637 zc14 : f (HasPrev.y pr) ≡ b
627 zc14 = begin f (HasPrev.y pr) ≡⟨ sym (HasPrev.x=fy pr) ⟩ 638 zc14 = begin f (HasPrev.y pr) ≡⟨ sym (HasPrev.x=fy pr) ⟩
628 & (* px) ≡⟨ &iso ⟩ 639 & (* px) ≡⟨ &iso ⟩