inductive divmod_rel :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool" where

 inductive divmod_rel :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool" where

     "k < l \<Longrightarrow> divmod_rel k l 0 k"

     "k < l \<Longrightarrow> divmod_rel k l 0 k"

   | "k \<ge> l \<Longrightarrow> divmod_rel (k - l) l q r \<Longrightarrow> divmod_rel k l (Suc q) r"

   | "k \<ge> l \<Longrightarrow> divmod_rel (k - l) l q r \<Longrightarrow> divmod_rel k l (Suc q) r"

 thm divmod_rel.equation

 thm divmod_rel.equation

 value [code] "Predicate.the (divmod_rel_i_i_o_o 1705 42)"

 value [code] "Predicate.the (divmod_rel_i_i_o_o 1705 42)"

 subsection {* Transforming predicate logic into logic programs *}

 subsection {* Transforming predicate logic into logic programs *}