---

Step * 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
⊢ (p⋅p
+ λ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 ⋅λ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 )
= (p⋅p + t^2)
BY
{ (Assert 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 ) BY
         ((D 0 THENA Auto) THEN Reduce 0 THEN AutoSplit)) }

1
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 )
⊢ (p⋅p
+ λ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 ⋅λ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 )
= (p⋅p + t^2)

---

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
\mvdash{}  (p\mcdot{}p
+  \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  \mcdot{}\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  )
=  (p\mcdot{}p  +  t\^{}2)


By

---

Latex:
(Assert  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  )  BY
              ((D  0  THENA  Auto)  THEN  Reduce  0  THEN  AutoSplit))

---

Home Index