diff options
| author |  Stephane Glondu <steph@glondu.net> | 2010-07-21 09:46:51 +0200 |
|---|---|---|
| committer | Stephane Glondu <steph@glondu.net> | 2010-07-21 09:46:51 +0200 |
| commit | 5b7eafd0f00a16d78f99a27f5c7d5a0de77dc7e6 (patch) | |
| tree | 631ad791a7685edafeb1fb2e8faeedc8379318ae /test-suite/output/Naming.out | |
| parent | da178a880e3ace820b41d38b191d3785b82991f5 (diff) | |
Imported Upstream snapshot 8.3~beta0+13298
Diffstat (limited to 'test-suite/output/Naming.out')
| -rw-r--r-- | test-suite/output/Naming.out | 83 |
1 files changed, 83 insertions, 0 deletions
diff --git a/test-suite/output/Naming.out b/test-suite/output/Naming.out new file mode 100644 index 00000000..105940a4 --- /dev/null +++ b/test-suite/output/Naming.out @@ -0,0 +1,83 @@ +1 subgoal + + x3 : nat + ============================ + forall x x1 x4 x0 : nat, + (forall x2 x5 : nat, x2 + x1 = x4 + x5) -> x + x1 = x4 + x0 +1 subgoal + + x3 : nat + x : nat + x1 : nat + x4 : nat + x0 : nat + H : forall x x3 : nat, x + x1 = x4 + x3 + ============================ + x + x1 = x4 + x0 +1 subgoal + + x3 : nat + ============================ + forall x x1 x4 x0 : nat, + (forall x2 x5 : nat, x2 + x1 = x4 + x5 -> foo (S x2 + x1)) -> + x + x1 = x4 + x0 -> foo (S x) +1 subgoal + + x3 : nat + ============================ + forall x x1 x4 x0 : nat, + (forall x2 x5 : nat, + x2 + x1 = x4 + x5 -> + forall x6 x7 x8 S0 : nat, x6 + S0 = x7 + x8 + (S x2 + x1)) -> + x + x1 = x4 + x0 -> + forall x5 x6 x7 S : nat, x5 + S = x6 + x7 + Datatypes.S x +1 subgoal + + x3 : nat + x : nat + x1 : nat + x4 : nat + x0 : nat + ============================ + (forall x2 x5 : nat, + x2 + x1 = x4 + x5 -> + forall x6 x7 x8 S0 : nat, x6 + S0 = x7 + x8 + (S x2 + x1)) -> + x + x1 = x4 + x0 -> + forall x5 x6 x7 S : nat, x5 + S = x6 + x7 + Datatypes.S x +1 subgoal + + x3 : nat + x : nat + x1 : nat + x4 : nat + x0 : nat + H : forall x x3 : nat, + x + x1 = x4 + x3 -> + forall x0 x4 x5 S0 : nat, x0 + S0 = x4 + x5 + (S x + x1) + H0 : x + x1 = x4 + x0 + ============================ + forall x5 x6 x7 S : nat, x5 + S = x6 + x7 + Datatypes.S x +1 subgoal + + x3 : nat + x : nat + x1 : nat + x4 : nat + x0 : nat + H : forall x x3 : nat, + x + x1 = x4 + x3 -> + forall x0 x4 x5 S0 : nat, x0 + S0 = x4 + x5 + (S x + x1) + H0 : x + x1 = x4 + x0 + x5 : nat + x6 : nat + x7 : nat + S : nat + ============================ + x5 + S = x6 + x7 + Datatypes.S x +1 subgoal + + x3 : nat + a : nat + H : a = 0 -> forall a : nat, a = 0 + ============================ + a = 0 |