diff options
Diffstat (limited to 'test-suite/output/Naming.out')
| -rw-r--r-- | test-suite/output/Naming.out | 40 |
1 files changed, 20 insertions, 20 deletions
diff --git a/test-suite/output/Naming.out b/test-suite/output/Naming.out index f0d2562e..c142d28e 100644 --- a/test-suite/output/Naming.out +++ b/test-suite/output/Naming.out @@ -2,40 +2,40 @@ x3 : nat ============================ - forall x x1 x4 x0 : nat, - (forall x2 x5 : nat, x2 + x1 = x4 + x5) -> x + x1 = x4 + x0 + forall x x1 x4 x0 : nat, + (forall x2 x5 : nat, x2 + x1 = x4 + x5) -> x + x1 = x4 + x0 1 subgoal x3, x, x1, x4, x0 : nat H : forall x x3 : nat, x + x1 = x4 + x3 ============================ - x + x1 = x4 + x0 + 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) + 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 + 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, 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 + (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, x, x1, x4, x0 : nat @@ -44,7 +44,7 @@ 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 + forall x5 x6 x7 S : nat, x5 + S = x6 + x7 + Datatypes.S x 1 subgoal x3, x, x1, x4, x0 : nat @@ -54,10 +54,10 @@ H0 : x + x1 = x4 + x0 x5, x6, x7, S : nat ============================ - x5 + S = x6 + x7 + Datatypes.S x + x5 + S = x6 + x7 + Datatypes.S x 1 subgoal x3, a : nat H : a = 0 -> forall a : nat, a = 0 ============================ - a = 0 + a = 0 |