---

Step * 1 1 of Lemma seq-append-bar

.....subterm..... T:t
2:n
1. k : ℕ@i
2. s : ℕk ⟶ ℕ@i
3. x : ℕ@i
4. Q : n:ℕ ⟶ (ℕn ⟶ ℕ) ⟶ ℙ@i'
5. ∀f:ℕ ⟶ ℕ. ∃n:ℕ. ∀m:{n...}. Q[m + k;seq-append(k;m;s;f)]
6. f : ℕ ⟶ ℕ@i
7. n : ℕ
8. ∀m:{n...}. Q[m + k;seq-append(k;m;s;λv.if v=0 then x else (f (v - 1)))]
9. m : {n...}@i
10. Q[m + k;seq-append(k;m;s;λv.if v=0 then x else (f (v - 1)))]
⊢ seq-append(k + 1;m;s.x@k;f) = seq-append(k;m;s;λv.if v=0 then x else (f (v - 1))) ∈ (ℕm + k ⟶ ℕ)
BY
{ ((Ext THENA Auto) THEN RepUR ``seq-append seq-add`` 0 THEN Repeat (AutoSplit)) }

---

Latex:

---

Latex:
.....subterm.....  T:t
2:n
1.  k  :  \mBbbN{}@i
2.  s  :  \mBbbN{}k  {}\mrightarrow{}  \mBbbN{}@i
3.  x  :  \mBbbN{}@i
4.  Q  :  n:\mBbbN{}  {}\mrightarrow{}  (\mBbbN{}n  {}\mrightarrow{}  \mBbbN{})  {}\mrightarrow{}  \mBbbP{}@i'
5.  \mforall{}f:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}.  \mexists{}n:\mBbbN{}.  \mforall{}m:\{n...\}.  Q[m  +  k;seq-append(k;m;s;f)]
6.  f  :  \mBbbN{}  {}\mrightarrow{}  \mBbbN{}@i
7.  n  :  \mBbbN{}
8.  \mforall{}m:\{n...\}.  Q[m  +  k;seq-append(k;m;s;\mlambda{}v.if  v=0  then  x  else  (f  (v  -  1)))]
9.  m  :  \{n...\}@i
10.  Q[m  +  k;seq-append(k;m;s;\mlambda{}v.if  v=0  then  x  else  (f  (v  -  1)))]
\mvdash{}  seq-append(k  +  1;m;s.x@k;f)  =  seq-append(k;m;s;\mlambda{}v.if  v=0  then  x  else  (f  (v  -  1)))


By

---

Latex:
((Ext  THENA  Auto)  THEN  RepUR  ``seq-append  seq-add``  0  THEN  Repeat  (AutoSplit))

---

Home Index