---

Step * of Lemma split-maximal-consecutive_wf

∀[T:Type]. ∀[g:T ⟶ ℤ]. ∀[L:T List+].
  (split-maximal-consecutive(g;L) ∈ {p:T List+ × (T List)| L = ((fst(p)) @ (snd(p))) ∈ (T List)} )
BY
{ (Auto
   THEN Unfold `split-maximal-consecutive` 0
   THEN GenConclAtAddr [2;1]
   THEN (CallByValueReduce 0 THENA Auto)
   THEN (RWO "eval_list_sq" 0 THENA Auto)
   THEN RepeatFor 2 ((CallByValueReduce 0 THENA Auto))
   THEN MemTypeCD
   THEN Auto
   THEN Reduce 0
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[g:T  {}\mrightarrow{}  \mBbbZ{}].  \mforall{}[L:T  List\msupplus{}].
    (split-maximal-consecutive(g;L)  \mmember{}  \{p:T  List\msupplus{}  \mtimes{}  (T  List)|  L  =  ((fst(p))  @  (snd(p)))\}  )


By

---

Latex:
(Auto
  THEN  Unfold  `split-maximal-consecutive`  0
  THEN  GenConclAtAddr  [2;1]
  THEN  (CallByValueReduce  0  THENA  Auto)
  THEN  (RWO  "eval\_list\_sq"  0  THENA  Auto)
  THEN  RepeatFor  2  ((CallByValueReduce  0  THENA  Auto))
  THEN  MemTypeCD
  THEN  Auto
  THEN  Reduce  0
  THEN  Auto)

---

Home Index