---

Step * of Lemma cantor2baire-aux-pos

∀[a:ℕ ⟶ 𝔹]. ∀[n:ℕ].
  cantor2baire-aux(a;n) ~ if a n then cantor2baire-aux(a;n-1) + 1 else cantor2baire-aux(a;n-1) fi  supposing 0 < n
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 RepeatFor 2 (AutoSplit)) }

---

Latex:

---

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


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  RepeatFor  2  (AutoSplit))

---

Home Index