---

Step * of Lemma app_permf_comp

∀m,n:ℕ. ∀p,p':ℕm ⟶ ℕm. ∀q,q':ℕn ⟶ ℕn.
  ((app_permf(m;n;p;q) o app_permf(m;n;p';q')) = app_permf(m;n;p o p';q o q') ∈ (ℕm + n ⟶ ℕm + n))
BY
{ (((Unfolds ``app_permf compose`` 0 THEN UnivCD) THENM (AbReduce 0 THEN EqCD)) THENA Auto) }

1
.....subterm..... T:t
1:n
1. m : ℕ
2. n : ℕ
3. p : ℕm ⟶ ℕm
4. p' : ℕm ⟶ ℕm
5. q : ℕn ⟶ ℕn
6. q' : ℕn ⟶ ℕn
7. x : ℕm + n
⊢ if if x <z m then p' x else (q' (x - m)) + m fi  <z m
then p if x <z m then p' x else (q' (x - m)) + m fi 
else (q (if x <z m then p' x else (q' (x - m)) + m fi  - m)) + m
fi 
= if x <z m then p (p' x) else (q (q' (x - m))) + m fi 
∈ ℕm + n

---

Latex:

---

Latex:
\mforall{}m,n:\mBbbN{}.  \mforall{}p,p':\mBbbN{}m  {}\mrightarrow{}  \mBbbN{}m.  \mforall{}q,q':\mBbbN{}n  {}\mrightarrow{}  \mBbbN{}n.
    ((app\_permf(m;n;p;q)  o  app\_permf(m;n;p';q'))  =  app\_permf(m;n;p  o  p';q  o  q'))


By

---

Latex:
(((Unfolds  ``app\_permf  compose``  0  THEN  UnivCD)  THENM  (AbReduce  0  THEN  EqCD))  THENA  Auto)

---

Home Index