diff options
| author |  Stephane Glondu <steph@glondu.net> | 2012-01-12 16:04:54 +0100 |
|---|---|---|
| committer | Stephane Glondu <steph@glondu.net> | 2012-01-12 16:04:54 +0100 |
| commit | 39efc41237ec906226a3a53d7396d51173495204 (patch) | |
| tree | 87cd58d72d43469d2a2a0a127c1060d7c9e0206b /test-suite/output/Search.out | |
| parent | 5fe4ac437bed43547b3695664974f492b55cb553 (diff) | |
| parent | 97fefe1fcca363a1317e066e7f4b99b9c1e9987b (diff) | |
Remove non-DFSG contentsupstream/8.4_beta+dfsg
Diffstat (limited to 'test-suite/output/Search.out')
| -rw-r--r-- | test-suite/output/Search.out | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/test-suite/output/Search.out b/test-suite/output/Search.out index 154d9cdd..5d8f98ed 100644 --- a/test-suite/output/Search.out +++ b/test-suite/output/Search.out @@ -1,5 +1,7 @@ le_S: forall n m : nat, n <= m -> n <= S m le_n: forall n : nat, n <= n +le_pred: forall n m : nat, n <= m -> pred n <= pred m +le_S_n: forall n m : nat, S n <= S m -> n <= m false: bool true: bool xorb: bool -> bool -> bool @@ -14,5 +16,9 @@ plus_Sn_m: forall n m : nat, S n + m = S (n + m) plus_O_n: forall n : nat, 0 + n = n mult_n_Sm: forall n m : nat, n * m + n = n * S m mult_n_O: forall n : nat, 0 = n * 0 +min_r: forall n m : nat, m <= n -> min n m = m +min_l: forall n m : nat, n <= m -> min n m = n +max_r: forall n m : nat, n <= m -> max n m = m +max_l: forall n m : nat, m <= n -> max n m = n eq_add_S: forall n m : nat, S n = S m -> n = m eq_S: forall x y : nat, x = y -> S x = S y |