# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1659689861 -32400
# Node ID 171123c92007b30dbdcdf9454c649606c8155dd3
# Parent  408e7e8a379786acc3aafe34f52a2b5efcfc86a7
...

diff -r 408e7e8a3797 -r 171123c92007 src/OrdUtil.agda
--- a/src/OrdUtil.agda	Fri Aug 05 16:21:46 2022 +0900
+++ b/src/OrdUtil.agda	Fri Aug 05 17:57:41 2022 +0900
@@ -57,7 +57,7 @@
 ob<x : {b x : Ordinal} (lim : ¬ (Oprev Ordinal osuc x ) ) (b<x : b o< x ) → osuc b o< x                                        
 ob<x {b} {x} lim b<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 ob=x ¬c = ⊥-elim ( lim record { oprev = b ; oprev=x = ob=x }  )                                                     
 ... | tri> ¬a ¬b c = ⊥-elim ( ¬p<x<op ⟪ b<x , c ⟫ )                           
 
 osucc :  {ox oy : Ordinal } → oy o< ox  → osuc oy o< osuc ox  
diff -r 408e7e8a3797 -r 171123c92007 src/zorn.agda
--- a/src/zorn.agda	Fri Aug 05 16:21:46 2022 +0900
+++ b/src/zorn.agda	Fri Aug 05 17:57:41 2022 +0900
@@ -124,115 +124,29 @@
 ... | case1 s≡x = case2 ( subst₂ (λ j k → j < k ) (sym s≡x) refl x<fx )
 ... | case2 s<x = case2 ( IsStrictPartialOrder.trans PO s<x x<fx )
 
