---

Step * 1 of Lemma extend_permf_over_comp


1. n : ℕ
2. f : ℕn ⟶ ℕn
3. g : ℕn ⟶ ℕn
⊢ extend_permf(g o f;n) = (extend_permf(g;n) o extend_permf(f;n)) ∈ (ℕn + 1 ⟶ ℕn + 1)
BY
{ ((((Unfolds ``extend_permf compose`` 0 THEN Reduce 0) THEN MemCD) THENM RenameVar `m' (-1)) THENA Auto) }

1
1. n : ℕ
2. f : ℕn ⟶ ℕn
3. g : ℕn ⟶ ℕn
4. m : ℕn + 1
⊢ if (m =z n) then m else g (f m) fi 
= if (if (m =z n) then m else f m fi  =z n)
  then if (m =z n) then m else f m fi 
  else g if (m =z n) then m else f m fi 
  fi 
∈ ℕn + 1

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}
2.  f  :  \mBbbN{}n  {}\mrightarrow{}  \mBbbN{}n
3.  g  :  \mBbbN{}n  {}\mrightarrow{}  \mBbbN{}n
\mvdash{}  extend\_permf(g  o  f;n)  =  (extend\_permf(g;n)  o  extend\_permf(f;n))


By

---

Latex:
((((Unfolds  ``extend\_permf  compose``  0  THEN  Reduce  0)  THEN  MemCD)  THENM  RenameVar  `m'  (-1))
  THENA  Auto
  )

---

Home Index