# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1669808581 -32400
# Node ID 382680c3e9be4490b8c4bac895df5ca28eda3048
# Parent  f276cf614fc5a105b1794ebe47251d107204ecfd
minsup is not obvious in ZChain

diff -r f276cf614fc5 -r 382680c3e9be src/zorn.agda
--- a/src/zorn.agda	Wed Nov 30 10:16:02 2022 +0900
+++ b/src/zorn.agda	Wed Nov 30 20:43:01 2022 +0900
@@ -83,6 +83,10 @@
 <-irr {a} {b} (case2 a<b) b<a = IsStrictPartialOrder.irrefl PO   refl
           (IsStrictPartialOrder.trans PO     b<a a<b)
 
+<<-irr : {a b : Ordinal } → a ≤ b  → b << a → ⊥
+<<-irr {a} {b} (case1 a=b) b<a = IsStrictPartialOrder.irrefl PO (cong (*) (sym a=b)) b<a
+<<-irr {a} {b} (case2 a<b) b<a = IsStrictPartialOrder.irrefl PO refl (IsStrictPartialOrder.trans PO b<a a<b)
+
 ptrans =  IsStrictPartialOrder.trans PO
 
 open _==_
@@ -219,7 +223,7 @@
 _⊆'_ A B = {x : Ordinal } → odef A x → odef B x
 
 --
--- inductive maxmum tree from x
+-- inductive masum tree from x
 -- tree structure
 --
 
@@ -266,15 +270,17 @@
     (order : {x y w : Ordinal } → x o< y → FClosure A f (supf x) w → w ≤ supf y)
    {s s1 a b : Ordinal } ( fa : FClosure A f (supf s) a )( fb : FClosure A f (supf s1) b )  → Tri (* a < * b) (* a ≡ * b) (* b < * a )
 fc-total A f mf supf order {xa} {xb} {a} {b} ca cb with trio< xa xb
-... | tri< a₁ ¬b ¬c with order a₁ ca 
+... | tri< a₁ ¬b ¬c with ≤-ftrans  (order a₁ ca ) (s≤fc (supf xb) f mf cb )
 ... | case1 eq1 = tri≈ (λ lt → ⊥-elim (<-irr (case1 (sym ct00)) lt)) ct00  (λ lt → ⊥-elim (<-irr (case1 ct00) lt)) where
           ct00 : * a ≡ * b
-          ct00 = ? -- trans (cong (*) eq) eq1
-... | case2 lt =  tri< ct02  (λ eq → <-irr (case1 (sym eq)) ct02) (λ lt → <-irr (case2 ct02) lt)  where
-          ct02 : * a < * b
-          ct02 = ? -- subst (λ k → * k < * b ) (sym eq) lt
-fc-total f mf supf {xa} {xb} {a} {b} ca cb | tri≈ a₁ ¬b ¬c = ?
-fc-total A f mf supf order {xa} {xb} {a} {b} ca cb | tri> ¬a ¬b c = ?
+          ct00 = cong (*) eq1  
+... | case2 a<b =  tri< a<b (λ eq → <-irr (case1 (sym eq)) a<b ) (λ lt → <-irr (case2 a<b ) lt)  
+fc-total A f mf supf order {xa} {xb} {a} {b} ca cb | tri≈ _ refl _ = fcn-cmp _ f mf ca cb 
+fc-total A f mf supf order {xa} {xb} {a} {b} ca cb | tri> ¬a ¬b c with ≤-ftrans  (order c cb ) (s≤fc (supf xa) f mf ca )
+... | case1 eq1 = tri≈ (λ lt → ⊥-elim (<-irr (case1 (sym ct00)) lt)) ct00  (λ lt → ⊥-elim (<-irr (case1 ct00) lt)) where
+          ct00 : * a ≡ * b
+          ct00 = cong (*) (sym eq1)  
+... | case2 b<a =  tri> (λ lt → <-irr (case2 b<a ) lt)  (λ eq → <-irr (case1 eq) b<a )  b<a
 
 
 ∈∧P→o< :  {A : HOD } {y : Ordinal} → {P : Set n} → odef A y ∧ P → y o< & A
@@ -311,7 +317,7 @@
 
 record IsMinSUP ( A B : HOD ) (sup : Ordinal) : Set n where
    field
