Step
*
of Lemma
mon_for_append
No Annotations
∀g:IMonoid. ∀A:Type. ∀f:A ⟶ |g|. ∀as,as':A List.
((For{g} x ∈ as @ as'. f[x]) = ((For{g} x ∈ as. f[x]) * (For{g} x ∈ as'. f[x])) ∈ |g|)
BY
{ (Unfold `mon_for` 0 THEN InductionOnListA THEN Reduce 0 THEN Auto) }
1
1. g : IMonoid
2. A : Type
3. f : A ⟶ |g|
4. a : A
5. as : A List
6. ∀as':A List. ((For{A,*,e} x ∈ as @ as'. f[x]) = ((For{A,*,e} x ∈ as. f[x]) * (For{A,*,e} x ∈ as'. f[x])) ∈ |g|)
7. as' : A List
⊢ (* f[a] (For{A,*,e} x ∈ as @ as'. f[x])) = ((* f[a] (For{A,*,e} x ∈ as. f[x])) * (For{A,*,e} x ∈ as'. f[x])) ∈ |g|
Latex:
Latex:
No Annotations
\mforall{}g:IMonoid. \mforall{}A:Type. \mforall{}f:A {}\mrightarrow{} |g|. \mforall{}as,as':A List.
((For\{g\} x \mmember{} as @ as'. f[x]) = ((For\{g\} x \mmember{} as. f[x]) * (For\{g\} x \mmember{} as'. f[x])))
By
Latex:
(Unfold `mon\_for` 0 THEN InductionOnListA THEN Reduce 0 THEN Auto)
Home
Index