Step
*
of Lemma
l_sum_functionality_wrt_permutation
∀[L1,L2:ℤ List]. l_sum(L1) = l_sum(L2) ∈ ℤ supposing permutation(ℤ;L1;L2)
BY
{ (Auto
THEN RWO "l_sum_as_reduce<" 0
THEN Auto
THEN BLemma `reduce-permutation`
THEN Auto
THEN (RepUR ``so_apply assoc comm`` 0 THEN Auto)⋅) }
Latex:
Latex:
\mforall{}[L1,L2:\mBbbZ{} List]. l\_sum(L1) = l\_sum(L2) supposing permutation(\mBbbZ{};L1;L2)
By
Latex:
(Auto
THEN RWO "l\_sum\_as\_reduce<" 0
THEN Auto
THEN BLemma `reduce-permutation`
THEN Auto
THEN (RepUR ``so\_apply assoc comm`` 0 THEN Auto)\mcdot{})
Home
Index