-fcn : {A : HOD} (s : Ordinal) { x : Ordinal} {f : Ordinal → Ordinal} → (mf : ≤-monotonic-f A f) → FClosure A f s x → ℕ
-fcn s mf (init as refl) = zero
-fcn {A} s {x} {f} mf (fsuc y p) with proj1 (mf y (A∋fc s f mf p))
-... | case1 eq = fcn s mf p
-... | case2 y<fy = suc (fcn s mf p )
-
-fcn-inject : {A : HOD} (s : Ordinal) { x y : Ordinal} {f : Ordinal → Ordinal} → (mf : ≤-monotonic-f A f) 
-     → (cx : FClosure A f s x ) (cy : FClosure A f s y ) → fcn s mf cx  ≡ fcn s mf cy → * x ≡ * y
-fcn-inject {A} s {x} {y} {f} mf cx cy eq = fc00 (fcn s mf cx) (fcn s mf cy) eq cx cy refl refl where
-     fc00 :  (i j : ℕ ) → i ≡ j  →  {x y : Ordinal } → (cx : FClosure A f s x ) (cy : FClosure A f s y ) → i ≡ fcn s mf cx  → j ≡ fcn s mf cy → * x ≡ * y
-     fc00 zero zero refl (init _ refl) (init x₁ refl) i=x i=y = refl
-     fc00 zero zero refl (init as refl) (fsuc y cy) i=x i=y with proj1 (mf y (A∋fc s f mf cy ) )
-     ... | case1 y=fy = subst (λ k → * s ≡ k ) y=fy ( fc00 zero zero refl (init as refl) cy i=x i=y )
-     fc00 zero zero refl (fsuc x cx) (init as refl) i=x i=y with proj1 (mf x (A∋fc s f mf cx ) )
-     ... | case1 x=fx = subst (λ k → k ≡ * s ) x=fx ( fc00 zero zero refl cx (init as refl) i=x i=y )
-     fc00 zero zero refl (fsuc x cx) (fsuc y cy) i=x i=y with proj1 (mf x (A∋fc s f mf cx ) ) | proj1 (mf y (A∋fc s f mf cy ) )
-     ... | case1 x=fx  | case1 y=fy = subst₂ (λ j k → j ≡ k ) x=fx y=fy ( fc00 zero zero refl cx cy  i=x i=y )
-     fc00 (suc i) (suc j) i=j {.(f x)} {.(f y)} (fsuc x cx) (fsuc y cy) i=x j=y with proj1 (mf x (A∋fc s f mf cx ) ) | proj1 (mf y (A∋fc s f mf cy ) )
-     ... | case1 x=fx | case1 y=fy = subst₂ (λ j k → j ≡ k ) x=fx y=fy ( fc00 (suc i) (suc j) i=j cx cy  i=x j=y )
-     ... | case1 x=fx | case2 y<fy = subst (λ k → k ≡ * (f y)) x=fx (fc02 x cx i=x) where
-          fc02 : (x1 : Ordinal) → (cx1 : FClosure A f s x1 ) →  suc i ≡ fcn s mf cx1 → * x1 ≡ * (f y)
-          fc02 .(f x1) (fsuc x1 cx1) i=x1 with proj1 (mf x1 (A∋fc s f mf cx1 ) )
-          ... | case1 eq = trans (sym eq) ( fc02  x1 cx1 i=x1 )  -- derefence while f x ≡ x
-          ... | case2 lt = subst₂ (λ j k → * (f j) ≡ * (f k )) &iso &iso ( cong (λ k → * ( f (& k ))) fc04) where
-               fc04 : * x1 ≡ * y
-               fc04 = fc00 i j (cong pred i=j) cx1 cy (cong pred i=x1) (cong pred j=y)
-     ... | case2 x<fx | case1 y=fy = subst (λ k → * (f x) ≡ k ) y=fy (fc03 y cy j=y) where
-          fc03 : (y1 : Ordinal) → (cy1 : FClosure A f s y1 ) →  suc j ≡ fcn s mf cy1 → * (f x)  ≡ * y1
-          fc03 .(f y1) (fsuc y1 cy1) j=y1 with proj1 (mf y1 (A∋fc s f mf cy1 ) )
-          ... | case1 eq = trans ( fc03  y1 cy1 j=y1 ) eq 
-          ... | case2 lt = subst₂ (λ j k → * (f j) ≡ * (f k )) &iso &iso ( cong (λ k → * ( f (& k ))) fc05) where
-               fc05 : * x ≡ * y1
-               fc05 = fc00 i j (cong pred i=j) cx cy1 (cong pred i=x) (cong pred j=y1)
-     ... | case2 x₁ | case2 x₂ = subst₂ (λ j k → * (f j) ≡ * (f k) ) &iso &iso (cong (λ k → * (f (& k))) (fc00 i j (cong pred i=j) cx cy (cong pred i=x) (cong pred j=y)))
-
-
-fcn-< : {A : HOD} (s : Ordinal ) { x y : Ordinal} {f : Ordinal → Ordinal} → (mf : ≤-monotonic-f A f)
-    → (cx : FClosure A f s x ) (cy : FClosure A f s y ) → fcn s mf cx Data.Nat.< fcn s mf cy  → * x < * y
-fcn-< {A} s {x} {y} {f} mf cx cy x<y = fc01 (fcn s mf cy) cx cy refl x<y where
-     fc01 : (i : ℕ ) → {y : Ordinal } → (cx : FClosure A f s x ) (cy : FClosure A f s y ) → (i ≡ fcn s mf cy ) → fcn s mf cx Data.Nat.< i → * x < * y
-     fc01 (suc i) {y} cx (fsuc y1 cy) i=y (s≤s x<i) with proj1 (mf y1 (A∋fc s f mf cy ) )
-     ... | case1 y=fy = subst (λ k → * x < k ) y=fy ( fc01 (suc i) {y1} cx cy i=y (s≤s x<i)  ) 
-     ... | case2 y<fy with <-cmp (fcn s mf cx ) i
-     ... | tri> ¬a ¬b c = ⊥-elim ( nat-≤> x<i c )
-     ... | tri≈ ¬a b ¬c = subst (λ k → k < * (f y1) ) (fcn-inject s mf cy cx (sym (trans b (cong pred i=y) ))) y<fy 
-     ... | tri< a ¬b ¬c = IsStrictPartialOrder.trans PO fc02 y<fy where
-          fc03 :  suc i ≡ suc (fcn s mf cy) → i ≡ fcn s mf cy
-          fc03 eq = cong pred eq 
-          fc02 :  * x < * y1 
-          fc02 =  fc01 i cx cy (fc03 i=y ) a
 
 fcn-cmp : {A : HOD} (s : Ordinal) { x y : Ordinal } (f : Ordinal → Ordinal) (mf : ≤-monotonic-f A f) 
     → (cx : FClosure A f s x) → (cy : FClosure A f s y ) → Tri (* x < * y) (* x ≡ * y) (* y < * x )
