Results for fold 1 Results for lemma canLR_on: x y : {on D2, cancel f & g} -> f y \in D2 -> x = f y -> g x = y SUCCESS! Proof Found in EFSM: [by move=> fK D1y ->;, auto ] Tactics applied: 1385 Original Proof: [by move=> fK D2fy ->; rewrite fK.] Shorter Proof Found? no This is a novel proof proof search time: 0 min, 2 sec Results for lemma introTn: : ~ P -> b' FAILURE! Tactics applied: 100000 Original Proof: [exact: introTFn true _.] Proof search time: 2 min, 15 sec Results for lemma classic_bind: : forall P Q, (P -> classically Q) -> (classically P -> classically Q) FAILURE! Tactics applied: 100000 Original Proof: [by move=> P Q IH IH_P b IH_Q; apply: IH_P; move/IH; exact.] Proof search time: 1 min, 29 sec Results for lemma addbCA: : left_commutative addb SUCCESS! Proof Found in EFSM: [by do 2!case ] Tactics applied: 22 Original Proof: [by do 3!case.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Results for lemma sub_in2: T d d' (P : T -> T -> Prop) : sub_mem d d' -> forall Ph : ph {all2 P}, prop_in2 d' Ph -> prop_in2 d Ph SUCCESS! Proof Found in EFSM: [by move=> Hf x y hx hy /Hf;, auto ] Tactics applied: 1063 Original Proof: [by move=> /= sub_dd'; exact: sub_in11.] Shorter Proof Found? no This is a novel proof proof search time: 0 min, 1 sec Results for lemma homo_mono: : {homo f : x y / aR x y >-> rR x y} -> {homo g : x y / rR x y >-> aR x y} -> {mono g : x y / rR x y >-> aR x y} FAILURE! Tactics applied: 100000 Original Proof: [move=> mf mg x y; case: (boolP (rR _ _))=> [/mg //|]. by apply: contraNF=> /mf; rewrite !fgK.] Proof search time: 1 min, 35 sec Results for lemma monoRL: : {mono f : x y / aR x y >-> rR x y} -> forall x y, rR x (f y) = aR (g x) y SUCCESS! Proof Found in EFSM: [by move=> mf x y /=;, rewrite -mf !fgK ] Tactics applied: 1719 Original Proof: [by move=> mf x y; rewrite -{1}[x]fgK mf.] Shorter Proof Found? no Proof reused from can_mono proof search time: 0 min, 2 sec Results for lemma sub_in21: T T3 d d' d3 d3' (P : T -> T -> T3 -> Prop) : sub_mem d d' -> sub_mem d3 d3' -> forall Ph : ph {all3 P}, prop_in21 d' d3' Ph -> prop_in21 d d3 Ph SUCCESS! Proof Found in EFSM: [by move=> /= sub1 sub;, exact sub_in111 ] Tactics applied: 904 Original Proof: [by move=> /= sub sub3; exact: sub_in111.] Shorter Proof Found? no Proof reused from sub_in12 proof search time: 0 min, 1 sec Results for lemma addbb: : self_inverse false addb SUCCESS! Proof Found in EFSM: [by case ] Tactics applied: 2 Original Proof: [by case.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Results for lemma in3T: : {in T1 & T2 & T3, {all3 P3}} -> {all3 P3} SUCCESS! Proof Found in EFSM: [by move=> *;, auto ] Tactics applied: 833 Original Proof: [by move=> ? ?; auto.] Shorter Proof Found? no This is a novel proof proof search time: 0 min, 1 sec Results for lemma app_predE: x p (ap : manifest_applicative_pred p) : ap x = (x \in p) FAILURE! Tactics applied: 100000 Original Proof: [by case: ap => _ /= ->.] Proof search time: 1 min, 25 sec Results for lemma andbF: : right_zero false andb SUCCESS! Proof Found in EFSM: [by case ] Tactics applied: 2 Original Proof: [by case.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Results for lemma idPn: : reflect (~~ b1) (~~ b1) SUCCESS! Proof Found in EFSM: [by case b1;, constructor ] Tactics applied: 231 Original Proof: [by case b1; constructor.] Shorter Proof Found? no Proof reused from negPn proof search time: 0 min, 0 sec Results for lemma contraL: (c b : bool) : (c -> ~~ b) -> b -> ~~ c SUCCESS! Proof Found in EFSM: [by case b;, case c ] Tactics applied: 267 Original Proof: [by case: b => //; case: c.] Shorter Proof Found? no This is a novel proof This proof contained a loop around a state proof search time: 0 min, 0 sec Results for lemma on_can_inj: : {on D2, cancel f & g} -> {on D2 &, injective f} SUCCESS! Proof Found in EFSM: [by move=> fK x y /fK{2}<- /fK{2}<- -> ] Tactics applied: 49 Original Proof: [by move=> fK x y /fK{2}<- /fK{2}<- ->.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 1 sec Results for lemma rwP: : P <-> b SUCCESS! Proof Found in EFSM: [by case Pb ] Tactics applied: 5 Original Proof: [by split; [exact: introT | exact: elimT].] Shorter Proof Found? yes Single step proof reused proof search time: 0 min, 0 sec Results for lemma orbACA: : interchange orb orb SUCCESS! Proof Found in EFSM: [by do 3!case ] Tactics applied: 23 Original Proof: [by do 4!case.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Results for lemma orb_idr: (a b : bool) : (b -> a) -> a || b = a SUCCESS! Proof Found in EFSM: [by case a;, case b => // -> ] Tactics applied: 542 Original Proof: [by case: a; case: b => // ->.] Shorter Proof Found? no Proof reused from orb_idl This proof contained a loop around a state proof search time: 0 min, 1 sec Results for lemma subrelUr: r1 r2 : subrel r2 (relU r1 r2) SUCCESS! Proof Found in EFSM: [by move=> *;, apply /orP;, auto ] Tactics applied: 10682 Original Proof: [by move=> *; apply/orP; right.] Shorter Proof Found? no This is a novel proof This proof contained a loop around a state proof search time: 0 min, 8 sec Results for lemma orbb: : idempotent orb SUCCESS! Proof Found in EFSM: [by case ] Tactics applied: 2 Original Proof: [by case.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Results for lemma orbAC: : right_commutative orb SUCCESS! Proof Found in EFSM: [by do 3!case ] Tactics applied: 23 Original Proof: [by do 3!case.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Results for lemma on1T: : {on T2, allQ1 f} -> allQ1 f SUCCESS! Proof Found in EFSM: [by move=> ? ?;, auto ] Tactics applied: 971 Original Proof: [by move=> ? ?; auto.] Shorter Proof Found? no Proof reused from in1T proof search time: 0 min, 1 sec Results for lemma andb_orl: : left_distributive andb orb SUCCESS! Proof Found in EFSM: [by do 3!case ] Tactics applied: 23 Original Proof: [by do 3!case.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Results for lemma monoLR_in: : {in aD &, {mono f : x y / aR x y >-> rR x y}} -> {in aD & rD, forall x y, rR (f x) y = aR x (g y)} SUCCESS! Proof Found in EFSM: [by move=> mf x y hx hy /=;, rewrite -mf // !fgK_on ] Tactics applied: 1766 Original Proof: [by move=> mf x y hx hy; rewrite -{1}[y]fgK_on // mf.] Shorter Proof Found? no Proof reused from can_mono_in proof search time: 0 min, 2 sec Results for fold 2 Results for lemma implybE: a b : (a ==> b) = ~~ a || b SUCCESS! Proof Found in EFSM: [by case a] Tactics applied: 11 Original Proof: [by case: a; case: b.] Shorter Proof Found? yes Single step proof reused proof search time: 0 min, 0 sec Results for lemma topredE: x (pp : pT) : topred pp x = (x \in pp) SUCCESS! Proof Found in EFSM: [by rewrite -mem_topred ] Tactics applied: 65 Original Proof: [by rewrite -mem_topred.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Results for lemma implybNN: a b : (~~ a ==> ~~ b) = b ==> a SUCCESS! Proof Found in EFSM: [by case a;, case b ] Tactics applied: 507 Original Proof: [by case: a; case: b.] Shorter Proof Found? no Proof reused from addbN proof search time: 0 min, 1 sec Results for lemma homoLR: : {homo f : x y / aR x y >-> rR x y} -> forall x y, aR x (g y) -> rR (f x) y SUCCESS! Proof Found in EFSM: [by move=> Hf x y /Hf;, rewrite fgK ] Tactics applied: 1045 Original Proof: [by move=> Hf x y /Hf; rewrite fgK.] Shorter Proof Found? no Proof reused from homoRL proof search time: 0 min, 1 sec Results for lemma homoRL_in: : {in aD &, {homo f : x y / aR x y >-> rR x y}} -> {in rD & aD, forall x y, aR (g x) y -> rR x (f y)} SUCCESS! Proof Found in EFSM: [by move=> Hf x y hx hy /Hf;, rewrite fgK_on //;, apply ] Tactics applied: 7490 Original Proof: [by move=> Hf x y hx hy /Hf; rewrite fgK_on //; apply.] Shorter Proof Found? no Proof reused from homoLR_in proof search time: 0 min, 9 sec Results for lemma contraT: b : (~~ b -> false) -> b SUCCESS! Proof Found in EFSM: [by case b => // -> ] Tactics applied: 15 Original Proof: [by case: b => // ->.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Results for lemma orb_id2r: (a b c : bool) : (~~ b -> a = c) -> a || b = c || b SUCCESS! Proof Found in EFSM: [by case a;, case b;, case c => // -> ] Tactics applied: 4608 Original Proof: [by case: a; case: b; case: c => // ->.] Shorter Proof Found? no Proof reused from andb_id2l This proof contained a loop around a state proof search time: 0 min, 3 sec Results for lemma or3P: : reflect [\/ b1, b2 | b3] [|| b1, b2 | b3] FAILURE! Tactics applied: 100000 Original Proof: [case b1; first by constructor; constructor 1. case b2; first by constructor; constructor 2. case b3; first by constructor; constructor 3. by constructor; case.] Proof search time: 1 min, 51 sec Results for lemma mem_simpl: sp : mem sp = sp :> pred T SUCCESS! Proof Found in EFSM: [by [] ] Tactics applied: 1 Original Proof: [by [].] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Results for lemma iffP: : (P -> Q) -> (Q -> P) -> reflect Q b SUCCESS! Proof Found in EFSM: [by case def_b b / Pb;, constructor ;, auto ] Tactics applied: 3816 Original Proof: [by case: Pb; constructor; auto.] Shorter Proof Found? no This is a novel proof proof search time: 0 min, 3 sec Results for lemma negbT: b : b = false -> ~~ b SUCCESS! Proof Found in EFSM: [by case b ] Tactics applied: 6 Original Proof: [by case: b.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Results for lemma negbNE: b : ~~ ~~ b -> b SUCCESS! Proof Found in EFSM: [by case b ] Tactics applied: 6 Original Proof: [by case: b.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Results for lemma elimNTF: : ~~ b = c -> if c then ~ P else P SUCCESS! Proof Found in EFSM: [by case Hb;, case c ] Tactics applied: 176 Original Proof: [by move <-; case Hb.] Shorter Proof Found? no This is a novel proof proof search time: 0 min, 0 sec Results for lemma fun_if: : f (if b then vT else vF) = if b then f vT else f vF SUCCESS! Proof Found in EFSM: [by case b ] Tactics applied: 6 Original Proof: [by case b.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Results for lemma negb_imply: a b : ~~ (a ==> b) = a && ~~ b SUCCESS! Proof Found in EFSM: [by case a] Tactics applied: 11 Original Proof: [by case: a; case: b.] Shorter Proof Found? yes Single step proof reused proof search time: 0 min, 0 sec Results for lemma andbACA: : interchange andb andb SUCCESS! Proof Found in EFSM: [by do 3!case ] Tactics applied: 23 Original Proof: [by do 4!case.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Results for lemma monoRL_in: : {in aD &, {mono f : x y / aR x y >-> rR x y}} -> {in rD & aD, forall x y, rR x (f y) = aR (g x) y} SUCCESS! Proof Found in EFSM: [by move=> mf x y hx hy /=;, rewrite -mf // !fgK_on ] Tactics applied: 1886 Original Proof: [by move=> mf x y hx hy; rewrite -{1}[x]fgK_on // mf.] Shorter Proof Found? no Proof reused from can_mono_in proof search time: 0 min, 3 sec Results for lemma contraLR: (c b : bool) : (~~ c -> ~~ b) -> b -> c SUCCESS! Proof Found in EFSM: [by case b;, case c ] Tactics applied: 274 Original Proof: [by case: b => //; case: c.] Shorter Proof Found? no This is a novel proof proof search time: 0 min, 0 sec Results for lemma orbF: : right_id false orb SUCCESS! Proof Found in EFSM: [by case ] Tactics applied: 2 Original Proof: [by case.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Results for lemma qualifE: n T p x : (x \in @Qualifier n T p) = p x SUCCESS! Proof Found in EFSM: [by [] ] Tactics applied: 1 Original Proof: [by [].] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Results for lemma elimTn: : b' -> ~ P FAILURE! Tactics applied: 100000 Original Proof: [exact: elimTFn true _.] Proof search time: 2 min, 10 sec Results for lemma orbT: : forall b, b || true SUCCESS! Proof Found in EFSM: [by case ] Tactics applied: 2 Original Proof: [by case.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Results for lemma contraFF: (c b : bool) : (c -> b) -> b = false -> c = false SUCCESS! Proof Found in EFSM: [by case c;, case b => // -> ] Tactics applied: 320 Original Proof: [by move/contraFN=> bF_notc /bF_notc/negbTE.] Shorter Proof Found? no This is a novel proof proof search time: 0 min, 0 sec Results for lemma addbT: b : b (+) true = ~~ b SUCCESS! Proof Found in EFSM: [by case b ] Tactics applied: 6 Original Proof: [by case: b.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Results for fold 3 Results for lemma negb_inj: : injective negb SUCCESS! Proof Found in EFSM: [by do 2!case ] Tactics applied: 23 Original Proof: [exact: can_inj negbK.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Results for lemma classic_EM: : forall P, classically (decidable P) FAILURE! Tactics applied: 100000 Original Proof: [by move=> P [] // IH; apply IH; right => ?; apply: notF (IH _); left.] Proof search time: 1 min, 50 sec Results for lemma addbN: a b : a (+) ~~ b = ~~ (a (+) b) SUCCESS! Proof Found in EFSM: [by case a] Tactics applied: 12 Original Proof: [by case: a; case: b.] Shorter Proof Found? yes Single step proof reused proof search time: 0 min, 0 sec Results for lemma contraNF: (c b : bool) : (c -> b) -> ~~ b -> c = false SUCCESS! Proof Found in EFSM: [by case c;, case b => // -> ] Tactics applied: 267 Original Proof: [by move/contra=> notb_notc /notb_notc/negbTE.] Shorter Proof Found? no This is a novel proof This proof contained a loop around a state proof search time: 0 min, 0 sec Results for lemma rev_trans: T (R : rel T) : transitive R -> transitive (fun x y => R y x) SUCCESS! Proof Found in EFSM: [by move=> Hf x y hx hy /Hf;, auto ] Tactics applied: 1091 Original Proof: [by move=> trR x y z Ryx Rzy; exact: trR Rzy Ryx.] Shorter Proof Found? no This is a novel proof proof search time: 0 min, 1 sec Results for lemma negbRL: b c : ~~ b = c -> b = ~~ c SUCCESS! Proof Found in EFSM: [by case c;, case b ] Tactics applied: 266 Original Proof: [exact: canRL negbK.] Shorter Proof Found? no This is a novel proof This proof contained a loop around a state proof search time: 0 min, 0 sec Results for lemma orb_idl: (a b : bool) : (a -> b) -> a || b = b SUCCESS! Proof Found in EFSM: [by case a;, case b => // -> ] Tactics applied: 497 Original Proof: [by case: a; case: b => // ->.] Shorter Proof Found? no Proof reused from andb_idr This proof contained a loop around a state proof search time: 0 min, 1 sec Results for lemma orbC: : commutative orb SUCCESS! Proof Found in EFSM: [by do 2!case ] Tactics applied: 23 Original Proof: [by do 2!case.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Results for lemma negPn: : reflect b1 (~~ ~~ b1) SUCCESS! Proof Found in EFSM: [by case b1;, constructor ] Tactics applied: 203 Original Proof: [by case b1; constructor.] Shorter Proof Found? no Proof reused from negPf This proof contained a loop around a state proof search time: 0 min, 0 sec Results for lemma monoW_in: : {in aD &, {mono f : x y / aR x y >-> rR x y}} -> {in aD &, {homo f : x y / aR x y >-> rR x y}} SUCCESS! Proof Found in EFSM: [by move=> mf x y hx hy /=;, rewrite -mf // !fgK_on ] Tactics applied: 1771 Original Proof: [by move=> hf x y hx hy axy; rewrite hf.] Shorter Proof Found? no Proof reused from can_mono_in proof search time: 0 min, 3 sec Results for lemma orP: : reflect (b1 \/ b2) (b1 || b2) FAILURE! Tactics applied: 100000 Original Proof: [by case b1; case b2; constructor; auto; case.] Proof search time: 1 min, 51 sec Results for lemma homoRL: : {homo f : x y / aR x y >-> rR x y} -> forall x y, aR (g x) y -> rR x (f y) SUCCESS! Proof Found in EFSM: [by move=> Hf x y /Hf;, rewrite fgK ] Tactics applied: 1042 Original Proof: [by move=> Hf x y /Hf; rewrite fgK.] Shorter Proof Found? no Proof reused from homoLR proof search time: 0 min, 2 sec Results for lemma boolP: : alt_spec b1 b1 b1 SUCCESS! Proof Found in EFSM: [by case b1;, constructor ] Tactics applied: 203 Original Proof: [exact: (altP idP).] Shorter Proof Found? no Proof reused from negPf This proof contained a loop around a state proof search time: 0 min, 0 sec Results for lemma implyb_idl: (a b : bool) : (~~ a -> b) -> (a ==> b) = b SUCCESS! Proof Found in EFSM: [by case a;, case b => // -> ] Tactics applied: 497 Original Proof: [by case: a; case: b => // ->.] Shorter Proof Found? no Proof reused from andb_idr This proof contained a loop around a state proof search time: 0 min, 1 sec Results for lemma negb_or: (a b : bool) : ~~ (a || b) = ~~ a && ~~ b SUCCESS! Proof Found in EFSM: [by case a] Tactics applied: 12 Original Proof: [by case: a; case: b.] Shorter Proof Found? yes Single step proof reused proof search time: 0 min, 0 sec Results for lemma introP: : (b -> Q) -> (~~ b -> ~ Q) -> reflect Q b SUCCESS! Proof Found in EFSM: [by case def_b b / Pb;, constructor ;, auto ] Tactics applied: 3728 Original Proof: [by case b; constructor; auto.] Shorter Proof Found? no This is a novel proof This proof contained a loop around a state proof search time: 0 min, 3 sec Results for lemma if_arg: (fT fF : A -> B) : (if b then fT else fF) x = if b then fT x else fF x SUCCESS! Proof Found in EFSM: [by case b ] Tactics applied: 6 Original Proof: [by case b.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Results for lemma on1W: : allQ1 f -> {on D2, allQ1 f} SUCCESS! Proof Found in EFSM: [by move=> *] Tactics applied: 34 Original Proof: [by move=> ? ?.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 1 sec Results for lemma contraR: (c b : bool) : (~~ c -> b) -> ~~ b -> c SUCCESS! Proof Found in EFSM: [by case c;, case b ] Tactics applied: 266 Original Proof: [by case: b => //; case: c.] Shorter Proof Found? no This is a novel proof This proof contained a loop around a state proof search time: 0 min, 0 sec Results for lemma xorPifn: : Q \/ P -> ~ (Q /\ P) -> if b then Q else ~ Q FAILURE! Tactics applied: 100000 Original Proof: [rewrite -if_neg; exact: xorPif.] Proof search time: 2 min, 10 sec Results for lemma andbCA: : left_commutative andb SUCCESS! Proof Found in EFSM: [by do 2!case ] Tactics applied: 23 Original Proof: [by do 3!case.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Results for lemma addbC: : commutative addb SUCCESS! Proof Found in EFSM: [by do 2!case ] Tactics applied: 23 Original Proof: [by do 2!case.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Results for lemma andbA: : associative andb SUCCESS! Proof Found in EFSM: [by case ] Tactics applied: 2 Original Proof: [by do 3!case.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Results for lemma negP: : reflect (~ b1) (~~ b1) SUCCESS! Proof Found in EFSM: [by case b1;, constructor ] Tactics applied: 203 Original Proof: [by case b1; constructor; auto.] Shorter Proof Found? yes Proof reused from negPf This proof contained a loop around a state proof search time: 0 min, 0 sec Results for fold 4 Results for lemma in1T: : {in T1, {all1 P1}} -> {all1 P1} SUCCESS! Proof Found in EFSM: [by move=> *;, auto ] Tactics applied: 781 Original Proof: [by move=> ? ?; auto.] Shorter Proof Found? no This is a novel proof proof search time: 0 min, 1 sec Results for lemma mem_topred: (pp : pT) : mem (topred pp) = mem pp FAILURE! Tactics applied: 100000 Original Proof: [by rewrite /mem; case: pT pp => T1 app1 [mem1 /= ->].] Proof search time: 1 min, 28 sec Results for lemma elimNf: : ~~ b = false -> P SUCCESS! Proof Found in EFSM: [by case Pb ] Tactics applied: 5 Original Proof: [exact: elimNTF false _.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Results for lemma in_collective: x p (msp : manifest_simpl_pred p) : (x \in collective_pred_of_simpl msp) = p x SUCCESS! Proof Found in EFSM: [by case msp => _ /= -> ] Tactics applied: 19 Original Proof: [by case: msp => _ /= ->.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Results for lemma equivPifn: : (Q -> P) -> (P -> Q) -> if b then ~ Q else Q FAILURE! Tactics applied: 100000 Original Proof: [rewrite -if_neg; exact: equivPif.] Proof search time: 2 min, 4 sec Results for lemma on1lT: : {on T2, allQ1l f & h} -> allQ1l f h SUCCESS! Proof Found in EFSM: [by move=> ? ?;, auto ] Tactics applied: 965 Original Proof: [by move=> ? ?; auto.] Shorter Proof Found? no Proof reused from on2T proof search time: 0 min, 1 sec Results for lemma all_and3: (hP : forall x, [/\ P1 x, P2 x & P3 x]) : [/\ a P1, a P2 & a P3] SUCCESS! Proof Found in EFSM: [by split=> x;, case (hP x) ] Tactics applied: 2144 Original Proof: [by split=> x; case: (hP x).] Shorter Proof Found? no Proof reused from all_and5 proof search time: 0 min, 1 sec Results for lemma addbACA: : interchange addb addb SUCCESS! Proof Found in EFSM: [by do 4!case ] Tactics applied: 23 Original Proof: [by do 4!case.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Results for lemma altP: : alt_spec b FAILURE! Tactics applied: 100000 Original Proof: [by case def_b: b / Pb; constructor; rewrite ?def_b.] Proof search time: 1 min, 46 sec Results for lemma in2W: : {all2 P2} -> {in D1 & D2, {all2 P2}} SUCCESS! Proof Found in EFSM: [by move=> *] Tactics applied: 32 Original Proof: [by move=> ? ?.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Results for lemma introF: : ~ P -> b = false SUCCESS! Proof Found in EFSM: [by case Pb ] Tactics applied: 5 Original Proof: [exact: introTF false _.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Results for lemma if_neg: : (if ~~ b then vT else vF) = if b then vF else vT SUCCESS! Proof Found in EFSM: [by case b ] Tactics applied: 6 Original Proof: [by case b.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Results for lemma sub_refl: T (p : mem_pred T) : sub_mem p p SUCCESS! Proof Found in EFSM: [by [] ] Tactics applied: 1 Original Proof: [by [].] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Results for lemma implyFb: b : false ==> b SUCCESS! Proof Found in EFSM: [by [] ] Tactics applied: 1 Original Proof: [by [].] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Results for lemma all_and4: (hP : forall x, [/\ P1 x, P2 x, P3 x & P4 x]) : [/\ a P1, a P2, a P3 & a P4] SUCCESS! Proof Found in EFSM: [by split=> x;, case (hP x) ] Tactics applied: 2144 Original Proof: [by split=> x; case: (hP x).] Shorter Proof Found? no Proof reused from all_and5 proof search time: 0 min, 1 sec Results for lemma rwP2: : reflect Q b -> (P <-> Q) FAILURE! Tactics applied: 100000 Original Proof: [by move=> Qb; split=> ?; [exact: appP | apply: elimT; case: Qb].] Proof search time: 2 min, 10 sec Results for lemma homo_mono_in: : {in aD &, {homo f : x y / aR x y >-> rR x y}} -> {in rD &, {homo g : x y / rR x y >-> aR x y}} -> {in rD &, {mono g : x y / rR x y >-> aR x y}} FAILURE! Tactics applied: 100000 Original Proof: [move=> mf mg x y hx hy; case: (boolP (rR _ _))=> [/mg //|]; first exact. by apply: contraNF=> /mf; rewrite !fgK_on //; apply.] Proof search time: 1 min, 53 sec Results for lemma negb_and: (a b : bool) : ~~ (a && b) = ~~ a || ~~ b SUCCESS! Proof Found in EFSM: [by case a] Tactics applied: 11 Original Proof: [by case: a; case: b.] Shorter Proof Found? yes Single step proof reused proof search time: 0 min, 0 sec Results for lemma sumboolP: (decQ : decidable Q) : reflect Q decQ FAILURE! Tactics applied: 100000 Original Proof: [by case: decQ; constructor.] Proof search time: 1 min, 51 sec Results for lemma andP: : reflect (b1 /\ b2) (b1 && b2) FAILURE! Tactics applied: 100000 Original Proof: [by case b1; case b2; constructor=> //; case.] Proof search time: 1 min, 27 sec Results for lemma contraFN: (c b : bool) : (c -> b) -> b = false -> ~~ c FAILURE! Tactics applied: 100000 Original Proof: [by move/contra=> notb_notc /negbT.] Proof search time: 1 min, 55 sec Results for lemma sym_left_transitive: : left_transitive FAILURE! Tactics applied: 100000 Original Proof: [by move=> x y Rxy z; apply/idP/idP; apply: trR; rewrite // symR.] Proof search time: 1 min, 33 sec Results for lemma ifT: : b -> (if b then vT else vF) = vT SUCCESS! Proof Found in EFSM: [by case b ] Tactics applied: 6 Original Proof: [by move->.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Results for lemma classic_imply: : forall P Q, (P -> classically Q) -> classically (P -> Q) FAILURE! Tactics applied: 100000 Original Proof: [move=> P Q IH [] // notPQ; apply notPQ; move/IH=> hQ; case: notF. by apply: hQ => hQ; case: notF; exact: notPQ.] Proof search time: 1 min, 34 sec Results for fold 5 Results for lemma simpl_predE: p : SimplPred p =1 p SUCCESS! Proof Found in EFSM: [split => ?] Tactics applied: 1 Original Proof: [by [].] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Results for lemma is_true_locked_true: : locked true FAILURE! Tactics applied: 100000 Original Proof: [by unlock.] Proof search time: 1 min, 8 sec Results for lemma orbCA: : left_commutative orb SUCCESS! Proof Found in EFSM: [by do 2!case ] Tactics applied: 81 Original Proof: [by do 3!case.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Results for lemma appP: : reflect Q b -> P -> Q FAILURE! Tactics applied: 100000 Original Proof: [by move=> Qb; move/introT; case: Qb.] Proof search time: 1 min, 7 sec Results for lemma in3W: : {all3 P3} -> {in D1 & D2 & D3, {all3 P3}} SUCCESS! Proof Found in EFSM: [by move=> *] Tactics applied: 93 Original Proof: [by move=> ? ?.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 1 sec Results for lemma can_mono_in: : {in aD &, {mono f : x y / aR x y >-> rR x y}} -> {in rD &, {mono g : x y / rR x y >-> aR x y}} FAILURE! Tactics applied: 100000 Original Proof: [by move=> mf x y hx hy /=; rewrite -mf // !fgK_on.] Proof search time: 1 min, 31 sec Results for lemma addTb: b : true (+) b = ~~ b SUCCESS! Proof Found in EFSM: [split => ?] Tactics applied: 1 Original Proof: [by [].] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Results for lemma on1lW: : allQ1l f h -> {on D2, allQ1l f & h} SUCCESS! Proof Found in EFSM: [move => T P [] // IH] Tactics applied: 47 Original Proof: [by move=> ? ?.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 1 sec Results for lemma addbF: : right_id false addb SUCCESS! Proof Found in EFSM: [by case ] Tactics applied: 61 Original Proof: [by case.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Results for lemma subrelUl: r1 r2 : subrel r1 (relU r1 r2) SUCCESS! Proof Found in EFSM: [by move=> /= sub sub3;, by move-> ] Tactics applied: 6813 Original Proof: [by move=> *; apply/orP; left.] Shorter Proof Found? yes This is a novel proof This proof contained a loop around a state proof search time: 0 min, 4 sec Results for lemma orKb: a b : a && (b || a) = a SUCCESS! Proof Found in EFSM: [by case b;, by case a] Tactics applied: 4302 Original Proof: [by case: a; case: b.] Shorter Proof Found? no This is a novel proof This proof contained a loop around a state proof search time: 0 min, 2 sec Results for lemma andbK: a b : a && b || a = a SUCCESS! Proof Found in EFSM: [by case b;, by case a] Tactics applied: 4458 Original Proof: [by case: a; case: b.] Shorter Proof Found? no This is a novel proof This proof contained a loop around a state proof search time: 0 min, 2 sec Results for lemma subon2: (Phf : ph (allQ2 f)) (Ph : ph (allQ2 f)) : prop_on2 d2' Phf Ph -> prop_on2 d2 Phf Ph SUCCESS! Proof Found in EFSM: [move => P Q IH [] // notPQ;, auto ] Tactics applied: 2360 Original Proof: [by move=> allQ x y /sub2=> d2fx /sub2; exact: allQ.] Shorter Proof Found? no This is a novel proof proof search time: 0 min, 4 sec Results for lemma negPf: : reflect (b1 = false) (~~ b1) SUCCESS! Proof Found in EFSM: [by case b1;, constructor ] Tactics applied: 3978 Original Proof: [by case b1; constructor.] Shorter Proof Found? no Proof reused from idP This proof contained a loop around a state proof search time: 0 min, 2 sec Results for lemma implybN: a b : (a ==> ~~ b) = (b ==> ~~ a) SUCCESS! Proof Found in EFSM: [by case b;, by case a] Tactics applied: 4302 Original Proof: [by case: a; case: b.] Shorter Proof Found? no This is a novel proof This proof contained a loop around a state proof search time: 0 min, 2 sec Results for lemma orFb: : left_id false orb SUCCESS! Proof Found in EFSM: [split => ?] Tactics applied: 1 Original Proof: [by [].] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Results for lemma inT_bij: : {in T1, bijective f} -> bijective f FAILURE! Tactics applied: 100000 Original Proof: [by case=> g' fK g'K; exists g' => * ? *; auto.] Proof search time: 2 min, 37 sec Results for lemma in_applicative: x p (amp : applicative_mem_pred p) : in_mem x amp = p x FAILURE! Tactics applied: 100000 Original Proof: [by case: amp => [[_ /= ->]].] Proof search time: 1 min, 17 sec Results for lemma implyNb: a b : (~~ a ==> b) = a || b SUCCESS! Proof Found in EFSM: [by case a] Tactics applied: 70 Original Proof: [by case: a; case: b.] Shorter Proof Found? yes Single step proof reused proof search time: 0 min, 0 sec Results for lemma or4P: : reflect [\/ b1, b2, b3 | b4] [|| b1, b2, b3 | b4] FAILURE! Tactics applied: 100000 Original Proof: [case b1; first by constructor; constructor 1. case b2; first by constructor; constructor 2. case b3; first by constructor; constructor 3. case b4; first by constructor; constructor 4. by constructor; case.] Proof search time: 1 min, 28 sec Results for lemma negbLR: b c : b = ~~ c -> ~~ b = c SUCCESS! Proof Found in EFSM: [by case b;, by case c] Tactics applied: 4298 Original Proof: [exact: canLR negbK.] Shorter Proof Found? no This is a novel proof This proof contained a loop around a state proof search time: 0 min, 2 sec Results for lemma on2W: : allQ2 f -> {on D2 &, allQ2 f} SUCCESS! Proof Found in EFSM: [move => P Q IH [] // notPQ] Tactics applied: 45 Original Proof: [by move=> ? ?.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 1 sec Results for lemma andNb: b : ~~ b && b = false SUCCESS! Proof Found in EFSM: [by case b ] Tactics applied: 64 Original Proof: [by case: b.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Results for lemma equivPif: : (Q -> P) -> (P -> Q) -> if b then Q else ~ Q FAILURE! Tactics applied: 100000 Original Proof: [by case Hb; auto.] Proof search time: 1 min, 11 sec Results for fold 6 Results for lemma andbb: : idempotent andb SUCCESS! Proof Found in EFSM: [try by case ] Tactics applied: 32 Original Proof: [by case.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Results for lemma and5P: : reflect [/\ b1, b2, b3, b4 & b5] [&& b1, b2, b3, b4 & b5] FAILURE! Tactics applied: 100000 Original Proof: [by case b1; case b2; case b3; case b4; case b5; constructor; try by case.] Proof search time: 1 min, 8 sec Results for lemma andb_addl: : left_distributive andb addb SUCCESS! Proof Found in EFSM: [by do 3!case ] Tactics applied: 122 Original Proof: [by do 3!case.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Results for lemma orbK: a b : (a || b) && a = a SUCCESS! Proof Found in EFSM: [case b;, by case a] Tactics applied: 5235 Original Proof: [by case: a; case: b.] Shorter Proof Found? no This is a novel proof This proof contained a loop around a state proof search time: 0 min, 4 sec Results for lemma introNf: : P -> ~~ b = false SUCCESS! Proof Found in EFSM: [by case def_b b / Pb] Tactics applied: 107 Original Proof: [exact: introNTF false _.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Results for lemma introTF: : (if c then P else ~ P) -> b = c SUCCESS! Proof Found in EFSM: [by case Hb;, case c ] Tactics applied: 7212 Original Proof: [by case c; case Hb.] Shorter Proof Found? no This is a novel proof This proof contained a loop around a state proof search time: 0 min, 5 sec Results for lemma andb_idr: (a b : bool) : (a -> b) -> a && b = a SUCCESS! Proof Found in EFSM: [by case a;, first exact ] Tactics applied: 8531 Original Proof: [by case: a; case: b => // ->.] Shorter Proof Found? no This is a novel proof proof search time: 0 min, 6 sec Results for lemma sameP: : reflect P c -> b = c SUCCESS! Proof Found in EFSM: [by case def_b b / Pb;, try by case ] Tactics applied: 7877 Original Proof: [case; [exact: introT | exact: introF].] Shorter Proof Found? no This is a novel proof proof search time: 0 min, 5 sec Results for lemma idP: : reflect b1 b1 SUCCESS! Proof Found in EFSM: [case b1;, constructor => //] Tactics applied: 5129 Original Proof: [by case b1; constructor.] Shorter Proof Found? no This is a novel proof This proof contained a loop around a state proof search time: 0 min, 3 sec Results for lemma if_same: : (if b then vT else vT) = vT SUCCESS! Proof Found in EFSM: [case b => // -> ] Tactics applied: 86 Original Proof: [by case b.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Results for lemma introT: : P -> b SUCCESS! Proof Found in EFSM: [by case def_b b / Pb] Tactics applied: 106 Original Proof: [exact: introTF true _.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Results for lemma andb_id2l: (a b c : bool) : (a -> b = c) -> a && b = a && c SUCCESS! Proof Found in EFSM: [by case a;, first exact ] Tactics applied: 9041 Original Proof: [by case: a; case: b; case: c => // ->.] Shorter Proof Found? yes This is a novel proof proof search time: 0 min, 7 sec Results for lemma addbP: a b : reflect (~~ a = b) (a (+) b) FAILURE! Tactics applied: 100000 Original Proof: [by case: a; case: b; constructor.] Proof search time: 1 min, 11 sec Results for lemma orb_id2l: (a b c : bool) : (~~ a -> b = c) -> a || b = a || c SUCCESS! Proof Found in EFSM: [by case a;, exact ] Tactics applied: 9066 Original Proof: [by case: a; case: b; case: c => // ->.] Shorter Proof Found? yes This is a novel proof proof search time: 0 min, 7 sec Results for lemma sub_in12: T1 T d1 d1' d d' (P : T1 -> T -> T -> Prop) : sub_mem d1 d1' -> sub_mem d d' -> forall Ph : ph {all3 P}, prop_in12 d1' d' Ph -> prop_in12 d1 d Ph SUCCESS! Proof Found in EFSM: [move => mf mg x y hx hy;, auto ] Tactics applied: 2639 Original Proof: [by move=> /= sub1 sub; exact: sub_in111.] Shorter Proof Found? no This is a novel proof proof search time: 0 min, 3 sec Results for lemma addFb: : left_id false addb SUCCESS! Proof Found in EFSM: [split => ?] Tactics applied: 1 Original Proof: [by [].] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Results for lemma in_simpl: x p (msp : manifest_simpl_pred p) : in_mem x (Mem [eta fun_of_simpl (msp : simpl_pred T)]) = p x SUCCESS! Proof Found in EFSM: [by case msp => _ /= -> ] Tactics applied: 119 Original Proof: [by case: msp => _ /= ->.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Results for lemma decPcases: : if b then P else ~ P SUCCESS! Proof Found in EFSM: [by case def_b b / Pb] Tactics applied: 107 Original Proof: [by case Pb.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Results for lemma contra: (c b : bool) : (c -> b) -> ~~ b -> ~~ c SUCCESS! Proof Found in EFSM: [case b;, case c => // -> ] Tactics applied: 5383 Original Proof: [by case: b => //; case: c.] Shorter Proof Found? no This is a novel proof This proof contained a loop around a state proof search time: 0 min, 3 sec Results for lemma mem_mem: (pp : pT) : (mem (mem pp) = mem pp) * (mem [mem pp] = mem pp) SUCCESS! Proof Found in EFSM: [by rewrite -mem_topred ] Tactics applied: 164 Original Proof: [by rewrite -mem_topred.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Results for lemma and4P: : reflect [/\ b1, b2, b3 & b4] [&& b1, b2, b3 & b4] FAILURE! Tactics applied: 100000 Original Proof: [by case b1; case b2; case b3; case b4; constructor; try by case.] Proof search time: 1 min, 12 sec Results for lemma addbA: : associative addb SUCCESS! Proof Found in EFSM: [by do 3!case ] Tactics applied: 122 Original Proof: [by do 3!case.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Results for lemma andb_addr: : right_distributive andb addb SUCCESS! Proof Found in EFSM: [try by case ] Tactics applied: 32 Original Proof: [by do 3!case.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Results for lemma bind_unless: C P {Q} : unless C P -> unless (unless C Q) P FAILURE! Tactics applied: 100000 Original Proof: [by move=> haveP suffPQ suffQ; apply: haveP => /suffPQ; exact.] Proof search time: 1 min, 11 sec Results for fold 7 Results for lemma elimN: : ~~ b -> ~P SUCCESS! Proof Found in EFSM: [by case Pb ] Tactics applied: 5 Original Proof: [exact: elimNTF true _.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Results for lemma sym_right_transitive: : right_transitive FAILURE! Tactics applied: 100000 Original Proof: [by move=> x y /sym_left_transitive Rxy z; rewrite !(symR z) Rxy.] Proof search time: 1 min, 45 sec Results for lemma onW_bij: : bijective f -> {on D2, bijective f} SUCCESS! Proof Found in EFSM: [by case=> g' fK g'K;, exists g' => * ? *] Tactics applied: 710 Original Proof: [by case=> g' fK g'K; exists g' => * ? *; auto.] Shorter Proof Found? yes Proof reused from inW_bij This proof contained a loop around a state proof search time: 0 min, 1 sec Results for lemma orTb: : forall b, true || b SUCCESS! Proof Found in EFSM: [by [] ] Tactics applied: 1 Original Proof: [by [].] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Results for lemma implyTb: b : (true ==> b) = b SUCCESS! Proof Found in EFSM: [by [] ] Tactics applied: 1 Original Proof: [by [].] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Results for lemma canRL_on: x y : {on D2, cancel f & g} -> f x \in D2 -> f x = y -> x = g y SUCCESS! Proof Found in EFSM: [by move=> fK D1x <-;, rewrite fK ] Tactics applied: 1447 Original Proof: [by move=> fK D2fx <-; rewrite fK.] Shorter Proof Found? no Proof reused from canRL_in proof search time: 0 min, 2 sec Results for lemma addbAC: : right_commutative addb SUCCESS! Proof Found in EFSM: [by do 3!case ] Tactics applied: 23 Original Proof: [by do 3!case.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Results for lemma addbI: : right_injective addb SUCCESS! Proof Found in EFSM: [by do 3!case ] Tactics applied: 23 Original Proof: [by do 3!case.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Results for lemma implyb_id2l: (a b c : bool) : (a -> b = c) -> (a ==> b) = (a ==> c) SUCCESS! Proof Found in EFSM: [by case a;, exact ] Tactics applied: 549 Original Proof: [by case: a; case: b; case: c => // ->.] Shorter Proof Found? yes This is a novel proof proof search time: 0 min, 1 sec Results for lemma unless_contra: b C : (~~ b -> C) -> unless C b FAILURE! Tactics applied: 100000 Original Proof: [by case: b => [_ haveC | haveC _]; exact: haveC.] Proof search time: 1 min, 57 sec Results for lemma addKb: : left_loop id addb SUCCESS! Proof Found in EFSM: [by do 2!case ] Tactics applied: 22 Original Proof: [by do 2!case.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Results for lemma equivalence_relP_in: T (R : rel T) (A : pred T) : {in A & &, equivalence_rel R} <-> {in A, reflexive R} /\ {in A &, forall x y, R x y -> {in A, R x =1 R y}} FAILURE! Tactics applied: 100000 Original Proof: [split=> [eqiR | [Rxx trR] x y z *]; last by split=> [|/trR-> //]; exact: Rxx. by split=> [x Ax|x y Ax Ay Rxy z Az]; [rewrite (eqiR x x) | rewrite (eqiR x y)].] Proof search time: 2 min, 11 sec Results for lemma elimT: : b -> P SUCCESS! Proof Found in EFSM: [by case Pb ] Tactics applied: 5 Original Proof: [exact: elimTF true _.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Results for lemma andb_id2r: (a b c : bool) : (b -> a = c) -> a && b = c && b SUCCESS! Proof Found in EFSM: [by case a;, case b;, case c => // -> ] Tactics applied: 6091 Original Proof: [by case: a; case: b; case: c => // ->.] Shorter Proof Found? no Proof reused from orb_id2r This proof contained a loop around a state proof search time: 0 min, 5 sec Results for lemma wlog_neg: b : (~~ b -> b) -> b SUCCESS! Proof Found in EFSM: [by case b => // -> ] Tactics applied: 16 Original Proof: [by case: b => // ->.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Results for lemma sub_in1: (Ph : ph {all1 P1}) : prop_in1 d1' Ph -> prop_in1 d1 Ph SUCCESS! Proof Found in EFSM: [by move=> ? ?;, auto ] Tactics applied: 1048 Original Proof: [move=> allP x /sub1; exact: allP.] Shorter Proof Found? no Proof reused from on2T proof search time: 0 min, 1 sec Results for lemma classicP: : forall P : Prop, classically P <-> ~ ~ P FAILURE! Tactics applied: 100000 Original Proof: [move=> P; split=> [cP nP | nnP [] // nP]; last by case nnP; move/nP. by have: P -> false; [move/nP | move/cP].] Proof search time: 1 min, 47 sec Results for lemma orbN: b : b || ~~ b = true SUCCESS! Proof Found in EFSM: [by case b ] Tactics applied: 6 Original Proof: [by case: b.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Results for lemma sub_in_bij: (D1' : pred T1) : {subset D1 <= D1'} -> {in D1', bijective f} -> {in D1, bijective f} SUCCESS! Proof Found in EFSM: [by move=> subD [g' fK g'K];, exists g' => * ? *;, auto ] Tactics applied: 18673 Original Proof: [by move=> subD [g' fK g'K]; exists g' => x; move/subD; [exact: fK | exact: g'K].] Shorter Proof Found? yes This is a novel proof This proof contained a loop around a state proof search time: 0 min, 20 sec Results for lemma canLR_in: x y : {in D1, cancel f g} -> y \in D1 -> x = f y -> g x = y SUCCESS! Proof Found in EFSM: [by move=> fK D2fy ->;, rewrite fK ] Tactics applied: 1495 Original Proof: [by move=> fK D1y ->; rewrite fK.] Shorter Proof Found? no Proof reused from canLR_on proof search time: 0 min, 2 sec Results for lemma orb_andr: : right_distributive orb andb SUCCESS! Proof Found in EFSM: [by case ] Tactics applied: 2 Original Proof: [by do 3!case.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Results for lemma elimF: : b = false -> ~ P SUCCESS! Proof Found in EFSM: [by case Pb ] Tactics applied: 5 Original Proof: [exact: elimTF false _.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Results for lemma elimTF: : b = c -> if c then P else ~ P SUCCESS! Proof Found in EFSM: [by case Hb;, case c ] Tactics applied: 171 Original Proof: [by move <-; case Hb.] Shorter Proof Found? no This is a novel proof This proof contained a loop around a state proof search time: 0 min, 0 sec Results for lemma onT_bij: : {on T2, bijective f} -> bijective f SUCCESS! Proof Found in EFSM: [by case=> g' fK g'K;, exists g' => * ? *;, auto ] Tactics applied: 7578 Original Proof: [by case=> g' fK g'K; exists g' => * ? *; auto.] Shorter Proof Found? no Proof reused from inW_bij This proof contained a loop around a state proof search time: 0 min, 8 sec Results for fold 8 Results for lemma subon1l: (Phf : ph (allQ1l f)) (Ph : ph (allQ1l f h)) : prop_on1 d2' Phf Ph -> prop_on1 d2 Phf Ph SUCCESS! Proof Found in EFSM: [by move=> ? ?;, auto ] Tactics applied: 1270 Original Proof: [by move=> allQ x /sub2; exact: allQ.] Shorter Proof Found? no Proof reused from in2T proof search time: 0 min, 2 sec Results for lemma negbFE: b : ~~ b = false -> b SUCCESS! Proof Found in EFSM: [by case b ] Tactics applied: 6 Original Proof: [by case: b.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Results for lemma ifN: : ~~ b -> (if b then vT else vF) = vF SUCCESS! Proof Found in EFSM: [by case b ] Tactics applied: 6 Original Proof: [by move/negbTE->.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Results for lemma sub_in111: (Ph : ph {all3 P3}) : prop_in111 d1' d2' d3' Ph -> prop_in111 d1 d2 d3 Ph SUCCESS! Proof Found in EFSM: [by move=> ? ?;, auto ] Tactics applied: 1270 Original Proof: [by move=> allP x1 x2 x3 /sub1 d1x1 /sub2 d2x2 /sub3; exact: allP.] Shorter Proof Found? no Proof reused from in2T proof search time: 0 min, 2 sec Results for lemma negbF: b : (b : bool) -> ~~ b = false SUCCESS! Proof Found in EFSM: [by case b ] Tactics applied: 6 Original Proof: [by case: b.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Results for lemma sub_in11: (Ph : ph {all2 P2}) : prop_in11 d1' d2' Ph -> prop_in11 d1 d2 Ph SUCCESS! Proof Found in EFSM: [by move=> ? ?;, auto ] Tactics applied: 1270 Original Proof: [move=> allP x1 x2 /sub1 d1x1 /sub2; exact: allP.] Shorter Proof Found? no Proof reused from in2T proof search time: 0 min, 2 sec Results for lemma introN: : ~ P -> ~~ b SUCCESS! Proof Found in EFSM: [by case Pb ] Tactics applied: 5 Original Proof: [exact: introNTF true _.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Results for lemma can_in_inj: : {in D1, cancel f g} -> {in D1 &, injective f} SUCCESS! Proof Found in EFSM: [by move=> fK x y /fK{2}<- /fK{2}<- -> ] Tactics applied: 49 Original Proof: [by move=> fK x y /fK{2}<- /fK{2}<- ->.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 1 sec Results for lemma implyP: : reflect (b1 -> b2) (b1 ==> b2) FAILURE! Tactics applied: 100000 Original Proof: [by case b1; case b2; constructor; auto.] Proof search time: 1 min, 25 sec Results for lemma nandP: : reflect (~~ b1 \/ ~~ b2) (~~ (b1 && b2)) FAILURE! Tactics applied: 100000 Original Proof: [by case b1; case b2; constructor; auto; case; auto.] Proof search time: 1 min, 25 sec Results for lemma orb_andl: : left_distributive orb andb SUCCESS! Proof Found in EFSM: [by do 3!case ] Tactics applied: 24 Original Proof: [by do 3!case.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Results for lemma monoW: : {mono f : x / aP x >-> rP x} -> {homo f : x / aP x >-> rP x} FAILURE! Tactics applied: 100000 Original Proof: [by move=> hf x ax; rewrite hf.] Proof search time: 1 min, 34 sec Results for lemma andb_orr: : right_distributive andb orb SUCCESS! Proof Found in EFSM: [by case ] Tactics applied: 2 Original Proof: [by do 3!case.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Results for lemma unfold_in: x p : (x \in ([eta p] : pred T)) = p x SUCCESS! Proof Found in EFSM: [by [] ] Tactics applied: 1 Original Proof: [by [].] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Results for lemma is_true_true: : true SUCCESS! Proof Found in EFSM: [by [] ] Tactics applied: 1 Original Proof: [by [].] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Results for lemma introTFn: : (if c then ~ P else P) -> b = c FAILURE! Tactics applied: 100000 Original Proof: [by move/(introNTF Hb) <-; case b.] Proof search time: 1 min, 46 sec Results for lemma andTb: : left_id true andb SUCCESS! Proof Found in EFSM: [by [] ] Tactics applied: 1 Original Proof: [by [].] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Results for lemma in1W: : {all1 P1} -> {in D1, {all1 P1}} SUCCESS! Proof Found in EFSM: [by move=> *] Tactics applied: 33 Original Proof: [by move=> ? ?.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 1 sec Results for lemma and3P: : reflect [/\ b1, b2 & b3] [&& b1, b2 & b3] FAILURE! Tactics applied: 100000 Original Proof: [by case b1; case b2; case b3; constructor; try by case.] Proof search time: 1 min, 23 sec Results for lemma implybF: b : (b ==> false) = ~~ b SUCCESS! Proof Found in EFSM: [by [] ] Tactics applied: 1 Original Proof: [by case: b.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Results for lemma prop_congr: : forall b b' : bool, b = b' -> b = b' :> Prop SUCCESS! Proof Found in EFSM: [by do 2!case ] Tactics applied: 23 Original Proof: [by move=> b b' ->.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Results for lemma on2T: : {on T2 &, allQ2 f} -> allQ2 f SUCCESS! Proof Found in EFSM: [by move=> ? ?;, auto ] Tactics applied: 1270 Original Proof: [by move=> ? ?; auto.] Shorter Proof Found? no Proof reused from in2T proof search time: 0 min, 1 sec Results for lemma classic_pick: : forall T P, classically ({x : T | P x} + (forall x, ~ P x)) FAILURE! Tactics applied: 100000 Original Proof: [move=> T P [] // IH; apply IH; right=> x Px; case: notF. by apply: IH; left; exists x.] Proof search time: 1 min, 22 sec Results for lemma ifF: : b = false -> (if b then vT else vF) = vF SUCCESS! Proof Found in EFSM: [by case b ] Tactics applied: 6 Original Proof: [by move->.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Results for fold 9 Results for lemma ifP: : if_spec (b = false) b (if b then vT else vF) SUCCESS! Proof Found in EFSM: [by case def_b b;, constructor ] Tactics applied: 379 Original Proof: [by case def_b: b; constructor.] Shorter Proof Found? no Proof reused from ifPn proof search time: 0 min, 0 sec Results for lemma all_and5: (hP : forall x, [/\ P1 x, P2 x, P3 x, P4 x & P5 x]) : [/\ a P1, a P2, a P3, a P4 & a P5] SUCCESS! Proof Found in EFSM: [by split=> x;, case (hP x) ] Tactics applied: 2190 Original Proof: [by split=> x; case: (hP x).] Shorter Proof Found? no Proof reused from all_and2 proof search time: 0 min, 1 sec Results for lemma contraFT: (c b : bool) : (~~ c -> b) -> b = false -> c SUCCESS! Proof Found in EFSM: [by case c;, case b => // -> ] Tactics applied: 307 Original Proof: [by move/contraR=> notb_c /negbT.] Shorter Proof Found? no This is a novel proof proof search time: 0 min, 0 sec Results for lemma negbK: : involutive negb SUCCESS! Proof Found in EFSM: [by case ] Tactics applied: 2 Original Proof: [by case.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Results for lemma subon_bij: (D2' : pred T2) : {subset D2 <= D2'} -> {on D2', bijective f} -> {on D2, bijective f} SUCCESS! Proof Found in EFSM: [by move=> subD [g' fK g'K];, exists g' => * ? *;, auto ] Tactics applied: 10011 Original Proof: [by move=> subD [g' fK g'K]; exists g' => x; move/subD; [exact: fK | exact: g'K].] Shorter Proof Found? yes This is a novel proof This proof contained a loop around a state proof search time: 0 min, 12 sec Results for lemma implybb: b : b ==> b SUCCESS! Proof Found in EFSM: [by case b ] Tactics applied: 6 Original Proof: [by case: b.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Results for lemma ifE: : (if b then vT else vF) = if_expr SUCCESS! Proof Found in EFSM: [by [] ] Tactics applied: 1 Original Proof: [by [].] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Results for lemma subon1: (Phf : ph (allQ1 f)) (Ph : ph (allQ1 f)) : prop_on1 d2' Phf Ph -> prop_on1 d2 Phf Ph SUCCESS! Proof Found in EFSM: [by move=> ? ?;, auto ] Tactics applied: 992 Original Proof: [by move=> allQ x /sub2; exact: allQ.] Shorter Proof Found? no Proof reused from in3T proof search time: 0 min, 1 sec Results for lemma negbTE: b : ~~ b -> b = false SUCCESS! Proof Found in EFSM: [by case b ] Tactics applied: 6 Original Proof: [by case: b.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Results for lemma in2T: : {in T1 & T2, {all2 P2}} -> {all2 P2} SUCCESS! Proof Found in EFSM: [by move=> *;, auto ] Tactics applied: 808 Original Proof: [by move=> ? ?; auto.] Shorter Proof Found? no This is a novel proof proof search time: 0 min, 1 sec Results for lemma elimFn: : b' = false -> P FAILURE! Tactics applied: 100000 Original Proof: [exact: elimTFn false _.] Proof search time: 2 min, 27 sec Results for lemma equivP: : (P <-> Q) -> reflect Q b FAILURE! Tactics applied: 100000 Original Proof: [by case; exact: iffP.] Proof search time: 2 min, 32 sec Results for lemma implybT: b : b ==> true SUCCESS! Proof Found in EFSM: [by case b ] Tactics applied: 6 Original Proof: [by case: b.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Results for lemma introFn: : P -> b' = false FAILURE! Tactics applied: 100000 Original Proof: [exact: introTFn false _.] Proof search time: 2 min, 25 sec Results for lemma andbC: : commutative andb SUCCESS! Proof Found in EFSM: [by do 2!case ] Tactics applied: 22 Original Proof: [by do 2!case.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Results for lemma symmetric_from_pre: : pre_symmetric -> symmetric FAILURE! Tactics applied: 100000 Original Proof: [move=> symR x y; apply/idP/idP; exact: symR.] Proof search time: 2 min, 20 sec Results for lemma mono2W: : {mono f : x y / aR x y >-> rR x y} -> {homo f : x y / aR x y >-> rR x y} SUCCESS! Proof Found in EFSM: [by move=> hf x ax;, rewrite hf ] Tactics applied: 1620 Original Proof: [by move=> hf x y axy; rewrite hf.] Shorter Proof Found? no Proof reused from monoW proof search time: 0 min, 2 sec Results for lemma contraTF: (c b : bool) : (c -> ~~ b) -> b -> c = false FAILURE! Tactics applied: 100000 Original Proof: [by move/contraL=> b_notc /b_notc/negbTE.] Proof search time: 2 min, 24 sec Results for lemma andbN: b : b && ~~ b = false SUCCESS! Proof Found in EFSM: [by case b ] Tactics applied: 6 Original Proof: [by case: b.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Results for lemma equivalence_relP: : equivalence_rel <-> reflexive /\ left_transitive FAILURE! Tactics applied: 100000 Original Proof: [split=> [eqiR | [Rxx trR] x y z]; last by split=> [|/trR->]. by split=> [x | x y Rxy z]; [rewrite (eqiR x x x) | rewrite (eqiR x y z)].] Proof search time: 2 min, 16 sec Results for lemma addbK: : right_loop id addb SUCCESS! Proof Found in EFSM: [by do 2!case ] Tactics applied: 22 Original Proof: [by do 2!case.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Results for lemma introNTF: : (if c then ~ P else P) -> ~~ b = c SUCCESS! Proof Found in EFSM: [by case Hb;, case c ] Tactics applied: 167 Original Proof: [by case c; case Hb.] Shorter Proof Found? no This is a novel proof proof search time: 0 min, 0 sec Results for lemma keyed_predE: : k_p =i p FAILURE! Tactics applied: 100000 Original Proof: [by case: k_p.] Proof search time: 2 min, 8 sec Results for lemma mono2W_in: : {in aD, {mono f : x / aP x >-> rP x}} -> {in aD, {homo f : x / aP x >-> rP x}} SUCCESS! Proof Found in EFSM: [by move=> hf x ax;, rewrite hf ] Tactics applied: 1620 Original Proof: [by move=> hf x hx ax; rewrite hf.] Shorter Proof Found? no Proof reused from monoW proof search time: 0 min, 2 sec Results for fold 10 Results for lemma ifPn: : if_spec (~~ b) b (if b then vT else vF) SUCCESS! Proof Found in EFSM: [by case def_b b;, constructor ] Tactics applied: 369 Original Proof: [by case def_b: b; constructor; rewrite ?def_b.] Shorter Proof Found? yes Proof reused from ifP proof search time: 0 min, 0 sec Results for lemma pair_andP: P Q : P /\ Q <-> P * Q SUCCESS! Proof Found in EFSM: [by move=> *;, constructor ;, case ] Tactics applied: 11184 Original Proof: [by split; case.] Shorter Proof Found? no This is a novel proof proof search time: 0 min, 7 sec Results for lemma sub_in3: T d d' (P : T -> T -> T -> Prop) : sub_mem d d' -> forall Ph : ph {all3 P}, prop_in3 d' Ph -> prop_in3 d Ph SUCCESS! Proof Found in EFSM: [by move=> /= sub sub3;, exact sub_in111 ] Tactics applied: 898 Original Proof: [by move=> /= sub_dd'; exact: sub_in111.] Shorter Proof Found? no Proof reused from sub_in21 proof search time: 0 min, 1 sec Results for lemma monoLR: : {mono f : x y / aR x y >-> rR x y} -> forall x y, rR (f x) y = aR x (g y) FAILURE! Tactics applied: 100000 Original Proof: [by move=> mf x y; rewrite -{1}[y]fgK mf.] Proof search time: 1 min, 46 sec Results for lemma norP: : reflect (~~ b1 /\ ~~ b2) (~~ (b1 || b2)) SUCCESS! Proof Found in EFSM: [by case b1;, case b2;, constructor ;, try by case ] Tactics applied: 42002 Original Proof: [by case b1; case b2; constructor; auto; case; auto.] Shorter Proof Found? yes This is a novel proof This proof contained a loop around a state proof search time: 0 min, 35 sec Results for lemma canRL_in: x y : {in D1, cancel f g} -> x \in D1 -> f x = y -> x = g y SUCCESS! Proof Found in EFSM: [by move=> fK D2fx <-;, rewrite fK ] Tactics applied: 1524 Original Proof: [by move=> fK D1x <-; rewrite fK.] Shorter Proof Found? no Proof reused from canRL_on proof search time: 0 min, 2 sec Results for lemma not_false_is_true: : ~ false SUCCESS! Proof Found in EFSM: [by [] ] Tactics applied: 1 Original Proof: [by [].] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Results for lemma orNb: b : ~~ b || b = true SUCCESS! Proof Found in EFSM: [by case b ] Tactics applied: 5 Original Proof: [by case: b.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Results for lemma xorPif: : Q \/ P -> ~ (Q /\ P) -> if b then ~ Q else Q FAILURE! Tactics applied: 100000 Original Proof: [by case Hb => [? _ H ? | ? H _]; case: H.] Proof search time: 2 min, 16 sec Results for lemma orbA: : associative orb SUCCESS! Proof Found in EFSM: [by case ] Tactics applied: 2 Original Proof: [by do 3!case.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Results for lemma andFb: : left_zero false andb SUCCESS! Proof Found in EFSM: [by [] ] Tactics applied: 1 Original Proof: [by [].] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Results for lemma andbT: : right_id true andb SUCCESS! Proof Found in EFSM: [by case ] Tactics applied: 2 Original Proof: [by case.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Results for lemma inW_bij: : bijective f -> {in D1, bijective f} SUCCESS! Proof Found in EFSM: [by case=> g' fK g'K;, exists g' => * ? *] Tactics applied: 714 Original Proof: [by case=> g' fK g'K; exists g' => * ? *; auto.] Shorter Proof Found? yes Proof reused from inT_bij This proof contained a loop around a state proof search time: 0 min, 1 sec Results for lemma addIb: : left_injective addb SUCCESS! Proof Found in EFSM: [by do 3!case ] Tactics applied: 23 Original Proof: [by do 3!case.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Results for lemma elimTFn: : b = c -> if c then ~ P else P FAILURE! Tactics applied: 100000 Original Proof: [by move <-; apply: (elimNTF Hb); case b.] Proof search time: 1 min, 55 sec Results for lemma addNb: a b : ~~ a (+) b = ~~ (a (+) b) SUCCESS! Proof Found in EFSM: [by case a;, case b ] Tactics applied: 528 Original Proof: [by case: a; case: b.] Shorter Proof Found? no Proof reused from orb_idr This proof contained a loop around a state proof search time: 0 min, 1 sec Results for lemma andb_idl: (a b : bool) : (b -> a) -> a && b = b SUCCESS! Proof Found in EFSM: [by case a;, case b => // -> ] Tactics applied: 529 Original Proof: [by case: a; case: b => // ->.] Shorter Proof Found? no Proof reused from orb_idr This proof contained a loop around a state proof search time: 0 min, 0 sec Results for lemma homoLR_in: : {in aD &, {homo f : x y / aR x y >-> rR x y}} -> {in aD & rD, forall x y, aR x (g y) -> rR (f x) y} SUCCESS! Proof Found in EFSM: [by move=> Hf x y hx hy /Hf;, rewrite fgK_on //;, apply ] Tactics applied: 14717 Original Proof: [by move=> Hf x y hx hy /Hf; rewrite fgK_on //; apply.] Shorter Proof Found? no Proof reused from homoRL_in proof search time: 0 min, 13 sec Results for lemma andKb: a b : a || b && a = a SUCCESS! Proof Found in EFSM: [by case a;, case b ] Tactics applied: 528 Original Proof: [by case: a; case: b.] Shorter Proof Found? no Proof reused from orb_idr This proof contained a loop around a state proof search time: 0 min, 0 sec Results for lemma implyb_idr: (a b : bool) : (b -> ~~ a) -> (a ==> b) = ~~ a SUCCESS! Proof Found in EFSM: [by case a;, case b => // -> ] Tactics applied: 529 Original Proof: [by case: a; case: b => // ->.] Shorter Proof Found? no Proof reused from orb_idr This proof contained a loop around a state proof search time: 0 min, 1 sec Results for lemma all_and2: (hP : forall x, [/\ P1 x & P2 x]) : [/\ a P1 & a P2] SUCCESS! Proof Found in EFSM: [by split=> x;, case (hP x) ] Tactics applied: 2339 Original Proof: [by split=> x; case: (hP x).] Shorter Proof Found? no Proof reused from all_and3 This proof contained a loop around a state proof search time: 0 min, 1 sec Results for lemma andbAC: : right_commutative andb SUCCESS! Proof Found in EFSM: [by do 3!case ] Tactics applied: 23 Original Proof: [by do 3!case.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Results for lemma can_mono: : {mono f : x y / aR x y >-> rR x y} -> {mono g : x y / rR x y >-> aR x y} FAILURE! Tactics applied: 100000 Original Proof: [by move=> mf x y /=; rewrite -mf !fgK.] Proof search time: 1 min, 53 sec Results for lemma forE: x P phP : @prop_for x P phP = P x SUCCESS! Proof Found in EFSM: [by [] ] Tactics applied: 1 Original Proof: [by [].] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec OVERALL RESULTS SUMMARY EFSMProver proved 189 out of 240 lemmas. Success rate of 78.75% There were 0 errors. 51 proof attempts exhausted the automaton On average, a proof was found after applying 1515 tactics The longest proof consisted of 4 tactics There were 18 shorter proofs found Of the 51 failures, 51 of them used all 100000 tactics There were 150 reused proofs found There were 39 novel proofs found Of the 51 failures, the average number of tactics used was 100000On average, a proof was found after 0 min, 1 sec On average, a failed proof attempt took 1 min, 46 sec On average, any (success or failure) proof attempt took 0 min, 24 sec The longest time to find a proof was 0 min, 35 sec The shortest time to find a proof was 0 min, 0 sec There were 0 proofs containing repeated tactics There were 36 proofs that repeated states