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

Axiom

nat.axiom_filter_nat_type_S

Statement

∀ return n, equal (filter_nat_type return (n+1)) (return (n+1))

Main Dependencies
Theory

Coq-Jumb
Statement

Axiom axiom_filter_nat_type_S : forall return_type, forall (return_:(nat -> return_type)), forall (n:nat), connectives.equal (return_type) (filter_nat_type (return_type) return_ (S n)) (return_ (S n))



Matita-Jumb
Statement

axiom axiom_filter_nat_type_S : \forall return_type. \forall (return_:nat -> return_type). \forall (n:nat). (equal) (return_type) ((filter_nat_type) (return_type) return_ ((S) n)) (return_ ((S) n))



Lean-jumb
Statement

axiom axiom_filter_nat_type_S : forall (return_type : Type) , forall (return:(nat.nat) -> return_type) , forall (n:nat.nat) , (((connectives.equal) (return_type)) ((((nat.filter_nat_type) (return_type)) (return)) (((nat.S) ) (n)))) ((return) (((nat.S) ) (n)))



PVS-jumb

Statement

axiom_filter_nat_type_S [return_type:TYPE+] : AXIOM (FORALL(return:[nat_sttfa.sttfa_nat -> return_type]):(FORALL(n:nat_sttfa.sttfa_nat):connectives_sttfa_th.equal[return_type](nat_sttfa.filter_nat_type[return_type](return)(nat_sttfa.sttfa_S(n)))(return(nat_sttfa.sttfa_S(n)))))



OpenTheory

Printing for OpenTheory is not working at the moment.