Results for fold 1 Results for lemma test_eq_neq_trans_1: : forall w x y z s, E.eq x w -> ~ ~ E.eq x y -> ~ E.eq y z -> In w s -> In w (remove z s) SUCCESS! Proof Found in EFSM: fsetdec. Tactics applied: 22 Original Proof: [fsetdec.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Number of successful tactic applications: 13 Number of failed tactic applications: 9 Results for fold 2 Results for lemma test_eq_neq_trans_2: : forall w x y z r1 r2 s, In x (singleton w) -> ~ In x r1 -> In x (add y r1) -> In y r2 -> In y (remove z r2) -> In w s -> In w (remove z s) SUCCESS! Proof Found in EFSM: fsetdec. Tactics applied: 22 Original Proof: [fsetdec.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Number of successful tactic applications: 13 Number of failed tactic applications: 9 Results for fold 3 Results for lemma test_not_In_disj: : forall x y s1 s2 s3 s4, ~ In x (union s1 (union s2 (union s3 (add y s4)))) -> ~ (In x s1 \/ In x s4 \/ E.eq y x) SUCCESS! Proof Found in EFSM: fsetdec. Tactics applied: 8 Original Proof: [fsetdec.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Number of successful tactic applications: 4 Number of failed tactic applications: 4 Results for fold 4 Results for lemma eq_refl_iff: (x : E.t) : E.eq x x <-> True FAILURE! Tactics applied: 218 Original Proof: [now split.] Proof search time: 0 min, 0 sec Number of successful tactic applications: 19 Number of failed tactic applications: 199 Results for fold 5 Results for lemma test_Subset_add_remove: : forall x s, s [<=] (add x (remove x s)) SUCCESS! Proof Found in EFSM: fsetdec. Tactics applied: 22 Original Proof: [fsetdec.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Number of successful tactic applications: 12 Number of failed tactic applications: 10 Results for fold 6 Results for lemma test_eq_trans_2: : forall x y z r s, In x (singleton y) -> ~ In z r -> ~ ~ In z (add y r) -> In x s -> In z s SUCCESS! Proof Found in EFSM: fsetdec. Tactics applied: 22 Original Proof: [fsetdec.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Number of successful tactic applications: 13 Number of failed tactic applications: 9 Results for fold 7 Results for lemma test_add_In: : forall x y s, In x (add y s) -> ~ E.eq x y -> In x s SUCCESS! Proof Found in EFSM: fsetdec. Tactics applied: 22 Original Proof: [fsetdec.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Number of successful tactic applications: 12 Number of failed tactic applications: 10 Results for fold 8 Results for lemma test_eq_disjunction: : forall w x y z, In w (add x (add y (singleton z))) -> E.eq w x \/ E.eq w y \/ E.eq w z SUCCESS! Proof Found in EFSM: fsetdec. Tactics applied: 22 Original Proof: [fsetdec.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Number of successful tactic applications: 8 Number of failed tactic applications: 14 Results for fold 9 Results for lemma test_set_ops_1: : forall x q r s, (singleton x) [<=] s -> Empty (union q r) -> Empty (inter (diff s q) (diff s r)) -> ~ In x s SUCCESS! Proof Found in EFSM: fsetdec. Tactics applied: 22 Original Proof: [fsetdec.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Number of successful tactic applications: 15 Number of failed tactic applications: 7 Results for fold 10 Results for lemma dec_In: : forall x s, decidable (In x s) FAILURE! Tactics applied: 1614 Original Proof: [red; intros; generalize (F.mem_iff s x); case (mem x s); intuition.] Proof search time: 0 min, 2 sec Number of successful tactic applications: 137 Number of failed tactic applications: 1477 Results for fold 11 Results for lemma test_too_complex: : forall x y z r s, E.eq x y -> (In x (singleton y) -> r [<=] s) -> In z r -> In z s FAILURE! Tactics applied: 1760 Original Proof: [(** [fsetdec] is not intended to solve this directly. *) intros until s; intros Heq H Hr; lapply H; fsetdec.] Proof search time: 0 min, 11 sec Number of successful tactic applications: 869 Number of failed tactic applications: 891 Results for fold 12 Results for lemma test_iff_conj: : forall a x s s', (In a s' <-> E.eq x a \/ In a s) -> (In a s' <-> In a (add x s)) SUCCESS! Proof Found in EFSM: fsetdec. Tactics applied: 22 Original Proof: [fsetdec.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Number of successful tactic applications: 14 Number of failed tactic applications: 8 Results for fold 13 Results for lemma test_push: : forall P Q R : Prop, decidable P -> decidable Q -> (~ True) -> (~ False) -> (~ ~ P) -> (~ (P /\ Q) -> ~ R) -> ((P /\ Q) \/ ~ R) -> (~ (P /\ Q) \/ R) -> (R \/ ~ (P /\ Q)) -> (~ R \/ (P /\ Q)) -> (~ P -> R) -> (~ ((R -> P) \/ (Q -> R))) -> (~ (P /\ R)) -> (~ (P -> R)) -> True SUCCESS! Proof Found in EFSM: now split. Tactics applied: 1 Original Proof: [intros. push not in *. (* note that ~(R->P) remains (since R isnt decidable) *) tauto.] Shorter Proof Found? yes Single step proof reused proof search time: 0 min, 0 sec Number of successful tactic applications: 1 Number of failed tactic applications: 0 Results for fold 14 Results for lemma test_eq_trans_1: : forall x y z s, E.eq x y -> ~ ~ E.eq z y -> In x s -> In z s SUCCESS! Proof Found in EFSM: fsetdec. Tactics applied: 22 Original Proof: [fsetdec.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Number of successful tactic applications: 13 Number of failed tactic applications: 9 Results for fold 15 Results for lemma dec_eq: : forall (x y : E.t), decidable (E.eq x y) FAILURE! Tactics applied: 75 Original Proof: [red; intros x y; destruct (E.eq_dec x y); auto.] Proof search time: 0 min, 0 sec Number of successful tactic applications: 14 Number of failed tactic applications: 61 Results for fold 16 Results for lemma test_pull: : forall P Q R : Prop, decidable P -> decidable Q -> (~ True) -> (~ False) -> (~ ~ P) -> (~ (P /\ Q) -> ~ R) -> ((P /\ Q) \/ ~ R) -> (~ (P /\ Q) \/ R) -> (R \/ ~ (P /\ Q)) -> (~ R \/ (P /\ Q)) -> (~ P -> R) -> (~ (R -> P) /\ ~ (Q -> R)) -> (~ P \/ ~ R) -> (P /\ ~ R) -> (~ R /\ P) -> True SUCCESS! Proof Found in EFSM: now split. Tactics applied: 2 Original Proof: [intros. pull not in *. tauto.] Shorter Proof Found? yes Single step proof reused proof search time: 0 min, 0 sec Number of successful tactic applications: 1 Number of failed tactic applications: 1 Results for fold 17 Results for lemma function_test_2: : forall (f : t -> t), forall (g : elt -> elt), forall (s1 s2 : t), forall (x1 x2 : elt), Equal s1 (f s2) -> E.eq x1 (g x2) -> In x1 s1 -> g x2 = g (g x2) -> In (g (g x2)) (f s2) SUCCESS! Proof Found in EFSM: fsetdec. Tactics applied: 19 Original Proof: [(** [fsetdec] is not intended to solve this directly. *) intros until 3. intros g_eq. rewrite <- g_eq. fsetdec.] Shorter Proof Found? yes Single step proof reused proof search time: 0 min, 0 sec Number of successful tactic applications: 7 Number of failed tactic applications: 12 Results for fold 18 Results for lemma test_not_In_conj: : forall x y s1 s2 s3 s4, ~ In x (union s1 (union s2 (union s3 (add y s4)))) -> ~ In x s1 /\ ~ In x s4 /\ ~ E.eq y x SUCCESS! Proof Found in EFSM: fsetdec. Tactics applied: 22 Original Proof: [fsetdec.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Number of successful tactic applications: 10 Number of failed tactic applications: 12 Results for fold 19 Results for lemma test_baydemir: : forall (f : t -> t), forall (s : t), forall (x y : elt), In x (add y (f s)) -> ~ E.eq x y -> In x (f s) SUCCESS! Proof Found in EFSM: fsetdec. Tactics applied: 22 Original Proof: [fsetdec.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Number of successful tactic applications: 12 Number of failed tactic applications: 10 Results for fold 20 Results for lemma function_test_1: : forall (f : t -> t), forall (g : elt -> elt), forall (s1 s2 : t), forall (x1 x2 : elt), Equal s1 (f s2) -> E.eq x1 (g (g x2)) -> In x1 s1 -> In (g (g x2)) (f s2) SUCCESS! Proof Found in EFSM: fsetdec. Tactics applied: 22 Original Proof: [fsetdec.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Number of successful tactic applications: 9 Number of failed tactic applications: 13 Results for fold 21 Results for lemma eq_chain_test: : forall x1 x2 x3 x4 s1 s2 s3 s4, Empty s1 -> In x2 (add x1 s1) -> In x3 s2 -> ~ In x3 (remove x2 s2) -> ~ In x4 s3 -> In x4 (add x3 s3) -> In x1 s4 -> Subset (add x4 s4) s4 SUCCESS! Proof Found in EFSM: fsetdec. Tactics applied: 22 Original Proof: [fsetdec.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Number of successful tactic applications: 13 Number of failed tactic applications: 9 Results for fold 22 Results for lemma test_In_singleton: : forall x, In x (singleton x) SUCCESS! Proof Found in EFSM: fsetdec. Tactics applied: 22 Original Proof: [fsetdec.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Number of successful tactic applications: 4 Number of failed tactic applications: 18 OVERALL RESULTS SUMMARY EFSMProver proved 18 out of 22 lemmas. Success rate of 81.81818181818183% There were 0 errors. 4 proof attempts exhausted the automaton On average, a proof was found after applying 18 tactics The longest proof consisted of 1 tactics There were 3 shorter proofs found Of the 4 failures, 0 of them used all 10000 tactics There were 18 reused proofs found There were 0 novel proofs found Of the 4 failures, the average number of tactics used was 916 On average, a proof was found after 0 min, 0 sec On average, a failed proof attempt took 0 min, 3 sec On average, any (success or failure) proof attempt took 0 min, 0 sec The longest time to find a proof was 0 min, 0 sec The shortest time to find a proof was 0 min, 0 sec There were 0 proofs containing repeated tactics There were 0 proofs that repeated states