Step
*
1
of Lemma
mk_dmon
1. T : Type
2. eq : T ⟶ T ⟶ 𝔹
3. le : T ⟶ T ⟶ 𝔹
4. op : T ⟶ T ⟶ T
5. id : T
6. inv : T ⟶ T
7. IsEqFun(T;eq)
8. Assoc(T;op)
9. Ident(T;op;id)
⊢ <T, eq, le, op, id, inv> ∈ DMon
BY
{ MemTypeCD THEN AbReduce 0 THEN Auto }
1
1. T : Type
2. eq : T ⟶ T ⟶ 𝔹
3. le : T ⟶ T ⟶ 𝔹
4. op : T ⟶ T ⟶ T
5. id : T
6. inv : T ⟶ T
7. IsEqFun(T;eq)
8. Assoc(T;op)
9. Ident(T;op;id)
⊢ <T, eq, le, op, id, inv> ∈ Mon
Latex:
Latex:
1. T : Type
2. eq : T {}\mrightarrow{} T {}\mrightarrow{} \mBbbB{}
3. le : T {}\mrightarrow{} T {}\mrightarrow{} \mBbbB{}
4. op : T {}\mrightarrow{} T {}\mrightarrow{} T
5. id : T
6. inv : T {}\mrightarrow{} T
7. IsEqFun(T;eq)
8. Assoc(T;op)
9. Ident(T;op;id)
\mvdash{} <T, eq, le, op, id, inv> \mmember{} DMon
By
Latex:
MemTypeCD THEN AbReduce 0 THEN Auto
Home
Index