Results for fold 1 Results for lemma singleton_1: : In y (singleton x) -> E.eq x y FAILURE! Tactics applied: 10000 Original Proof: [rewrite singleton_spec; auto with relations.] Proof search time: 0 min, 28 sec Results for lemma remove_2: : ~ E.eq x y -> In y s -> In y (remove x s) FAILURE! Tactics applied: 10000 Original Proof: [intros; apply <- remove_spec; auto with relations.] Proof search time: 0 min, 29 sec Results for lemma union_2: : In x s -> In x (union s s') FAILURE! Tactics applied: 10000 Original Proof: [rewrite union_spec; auto.] Proof search time: 0 min, 24 sec Results for lemma for_all_iff: : Proper (E.eq==>Logic.eq) f -> (For_all (fun x => f x = true) s <-> for_all f s = true) SUCCESS! Proof Found in EFSM: [intuition ] Tactics applied: 76 Original Proof: [intros; apply iff_sym, for_all_spec; auto.] Shorter Proof Found? yes Single step proof reused proof search time: 0 min, 3 sec Results for lemma remove_3: : In y (remove x s) -> In y s FAILURE! Tactics applied: 10000 Original Proof: [rewrite remove_spec; intuition.] Proof search time: 0 min, 21 sec Results for lemma remove_iff: : In y (remove x s) <-> In y s /\ ~E.eq x y FAILURE! Tactics applied: 10000 Original Proof: [rewrite remove_spec; intuition.] Proof search time: 0 min, 34 sec Results for lemma mem_iff: : In x s <-> mem x s = true SUCCESS! Proof Found in EFSM: [intuition ] Tactics applied: 65 Original Proof: [apply iff_sym, mem_spec.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 2 sec Results for fold 2 Results for lemma not_mem_iff: : ~In x s <-> mem x s = false FAILURE! Tactics applied: 1 Original Proof: [rewrite <-mem_spec; destruct (mem x s); intuition.] Proof search time: 0 min, 3 sec Results for lemma In_1: : E.eq x y -> In x s -> In y s FAILURE! Tactics applied: 10000 Original Proof: [intros E; rewrite E; auto.] Proof search time: 0 min, 13 sec Results for lemma remove_1: : E.eq x y -> ~ In y (remove x s) FAILURE! Tactics applied: 10000 Original Proof: [intros; rewrite remove_spec; intuition.] Proof search time: 0 min, 13 sec Results for lemma inter_b: : mem x (inter s s') = mem x s && mem x s' FAILURE! Tactics applied: 1 Original Proof: [generalize (mem_iff (inter s s') x)(mem_iff s x)(mem_iff s' x)(inter_iff s s' x). destruct (mem x s); destruct (mem x s'); destruct (mem x (inter s s')); intuition.] Proof search time: 0 min, 3 sec Results for lemma inter_3: : In x s -> In x s' -> In x (inter s s') FAILURE! Tactics applied: 10000 Original Proof: [rewrite inter_spec; intuition.] Proof search time: 0 min, 13 sec Results for lemma elements_b: : mem x s = existsb (eqb x) (elements s) FAILURE! Tactics applied: 1 Original Proof: [generalize (mem_iff s x)(elements_iff s x)(existsb_exists (eqb x) (elements s)). rewrite InA_alt. destruct (mem x s); destruct (existsb (eqb x) (elements s)); auto; intros. symmetry. rewrite H1. destruct H0 as (H0,_). destruct H0 as (a,(Ha1,Ha2)); [ intuition |]. exists a; intuition. unfold eqb; destruct (eq_dec x a); auto. rewrite <- H. rewrite H0. destruct H1 as (H1,_). destruct H1 as (a,(Ha1,Ha2)); [intuition|]. exists a; intuition. unfold eqb in *; destruct (eq_dec x a); auto; discriminate.] Proof search time: 0 min, 4 sec Results for lemma for_all_2: : compatb f -> for_all f s = true -> For_all (fun x => f x = true) s FAILURE! Tactics applied: 10000 Original Proof: [intros; apply -> for_all_spec; auto.] Proof search time: 0 min, 14 sec Results for fold 3 Results for lemma remove_neq_iff: : ~ E.eq x y -> (In y (remove x s) <-> In y s) FAILURE! Tactics applied: 10000 Original Proof: [rewrite remove_spec; intuition.] Proof search time: 0 min, 12 sec Results for lemma filter_b: : Proper (E.eq==>Logic.eq) f -> mem x (filter f s) = mem x s && f x FAILURE! Tactics applied: 10000 Original Proof: [intros. generalize (mem_iff (filter f s) x)(mem_iff s x)(filter_iff s x H). destruct (mem x s); destruct (mem x (filter f s)); destruct (f x); simpl; intuition.] Proof search time: 0 min, 16 sec Results for lemma union_b: : mem x (union s s') = mem x s || mem x s' FAILURE! Tactics applied: 10000 Original Proof: [generalize (mem_iff (union s s') x)(mem_iff s x)(mem_iff s' x)(union_iff s s' x). destruct (mem x s); destruct (mem x s'); destruct (mem x (union s s')); intuition.] Proof search time: 0 min, 11 sec Results for lemma empty_b: : mem y empty = false FAILURE! Tactics applied: 10000 Original Proof: [generalize (empty_iff y)(mem_iff empty y). destruct (mem y empty); intuition.] Proof search time: 0 min, 10 sec Results for lemma subset_1: : Subset s s' -> subset s s' = true FAILURE! Tactics applied: 10000 Original Proof: [intros; apply <- subset_spec; auto.] Proof search time: 0 min, 11 sec Results for lemma is_empty_2: : is_empty s = true -> Empty s SUCCESS! Proof Found in EFSM: [apply iff_sym, is_empty_spec ] Tactics applied: 43 Original Proof: [intros; apply -> is_empty_spec; auto.] Shorter Proof Found? yes Single step proof reused proof search time: 0 min, 1 sec Results for lemma union_3: : In x s' -> In x (union s s') FAILURE! Tactics applied: 10000 Original Proof: [rewrite union_spec; auto.] Proof search time: 0 min, 10 sec Results for fold 4 Results for lemma for_all_b: : Proper (E.eq==>Logic.eq) f -> for_all f s = forallb f (elements s) FAILURE! Tactics applied: 10000 Original Proof: [intros. generalize (forallb_forall f (elements s))(for_all_iff s H)(elements_iff s). unfold For_all. destruct (forallb f (elements s)); destruct (for_all f s); auto; intros. rewrite <- H1; intros. destruct H0 as (H0,_). rewrite (H2 x0) in H3. rewrite (InA_alt E.eq x0 (elements s)) in H3. destruct H3 as (a,(Ha1,Ha2)). rewrite (H _ _ Ha1). apply H0; auto. symmetry. rewrite H0; intros. destruct H1 as (_,H1). apply H1; auto. rewrite H2. rewrite InA_alt. exists x0; split; auto with relations.] Proof search time: 0 min, 26 sec Results for lemma filter_1: : compatb f -> In x (filter f s) -> In x s FAILURE! Tactics applied: 10000 Original Proof: [intros P; rewrite filter_spec; intuition.] Proof search time: 0 min, 23 sec Results for lemma equal_2: : equal s s' = true -> Equal s s' SUCCESS! Proof Found in EFSM: [apply iff_sym, equal_spec ] Tactics applied: 24 Original Proof: [intros; apply -> equal_spec; auto.] Shorter Proof Found? yes Single step proof reused proof search time: 0 min, 1 sec Results for lemma union_1: : In x (union s s') -> In x s \/ In x s' FAILURE! Tactics applied: 10000 Original Proof: [rewrite union_spec; auto.] Proof search time: 0 min, 20 sec Results for lemma add_neq_iff: : ~ E.eq x y -> (In y (add x s) <-> In y s) FAILURE! Tactics applied: 10000 Original Proof: [rewrite add_spec; intuition. elim H; auto with relations.] Proof search time: 0 min, 22 sec Results for lemma exists_iff: : Proper (E.eq==>Logic.eq) f -> (Exists (fun x => f x = true) s <-> exists_ f s = true) SUCCESS! Proof Found in EFSM: [intuition ] Tactics applied: 29 Original Proof: [intros; apply iff_sym, exists_spec; auto.] Shorter Proof Found? yes Single step proof reused proof search time: 0 min, 1 sec Results for lemma diff_b: : mem x (diff s s') = mem x s && negb (mem x s') FAILURE! Tactics applied: 10000 Original Proof: [generalize (mem_iff (diff s s') x)(mem_iff s x)(mem_iff s' x)(diff_iff s s' x). destruct (mem x s); destruct (mem x s'); destruct (mem x (diff s s')); simpl; intuition.] Proof search time: 0 min, 21 sec Results for fold 5 Results for lemma elements_1: : In x s -> InA E.eq x (elements s) FAILURE! Tactics applied: 10000 Original Proof: [intros; apply <- elements_spec1; auto.] Proof search time: 0 min, 13 sec Results for lemma is_empty_1: : Empty s -> is_empty s = true FAILURE! Tactics applied: 10000 Original Proof: [intros; apply <- is_empty_spec; auto.] Proof search time: 0 min, 13 sec Results for lemma filter_2: : compatb f -> In x (filter f s) -> f x = true FAILURE! Tactics applied: 10000 Original Proof: [intros P; rewrite filter_spec; intuition.] Proof search time: 0 min, 17 sec Results for lemma In_eq_iff: : E.eq x y -> (In x s <-> In y s) FAILURE! Tactics applied: 10000 Original Proof: [intros E; rewrite E; intuition.] Proof search time: 0 min, 14 sec Results for lemma exists_1: : compatb f -> Exists (fun x => f x = true) s -> exists_ f s = true FAILURE! Tactics applied: 10000 Original Proof: [intros; apply <- exists_spec; auto.] Proof search time: 0 min, 18 sec Results for lemma add_neq_b: : ~ E.eq x y -> mem y (add x s) = mem y s FAILURE! Tactics applied: 10000 Original Proof: [intros; generalize (mem_iff (add x s) y)(mem_iff s y)(add_neq_iff s H). destruct (mem y s); destruct (mem y (add x s)); intuition.] Proof search time: 0 min, 19 sec Results for lemma for_all_1: : compatb f -> For_all (fun x => f x = true) s -> for_all f s = true FAILURE! Tactics applied: 10000 Original Proof: [intros; apply <- for_all_spec; auto.] Proof search time: 0 min, 18 sec Results for fold 6 Results for lemma filter_ext: : forall f f', Proper (E.eq==>Logic.eq) f -> (forall x, f x = f' x) -> forall s s', s[=]s' -> filter f s [=] filter f' s' FAILURE! Tactics applied: 10000 Original Proof: [intros f f' Hf Hff' s s' Hss' x. rewrite 2 filter_iff; auto. rewrite Hff', Hss'; intuition. red; red; intros; rewrite <- 2 Hff'; auto.] Proof search time: 0 min, 11 sec Results for lemma remove_neq_b: : ~ E.eq x y -> mem y (remove x s) = mem y s FAILURE! Tactics applied: 10000 Original Proof: [intros; generalize (mem_iff (remove x s) y)(mem_iff s y)(remove_neq_iff s H). destruct (mem y s); destruct (mem y (remove x s)); intuition.] Proof search time: 0 min, 14 sec Results for lemma diff_3: : In x s -> ~ In x s' -> In x (diff s s') FAILURE! Tactics applied: 10000 Original Proof: [rewrite diff_spec; auto.] Proof search time: 0 min, 10 sec Results for lemma add_iff: : In y (add x s) <-> E.eq x y \/ In y s FAILURE! Tactics applied: 10000 Original Proof: [rewrite add_spec; intuition.] Proof search time: 0 min, 14 sec Results for lemma filter_3: : compatb f -> In x s -> f x = true -> In x (filter f s) FAILURE! Tactics applied: 10000 Original Proof: [intros P; rewrite filter_spec; intuition.] Proof search time: 0 min, 13 sec Results for lemma add_1: : E.eq x y -> In y (add x s) FAILURE! Tactics applied: 10000 Original Proof: [intros; apply <- add_spec. auto with relations.] Proof search time: 0 min, 10 sec Results for lemma remove_b: : mem y (remove x s) = mem y s && negb (eqb x y) FAILURE! Tactics applied: 10000 Original Proof: [generalize (mem_iff (remove x s) y)(mem_iff s y)(remove_iff s x y); unfold eqb. destruct (eq_dec x y); destruct (mem y s); destruct (mem y (remove x s)); simpl; intuition.] Proof search time: 0 min, 14 sec Results for fold 7 Results for lemma exists_2: : compatb f -> exists_ f s = true -> Exists (fun x => f x = true) s FAILURE! Tactics applied: 10000 Original Proof: [intros; apply -> exists_spec; auto.] Proof search time: 0 min, 13 sec Results for lemma elements_2: : InA E.eq x (elements s) -> In x s SUCCESS! Proof Found in EFSM: [apply iff_sym, elements_spec1 ] Tactics applied: 67 Original Proof: [intros; apply -> elements_spec1; auto.] Shorter Proof Found? yes Single step proof reused proof search time: 0 min, 1 sec Results for lemma empty_iff: : In x empty <-> False FAILURE! Tactics applied: 10000 Original Proof: [intuition; apply (empty_spec H).] Proof search time: 0 min, 11 sec Results for lemma inter_1: : In x (inter s s') -> In x s FAILURE! Tactics applied: 10000 Original Proof: [rewrite inter_spec; intuition.] Proof search time: 0 min, 10 sec Results for lemma exists_b: : Proper (E.eq==>Logic.eq) f -> exists_ f s = existsb f (elements s) FAILURE! Tactics applied: 10000 Original Proof: [intros. generalize (existsb_exists f (elements s))(exists_iff s H)(elements_iff s). unfold Exists. destruct (existsb f (elements s)); destruct (exists_ f s); auto; intros. rewrite <- H1; intros. destruct H0 as (H0,_). destruct H0 as (a,(Ha1,Ha2)); auto. exists a; split; auto. rewrite H2; rewrite InA_alt; exists a; auto with relations. symmetry. rewrite H0. destruct H1 as (_,H1). destruct H1 as (a,(Ha1,Ha2)); auto. rewrite (H2 a) in Ha1. rewrite (InA_alt E.eq a (elements s)) in Ha1. destruct Ha1 as (b,(Hb1,Hb2)). exists b; auto. rewrite <- (H _ _ Hb1); auto.] Proof search time: 0 min, 19 sec Results for lemma singleton_iff: : In y (singleton x) <-> E.eq x y SUCCESS! Proof Found in EFSM: [intuition ] Tactics applied: 16 Original Proof: [rewrite singleton_spec; intuition.] Shorter Proof Found? yes Single step proof reused proof search time: 0 min, 1 sec Results for lemma subset_iff: : s[<=]s' <-> subset s s' = true SUCCESS! Proof Found in EFSM: [intuition ] Tactics applied: 17 Original Proof: [apply iff_sym, subset_spec.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 1 sec Results for fold 8 Results for lemma singleton_b: : mem y (singleton x) = eqb x y FAILURE! Tactics applied: 10000 Original Proof: [generalize (mem_iff (singleton x) y)(singleton_iff x y); unfold eqb. destruct (eq_dec x y); destruct (mem y (singleton x)); intuition.] Proof search time: 0 min, 13 sec Results for lemma mem_2: : mem x s = true -> In x s SUCCESS! Proof Found in EFSM: [apply iff_sym, mem_spec ] Tactics applied: 66 Original Proof: [intros; apply -> mem_spec; auto.] Shorter Proof Found? yes Single step proof reused proof search time: 0 min, 1 sec Results for lemma is_empty_iff: : Empty s <-> is_empty s = true SUCCESS! Proof Found in EFSM: [intuition ] Tactics applied: 73 Original Proof: [apply iff_sym, is_empty_spec.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 1 sec Results for lemma equal_1: : Equal s s' -> equal s s' = true FAILURE! Tactics applied: 10000 Original Proof: [intros; apply <- equal_spec; auto.] Proof search time: 0 min, 11 sec Results for lemma add_b: : mem y (add x s) = eqb x y || mem y s FAILURE! Tactics applied: 10000 Original Proof: [generalize (mem_iff (add x s) y)(mem_iff s y)(add_iff s x y); unfold eqb. destruct (eq_dec x y); destruct (mem y s); destruct (mem y (add x s)); intuition.] Proof search time: 0 min, 13 sec Results for lemma mem_b: : E.eq x y -> mem x s = mem y s FAILURE! Tactics applied: 10000 Original Proof: [intros. generalize (mem_iff s x) (mem_iff s y)(In_eq_iff s H). destruct (mem x s); destruct (mem y s); intuition.] Proof search time: 0 min, 13 sec Results for lemma diff_2: : In x (diff s s') -> ~ In x s' FAILURE! Tactics applied: 10000 Original Proof: [rewrite diff_spec; intuition.] Proof search time: 0 min, 11 sec Results for fold 9 Results for lemma elements_iff: : In x s <-> InA E.eq x (elements s) SUCCESS! Proof Found in EFSM: [intuition ] Tactics applied: 81 Original Proof: [apply iff_sym, elements_spec1.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 1 sec Results for lemma add_3: : ~ E.eq x y -> In y (add x s) -> In y s FAILURE! Tactics applied: 10000 Original Proof: [rewrite add_spec. intros H [H'|H']; auto. elim H; auto with relations.] Proof search time: 0 min, 11 sec Results for lemma add_2: : In y s -> In y (add x s) FAILURE! Tactics applied: 10000 Original Proof: [intros; apply <- add_spec; auto.] Proof search time: 0 min, 12 sec Results for lemma equal_iff: : s[=]s' <-> equal s s' = true SUCCESS! Proof Found in EFSM: [intuition ] Tactics applied: 84 Original Proof: [apply iff_sym, equal_spec.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 1 sec Results for lemma diff_1: : In x (diff s s') -> In x s FAILURE! Tactics applied: 10000 Original Proof: [rewrite diff_spec; intuition.] Proof search time: 0 min, 11 sec Results for lemma singleton_2: : E.eq x y -> In y (singleton x) FAILURE! Tactics applied: 10000 Original Proof: [rewrite singleton_spec; auto with relations.] Proof search time: 0 min, 11 sec Results for lemma mem_1: : In x s -> mem x s = true FAILURE! Tactics applied: 10000 Original Proof: [intros; apply <- mem_spec; auto.] Proof search time: 0 min, 15 sec Results for fold 10 Results for lemma subset_2: : subset s s' = true -> Subset s s' SUCCESS! Proof Found in EFSM: [apply iff_sym, subset_spec ] Tactics applied: 84 Original Proof: [intros; apply -> subset_spec; auto.] Shorter Proof Found? yes Single step proof reused proof search time: 0 min, 1 sec Results for lemma inter_2: : In x (inter s s') -> In x s' FAILURE! Tactics applied: 10000 Original Proof: [rewrite inter_spec; intuition.] Proof search time: 0 min, 13 sec OVERALL RESULTS SUMMARY EFSMProver proved 13 out of 65 lemmas. Success rate of 20.0% There were 0 errors. 52 proof attempts exhausted the automaton On average, a proof was found after applying 55 tactics The longest proof consisted of 1 tactics There were 8 shorter proofs found Of the 52 failures, 49 of them used all 10000 tactics There were 13 reused proofs found There were 0 novel proofs found Of the 52 failures, the average number of tactics used was 9423 On average, a proof was found after 0 min, 1 sec On average, a failed proof attempt took 0 min, 15 sec On average, any (success or failure) proof attempt took 0 min, 12 sec The longest time to find a proof was 0 min, 3 sec The shortest time to find a proof was 0 min, 1 sec There were 0 proofs containing repeated tactics There were 0 proofs that repeated states