%% Arithmetic examples involving subtraction and gcd %% Author : Brigitte Pientka sub: nat -> nat -> nat -> type. %name sub S. %mode sub +X +Y -Z. s_z1 : sub X z X. % s_z2 : sub z Y z. s_ss : sub (s X) (s Y) Z <- sub X Y Z. %terminates X (sub X Y _). %reduces Z <= X (sub X Y Z). rminus: nat -> nat -> nat -> type. %name rminus M. %mode rminus +X +Y -Z. rmin : rminus (s X) (s Y) Z <- sub X Y Z. %terminates [X Y] (rminus X Y _). %reduces Z < X (rminus X Y Z). less: nat -> nat -> bool -> type. %name less L. %mode less +X +Y -Z. l_z1 : less z (s X) true. l_z2 : less X z false. l_ss : less (s X) (s Y) B <- less X Y B. %terminates X (less X Y _). gcd: nat -> nat -> nat -> type. %name gcd G. %mode gcd +X +Y -Z. gcd_z1: gcd z Y Y. gcd_z2: gcd X z X. gcd_s1: gcd (s X) (s Y) Z <- less (s X) (s Y) true <- rminus (s Y) (s X) Y' <- gcd (s X) Y' Z. gcd_s1: gcd (s X) (s Y) Z <- less (s X)(s Y) false <- rminus (s X) (s Y) X' <- gcd X' (s Y) Z. %terminates [X Y] (gcd X Y _). %terminates {X Y} (gcd X Y Z).