---

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

∀[f,g,h:finite-nat-seq()].  (f**g**h = f**g**h ∈ finite-nat-seq())
BY
{ ((UnivCD THENA Auto)
   THEN D 3
   THEN D 2
   THEN D 1
   THEN RepUR ``append-finite-nat-seq finite-nat-seq mk-finite-nat-seq`` 0
   THEN EqCD
   THEN Auto) }

1
.....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 ⟶ ℕ)

---

Latex:

---

Latex:
\mforall{}[f,g,h:finite-nat-seq()].    (f**g**h  =  f**g**h)


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  D  3
  THEN  D  2
  THEN  D  1
  THEN  RepUR  ``append-finite-nat-seq  finite-nat-seq  mk-finite-nat-seq``  0
  THEN  EqCD
  THEN  Auto)

---

Home Index