---

Step * of Lemma accum_induction

∀[T:Type]. ∀[Q:(T List) ⟶ ℙ].  ((∀[ys:T List]. (Q[ys] ⇒ (∀y:T. Q[ys @ [y]]))) ⇒ Q[[]] ⇒ {∀zs:T List. Q[zs]})
BY
{ (UseWitness ⌜λf,b,L. accumulate (with value p and list item y): f p yover list:  Lwith starting value: b)⌝⋅
   THEN Unfolds ``uall`` 0
   THEN RepeatFor 2 ((MemTypeCD THENW Auto))
   THEN RepeatFor 2 ((MemCD THENA Auto))
   THEN Unfold `guard` 0
   THEN (MemCD THENA Auto)) }

1
.....subterm..... T:t
1:n
1. T : Type
2. Q : (T List) ⟶ ℙ
3. f : ⋂ys:T List. (Q[ys] ⇒ (∀y:T. Q[ys @ [y]]))
4. b : Q[[]]
5. L : T List
⊢ accumulate (with value p and list item y):
   f p y
  over list:
    L
  with starting value:
   b) ∈ Q[L]

---

Latex:

---

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


By

---

Latex:
(UseWitness  \mkleeneopen{}\mlambda{}f,b,L.  accumulate  (with  value  p  and  list  item  y):
                                            f  p  y
                                          over  list:
                                              L
                                          with  starting  value:
                                            b)\mkleeneclose{}\mcdot{}
  THEN  Unfolds  ``uall``  0
  THEN  RepeatFor  2  ((MemTypeCD  THENW  Auto))
  THEN  RepeatFor  2  ((MemCD  THENA  Auto))
  THEN  Unfold  `guard`  0
  THEN  (MemCD  THENA  Auto))

---

Home Index