Results for fold 1 Results for lemma partition_aux_spec: s f acc1 acc2 : partition_aux f s acc1 acc2 = (filter_aux f s acc1, filter_aux (fun x => negb (f x)) s acc2) FAILURE! Tactics applied: 10000 Original Proof: [revert acc1 acc2. induction s as [ | c l Hl x r Hr ]; simpl. - trivial. - intros acc1 acc2. destruct (f x); simpl; now rewrite Hr, Hl.] Proof search time: 0 min, 39 sec Number of successful tactic applications: 1625 Number of failed tactic applications: 8376 Results for lemma treeify_zero_rb: : treeify_rb_invariant 0 0 treeify_zero SUCCESS! Proof Found in EFSM: intro. inA. Tactics applied: 362 Original Proof: [intros acc _; simpl; auto.] Shorter Proof Found? yes This is a novel proof proof search time: 0 min, 16 sec Number of successful tactic applications: 58 Number of failed tactic applications: 304 Results for lemma rbal_spec: l x r y : InT y (rbal l x r) <-> X.eq y x \/ InT y l \/ InT y r FAILURE! Tactics applied: 10000 Original Proof: [case rbal_match; intuition_in.] Proof search time: 0 min, 36 sec Number of successful tactic applications: 1616 Number of failed tactic applications: 8385 Results for lemma diff_spec: s1 s2 y `{Ok s1, Ok s2} : InT y (diff s1 s2) <-> InT y s1 /\ ~InT y s2 FAILURE! Tactics applied: 10000 Original Proof: [unfold diff. destruct compare_height. - now apply linear_diff_spec. - rewrite filter_spec, Bool.negb_true_iff, <- Bool.not_true_iff_false, mem_spec; intuition. intros x1 x2 EQ. f_equal. now apply mem_proper. - now apply fold_remove_spec.] Proof search time: 0 min, 37 sec Number of successful tactic applications: 1607 Number of failed tactic applications: 8394 Results for lemma ins_arb: x s n : rbt n s -> arbt n (ins x s) FAILURE! Tactics applied: 10000 Original Proof: [intros H. apply (ins_rr_rb x), ifred_or in H. intuition.] Proof search time: 0 min, 35 sec Number of successful tactic applications: 1770 Number of failed tactic applications: 8231 Results for lemma add_spec: s x y `{Ok s} : InT y (add x s) <-> X.eq y x \/ InT y s SUCCESS! Proof Found in EFSM: unfold elt in *. now autorew. Tactics applied: 116 Original Proof: [apply add_spec'.] Shorter Proof Found? no This is a novel proof proof search time: 0 min, 16 sec Number of successful tactic applications: 14 Number of failed tactic applications: 102 Results for lemma ifred_or: s A B : ifred s A B -> A\/B FAILURE! Tactics applied: 10000 Original Proof: [destruct s; descolor; simpl; intuition.] Proof search time: 0 min, 29 sec Number of successful tactic applications: 1358 Number of failed tactic applications: 8643 Results for lemma plength_aux_spec: l p : Pos.to_nat (plength_aux l p) = length l + Pos.to_nat p FAILURE! Tactics applied: 10000 Original Proof: [revert p. induction l; simpl; trivial. intros. now rewrite IHl, Pos2Nat.inj_succ, Nat.add_succ_r.] Proof search time: 0 min, 32 sec Number of successful tactic applications: 1128 Number of failed tactic applications: 8873 Results for lemma singleton_rb: x : Rbt (singleton x) FAILURE! Tactics applied: 10000 Original Proof: [unfold singleton. exists 1; auto.] Proof search time: 0 min, 31 sec Number of successful tactic applications: 1140 Number of failed tactic applications: 8861 Results for lemma diff_list_ok: l1 l2 acc : INV l1 l2 acc -> sort X.lt (diff_list l1 l2 acc) FAILURE! Tactics applied: 10000 Original Proof: [revert l2 acc. induction l1 as [|x1 l1 IH1]; [intro l2|induction l2 as [|x2 l2 IH2]]; intros acc inv. - eauto. - unfold diff_list. eapply INV_rev; eauto. - simpl. case X.compare_spec; intro C. * apply IH1. eapply INV_drop, INV_sym, INV_drop, INV_sym; eauto. * apply (IH2 acc). eapply INV_sym, INV_drop, INV_sym; eauto. * apply IH1. eapply INV_sym, INV_lt; eauto. now apply INV_sym.] Proof search time: 0 min, 30 sec Number of successful tactic applications: 1396 Number of failed tactic applications: 8605 Results for lemma linear_inter_spec: s1 s2 x `(Ok s1, Ok s2) : InT x (linear_inter s1 s2) <-> InT x s1 /\ InT x s2 FAILURE! Tactics applied: 10000 Original Proof: [unfold linear_inter. rewrite !rev_elements_rev, treeify_spec, inter_list_spec by (rewrite rev_involutive; auto_tc). rewrite !InA_rev, InA_nil, !elements_spec1 by auto_tc. tauto.] Proof search time: 0 min, 36 sec Number of successful tactic applications: 1568 Number of failed tactic applications: 8433 Results for lemma treeify_elements: l : elements (treeify l) = l FAILURE! Tactics applied: 10000 Original Proof: [assert (H := treeify_aux_spec (plength l) true l). unfold treeify. destruct treeify_aux as (t,acc); simpl in *. destruct H as (H,H'). { now rewrite plength_spec. } subst l. rewrite plength_spec, app_length, <- elements_cardinal in *. destruct acc. * now rewrite app_nil_r. * exfalso. revert H. simpl. rewrite Nat.add_succ_r, Nat.add_comm. apply Nat.succ_add_discr.] Proof search time: 0 min, 30 sec Number of successful tactic applications: 1129 Number of failed tactic applications: 8872 Results for lemma partition_spec: s f : partition f s = (filter f s, filter (fun x => negb (f x)) s) FAILURE! Tactics applied: 10000 Original Proof: [unfold partition, filter. now rewrite partition_aux_spec.] Proof search time: 0 min, 36 sec Number of successful tactic applications: 1520 Number of failed tactic applications: 8481 Results for lemma diff_rb: s1 s2 : Rbt s1 -> Rbt s2 -> Rbt (diff s1 s2) FAILURE! Tactics applied: 10000 Original Proof: [intros. unfold diff, linear_diff. destruct compare_height; auto_tc.] Proof search time: 0 min, 30 sec Number of successful tactic applications: 1722 Number of failed tactic applications: 8279 Results for lemma union_list_ok: l1 l2 acc : INV l1 l2 acc -> sort X.lt (union_list l1 l2 acc) FAILURE! Tactics applied: 10000 Original Proof: [revert l2 acc. induction l1 as [|x1 l1 IH1]; [intro l2|induction l2 as [|x2 l2 IH2]]; intros acc inv. - eapply INV_rev, INV_sym; eauto. - eapply INV_rev; eauto. - simpl. case X.compare_spec; intro C. * apply IH1. eapply INV_eq; eauto. * apply (IH2 (x2::acc)). eapply INV_lt; eauto. * apply IH1. eapply INV_sym, INV_lt; eauto. now apply INV_sym.] Proof search time: 0 min, 29 sec Number of successful tactic applications: 1345 Number of failed tactic applications: 8656 Results for lemma INV_init: s1 s2 `(Ok s1, Ok s2) : INV (rev_elements s1) (rev_elements s2) nil FAILURE! Tactics applied: 10000 Original Proof: [rewrite !rev_elements_rev. split; rewrite ?rev_involutive; auto; intros; now inA.] Proof search time: 0 min, 33 sec Number of successful tactic applications: 1386 Number of failed tactic applications: 8615 Results for lemma rbalS_rb: n l x r : rbt (S n) l -> notred l -> arbt n r -> rbt (S n) (rbalS l x r) FAILURE! Tactics applied: 10000 Original Proof: [intros Hl Hl' Hr. destruct l as [|[|] ll lx lr]; invrb. clear Hl'. revert Hr. case rbalS_match. - destruct 1; invrb; auto. - intros. apply lbal_rb; auto.] Proof search time: 0 min, 45 sec Number of successful tactic applications: 2834 Number of failed tactic applications: 7167 Results for lemma inter_spec: s1 s2 y `{Ok s1, Ok s2} : InT y (inter s1 s2) <-> InT y s1 /\ InT y s2 FAILURE! Tactics applied: 10000 Original Proof: [unfold inter. destruct compare_height. - now apply linear_inter_spec. - rewrite filter_spec, mem_spec by auto_tc; tauto. - rewrite filter_spec, mem_spec by auto_tc; tauto.] Proof search time: 0 min, 36 sec Number of successful tactic applications: 1574 Number of failed tactic applications: 8427 Results for lemma rb_maxdepth: s n : rbt n s -> maxdepth s <= 2*n + redcarac s FAILURE! Tactics applied: 10000 Original Proof: [induction 1. - simpl; auto. - replace (redcarac l) with 0 in * by now destree l. replace (redcarac r) with 0 in * by now destree r. simpl maxdepth. simpl redcarac. rewrite Nat.add_succ_r, <- Nat.succ_le_mono. now apply Nat.max_lub. - simpl. rewrite <- Nat.succ_le_mono. apply Nat.max_lub; eapply Nat.le_trans; eauto; [destree l | destree r]; simpl; rewrite !Nat.add_0_r, ?Nat.add_1_r; auto with arith.] Proof search time: 0 min, 33 sec Number of successful tactic applications: 1896 Number of failed tactic applications: 8105 Results for lemma append_spec: l r x : InT x (append l r) <-> InT x l \/ InT x r FAILURE! Tactics applied: 10000 Original Proof: [revert r. append_tac l r; autorew; try tauto. - revert IHlr; case append_rr_match; [intros a y b | intros t Ht]; autorew; tauto. - revert IHlr; case append_bb_match; [intros a y b | intros t Ht]; autorew; tauto.] Proof search time: 0 min, 42 sec Number of successful tactic applications: 2079 Number of failed tactic applications: 7922 Results for lemma add_spec': s x y : InT y (add x s) <-> X.eq y x \/ InT y s FAILURE! Tactics applied: 10000 Original Proof: [unfold add. now autorew.] Proof search time: 0 min, 37 sec Number of successful tactic applications: 1541 Number of failed tactic applications: 8460 Results for lemma remove_min_spec1: s x s' : remove_min s = Some (x,s') -> min_elt s = Some x /\ Equal (remove x s) s' FAILURE! Tactics applied: 10000 Original Proof: [destruct s as (s,Hs). unfold remove_min, mk_opt_t, min_elt, remove, Equal, In; simpl. generalize (fun x s' => @Raw.remove_min_spec1 s x s' Hs). set (P := Raw.remove_min_ok s). clearbody P. destruct (Raw.remove_min s) as [(x0,s0)|]; try easy. intros H U. injection U. clear U; intros; subst. simpl. destruct (H x s0); auto. subst; intuition.] Proof search time: 0 min, 27 sec Number of successful tactic applications: 847 Number of failed tactic applications: 9154 Results for lemma rbal_rb: n l k r : rbt n l -> arbt n r -> rbt (S n) (rbal l k r) FAILURE! Tactics applied: 10000 Original Proof: [case rbal_match; intros; desarb; invrb; auto.] Proof search time: 0 min, 44 sec Number of successful tactic applications: 2478 Number of failed tactic applications: 7523 Results for lemma treeify_cont_spec: f g size1 size2 size : treeify_invariant size1 f -> treeify_invariant size2 g -> size = S (size1 + size2) -> treeify_invariant size (treeify_cont f g) FAILURE! Tactics applied: 10000 Original Proof: [intros Hf Hg EQ acc LE. unfold treeify_cont. specialize (Hf acc). destruct (f acc) as (t1,acc1). destruct Hf as (Hf1,Hf2). { transitivity size; trivial. subst. auto with arith. } destruct acc1 as [|x acc1]. { exfalso. revert LE. apply Nat.lt_nge. subst. rewrite <- app_nil_end, <- elements_cardinal; auto with arith. } specialize (Hg acc1). destruct (g acc1) as (t2,acc2). destruct Hg as (Hg1,Hg2). { revert LE. subst. rewrite app_length, <- elements_cardinal. simpl. rewrite Nat.add_succ_r, <- Nat.succ_le_mono. apply Nat.add_le_mono_l. } simpl. rewrite elements_node, app_ass. now subst.] Proof search time: 0 min, 29 sec Number of successful tactic applications: 1483 Number of failed tactic applications: 8518 Results for lemma rbal'_rb: n l k r : rbt n l -> arbt n r -> rbt (S n) (rbal' l k r) FAILURE! Tactics applied: 10000 Original Proof: [case rbal'_match; intros; desarb; invrb; auto.] Proof search time: 0 min, 52 sec Number of successful tactic applications: 2700 Number of failed tactic applications: 7301 Results for lemma arb_nrr_rb: n t : arbt n t -> notredred t -> rbt n t SUCCESS! Proof Found in EFSM: destruct 1; auto. Tactics applied: 464 Original Proof: [destruct 1; auto.] Shorter Proof Found? no This is a novel proof proof search time: 0 min, 16 sec Number of successful tactic applications: 65 Number of failed tactic applications: 399 Results for lemma singleton_spec: x y : InT y (singleton x) <-> X.eq y x FAILURE! Tactics applied: 10000 Original Proof: [unfold singleton; intuition_in.] Proof search time: 0 min, 29 sec Number of successful tactic applications: 908 Number of failed tactic applications: 9093 Results for lemma treeify_aux_spec: n (p:bool) : treeify_invariant (ifpred p (Pos.to_nat n)) (treeify_aux p n) FAILURE! Tactics applied: 10000 Original Proof: [revert p. induction n as [n|n|]; intros p; simpl treeify_aux. - eapply treeify_cont_spec; [ apply (IHn false) | apply (IHn p) | ]. rewrite Pos2Nat.inj_xI. assert (H := Pos2Nat.is_pos n). apply Nat.neq_0_lt_0 in H. destruct p; simpl; intros; rewrite Nat.add_0_r; trivial. now rewrite <- Nat.add_succ_r, Nat.succ_pred; trivial. - eapply treeify_cont_spec; [ apply (IHn p) | apply (IHn true) | ]. rewrite Pos2Nat.inj_xO. assert (H := Pos2Nat.is_pos n). apply Nat.neq_0_lt_0 in H. rewrite <- Nat.add_succ_r, Nat.succ_pred by trivial. destruct p; simpl; intros; rewrite Nat.add_0_r; trivial. symmetry. now apply Nat.add_pred_l. - destruct p; [ apply treeify_zero_spec | apply treeify_one_spec ].] Proof search time: 0 min, 30 sec Number of successful tactic applications: 1264 Number of failed tactic applications: 8737 Results for lemma maxdepth_upperbound: s : Rbt s -> maxdepth s <= 2 * log2 (S (cardinal s)) FAILURE! Tactics applied: 10000 Original Proof: [intros (n,H). eapply Nat.le_trans; [eapply rb_maxdepth; eauto|]. transitivity (2*(n+redcarac s)). - rewrite Nat.mul_add_distr_l. apply Nat.add_le_mono_l. rewrite <- Nat.mul_1_l at 1. apply Nat.mul_le_mono_r. auto with arith. - apply Nat.mul_le_mono_l. transitivity (mindepth s). + now apply rb_mindepth. + apply mindepth_log_cardinal.] Proof search time: 0 min, 32 sec Number of successful tactic applications: 1954 Number of failed tactic applications: 8047 Results for lemma ins_spec: : forall s x y, InT y (ins x s) <-> X.eq y x \/ InT y s FAILURE! Tactics applied: 10000 Original Proof: [induct s x. - intuition_in. - intuition_in. setoid_replace y with x; eauto. - descolor; autorew; rewrite IHl; intuition_in. - descolor; autorew; rewrite IHr; intuition_in.] Proof search time: 0 min, 31 sec Number of successful tactic applications: 1514 Number of failed tactic applications: 8487 Results for lemma lbal_rb: n l k r : arbt n l -> rbt n r -> rbt (S n) (lbal l k r) FAILURE! Tactics applied: 10000 Original Proof: [case lbal_match; intros; desarb; invrb; auto.] Proof search time: 0 min, 50 sec Number of successful tactic applications: 2845 Number of failed tactic applications: 7156 Results for lemma treeify_one_rb: : treeify_rb_invariant 1 0 treeify_one FAILURE! Tactics applied: 10000 Original Proof: [intros [|x acc]; simpl; auto; inversion 1.] Proof search time: 0 min, 35 sec Number of successful tactic applications: 1399 Number of failed tactic applications: 8602 Results for lemma filter_app: A f (l l':list A) : List.filter f (l ++ l') = List.filter f l ++ List.filter f l' FAILURE! Tactics applied: 10000 Original Proof: [induction l as [|x l IH]; simpl; trivial. destruct (f x); simpl; now rewrite IH.] Proof search time: 0 min, 32 sec Number of successful tactic applications: 1186 Number of failed tactic applications: 8815 Results for lemma INV_eq: x1 x2 l1 l2 acc : INV (x1 :: l1) (x2 :: l2) acc -> X.eq x1 x2 -> INV l1 l2 (x1 :: acc) FAILURE! Tactics applied: 10000 Original Proof: [intros (U,V,W,X,Y) EQ. simpl in *. destruct (sorted_app_inv _ _ U) as (U1 & U2 & U3); auto. destruct (sorted_app_inv _ _ V) as (V1 & V2 & V3); auto. split; auto. - constructor; auto. apply InA_InfA with X.eq; auto_tc. - intros x y; inA; intros Hx [Hy|Hy]. + apply U3; inA. + apply X; inA. - intros x y; inA; intros Hx [Hy|Hy]. + rewrite Hy, EQ; apply V3; inA. + apply Y; inA.] Proof search time: 0 min, 31 sec Number of successful tactic applications: 1345 Number of failed tactic applications: 8656 Results for lemma inter_list_ok: l1 l2 acc : INV l1 l2 acc -> sort X.lt (inter_list l1 l2 acc) FAILURE! Tactics applied: 10000 Original Proof: [revert l2 acc. induction l1 as [|x1 l1 IH1]; [|induction l2 as [|x2 l2 IH2]]; simpl. - eauto. - eauto. - intros acc inv. case X.compare_spec; intro C. * apply IH1. eapply INV_eq; eauto. * apply (IH2 acc). eapply INV_sym, INV_drop, INV_sym; eauto. * apply IH1. eapply INV_drop; eauto.] Proof search time: 0 min, 29 sec Number of successful tactic applications: 1396 Number of failed tactic applications: 8605 Results for lemma treeify_one_spec: : treeify_invariant 1 treeify_one FAILURE! Tactics applied: 10000 Original Proof: [intros [|x acc]; simpl; auto; inversion 1.] Proof search time: 0 min, 30 sec Number of successful tactic applications: 1120 Number of failed tactic applications: 8881 Results for lemma rbalS_arb: n l x r : rbt (S n) l -> arbt n r -> arbt (S n) (rbalS l x r) FAILURE! Tactics applied: 10000 Original Proof: [case rbalS_match. - destruct 2; invrb; auto. - clear r. intros r Hr Hr' Hl. destruct l as [|[|] ll lx lr]; invrb. * destruct lr as [|[|] lrl lrx lrr]; invrb. right; auto using lbal_rb, makeRed_rr. * left; apply lbal_rb; auto.] Proof search time: 0 min, 45 sec Number of successful tactic applications: 2563 Number of failed tactic applications: 7438 Results for lemma append_ok: : forall x l r `{Ok l, Ok r}, lt_tree x l -> gt_tree x r -> Ok (append l r) FAILURE! Tactics applied: 10000 Original Proof: [append_tac l r. - trivial. - trivial. - intros; inv. assert (IH : Ok (append lr rl)) by (apply IHlr; eauto). clear IHlr. assert (X.lt lx rx) by (transitivity x; eauto). assert (G : gt_tree lx (append lr rl)). { intros w. autorew. destruct 1; [|transitivity x]; eauto. } assert (L : lt_tree rx (append lr rl)). { intros w. autorew. destruct 1; [transitivity x|]; eauto. } revert IH G L; case append_rr_match; intros; ok. - intros; ok. intros w; autorew; destruct 1; eauto. - intros; ok. intros w; autorew; destruct 1; eauto. - intros; inv. assert (IH : Ok (append lr rl)) by (apply IHlr; eauto). clear IHlr. assert (X.lt lx rx) by (transitivity x; eauto). assert (G : gt_tree lx (append lr rl)). { intros w. autorew. destruct 1; [|transitivity x]; eauto. } assert (L : lt_tree rx (append lr rl)). { intros w. autorew. destruct 1; [transitivity x|]; eauto. } revert IH G L; case append_bb_match; intros; ok. apply lbalS_ok; ok.] Proof search time: 0 min, 40 sec Number of successful tactic applications: 2642 Number of failed tactic applications: 7359 Results for lemma partition_spec2: s f : Proper (X.eq==>Logic.eq) f -> Equal (snd (partition f s)) (filter (fun x => negb (f x)) s) FAILURE! Tactics applied: 10000 Original Proof: [now rewrite partition_spec.] Proof search time: 0 min, 32 sec Number of successful tactic applications: 1575 Number of failed tactic applications: 8426 Results for lemma INV_drop: x1 l1 l2 acc : INV (x1 :: l1) l2 acc -> INV l1 l2 acc FAILURE! Tactics applied: 10000 Original Proof: [intros (l1s,l2s,accs,l1a,l2a). simpl in *. destruct (sorted_app_inv _ _ l1s) as (U & V & W); auto. split; auto.] Proof search time: 0 min, 29 sec Number of successful tactic applications: 1088 Number of failed tactic applications: 8913 Results for lemma INV_lt: x1 x2 l1 l2 acc : INV (x1 :: l1) (x2 :: l2) acc -> X.lt x1 x2 -> INV (x1 :: l1) l2 (x2 :: acc) FAILURE! Tactics applied: 10000 Original Proof: [intros (U,V,W,X,Y) EQ. simpl in *. destruct (sorted_app_inv _ _ U) as (U1 & U2 & U3); auto. destruct (sorted_app_inv _ _ V) as (V1 & V2 & V3); auto. split; auto. - constructor; auto. apply InA_InfA with X.eq; auto_tc. - intros x y; inA; intros Hx [Hy|Hy]. + rewrite Hy; clear Hy. destruct Hx; [order|]. transitivity x1; auto. apply U3; inA. + apply X; inA. - intros x y; inA; intros Hx [Hy|Hy]. + rewrite Hy. apply V3; inA. + apply Y; inA.] Proof search time: 0 min, 31 sec Number of successful tactic applications: 1345 Number of failed tactic applications: 8656 Results for lemma partition_spec1: s f : Proper (X.eq==>Logic.eq) f -> Equal (fst (partition f s)) (filter f s) FAILURE! Tactics applied: 10000 Original Proof: [now rewrite partition_spec.] Proof search time: 0 min, 31 sec Number of successful tactic applications: 1520 Number of failed tactic applications: 8481 Results for lemma makeRed_spec: s x : InT x (makeRed s) <-> InT x s SUCCESS! Proof Found in EFSM: induct s x; intuition_in. Tactics applied: 109 Original Proof: [destruct s; simpl; intuition_in.] Shorter Proof Found? yes This is a novel proof proof search time: 0 min, 16 sec Number of successful tactic applications: 10 Number of failed tactic applications: 99 Results for lemma makeBlack_rb: n t : arbt n t -> Rbt (makeBlack t) FAILURE! Tactics applied: 10000 Original Proof: [destruct t as [|[|] l x r]. - exists 0; auto. - destruct 1; invrb; exists (S n); simpl; auto. - exists n; auto.] Proof search time: 0 min, 29 sec Number of successful tactic applications: 1394 Number of failed tactic applications: 8607 Results for lemma makeRed_rr: t n : rbt (S n) t -> notred t -> rrt n (makeRed t) FAILURE! Tactics applied: 10000 Original Proof: [destruct t as [|[|] l x r]; invrb; simpl; auto.] Proof search time: 0 min, 30 sec Number of successful tactic applications: 1598 Number of failed tactic applications: 8403 Results for fold 2 Results for lemma ifred_notred: s A B : notred s -> (ifred s A B <-> B) FAILURE! Tactics applied: 10000 Original Proof: [destruct s; descolor; simpl; intuition.] Proof search time: 0 min, 17 sec Number of successful tactic applications: 1375 Number of failed tactic applications: 8626 Results for lemma INV_sym: l1 l2 acc : INV l1 l2 acc -> INV l2 l1 acc FAILURE! Tactics applied: 10000 Original Proof: [destruct 1; now split.] Proof search time: 0 min, 16 sec Number of successful tactic applications: 1056 Number of failed tactic applications: 8945 Results for lemma remove_min_ok: (s:t) `{Ok s}: match remove_min s with | Some (_,s') => Ok s' | None => True end FAILURE! Tactics applied: 10000 Original Proof: [generalize (remove_min_spec1 s). destruct remove_min as [(x0,s0)|]; auto. intros R. destruct (R x0 s0); auto. subst s0. auto_tc.] Proof search time: 0 min, 19 sec Number of successful tactic applications: 1714 Number of failed tactic applications: 8287 Results for lemma lbalS_rb: n l x r : arbt n l -> rbt (S n) r -> notred r -> rbt (S n) (lbalS l x r) FAILURE! Tactics applied: 10000 Original Proof: [intros Hl Hr Hr'. destruct r as [|[|] rl rx rr]; invrb. clear Hr'. revert Hl. case lbalS_match. - destruct 1; invrb; auto. - intros. apply rbal'_rb; auto.] Proof search time: 0 min, 24 sec Number of successful tactic applications: 1745 Number of failed tactic applications: 8256 Results for lemma union_rb: s1 s2 : Rbt s1 -> Rbt s2 -> Rbt (union s1 s2) FAILURE! Tactics applied: 10000 Original Proof: [intros. unfold union, linear_union. destruct compare_height; auto_tc.] Proof search time: 0 min, 16 sec Number of successful tactic applications: 1167 Number of failed tactic applications: 8834 Results for lemma INV_rev: l1 l2 acc : INV l1 l2 acc -> Sorted X.lt (rev_append l1 acc) FAILURE! Tactics applied: 10000 Original Proof: [intros. rewrite rev_append_rev. apply SortA_app with X.eq; eauto with *. intros x y. inA. eapply l1_lt_acc; eauto.] Proof search time: 0 min, 17 sec Number of successful tactic applications: 1169 Number of failed tactic applications: 8832 Results for lemma union_list_spec: x l1 l2 acc : InA X.eq x (union_list l1 l2 acc) <-> InA X.eq x l1 \/ InA X.eq x l2 \/ InA X.eq x acc FAILURE! Tactics applied: 10000 Original Proof: [revert l2 acc. induction l1 as [|x1 l1 IH1]. - intros l2 acc; simpl. rewrite rev_append_rev. inA. tauto. - induction l2 as [|x2 l2 IH2]; intros acc; simpl. * rewrite rev_append_rev. inA. tauto. * case X.compare_spec; intro C. + rewrite IH1, !InA_cons, C; tauto. + rewrite (IH2 (x2::acc)), !InA_cons. tauto. + rewrite IH1, !InA_cons; tauto.] Proof search time: 0 min, 19 sec Number of successful tactic applications: 1047 Number of failed tactic applications: 8954 Results for lemma delmin_spec: l y r c x s' `{O : Ok (Node c l y r)} : delmin l y r = (x,s') -> min_elt (Node c l y r) = Some x /\ del x (Node c l y r) = s' FAILURE! Tactics applied: 10000 Original Proof: [revert y r c x s' O. induction l as [|lc ll IH ly lr _]. - simpl. intros y r _ x s' _. injection 1; intros; subst. now rewrite MX.compare_refl. - intros y r c x s' O. simpl delmin. specialize (IH ly lr). destruct delmin as (x0,s0). destruct (IH lc x0 s0); clear IH; [ok|trivial|]. remember (Node lc ll ly lr) as l. simpl min_elt in *. intros E. replace x0 with x in * by (destruct lc; now injection E). split. * subst l; intuition. * assert (X.lt x y). { inversion_clear O. assert (InT x l) by now apply min_elt_spec1. auto. } simpl. case X.compare_spec; try order. destruct lc; injection E; clear E; intros; subst l s0; auto.] Proof search time: 0 min, 31 sec Number of successful tactic applications: 1672 Number of failed tactic applications: 8329 Results for lemma fold_add_spec: s1 s2 x : InT x (fold add s1 s2) <-> InT x s1 \/ InT x s2 FAILURE! Tactics applied: 684 Original Proof: [rewrite fold_spec, <- fold_left_rev_right. rewrite <- (elements_spec1 s1), <- InA_rev by auto_tc. unfold elt in *. induction (rev (elements s1)); simpl. - rewrite InA_nil. tauto. - unfold flip. rewrite add_spec', IHl, InA_cons. tauto.] Proof search time: 0 min, 6 sec Number of successful tactic applications: 12 Number of failed tactic applications: 672 Results for lemma fold_remove_spec: s1 s2 x `(Ok s2) : InT x (fold remove s1 s2) <-> InT x s2 /\ ~InT x s1 FAILURE! Tactics applied: 10000 Original Proof: [rewrite fold_spec, <- fold_left_rev_right. rewrite <- (elements_spec1 s1), <- InA_rev by auto_tc. unfold elt in *. induction (rev (elements s1)); simpl; intros. - rewrite InA_nil. intuition. - unfold flip in *. rewrite remove_spec, IHl, InA_cons. tauto. clear IHl. induction l; simpl; auto_tc.] Proof search time: 0 min, 17 sec Number of successful tactic applications: 788 Number of failed tactic applications: 9213 Results for lemma remove_min_spec2: s : remove_min s = None -> Empty s FAILURE! Tactics applied: 10000 Original Proof: [destruct s as (s,Hs). unfold remove_min, mk_opt_t, Empty, In; simpl. generalize (Raw.remove_min_spec2 s). set (P := Raw.remove_min_ok s). clearbody P. destruct (Raw.remove_min s) as [(x0,s0)|]; now intuition.] Proof search time: 0 min, 17 sec Number of successful tactic applications: 1247 Number of failed tactic applications: 8754 Results for lemma filter_aux_elements: s f acc : filter_aux f s acc = List.filter f (elements s) ++ acc FAILURE! Tactics applied: 10000 Original Proof: [revert acc. induction s as [|c l IHl x r IHr]; simpl; trivial. intros acc. rewrite elements_node, filter_app. simpl. destruct (f x); now rewrite IHl, IHr, app_ass.] Proof search time: 0 min, 20 sec Number of successful tactic applications: 1834 Number of failed tactic applications: 8167 Results for lemma plength_spec: l : Pos.to_nat (plength l) = S (length l) FAILURE! Tactics applied: 10000 Original Proof: [unfold plength. rewrite plength_aux_spec. apply Nat.add_1_r.] Proof search time: 0 min, 20 sec Number of successful tactic applications: 2260 Number of failed tactic applications: 7741 Results for lemma del_arb: s x n : rbt (S n) s -> isblack s -> arbt n (del x s) with del_rb s x n : rbt n s -> notblack s -> rbt n (del x s) SUCCESS! Proof Found in EFSM: intuition_in. intuition_in. Tactics applied: 1106 Original Proof: [{ revert n. induct s x; try destruct c; try contradiction; invrb. - apply append_arb_rb; assumption. - assert (IHl' := del_rb l x). clear IHr del_arb del_rb. destruct l as [|[|] ll lx lr]; auto. nonzero n. apply lbalS_arb; auto. - assert (IHr' := del_rb r x). clear IHl del_arb del_rb. destruct r as [|[|] rl rx rr]; auto. nonzero n. apply rbalS_arb; auto. } { revert n. induct s x; try assumption; try destruct c; try contradiction; invrb. - apply append_arb_rb; assumption. - assert (IHl' := del_arb l x). clear IHr del_arb del_rb. destruct l as [|[|] ll lx lr]; auto. nonzero n. destruct n as [|n]; [invrb|]; apply lbalS_rb; auto. - assert (IHr' := del_arb r x). clear IHl del_arb del_rb. destruct r as [|[|] rl rx rr]; auto. nonzero n. apply rbalS_rb; auto. }] Shorter Proof Found? yes This is a novel proof This proof contained a sequence of repeated tactics proof search time: 0 min, 7 sec Number of successful tactic applications: 148 Number of failed tactic applications: 958 Results for lemma filter_spec: s x f : Proper (X.eq==>Logic.eq) f -> (InT x (filter f s) <-> InT x s /\ f x = true) FAILURE! Tactics applied: 10000 Original Proof: [intros Hf. rewrite <- elements_spec1, filter_elements, filter_InA, elements_spec1; now auto_tc.] Proof search time: 0 min, 18 sec Number of successful tactic applications: 898 Number of failed tactic applications: 9103 Results for lemma filter_elements: s f : elements (filter f s) = List.filter f (elements s) FAILURE! Tactics applied: 10000 Original Proof: [unfold filter. now rewrite treeify_elements, filter_aux_elements, app_nil_r.] Proof search time: 0 min, 20 sec Number of successful tactic applications: 1783 Number of failed tactic applications: 8218 Results for lemma treeify_spec: x l : InT x (treeify l) <-> InA X.eq x l FAILURE! Tactics applied: 10000 Original Proof: [intros. now rewrite <- elements_spec1, treeify_elements.] Proof search time: 0 min, 17 sec Number of successful tactic applications: 714 Number of failed tactic applications: 9287 Results for lemma rbalS_spec: l x r y : InT y (rbalS l x r) <-> X.eq y x \/ InT y l \/ InT y r FAILURE! Tactics applied: 10000 Original Proof: [case rbalS_match. - intros; autorew; intuition_in. - intros t _. destruct l as [|[|] ll lx lr]. * autorew. intuition_in. * destruct lr as [|[|] lrl lrx lrr]; autorew; intuition_in. * autorew. intuition_in.] Proof search time: 0 min, 25 sec Number of successful tactic applications: 1222 Number of failed tactic applications: 8779 Results for lemma diff_list_spec: x l1 l2 acc : sort X.lt (rev l1) -> sort X.lt (rev l2) -> (InA X.eq x (diff_list l1 l2 acc) <-> (InA X.eq x l1 /\ ~InA X.eq x l2) \/ InA X.eq x acc) FAILURE! Tactics applied: 10000 Original Proof: [revert l2 acc. induction l1 as [|x1 l1 IH1]. - intros l2 acc; simpl. inA. tauto. - induction l2 as [|x2 l2 IH2]; intros acc. * intros; simpl. rewrite rev_append_rev. inA. tauto. * simpl. intros U V. destruct (sorted_app_inv _ _ U) as (U1 & U2 & U3); auto. destruct (sorted_app_inv _ _ V) as (V1 & V2 & V3); auto. case X.compare_spec; intro C. + rewrite IH1; auto. f_equiv. inA. intuition; try order. assert (X.lt x x1) by (apply U3; inA). order. + rewrite (IH2 acc); auto. f_equiv. inA. intuition; try order. assert (X.lt x x1) by (apply U3; inA). order. + rewrite IH1; auto. inA. intuition; try order. left; split; auto. destruct 1. order. assert (X.lt x x2) by (apply V3; inA). order.] Proof search time: 0 min, 23 sec Number of successful tactic applications: 1349 Number of failed tactic applications: 8652 Results for lemma rbal'_spec: l x r y : InT y (rbal' l x r) <-> X.eq y x \/ InT y l \/ InT y r SUCCESS! Proof Found in EFSM: case rbal'_match; intuition_in. Tactics applied: 224 Original Proof: [case rbal'_match; intuition_in.] Shorter Proof Found? no This is a novel proof proof search time: 0 min, 6 sec Number of successful tactic applications: 36 Number of failed tactic applications: 188 Results for lemma remove_spec: s x y `{Ok s} : InT y (remove x s) <-> InT y s /\ ~X.eq y x FAILURE! Tactics applied: 10000 Original Proof: [unfold remove. now autorew.] Proof search time: 0 min, 18 sec Number of successful tactic applications: 830 Number of failed tactic applications: 9171 Results for lemma treeify_cont_rb: f g size1 size2 size d : treeify_rb_invariant size1 d f -> treeify_rb_invariant size2 d g -> size = S (size1 + size2) -> treeify_rb_invariant size (S d) (treeify_cont f g) FAILURE! Tactics applied: 10000 Original Proof: [intros Hf Hg H acc Hacc. unfold treeify_cont. specialize (Hf acc). destruct (f acc) as (l, acc1). simpl in *. destruct Hf as (Hf1, Hf2). { subst. eauto with arith. } destruct acc1 as [|x acc2]; simpl in *. - exfalso. revert Hacc. apply Nat.lt_nge. rewrite H, <- Hf2. auto with arith. - specialize (Hg acc2). destruct (g acc2) as (r, acc3). simpl in *. destruct Hg as (Hg1, Hg2). { revert Hacc. rewrite H, <- Hf2, Nat.add_succ_r, <- Nat.succ_le_mono. apply Nat.add_le_mono_l. } split; auto. now rewrite H, <- Hf2, <- Hg2, Nat.add_succ_r, Nat.add_assoc.] Proof search time: 0 min, 21 sec Number of successful tactic applications: 1345 Number of failed tactic applications: 8656 Results for lemma remove_min_spec1: s x s' `{Ok s}: remove_min s = Some (x,s') -> min_elt s = Some x /\ remove x s = s' ERROR! Error: Unbound and ungeneralizable variable Ok Original Proof: [destruct s as (s,Hs). unfold remove_min, mk_opt_t, min_elt, remove, Equal, In; simpl. generalize (fun x s' => @Raw.remove_min_spec1 s x s' Hs). set (P := Raw.remove_min_ok s). clearbody P. destruct (Raw.remove_min s) as [(x0,s0)|]; try easy. intros H U. injection U. clear U; intros; subst. simpl. destruct (H x s0); auto. subst; intuition.] Proof effort time: 0 min, 0 sec Results for lemma arb_nr_rb: n t : arbt n t -> notred t -> rbt n t SUCCESS! Proof Found in EFSM: destruct 1; destruct t as [|[|] l x r]; now subst. Tactics applied: 9927 Original Proof: [destruct 1; destruct t; descolor; invrb; auto.] Shorter Proof Found? yes This is a novel proof This proof contained a loop around a state proof search time: 0 min, 18 sec Number of successful tactic applications: 1500 Number of failed tactic applications: 8427 Results for lemma union_spec': s1 s2 x : InT x (union s1 s2) <-> InT x s1 \/ InT x s2 FAILURE! Tactics applied: 267 Original Proof: [unfold union. destruct compare_height. - apply linear_union_spec. - apply fold_add_spec. - rewrite fold_add_spec. tauto.] Proof search time: 0 min, 6 sec Number of successful tactic applications: 2 Number of failed tactic applications: 265 Results for lemma remove_min_spec2: s : remove_min s = None -> Empty s FAILURE! Tactics applied: 10000 Original Proof: [destruct s as (s,Hs). unfold remove_min, mk_opt_t, Empty, In; simpl. generalize (Raw.remove_min_spec2 s). set (P := Raw.remove_min_ok s). clearbody P. destruct (Raw.remove_min s) as [(x0,s0)|]; now intuition.] Proof search time: 0 min, 17 sec Number of successful tactic applications: 1247 Number of failed tactic applications: 8754 Results for lemma makeBlack_spec: s x : InT x (makeBlack s) <-> InT x s SUCCESS! Proof Found in EFSM: destruct s; simpl ; intuition_in. Tactics applied: 1336 Original Proof: [destruct s; simpl; intuition_in.] Shorter Proof Found? no Proof reused from makeRed_spec proof search time: 0 min, 7 sec Number of successful tactic applications: 119 Number of failed tactic applications: 1217 Results for lemma lbalS_spec: l x r y : InT y (lbalS l x r) <-> X.eq y x \/ InT y l \/ InT y r FAILURE! Tactics applied: 10000 Original Proof: [case lbalS_match. - intros; autorew; intuition_in. - clear l. intros l _. destruct r as [|[|] rl rx rr]. * autorew. intuition_in. * destree rl; autorew; intuition_in. * autorew. intuition_in.] Proof search time: 0 min, 25 sec Number of successful tactic applications: 1059 Number of failed tactic applications: 8942 Results for lemma inter_list_spec: x l1 l2 acc : sort X.lt (rev l1) -> sort X.lt (rev l2) -> (InA X.eq x (inter_list l1 l2 acc) <-> (InA X.eq x l1 /\ InA X.eq x l2) \/ InA X.eq x acc) FAILURE! Tactics applied: 10000 Original Proof: [revert l2 acc. induction l1 as [|x1 l1 IH1]. - intros l2 acc; simpl. inA. tauto. - induction l2 as [|x2 l2 IH2]; intros acc. * simpl. inA. tauto. * simpl. intros U V. destruct (sorted_app_inv _ _ U) as (U1 & U2 & U3); auto. destruct (sorted_app_inv _ _ V) as (V1 & V2 & V3); auto. case X.compare_spec; intro C. + rewrite IH1, !InA_cons, C; tauto. + rewrite (IH2 acc); auto. inA. intuition; try order. assert (X.lt x x1) by (apply U3; inA). order. + rewrite IH1; auto. inA. intuition; try order. assert (X.lt x x2) by (apply V3; inA). order.] Proof search time: 0 min, 22 sec Number of successful tactic applications: 1349 Number of failed tactic applications: 8652 Results for lemma treeify_ok: l : sort X.lt l -> Ok (treeify l) FAILURE! Tactics applied: 10000 Original Proof: [intros. apply elements_sort_ok. rewrite treeify_elements; auto.] Proof search time: 0 min, 18 sec Number of successful tactic applications: 1454 Number of failed tactic applications: 8547 Results for lemma linear_union_spec: s1 s2 x : InT x (linear_union s1 s2) <-> InT x s1 \/ InT x s2 FAILURE! Tactics applied: 267 Original Proof: [unfold linear_union. rewrite treeify_spec, union_list_spec, !rev_elements_rev. rewrite !InA_rev, InA_nil, !elements_spec1 by auto_tc. tauto.] Proof search time: 0 min, 6 sec Number of successful tactic applications: 2 Number of failed tactic applications: 265 Results for lemma rr_nrr_rb: n t : rrt n t -> notredred t -> rbt n t FAILURE! Tactics applied: 10000 Original Proof: [destruct 1 as [l x r Hl Hr]. destruct l, r; descolor; invrb; auto.] Proof search time: 0 min, 18 sec Number of successful tactic applications: 1382 Number of failed tactic applications: 8619 Results for lemma treeify_aux_rb: n : exists d, forall (b:bool), treeify_rb_invariant (ifpred b (Pos.to_nat n)) d (treeify_aux b n) FAILURE! Tactics applied: 10000 Original Proof: [induction n as [n (d,IHn)|n (d,IHn)| ]. - exists (S d). intros b. eapply treeify_cont_rb; [ apply (IHn false) | apply (IHn b) | ]. rewrite Pos2Nat.inj_xI. assert (H := Pos2Nat.is_pos n). apply Nat.neq_0_lt_0 in H. destruct b; simpl; intros; rewrite Nat.add_0_r; trivial. now rewrite <- Nat.add_succ_r, Nat.succ_pred; trivial. - exists (S d). intros b. eapply treeify_cont_rb; [ apply (IHn b) | apply (IHn true) | ]. rewrite Pos2Nat.inj_xO. assert (H := Pos2Nat.is_pos n). apply Nat.neq_0_lt_0 in H. rewrite <- Nat.add_succ_r, Nat.succ_pred by trivial. destruct b; simpl; intros; rewrite Nat.add_0_r; trivial. symmetry. now apply Nat.add_pred_l. - exists 0; destruct b; [ apply treeify_zero_rb | apply treeify_one_rb ].] Proof search time: 0 min, 23 sec Number of successful tactic applications: 1305 Number of failed tactic applications: 8696 Results for lemma append_arb_rb: n l r : rbt n l -> rbt n r -> (arbt n (append l r)) /\ (notred l -> notred r -> rbt n (append l r)) FAILURE! Tactics applied: 10000 Original Proof: [revert r n. append_tac l r. - split; auto. - split; auto. - intros n. invrb. case (IHlr n); auto; clear IHlr. case append_rr_match. + intros a x b _ H; split; invrb. assert (rbt n (Rd a x b)) by auto. invrb. auto. + split; invrb; auto. - split; invrb. destruct (IHlr n) as (_,IH); auto. - split; invrb. destruct (IHrl n) as (_,IH); auto. - nonzero n. invrb. destruct (IHlr n) as (IH,_); auto; clear IHlr. revert IH. case append_bb_match. + intros a x b IH; split; destruct IH; invrb; auto. + split; [left | invrb]; auto using lbalS_rb.] Proof search time: 0 min, 29 sec Number of successful tactic applications: 1768 Number of failed tactic applications: 8233 Results for lemma treeify_zero_spec: : treeify_invariant 0 treeify_zero SUCCESS! Proof Found in EFSM: now subst. Tactics applied: 120 Original Proof: [intro. simpl. auto.] Shorter Proof Found? yes Single step proof reused proof search time: 0 min, 6 sec Number of successful tactic applications: 12 Number of failed tactic applications: 108 Results for lemma lbalS_arb: n l x r : arbt n l -> rbt (S n) r -> arbt (S n) (lbalS l x r) FAILURE! Tactics applied: 10000 Original Proof: [case lbalS_match. - destruct 1; invrb; auto. - clear l. intros l Hl Hl' Hr. destruct r as [|[|] rl rx rr]; invrb. * destruct rl as [|[|] rll rlx rlr]; invrb. right; auto using rbal'_rb, makeRed_rr. * left; apply rbal'_rb; auto.] Proof search time: 0 min, 25 sec Number of successful tactic applications: 1653 Number of failed tactic applications: 8348 Results for lemma inter_rb: s1 s2 : Rbt s1 -> Rbt s2 -> Rbt (inter s1 s2) FAILURE! Tactics applied: 10000 Original Proof: [intros. unfold inter, linear_inter. destruct compare_height; auto_tc.] Proof search time: 0 min, 17 sec Number of successful tactic applications: 1260 Number of failed tactic applications: 8741 Results for lemma union_spec: : forall s1 s2 y `{Ok s1, Ok s2}, (InT y (union s1 s2) <-> InT y s1 \/ InT y s2) FAILURE! Tactics applied: 10000 Original Proof: [intros; apply union_spec'.] Proof search time: 0 min, 20 sec Number of successful tactic applications: 1223 Number of failed tactic applications: 8778 Results for lemma del_spec: : forall s x y `{Ok s}, InT y (del x s) <-> InT y s /\ ~X.eq y x FAILURE! Tactics applied: 10000 Original Proof: [induct s x. - intuition_in. - autorew; intuition_in. assert (X.lt y x') by eauto. order. assert (X.lt x' y) by eauto. order. order. - destruct l as [|[|] ll lx lr]; autorew; rewrite ?IHl by trivial; intuition_in; order. - destruct r as [|[|] rl rx rr]; autorew; rewrite ?IHr by trivial; intuition_in; order.] Proof search time: 0 min, 19 sec Number of successful tactic applications: 1200 Number of failed tactic applications: 8801 Results for lemma ins_rr_rb: x s n : rbt n s -> ifred s (rrt n (ins x s)) (rbt n (ins x s)) FAILURE! Tactics applied: 10000 Original Proof: [induction 1 as [ | n l k r | n l k r Hl IHl Hr IHr ]. - simpl; auto. - simpl. rewrite ifred_notred in * by trivial. elim_compare x k; auto. - rewrite ifred_notred by trivial. unfold ins; fold ins. elim_compare x k. * auto. * apply lbal_rb; trivial. apply ifred_or in IHl; intuition. * apply rbal_rb; trivial. apply ifred_or in IHr; intuition.] Proof search time: 0 min, 21 sec Number of successful tactic applications: 1396 Number of failed tactic applications: 8605 Results for lemma lbal_spec: l x r y : InT y (lbal l x r) <-> X.eq y x \/ InT y l \/ InT y r SUCCESS! Proof Found in EFSM: case lbal_match; intuition_in. Tactics applied: 224 Original Proof: [case lbal_match; intuition_in.] Shorter Proof Found? no This is a novel proof proof search time: 0 min, 6 sec Number of successful tactic applications: 40 Number of failed tactic applications: 184 Results for lemma maxdepth_lowerbound: s : s<>Leaf -> log2 (cardinal s) < maxdepth s FAILURE! Tactics applied: 10000 Original Proof: [apply maxdepth_log_cardinal.] Proof search time: 0 min, 20 sec Number of successful tactic applications: 1427 Number of failed tactic applications: 8574 Results for lemma linear_diff_spec: s1 s2 x `(Ok s1, Ok s2) : InT x (linear_diff s1 s2) <-> InT x s1 /\ ~InT x s2 FAILURE! Tactics applied: 10000 Original Proof: [unfold linear_diff. rewrite !rev_elements_rev, treeify_spec, diff_list_spec by (rewrite rev_involutive; auto_tc). rewrite !InA_rev, InA_nil, !elements_spec1 by auto_tc. tauto.] Proof search time: 0 min, 18 sec Number of successful tactic applications: 799 Number of failed tactic applications: 9202 Results for lemma rb_mindepth: s n : rbt n s -> n + redcarac s <= mindepth s FAILURE! Tactics applied: 10000 Original Proof: [induction 1; simpl. - trivial. - rewrite Nat.add_succ_r. apply -> Nat.succ_le_mono. replace (redcarac l) with 0 in * by now destree l. replace (redcarac r) with 0 in * by now destree r. now apply Nat.min_glb. - apply -> Nat.succ_le_mono. rewrite Nat.add_0_r. apply Nat.min_glb; eauto with arith.] Proof search time: 0 min, 20 sec Number of successful tactic applications: 1683 Number of failed tactic applications: 8318 OVERALL RESULTS SUMMARY EFSMProver proved 10 out of 89 lemmas. Success rate of 11.235955056179774% There were 0 errors. 78 proof attempts exhausted the automaton On average, a proof was found after applying 1398 tactics The longest proof consisted of 3 tactics There were 5 shorter proofs found Of the 78 failures, 75 of them used all 10000 tactics There were 2 reused proofs found There were 8 novel proofs found Of the 78 failures, the average number of tactics used was 9631 On average, a proof was found after 0 min, 11 sec On average, a failed proof attempt took 0 min, 27 sec On average, any (success or failure) proof attempt took 0 min, 25 sec The longest time to find a proof was 0 min, 18 sec The shortest time to find a proof was 0 min, 6 sec There were 1 proofs containing repeated tactics There were 1 proofs that repeated states