Step
*
1
2
1
of Lemma
even-int-list_wf
1. n : ℕ
2. u : ℤ
3. ∀L1:ℤ List. (||L1|| < ||[u]||
⇒ (even-int-list(L1) ∈ 𝔹))
⊢ even-int-list([u]) ∈ 𝔹
BY
{ (RepUR ``even-int-list`` 0 THEN Auto) }
Latex:
Latex:
1. n : \mBbbN{}
2. u : \mBbbZ{}
3. \mforall{}L1:\mBbbZ{} List. (||L1|| < ||[u]|| {}\mRightarrow{} (even-int-list(L1) \mmember{} \mBbbB{}))
\mvdash{} even-int-list([u]) \mmember{} \mBbbB{}
By
Latex:
(RepUR ``even-int-list`` 0 THEN Auto)
Home
Index