# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1655514979 -32400
# Node ID e766238b69d23973784b138bfb41e86725ed8038
# Parent  b726eedf9041e34ccab2879a3cbe70831f5120c7
...

diff -r b726eedf9041 -r e766238b69d2 src/zorn.agda
--- a/src/zorn.agda	Sat Jun 18 09:26:06 2022 +0900
+++ b/src/zorn.agda	Sat Jun 18 10:16:19 2022 +0900
@@ -586,23 +586,22 @@
          u-chain∋x :  odef Uz y
          u-chain∋x = record { u = y ; u<x = y<x ; chain∋z = ZChain.chain∋x (prev y y<x ay ) }
 
-         ind-mono :  {a b : Ordinal } → (zb : ZChain A y f b) →
-             (z : Ordinal)
-                → ((c : Ordinal) → c o< z → a o≤ b → b o≤ c → (za : ZChain A y f a) {i : Ordinal} → odef (ZChain.chain za) i → odef (ZChain.chain zb) i)
-                → a o≤ b → b o≤ z → (za : ZChain A y f a) {i : Ordinal} → odef (ZChain.chain za) i → odef (ZChain.chain zb) i
-         ind-mono {a} {b} zb z prev-mono a≤b b≤z za {i} zai = mc01 where
+         ind-mono :  {a : Ordinal }
+           → (b : Ordinal)
+                → ((c : Ordinal) → c o< b → a o≤ c → c o≤ x → (za : ZChain A y f a) (zc : ZChain A y f c) {i : Ordinal}
+                    → odef (ZChain.chain za) i → odef (ZChain.chain zc) i)
+                → a o≤ b → b o≤ x → (za : ZChain A y f a) (zb : ZChain A y f b) {i : Ordinal} → odef (ZChain.chain za) i → odef (ZChain.chain zb) i
+         ind-mono {a} z prev-mono a≤b b≤z za zb {i} zai = mc01 where
            open ZChain
            mc01 : odef (chain zb) i
-           mc01 with trio< b z | osuc-≡< b≤z
-           ... | tri< b<z ¬b ¬c | _ = prev-mono b b<z a≤b <-osuc za zai
-           ... | tri> ¬a ¬b b>z | case1 b=z = ⊥-elim ( ¬b b=z )
-           ... | tri> ¬a ¬b b>z | case2 b<z = ⊥-elim ( ¬a b<z )
-           ... | tri≈ ¬a b=z ¬c | _  with Oprev-p z
+           mc01 with Oprev-p z
            ... | yes op = mc00 where
               open ZChain
               pz = Oprev.oprev op
               zc0 : ZChain A y f (Oprev.oprev op)
-              zc0 = prev pz (subst (λ k → pz o< k) {!!} <-osuc ) ay
+              zc0 = prev pz {!!} ay
+              zc0∋i : odef (chain zc0) i
+              zc0∋i = prev-mono pz {!!} {!!} {!!} za zc0 zai
               mc00 : odef (chain zb) i
               mc00 with ODC.∋-p O A (* z)
               ... | no noaz = {!!}
@@ -618,12 +617,13 @@
     
          chain-mono : { a b : Ordinal }
               → (zx : ZChain A y f a ) → (zy : ZChain A y f b)  → a o≤ b → b o< osuc x →  ZChain.chain zx ⊆' ZChain.chain zy
-         chain-mono {a} {b} za zb a≤b b≤x = TransFinite {λ x →  
-             a o≤ b → b o≤ x  → (za : ZChain A y f a) → {i : Ordinal } → odef (ZChain.chain za) i → odef (ZChain.chain zb) i }
-             (ind-mono zb) x a≤b b≤x za  
+         chain-mono {a} {b} za zb a≤b b≤x = TransFinite {λ b →  
+             a o≤ b → b o≤ x  → (za : ZChain A y f a) (zb : ZChain A y f b) → {i : Ordinal } → odef (ZChain.chain za) i → odef (ZChain.chain zb) i }
+             ind-mono b a≤b b≤x za zb
 
          u-mono :  ( a b : Ordinal ) → b o< osuc x → a o< osuc b → (za : ZChain A y f a) (zb : ZChain A y f b) → ZChain.chain za  ⊆' ZChain.chain zb
          u-mono a b b≤x a≤b za zb {i} zai = {!!} -- chain-mono ay f mf za zb a≤b  b≤x zai
+
          u-total : IsTotalOrderSet Uz
          u-total {x} {y} ux uy  with trio< (UZFChain.u ux) (UZFChain.u uy)
          ... | tri< a ¬b ¬c = ZChain.f-total (uzc uy) (u-mono (UZFChain.u ux) (UZFChain.u uy)