# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1655104495 -32400
# Node ID 4af13e0001282953185d9dc3888afe18883fb143
# Parent  5f329a1c1d09aca8b1998337d90c9c5d3e80f47c
...

diff -r 5f329a1c1d09 -r 4af13e000128 src/zorn.agda
--- a/src/zorn.agda	Mon Jun 13 10:47:53 2022 +0900
+++ b/src/zorn.agda	Mon Jun 13 16:14:55 2022 +0900
@@ -596,25 +596,25 @@
                 um01 : odef (chain zb) i
                 um01 with FC
                 ... | Finit i=y = subst (λ k → odef (chain zb) k ) (sym i=y) ( chain∋x zb )
-                ... | Fc {p} {x1} pFC fc with initial za zai
+                ... | Fc {p} {i} pFC fc with initial za zai
                 ... | 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 = is-max zb {y} {i} (chain∋x zb) i<b (chain⊆A za zai) um05 y<i
-                  where
-                    i<b : i o< osuc b
-                    i<b = {!!}
-                    um05 : HasPrev A (chain zb) (chain⊆A za zai) f ∨ IsSup A (chain zb) (chain⊆A za zai)
-                    um05 with FChain.fc∨sup fc
-                    ... | case1 (init {p} ap i=p) = case2 {!!}
-                    ... | case1 (fsuc p pfci) = case1 record { y = p ; ay = um07 ; x=fy = refl }  where
-                        -- p should be the top of fc
-                        p<a : p o< a
-                        p<a = {!!}
-                        um08 : odef (chain (prev p {!!} ay)) p
-                        um08 = {!!}
-                        um07 : odef (chain zb) p
-                        um07 = previ p p<a {!!} (prev p {!!} ay )  zb um08 
-                    ... | case2 supi = case2 record { x<sup = um06 supi } where
-                        um06 : ((z : Ordinal) → FClosure A f p z → (z ≡ i) ∨ (z << i) ) → {w : Ordinal} → odef (chain zb) w → (w ≡ i) ∨ (w << i)
+                ... | case2 y<i with FChain.fc∨sup fc 
+                ... | case1 fci  = um10 i p y<i fci where
+                     um10 : (i p : Ordinal) → y << i → FClosure A f p i → odef (chain zb) i
+                     um10 i p y<i (init {q} ap q=p) = um02 where
+                        q<a : q o< a
+                        q<a = {!!}
+                        um03 : odef (chain (prev q (ordtrans q<a (ordtrans a<b b<x)) ay)) q
+                        um03 = ?
+                        um02 : odef (chain zb) q
+                        um02 = previ a {!!} {!!} za zb ?
+                     um10 i p y<i (fsuc j pfci) = f-next zb (um10 j p y<j pfci)  where
+                        y<j : y << j
+                        y<j = {!!}
+                ... | case2 supi = um06 supi where
+                        um05 : FChain A f p i
+                        um05 = fc 
+                        um06 : ((z : Ordinal) → FClosure A f p z → (z ≡ i) ∨ (z << i) ) → odef (chain zb) i
                         um06 supi = {!!}
          u-total : IsTotalOrderSet Uz
          u-total {x} {y} ux uy = {!!}