Results for fold 1
Results for lemma dec_eq: : forall (x y : E.t), decidable (E.eq x y)
FAILURE!
Tactics applied: 25
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: 7
Number of failed tactic applications: 18
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: 8
Original Proof: [fsetdec.]
Shorter Proof Found? no
Single step proof reused
proof search time: 0 min, 0 sec
Number of successful tactic applications: 5
Number of failed tactic applications: 3
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: 8
Original Proof: [fsetdec.]
Shorter Proof Found? no
Single step proof reused
proof search time: 0 min, 0 sec
Number of successful tactic applications: 5
Number of failed tactic applications: 3
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: 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 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: 8
Original Proof: [fsetdec.]
Shorter Proof Found? no
Single step proof reused
proof search time: 0 min, 0 sec
Number of successful tactic applications: 5
Number of failed tactic applications: 3
Results for fold 2
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: 1688
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: 819
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: 3
Original Proof: [fsetdec.]
Shorter Proof Found? no
Single step proof reused
proof search time: 0 min, 0 sec
Number of successful tactic applications: 3
Number of failed tactic applications: 0
Results for lemma test_Subset_add_remove: : forall x s, s [<=] (add x (remove x s))
SUCCESS!
Proof Found in EFSM: fsetdec.
Tactics applied: 3
Original Proof: [fsetdec.]
Shorter Proof Found? no
Single step proof reused
proof search time: 0 min, 0 sec
Number of successful tactic applications: 1
Number of failed tactic applications: 2
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: 3
Original Proof: [fsetdec.]
Shorter Proof Found? no
Single step proof reused
proof search time: 0 min, 0 sec
Number of successful tactic applications: 3
Number of failed tactic applications: 0
Results for lemma eq_refl_iff: (x : E.t) : E.eq x x <-> True
FAILURE!
Tactics applied: 158
Original Proof: [now split.]
Proof search time: 0 min, 0 sec
Number of successful tactic applications: 19
Number of failed tactic applications: 139
Results for fold 3
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: 6
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: 2
Number of failed tactic applications: 4
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: 7
Original Proof: [fsetdec.]
Shorter Proof Found? no
Single step proof reused
proof search time: 0 min, 0 sec
Number of successful tactic applications: 3
Number of failed tactic applications: 4
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: 7
Original Proof: [fsetdec.]
Shorter Proof Found? no
Single step proof reused
proof search time: 0 min, 0 sec
Number of successful tactic applications: 3
Number of failed tactic applications: 4
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: 7
Original Proof: [fsetdec.]
Shorter Proof Found? no
Single step proof reused
proof search time: 0 min, 0 sec
Number of successful tactic applications: 2
Number of failed tactic applications: 5
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: 6
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: 2
Number of failed tactic applications: 4
Results for fold 4
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: 17
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: 6
Number of failed tactic applications: 11
Results for lemma dec_In: : forall x s, decidable (In x s)
FAILURE!
Tactics applied: 795
Original Proof: [red; intros; generalize (F.mem_iff s x); case (mem x s); intuition.]
Proof search time: 0 min, 0 sec
Number of successful tactic applications: 74
Number of failed tactic applications: 721
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: 17
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: 5
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: 17
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: 5
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: 17
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: 7
Results for fold 5
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
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
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 10 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 666
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