---

Step * of Lemma sbcode_wf

∀[m,n:ℕ+].  (sbcode(m;n) ∈ ℕ2 List)
BY
{ ((Assert ∀[m,n:ℕ].  (0 < m ⇒ 0 < n ⇒ (sbcode(m;n) ∈ ℕ2 List)) BY
          RepeatFor 2 (CompleteInductionOnNat))
   THEN Auto
   THEN RecUnfold `sbcode` 0
   THEN RepeatFor 2 (AutoSplit)) }

---

Latex:

---

Latex:
\mforall{}[m,n:\mBbbN{}\msupplus{}].    (sbcode(m;n)  \mmember{}  \mBbbN{}2  List)


By

---

Latex:
((Assert  \mforall{}[m,n:\mBbbN{}].    (0  <  m  {}\mRightarrow{}  0  <  n  {}\mRightarrow{}  (sbcode(m;n)  \mmember{}  \mBbbN{}2  List))  BY
                RepeatFor  2  (CompleteInductionOnNat))
  THEN  Auto
  THEN  RecUnfold  `sbcode`  0
  THEN  RepeatFor  2  (AutoSplit))

---

Home Index