assign(order,kbo). set(lex_order_vars). set(para_units_only). clear(back_demod). set(restrict_denials). formulas(assumptions). % neardomain axioms % additive Bruck loop x + 0 = x. 0 + x = x. -x + (x + y) = y. (x + (y + x)) + z = x + (y + (x + z)). -(x + y) = -x + -y. % multiplicative group (x * y) * z = x * (y * z). 1 * x = x. x * 1 = x. x != 0 -> x' * x = 1. x != 0 -> x * x' = 1. x != 0 -> x'' = x. x != 0 & y != 0 -> (x * y)' = y' * x'. % compatibility 0 * x = 0. x * (y + z) = (x * y) + (x * z). 1 != 0. 1' = 1. -1 != 0. (-1)' = -1. % special automorphism -(x + y) + (x + (y + z)) = d(x,y) * z. % ----------------- % extra assumptions % ----------------- % suffices d(x,y) = 1 # label("nearfield"). end_of_list. formulas(goals). x + y = y + x # label("commutativity of +"). end_of_list. formulas(hints). -x + x = 0. --x + y = x + y. -(x * y) + (x * (y + z)) = x * z. 0 = -0. -0 = 0. --x + 0 = x. x + 0 = --x. --x = x + 0. x + (-x + y) = y. x + -x = 0. x + -(x + y) = -y. (x + y) + (d(x,y) * z) = x + (y + z). -(x * y) + (x * y) = x * 0. -(x * y) + (x * 0) = x * -y. x * 0 = 0. x * -0 = 0. -(x * y) + 0 = x * -y. x * -y = -(x * y). -(x * y) = x * -y. -(0 * x) = 0. (x + y) + (1 * z) = x + (y + z). (x + y) + z = x + (y + z). 0 + (0 + x) = x. -(x * 0) = 0. 0 + (0 * x) = 0. 0 + (x * 0) = 0. (x + 0) + 0 = x. 0 + 0 = 0 * x. 0 * x = 0 + 0. 0 + 0 = x * 0. x * 0 = 0 + 0. x = x + (0 + 0). x + (0 + 0) = x. x + (0 * y) = x. x + (y * 0) = x. -x + x = y * 0. x * 0 = -y + y. x + (-y + y) = x. (x + -y) + y = x. -x + (y + x) = y. end_of_list.