---

Step * 1 1 1 of Lemma swap_order_2


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
BY
{ AutoSplit }

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}
2.  i  :  \mBbbN{}n
3.  j  :  \mBbbN{}n
4.  x  :  \mBbbN{}n
\mvdash{}  if  (if  (x  =\msubz{}  i)  then  j  if  (x  =\msubz{}  j)  then  i  else  x  fi    =\msubz{}  i)  then  j
if  (if  (x  =\msubz{}  i)  then  j  if  (x  =\msubz{}  j)  then  i  else  x  fi    =\msubz{}  j)  then  i
if  (x  =\msubz{}  i)  then  j
if  (x  =\msubz{}  j)  then  i
else  x
fi 
=  x


By

---

Latex:
AutoSplit

---

Home Index