---

Step * of Lemma int-list-index-append

No Annotations
∀[x:ℤ]. ∀[L1,L2:ℤ List].
  (int-list-index(L1 @ L2;x) ~ if int-list-member(x;L1)
  then int-list-index(L1;x)
  else ||L1|| + int-list-index(L2;x)
  fi )
BY
{ (InductionOnList THEN Reduce 0) }

1
1. x : ℤ
⊢ ∀[L2:ℤ List]
    (int-list-index(L2;x) ~ if int-list-member(x;[]) then int-list-index([];x) else 0 + int-list-index(L2;x) fi )

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

---

Latex:

---

Latex:
No  Annotations
\mforall{}[x:\mBbbZ{}].  \mforall{}[L1,L2:\mBbbZ{}  List].
    (int-list-index(L1  @  L2;x)  \msim{}  if  int-list-member(x;L1)
    then  int-list-index(L1;x)
    else  ||L1||  +  int-list-index(L2;x)
    fi  )


By

---

Latex:
(InductionOnList  THEN  Reduce  0)

---

Home Index