-fcn-cmp {A} s {x} {y} f mf cx cy with <-cmp ( fcn s mf cx ) (fcn s mf cy )
-... | tri< a ¬b ¬c = tri< fc11 (λ eq → <-irr (case1 (sym eq)) fc11) (λ lt → <-irr (case2 fc11) lt) where
-      fc11 : * x < * y
-      fc11 = fcn-< {A} s {x} {y} {f} mf cx cy a
-... | tri≈ ¬a b ¬c = tri≈ (λ lt → <-irr (case1 (sym fc10)) lt) fc10 (λ lt → <-irr (case1 fc10) lt) where
-      fc10 : * x ≡ * y
-      fc10 = fcn-inject {A} s {x} {y} {f} mf cx cy b
-... | tri> ¬a ¬b c = tri> (λ lt → <-irr (case2 fc12) lt) (λ eq → <-irr (case1 eq) fc12) fc12  where 
-      fc12 : * y < * x
-      fc12 = fcn-< {A} s {y} {x} {f} mf cy cx c
-
+fcn-cmp-1 : {A : HOD} (s : Ordinal) { x y : Ordinal } (f : Ordinal → Ordinal) (mf : ≤-monotonic-f A f) 
+    → (cx : FClosure A f s x) → (cy : FClosure A f s y ) → * x < * y → (* (f x) ≡ * y) ∨ ( * (f x) < * y )
+fcn-cmp-1 {A} s f mf (init x refl) (init x₁ refl) x<y = {!!}
+fcn-cmp-1 {A} s f mf (init x refl) (fsuc x₁ cy) x<y = {!!}
+fcn-cmp-1 {A} s f mf (fsuc x cx) (init ay refl) x<y = {!!}
+fcn-cmp-1 {A} s f mf (fsuc x cx) (fsuc y cy) x<y with proj1 (mf x (A∋fc s f mf cx)) | proj1 (mf y (A∋fc s f mf cy)) 
+... | case1 eqx | case1 eqy = {!!}
+... | case1 eqx | case2 lt = {!!}
+... | case2 lt  | case1 eqy = {!!}
+... | case2 ltx | case2 lty = {!!}
 
