# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1670854462 -32400
# Node ID e053ad9c1afbaa9da73666f28d1158164f40c73d
# Parent  77740070e0088414d3a04005e5ffd96c13fbaae3
equal case

diff -r 77740070e008 -r e053ad9c1afb src/zorn.agda
--- a/src/zorn.agda	Mon Dec 12 18:55:31 2022 +0900
+++ b/src/zorn.agda	Mon Dec 12 23:14:22 2022 +0900
@@ -1309,12 +1309,16 @@
           ichain-inject : {a b : Ordinal } {ia : IChain ay supfz a } {ib : IChain ay supfz b }
             → ZChain.supf (pzc (pic<x ia)) (IChain-i ia) o< ZChain.supf (pzc (pic<x ib)) (IChain-i ib)
             → IChain-i ia o< IChain-i ib
-          ichain-inject {a} {b} {ia} {ib} sa<sb = osucprev ( begin
-                    osuc (IChain-i ia)  ≤⟨ osucc ( ZChain.supf-inject (pzc (pic<x ib)) (osucprev ( begin 
-                        osuc (ZChain.supf (pzc (pic<x ib)) (IChain-i ia))  ≡⟨ cong osuc ( zeq _ _ ? ?)  ⟩ 
-                        osuc (ZChain.supf (pzc (pic<x ia)) (IChain-i ia))  ≤⟨ osucc sa<sb ⟩ 
-                        ZChain.supf (pzc (pic<x ib)) (IChain-i ib)  ∎ ))) ⟩
-                    IChain-i ib ∎ ) where open o≤-Reasoning O
+          ichain-inject {a} {b} {ia} {ib} sa<sb = uz11 where
+                 uz11 : IChain-i ia o< IChain-i ib
+                 uz11 with trio< (IChain-i ia ) (IChain-i ib)
+                 ... | tri< a ¬b ¬c = a
+                 ... | tri≈ ¬a b ¬c = ⊥-elim ( o<¬≡ (trans (zeq _ _ (o≤-refl0 (cong osuc b)) (o<→≤ <-osuc) ) 
+                     ( cong (ZChain.supf (pzc (pic<x ib))) b )) sa<sb )
+                 ... | tri> ¬a ¬b c = ⊥-elim ( o≤> ( begin
+                     ZChain.supf (pzc (pic<x ib)) (IChain-i ib)  ≡⟨ zeq _ _ (o<→≤ (osucc c)) (o<→≤ <-osuc)  ⟩ 
+                     ZChain.supf (pzc (pic<x ia)) (IChain-i ib)  ≤⟨ ZChain.supf-mono (pzc (pic<x ia)) (o<→≤ c) ⟩ 
+                     ZChain.supf (pzc (pic<x ia)) (IChain-i ia)  ∎ ) sa<sb ) where open o≤-Reasoning O
 
           ptotalx : IsTotalOrderSet pchainx
           ptotalx {a} {b} ia ib with trio< (ZChain.supf (pzc (pic<x (proj2 ia))) (IChain-i (proj2 ia)))  
@@ -1324,20 +1328,36 @@
               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
-                 uz05 : IChain-i (proj2 ia) o< IChain-i (proj2 ib)
-                 uz05 = ichain-inject {_} {_} {proj2 ia} {proj2 ib} ia<ib
+                 a<b : IChain-i (proj2 ia) o< IChain-i (proj2 ib)
+                 a<b = ichain-inject {_} {_} {proj2 ia} {proj2 ib} ia<ib
                  uz02 : u o< osuc (IChain-i (proj2 ib))
-                 uz02 = ordtrans<-≤ u<x ?
+                 uz02 = ordtrans<-≤ u<x (o<→≤ (osucc a<b))
                  uz03 : ZChain.supf (pzc (pic<x (proj2 ib))) u ≡ u
-                 uz03 = trans ( zeq _ _ ? ? ) su=u
+                 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)) ? fc
+                 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 ? ? ? ⟫ (pchainx⊆chain ib) 
-          ... | tri> ¬a ¬b ib<ia = ?
+                 uz02 : u o< osuc (IChain-i (proj2 ia))
+                 uz02 = ?
+                 uz04 :  FClosure A f (ZChain.supf (pzc (pic<x (proj2 ib))) u) (& a)
+                 uz04 = subst (λ k → FClosure A f k (& a)) ? fc
+          ... | tri> ¬a ¬b ib<ia = uz01 where
+              uz01 : Tri (a < b) (a ≡ b) (b < a )
+              uz01 with pchainx⊆chain ib
+              ... | ⟪ bi , ch-init fc ⟫ = ZChain.f-total (pzc (pic<x (proj2 ia))) (pchainx⊆chain ia)  ⟪ bi , ch-init fc ⟫ 
+              ... | ⟪ 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
+                 b<a : IChain-i (proj2 ib) o< IChain-i (proj2 ia)
+                 b<a = ichain-inject {_} {_} {proj2 ib} {proj2 ia} ib<ia
+                 uz02 : u o< osuc (IChain-i (proj2 ia))
+                 uz02 = ordtrans<-≤ u<x (o<→≤ (osucc b<a))
+                 uz03 : ZChain.supf (pzc (pic<x (proj2 ia))) u ≡ u
+                 uz03 = trans (sym ( zeq _ _ (o<→≤ (osucc b<a)) (o<→≤ u<x) )) su=u
+                 uz04 : FClosure A f (ZChain.supf (pzc (pic<x (proj2 ia))) u) (& b)
+                 uz04 = subst (λ k → FClosure A f k (& b)) ( zeq _ _ (o<→≤ (osucc b<a)) (o<→≤ u<x) ) fc
 
           usup : MinSUP A pchainx
           usup = minsupP pchainx (λ ic → ? ) ptotalx