---

Step * 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 )
⊢ (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 λj.if (j =z 0) then t else p ((i + j) - 1) fi  ∈ ℝ^n - i BY
          (All (RepUR ``real-vec``) THEN Auto))
   THEN (RWO "-2" 0
         THENA (Try (Complete ((RepeatFor 2 (MemCD) THEN Try (QuickAuto) THEN All (Unfold `real-vec`) THEN Auto)))
                THEN Try (QuickAuto)
                )
         )
   ) }

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 )
10. λj.if (j =z 0) then t else p ((i + j) - 1) fi  ∈ ℝ^n - i
⊢ (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)

---

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  )
\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  \mlambda{}j.if  (j  =\msubz{}  0)  then  t  else  p  ((i  +  j)  -  1)  fi    \mmember{}  \mBbbR{}\^{}n  -  i  BY
                (All  (RepUR  ``real-vec``)  THEN  Auto))
  THEN  (RWO  "-2"  0
              THENA  (Try  (Complete  ((RepeatFor  2  (MemCD)
                                                            THEN  Try  (QuickAuto)
                                                            THEN  All  (Unfold  `real-vec`)
                                                            THEN  Auto)))
                            THEN  Try  (QuickAuto)
                            )
              )
  )

---

Home Index