Results for fold 1 Results for lemma rolm_rolm: : forall x n1 m1 n2 m2, rolm (rolm x n1 m1) n2 m2 = rolm x (Int.modu (Int.add n1 n2) Int.iwordsize) (Int.and (Int.rol m1 n2) m2) FAILURE! Tactics applied: 10000 Original Proof: [intros; destruct x; simpl; auto. decEq. apply Int.rolm_rolm. apply int_wordsize_divides_modulus.] Proof search time: 0 min, 38 sec Number of successful tactic applications: 1688 Number of failed tactic applications: 8313 Results for fold 2 Results for lemma mul_commut: : forall x y, mul x y = mul y x FAILURE! Tactics applied: 10000 Original Proof: [destruct x; destruct y; simpl; auto. decEq. apply Int.mul_commut.] Proof search time: 0 min, 35 sec Number of successful tactic applications: 2179 Number of failed tactic applications: 7822 Results for fold 3 Results for lemma cmpu_eq_0_optbool: : forall valid_ptr ob, cmpu valid_ptr Ceq (of_optbool ob) (Vint Int.zero) = of_optbool (option_map negb ob) SUCCESS! Proof Found in EFSM: destruct ob; auto ; destruct b; auto. Tactics applied: 7635 Original Proof: [intros. destruct ob; simpl; auto. destruct b; auto.] Shorter Proof Found? yes This is a novel proof proof search time: 0 min, 36 sec Number of successful tactic applications: 1105 Number of failed tactic applications: 6530 Results for fold 4 Results for lemma negate_cmpf_ne: : forall v1 v2, notbool (cmpf Ceq v1 v2) = cmpf Cne v1 v2 FAILURE! Tactics applied: 10000 Original Proof: [destruct v1; destruct v2; auto. unfold cmpf, cmpf_bool. rewrite Float.cmp_ne_eq. destruct (Float.cmp Ceq f f0); auto.] Proof search time: 0 min, 30 sec Number of successful tactic applications: 1619 Number of failed tactic applications: 8382 Results for fold 5 Results for lemma add_assoc: : forall x y z, add (add x y) z = add x (add y z) FAILURE! Tactics applied: 10000 Original Proof: [destruct x; destruct y; destruct z; simpl; auto. rewrite Int.add_assoc; auto. rewrite Int.add_assoc; auto. decEq. decEq. apply Int.add_commut. decEq. rewrite Int.add_commut. rewrite <- Int.add_assoc. decEq. apply Int.add_commut. decEq. rewrite Int.add_assoc. auto.] Proof search time: 0 min, 57 sec Number of successful tactic applications: 2575 Number of failed tactic applications: 7426 Results for fold 6 Results for lemma negate_cmp_bool: : forall c x y, cmp_bool (negate_comparison c) x y = option_map negb (cmp_bool c x y) FAILURE! Tactics applied: 10000 Original Proof: [destruct x; destruct y; simpl; auto. rewrite Int.negate_cmp. auto.] Proof search time: 1 min, 15 sec Number of successful tactic applications: 2621 Number of failed tactic applications: 7380 Results for fold 7 Results for lemma val_list_inject_incr: : forall f1 f2 vl vl' , inject_incr f1 f2 -> val_list_inject f1 vl vl' -> val_list_inject f2 vl vl' FAILURE! Tactics applied: 10000 Original Proof: [induction vl; intros; inv H0. auto. constructor. eapply val_inject_incr; eauto. auto.] Proof search time: 0 min, 38 sec Number of successful tactic applications: 1735 Number of failed tactic applications: 8266 Results for fold 8 Results for lemma val_list_inject_lessdef: : forall vl1 vl2, Val.lessdef_list vl1 vl2 <-> val_list_inject (fun b => Some(b, 0)) vl1 vl2 FAILURE! Tactics applied: 10000 Original Proof: [intros; split. induction 1; constructor; auto. apply val_inject_lessdef; auto. induction 1; constructor; auto. apply val_inject_lessdef; auto.] Proof search time: 0 min, 35 sec Number of successful tactic applications: 1418 Number of failed tactic applications: 8583 Results for fold 9 Results for lemma not_of_optbool: : forall ob, of_optbool (option_map negb ob) = notbool (of_optbool ob) SUCCESS! Proof Found in EFSM: destruct ob; auto. destruct b; reflexivity. Tactics applied: 5590 Original Proof: [destruct ob; auto. destruct b; auto.] Shorter Proof Found? no This is a novel proof proof search time: 0 min, 24 sec Number of successful tactic applications: 688 Number of failed tactic applications: 4902 Results for fold 10 Results for lemma load_result_lessdef: : forall chunk v1 v2, lessdef v1 v2 -> lessdef (load_result chunk v1) (load_result chunk v2) SUCCESS! Proof Found in EFSM: induction 1; destruct chunk; econstructor ; Tactics applied: 2572 Original Proof: [intros. inv H. auto. destruct chunk; simpl; auto.] Shorter Proof Found? yes This is a novel proof proof search time: 0 min, 22 sec Number of successful tactic applications: 475 Number of failed tactic applications: 2097 Results for fold 11 Results for lemma val_load_result_inject: : forall chunk v1 v2, val_inject f v1 v2 -> val_inject f (Val.load_result chunk v1) (Val.load_result chunk v2) FAILURE! Tactics applied: 10000 Original Proof: [intros. inv H; destruct chunk; simpl; econstructor; eauto.] Proof search time: 1 min, 14 sec Number of successful tactic applications: 1588 Number of failed tactic applications: 8413 Results for fold 12 Results for lemma cmpf_ge: : forall v1 v2, cmpf Cge v1 v2 = or (cmpf Cgt v1 v2) (cmpf Ceq v1 v2) FAILURE! Tactics applied: 10000 Original Proof: [destruct v1; destruct v2; auto. unfold cmpf, cmpf_bool. rewrite Float.cmp_ge_gt_eq. destruct (Float.cmp Cgt f f0); destruct (Float.cmp Ceq f f0); auto.] Proof search time: 0 min, 38 sec Number of successful tactic applications: 1943 Number of failed tactic applications: 8058 Results for fold 13 Results for lemma rolm_zero: : forall x m, rolm x Int.zero m = and x (Vint m) FAILURE! Tactics applied: 10000 Original Proof: [intros; destruct x; simpl; auto. decEq. apply Int.rolm_zero.] Proof search time: 0 min, 36 sec Number of successful tactic applications: 1906 Number of failed tactic applications: 8095 Results for fold 14 Results for lemma not_xor: : forall x, notint x = xor x (Vint Int.mone) SUCCESS! Proof Found in EFSM: constructor ; Tactics applied: 15 Original Proof: [destruct x; simpl; auto.] Shorter Proof Found? yes Single step proof reused proof search time: 0 min, 18 sec Number of successful tactic applications: 3 Number of failed tactic applications: 12 Results for fold 15 Results for lemma mul_add_distr_r: : forall x y z, mul x (add y z) = add (mul x y) (mul x z) FAILURE! Tactics applied: 10000 Original Proof: [destruct x; destruct y; destruct z; simpl; auto. decEq. apply Int.mul_add_distr_r.] Proof search time: 1 min, 4 sec Number of successful tactic applications: 2112 Number of failed tactic applications: 7889 Results for fold 16 Results for lemma cast16unsigned_and: : forall x, zero_ext 16 x = and x (Vint(Int.repr 65535)) FAILURE! Tactics applied: 10000 Original Proof: [destruct x; simpl; auto. decEq. change 65535 with (two_p 16 - 1). apply Int.zero_ext_and. omega.] Proof search time: 0 min, 31 sec Number of successful tactic applications: 2445 Number of failed tactic applications: 7556 Results for fold 17 Results for lemma val_inject_id: : forall v1 v2, val_inject inject_id v1 v2 <-> Val.lessdef v1 v2 SUCCESS! Proof Found in EFSM: symmetry. apply val_inject_lessdef; Tactics applied: 303 Original Proof: [intros; split; intros. inv H; auto. unfold inject_id in H0. inv H0. rewrite Int.add_zero. constructor. inv H. destruct v2; econstructor. unfold inject_id; reflexivity. rewrite Int.add_zero; auto. constructor.] Shorter Proof Found? yes This is a novel proof proof search time: 0 min, 9 sec Number of successful tactic applications: 51 Number of failed tactic applications: 252 Results for fold 18 Results for lemma sign_ext_lessdef: : forall n v1 v2, lessdef v1 v2 -> lessdef (sign_ext n v1) (sign_ext n v2) SUCCESS! Proof Found in EFSM: induction 1; auto. Tactics applied: 425 Original Proof: [intros; inv H; simpl; auto.] Shorter Proof Found? yes This is a novel proof proof search time: 0 min, 12 sec Number of successful tactic applications: 63 Number of failed tactic applications: 362 Results for fold 19 Results for lemma shrx_carry: : forall x y z, shrx x y = Some z -> add (shr x y) (shr_carry x y) = z FAILURE! Tactics applied: 10000 Original Proof: [intros. destruct x; destruct y; simpl in H; inv H. destruct (Int.ltu i0 (Int.repr 31)) eqn:?; inv H1. exploit Int.ltu_inv; eauto. change (Int.unsigned (Int.repr 31)) with 31. intros. assert (Int.ltu i0 Int.iwordsize = true). unfold Int.ltu. apply zlt_true. change (Int.unsigned Int.iwordsize) with 32. omega. simpl. rewrite H0. simpl. decEq. rewrite Int.shrx_carry; auto.] Proof search time: 0 min, 33 sec Number of successful tactic applications: 2389 Number of failed tactic applications: 7612 Results for fold 20 Results for lemma cmpu_ne_1_optbool: : forall valid_ptr ob, cmpu valid_ptr Cne (of_optbool ob) (Vint Int.one) = of_optbool (option_map negb ob) FAILURE! Tactics applied: 10000 Original Proof: [intros. destruct ob; simpl; auto. destruct b; auto.] Proof search time: 0 min, 46 sec Number of successful tactic applications: 2108 Number of failed tactic applications: 7893 Results for fold 21 Results for lemma zero_ext_and: : forall n v, 0 < n < Int.zwordsize -> Val.zero_ext n v = Val.and v (Vint (Int.repr (two_p n - 1))) FAILURE! Tactics applied: 10000 Original Proof: [intros. destruct v; simpl; auto. decEq. apply Int.zero_ext_and; auto. omega.] Proof search time: 0 min, 44 sec Number of successful tactic applications: 1865 Number of failed tactic applications: 8136 Results for fold 22 Results for lemma has_subtype_list: : forall tyl1 tyl2 vl, subtype_list tyl1 tyl2 = true -> has_type_list vl tyl1 -> has_type_list vl tyl2 FAILURE! Tactics applied: 10000 Original Proof: [induction tyl1; intros; destruct tyl2; try discriminate; destruct vl; try contradiction. red; auto. simpl in *. InvBooleans. destruct H0. split; auto. eapply has_subtype; eauto.] Proof search time: 0 min, 17 sec Number of successful tactic applications: 943 Number of failed tactic applications: 9058 Results for fold 23 Results for lemma cmpu_bool_lessdef: : forall valid_ptr valid_ptr' c v1 v1' v2 v2' b, (forall b ofs, valid_ptr b ofs = true -> valid_ptr' b ofs = true) -> lessdef v1 v1' -> lessdef v2 v2' -> cmpu_bool valid_ptr c v1 v2 = Some b -> cmpu_bool valid_ptr' c v1' v2' = Some b FAILURE! Tactics applied: 10000 Original Proof: [intros. destruct v1; simpl in H2; try discriminate; destruct v2; simpl in H2; try discriminate; inv H0; inv H1; simpl; auto. destruct (eq_block b0 b1). assert (forall b ofs, valid_ptr b ofs || valid_ptr b (ofs - 1) = true -> valid_ptr' b ofs || valid_ptr' b (ofs - 1) = true). intros until ofs. rewrite ! orb_true_iff. intuition. destruct (valid_ptr b0 (Int.unsigned i) || valid_ptr b0 (Int.unsigned i - 1)) eqn:?; try discriminate. destruct (valid_ptr b1 (Int.unsigned i0) || valid_ptr b1 (Int.unsigned i0 - 1)) eqn:?; try discriminate. erewrite !H0 by eauto. auto. destruct (valid_ptr b0 (Int.unsigned i)) eqn:?; try discriminate. destruct (valid_ptr b1 (Int.unsigned i0)) eqn:?; try discriminate. erewrite !H by eauto. auto.] Proof search time: 0 min, 55 sec Number of successful tactic applications: 2377 Number of failed tactic applications: 7624 Results for fold 24 Results for lemma inject_incr_refl: : forall f , inject_incr f f SUCCESS! Proof Found in EFSM: unfold inject_incr; eauto. Tactics applied: 238 Original Proof: [unfold inject_incr. auto.] Shorter Proof Found? no This is a novel proof proof search time: 0 min, 20 sec Number of successful tactic applications: 44 Number of failed tactic applications: 194 Results for fold 25 Results for lemma shl_rolm: : forall x n, Int.ltu n Int.iwordsize = true -> shl x (Vint n) = rolm x n (Int.shl Int.mone n) FAILURE! Tactics applied: 10000 Original Proof: [intros; destruct x; simpl; auto. rewrite H. decEq. apply Int.shl_rolm. exact H.] Proof search time: 0 min, 46 sec Number of successful tactic applications: 1968 Number of failed tactic applications: 8033 Results for fold 26 Results for lemma notbool_negb_1: : forall b, of_bool (negb b) = notbool (of_bool b) SUCCESS! Proof Found in EFSM: destruct b; reflexivity. Tactics applied: 340 Original Proof: [destruct b; reflexivity.] Shorter Proof Found? no Proof reused from notbool_idem2 proof search time: 0 min, 8 sec Number of successful tactic applications: 41 Number of failed tactic applications: 299 Results for fold 27 Results for lemma and_commut: : forall x y, and x y = and y x FAILURE! Tactics applied: 10000 Original Proof: [destruct x; destruct y; simpl; auto. decEq. apply Int.and_commut.] Proof search time: 0 min, 29 sec Number of successful tactic applications: 1510 Number of failed tactic applications: 8491 Results for fold 28 Results for lemma val_inject_compose: : forall f f' v1 v2 v3, val_inject f v1 v2 -> val_inject f' v2 v3 -> val_inject (compose_meminj f f') v1 v3 FAILURE! Tactics applied: 10000 Original Proof: [intros. inv H; auto; inv H0; auto. econstructor. unfold compose_meminj; rewrite H1; rewrite H3; eauto. rewrite Int.add_assoc. decEq. unfold Int.add. apply Int.eqm_samerepr. auto with ints.] Proof search time: 0 min, 45 sec Number of successful tactic applications: 1913 Number of failed tactic applications: 8088 Results for fold 29 Results for lemma notbool_idem4: : forall ob, notbool (notbool (of_optbool ob)) = of_optbool ob SUCCESS! Proof Found in EFSM: destruct ob; auto ; destruct b; tauto. Tactics applied: 7312 Original Proof: [destruct ob; auto. destruct b; auto.] Shorter Proof Found? no This is a novel proof proof search time: 0 min, 24 sec Number of successful tactic applications: 1394 Number of failed tactic applications: 5918 Results for fold 30 Results for lemma val_hiword_inject: : forall v v', val_inject f v v' -> val_inject f (Val.hiword v) (Val.hiword v') SUCCESS! Proof Found in EFSM: induction 1; econstructor ; Tactics applied: 115 Original Proof: [intros. unfold Val.hiword; inv H; auto.] Shorter Proof Found? yes This is a novel proof proof search time: 0 min, 8 sec Number of successful tactic applications: 10 Number of failed tactic applications: 105 Results for fold 31 Results for lemma or_rolm: : forall x n m1 m2, or (rolm x n m1) (rolm x n m2) = rolm x n (Int.or m1 m2) FAILURE! Tactics applied: 10000 Original Proof: [intros; destruct x; simpl; auto. decEq. apply Int.or_rolm.] Proof search time: 0 min, 31 sec Number of successful tactic applications: 1645 Number of failed tactic applications: 8356 Results for fold 32 Results for lemma val_longofwords_inject: : forall v1 v2 v1' v2', val_inject f v1 v1' -> val_inject f v2 v2' -> val_inject f (Val.longofwords v1 v2) (Val.longofwords v1' v2') SUCCESS! Proof Found in EFSM: induction 1; induction 1; constructor ; Tactics applied: 1316 Original Proof: [intros. unfold Val.longofwords. inv H; auto. inv H0; auto.] Shorter Proof Found? yes This is a novel proof This proof contained a loop around a state This proof contained a sequence of repeated tactics proof search time: 0 min, 19 sec Number of successful tactic applications: 286 Number of failed tactic applications: 1030 Results for fold 33 Results for lemma neg_add_distr: : forall x y, neg(add x y) = add (neg x) (neg y) FAILURE! Tactics applied: 10000 Original Proof: [destruct x; destruct y; simpl; auto. decEq. apply Int.neg_add_distr.] Proof search time: 0 min, 50 sec Number of successful tactic applications: 2460 Number of failed tactic applications: 7541 Results for fold 34 Results for lemma of_optbool_lessdef: : forall ob ob', (forall b, ob = Some b -> ob' = Some b) -> lessdef (of_optbool ob) (of_optbool ob') FAILURE! Tactics applied: 10000 Original Proof: [intros. destruct ob; simpl; auto. rewrite (H b); auto.] Proof search time: 0 min, 38 sec Number of successful tactic applications: 1626 Number of failed tactic applications: 8375 Results for fold 35 Results for lemma and_assoc: : forall x y z, and (and x y) z = and x (and y z) FAILURE! Tactics applied: 10000 Original Proof: [destruct x; destruct y; destruct z; simpl; auto. decEq. apply Int.and_assoc.] Proof search time: 0 min, 45 sec Number of successful tactic applications: 1870 Number of failed tactic applications: 8131 Results for fold 36 Results for lemma hiword_lessdef: : forall v v', lessdef v v' -> lessdef (hiword v) (hiword v') SUCCESS! Proof Found in EFSM: induction 1; auto. Tactics applied: 129 Original Proof: [intros. inv H; auto.] Shorter Proof Found? yes This is a novel proof proof search time: 0 min, 7 sec Number of successful tactic applications: 19 Number of failed tactic applications: 110 Results for fold 37 Results for lemma bool_of_val_of_optbool: : forall ob b, bool_of_val (of_optbool ob) b -> ob = Some b FAILURE! Tactics applied: 10000 Original Proof: [intros. destruct ob; simpl in H. destruct b0; simpl in H; inv H; auto. inv H.] Proof search time: 0 min, 32 sec Number of successful tactic applications: 1670 Number of failed tactic applications: 8331 Results for fold 38 Results for lemma add_permut_4: : forall x y z t, add (add x y) (add z t) = add (add x z) (add y t) FAILURE! Tactics applied: 10000 Original Proof: [intros. rewrite add_permut. rewrite add_assoc. rewrite add_permut. symmetry. apply add_assoc.] Proof search time: 0 min, 35 sec Number of successful tactic applications: 1795 Number of failed tactic applications: 8206 Results for fold 39 Results for lemma longofwords_lessdef: : forall v1 v2 v1' v2', lessdef v1 v1' -> lessdef v2 v2' -> lessdef (longofwords v1 v2) (longofwords v1' v2') FAILURE! Tactics applied: 10000 Original Proof: [intros. unfold longofwords. inv H; auto. inv H0; auto. destruct v1'; auto.] Proof search time: 0 min, 49 sec Number of successful tactic applications: 2153 Number of failed tactic applications: 7848 Results for fold 40 Results for lemma notbool_idem3: : forall x, notbool(notbool(notbool x)) = notbool x FAILURE! Tactics applied: 10000 Original Proof: [destruct x; simpl; auto. case (Int.eq i Int.zero); reflexivity.] Proof search time: 0 min, 29 sec Number of successful tactic applications: 1604 Number of failed tactic applications: 8397 Results for fold 41 Results for lemma cmp_ne_1_optbool: : forall ob, cmp Cne (of_optbool ob) (Vint Int.one) = of_optbool (option_map negb ob) FAILURE! Tactics applied: 10000 Original Proof: [intros. destruct ob; simpl; auto. destruct b; auto.] Proof search time: 0 min, 42 sec Number of successful tactic applications: 1459 Number of failed tactic applications: 8542 Results for fold 42 Results for lemma cmp_eq_0_optbool: : forall ob, cmp Ceq (of_optbool ob) (Vint Int.zero) = of_optbool (option_map negb ob) FAILURE! Tactics applied: 10000 Original Proof: [intros. destruct ob; simpl; auto. destruct b; auto.] Proof search time: 0 min, 40 sec Number of successful tactic applications: 2232 Number of failed tactic applications: 7769 Results for fold 43 Results for lemma zero_ext_lessdef: : forall n v1 v2, lessdef v1 v2 -> lessdef (zero_ext n v1) (zero_ext n v2) SUCCESS! Proof Found in EFSM: induction 1; constructor. Tactics applied: 64 Original Proof: [intros; inv H; simpl; auto.] Shorter Proof Found? yes This is a novel proof proof search time: 0 min, 7 sec Number of successful tactic applications: 17 Number of failed tactic applications: 47 Results for fold 44 Results for lemma val_inject_incr: : forall f1 f2 v v', inject_incr f1 f2 -> val_inject f1 v v' -> val_inject f2 v v' SUCCESS! Proof Found in EFSM: intros ; inv H0; auto ; eauto. Tactics applied: 4844 Original Proof: [intros. inv H0; eauto.] Shorter Proof Found? no This is a novel proof proof search time: 0 min, 24 sec Number of successful tactic applications: 905 Number of failed tactic applications: 3939 Results for fold 45 Results for lemma add_lessdef: : forall v1 v1' v2 v2', lessdef v1 v1' -> lessdef v2 v2' -> lessdef (add v1 v2) (add v1' v2') FAILURE! Tactics applied: 10000 Original Proof: [intros. inv H. inv H0. auto. destruct v1'; simpl; auto. simpl; auto.] Proof search time: 0 min, 57 sec Number of successful tactic applications: 2007 Number of failed tactic applications: 7994 Results for fold 46 Results for lemma add_commut: : forall x y, add x y = add y x FAILURE! Tactics applied: 10000 Original Proof: [destruct x; destruct y; simpl; auto. decEq. apply Int.add_commut.] Proof search time: 0 min, 30 sec Number of successful tactic applications: 2033 Number of failed tactic applications: 7968 Results for fold 47 Results for lemma sub_zero_r: : forall x, sub Vzero x = neg x SUCCESS! Proof Found in EFSM: reflexivity. Tactics applied: 1 Original Proof: [destruct x; simpl; auto.] Shorter Proof Found? yes Single step proof reused proof search time: 0 min, 12 sec Number of successful tactic applications: 1 Number of failed tactic applications: 0 Results for fold 48 Results for lemma mods_divs: : forall x y z, mods x y = Some z -> exists v, divs x y = Some v /\ z = sub x (mul v y) FAILURE! Tactics applied: 10000 Original Proof: [intros. destruct x; destruct y; simpl in *; try discriminate. destruct (Int.eq i0 Int.zero || Int.eq i (Int.repr Int.min_signed) && Int.eq i0 Int.mone); inv H. exists (Vint (Int.divs i i0)); split; auto. simpl. rewrite Int.mods_divs. auto.] Proof search time: 1 min, 9 sec Number of successful tactic applications: 1965 Number of failed tactic applications: 8036 Results for fold 49 Results for lemma val_inject_lessdef: : forall v1 v2, Val.lessdef v1 v2 <-> val_inject (fun b => Some(b, 0)) v1 v2 FAILURE! Tactics applied: 10000 Original Proof: [intros; split; intros. inv H; auto. destruct v2; econstructor; eauto. rewrite Int.add_zero; auto. inv H; auto. inv H0. rewrite Int.add_zero; auto.] Proof search time: 0 min, 42 sec Number of successful tactic applications: 1639 Number of failed tactic applications: 8362 Results for fold 50 Results for lemma or_commut: : forall x y, or x y = or y x FAILURE! Tactics applied: 10000 Original Proof: [destruct x; destruct y; simpl; auto. decEq. apply Int.or_commut.] Proof search time: 0 min, 53 sec Number of successful tactic applications: 2141 Number of failed tactic applications: 7860 Results for fold 51 Results for lemma notbool_idem2: : forall b, notbool(notbool(of_bool b)) = of_bool b SUCCESS! Proof Found in EFSM: destruct b; auto. Tactics applied: 238 Original Proof: [destruct b; reflexivity.] Shorter Proof Found? no This is a novel proof proof search time: 0 min, 9 sec Number of successful tactic applications: 32 Number of failed tactic applications: 206 Results for fold 52 Results for lemma divs_pow2: : forall x n logn y, Int.is_power2 n = Some logn -> Int.ltu logn (Int.repr 31) = true -> divs x (Vint n) = Some y -> shrx x (Vint logn) = Some y FAILURE! Tactics applied: 10000 Original Proof: [intros; destruct x; simpl in H1; inv H1. destruct (Int.eq n Int.zero || Int.eq i (Int.repr Int.min_signed) && Int.eq n Int.mone); inv H3. simpl. rewrite H0. decEq. decEq. symmetry. apply Int.divs_pow2. auto.] Proof search time: 0 min, 37 sec Number of successful tactic applications: 2279 Number of failed tactic applications: 7722 Results for fold 53 Results for lemma cast8unsigned_and: : forall x, zero_ext 8 x = and x (Vint(Int.repr 255)) FAILURE! Tactics applied: 10000 Original Proof: [destruct x; simpl; auto. decEq. change 255 with (two_p 8 - 1). apply Int.zero_ext_and. omega.] Proof search time: 0 min, 39 sec Number of successful tactic applications: 1816 Number of failed tactic applications: 8185 Results for fold 54 Results for lemma val_cmp_bool_inject: : forall c v1 v2 v1' v2' b, val_inject f v1 v1' -> val_inject f v2 v2' -> Val.cmp_bool c v1 v2 = Some b -> Val.cmp_bool c v1' v2' = Some b FAILURE! Tactics applied: 10000 Original Proof: [intros. inv H; simpl in H1; try discriminate; inv H0; simpl in H1; try discriminate; simpl; auto.] Proof search time: 1 min, 7 sec Number of successful tactic applications: 2173 Number of failed tactic applications: 7828 Results for fold 55 Results for lemma shrx_shr: : forall x y z, shrx x y = Some z -> exists p, exists q, x = Vint p /\ y = Vint q /\ z = shr (if Int.lt p Int.zero then add x (Vint (Int.sub (Int.shl Int.one q) Int.one)) else x) (Vint q) FAILURE! Tactics applied: 10000 Original Proof: [intros. destruct x; destruct y; simpl in H; inv H. destruct (Int.ltu i0 (Int.repr 31)) eqn:?; inv H1. exploit Int.ltu_inv; eauto. change (Int.unsigned (Int.repr 31)) with 31. intros. assert (Int.ltu i0 Int.iwordsize = true). unfold Int.ltu. apply zlt_true. change (Int.unsigned Int.iwordsize) with 32. omega. exists i; exists i0; intuition. rewrite Int.shrx_shr; auto. destruct (Int.lt i Int.zero); simpl; rewrite H0; auto.] Proof search time: 0 min, 54 sec Number of successful tactic applications: 1576 Number of failed tactic applications: 8425 Results for fold 56 Results for lemma load_result_type: : forall chunk v, has_type (load_result chunk v) (type_of_chunk chunk) FAILURE! Tactics applied: 10000 Original Proof: [intros. destruct chunk; destruct v; simpl; auto.] Proof search time: 0 min, 47 sec Number of successful tactic applications: 1497 Number of failed tactic applications: 8504 Results for fold 57 Results for lemma has_subtype: : forall ty1 ty2 v, subtype ty1 ty2 = true -> has_type v ty1 -> has_type v ty2 FAILURE! Tactics applied: 10000 Original Proof: [intros. destruct ty1; destruct ty2; simpl in H; discriminate || assumption || idtac; unfold has_type in *; destruct v; auto.] Proof search time: 0 min, 46 sec Number of successful tactic applications: 1783 Number of failed tactic applications: 8218 Results for fold 58 Results for lemma val_loword_inject: : forall v v', val_inject f v v' -> val_inject f (Val.loword v) (Val.loword v') SUCCESS! Proof Found in EFSM: induction 1; constructor. Tactics applied: 185 Original Proof: [intros. unfold Val.loword; inv H; auto.] Shorter Proof Found? yes This is a novel proof proof search time: 0 min, 12 sec Number of successful tactic applications: 22 Number of failed tactic applications: 163 Results for fold 59 Results for lemma sub_add_r: : forall v1 v2 i, sub v1 (add v2 (Vint i)) = add (sub v1 v2) (Vint (Int.neg i)) FAILURE! Tactics applied: 10000 Original Proof: [destruct v1; destruct v2; intros; simpl; auto. rewrite Int.sub_add_r. auto. repeat rewrite Int.sub_add_opp. decEq. repeat rewrite Int.add_assoc. decEq. apply Int.add_commut. decEq. repeat rewrite Int.sub_add_opp. rewrite Int.add_assoc. decEq. apply Int.neg_add_distr. case (eq_block b b0); intro. simpl. decEq. repeat rewrite Int.sub_add_opp. rewrite Int.add_assoc. decEq. apply Int.neg_add_distr. reflexivity.] Proof search time: 0 min, 43 sec Number of successful tactic applications: 2602 Number of failed tactic applications: 7399 Results for fold 60 Results for lemma cmpf_le: : forall v1 v2, cmpf Cle v1 v2 = or (cmpf Clt v1 v2) (cmpf Ceq v1 v2) FAILURE! Tactics applied: 10000 Original Proof: [destruct v1; destruct v2; auto. unfold cmpf, cmpf_bool. rewrite Float.cmp_le_lt_eq. destruct (Float.cmp Clt f f0); destruct (Float.cmp Ceq f f0); auto.] Proof search time: 0 min, 39 sec Number of successful tactic applications: 1936 Number of failed tactic applications: 8065 Results for fold 61 Results for lemma or_assoc: : forall x y z, or (or x y) z = or x (or y z) FAILURE! Tactics applied: 10000 Original Proof: [destruct x; destruct y; destruct z; simpl; auto. decEq. apply Int.or_assoc.] Proof search time: 0 min, 56 sec Number of successful tactic applications: 3048 Number of failed tactic applications: 6953 Results for fold 62 Results for lemma shru_rolm: : forall x n, Int.ltu n Int.iwordsize = true -> shru x (Vint n) = rolm x (Int.sub Int.iwordsize n) (Int.shru Int.mone n) FAILURE! Tactics applied: 10000 Original Proof: [intros; destruct x; simpl; auto. rewrite H. decEq. apply Int.shru_rolm. exact H.] Proof search time: 0 min, 41 sec Number of successful tactic applications: 2828 Number of failed tactic applications: 7173 Results for fold 63 Results for lemma load_result_same: : forall v ty, has_type v ty -> load_result (chunk_of_type ty) v = v FAILURE! Tactics applied: 10000 Original Proof: [unfold has_type; intros. destruct v; destruct ty; try contradiction; auto.] Proof search time: 1 min, 28 sec Number of successful tactic applications: 1415 Number of failed tactic applications: 8586 Results for fold 64 Results for lemma inject_incr_trans: : forall f1 f2 f3, inject_incr f1 f2 -> inject_incr f2 f3 -> inject_incr f1 f3 SUCCESS! Proof Found in EFSM: unfold inject_incr. auto. Tactics applied: 120 Original Proof: [unfold inject_incr; intros. eauto.] Shorter Proof Found? yes Proof reused from inject_incr_refl proof search time: 0 min, 20 sec Number of successful tactic applications: 12 Number of failed tactic applications: 108 Results for fold 65 Results for lemma neg_zero: : neg Vzero = Vzero SUCCESS! Proof Found in EFSM: auto. Tactics applied: 9 Original Proof: [reflexivity.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 16 sec Number of successful tactic applications: 2 Number of failed tactic applications: 7 Results for fold 66 Results for lemma modu_divu: : forall x y z, modu x y = Some z -> exists v, divu x y = Some v /\ z = sub x (mul v y) FAILURE! Tactics applied: 10000 Original Proof: [intros. destruct x; destruct y; simpl in *; try discriminate. destruct (Int.eq i0 Int.zero) eqn:?; inv H. exists (Vint (Int.divu i i0)); split; auto. simpl. rewrite Int.modu_divu. auto. generalize (Int.eq_spec i0 Int.zero). rewrite Heqb; auto.] Proof search time: 0 min, 53 sec Number of successful tactic applications: 1525 Number of failed tactic applications: 8476 Results for fold 67 Results for lemma val_cmpu_bool_inject: : forall c v1 v2 v1' v2' b, val_inject f v1 v1' -> val_inject f v2 v2' -> Val.cmpu_bool valid_ptr1 c v1 v2 = Some b -> Val.cmpu_bool valid_ptr2 c v1' v2' = Some b FAILURE! Tactics applied: 10000 Original Proof: [Local Opaque Int.add. intros. inv H; simpl in H1; try discriminate; inv H0; simpl in H1; try discriminate; simpl; auto. fold (weak_valid_ptr1 b1 (Int.unsigned ofs1)) in H1. fold (weak_valid_ptr1 b0 (Int.unsigned ofs0)) in H1. fold (weak_valid_ptr2 b2 (Int.unsigned (Int.add ofs1 (Int.repr delta)))). fold (weak_valid_ptr2 b3 (Int.unsigned (Int.add ofs0 (Int.repr delta0)))). destruct (eq_block b1 b0); subst. rewrite H in H2. inv H2. rewrite dec_eq_true. destruct (weak_valid_ptr1 b0 (Int.unsigned ofs1)) eqn:?; try discriminate. destruct (weak_valid_ptr1 b0 (Int.unsigned ofs0)) eqn:?; try discriminate. erewrite !weak_valid_ptr_inj by eauto. simpl. rewrite <-H1. simpl. decEq. apply Int.translate_cmpu; eauto. destruct (valid_ptr1 b1 (Int.unsigned ofs1)) eqn:?; try discriminate. destruct (valid_ptr1 b0 (Int.unsigned ofs0)) eqn:?; try discriminate. destruct (eq_block b2 b3); subst. assert (valid_ptr_implies: forall b ofs, valid_ptr1 b ofs = true -> weak_valid_ptr1 b ofs = true). intros. unfold weak_valid_ptr1. rewrite H0; auto. erewrite !weak_valid_ptr_inj by eauto using valid_ptr_implies. simpl. exploit valid_different_ptrs_inj; eauto. intros [?|?]; [congruence |]. destruct c; simpl in H1; inv H1. simpl; decEq. rewrite Int.eq_false; auto. congruence. simpl; decEq. rewrite Int.eq_false; auto. congruence. now erewrite !valid_ptr_inj by eauto.] Proof search time: 2 min, 24 sec Number of successful tactic applications: 2238 Number of failed tactic applications: 7763 Results for fold 68 Results for lemma negate_cmp: : forall c x y, cmp (negate_comparison c) x y = notbool (cmp c x y) FAILURE! Tactics applied: 10000 Original Proof: [intros. unfold cmp. rewrite negate_cmp_bool. apply not_of_optbool.] Proof search time: 0 min, 38 sec Number of successful tactic applications: 2129 Number of failed tactic applications: 7872 Results for fold 69 Results for lemma cmp_eq_1_optbool: : forall ob, cmp Ceq (of_optbool ob) (Vint Int.one) = of_optbool ob FAILURE! Tactics applied: 10000 Original Proof: [intros. destruct ob; simpl; auto. destruct b; auto.] Proof search time: 0 min, 29 sec Number of successful tactic applications: 1738 Number of failed tactic applications: 8263 Results for fold 70 Results for lemma notbool_negb_3: : forall ob, of_optbool (option_map negb ob) = notbool (of_optbool ob) FAILURE! Tactics applied: 10000 Original Proof: [destruct ob; auto. destruct b; auto.] Proof search time: 0 min, 42 sec Number of successful tactic applications: 1059 Number of failed tactic applications: 8942 Results for fold 71 Results for lemma mul_pow2: : forall x n logn, Int.is_power2 n = Some logn -> mul x (Vint n) = shl x (Vint logn) FAILURE! Tactics applied: 10000 Original Proof: [intros; destruct x; simpl; auto. change 32 with Int.zwordsize. rewrite (Int.is_power2_range _ _ H). decEq. apply Int.mul_pow2. auto.] Proof search time: 0 min, 40 sec Number of successful tactic applications: 1760 Number of failed tactic applications: 8241 Results for fold 72 Results for lemma bool_of_val_of_bool: : forall b1 b2, bool_of_val (of_bool b1) b2 -> b1 = b2 FAILURE! Tactics applied: 10000 Original Proof: [intros. destruct b1; simpl in H; inv H; auto.] Proof search time: 0 min, 50 sec Number of successful tactic applications: 963 Number of failed tactic applications: 9038 Results for fold 73 Results for lemma sub_opp_add: : forall x y, sub x (Vint (Int.neg y)) = add x (Vint y) FAILURE! Tactics applied: 10000 Original Proof: [intros. unfold sub, add. destruct x; auto; rewrite Int.sub_add_opp; rewrite Int.neg_involutive; auto.] Proof search time: 0 min, 42 sec Number of successful tactic applications: 2296 Number of failed tactic applications: 7705 Results for fold 74 Results for lemma shl_mul: : forall x y, mul x (shl Vone y) = shl x y FAILURE! Tactics applied: 10000 Original Proof: [destruct x; destruct y; simpl; auto. case (Int.ltu i0 Int.iwordsize); auto. decEq. symmetry. apply Int.shl_mul.] Proof search time: 0 min, 47 sec Number of successful tactic applications: 2049 Number of failed tactic applications: 7952 Results for fold 75 Results for lemma cmp_ne_0_optbool: : forall ob, cmp Cne (of_optbool ob) (Vint Int.zero) = of_optbool ob FAILURE! Tactics applied: 10000 Original Proof: [intros. destruct ob; simpl; auto. destruct b; auto.] Proof search time: 0 min, 43 sec Number of successful tactic applications: 2711 Number of failed tactic applications: 7290 Results for fold 76 Results for lemma negate_cmpu: : forall valid_ptr c x y, cmpu valid_ptr (negate_comparison c) x y = notbool (cmpu valid_ptr c x y) FAILURE! Tactics applied: 10000 Original Proof: [intros. unfold cmpu. rewrite negate_cmpu_bool. apply not_of_optbool.] Proof search time: 0 min, 49 sec Number of successful tactic applications: 1823 Number of failed tactic applications: 8178 Results for fold 77 Results for lemma xor_assoc: : forall x y z, xor (xor x y) z = xor x (xor y z) FAILURE! Tactics applied: 10000 Original Proof: [destruct x; destruct y; destruct z; simpl; auto. decEq. apply Int.xor_assoc.] Proof search time: 1 min, 9 sec Number of successful tactic applications: 2841 Number of failed tactic applications: 7160 Results for fold 78 Results for lemma mul_add_distr_l: : forall x y z, mul (add x y) z = add (mul x z) (mul y z) FAILURE! Tactics applied: 10000 Original Proof: [destruct x; destruct y; destruct z; simpl; auto. decEq. apply Int.mul_add_distr_l.] Proof search time: 0 min, 39 sec Number of successful tactic applications: 2595 Number of failed tactic applications: 7406 Results for fold 79 Results for lemma swap_cmp_bool: : forall c x y, cmp_bool (swap_comparison c) x y = cmp_bool c y x FAILURE! Tactics applied: 10000 Original Proof: [destruct x; destruct y; simpl; auto. rewrite Int.swap_cmp. auto.] Proof search time: 0 min, 35 sec Number of successful tactic applications: 1882 Number of failed tactic applications: 8119 Results for fold 80 Results for lemma negate_cmpu_bool: : forall valid_ptr c x y, cmpu_bool valid_ptr (negate_comparison c) x y = option_map negb (cmpu_bool valid_ptr c x y) FAILURE! Tactics applied: 10000 Original Proof: [assert (forall c, cmp_different_blocks (negate_comparison c) = option_map negb (cmp_different_blocks c)). destruct c; auto. destruct x; destruct y; simpl; auto. rewrite Int.negate_cmpu. auto. destruct (Int.eq i Int.zero); auto. destruct (Int.eq i0 Int.zero); auto. destruct (eq_block b b0). destruct ((valid_ptr b (Int.unsigned i) || valid_ptr b (Int.unsigned i - 1)) && (valid_ptr b0 (Int.unsigned i0) || valid_ptr b0 (Int.unsigned i0 - 1))). rewrite Int.negate_cmpu. auto. auto. destruct (valid_ptr b (Int.unsigned i) && valid_ptr b0 (Int.unsigned i0)); auto.] Proof search time: 0 min, 34 sec Number of successful tactic applications: 1875 Number of failed tactic applications: 8126 Results for fold 81 Results for lemma lessdef_trans: : forall v1 v2 v3, lessdef v1 v2 -> lessdef v2 v3 -> lessdef v1 v3 SUCCESS! Proof Found in EFSM: induction 1; auto. econstructor. Tactics applied: 1555 Original Proof: [intros. inv H. auto. constructor.] Shorter Proof Found? yes This is a novel proof proof search time: 0 min, 25 sec Number of successful tactic applications: 248 Number of failed tactic applications: 1307 Results for fold 82 Results for lemma mul_assoc: : forall x y z, mul (mul x y) z = mul x (mul y z) FAILURE! Tactics applied: 10000 Original Proof: [destruct x; destruct y; destruct z; simpl; auto. decEq. apply Int.mul_assoc.] Proof search time: 0 min, 48 sec Number of successful tactic applications: 1882 Number of failed tactic applications: 8119 Results for fold 83 Results for lemma xor_commut: : forall x y, xor x y = xor y x FAILURE! Tactics applied: 10000 Original Proof: [destruct x; destruct y; simpl; auto. decEq. apply Int.xor_commut.] Proof search time: 0 min, 22 sec Number of successful tactic applications: 1356 Number of failed tactic applications: 8645 Results for fold 84 Results for lemma modu_pow2: : forall x n logn y, Int.is_power2 n = Some logn -> modu x (Vint n) = Some y -> and x (Vint (Int.sub n Int.one)) = y FAILURE! Tactics applied: 10000 Original Proof: [intros; destruct x; simpl in H0; inv H0. destruct (Int.eq n Int.zero); inv H2. simpl. decEq. symmetry. eapply Int.modu_and; eauto.] Proof search time: 0 min, 43 sec Number of successful tactic applications: 2105 Number of failed tactic applications: 7896 Results for fold 85 Results for lemma sub_add_opp: : forall x y, sub x (Vint y) = add x (Vint (Int.neg y)) FAILURE! Tactics applied: 10000 Original Proof: [destruct x; intro y; simpl; auto; rewrite Int.sub_add_opp; auto.] Proof search time: 0 min, 30 sec Number of successful tactic applications: 2487 Number of failed tactic applications: 7514 Results for fold 86 Results for lemma rolm_lt_zero: : forall v, rolm v Int.one Int.one = cmp Clt v (Vint Int.zero) FAILURE! Tactics applied: 10000 Original Proof: [intros. unfold cmp, cmp_bool; destruct v; simpl; auto. transitivity (Vint (Int.shru i (Int.repr (Int.zwordsize - 1)))). decEq. symmetry. rewrite Int.shru_rolm. auto. auto. rewrite Int.shru_lt_zero. destruct (Int.lt i Int.zero); auto.] Proof search time: 0 min, 43 sec Number of successful tactic applications: 2014 Number of failed tactic applications: 7987 Results for fold 87 Results for lemma rolm_ge_zero: : forall v, xor (rolm v Int.one Int.one) (Vint Int.one) = cmp Cge v (Vint Int.zero) FAILURE! Tactics applied: 10000 Original Proof: [intros. rewrite rolm_lt_zero. destruct v; simpl; auto. unfold cmp; simpl. destruct (Int.lt i Int.zero); auto.] Proof search time: 0 min, 33 sec Number of successful tactic applications: 1964 Number of failed tactic applications: 8037 Results for fold 88 Results for lemma cmpu_ne_0_optbool: : forall valid_ptr ob, cmpu valid_ptr Cne (of_optbool ob) (Vint Int.zero) = of_optbool ob FAILURE! Tactics applied: 10000 Original Proof: [intros. destruct ob; simpl; auto. destruct b; auto.] Proof search time: 0 min, 33 sec Number of successful tactic applications: 2050 Number of failed tactic applications: 7951 Results for fold 89 Results for lemma sub_add_l: : forall v1 v2 i, sub (add v1 (Vint i)) v2 = add (sub v1 v2) (Vint i) FAILURE! Tactics applied: 10000 Original Proof: [destruct v1; destruct v2; intros; simpl; auto. rewrite Int.sub_add_l. auto. rewrite Int.sub_add_l. auto. case (eq_block b b0); intro. rewrite Int.sub_add_l. auto. reflexivity.] Proof search time: 0 min, 36 sec Number of successful tactic applications: 1897 Number of failed tactic applications: 8104 Results for fold 90 Results for lemma add_permut: : forall x y z, add x (add y z) = add y (add x z) FAILURE! Tactics applied: 10000 Original Proof: [intros. rewrite (add_commut y z). rewrite <- add_assoc. apply add_commut.] Proof search time: 0 min, 31 sec Number of successful tactic applications: 1598 Number of failed tactic applications: 8403 Results for fold 91 Results for lemma swap_cmpu_bool: : forall valid_ptr c x y, cmpu_bool valid_ptr (swap_comparison c) x y = cmpu_bool valid_ptr c y x FAILURE! Tactics applied: 10000 Original Proof: [assert (forall c, cmp_different_blocks (swap_comparison c) = cmp_different_blocks c). destruct c; auto. destruct x; destruct y; simpl; auto. rewrite Int.swap_cmpu. auto. case (Int.eq i Int.zero); auto. case (Int.eq i0 Int.zero); auto. destruct (eq_block b b0); subst. rewrite dec_eq_true. destruct (valid_ptr b0 (Int.unsigned i) || valid_ptr b0 (Int.unsigned i - 1)); destruct (valid_ptr b0 (Int.unsigned i0) || valid_ptr b0 (Int.unsigned i0 - 1)); simpl; auto. rewrite Int.swap_cmpu. auto. rewrite dec_eq_false by auto. destruct (valid_ptr b (Int.unsigned i)); destruct (valid_ptr b0 (Int.unsigned i0)); simpl; auto.] Proof search time: 0 min, 45 sec Number of successful tactic applications: 1854 Number of failed tactic applications: 8147 Results for fold 92 Results for lemma singleoffloat_lessdef: : forall v1 v2, lessdef v1 v2 -> lessdef (singleoffloat v1) (singleoffloat v2) SUCCESS! Proof Found in EFSM: induction 1; auto. Tactics applied: 106 Original Proof: [intros; inv H; simpl; auto.] Shorter Proof Found? yes This is a novel proof proof search time: 0 min, 12 sec Number of successful tactic applications: 13 Number of failed tactic applications: 93 Results for fold 93 Results for lemma cmpu_eq_1_optbool: : forall valid_ptr ob, cmpu valid_ptr Ceq (of_optbool ob) (Vint Int.one) = of_optbool ob SUCCESS! Proof Found in EFSM: destruct ob; auto. destruct b; split ; Tactics applied: 4742 Original Proof: [intros. destruct ob; simpl; auto. destruct b; auto.] Shorter Proof Found? yes This is a novel proof proof search time: 0 min, 24 sec Number of successful tactic applications: 638 Number of failed tactic applications: 4104 Results for fold 94 Results for lemma loword_lessdef: : forall v v', lessdef v v' -> lessdef (loword v) (loword v') SUCCESS! Proof Found in EFSM: induction 1; intuition. Tactics applied: 65 Original Proof: [intros. inv H; auto.] Shorter Proof Found? yes This is a novel proof proof search time: 0 min, 9 sec Number of successful tactic applications: 15 Number of failed tactic applications: 50 Results for fold 95 Results for lemma notbool_negb_2: : forall b, of_bool b = notbool (of_bool (negb b)) SUCCESS! Proof Found in EFSM: destruct b; reflexivity. Tactics applied: 417 Original Proof: [destruct b; reflexivity.] Shorter Proof Found? no Proof reused from notbool_negb_1 proof search time: 0 min, 8 sec Number of successful tactic applications: 62 Number of failed tactic applications: 355 Results for fold 96 Results for lemma negate_cmpf_eq: : forall v1 v2, notbool (cmpf Cne v1 v2) = cmpf Ceq v1 v2 FAILURE! Tactics applied: 10000 Original Proof: [destruct v1; destruct v2; auto. unfold cmpf, cmpf_bool. rewrite Float.cmp_ne_eq. destruct (Float.cmp Ceq f f0); auto.] Proof search time: 0 min, 28 sec Number of successful tactic applications: 1562 Number of failed tactic applications: 8439 Results for fold 97 Results for lemma lessdef_list_inv: : forall vl1 vl2, lessdef_list vl1 vl2 -> vl1 = vl2 \/ In Vundef vl1 FAILURE! Tactics applied: 10000 Original Proof: [induction 1; simpl. tauto. inv H. destruct IHlessdef_list. left; congruence. tauto. tauto.] Proof search time: 1 min, 19 sec Number of successful tactic applications: 1856 Number of failed tactic applications: 8145 Results for fold 98 Results for lemma divu_pow2: : forall x n logn y, Int.is_power2 n = Some logn -> divu x (Vint n) = Some y -> shru x (Vint logn) = y FAILURE! Tactics applied: 10000 Original Proof: [intros; destruct x; simpl in H0; inv H0. destruct (Int.eq n Int.zero); inv H2. simpl. rewrite (Int.is_power2_range _ _ H). decEq. symmetry. apply Int.divu_pow2. auto.] Proof search time: 0 min, 41 sec Number of successful tactic applications: 1855 Number of failed tactic applications: 8146 Results for fold 99 Results for lemma lessdef_same: : forall v1 v2, v1 = v2 -> lessdef v1 v2 SUCCESS! Proof Found in EFSM: induction 1; intros ; econstructor. Tactics applied: 551 Original Proof: [intros. subst v2. constructor.] Shorter Proof Found? no This is a novel proof proof search time: 0 min, 14 sec Number of successful tactic applications: 93 Number of failed tactic applications: 458 OVERALL RESULTS SUMMARY EFSMProver proved 25 out of 99 lemmas. Success rate of 25.252525252525253% There were 0 errors. 74 proof attempts exhausted the automaton On average, a proof was found after applying 1555 tactics The longest proof consisted of 4 tactics There were 16 shorter proofs found Of the 74 failures, 74 of them used all 10000 tactics There were 6 reused proofs found There were 19 novel proofs found Of the 74 failures, the average number of tactics used was 10000 On average, a proof was found after 0 min, 16 sec On average, a failed proof attempt took 0 min, 45 sec On average, any (success or failure) proof attempt took 0 min, 38 sec The longest time to find a proof was 0 min, 36 sec The shortest time to find a proof was 0 min, 7 sec There were 1 proofs containing repeated tactics There were 1 proofs that repeated states