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

comparison src/zorn.agda @ 720:6c9fed204440

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 Sat, 16 Jul 2022 00:45:38 +0900
parents b0cad3ec7da0
children 562ddd33fe21
comparison
equal deleted inserted replaced
716:b0cad3ec7da0 720:6c9fed204440
626 ... | 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 } ⟫
627 ... | 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 628 ... | tri≈ ¬a b ¬c = ? where
629 zc13 : odef (UnionCF A f mf ay (ZChain.supf zc) (Oprev.oprev op)) (HasPrev.y pr) 629 zc13 : odef (UnionCF A f mf ay (ZChain.supf zc) (Oprev.oprev op)) (HasPrev.y pr)
630 zc13 = HasPrev.ay 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 ⟫ = ?
635 ... | tri> ¬a ¬b c = ⊥-elim ( ¬p<x<op ⟪ c , subst (λ k → b o< k ) (sym (Oprev.oprev=x op)) b<x ⟫ ) 631 ... | tri> ¬a ¬b c = ⊥-elim ( ¬p<x<op ⟪ c , subst (λ k → b o< k ) (sym (Oprev.oprev=x op)) b<x ⟫ )
636 ... | tri≈ ¬a b=px ¬c = zc15 where 632 ... | tri≈ ¬a b=px ¬c = zc15 where
637 zc14 : f (HasPrev.y pr) ≡ b 633 zc14 : f (HasPrev.y pr) ≡ b
638 zc14 = begin f (HasPrev.y pr) ≡⟨ sym (HasPrev.x=fy pr) ⟩ 634 zc14 = begin f (HasPrev.y pr) ≡⟨ sym (HasPrev.x=fy pr) ⟩
639 & (* px) ≡⟨ &iso ⟩ 635 & (* px) ≡⟨ &iso ⟩
664 ... | case2 ¬x=sup = no-extenion z18 where -- px is not f y' nor sup of former ZChain from y -- no extention 660 ... | case2 ¬x=sup = no-extenion z18 where -- px is not f y' nor sup of former ZChain from y -- no extention
665 z18 : {a b : Ordinal} → odef pchain a → b o< x → (ab : odef A b) → 661 z18 : {a b : Ordinal} → odef pchain a → b o< x → (ab : odef A b) →
666 HasPrev A pchain ab f ∨ IsSup A pchain ab → 662 HasPrev A pchain ab f ∨ IsSup A pchain ab →
667 * a < * b → odef pchain b 663 * a < * b → odef pchain b
668 z18 {a} {b} za b<x ab P a<b with trio< b px 664 z18 {a} {b} za b<x ab P a<b with trio< b px
669 ... | tri< lt ¬b ¬c = zcp za (chain-≡ ? ) lt ab P a<b 665 ... | tri< lt ¬b ¬c = ? where
666 z20 : odef pchain b
667 z20 = chain-mono ( ZChain.is-max zc ? lt ab ? a<b )
670 ... | tri> ¬a ¬b c = ⊥-elim ( ¬p<x<op ⟪ c , subst (λ k → b o< k ) (sym (Oprev.oprev=x op)) b<x ⟫ ) 668 ... | tri> ¬a ¬b c = ⊥-elim ( ¬p<x<op ⟪ c , subst (λ k → b o< k ) (sym (Oprev.oprev=x op)) b<x ⟫ )
671 ... | tri≈ ¬a b=px ¬c with P 669 ... | tri≈ ¬a b=px ¬c with P
672 ... | case1 pr = subst (λ k → odef pchain k ) (sym (HasPrev.x=fy pr)) ( pnext (HasPrev.ay pr) ) 670 ... | case1 pr = subst (λ k → odef pchain k ) (sym (HasPrev.x=fy pr)) ( pnext (HasPrev.ay pr) )
673 ... | case2 b=sup = ⊥-elim ( ¬x=sup record { 671 ... | case2 b=sup = ⊥-elim ( ¬x=sup record {
674 x<sup = λ {y} zy → subst (λ k → (y ≡ k) ∨ (y << k)) (trans b=px (sym &iso)) 672 x<sup = λ {y} zy → subst (λ k → (y ≡ k) ∨ (y << k)) (trans b=px (sym &iso))