Mercurial > hg > Members > kono > Proof > ZF-in-agda
comparison src/zorn.agda @ 841:01361e10ad96
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Mon, 29 Aug 2022 19:56:39 +0900 |
| parents | 52bff0b4cb37 |
| children | 962a9f3dbd3c |
comparison
equal
deleted
inserted
replaced
| 840:52bff0b4cb37 | 841:01361e10ad96 |
|---|---|
| 769 ; chain⊆A = λ lt → proj1 lt ; f-next = pnext1 ; f-total = ptotal1 } where | 769 ; chain⊆A = λ lt → proj1 lt ; f-next = pnext1 ; f-total = ptotal1 } where |
| 770 pchain0=1 : pchain ≡ pchain1 | 770 pchain0=1 : pchain ≡ pchain1 |
| 771 pchain0=1 = ==→o≡ record { eq→ = zc10 ; eq← = zc11 } where | 771 pchain0=1 = ==→o≡ record { eq→ = zc10 ; eq← = zc11 } where |
| 772 zc10 : {z : Ordinal} → OD.def (od pchain) z → OD.def (od pchain1) z | 772 zc10 : {z : Ordinal} → OD.def (od pchain) z → OD.def (od pchain1) z |
| 773 zc10 {z} ⟪ az , ch-init fc ⟫ = ⟪ az , ch-init fc ⟫ | 773 zc10 {z} ⟪ az , ch-init fc ⟫ = ⟪ az , ch-init fc ⟫ |
| 774 zc10 {z} ⟪ az , ch-is-sup u u≤px is-sup fc ⟫ = zc12 fc where | 774 zc10 {z} ⟪ az , ch-is-sup u1 u1≤x u1-is-sup fc ⟫ = zc12 fc where |
| 775 zc12 : {z : Ordinal} → FClosure A f (supf0 u) z → odef pchain1 z | 775 zc12 : {z : Ordinal} → FClosure A f (supf0 u1) z → odef pchain1 z |
| 776 zc12 (fsuc x fc) with zc12 fc | 776 zc12 (fsuc x fc) with zc12 fc |
| 777 ... | ⟪ ua1 , ch-init fc₁ ⟫ = ⟪ proj2 ( mf _ ua1) , ch-init (fsuc _ fc₁) ⟫ | 777 ... | ⟪ ua1 , ch-init fc₁ ⟫ = ⟪ proj2 ( mf _ ua1) , ch-init (fsuc _ fc₁) ⟫ |
| 778 ... | ⟪ ua1 , ch-is-sup u u≤x is-sup fc₁ ⟫ = ⟪ proj2 ( mf _ ua1) , ch-is-sup u u≤x is-sup (fsuc _ fc₁) ⟫ | 778 ... | ⟪ ua1 , ch-is-sup u u≤x u1-is-sup fc₁ ⟫ = ⟪ proj2 ( mf _ ua1) , ch-is-sup u u≤x u1-is-sup (fsuc _ fc₁) ⟫ |
| 779 zc12 (init asu su=z ) with trio< u px | 779 zc12 (init asp refl ) with trio< u1 px | inspect supf1 u1 |
| 780 ... | tri< a ¬b ¬c = ⟪ subst (λ k → odef A k) su=z asu , ch-is-sup u (ordtrans u≤px (osucc (pxo<x op)) ) | 780 ... | tri< a ¬b ¬c | record { eq = eq1 } = ⟪ A∋fcs _ f mf fc , ch-is-sup u1 (OrdTrans u1≤x ? ) |
| 781 record { fcy<sup = ? ; order = ? ; supu=u = ? } (init ? ? ) ⟫ | 781 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 |
| 782 ... | tri≈ ¬a b ¬c = ? | 782 fcy<sup : {z : Ordinal} → FClosure A f y z → (z ≡ supf1 u1) ∨ (z << supf1 u1 ) |
| 783 ... | tri> ¬a ¬b c = ? | 783 fcy<sup {z} fc = subst ( λ k → (z ≡ k) ∨ (z << k )) (sym eq1) ( ChainP.fcy<sup u1-is-sup fc ) |
| 784 order : {s : Ordinal} {z2 : Ordinal} → supf1 s o< supf1 u1 → FClosure A f (supf1 s) z2 → | |
| 785 (z2 ≡ supf1 u1) ∨ (z2 << supf1 u1) | |
| 786 order {s} {z2} s<u1 fc with trio< s px | |
| 787 ... | tri< a ¬b ¬c = subst (λ k → (z2 ≡ k) ∨ (z2 << k) ) (sym eq1) ( ChainP.order u1-is-sup ? fc ) | |
| 788 ... | tri≈ ¬a b ¬c = subst (λ k → (z2 ≡ k) ∨ (z2 << k) ) (sym eq1) ( ChainP.order u1-is-sup ? fc ) | |
| 789 ... | tri> ¬a ¬b px<s = ⊥-elim ( o<¬≡ refl (ordtrans px<s ? )) -- px o< s < u1 < px | |
| 790 ... | tri≈ ¬a b ¬c | record { eq = eq1 } = ⟪ A∋fcs _ f mf fc , ch-is-sup u1 (OrdTrans u1≤x ? ) | |
| 791 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 | |
| 792 fcy<sup : {z : Ordinal} → FClosure A f y z → (z ≡ supf1 u1) ∨ (z << supf1 u1 ) | |
| 793 fcy<sup {z} fc = subst ( λ k → (z ≡ k) ∨ (z << k )) (sym eq1) ( ChainP.fcy<sup u1-is-sup fc ) | |
| 794 order : {s : Ordinal} {z2 : Ordinal} → supf1 s o< supf1 u1 → FClosure A f (supf1 s) z2 → | |
| 795 (z2 ≡ supf1 u1) ∨ (z2 << supf1 u1) | |
| 796 order {s} {z2} s<u1 fc with trio< s px | |
| 797 ... | tri< a ¬b ¬c = subst (λ k → (z2 ≡ k) ∨ (z2 << k) ) (sym eq1) ( ChainP.order u1-is-sup ? fc ) | |
| 798 ... | tri≈ ¬a b ¬c = subst (λ k → (z2 ≡ k) ∨ (z2 << k) ) (sym eq1) ( ChainP.order u1-is-sup ? fc ) | |
| 799 ... | tri> ¬a ¬b px<s = ⊥-elim ( o<¬≡ refl (ordtrans px<s (subst (λ k → s o< k) b ? ) )) -- px o< s < u1 = px | |
| 800 ... | tri> ¬a ¬b px<u1 | record { eq = eq1 } with osuc-≡< u1≤x | |
| 801 ... | case1 eq = ⊥-elim ( o<¬≡ (sym eq) px<u1 ) | |
| 802 ... | case2 lt = ⊥-elim ( o<> lt px<u1 ) | |
| 803 | |
| 784 zc11 : {z : Ordinal} → OD.def (od pchain1) z → OD.def (od pchain) z | 804 zc11 : {z : Ordinal} → OD.def (od pchain1) z → OD.def (od pchain) z |
| 785 zc11 {z} ⟪ az , ch-init fc ⟫ = ⟪ az , ch-init fc ⟫ | 805 zc11 {z} ⟪ az , ch-init fc ⟫ = ⟪ az , ch-init fc ⟫ |
| 786 zc11 {z} ⟪ az , ch-is-sup u u≤x is-sup fc ⟫ = zc13 fc where | 806 zc11 {z} ⟪ az , ch-is-sup u1 u1≤x u1-is-sup fc ⟫ = zc13 fc where |
| 787 zc13 : {z : Ordinal} → FClosure A f (supf1 u) z → odef pchain z | 807 zc13 : {z : Ordinal} → FClosure A f (supf1 u1) z → odef pchain z |
| 788 zc13 (fsuc x fc) with zc13 fc | 808 zc13 (fsuc x fc) with zc13 fc |
| 789 ... | ⟪ ua1 , ch-init fc₁ ⟫ = ⟪ proj2 ( mf _ ua1) , ch-init (fsuc _ fc₁) ⟫ | 809 ... | ⟪ ua1 , ch-init fc₁ ⟫ = ⟪ proj2 ( mf _ ua1) , ch-init (fsuc _ fc₁) ⟫ |
| 790 ... | ⟪ ua1 , ch-is-sup u u≤x is-sup fc₁ ⟫ = ⟪ proj2 ( mf _ ua1) , ch-is-sup u u≤x is-sup (fsuc _ fc₁) ⟫ | 810 ... | ⟪ ua1 , ch-is-sup u u≤x is-sup fc₁ ⟫ = ⟪ proj2 ( mf _ ua1) , ch-is-sup u u≤x is-sup (fsuc _ fc₁) ⟫ |
| 791 zc13 (init asu su=z ) with trio< u x | 811 zc13 (init asp refl ) with trio< u1 px | inspect supf1 u1 |
| 792 ... | tri< a ¬b ¬c = ⟪ subst (λ k → odef A k) su=z asu , ch-is-sup u (subst (λ k → u o< k) (sym (Oprev.oprev=x op)) a) ? (init ? ? ) ⟫ | 812 ... | tri< a ¬b ¬c | record { eq = eq1 } = ⟪ A∋fcs _ f mf fc , ch-is-sup u1 (subst (λ k → u1 o< k ) ? a ) |
| 793 ... | tri≈ ¬a b ¬c = ? | 813 record { fcy<sup = fcy<sup ; order = order ; supu=u = trans ? (ChainP.supu=u u1-is-sup) } (init ? ?) ⟫ where |
| 794 ... | tri> ¬a ¬b c = ⊥-elim ( o≤> u≤x c ) | 814 fcy<sup : {z : Ordinal} → FClosure A f y z → (z ≡ supf0 u1) ∨ (z << supf0 u1 ) |
| 815 fcy<sup {z} fc = subst ( λ k → (z ≡ k) ∨ (z << k )) ? ( ChainP.fcy<sup u1-is-sup fc ) | |
| 816 order : {s : Ordinal} {z2 : Ordinal} → supf0 s o< supf0 u1 → FClosure A f (supf0 s) z2 → | |
| 817 (z2 ≡ supf0 u1) ∨ (z2 << supf0 u1) | |
| 818 order {s} {z2} s<u1 fc with trio< s px | inspect supf1 s | |
| 819 ... | tri< a ¬b ¬c | record { eq = eq2 } = subst (λ k → (z2 ≡ k) ∨ (z2 << k) ) ? ( ChainP.order u1-is-sup ? (subst (λ k → FClosure A f k z2) (sym eq2) fc )) | |
| 820 ... | tri≈ ¬a b ¬c | record { eq = eq2 } = subst (λ k → (z2 ≡ k) ∨ (z2 << k) ) ? ( ChainP.order u1-is-sup ? (subst (λ k → FClosure A f k z2) (sym eq2) fc )) | |
| 821 ... | tri> ¬a ¬b px<s | record { eq = eq2 } = ⊥-elim ( o<¬≡ refl (ordtrans px<s ? )) -- px o< s < u1 < px | |
| 822 ... | tri≈ ¬a b ¬c | record { eq = eq1 } = ⟪ A∋fcs _ f mf fc , ch-is-sup u1 (OrdTrans u1≤x ? ) | |
| 823 record { fcy<sup = fcy<sup ; order = order ; supu=u = trans (sym ?) (ChainP.supu=u u1-is-sup) } (init ? ? ) ⟫ where | |
| 824 fcy<sup : {z : Ordinal} → FClosure A f y z → (z ≡ supf0 u1) ∨ (z << supf0 u1 ) | |
| 825 fcy<sup {z} fc = subst ( λ k → (z ≡ k) ∨ (z << k )) ? ( ChainP.fcy<sup u1-is-sup fc ) | |
| 826 order : {s : Ordinal} {z2 : Ordinal} → supf0 s o< supf0 u1 → FClosure A f (supf0 s) z2 → | |
| 827 (z2 ≡ supf0 u1) ∨ (z2 << supf0 u1) | |
| 828 order {s} {z2} s<u1 fc with trio< s px | inspect supf1 s | |
| 829 ... | tri< a ¬b ¬c | record { eq = eq2 } = subst (λ k → (z2 ≡ k) ∨ (z2 << k) ) ? ( ChainP.order u1-is-sup ? (subst (λ k → FClosure A f k z2) (sym eq2) fc )) | |
| 830 ... | tri≈ ¬a b ¬c | record { eq = eq2 } = subst (λ k → (z2 ≡ k) ∨ (z2 << k) ) ? ( ChainP.order u1-is-sup ? (subst (λ k → FClosure A f k z2) (sym eq2) fc )) | |
| 831 ... | tri> ¬a ¬b px<s | _ = ⊥-elim ( o<¬≡ refl (ordtrans px<s ? )) -- px o< s < u1 = px | |
| 832 ... | tri> ¬a ¬b c | _ = ⊥-elim ( o≤> u1≤x ? ) | |
| 795 sup : {z : Ordinal} → z o≤ x → SUP A (UnionCF A f mf ay supf1 z) | 833 sup : {z : Ordinal} → z o≤ x → SUP A (UnionCF A f mf ay supf1 z) |
| 796 sup {z} z≤x with trio< z px | inspect supf1 z | 834 sup {z} z≤x with trio< z px | inspect supf1 z |
| 797 ... | tri< a ¬b ¬c | record { eq = eq1} = ? -- ZChain.sup zc (o<→≤ a) | 835 ... | tri< a ¬b ¬c | record { eq = eq1} = ? -- ZChain.sup zc (o<→≤ a) |
| 798 ... | tri≈ ¬a b ¬c | record { eq = eq1} = ? -- ZChain.sup zc (o≤-refl0 b) | 836 ... | tri≈ ¬a b ¬c | record { eq = eq1} = ? -- ZChain.sup zc (o≤-refl0 b) |
| 799 ... | tri> ¬a ¬b px<z | record { eq = eq1} = record { sup = SUP.sup sup1 ; as = SUP.as sup1 ; x<sup = zc31 } where | 837 ... | tri> ¬a ¬b px<z | record { eq = eq1} = record { sup = SUP.sup sup1 ; as = SUP.as sup1 ; x<sup = zc31 } where |
| 825 zc30 with osuc-≡< b≤x | 863 zc30 with osuc-≡< b≤x |
| 826 ... | case1 eq = sym (eq) | 864 ... | case1 eq = sym (eq) |
| 827 ... | case2 b<x = ⊥-elim (¬p<x<op ⟪ px<b , subst (λ k → b o< k ) (sym (Oprev.oprev=x op)) b<x ⟫ ) | 865 ... | case2 b<x = ⊥-elim (¬p<x<op ⟪ px<b , subst (λ k → b o< k ) (sym (Oprev.oprev=x op)) b<x ⟫ ) |
| 828 sis : {z : Ordinal} (z≤x : z o≤ x) → supf1 z ≡ & (SUP.sup (sup z≤x)) | 866 sis : {z : Ordinal} (z≤x : z o≤ x) → supf1 z ≡ & (SUP.sup (sup z≤x)) |
| 829 sis {z} z≤x = zc40 where | 867 sis {z} z≤x = zc40 where |
| 830 zc40 : supf1 z ≡ & (SUP.sup (sup z≤x)) | 868 zc40 : supf1 z ≡ & (SUP.sup (sup z≤x)) -- direct with statment causes error |
| 831 zc40 with trio< z px | inspect supf1 z | inspect sup z≤x | 869 zc40 with trio< z px | inspect supf1 z | inspect sup z≤x |
| 832 ... | tri< a ¬b ¬c | record { eq = eq1 } | record { eq = eq2 } = ? | 870 ... | tri< a ¬b ¬c | record { eq = eq1 } | record { eq = eq2 } = ? |
| 833 ... | tri≈ ¬a b ¬c | record { eq = eq1 } | record { eq = eq2 } = ? | 871 ... | tri≈ ¬a b ¬c | record { eq = eq1 } | record { eq = eq2 } = ? |
| 834 ... | tri> ¬a ¬b c | record { eq = eq1 } | record { eq = eq2 } = ? | 872 ... | tri> ¬a ¬b c | record { eq = eq1 } | record { eq = eq2 } = ? |
| 835 -- ... | tri< a ¬b ¬c = ? -- jZChain.supf-is-sup zc (o<→≤ a ) | |
| 836 -- ... | tri≈ ¬a b ¬c = ? -- jZChain.supf-is-sup zc (o≤-refl0 b ) | |
| 837 -- ... | tri> ¬a ¬b px<z = ? | |
| 838 -- ... | tri< a ¬b ¬c | _ = ? -- jZChain.supf-is-sup zc (o<→≤ a ) | |
| 839 -- ... | tri≈ ¬a b ¬c | _ = ? -- jZChain.supf-is-sup zc (o≤-refl0 b ) | |
| 840 -- ... | tri> ¬a ¬b px<z | record { eq = eq1 } = ? where | |
| 841 -- zc30 : z ≡ x | |
| 842 -- zc30 with osuc-≡< z≤x | |
| 843 -- ... | case1 eq = eq | |
| 844 -- ... | case2 z<x = ⊥-elim (¬p<x<op ⟪ px<z , subst (λ k → z o< k ) (sym (Oprev.oprev=x op)) z<x ⟫ ) | |
| 845 | 873 |
| 846 zc4 : ZChain A f mf ay x | 874 zc4 : ZChain A f mf ay x |
| 847 zc4 with ODC.∋-p O A (* x) | 875 zc4 with ODC.∋-p O A (* x) |
| 848 ... | no noax = no-extension {!!} -- ¬ A ∋ p, just skip | 876 ... | no noax = no-extension {!!} -- ¬ A ∋ p, just skip |
| 849 ... | yes ax with ODC.p∨¬p O ( HasPrev A (ZChain.chain zc ) x f ) | 877 ... | yes ax with ODC.p∨¬p O ( HasPrev A (ZChain.chain zc ) x f ) |