plus2(ac)R(T, T) → T
	bTx + y
minus2R(T, T) → T
	bTx - y
multiplies2(ac)R(T, T) → T
	bTx * y
divides2R(T, T) → T
	bTx / y
modulus2R(T, T) → T
	bTx % y
negate1uT(T) → T
	uT-x

equal_to2(c)bP(T, T) → bool
	bTx == y
not_equal_to2(c)bP(T, T) → bool
	bTx != y
less2bP(T, T) → bool
	bTx < y
greater2bP(T, T) → bool
	bTx > y
less_equal2bP(T, T) → bool
	bTx <= y
greater_equal2bP(T, T) → bool
	bTx >= y

logical_and2(c)bP(T, T) → bool
	bTx and y
logical_or2(c)bP(T, T) → bool
	bTx or y
logical_not1uP(T) → bool
	uTnot x

bit_and2(ac)R(T, T) → T
	bTx & y
bit_or2(ac)R(T, T) → T
	bTx | y
bit_xor2(ac)R(T, T) → T
	bTx ^ y
bit_not1uT(T) → T
	uT~x