---

Step * 1 1 of Lemma rv-nontrivial

.....assertion..... 
1. n : {2...}
⊢ d(λi.r0;λi.if (i =z 0) then r1 else r0 fi ) = r1
BY
{ (RepUR ``real-vec-dist real-vec-norm`` 0
   THEN (Assert ⌜λi.r0 - λi.if (i =z 0) then r1 else r0 fi ⋅λi.r0 - λi.if (i =z 0) then r1 else r0 fi  = r1⌝⋅
        THENM (RWO "-1" 0 THEN Auto THEN (InstLemma `rsqrt-of-square` [⌜r1⌝]⋅ THENA Auto) THEN nRNorm (-1) THEN Auto)
        )
   ) }

1
.....assertion..... 
1. n : {2...}
⊢ λi.r0 - λi.if (i =z 0) then r1 else r0 fi ⋅λi.r0 - λi.if (i =z 0) then r1 else r0 fi  = r1

---

Latex:

---

Latex:
.....assertion..... 
1.  n  :  \{2...\}
\mvdash{}  d(\mlambda{}i.r0;\mlambda{}i.if  (i  =\msubz{}  0)  then  r1  else  r0  fi  )  =  r1


By

---

Latex:
(RepUR  ``real-vec-dist  real-vec-norm``  0
  THEN  (Assert  \mkleeneopen{}\mlambda{}i.r0  -  \mlambda{}i.if  (i  =\msubz{}  0)  then  r1  else  r0  fi  \mcdot{}\mlambda{}i.r0  -  \mlambda{}i.if  (i  =\msubz{}  0)  then  r1  else  r0  fi 
                              =  r1\mkleeneclose{}\mcdot{}
            THENM  (RWO  "-1"  0
                          THEN  Auto
                          THEN  (InstLemma  `rsqrt-of-square`  [\mkleeneopen{}r1\mkleeneclose{}]\mcdot{}  THENA  Auto)
                          THEN  nRNorm  (-1)
                          THEN  Auto)
            )
  )

---

Home Index