-fcn-imm : {A : HOD} (s : Ordinal) { x y : Ordinal } (f : Ordinal → Ordinal) (mf : ≤-monotonic-f A f) 
-    → (cx : FClosure A f s x) → (cy : FClosure A f s y ) → ¬ ( ( * x < * y ) ∧ ( * y < * (f x )) ) 
-fcn-imm {A} s {x} {y} f mf cx cy ⟪ x<y , y<fx ⟫ = fc21 where
-      fc20 : fcn s mf cy Data.Nat.< suc (fcn s mf cx) → (fcn s mf cy ≡ fcn s mf cx) ∨ ( fcn s mf cy Data.Nat.< fcn s mf cx )
-      fc20 y<sx with <-cmp ( fcn s mf cy ) (fcn s mf cx )
-      ... | tri< a ¬b ¬c = case2 a
-      ... | tri≈ ¬a b ¬c = case1 b
-      ... | tri> ¬a ¬b c = ⊥-elim ( nat-≤> y<sx (s≤s c))
-      fc17 : {x y : Ordinal } → (cx : FClosure A f s x) → (cy : FClosure A f s y ) → suc (fcn s mf cx) ≡ fcn s mf cy → * (f x ) ≡ * y
-      fc17 {x} {y} cx cy sx=y = fc18 (fcn s mf cy) cx cy refl sx=y  where
-          fc18 : (i : ℕ ) → {y : Ordinal } → (cx : FClosure A f s x ) (cy : FClosure A f s y ) → (i ≡ fcn s mf cy ) → suc (fcn s mf cx) ≡  i → * (f x) ≡ * y
-          fc18 (suc i) {y} cx (fsuc y1 cy)  i=y sx=i with proj1 (mf y1 (A∋fc s f mf cy ) )
-          ... | case1 y=fy = subst (λ k → * (f x) ≡  k ) y=fy ( fc18 (suc i) {y1} cx cy i=y sx=i)  -- dereference
-          ... | case2 y<fy = subst₂ (λ j k → * (f j) ≡ * (f k) ) &iso &iso (cong (λ k → * (f (& k) ) ) fc19) where
-               fc19 : * x ≡ * y1
-               fc19 = fcn-inject s mf cx cy (cong pred ( trans sx=i i=y ))
-      fc21 :  ⊥
-      fc21 with <-cmp (suc ( fcn s mf cx )) (fcn s mf cy )
-      ... | tri< a ¬b ¬c = <-irr (case2 y<fx) (fc22 a) where -- suc ncx < ncy
-           cxx :  FClosure A f s (f x)
-           cxx = fsuc x cx 
-           fc16 : (x : Ordinal ) → (cx : FClosure A f s x) → (fcn s mf cx  ≡ fcn s mf (fsuc x cx)) ∨ ( suc (fcn s mf cx ) ≡ fcn s mf (fsuc x cx))
-           fc16 x (init as refl) with proj1 (mf s as )
-           ... | case1 _ = case1 refl
-           ... | case2 _ = case2 refl
-           fc16 .(f x) (fsuc x cx ) with proj1 (mf (f x) (A∋fc s f mf (fsuc x cx)) )
-           ... | case1 _ = case1 refl 
-           ... | case2 _ = case2 refl
-           fc22 : (suc ( fcn s mf cx ))  Data.Nat.< (fcn s mf cy ) → * (f x) < * y
-           fc22 a with fc16 x cx
-           ... | case1 eq = fcn-< s mf cxx cy (subst (λ k → k Data.Nat.< fcn s mf cy ) eq (<-trans a<sa a))
-           ... | case2 eq = fcn-< s mf cxx cy (subst (λ k → k Data.Nat.< fcn s mf cy ) eq a )
-      ... | tri≈ ¬a b ¬c = <-irr (case1 (fc17 cx cy b)) y<fx
-      ... | tri> ¬a ¬b c with fc20 c -- ncy < suc ncx
-      ... | case1 y=x = <-irr (case1 ( fcn-inject s mf cy cx  y=x ))  x<y
-      ... | case2 y<x = <-irr (case2 x<y) (fcn-< s mf cy cx y<x ) 
+fcn-cmp {A} s {.s} {y} f mf (init ax refl) (init ay refl) = {!!}
+fcn-cmp {A} s {.s} {.(f x)} f mf (init ax refl) (fsuc x cy) = {!!}
+fcn-cmp {A} s {.(f x)} {y} f mf (fsuc x cx) (init ay refl) = {!!}
+fcn-cmp {A} s {.(f x)} {.(f y)} f mf (fsuc x cx) (fsuc y cy) with proj1 (mf x (A∋fc s f mf cx)) | proj1 (mf y (A∋fc s f mf cy)) 
+... | case1 eqx | case1 eqy = {!!}
+... | case1 eqx | case2 lt = {!!}
+... | case2 lt  | case1 eqy = {!!}
+... | case2 ltx | case2 lty = {!!}
 
-fc-conv : (A : HOD ) (f : Ordinal → Ordinal) {b u : Ordinal } 
-      →  {p0 p1 : Ordinal → Ordinal}
-      →  p0 u ≡ p1 u
-      →  FClosure A f (p0 u) b → FClosure A f (p1 u) b 
-fc-conv A f {.(p0 u)} {u}  {p0} {p1} p0u=p1u (init ap0u refl) = subst (λ k → FClosure A f (p1 u) k) (sym p0u=p1u) 
-       ( init (subst (λ k → odef A k) p0u=p1u ap0u ) refl)
-fc-conv A f {_} {u}  {p0} {p1} p0u=p1u (fsuc z fc) = fsuc z (fc-conv A f {_} {u}  {p0} {p1} p0u=p1u fc)
 
 -- open import Relation.Binary.Properties.Poset as Poset
 
@@ -312,25 +226,13 @@
       sup : {x : Ordinal } → x o≤ z  → SUP A (UnionCF A f mf ay supf x)
       sup=u : {b : Ordinal} → (ab : odef A b) → b o< z  → IsSup A (UnionCF A f mf ay supf (osuc b)) ab → supf b ≡ b 
       supf-is-sup : {x : Ordinal } → (x≤z : x o≤ z) → supf x ≡ & (SUP.sup (sup x≤z) )
