b introduce_premises
(* print goal with premisses introduced *)
b cut "He" "exists x: int. x = x"
(* print goal with h in context *)
b exists "5"
(* print new goal G1 with (x = (2 * 5)) *)
b case "exists x. exists y. x + y = y - x"
(* print the goal with the hypothesis in context *)
pg
(* return to context with positive exists *)
b cut "H" "exists x. exists y. x + y = 0"
ng
(* Have to prove h1 with 2 exists *)
b exists "4"
(* Instantiate x1 *)
b cut "H" "forall x. forall y. x + y = 0"
(* print with h2 in context *)
b instantiate "h2" "4"
(* create h21 which is correct *)
b exists "3"
(* instantiate y in the goal *)
b cut "forall y. true -> 4 + y = 0"
(* generate h3 *)
b apply h2
(* apply h2 to the goal and generate the new goal*)
gu
(* go back to the 4 + 3 = 0 goal *)
b cut "forall y. y = 5 -> 4 + y = 0"
(* new hypothesis to apply *)
b apply h3
(* apply hypothesis and generate the goal 3 = 5 which is correct. *)
b remove h2
(* remove correct hypothesis h2 *)
b remove CompatOrderMult
(* Success *)