Step * 1 1 of Lemma mset_for_wf


1. DSet
2. IAbMonoid
3. |s| ⟶ |g|
4. as |s| List
5. bs |s| List
6. as ≡(|s|) bs
⊢ (For{g} x ∈ as. f[x]) (For{g} x ∈ bs. f[x]) ∈ |g|
BY
((RWH (HypC (-1)) 0) THEN Auto) }


Latex:


Latex:

1.  s  :  DSet
2.  g  :  IAbMonoid
3.  f  :  |s|  {}\mrightarrow{}  |g|
4.  as  :  |s|  List
5.  bs  :  |s|  List
6.  as  \mequiv{}(|s|)  bs
\mvdash{}  (For\{g\}  x  \mmember{}  as.  f[x])  =  (For\{g\}  x  \mmember{}  bs.  f[x])


By


Latex:
((RWH  (HypC  (-1))  0)  THEN  Auto)




Home Index