# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1655135083 -32400
# Node ID 2595d2f6487be61276e366779a5735b3484db4da
# Parent  f484cff027e4463b67ae1e50d0e6685e4b7cb82a
...

diff -r f484cff027e4 -r 2595d2f6487b src/zorn.agda
--- a/src/zorn.agda	Tue Jun 14 00:25:59 2022 +0900
+++ b/src/zorn.agda	Tue Jun 14 00:44:43 2022 +0900
@@ -585,13 +585,12 @@
          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 ) }
          u-mono :  ( a b : Ordinal ) → b o< 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 = TransFinite {λ a → a o< osuc b → (za : ZChain A y f a) (zb : ZChain A y f b)
-             → ZChain.chain za  ⊆' ZChain.chain zb } uind a where
+         u-mono a b b<x a≤b za zb {i} zai = TransFinite0 {λ i → odef (chain za) i → odef (chain zb) i } uind i zai where
             open ZChain
-            uind :  (a : Ordinal)
-                 → ((c : Ordinal) → c o< a →  c o< osuc b → (za : ZChain A y f c) (zb : ZChain A y f b) → chain za ⊆' chain zb)
-                 → a o< osuc b → (za : ZChain A y f a) (zb : ZChain A y f b) → chain za ⊆' chain zb
-            uind a previ a≤b za zb {i} zai = um01 where
+            uind :  (i : Ordinal)
+                 → ((j : Ordinal) → j o< i →  odef (chain za) j → odef (chain zb) j)
+                 → odef (chain za) i → odef (chain zb) i
+            uind i previ zai = um01 where
                 FC : Fc∨sup A (chain⊆A za (chain∋x za)) f i 
                 FC = fc∨sup za zai 
                 -- y≤fc : {a p : Ordinal} → Fc∨sup A p f i → * y ≤ * p
@@ -603,8 +602,12 @@
                 ... | case1 y=i = subst (λ k → odef (chain zb) k ) (subst₂ (λ j k → j ≡ k ) &iso &iso (cong (&) y=i)) ( chain∋x zb )
                 ... | case2 y<i with (FChain.fc∨sup fc) 
                 ... | case1 fc = um02 i fc where
-                     um02 : (i : Ordinal) → FClosure A f p i → odef (chain zb) i
-                     um02 i (init ap i=p ) = subst (λ k → odef (chain zb) k ) (sym i=p) (previ a {!!} {!!} za zb {!!} ) where
+                     um02 : (i2 : Ordinal) → FClosure A f p i2 → odef (chain zb) i2
+                     um02 i2 (init ap i=p ) = subst (λ k → odef (chain zb) k ) (sym i=p) (previ p um03 um04 ) where
+                        um03 : p o< i
+                        um03 = {!!}
+                        um04 : odef (chain za) p
+                        um04 = {!!}
                      um02 i (fsuc j fc) = f-next zb ( um02 j fc )
                 ... | case2 sup = {!!}
                 -- is-max zb (chain∋x zb) {!!} (chain⊆A za zai) {!!} y<i where