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

Axiom

bigops.axiom_bigop_body_S

Statement

∀ n, equal (bigop_body (n+1)) (λp. λnil. λop. λf. if (p n) then (op (f n) (bigop n p nil op f)) else (bigop n p nil op f))

Main Dependencies
Theory

Coq-Jumb
Statement

Axiom axiom_bigop_body_S : forall H, forall (n:nat.nat), connectives.equal ((nat.nat -> bool.bool) -> H -> (H -> H -> H) -> (nat.nat -> H) -> H) (bigop_body (H) (nat.S n)) (fun (p:(nat.nat -> bool.bool)) => fun (nil:H) => fun (op:(H -> H -> H)) => fun (f:(nat.nat -> H)) => bool.match_bool_type (H) (op (f n) (bigop (H) n p nil op f)) (bigop (H) n p nil op f) (p n))



Matita-Jumb
Statement

axiom axiom_bigop_body_S : \forall H. \forall (n:nat). (equal) ((nat -> bool) -> H -> (H -> H -> H) -> (nat -> H) -> H) ((bigop_body) (H) ((S) n)) (\lambda p : nat -> bool. \lambda nil : H. \lambda op : H -> H -> H. \lambda f : nat -> H. (match_bool_type) (H) (op (f n) ((bigop) (H) n p nil op f)) ((bigop) (H) n p nil op f) (p n))



Lean-jumb
Statement

axiom axiom_bigop_body_S : forall (H : Type) , forall (n:nat.nat) , (((connectives.equal) (((nat.nat) -> bool.bool) -> (H) -> ((H) -> (H) -> H) -> ((nat.nat) -> H) -> H)) (((bigops.bigop_body) (H)) (((nat.S) ) (n)))) (fun (p : (nat.nat) -> bool.bool) , fun (nil : H) , fun (op : (H) -> (H) -> H) , fun (f : (nat.nat) -> H) , ((((bool.match_bool_type) (H)) (((op) ((f) (n))) (((((((bigops.bigop) (H)) (n)) (p)) (nil)) (op)) (f)))) (((((((bigops.bigop) (H)) (n)) (p)) (nil)) (op)) (f))) ((p) (n)))



PVS-jumb

Statement

axiom_bigop_body_S [H:TYPE+] : AXIOM (FORALL(n:nat_sttfa_th.sttfa_nat):connectives_sttfa_th.equal[[[nat_sttfa_th.sttfa_nat -> bool_sttfa_th.sttfa_bool] -> [H -> [[H -> [H -> H]] -> [[nat_sttfa_th.sttfa_nat -> H] -> H]]]]](bigops_sttfa.bigop_body[H](nat_sttfa_th.sttfa_S(n)))((LAMBDA(p:[nat_sttfa_th.sttfa_nat -> bool_sttfa_th.sttfa_bool]):(LAMBDA(nil:H):(LAMBDA(op:[H -> [H -> H]]):(LAMBDA(f:[nat_sttfa_th.sttfa_nat -> H]):bool_sttfa_th.match_bool_type[H](op(f(n))(bigops_sttfa.bigop[H](n)(p)(nil)(op)(f)))(bigops_sttfa.bigop[H](n)(p)(nil)(op)(f))(p(n))))))))



OpenTheory

Printing for OpenTheory is not working at the moment.