From 97fefe1fcca363a1317e066e7f4b99b9c1e9987b Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Thu, 12 Jan 2012 16:02:20 +0100 Subject: Imported Upstream version 8.4~beta --- test-suite/output/Search.out | 6 ++++++ 1 file changed, 6 insertions(+) (limited to 'test-suite/output/Search.out') 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 -- cgit v1.2.3