Theory: operator

Parents

• bool

Types

Constants

• LEFT_ID  :('a -> 'b -> 'b) -> 'a -> bool
• ASSOC  :('a -> 'a -> 'a) -> bool
• MONOID  :('a -> 'a -> 'a) -> 'a -> bool
• RIGHT_ID  :('a -> 'b -> 'a) -> 'b -> bool
• FCOMM  :('a -> 'b -> 'a) -> ('c -> 'a -> 'a) -> bool
• COMM  :('a -> 'a -> 'b) -> bool

Definitions

ASSOC_DEF

|- !f. ASSOC f = !x y z. f x (f y z) = f (f x y) z

COMM_DEF

|- !f. COMM f = !x y. f x y = f y x

FCOMM_DEF

|- !f g. FCOMM f g = !x y z. g x (f y z) = f (g x y) z

LEFT_ID_DEF

|- !f e. LEFT_ID f e = !x. f e x = x

MONOID_DEF

|- !f e. MONOID f e = ASSOC f /\ RIGHT_ID f e /\ LEFT_ID f e

RIGHT_ID_DEF

|- !f e. RIGHT_ID f e = !x. f x e = x

Theorems

ASSOC_CONJ

|- ASSOC $/\

ASSOC_DISJ

|- ASSOC $\/

FCOMM_ASSOC

|- !f. FCOMM f f = ASSOC f

MONOID_CONJ_T

|- MONOID $/\ T

MONOID_DISJ_F

|- MONOID $\/ F