Interpretations.CnfToBrw

----------------------------------------------------------------------------------------------------
-- An order-preserving embedding from Cantor Normal Forms to Brouwer trees
----------------------------------------------------------------------------------------------------

{-# OPTIONS --cubical #-}

module Interpretations.CnfToBrw where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Function
open import Cubical.Data.Sigma
open import Cubical.Data.Sum
open import Cubical.Data.Empty as ⊥
open import Cubical.Data.Nat
  using (ℕ ; zero ; suc ; +-comm)
open import Cubical.Relation.Nullary

open import CantorNormalForm.Everything as C hiding (succ ; _^_)
open import BrouwerTree.Everything as B

{- The interpretation -}

CtoB : Cnf → Brw
CtoB  𝟎               = zero
CtoB (ω^ a + b [ _ ]) = B.ω^ (CtoB a) B.+ CtoB b


{- The interpretation of any CNF is below ε₀ -}

CNF<ε₀ : (a : Cnf) → CtoB a B.< ε₀
CNF<ε₀ a = subst (λ z → CtoB a B.< z) (sym ε₀≡ω^ε₀) (CNF<ω^ε₀ a) where
  CNF<ω^ε₀ : (a : Cnf) → CtoB a B.< ω^ ε₀
  CNF<ω^ε₀ 𝟎 = zero<lim
  CNF<ω^ε₀ (ω^ a + b [ r ]) =
    additive-principal-ω^-closure ε₀
                                  (ω^-mono-< (subst (λ z → CtoB a B.< z) (sym ε₀≡ω^ε₀) (CNF<ω^ε₀ a)))
                                  (CNF<ω^ε₀ b)


{- CtoB is monotone wrt both < and ≤ -}

CtoB-<-monotone : {a b : Cnf} → a C.< b → CtoB a B.< CtoB b
CtoB-<-monotone  {𝟎}              {ω^ b + d [ s ]}  <₁
  = B.≤-trans (B.zero<ω^c (CtoB b)) (B.x+-mono (B.≤-zero {CtoB d}))
CtoB-<-monotone {ω^ a + c [ r ]} {ω^ b + d [ s ]} (<₂ a<b)
  = B.<∘≤-in-< (lemma (ω^ a + c [ r ]) a<b) (B.x+-mono (B.≤-zero {CtoB d}))
 where
  lemma : ∀ a {b} → left a C.< b → CtoB a B.< B.ω^ (CtoB b)
  lemma  𝟎               {b} _   = B.zero<ω^c (CtoB b)
  lemma (ω^ a + c [ r ]) {b} a<b =
    additive-principal-ω^-closure (CtoB b) (B.ω^-mono-< (CtoB-<-monotone a<b))
                                           (lemma c (C.≤∘<-in-< r a<b))
CtoB-<-monotone {ω^ a + c [ r ]} {ω^ b + d [ s ]} (<₃ a≡b c<d)
  = B.<∘≤-in-< (B.x+-mono-< (CtoB-<-monotone c<d))
               (≤-refl-≡ (cong (λ z → ω^ (CtoB z) B.+ CtoB d) a≡b))

CtoB-≤-monotone : {a b : Cnf} → a C.≤ b → CtoB a B.≤ CtoB b
CtoB-≤-monotone (inl a<b) = B.<-in-≤ (CtoB-<-monotone a<b)
CtoB-≤-monotone (inr b≡a) = ≤-refl-≡ (cong CtoB (sym b≡a))

CtoB-preserves-increasing : ∀ {f} → C.is-<-increasing f → increasing (CtoB ∘ f)
CtoB-preserves-increasing f↑ = CtoB-<-monotone ∘ f↑


{- CtoB reflects both < and ≤ -}

CtoB-reflects-< : {a b : Cnf} → CtoB a B.< CtoB b → a C.< b
CtoB-reflects-< {a} {b} Ba<Bb with <-tri a b
... | inl a<b = a<b
... | inr (inl b<a) = ⊥.rec (B.<-irreflexive (CtoB a) (B.<-trans _ _ _ Ba<Bb (CtoB-<-monotone b<a)))
... | inr (inr a≡b) = ⊥.rec (B.<-irreflexive (CtoB b) (subst (λ z → CtoB z B.< CtoB b) a≡b Ba<Bb))

CtoB-reflects-≤ : {a b : Cnf} → CtoB a B.≤ CtoB b → a C.≤ b
CtoB-reflects-≤ {a} {b} a≤b with <-tri a b
... | inl a<b = inl a<b
... | inr (inl b<a) = ⊥.rec (B.<-irreflexive _ (B.<∘≤-in-< (CtoB-<-monotone b<a) a≤b))
... | inr (inr a≡b) = inr (sym a≡b)


{- CtoB is injective -}

CtoB-injective : {a b : Cnf} → CtoB a ≡ CtoB b → a ≡ b
CtoB-injective p = C.≤-antisym (CtoB-reflects-≤ (B.≤-refl-≡ p))
                               (CtoB-reflects-≤ (B.≤-refl-≡ (sym p)))


{- CtoB preserves arithmetic operations -}

CtoB-preserves-suc : (a : Cnf) → CtoB (a C.+ 𝟏) ≡ B.succ (CtoB a)
CtoB-preserves-suc 𝟎 = refl
CtoB-preserves-suc (ω^ a + b [ r ]) with <-tri a 𝟎
... | inr _ =
   ω^ (CtoB a) B.+ CtoB (b C.+ 𝟏)
  ≡⟨ cong (ω^ (CtoB a) B.+_) (CtoB-preserves-suc b) ⟩
   ω^ (CtoB a) B.+ B.succ (CtoB b)
  ≡⟨ refl ⟩
   B.succ (ω^ (CtoB a) B.+ CtoB b) ∎

CtoB-preserves-add : (a b : Cnf) → CtoB (a C.+ b) ≡ CtoB a B.+ CtoB b
CtoB-preserves-add  𝟎                𝟎               = refl
CtoB-preserves-add  𝟎               (ω^ b + d [ s ]) = sym (zero+y≡y _)
CtoB-preserves-add (ω^ a + c [ r ])  𝟎               = refl
CtoB-preserves-add (ω^ a + c [ r ]) (ω^ b + d [ s ]) with <-tri a b
... | inl a<b =
   ω^ (CtoB b) B.+ CtoB d
  ≡⟨ cong (B._+ CtoB d) (sym ω^a+ω^b≡ω^b) ⟩
   (ω^ (CtoB a) B.+ ω^ (CtoB b)) B.+ CtoB d
  ≡⟨ sym (+-assoc (CtoB d)) ⟩
   ω^ (CtoB a) B.+ ω^ (CtoB b) B.+ CtoB d
  ≡⟨ cong (λ z → _ B.+ z B.+ CtoB d) (sym c+ω^b≡ω^b) ⟩
   ω^ (CtoB a) B.+ (CtoB c B.+ ω^ (CtoB b)) B.+ CtoB d
  ≡⟨ cong (ω^ (CtoB a) B.+_) (sym (+-assoc (CtoB d))) ⟩
   ω^ (CtoB a) B.+ CtoB c B.+ ω^ (CtoB b) B.+ CtoB d
  ≡⟨ +-assoc (ω^ (CtoB b) B.+ CtoB d) ⟩
   (ω^ (CtoB a) B.+ CtoB c) B.+ ω^ (CtoB b) B.+ CtoB d ∎
 where
  ω^a<ω^b : ω^ (CtoB a) B.< ω^ (CtoB b)
  ω^a<ω^b = CtoB-<-monotone {ω^⟨ a ⟩} {ω^⟨ b ⟩} (<₂ a<b)
  ω^a+ω^b≡ω^b : ω^ (CtoB a) B.+ ω^ (CtoB b) ≡ ω^ (CtoB b)
  ω^a+ω^b≡ω^b = additive-principal-ω^ (CtoB b) _ ω^a<ω^b
  c<ω^b : CtoB c B.< ω^ (CtoB b)
  c<ω^b = CtoB-<-monotone {c} {ω^⟨ b ⟩} (<₂'' (C.≤∘<-in-< r a<b))
  c+ω^b≡ω^b : CtoB c B.+ ω^ (CtoB b) ≡ ω^ (CtoB b)
  c+ω^b≡ω^b = additive-principal-ω^ (CtoB b) _ c<ω^b
... | inr a≥b =
   ω^ (CtoB a) B.+ CtoB (c C.+ ω^ b + d [ s ])
  ≡⟨ cong (ω^ (CtoB a) B.+_) (CtoB-preserves-add c (ω^ b + d [ s ])) ⟩
   ω^ (CtoB a) B.+ CtoB c B.+ ω^ (CtoB b) B.+ CtoB d
  ≡⟨ +-assoc (ω^ (CtoB b) B.+ CtoB d) ⟩
   (ω^ (CtoB a) B.+ CtoB c) B.+ ω^ (CtoB b) B.+ CtoB d ∎

private
 NviaCtoB : ℕ → Brw
 NviaCtoB n = CtoB (NtoC n)

 NviaCtoB≡ι : (n : ℕ) → NviaCtoB n ≡ ι n
 NviaCtoB≡ι zero = refl
 NviaCtoB≡ι (suc n) = cong (one B.+_) (NviaCtoB≡ι n) ∙ sym (ι-+-commutes 1 n) ∙ cong ι (+-comm n 1)

CtoB-preserves-mul-nat : (a : Cnf) (n : ℕ) → CtoB (a • n) ≡ CtoB a B.· NviaCtoB n
CtoB-preserves-mul-nat 𝟎 0 = refl
CtoB-preserves-mul-nat 𝟎 (suc n) = sym (zero·y≡zero (NviaCtoB (suc n)))
CtoB-preserves-mul-nat (ω^ _ + _ [ _ ]) 0 = refl
CtoB-preserves-mul-nat a@(ω^ _ + _ [ _ ]) (suc n) =
   CtoB (a • suc n)
  ≡⟨ cong CtoB (•suc-spec' a n) ⟩
   CtoB (a C.+ a • n)
  ≡⟨ CtoB-preserves-add a (a • n) ⟩
   CtoB a B.+ CtoB (a • n)
  ≡⟨ cong (CtoB a B.+_) (CtoB-preserves-mul-nat a n) ⟩
   CtoB a B.+ CtoB a B.· NviaCtoB n
  ≡⟨ cong (B._+ CtoB a B.· NviaCtoB n) (sym (zero+y≡y (CtoB a))) ⟩
   (zero B.+ CtoB a) B.+ CtoB a B.· NviaCtoB n
  ≡⟨ ·-+-distributivity (NviaCtoB n) ⟩
   CtoB a B.· (succ zero B.+ NviaCtoB n) ∎

CtoB-preserves-mul-ι : (a : Cnf) (n : ℕ) → CtoB (a • n) ≡ CtoB a B.· ι n
CtoB-preserves-mul-ι a n = subst (λ x → CtoB (a • n) ≡ CtoB a B.· x) (NviaCtoB≡ι n) (CtoB-preserves-mul-nat a n)

CtoB-preserves-mul : (a b : Cnf) → CtoB (a C.· b) ≡ CtoB a B.· CtoB b
CtoB-preserves-mul  𝟎                𝟎               = refl
CtoB-preserves-mul  𝟎               (ω^ b + d [ s ]) = sym (zero·y≡zero (CtoB (ω^ b + d [ s ])))
CtoB-preserves-mul (ω^ a + c [ r ])  𝟎               = refl
CtoB-preserves-mul x@(ω^ a + c [ r ]) (ω^ 𝟎 + d [ s ]) =
   CtoB (x C.+ x C.· d)
  ≡⟨ CtoB-preserves-add x (x C.· d) ⟩
   CtoB x B.+ CtoB (x C.· d)
  ≡⟨ cong (_ B.+_) (CtoB-preserves-mul _ d) ⟩
   CtoB x B.+ CtoB x B.· CtoB d
  ≡⟨ cong (B._+ CtoB x B.· CtoB d) (sym (zero+y≡y _)) ⟩
   CtoB x B.· ω^ zero B.+ CtoB x B.· CtoB d
  ≡⟨ ·-+-distributivity (CtoB d) ⟩
   CtoB x B.· (ω^ zero B.+ CtoB d) ∎
CtoB-preserves-mul (ω^ a + c [ r ]) (ω^ b@(ω^ b' + b'' [ _ ]) + d [ s ]) =
   (ω^ (CtoB (a C.+ b))) B.+ CtoB ((ω^ a + c [ r ]) C.· d)
  ≡⟨ cong (λ z → (ω^ z) B.+ CtoB ((ω^ a + c [ r ]) C.· d)) (CtoB-preserves-add a b) ⟩
   (ω^ (CtoB a B.+ CtoB b)) B.+ CtoB ((ω^ a + c [ r ]) C.· d)
  ≡⟨ cong ((ω^ (CtoB a B.+ CtoB b)) B.+_) (CtoB-preserves-mul _ d) ⟩
   (ω^ (CtoB a B.+ CtoB b)) B.+ (ω^ (CtoB a) B.+ CtoB c) B.· CtoB d
  ≡⟨ cong (B._+ (ω^ (CtoB a) B.+ CtoB c) B.· CtoB d) goal ⟩
   (ω^ (CtoB a) B.+ CtoB c) B.· ω^ (CtoB b) B.+ (ω^ (CtoB a) B.+ CtoB c) B.· CtoB d
  ≡⟨ ·-+-distributivity (CtoB d) ⟩
   (ω^ (CtoB a) B.+ CtoB c) B.· (ω^ (CtoB b) B.+ CtoB d) ∎
 where
  fact : Σ[ n ∈ ℕ ] (ω^ a + c [ r ] C.< ω^⟨ a ⟩ • suc n)
  fact = Σn<•sn (ω^ a + c [ r ]) (inr refl)
  n : ℕ
  n = suc (fst fact)
  t : ω^ a + c [ r ] C.< ω^⟨ a ⟩ • n
  t = snd fact
  claim₀ : ω^ (CtoB a) B.+ CtoB c B.< CtoB (ω^⟨ a ⟩ • n)
  claim₀ = CtoB-<-monotone t
  claim₁ : CtoB (ω^⟨ a ⟩ • n) ≡ CtoB (ω^⟨ a ⟩) B.· NviaCtoB n
  claim₁ = CtoB-preserves-mul-nat ω^⟨ a ⟩ n
  claim₂ : ω^ (CtoB a) B.+ CtoB c B.< CtoB (ω^⟨ a ⟩) B.· NviaCtoB n
  claim₂ = subst (ω^ (CtoB a) B.+ CtoB c B.<_) claim₁ claim₀
  claim₃ : (ω^ (CtoB a) B.+ CtoB c) B.· ω^ (CtoB b) B.≤
           (CtoB (ω^⟨ a ⟩) B.· NviaCtoB n) B.· ω^ (CtoB b)
  claim₃ = ·x-mono (ω^ (CtoB b)) (B.<-in-≤ claim₂)
  claim₄ : NviaCtoB n B.· ω^ (CtoB b) ≡ ω^ (CtoB b)
  claim₄ = cong (B._· ω^ (CtoB b)) (NviaCtoB≡ι n) ∙
           ω^x-absorbs-finite {x = CtoB b} (B.<∘≤-in-< (zero<ω^c (CtoB b'))
                                                       (x+-mono {ω^ (CtoB b')} (≤-zero {CtoB b''})))
  claim₅ : (CtoB (ω^⟨ a ⟩) B.· NviaCtoB n) B.· ω^ (CtoB b) ≡ ω^ (CtoB a B.+ CtoB b)
  claim₅ =
     (ω^ (CtoB a) B.· NviaCtoB n) B.· ω^ (CtoB b)
    ≡⟨ sym (·-assoc (ω^ (CtoB b))) ⟩
     ω^ (CtoB a) B.· (NviaCtoB n B.· ω^ (CtoB b))
    ≡⟨ cong (CtoB (ω^⟨ a ⟩) B.·_) claim₄ ⟩
     ω^ (CtoB a) B.· ω^ (CtoB b)
    ≡⟨ sym (exp-homomorphism {B.ω} {CtoB a} {CtoB b}) ⟩
     ω^ (CtoB a B.+ CtoB b) ∎
  claim₆ : (ω^ (CtoB a) B.+ CtoB c) B.· ω^ (CtoB b) B.≤ ω^ (CtoB a B.+ CtoB b)
  claim₆ = subst ((ω^ (CtoB a) B.+ CtoB c) B.· ω^ (CtoB b) B.≤_) claim₅ claim₃
  claim₇ : ω^ (CtoB a B.+ CtoB b) ≡ ω^ (CtoB a) B.· ω^ (CtoB b)
  claim₇ = exp-homomorphism {B.ω} {CtoB a} {CtoB b}
  claim₈ : ω^ (CtoB a) B.· ω^ (CtoB b) B.≤ (ω^ (CtoB a) B.+ CtoB c) B.· ω^ (CtoB b)
  claim₈ = ·x-mono (ω^ (CtoB b)) (CtoB-≤-monotone {ω^⟨ a ⟩} {ω^ a + c [ r ]} (≤₃ refl 𝟎≤))
  claim₉ : ω^ (CtoB a B.+ CtoB b) B.≤ (ω^ (CtoB a) B.+ CtoB c) B.· ω^ (CtoB b)
  claim₉ = subst (B._≤ (ω^ (CtoB a) B.+ CtoB c) B.· ω^ (CtoB b)) (sym claim₇) claim₈
  goal : ω^ (CtoB a B.+ CtoB b) ≡ (ω^ (CtoB a) B.+ CtoB c) B.· ω^ (CtoB b)
  goal = B.≤-antisym claim₉ claim₆

CtoB-preserves-exp-with-base-ω : (a : Cnf) → CtoB (ω^⟨ a ⟩) ≡ ω^ (CtoB a)
CtoB-preserves-exp-with-base-ω a = refl


{- CtoB preserves fundamental sequences -}

private
 P : Cnf → Type
 P x = x C.> 𝟎 → ¬ (C.is-strong-suc x)
     → Σ[ s ∈ (ℕ → Cnf) ] Σ[ s↑ ∈ C.is-<-increasing s ]
        ((x C.is-lim-of (s , s↑)) × (CtoB x ≡ limit (CtoB ∘ s) {CtoB-preserves-increasing s↑}))
CtoB-preserves-FS-step : ∀ a → (∀ b → b C.< a → P b) → P a
CtoB-preserves-FS-step (ω^ 𝟎 + b [ _ ]) H _ not-suc = ⊥.rec (not-suc (ω^𝟎+-is-strong-suc b _))
CtoB-preserves-FS-step x@(ω^ a@(ω^ _ + _ [ _ ]) + 𝟎 [ _ ]) H _ not-suc with is-strong-suc-dec a
CtoB-preserves-FS-step x@(ω^ a@(ω^ _ + _ [ _ ]) + 𝟎 [ _ ]) H _ not-suc | inl (y , (y<a , p) , q) =
  s , s↑ , (s≤x , x-min) , CtoB⟨x⟩≡lim⟨CtoB∘s⟩
 where -- ω^a = ω^{y+1} = ω^y·ω = lim(λi.ω^y·i)
  s : ℕ → Cnf
  s i = ω^⟨ y ⟩ • i
  s↑ : C.is-<-increasing s
  s↑ = ω^•-is-<-increasing ω^⟨ y ⟩ <₁
  s≤x : ∀ i → s i C.≤ x
  s≤x i = inl (<₂' (C.≤∘<-in-< (left•≤ ω^⟨ y ⟩ i) y<a))
  x-min : ∀ z → (∀ i → s i C.≤ z) → x C.≤ z
  x-min 𝟎 h = ⊥.rec (ω^≰𝟎 (h 1))
  x-min (ω^ u + v [ _ ]) h with <-tri a u
  ... | inl a<u = inl (<₂ a<u)
  ... | inr (inl a>u) = ⊥.rec (≤→≯ claim₂ claim₁)
   where
    claim₀ : Σ[ n ∈ ℕ ] (ω^ u + v [ _ ] C.< ω^⟨ y ⟩ • suc n)
    claim₀ = Σn<•sn _ (q u a>u)
    n : ℕ
    n = suc (fst claim₀)
    claim₁ : ω^ u + v [ _ ] C.< ω^⟨ y ⟩ • n
    claim₁ = snd claim₀
    claim₂ : ω^⟨ y ⟩ • n C.≤ ω^ u + v [ _ ]
    claim₂ = h n
  ... | inr (inr x≡u) = ≤₃ x≡u 𝟎≤
  CtoB⟨x⟩≡lim⟨CtoB∘s⟩ : CtoB x ≡ limit (CtoB ∘ s) {CtoB-preserves-increasing s↑}
  CtoB⟨x⟩≡lim⟨CtoB∘s⟩ =
         CtoB x
       ≡⟨ refl ⟩
         B.ω ^ CtoB a
       ≡⟨ cong (λ z → B.ω ^ CtoB z) (sym (suc→+𝟏 (y<a , p))) ⟩
         B.ω ^ CtoB (y C.+ 𝟏)
       ≡⟨ cong (B.ω ^_) (CtoB-preserves-add y 𝟏) ⟩
         B.ω ^ (CtoB y B.+ CtoB 𝟏)
       ≡⟨ refl ⟩
         B.ω ^ CtoB y B.· limit ι
       ≡⟨ not-zero-·-limit _ _ _ (zero≢a^ (CtoB y) (zero≠lim ∘ sym) ∘ sym) ⟩
         limit (λ n → B.ω ^ CtoB y B.· ι n)
       ≡⟨ limit-pointwise-equal _ _ (sym ∘ (CtoB-preserves-mul-ι _)) ⟩
         limit (CtoB ∘ s) ∎
CtoB-preserves-FS-step x@(ω^ a@(ω^ _ + _ [ _ ]) + 𝟎 [ _ ]) H _ not-suc | inr a-is-not-suc =
  s , s↑ , (s≤x , x-min) , CtoB⟨x⟩≡lim⟨CtoB∘s⟩
 where -- ω^a = ω^(lim(r)) = lim(λi.ω^(ri))
  IH : Σ[ r ∈ (ℕ → Cnf) ] Σ[ r↑ ∈ C.is-<-increasing r ]
        ((a C.is-lim-of (r , r↑)) × (CtoB a ≡ limit (CtoB ∘ r) {CtoB-preserves-increasing r↑}))
  IH = H a left< <₁ a-is-not-suc
  r : ℕ → Cnf
  r = fst IH
  r↑ : C.is-<-increasing r
  r↑ = fst (snd IH)
  alimr : a C.is-lim-of (r , r↑)
  alimr = fst (snd (snd IH))
  CtoB⟨a⟩≡lim⟨CtoB∘r⟩ : CtoB a ≡ limit (CtoB ∘ r) {CtoB-preserves-increasing r↑}
  CtoB⟨a⟩≡lim⟨CtoB∘r⟩ = snd (snd (snd IH))
  s : ℕ → Cnf
  s i = ω^⟨ r i ⟩
  s↑ : C.is-<-increasing s
  s↑ i = <₂ (r↑ i)
  s≤x : ∀ i → s i C.≤ x
  s≤x i = ≤₂ (fst alimr i)
  x-min : ∀ z → (∀ i → s i C.≤ z) → x C.≤ z
  x-min 𝟎 h = ⊥.rec (ω^≰𝟎 (h 0))
  x-min (ω^ u + v [ _ ]) h = C.≤-trans claim₀ claim₁
   where
    r≤u : ∀ i → r i C.≤ u
    r≤u i = left-is-≤-monotone (h i)
    a≤u : a C.≤ u
    a≤u = snd alimr u r≤u
    claim₀ : ω^ a + 𝟎 [ _ ] C.≤ ω^ u + 𝟎 [ 𝟎≤ ]
    claim₀ = ≤₂ a≤u
    claim₁ : ω^ u + 𝟎 [ _ ] C.≤ ω^ u + v [ _ ]
    claim₁ = ≤₃ refl 𝟎≤
  CtoB⟨x⟩≡lim⟨CtoB∘s⟩ : CtoB x ≡ limit (CtoB ∘ s) {CtoB-preserves-increasing s↑}
  CtoB⟨x⟩≡lim⟨CtoB∘s⟩ =
         CtoB x
       ≡⟨ refl ⟩
         B.ω ^ CtoB a
       ≡⟨ cong (B.ω ^_) CtoB⟨a⟩≡lim⟨CtoB∘r⟩ ⟩
         B.ω ^ limit (CtoB ∘ r) {CtoB-preserves-increasing r↑}
       ≡⟨ ω^⟨limf⟩≡lim⟨ω^⟨fn⟩⟩ (CtoB ∘ r) (CtoB-preserves-increasing r↑) ⟩
         limit (CtoB ∘ s)  -- having different monotonicity proofs
       ≡⟨ limit-pointwise-equal _ _ (λ _ → refl) ⟩
         limit (CtoB ∘ s) ∎
CtoB-preserves-FS-step x@(ω^ a@(ω^ _ + _ [ _ ]) + b@(ω^ _ + _ [ _ ]) [ _ ]) H _ not-suc with is-strong-suc-dec b
CtoB-preserves-FS-step x@(ω^ a@(ω^ _ + _ [ _ ]) + b@(ω^ _ + _ [ _ ]) [ _ ]) H _ not-suc | inl b-is-suc = ⊥.rec (not-suc (right-is-strong-suc₀ b-is-suc))
CtoB-preserves-FS-step x@(ω^ a@(ω^ _ + _ [ _ ]) + b@(ω^ _ + _ [ _ ]) [ w ]) H _ not-suc | inr b-is-not-suc =
  s , s↑ , (s≤x , x-min) , CtoB⟨x⟩≡lim⟨CtoB∘s⟩
 where -- ω^a+b = ω^a+lim(r) = lim(λi.ω^a+ri)
  IH : Σ[ r ∈ (ℕ → Cnf) ] Σ[ r↑ ∈ C.is-<-increasing r ]
        ((b C.is-lim-of (r , r↑)) × (CtoB b ≡ limit (CtoB ∘ r) {CtoB-preserves-increasing r↑}))
  IH = H b (right< _ _ _) <₁ b-is-not-suc
  r : ℕ → Cnf
  r = fst IH
  r↑ : C.is-<-increasing r
  r↑ = fst (snd IH)
  blimr : b C.is-lim-of (r , r↑)
  blimr = fst (snd (snd IH))
  CtoB⟨b⟩≡lim⟨CtoB∘r⟩ : CtoB b ≡ limit (CtoB ∘ r) {CtoB-preserves-increasing r↑}
  CtoB⟨b⟩≡lim⟨CtoB∘r⟩ = snd (snd (snd IH))
  a≥lr : ∀ i → a ≥ left (r i)
  a≥lr i = C.≤-trans (left-is-≤-monotone (fst blimr i)) w
  s : ℕ → Cnf
  s i = ω^ a + r i [ a≥lr i ]
  s↑ : C.is-<-increasing s
  s↑ i = <₃ refl (r↑ i)
  s≤x : ∀ i → s i C.≤ x
  s≤x i = ≤₃ refl (fst blimr i)
  x-min : ∀ z → (∀ i → s i C.≤ z) → x C.≤ z
  x-min 𝟎 h = ⊥.rec (ω^≰𝟎 (h 0))
  x-min (ω^ u + v [ _ ]) h with <-tri a u
  ... | inl a<u = inl (<₂ a<u)
  ... | inr (inl a>u) = ⊥.rec (≤→≯ (h 0) (<₂ a>u))
  ... | inr (inr a≡u) = ≤₃ a≡u (snd blimr v (λ i → ≤₃⁻¹ a≡u (h i)))
  CtoB⟨x⟩≡lim⟨CtoB∘s⟩ : CtoB x ≡ limit (CtoB ∘ s) {CtoB-preserves-increasing s↑}
  CtoB⟨x⟩≡lim⟨CtoB∘s⟩ =
         CtoB x
       ≡⟨ refl ⟩
         B.ω ^ CtoB a B.+ CtoB b
       ≡⟨ cong (B.ω ^ CtoB a B.+_) CtoB⟨b⟩≡lim⟨CtoB∘r⟩ ⟩
         B.ω ^ CtoB a B.+ limit (CtoB ∘ r) {CtoB-preserves-increasing r↑}
       ≡⟨ refl ⟩
         limit (λ i → B.ω ^ CtoB a B.+ CtoB (r i))
       ≡⟨ refl ⟩
         limit (CtoB ∘ s) -- having different monotonicity proofs
       ≡⟨ limit-pointwise-equal _ _ (λ _ → refl) ⟩
         limit (CtoB ∘ s) ∎

CtoB-preserves-FS : ∀ x → x C.> 𝟎 → ¬ (C.is-strong-suc x)
  → Σ[ s ∈ (ℕ → Cnf) ] Σ[ s↑ ∈ C.is-<-increasing s ]
     ((x C.is-lim-of (s , s↑)) × (CtoB x ≡ limit (CtoB ∘ s) {CtoB-preserves-increasing s↑}))
CtoB-preserves-FS = C.wf-ind CtoB-preserves-FS-step

fund-sequence : (x : Cnf) → C.is-lim x → (ℕ → Cnf)
fund-sequence x p = fst (CtoB-preserves-FS x (lim>𝟎 p) (lim-is-not-suc p))

fund-sequence↑ : (x : Cnf) → (p : C.is-lim x) → C.is-<-increasing (fund-sequence x p)
fund-sequence↑ x p = fst (snd (CtoB-preserves-FS x (lim>𝟎 p) (lim-is-not-suc p)))
CtoB-preserves-fund-sequence : (x : Cnf) → (p : C.is-lim x)
                             → CtoB x ≡ limit (CtoB ∘ fund-sequence x p) {CtoB-preserves-increasing (fund-sequence↑ x p)}
CtoB-preserves-fund-sequence x p = snd (snd (snd (CtoB-preserves-FS x (lim>𝟎 p) (lim-is-not-suc p))))