---

Step * 1 1 1 1 2 1 of Lemma assert-init-seg-nat-seq


1. n : ℕ
2. k : ℕ
3. s : ℕn ⟶ ℕ
4. r : ℕn + k ⟶ ℕ
5. n + k ∈ ℕ
6. n1 : ℕ
7. h1 : ℕn1 ⟶ ℕ
8. (n + k) = (n + n1) ∈ ℕ
9. r = (λx.if (x) < (n)  then s x  else (h1 (x - n))) ∈ (ℕn + k ⟶ ℕ)
⊢ s = r ∈ (ℕn ⟶ ℕ)
BY
{ ((Assert ⌜k = n1 ∈ ℤ⌝⋅ THENA Auto)
   THEN Eliminate ⌜n1⌝⋅
   THEN ThinVar `n1'
   THEN (RWO "-1" 0 THENA Auto)
   THEN (Ext THENA Auto)
   THEN Reduce 0
   THEN AutoSplit) }

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}
2.  k  :  \mBbbN{}
3.  s  :  \mBbbN{}n  {}\mrightarrow{}  \mBbbN{}
4.  r  :  \mBbbN{}n  +  k  {}\mrightarrow{}  \mBbbN{}
5.  n  +  k  \mmember{}  \mBbbN{}
6.  n1  :  \mBbbN{}
7.  h1  :  \mBbbN{}n1  {}\mrightarrow{}  \mBbbN{}
8.  (n  +  k)  =  (n  +  n1)
9.  r  =  (\mlambda{}x.if  (x)  <  (n)    then  s  x    else  (h1  (x  -  n)))
\mvdash{}  s  =  r


By

---

Latex:
((Assert  \mkleeneopen{}k  =  n1\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  Eliminate  \mkleeneopen{}n1\mkleeneclose{}\mcdot{}
  THEN  ThinVar  `n1'
  THEN  (RWO  "-1"  0  THENA  Auto)
  THEN  (Ext  THENA  Auto)
  THEN  Reduce  0
  THEN  AutoSplit)

---

Home Index