test_argument.whyitp 1015 Bytes
Newer Older
1 2
b introduce_premises
(* print goal with premisses introduced *)
3
b cut "exists x: int. x = x"
4 5 6
(* print goal with h in context *)
b exists "5"
(* print new goal G1 with (x = (2 * 5)) *)
7
b case "exists x. exists y. x + y = y - x" "h10"
8 9 10
(* print the goal with the hypothesis in context *)
pg
(* return to context with positive exists *)
11
b cut "exists x. exists y. x + y = 0" "he"
12 13 14 15
ng
(* Have to prove h1 with 2 exists *)
b exists "4"
(* Instantiate x1 *)
16
b cut "forall x. forall y. x + y = 0" "hf"
17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35
(* 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 *)