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

Theorem

bigops.bigop_iso

Statement

∀ n1 n2 p1 p2 f1 f2, iso n1 n2 p1 p2 f1 f2 ⇒ (bigop n1 (λi. p1 i) 1 times (λi. f1 i)) = (bigop n2 (λi. p2 i) 1 times (λi. f2 i))

Main Dependencies
Theory
definition

Coq-Jumb
Statement

Theorem bigop_iso : forall (n1:nat.nat), forall (n2:nat.nat), forall (p1:(nat.nat -> bool.bool)), forall (p2:(nat.nat -> bool.bool)), forall (f1:(nat.nat -> nat.nat)), forall (f2:(nat.nat -> nat.nat)), (iso n1 n2 p1 p2 f1 f2) -> logic.eq (nat.nat) (bigop (nat.nat) n1 (fun (i:nat.nat) => p1 i) (nat.S nat.O) nat.times (fun (i:nat.nat) => f1 i)) (bigop (nat.nat) n2 (fun (i:nat.nat) => p2 i) (nat.S nat.O) nat.times (fun (i:nat.nat) => f2 i)).



Matita-Jumb
Statement

theorem bigop_iso : \forall (n1:nat). \forall (n2:nat). \forall (p1:nat -> bool). \forall (p2:nat -> bool). \forall (f1:nat -> nat). \forall (f2:nat -> nat). ((iso) n1 n2 p1 p2 f1 f2) -> (eq) (nat) ((bigop) (nat) n1 (\lambda i : nat. p1 i) ((S) (O) ) (times) (\lambda i : nat. f1 i)) ((bigop) (nat) n2 (\lambda i : nat. p2 i) ((S) (O) ) (times) (\lambda i : nat. f2 i)).



Lean-jumb
Statement

theorem bigop_iso : forall (n1:nat.nat) , forall (n2:nat.nat) , forall (p1:(nat.nat) -> bool.bool) , forall (p2:(nat.nat) -> bool.bool) , forall (f1:(nat.nat) -> nat.nat) , forall (f2:(nat.nat) -> nat.nat) , ((((((((bigops.iso) ) (n1)) (n2)) (p1)) (p2)) (f1)) (f2)) -> (((logic.eq_) (nat.nat)) (((((((bigops.bigop) (nat.nat)) (n1)) (fun (i : nat.nat) , (p1) (i))) (((nat.S) ) ((nat.O) ))) ((nat.times) )) (fun (i : nat.nat) , (f1) (i)))) (((((((bigops.bigop) (nat.nat)) (n2)) (fun (i : nat.nat) , (p2) (i))) (((nat.S) ) ((nat.O) ))) ((nat.times) )) (fun (i : nat.nat) , (f2) (i))).



PVS-jumb

Statement

bigop_iso : LEMMA (FORALL(n1:nat_sttfa_th.sttfa_nat):(FORALL(n2:nat_sttfa_th.sttfa_nat):(FORALL(p1:[nat_sttfa_th.sttfa_nat -> bool_sttfa_th.sttfa_bool]):(FORALL(p2:[nat_sttfa_th.sttfa_nat -> bool_sttfa_th.sttfa_bool]):(FORALL(f1:[nat_sttfa_th.sttfa_nat -> nat_sttfa_th.sttfa_nat]):(FORALL(f2:[nat_sttfa_th.sttfa_nat -> nat_sttfa_th.sttfa_nat]):(bigops_sttfa.iso(n1)(n2)(p1)(p2)(f1)(f2) => logic_sttfa_th.eq[nat_sttfa_th.sttfa_nat](bigops_sttfa.bigop[nat_sttfa_th.sttfa_nat](n1)((LAMBDA(i:nat_sttfa_th.sttfa_nat):p1(i)))(nat_sttfa_th.sttfa_S(nat_sttfa_th.sttfa_O))(nat_sttfa_th.times)((LAMBDA(i:nat_sttfa_th.sttfa_nat):f1(i))))(bigops_sttfa.bigop[nat_sttfa_th.sttfa_nat](n2)((LAMBDA(i:nat_sttfa_th.sttfa_nat):p2(i)))(nat_sttfa_th.sttfa_S(nat_sttfa_th.sttfa_O))(nat_sttfa_th.times)((LAMBDA(i:nat_sttfa_th.sttfa_nat):f2(i)))))))))))



OpenTheory

Printing for OpenTheory is not working at the moment.