nat.nat → nat.nat → nat.nat → nat.nat → ℙ

Parameter div_mod_spec : nat.nat -> nat.nat -> nat.nat -> nat.nat -> Prop

axiom div_mod_spec : nat -> nat -> nat -> nat -> Prop

constant div_mod_spec : (nat.nat) -> (nat.nat) -> (nat.nat) -> (nat.nat) -> Prop

div_mod_spec : [nat_sttfa_th.sttfa_nat -> [nat_sttfa_th.sttfa_nat -> [nat_sttfa_th.sttfa_nat -> [nat_sttfa_th.sttfa_nat -> bool]]]]

Printing for OpenTheory is not working at the moment.