# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1662382495 -32400
# Node ID 717b8c3f55c9f07b9c05ecc022e1df92df6f66d6
# Parent  2d8ce664ae31385f9069712a5ec225198c4acfa0
...

diff -r 2d8ce664ae31 -r 717b8c3f55c9 src/zorn.agda
--- a/src/zorn.agda	Mon Sep 05 14:04:41 2022 +0900
+++ b/src/zorn.agda	Mon Sep 05 21:54:55 2022 +0900
@@ -738,19 +738,19 @@
 
           supf0 = ZChain.supf zc
 
-          supf1 : Ordinal → Ordinal
-          supf1 z with trio< z px
+          supf1 : (px z : Ordinal) → Ordinal
+          supf1 px z with trio< z px
           ... | tri< a ¬b ¬c = ZChain.supf zc z
           ... | tri≈ ¬a b ¬c = ZChain.supf zc z
           ... | tri> ¬a ¬b c = ZChain.supf zc px
 
           pchain1 : HOD
-          pchain1  = UnionCF A f mf ay supf1 x
+          pchain1  = UnionCF A f mf ay (supf1 px) x
 
           ptotal1 : IsTotalOrderSet pchain1
           ptotal1 {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 mf ay supf1 ( (proj2 ca)) ( (proj2 cb)) 
+               uz01 = chain-total A f mf ay (supf1 px) ( (proj2 ca)) ( (proj2 cb)) 
           pchain⊆A1 : {y : Ordinal} → odef pchain1 y →  odef A y
           pchain⊆A1 {y} ny = proj1 ny
           pnext1 : {a : Ordinal} → odef pchain1 a → odef pchain1 (f a)
@@ -760,49 +760,48 @@
           pinit1 {a} ⟪ aa , ua ⟫  with  ua
           ... | ch-init fc = s≤fc y f mf fc
           ... | ch-is-sup u u≤x is-sup fc = ≤-ftrans (<=to≤ zc7) (s≤fc _ f mf fc)  where
-               zc7 : y <= supf1 u 
+               zc7 : y <= supf1 px u 
                zc7 = ChainP.fcy<sup is-sup (init ay refl)
           pcy1 : odef pchain1 y
           pcy1 = ⟪ ay , ch-init (init ay refl)    ⟫
 
-          supf0=1 : {z : Ordinal } → z o≤ px  → supf0 z ≡ supf1 z
-          supf0=1 {z} z≤px with trio< z px
+          supf0=1 : {px z : Ordinal } → z o≤ px  → supf0 z ≡ supf1 px z
+          supf0=1 {px} {z} z≤px with trio< z px
           ... | tri< a ¬b ¬c = refl
           ... | tri≈ ¬a b ¬c = refl
           ... | tri> ¬a ¬b c = ⊥-elim ( o≤> z≤px c )
 
-          supf∈A : {b : Ordinal} → b o≤ x → odef A (supf1 b)
+          supf∈A : {b : Ordinal} → b o≤ x → odef A (supf1 px b)
           supf∈A {b} b≤z with trio< b px
           ... | tri< a ¬b ¬c = proj1 ( ZChain.csupf zc (o<→≤ a ))
           ... | tri≈ ¬a b ¬c = proj1 ( ZChain.csupf zc (o≤-refl0 b ))
           ... | tri> ¬a ¬b c = proj1 ( ZChain.csupf zc o≤-refl )
 
-          supf-mono : {a b : Ordinal } → a o≤ b → supf1 a o≤ supf1 b 
+          supf-mono : {a b : Ordinal } → a o≤ b → supf1 px a o≤ supf1 px b 
           supf-mono = ?
 
-          zc70 : HasPrev A pchain x f → ¬ xSUP pchain x 
-          zc70 pr xsup = ?
+          fc0→1 : {px s z : Ordinal } → s o≤ px  → FClosure A f (supf0 s) z → FClosure A f (supf1 px s) z  
+          fc0→1 {px} {s} {z} s≤px fc = subst (λ k → FClosure A f k z ) (supf0=1 s≤px) fc
 
-          fc0→1 : {s z : Ordinal } → s o≤ px  → FClosure A f (supf0 s) z → FClosure A f (supf1 s) z  
-          fc0→1 {s} {z} s≤px fc = subst (λ k → FClosure A f k z ) (supf0=1 s≤px) fc
+          fc1→0 : {px s z : Ordinal } → s o≤ px  → FClosure A f (supf1 px s) z → FClosure A f (supf0 s) z  
+          fc1→0 {px} {s} {z} s≤px fc = subst (λ k → FClosure A f k z ) (sym (supf0=1 s≤px)) fc
 
-          fc1→0 : {s z : Ordinal } → s o≤ px  → FClosure A f (supf1 s) z → FClosure A f (supf0 s) z  
-          fc1→0 {s} {z} s≤px fc = subst (λ k → FClosure A f k z ) (sym (supf0=1 s≤px)) fc
-
-          CP0→1 : {u : Ordinal } → u o≤ px  → ChainP A f mf ay supf0 u → ChainP A f mf ay supf1 u  
-          CP0→1 {u} u≤px cp = record { fcy<sup = fcy<sup ; order = order ; supu=u = trans (sym (supf0=1 u≤px)) (ChainP.supu=u cp) } where
-                  fcy<sup : {z : Ordinal} → FClosure A f y z → (z ≡ supf1 u) ∨ (z << supf1 u )
+          CP0→1 : {px u : Ordinal } → ({a b : Ordinal } → a o≤ b → supf1 px a o≤ supf1 px b)  
+              → u o≤ px  → ChainP A f mf ay supf0 u → ChainP A f mf ay (supf1 px) u  
+          CP0→1 {px} {u} supf-mono u≤px cp = record { fcy<sup = fcy<sup ; order = order ; supu=u = trans (sym (supf0=1 u≤px)) (ChainP.supu=u cp) } where
+                  fcy<sup : {z : Ordinal} → FClosure A f y z → (z ≡ supf1 px u) ∨ (z << supf1 px u )
                   fcy<sup {z} fc = subst ( λ k → (z ≡ k) ∨ (z << k )) (supf0=1 u≤px) ( ChainP.fcy<sup cp fc )
-                  order : {s : Ordinal} {z2 : Ordinal} → supf1 s o< supf1 u → FClosure A f (supf1 s) z2 →
-                    (z2 ≡ supf1 u) ∨ (z2 << supf1 u)
+                  order : {s : Ordinal} {z2 : Ordinal} → supf1 px s o< supf1 px u → FClosure A f (supf1 px s) z2 →
+                    (z2 ≡ supf1 px u) ∨ (z2 << supf1 px u)
                   order {s} {z2} s<u fc = subst (λ k → (z2 ≡ k) ∨ (z2 << k) ) (supf0=1 u≤px) ( ChainP.order cp ss<su (fc1→0 s≤px fc )) where
                       s≤px : s o≤ px
                       s≤px = ordtrans (supf-inject0 supf-mono s<u) u≤px
                       ss<su : supf0 s o< supf0 u
                       ss<su = subst₂ (λ j k → j o< k ) (sym (supf0=1 s≤px )) (sym (supf0=1 u≤px)) s<u
 
-          CP1→0 : {u : Ordinal } → u o≤ px  → ChainP A f mf ay supf1 u → ChainP A f mf ay supf0 u  
-          CP1→0 {u} u≤px cp = record { fcy<sup = fcy<sup ; order = order ; supu=u = trans (supf0=1 u≤px) (ChainP.supu=u cp) } where
+          CP1→0 : {px u : Ordinal } → ( {a b : Ordinal } → a o≤ b → supf1 px a o≤ supf1 px b) 
+               → u o≤ px  → ChainP A f mf ay (supf1 px) u → ChainP A f mf ay supf0 u  
+          CP1→0 {px} {u} supf-mono u≤px cp = record { fcy<sup = fcy<sup ; order = order ; supu=u = trans (supf0=1 u≤px) (ChainP.supu=u cp) } where
                   fcy<sup : {z : Ordinal} → FClosure A f y z → (z ≡ supf0 u) ∨ (z << supf0 u )
                   fcy<sup {z} fc = subst ( λ k → (z ≡ k) ∨ (z << k )) (sym (supf0=1 u≤px)) ( ChainP.fcy<sup cp fc )
                   order : {s : Ordinal} {z2 : Ordinal} → supf0 s o< supf0 u → FClosure A f (supf0 s) z2 →
@@ -810,18 +809,18 @@
                   order {s} {z2} s<u fc = subst (λ k → (z2 ≡ k) ∨ (z2 << k) ) (sym (supf0=1 u≤px)) ( ChainP.order cp ss<su (fc0→1 s≤px fc )) where
                       s≤px : s o≤ px
                       s≤px = ordtrans (supf-inject0 (ZChain.supf-mono zc) s<u) u≤px
-                      ss<su : supf1 s o< supf1 u
+                      ss<su : supf1 px s o< supf1 px u
                       ss<su = subst₂ (λ j k → j o< k ) (supf0=1 s≤px ) (supf0=1 u≤px) s<u
 
-          UnionCF0⊆1  : {z : Ordinal } → z o≤ px →  UnionCF A f mf ay supf0 z ⊆' UnionCF A f mf ay supf1 z
-          UnionCF0⊆1  {z} z≤px ⟪ au , ch-init fc ⟫ = ⟪ au , ch-init fc ⟫ 
-          UnionCF0⊆1  {z} z≤px ⟪ au , ch-is-sup u u≤z is-sup fc ⟫ = 
-               ⟪ au , ch-is-sup u u≤z (CP0→1 (OrdTrans u≤z z≤px ) is-sup) (fc0→1 (OrdTrans u≤z z≤px ) fc) ⟫ 
+          UnionCF0⊆1  : {px z : Ordinal } → ({a b : Ordinal } → a o≤ b → supf1 px a o≤ supf1 px b) → z o≤ px →  UnionCF A f mf ay supf0 z ⊆' UnionCF A f mf ay (supf1 px) z
+          UnionCF0⊆1 {px} {z} supf-mono z≤px ⟪ au , ch-init fc ⟫ = ⟪ au , ch-init fc ⟫ 
+          UnionCF0⊆1 {px} {z} supf-mono z≤px ⟪ au , ch-is-sup u u≤z is-sup fc ⟫ = 
+               ⟪ au , ch-is-sup u u≤z (CP0→1 supf-mono (OrdTrans u≤z z≤px ) is-sup) (fc0→1 (OrdTrans u≤z z≤px ) fc) ⟫ 
 
-          UnionCF1⊆0  : {z : Ordinal } → z o≤ px →  UnionCF A f mf ay supf1 z ⊆' UnionCF A f mf ay supf0 z
-          UnionCF1⊆0  {z} z≤px ⟪ au , ch-init fc ⟫ = ⟪ au , ch-init fc ⟫ 
-          UnionCF1⊆0  {z} z≤px ⟪ au , ch-is-sup u u≤z is-sup fc ⟫ = 
-               ⟪ au , ch-is-sup u u≤z (CP1→0 (OrdTrans u≤z z≤px ) is-sup) 
+          UnionCF1⊆0  : {px z : Ordinal } → ({a b : Ordinal } → a o≤ b → supf1 px a o≤ supf1 px b) → z o≤ px →  UnionCF A f mf ay (supf1 px) z ⊆' UnionCF A f mf ay supf0 z
+          UnionCF1⊆0 {px} {z} supf-mono z≤px ⟪ au , ch-init fc ⟫ = ⟪ au , ch-init fc ⟫ 
+          UnionCF1⊆0 {px} {z} supf-mono z≤px ⟪ au , ch-is-sup u u≤z is-sup fc ⟫ = 
+               ⟪ au , ch-is-sup u u≤z (CP1→0 supf-mono (OrdTrans u≤z z≤px ) is-sup) 
                                       (fc1→0 (OrdTrans u≤z z≤px ) fc) ⟫ 
 
           -- zc100  : xSUP (UnionCF A f mf ay supf0 px) x → x ≡ sp1
@@ -832,41 +831,59 @@
           --  supf0 px is sup of UnionCF px , supf0 x is sup of UnionCF x 
 
           no-extension : ¬ xSUP (UnionCF A f mf ay supf0 px) x → ZChain A f mf ay x
-          no-extension ¬sp=x = record { supf = supf1 ;  sup = sup ; supf-mono = supf-mono
+          no-extension ¬sp=x = record { supf = supf1 px ;  sup = sup ; supf-mono = supf-mono
                ; initial = pinit1 ; chain∋init = pcy1 ; sup=u = sup=u ; supf-is-sup = sis ; csupf = csupf
               ;  chain⊆A = λ lt → proj1 lt ;  f-next = pnext1 ;  f-total = ptotal1 }  where
                  pchain0=1 : pchain ≡ pchain1
                  pchain0=1 =  ==→o≡ record { eq→ = zc10 ; eq← = zc11 } where
                      zc10 :  {z : Ordinal} → OD.def (od pchain) z → OD.def (od pchain1) z
                      zc10 {z} ⟪ az , ch-init fc ⟫ = ⟪ az , ch-init fc ⟫ 
-                     zc10 {z} ⟪ az , ch-is-sup u1 u1≤x u1-is-sup fc ⟫ = ⟪ az , ch-is-sup u1 (ordtrans u1≤x (osucc (pxo<x op))) (CP0→1 u1≤x u1-is-sup)  (fc0→1 u1≤x fc)  ⟫
+                     zc10 {z} ⟪ az , ch-is-sup u1 u1≤x u1-is-sup fc ⟫ = ⟪ az , ch-is-sup u1 (ordtrans u1≤x (osucc (pxo<x op))) (CP0→1 supf-mono u1≤x u1-is-sup)  (fc0→1 u1≤x fc)  ⟫
                      zc11 :  {z : Ordinal} → OD.def (od pchain1) z → OD.def (od pchain) z
                      zc11 {z} ⟪ az , ch-init fc ⟫ = ⟪ az , ch-init fc ⟫ 
                      zc11 {z} ⟪ az , ch-is-sup u1 u1≤x u1-is-sup fc ⟫ with osuc-≡< u1≤x
-                     ... | case1 eq = ⊥-elim (¬sp=x zcsup) where
-                             x<sup : {w : Ordinal} → odef (UnionCF A f mf ay supf0 px) w → (w ≡ x) ∨ (w << x)
-                             x<sup = ?
-                             zc12 : supf1 x ≡ u1
-                             zc12 = subst  (λ k → supf1 k ≡ u1) eq  (ChainP.supu=u u1-is-sup)
-                             zcsup : xSUP (UnionCF A f mf ay supf0 px) x 
-                             zcsup = record { ax = subst (λ k → odef A k) (trans zc12 eq) (supf∈A o≤-refl) ; is-sup = record { x<sup = x<sup } }
-                     ... | case2 lt = ⟪ az , ch-is-sup u1 u1≤px (CP1→0 u1≤px u1-is-sup)  (fc1→0 u1≤px fc)  ⟫ where
+                     ... | case2 lt = ⟪ az , ch-is-sup u1 u1≤px (CP1→0 supf-mono u1≤px u1-is-sup)  (fc1→0 u1≤px fc)  ⟫ where
                                 u1≤px : u1 o≤ px  
                                 u1≤px = (subst (λ k → u1 o< k) (sym (Oprev.oprev=x op)) lt)
-                 sup : {z : Ordinal} → z o≤ x → SUP A (UnionCF A f mf ay supf1 z)
-                 sup {z} z≤x with trio< z px | inspect supf1 z
-                 ... | tri< a ¬b ¬c | record { eq = eq1} = SUP⊆ (UnionCF1⊆0 (o<→≤ a)) (ZChain.sup zc (o<→≤ a) ) 
-                 ... | tri≈ ¬a b ¬c | record { eq = eq1} = SUP⊆ (UnionCF1⊆0 (o≤-refl0 b)) (ZChain.sup zc (o≤-refl0 b) )
-                 ... | tri> ¬a ¬b px<z | record { eq = eq1} = ? where
+                     ... | case1 eq = ⊥-elim (¬sp=x zcsup) where
+                             s1u=x : supf1 px u1 ≡ x
+                             s1u=x = trans (ChainP.supu=u u1-is-sup) eq
+                             zc13 : osuc px o< osuc u1
+                             zc13 = o≤-refl0 ( trans (Oprev.oprev=x op) (sym eq) ) 
+                             x<sup : {w : Ordinal} → odef (UnionCF A f mf ay supf0 px) w → (w ≡ x) ∨ (w << x)
+                             x<sup {w} ⟪ az , ch-init {w} fc ⟫ = subst (λ k → (w ≡ k) ∨ (w << k)) s1u=x 
+                                  ( ChainP.fcy<sup u1-is-sup {w} fc  )
+                             x<sup {w} ⟪ az , ch-is-sup u u≤x is-sup fc ⟫ with osuc-≡< ( supf-mono (ordtrans u≤x zc13 ))
+                             ... | case1 eq1 = ⊥-elim ( o<¬≡ zc14 u≤x ) where
+                                 zc14 : u ≡ osuc px
+                                 zc14 = begin
+                                    u ≡⟨ sym ( ChainP.supu=u is-sup) ⟩ 
+                                    supf0 u ≡⟨ supf0=1 u≤x ⟩ 
+                                    supf1 px u ≡⟨ eq1 ⟩ 
+                                    supf1 px u1 ≡⟨ s1u=x ⟩ 
+                                    x ≡⟨ sym (Oprev.oprev=x op) ⟩ 
+                                    osuc px ∎ where open ≡-Reasoning
+                             ... | case2 lt = subst (λ k → (w ≡ k) ∨ (w << k)) s1u=x ( ChainP.order u1-is-sup lt (fc0→1 u≤x fc) ) 
+                             zc12 : supf1 px x ≡ u1
+                             zc12 = subst  (λ k → supf1 px k ≡ u1) eq  (ChainP.supu=u u1-is-sup)
+                             zcsup : xSUP (UnionCF A f mf ay supf0 px) x 
+                             zcsup = record { ax = subst (λ k → odef A k) (trans zc12 eq) (supf∈A o≤-refl) 
+                                 ; is-sup = record { x<sup = x<sup } }
+                 sup : {z : Ordinal} → z o≤ x → SUP A (UnionCF A f mf ay (supf1 px) z)
+                 sup {z} z≤x with trio< z px | inspect (supf1 px) z
+                 ... | tri< a ¬b ¬c | record { eq = eq1} = SUP⊆ (UnionCF1⊆0 supf-mono (o<→≤ a)) (ZChain.sup zc (o<→≤ a) ) 
+                 ... | tri≈ ¬a b ¬c | record { eq = eq1} = SUP⊆ (UnionCF1⊆0 supf-mono (o≤-refl0 b)) (ZChain.sup zc (o≤-refl0 b) )
+                 ... | tri> ¬a ¬b px<z | record { eq = eq1} = subst (λ k → SUP A k ) 
+                         (trans pchain0=1 (cong (λ k → UnionCF A f mf ay (supf1 px) k ) (sym zc30) )) (ZChain.sup zc o≤-refl ) where
                      zc30 : z ≡ x
                      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 ⟫ )
                  sup=u : {b : Ordinal} (ab : odef A b) →
-                    b o≤ x → IsSup A (UnionCF A f mf ay supf1 b) ab → supf1 b ≡ b
+                    b o≤ x → IsSup A (UnionCF A f mf ay (supf1 px) b) ab → (supf1 px) b ≡ b
                  sup=u {b} ab b≤x is-sup with trio< b px
-                 ... | tri< a ¬b ¬c = ZChain.sup=u zc ab (o<→≤ a) record { x<sup = λ lt → IsSup.x<sup is-sup (UnionCF0⊆1 (o<→≤ a) lt) } 
-                 ... | tri≈ ¬a b ¬c = ZChain.sup=u zc ab (o≤-refl0 b) record { x<sup = λ lt → IsSup.x<sup is-sup (UnionCF0⊆1 (o≤-refl0 b) lt) } 
+                 ... | tri< a ¬b ¬c = ZChain.sup=u zc ab (o<→≤ a) record { x<sup = λ lt → IsSup.x<sup is-sup (UnionCF0⊆1 supf-mono (o<→≤ a) lt) } 
+                 ... | tri≈ ¬a b ¬c = ZChain.sup=u zc ab (o≤-refl0 b) record { x<sup = λ lt → IsSup.x<sup is-sup (UnionCF0⊆1 supf-mono (o≤-refl0 b) lt) } 
                  ... | tri> ¬a ¬b px<b = ⊥-elim (¬sp=x zcsup ) where
                      zc30 : x ≡ b
                      zc30 with osuc-≡< b≤x
@@ -876,10 +893,10 @@
                      zcsup with zc30
                      ... | refl = record { ax = ab ; is-sup = record { x<sup = λ {w} lt → 
                         IsSup.x<sup is-sup (subst (λ k → odef k w) pchain0=1 lt)  } }
-                 csupf :  {b : Ordinal} → b o≤ x → odef (UnionCF A f mf ay supf1 (supf1 b)) (supf1 b)
+                 csupf :  {b : Ordinal} → b o≤ x → odef (UnionCF A f mf ay (supf1 px) (supf1 px b)) (supf1 px b)
                  csupf {b} b≤x = ⟪ zc01 , ch-is-sup u o≤-refl 
                           record { fcy<sup = fcy<sup ; order = order ; supu=u = supu=u } fc  ⟫  where
-                     csupf0 : b o≤ px → odef (UnionCF A f mf ay supf0 (supf1 b)) (supf1 b)
+                     csupf0 : b o≤ px → odef (UnionCF A f mf ay supf0 (supf1 px b)) (supf1 px b)
                      csupf0 b≤px = subst (λ k → odef (UnionCF A f mf ay supf0 k) k ) (supf0=1 b≤px) ( ZChain.csupf zc b≤px )
                      zc04 : (b o≤ px ) ∨ (b ≡ x )
                      zc04 with trio< b px 
@@ -888,36 +905,33 @@
                      ... | tri> ¬a ¬b px<b with osuc-≡< b≤x
                      ... | case1 eq = case2 eq
                      ... | case2 b<x = ⊥-elim ( ¬p<x<op ⟪ px<b , subst (λ k → b o< k ) (sym (Oprev.oprev=x op)) b<x  ⟫ ) 
-                     zc01 : odef A (supf1 b)
-                     zc01 with zc04
-                     ... | case1 le = proj1 ( csupf0 le )
-                     ... | case2 eq = ? -- subst (λ k → odef A k ) (sym (supf1=sp (o≤-refl0 (sym eq)))) (SUP.as sup1)
-                     u = supf1 b
-                     supu=u : supf1 u ≡ u
+                     zc01 : odef A (supf1 px b)
+                     zc01 = supf∈A b≤x
+                     u = supf1 px b
+                     supu=u : supf1 px u ≡ u
                      supu=u with zc04
                      ... | case2 eq = begin
-                        supf1 u ≡⟨ ? ⟩
+                        supf1 px u ≡⟨ ? ⟩
+                        supf0 px ≡⟨ ? ⟩
                         u ∎ where open ≡-Reasoning
-                     ... | case1 le = subst (λ k → k ≡ u ) (supf0=1 zc05 ) ( ZChain.sup=u zc zc01 zc05 ? )  where
+                     ... | case1 le = ? where
                          zc06 : b o≤ px
                          zc06 = le
-                         zc05 : supf1 b o≤ px
-                         zc05 = ?
-                     zc02 : odef A (supf1 u)
+                     zc02 : odef A (supf1 px u)
                      zc02 = subst (λ k → odef A k ) (sym supu=u) zc01
-                     zc03 : supf1 u ≡ supf1 b
+                     zc03 : supf1 px u ≡ supf1 px b
                      zc03 = ?
-                     fc : FClosure A f (supf1 u) (supf1 b)
+                     fc : FClosure A f (supf1 px u) (supf1 px b)
                      fc = init zc02 zc03 
-                     fcy<sup : {z : Ordinal} → FClosure A f y z → (z ≡ supf1 u) ∨ (z << supf1 u)
+                     fcy<sup : {z : Ordinal} → FClosure A f y z → (z ≡ supf1 px u) ∨ (z << supf1 px u)
                      fcy<sup = ? 
-                     order : {s z1 : Ordinal} → supf1 s o< supf1 u → FClosure A f (supf1 s) z1 
-                             → (z1 ≡ supf1 u) ∨ (z1 << supf1 u)
+                     order : {s z1 : Ordinal} → supf1 px s o< supf1 px u → FClosure A f (supf1 px s) z1 
+                             → (z1 ≡ supf1 px u) ∨ (z1 << supf1 px u)
                      order = ?
-                 sis : {z : Ordinal} (z≤x : z o≤ x) → supf1 z ≡ & (SUP.sup (sup z≤x))
+                 sis : {z : Ordinal} (z≤x : z o≤ x) → supf1 px z ≡ & (SUP.sup (sup z≤x))
                  sis {z} z≤x  = zc40 where
-                      zc40 : supf1 z ≡ & (SUP.sup (sup z≤x))  -- direct with statment causes error
-                      zc40 with trio< z px | inspect supf1 z | inspect sup z≤x
+                      zc40 : supf1 px z ≡ & (SUP.sup (sup z≤x))  -- direct with statment causes error
+                      zc40 with trio< z px | inspect (supf1 px) z | inspect sup z≤x
                       ... | tri< a ¬b ¬c | record { eq = eq1 } | record { eq = eq2 } = ?
                       ... | tri≈ ¬a b ¬c | record { eq = eq1 } | record { eq = eq2 } = ?
                       ... | tri> ¬a ¬b c | record { eq = eq1 } | record { eq = eq2 } = ?
@@ -930,7 +944,7 @@
           ... | case1 pr = no-extension {!!} -- we have previous A ∋ z < x , f z ≡ x, so chain ∋ f z ≡ x because of f-next
           ... | case2 ¬fy<x with ODC.p∨¬p O (IsSup A (ZChain.chain zc ) ax )
           ... | case1 is-sup = -- x is a sup of zc 
-                record {  supf = psupf1 ; chain⊆A = {!!} ; f-next = {!!} ; f-total = {!!} ; csupf = {!!} ; sup=u = {!!} ; supf-mono = {!!}
+                record {  supf = supf1 x ; chain⊆A = {!!} ; f-next = {!!} ; f-total = {!!} ; csupf = {!!} ; sup=u = {!!} ; supf-mono = {!!}
                    ;  initial = {!!} ; chain∋init  = {!!} ; sup = {!!} ; supf-is-sup = {!!}   }  where
              supx : SUP A (UnionCF A f mf ay supf0 x)
              supx = record { sup = * x ; as = subst (λ k → odef A k ) {!!} ax ; x<sup = {!!} }
@@ -938,10 +952,7 @@
              x=spx : x ≡ spx
              x=spx = sym &iso
              psupf1 : Ordinal → Ordinal
-             psupf1 z with trio< z x 
-             ... | tri< a ¬b ¬c = ZChain.supf zc z
-             ... | tri≈ ¬a b ¬c = x
-             ... | tri> ¬a ¬b c = x
+             psupf1 z = supf1 x z
              csupf : {b : Ordinal} → b o≤ x → odef (UnionCF A f mf ay psupf1 b) (psupf1 b)
              csupf {b} b≤x with trio< b px | inspect psupf1 b
              ... | tri< a ¬b ¬c | record { eq = eq1 } = ⟪ {!!} , {!!} ⟫