---

Step * of Lemma tswap_eval_1

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

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

---

Latex:

---

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


By

---

Latex:
Unfold  `tswap`  0

---

Home Index