1N/Aop a : bc

1N/Aop a : b -> c

1N/Aop a : s = e

1N/Aop a :? s = e

1N/Aops __<__ : a * a -> b;

1N/A a : b -> c

1N/Aop a :? b %(opbla)%

1N/A %(a)%

1N/A %(b)%

1N/Aop a :? b %(op bla)%

1N/A %(a)%

1N/A %(b)%

1N/Aop a : b -> c

1N/Aop __<__ : a * a -> b

1N/Aop a : b -> c

1N/Aop a : b, assoc, comm, idem, assoc, unit 1, unit -, assoc

1N/Aop a(a : b; a : b; a, b : c) :? b = e

1N/Aops a, bc, d, e : a ->? b, assoc, idem, comm

1N/Aop a :? b

1N/Aop e : a = e == e

1N/A