-      axm : odef A sup
+      as : odef A sup
       x≤sup : {x : Ordinal } → odef B x → (x ≡ sup ) ∨ (x << sup )
       minsup : { sup1 : Ordinal } → odef A sup1
          →  ( {x : Ordinal  } → odef B x → (x ≡ sup1 ) ∨ (x << sup1 ))  → sup o≤ sup1
@@ -320,7 +326,7 @@
    field
       sup : Ordinal
       isMinSUP : IsMinSUP A B sup
-   axm = IsMinSUP.axm isMinSUP
+   as = IsMinSUP.as isMinSUP
    x≤sup = IsMinSUP.x≤sup isMinSUP
    minsup = IsMinSUP.minsup isMinSUP
 
@@ -332,12 +338,11 @@
       →  MinSUP A (UnionCF A f supf x)
       → SUP A (UnionCF A f supf x)
 M→S {A} {f} {mf} {y} {ay} {x} supf ms = record { sup = * (MinSUP.sup ms)
-        ; isSUP = record { ax = subst (λ k → odef A k) (sym &iso) (MinSUP.axm ms) ; x≤sup = ? } } where
-   msup = MinSUP.sup ms
-   ms00 : {z : HOD} → UnionCF A f supf x ∋ z → (z ≡ * msup) ∨ (z < * msup)
+        ; isSUP = record { ax = subst (λ k → odef A k) (sym &iso) (MinSUP.as ms) ; x≤sup = ms00 } } where
+   ms00 :  {z : Ordinal} → odef (UnionCF A f supf x) z → (z ≡ & (* (MinSUP.sup ms))) ∨ (z << & (* (MinSUP.sup ms)))
    ms00 {z} uz with MinSUP.x≤sup ms uz
-   ... | case1 eq = case1 (subst (λ k → k ≡ _) *iso ( cong (*) eq))
-   ... | case2 lt = case2 (subst₂ (λ j k →  j < k ) *iso refl lt )
+   ... | case1 eq = case1 (subst (λ k → z ≡ k) (sym &iso) eq)
+   ... | case2 lt = case2  (subst (λ k →  * z < k ) (sym *iso) lt )
 
 
 chain-mono : {A : HOD}  ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f )  {y : Ordinal} (ay : odef A y) (supf : Ordinal → Ordinal )
@@ -345,41 +350,29 @@
         → odef (UnionCF A f supf a) c → odef (UnionCF A f supf b) c
 chain-mono f mf ay supf supf-mono {a} {b} {c} a≤b ⟪ ua , ch-is-sup u u<x supu=u fc ⟫ = ⟪ ua , ch-is-sup u (ordtrans<-≤ u<x a≤b) supu=u fc ⟫ 
 
-chain-minsup : {A : HOD}  ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f )    (supf : Ordinal → Ordinal )
-    ( order : {x y w : Ordinal } → x o< y → FClosure A f (supf x) w → w ≤ supf y)
-   {x : Ordinal} → IsMinSUP A (UnionCF A f supf x) x
-chain-minsup = ?
-
 record ZChain ( A : HOD )    ( f : Ordinal → Ordinal )  (mf : ≤-monotonic-f A f)
         {y : Ordinal} (ay : odef A y)  ( z : Ordinal ) : Set (Level.suc n) where
    field
       supf :  Ordinal → Ordinal
 
-      sup=u : {b : Ordinal} → (ab : odef A b) → b o≤ z
-           → IsSUP A (UnionCF A f supf b) b ∧ (¬ HasPrev A (UnionCF A f supf b) f b ) → supf b ≡ b
       cfcs : (mf< : <-monotonic-f A f)
          {a b w : Ordinal } → a o< b → b o≤ z → supf a o< b  → FClosure A f (supf a) w → odef (UnionCF A f supf b) w
+      fcy<sup  : {w : Ordinal } → FClosure A f y w → (w ≡ supf o∅  ) ∨ ( w << supf o∅  ) 
       order : {x y w : Ordinal } → x o< y → FClosure A f (supf x) w → w ≤ supf y
 
       asupf :  {x : Ordinal } → odef A (supf x)
       supf-mono : {x y : Ordinal } → x o≤  y → supf x o≤ supf y
       supfmax : {x : Ordinal } → z o< x → supf x ≡ supf z
-      supf0 : supf o∅ ≡ y
 
