---

Step * of Lemma swap_eval_2

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

---

Latex:

---

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


By

---

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

---

Home Index