+      csupf : {b : Ordinal } → b o< z → odef (UnionCF A f mf ay supf b) (supf b) 
+      supf-mono : {x y : Ordinal } → x o< y → supf x o≤ supf y
    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 SUP.x<sup (sup (o<→≤ u<z)) ⟪ subst (λ k → odef A k ) (sym &iso) (A∋fc {A} y f mf fc)  
        , ch-init (subst (λ k → FClosure A f y k) (sym &iso) fc ) ⟫ 
    ... | case1 eq = case1 (subst (λ k → k ≡ supf u ) &iso  (trans (cong (&) eq) (sym (supf-is-sup (o<→≤ u<z) ) ) ))
    ... | case2 lt = case2 (subst (λ k → * w < k ) (subst (λ k → k ≡ _ ) *iso (cong (*) (sym (supf-is-sup (o<→≤ u<z) ))) ) lt )
-
-   csupf : {b : Ordinal } → b o< z → odef (UnionCF A f mf ay supf b) (supf b) 
-   csupf {b} b<z = ⟪ asb , ch-is-sup b o≤-refl is-sup (init asb refl)  ⟫ where
-       asb : odef A (supf b)
-       asb = subst (λ k → odef A k ) (sym (supf-is-sup ? )) (SUP.A∋maximal (sup ? ))
-       is-sup : ChainP A f mf ay supf b
-       is-sup = record { fcy<sup = fcy<sup b<z ; order = ? ; supu=u = ? }
-   supf-mono : {x y : Ordinal } → x o< y → supf x o≤ supf y
-   supf-mono = ?
-   -- supf-is-sup {x} x≤z  = ? where
-   --   zc51 : * (supf x) ≡ SUP.sup (sup x≤z )  
-   --   zc51 = ==→o≡ record { eq→  ? ; eq← = ? }
-   --   zc50 : supf x ≡ & (SUP.sup (sup x<z) )
-   --   zc50 = ?
    order : {b s z1 : Ordinal} → b o< z → supf s o< supf b → FClosure A f (supf s) z1 → (z1 ≡ supf b) ∨ (z1 << supf b)
    order {b} {s} {z1} b<z sf<sb fc = zc04 where
         zc01 : {z1 : Ordinal } → FClosure A f (supf s) z1 → UnionCF A f mf ay supf b ∋ * z1
@@ -558,7 +460,7 @@
                            → FClosure A f (ZChain.supf zc sup1) z1 → z1 <= ZChain.supf zc b
               m09 {sup1} {z} s<b fcz = ZChain.order zc b<A s<b fcz
               m06 : ChainP A f mf ay (ZChain.supf zc) b 
-              m06 = record {  fcy<sup = m08  ; order = m09 ; supu=u = λ _ → ZChain.sup=u zc ab b<A ? } 
+              m06 = record {  fcy<sup = m08  ; order = m09 ; supu=u = λ _ → ZChain.sup=u zc ab b<A {!!} } 
         ... | no lim = record { is-max = is-max }  where
            is-max :  {a : Ordinal} {b : Ordinal} → odef (UnionCF A f mf ay (ZChain.supf zc) x) a →
               b o< x → (ab : odef A b) →
@@ -580,7 +482,7 @@
               m05 = sym (ZChain.sup=u zc ab m09
                       record { x<sup = λ lt → IsSup.x<sup is-sup (chain-mono1 (osucc b<x) lt )} )   -- ZChain on x
               m06 : ChainP A f mf ay (ZChain.supf zc) b 
-              m06 = record { fcy<sup = m07 ;  order = m08 ; supu=u = λ _ → ZChain.sup=u zc ab m09 ? }
+              m06 = record { fcy<sup = m07 ;  order = m08 ; supu=u = λ _ → ZChain.sup=u zc ab m09 {!!} }
 
      ---
      --- the maximum chain  has fix point of any ≤-monotonic function
@@ -660,8 +562,8 @@
      ysup f mf {y} ay = supP (uchain f mf ay) (λ lt → A∋fc y f mf lt)  (utotal f mf ay) 
 
      initChain : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) {y : Ordinal} (ay : odef A y) → ZChain A f mf ay o∅
