% ----------------------------------------------------------------------- % Theorem 2, part (1). % ----------------------------------------------------------------------- assign(order,kbo). set(lex_order_vars). clear(back_demod). set(restrict_denials). set(para_from_small). set(para_units_only). formulas(assumptions). % assumption (x * y) * x = y. % ---------- % gL Clauses % ---------- z * x0 != z * y0 | w * x0 = w * y0 # label("gL"). (z * x0) * x1 != (z * y0) * y1 | (w * x0) * x1 = (w * y0) * y1 # label("gL"). x0 * (z * x1) != y0 * (z * y1) | x0 * (w * x1) = y0 * (w * y1) # label("gL"). x0 * z != y0 * z | x0 * w = y0 * w # label("gL"). (x0 * z) * x1 != (y0 * z) * y1 | (x0 * w) * x1 = (y0 * w) * y1 # label("gL"). x0 * (x1 * z) != y0 * (y1 * z) | x0 * (x1 * w) = y0 * (y1 * w) # label("gL"). end_of_list. formulas(goals). % Medial Law (x * y) * (z * u) = (x * z) * (y * u). end_of_list.