--- a/src/zorn.agda	Sat Jun 11 18:33:12 2022 +0900
+++ b/src/zorn.agda	Sun Jun 12 12:20:16 2022 +0900
@@ -239,7 +239,7 @@
    field
       sup  : Ordinal
       B∋sup  : odef B sup
-      issup  : {y : Ordinal} → odef B y → (x ≡ y ) ∨ (y << x )  
+      issup  : {y : Ordinal} → odef B y → (y ≡ x ) ∨ (y << x )  
       minsup : {z : Ordinal} → (za : odef A z) → IsSup A B za → sup o≤ z
       fc : FClosure A f sup x
 
@@ -257,7 +257,7 @@
           → HasPrev A chain ab f ∨  IsSup A chain ab  
           → * a < * b  → odef chain b
       fc∨sup :  {a : Ordinal } → ( ca : odef chain a ) → IsMinSup A chain f ( chain⊆A ca)
-      sup≤x :  {a : Ordinal } → ( ca : odef chain a ) → IsMinSup.sup (fc∨sup ca)  o≤ x
+      sup≤z :  {a : Ordinal } → ( ca : odef chain a ) → IsMinSup.sup (fc∨sup ca)  o≤ z
 
 record Maximal ( A : HOD )  : Set (Level.suc n) where
    field
@@ -586,23 +586,45 @@
                  → ((c : Ordinal) → c o< a →  c o< b → (za : ZChain A y f c) (zb : ZChain A y f b) → chain za ⊆' chain zb)
                  → a o< 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 (IsMinSup.fc (fc∨sup za zai)) where
-               um01 : {i : Ordinal} → FClosure A f (IsMinSup.sup (fc∨sup za zai)) i → odef (chain zb) i
+               um01 : {j : Ordinal} → FClosure A f (IsMinSup.sup (fc∨sup za zai)) j → odef (chain zb) j
                um01 (fsuc x t) = f-next zb (um01 t)
-               um01 {j} (init s j=minsup ) with trio< j b
-               ... | tri> ¬a ¬b b<j = {!!}
-               ... | tri≈ ¬a b=j ¬c = {!!}
-               ... | tri< j<b ¬b ¬c = previ j j<a j<b {!!} zb {!!}
+               um01 {j} (init as j=minsup ) with trio< j y
+               ... | tri< j<y ¬b ¬c = {!!}
+               ... | tri≈ ¬a j=y ¬c = {!!}
+               ... | tri> ¬a ¬b j>y = um10
                 where
-                 zj : ZChain A y f j
-                 zj = prev (osuc j) j<x ay
-                 um10 : j ≡ IsMinSup.sup (fc∨sup za zai)
-                 um10 = j=minsup
-                 -- zcj : odef (chain zj  ) j
-                 -- zcj = ZChain.is-max zj {!!} {!!} {!!} (case2 ?) {!!}
-                 j<a  : j o< a
-                 j<a  = {!!}
-                 -- um00 : odef (chain zb) j
-                 -- um00 = previ (osuc j) {!!} {!!} zj zb zcj 
+                 aj : odef A j
+                 aj = subst (λ k → odef A k ) (sym j=minsup) as
+                 zj : odef (chain za) j
+                 zj = subst (λ k → odef (chain za) k ) (sym j=minsup) ( IsMinSup.B∋sup (fc∨sup za zai) )
+                 j<a : j o< a
+                 j<a = {!!}
+                 um04 : j o< osuc b
+                 um04 = {!!}
+                 j<x : j o< x
+                 j<x = {!!}
+                 j<b : j o< b
+                 j<b = {!!}
+                 um05 : odef (chain (prev j j<x ay)) y
+                 um05 = {!!}
+                 um03 : * y < * j
+                 um03 with initial za zj
+                 ... | case1 eq = {!!}
+                 ... | case2 lt = lt
+                 um09 :  odef (chain (prev j j<x ay)) j
+                 um09 = {!!}
+                 um06 : IsSup A (chain (prev j j<x ay)) aj
+                 um06 = record { x<sup = λ {c} pc → um07 pc } where
+                    um08 : ZChain A y f j
+                    um08 = prev j j<x ay
+                    um07 : {c : Ordinal} → odef (chain (prev j j<x ay)) c →  (c ≡ j) ∨ (c << j)
+                    um07 {c} pc = {!!} where
+                       um11 : odef (chain za) c
+                       um11 = ?
+                       um10  : (c ≡ i) ∨ (c << i)
+                       um10  = IsMinSup.issup (fc∨sup za zai) um11
+                 um10 : odef (chain zb) j
+                 um10 = previ j j<a {!!} (prev j j<x ay ) zb um09 -- (is-max (prev j j<x ay ) um05 <-osuc aj (case2 um06) um03 )
          u-total : IsTotalOrderSet Uz
          u-total {x} {y} ux uy = {!!}
          --- ux ⊆ uy ∨ uy ⊆ ux