// This prints the left floatting menu
Dedukti    Load Matita      Load Coq         Load Lean        Load PVS         Load OpenTheory Load
Dedukti-jumb

Theorem

sigma_pi.exp_pi_bc

Statement

∀ a b c f, ((a ^ (c - b)) × (bigop (c - b) (λi. true) 1 times (λi. f (i + b)))) = (bigop (c - b) (λi. true) 1 times (λi. a × (f (i + b))))

Main Dependencies
Theory

Coq-Jumb
Statement

Theorem exp_pi_bc : forall (a:nat.nat), forall (b:nat.nat), forall (c:nat.nat), forall (f:(nat.nat -> nat.nat)), logic.eq (nat.nat) (nat.times (exp.exp a (nat.minus c b)) (bigops.bigop (nat.nat) (nat.minus c b) (fun (i:nat.nat) => bool.true) (nat.S nat.O) nat.times (fun (i:nat.nat) => f (nat.plus i b)))) (bigops.bigop (nat.nat) (nat.minus c b) (fun (i:nat.nat) => bool.true) (nat.S nat.O) nat.times (fun (i:nat.nat) => nat.times a (f (nat.plus i b)))).



Matita-Jumb
Statement

theorem exp_pi_bc : \forall (a:nat). \forall (b:nat). \forall (c:nat). \forall (f:nat -> nat). (eq) (nat) ((times) ((exp) a ((minus) c b)) ((bigop) (nat) ((minus) c b) (\lambda i : nat. (true) ) ((S) (O) ) (times) (\lambda i : nat. f ((plus) i b)))) ((bigop) (nat) ((minus) c b) (\lambda i : nat. (true) ) ((S) (O) ) (times) (\lambda i : nat. (times) a (f ((plus) i b)))).



Lean-jumb
Statement

theorem exp_pi_bc : forall (a:nat.nat) , forall (b:nat.nat) , forall (c:nat.nat) , forall (f:(nat.nat) -> nat.nat) , (((logic.eq_) (nat.nat)) ((((nat.times) ) ((((exp.exp) ) (a)) ((((nat.minus) ) (c)) (b)))) (((((((bigops.bigop) (nat.nat)) ((((nat.minus) ) (c)) (b))) (fun (i : nat.nat) , (bool.true) )) (((nat.S) ) ((nat.O) ))) ((nat.times) )) (fun (i : nat.nat) , (f) ((((nat.plus) ) (i)) (b)))))) (((((((bigops.bigop) (nat.nat)) ((((nat.minus) ) (c)) (b))) (fun (i : nat.nat) , (bool.true) )) (((nat.S) ) ((nat.O) ))) ((nat.times) )) (fun (i : nat.nat) , (((nat.times) ) (a)) ((f) ((((nat.plus) ) (i)) (b))))).



PVS-jumb

Statement

exp_pi_bc : LEMMA (FORALL(a:nat_sttfa_th.sttfa_nat):(FORALL(b:nat_sttfa_th.sttfa_nat):(FORALL(c:nat_sttfa_th.sttfa_nat):(FORALL(f:[nat_sttfa_th.sttfa_nat -> nat_sttfa_th.sttfa_nat]):logic_sttfa_th.eq[nat_sttfa_th.sttfa_nat](nat_sttfa_th.times(exp_sttfa_th.sttfa_exp(a)(nat_sttfa_th.minus(c)(b)))(bigops_sttfa_th.bigop[nat_sttfa_th.sttfa_nat](nat_sttfa_th.minus(c)(b))((LAMBDA(i:nat_sttfa_th.sttfa_nat):bool_sttfa_th.sttfa_true))(nat_sttfa_th.sttfa_S(nat_sttfa_th.sttfa_O))(nat_sttfa_th.times)((LAMBDA(i:nat_sttfa_th.sttfa_nat):f(nat_sttfa_th.plus(i)(b))))))(bigops_sttfa_th.bigop[nat_sttfa_th.sttfa_nat](nat_sttfa_th.minus(c)(b))((LAMBDA(i:nat_sttfa_th.sttfa_nat):bool_sttfa_th.sttfa_true))(nat_sttfa_th.sttfa_S(nat_sttfa_th.sttfa_O))(nat_sttfa_th.times)((LAMBDA(i:nat_sttfa_th.sttfa_nat):nat_sttfa_th.times(a)(f(nat_sttfa_th.plus(i)(b))))))))))



OpenTheory

Printing for OpenTheory is not working at the moment.