---

Step * 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)
⊢ (λ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)
BY
{ ((Assert λ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 BY
          (All (Unfold `real-vec`) THEN Auto))
   THEN RWO "-2" 0
   THEN (Try (QuickAuto) THEN Try (Fold `member` 0))
   THEN Try (Complete (((MemCD THEN Try (MemCD))
                        THEN Reduce 0
                        THEN Try (QuickAuto)
                        THEN All (Unfold `real-vec`)
                        THEN Auto)))) }

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
⊢ (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)
\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.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{}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  BY
                (All  (Unfold  `real-vec`)  THEN  Auto))
  THEN  RWO  "-2"  0
  THEN  (Try  (QuickAuto)  THEN  Try  (Fold  `member`  0))
  THEN  Try  (Complete  (((MemCD  THEN  Try  (MemCD))
                                            THEN  Reduce  0
                                            THEN  Try  (QuickAuto)
                                            THEN  All  (Unfold  `real-vec`)
                                            THEN  Auto))))

---

Home Index