Step
*
1
of Lemma
exact-reduce-constraints_wf
1. w : ℤ List
2. j : ℕ||w||
3. L : {l:ℤ List| ||l|| = ||w|| ∈ ℤ} List
⊢ evalall(map(λv.-(w[j] * v[j]) * w\j + v\j;L)) ∈ {l:ℤ List| ||l|| = (||w|| - 1) ∈ ℤ} List
BY
{ (GenConcl ⌜map(λv.-(w[j] * v[j]) * w\j + v\j;L) = L' ∈ ({l:ℤ List| ||l|| = (||w|| - 1) ∈ ℤ} List)⌝⋅ THENA Auto) }
1
1. w : ℤ List
2. j : ℕ||w||
3. L : {l:ℤ List| ||l|| = ||w|| ∈ ℤ} List
4. ∀l:ℤ List. (||l|| = ||w|| ∈ ℤ ∈ Type)
5. v : ℤ List
6. ||v|| = ||w|| ∈ ℤ
⊢ -(w[j] * v[j]) * w\j + v\j ∈ {l:ℤ List| ||l|| = (||w|| - 1) ∈ ℤ}
2
1. w : ℤ List
2. j : ℕ||w||
3. L : {l:ℤ List| ||l|| = ||w|| ∈ ℤ} List
4. L' : {l:ℤ List| ||l|| = (||w|| - 1) ∈ ℤ} List
5. map(λv.-(w[j] * v[j]) * w\j + v\j;L) = L' ∈ ({l:ℤ List| ||l|| = (||w|| - 1) ∈ ℤ} List)
⊢ evalall(L') ∈ {l:ℤ List| ||l|| = (||w|| - 1) ∈ ℤ} List
Latex:
Latex:
1. w : \mBbbZ{} List
2. j : \mBbbN{}||w||
3. L : \{l:\mBbbZ{} List| ||l|| = ||w||\} List
\mvdash{} evalall(map(\mlambda{}v.-(w[j] * v[j]) * w\mbackslash{}j + v\mbackslash{}j;L)) \mmember{} \{l:\mBbbZ{} List| ||l|| = (||w|| - 1)\} List
By
Latex:
(GenConcl \mkleeneopen{}map(\mlambda{}v.-(w[j] * v[j]) * w\mbackslash{}j + v\mbackslash{}j;L) = L'\mkleeneclose{}\mcdot{} THENA Auto)
Home
Index