-      minsup : {x : Ordinal } → x o≤ z  → MinSUP A (UnionCF A f supf x)
-      supf-is-minsup : {x : Ordinal } → (x≤z : x o≤ z) → supf x ≡ MinSUP.sup ( minsup x≤z )
+      is-minsup : {x : Ordinal } → (x≤z : x o≤ z) → IsMinSUP A (UnionCF A f supf x) (supf x) 
+      sup=u : {b : Ordinal} → (ab : odef A b) → b o≤ z
+           → IsSUP A (UnionCF A f supf b) b ∧ (¬ HasPrev A (UnionCF A f supf b) f b ) → supf b ≡ b
 
    chain : HOD
    chain = UnionCF A f supf z
    chain⊆A : chain ⊆' A
    chain⊆A = λ lt → proj1 lt
 
-   sup : {x : Ordinal } → x o≤ z  → SUP A (UnionCF A f supf x)
-   sup {x} x≤z = M→S supf (minsup x≤z)
-
-   s=ms : {x : Ordinal } → (x≤z : x o≤ z ) → & (SUP.sup (sup x≤z)) ≡ MinSUP.sup (minsup x≤z)
-   s=ms {x} x≤z = &iso
-
    chain∋init : odef chain y
    chain∋init = ⟪ ay , ?   ⟫
    f-next : {a z : Ordinal} → odef (UnionCF A f supf z) a → odef (UnionCF A f supf z) (f a)
@@ -387,9 +380,13 @@
    initial : {z : Ordinal } → odef chain z →  y ≤  z
    initial {a} ⟪ aa , ua ⟫  = ?
    f-total : IsTotalOrderSet chain
-   f-total {a} {b} ca cb = subst₂ (λ j k → Tri (j < k) (j ≡ k) (k < j)) *iso *iso uz01 where
-               uz01 : Tri (* (& a) < * (& b)) (* (& a) ≡ * (& b)) (* (& b) < * (& a) )
-               uz01 = ? -- chain-total A f supf ( (proj2 ca)) ( (proj2 cb))
+   f-total {a} {b} ca cb = ?
+  -- subst₂ (λ j k → Tri (j < k) (j ≡ k) (k < j)) *iso *iso uz01 where
+  --     uz01 : Tri (* (& a) < * (& b)) (* (& a) ≡ * (& b)) (* (& b) < * (& a) )
+   --    uz01 with trio< (& a) (& b)
+   --    ... | tri> ¬a ¬b c = ?
+    --   ... | tri≈ ¬a b ¬c = ?
+     --  ... | tri< a ¬b ¬c = ? 
 
    supf-inject : {x y : Ordinal } → supf x o< supf y → x o<  y
    supf-inject {x} {y} sx<sy with trio< x y
@@ -406,18 +403,37 @@
       → supf b o< supf z → supf b o< z → odef (UnionCF A f supf z) (supf b) -- supf z is not an element of this chain
    csupf mf< {b} sb<sz sb<z = cfcs mf< (supf-inject sb<sz) o≤-refl sb<z (init asupf refl)
 
-   fcy<sup  : {u w : Ordinal } → u o≤ z  → FClosure A f y w → (w ≡ supf u ) ∨ ( w << supf u ) -- different from order because y o< supf
-   fcy<sup  {u} {w} u≤z fc with MinSUP.x≤sup (minsup u≤z) ⟪ subst (λ k → odef A k ) (sym &iso) (A∋fc {A} y f mf fc) , ? ⟫ 
-   ... | case1 eq = case1 (subst (λ k → k ≡ supf u ) &iso  (trans eq (sym (supf-is-minsup u≤z ) ) ))
-   ... | case2 lt = case2 (subst₂ (λ j k → j << k ) &iso (sym (supf-is-minsup u≤z )) lt )
+   minsup : {x : Ordinal } → x o≤ z  → MinSUP A (UnionCF A f supf x)
+   minsup {x} x≤z = record { sup = supf x ; isMinSUP = is-minsup x≤z }
+
+   supf-is-minsup : {x : Ordinal } → (x≤z : x o≤ z) → supf x ≡ MinSUP.sup (minsup x≤z)
+   supf-is-minsup _ = refl
 
