---

Step * 1 of Lemma append-finite-nat-seq-assoc

.....subterm..... T:t
2:n
1. n2 : ℕ
2. f1 : ℕn2 ⟶ ℕ
3. n1 : ℕ
4. g1 : ℕn1 ⟶ ℕ
5. n : ℕ
6. h1 : ℕn ⟶ ℕ
⊢ (λx.if (x) < (n2 + n1)  then if (x) < (n2)  then f1 x  else (g1 (x - n2))  else (h1 (x - n2 + n1)))
= (λx.if (x) < (n2)  then f1 x  else if (x - n2) < (n1)  then g1 (x - n2)  else (h1 (x - n2 - n1)))
∈ (ℕ(n2 + n1) + n ⟶ ℕ)
BY
{ ((Ext THENA Auto) THEN Reduce 0 THEN AutoSplit) }

---

Latex:

---

Latex:
.....subterm.....  T:t
2:n
1.  n2  :  \mBbbN{}
2.  f1  :  \mBbbN{}n2  {}\mrightarrow{}  \mBbbN{}
3.  n1  :  \mBbbN{}
4.  g1  :  \mBbbN{}n1  {}\mrightarrow{}  \mBbbN{}
5.  n  :  \mBbbN{}
6.  h1  :  \mBbbN{}n  {}\mrightarrow{}  \mBbbN{}
\mvdash{}  (\mlambda{}x.if  (x)  <  (n2  +  n1)
                  then  if  (x)  <  (n2)    then  f1  x    else  (g1  (x  -  n2))
                  else  (h1  (x  -  n2  +  n1)))
=  (\mlambda{}x.if  (x)  <  (n2)    then  f1  x    else  if  (x  -  n2)  <  (n1)    then  g1  (x  -  n2)    else  (h1  (x  -  n2  -  n1)))


By

---

Latex:
((Ext  THENA  Auto)  THEN  Reduce  0  THEN  AutoSplit)

---

Home Index