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

comparison src/zorn.agda @ 726:b2e2cd12e38f

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
psupf-mono and is-max conflict
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 18 Jul 2022 15:30:35 +0900
parents 3c42f0441bbc
children 322dd6569072
comparison
equal deleted inserted replaced
725:3c42f0441bbc 726:b2e2cd12e38f
677 pa : odef (UnionCF A f mf ay (ZChain.supf zc) (Oprev.oprev op)) a 677 pa : odef (UnionCF A f mf ay (ZChain.supf zc) (Oprev.oprev op)) a
678 pa = chain-x z19 za 678 pa = chain-x z19 za
679 sup1 : {z : Ordinal} → odef (UnionCF A f mf ay (ZChain.supf zc) (Oprev.oprev op)) z → (z ≡ b) ∨ (z << b) 679 sup1 : {z : Ordinal} → odef (UnionCF A f mf ay (ZChain.supf zc) (Oprev.oprev op)) z → (z ≡ b) ∨ (z << b)
680 sup1 {z} uz = IsSup.x<sup b=sup ( chain-mono uz ) 680 sup1 {z} uz = IsSup.x<sup b=sup ( chain-mono uz )
681 ... | no op = zc5 where 681 ... | no op = zc5 where
682
682 pzc : (z : Ordinal) → z o< x → ZChain A f mf ay z 683 pzc : (z : Ordinal) → z o< x → ZChain A f mf ay z
683 pzc z z<x = prev z z<x 684 pzc z z<x = prev z z<x
685
684 psupf0 : (z : Ordinal) → Ordinal 686 psupf0 : (z : Ordinal) → Ordinal
685 psupf0 z with trio< z x 687 psupf0 z with trio< z x
686 ... | tri< a ¬b ¬c = ZChain.supf (pzc z a) z 688 ... | tri< a ¬b ¬c = ZChain.supf (pzc z a) z
687 ... | tri≈ ¬a b ¬c = y 689 ... | tri≈ ¬a b ¬c = y
688 ... | tri> ¬a ¬b c = y 690 ... | tri> ¬a ¬b c = y
691
689 pchain : HOD 692 pchain : HOD
690 pchain = UnionCF A f mf ay psupf0 x 693 pchain = UnionCF A f mf ay psupf0 x
694
695 psupf0=pzc : {z : Ordinal} → (z<x : z o< x) → psupf0 z ≡ ZChain.supf (pzc z z<x) z
696 psupf0=pzc {z} z<x with trio< z x
697 ... | tri≈ ¬a b ¬c = ⊥-elim (¬a z<x)
698 ... | tri> ¬a ¬b c = ⊥-elim (¬a z<x)
699 ... | tri< a ¬b ¬c with o<-irr z<x a
700 ... | refl = refl
701
702 psupf-mono : {z x1 : Ordinal} → (z<x1 : z o< x1) → x1 o≤ x → psupf0 z ≡ ZChain.supf (pzc z z<x1) z
703 psupf-mono {z} z<x1 x1≤x =?
704
691 ptotal : IsTotalOrderSet pchain 705 ptotal : IsTotalOrderSet pchain
692 ptotal {a} {b} ca cb = subst₂ (λ j k → Tri (j < k) (j ≡ k) (k < j)) *iso *iso uz01 where 706 ptotal {a} {b} ca cb = subst₂ (λ j k → Tri (j < k) (j ≡ k) (k < j)) *iso *iso uz01 where
693 uz01 : Tri (* (& a) < * (& b)) (* (& a) ≡ * (& b)) (* (& b) < * (& a) ) 707 uz01 : Tri (* (& a) < * (& b)) (* (& a) ≡ * (& b)) (* (& b) < * (& a) )
694 uz01 = chain-total A f mf ay psupf0 (UChain.uchain (proj2 ca)) (UChain.uchain (proj2 cb)) 708 uz01 = chain-total A f mf ay psupf0 (UChain.uchain (proj2 ca)) (UChain.uchain (proj2 cb))
695 709
755 → odef (UnionCF A f mf ay (ZChain.supf (prev (osuc b) ob<x))(osuc b)) b → odef pchain b 769 → odef (UnionCF A f mf ay (ZChain.supf (prev (osuc b) ob<x))(osuc b)) b → odef pchain b
756 uzc-mono {b} {ob<x} ⟪ ab , record { u = x=0 ; u<x = u<x ; uchain = ch-init .b fc } ⟫ = 770 uzc-mono {b} {ob<x} ⟪ ab , record { u = x=0 ; u<x = u<x ; uchain = ch-init .b fc } ⟫ =
757 ⟪ ab , record { u = x=0 ; u<x = case2 refl ; uchain = ch-init b fc } ⟫ 771 ⟪ ab , record { u = x=0 ; u<x = case2 refl ; uchain = ch-init b fc } ⟫
758 uzc-mono {b} {ob<x} ⟪ ab , record { u = u ; u<x = case2 x=0 ; uchain = ch-is-sup is-sup fc } ⟫ = ? 772 uzc-mono {b} {ob<x} ⟪ ab , record { u = u ; u<x = case2 x=0 ; uchain = ch-is-sup is-sup fc } ⟫ = ?
759 uzc-mono {b} {ob<x} ⟪ ab , record { u = u ; u<x = case1 u<x ; uchain = ch-is-sup is-sup fc } ⟫ = 773 uzc-mono {b} {ob<x} ⟪ ab , record { u = u ; u<x = case1 u<x ; uchain = ch-is-sup is-sup fc } ⟫ =
760 ⟪ ab , record { u = u ; u<x = case1 (ordtrans u<x ob<x) ; uchain = ch-is-sup uzc00 (fc-conv {b} {u} {ZChain.supf (prev (osuc b) ob<x)} {psupf0} uzc01 fc) } ⟫ where 774 ⟪ ab , record { u = u ; u<x = case1 (ordtrans u<x ob<x) ; uchain = ch-is-sup uzc00
775 (fc-conv {b} {u} {ZChain.supf (prev (osuc b) ob<x)} {psupf0} uzc01 fc) } ⟫ where
761 uzc01 : ZChain.supf (prev (osuc b) ob<x) u ≡ psupf0 u 776 uzc01 : ZChain.supf (prev (osuc b) ob<x) u ≡ psupf0 u
762 uzc01 = ? 777 uzc01 = ? -- trans (sym (psupf0=pzc (ordtrans u<x ob<x ) )) ?
763 uzc00 : ChainP A f mf ay psupf0 u b 778 uzc00 : ChainP A f mf ay psupf0 u b
764 uzc00 = ? 779 uzc00 = ?
765 780
766 781
767 zc5 : ZChain A f mf ay x 782 zc5 : ZChain A f mf ay x