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

comparison src/zorn.agda @ 980:49cf50d451e1

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 Wed, 09 Nov 2022 11:10:11 +0900
parents 6229017a6176
children 6b67e43733ca
comparison
equal deleted inserted replaced
979:6229017a6176 980:49cf50d451e1
1176 csupf0 : {z1 : Ordinal } → supf1 z1 o< px → z1 o≤ px → odef (UnionCF A f mf ay supf1 x) (supf1 z1) 1176 csupf0 : {z1 : Ordinal } → supf1 z1 o< px → z1 o≤ px → odef (UnionCF A f mf ay supf1 x) (supf1 z1)
1177 csupf0 {z1} s0z<px z≤px = subst (λ k → odef (UnionCF A f mf ay supf1 x) k ) (sym (sf1=sf0 z≤px)) ( 1177 csupf0 {z1} s0z<px z≤px = subst (λ k → odef (UnionCF A f mf ay supf1 x) k ) (sym (sf1=sf0 z≤px)) (
1178 UChain⊆ A f mf {x} {y} ay {supf0} {supf1} (ZChain.supf-mono zc) sf=eq sf≤ 1178 UChain⊆ A f mf {x} {y} ay {supf0} {supf1} (ZChain.supf-mono zc) sf=eq sf≤
1179 (chain-mono f mf ay supf0 (ZChain.supf-mono zc) (o<→≤ px<x) 1179 (chain-mono f mf ay supf0 (ZChain.supf-mono zc) (o<→≤ px<x)
1180 (ZChain.csupf zc (subst (λ k → k o< px) (sf1=sf0 z≤px) s0z<px)))) 1180 (ZChain.csupf zc (subst (λ k → k o< px) (sf1=sf0 z≤px) s0z<px))))
1181 -- px o< z1 , px o≤ supf1 z1 --> px o≤ sp1 o< x -- sp1 ≡ px--> odef (UnionCF A f mf ay supf1 x) sp1 1181 -- px o< z1 , supf1 z1 o< x -> sp1 o≤ z1 -- sp1 o≤ supf1 x
1182 -- supf1 px ≡ sp1 o< supf1 x 1182 -- px o≤ supf1 z1 , supf1 z1 o< x -> supf1 z1 ≡ px --> z1 o≤ px → supf0 z1 ≡ px
1183 --> px o< x1 → sp1 ≡ px
1183 1184
1184 csupf1 : {z1 : Ordinal } → supf1 z1 o< x → odef (UnionCF A f mf ay supf1 x) (supf1 z1) 1185 csupf1 : {z1 : Ordinal } → supf1 z1 o< x → odef (UnionCF A f mf ay supf1 x) (supf1 z1)
1185 csupf1 {z1} sz1<x = csupf2 where 1186 csupf1 {z1} sz1<x = csupf2 where
1186 -- z1 o< px → supf1 z1 ≡ supf0 z1
1187 -- z1 ≡ px , supf0 px o< px .. px o< z1, x o≤ z1 ... supf1 z1 ≡ sp1
1188 -- z1 ≡ px , supf0 px ≡ px
1189 psz1≤px : supf1 z1 o≤ px 1187 psz1≤px : supf1 z1 o≤ px
1190 psz1≤px = subst (λ k → supf1 z1 o< k ) (sym opx=x) sz1<x 1188 psz1≤px = subst (λ k → supf1 z1 o< k ) (sym opx=x) sz1<x
1191 csupf2 : odef (UnionCF A f mf ay supf1 x) (supf1 z1) 1189 csupf2 : odef (UnionCF A f mf ay supf1 x) (supf1 z1)
1192 csupf2 with 3cases 1190 csupf2 with osuc-≡< psz1≤px
1193 ... | case2 (case2 p) with trio< z1 px | inspect supf1 z1 1191 ... | case2 lt with trio< z1 px | inspect supf1 z1
1194 ... | tri< a ¬b ¬c | record { eq = eq1 } with osuc-≡< psz1≤px 1192 ... | tri< a ¬b ¬c | record { eq = eq } =
1195 ... | case2 lt = zc12 (proj1 p) (proj2 p) (case1 cs03) where 1193 subst (λ k → odef (UnionCF A f mf ay supf1 x) k ) eq ( csupf0 (subst (λ k → k o< px) (sym eq) lt) (o<→≤ a ))
1196 cs03 : odef (UnionCF A f mf ay supf0 px) (supf0 z1) 1194 ... | tri≈ ¬a b ¬c | record { eq = eq } =
1197 cs03 = ZChain.csupf zc (subst (λ k → k o< px) (sf1=sf0 (o<→≤ a)) lt ) 1195 subst (λ k → odef (UnionCF A f mf ay supf1 x) k ) eq ( csupf0 (subst (λ k → k o< px) (sym eq) lt) (o≤-refl0 b ))
1198 ... | case1 sfz=px with osuc-≡< ( supf1-mono (o<→≤ a) ) 1196 ... | tri> ¬a ¬b px<z1 | record { eq = eq } = ⟪ MinSUP.asm sup1 , ch-is-sup sp1 cs00 ? (init asupf1 ssp1=sp1 ) ⟫ where
1199 ... | case1 sfz=sfpx = zc12 (proj1 p) (proj2 p) (case2 (init (ZChain.asupf zc) cs04 )) where 1197 ssp1=sp1 : supf1 sp1 ≡ sp1
1200 cs04 : supf0 px ≡ supf0 z1 1198 ssp1=sp1 = ?
1201 cs04 = begin 1199 cs00 : supf1 sp1 o≤ supf1 x
1202 supf0 px ≡⟨ sym (sf1=sf0 o≤-refl) ⟩ 1200 cs00 = ?
1203 supf1 px ≡⟨ sym sfz=sfpx ⟩ 1201 csupf2 | case1 psz1=px with trio< z1 px | inspect supf1 z1
1204 supf1 z1 ≡⟨ sf1=sf0 (o<→≤ a) ⟩ 1202 ... | tri< a ¬b ¬c | record { eq = eq } = ⟪ ZChain.asupf zc , ch-is-sup px cs00 ? (init asupf1 cs01 ) ⟫ where
1205 supf0 z1 ∎ where open ≡-Reasoning 1203 -- spuf1 z1 == px o< x , z1 o< px,
1206 ... | case2 sfz<sfpx = ⊥-elim ( ¬p<x<op ⟪ cs05 , cs06 ⟫ ) where 1204 cs03 : supf0 z1 o< px
1207 --- supf1 z1 ≡ px , z1 o< px , px ≡ supf0 z1 o< supf0 px o< x 1205 cs03 = ?
1208 cs05 : px o< supf0 px 1206 cs02 : odef (UnionCF A f mf ay supf0 px) (supf0 z1)
1209 cs05 = subst₂ ( λ j k → j o< k ) sfz=px (sf1=sf0 o≤-refl ) sfz<sfpx 1207 cs02 = ZChain.csupf zc cs03
1210 cs06 : supf0 px o< osuc px 1208 cs01 : supf1 px ≡ supf0 z1
1211 cs06 = subst₂ (λ j k → j o< k ) (sym (proj1 p)) (sym opx=x) px<x 1209 cs01 = ?
1212 csupf2 | case2 (case2 p) | tri≈ ¬a b ¬c | record { eq = eq1 } = zc12 (proj1 p) (proj2 p) 1210 cs00 : supf1 px o≤ supf1 x
1213 (case2 (init (ZChain.asupf zc) (cong supf0 (sym b)))) 1211 cs00 = supf1-mono (o<→≤ px<x)
1214 csupf2 | case2 (case2 p) | tri> ¬a ¬b px<z1 | record { eq = eq1 } = ⊥-elim ( ¬p<x<op ⟪ cs08 , cs09 ⟫ ) where 1212 ... | tri≈ ¬a b ¬c | record { eq = eq } = ⟪ ZChain.asupf zc , ch-is-sup px cs00 ? (init asupf1 cs01 ) ⟫ where
1215 cs08 : px o< sp1 1213 cs01 : supf1 px ≡ supf0 z1
1216 cs08 = subst (λ k → k o< sp1 ) (proj1 p) (proj2 p ) 1214 cs01 = trans (sf1=sf0 o≤-refl) (cong supf0 (sym b) )
1217 cs09 : sp1 o< osuc px 1215 cs00 : supf1 px o≤ supf1 x
1218 cs09 = subst ( λ k → sp1 o< k ) (sym (Oprev.oprev=x op)) sz1<x 1216 cs00 = supf1-mono (o<→≤ px<x)
1219 csupf2 | case2 (case1 p) with trio< (supf0 px) sp1 -- ¬ (supf0 px o< sp1 -- sp1 o≤ supf px) 1217 ... | tri> ¬a ¬b c | record { eq = eq } = ⟪ MinSUP.asm sup1 , ch-is-sup x o≤-refl ? (init asupf1 cs01 ) ⟫ where
1220 ... | tri< a ¬b ¬c = ⊥-elim (p a) 1218 cs01 : supf1 x ≡ sp1
1221 ... | tri≈ ¬a b ¬c = ? 1219 cs01 = sf1=sp1 px<x
1222 ... | tri> ¬a ¬b c = ⊥-elim ( o≤> sfpx≤sp1 c )
1223 csupf2 | case1 p with trio< (supf0 px) px -- ¬ (supf0 px ≡ px )
1224 ... | tri< sf0px<px ¬b ¬c = ? where
1225 cs10 : odef (UnionCF A f mf ay supf0 px) (supf0 px)
1226 cs10 = ZChain.csupf zc sf0px<px
1227 ... | tri≈ ¬a b ¬c = ⊥-elim (p b)
1228 ... | tri> ¬a ¬b px<sf0px = ? where
1229 cs11 : px o< z1 → odef (UnionCF A f mf ay supf1 x) (supf1 z1)
1230 cs11 px<z1 = ⊥-elim ( ¬p<x<op ⟪ px<sf0px , subst₂ (λ j k → j o< k ) refl (sym (Oprev.oprev=x op))
1231 (ordtrans≤-< (subst (λ k → supf0 px o< k) (cong osuc (sym (sf1=sp1 px<z1 ))) sfpx≤sp1 ) sz1<x) ⟫ )
1232 cs12 : z1 o≤ px → odef (UnionCF A f mf ay supf1 x) (supf1 z1)
1233 cs12 = ?
1234
1235 1220
1236 zc41 | (case1 x<sp ) = record { supf = supf0 ; sup=u = ? ; asupf = ? ; supf-mono = ? ; supf-< = ? 1221 zc41 | (case1 x<sp ) = record { supf = supf0 ; sup=u = ? ; asupf = ? ; supf-mono = ? ; supf-< = ?
1237 ; supfmax = ? ; minsup = ? ; supf-is-minsup = ? ; csupf = ? } where 1222 ; supfmax = ? ; minsup = ? ; supf-is-minsup = ? ; csupf = ? } where
1238 1223
1239 -- supf0 px not is included by the chain 1224 -- supf0 px not is included by the chain