Results for fold 1 Results for lemma codomP: y : reflect (exists x, y = f x) (y \in codom f) FAILURE! Tactics applied: 100000 Original Proof: [by apply: (iffP (imageP _ y)) => [][x]; exists x.] Proof search time: 1 min, 39 sec Results for lemma card_uniqP: s : reflect (#|s| = size s) (uniq s) FAILURE! Tactics applied: 100000 Original Proof: [elim: s => [|x s IHs]; first by left; exact card0. rewrite cardU1 /= /addn; case: {+}(x \in s) => /=. by right=> card_Ssz; have:= card_size s; rewrite card_Ssz ltnn. by apply: (iffP IHs) => [<-| [<-]].] Proof search time: 1 min, 16 sec Results for lemma eq_card_prod: (A : pred (T1 * T2)) : A =i predT -> #|A| = #|T1| * #|T2| SUCCESS! Proof Found in EFSM: [by rewrite -cardX;, apply eq_card => x] Tactics applied: 3661 Original Proof: [exact: eq_card_trans card_prod.] Shorter Proof Found? no This is a novel proof proof search time: 0 min, 12 sec Results for lemma rev_ord_proof: n (i : 'I_n) : n - i.+1 < n FAILURE! Tactics applied: 100000 Original Proof: [by case: n i => [|n] [i lt_i_n] //; rewrite ltnS subSS leq_subr.] Proof search time: 1 min, 44 sec Results for lemma injF_onto: y : y \in codom f SUCCESS! Proof Found in EFSM: [by move y;, apply /subset_cardP;, rewrite ?card_codom ?subset_predT ] Tactics applied: 36013 Original Proof: [exact: inj_card_onto.] Shorter Proof Found? no Proof reused from inj_card_onto proof search time: 0 min, 58 sec Results for lemma subset_leqif_card: A B : A \subset B -> #|A| <= #|B| ?= iff (B \subset A) FAILURE! Tactics applied: 100000 Original Proof: [move=> sAB; split; [exact: subset_leq_card | apply/eqP/idP]. by move/subset_cardP=> sABP; rewrite (eq_subset_r (sABP sAB)). by move=> sBA; apply: eq_card; apply/subset_eqP; rewrite sAB.] Proof search time: 2 min, 30 sec Results for lemma map_preim: (s : seq T') : {subset s <= codom f} -> map f (preim_seq s) = s FAILURE! Tactics applied: 100000 Original Proof: [elim: s => //= y s IHs; case: pickP => [x /eqP fx_y | nfTy] fTs. by rewrite /= fx_y IHs // => z s_z; apply: fTs; exact: predU1r. by case/imageP: (fTs y (mem_head y s)) => x _ fx_y; case/eqP: (nfTy x).] Proof search time: 2 min, 38 sec Results for lemma bumpS: h i : bump h.+1 i.+1 = (bump h i).+1 FAILURE! Tactics applied: 100000 Original Proof: [exact: addnS.] Proof search time: 1 min, 34 sec Results for lemma unlift_some: n (h i : 'I_n) : h != i -> {j | i = lift h j & unlift h i = Some j} FAILURE! Tactics applied: 100000 Original Proof: [rewrite eq_sym => /eqP neq_ih. by case Dui: (unlift h i) / (unliftP h i) => [j Dh|//]; exists j.] Proof search time: 3 min, 22 sec Results for lemma enum0: : enum pred0 = Nil T FAILURE! Tactics applied: 100000 Original Proof: [exact: filter_pred0.] Proof search time: 1 min, 14 sec Results for lemma enum_rankK: : cancel enum_rank enum_val SUCCESS! Proof Found in EFSM: [by move=> ?;, exact nth_enum_rank_in ] Tactics applied: 2420 Original Proof: [by move=> x; exact: enum_rankK_in.] Shorter Proof Found? no This is a novel proof proof search time: 0 min, 8 sec Results for lemma bool_enumP: : Finite.axiom [:: true; false] SUCCESS! Proof Found in EFSM: [by case ] Tactics applied: 21 Original Proof: [by case.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 4 sec Results for lemma pred0P: P : reflect (P =1 pred0) (pred0b P) FAILURE! Tactics applied: 100000 Original Proof: [apply: (iffP eqP); [exact: card0_eq | exact: eq_card0].] Proof search time: 1 min, 15 sec Results for lemma inordK: m : m < n -> inord m = m :> nat SUCCESS! Proof Found in EFSM: [by move=> ?;, rewrite insubdK ?index_enum_ord // card_ord [_ \in _]ltn_ord ] Tactics applied: 2535 Original Proof: [by move=> lt_m; rewrite val_insubd lt_m.] Shorter Proof Found? no This is a novel proof proof search time: 0 min, 9 sec Results for lemma subsetPn: A B : reflect (exists2 x, x \in A & x \notin B) (~~ (A \subset B)) FAILURE! Tactics applied: 100000 Original Proof: [rewrite unlock; apply: (iffP (pred0Pn _)) => [[x] | [x Ax nBx]]. by case/andP; exists x. by exists x; rewrite /= nBx.] Proof search time: 1 min, 27 sec Results for lemma eq_disjoint: A1 A2 : A1 =i A2 -> disjoint (mem A1) =1 disjoint (mem A2) FAILURE! Tactics applied: 100000 Original Proof: [by move=> eqA12 [B]; congr (_ == 0); apply: eq_card => x; rewrite !inE eqA12.] Proof search time: 2 min, 26 sec Results for lemma eq_codom: (f g : T -> T') : f =1 g -> codom f = codom g FAILURE! Tactics applied: 100000 Original Proof: [exact: eq_image.] Proof search time: 2 min, 33 sec Results for lemma neq_lift: n (h : 'I_n) i : h != lift h i FAILURE! Tactics applied: 100000 Original Proof: [exact: neq_bump.] Proof search time: 1 min, 48 sec Results for lemma in_iinv_f: A : {in A &, injective f} -> forall x fAfx, x \in A -> @iinv A (f x) fAfx = x FAILURE! Tactics applied: 100000 Original Proof: [move=> injf x fAfx Ax; apply: injf => //; [exact: mem_iinv | exact: f_iinv].] Proof search time: 3 min, 17 sec Results for lemma card_ord: : #|'I_n| = n FAILURE! Tactics applied: 100000 Original Proof: [by rewrite cardE size_enum_ord.] Proof search time: 1 min, 31 sec Results for lemma card_sub: : #|sfT| = #|[pred x | P x]| FAILURE! Tactics applied: 100000 Original Proof: [by rewrite !cardE enumT unlock -(size_map val) val_sub_enum.] Proof search time: 2 min, 4 sec Results for lemma mem_iinv: A y fAy : @iinv A y fAy \in A FAILURE! Tactics applied: 100000 Original Proof: [exact: s2valP (iinv_proof fAy).] Proof search time: 1 min, 54 sec Results for lemma enumT: : enum T = Finite.enum T FAILURE! Tactics applied: 100000 Original Proof: [exact: filter_predT.] Proof search time: 1 min, 32 sec Results for lemma card_size: s : #|s| <= size s FAILURE! Tactics applied: 100000 Original Proof: [elim: s => [|x s IHs] /=; first by rewrite card0. rewrite cardU1 /=; case: (~~ _) => //; exact: leqW.] Proof search time: 1 min, 22 sec Results for lemma eq_existsb: P1 P2 : P1 =1 P2 -> [exists x, P1 x] = [exists x, P2 x] FAILURE! Tactics applied: 100000 Original Proof: [by move=> eqP12; congr (_ != 0); apply: eq_card.] Proof search time: 2 min, 52 sec Results for fold 2 Results for lemma unlift_subproof: n (h : 'I_n) (u : {j | j != h}) : unbump h (val u) < n.-1 FAILURE! Tactics applied: 100000 Original Proof: [case: n h u => [|n h] [] //= j ne_jh. rewrite -(leq_bump2 h.+1) bumpS unbumpK // /bump. case: (ltngtP n h) => [|_|eq_nh]; rewrite ?(leqNgt _ h) ?ltn_ord //. by rewrite ltn_neqAle [j <= _](valP j) {2}eq_nh andbT.] Proof search time: 2 min, 48 sec Results for lemma proper_subn: A B : A \proper B -> ~~ (B \subset A) SUCCESS! Proof Found in EFSM: [by case/andP ] Tactics applied: 111 Original Proof: [by case/andP.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 2 sec Results for lemma cast_ord_proof: n m (i : 'I_n) : n = m -> i < m SUCCESS! Proof Found in EFSM: [by case n i => [n] [i lt_i_n] //;, move <-] Tactics applied: 6786 Original Proof: [by move <-.] Shorter Proof Found? no This is a novel proof proof search time: 0 min, 14 sec Results for lemma rev_ord_inj: {n} : injective (@rev_ord n) FAILURE! Tactics applied: 100000 Original Proof: [exact: inv_inj (@rev_ordK n).] Proof search time: 2 min, 42 sec Results for lemma inj_card_bij: : bijective f FAILURE! Tactics applied: 100000 Original Proof: [by exists (fun y => iinv (inj_card_onto y)) => y; rewrite ?iinv_f ?f_iinv.] Proof search time: 2 min, 21 sec Results for lemma exists_eq_inP: D f1 f2 : reflect (exists2 x, D x & f1 x = f2 x) [exists (x | D x), f1 x == f2 x] FAILURE! Tactics applied: 100000 Original Proof: [by apply: (iffP (exists_inP _ _)) => [] [x Dx /eqP]; exists x.] Proof search time: 4 min, 48 sec Results for lemma disjoint1: x A : [disjoint pred1 x & A] = (x \notin A) FAILURE! Tactics applied: 100000 Original Proof: [apply/negbRL/(sameP (pred0Pn _)). apply: introP => [Ax | notAx [_ /andP[/eqP->]]]; last exact: negP. by exists x; rewrite !inE eqxx.] Proof search time: 1 min, 54 sec Results for lemma injectivePn: : reflect (exists x, exists2 y, x != y & f x = f y) (~~ injectiveb) FAILURE! Tactics applied: 100000 Original Proof: [apply: (iffP (dinjectivePn _)) => [[x _ [y nxy eqfxy]] | [x [y nxy eqfxy]]]; by exists x => //; exists y => //; rewrite inE /= andbT eq_sym in nxy *.] Proof search time: 1 min, 56 sec Results for lemma properP: A B : reflect (A \subset B /\ (exists2 x, x \in B & x \notin A)) (A \proper B) FAILURE! Tactics applied: 100000 Original Proof: [by rewrite properE; apply: (iffP andP) => [] [-> /subsetPn].] Proof search time: 1 min, 54 sec Results for lemma subset_pred1: A x : (pred1 x \subset A) = (x \in A) FAILURE! Tactics applied: 100000 Original Proof: [by apply/subsetP/idP=> [-> // | Ax y /eqP-> //]; exact: eqxx.] Proof search time: 1 min, 56 sec Results for lemma card_unit: : #|{: unit}| = 1 SUCCESS! Proof Found in EFSM: [by rewrite cardT enumT unlock ] Tactics applied: 172 Original Proof: [by rewrite cardT enumT unlock.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 4 sec Results for lemma cardE: A : #|A| = size (enum A) SUCCESS! Proof Found in EFSM: [by rewrite unlock ] Tactics applied: 185 Original Proof: [by rewrite unlock.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 1 sec Results for lemma subset_leq_card: A B : A \subset B -> #|A| <= #|B| FAILURE! Tactics applied: 100000 Original Proof: [move=> sAB. rewrite -(cardID A B) [#|predI _ _|](@eq_card _ A) ?leq_addr //= => x. rewrite !inE andbC; case Ax: (x \in A) => //; exact: subsetP Ax.] Proof search time: 2 min, 12 sec Results for lemma card_sum: : #|{: T1 + T2}| = #|T1| + #|T2| FAILURE! Tactics applied: 100000 Original Proof: [by rewrite !cardT !enumT {1}unlock size_cat !size_map.] Proof search time: 2 min, 24 sec Results for lemma sum_enum_uniq: : uniq sum_enum FAILURE! Tactics applied: 100000 Original Proof: [rewrite cat_uniq -!enumT !(enum_uniq, map_inj_uniq); try by move=> ? ? []. by rewrite andbT; apply/hasP=> [[_ /mapP[x _ ->] /mapP[]]].] Proof search time: 2 min, 45 sec Results for lemma card1: x : #|pred1 x| = 1 SUCCESS! Proof Found in EFSM: [rewrite unlock;, first by rewrite -count_filter enumP ] Tactics applied: 17020 Original Proof: [by rewrite cardE enum1.] Shorter Proof Found? no This is a novel proof proof search time: 0 min, 11 sec Results for lemma subset_predT: A : A \subset T SUCCESS! Proof Found in EFSM: [by rewrite unlock;, exact /pred0P ] Tactics applied: 16085 Original Proof: [by apply/subsetP.] Shorter Proof Found? no This is a novel proof proof search time: 0 min, 12 sec Results for lemma split_subproof: m n (i : 'I_(m + n)) : i >= m -> i - m < n FAILURE! Tactics applied: 100000 Original Proof: [by move/subSn <-; rewrite leq_subLR.] Proof search time: 2 min, 47 sec Results for lemma injF_bij: : bijective f FAILURE! Tactics applied: 100000 Original Proof: [exact: inj_card_bij.] Proof search time: 2 min, 18 sec Results for lemma unliftP: n (h i : 'I_n) : unlift_spec h i (unlift h i) FAILURE! Tactics applied: 100000 Original Proof: [rewrite /unlift; case: insubP => [u nhi | ] def_i /=; constructor. by apply: val_inj; rewrite /= def_i unbumpK. by rewrite negbK in def_i; exact/eqP.] Proof search time: 2 min, 24 sec Results for lemma eq_subxx: A B : A =i B -> A \subset B FAILURE! Tactics applied: 100000 Original Proof: [by move/eq_subset->.] Proof search time: 2 min, 3 sec Results for lemma properxx: A : (A \proper A) = false SUCCESS! Proof Found in EFSM: [by rewrite properE subxx ] Tactics applied: 187 Original Proof: [by rewrite properE subxx.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 2 sec Results for lemma unit_enumP: : Finite.axiom [::tt] SUCCESS! Proof Found in EFSM: [by [] ] Tactics applied: 92 Original Proof: [by case.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 4 sec Results for lemma neq_bump: h i : h != bump h i FAILURE! Tactics applied: 100000 Original Proof: [rewrite /bump eqn_leq; have [le_hi | lt_ih] := leqP h i. by rewrite ltnNge le_hi andbF. by rewrite leqNgt lt_ih.] Proof search time: 3 min, 5 sec Results for lemma image_pred0: : image f pred0 =i pred0 FAILURE! Tactics applied: 100000 Original Proof: [by move=> x; rewrite /image_mem /= enum0.] Proof search time: 2 min, 32 sec Results for fold 3 Results for lemma cardID: B A : #|[predI A & B]| + #|[predD A & B]| = #|A| FAILURE! Tactics applied: 100000 Original Proof: [rewrite -cardUI addnC [#|predI _ _|]eq_card0 => [|x] /=. by apply: eq_card => x; rewrite !inE andbC -andb_orl orbN. by rewrite !inE -!andbA andbC andbA andbN.] Proof search time: 1 min, 48 sec Results for lemma codom_f: x : f x \in codom f FAILURE! Tactics applied: 100000 Original Proof: [by exact: image_f.] Proof search time: 1 min, 53 sec Results for lemma enum_val_ord: n i : enum_val i = cast_ord (card_ord n) i FAILURE! Tactics applied: 100000 Original Proof: [by apply: canLR (@enum_rankK _) _; apply: val_inj; rewrite enum_rank_ord.] Proof search time: 2 min, 42 sec Results for lemma enum_uniq: : uniq (enum P) FAILURE! Tactics applied: 100000 Original Proof: [by apply/filter_uniq/count_mem_uniq => x; rewrite enumP -enumT mem_enum.] Proof search time: 1 min, 36 sec Results for lemma size_codom: : size (codom f) = #|T| SUCCESS! Proof Found in EFSM: [by rewrite size_map -cardE ] Tactics applied: 202 Original Proof: [exact: size_image.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 3 sec Results for lemma subsetE: A B : (A \subset B) = pred0b [predD A & B] SUCCESS! Proof Found in EFSM: [by rewrite unlock ] Tactics applied: 205 Original Proof: [by rewrite unlock.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 2 sec Results for lemma cardD1: x A : #|A| = (x \in A) + #|[predD1 A & x]| FAILURE! Tactics applied: 100000 Original Proof: [case Ax: (x \in A); last first. by apply: eq_card => y; rewrite !inE /=; case: eqP => // ->. rewrite /= -(card1 x) -cardUI addnC /=. rewrite [#|predI _ _|]eq_card0 => [|y]; last by rewrite !inE; case: eqP. by apply: eq_card => y; rewrite !inE; case: eqP => // ->.] Proof search time: 1 min, 40 sec Results for lemma enum_val_nth: A x i : @enum_val A i = nth x (enum A) i FAILURE! Tactics applied: 100000 Original Proof: [by apply: set_nth_default; rewrite cardE in i *; exact: ltn_ord.] Proof search time: 2 min, 10 sec Results for lemma ord_inj: : injective nat_of_ord SUCCESS! Proof Found in EFSM: [exact val_inj ] Tactics applied: 61 Original Proof: [exact: val_inj.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 5 sec Results for lemma max_card: A : #|A| <= #|T| FAILURE! Tactics applied: 100000 Original Proof: [by rewrite -(cardC A) leq_addr.] Proof search time: 1 min, 38 sec Results for lemma subset_trans: A B C : A \subset B -> B \subset C -> A \subset C FAILURE! Tactics applied: 100000 Original Proof: [by move/subsetP=> sAB /subsetP=> sBC; apply/subsetP=> x /sAB; exact: sBC.] Proof search time: 2 min, 35 sec Results for lemma count_enumP: : axiom count_enum FAILURE! Tactics applied: 100000 Original Proof: [apply: uniq_enumP (pmap_uniq (@pickle_invK T) (iota_uniq _ _)) _ => x. by rewrite mem_pmap -pickleK_inv map_f // mem_iota ubT.] Proof search time: 1 min, 37 sec Results for lemma cast_ord_id: n eq_n i : cast_ord eq_n i = i :> 'I_n SUCCESS! Proof Found in EFSM: [exact val_inj ] Tactics applied: 61 Original Proof: [exact: val_inj.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 5 sec Results for lemma nth_enum_rank: x0 : cancel enum_rank (nth x0 (enum T)) SUCCESS! Proof Found in EFSM: [rewrite /seq_sub_unpickle => x , exact nth_enum_rank_in ] Tactics applied: 1477 Original Proof: [by move=> x; exact: nth_enum_rank_in.] Shorter Proof Found? no This is a novel proof proof search time: 0 min, 7 sec Results for lemma canF_sym: : cancel g f FAILURE! Tactics applied: 100000 Original Proof: [exact/(bij_can_sym (injF_bij (can_inj fK))).] Proof search time: 2 min, 55 sec Results for lemma cardT: : #|T| = size (enum T) SUCCESS! Proof Found in EFSM: [by rewrite cardE] Tactics applied: 183 Original Proof: [by rewrite cardE.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 1 sec Results for lemma proper_irrefl: A : ~~ (A \proper A) SUCCESS! Proof Found in EFSM: [by rewrite properE subxx ] Tactics applied: 200 Original Proof: [by rewrite properE subxx.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 2 sec Results for lemma disjoint_sym: A B : [disjoint A & B] = [disjoint B & A] FAILURE! Tactics applied: 100000 Original Proof: [by congr (_ == 0); apply: eq_card => x; exact: andbC.] Proof search time: 1 min, 46 sec Results for lemma subset_eqP: A B : reflect (A =i B) ((A \subset B) && (B \subset A)) FAILURE! Tactics applied: 100000 Original Proof: [apply: (iffP andP) => [[sAB sBA] x| eqAB]; last by rewrite !eq_subxx. by apply/idP/idP; apply: subsetP.] Proof search time: 1 min, 39 sec Results for lemma subsetP: A B : reflect {subset A <= B} (A \subset B) FAILURE! Tactics applied: 100000 Original Proof: [rewrite unlock; apply: (iffP (pred0P _)) => [AB0 x | sAB x /=]. by apply/implyP; apply/idPn; rewrite negb_imply andbC [_ && _]AB0. by rewrite andbC -negb_imply; apply/negbF/implyP; exact: sAB.] Proof search time: 1 min, 39 sec Results for lemma nth_image: T' y0 (f : T -> T') A (i : 'I_#|A|) : nth y0 (image f A) i = f (enum_val i) FAILURE! Tactics applied: 100000 Original Proof: [by rewrite -(nth_map _ y0) // -cardE.] Proof search time: 2 min, 13 sec Results for lemma val_seq_sub_enum: : uniq s -> map val seq_sub_enum = s FAILURE! Tactics applied: 100000 Original Proof: [move=> Us; rewrite /seq_sub_enum undup_id ?pmap_sub_uniq //. rewrite (pmap_filter (@insubK _ _ _)); apply/all_filterP. by apply/allP => x; rewrite isSome_insub.] Proof search time: 3 min, 1 sec Results for lemma leq_bump2: h i j : (bump h i <= bump h j) = (i <= j) FAILURE! Tactics applied: 100000 Original Proof: [by rewrite leq_bump bumpK.] Proof search time: 1 min, 53 sec Results for lemma card_option: : #|{: option T}| = #|T|.+1 FAILURE! Tactics applied: 100000 Original Proof: [by rewrite !cardT !enumT {1}unlock /= !size_map.] Proof search time: 1 min, 59 sec Results for lemma sub_proper_trans: A B C : A \subset B -> B \proper C -> A \proper C FAILURE! Tactics applied: 100000 Original Proof: [move=> sAB /properP[sBC [x Cx nBx]]; rewrite properE (subset_trans sAB) //. by apply/subsetPn; exists x => //; apply: contra nBx; exact: subsetP.] Proof search time: 2 min, 33 sec Results for fold 4 Results for lemma predT_subset: A : T \subset A -> forall x, x \in A FAILURE! Tactics applied: 100000 Original Proof: [move/subsetP=> allA x; exact: allA.] Proof search time: 3 min, 9 sec Results for lemma val_ord_enum: : map val ord_enum = iota 0 n FAILURE! Tactics applied: 100000 Original Proof: [rewrite pmap_filter; last exact: insubK. by apply/all_filterP; apply/allP=> i; rewrite mem_iota isSome_insub.] Proof search time: 2 min, 58 sec Results for lemma sub_ordK: (i : 'I_n) : n' - (n' - i) = i FAILURE! Tactics applied: 100000 Original Proof: [by rewrite subKn ?leq_ord.] Proof search time: 3 min, 2 sec Results for lemma cardX: (A1 : pred T1) (A2 : pred T2) : #|[predX A1 & A2]| = #|A1| * #|A2| FAILURE! Tactics applied: 100000 Original Proof: [by rewrite -predX_prod_enum unlock -count_filter unlock.] Proof search time: 4 min, 12 sec Results for lemma image_f: A x : x \in A -> f x \in image f A FAILURE! Tactics applied: 100000 Original Proof: [by move=> Ax; apply/imageP; exists x.] Proof search time: 3 min, 56 sec Results for lemma eq_subset: A1 A2 : A1 =i A2 -> subset (mem A1) =1 subset (mem A2) FAILURE! Tactics applied: 100000 Original Proof: [move=> eqA12 [B]; rewrite !unlock; congr (_ == 0). by apply: eq_card => x; rewrite inE /= eqA12.] Proof search time: 3 min, 9 sec Results for lemma image_codom: A : {subset image f A <= codom f} FAILURE! Tactics applied: 100000 Original Proof: [by move=> _ /imageP[x _ ->]; exact: codom_f.] Proof search time: 3 min, 47 sec Results for lemma eqfun_inP: D f1 f2 : reflect {in D, forall x, f1 x = f2 x} [forall (x | x \in D), f1 x == f2 x] FAILURE! Tactics applied: 100000 Original Proof: [by apply: (iffP (forall_inP _ _)) => eq_f12 x Dx; apply/eqP/eq_f12.] Proof search time: 3 min, 40 sec Results for lemma inord_val: (i : 'I_n) : inord i = i FAILURE! Tactics applied: 100000 Original Proof: [by rewrite /inord /insubd valK.] Proof search time: 2 min, 51 sec Results for lemma disjoint_has: s A : [disjoint s & A] = ~~ has (mem A) s FAILURE! Tactics applied: 100000 Original Proof: [rewrite -(@eq_has _ (mem (enum A))) => [|x]; last exact: mem_enum. rewrite has_sym has_filter -filter_predI -has_filter has_count -eqn0Ngt. by rewrite count_filter /disjoint /pred0b unlock.] Proof search time: 2 min, 41 sec Results for lemma enum_rank_subproof: x0 A : x0 \in A -> 0 < #|A| FAILURE! Tactics applied: 100000 Original Proof: [by move=> Ax0; rewrite (cardD1 x0) Ax0.] Proof search time: 3 min, 45 sec Results for lemma eq_subset_r: B1 B2 : B1 =i B2 -> (@subset T)^~ (mem B1) =1 (@subset T)^~ (mem B2) FAILURE! Tactics applied: 100000 Original Proof: [move=> eqB12 [A]; rewrite !unlock; congr (_ == 0). by apply: eq_card => x; rewrite !inE /= eqB12.] Proof search time: 3 min, 13 sec Results for lemma enum1: x : enum (pred1 x) = [:: x] FAILURE! Tactics applied: 100000 Original Proof: [rewrite [enum _](all_pred1P x _ _); first by rewrite -count_filter enumP. by apply/allP=> y; rewrite mem_enum.] Proof search time: 2 min, 17 sec Results for lemma negb_forall_in: D P : ~~ [forall (x | D x), P x] = [exists (x | D x), ~~ P x] FAILURE! Tactics applied: 100000 Original Proof: [by apply: eq_existsb => x; rewrite negb_imply.] Proof search time: 3 min, 13 sec Results for lemma enum_rankK_in: x0 A Ax0 : {in A, cancel (@enum_rank_in x0 A Ax0) enum_val} SUCCESS! Proof Found in EFSM: [by move=> ?;, exact nth_enum_rank_in ] Tactics applied: 3756 Original Proof: [by move=> x; exact: nth_enum_rank_in.] Shorter Proof Found? no This is a novel proof proof search time: 0 min, 11 sec Results for lemma properE: A B : A \proper B = (A \subset B) && ~~(B \subset A) SUCCESS! Proof Found in EFSM: [by [] ] Tactics applied: 68 Original Proof: [by [].] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 2 sec Results for lemma card_codom: : #|codom f| = #|T| SUCCESS! Proof Found in EFSM: [apply card_in_image;, exact in2W ] Tactics applied: 7194 Original Proof: [exact: card_image.] Shorter Proof Found? no Proof reused from card_image proof search time: 0 min, 14 sec Results for lemma option_enumP: : Finite.axiom option_enum FAILURE! Tactics applied: 100000 Original Proof: [by case=> [x|]; rewrite /= count_map (count_pred0, enumP).] Proof search time: 3 min, 3 sec Results for lemma negb_exists_in: D P : ~~ [exists (x | D x), P x] = [forall (x | D x), ~~ P x] FAILURE! Tactics applied: 100000 Original Proof: [by rewrite negb_exists; apply/eq_forallb => x; rewrite [~~ _]fun_if.] Proof search time: 3 min, 16 sec Results for lemma iinv_f: x fTfx : @iinv T (f x) fTfx = x FAILURE! Tactics applied: 100000 Original Proof: [by apply: in_iinv_f; first exact: in2W.] Proof search time: 3 min, 29 sec Results for lemma ord_enum_uniq: : uniq ord_enum FAILURE! Tactics applied: 100000 Original Proof: [by rewrite pmap_sub_uniq ?iota_uniq.] Proof search time: 2 min, 44 sec Results for lemma lift_subproof: n h (i : 'I_n.-1) : bump h i < n FAILURE! Tactics applied: 100000 Original Proof: [by case: n i => [[]|n] //= i; rewrite -addnS (leq_add (leq_b1 _)).] Proof search time: 3 min, 20 sec Results for lemma enum_rank_ord: n i : enum_rank i = cast_ord (esym (card_ord n)) i FAILURE! Tactics applied: 100000 Original Proof: [by apply: val_inj; rewrite insubdK ?index_enum_ord // card_ord [_ \in _]ltn_ord.] Proof search time: 4 min, 59 sec Results for lemma card_preim: (B : pred T') : #|[preim f of B]| = #|[predI codom f & B]| FAILURE! Tactics applied: 100000 Original Proof: [rewrite -card_image /=; apply: eq_card => y. by rewrite [y \in _]image_pre !inE andbC.] Proof search time: 4 min, 12 sec Results for lemma liftK: n (h : 'I_n) : pcancel (lift h) (unlift h) FAILURE! Tactics applied: 100000 Original Proof: [by move=> i; case: (unlift_some (neq_lift h i)) => j; move/lift_inj->.] Proof search time: 3 min, 1 sec Results for fold 5 Results for lemma exists_inP: D P : reflect (exists2 x, D x & P x) [exists (x | D x), P x] FAILURE! Tactics applied: 100000 Original Proof: [by apply: (iffP pred0Pn) => [[x /andP[]] | [x]]; exists x => //; apply/andP.] Proof search time: 3 min, 28 sec Results for lemma pickP: : pick_spec (pick P) FAILURE! Tactics applied: 100000 Original Proof: [rewrite /pick; case: (enum _) (mem_enum P) => [|x s] Pxs /=. by right; exact: fsym. by left; rewrite -[P _]Pxs mem_head.] Proof search time: 2 min, 1 sec Results for lemma mem_enum: A : enum A =i A FAILURE! Tactics applied: 100000 Original Proof: [by move=> x; rewrite mem_filter andbC -has_pred1 has_count enumP.] Proof search time: 2 min, 49 sec Results for lemma cardC: A : #|A| + #|[predC A]| = #|T| FAILURE! Tactics applied: 100000 Original Proof: [by rewrite !cardE -!count_filter count_predC.] Proof search time: 2 min, 53 sec Results for lemma eq_enum: P Q : P =i Q -> enum P = enum Q FAILURE! Tactics applied: 100000 Original Proof: [move=> eqPQ; exact: eq_filter.] Proof search time: 2 min, 48 sec Results for lemma pcan_enumP: g : pcancel f g -> Finite.axiom (undup (pmap g (enumF fT))) FAILURE! Tactics applied: 100000 Original Proof: [move=> fK x; rewrite count_uniq_mem ?undup_uniq // mem_undup. by rewrite mem_pmap -fK map_f // -enumT mem_enum.] Proof search time: 3 min, 34 sec Results for lemma nth_ord_enum: (i0 i : 'I_n) : nth i0 (enum 'I_n) i = i SUCCESS! Proof Found in EFSM: [by apply val_inj;, rewrite -(nth_map _ 0) (size_enum_ord, val_enum_ord) // nth_iota ] Tactics applied: 7696 Original Proof: [apply: val_inj; exact: nth_enum_ord.] Shorter Proof Found? no This is a novel proof This proof contained a loop around a state proof search time: 0 min, 13 sec Results for lemma bump_addl: h i k : bump (k + h) (k + i) = k + bump h i FAILURE! Tactics applied: 100000 Original Proof: [by rewrite /bump leq_add2l addnCA.] Proof search time: 3 min, 20 sec Results for lemma disjoint0: A : [disjoint pred0 & A] FAILURE! Tactics applied: 100000 Original Proof: [exact/pred0P.] Proof search time: 2 min, 46 sec Results for lemma f_iinv: A y fAy : f (@iinv A y fAy) = y FAILURE! Tactics applied: 100000 Original Proof: [exact: s2valP' (iinv_proof fAy).] Proof search time: 3 min, 23 sec Results for lemma enumP: : Finite.axiom (Finite.enum T) FAILURE! Tactics applied: 100000 Original Proof: [by rewrite unlock; case T => ? [? []].] Proof search time: 2 min, 15 sec Results for lemma disjoint_cons: x s B : [disjoint x :: s & B] = (x \notin B) && [disjoint s & B] FAILURE! Tactics applied: 100000 Original Proof: [exact: disjointU1.] Proof search time: 3 min, 46 sec Results for lemma uniq_enumP: e : uniq e -> e =i T -> axiom e FAILURE! Tactics applied: 100000 Original Proof: [by move=> Ue sT x; rewrite count_uniq_mem ?sT.] Proof search time: 2 min, 23 sec Results for lemma card_sig: : #|{: {x | P x}}| = #|[pred x | P x]| SUCCESS! Proof Found in EFSM: [by rewrite !cardE enumT unlock -(size_map val) val_sub_enum ] Tactics applied: 184 Original Proof: [exact: card_sub.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 4 sec Results for lemma disjointU1: x A B : [disjoint predU1 x A & B] = (x \notin B) && [disjoint A & B] FAILURE! Tactics applied: 100000 Original Proof: [by rewrite disjointU disjoint1.] Proof search time: 3 min, 35 sec Results for lemma cast_ordKV: n1 n2 eq_n : cancel (cast_ord (esym eq_n)) (@cast_ord n1 n2 eq_n) SUCCESS! Proof Found in EFSM: [rewrite /seq_sub_unpickle => x , exact val_inj ] Tactics applied: 4464 Original Proof: [by move=> i; exact: val_inj.] Shorter Proof Found? no This is a novel proof proof search time: 0 min, 10 sec Results for lemma mem_ord_enum: i : i \in ord_enum FAILURE! Tactics applied: 100000 Original Proof: [by rewrite -(mem_map ord_inj) val_ord_enum mem_iota ltn_ord.] Proof search time: 2 min, 56 sec Results for lemma card_seq_sub: : uniq s -> #|{:seq_sub}| = size s FAILURE! Tactics applied: 100000 Original Proof: [by move=> Us; rewrite cardE enumT -(size_map val) unlock val_seq_sub_enum.] Proof search time: 3 min, 23 sec Results for lemma mem_sum_enum: u : u \in sum_enum FAILURE! Tactics applied: 100000 Original Proof: [by case: u => x; rewrite mem_cat -!enumT map_f ?mem_enum ?orbT.] Proof search time: 3 min, 29 sec Results for lemma forall_inP: D P : reflect (forall x, D x -> P x) [forall (x | D x), P x] FAILURE! Tactics applied: 100000 Original Proof: [by apply: (iffP (forallP _)) => /= P_ x /=; apply/implyP; apply: P_.] Proof search time: 3 min, 7 sec Results for lemma enum_rank_bij: : bijective enum_rank FAILURE! Tactics applied: 100000 Original Proof: [by move: enum_rankK enum_valK; exists (@enum_val T).] Proof search time: 3 min, 39 sec Results for lemma image_injP: A : reflect {in A &, injective f} (#|image f A| == #|A|) FAILURE! Tactics applied: 100000 Original Proof: [apply: (iffP eqP) => [eqfA |]; last exact: card_in_image. by apply/dinjectiveP; apply/card_uniqP; rewrite size_map -cardE.] Proof search time: 4 min, 22 sec Results for lemma rev_ordK: n : involutive (@rev_ord n) FAILURE! Tactics applied: 100000 Original Proof: [by case: n => [|n] [i lti] //; apply: val_inj; rewrite /= !subSS subKn.] Proof search time: 2 min, 51 sec Results for lemma subset_cardP: A B : #|A| = #|B| -> reflect (A =i B) (A \subset B) FAILURE! Tactics applied: 100000 Original Proof: [move=> eqcAB; case: (subsetP A B) (subset_eqP A B) => //= sAB. case: (subsetP B A) => [//|[]] x Bx; apply/idPn => Ax. case/idP: (ltnn #|A|); rewrite {2}eqcAB (cardD1 x B) Bx /=. apply: subset_leq_card; apply/subsetP=> y Ay; rewrite inE /= andbC. by rewrite sAB //; apply/eqP => eqyx; rewrite -eqyx Ay in Ax.] Proof search time: 3 min, 37 sec Results for lemma eq_disjoint_r: B1 B2 : B1 =i B2 -> (@disjoint T)^~ (mem B1) =1 (@disjoint T)^~ (mem B2) FAILURE! Tactics applied: 100000 Original Proof: [by move=> eqB12 [A]; congr (_ == 0); apply: eq_card => x; rewrite !inE eqB12.] Proof search time: 3 min, 22 sec Results for fold 6 Results for lemma eq_card: A B : A =i B -> #|A| = #|B| FAILURE! Tactics applied: 100000 Original Proof: [by move=>eqAB; rewrite !cardE (eq_enum eqAB).] Proof search time: 3 min, 34 sec Results for lemma eq_disjoint1: x A B : A =i pred1 x -> [disjoint A & B] = (x \notin B) FAILURE! Tactics applied: 100000 Original Proof: [by move/eq_disjoint->; exact: disjoint1.] Proof search time: 4 min, 13 sec Results for lemma bumpC: h1 h2 i : bump h1 (bump h2 i) = bump (bump h1 h2) (bump (unbump h2 h1) i) FAILURE! Tactics applied: 100000 Original Proof: [rewrite {1 5}/bump -leq_bump addnCA; congr (_ + (_ + _)). rewrite 2!leq_bump /unbump /bump; case: (leqP h1 h2) => [le_h12 | lt_h21]. by rewrite subn0 ltnS le_h12 subn1. by rewrite subn1 (ltn_predK lt_h21) (leqNgt h1) lt_h21 subn0.] Proof search time: 3 min, 4 sec Results for lemma invF_f: : cancel f invF FAILURE! Tactics applied: 100000 Original Proof: [by move=> x; exact: iinv_f.] Proof search time: 3 min, 18 sec Results for lemma eq_cardT: A : A =i predT -> #|A| = size (enum T) SUCCESS! Proof Found in EFSM: [rewrite /= size_map -enumT -cardE , by apply eq_card => x] Tactics applied: 9113 Original Proof: [exact: eq_card_trans cardT.] Shorter Proof Found? no This is a novel proof This proof contained a loop around a state proof search time: 0 min, 12 sec Results for lemma imageP: A y : reflect (exists2 x, x \in A & y = f x) (y \in image f A) FAILURE! Tactics applied: 100000 Original Proof: [by apply: (iffP mapP) => [] [x Ax y_fx]; exists x; rewrite // mem_enum in Ax *.] Proof search time: 4 min, 40 sec Results for lemma unbumpK: h : {in predC1 h, cancel (unbump h) (bump h)} FAILURE! Tactics applied: 100000 Original Proof: [by move=> i; move/negbTE=> neq_h_i; rewrite unbumpKcond neq_h_i.] Proof search time: 4 min, 7 sec Results for lemma negb_exists: P : ~~ [exists x, P x] = [forall x, ~~ P x] FAILURE! Tactics applied: 100000 Original Proof: [by apply/negbLR/esym/eq_existsb=> x; apply: negbK.] Proof search time: 2 min, 53 sec Results for lemma image_pre: (B : pred T') : image f [preim f of B] =i [predI B & codom f] FAILURE! Tactics applied: 100000 Original Proof: [by move=> y; rewrite /image_mem -filter_map /= mem_filter -enumT.] Proof search time: 5 min, 10 sec Results for lemma val_enum_ord: : map val (enum 'I_n) = iota 0 n FAILURE! Tactics applied: 100000 Original Proof: [by rewrite enumT unlock val_ord_enum.] Proof search time: 4 min, 8 sec Results for lemma unlift_none: n (h : 'I_n) : unlift h h = None FAILURE! Tactics applied: 100000 Original Proof: [by case: unliftP => // j Dh; case/eqP: (neq_lift h j).] Proof search time: 3 min, 1 sec Results for lemma exists_eqP: f1 f2 : reflect (exists x, f1 x = f2 x) [exists x, f1 x == f2 x] FAILURE! Tactics applied: 100000 Original Proof: [by apply: (iffP (existsP _)) => [] [x /eqP]; exists x.] Proof search time: 3 min, 50 sec Results for lemma negb_forall: P : ~~ [forall x, P x] = [exists x, ~~ P x] SUCCESS! Proof Found in EFSM: [by [] ] Tactics applied: 44 Original Proof: [by [].] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 3 sec Results for lemma arg_maxP: : extremum_spec geq arg_max FAILURE! Tactics applied: 100000 Original Proof: [rewrite /arg_max; case: pickP => [i /andP[Pi /forall_inP/= max_i] | no_i]. by split=> // j; apply/implyP. have (n): FP n -> n <= foldr maxn 0 (map F (enum P)). case/existsP=> i; rewrite -[P i]mem_enum andbC /= => /andP[/eqP <-]. elim: (enum P) => //= j e IHe; rewrite leq_max orbC !inE. by case/predU1P=> [-> | /IHe-> //]; rewrite leqnn orbT. case/ex_maxnP=> // n ex_i max_i; case/pred0P: ex_i => i /=. apply: contraFF (no_i i) => /andP[Pi def_n]; rewrite /= Pi. by apply/forall_inP=> j Pj; rewrite (eqP def_n) max_i ?FP_F.] Proof search time: 3 min, 32 sec Results for lemma bij_on_codom: (x0 : T) : {on [pred y in codom f], bijective f} FAILURE! Tactics applied: 100000 Original Proof: [pose g y := iinv (valP (insigd (codom_f x0) y)). by exists g => [x fAfx | y fAy]; first apply: injf; rewrite f_iinv insubdK.] Proof search time: 3 min, 45 sec Results for lemma card0: : #|@pred0 T| = 0 FAILURE! Tactics applied: 100000 Original Proof: [by rewrite cardE enum0.] Proof search time: 2 min, 26 sec Results for lemma leq_bump: h i j : (i <= bump h j) = (unbump h i <= j) FAILURE! Tactics applied: 100000 Original Proof: [rewrite /bump leq_subLR. case: (leqP i h) (leqP h j) => [le_i_h | lt_h_i] [le_h_j | lt_j_h] //. by rewrite leqW (leq_trans le_i_h). by rewrite !(leqNgt i) ltnW (leq_trans _ lt_h_i).] Proof search time: 3 min, 5 sec Results for lemma lshift_subproof: m n (i : 'I_m) : i < m + n FAILURE! Tactics applied: 100000 Original Proof: [by apply: leq_trans (valP i) _; exact: leq_addr.] Proof search time: 3 min, 10 sec Results for lemma val_sub_enum: : map val sub_enum = enum P FAILURE! Tactics applied: 100000 Original Proof: [rewrite pmap_filter; last exact: insubK. by apply: eq_filter => x; exact: isSome_insub.] Proof search time: 3 min, 58 sec Results for lemma inj_card_onto: y : y \in codom f FAILURE! Tactics applied: 100000 Original Proof: [by move: y; apply/subset_cardP; rewrite ?card_codom ?subset_predT.] Proof search time: 3 min, 36 sec Results for lemma leq_ord: (i : 'I_n) : i <= n' SUCCESS! Proof Found in EFSM: [exact valP i ] Tactics applied: 180 Original Proof: [exact: valP i.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 5 sec Results for lemma subset_all: s A : (s \subset A) = all (mem A) s FAILURE! Tactics applied: 100000 Original Proof: [by exact (sameP (subsetP _ _) allP).] Proof search time: 3 min, 31 sec Results for lemma enum_default: A : 'I_(#|A|) -> T FAILURE! Tactics applied: 100000 Original Proof: [by rewrite cardE; case: (enum A) => [|//] [].] Proof search time: 3 min, 8 sec Results for lemma disjoint_cat: s1 s2 A : [disjoint s1 ++ s2 & A] = [disjoint s1 & A] && [disjoint s2 & A] FAILURE! Tactics applied: 100000 Original Proof: [by rewrite !disjoint_has has_cat negb_or.] Proof search time: 4 min, 12 sec Results for lemma mem_sub_enum: u : u \in sub_enum FAILURE! Tactics applied: 100000 Original Proof: [by rewrite mem_pmap_sub -enumT mem_enum.] Proof search time: 4 min, 15 sec Results for fold 7 Results for lemma splitP: m n (i : 'I_(m + n)) : split_spec i (split i) (i < m) FAILURE! Tactics applied: 100000 Original Proof: [rewrite /split {-3}/leq. by case: (@ltnP i m) => cmp_i_m //=; constructor; rewrite ?subnKC.] Proof search time: 3 min, 11 sec Results for lemma dinjectiveP: D : reflect {in D &, injective f} (dinjectiveb D) FAILURE! Tactics applied: 100000 Original Proof: [rewrite -[dinjectiveb D]negbK. case: dinjectivePn=> [noinjf | injf]; constructor. case: noinjf => x Dx [y /andP[neqxy /= Dy] eqfxy] injf. by case/eqP: neqxy; exact: injf. move=> x y Dx Dy /= eqfxy; apply/eqP; apply/idPn=> nxy; case: injf. by exists x => //; exists y => //=; rewrite inE /= eq_sym nxy.] Proof search time: 4 min, 35 sec Results for lemma cardC1: x : #|predC1 x| = #|T|.-1 FAILURE! Tactics applied: 100000 Original Proof: [by rewrite -(cardC (pred1 x)) card1.] Proof search time: 2 min, 57 sec Results for lemma size_image: A : size (image f A) = #|A| FAILURE! Tactics applied: 100000 Original Proof: [by rewrite size_map -cardE.] Proof search time: 3 min, 12 sec Results for lemma eq_forallb: P1 P2 : P1 =1 P2 -> [forall x, P1 x] = [forall x, P2 x] FAILURE! Tactics applied: 100000 Original Proof: [by move=> eqP12; apply/negb_inj/eq_existsb=> /= x; rewrite eqP12.] Proof search time: 3 min, 23 sec Results for lemma pre_image: A : [preim f of image f A] =i A FAILURE! Tactics applied: 100000 Original Proof: [by move=> x; rewrite inE /= mem_image.] Proof search time: 4 min, 12 sec Results for lemma sub_enum_uniq: : uniq sub_enum FAILURE! Tactics applied: 100000 Original Proof: [by rewrite pmap_sub_uniq // -enumT enum_uniq.] Proof search time: 3 min, 10 sec Results for lemma eq_card0: A : A =i pred0 -> #|A| = 0 FAILURE! Tactics applied: 100000 Original Proof: [exact: eq_card_trans card0.] Proof search time: 3 min, 0 sec Results for lemma image_iinv: A y (fTy : y \in codom f) : (y \in image f A) = (iinv fTy \in A) FAILURE! Tactics applied: 100000 Original Proof: [by rewrite -mem_image ?f_iinv.] Proof search time: 4 min, 39 sec Results for lemma enum_valP: A i : @enum_val A i \in A FAILURE! Tactics applied: 100000 Original Proof: [by rewrite -mem_enum mem_nth -?cardE.] Proof search time: 3 min, 6 sec Results for lemma canF_RL: x y : g x = y -> x = f y FAILURE! Tactics applied: 100000 Original Proof: [exact: canRL canF_sym.] Proof search time: 3 min, 21 sec Results for lemma eq_card_trans: A B n : #|A| = n -> B =i A -> #|B| = n FAILURE! Tactics applied: 100000 Original Proof: [move <-; exact: eq_card.] Proof search time: 3 min, 22 sec Results for lemma lift0: (i : 'I_n') : lift ord0 i = i.+1 :> nat SUCCESS! Proof Found in EFSM: [by [] ] Tactics applied: 97 Original Proof: [by [].] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 5 sec Results for lemma enum_val_bij: : bijective (@enum_val T) FAILURE! Tactics applied: 100000 Original Proof: [by move: enum_rankK enum_valK; exists enum_rank.] Proof search time: 3 min, 22 sec Results for lemma fin_all_exists: U (P : forall x : T, U x -> Prop) : (forall x, exists u, P x u) -> (exists u, forall x, P x (u x)) FAILURE! Tactics applied: 100000 Original Proof: [move=> ex_u; pose Q m x := enum_rank x < m -> {ux | P x ux}. suffices: forall m, m <= #|T| -> exists w : forall x, Q m x, True. case/(_ #|T|)=> // w _; pose u x := sval (w x (ltn_ord _)). by exists u => x; rewrite {}/u; case: (w x _). elim=> [|m IHm] ltmX; first by have w x: Q 0 x by []; exists w. have{IHm} [w _] := IHm (ltnW ltmX); pose i := Ordinal ltmX. have [u Pu] := ex_u (enum_val i); suffices w' x: Q m.+1 x by exists w'. rewrite /Q ltnS leq_eqVlt (val_eqE _ i); case: eqP => [def_i _ | _ /w //]. by rewrite -def_i enum_rankK in u Pu; exists u.] Proof search time: 3 min, 14 sec Results for lemma ltn_ord: (i : ordinal) : i < n SUCCESS! Proof Found in EFSM: [exact valP i ] Tactics applied: 57 Original Proof: [exact: valP i.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 4 sec Results for lemma proper_trans: A B C : A \proper B -> B \proper C -> A \proper C FAILURE! Tactics applied: 100000 Original Proof: [case/properP=> sAB [x Bx nAx] /properP[sBC [y Cy nBy]]. rewrite properE (subset_trans sAB) //=; apply/subsetPn; exists y => //. by apply: contra nBy; exact: subsetP.] Proof search time: 4 min, 17 sec Results for lemma bumpK: h : cancel (bump h) (unbump h) FAILURE! Tactics applied: 100000 Original Proof: [rewrite /bump /unbump => i. have [le_hi | lt_ih] := leqP h i; first by rewrite ltnS le_hi subn1. by rewrite ltnNge ltnW ?subn0.] Proof search time: 2 min, 55 sec Results for lemma canF_LR: x y : x = g y -> f x = y FAILURE! Tactics applied: 100000 Original Proof: [exact: canLR canF_sym.] Proof search time: 3 min, 20 sec Results for lemma eq_card1: x A : A =i pred1 x -> #|A| = 1 FAILURE! Tactics applied: 100000 Original Proof: [exact: eq_card_trans (card1 x).] Proof search time: 3 min, 20 sec Results for lemma card_tagged: : #|{: {i : I & T_ i}}| = sumn (map (fun i => #|T_ i|) (enum I)) FAILURE! Tactics applied: 100000 Original Proof: [rewrite cardE !enumT {1}unlock size_flatten /shape -map_comp. by congr (sumn _); apply: eq_map => i; rewrite /= size_map -enumT -cardE.] Proof search time: 4 min, 39 sec Results for lemma lift_max: (i : 'I_n') : lift ord_max i = i :> nat FAILURE! Tactics applied: 100000 Original Proof: [by rewrite /= /bump leqNgt ltn_ord.] Proof search time: 2 min, 48 sec Results for lemma nth_codom: T' y0 (f : T -> T') (i : 'I_#|T|) : nth y0 (codom f) i = f (enum_val i) SUCCESS! Proof Found in EFSM: [by rewrite -(nth_map _ y0) // -cardE ] Tactics applied: 169 Original Proof: [exact: nth_image.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 5 sec Results for lemma ltn_unsplit: m n (jk : 'I_m + 'I_n) : (unsplit jk < m) = jk FAILURE! Tactics applied: 100000 Original Proof: [by case: jk => [j|k]; rewrite /= ?ltn_ord // ltnNge leq_addr.] Proof search time: 3 min, 7 sec Results for lemma card0_eq: A : #|A| = 0 -> A =i pred0 FAILURE! Tactics applied: 100000 Original Proof: [by move=> A0 x; apply/idP => Ax; rewrite (cardD1 x) Ax in A0.] Proof search time: 2 min, 52 sec Results for fold 8 Results for lemma existsP: P : reflect (exists x, P x) [exists x, P x] SUCCESS! Proof Found in EFSM: [exact pred0Pn ] Tactics applied: 130 Original Proof: [by apply: (iffP pred0Pn) => [] [x]; exists x.] Shorter Proof Found? yes Single step proof reused proof search time: 0 min, 3 sec Results for lemma subset_disjoint: A B : (A \subset B) = [disjoint A & [predC B]] FAILURE! Tactics applied: 100000 Original Proof: [by rewrite disjoint_sym unlock.] Proof search time: 1 min, 25 sec Results for lemma dinjectivePn: D : reflect (exists2 x, x \in D & exists2 y, y \in [predD1 D & x] & f x = f y) (~~ dinjectiveb D) FAILURE! Tactics applied: 100000 Original Proof: [apply: (iffP idP) => [injf | [x Dx [y Dxy eqfxy]]]; last first. move: Dx; rewrite -(mem_enum D) => /rot_to[i E defE]. rewrite /dinjectiveb -(rot_uniq i) -map_rot defE /=; apply/nandP; left. rewrite inE /= -(mem_enum D) -(mem_rot i) defE inE in Dxy. rewrite andb_orr andbC andbN in Dxy. by rewrite eqfxy map_f //; case/andP: Dxy. pose p := [pred x in D | [exists (y | y \in [predD1 D & x]), f x == f y]]. case: (pickP p) => [x /= /andP[Dx /exists_inP[y Dxy /eqP eqfxy]] | no_p]. by exists x; last exists y. rewrite /dinjectiveb map_inj_in_uniq ?enum_uniq // in injf => x y Dx Dy eqfxy. apply: contraNeq (negbT (no_p x)) => ne_xy /=; rewrite -mem_enum Dx. by apply/existsP; exists y; rewrite /= !inE eq_sym ne_xy -mem_enum Dy eqfxy /=.] Proof search time: 2 min, 36 sec Results for lemma eq_image: (A B : pred T) (f g : T -> T') : A =i B -> f =1 g -> image f A = image g B FAILURE! Tactics applied: 100000 Original Proof: [by move=> eqAB eqfg; rewrite /image_mem (eq_enum eqAB) (eq_map eqfg).] Proof search time: 1 min, 50 sec Results for lemma card_prod: : #|{: T1 * T2}| = #|T1| * #|T2| SUCCESS! Proof Found in EFSM: [by rewrite -predX_prod_enum unlock -count_filter unlock ] Tactics applied: 217 Original Proof: [by rewrite -cardX; apply: eq_card; case.] Shorter Proof Found? yes Single step proof reused proof search time: 0 min, 5 sec Results for lemma enum_valK: : cancel enum_val enum_rank FAILURE! Tactics applied: 100000 Original Proof: [by move=> x; exact: enum_valK_in.] Proof search time: 2 min, 0 sec Results for lemma codomE: : codom f = map f (enum T) SUCCESS! Proof Found in EFSM: [by [] ] Tactics applied: 139 Original Proof: [by [].] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 3 sec Results for lemma card2: x y : #|pred2 x y| = (x != y).+1 FAILURE! Tactics applied: 100000 Original Proof: [by rewrite cardU1 card1 addn1.] Proof search time: 1 min, 35 sec Results for lemma mem_seq_sub_enum: x : x \in seq_sub_enum FAILURE! Tactics applied: 100000 Original Proof: [by rewrite mem_undup mem_pmap -valK map_f ?ssvalP.] Proof search time: 2 min, 24 sec Results for lemma prod_enumP: : Finite.axiom prod_enum FAILURE! Tactics applied: 100000 Original Proof: [by case=> x1 x2; rewrite (predX_prod_enum (pred1 x1) (pred1 x2)) !card1.] Proof search time: 2 min, 21 sec Results for lemma bij_on_image: A (x0 : T) : {on [pred y in image f A], bijective f} FAILURE! Tactics applied: 100000 Original Proof: [exact: subon_bij (@image_codom A) (bij_on_codom x0).] Proof search time: 1 min, 57 sec Results for lemma arg_minP: : extremum_spec leq arg_min FAILURE! Tactics applied: 100000 Original Proof: [rewrite /arg_min; case: pickP => [i /andP[Pi /forallP/= min_i] | no_i]. by split=> // j; apply/implyP. case/ex_minnP: exFP => n ex_i min_i; case/pred0P: ex_i => i /=. apply: contraFF (no_i i) => /andP[Pi /eqP def_n]; rewrite /= Pi. by apply/forall_inP=> j Pj; rewrite def_n min_i ?FP_F.] Proof search time: 1 min, 40 sec Results for lemma eq_card_sub: (A : pred sfT) : A =i predT -> #|A| = #|[pred x | P x]| FAILURE! Tactics applied: 100000 Original Proof: [exact: eq_card_trans card_sub.] Proof search time: 2 min, 9 sec Results for lemma enum_valK_in: x0 A Ax0 : cancel enum_val (@enum_rank_in x0 A Ax0) FAILURE! Tactics applied: 100000 Original Proof: [move=> x; apply: ord_inj; rewrite insubdK; last first. by rewrite cardE [_ \in _]index_mem mem_nth // -cardE. by rewrite index_uniq ?enum_uniq // -cardE.] Proof search time: 1 min, 59 sec Results for lemma eq_proper_r: A B : A =i B -> (@proper T)^~ (mem A) =1 (@proper T)^~ (mem B) FAILURE! Tactics applied: 100000 Original Proof: [move=> eAB [C]; congr (_ && _); first exact: (eq_subset_r eAB). by rewrite (eq_subset eAB).] Proof search time: 1 min, 43 sec Results for lemma proper_card: A B : A \proper B -> #|A| < #|B| FAILURE! Tactics applied: 100000 Original Proof: [by case/andP=> sAB nsBA; rewrite ltn_neqAle !(subset_leqif_card sAB) andbT.] Proof search time: 1 min, 42 sec Results for lemma eq_invF: f g injf injg : f =1 g -> @invF T f injf =1 @invF T g injg FAILURE! Tactics applied: 100000 Original Proof: [by move=> eq_fg x; apply: (canLR (invF_f injf)); rewrite eq_fg f_invF.] Proof search time: 1 min, 55 sec Results for lemma enum_val_bij_in: x0 A : x0 \in A -> {on A, bijective (@enum_val A)} FAILURE! Tactics applied: 100000 Original Proof: [move=> Ax0; exists (enum_rank_in Ax0) => [i _|]; last exact: enum_rankK_in. exact: enum_valK_in.] Proof search time: 1 min, 58 sec Results for lemma unbumpKcond: h i : bump h (unbump h i) = (i == h) + i FAILURE! Tactics applied: 100000 Original Proof: [rewrite /bump /unbump leqNgt -subSKn. case: (ltngtP i h) => /= [-> | ltih | ->] //; last by rewrite ltnn. by rewrite subn1 /= leqNgt !(ltn_predK ltih, ltih, add1n).] Proof search time: 2 min, 7 sec Results for lemma cast_ord_comp: n1 n2 n3 eq_n2 eq_n3 i : @cast_ord n2 n3 eq_n3 (@cast_ord n1 n2 eq_n2 i) = cast_ord (etrans eq_n2 eq_n3) i SUCCESS! Proof Found in EFSM: [exact val_inj ] Tactics applied: 138 Original Proof: [exact: val_inj.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 4 sec Results for lemma nth_enum_ord: i0 m : m < n -> nth i0 (enum 'I_n) m = m :> nat FAILURE! Tactics applied: 100000 Original Proof: [by move=> ?; rewrite -(nth_map _ 0) (size_enum_ord, val_enum_ord) // nth_iota.] Proof search time: 1 min, 54 sec Results for lemma canF_eq: x y : (f x == y) = (x == g y) FAILURE! Tactics applied: 100000 Original Proof: [exact: (can2_eq fK canF_sym).] Proof search time: 1 min, 53 sec Results for lemma leq_image_card: A : #|image f A| <= #|A| FAILURE! Tactics applied: 100000 Original Proof: [by rewrite (cardE A) -(size_map f) card_size.] Proof search time: 1 min, 53 sec Results for lemma disjoint_subset: A B : [disjoint A & B] = (A \subset [predC B]) FAILURE! Tactics applied: 100000 Original Proof: [by rewrite subset_disjoint; apply: eq_disjoint_r => x; rewrite !inE /= negbK.] Proof search time: 1 min, 37 sec Results for lemma forallP: P : reflect (forall x, P x) [forall x, P x] FAILURE! Tactics applied: 100000 Original Proof: [by apply: (iffP pred0P) => /= P_ x; rewrite /= ?P_ ?(negbFE (P_ x)).] Proof search time: 1 min, 39 sec Results for fold 9 Results for lemma pred0Pn: P : reflect (exists x, P x) (~~ pred0b P) FAILURE! Tactics applied: 100000 Original Proof: [case: (pickP P) => [x Px | P0]. by rewrite (introN (pred0P P)) => [|P0]; [left; exists x | rewrite P0 in Px]. by rewrite -lt0n eq_card0 //; right=> [[x]]; rewrite P0.] Proof search time: 1 min, 23 sec Results for lemma subxx: (pT : predType T) (pA : pT) : pA \subset pA SUCCESS! Proof Found in EFSM: [by [] ] Tactics applied: 6 Original Proof: [by [].] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 2 sec Results for lemma canF_invF: : g =1 invF (can_inj fK) FAILURE! Tactics applied: 100000 Original Proof: [by move=> y; apply: (canLR fK); rewrite f_invF.] Proof search time: 2 min, 32 sec Results for lemma mem_image: A x : (f x \in image f A) = (x \in A) FAILURE! Tactics applied: 100000 Original Proof: [by rewrite mem_map ?mem_enum.] Proof search time: 2 min, 38 sec Results for lemma proper_sub_trans: A B C : A \proper B -> B \subset C -> A \proper C FAILURE! Tactics applied: 100000 Original Proof: [case/properP=> sAB [x Bx nAx] sBC; rewrite properE (subset_trans sAB) //. by apply/subsetPn; exists x; rewrite ?(subsetP _ _ sBC).] Proof search time: 2 min, 28 sec Results for lemma cast_ord_inj: n1 n2 eq_n : injective (@cast_ord n1 n2 eq_n) FAILURE! Tactics applied: 100000 Original Proof: [exact: can_inj (cast_ordK eq_n).] Proof search time: 2 min, 44 sec Results for lemma enum_ordS: : enum 'I_n = ord0 :: map (lift ord0) (enum 'I_n') FAILURE! Tactics applied: 100000 Original Proof: [apply: (inj_map val_inj); rewrite val_enum_ord /= -map_comp. by rewrite (map_comp (addn 1)) val_enum_ord -iota_addl.] Proof search time: 3 min, 5 sec Results for lemma cardUI: A B : #|[predU A & B]| + #|[predI A & B]| = #|A| + #|B| FAILURE! Tactics applied: 100000 Original Proof: [by rewrite !cardE -!count_filter count_predUI.] Proof search time: 1 min, 49 sec Results for lemma rshift_subproof: m n (i : 'I_n) : m + i < m + n FAILURE! Tactics applied: 100000 Original Proof: [by rewrite ltn_add2l.] Proof search time: 3 min, 24 sec Results for lemma eq_forallb_in: D P1 P2 : (forall x, D x -> P1 x = P2 x) -> [forall (x | D x), P1 x] = [forall (x | D x), P2 x] FAILURE! Tactics applied: 100000 Original Proof: [by move=> eqP12; apply: eq_forallb => i; case Di: (D i); rewrite // eqP12.] Proof search time: 3 min, 10 sec Results for lemma tag_enumP: : Finite.axiom tag_enum FAILURE! Tactics applied: 100000 Original Proof: [case=> i x; rewrite -(enumP i) /tag_enum -enumT. elim: (enum I) => //= j e IHe. rewrite count_cat count_map {}IHe; congr (_ + _). rewrite count_filter -cardE /=; case: eqP => [-> | ne_j_i]. by apply: (@eq_card1 _ x) => y; rewrite -topredE /= tagged_asE ?eqxx. by apply: eq_card0 => y.] Proof search time: 3 min, 0 sec Results for lemma preim_iinv: A B y fAy : preim f B (@iinv A y fAy) = B y FAILURE! Tactics applied: 100000 Original Proof: [by rewrite /= f_iinv.] Proof search time: 2 min, 54 sec Results for lemma cardU1: x A : #|[predU1 x & A]| = (x \notin A) + #|A| FAILURE! Tactics applied: 100000 Original Proof: [case Ax: (x \in A). by apply: eq_card => y; rewrite inE /=; case: eqP => // ->. rewrite /= -(card1 x) -cardUI addnC. rewrite [#|predI _ _|]eq_card0 => [|y /=]; first exact: eq_card. by rewrite !inE; case: eqP => // ->.] Proof search time: 1 min, 34 sec Results for lemma unbump_addl: h i k : unbump (k + h) (k + i) = k + unbump h i FAILURE! Tactics applied: 100000 Original Proof: [apply: (can_inj (bumpK (k + h))). by rewrite bump_addl !unbumpKcond eqn_add2l addnCA.] Proof search time: 2 min, 32 sec Results for lemma eqfunP: f1 f2 : reflect (forall x, f1 x = f2 x) [forall x, f1 x == f2 x] FAILURE! Tactics applied: 100000 Original Proof: [by apply: (iffP (forallP _)) => eq_f12 x; apply/eqP/eq_f12.] Proof search time: 2 min, 26 sec Results for lemma nth_enum_rank_in: x00 x0 A Ax0 : {in A, cancel (@enum_rank_in x0 A Ax0) (nth x00 (enum A))} FAILURE! Tactics applied: 100000 Original Proof: [move=> x Ax; rewrite /= insubdK ?nth_index ?mem_enum //. by rewrite cardE [_ \in _]index_mem mem_enum.] Proof search time: 4 min, 40 sec Results for lemma widen_ord_proof: n m (i : 'I_n) : n <= m -> i < m FAILURE! Tactics applied: 100000 Original Proof: [exact: leq_trans.] Proof search time: 3 min, 19 sec Results for lemma lift_inj: n (h : 'I_n) : injective (lift h) FAILURE! Tactics applied: 100000 Original Proof: [move=> i1 i2; move/eqP; rewrite [_ == _](can_eq (@bumpK _)) => eq_i12. exact/eqP.] Proof search time: 2 min, 57 sec Results for lemma sub_ord_proof: m : n' - m < n FAILURE! Tactics applied: 100000 Original Proof: [by rewrite ltnS leq_subr.] Proof search time: 2 min, 41 sec Results for lemma card_gt0P: A : reflect (exists i, i \in A) (#|A| > 0) FAILURE! Tactics applied: 100000 Original Proof: [rewrite lt0n; exact: pred0Pn.] Proof search time: 1 min, 33 sec Results for lemma enum_val_inj: A : injective (@enum_val A) FAILURE! Tactics applied: 100000 Original Proof: [by move=> i; exact: can_inj (enum_valK_in (enum_valP i)) (i).] Proof search time: 2 min, 50 sec Results for lemma unsplitK: m n : cancel (@unsplit m n) (@split m n) FAILURE! Tactics applied: 100000 Original Proof: [move=> jk; have:= ltn_unsplit jk. by do [case: splitP; case: jk => //= i j] => [|/addnI] => /ord_inj->.] Proof search time: 2 min, 54 sec Results for lemma enum_rank_inj: : injective enum_rank FAILURE! Tactics applied: 100000 Original Proof: [exact: can_inj enum_rankK.] Proof search time: 3 min, 8 sec Results for lemma eq_pick: P Q : P =1 Q -> pick P = pick Q FAILURE! Tactics applied: 100000 Original Proof: [by move=> eqPQ; rewrite /pick (eq_enum eqPQ).] Proof search time: 1 min, 43 sec Results for lemma index_enum_ord: (i : 'I_n) : index i (enum 'I_n) = i FAILURE! Tactics applied: 100000 Original Proof: [by rewrite -{1}(nth_ord_enum i i) index_uniq ?(enum_uniq, size_enum_ord).] Proof search time: 2 min, 35 sec Results for fold 10 Results for lemma eq_existsb_in: D P1 P2 : (forall x, D x -> P1 x = P2 x) -> [exists (x | D x), P1 x] = [exists (x | D x), P2 x] FAILURE! Tactics applied: 100000 Original Proof: [by move=> eqP12; apply: eq_existsb => x; apply: andb_id2l => /eqP12.] Proof search time: 2 min, 39 sec Results for lemma unbumpS: h i : unbump h.+1 i.+1 = (unbump h i).+1 FAILURE! Tactics applied: 100000 Original Proof: [exact: unbump_addl 1.] Proof search time: 2 min, 42 sec Results for lemma card_bool: : #|{: bool}| = 2 SUCCESS! Proof Found in EFSM: [by rewrite cardT enumT unlock ] Tactics applied: 169 Original Proof: [by rewrite cardT enumT unlock.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 4 sec Results for lemma card_in_image: A : {in A &, injective f} -> #|image f A| = #|A| FAILURE! Tactics applied: 100000 Original Proof: [move=> injf; rewrite (cardE A) -(size_map f); apply/card_uniqP. rewrite map_inj_in_uniq ?enum_uniq // => x y; rewrite !mem_enum; exact: injf.] Proof search time: 3 min, 19 sec Results for lemma eq_disjoint0: A B : A =i pred0 -> [disjoint A & B] SUCCESS! Proof Found in EFSM: [by move/eq_disjoint->;, exact /pred0P ] Tactics applied: 18766 Original Proof: [by move/eq_disjoint->; exact: disjoint0.] Shorter Proof Found? no This is a novel proof proof search time: 0 min, 24 sec Results for lemma size_enum_ord: : size (enum 'I_n) = n FAILURE! Tactics applied: 100000 Original Proof: [by rewrite -(size_map val) val_enum_ord size_iota.] Proof search time: 2 min, 25 sec Results for lemma eq_proper: A B : A =i B -> proper (mem A) =1 proper (mem B) FAILURE! Tactics applied: 100000 Original Proof: [move=> eAB [C]; congr (_ && _); first exact: (eq_subset eAB). by rewrite (eq_subset_r eAB).] Proof search time: 2 min, 12 sec Results for lemma f_invF: : cancel invF f SUCCESS! Proof Found in EFSM: [by move=> ?;, by rewrite /= f_iinv ] Tactics applied: 20157 Original Proof: [by move=> y; exact: f_iinv.] Shorter Proof Found? no This is a novel proof This proof contained a loop around a state proof search time: 0 min, 34 sec Results for lemma disjointU: A B C : [disjoint predU A B & C] = [disjoint A & C] && [disjoint B & C] FAILURE! Tactics applied: 100000 Original Proof: [case: [disjoint A & C] / (pred0P (xpredI A C)) => [A0 | nA0] /=. by congr (_ == 0); apply: eq_card => x; rewrite [x \in _]andb_orl A0. apply/pred0P=> nABC; case: nA0 => x; apply/idPn=> /=; move/(_ x): nABC. by rewrite [_ x]andb_orl; case/norP.] Proof search time: 2 min, 35 sec Results for lemma disjoint_trans: A B C : A \subset B -> [disjoint B & C] -> [disjoint A & C] FAILURE! Tactics applied: 100000 Original Proof: [by rewrite 2!disjoint_subset; exact: subset_trans.] Proof search time: 2 min, 32 sec Results for lemma splitK: m n : cancel (@split m n) (@unsplit m n) FAILURE! Tactics applied: 100000 Original Proof: [by move=> i; apply: val_inj; case: splitP.] Proof search time: 3 min, 8 sec Results for lemma injectiveP: : reflect (injective f) injectiveb FAILURE! Tactics applied: 100000 Original Proof: [apply: (iffP (dinjectiveP _)) => injf x y => [|_ _]; exact: injf.] Proof search time: 2 min, 32 sec Results for lemma cast_ordK: n1 n2 eq_n : cancel (@cast_ord n1 n2 eq_n) (cast_ord (esym eq_n)) SUCCESS! Proof Found in EFSM: [by case=> x1 x2;, apply val_inj] Tactics applied: 17112 Original Proof: [by move=> i; exact: val_inj.] Shorter Proof Found? no This is a novel proof This proof contained a loop around a state proof search time: 0 min, 32 sec Results for lemma subxx_hint: (mA : mem_pred T) : subset mA mA FAILURE! Tactics applied: 100000 Original Proof: [by case: mA => A; have:= introT (subsetP A A); rewrite !unlock => ->.] Proof search time: 1 min, 41 sec Results for lemma card_image: A : #|image f A| = #|A| FAILURE! Tactics applied: 100000 Original Proof: [apply: card_in_image; exact: in2W.] Proof search time: 2 min, 59 sec Results for lemma proper_sub: A B : A \proper B -> A \subset B SUCCESS! Proof Found in EFSM: [by case/andP ] Tactics applied: 103 Original Proof: [by case/andP.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 2 sec Results for lemma predX_prod_enum: (A1 : pred T1) (A2 : pred T2) : count [predX A1 & A2] prod_enum = #|A1| * #|A2| FAILURE! Tactics applied: 100000 Original Proof: [rewrite !cardE -!count_filter -!enumT /prod_enum. elim: (enum T1) => //= x1 s1 IHs; rewrite count_cat {}IHs count_map /preim /=. by case: (x1 \in A1); rewrite ?count_pred0.] Proof search time: 2 min, 59 sec Results for lemma seq_sub_pickleK: : pcancel seq_sub_pickle seq_sub_unpickle FAILURE! Tactics applied: 100000 Original Proof: [rewrite /seq_sub_unpickle => x. by rewrite (nth_map x) ?nth_index ?index_mem ?mem_seq_sub_enum.] Proof search time: 2 min, 48 sec OVERALL RESULTS SUMMARY EFSMProver proved 42 out of 243 lemmas. Success rate of 17.28395061728395% There were 0 errors. 201 proof attempts exhausted the automaton On average, a proof was found after applying 4229 tactics The longest proof consisted of 3 tactics There were 2 shorter proofs found Of the 201 failures, 201 of them used all 100000 tactics There were 28 reused proofs found There were 14 novel proofs found Of the 201 failures, the average number of tactics used was 100000On average, a proof was found after 0 min, 9 sec On average, a failed proof attempt took 2 min, 47 sec On average, any (success or failure) proof attempt took 2 min, 20 sec The longest time to find a proof was 0 min, 58 sec The shortest time to find a proof was 0 min, 1 sec There were 0 proofs containing repeated tactics There were 4 proofs that repeated states