Theory "operator"

Parents     while   numeral

Signature

Constant Type
ASSOC :(α -> α -> α) -> bool
COMM :(α -> α -> β) -> bool
FCOMM :(α -> β -> α) -> (γ -> α -> α) -> bool
LEFT_ID :(α -> β -> β) -> α -> bool
MONOID :(α -> α -> α) -> α -> bool
RIGHT_ID :(α -> β -> α) -> β -> 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
RIGHT_ID_DEF 
|- ∀f e. RIGHT_ID f e ⇔ ∀x. f x e = x
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

Theorems

ASSOC_CONJ 
|- ASSOC $/\
ASSOC_SYM 
|- ∀f. ASSOC f ⇔ ∀x y z. f (f x y) z = f x (f y z)
ASSOC_DISJ 
|- ASSOC $\/
FCOMM_ASSOC 
|- ∀f. FCOMM f f ⇔ ASSOC f
MONOID_CONJ_T 
|- MONOID $/\ T
MONOID_DISJ_F 
|- MONOID $\/ F