Results for fold 1 Results for lemma Subset_Included: : forall s s', s[<=]s' <-> Included _ (!!s) (!!s') SUCCESS! Proof Found in EFSM: [unfold Same_set, Included, mkEns, In , compute ;, auto ] Tactics applied: 51 Original Proof: [unfold Subset, Included, In, mkEns; intuition.] Shorter Proof Found? no This is a novel proof proof search time: 0 min, 1 sec Results for lemma singleton_Singleton: : forall x, !!(M.singleton x) === Singleton _ x SUCCESS! Proof Found in EFSM: [unfold Same_set, Included, mkEns, In , split ;, intro ;, set_iff ;, inversion 1;, constructor 1] Tactics applied: 5483 Original Proof: [unfold Same_set, Included, mkEns, In. split; intro; set_iff; inversion 1; try constructor; auto.] Shorter Proof Found? yes This is a novel proof This proof contained a loop around a state proof search time: 0 min, 7 sec Results for fold 2 Results for lemma union_Union: : forall s s', !!(union s s') === Union _ (!!s) (!!s') FAILURE! Tactics applied: 3192 Original Proof: [unfold Same_set, Included, mkEns, In. split; intro; set_iff; inversion 1; [ constructor 1 | constructor 2 | | ]; auto.] Proof search time: 0 min, 31 sec Results for lemma Equal_Same_set: : forall s s', s[=]s' <-> !!s === !!s' FAILURE! Tactics applied: 358 Original Proof: [intros. rewrite double_inclusion. unfold Subset, Included, Same_set, In, mkEns; intuition.] Proof search time: 0 min, 2 sec Results for fold 3 Results for lemma mkEns_Finite: : forall s, Finite _ (!!s) FAILURE! Tactics applied: 100000 Original Proof: [intro s; pattern s; apply set_induction; clear s; intros. intros; replace (!!s) with (Empty_set elt); auto with sets. symmetry; apply Extensionality_Ensembles. apply Empty_Empty_set; auto. replace (!!s') with (Add _ (!!s) x). constructor 2; auto. symmetry; apply Extensionality_Ensembles. apply Add_Add; auto.] Proof search time: 10 min, 47 sec Results for lemma Ens_to_MSet: : forall e : Ensemble M.elt, Finite _ e -> exists s:M.t, !!s === e FAILURE! Tactics applied: 100000 Original Proof: [induction 1. exists M.empty. apply empty_Empty_Set. destruct IHFinite as (s,Hs). exists (M.add x s). apply Extensionality_Ensembles in Hs. rewrite <- Hs. apply add_Add.] Proof search time: 3 min, 35 sec Results for fold 4 Results for lemma remove_Subtract: : forall x s, !!(remove x s) === Subtract _ (!!s) x SUCCESS! Proof Found in EFSM: [unfold Same_set, Included, mkEns, In , split ;, intro ;, set_iff ;, inversion 1;, constructor 1;, auto with sets ] Tactics applied: 399 Original Proof: [unfold Same_set, Included, mkEns, In. split; intro; set_iff; inversion 1; auto with sets. split; auto. contradict H1. inversion H1; auto.] Shorter Proof Found? yes This is a novel proof This proof contained a loop around a state proof search time: 0 min, 3 sec Results for lemma In_In: : forall s x, M.In x s <-> In _ (!!s) x SUCCESS! Proof Found in EFSM: [unfold Same_set, Included, mkEns, In , intuition ] Tactics applied: 9 Original Proof: [unfold In; compute; auto with extcore.] Shorter Proof Found? yes This is a novel proof proof search time: 0 min, 1 sec Results for fold 5 Results for lemma mkEns_cardinal: : forall s, cardinal _ (!!s) (M.cardinal s) FAILURE! Tactics applied: 716 Original Proof: [intro s; pattern s; apply set_induction; clear s; intros. intros; replace (!!s) with (Empty_set elt); auto with sets. rewrite MP.cardinal_1; auto with sets. symmetry; apply Extensionality_Ensembles. apply Empty_Empty_set; auto. replace (!!s') with (Add _ (!!s) x). rewrite (cardinal_2 H0 H1); auto with sets. symmetry; apply Extensionality_Ensembles. apply Add_Add; auto.] Proof search time: 0 min, 3 sec Results for lemma inter_Intersection: : forall s s', !!(inter s s') === Intersection _ (!!s) (!!s') SUCCESS! Proof Found in EFSM: [unfold Same_set, Included, mkEns, In , split ;, intro ;, set_iff ;, inversion 1;, try constructor;, auto ] Tactics applied: 330 Original Proof: [unfold Same_set, Included, mkEns, In. split; intro; set_iff; inversion 1; try constructor; auto.] Shorter Proof Found? no This is a novel proof proof search time: 0 min, 2 sec Results for fold 6 Results for lemma add_Add: : forall x s, !!(add x s) === Add _ (!!s) x FAILURE! Tactics applied: 464 Original Proof: [unfold Same_set, Included, mkEns, In. split; intro; set_iff; inversion 1; auto with sets. inversion H0. constructor 2; constructor. constructor 1; auto.] Proof search time: 0 min, 4 sec Results for lemma empty_Empty_Set: : !!M.empty === Empty_set _ SUCCESS! Proof Found in EFSM: [unfold Same_set, Included, mkEns, In , split ;, intro ;, set_iff ;, inversion 1] Tactics applied: 69 Original Proof: [unfold Same_set, Included, mkEns, In. split; intro; set_iff; inversion 1.] Shorter Proof Found? no This is a novel proof proof search time: 0 min, 1 sec Results for fold 7 Results for lemma Add_Add: : forall x s s', MP.Add x s s' -> !!s' === Add _ (!!s) x FAILURE! Tactics applied: 255 Original Proof: [unfold Same_set, Included, mkEns, In. split; intros. red in H; rewrite H in H0. destruct H0. inversion H0. constructor 2; constructor. constructor 1; auto. red in H; rewrite H. inversion H0; auto. inversion H1; auto.] Proof search time: 0 min, 2 sec Results for lemma Empty_Empty_set: : forall s, Empty s -> !!s === Empty_set _ FAILURE! Tactics applied: 3827 Original Proof: [unfold Same_set, Included, mkEns, In. split; intros. destruct(H x H0). inversion H0.] Proof search time: 0 min, 25 sec Results for fold 8 OVERALL RESULTS SUMMARY EFSMProver proved 6 out of 14 lemmas. Success rate of 42.857142857142854% There were 0 errors. 8 proof attempts exhausted the automaton On average, a proof was found after applying 1056 tactics The longest proof consisted of 7 tactics There were 3 shorter proofs found Of the 8 failures, 2 of them used all 100000 tactics There were 0 reused proofs found There were 6 novel proofs found Of the 8 failures, the average number of tactics used was 26101 On average, a proof was found after 0 min, 3 sec On average, a failed proof attempt took 1 min, 56 sec On average, any (success or failure) proof attempt took 1 min, 7 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 2 proofs that repeated states