---

Step * of Lemma seq-append-bar

∀k:ℕ. ∀s:ℕk ⟶ ℕ. ∀x:ℕ. ∀Q:n:ℕ ⟶ (ℕn ⟶ ℕ) ⟶ ℙ.
  ((∀f:ℕ ⟶ ℕ. ∃n:ℕ. ∀m:{n...}. Q[m + k;seq-append(k;m;s;f)])
  ⇒ (∀f:ℕ ⟶ ℕ. ∃n:ℕ. ∀m:{n...}. Q[m + k;seq-append(k + 1;m;s.x@k;f)]))
BY
{ ((UnivCD THENA Auto)
   THEN (InstHyp [⌜λv.if v=0 then x else (f (v - 1))⌝] (-2)⋅ THENA Auto)
   THEN ExRepD
   THEN InstConcl [⌜n⌝]⋅
   THEN Auto) }

1
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)]

---

Latex:

---

Latex:
\mforall{}k:\mBbbN{}.  \mforall{}s:\mBbbN{}k  {}\mrightarrow{}  \mBbbN{}.  \mforall{}x:\mBbbN{}.  \mforall{}Q:n:\mBbbN{}  {}\mrightarrow{}  (\mBbbN{}n  {}\mrightarrow{}  \mBbbN{})  {}\mrightarrow{}  \mBbbP{}.
    ((\mforall{}f:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}.  \mexists{}n:\mBbbN{}.  \mforall{}m:\{n...\}.  Q[m  +  k;seq-append(k;m;s;f)])
    {}\mRightarrow{}  (\mforall{}f:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}.  \mexists{}n:\mBbbN{}.  \mforall{}m:\{n...\}.  Q[m  +  k;seq-append(k  +  1;m;s.x@k;f)]))


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  (InstHyp  [\mkleeneopen{}\mlambda{}v.if  v=0  then  x  else  (f  (v  -  1))\mkleeneclose{}]  (-2)\mcdot{}  THENA  Auto)
  THEN  ExRepD
  THEN  InstConcl  [\mkleeneopen{}n\mkleeneclose{}]\mcdot{}
  THEN  Auto)

---

Home Index