Step
*
2
of Lemma
rv-nontrivial
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 
BY
{ (RepUR ``real-vec-sep`` 0
   THEN Assert ⌜d(λi.if (i =z 0) then r1 else r0 fi λi.if (i =z 1) then r1 else r0 fi ) = rsqrt(r(2))⌝⋅
   ) }
1
.....assertion..... 
1. n : {2...}
2. λi.r0 ≠ λi.if (i =z 0) then r1 else r0 fi 
⊢ d(λi.if (i =z 0) then r1 else r0 fi λi.if (i =z 1) then r1 else r0 fi ) = rsqrt(r(2))
2
1. n : {2...}
2. λi.r0 ≠ λi.if (i =z 0) then r1 else r0 fi 
3. d(λi.if (i =z 0) then r1 else r0 fi λi.if (i =z 1) then r1 else r0 fi ) = rsqrt(r(2))
⊢ r0 < d(λi.if (i =z 0) then r1 else r0 fi λi.if (i =z 1) then r1 else r0 fi )
Latex:
Latex:
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    \mneq{}  \mlambda{}i.if  (i  =\msubz{}  1)  then  r1  else  r0  fi 
By
Latex:
(RepUR  ``real-vec-sep``  0
  THEN  Assert 
            \mkleeneopen{}d(\mlambda{}i.if  (i  =\msubz{}  0)  then  r1  else  r0  fi  ;\mlambda{}i.if  (i  =\msubz{}  1)  then  r1  else  r0  fi  )  =  rsqrt(r(2))\mkleeneclose{}\mcdot{}
  )
Home
Index