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

Theorem

bigops.bigop_Sfalse

Statement

∀ k p nil op f, (p k) = false ⇒ (bigop (k+1) (λi. p i) nil op (λi. f i)) = (bigop k (λi. p i) nil op (λi. f i))

Main Dependencies
Theory

Coq-Jumb
Statement

Theorem bigop_Sfalse : forall B, forall (k:nat.nat), forall (p:(nat.nat -> bool.bool)), forall (nil:B), forall (op:(B -> B -> B)), forall (f:(nat.nat -> B)), (logic.eq (bool.bool) (p k) bool.false) -> logic.eq (B) (bigop (B) (nat.S k) (fun (i:nat.nat) => p i) nil op (fun (i:nat.nat) => f i)) (bigop (B) k (fun (i:nat.nat) => p i) nil op (fun (i:nat.nat) => f i)).



Matita-Jumb
Statement

theorem bigop_Sfalse : \forall B. \forall (k:nat). \forall (p:nat -> bool). \forall (nil:B). \forall (op:B -> B -> B). \forall (f:nat -> B). ((eq) (bool) (p k) (false) ) -> (eq) (B) ((bigop) (B) ((S) k) (\lambda i : nat. p i) nil op (\lambda i : nat. f i)) ((bigop) (B) k (\lambda i : nat. p i) nil op (\lambda i : nat. f i)).



Lean-jumb
Statement

theorem bigop_Sfalse : forall (B : Type) , forall (k:nat.nat) , forall (p:(nat.nat) -> bool.bool) , forall (nil:B) , forall (op:(B) -> (B) -> B) , forall (f:(nat.nat) -> B) , ((((logic.eq_) (bool.bool)) ((p) (k))) ((bool.false) )) -> (((logic.eq_) (B)) (((((((bigops.bigop) (B)) (((nat.S) ) (k))) (fun (i : nat.nat) , (p) (i))) (nil)) (op)) (fun (i : nat.nat) , (f) (i)))) (((((((bigops.bigop) (B)) (k)) (fun (i : nat.nat) , (p) (i))) (nil)) (op)) (fun (i : nat.nat) , (f) (i))).



PVS-jumb

Statement

bigop_Sfalse [B:TYPE+] : LEMMA (FORALL(k:nat_sttfa_th.sttfa_nat):(FORALL(p:[nat_sttfa_th.sttfa_nat -> bool_sttfa_th.sttfa_bool]):(FORALL(nil:B):(FORALL(op:[B -> [B -> B]]):(FORALL(f:[nat_sttfa_th.sttfa_nat -> B]):(logic_sttfa_th.eq[bool_sttfa_th.sttfa_bool](p(k))(bool_sttfa_th.sttfa_false) => logic_sttfa_th.eq[B](bigops_sttfa.bigop[B](nat_sttfa_th.sttfa_S(k))((LAMBDA(i:nat_sttfa_th.sttfa_nat):p(i)))(nil)(op)((LAMBDA(i:nat_sttfa_th.sttfa_nat):f(i))))(bigops_sttfa.bigop[B](k)((LAMBDA(i:nat_sttfa_th.sttfa_nat):p(i)))(nil)(op)((LAMBDA(i:nat_sttfa_th.sttfa_nat):f(i))))))))))



OpenTheory

Printing for OpenTheory is not working at the moment.