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

comparison src/zorn.agda @ 715:e4587714c376

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 14:14:53 +0900
parents e1ef5e6961ce
children b0cad3ec7da0
comparison
equal deleted inserted replaced
714:e1ef5e6961ce 715:e4587714c376
619 ... | tri> ¬a ¬b c = ⊥-elim ( ¬x<0 c ) 619 ... | 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 620 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 } ⟫ 621 ... | 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 ) )) 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 ⟫ ) 623 ... | tri> ¬a ¬b c = ⊥-elim ( ¬p<x<op ⟪ c , subst (λ k → u o< k ) (sym (Oprev.oprev=x op)) u<x ⟫ )
624 ... | tri≈ ¬a b=px ¬c = ? -- ⊥-elim ( noapx (subst (λ k → odef A k ) (trans b=px (sym &iso)) ab ) )
625 ... | tri> ¬a ¬b c = ⊥-elim ( ¬p<x<op ⟪ c , subst (λ k → b o< k ) (sym (Oprev.oprev=x op)) b<x ⟫ ) 624 ... | tri> ¬a ¬b c = ⊥-elim ( ¬p<x<op ⟪ c , subst (λ k → b o< k ) (sym (Oprev.oprev=x op)) b<x ⟫ )
626 -- subst (λ k → odef chain0 k ) (trans (sym (HasPrev.x=fy pr )) (trans &iso (sym b=x)) ) ( ZChain.f-next zc (HasPrev.ay pr)) 625 ... | tri≈ ¬a b=px ¬c = zc15 where
626 zc14 : f (HasPrev.y pr) ≡ b
627 zc14 = begin f (HasPrev.y pr) ≡⟨ sym (HasPrev.x=fy pr) ⟩
628 & (* px) ≡⟨ &iso ⟩
629 px ≡⟨ sym b=px ⟩
630 b ∎ where open ≡-Reasoning
631 zc15 : odef pchain b
632 zc15 with ZChain.f-next zc (HasPrev.ay pr)
633 ... | ⟪ az , record { u = u ; u<x = case2 refl ; uchain = ch-init z fc } ⟫
634 = ⟪ subst (λ k → odef A k ) zc14 az , record { u = u ; u<x = case2 refl
635 ; uchain = ch-init _ (subst (λ k → FClosure A f y k ) zc14 fc) } ⟫
636 ... | ⟪ az , record { u = u ; u<x = case1 u<x ; uchain = ch-init z fc } ⟫
637 = ⟪ subst (λ k → odef A k ) zc14 az , record { u = u ; u<x = case1 (b<x→0<x b<x )
638 ; uchain = ch-init _ (subst (λ k → FClosure A f y k ) zc14 fc) } ⟫
627 ... | case2 ¬fy<x with ODC.p∨¬p O (IsSup A (ZChain.chain zc ) apx ) 639 ... | case2 ¬fy<x with ODC.p∨¬p O (IsSup A (ZChain.chain zc ) apx )
628 ... | case1 is-sup = -- x is a sup of zc 640 ... | case1 is-sup = -- x is a sup of zc
629 record { chain⊆A = pchain⊆A ; f-next = pnext ; f-total = ptotal 641 record { chain⊆A = pchain⊆A ; f-next = pnext ; f-total = ptotal
630 ; initial = pinit ; chain∋init = pcy ; is-max = p-ismax } where 642 ; initial = pinit ; chain∋init = pcy ; is-max = p-ismax } where
631 p-ismax : {a b : Ordinal} → odef pchain a → 643 p-ismax : {a b : Ordinal} → odef pchain a →