Mercurial > hg > Members > kono > Proof > ZF-in-agda
comparison src/zorn.agda @ 1067:074b6a506b1b
ic case
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Tue, 13 Dec 2022 00:14:32 +0900 |
parents | 86f6cc26e315 |
children | f24f4de4d459 |
comparison
equal
deleted
inserted
replaced
1066:86f6cc26e315 | 1067:074b6a506b1b |
---|---|
1334 uz02 = ordtrans<-≤ u<x (o<→≤ (osucc a<b)) | 1334 uz02 = ordtrans<-≤ u<x (o<→≤ (osucc a<b)) |
1335 uz03 : ZChain.supf (pzc (pic<x (proj2 ib))) u ≡ u | 1335 uz03 : ZChain.supf (pzc (pic<x (proj2 ib))) u ≡ u |
1336 uz03 = trans (sym ( zeq _ _ (o<→≤ (osucc a<b)) (o<→≤ u<x) )) su=u | 1336 uz03 = trans (sym ( zeq _ _ (o<→≤ (osucc a<b)) (o<→≤ u<x) )) su=u |
1337 uz04 : FClosure A f (ZChain.supf (pzc (pic<x (proj2 ib))) u) (& a) | 1337 uz04 : FClosure A f (ZChain.supf (pzc (pic<x (proj2 ib))) u) (& a) |
1338 uz04 = subst (λ k → FClosure A f k (& a)) ( zeq _ _ (o<→≤ (osucc a<b)) (o<→≤ u<x) ) fc | 1338 uz04 = subst (λ k → FClosure A f k (& a)) ( zeq _ _ (o<→≤ (osucc a<b)) (o<→≤ u<x) ) fc |
1339 ... | tri≈ ¬a ia=ib ¬c = uz01 where | 1339 ... | tri≈ ¬a ia=ib ¬c = ? where |
1340 uz01 : Tri (a < b) (a ≡ b) (b < a ) | 1340 uz01 : Tri (* (& a ) < * (& b)) (* (& a) ≡ * (& b)) (* (& b) < * (& a )) |
1341 uz01 with pchainx⊆chain ia | 1341 uz01 with proj2 ia | proj2 ib |
1342 ... | ⟪ ai , ch-init fc ⟫ = ZChain.f-total (pzc (pic<x (proj2 ib))) ⟪ ai , ch-init fc ⟫ (pchainx⊆chain ib) | 1342 ... | ic-init fca | ic-init fcb = fcn-cmp y f mf fca fcb |
1343 ... | ⟪ ai , ch-is-sup u u<x su=u fc ⟫ = ZChain.f-total (pzc (pic<x (proj2 ib))) ⟪ ai , ch-is-sup u uz02 uz03 uz04 ⟫ (pchainx⊆chain ib) where | 1343 ... | ic-isup ia ia<x sa<x fca | ic-init fcb = ? |
1344 uz02 : u o< osuc (IChain-i (proj2 ib)) | 1344 ... | ic-init fca | ic-isup ib ib<x sb<x fcb = ? |
1345 uz02 with osuc-≡< (ZChain.supf-mono (pzc (pic<x (proj2 ia))) (o<→≤ u<x)) | 1345 ... | ic-isup ia ia<x sa<x fca | ic-isup ib ib<x sb<x fcb = fcn-cmp ? f mf ? ? |
1346 ... | case1 eq = ⊥-elim ( o<¬≡ (trans (sym su=u) eq) (subst (λ k → u o< k) ? u<x) ) | |
1347 ... | case2 lt = ZChain.supf-inject (pzc (pic<x (proj2 ia))) ? | |
1348 uz03 : ZChain.supf (pzc (pic<x (proj2 ib))) u ≡ u | |
1349 uz03 = trans (zeq _ _ ? ?) su=u | |
1350 uz04 : FClosure A f (ZChain.supf (pzc (pic<x (proj2 ib))) u) (& a) | |
1351 uz04 = subst (λ k → FClosure A f k (& a)) ? fc | |
1352 ... | tri> ¬a ¬b ib<ia = uz01 where | 1346 ... | tri> ¬a ¬b ib<ia = uz01 where |
1353 uz01 : Tri (a < b) (a ≡ b) (b < a ) | 1347 uz01 : Tri (a < b) (a ≡ b) (b < a ) |
1354 uz01 with pchainx⊆chain ib | 1348 uz01 with pchainx⊆chain ib |
1355 ... | ⟪ bi , ch-init fc ⟫ = ZChain.f-total (pzc (pic<x (proj2 ia))) (pchainx⊆chain ia) ⟪ bi , ch-init fc ⟫ | 1349 ... | ⟪ bi , ch-init fc ⟫ = ZChain.f-total (pzc (pic<x (proj2 ia))) (pchainx⊆chain ia) ⟪ bi , ch-init fc ⟫ |
1356 ... | ⟪ bi , ch-is-sup u u<x su=u fc ⟫ = ZChain.f-total (pzc (pic<x (proj2 ia))) (pchainx⊆chain ia) ⟪ bi , ch-is-sup u uz02 uz03 uz04 ⟫ where | 1350 ... | ⟪ bi , ch-is-sup u u<x su=u fc ⟫ = ZChain.f-total (pzc (pic<x (proj2 ia))) (pchainx⊆chain ia) ⟪ bi , ch-is-sup u uz02 uz03 uz04 ⟫ where |