---

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


1. n : finite-nat-seq()@i
2. a : finite-nat-seq()@i
3. b : finite-nat-seq()@i
4. x : ℕ@i
5. ↑init-seg-nat-seq(n**λi.x^(1);a**b)
⊢ (↑init-seg-nat-seq(a;n)) ∨ (↑init-seg-nat-seq(n**λi.x^(1);a))
BY
{ ((DVar `b' THEN DVar `a' THEN DVar `n')
   THEN (RenameVar `nn' 1⋅ THEN RenameVar `ns' 2⋅)
   THEN (RenameVar `an' 3⋅ THEN RenameVar `as' 4⋅)
   THEN RenameVar `bn' 5⋅
   THEN RenameVar `bs' 6⋅) }

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

---

Latex:

---

Latex:

1.  n  :  finite-nat-seq()@i
2.  a  :  finite-nat-seq()@i
3.  b  :  finite-nat-seq()@i
4.  x  :  \mBbbN{}@i
5.  \muparrow{}init-seg-nat-seq(n**\mlambda{}i.x\^{}(1);a**b)
\mvdash{}  (\muparrow{}init-seg-nat-seq(a;n))  \mvee{}  (\muparrow{}init-seg-nat-seq(n**\mlambda{}i.x\^{}(1);a))


By

---

Latex:
((DVar  `b'  THEN  DVar  `a'  THEN  DVar  `n')
  THEN  (RenameVar  `nn'  1\mcdot{}  THEN  RenameVar  `ns'  2\mcdot{})
  THEN  (RenameVar  `an'  3\mcdot{}  THEN  RenameVar  `as'  4\mcdot{})
  THEN  RenameVar  `bn'  5\mcdot{}
  THEN  RenameVar  `bs'  6\mcdot{})

---

Home Index