-     initChain f mf {y} ay = record { supf = isupf ; chain⊆A = λ lt → proj1 lt ; chain∋init = cy  ; sup = ? ; supf-is-sup = ? 
-      ; initial = isy ; f-next = inext ; f-total = itotal ; sup=u = λ _ b<0 → ⊥-elim (¬x<0 b<0) ; supf-mono = mono ; csupf = csupf } where
+     initChain f mf {y} ay = record { supf = isupf ; chain⊆A = λ lt → proj1 lt ; chain∋init = cy  ; sup = {!!} ; supf-is-sup = {!!} 
+      ; initial = isy ; f-next = inext ; f-total = itotal ; sup=u = λ _ b<0 → ⊥-elim (¬x<0 b<0) ; supf-mono = mono ; csupf = {!!} } where
           spi =  & (SUP.sup (ysup f mf ay))
           isupf : Ordinal → Ordinal
           isupf z = spi
@@ -733,7 +635,7 @@
           pchain⊆A {y} ny = proj1 ny
           pnext : {a : Ordinal} → odef pchain a → odef pchain (f a)
           pnext {a} ⟪ aa , ch-init fc ⟫ = ⟪ proj2 (mf a aa) , ch-init (fsuc _ fc)  ⟫
-          pnext {a} ⟪ aa , ch-is-sup u u≤x is-sup fc ⟫ = ⟪ proj2 (mf a aa) , ch-is-sup u ? is-sup (fsuc _ fc ) ⟫
+          pnext {a} ⟪ aa , ch-is-sup u u≤x is-sup fc ⟫ = ⟪ proj2 (mf a aa) , ch-is-sup u {!!} is-sup (fsuc _ fc ) ⟫
           pinit :  {y₁ : Ordinal} → odef pchain y₁ → * y ≤ * y₁
           pinit {a} ⟪ aa , ua ⟫  with  ua
           ... | ch-init fc = s≤fc y f mf fc
@@ -758,13 +660,13 @@
           --
           --  supf0 px is sup of UnionCF px , supf0 x is sup of UnionCF x 
           no-extension : ¬  sp1 ≡ x → ZChain A f mf ay x
-          no-extension ¬sp=x = record { supf = supf1 ; supf-mono = ? ; sup = sup
-               ; initial = ? ; chain∋init = ?  ; sup=u = {!!} ; supf-is-sup = ? ; csupf = ? 
-              ;  chain⊆A = ? ;  f-next = ? ;  f-total = ? }  where
+          no-extension ¬sp=x = record { supf = supf1 ; supf-mono = {!!} ; sup = sup
+               ; initial = {!!} ; chain∋init = {!!}  ; sup=u = {!!} ; supf-is-sup = {!!} ; csupf = {!!} 
+              ;  chain⊆A = {!!} ;  f-next = {!!} ;  f-total = {!!} }  where
                  UnionCF⊆ : UnionCF A f mf ay supf1 x ⊆' UnionCF A f mf ay supf0 x 
                  UnionCF⊆ ⟪ as , ch-init fc ⟫ = UnionCF⊆ ⟪ as , ch-init fc ⟫ 
                  UnionCF⊆ ⟪ as , ch-is-sup u {z} u≤x record { fcy<sup = f1 ; order = o1 ; supu=u = su=u1 }  fc ⟫ with trio< u px
-                 ... | tri< a ¬b ¬c = ⟪ as , ch-is-sup u {z} u≤x record { fcy<sup = f1 ; order = order0 ; supu=u = ? } fc ⟫  where
+                 ... | tri< a ¬b ¬c = ⟪ as , ch-is-sup u {z} u≤x record { fcy<sup = f1 ; order = order0 ; supu=u = {!!} } fc ⟫  where
                      order0 : {s z1 : Ordinal}  → supf0 s o< supf0 u → FClosure A f (supf0 s) z1 
                         → (z1 ≡ supf0 u) ∨ (z1 << supf0 u)
                      order0 {s} {z1} ss<su fc with trio< s px | inspect supf1 s
@@ -772,8 +674,8 @@
                                                                           (subst (λ k → FClosure A f k z1 ) (sym eq1) fc )
                      ... | tri≈ ¬a b ¬c | record {eq = eq1} = o1 {s} {z1} (subst (λ k → k o< supf0 u) (sym eq1) ss<su )  
                                                                           (subst (λ k → FClosure A f k z1 ) (sym eq1) fc )