-   -- ordering is not proved here but in ZChain1
+   chain-minsup : {x : Ordinal} → IsMinSUP A (UnionCF A f supf x) (supf x)
+   chain-minsup {x} = record { as = as ; x≤sup = cp1 ; minsup = cpm } where
+        as : odef A (supf x)
+        as = asupf
+        cp1 : {z : Ordinal} → odef (UnionCF A f supf x) z → (z ≡ supf x) ∨ (z << supf x)
+        cp1 {z} ⟪ az , ch-is-sup u u<x supu=u fc ⟫ = order u<x fc
+        cpm :  {s : Ordinal} → odef A s → ({z : Ordinal} → odef (UnionCF A f supf x) z → (z ≡ s) ∨ (z << s)) → supf x o≤ s 
+        cpm {s} as z≤s with trio< (supf x) s
+        ... | tri< a ¬b ¬c = o<→≤ a
+        ... | tri≈ ¬a b ¬c = o≤-refl0 b
+        ... | tri> ¬a ¬b c = ? where
+             cp4 : supf (supf s) ≡ supf s
+             cp4 = ?
+             cp3 : supf s o< x
+             cp3 = ?
+             cp2 : odef (UnionCF A f supf x) (supf s)
+             cp2 =  ⟪ asupf , ch-is-sup (supf s) cp3 cp4 (init asupf cp4)  ⟫
+--        ... | case1 eq = ?
+--        ... | case2 lt = ?
 
    IsMinSUP→NotHasPrev : {x sp : Ordinal } → odef A sp
        → ({y : Ordinal} → odef (UnionCF A f supf x) y → (y ≡ sp ) ∨ (y << sp ))
        → ( {a : Ordinal } → odef A a → a << f a )
        → ¬ ( HasPrev A (UnionCF A f supf x) f sp )
-   IsMinSUP→NotHasPrev {x} {sp} asp is-sup <-mono-f hp = ⊥-elim (<-irr  ? sp<fsp ) where
+   IsMinSUP→NotHasPrev {x} {sp} asp is-sup <-mono-f hp = ⊥-elim (<<-irr fsp≤sp sp<fsp ) where
        sp<fsp : sp << f sp
        sp<fsp = <-mono-f asp
        pr = HasPrev.y hp
@@ -493,7 +509,7 @@
            ... | tri< a ¬b ¬c = ⊥-elim ( o≤> (
                begin
                  supfb x  ≡⟨ sbx=spb ⟩
-                 spb  ≤⟨ MinSUP.minsup mb (MinSUP.axm ma) (λ {z} uzb → MinSUP.x≤sup ma (z53 uzb)) ⟩
+                 spb  ≤⟨ MinSUP.minsup mb (MinSUP.as ma) (λ {z} uzb → MinSUP.x≤sup ma (z53 uzb)) ⟩
                  spa ≡⟨ sym sax=spa ⟩ 
                  supfa x ∎ ) a ) where 
                     open o≤-Reasoning O
@@ -502,7 +518,7 @@
            ... | tri> ¬a ¬b c = ⊥-elim ( o≤> (
                begin
                  supfa x  ≡⟨ sax=spa ⟩
-                 spa  ≤⟨ MinSUP.minsup ma (MinSUP.axm mb) (λ uza → MinSUP.x≤sup mb (z53 uza)) ⟩
+                 spa  ≤⟨ MinSUP.minsup ma (MinSUP.as mb) (λ uza → MinSUP.x≤sup mb (z53 uza)) ⟩
                  spb  ≡⟨ sym sbx=spb ⟩
                  supfb x ∎ ) c ) where 
                     open o≤-Reasoning O
@@ -578,7 +594,7 @@
                 ... | tri< a ¬b ¬c with prev z a
                 ... | case2 mins = case2 mins
                 ... | case1 not with ODC.p∨¬p O (odef A z ∧ xsup z)
-                ... | case1 mins = case2 record { sup = z ; isMinSUP = record { axm = proj1 mins ; x≤sup = proj2 mins ; minsup = m04 } } where
+                ... | case1 mins = case2 record { sup = z ; isMinSUP = record { as = proj1 mins ; x≤sup = proj2 mins ; minsup = m04 } } where
                   m04 : {sup1 : Ordinal} → odef A sup1 → ({w : Ordinal} → odef B w → (w ≡ sup1) ∨ (w << sup1)) → z o≤ sup1
                   m04 {s} as lt with trio< z s
                   ... | tri< a ¬b ¬c = o<→≤ a
@@ -869,7 +885,7 @@
                  asupf1 {z} with trio< z px
                  ... | tri< a ¬b ¬c = ZChain.asupf zc
                  ... | tri≈ ¬a b ¬c = ZChain.asupf zc
