---

Step * of Lemma int-list-member-append

∀[i:ℤ]. ∀[xs,ys:ℤ List].  (int-list-member(i;xs @ ys) ~ int-list-member(i;xs) ∨bint-list-member(i;ys))
BY
{ xxx(InductionOnList
      THEN Reduce 0
      THEN Unfold `int-list-member` 0
      THEN Reduce 0
      THEN Fold `int-list-member` 0
      THEN Auto
      THEN RWO "-2" 0
      THEN Auto
      THEN AutoBoolCase ⌜(i =z u)⌝⋅)xxx }

---

Latex:

---

Latex:
\mforall{}[i:\mBbbZ{}].  \mforall{}[xs,ys:\mBbbZ{}  List].
    (int-list-member(i;xs  @  ys)  \msim{}  int-list-member(i;xs)  \mvee{}\msubb{}int-list-member(i;ys))


By

---

Latex:
xxx(InductionOnList
        THEN  Reduce  0
        THEN  Unfold  `int-list-member`  0
        THEN  Reduce  0
        THEN  Fold  `int-list-member`  0
        THEN  Auto
        THEN  RWO  "-2"  0
        THEN  Auto
        THEN  AutoBoolCase  \mkleeneopen{}(i  =\msubz{}  u)\mkleeneclose{}\mcdot{})xxx

---

Home Index