diff options
Diffstat (limited to 'test-suite/output/Search.out')
-rw-r--r-- | test-suite/output/Search.out | 116 |
1 files changed, 100 insertions, 16 deletions
diff --git a/test-suite/output/Search.out b/test-suite/output/Search.out index 5d8f98ed..c17b285b 100644 --- a/test-suite/output/Search.out +++ b/test-suite/output/Search.out @@ -1,24 +1,108 @@ -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: forall n m : nat, n <= m -> n <= S m +le_ind: + forall (n : nat) (P : nat -> Prop), + P n -> + (forall m : nat, n <= m -> P m -> P (S m)) -> + forall n0 : nat, n <= n0 -> P n0 +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 -false: bool +le_0_n: forall n : nat, 0 <= n +le_n_S: forall n m : nat, n <= m -> S 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 true: bool -xorb: bool -> bool -> bool +false: bool +bool_rect: forall P : bool -> Type, P true -> P false -> forall b : bool, P b +bool_ind: forall P : bool -> Prop, P true -> P false -> forall b : bool, P b +bool_rec: forall P : bool -> Set, P true -> P false -> forall b : bool, P b +andb: bool -> bool -> bool orb: bool -> bool -> bool -negb: bool -> bool implb: bool -> bool -> bool -andb: bool -> bool -> bool -pred_Sn: forall n : nat, n = pred (S n) -plus_n_Sm: forall n m : nat, S (n + m) = n + S m +xorb: bool -> bool -> bool +negb: bool -> bool +andb_prop: forall a b : bool, (a && b)%bool = true -> a = true /\ b = true +andb_true_intro: + forall b1 b2 : bool, b1 = true /\ b2 = true -> (b1 && b2)%bool = true +eq_true: bool -> Prop +eq_true_rect: + forall P : bool -> Type, P true -> forall b : bool, eq_true b -> P b +eq_true_ind: + forall P : bool -> Prop, P true -> forall b : bool, eq_true b -> P b +eq_true_rec: + forall P : bool -> Set, P true -> forall b : bool, eq_true b -> P b +is_true: bool -> Prop +eq_true_ind_r: + forall (P : bool -> Prop) (b : bool), P b -> eq_true b -> P true +eq_true_rec_r: + forall (P : bool -> Set) (b : bool), P b -> eq_true b -> P true +eq_true_rect_r: + forall (P : bool -> Type) (b : bool), P b -> eq_true b -> P true +BoolSpec: Prop -> Prop -> bool -> Prop +BoolSpec_ind: + forall (P Q : Prop) (P0 : bool -> Prop), + (P -> P0 true) -> + (Q -> P0 false) -> forall b : bool, BoolSpec P Q b -> P0 b +Nat.eqb: nat -> nat -> bool +Nat.leb: nat -> nat -> bool +Nat.ltb: nat -> nat -> bool +Nat.even: nat -> bool +Nat.odd: nat -> bool +Nat.testbit: nat -> nat -> bool +Nat.bitwise: (bool -> bool -> bool) -> nat -> nat -> nat -> nat +bool_choice: + forall (S : Set) (R1 R2 : S -> Prop), + (forall x : S, {R1 x} + {R2 x}) -> + {f : S -> bool | forall x : S, f x = true /\ R1 x \/ f x = false /\ R2 x} +eq_S: forall x y : nat, x = y -> S x = S y +f_equal_nat: forall (B : Type) (f : nat -> B) (x y : nat), x = y -> f x = f y +f_equal_pred: forall x y : nat, x = y -> Nat.pred x = Nat.pred y +pred_Sn: forall n : nat, n = Nat.pred (S n) +eq_add_S: forall n m : nat, S n = S m -> n = m +not_eq_S: forall n m : nat, n <> m -> S n <> S m +O_S: forall n : nat, 0 <> S n +n_Sn: forall n : nat, n <> S n +f_equal2_plus: + forall x1 y1 x2 y2 : nat, x1 = y1 -> x2 = y2 -> x1 + x2 = y1 + y2 +f_equal2_nat: + forall (B : Type) (f : nat -> nat -> B) (x1 y1 x2 y2 : nat), + x1 = y1 -> x2 = y2 -> f x1 x2 = f y1 y2 plus_n_O: forall n : nat, n = n + 0 -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 +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) +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 -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 +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 +andb_prop: forall a b : bool, (a && b)%bool = true -> a = true /\ b = true +andb_true_intro: + forall b1 b2 : bool, b1 = true /\ b2 = true -> (b1 && b2)%bool = true +bool_choice: + forall (S : Set) (R1 R2 : S -> Prop), + (forall x : S, {R1 x} + {R2 x}) -> + {f : S -> bool | forall x : S, f x = true /\ R1 x \/ f x = false /\ R2 x} +andb_prop: forall a b : bool, (a && b)%bool = true -> a = true /\ b = true +andb_true_intro: + forall b1 b2 : bool, b1 = true /\ b2 = true -> (b1 && b2)%bool = true +andb_prop: forall a b : bool, (a && b)%bool = true -> a = true /\ b = true +h': newdef n <> n +h: n <> newdef n +h': newdef n <> n +h: n <> newdef n +h: n <> newdef n +h: n <> newdef n +h': ~ P n +h: P n +h': ~ P n +h: P n +h': ~ P n +h: P n +h: P n +h: P n |