---

Step * 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))))
⊢ (λj.if j <z i then p j
      if i <z j then p (j - 1)
      else t
      fi ⋅λj.if j <z i then p j
             if i <z j then p (j - 1)
             else t
             fi 
+ λi@0.((λj.if j <z i then p j if i <z j then p (j - 1) else t fi ) (i + i@0))⋅λi@0.((λj.if j <z i then p j
                                                                                         if i <z j then p (j - 1)
                                                                                         else t
                                                                                         fi ) 
                                                                                     (i + i@0)))
= (p⋅p + t^2)
BY
{ (Reduce 0
   THEN (Assert req-vec(i;λj.if j <z i then p j
                             if i <z j then p (j - 1)
                             else t
                             fi ;p) 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)
⊢ (λj.if j <z i then p j
      if i <z j then p (j - 1)
      else t
      fi ⋅λj.if j <z i then p j
             if i <z j then p (j - 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 ⋅λ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))))
\mvdash{}  (\mlambda{}j.if  j  <z  i  then  p  j
            if  i  <z  j  then  p  (j  -  1)
            else  t
            fi  \mcdot{}\mlambda{}j.if  j  <z  i  then  p  j
                          if  i  <z  j  then  p  (j  -  1)
                          else  t
                          fi 
+  \mlambda{}i@0.((\mlambda{}j.if  j  <z  i  then  p  j  if  i  <z  j  then  p  (j  -  1)  else  t  fi  )  (i  +  i@0))\mcdot{}\mlambda{}i@0.((\mlambda{}j.if  j  <z  i
                                                                                                                                                                                      then  p  j
                                                                                                                                                                                  if  i  <z  j
                                                                                                                                                                                      then  p 
                                                                                                                                                                                                (j 
                                                                                                                                                                                                -  1)
                                                                                                                                                                                  else  t
                                                                                                                                                                                  fi  ) 
                                                                                                                                                                          (i  +  i@0)))
=  (p\mcdot{}p  +  t\^{}2)


By

---

Latex:
(Reduce  0
  THEN  (Assert  req-vec(i;\mlambda{}j.if  j  <z  i  then  p  j
                                                      if  i  <z  j  then  p  (j  -  1)
                                                      else  t
                                                      fi  ;p)  BY
                          ((D  0  THENA  Auto)  THEN  Reduce  0  THEN  AutoSplit))
  )

---

Home Index