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

comparison src/zorn.agda @ 936:f160556a7c9a

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 Mon, 24 Oct 2022 16:16:15 +0900
parents ed711d7be191
children 3a511519bd10
comparison
equal deleted inserted replaced
935:ed711d7be191 936:f160556a7c9a
1364 → * a < * b → odef chain b 1364 → * a < * b → odef chain b
1365 z10 = ZChain1.is-max (SZ1 f mf as0 zc (& A) ) 1365 z10 = ZChain1.is-max (SZ1 f mf as0 zc (& A) )
1366 z22 : sp o< & A 1366 z22 : sp o< & A
1367 z22 = z09 asp 1367 z22 = z09 asp
1368 x<sup : {x : HOD} → chain ∋ x → (x ≡ SUP.sup sp1 ) ∨ (x < SUP.sup sp1 ) 1368 x<sup : {x : HOD} → chain ∋ x → (x ≡ SUP.sup sp1 ) ∨ (x < SUP.sup sp1 )
1369 x<sup bz with SUP.x<sup sp1 bz 1369 x<sup bz = SUP.x<sup sp1 bz
1370 ... | case1 eq = case1 ?
1371 ... | case2 lt = case2 ?
1372 z12 : odef chain sp 1370 z12 : odef chain sp
1373 z12 with o≡? (& s) sp 1371 z12 with o≡? (& s) sp
1374 ... | yes eq = subst (λ k → odef chain k) eq ( ZChain.chain∋init zc ) 1372 ... | yes eq = subst (λ k → odef chain k) eq ( ZChain.chain∋init zc )
1375 ... | no ne = ZChain1.is-max (SZ1 f mf as0 zc (& A)) {& s} {sp} ( ZChain.chain∋init zc ) ssp<as asp 1373 ... | no ne = ZChain1.is-max (SZ1 f mf as0 zc (& A)) {& s} {sp} ( ZChain.chain∋init zc ) ssp<as asp
1376 (case2 z19 ) z13 where 1374 (case2 z19 ) z13 where
1395 z16 with proj1 (mf (& ( SUP.sup sp1)) ( SUP.as sp1 )) 1393 z16 with proj1 (mf (& ( SUP.sup sp1)) ( SUP.as sp1 ))
1396 ... | case1 eq = ⊥-elim (¬b (subst₂ (λ j k → j ≡ k ) refl *iso (sym eq) )) 1394 ... | case1 eq = ⊥-elim (¬b (subst₂ (λ j k → j ≡ k ) refl *iso (sym eq) ))
1397 ... | case2 lt = ⊥-elim (¬c (subst₂ (λ j k → k < j ) refl *iso lt )) 1395 ... | case2 lt = ⊥-elim (¬c (subst₂ (λ j k → k < j ) refl *iso lt ))
1398 ... | tri≈ ¬a b ¬c = subst ( λ k → k ≡ & (SUP.sup sp1) ) &iso ( cong (&) b ) 1396 ... | tri≈ ¬a b ¬c = subst ( λ k → k ≡ & (SUP.sup sp1) ) &iso ( cong (&) b )
1399 ... | tri> ¬a ¬b c = ⊥-elim z17 where 1397 ... | tri> ¬a ¬b c = ⊥-elim z17 where
1400 z15 : (* (f sp) ≡ SUP.sup sp1) ∨ (* (f sp) < * sp ) 1398 z15 : (* (f sp) ≡ SUP.sup sp1) ∨ (* (f sp) < SUP.sup sp1 )
1401 z15 = ? -- x<sup (subst (λ k → odef chain k ) (sym &iso) (ZChain.f-next zc z12 )) 1399 z15 = x<sup (subst (λ k → odef chain k ) (sym &iso) (ZChain.f-next zc z12 ))
1402 z17 : ⊥ 1400 z17 : ⊥
1403 z17 with z15 1401 z17 with z15
1404 ... | case1 eq = ¬b eq 1402 ... | case1 eq = ¬b eq
1405 ... | case2 lt = ¬a ? 1403 ... | case2 lt = ¬a lt
1406 1404
1407 1405
1408 -- ZChain contradicts ¬ Maximal 1406 -- ZChain contradicts ¬ Maximal
1409 -- 1407 --
1410 -- ZChain forces fix point on any ≤-monotonic function (fixpoint) 1408 -- ZChain forces fix point on any ≤-monotonic function (fixpoint)