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

changeset 1067:074b6a506b1b

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
ic case
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Tue, 13 Dec 2022 00:14:32 +0900
parents 86f6cc26e315
children f24f4de4d459
files src/zorn.agda
diffstat 1 files changed, 7 insertions(+), 13 deletions(-) [+]
line wrap: on
line diff
--- a/src/zorn.agda	Tue Dec 13 00:14:03 2022 +0900
+++ b/src/zorn.agda	Tue Dec 13 00:14:32 2022 +0900
@@ -1336,19 +1336,13 @@
                  uz03 = trans (sym ( zeq _ _ (o<→≤ (osucc a<b)) (o<→≤ u<x) )) su=u
                  uz04 : FClosure A f (ZChain.supf (pzc (pic<x (proj2 ib))) u) (& a)
                  uz04 = subst (λ k → FClosure A f k (& a)) ( zeq _ _ (o<→≤ (osucc a<b)) (o<→≤ u<x) ) fc
-          ... | tri≈ ¬a ia=ib ¬c = uz01 where
-              uz01 : Tri (a < b) (a ≡ b) (b < a )
-              uz01 with pchainx⊆chain ia
-              ... | ⟪ ai , ch-init fc ⟫ = ZChain.f-total (pzc (pic<x (proj2 ib)))  ⟪ ai , ch-init fc ⟫  (pchainx⊆chain ib) 
-              ... | ⟪ 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
-                 uz02 : u o< osuc (IChain-i (proj2 ib))
-                 uz02 with osuc-≡< (ZChain.supf-mono (pzc (pic<x (proj2 ia))) (o<→≤ u<x))
-                 ... | case1 eq = ⊥-elim ( o<¬≡ (trans (sym su=u) eq) (subst (λ k → u o< k) ? u<x) )
-                 ... | case2 lt = ZChain.supf-inject (pzc (pic<x (proj2 ia))) ?
-                 uz03 :  ZChain.supf (pzc (pic<x (proj2 ib))) u ≡ u
-                 uz03 =  trans (zeq _ _ ? ?) su=u
-                 uz04 :  FClosure A f (ZChain.supf (pzc (pic<x (proj2 ib))) u) (& a)
-                 uz04 = subst (λ k → FClosure A f k (& a)) ? fc
+          ... | tri≈ ¬a ia=ib ¬c = ? where
+              uz01 : Tri (* (& a ) < * (& b)) (* (& a) ≡ * (& b)) (* (& b) < * (& a ))
+              uz01 with proj2 ia | proj2 ib
+              ... | ic-init fca | ic-init fcb = fcn-cmp y f mf fca fcb
+              ... | ic-isup ia ia<x sa<x fca | ic-init fcb = ?
+              ... | ic-init fca | ic-isup ib ib<x sb<x fcb  = ?
+              ... | ic-isup ia ia<x sa<x fca | ic-isup ib ib<x sb<x fcb = fcn-cmp ? f mf ? ? 
           ... | tri> ¬a ¬b ib<ia = uz01 where
               uz01 : Tri (a < b) (a ≡ b) (b < a )
               uz01 with pchainx⊆chain ib