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

comparison src/zorn.agda @ 1066:86f6cc26e315

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 Tue, 13 Dec 2022 00:14:03 +0900
parents e053ad9c1afb
children 074b6a506b1b
comparison
equal deleted inserted replaced
1065:e053ad9c1afb 1066:86f6cc26e315
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 = uz01 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 pchainx⊆chain ia
1342 ... | ⟪ ai , ch-init fc ⟫ = ZChain.f-total (pzc (pic<x (proj2 ib))) ⟪ ai , ch-init fc ⟫ (pchainx⊆chain ib) 1342 ... | ⟪ ai , ch-init fc ⟫ = ZChain.f-total (pzc (pic<x (proj2 ib))) ⟪ ai , ch-init fc ⟫ (pchainx⊆chain ib)
1343 ... | ⟪ ai , ch-is-sup u u<x su=u fc ⟫ = ZChain.f-total (pzc (pic<x (proj2 ib))) ⟪ ai , ch-is-sup u ? ? ? ⟫ (pchainx⊆chain ib) 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
1344 uz02 : u o< osuc (IChain-i (proj2 ia)) 1344 uz02 : u o< osuc (IChain-i (proj2 ib))
1345 uz02 = ? 1345 uz02 with osuc-≡< (ZChain.supf-mono (pzc (pic<x (proj2 ia))) (o<→≤ u<x))
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
1346 uz04 : FClosure A f (ZChain.supf (pzc (pic<x (proj2 ib))) u) (& a) 1350 uz04 : FClosure A f (ZChain.supf (pzc (pic<x (proj2 ib))) u) (& a)
1347 uz04 = subst (λ k → FClosure A f k (& a)) ? fc 1351 uz04 = subst (λ k → FClosure A f k (& a)) ? fc
1348 ... | tri> ¬a ¬b ib<ia = uz01 where 1352 ... | tri> ¬a ¬b ib<ia = uz01 where
1349 uz01 : Tri (a < b) (a ≡ b) (b < a ) 1353 uz01 : Tri (a < b) (a ≡ b) (b < a )
1350 uz01 with pchainx⊆chain ib 1354 uz01 with pchainx⊆chain ib