---

Step * 1 of Lemma app_permf_comp

.....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
BY
{ ((BoolCasesOnCExp x <z m THENM AbReduce 0) THENA Auto) }

1
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. x < m
⊢ if p' x <z m then p (p' x) else (q ((p' x) - m)) + m fi  = (p (p' x)) ∈ ℕm + n

2
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

---

Latex:

---

Latex:
.....subterm.....  T:t
1:n
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
\mvdash{}  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 


By

---

Latex:
((BoolCasesOnCExp  x  <z  m  THENM  AbReduce  0)  THENA  Auto)

---

Home Index