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 ->;, rewrite fK ] Tactics applied: 1738 Original Proof: [by move=> fK D2fy ->; rewrite fK.] Shorter Proof Found? no Proof reused from canLR_in This proof contained a loop around a state 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: 1 min, 8 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: 0 min, 59 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: 1343 Original Proof: [by move=> /= sub_dd'; exact: sub_in11.] Shorter Proof Found? no This is a novel proof This proof contained a loop around a state 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, 10 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: 2138 Original Proof: [by move=> mf x y; rewrite -{1}[x]fgK mf.] Shorter Proof Found? no Proof reused from can_mono This proof contained a loop around a state 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: 1089 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: 1053 Original Proof: [by move=> ? ?; auto.] Shorter Proof Found? no This is a novel proof This proof contained a loop around a state 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, 2 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: 238 Original Proof: [by case b1; constructor.] Shorter Proof Found? no Proof reused from negPn This proof contained a loop around a state 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: 316 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: 663 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: 19754 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, 13 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: 1227 Original Proof: [by move=> ? ?; auto.] Shorter Proof Found? no Proof reused from in1T This proof contained a loop around a state 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: 2197 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 This proof contained a loop around a state proof search time: 0 min, 3 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: 42 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: 96 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: 1583 Original Proof: [by case: a; case: b.] Shorter Proof Found? no Proof reused from addbN This proof contained a loop around a state 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: 2906 Original Proof: [by move=> Hf x y /Hf; rewrite fgK.] 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 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)} FAILURE! Tactics applied: 100000 Original Proof: [by move=> Hf x y hx hy /Hf; rewrite fgK_on //; apply.] Proof search time: 1 min, 46 sec Results for lemma contraT: b : (~~ b -> false) -> b SUCCESS! Proof Found in EFSM: [by case b => // -> ] Tactics applied: 46 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: 62625 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, 52 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, 11 sec Results for lemma mem_simpl: sp : mem sp = sp :> pred T SUCCESS! Proof Found in EFSM: [split => [eqiR [Rxx trR] x y z *]] 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: 52755 Original Proof: [by case: Pb; constructor; auto.] Shorter Proof Found? no This is a novel proof proof search time: 0 min, 45 sec Results for lemma negbT: b : b = false -> ~~ b SUCCESS! Proof Found in EFSM: [by case b ] Tactics applied: 37 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: 37 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: 1112 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, 1 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: 37 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: 42 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: 54 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: 4349 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 This proof contained a loop around a state proof search time: 0 min, 5 sec Results for lemma contraLR: (c b : bool) : (~~ c -> ~~ b) -> b -> c SUCCESS! Proof Found in EFSM: [by case b;, case c ] Tactics applied: 1265 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, 1 sec Results for lemma orbF: : right_id false orb SUCCESS! Proof Found in EFSM: [by case ] Tactics applied: 33 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: [split => [eqiR [Rxx trR] x y z *]] 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: 1 min, 26 sec Results for lemma orbT: : forall b, b || true SUCCESS! Proof Found in EFSM: [by case ] Tactics applied: 33 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 b;, case c => // -> ] Tactics applied: 1266 Original Proof: [by move/contraFN=> bF_notc /bF_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 addbT: b : b (+) true = ~~ b SUCCESS! Proof Found in EFSM: [by case b ] Tactics applied: 37 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: 50 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, 2 sec Results for lemma addbN: a b : a (+) ~~ b = ~~ (a (+) b) SUCCESS! Proof Found in EFSM: [by case a] Tactics applied: 39 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: 482 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;, apply ] Tactics applied: 1672 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: 481 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: 812 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: 50 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: 392 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: 2719 Original Proof: [by move=> hf x y hx hy axy; rewrite hf.] Shorter Proof Found? no Proof reused from can_mono_in This proof contained a loop around a state 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: 0 min, 58 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: 1652 Original Proof: [by move=> Hf x y /Hf; rewrite fgK.] 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 boolP: : alt_spec b1 b1 b1 SUCCESS! Proof Found in EFSM: [by case b1;, constructor ] Tactics applied: 384 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: 812 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: 39 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: 11883 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, 9 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: 33 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: [move => T P [] // IH] Tactics applied: 18 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: 481 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: 1 min, 34 sec Results for lemma andbCA: : left_commutative andb SUCCESS! Proof Found in EFSM: [by do 2!case ] Tactics applied: 50 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: 50 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: 29 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: 392 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: [auto ] Tactics applied: 94 Original Proof: [by move=> ? ?; auto.] Shorter Proof Found? yes Single step proof reused 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, 27 sec Results for lemma elimNf: : ~~ b = false -> P SUCCESS! Proof Found in EFSM: [by case Pb ] Tactics applied: 32 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: 46 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 SUCCESS! Proof Found in EFSM: [rewrite -if_neg;, by case Hb;, auto ] Tactics applied: 4577 Original Proof: [rewrite -if_neg; exact: equivPif.] Shorter Proof Found? no This is a novel proof proof search time: 0 min, 2 sec Results for lemma on1lT: : {on T2, allQ1l f & h} -> allQ1l f h SUCCESS! Proof Found in EFSM: [by move=> ? ?;, auto ] Tactics applied: 1350 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: 2843 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: 50 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 SUCCESS! Proof Found in EFSM: [by case Pb;, constructor ;, by case Pb ] Tactics applied: 14486 Original Proof: [by case def_b: b / Pb; constructor; rewrite ?def_b.] Shorter Proof Found? no This is a novel proof proof search time: 0 min, 8 sec Results for lemma in2W: : {all2 P2} -> {in D1 & D2, {all2 P2}} SUCCESS! Proof Found in EFSM: [by move=> *] Tactics applied: 59 Original Proof: [by move=> ? ?.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 1 sec Results for lemma introF: : ~ P -> b = false SUCCESS! Proof Found in EFSM: [by case Pb ] Tactics applied: 32 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: 33 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: 27 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: [split => [eqiR [Rxx trR] x y z *]] 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: 2843 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: 1 min, 13 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, 59 sec Results for lemma negb_and: (a b : bool) : ~~ (a && b) = ~~ a || ~~ b SUCCESS! Proof Found in EFSM: [by case a] Tactics applied: 38 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, 29 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, 33 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, 33 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, 45 sec Results for lemma ifT: : b -> (if b then vT else vF) = vT SUCCESS! Proof Found in EFSM: [by case b ] Tactics applied: 33 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, 35 sec Results for fold 5 Results for lemma simpl_predE: p : SimplPred p =1 p SUCCESS! Proof Found in EFSM: [exact ] Tactics applied: 32 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: 0 min, 55 sec Results for lemma orbCA: : left_commutative orb SUCCESS! Proof Found in EFSM: [by do 2!case ] Tactics applied: 116 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, 0 sec Results for lemma in3W: : {all3 P3} -> {in D1 & D2 & D3, {all3 P3}} SUCCESS! Proof Found in EFSM: [by move=> *] Tactics applied: 129 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, 40 sec Results for lemma addTb: b : true (+) b = ~~ b SUCCESS! Proof Found in EFSM: [exact ] Tactics applied: 32 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: 38 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: [try by case ] Tactics applied: 77 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: 8035 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: 5219 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, 3 sec Results for lemma andbK: a b : a && b || a = a SUCCESS! Proof Found in EFSM: [by case b;, by case a] Tactics applied: 5385 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, 3 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: 2077 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, 3 sec Results for lemma negPf: : reflect (b1 = false) (~~ b1) SUCCESS! Proof Found in EFSM: [case b1;, constructor => //] Tactics applied: 3393 Original Proof: [by case b1; constructor.] Shorter Proof Found? no This is a novel proof proof search time: 0 min, 1 sec Results for lemma implybN: a b : (a ==> ~~ b) = (b ==> ~~ a) SUCCESS! Proof Found in EFSM: [by case b;, by case a] Tactics applied: 5219 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, 3 sec Results for lemma orFb: : left_id false orb SUCCESS! Proof Found in EFSM: [exact ] Tactics applied: 32 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, 48 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, 12 sec Results for lemma implyNb: a b : (~~ a ==> b) = a || b SUCCESS! Proof Found in EFSM: [by case a] Tactics applied: 105 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, 27 sec Results for lemma negbLR: b c : b = ~~ c -> ~~ b = c SUCCESS! Proof Found in EFSM: [case b;, case c => // -> ] Tactics applied: 3540 Original Proof: [exact: canLR negbK.] Shorter Proof Found? no This is a novel proof 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: 36 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: [case b => // -> ] Tactics applied: 63 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, 15 sec Results for fold 6 Results for lemma andbb: : idempotent andb SUCCESS! Proof Found in EFSM: [try by case ] Tactics applied: 7 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: 0 min, 51 sec Results for lemma andb_addl: : left_distributive andb addb SUCCESS! Proof Found in EFSM: [by do 3!case ] Tactics applied: 114 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: [by case b;, by case a] Tactics applied: 7022 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, 5 sec Results for lemma introNf: : P -> ~~ b = false SUCCESS! Proof Found in EFSM: [by case def_b b / Pb] Tactics applied: 98 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;, by case c] Tactics applied: 6626 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, 4 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: 8166 Original Proof: [by case: a; case: b => // ->.] Shorter Proof Found? no This is a novel proof proof search time: 0 min, 5 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: 7105 Original Proof: [case; [exact: introT | exact: introF].] Shorter Proof Found? no This is a novel proof proof search time: 0 min, 4 sec Results for lemma idP: : reflect b1 b1 SUCCESS! Proof Found in EFSM: [by case b1;, constructor ] Tactics applied: 6439 Original Proof: [by case b1; constructor.] Shorter Proof Found? no Proof reused from idPn 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: [by case b ] Tactics applied: 95 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: 97 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: 8166 Original Proof: [by case: a; case: b; case: c => // ->.] Shorter Proof Found? yes This is a novel proof proof search time: 0 min, 6 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, 9 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: 8194 Original Proof: [by case: a; case: b; case: c => // ->.] Shorter Proof Found? yes This is a novel proof proof search time: 0 min, 6 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: 2020 Original Proof: [by move=> /= sub1 sub; exact: sub_in111.] 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 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: 110 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: 98 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: [by case b;, by case c] Tactics applied: 7018 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, 4 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: 156 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, 10 sec Results for lemma addbA: : associative addb SUCCESS! Proof Found in EFSM: [by do 3!case ] Tactics applied: 114 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: 7 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, 22 sec Results for fold 7 Results for lemma elimN: : ~~ b -> ~P SUCCESS! Proof Found in EFSM: [by case Pb ] Tactics applied: 28 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, 23 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: 1310 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, 2 sec Results for lemma orTb: : forall b, true || b SUCCESS! Proof Found in EFSM: [split => [eqiR [Rxx trR] x y z]] 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: [split => [eqiR [Rxx trR] x y z]] 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: 2392 Original Proof: [by move=> fK D2fx <-; rewrite fK.] Shorter Proof Found? no Proof reused from canRL_in This proof contained a loop around a state proof search time: 0 min, 3 sec Results for lemma addbAC: : right_commutative addb SUCCESS! Proof Found in EFSM: [by do 3!case ] Tactics applied: 46 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: 46 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;, first exact ] Tactics applied: 1109 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, 29 sec Results for lemma addKb: : left_loop id addb SUCCESS! Proof Found in EFSM: [by do 2!case ] Tactics applied: 45 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: 1 min, 48 sec Results for lemma elimT: : b -> P SUCCESS! Proof Found in EFSM: [by case Pb ] Tactics applied: 28 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: 26145 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, 22 sec Results for lemma wlog_neg: b : (~~ b -> b) -> b SUCCESS! Proof Found in EFSM: [by case b => // -> ] Tactics applied: 39 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: [move => T P [] // IH;, auto ] Tactics applied: 204 Original Proof: [move=> allP x /sub1; exact: allP.] Shorter Proof Found? no This is a novel proof 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, 14 sec Results for lemma orbN: b : b || ~~ b = true SUCCESS! Proof Found in EFSM: [by case b ] Tactics applied: 29 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: 66127 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: 1 min, 8 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: 2455 Original Proof: [by move=> fK D1y ->; rewrite fK.] Shorter Proof Found? no Proof reused from canLR_on This proof contained a loop around a state proof search time: 0 min, 3 sec Results for lemma orb_andr: : right_distributive orb andb SUCCESS! Proof Found in EFSM: [by case ] Tactics applied: 25 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: 28 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: 652 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' => * ? *;, gs [exact fK exact g'K]] Tactics applied: 29790 Original Proof: [by case=> g' fK g'K; exists g' => * ? *; auto.] Shorter Proof Found? no This is a novel proof This proof contained a loop around a state proof search time: 0 min, 26 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: 1645 Original Proof: [by move=> allQ x /sub2; exact: allQ.] Shorter Proof Found? no Proof reused from in2T This proof contained a loop around a state 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: 15 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: 15 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: 1667 Original Proof: [by move=> allP x1 x2 x3 /sub1 d1x1 /sub2 d2x2 /sub3; exact: allP.] Shorter Proof Found? no Proof reused from in2T This proof contained a loop around a state 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: 15 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: 1667 Original Proof: [move=> allP x1 x2 /sub1 d1x1 /sub2; exact: allP.] Shorter Proof Found? no Proof reused from in2T This proof contained a loop around a state proof search time: 0 min, 2 sec Results for lemma introN: : ~ P -> ~~ b SUCCESS! Proof Found in EFSM: [by case Pb ] Tactics applied: 14 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: 58 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: 0 min, 53 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, 15 sec Results for lemma orb_andl: : left_distributive orb andb SUCCESS! Proof Found in EFSM: [by do 3!case ] Tactics applied: 33 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: 11 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: [split => [eqiR [Rxx trR] x y z *]] Tactics applied: 7 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: [split => [eqiR [Rxx trR] x y z *]] Tactics applied: 7 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, 27 sec Results for lemma andTb: : left_id true andb SUCCESS! Proof Found in EFSM: [split => [eqiR [Rxx trR] x y z *]] Tactics applied: 7 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: 42 Original Proof: [by move=> ? ?.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 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, 20 sec Results for lemma implybF: b : (b ==> false) = ~~ b SUCCESS! Proof Found in EFSM: [split => [eqiR [Rxx trR] x y z *]] Tactics applied: 7 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: 32 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: 1645 Original Proof: [by move=> ? ?; auto.] Shorter Proof Found? no Proof reused from in2T This proof contained a loop around a state proof search time: 0 min, 2 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, 20 sec Results for lemma ifF: : b = false -> (if b then vT else vF) = vF SUCCESS! Proof Found in EFSM: [by case b ] Tactics applied: 15 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: 1173 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: 3415 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: 1123 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: [try by case ] Tactics applied: 1 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: 54877 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, 46 sec Results for lemma implybb: b : b ==> b SUCCESS! Proof Found in EFSM: [by case b ] Tactics applied: 40 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: [auto ] Tactics applied: 2 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: [move => T P [] // IH;, auto ] Tactics applied: 344 Original Proof: [by move=> allQ x /sub2; exact: allQ.] Shorter Proof Found? no This is a novel proof 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: 40 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: [auto ] Tactics applied: 2 Original Proof: [by move=> ? ?; auto.] Shorter Proof Found? yes Single step proof reused proof search time: 0 min, 0 sec Results for lemma elimFn: : b' = false -> P FAILURE! Tactics applied: 100000 Original Proof: [exact: elimTFn false _.] Proof search time: 1 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: 1 min, 35 sec Results for lemma implybT: b : b ==> true SUCCESS! Proof Found in EFSM: [by case b ] Tactics applied: 40 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: 1 min, 37 sec Results for lemma andbC: : commutative andb SUCCESS! Proof Found in EFSM: [by do 2!case ] Tactics applied: 57 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: 1 min, 36 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: 2878 Original Proof: [by move=> hf x y axy; rewrite hf.] Shorter Proof Found? no Proof reused from monoW proof search time: 0 min, 3 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: 1 min, 32 sec Results for lemma andbN: b : b && ~~ b = false SUCCESS! Proof Found in EFSM: [by case b ] Tactics applied: 40 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: 1 min, 48 sec Results for lemma addbK: : right_loop id addb SUCCESS! Proof Found in EFSM: [by do 2!case ] Tactics applied: 57 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: 989 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: 1 min, 32 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: 2934 Original Proof: [by move=> hf x hx ax; rewrite hf.] Shorter Proof Found? no Proof reused from monoW proof search time: 0 min, 3 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: 1380 Original Proof: [by case def_b: b; constructor; rewrite ?def_b.] Shorter Proof Found? yes Proof reused from ifP This proof contained a loop around a state proof search time: 0 min, 0 sec Results for lemma pair_andP: P Q : P /\ Q <-> P * Q SUCCESS! Proof Found in EFSM: [by split;, try by case ] Tactics applied: 4538 Original Proof: [by split; case.] Shorter Proof Found? no This is a novel proof proof search time: 0 min, 2 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: [move => mf mg x y hx hy;, auto ] Tactics applied: 530 Original Proof: [by move=> /= sub_dd'; exact: sub_in111.] Shorter Proof Found? no This is a novel proof This proof contained a loop around a state 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, 3 sec Results for lemma norP: : 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, 13 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: 3525 Original Proof: [by move=> fK D1x <-; rewrite fK.] Shorter Proof Found? no Proof reused from canRL_on This proof contained a loop around a state proof search time: 0 min, 4 sec Results for lemma not_false_is_true: : ~ false SUCCESS! Proof Found in EFSM: [by [] ] Tactics applied: 30 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: 35 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: 1 min, 42 sec Results for lemma orbA: : associative orb SUCCESS! Proof Found in EFSM: [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 andFb: : left_zero false andb SUCCESS! Proof Found in EFSM: [split => [eqiR [Rxx trR] x y z *]] 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: 32 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: 2005 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, 2 sec Results for lemma addIb: : left_injective addb SUCCESS! Proof Found in EFSM: [by do 3!case ] Tactics applied: 53 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, 23 sec Results for lemma addNb: a b : ~~ a (+) b = ~~ (a (+) b) SUCCESS! Proof Found in EFSM: [by case a;, case b ] Tactics applied: 1655 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: 1738 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 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} FAILURE! Tactics applied: 100000 Original Proof: [by move=> Hf x y hx hy /Hf; rewrite fgK_on //; apply.] Proof search time: 1 min, 50 sec Results for lemma andKb: a b : a || b && a = a SUCCESS! Proof Found in EFSM: [by case a;, case b ] Tactics applied: 1655 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 implyb_idr: (a b : bool) : (b -> ~~ a) -> (a ==> b) = ~~ a SUCCESS! Proof Found in EFSM: [by case a;, case b => // -> ] Tactics applied: 1738 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: 4769 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, 2 sec Results for lemma andbAC: : right_commutative andb SUCCESS! Proof Found in EFSM: [by do 3!case ] Tactics applied: 53 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, 25 sec Results for lemma forE: x P phP : @prop_for x P phP = P x SUCCESS! Proof Found in EFSM: [split => [eqiR [Rxx trR] x y z *]] 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 188 out of 240 lemmas. Success rate of 78.33333333333333% There were 0 errors. 52 proof attempts exhausted the automaton On average, a proof was found after applying 2838 tactics The longest proof consisted of 3 tactics There were 19 shorter proofs found Of the 52 failures, 52 of them used all 100000 tactics There were 145 reused proofs found There were 43 novel proofs found Of the 52 failures, the average number of tactics used was 100000On average, a proof was found after 0 min, 2 sec On average, a failed proof attempt took 1 min, 24 sec On average, any (success or failure) proof attempt took 0 min, 20 sec The longest time to find a proof was 1 min, 8 sec The shortest time to find a proof was 0 min, 0 sec There were 0 proofs containing repeated tactics There were 58 proofs that repeated states