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

comparison src/zorn.agda @ 1022:1b87669d9b11

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 Fri, 25 Nov 2022 12:22:22 +0900
parents 1407fed90475
children 52272b5c9d58
comparison
equal deleted inserted replaced
1021:1407fed90475 1022:1b87669d9b11
1286 cfcs : (mf< : <-monotonic-f A f) {a b w : Ordinal } 1286 cfcs : (mf< : <-monotonic-f A f) {a b w : Ordinal }
1287 → a o< b → b o≤ x → supf0 a o< b → FClosure A f (supf0 a) w → odef (UnionCF A f mf ay supf0 b) w 1287 → a o< b → b o≤ x → supf0 a o< b → FClosure A f (supf0 a) w → odef (UnionCF A f mf ay supf0 b) w
1288 cfcs mf< {a} {b} {w} a<b b≤x sa<b fc with trio< b px 1288 cfcs mf< {a} {b} {w} a<b b≤x sa<b fc with trio< b px
1289 ... | tri< a ¬b ¬c = ZChain.cfcs zc mf< a<b (o<→≤ a) sa<b fc 1289 ... | tri< a ¬b ¬c = ZChain.cfcs zc mf< a<b (o<→≤ a) sa<b fc
1290 ... | tri≈ ¬a refl ¬c = ZChain.cfcs zc mf< a<b o≤-refl sa<b fc 1290 ... | tri≈ ¬a refl ¬c = ZChain.cfcs zc mf< a<b o≤-refl sa<b fc
1291 ... | tri> ¬a ¬b px<b = ? where 1291 ... | tri> ¬a ¬b px<b = cfcs1 where
1292 x=b : x ≡ b 1292 x=b : x ≡ b
1293 x=b = ? 1293 x=b with trio< x b
1294 ... | tri< a ¬b ¬c = ⊥-elim ( o≤> b≤x a )
1295 ... | tri≈ ¬a b ¬c = b
1296 ... | tri> ¬a ¬b c = ⊥-elim ( ¬p<x<op ⟪ px<b , zc-b<x _ c ⟫ ) -- px o< b o< x
1294 -- a o< x, supf a o< x 1297 -- a o< x, supf a o< x
1295 -- a o< px , supf a o< px → odef U w 1298 -- a o< px , supf a o< px → odef U w
1296 -- a ≡ px -- supf0 px o< x → odef U w 1299 -- a ≡ px -- supf0 px o< x → odef U w
1297 -- -- x o≤ supf0 px o< x → ⊥
1298 -- supf a ≡ px -- a o< px → odef U w 1300 -- supf a ≡ px -- a o< px → odef U w
1299 -- a ≡ px → supf px ≡ px → odef U w 1301 -- a ≡ px → supf px ≡ px → odef U w
1300 1302
1303 cfcs0 : a ≡ px → odef (UnionCF A f mf ay supf0 b) w
1304 cfcs0 a=px = ⟪ A∋fc {A} _ f mf fc , ch-is-sup (supf0 px) spx<b ? ? ⟫ where
1305 spx<b : supf0 px o< b
1306 spx<b = ?
1307
1301 cfcs1 : odef (UnionCF A f mf ay supf0 b) w 1308 cfcs1 : odef (UnionCF A f mf ay supf0 b) w
1302 cfcs1 with trio< a px 1309 cfcs1 with trio< a px
1303 ... | tri< a<px ¬b ¬c = chain-mono f mf ay (ZChain.supf zc) (ZChain.supf-mono zc) (o<→≤ px<b) 1310 ... | tri< a<px ¬b ¬c = cfcs2 where
1304 ( ZChain.cfcs zc mf< a<px o≤-refl ? fc ) 1311 sa<x : supf0 a o< x
1305 ... | tri> ¬a ¬b c = ⊥-elim ( o≤> ? c ) 1312 sa<x = ordtrans<-≤ sa<b b≤x
1306 ... | tri≈ ¬a refl ¬c = ? -- supf0 px o< x → odef (UnionCF A f mf ay supf0 x) (supf0 px) 1313 cfcs2 : odef (UnionCF A f mf ay supf0 b) w
1307 -- x o≤ supf0 px o≤ sp → 1314 cfcs2 with trio< (supf0 a) px
1315 ... | tri< sa<x ¬b ¬c = chain-mono f mf ay (ZChain.supf zc) (ZChain.supf-mono zc) (o<→≤ px<b)
1316 ( ZChain.cfcs zc mf< a<px o≤-refl sa<x fc )
1317 ... | tri> ¬a ¬b c = ⊥-elim ( ¬p<x<op ⟪ c , (zc-b<x _ sa<x) ⟫ )
1318 ... | tri≈ ¬a sa=px ¬c with trio< a px
1319 ... | tri< a<px ¬b ¬c = ⟪ A∋fc {A} _ f mf fc , ch-is-sup (supf0 a) sa<b ? ? ⟫
1320 ... | tri≈ ¬a a=px ¬c = cfcs0 a=px
1321 ... | tri> ¬a ¬b c = ⊥-elim ( ¬p<x<op ⟪ c , (zc-b<x _ (ordtrans<-≤ a<b b≤x) ) ⟫ )
1322 ... | tri≈ ¬a a=px ¬c = cfcs0 a=px
1323 ... | tri> ¬a ¬b c = ⊥-elim ( o≤> (zc-b<x _ (ordtrans<-≤ a<b b≤x)) c )
1308 1324
1309 zc17 : {z : Ordinal } → supf0 z o≤ supf0 px 1325 zc17 : {z : Ordinal } → supf0 z o≤ supf0 px
1310 zc17 {z} with trio< z px 1326 zc17 {z} with trio< z px
1311 ... | tri< a ¬b ¬c = ZChain.supf-mono zc (o<→≤ a) 1327 ... | tri< a ¬b ¬c = ZChain.supf-mono zc (o<→≤ a)
1312 ... | tri≈ ¬a b ¬c = o≤-refl0 (cong supf0 b) 1328 ... | tri≈ ¬a b ¬c = o≤-refl0 (cong supf0 b)