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

comparison src/zorn.agda @ 864:06f692bf7a97

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, 10 Sep 2022 02:35:23 +0900
parents f5fc3f5f618f
children b095c84310df
comparison
equal deleted inserted replaced
863:f5fc3f5f618f 864:06f692bf7a97
778 ; sup=u = sup=u ; supf-is-sup = λ lt → STMP.tsup=sup (sup lt) ; csupf = csupf } where 778 ; sup=u = sup=u ; supf-is-sup = λ lt → STMP.tsup=sup (sup lt) ; csupf = csupf } where
779 zc10 : {z : Ordinal} → OD.def (od pchain) z → OD.def (od pchain1) z 779 zc10 : {z : Ordinal} → OD.def (od pchain) z → OD.def (od pchain1) z
780 zc10 {z} ⟪ az , ch-init fc ⟫ = ⟪ az , ch-init fc ⟫ 780 zc10 {z} ⟪ az , ch-init fc ⟫ = ⟪ az , ch-init fc ⟫
781 zc10 {z} ⟪ az , ch-is-sup u1 u1<x u1-is-sup fc ⟫ = ⟪ az , ch-is-sup u1 (ordtrans u1<x (pxo<x op)) u1-is-sup fc ⟫ 781 zc10 {z} ⟪ az , ch-is-sup u1 u1<x u1-is-sup fc ⟫ = ⟪ az , ch-is-sup u1 (ordtrans u1<x (pxo<x op)) u1-is-sup fc ⟫
782 zc11 : (¬ xSUP (UnionCF A f mf ay supf0 px) x ) ∨ (HasPrev A pchain x f ) 782 zc11 : (¬ xSUP (UnionCF A f mf ay supf0 px) x ) ∨ (HasPrev A pchain x f )
783 → {z : Ordinal} → OD.def (od pchain1) z → OD.def (od pchain) z ∨ ( supf0 px ≡ px ) 783 → {z : Ordinal} → OD.def (od pchain1) z → OD.def (od pchain) z ∨ ( (supf0 px ≡ px) ∧ FClosure A f px z )
784 zc11 P {z} ⟪ az , ch-init fc ⟫ = case1 ⟪ az , ch-init fc ⟫ 784 zc11 P {z} ⟪ az , ch-init fc ⟫ = case1 ⟪ az , ch-init fc ⟫
785 zc11 P {z} ⟪ az , ch-is-sup u1 u1<x u1-is-sup fc ⟫ with trio< u1 px 785 zc11 P {z} ⟪ az , ch-is-sup u1 u1<x u1-is-sup fc ⟫ with trio< u1 px
786 ... | tri< u1<px ¬b ¬c = case1 ⟪ az , ch-is-sup u1 u1<px u1-is-sup fc ⟫ 786 ... | tri< u1<px ¬b ¬c = case1 ⟪ az , ch-is-sup u1 u1<px u1-is-sup fc ⟫
787 ... | tri≈ ¬a eq ¬c = case2 (subst (λ k → supf0 k ≡ k) eq s1u=u) where 787 ... | tri≈ ¬a eq ¬c = case2 ⟪ subst (λ k → supf0 k ≡ k) eq s1u=u , subst (λ k → FClosure A f k z) zc12 fc ⟫ where
788 s1u=u : supf0 u1 ≡ u1 788 s1u=u : supf0 u1 ≡ u1
789 s1u=u = ChainP.supu=u u1-is-sup 789 s1u=u = ChainP.supu=u u1-is-sup
790 zc12 : supf0 u1 ≡ px
791 zc12 = trans (ChainP.supu=u u1-is-sup) eq
790 zc11 (case1 ¬sp=x) {z} ⟪ az , ch-is-sup u1 u1<x u1-is-sup fc ⟫ | tri> ¬a ¬b px<u = ⊥-elim (¬sp=x zcsup) where 792 zc11 (case1 ¬sp=x) {z} ⟪ az , ch-is-sup u1 u1<x u1-is-sup fc ⟫ | tri> ¬a ¬b px<u = ⊥-elim (¬sp=x zcsup) where
791 eq : u1 ≡ x 793 eq : u1 ≡ x
792 eq with trio< u1 x 794 eq with trio< u1 x
793 ... | tri< a ¬b ¬c = ⊥-elim ( ¬p<x<op ⟪ px<u , subst (λ k → u1 o< k ) (sym (Oprev.oprev=x op )) a ⟫ ) 795 ... | tri< a ¬b ¬c = ⊥-elim ( ¬p<x<op ⟪ px<u , subst (λ k → u1 o< k ) (sym (Oprev.oprev=x op )) a ⟫ )
794 ... | tri≈ ¬a b ¬c = b 796 ... | tri≈ ¬a b ¬c = b
813 zc12 : supf0 x ≡ u1 815 zc12 : supf0 x ≡ u1
814 zc12 = subst (λ k → supf0 k ≡ u1) eq (ChainP.supu=u u1-is-sup) 816 zc12 = subst (λ k → supf0 k ≡ u1) eq (ChainP.supu=u u1-is-sup)
815 zcsup : xSUP (UnionCF A f mf ay supf0 px) x 817 zcsup : xSUP (UnionCF A f mf ay supf0 px) x
816 zcsup = record { ax = subst (λ k → odef A k) (trans zc12 eq) (supf∈A o≤-refl) 818 zcsup = record { ax = subst (λ k → odef A k) (trans zc12 eq) (supf∈A o≤-refl)
817 ; is-sup = record { x<sup = x<sup } } 819 ; is-sup = record { x<sup = x<sup } }
818 zc11 (case2 hp) {z} ⟪ az , ch-is-sup u1 u1≤x u1-is-sup fc ⟫ | tri> ¬a ¬b px<u = case1 (zc20 fc ) where 820 zc11 (case2 hp) {z} ⟪ az , ch-is-sup u1 u1<x u1-is-sup fc ⟫ | tri> ¬a ¬b px<u = case1 (zc20 fc ) where
819 eq : u1 ≡ x 821 eq : u1 ≡ x
820 eq = ? 822 eq with trio< u1 x
823 ... | tri< a ¬b ¬c = ⊥-elim ( ¬p<x<op ⟪ px<u , subst (λ k → u1 o< k ) (sym (Oprev.oprev=x op )) a ⟫ )
824 ... | tri≈ ¬a b ¬c = b
825 ... | tri> ¬a ¬b c = ⊥-elim ( o<> u1<x c )
821 zc20 : {z : Ordinal} → FClosure A f (supf0 u1) z → OD.def (od pchain) z 826 zc20 : {z : Ordinal} → FClosure A f (supf0 u1) z → OD.def (od pchain) z
822 zc20 {z} (init asu su=z ) = zc13 where 827 zc20 {z} (init asu su=z ) = zc13 where
823 zc14 : x ≡ z 828 zc14 : x ≡ z
824 zc14 = begin 829 zc14 = begin
825 x ≡⟨ sym eq ⟩ 830 x ≡⟨ sym eq ⟩
842 zc30 : z ≡ x 847 zc30 : z ≡ x
843 zc30 with osuc-≡< z≤x 848 zc30 with osuc-≡< z≤x
844 ... | case1 eq = eq 849 ... | case1 eq = eq
845 ... | case2 z<x = ⊥-elim (¬p<x<op ⟪ px<z , subst (λ k → z o< k ) (sym (Oprev.oprev=x op)) z<x ⟫ ) 850 ... | case2 z<x = ⊥-elim (¬p<x<op ⟪ px<z , subst (λ k → z o< k ) (sym (Oprev.oprev=x op)) z<x ⟫ )
846 zc34 : {w : HOD} → UnionCF A f mf ay supf0 z ∋ w → (w ≡ SUP.sup zc32) ∨ (w < SUP.sup zc32) 851 zc34 : {w : HOD} → UnionCF A f mf ay supf0 z ∋ w → (w ≡ SUP.sup zc32) ∨ (w < SUP.sup zc32)
847 zc34 {w} lt = SUP.x<sup zc32 ? where 852 zc34 {w} lt with zc11 P (subst (λ k → odef (UnionCF A f mf ay supf0 k) (& w)) zc30 lt)
848 zc35 : odef (UnionCF A f mf ay supf0 x) (& w) 853 ... | case1 lt = SUP.x<sup zc32 lt
849 zc35 = subst (λ k → odef (UnionCF A f mf ay supf0 k) (& w)) zc30 lt 854 ... | case2 P = ?
855 -- FClosure A f px z
856 -- where
857 -- zc35 : odef (UnionCF A f mf ay supf0 x) (& w)
858 -- zc35 =
850 zc33 : supf0 z ≡ & (SUP.sup zc32) 859 zc33 : supf0 z ≡ & (SUP.sup zc32)
851 zc33 = trans (sym (supfx (o≤-refl0 (sym zc30)))) ( ZChain.supf-is-sup zc o≤-refl ) 860 zc33 = trans (sym (supfx (o≤-refl0 (sym zc30)))) ( ZChain.supf-is-sup zc o≤-refl )
852 sup=u : {b : Ordinal} (ab : odef A b) → 861 sup=u : {b : Ordinal} (ab : odef A b) →
853 b o≤ x → IsSup A (UnionCF A f mf ay supf0 b) ab ∧ (¬ HasPrev A (UnionCF A f mf ay supf0 b) b f ) → supf0 b ≡ b 862 b o≤ x → IsSup A (UnionCF A f mf ay supf0 b) ab ∧ (¬ HasPrev A (UnionCF A f mf ay supf0 b) b f ) → supf0 b ≡ b
854 sup=u {b} ab b≤x is-sup with trio< b px 863 sup=u {b} ab b≤x is-sup with trio< b px