--- a/src/zorn.agda	Sat Apr 30 17:07:35 2022 +0900
+++ b/src/zorn.agda	Sat Apr 30 17:30:20 2022 +0900
@@ -404,7 +404,7 @@
           ... | case2 ¬fy<x with ODC.p∨¬p O ( x ≡ & ( SUP.sup ( supP ( ZChain.chain zc0 ) (ZChain.chain⊆A zc0 ) (ZChain.f-total zc0) ) ))
           ... | case1 x=sup = -- previous ordinal is a sup of a smaller ZChain
                  record { chain = schain ; chain⊆A = record { incl = A∋schain } ; f-total = scmp ; f-next = scnext 
-                     ; initial = scinit ; f-immediate =  simm ; chain∋x  = case1 (ZChain.chain∋x zc0) ; is-max = {!!} } where -- x is sup
+                     ; initial = scinit ; f-immediate =  simm ; chain∋x  = case1 (ZChain.chain∋x zc0) ; is-max = s-ismax } where -- x is sup
                 sup0 = supP ( ZChain.chain zc0 ) (ZChain.chain⊆A zc0 ) (ZChain.f-total zc0) 
                 sp = SUP.sup sup0 
                 chain = ZChain.chain zc0
@@ -468,7 +468,18 @@
                 ... | case1 sp=a | case2 b<sp = <-irr (case2 (subst (λ k → * b < k ) (trans (sym *iso) sp=a)  b<sp ) ) (proj1 p )
                 ... | case2 sp<a | case1 b=sp = <-irr (case2 (subst ( λ  k → k < * a ) (trans *iso (sym b=sp)) sp<a  )) (proj1 p )
                 ... | case2 sp<a | case2 b<sp = <-irr (case2 (ptrans b<sp (subst (λ k → k < * a) *iso sp<a ))) (proj1 p )
-                simm {a} {b} (case2 sa) (case2 sb) p = {!!}
+                simm {a} {b} (case2 sa) (case2 sb) p = fcn-imm {A} (& sp) {a} {b} f mf sa sb p
+                s-ismax : {a b : Ordinal} → odef schain a → b o< x → (ba : odef A b) →
+                    Prev< A schain ba f ∨ (& (SUP.sup (supP (* (& schain))
+                       (subst (λ k → k ⊆ A) (sym *iso) (record { incl = A∋schain }))
+                       (subst IsTotalOrderSet (sym *iso) scmp)))
+                     ≡ b) →
+                    * a < * b → odef schain b
+                s-ismax {a} {b} (case2 sa) b<x ba P a<b = {!!}
+                s-ismax {a} {b} (case1 sa) b<x ba P a<b with trio< b px
+                ... | tri< a₁ ¬b ¬c = case1 ( ZChain.is-max zc0 sa a₁ ba {!!} a<b )
+                ... | tri≈ ¬a b₁ ¬c = {!!}
+                ... | tri> ¬a ¬b c = {!!}
           ... | case2 ¬x=sup =  -- x is not f y' nor sup of former ZChain from y
                    record { chain = ZChain.chain zc0 ; chain⊆A = ZChain.chain⊆A zc0 ; f-total = ZChain.f-total zc0 ; f-next = ZChain.f-next zc0
                      ; initial = ZChain.initial zc0 ; f-immediate = ZChain.f-immediate zc0 ; chain∋x  =  ZChain.chain∋x zc0 ; is-max = {!!} }  where -- no extention