---

Step * of Lemma lsum-of-even

No Annotations
∀[T:Type]. ∀[L:T List]. ∀[f:{x:T| (x ∈ L)}  ⟶ ℤ].  ↑isEven(Σ(f[x] | x ∈ L)) supposing (∀x∈L.↑isEven(f[x]))
BY
{ (InductionOnList
   THEN Reduce 0
   THEN ((RepeatFor 2 (ParallelLast)
          THEN (InstLemma `l_all_cons` [⌜{x:T| (x ∈ [u / v])} ⌝]⋅ THENA Auto)
          THEN RWO "-1" 6
          THEN Auto)
   ORELSE Auto
   )) }

1
1. T : Type
2. u : T
3. v : T List
4. ∀[f:{x:T| (x ∈ v)}  ⟶ ℤ]. ↑isEven(Σ(f[x] | x ∈ v)) supposing (∀x∈v.↑isEven(f[x]))
5. f : {x:T| (x ∈ [u / v])}  ⟶ ℤ
6. ↑isEven(f[u])
7. (∀x∈v.↑isEven(f[x]))
8. ↑isEven(Σ(f[x] | x ∈ v))
9. ∀[P:{x:T| (x ∈ [u / v])}  ⟶ ℙ]
     ∀x:{x:T| (x ∈ [u / v])} . ∀L:{x:T| (x ∈ [u / v])}  List.  ((∀y∈[x / L].P[y]) ⇐⇒ P[x] ∧ (∀y∈L.P[y]))
⊢ ↑isEven(f[u] + Σ(f[x] | x ∈ v))

---

Latex:

---

Latex:
No  Annotations
\mforall{}[T:Type].  \mforall{}[L:T  List].  \mforall{}[f:\{x:T|  (x  \mmember{}  L)\}    {}\mrightarrow{}  \mBbbZ{}].
    \muparrow{}isEven(\mSigma{}(f[x]  |  x  \mmember{}  L))  supposing  (\mforall{}x\mmember{}L.\muparrow{}isEven(f[x]))


By

---

Latex:
(InductionOnList
  THEN  Reduce  0
  THEN  ((RepeatFor  2  (ParallelLast)
                THEN  (InstLemma  `l\_all\_cons`  [\mkleeneopen{}\{x:T|  (x  \mmember{}  [u  /  v])\}  \mkleeneclose{}]\mcdot{}  THENA  Auto)
                THEN  RWO  "-1"  6
                THEN  Auto)
  ORELSE  Auto
  ))

---

Home Index