Step * 1 of Lemma mk_abdmonoid


1. 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)
10. Comm(T;op)
⊢ <T, eq, le, op, id, inv> ∈ AbDMon
BY
MemTypeCD THEN AbReduce THEN Auto }

1
1. 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)
10. Comm(T;op)
⊢ <T, eq, le, op, id, inv> ∈ DMon


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)
10.  Comm(T;op)
\mvdash{}  <T,  eq,  le,  op,  id,  inv>  \mmember{}  AbDMon


By


Latex:
MemTypeCD  THEN  AbReduce  0  THEN  Auto




Home Index