---

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