--- a/src/zorn.agda	Wed Jul 20 11:38:00 2022 +0900
+++ b/src/zorn.agda	Thu Jul 21 03:56:54 2022 +0900
@@ -249,12 +249,6 @@
       A∋maximal : A ∋ sup
       x<sup : {x : HOD} → B ∋ x → (x ≡ sup ) ∨ (x < sup )   -- B is Total, use positive
 
-record IsSup>b (A : HOD) (b : Ordinal) (p : Ordinal) : Set n where
-  field
-     x2 : Ordinal
-     ax2 : odef A x2
-     b<x2 : b o< x2
-     is-sup>b : IsSup A (* p) ax2
 --
 --  sup and its fclosure is in a chain HOD
 --    chain HOD is sorted by sup as Ordinal and <-ordered
@@ -268,15 +262,6 @@
       csupz    : FClosure A f (supf u) z 
       order    : {sup1 z1 : Ordinal} → (lt : sup1 o< u ) → FClosure A f (supf sup1 ) z1 → z1 << supf u
 
-      -- u>0      : o∅ o< u    -- ¬ ch-init
-      -- supf=u   : supf u ≡ u  
-      -- supf-mono  : {a b : Ordinal } → a o≤ b → supf a o≤ supf b
-      -- supf-<  : {a b : Ordinal } → a o≤ b → (supf a ≡ supf b) ∨ (supf a << supf b)
-      -- au       : odef A u
-      -- ¬u=fx    : {x : Ordinal} → ¬ ( u ≡ f x )
-      -- asup     : (x : Ordinal) → odef A (supf x)
-
-
 data Chain (A : HOD ) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f)  {y : Ordinal} (ay : odef A y) (supf : Ordinal → Ordinal) : Ordinal →  Ordinal → Set n where
     ch-init    : (z : Ordinal) → FClosure A f y z  → Chain A f mf  ay supf o∅ z 
     ch-is-sup : {sup z : Ordinal } 
@@ -313,8 +298,8 @@
       initial : {y : Ordinal } → odef chain y → * init ≤ * y
       f-next : {a : Ordinal } → odef chain a → odef chain (f a)
       f-total : IsTotalOrderSet chain
-      sup=u : {b : Ordinal} → (ab : odef A b)  → IsSup A chain ab → supf b ≡ b 
-      -- chain<A : {z : Ordinal } → UnionCF A f mf ay supf z ⊆' UnionCF A f mf ay supf (& A) 
+      sup=u : {b : Ordinal} → {ab : odef A b}  → b o< z → IsSup A chain ab → supf b ≡ b 
+      order : {sup1 b z1 : Ordinal} → b o< z → sup1 o< b → FClosure A f (supf sup1) z1 → z1 << supf b
 
 record ZChain1 ( A : HOD )    ( f : Ordinal → Ordinal )  (mf : ≤-monotonic-f A f) 
         {init : Ordinal} (ay : odef A init)  (zc : ZChain A f mf ay (& A)) ( z : Ordinal ) : Set (Level.suc n) where
@@ -324,6 +309,7 @@
       is-max :  {a b : Ordinal } → (ca : odef (UnionCF A f mf ay (ZChain.supf zc) z) a ) →  b o< z  → (ab : odef A b) 
           → HasPrev A (UnionCF A f mf ay (ZChain.supf zc) z) ab f ∨  IsSup A (UnionCF A f mf ay (ZChain.supf zc) z) ab  
           → * a < * b  → odef ((UnionCF A f mf ay (ZChain.supf zc) z)) b
+      fcy<sup  : {u w : Ordinal } → u o< z  → FClosure A f init w → w << (ZChain.supf zc) u
 
 record Maximal ( A : HOD )  : Set (Level.suc n) where
    field
@@ -500,30 +486,21 @@
               HasPrev A (UnionCF A f mf ay (ZChain.supf zc) x) ab f ∨ IsSup A (UnionCF A f mf ay (ZChain.supf zc) x) ab →
               * a < * b → odef (UnionCF A f mf ay (ZChain.supf zc) x) b
            is-max {a} {b} ua b<x ab (case1 has-prev) a<b = is-max-hp x {a} {b} ua b<x ab has-prev a<b 
