---

Step * of Lemma sublist_accum

∀[T:Type]
  ∀L,l1,l2:T List. ∀f:(T List) ⟶ T ⟶ (T List).
    (l1 ⊆ l2
    ⇒ (∀x:T. ∀l:T List.  l ⊆ f[l;x])
    ⇒ l1 ⊆ accumulate (with value l and list item x):
             f[l;x]
            over list:
              L
            with starting value:
             l2))
BY
{ (InductionOnList
   THEN Reduce 0
   THEN Auto
   THEN (InstHyp [⌜l1⌝;⌜f[l2;u]⌝;⌜f⌝] (-6)⋅ THEN Auto)
   THEN (InstHyp [⌜u⌝;⌜l2⌝] (-1)⋅ THENA Auto)
   THEN FLemma `sublist_transitivity` [-3;-1]
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[T:Type]
    \mforall{}L,l1,l2:T  List.  \mforall{}f:(T  List)  {}\mrightarrow{}  T  {}\mrightarrow{}  (T  List).
        (l1  \msubseteq{}  l2
        {}\mRightarrow{}  (\mforall{}x:T.  \mforall{}l:T  List.    l  \msubseteq{}  f[l;x])
        {}\mRightarrow{}  l1  \msubseteq{}  accumulate  (with  value  l  and  list  item  x):
                          f[l;x]
                        over  list:
                            L
                        with  starting  value:
                          l2))


By

---

Latex:
(InductionOnList
  THEN  Reduce  0
  THEN  Auto
  THEN  (InstHyp  [\mkleeneopen{}l1\mkleeneclose{};\mkleeneopen{}f[l2;u]\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{}]  (-6)\mcdot{}  THEN  Auto)
  THEN  (InstHyp  [\mkleeneopen{}u\mkleeneclose{};\mkleeneopen{}l2\mkleeneclose{}]  (-1)\mcdot{}  THENA  Auto)
  THEN  FLemma  `sublist\_transitivity`  [-3;-1]
  THEN  Auto)

---

Home Index