---

Step * of Lemma swap_eval_3

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

---

Latex:

---

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


By

---

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

---

Home Index