%% Arithmetic examples involving minus and quotient %% Author : Brigitte Pientka minus: nat -> nat -> nat -> type. %name minus M. %mode minus +X +Y -Z. m_z : minus X z X. m_s : minus (s X) (s Y) Z <- minus X Y Z. %terminates X (minus X Y _). %reduces Z <= X (minus X Y Z). quot : nat -> nat -> nat -> type. %name quot Q. %mode quot +X +Y -Z. q_z: quot z (s Y) z. q_s: quot (s X) (s Y) (s Z) <- minus X Y X' <- quot X' (s Y) Z. %terminates X (quot X Y Z).