---

Step * 1 2 of Lemma app_permf_comp


1. m : ℕ
2. n : ℕ
3. p : ℕm ⟶ ℕm
4. p' : ℕm ⟶ ℕm
5. q : ℕn ⟶ ℕn
6. q' : ℕn ⟶ ℕn
7. x : ℕm + n
8. m ≤ x
⊢ if (q' (x - m)) + m <z m then p ((q' (x - m)) + m) else (q (((q' (x - m)) + m) - m)) + m fi 
= ((q (q' (x - m))) + m)
∈ ℕm + n
BY
{ (SplitOnConclITE THENA Auto') }

1
.....truecase..... 
1. m : ℕ
2. n : ℕ
3. p : ℕm ⟶ ℕm
4. p' : ℕm ⟶ ℕm
5. q : ℕn ⟶ ℕn
6. q' : ℕn ⟶ ℕn
7. x : ℕm + n
8. m ≤ x
9. (q' (x - m)) + m < m
⊢ (p ((q' (x - m)) + m)) = ((q (q' (x - m))) + m) ∈ ℕm + n

2
.....falsecase..... 
1. m : ℕ
2. n : ℕ
3. p : ℕm ⟶ ℕm
4. p' : ℕm ⟶ ℕm
5. q : ℕn ⟶ ℕn
6. q' : ℕn ⟶ ℕn
7. x : ℕm + n
8. m ≤ x
9. m ≤ ((q' (x - m)) + m)
⊢ ((q (((q' (x - m)) + m) - m)) + m) = ((q (q' (x - m))) + m) ∈ ℕm + n

---

Latex:

---

Latex:

1.  m  :  \mBbbN{}
2.  n  :  \mBbbN{}
3.  p  :  \mBbbN{}m  {}\mrightarrow{}  \mBbbN{}m
4.  p'  :  \mBbbN{}m  {}\mrightarrow{}  \mBbbN{}m
5.  q  :  \mBbbN{}n  {}\mrightarrow{}  \mBbbN{}n
6.  q'  :  \mBbbN{}n  {}\mrightarrow{}  \mBbbN{}n
7.  x  :  \mBbbN{}m  +  n
8.  m  \mleq{}  x
\mvdash{}  if  (q'  (x  -  m))  +  m  <z  m  then  p  ((q'  (x  -  m))  +  m)  else  (q  (((q'  (x  -  m))  +  m)  -  m))  +  m  fi 
=  ((q  (q'  (x  -  m)))  +  m)


By

---

Latex:
(SplitOnConclITE  THENA  Auto')

---

Home Index