-                 ... | tri> ¬a ¬b c = MinSUP.axm sup1
+                 ... | tri> ¬a ¬b c = MinSUP.as sup1
 
                  supf1-mono : {a b : Ordinal } → a o≤ b → supf1 a o≤ supf1 b
                  supf1-mono {a} {b} a≤b with trio< b px
@@ -882,7 +898,7 @@
                        zc24 : {x₁ : Ordinal} → odef (UnionCF A f supf0 a) x₁ → (x₁ ≡ sp1) ∨ (x₁ << sp1)
                        zc24 {x₁} ux = MinSUP.x≤sup sup1 (case1 (chain-mono f mf ay supf0 (ZChain.supf-mono zc) (o<→≤ a<px) ux ) )
                        zc19 : supf0 a o≤ sp1
-                       zc19 = subst (λ k → k o≤ sp1) (sym (ZChain.supf-is-minsup zc  (o<→≤ a<px))) ( MinSUP.minsup zc21 (MinSUP.axm sup1) zc24 )
+                       zc19 = subst (λ k → k o≤ sp1) (sym (ZChain.supf-is-minsup zc  (o<→≤ a<px))) ( MinSUP.minsup zc21 (MinSUP.as sup1) zc24 )
                  ... | tri≈ ¬a b ¬c = zc18 where
                        zc21 : MinSUP A (UnionCF A f supf0 a)
                        zc21 = ZChain.minsup zc (o≤-refl0 b)
@@ -891,7 +907,7 @@
                        zc24 : {x₁ : Ordinal} → odef (UnionCF A f supf0 a) x₁ → (x₁ ≡ sp1) ∨ (x₁ << sp1)
                        zc24 {x₁} ux = MinSUP.x≤sup sup1 (case1 (chain-mono f mf ay supf0 (ZChain.supf-mono zc) (o≤-refl0 b) ux ) )
                        zc18 : supf0 a o≤ sp1
-                       zc18 = subst (λ k → k o≤ sp1) zc20( MinSUP.minsup zc21 (MinSUP.axm sup1) zc24 )
+                       zc18 = subst (λ k → k o≤ sp1) zc20( MinSUP.minsup zc21 (MinSUP.as sup1) zc24 )
                  ... | tri> ¬a ¬b c = o≤-refl
 
                  sf≤ :  { z : Ordinal } → x o≤ z → supf0 x o≤ supf1 z
@@ -1055,7 +1071,7 @@
 
                  sup : {z : Ordinal} → (z≤x : z o≤ x ) → STMP z≤x
                  sup {z} z≤x with trio< z px
