---

Step * 1 1 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(ns^(nn)**λi.x^(1);as^(an)**bs^(bn))
9. (nn + 1) ≤ an
⊢ ↑init-seg-nat-seq(ns^(nn)**λi.x^(1);as^(an))
BY
{ ((RWO "assert-init-seg-nat-seq2" (-2) THENA Auto)
   THEN (RWO "assert-init-seg-nat-seq2" 0 THENA Auto)
   THEN All(RepUR ``append-finite-nat-seq mk-finite-nat-seq``)
   THEN RepD) }

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. (nn + 1) ≤ (an + bn)
9. (λx@0.if (x@0) < (nn)  then ns x@0  else x) = (λx.if (x) < (an)  then as x  else (bs (x - an))) ∈ (ℕnn + 1 ⟶ ℕ)
10. (nn + 1) ≤ an
⊢ ((nn + 1) ≤ an) ∧ ((λx@0.if (x@0) < (nn)  then ns x@0  else x) = as ∈ (ℕnn + 1 ⟶ ℕ))

---

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(ns\^{}(nn)**\mlambda{}i.x\^{}(1);as\^{}(an)**bs\^{}(bn))
9.  (nn  +  1)  \mleq{}  an
\mvdash{}  \muparrow{}init-seg-nat-seq(ns\^{}(nn)**\mlambda{}i.x\^{}(1);as\^{}(an))


By

---

Latex:
((RWO  "assert-init-seg-nat-seq2"  (-2)  THENA  Auto)
  THEN  (RWO  "assert-init-seg-nat-seq2"  0  THENA  Auto)
  THEN  All(RepUR  ``append-finite-nat-seq  mk-finite-nat-seq``)
  THEN  RepD)

---

Home Index