∀ p f i n, i < n ⇒ (p i) = true ⇒ (bigop n (λx. p x) 1 times (λx. f x)) = ((f i) × (bigop n (λx. andb (notb (i = x)) (p x)) 1 times (λx. f x)))

Theorem bigop_diff : forall (p:(nat.nat -> bool.bool)), forall (f:(nat.nat -> nat.nat)), forall (i:nat.nat), forall (n:nat.nat), (nat.lt i n) -> (logic.eq (bool.bool) (p i) bool.true) -> logic.eq (nat.nat) (bigop (nat.nat) n (fun (x:nat.nat) => p x) (nat.S nat.O) nat.times (fun (x:nat.nat) => f x)) (nat.times (f i) (bigop (nat.nat) n (fun (x:nat.nat) => bool.andb (bool.notb (nat.eqb i x)) (p x)) (nat.S nat.O) nat.times (fun (x:nat.nat) => f x))).

theorem bigop_diff : \forall (p:nat -> bool). \forall (f:nat -> nat). \forall (i:nat). \forall (n:nat). ((lt) i n) -> ((eq) (bool) (p i) (true) ) -> (eq) (nat) ((bigop) (nat) n (\lambda x : nat. p x) ((S) (O) ) (times) (\lambda x : nat. f x)) ((times) (f i) ((bigop) (nat) n (\lambda x : nat. (andb) ((notb) ((eqb) i x)) (p x)) ((S) (O) ) (times) (\lambda x : nat. f x))).

theorem bigop_diff : forall (p:(nat.nat) -> bool.bool) , forall (f:(nat.nat) -> nat.nat) , forall (i:nat.nat) , forall (n:nat.nat) , ((((nat.lt_) ) (i)) (n)) -> ((((logic.eq_) (bool.bool)) ((p) (i))) ((bool.true) )) -> (((logic.eq_) (nat.nat)) (((((((bigops.bigop) (nat.nat)) (n)) (fun (x : nat.nat) , (p) (x))) (((nat.S) ) ((nat.O) ))) ((nat.times) )) (fun (x : nat.nat) , (f) (x)))) ((((nat.times) ) ((f) (i))) (((((((bigops.bigop) (nat.nat)) (n)) (fun (x : nat.nat) , (((bool.andb) ) (((bool.notb) ) ((((nat.eqb) ) (i)) (x)))) ((p) (x)))) (((nat.S) ) ((nat.O) ))) ((nat.times) )) (fun (x : nat.nat) , (f) (x)))).

bigop_diff : LEMMA (FORALL(p:[nat_sttfa_th.sttfa_nat -> bool_sttfa_th.sttfa_bool]):(FORALL(f:[nat_sttfa_th.sttfa_nat -> nat_sttfa_th.sttfa_nat]):(FORALL(i:nat_sttfa_th.sttfa_nat):(FORALL(n:nat_sttfa_th.sttfa_nat):(nat_sttfa_th.lt(i)(n) => (logic_sttfa_th.eq[bool_sttfa_th.sttfa_bool](p(i))(bool_sttfa_th.sttfa_true) => logic_sttfa_th.eq[nat_sttfa_th.sttfa_nat](bigops_sttfa.bigop[nat_sttfa_th.sttfa_nat](n)((LAMBDA(x:nat_sttfa_th.sttfa_nat):p(x)))(nat_sttfa_th.sttfa_S(nat_sttfa_th.sttfa_O))(nat_sttfa_th.times)((LAMBDA(x:nat_sttfa_th.sttfa_nat):f(x))))(nat_sttfa_th.times(f(i))(bigops_sttfa.bigop[nat_sttfa_th.sttfa_nat](n)((LAMBDA(x:nat_sttfa_th.sttfa_nat):bool_sttfa_th.andb(bool_sttfa_th.notb(nat_sttfa_th.eqb(i)(x)))(p(x))))(nat_sttfa_th.sttfa_S(nat_sttfa_th.sttfa_O))(nat_sttfa_th.times)((LAMBDA(x:nat_sttfa_th.sttfa_nat):f(x)))))))))))

Printing for OpenTheory is not working at the moment.