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: 1553 Original Proof: [by move=> fK D2fy ->; rewrite fK.] Shorter Proof Found? no Proof reused from canLR_in proof search time: 0 min, 2 sec Results for lemma introTn: : ~ P -> b' FAILURE! Tactics applied: 11457 Original Proof: [exact: introTFn true _.] Proof search time: 0 min, 15 sec Results for lemma classic_bind: : forall P Q, (P -> classically Q) -> (classically P -> classically Q) FAILURE! Tactics applied: 12098 Original Proof: [by move=> P Q IH IH_P b IH_Q; apply: IH_P; move/IH; exact.] Proof search time: 0 min, 16 sec Results for lemma addbCA: : left_commutative addb SUCCESS! Proof Found in EFSM: [by do 2!case ] Tactics applied: 49 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: [move => mf mg x y hx hy;, auto ] Tactics applied: 306 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: 11884 Original Proof: [move=> mf mg x y; case: (boolP (rR _ _))=> [/mg //|]. by apply: contraNF=> /mf; rewrite !fgK.] Proof search time: 0 min, 22 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: 1822 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: [move => mf mg x y hx hy;, auto ] Tactics applied: 306 Original Proof: [by move=> /= sub sub3; exact: sub_in111.] Shorter Proof Found? no This is a novel proof proof search time: 0 min, 1 sec Results for lemma addbb: : self_inverse false addb SUCCESS! Proof Found in EFSM: [by case ] Tactics applied: 29 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: [move => P;, auto ] Tactics applied: 150 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: 11454 Original Proof: [by case: ap => _ /= ->.] Proof search time: 0 min, 11 sec Results for lemma andbF: : right_zero false andb SUCCESS! Proof Found in EFSM: [by case ] Tactics applied: 29 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: 469 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: 567 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 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: 76 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: 32 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: 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 orb_idr: (a b : bool) : (b -> a) -> a || b = a SUCCESS! Proof Found in EFSM: [by case a;, case b => // -> ] Tactics applied: 800 Original Proof: [by case: a; case: b => // ->.] Shorter Proof Found? no Proof reused from orb_idl proof search time: 0 min, 1 sec Results for lemma subrelUr: r1 r2 : subrel r2 (relU r1 r2) FAILURE! Tactics applied: 11930 Original Proof: [by move=> *; apply/orP; right.] Proof search time: 0 min, 13 sec Results for lemma orbb: : idempotent orb SUCCESS! Proof Found in EFSM: [by case ] Tactics applied: 29 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: 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 on1T: : {on T2, allQ1 f} -> allQ1 f SUCCESS! Proof Found in EFSM: [by move=> ? ?;, auto ] Tactics applied: 1170 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: 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 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: 1901 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, 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: 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 topredE: x (pp : pT) : topred pp x = (x \in pp) SUCCESS! Proof Found in EFSM: [by rewrite -mem_topred ] Tactics applied: 93 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: 831 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: 1491 Original Proof: [by move=> Hf x y /Hf; rewrite fgK.] Shorter Proof Found? no Proof reused from homoRL proof search time: 0 min, 2 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: 6171 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: 43 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: 4405 Original Proof: [by case: a; case: b; case: c => // ->.] Shorter Proof Found? no Proof reused from andb_id2l proof search time: 0 min, 4 sec Results for lemma or3P: : reflect [\/ b1, b2 | b3] [|| b1, b2 | b3] FAILURE! Tactics applied: 15533 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: 0 min, 19 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: 27 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: 3823 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: 34 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: 34 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: 522 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: 34 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: 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 andbACA: : interchange andb andb SUCCESS! Proof Found in EFSM: [by do 3!case ] Tactics applied: 51 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: 2260 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: 661 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: 30 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: 27 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: 15515 Original Proof: [exact: elimTFn true _.] Proof search time: 0 min, 15 sec Results for lemma orbT: : forall b, b || true SUCCESS! Proof Found in EFSM: [by case ] Tactics applied: 30 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: 703 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: 34 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: 6220 Original Proof: [by move=> P [] // IH; apply IH; right => ?; apply: notF (IH _); left.] Proof search time: 0 min, 5 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: 214 Original Proof: [by move/contra=> notb_notc /notb_notc/negbTE.] Shorter Proof Found? no This is a novel proof 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: 949 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: 213 Original Proof: [exact: canRL negbK.] Shorter Proof Found? no This is a novel proof 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: 409 Original Proof: [by case: a; case: b => // ->.] Shorter Proof Found? no Proof reused from andb_idr proof search time: 0 min, 0 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: 193 Original Proof: [by case b1; constructor.] Shorter Proof Found? no Proof reused from negPf 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: 1510 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, 2 sec Results for lemma orP: : reflect (b1 \/ b2) (b1 || b2) SUCCESS! Proof Found in EFSM: [by case b1;, case b2;, constructor ;, auto ;, case ] Tactics applied: 5301 Original Proof: [by case b1; case b2; constructor; auto; case.] Shorter Proof Found? no Proof reused from nandP proof search time: 0 min, 3 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: 892 Original Proof: [by move=> Hf x y /Hf; rewrite fgK.] Shorter Proof Found? no Proof reused from homoLR proof search time: 0 min, 1 sec Results for lemma boolP: : alt_spec b1 b1 b1 SUCCESS! Proof Found in EFSM: [by case b1;, constructor ] Tactics applied: 193 Original Proof: [exact: (altP idP).] Shorter Proof Found? no Proof reused from negPf 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: 409 Original Proof: [by case: a; case: b => // ->.] Shorter Proof Found? no Proof reused from andb_idr proof search time: 0 min, 0 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: 2103 Original Proof: [by case b; constructor; auto.] Shorter Proof Found? no This is a novel proof proof search time: 0 min, 1 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: 213 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 xorPifn: : Q \/ P -> ~ (Q /\ P) -> if b then Q else ~ Q FAILURE! Tactics applied: 6172 Original Proof: [rewrite -if_neg; exact: xorPif.] Proof search time: 0 min, 6 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: 193 Original Proof: [by case b1; constructor; auto.] Shorter Proof Found? yes Proof reused from negPf 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: [move => P;, auto ] Tactics applied: 106 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: 10767 Original Proof: [by rewrite /mem; case: pT pp => T1 app1 [mem1 /= ->].] Proof search time: 0 min, 14 sec Results for lemma elimNf: : ~~ b = false -> P SUCCESS! Proof Found in EFSM: [by case Pb ] Tactics applied: 30 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: 44 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: 10768 Original Proof: [rewrite -if_neg; exact: equivPif.] Proof search time: 0 min, 12 sec Results for lemma on1lT: : {on T2, allQ1l f & h} -> allQ1l f h SUCCESS! Proof Found in EFSM: [by move=> ? ?;, auto ] Tactics applied: 1139 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: 2170 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: 48 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: 10766 Original Proof: [by case def_b: b / Pb; constructor; rewrite ?def_b.] Proof search time: 0 min, 10 sec Results for lemma in2W: : {all2 P2} -> {in D1 & D2, {all2 P2}} SUCCESS! Proof Found in EFSM: [by move=> *] Tactics applied: 57 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: 30 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: 31 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: 26 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: 22 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: 2170 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: 10770 Original Proof: [by move=> Qb; split=> ?; [exact: appP | apply: elimT; case: Qb].] Proof search time: 0 min, 11 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: 11497 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: 0 min, 25 sec Results for lemma negb_and: (a b : bool) : ~~ (a && b) = ~~ a || ~~ b SUCCESS! Proof Found in EFSM: [by case a] Tactics applied: 36 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: 10767 Original Proof: [by case: decQ; constructor.] Proof search time: 0 min, 10 sec Results for lemma andP: : reflect (b1 /\ b2) (b1 && b2) SUCCESS! Proof Found in EFSM: [by case b1;, case b2;, constructor ;, auto ;, case ] Tactics applied: 8776 Original Proof: [by case b1; case b2; constructor=> //; case.] Shorter Proof Found? no Proof reused from nandP proof search time: 0 min, 7 sec Results for lemma contraFN: (c b : bool) : (c -> b) -> b = false -> ~~ c FAILURE! Tactics applied: 11075 Original Proof: [by move/contra=> notb_notc /negbT.] Proof search time: 0 min, 12 sec Results for lemma sym_left_transitive: : left_transitive FAILURE! Tactics applied: 11005 Original Proof: [by move=> x y Rxy z; apply/idP/idP; apply: trR; rewrite // symR.] Proof search time: 0 min, 14 sec Results for lemma ifT: : b -> (if b then vT else vF) = vT SUCCESS! Proof Found in EFSM: [by case b ] Tactics applied: 31 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: 11478 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: 0 min, 12 sec Results for fold 5 Results for lemma simpl_predE: p : SimplPred p =1 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 is_true_locked_true: : locked true FAILURE! Tactics applied: 14476 Original Proof: [by unlock.] Proof search time: 0 min, 16 sec Results for lemma orbCA: : left_commutative orb SUCCESS! Proof Found in EFSM: [by do 2!case ] Tactics applied: 21 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: 14371 Original Proof: [by move=> Qb; move/introT; case: Qb.] Proof search time: 0 min, 19 sec Results for lemma in3W: : {all3 P3} -> {in D1 & D2 & D3, {all3 P3}} 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 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: 15609 Original Proof: [by move=> mf x y hx hy /=; rewrite -mf // !fgK_on.] Proof search time: 0 min, 34 sec Results for lemma addTb: 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 on1lW: : allQ1l f h -> {on D2, allQ1l f & h} 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 addbF: : right_id 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 subrelUl: r1 r2 : subrel r1 (relU r1 r2) FAILURE! Tactics applied: 15092 Original Proof: [by move=> *; apply/orP; left.] Proof search time: 0 min, 18 sec Results for lemma orKb: a b : a && (b || a) = a SUCCESS! Proof Found in EFSM: [by case a;, case b ] Tactics applied: 465 Original Proof: [by case: a; case: b.] Shorter Proof Found? no Proof reused from orbK proof search time: 0 min, 0 sec Results for lemma andbK: a b : a && b || a = a SUCCESS! Proof Found in EFSM: [by case a;, case b ] Tactics applied: 465 Original Proof: [by case: a; case: b.] Shorter Proof Found? no Proof reused from orbK proof search time: 0 min, 0 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: [by move=> ? ?;, auto ] Tactics applied: 894 Original Proof: [by move=> allQ x y /sub2=> d2fx /sub2; exact: allQ.] Shorter Proof Found? no Proof reused from on2T proof search time: 0 min, 1 sec Results for lemma negPf: : reflect (b1 = false) (~~ b1) SUCCESS! Proof Found in EFSM: [by case b1;, constructor ] Tactics applied: 137 Original Proof: [by case b1; constructor.] Shorter Proof Found? no Proof reused from idP proof search time: 0 min, 0 sec Results for lemma implybN: a b : (a ==> ~~ b) = (b ==> ~~ a) SUCCESS! Proof Found in EFSM: [by case a;, case b ] Tactics applied: 465 Original Proof: [by case: a; case: b.] Shorter Proof Found? no Proof reused from orbK proof search time: 0 min, 1 sec Results for lemma orFb: : left_id false orb 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 inT_bij: : {in T1, bijective f} -> bijective f SUCCESS! Proof Found in EFSM: [by case=> g' fK g'K;, exists g' => * ? *;, auto ] Tactics applied: 3525 Original Proof: [by case=> g' fK g'K; exists g' => * ? *; auto.] Shorter Proof Found? no Proof reused from onW_bij proof search time: 0 min, 3 sec Results for lemma in_applicative: x p (amp : applicative_mem_pred p) : in_mem x amp = p x FAILURE! Tactics applied: 14476 Original Proof: [by case: amp => [[_ /= ->]].] Proof search time: 0 min, 19 sec Results for lemma implyNb: 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 or4P: : reflect [\/ b1, b2, b3 | b4] [|| b1, b2, b3 | b4] FAILURE! Tactics applied: 14491 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: 0 min, 17 sec Results for lemma negbLR: b c : b = ~~ c -> ~~ b = c SUCCESS! Proof Found in EFSM: [by case b;, case c ] Tactics applied: 215 Original Proof: [exact: canLR negbK.] Shorter Proof Found? no This is a novel proof proof search time: 0 min, 0 sec Results for lemma on2W: : allQ2 f -> {on D2 &, allQ2 f} 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, 0 sec Results for lemma andNb: b : ~~ b && b = false 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 equivPif: : (Q -> P) -> (P -> Q) -> if b then Q else ~ Q FAILURE! Tactics applied: 14478 Original Proof: [by case Hb; auto.] Proof search time: 0 min, 18 sec Results for fold 6 Results for lemma andbb: : idempotent andb SUCCESS! Proof Found in EFSM: [by case ] Tactics applied: 28 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: 12760 Original Proof: [by case b1; case b2; case b3; case b4; case b5; constructor; try by case.] Proof search time: 0 min, 14 sec Results for lemma andb_addl: : left_distributive andb addb SUCCESS! Proof Found in EFSM: [by do 3!case ] Tactics applied: 49 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 a;, case b ] Tactics applied: 853 Original Proof: [by case: a; case: b.] Shorter Proof Found? no Proof reused from implyb_id2l proof search time: 0 min, 1 sec Results for lemma introNf: : P -> ~~ b = false SUCCESS! Proof Found in EFSM: [by case def_b b / Pb] Tactics applied: 34 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: 512 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 andb_idr: (a b : bool) : (a -> b) -> a && b = a SUCCESS! Proof Found in EFSM: [by case a;, case b => // -> ] Tactics applied: 897 Original Proof: [by case: a; case: b => // ->.] Shorter Proof Found? no Proof reused from andb_idl proof search time: 0 min, 1 sec Results for lemma sameP: : reflect P c -> b = c SUCCESS! Proof Found in EFSM: [by case def_b b / Pb;, case ] Tactics applied: 685 Original Proof: [case; [exact: introT | exact: introF].] Shorter Proof Found? no This is a novel proof proof search time: 0 min, 0 sec Results for lemma idP: : reflect b1 b1 SUCCESS! Proof Found in EFSM: [by case b1;, constructor ] Tactics applied: 526 Original Proof: [by case b1; constructor.] Shorter Proof Found? no Proof reused from idPn proof search time: 0 min, 0 sec Results for lemma if_same: : (if b then vT else vT) = vT SUCCESS! Proof Found in EFSM: [by case b ] Tactics applied: 31 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: 34 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;, auto ] Tactics applied: 876 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 addbP: a b : reflect (~~ a = b) (a (+) b) SUCCESS! Proof Found in EFSM: [by case a;, case b;, constructor ] Tactics applied: 3914 Original Proof: [by case: a; case: b; constructor.] Shorter Proof Found? no This is a novel proof proof search time: 0 min, 3 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;, auto ] Tactics applied: 876 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 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: 315 Original Proof: [by move=> /= sub1 sub; exact: sub_in111.] Shorter Proof Found? no This is a novel proof proof search time: 0 min, 1 sec Results for lemma addFb: : left_id false addb SUCCESS! Proof Found in EFSM: [split => [eqiR [Rxx trR] x y z *]] Tactics applied: 16 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: 46 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: 34 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;, case c ] Tactics applied: 640 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 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: 90 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: 12760 Original Proof: [by case b1; case b2; case b3; case b4; constructor; try by case.] Proof search time: 0 min, 14 sec Results for lemma addbA: : associative addb SUCCESS! Proof Found in EFSM: [by do 3!case ] Tactics applied: 49 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: [by case ] Tactics applied: 28 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: 12988 Original Proof: [by move=> haveP suffPQ suffQ; apply: haveP => /suffPQ; exact.] Proof search time: 0 min, 14 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: 14077 Original Proof: [by move=> x y /sym_left_transitive Rxy z; rewrite !(symR z) Rxy.] Proof search time: 0 min, 18 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: 851 Original Proof: [by case=> g' fK g'K; exists g' => * ? *; auto.] Shorter Proof Found? yes Proof reused from inW_bij proof search time: 0 min, 1 sec Results for lemma orTb: : forall b, true || b SUCCESS! Proof Found in EFSM: [split => [eqiR [Rxx trR] x y z]] Tactics applied: 22 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: 22 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: 1540 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: 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;, auto ] Tactics applied: 724 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: 13767 Original Proof: [by case: b => [_ haveC | haveC _]; exact: haveC.] Proof search time: 0 min, 14 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: 13768 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: 0 min, 22 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: 3661 Original Proof: [by case: a; case: b; case: c => // ->.] Shorter Proof Found? no Proof reused from orb_id2r proof search time: 0 min, 3 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: 147 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: 13767 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: 0 min, 12 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: 6559 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 proof search time: 0 min, 9 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: 1581 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: 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: 409 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 onT_bij: : {on T2, bijective f} -> bijective f SUCCESS! Proof Found in EFSM: [by case=> g' fK g'K;, exists g' => * ? *;, auto ] Tactics applied: 3943 Original Proof: [by case=> g' fK g'K; exists g' => * ? *; auto.] Shorter Proof Found? no Proof reused from inW_bij proof search time: 0 min, 4 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: [move => symR x y;, auto ] Tactics applied: 365 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 negbFE: b : ~~ b = false -> b SUCCESS! Proof Found in EFSM: [by case b ] Tactics applied: 32 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: 32 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: [move => mf mg x y hx hy;, auto ] Tactics applied: 279 Original Proof: [by move=> allP x1 x2 x3 /sub1 d1x1 /sub2 d2x2 /sub3; exact: allP.] Shorter Proof Found? no This is a novel proof proof search time: 0 min, 1 sec Results for lemma negbF: b : (b : bool) -> ~~ b = false SUCCESS! Proof Found in EFSM: [by case b ] Tactics applied: 32 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: [move => P Q IH [] // notPQ;, auto ] Tactics applied: 107 Original Proof: [move=> allP x1 x2 /sub1 d1x1 /sub2; exact: allP.] Shorter Proof Found? no This is a novel proof proof search time: 0 min, 1 sec Results for lemma introN: : ~ P -> ~~ b SUCCESS! Proof Found in EFSM: [by case Pb ] Tactics applied: 31 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: 75 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) SUCCESS! Proof Found in EFSM: [by case b1;, case b2;, constructor ;, auto ] Tactics applied: 8222 Original Proof: [by case b1; case b2; constructor; auto.] Shorter Proof Found? no Proof reused from norP proof search time: 0 min, 7 sec Results for lemma nandP: : reflect (~~ b1 \/ ~~ b2) (~~ (b1 && b2)) SUCCESS! Proof Found in EFSM: [by case b1;, case b2;, constructor ;, auto ;, case ] Tactics applied: 12033 Original Proof: [by case b1; case b2; constructor; auto; case; auto.] Shorter Proof Found? yes Proof reused from norP proof search time: 0 min, 13 sec Results for lemma orb_andl: : left_distributive orb andb SUCCESS! Proof Found in EFSM: [by do 3!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 monoW: : {mono f : x / aP x >-> rP x} -> {homo f : x / aP x >-> rP x} FAILURE! Tactics applied: 15192 Original Proof: [by move=> hf x ax; rewrite hf.] Proof search time: 0 min, 26 sec Results for lemma andb_orr: : right_distributive andb orb SUCCESS! Proof Found in EFSM: [by case ] Tactics applied: 28 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: 22 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: 22 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: 14618 Original Proof: [by move/(introNTF Hb) <-; case b.] Proof search time: 0 min, 17 sec Results for lemma andTb: : left_id true andb SUCCESS! Proof Found in EFSM: [split => [eqiR [Rxx trR] x y z *]] Tactics applied: 22 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: 59 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] SUCCESS! Proof Found in EFSM: [by case b1;, case b2;, case b3;, case b4;, constructor ;, try by case ] Tactics applied: 13533 Original Proof: [by case b1; case b2; case b3; constructor; try by case.] Shorter Proof Found? no Proof reused from and4P proof search time: 0 min, 13 sec Results for lemma implybF: b : (b ==> false) = ~~ b SUCCESS! Proof Found in EFSM: [split => [eqiR [Rxx trR] x y z *]] Tactics applied: 22 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: 49 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: [move => symR x y;, auto ] Tactics applied: 365 Original Proof: [by move=> ? ?; auto.] Shorter Proof Found? no This is a novel proof 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: 15457 Original Proof: [move=> T P [] // IH; apply IH; right=> x Px; case: notF. by apply: IH; left; exists x.] Proof search time: 0 min, 18 sec Results for lemma ifF: : b = false -> (if b then vT else vF) = vF SUCCESS! Proof Found in EFSM: [by case b ] Tactics applied: 32 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: 670 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: 2353 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: 636 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: 27 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: 6812 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 proof search time: 0 min, 10 sec Results for lemma implybb: b : b ==> b SUCCESS! Proof Found in EFSM: [by case b ] Tactics applied: 31 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: [split => [eqiR [Rxx trR] x y z *]] Tactics applied: 25 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: 221 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: 31 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: [move => P;, auto ] Tactics applied: 135 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: 14305 Original Proof: [exact: elimTFn false _.] Proof search time: 0 min, 19 sec Results for lemma equivP: : (P <-> Q) -> reflect Q b FAILURE! Tactics applied: 14308 Original Proof: [by case; exact: iffP.] Proof search time: 0 min, 19 sec Results for lemma implybT: b : b ==> true SUCCESS! Proof Found in EFSM: [by case b ] Tactics applied: 31 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: 14305 Original Proof: [exact: introTFn false _.] Proof search time: 0 min, 17 sec Results for lemma andbC: : commutative andb SUCCESS! Proof Found in EFSM: [by do 2!case ] Tactics applied: 47 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: 14573 Original Proof: [move=> symR x y; apply/idP/idP; exact: symR.] Proof search time: 0 min, 17 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: 1959 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: 14642 Original Proof: [by move/contraL=> b_notc /b_notc/negbTE.] Proof search time: 0 min, 18 sec Results for lemma andbN: b : b && ~~ b = false SUCCESS! Proof Found in EFSM: [by case b ] Tactics applied: 31 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: 14310 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: 0 min, 17 sec Results for lemma addbK: : right_loop id addb SUCCESS! Proof Found in EFSM: [by do 2!case ] Tactics applied: 47 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: 464 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: 14613 Original Proof: [by case: k_p.] Proof search time: 0 min, 17 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: 2002 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: 627 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 FAILURE! Tactics applied: 16045 Original Proof: [by split; case.] Proof search time: 0 min, 18 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: 306 Original Proof: [by move=> /= sub_dd'; exact: sub_in111.] Shorter Proof Found? no This is a novel proof 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: 16675 Original Proof: [by move=> mf x y; rewrite -{1}[y]fgK mf.] Proof search time: 0 min, 33 sec Results for lemma norP: : reflect (~~ b1 /\ ~~ b2) (~~ (b1 || b2)) SUCCESS! Proof Found in EFSM: [by case b1;, case b2;, constructor => //;, case ] Tactics applied: 8073 Original Proof: [by case b1; case b2; constructor; auto; case; auto.] Shorter Proof Found? yes Proof reused from andP proof search time: 0 min, 6 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: 1634 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: 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: 34 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: 16050 Original Proof: [by case Hb => [? _ H ? | ? H _]; case: H.] Proof search time: 0 min, 21 sec Results for lemma orbA: : associative orb SUCCESS! Proof Found in EFSM: [by case ] Tactics applied: 31 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: 31 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: 939 Original Proof: [by case=> g' fK g'K; exists g' => * ? *; auto.] Shorter Proof Found? yes Proof reused from inT_bij 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: 52 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: 16045 Original Proof: [by move <-; apply: (elimNTF Hb); case b.] Proof search time: 0 min, 17 sec Results for lemma addNb: a b : ~~ a (+) b = ~~ (a (+) b) SUCCESS! Proof Found in EFSM: [by case a;, case b ] Tactics applied: 764 Original Proof: [by case: a; case: b.] Shorter Proof Found? no Proof reused from orb_idr 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: 804 Original Proof: [by case: a; case: b => // ->.] Shorter Proof Found? no Proof reused from orb_idr 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} SUCCESS! Proof Found in EFSM: [by move=> Hf x y hx hy /Hf;, rewrite fgK_on //;, apply ] Tactics applied: 5492 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, 8 sec Results for lemma andKb: a b : a || b && a = a SUCCESS! Proof Found in EFSM: [by case a;, case b ] Tactics applied: 764 Original Proof: [by case: a; case: b.] Shorter Proof Found? no Proof reused from orb_idr 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: 804 Original Proof: [by case: a; case: b => // ->.] Shorter Proof Found? no Proof reused from orb_idr 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: 2206 Original Proof: [by split=> x; case: (hP x).] Shorter Proof Found? no Proof reused from all_and3 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: 52 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: 16675 Original Proof: [by move=> mf x y /=; rewrite -mf !fgK.] Proof search time: 0 min, 31 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 193 out of 240 lemmas. Success rate of 80.41666666666667% There were 0 errors. 47 proof attempts exhausted the automaton On average, a proof was found after applying 873 tactics The longest proof consisted of 6 tactics There were 18 shorter proofs found Of the 47 failures, 0 of them used all 100000 tactics There were 157 reused proofs found There were 36 novel proofs found Of the 47 failures, the average number of tactics used was 13315On average, a proof was found after 0 min, 1 sec On average, a failed proof attempt took 0 min, 17 sec On average, any (success or failure) proof attempt took 0 min, 4 sec The longest time to find a proof was 0 min, 13 sec The shortest time to find a proof was 0 min, 0 sec There were 0 proofs containing repeated tactics There were 0 proofs that repeated states