---

Step * 1 of Lemma seq-append-bar


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
⊢ Q[m + k;seq-append(k + 1;m;s.x@k;f)]
BY
{ ((InstHyp [⌜m⌝] (-2)⋅ THENA Auto) THEN NthHypEq (-1) THEN EqCD THEN Try (CpltAuto)) }

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

---

Latex:

---

Latex:

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
\mvdash{}  Q[m  +  k;seq-append(k  +  1;m;s.x@k;f)]


By

---

Latex:
((InstHyp  [\mkleeneopen{}m\mkleeneclose{}]  (-2)\mcdot{}  THENA  Auto)  THEN  NthHypEq  (-1)  THEN  EqCD  THEN  Try  (CpltAuto))

---

Home Index