---

Step * 2 1 of Lemma rv-nontrivial

.....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))
BY
{ (RepUR ``real-vec-dist real-vec-norm`` 0
   THEN (Assert ⌜λ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)⌝⋅
        THENM (RWO "-1" 0 THEN Auto)
        )
   ) }

1
.....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)

---

Latex:

---

Latex:
.....assertion..... 
1.  n  :  \{2...\}
2.  \mlambda{}i.r0  \mneq{}  \mlambda{}i.if  (i  =\msubz{}  0)  then  r1  else  r0  fi 
\mvdash{}  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))


By

---

Latex:
(RepUR  ``real-vec-dist  real-vec-norm``  0
  THEN  (Assert 
              \mkleeneopen{}\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  ...
                                                                                                                                                                                        then  r1
                                                                                                                                                                                        else  r0
                                                                                                                                                                                        fi 
                =  r(2)\mkleeneclose{}\mcdot{}
            THENM  (RWO  "-1"  0  THEN  Auto)
            )
  )

---

Home Index