---

Step * 2 3 of Lemma int-list-index-append


1. x : ℤ
2. u : ℤ
3. u ≠ x
4. v : ℤ List
5. ¬(x ∈ [u / v])
6. ∀[L2:ℤ List]
     (int-list-index(v @ L2;x) ~ if int-list-member(x;v) then int-list-index(v;x) else ||v|| + int-list-index(L2;x) fi )
7. L2 : ℤ List
⊢ (int-list-index(v @ L2;x) + 1) = ((||v|| + 1) + int-list-index(L2;x)) ∈ ℕ(||v @ L2|| + 1) + 1
BY
{ ((RW (SweepUpC (HypC 6)) 0 THENW Auto) THEN AutoSplit THEN Assert ⌜(x ∈ [u / v])⌝⋅ THEN Auto) }

---

Latex:

---

Latex:

1.  x  :  \mBbbZ{}
2.  u  :  \mBbbZ{}
3.  u  \mneq{}  x
4.  v  :  \mBbbZ{}  List
5.  \mneg{}(x  \mmember{}  [u  /  v])
6.  \mforall{}[L2:\mBbbZ{}  List]
          (int-list-index(v  @  L2;x)  \msim{}  if  int-list-member(x;v)
          then  int-list-index(v;x)
          else  ||v||  +  int-list-index(L2;x)
          fi  )
7.  L2  :  \mBbbZ{}  List
\mvdash{}  (int-list-index(v  @  L2;x)  +  1)  =  ((||v||  +  1)  +  int-list-index(L2;x))


By

---

Latex:
((RW  (SweepUpC  (HypC  6))  0  THENW  Auto)  THEN  AutoSplit  THEN  Assert  \mkleeneopen{}(x  \mmember{}  [u  /  v])\mkleeneclose{}\mcdot{}  THEN  Auto)

---

Home Index