---

Step * of Lemma tswap_eval_2

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

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

---

Latex:

---

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


By

---

Latex:
Unfold  `tswap`  0

---

Home Index