---

Step * of Lemma bl-exists-as-accum

∀[T:Type]. ∀[L:T List]. ∀[P:T ⟶ 𝔹].
  ((∃x∈L.P[x])_b ~ accumulate (with value p and list item x):
                    p ∨bP[x]
                   over list:
                     L
                   with starting value:
                    ff))
BY
{ (Auto
   THEN Unfold `bl-exists` 0
   THEN RWO "reduce-as-accum" 0
   THEN Reduce 0
   THEN Auto
   THEN Try ((AutoBoolCase ⌜P[y]⌝⋅ THEN AutoBoolCase ⌜P[x]⌝⋅))
   THEN EqCD
   THEN Auto) }

1
.....subterm..... T:t
1:n
1. T : Type
2. L : T List
3. P : T ⟶ 𝔹
4. p : 𝔹
5. x : T
⊢ P[x] ∨bp = p ∨bP[x]

---

Latex:

---

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


By

---

Latex:
(Auto
  THEN  Unfold  `bl-exists`  0
  THEN  RWO  "reduce-as-accum"  0
  THEN  Reduce  0
  THEN  Auto
  THEN  Try  ((AutoBoolCase  \mkleeneopen{}P[y]\mkleeneclose{}\mcdot{}  THEN  AutoBoolCase  \mkleeneopen{}P[x]\mkleeneclose{}\mcdot{}))
  THEN  EqCD
  THEN  Auto)

---

Home Index