---

Step * 1 1 of Lemma extend_permf_over_swap


1. n : ℕ
2. i : ℕn
3. j : ℕn
4. k : ℕn + 1
⊢ (extend_permf(swap(i;j);n) k) = (swap(i;j) k) ∈ ℕn + 1
BY
{ (Unfolds ``extend_permf swap`` 0 THEN AbReduce 0) }

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

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}
2.  i  :  \mBbbN{}n
3.  j  :  \mBbbN{}n
4.  k  :  \mBbbN{}n  +  1
\mvdash{}  (extend\_permf(swap(i;j);n)  k)  =  (swap(i;j)  k)


By

---

Latex:
(Unfolds  ``extend\_permf  swap``  0  THEN  AbReduce  0)

---

Home Index