tests/test_argument.whyitp

   1 ?
   2 t introduce_premises
   3 t cut "forall x. forall y. x = y -> y + x = 0" H2
   4 t cut "5 * (3 + 4) = 0"
   5 ng
   6 t rewrite H2 h
   7 p
   8 t rewrite H G
   9 t replace y 5 G
  10 t replace y 5 G
  11
  12 ng
  13 (* print goal with premisses introduced *)
  14 k
  15 t cut "y = y"
  16 t cut "forall a: int. forall b: int. a = b -> forall c: int. c = a -> c = a * b"
  17 t apply h1
  18 ng
  19 ng
  20
  21 t cut "TOTO = TOTO"
  22 t cut "exists x: int. x = x"
  23 ng
  24 (* print goal with h in context *)
  25 t exists "5"
  26 list-provers
  27 t cut "0=0"
  28 ng
  29 list-provers
  30 p
  31 c Alt-Ergo
  32 c Alt-ergo
  33 c CVC4,1.5-prerelease 10 1100
  34 g
  35 p
  36 t cut "forall x. forall y: int. x = y + x"
  37 ng
  38 p
  39
  40 c CVC4,1.5-prerelease 10 1100
  41 p
  42 c Alt-ergo
  43 (* print new goal G1 with (x = (2 * 5)) *)
  44 t case "exists x. exists y. x + y = y - x" "h10"
  45 (* print the goal with the hypothesis in context *)
  46 pg
  47 (* return to context with positive exists *)
  48 t cut "exists x. exists y. x + y = 0" "he"
  49 ng
  50 (* Have to prove h1 with 2 exists *)
  51 t exists "4"
  52 (* Instantiate x1 *)
  53 t cut "forall x. forall y. x + y = 0" "hf"
  54 (* print with h2 in context *)
  55 t instantiate "h2" "4"
  56 (* create h21 which is correct *)
  57 t exists "3"
  58 (* instantiate y in the goal *)
  59 t cut "forall y. true -> 4 + y = 0"
  60 (* generate h3 *)
  61 t apply h2
  62 (* apply h2 to the goal and generate the new goal*)
  63 gu
  64 (* go back to the 4 + 3 = 0 goal *)
  65 t cut "forall y. y = 5 -> 4 + y = 0"
  66 (* new hypothesis to apply *)
  67 t apply h3
  68 (* apply hypothesis and generate the goal 3 = 5 which is correct. *)
  69 t remove h2
  70 (* remove correct hypothesis h2 *)
  71 t remove CompatOrderMult
  72 (* Success *)