---

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


1. x : ℤ
2. u : ℤ
3. v : ℤ List
4. ∀[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 )
⊢ ∀[L2:ℤ List]
    (int-list-index([u / (v @ L2)];x) ~ if int-list-member(x;[u / v])
    then int-list-index([u / v];x)
    else (||v|| + 1) + int-list-index(L2;x)
    fi )
BY
{ (Auto THEN AutoSplit THEN Unfold `int-list-index` 0 THEN Reduce 0 THEN Fold `int-list-index` 0 THEN AutoSplit) }

1
1. x : ℤ
2. u : ℤ
3. u ≠ x
4. v : ℤ List
5. ∀[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 )
6. L2 : ℤ List
7. (x ∈ [u / v])
⊢ (int-list-index(v @ L2;x) + 1) = (int-list-index(v;x) + 1) ∈ ℕ(||v @ L2|| + 1) + 1

2
1. x : ℤ
2. u : ℤ
3. v : ℤ List
4. ¬(x ∈ [u / v])
5. ∀[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 )
6. L2 : ℤ List
7. u = x ∈ ℤ
⊢ 0 = ((||v|| + 1) + int-list-index(L2;x)) ∈ ℕ(||v @ L2|| + 1) + 1

3
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

---

Latex:

---

Latex:

1.  x  :  \mBbbZ{}
2.  u  :  \mBbbZ{}
3.  v  :  \mBbbZ{}  List
4.  \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  )
\mvdash{}  \mforall{}[L2:\mBbbZ{}  List]
        (int-list-index([u  /  (v  @  L2)];x)  \msim{}  if  int-list-member(x;[u  /  v])
        then  int-list-index([u  /  v];x)
        else  (||v||  +  1)  +  int-list-index(L2;x)
        fi  )


By

---

Latex:
(Auto
  THEN  AutoSplit
  THEN  Unfold  `int-list-index`  0
  THEN  Reduce  0
  THEN  Fold  `int-list-index`  0
  THEN  AutoSplit)

---

Home Index