diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-05-04 13:30:00 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-05-04 13:33:08 +0200 |
| commit | a6de02fcfde76f49b10d8481a2423692fa105756 (patch) | |
| tree | 344a2e7114b8cb9cc0e54d8d801b4f7cdf5d6d7b /test-suite/output/Naming.out | |
| parent | c81228e693dea839f648ddc95f7cedec22d6a47a (diff) | |
| parent | 174fd1f853f47d24b350a53e7f186ab37829dc2a (diff) | |
Merge branch 'v8.5'
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 f0d2562e0..c142d28eb 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 |