From 9043add656177eeac1491a73d2f3ab92bec0013c Mon Sep 17 00:00:00 2001
From: Benjamin Barenblat <bbaren@debian.org>
Date: Sat, 29 Dec 2018 14:31:27 -0500
Subject: Imported Upstream version 8.8.2

---
 test-suite/output/SearchHead.out | 42 ++++++++++++++++++++--------------------
 1 file changed, 21 insertions(+), 21 deletions(-)

(limited to 'test-suite/output/SearchHead.out')

diff --git a/test-suite/output/SearchHead.out b/test-suite/output/SearchHead.out
index 0d5924ec..7038eac2 100644
--- a/test-suite/output/SearchHead.out
+++ b/test-suite/output/SearchHead.out
@@ -1,39 +1,39 @@
 le_n: forall n : nat, n <= n
+le_0_n: forall n : nat, 0 <= n
 le_S: forall n m : nat, n <= m -> n <= S m
 le_pred: forall n m : nat, n <= m -> Nat.pred n <= Nat.pred m
-le_S_n: forall n m : nat, S n <= S m -> n <= m
-le_0_n: forall n : nat, 0 <= n
 le_n_S: forall n m : nat, n <= m -> S n <= S m
-true: bool
+le_S_n: forall n m : nat, S n <= S m -> n <= m
 false: bool
-andb: bool -> bool -> bool
-orb: bool -> bool -> bool
+true: bool
+negb: bool -> bool
 implb: bool -> bool -> bool
+orb: bool -> bool -> bool
+andb: bool -> bool -> bool
 xorb: bool -> bool -> bool
-negb: bool -> bool
-Nat.eqb: nat -> nat -> bool
-Nat.leb: nat -> nat -> bool
-Nat.ltb: nat -> nat -> bool
 Nat.even: nat -> bool
 Nat.odd: nat -> bool
+Nat.leb: nat -> nat -> bool
+Nat.ltb: nat -> nat -> bool
 Nat.testbit: nat -> nat -> bool
-eq_S: forall x y : nat, x = y -> S x = S y
-f_equal_pred: forall x y : nat, x = y -> Nat.pred x = Nat.pred y
+Nat.eqb: nat -> nat -> bool
+mult_n_O: forall n : nat, 0 = n * 0
+plus_O_n: forall n : nat, 0 + n = n
+plus_n_O: forall n : nat, n = n + 0
 pred_Sn: forall n : nat, n = Nat.pred (S n)
+f_equal_pred: forall x y : nat, x = y -> Nat.pred x = Nat.pred y
 eq_add_S: forall n m : nat, S n = S m -> n = m
-f_equal2_plus:
-  forall x1 y1 x2 y2 : nat, x1 = y1 -> x2 = y2 -> x1 + x2 = y1 + y2
-plus_n_O: forall n : nat, n = n + 0
-plus_O_n: forall n : nat, 0 + n = n
+eq_S: forall x y : nat, x = y -> S x = S y
+max_r: forall n m : nat, n <= m -> Nat.max n m = m
+max_l: forall n m : nat, m <= n -> Nat.max n m = n
+min_r: forall n m : nat, m <= n -> Nat.min n m = m
+min_l: forall n m : nat, n <= m -> Nat.min n m = n
 plus_n_Sm: forall n m : nat, S (n + m) = n + S m
 plus_Sn_m: forall n m : nat, S n + m = S (n + m)
+mult_n_Sm: forall n m : nat, n * m + n = n * S m
+f_equal2_plus:
+  forall x1 y1 x2 y2 : nat, x1 = y1 -> x2 = y2 -> x1 + x2 = y1 + y2
 f_equal2_mult:
   forall x1 y1 x2 y2 : nat, x1 = y1 -> x2 = y2 -> x1 * x2 = y1 * y2
-mult_n_O: forall n : nat, 0 = n * 0
-mult_n_Sm: forall n m : nat, n * m + n = n * S m
-max_l: forall n m : nat, m <= n -> Nat.max n m = n
-max_r: forall n m : nat, n <= m -> Nat.max n m = m
-min_l: forall n m : nat, n <= m -> Nat.min n m = n
-min_r: forall n m : nat, m <= n -> Nat.min n m = m
 h: newdef n
 h: P n
-- 
cgit v1.2.3