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

Theorem

bigops.bigop_false

Statement

∀ n nil op f, (bigop n (λi. false) nil op (λi. f i)) = nil

Main Dependencies
Theory

Coq-Jumb
Statement

Theorem bigop_false : forall B, forall (n:nat.nat), forall (nil:B), forall (op:(B -> B -> B)), forall (f:(nat.nat -> B)), logic.eq (B) (bigop (B) n (fun (i:nat.nat) => bool.false) nil op (fun (i:nat.nat) => f i)) nil.



Matita-Jumb
Statement

theorem bigop_false : \forall B. \forall (n:nat). \forall (nil:B). \forall (op:B -> B -> B). \forall (f:nat -> B). (eq) (B) ((bigop) (B) n (\lambda i : nat. (false) ) nil op (\lambda i : nat. f i)) nil.



Lean-jumb
Statement

theorem bigop_false : forall (B : Type) , forall (n:nat.nat) , forall (nil:B) , forall (op:(B) -> (B) -> B) , forall (f:(nat.nat) -> B) , (((logic.eq_) (B)) (((((((bigops.bigop) (B)) (n)) (fun (i : nat.nat) , (bool.false) )) (nil)) (op)) (fun (i : nat.nat) , (f) (i)))) (nil).



PVS-jumb

Statement

bigop_false [B:TYPE+] : LEMMA (FORALL(n:nat_sttfa_th.sttfa_nat):(FORALL(nil:B):(FORALL(op:[B -> [B -> B]]):(FORALL(f:[nat_sttfa_th.sttfa_nat -> B]):logic_sttfa_th.eq[B](bigops_sttfa.bigop[B](n)((LAMBDA(i:nat_sttfa_th.sttfa_nat):bool_sttfa_th.sttfa_false))(nil)(op)((LAMBDA(i:nat_sttfa_th.sttfa_nat):f(i))))(nil)))))



OpenTheory

Printing for OpenTheory is not working at the moment.