Results for fold 1 Results for lemma subset_mem_1: : (forall a, mem a s=true->mem a s'=true) -> subset s s'=true FAILURE! Tactics applied: 2578 Original Proof: [intros; apply subset_1; unfold Subset; intros a. do 2 rewrite mem_iff; auto.] Proof search time: 0 min, 14 sec Results for lemma for_all_mem_3: : forall s x,(mem x s)=true -> (f x)=false -> (for_all f s)=false FAILURE! Tactics applied: 2246 Original Proof: [intros. apply (bool_eq_ind (for_all f s));intros;auto. rewrite for_all_filter in H1; auto. rewrite is_empty_equal_empty in H1. generalize (equal_mem_2 _ _ H1 x). rewrite filter_b; auto. rewrite empty_mem. rewrite H. rewrite H0. simpl;auto.] Proof search time: 0 min, 13 sec Results for lemma remove_mem_2: : ~E.eq x y -> mem y (remove x s)=mem y s FAILURE! Tactics applied: 2406 Original Proof: [apply remove_neq_b.] Proof search time: 0 min, 13 sec Results for lemma sum_compat: : forall f g, Proper (E.eq==>Logic.eq) f -> Proper (E.eq==>Logic.eq) g -> forall s, (forall x, In x s -> f x=g x) -> sum f s=sum g s FAILURE! Tactics applied: 2161 Original Proof: [intros. unfold sum; apply (@fold_compat _ (@Logic.eq nat)); repeat red; auto with *.] Proof search time: 0 min, 19 sec Results for lemma diff_subset: : subset (diff s s') s=true SUCCESS! Proof Found in EFSM: [auto with set ] Tactics applied: 1 Original Proof: [auto with set.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 3 sec Results for lemma union_filter: : forall f g, Proper (E.eq==>Logic.eq) f -> Proper (E.eq==>Logic.eq) g -> forall s, union (filter f s) (filter g s) [=] filter (fun x=>orb (f x) (g x)) s FAILURE! Tactics applied: 2287 Original Proof: [clear Comp' Comp f. intros. assert (Proper (E.eq==>Logic.eq) (fun x => orb (f x) (g x))). repeat red; intros. rewrite (H x y H1); rewrite (H0 x y H1); auto. unfold Equal; intros; set_iff; repeat rewrite filter_iff; auto. assert (f a || g a = true <-> f a = true \/ g a = true). split; auto with bool. intro H3; destruct (orb_prop _ _ H3); auto. tauto.] Proof search time: 0 min, 18 sec Results for lemma choose_mem_1: : choose s=Some x -> mem x s=true SUCCESS! Proof Found in EFSM: [auto with set ] Tactics applied: 1 Original Proof: [auto with set.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 2 sec Results for lemma add_mem_3: : mem y s=true -> mem y (add x s)=true SUCCESS! Proof Found in EFSM: [auto with set ] Tactics applied: 1 Original Proof: [auto with set.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 2 sec Results for lemma add_filter_1: : forall s s' x, f x=true -> (Add x s s') -> (Add x (filter f s) (filter f s')) FAILURE! Tactics applied: 2278 Original Proof: [unfold Add, MP.Add; intros. repeat rewrite filter_iff; auto. rewrite H0; clear H0. intuition. setoid_replace y with x; auto with relations.] Proof search time: 0 min, 12 sec Results for lemma for_all_mem_4: : forall s, for_all f s=false -> {x:elt | mem x s=true /\ f x=false} FAILURE! Tactics applied: 2034 Original Proof: [intros. rewrite for_all_filter in H; auto. destruct (choose_mem_3 _ H) as (x,(H0,H1));intros. exists x. rewrite filter_b in H1; auto. elim (andb_prop _ _ H1). split;auto. rewrite <- negb_true_iff; auto.] Proof search time: 0 min, 13 sec Results for lemma mem_3: : ~In x s -> mem x s=false FAILURE! Tactics applied: 2246 Original Proof: [intros; rewrite <- not_mem_iff; auto.] Proof search time: 0 min, 11 sec