---

Step * of Lemma list_decomp_member

∀[T:Type]. ∀L:T List. ∀i:ℕ||L||.  ∃as,bs:T List. (L = (as @ [L[i]] @ bs) ∈ (T List))
BY
{ ((UnivCD THENA Auto)
   THEN (InstConcl [⌜firstn(i;L)⌝;⌜nth_tl(1 + i;L)⌝]⋅ THENA Auto)
   THEN (InstLemma `nth_tl_decomp_eq` [⌜T⌝;⌜i⌝;⌜L⌝]⋅ THENA Auto)⋅
   THEN Reduce 0
   THEN (RWO "-1<" 0 THENA Auto)
   THEN (RWO "append_firstn_lastn" 0 THENA Auto)) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}L:T  List.  \mforall{}i:\mBbbN{}||L||.    \mexists{}as,bs:T  List.  (L  =  (as  @  [L[i]]  @  bs))


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  (InstConcl  [\mkleeneopen{}firstn(i;L)\mkleeneclose{};\mkleeneopen{}nth\_tl(1  +  i;L)\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (InstLemma  `nth\_tl\_decomp\_eq`  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}i\mkleeneclose{};\mkleeneopen{}L\mkleeneclose{}]\mcdot{}  THENA  Auto)\mcdot{}
  THEN  Reduce  0
  THEN  (RWO  "-1<"  0  THENA  Auto)
  THEN  (RWO  "append\_firstn\_lastn"  0  THENA  Auto))

---

Home Index