---

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


1. nn : ℕ@i
2. ns : ℕnn ⟶ ℕ@i
3. an : ℕ@i
4. as : ℕan ⟶ ℕ@i
5. bn : ℕ@i
6. bs : ℕbn ⟶ ℕ@i
7. x : ℕ@i
8. ↑init-seg-nat-seq(<nn, ns>**λi.x^(1);<an, as>**<bn, bs>)
⊢ (↑init-seg-nat-seq(<an, as>;<nn, ns>)) ∨ (↑init-seg-nat-seq(<nn, ns>**λi.x^(1);<an, as>))
BY
{ (Decide ⌜(nn + 1) ≤ an⌝⋅ THENA Auto) }

1
1. nn : ℕ@i
2. ns : ℕnn ⟶ ℕ@i
3. an : ℕ@i
4. as : ℕan ⟶ ℕ@i
5. bn : ℕ@i
6. bs : ℕbn ⟶ ℕ@i
7. x : ℕ@i
8. ↑init-seg-nat-seq(<nn, ns>**λi.x^(1);<an, as>**<bn, bs>)
9. (nn + 1) ≤ an
⊢ (↑init-seg-nat-seq(<an, as>;<nn, ns>)) ∨ (↑init-seg-nat-seq(<nn, ns>**λi.x^(1);<an, as>))

2
1. nn : ℕ@i
2. ns : ℕnn ⟶ ℕ@i
3. an : ℕ@i
4. as : ℕan ⟶ ℕ@i
5. bn : ℕ@i
6. bs : ℕbn ⟶ ℕ@i
7. x : ℕ@i
8. ↑init-seg-nat-seq(<nn, ns>**λi.x^(1);<an, as>**<bn, bs>)
9. ¬((nn + 1) ≤ an)
⊢ (↑init-seg-nat-seq(<an, as>;<nn, ns>)) ∨ (↑init-seg-nat-seq(<nn, ns>**λi.x^(1);<an, as>))

---

Latex:

---

Latex:

1.  nn  :  \mBbbN{}@i
2.  ns  :  \mBbbN{}nn  {}\mrightarrow{}  \mBbbN{}@i
3.  an  :  \mBbbN{}@i
4.  as  :  \mBbbN{}an  {}\mrightarrow{}  \mBbbN{}@i
5.  bn  :  \mBbbN{}@i
6.  bs  :  \mBbbN{}bn  {}\mrightarrow{}  \mBbbN{}@i
7.  x  :  \mBbbN{}@i
8.  \muparrow{}init-seg-nat-seq(<nn,  ns>**\mlambda{}i.x\^{}(1);<an,  as>**<bn,  bs>)
\mvdash{}  (\muparrow{}init-seg-nat-seq(<an,  as><nn,  ns>))  \mvee{}  (\muparrow{}init-seg-nat-seq(<nn,  ns>**\mlambda{}i.x\^{}(1);<an,  as>))


By

---

Latex:
(Decide  \mkleeneopen{}(nn  +  1)  \mleq{}  an\mkleeneclose{}\mcdot{}  THENA  Auto)

---

Home Index