%%%
%%% All valid results are provable by ASSERT
%%%

decisions: THEORY
 BEGIN

 x,y,v: VAR real
 f: [real -> real]

eq1: THEOREM x = f(x) IMPLIES f(f(f(x))) = x

 g: [real, real -> real]

eq2: THEOREM x = f(y) IMPLIES g(f(y + 2 - 2), x + 2) = g(x, f(y) + 2)

fact3: THEOREM x < 2*y AND y < 3*v IMPLIES 3*x < 18*v

flaw4: CONJECTURE x < 2*y AND y < 3*v IMPLIES 3*x < 17*v

fact5: CONJECTURE x < 0 and y < 0 IMPLIES x * y > 0

i, j, k: VAR int

fact6: THEOREM 2*i < 5 and i > 1 IMPLIES i = 2

flaw7: CONJECTURE 2*x < 5 AND x > 1 IMPLIES x = 2

fact7: CONJECTURE i > 0 and i < 3 IMPLIES i = 1 OR i = 2

END decisions