---

Step * 1 1 1 1 1 1 1 of Lemma real-ball-slice_wf


1. n : ℕ+
2. t : ℝ
3. i : ℕn
4. p : ℝ^n - 1
5. λj.if j <z i then p j
      if i <z j then p (j - 1)
      else t
      fi  ∈ ℝ^n
6. ∀[x,y:ℝ^n].  (x⋅y = (x⋅y + λi@0.(x (i + i@0))⋅λi@0.(y (i + i@0))))
7. req-vec(i;λj.if j <z i then p j
                if i <z j then p (j - 1)
                else t
                fi ;p)
8. λi@0.if i + i@0 <z i then p (i + i@0)
        if i <z i + i@0 then p ((i + i@0) - 1)
        else t
        fi  ∈ ℝ^n - i
9. req-vec(n - i;λi@0.if i + i@0 <z i then p (i + i@0)
                      if i <z i + i@0 then p ((i + i@0) - 1)
                      else t
                      fi ;λj.if (j =z 0) then t else p ((i + j) - 1) fi )
10. λj.if (j =z 0) then t else p ((i + j) - 1) fi  ∈ ℝ^n - i
11. i = (n - 1) ∈ ℤ
⊢ (p⋅p + λj.if (j =z 0) then t else p ((i + j) - 1) fi ⋅λj.if (j =z 0) then t else p ((i + j) - 1) fi ) = (p⋅p + t^2)
BY
{ (Eliminate ⌜i⌝⋅
   THEN (Subst' n - n - 1 ~ 1 0 THENA Auto)
   THEN BLemma `radd_functionality`
   THEN Auto
   THEN (RepUR ``dot-product`` 0 THEN (RWO  "rsum-single" 0 THENA Auto))
   THEN Reduce 0
   THEN RWO  "rnexp2" 0
   THEN Auto) }

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}\msupplus{}
2.  t  :  \mBbbR{}
3.  i  :  \mBbbN{}n
4.  p  :  \mBbbR{}\^{}n  -  1
5.  \mlambda{}j.if  j  <z  i  then  p  j
            if  i  <z  j  then  p  (j  -  1)
            else  t
            fi    \mmember{}  \mBbbR{}\^{}n
6.  \mforall{}[x,y:\mBbbR{}\^{}n].    (x\mcdot{}y  =  (x\mcdot{}y  +  \mlambda{}i@0.(x  (i  +  i@0))\mcdot{}\mlambda{}i@0.(y  (i  +  i@0))))
7.  req-vec(i;\mlambda{}j.if  j  <z  i  then  p  j
                                if  i  <z  j  then  p  (j  -  1)
                                else  t
                                fi  ;p)
8.  \mlambda{}i@0.if  i  +  i@0  <z  i  then  p  (i  +  i@0)
                if  i  <z  i  +  i@0  then  p  ((i  +  i@0)  -  1)
                else  t
                fi    \mmember{}  \mBbbR{}\^{}n  -  i
9.  req-vec(n  -  i;\mlambda{}i@0.if  i  +  i@0  <z  i  then  p  (i  +  i@0)
                                            if  i  <z  i  +  i@0  then  p  ((i  +  i@0)  -  1)
                                            else  t
                                            fi  ;\mlambda{}j.if  (j  =\msubz{}  0)  then  t  else  p  ((i  +  j)  -  1)  fi  )
10.  \mlambda{}j.if  (j  =\msubz{}  0)  then  t  else  p  ((i  +  j)  -  1)  fi    \mmember{}  \mBbbR{}\^{}n  -  i
11.  i  =  (n  -  1)
\mvdash{}  (p\mcdot{}p
+  \mlambda{}j.if  (j  =\msubz{}  0)  then  t  else  p  ((i  +  j)  -  1)  fi  \mcdot{}\mlambda{}j.if  (j  =\msubz{}  0)  then  t  else  p  ((i  +  j)  -  1)  fi  )
=  (p\mcdot{}p  +  t\^{}2)


By

---

Latex:
(Eliminate  \mkleeneopen{}i\mkleeneclose{}\mcdot{}
  THEN  (Subst'  n  -  n  -  1  \msim{}  1  0  THENA  Auto)
  THEN  BLemma  `radd\_functionality`
  THEN  Auto
  THEN  (RepUR  ``dot-product``  0  THEN  (RWO    "rsum-single"  0  THENA  Auto))
  THEN  Reduce  0
  THEN  RWO    "rnexp2"  0
  THEN  Auto)

---

Home Index