-           is-max {a} {b} ua b<x ab (case2 is-sup) a<b = chain-mono2 x ? o≤-refl m04 where
-                 m12 : {sup1 z1 : Ordinal} → sup1 o< b → FClosure A f (ZChain.supf zc sup1) z1 → odef (UnionCF A f mf ay (ZChain.supf zc) x) z1
-                 m12 = ?
-                 m11 : {sup1 z1 : Ordinal} → sup1 o< b → FClosure A f (ZChain.supf zc sup1) z1 → z1 << ZChain.supf zc b
-                 m11 {sup1} {z1} s<b fc with IsSup.x<sup is-sup (m12 s<b fc)
-                 ... | t = ?
+           is-max {a} {b} ua b<x ab (case2 is-sup) a<b = chain-mono2 x (o<→≤ ob<x) o≤-refl m04 where
+                 ob<x : osuc b o< x
+                 ob<x with trio< (osuc b) x
+                 ... | tri< a ¬b ¬c = a
+                 ... | tri≈ ¬a ob=x ¬c = ⊥-elim ( lim record { op = b ; oprev=x = ob=x }  )
+                 ... | tri> ¬a ¬b c = ⊥-elim ( ¬p<x<op ⟪ b<x , c ⟫ )
                  m07 : {z : Ordinal} → FClosure A f y z → z << ZChain.supf zc b
-                 m07 {y} (init ay1) = ?
-                 m07 {.(f x)} (fsuc x fc) with proj1 (mf x (A∋fc y f mf  fc))
-                 ... | case1 eq = subst ( λ k → k << ZChain.supf zc b) (subst₂ (λ j k → j ≡ k) &iso  &iso (cong (&) eq))  (m07 fc)
-                 ... | case2 lt  with ODC.p∨¬p O ( f x << ZChain.supf zc b )
-                 ... | case1 p = p
-                 ... | case2 np = ? where
-                     m08 : x <<　ZChain.supf zc b
-                     m08 = m07 fc
-                     m09 : ⊥
-                     m09 = fcn-imm y f mf ? ? ⟪ m08 , ?  ⟫
-                     m10 : ? ∨ ( ? <<  b )
-                     m10 = IsSup.x<sup is-sup ? -- (proj2 (mf x (A∋fc y f mf  fc)))
+                 m07 {z} fc = ZChain1.fcy<sup (prev (osuc b) ob<x) <-osuc fc
+                 m08 : {sup1 z1 : Ordinal} → sup1 o< b → FClosure A f (ZChain.supf zc sup1) z1 → z1 << ZChain.supf zc b
+                 m08 = ?
                  m05 : b ≡ ZChain.supf zc b
-                 m10 : {sup1 z1 : Ordinal} → sup1 o< b → FClosure A f (ZChain.supf zc sup1) z1 → z1 << ZChain.supf zc b
-                 m05 = sym (ZChain.sup=u ? ab is-sup)   -- ZChain on x
+                 m05 = sym (ZChain.sup=u zc {_} {ab} ?
+                        record { x<sup = λ lt → IsSup.x<sup is-sup (chain-mono2 x (o<→≤ ob<x) o≤-refl ? )} )   -- ZChain on x
                  m06 : ChainP A f mf ay (ZChain.supf zc) b b
-                 m06 = record { fcy<sup = ? ; csupz = subst (λ k →  FClosure A f k b ) m05 (init ab) ; order = ? }
+                 m06 = record { fcy<sup = m07 ; csupz = subst (λ k →  FClosure A f k b ) m05 (init ab) ; order = m08 }
                  m04 : odef (UnionCF A f mf ay (ZChain.supf zc) (osuc b)) b
                  m04 = ⟪ ab , record { u = b ; u<x = case1 <-osuc ; uchain = ch-is-sup m06 (subst (λ k → FClosure A f k b) m05 (init ab)) } ⟫