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 x + y = y + x. end_of_list. formulas(goals). d(x,y) = 1 # label("nearfield"). end_of_list. formulas(hints). -x + x = 0. --x + y = x + y. -(x * y) + (x * (y + z)) = x * z. --(x + y) + (-x + (-y + z)) = d(-x,-y) * z. -(x + y) + (y + (x + z)) = d(y,x) * z. 0 = x + -x. x + -x = 0. -(x + y) + (x + 0) = d(x,y) * -y. d(x,y) * -y = -(x + y) + (x + 0). x + 0 = --x. --x = x + 0. x + (-x + y) = y. --x = x. x + -(x + y) = -y. (x + y) + (d(x,y) * z) = x + (y + z). x + (y + -x) = y. -(x * y) + (x * y) = x * 0. -(x * y) + (x * 0) = x * -y. x * 0 = 0. -(x * y) + 0 = x * -y. x * -y = -(x * y). -(x * y) = x * -y. d(x,y) * -y = -(x + y) + x. d(x,y) * -y = x + -(x + y). d(x,y) * -y = -y. --x = d(y,x) * --x. d(x,y) * --y = --y. d(x,y) * --y = y. d(x,y) * y = y. 1 = d(x,1). d(x,1) = 1. (x + y) + (d(y,x) * z) = y + (x + z). (x + 1) + (1 * y) = x + (1 + y). (x + 1) + y = x + (1 + y). x + (1 + y) = y + (x + 1). x + (y + 1) = y + (x + 1). -(x + y) + (y + (x + 1)) = d(y,x). -(x + y) + (x + (y + 1)) = d(y,x). d(x,y) = d(y,x) * 1. d(x,y) * 1 = d(y,x). d(x,y) = d(y,x). (x + y) + (d(x,y) * z) = y + (x + z). x + (y + z) = y + (x + z). d(-x,-y) * z = (x + y) + (-x + (-y + z)). (x + y) + (-x + (-y + z)) = d(-x,-y) * z. (x + y) + (-x + (z + -y)) = d(-x,-y) * z. (-x + y) + (x + (z + -y)) = d(--x,-y) * z. (x + -y) + (y + (z + -x)) = d(--y,-x) * z. (x + -y) + (y + (z + -x)) = d(y,-x) * z. d(x,-y) * z = x + ((y + -x) + (z + -y)). x + ((y + -x) + (z + -y)) = d(x,-y) * z. x + (y + ((z + -x) + -z)) = d(x,-z) * y. x + (y + (-z + (z + -x))) = d(x,-z) * y. x + (y + -x) = d(x,-z) * y. d(x,-y) * z = x + (z + -x). d(x,-y) * z = z. d(x,y) * z = z. 1 = d(x,y). end_of_list.