Step
*
2
1
1
of Lemma
rv-nontrivial
.....assertion.....
1. n : {2...}
2. λi.r0 ≠ λi.if (i =z 0) then r1 else r0 fi
⊢ λi.if (i =z 0) then r1 else r0 fi - λi.if (i =z 1) then r1 else r0 fi ⋅λi.if (i =z 0)
then r1
else r0
fi - λi.if (i =z 1) then r1 else r0 fi
= r(2)
BY
{ RepUR ``dot-product real-vec-sub`` 0 }
1
1. n : {2...}
2. λi.r0 ≠ λi.if (i =z 0) then r1 else r0 fi
⊢ Σ{(if (i =z 0) then r1 else r0 fi - if (i =z 1) then r1 else r0 fi )
* (if (i =z 0) then r1 else r0 fi - if (i =z 1) then r1 else r0 fi ) | 0≤i≤n - 1}
= r(2)
Latex:
Latex:
.....assertion.....
1. n : \{2...\}
2. \mlambda{}i.r0 \mneq{} \mlambda{}i.if (i =\msubz{} 0) then r1 else r0 fi
\mvdash{} \mlambda{}i.if (i =\msubz{} 0) then r1 else r0 fi - \mlambda{}i.if (i =\msubz{} 1) then r1 else r0 fi \mcdot{}\mlambda{}i.if (i =\msubz{} 0)
then r1
else r0
fi - \mlambda{}i.if (i =\msubz{} 1)
then r1
else r0
fi
= r(2)
By
Latex:
RepUR ``dot-product real-vec-sub`` 0
Home
Index