Step
*
1
of Lemma
mset_sum_ident_r
1. s : DSet@i'
2. a : MSet{s}@i
3. mset_mon{s} ∈ AbMon
⊢ (a + 0{s}) = a ∈ MSet{s}
BY
{ ((AddAllProperties 3
THENM ARepD ["compound";"basic"]
THENM All Reduce) THEN Auto) }
Latex:
Latex:
1. s : DSet@i'
2. a : MSet\{s\}@i
3. mset\_mon\{s\} \mmember{} AbMon
\mvdash{} (a + 0\{s\}) = a
By
Latex:
((AddAllProperties 3
THENM ARepD ["compound";"basic"]
THENM All Reduce) THEN Auto)
Home
Index