-                     ... | tri> ¬a ¬b c | record {eq = eq1} = ?
-                 ... | tri≈ ¬a b ¬c = ⟪ as , ch-is-sup u {z} u≤x record { fcy<sup = f1 ; order = order0  ; supu=u = ?} fc ⟫ where
+                     ... | tri> ¬a ¬b c | record {eq = eq1} = {!!}
+                 ... | tri≈ ¬a b ¬c = ⟪ as , ch-is-sup u {z} u≤x record { fcy<sup = f1 ; order = order0  ; supu=u = {!!}} fc ⟫ where
                      order0 : {s z1 : Ordinal}  → supf0 s o< supf0 u → FClosure A f (supf0 s) z1 
                         → (z1 ≡ supf0 u) ∨ (z1 << supf0 u)
                      order0 {s} {z1} ss<su fc with trio< s px | inspect supf1 s
@@ -781,48 +683,48 @@
                                                                           (subst (λ k → FClosure A f k z1 ) (sym eq1) fc )
                      ... | tri≈ ¬a b ¬c | record {eq = eq1} = o1 {s} {z1} (subst (λ k → k o< supf0 u) (sym eq1) ss<su )  
                                                                           (subst (λ k → FClosure A f k z1 ) (sym eq1) fc )
-                     ... | tri> ¬a ¬b px<s | record {eq = eq1} = ⊥-elim ( ¬sp=x (subst (λ k → sp1 ≡ k ) u=x ? )) where
+                     ... | tri> ¬a ¬b px<s | record {eq = eq1} = ⊥-elim ( ¬sp=x (subst (λ k → sp1 ≡ k ) u=x {!!} )) where
                          s≤u : s o≤ u
-                         s≤u = ?
+                         s≤u = {!!}
                          u=x : u ≡ x
                          u=x with trio< u x
-                         ... | tri< a ¬b ¬c = ?
+                         ... | tri< a ¬b ¬c = {!!}
                          ... | tri≈ ¬a b ¬c = b
-                         ... | tri> ¬a ¬b c = ?
-                 ... | tri> ¬a ¬b c = ⊥-elim ( ¬sp=x (subst (λ k → sp1 ≡ k ) u=x (su=u1 ?) )) where
+                         ... | tri> ¬a ¬b c = {!!}
+                 ... | tri> ¬a ¬b c = ⊥-elim ( ¬sp=x (subst (λ k → sp1 ≡ k ) u=x (su=u1 {!!}) )) where
                       u=x : u ≡ x
                       u=x with trio< u x
-                      ... | tri< a ¬b ¬c = ?
+                      ... | tri< a ¬b ¬c = {!!}
                       ... | tri≈ ¬a b ¬c = b
-                      ... | tri> ¬a ¬b c = ?
+                      ... | tri> ¬a ¬b c = {!!}
                  sup : {z : Ordinal} → z o≤ x → SUP A (UnionCF A f mf ay supf1 z)
                  sup {z} z≤x with trio< z px
-                 ... | tri< a ¬b ¬c = SUP⊆ ? (ZChain.sup zc (o<→≤ a))
-                 ... | tri≈ ¬a b ¬c = SUP⊆ ? (ZChain.sup zc (o≤-refl0 b))
-                 ... | tri> ¬a ¬b c = SUP⊆ ? sup1
+                 ... | tri< a ¬b ¬c = SUP⊆ {!!} (ZChain.sup zc (o<→≤ a))
+                 ... | tri≈ ¬a b ¬c = SUP⊆ {!!} (ZChain.sup zc (o≤-refl0 b))
+                 ... | tri> ¬a ¬b c = SUP⊆ {!!} sup1
 
           zc4 : ZChain A f mf ay x 
           zc4 with ODC.∋-p O A (* x)
-          ... | no noax = no-extension ? -- ¬ A ∋ p, just skip
+          ... | no noax = no-extension {!!} -- ¬ A ∋ p, just skip
           ... | yes ax with ODC.p∨¬p O ( HasPrev A (ZChain.chain zc ) ax f )   
                -- we have to check adding x preserve is-max ZChain A y f mf x
