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

comparison src/zorn.agda @ 824:8a06fe74721b

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
sp1 on supf1 px
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Thu, 18 Aug 2022 14:11:58 +0900
parents 497b5db603e7
children eec82adba99b
comparison
equal deleted inserted replaced
823:497b5db603e7 824:8a06fe74721b
670 sup1 = supP pchain pchain⊆A ptotal 670 sup1 = supP pchain pchain⊆A ptotal
671 sp1 = & (SUP.sup sup1 ) 671 sp1 = & (SUP.sup sup1 )
672 supf1 : Ordinal → Ordinal 672 supf1 : Ordinal → Ordinal
673 supf1 z with trio< z px 673 supf1 z with trio< z px
674 ... | tri< a ¬b ¬c = ZChain.supf zc z 674 ... | tri< a ¬b ¬c = ZChain.supf zc z
675 ... | tri≈ ¬a b ¬c = ZChain.supf zc z 675 ... | tri≈ ¬a b ¬c = sp1 -- ZChain.supf zc z
676 ... | tri> ¬a ¬b c = ZChain.supf zc px 676 ... | tri> ¬a ¬b c = sp1 -- ZChain.supf zc px
677 677
678 pchain1 : HOD 678 pchain1 : HOD
679 pchain1 = UnionCF A f mf ay supf1 x 679 pchain1 = UnionCF A f mf ay supf1 x
680 pcy1 : odef pchain1 y 680 pcy1 : odef pchain1 y
681 pcy1 = ⟪ ay , ch-init (init ay refl) ⟫ 681 pcy1 = ⟪ ay , ch-init (init ay refl) ⟫
713 fcy<sup {z} fc = subst ( λ k → (z ≡ k) ∨ (z << k )) (sym eq1) ( ChainP.fcy<sup u1-is-sup fc ) 713 fcy<sup {z} fc = subst ( λ k → (z ≡ k) ∨ (z << k )) (sym eq1) ( ChainP.fcy<sup u1-is-sup fc )
714 order : {s : Ordinal} {z2 : Ordinal} → s o< u1 → FClosure A f (supf1 s) z2 → 714 order : {s : Ordinal} {z2 : Ordinal} → s o< u1 → FClosure A f (supf1 s) z2 →
715 (z2 ≡ supf1 u1) ∨ (z2 << supf1 u1) 715 (z2 ≡ supf1 u1) ∨ (z2 << supf1 u1)
716 order {s} {z2} s<u1 fc with trio< s px 716 order {s} {z2} s<u1 fc with trio< s px
717 ... | tri< a ¬b ¬c = subst (λ k → (z2 ≡ k) ∨ (z2 << k) ) (sym eq1) ( ChainP.order u1-is-sup s<u1 fc ) 717 ... | tri< a ¬b ¬c = subst (λ k → (z2 ≡ k) ∨ (z2 << k) ) (sym eq1) ( ChainP.order u1-is-sup s<u1 fc )
718 ... | tri≈ ¬a b ¬c = subst (λ k → (z2 ≡ k) ∨ (z2 << k) ) (sym eq1) ( ChainP.order u1-is-sup s<u1 fc ) 718 ... | tri≈ ¬a b ¬c = subst (λ k → (z2 ≡ k) ∨ (z2 << k) ) (sym eq1) ( ChainP.order u1-is-sup s<u1 ? )
719 ... | tri> ¬a ¬b px<s = ⊥-elim ( o<¬≡ refl (ordtrans px<s (ordtrans s<u1 a) )) -- px o< s < u1 < px 719 ... | tri> ¬a ¬b px<s = ⊥-elim ( o<¬≡ refl (ordtrans px<s (ordtrans s<u1 a) )) -- px o< s < u1 < px
720 ... | tri≈ ¬a b ¬c | record { eq = eq1 } = ⟪ A∋fcs _ f mf fc , ch-is-sup u1 (OrdTrans u1≤x z0≤1 ) 720 ... | tri≈ ¬a b ¬c | record { eq = eq1 } = ⟪ A∋fcs _ f mf fc , ch-is-sup u1 (OrdTrans u1≤x z0≤1 )
721 record { fcy<sup = fcy<sup ; order = order ; supu=u = trans eq1 (ChainP.supu=u u1-is-sup) } (init (subst (λ k → odef A k ) (sym eq1) asp) eq1 ) ⟫ where 721 record { fcy<sup = fcy<sup ; order = order ; supu=u = trans eq1 ? } (init (subst (λ k → odef A k ) (sym eq1) ? ) ? ) ⟫ where
722 fcy<sup : {z : Ordinal} → FClosure A f y z → (z ≡ supf1 u1) ∨ (z << supf1 u1 ) 722 fcy<sup : {z : Ordinal} → FClosure A f y z → (z ≡ supf1 u1) ∨ (z << supf1 u1 )
723 fcy<sup {z} fc = subst ( λ k → (z ≡ k) ∨ (z << k )) (sym eq1) ( ChainP.fcy<sup u1-is-sup fc ) 723 fcy<sup {z} fc = subst ( λ k → (z ≡ k) ∨ (z << k )) (sym eq1) ? -- ( ChainP.fcy<sup u1-is-sup fc )
724 order : {s : Ordinal} {z2 : Ordinal} → s o< u1 → FClosure A f (supf1 s) z2 → 724 order : {s : Ordinal} {z2 : Ordinal} → s o< u1 → FClosure A f (supf1 s) z2 →
725 (z2 ≡ supf1 u1) ∨ (z2 << supf1 u1) 725 (z2 ≡ supf1 u1) ∨ (z2 << supf1 u1)
726 order {s} {z2} s<u1 fc with trio< s px 726 order {s} {z2} s<u1 fc with trio< s px
727 ... | tri< a ¬b ¬c = subst (λ k → (z2 ≡ k) ∨ (z2 << k) ) (sym eq1) ( ChainP.order u1-is-sup s<u1 fc ) 727 ... | tri< a ¬b ¬c = subst (λ k → (z2 ≡ k) ∨ (z2 << k) ) (sym eq1) ? -- ( ChainP.order u1-is-sup s<u1 fc )
728 ... | tri≈ ¬a b ¬c = subst (λ k → (z2 ≡ k) ∨ (z2 << k) ) (sym eq1) ( ChainP.order u1-is-sup s<u1 fc ) 728 ... | tri≈ ¬a b ¬c = subst (λ k → (z2 ≡ k) ∨ (z2 << k) ) (sym eq1) ? -- ( ChainP.order u1-is-sup s<u1 fc )
729 ... | tri> ¬a ¬b px<s = ⊥-elim ( o<¬≡ refl (ordtrans px<s (subst (λ k → s o< k) b s<u1 ) )) -- px o< s < u1 = px 729 ... | tri> ¬a ¬b px<s = ⊥-elim ( o<¬≡ refl (ordtrans px<s (subst (λ k → s o< k) b s<u1 ) )) -- px o< s < u1 = px
730 ... | tri> ¬a ¬b px<u1 | record { eq = eq1 } with osuc-≡< (OrdTrans u1≤x z0≤px) 730 ... | tri> ¬a ¬b px<u1 | record { eq = eq1 } with osuc-≡< (OrdTrans u1≤x z0≤px)
731 ... | case1 eq = ⊥-elim ( o<¬≡ (sym eq) px<u1 ) 731 ... | case1 eq = ⊥-elim ( o<¬≡ (sym eq) px<u1 )
732 ... | case2 lt = ⊥-elim ( o<> lt px<u1 ) 732 ... | case2 lt = ⊥-elim ( o<> lt px<u1 )
733 zc60 (fsuc w1 fc) with zc60 fc 733 zc60 (fsuc w1 fc) with zc60 fc
748 fcy<sup {z} fc = subst ( λ k → (z ≡ k) ∨ (z << k )) eq1 ( ChainP.fcy<sup u1-is-sup fc ) 748 fcy<sup {z} fc = subst ( λ k → (z ≡ k) ∨ (z << k )) eq1 ( ChainP.fcy<sup u1-is-sup fc )
749 order : {s : Ordinal} {z2 : Ordinal} → s o< u1 → FClosure A f (supf0 s) z2 → 749 order : {s : Ordinal} {z2 : Ordinal} → s o< u1 → FClosure A f (supf0 s) z2 →
750 (z2 ≡ supf0 u1) ∨ (z2 << supf0 u1) 750 (z2 ≡ supf0 u1) ∨ (z2 << supf0 u1)
751 order {s} {z2} s<u1 fc with trio< s px | inspect supf1 s 751 order {s} {z2} s<u1 fc with trio< s px | inspect supf1 s
752 ... | tri< a ¬b ¬c | record { eq = eq2 } = subst (λ k → (z2 ≡ k) ∨ (z2 << k) ) eq1 ( ChainP.order u1-is-sup s<u1 (subst (λ k → FClosure A f k z2) (sym eq2) fc )) 752 ... | tri< a ¬b ¬c | record { eq = eq2 } = subst (λ k → (z2 ≡ k) ∨ (z2 << k) ) eq1 ( ChainP.order u1-is-sup s<u1 (subst (λ k → FClosure A f k z2) (sym eq2) fc ))
753 ... | tri≈ ¬a b ¬c | record { eq = eq2 } = subst (λ k → (z2 ≡ k) ∨ (z2 << k) ) eq1 ( ChainP.order u1-is-sup s<u1 (subst (λ k → FClosure A f k z2) (sym eq2) fc )) 753 ... | tri≈ ¬a b ¬c | record { eq = eq2 } = subst (λ k → (z2 ≡ k) ∨ (z2 << k) ) eq1 ( ChainP.order u1-is-sup s<u1 (subst (λ k → FClosure A f k z2) (sym eq2) ? ))
754 ... | tri> ¬a ¬b px<s | record { eq = eq2 } = ⊥-elim ( o<¬≡ refl (ordtrans px<s (ordtrans s<u1 a) )) -- px o< s < u1 < px 754 ... | tri> ¬a ¬b px<s | record { eq = eq2 } = ⊥-elim ( o<¬≡ refl (ordtrans px<s (ordtrans s<u1 a) )) -- px o< s < u1 < px
755 ... | tri≈ ¬a b ¬c | record { eq = eq1 } = ⟪ A∋fcs _ f mf fc , ch-is-sup u1 (OrdTrans u1≤x z0≤1 ) 755 ... | tri≈ ¬a b ¬c | record { eq = eq1 } = ⟪ A∋fcs _ f mf fc , ch-is-sup u1 (OrdTrans u1≤x z0≤1 )
756 record { fcy<sup = fcy<sup ; order = order ; supu=u = trans (sym eq1) (ChainP.supu=u u1-is-sup) } (init asp refl ) ⟫ where 756 record { fcy<sup = fcy<sup ; order = order ; supu=u = trans (sym ? ) (ChainP.supu=u u1-is-sup) } (init ? ? ) ⟫ where
757 fcy<sup : {z : Ordinal} → FClosure A f y z → (z ≡ supf0 u1) ∨ (z << supf0 u1 ) 757 fcy<sup : {z : Ordinal} → FClosure A f y z → (z ≡ supf0 u1) ∨ (z << supf0 u1 )
758 fcy<sup {z} fc = subst ( λ k → (z ≡ k) ∨ (z << k )) eq1 ( ChainP.fcy<sup u1-is-sup fc ) 758 fcy<sup {z} fc = subst ( λ k → (z ≡ k) ∨ (z << k )) ? ( ChainP.fcy<sup u1-is-sup fc )
759 order : {s : Ordinal} {z2 : Ordinal} → s o< u1 → FClosure A f (supf0 s) z2 → 759 order : {s : Ordinal} {z2 : Ordinal} → s o< u1 → FClosure A f (supf0 s) z2 →
760 (z2 ≡ supf0 u1) ∨ (z2 << supf0 u1) 760 (z2 ≡ supf0 u1) ∨ (z2 << supf0 u1)
761 order {s} {z2} s<u1 fc with trio< s px | inspect supf1 s 761 order {s} {z2} s<u1 fc with trio< s px | inspect supf1 s
762 ... | tri< a ¬b ¬c | record { eq = eq2 } = subst (λ k → (z2 ≡ k) ∨ (z2 << k) ) eq1 ( ChainP.order u1-is-sup s<u1 (subst (λ k → FClosure A f k z2) (sym eq2) fc )) 762 ... | tri< a ¬b ¬c | record { eq = eq2 } = subst (λ k → (z2 ≡ k) ∨ (z2 << k) ) ?( ChainP.order u1-is-sup s<u1 (subst (λ k → FClosure A f k z2) (sym eq2) fc ))
763 ... | tri≈ ¬a b ¬c | record { eq = eq2 } = subst (λ k → (z2 ≡ k) ∨ (z2 << k) ) eq1 ( ChainP.order u1-is-sup s<u1 (subst (λ k → FClosure A f k z2) (sym eq2) fc )) 763 ... | tri≈ ¬a b ¬c | record { eq = eq2 } = subst (λ k → (z2 ≡ k) ∨ (z2 << k) ) ? ( ChainP.order u1-is-sup s<u1 (subst (λ k → FClosure A f k z2) (sym eq2) ? ))
764 ... | tri> ¬a ¬b px<s | _ = ⊥-elim ( o<¬≡ refl (ordtrans px<s (subst (λ k → s o< k) b s<u1 ) )) -- px o< s < u1 = px 764 ... | tri> ¬a ¬b px<s | _ = ⊥-elim ( o<¬≡ refl (ordtrans px<s (subst (λ k → s o< k) b s<u1 ) )) -- px o< s < u1 = px
765 ... | tri> ¬a ¬b px<u1 | record { eq = eq1 } with trio< z0 px 765 ... | tri> ¬a ¬b px<u1 | record { eq = eq1 } with trio< z0 px
766 ... | tri< a ¬b ¬c with osuc-≡< (OrdTrans u1≤x (o<→≤ a) ) 766 ... | tri< a ¬b ¬c with osuc-≡< (OrdTrans u1≤x (o<→≤ a) )
767 ... | case1 eq = ⊥-elim ( o<¬≡ (sym eq) px<u1 ) 767 ... | case1 eq = ⊥-elim ( o<¬≡ (sym eq) px<u1 )
768 ... | case2 lt = ⊥-elim ( o<> lt px<u1 ) 768 ... | case2 lt = ⊥-elim ( o<> lt px<u1 )
782 ... | tri> ¬a ¬b px<z = ⊥-elim (¬p<x<op ⟪ px<z , subst (λ k → z o< k ) (sym (Oprev.oprev=x op)) z<x ⟫ ) 782 ... | tri> ¬a ¬b px<z = ⊥-elim (¬p<x<op ⟪ px<z , subst (λ k → z o< k ) (sym (Oprev.oprev=x op)) z<x ⟫ )
783 sup=u : {b : Ordinal} (ab : odef A b) → 783 sup=u : {b : Ordinal} (ab : odef A b) →
784 b o≤ x → IsSup A (UnionCF A f mf ay supf1 b) ab → supf1 b ≡ b 784 b o≤ x → IsSup A (UnionCF A f mf ay supf1 b) ab → supf1 b ≡ b
785 sup=u {b} ab b≤x is-sup with trio< b px 785 sup=u {b} ab b≤x is-sup with trio< b px
786 ... | tri< a ¬b ¬c = ZChain.sup=u zc ab (o<→≤ a) record { x<sup = λ lt → IsSup.x<sup is-sup (UnionCF⊆ o≤-refl (o<→≤ a) lt) } 786 ... | tri< a ¬b ¬c = ZChain.sup=u zc ab (o<→≤ a) record { x<sup = λ lt → IsSup.x<sup is-sup (UnionCF⊆ o≤-refl (o<→≤ a) lt) }
787 ... | tri≈ ¬a b ¬c = ZChain.sup=u zc ab (o≤-refl0 b) record { x<sup = λ lt → IsSup.x<sup is-sup (UnionCF⊆ o≤-refl (o≤-refl0 b) lt) } 787 ... | tri≈ ¬a b ¬c = ? -- ZChain.sup=u zc ab (o≤-refl0 b) record { x<sup = λ lt → IsSup.x<sup is-sup (UnionCF⊆ o≤-refl (o≤-refl0 b) lt) }
788 ... | tri> ¬a ¬b px<b = ⊥-elim (¬sp=x zcsup ) where 788 ... | tri> ¬a ¬b px<b = ⊥-elim (¬sp=x zcsup ) where
789 zc30 : x ≡ b 789 zc30 : x ≡ b
790 zc30 with osuc-≡< b≤x 790 zc30 with osuc-≡< b≤x
791 ... | case1 eq = sym (eq) 791 ... | case1 eq = sym (eq)
792 ... | case2 b<x = ⊥-elim (¬p<x<op ⟪ px<b , subst (λ k → b o< k ) (sym (Oprev.oprev=x op)) b<x ⟫ ) 792 ... | case2 b<x = ⊥-elim (¬p<x<op ⟪ px<b , subst (λ k → b o< k ) (sym (Oprev.oprev=x op)) b<x ⟫ )
794 zcsup with zc30 794 zcsup with zc30
795 ... | refl = record { ax = ab ; is-sup = record { x<sup = λ lt → IsSup.x<sup is-sup (UnionCF⊆ (pxo≤x op) o≤-refl lt) } } 795 ... | refl = record { ax = ab ; is-sup = record { x<sup = λ lt → IsSup.x<sup is-sup (UnionCF⊆ (pxo≤x op) o≤-refl lt) } }
796 csupf : {b : Ordinal} → b o≤ x → odef (UnionCF A f mf ay supf1 b) (supf1 b) 796 csupf : {b : Ordinal} → b o≤ x → odef (UnionCF A f mf ay supf1 b) (supf1 b)
797 csupf {b} b<x with trio< b px | inspect supf1 b 797 csupf {b} b<x with trio< b px | inspect supf1 b
798 ... | tri< a ¬b ¬c | _ = UnionCF⊆ o≤-refl (o<→≤ a) ( ZChain.csupf zc (o<→≤ a) ) 798 ... | tri< a ¬b ¬c | _ = UnionCF⊆ o≤-refl (o<→≤ a) ( ZChain.csupf zc (o<→≤ a) )
799 ... | tri≈ ¬a refl ¬c | _ = UnionCF⊆ o≤-refl o≤-refl ( ZChain.csupf zc o≤-refl ) 799 ... | tri≈ ¬a refl ¬c | _ = ? -- UnionCF⊆ o≤-refl o≤-refl ( ZChain.csupf zc o≤-refl )
800 ... | tri> ¬a ¬b px<b | record { eq = eq1 } = UnionCF⊆ (o<→≤ px<b) o≤-refl ( ZChain.csupf zc o≤-refl ) 800 ... | tri> ¬a ¬b px<b | record { eq = eq1 } = ? -- UnionCF⊆ (o<→≤ px<b) o≤-refl ( ZChain.csupf zc o≤-refl )
801 sis : {z : Ordinal} (z<x : z o< x) → supf1 z ≡ & (SUP.sup (sup z<x)) 801 sis : {z : Ordinal} (z<x : z o< x) → supf1 z ≡ & (SUP.sup (sup z<x))
802 sis {z} z<x with trio< z px 802 sis {z} z<x with trio< z px
803 ... | tri< a ¬b ¬c = ZChain.supf-is-sup zc a 803 ... | tri< a ¬b ¬c = ZChain.supf-is-sup zc a
804 ... | tri≈ ¬a b ¬c = ? 804 ... | tri≈ ¬a b ¬c = ?
805 ... | tri> ¬a ¬b px<z = ⊥-elim (¬p<x<op ⟪ px<z , subst (λ k → z o< k ) (sym (Oprev.oprev=x op)) z<x ⟫ ) 805 ... | tri> ¬a ¬b px<z = ⊥-elim (¬p<x<op ⟪ px<z , subst (λ k → z o< k ) (sym (Oprev.oprev=x op)) z<x ⟫ )