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

comparison src/zorn.agda @ 918:4c33f8383d7d

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
supf px o< px is in csupf
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 15 Oct 2022 20:05:34 +0900
parents 3105feb3c4e1
children 213f12f27003
comparison
equal deleted inserted replaced
911:3105feb3c4e1 918:4c33f8383d7d
794 px = Oprev.oprev op 794 px = Oprev.oprev op
795 zc : ZChain A f mf ay (Oprev.oprev op) 795 zc : ZChain A f mf ay (Oprev.oprev op)
796 zc = prev px (subst (λ k → px o< k) (Oprev.oprev=x op) <-osuc ) 796 zc = prev px (subst (λ k → px o< k) (Oprev.oprev=x op) <-osuc )
797 px<x : px o< x 797 px<x : px o< x
798 px<x = subst (λ k → px o< k) (Oprev.oprev=x op) <-osuc 798 px<x = subst (λ k → px o< k) (Oprev.oprev=x op) <-osuc
799 opx=x : osuc px ≡ x
800 opx=x = Oprev.oprev=x op
801
799 zc-b<x : (b : Ordinal ) → b o< x → b o< osuc px 802 zc-b<x : (b : Ordinal ) → b o< x → b o< osuc px
800 zc-b<x b lt = subst (λ k → b o< k ) (sym (Oprev.oprev=x op)) lt 803 zc-b<x b lt = subst (λ k → b o< k ) (sym (Oprev.oprev=x op)) lt
801 804
802 supf0 = ZChain.supf zc 805 supf0 = ZChain.supf zc
803 pchain : HOD 806 pchain : HOD
1074 csupf1 {z1} sz1<x = csupf2 where 1077 csupf1 {z1} sz1<x = csupf2 where
1075 -- z1 o< px → supf1 z1 ≡ supf0 z1 1078 -- z1 o< px → supf1 z1 ≡ supf0 z1
1076 -- z1 ≡ px , supf0 px o< px .. px o< z1, x o≤ z1 ... supf1 z1 ≡ sp1 1079 -- z1 ≡ px , supf0 px o< px .. px o< z1, x o≤ z1 ... supf1 z1 ≡ sp1
1077 -- z1 ≡ px , supf0 px ≡ px 1080 -- z1 ≡ px , supf0 px ≡ px
1078 psz1≤px : supf1 z1 o≤ px 1081 psz1≤px : supf1 z1 o≤ px
1079 psz1≤px = subst (λ k → supf1 z1 o< k ) (sym (Oprev.oprev=x op)) sz1<x 1082 psz1≤px = subst (λ k → supf1 z1 o< k ) (sym opx=x) sz1<x
1080 cs01 : supf0 px o< px → odef (UnionCF A f mf ay supf0 px) (supf0 px)
1081 cs01 spx<px = ZChain.csupf zc spx<px
1082 csupf2 : odef (UnionCF A f mf ay supf1 x) (supf1 z1) 1083 csupf2 : odef (UnionCF A f mf ay supf1 x) (supf1 z1)
1083 csupf2 with trio< z1 px | inspect supf1 z1 1084 csupf2 with trio< z1 px | inspect supf1 z1
1084 csupf2 | tri< a ¬b ¬c | record { eq = eq1 } with osuc-≡< psz1≤px 1085 csupf2 | tri< a ¬b ¬c | record { eq = eq1 } with osuc-≡< psz1≤px
1085 ... | case2 lt = zc12 (case1 cs03) where 1086 ... | case2 lt = zc12 (case1 cs03) where
1086 cs03 : odef (UnionCF A f mf ay supf0 px) (supf0 z1) 1087 cs03 : odef (UnionCF A f mf ay supf0 px) (supf0 z1)
1093 cs04 = begin 1094 cs04 = begin
1094 supf0 px ≡⟨ sym (sf1=sf0 o≤-refl) ⟩ 1095 supf0 px ≡⟨ sym (sf1=sf0 o≤-refl) ⟩
1095 supf1 px ≡⟨ sym sfz=sfpx ⟩ 1096 supf1 px ≡⟨ sym sfz=sfpx ⟩
1096 supf1 z1 ≡⟨ sf1=sf0 (o<→≤ a) ⟩ 1097 supf1 z1 ≡⟨ sf1=sf0 (o<→≤ a) ⟩
1097 supf0 z1 ∎ where open ≡-Reasoning 1098 supf0 z1 ∎ where open ≡-Reasoning
1098 ... | case2 sfz<sfpx = ? --- supf0 z1 o< supf0 px 1099 ... | case2 sfz<sfpx = ⊥-elim ( ¬p<x<op ⟪ cs05 , cs06 ⟫ ) where
1100 --- supf1 z1 ≡ px , z1 o< px , px ≡ supf0 z1 o< supf0 px o< x
1101 cs05 : px o< supf0 px
1102 cs05 = subst₂ ( λ j k → j o< k ) sfz=px (sf1=sf0 o≤-refl ) sfz<sfpx
1103 cs06 : supf0 px o< osuc px
1104 cs06 = subst (λ k → supf0 px o< k ) (sym opx=x) sfpx<x
1099 csupf2 | tri≈ ¬a b ¬c | record { eq = eq1 } = zc12 (case2 (init (ZChain.asupf zc) (cong supf0 (sym b)))) 1105 csupf2 | tri≈ ¬a b ¬c | record { eq = eq1 } = zc12 (case2 (init (ZChain.asupf zc) (cong supf0 (sym b))))
1100 csupf2 | tri> ¬a ¬b px<z1 | record { eq = eq1 } with trio< sp1 px 1106 csupf2 | tri> ¬a ¬b px<z1 | record { eq = eq1 } = ? -- ⊥-elim ( ¬p<x<op ⟪ px<z1 , subst (λ k → z1 o< k) (sym opx=x) z1<x ⟫ )
1101 ... | tri< sp1<px ¬b ¬c = ? -- sp1 o< px, supf0 sp1 ≡ supf0 px, sp1 o< z1 1107
1102 ... | tri≈ ¬a sp1=px ¬c = ⟪ MinSUP.asm sup1 , ch-is-sup (supf1 z1) (subst (λ k → k o< x) (sym eq1) sz1<x)
1103 record { fcy<sup = ? ; order = ? ; supu=u = supu=u } (init asupf1 (trans supu=u eq1) ) ⟫ where
1104 -- supf1 z1 ≡ sp1, px o< z1, sp1 o< x -- sp1 o< z1
1105 -- supf1 sp1 o≤ supf1 z1 ≡ sp1 o< z1
1106 asm : odef A (supf1 z1)
1107 asm = subst (λ k → odef A k ) (sym (sf1=sp1 px<z1)) ( MinSUP.asm sup1)
1108 cs05 : odef (UnionCF A f mf ay supf1 x) (supf1 sp1)
1109 cs05 = zc12 (case2 (init (ZChain.asupf zc) ( begin
1110 supf0 px ≡⟨ sym (sf1=sf0 o≤-refl ) ⟩
1111 supf1 px ≡⟨ cong supf1 (sym sp1=px) ⟩
1112 supf1 sp1 ∎ ))) where open ≡-Reasoning
1113 supu=u : supf1 (supf1 z1) ≡ supf1 z1
1114 supu=u = ?
1115 ... | tri> ¬a ¬b px<sp1 = ⊥-elim (¬p<x<op ⟪ px<sp1 , subst (λ k → sp1 o< k) (sym (Oprev.oprev=x op)) sz1<x ⟫ )
1116 1108
1117 zc4 : ZChain A f mf ay x --- x o≤ supf px 1109 zc4 : ZChain A f mf ay x --- x o≤ supf px
1118 zc4 with trio< x (supf0 px) 1110 zc4 with trio< x (supf0 px)
1119 ... | tri> ¬a ¬b c = zc41 c 1111 ... | tri> ¬a ¬b c = zc41 c
1120 ... | tri≈ ¬a b ¬c = ? 1112 ... | tri≈ ¬a b ¬c = ?