-          ... | case1 pr = no-extension ? -- we have previous A ∋ z < x , f z ≡ x, so chain ∋ f z ≡ x because of f-next
+          ... | 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 = {!!} ; initial = {!!} ; chain∋init  = {!!} ; sup = ? ; supf-is-sup = ? ; supf-mono = ? }  where
+                   ; supf-mono = {!!} ; initial = {!!} ; chain∋init  = {!!} ; sup = {!!} ; supf-is-sup = {!!} ; supf-mono = {!!} }  where
              supx : SUP A (UnionCF A f mf ay supf0 x)
-             supx = record { sup = * x ; A∋maximal = subst (λ k → odef A k ) ? ax ; x<sup = ? }
+             supx = record { sup = * x ; A∋maximal = subst (λ k → odef A k ) {!!} ax ; x<sup = {!!} }
              spx = & (SUP.sup supx )
              x=spx : x ≡ spx
-             x=spx = ?
+             x=spx = {!!}
              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
 
-          ... | case2 ¬x=sup =  no-extension ? -- px is not f y' nor sup of former ZChain from y -- no extention
+          ... | case2 ¬x=sup =  no-extension {!!} -- px is not f y' nor sup of former ZChain from y -- no extention
 
      ... | no lim = zc5 where
 
@@ -894,23 +796,23 @@
 
           no-extension : ¬ spu ≡ x → ZChain A f mf ay x
           no-extension ¬sp=x  = record { initial = pinit ; chain∋init = pcy  ; supf = supf1  ; sup=u = {!!} 
-               ; sup = ? ; supf-is-sup = ?
-               ; csupf = ? ; chain⊆A = pchain⊆A ;  f-next = pnext ;  f-total = ptotal ; supf-mono = ? } where
+               ; sup = {!!} ; supf-is-sup = {!!}
+               ; csupf = {!!} ; chain⊆A = pchain⊆A ;  f-next = pnext ;  f-total = ptotal ; supf-mono = {!!} } where
                  supfu : {u : Ordinal } → ( a : u o< x ) → (z : Ordinal) → Ordinal
                  supfu {u} a z = ZChain.supf (pzc (osuc u) (ob<x lim a)) z
                  UnionCF⊆ : {u : Ordinal} → (a : u o< x ) → UnionCF A f mf ay supf1 x ⊆' UnionCF A f mf ay (supfu a) x 
-                 UnionCF⊆ = ?
+                 UnionCF⊆ = {!!}
           zc5 : ZChain A f mf ay x 
           zc5 with ODC.∋-p O A (* x)
-          ... | no noax = no-extension ? -- ¬ A ∋ p, just skip
+          ... | no noax = no-extension {!!} -- ¬ A ∋ p, just skip
           ... | yes ax with ODC.p∨¬p O ( HasPrev A pchain ax f )   
                -- we have to check adding x preserve is-max ZChain A y f mf x
-          ... | case1 pr = no-extension ? 
+          ... | case1 pr = no-extension {!!} 
           ... | case2 ¬fy<x with ODC.p∨¬p O (IsSup A pchain ax )
           ... | case1 is-sup = record { initial = {!!} ; chain∋init = {!!}  ; supf = supf1  ; sup=u = {!!} 
-               ; sup = ? ; supf-is-sup = ?
-               ;  chain⊆A = {!!} ;  f-next = {!!} ;  f-total = {!!} ; csupf = ? ; supf-mono = ? } where -- x is a sup of (zc ?) 
-          ... | case2 ¬x=sup =  no-extension ? -- x is not f y' nor sup of former ZChain from y -- no extention
+               ; sup = {!!} ; supf-is-sup = {!!}
+               ;  chain⊆A = {!!} ;  f-next = {!!} ;  f-total = {!!} ; csupf = {!!} ; supf-mono = {!!} } where -- x is a sup of (zc ?) 
+          ... | case2 ¬x=sup =  no-extension {!!} -- x is not f y' nor sup of former ZChain from y -- no extention
          
      SZ : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) → {y : Ordinal} (ay : odef A y) → ZChain A f mf ay   (& A)
      SZ f mf {y} ay = TransFinite {λ z → ZChain A f mf ay   z  } (λ x → ind f mf ay x   ) (& A)