Step
*
1
1
1
1
1
1
2
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
{ ((Assert λi@0.(p (i + i@0)) ∈ ℝ^n - 1 - i BY
(All (RepUR ``real-vec``) THEN Auto))
THEN (Assert p ∈ ℝ^i BY
(All (RepUR ``real-vec``) THEN Auto))
THEN (InstLemma `dot-product-split` [⌜n - 1⌝;⌜i⌝]⋅ THENA Auto)
THEN (RWO "-1" 0 THENA Try (QuickAuto))
THEN (nRAdd ⌜-(p⋅p)⌝ 0⋅ THENA 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
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) ∈ ℤ)
12. λi@0.(p (i + i@0)) ∈ ℝ^n - 1 - i
13. p ∈ ℝ^i
14. ∀[x,y:ℝ^n - 1]. (x⋅y = (x⋅y + λi@0.(x (i + i@0))⋅λi@0.(y (i + i@0))))
⊢ λ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
= (λi@0.(p (i + i@0))⋅λi@0.(p (i + i@0)) + 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 )
10. \mlambda{}j.if (j =\msubz{} 0) then t else p ((i + j) - 1) fi \mmember{} \mBbbR{}\^{}n - i
11. \mneg{}(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:
((Assert \mlambda{}i@0.(p (i + i@0)) \mmember{} \mBbbR{}\^{}n - 1 - i BY
(All (RepUR ``real-vec``) THEN Auto))
THEN (Assert p \mmember{} \mBbbR{}\^{}i BY
(All (RepUR ``real-vec``) THEN Auto))
THEN (InstLemma `dot-product-split` [\mkleeneopen{}n - 1\mkleeneclose{};\mkleeneopen{}i\mkleeneclose{}]\mcdot{} THENA Auto)
THEN (RWO "-1" 0 THENA Try (QuickAuto))
THEN (nRAdd \mkleeneopen{}-(p\mcdot{}p)\mkleeneclose{} 0\mcdot{} THENA Auto))
Home
Index