Results for fold 1 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: 9 Original Proof: [fsetdec.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 1 sec 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: 9 Original Proof: [fsetdec.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 1 sec Results for lemma dec_In: : forall x s, decidable (In x s) FAILURE! Tactics applied: 100000 Original Proof: [red; intros; generalize (F.mem_iff s x); case (mem x s); intuition.] Proof search time: 2 min, 52 sec Results for fold 2 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: 14 Original Proof: [fsetdec.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 1 sec Results for lemma test_Subset_add_remove: : forall x s, s [<=] (add x (remove x s)) SUCCESS! Proof Found in EFSM: [fsetdec ] Tactics applied: 14 Original Proof: [fsetdec.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 1 sec Results for lemma eq_refl_iff: (x : E.t) : E.eq x x <-> True SUCCESS! Proof Found in EFSM: [intuition ] Tactics applied: 13 Original Proof: [now split.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 1 sec Results for fold 3 Results for lemma test_In_singleton: : forall x, In x (singleton x) SUCCESS! Proof Found in EFSM: [intuition ] Tactics applied: 7 Original Proof: [fsetdec.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 1 sec 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: 5 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, 1 sec 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: 11 Original Proof: [fsetdec.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 1 sec Results for fold 4 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: 9 Original Proof: [fsetdec.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 1 sec 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: 9 Original Proof: [fsetdec.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 1 sec 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: 9 Original Proof: [fsetdec.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 1 sec Results for fold 5 Results for lemma dec_eq: : forall (x y : E.t), decidable (E.eq x y) FAILURE! Tactics applied: 100000 Original Proof: [red; intros x y; destruct (E.eq_dec x y); auto.] Proof search time: 5 min, 6 sec 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: 7 Original Proof: [fsetdec.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 1 sec 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: 5 Original Proof: [intros. pull not in *. tauto.] Shorter Proof Found? yes Single step proof reused proof search time: 0 min, 1 sec Results for fold 6 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: 15 Original Proof: [fsetdec.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 1 sec 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: 15 Original Proof: [fsetdec.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 1 sec 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: 15 Original Proof: [fsetdec.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 1 sec Results for fold 7 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: 100000 Original Proof: [(** [fsetdec] is not intended to solve this directly. *) intros until s; intros Heq H Hr; lapply H; fsetdec.] Proof search time: 10 min, 51 sec 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: 2 Original Proof: [fsetdec.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 7 sec 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: 2 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, 1 sec Results for fold 8 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: 13 Original Proof: [fsetdec.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 2 sec OVERALL RESULTS SUMMARY EFSMProver proved 19 out of 22 lemmas. Success rate of 86.36363636363636% There were 0 errors. 3 proof attempts exhausted the automaton On average, a proof was found after applying 9 tactics The longest proof consisted of 1 tactics There were 3 shorter proofs found Of the 3 failures, 3 of them used all 100000 tactics There were 19 reused proofs found There were 0 novel proofs found Of the 3 failures, the average number of tactics used was 100000 On average, a proof was found after 0 min, 1 sec On average, a failed proof attempt took 6 min, 16 sec On average, any (success or failure) proof attempt took 0 min, 52 sec The longest time to find a proof was 0 min, 7 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