-                 ... | tri< a ¬b ¬c = record { tsup = record { sup = MinSUP.sup m  ; asm = MinSUP.axm m
+                 ... | tri< a ¬b ¬c = record { tsup = record { sup = MinSUP.sup m  ; asm = MinSUP.as m
                          ; x≤sup = ms00 ; minsup = ms01 } ; tsup=sup = trans (sf1=sf0 (o<→≤ a) ) (ZChain.supf-is-minsup zc (o<→≤ a)) } where
                     m = ZChain.minsup zc (o<→≤ a)
                     ms00 :  {x : Ordinal} → odef (UnionCF A f supf1 z) x → (x ≡ MinSUP.sup m) ∨ (x << MinSUP.sup m)
@@ -1063,7 +1079,7 @@
                     ms01 : {sup2 : Ordinal} → odef A sup2 → ({x : Ordinal} →
                         odef (UnionCF A f supf1 z) x → (x ≡ sup2) ∨ (x << sup2)) → MinSUP.sup m o≤ sup2
                     ms01 {sup2} us P = MinSUP.minsup m us ?
-                 ... | tri≈ ¬a b ¬c = record { tsup = record { sup = MinSUP.sup m  ; asm = MinSUP.axm m
+                 ... | tri≈ ¬a b ¬c = record { tsup = record { sup = MinSUP.sup m  ; asm = MinSUP.as m
                          ; x≤sup = ms00 ; minsup = ms01 } ; tsup=sup = trans (sf1=sf0 (o≤-refl0 b) ) (ZChain.supf-is-minsup zc (o≤-refl0 b))  } where
                     m = ZChain.minsup zc (o≤-refl0 b)
                     ms00 :  {x : Ordinal} → odef (UnionCF A f supf1 z) x → (x ≡ MinSUP.sup m) ∨ (x << MinSUP.sup m)
@@ -1071,7 +1087,7 @@
                     ms01 : {sup2 : Ordinal} → odef A sup2 → ({x : Ordinal} →
                         odef (UnionCF A f supf1 z) x → (x ≡ sup2) ∨ (x << sup2)) → MinSUP.sup m o≤ sup2
                     ms01 {sup2} us P = MinSUP.minsup m us ?
-                 ... | tri> ¬a ¬b px<z = record { tsup = record { sup = sp1 ; asm = MinSUP.axm sup1
+                 ... | tri> ¬a ¬b px<z = record { tsup = record { sup = sp1 ; asm = MinSUP.as sup1
                          ; x≤sup = ms00 ; minsup = ms01 } ; tsup=sup = sf1=sp1 px<z } where
                     m = sup1
                     ms00 :  {x : Ordinal} → odef (UnionCF A f supf1 z) x → (x ≡ MinSUP.sup m) ∨ (x << MinSUP.sup m)
@@ -1173,7 +1189,7 @@
                      zc30 with osuc-≡< z≤x
                      ... | case1 eq = eq
                      ... | case2 z<x = ⊥-elim (¬p<x<op ⟪ px<z , subst (λ k → z o< k ) (sym (Oprev.oprev=x op)) z<x ⟫ )
-                     zc32 = ZChain.sup zc o≤-refl
+                     zc32 = ?
                      zc34 : ¬ (supf0 px ≡ px) → {w : HOD} → UnionCF A f supf0 z ∋ w → (w ≡ SUP.sup zc32) ∨ (w < SUP.sup zc32)
                      zc34 ne {w} lt = ?
                      zc33 : supf0 z ≡ & (SUP.sup zc32)
@@ -1374,7 +1390,7 @@
            sp : Ordinal
            sp = MinSUP.sup sp1
            asp : odef A sp
-           asp = MinSUP.axm sp1
+           asp = MinSUP.as sp1
            z10 :  {a b : Ordinal } → (ca : odef chain a ) → b o< (& A) → (ab : odef A b )
               →  HasPrev A chain f b  ∨  IsSUP A (UnionCF A f (ZChain.supf zc) b) b
               → * a < * b  → odef chain b
@@ -1400,7 +1416,7 @@
            z14 with ZChain.f-total zc (subst (λ k → odef chain k) (sym &iso)  (ZChain.f-next zc z12 )) (subst (λ k → odef chain k) (sym &iso) z12 )
            ... | tri< a ¬b ¬c = ⊥-elim z16 where
                z16 : ⊥
-               z16 with proj1 (mf (( MinSUP.sup sp1)) ( MinSUP.axm sp1 ))
+               z16 with proj1 (mf (( MinSUP.sup sp1)) ( MinSUP.as sp1 ))
                ... | case1 eq = ⊥-elim (¬b (sym (cong (*) eq ) ))
                ... | case2 lt = ⊥-elim (¬c lt )
            ... | tri≈ ¬a b ¬c = subst₂ (λ j k → j ≡ k ) &iso &iso ( cong (&) b )
@@ -1431,10 +1447,10 @@
 
      z04 :  (nmx : ¬ Maximal A ) → (zc : ZChain A (cf nmx) (cf-is-≤-monotonic nmx) as0 (& A)) → ⊥
      z04 nmx zc = <-irr0  {* (cf nmx c)} {* c}
-           (subst (λ k → odef A k ) (sym &iso) (proj1 (is-cf nmx (MinSUP.axm  msp1 ))))
-           (subst (λ k → odef A k) (sym &iso) (MinSUP.axm msp1) )
+           (subst (λ k → odef A k ) (sym &iso) (proj1 (is-cf nmx (MinSUP.as  msp1 ))))
+           (subst (λ k → odef A k) (sym &iso) (MinSUP.as msp1) )
            (case1 ( cong (*)( fixpoint (cf nmx) (cf-is-≤-monotonic nmx ) (cf-is-<-monotonic nmx ) zc msp1  ))) -- x ≡ f x ̄
-                (proj1 (cf-is-<-monotonic nmx c (MinSUP.axm msp1 ))) where          -- x < f x
+                (proj1 (cf-is-<-monotonic nmx c (MinSUP.as msp1 ))) where          -- x < f x
 
           supf = ZChain.supf zc
           msp1 : MinSUP A (ZChain.chain zc)