---

Step * of Lemma bl-all-as-accum

∀[T:Type]. ∀[L:T List]. ∀[P:T ⟶ 𝔹].
  ((∀x∈L.P[x])_b ~ accumulate (with value p and list item x):
                    p ∧b P[x]
                   over list:
                     L
                   with starting value:
                    tt))
BY
{ (Auto THEN Unfold `bl-all` 0 THEN RWO "reduce-as-accum" 0 THEN Reduce 0 THEN Auto) }

1
1. T : Type
2. L : T List
3. P : T ⟶ 𝔹
⊢ accumulate (with value p and list item x):
   P[x] ∧b p
  over list:
    L
  with starting value:
   tt) 
= accumulate (with value p and list item x):
   p ∧b P[x]
  over list:
    L
  with starting value:
   tt)

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[L:T  List].  \mforall{}[P:T  {}\mrightarrow{}  \mBbbB{}].
    ((\mforall{}x\mmember{}L.P[x])\_b  \msim{}  accumulate  (with  value  p  and  list  item  x):
                                        p  \mwedge{}\msubb{}  P[x]
                                      over  list:
                                          L
                                      with  starting  value:
                                        tt))


By

---

Latex:
(Auto  THEN  Unfold  `bl-all`  0  THEN  RWO  "reduce-as-accum"  0  THEN  Reduce  0  THEN  Auto)

---

Home Index