---

Step * of Lemma cantor2baire-aux+1

∀[a:ℕ ⟶ 𝔹]. ∀[n:ℕ].
  (cantor2baire-aux(a;n + 1) ~ if a (n + 1) then cantor2baire-aux(a;n) + 1 else cantor2baire-aux(a;n) fi )
BY
{ ((UnivCD THENA Auto)
   THEN UnfoldAtAddr [1] 0
   THEN (RWO "primrec-unroll" 0 THENA Auto)
   THEN Reduce 0
   THEN (Subst ⌜(n + 1) - 1 ~ n⌝ 0⋅ THENA Auto)
   THEN Fold `cantor2baire-aux` 0
   THEN AutoSplit) }

---

Latex:

---

Latex:
\mforall{}[a:\mBbbN{}  {}\mrightarrow{}  \mBbbB{}].  \mforall{}[n:\mBbbN{}].
    (cantor2baire-aux(a;n  +  1)  \msim{}  if  a  (n  +  1)
    then  cantor2baire-aux(a;n)  +  1
    else  cantor2baire-aux(a;n)
    fi  )


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  UnfoldAtAddr  [1]  0
  THEN  (RWO  "primrec-unroll"  0  THENA  Auto)
  THEN  Reduce  0
  THEN  (Subst  \mkleeneopen{}(n  +  1)  -  1  \msim{}  n\mkleeneclose{}  0\mcdot{}  THENA  Auto)
  THEN  Fold  `cantor2baire-aux`  0
  THEN  AutoSplit)

---

Home Index