---

Step * of Lemma l_all_reduce

∀[T:Type]. ∀[L:T List]. ∀[P:T ⟶ 𝔹].  uiff((∀x∈L.↑P[x]);↑reduce(λx,y. (P[x] ∧b y);tt;L))
BY
{ TACTIC:(RepeatFor 2 ((TACTIC:D 0 THENA Auto)) THEN ListInd (-1) THEN Reduce 0) }

1
1. T : Type
⊢ ∀[P:T ⟶ 𝔹]. uiff((∀x∈[].↑P[x]);True)

2
1. T : Type
2. u : T
3. v : T List
4. ∀[P:T ⟶ 𝔹]. uiff((∀x∈v.↑P[x]);↑reduce(λx,y. (P[x] ∧b y);tt;v))
⊢ ∀[P:T ⟶ 𝔹]. uiff((∀x∈[u / v].↑P[x]);↑(P[u] ∧b reduce(λx,y. (P[x] ∧b y);tt;v)))

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[L:T  List].  \mforall{}[P:T  {}\mrightarrow{}  \mBbbB{}].    uiff((\mforall{}x\mmember{}L.\muparrow{}P[x]);\muparrow{}reduce(\mlambda{}x,y.  (P[x]  \mwedge{}\msubb{}  y);tt;L))


By

---

Latex:
TACTIC:(RepeatFor  2  ((TACTIC:D  0  THENA  Auto))  THEN  ListInd  (-1)  THEN  Reduce  0)

---

Home Index