---

Step * of Lemma swap_eval_1

∀i,j,k:ℤ.  ((k = i ∈ ℤ) ⇒ ((swap(i;j) k) = j ∈ ℤ))
BY
{ (Auto THEN AbEval ``swap`` 0 THEN AutoSplit) }

---

Latex:

---

Latex:
\mforall{}i,j,k:\mBbbZ{}.    ((k  =  i)  {}\mRightarrow{}  ((swap(i;j)  k)  =  j))


By

---

Latex:
(Auto  THEN  AbEval  ``swap``  0  THEN  AutoSplit)

---

Home Index