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