---

Step * of Lemma tswap_eval_3

∀n:ℕ. ∀i,j,k:ℕn.  ((¬(k = i ∈ ℕn)) ⇒ (¬(k = j ∈ ℕn)) ⇒ ((swap{n}(i;j) k) = k ∈ ℕn))
BY
{ Unfold `tswap` 0 }

1
∀n:ℕ. ∀i,j,k:ℕn.  ((¬(k = i ∈ ℕn)) ⇒ (¬(k = j ∈ ℕn)) ⇒ ((swap(i;j) k) = k ∈ ℕn))

---

Latex:

---

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


By

---

Latex:
Unfold  `tswap`  0

---

Home Index