∀ n m q r return, r < m ⇒ n = ((q × m) + r) ⇒ return ⇒ div_mod_spec n m q r ⇒ return

Axiom match_div_mod_spec_prop : forall (n:nat.nat), forall (m:nat.nat), forall (q:nat.nat), forall (r:nat.nat), forall (return_:Prop), ((nat.lt r m) -> (logic.eq (nat.nat) n (nat.plus (nat.times q m) r)) -> return_) -> (div_mod_spec n m q r) -> return_

axiom match_div_mod_spec_prop : \forall (n:nat). \forall (m:nat). \forall (q:nat). \forall (r:nat). \forall (return_:Prop). (((lt) r m) -> ((eq) (nat) n ((plus) ((times) q m) r)) -> return_) -> ((div_mod_spec) n m q r) -> return_

axiom match_div_mod_spec_prop : forall (n:nat.nat) , forall (m:nat.nat) , forall (q:nat.nat) , forall (r:nat.nat) , forall (return:Prop) , (((((nat.lt_) ) (r)) (m)) -> ((((logic.eq_) (nat.nat)) (n)) ((((nat.plus) ) ((((nat.times) ) (q)) (m))) (r))) -> return) -> ((((((div_mod.div_mod_spec) ) (n)) (m)) (q)) (r)) -> return

match_div_mod_spec_prop : AXIOM (FORALL(n:nat_sttfa_th.sttfa_nat):(FORALL(m:nat_sttfa_th.sttfa_nat):(FORALL(q:nat_sttfa_th.sttfa_nat):(FORALL(r:nat_sttfa_th.sttfa_nat):(FORALL(return:bool):((nat_sttfa_th.lt(r)(m) => (logic_sttfa_th.eq[nat_sttfa_th.sttfa_nat](n)(nat_sttfa_th.plus(nat_sttfa_th.times(q)(m))(r)) => return)) => (div_mod_sttfa.div_mod_spec(n)(m)(q)(r) => return)))))))

Printing for OpenTheory is not working at the moment.