---

Step * 1 1 of Lemma swap_order_2


1. n : ℕ
2. i : ℕn
3. j : ℕn
4. x : ℕn
⊢ (swap(i;j) (swap(i;j) x)) = x ∈ ℕn
BY
{ (Unfold `swap` 0 THEN Reduce 0) }

1
1. n : ℕ
2. i : ℕn
3. j : ℕn
4. x : ℕn
⊢ if (if (x =z i) then j if (x =z j) then i else x fi  =z i) then j
if (if (x =z i) then j if (x =z j) then i else x fi  =z j) then i
if (x =z i) then j
if (x =z j) then i
else x
fi 
= x
∈ ℕn

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}
2.  i  :  \mBbbN{}n
3.  j  :  \mBbbN{}n
4.  x  :  \mBbbN{}n
\mvdash{}  (swap(i;j)  (swap(i;j)  x))  =  x


By

---

Latex:
(Unfold  `swap`  0  THEN  Reduce  0)

---

Home Index