---

Step * of Lemma last_induction_accum

∀[T:Type]. ∀[Q:(T List) ⟶ ℙ].  (Q[[]] ⇒ (∀[ys:T List]. (Q[ys] ⇒ (∀y:T. Q[ys @ [y]]))) ⇒ {∀zs:T List. Q[zs]})
BY
{ (Auto
   THEN Unfold `guard` 0
   THEN Auto
   THEN RenameVar `base' (-3)
   THEN RenameVar `step' (-2)
   THEN UseWitness ⌜accumulate (with value a and list item x):
                     step a x
                    over list:
                      zs
                    with starting value:
                     base)⌝⋅) }

1
1. T : Type
2. Q : (T List) ⟶ ℙ
3. base : Q[[]]
4. step : ∀[ys:T List]. (Q[ys] ⇒ (∀y:T. Q[ys @ [y]]))
5. zs : T List
⊢ accumulate (with value a and list item x):
   step a x
  over list:
    zs
  with starting value:
   base) ∈ Q[zs]

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[Q:(T  List)  {}\mrightarrow{}  \mBbbP{}].
    (Q[[]]  {}\mRightarrow{}  (\mforall{}[ys:T  List].  (Q[ys]  {}\mRightarrow{}  (\mforall{}y:T.  Q[ys  @  [y]])))  {}\mRightarrow{}  \{\mforall{}zs:T  List.  Q[zs]\})


By

---

Latex:
(Auto
  THEN  Unfold  `guard`  0
  THEN  Auto
  THEN  RenameVar  `base'  (-3)
  THEN  RenameVar  `step'  (-2)
  THEN  UseWitness  \mkleeneopen{}accumulate  (with  value  a  and  list  item  x):
                                      step  a  x
                                    over  list:
                                        zs
                                    with  starting  value:
                                      base)\mkleeneclose{}\mcdot{})

---

Home Index