21 

    22 section {* Some Sample Abacus programs *}

    23 

    24 (* Abacus for addition and clearance *)

    25 fun plus_clear :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> abc_prog"  

    26   where

    27   "plus_clear m n e = [Dec m e, Inc n, Goto 0]"

    28 

    29 (* Abacus for clearing memory untis *)

    30 fun clear :: "nat \<Rightarrow> nat \<Rightarrow> abc_prog"

    31   where

    32   "clear n e = [Dec n e, Goto 0]"

    33 

    34 fun plus:: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> abc_prog"

    35   where

    36   "plus m n p e = [Dec m 4, Inc n, Inc p,

    37                    Goto 0, Dec p e, Inc m, Goto 4]"

    38 

    39 fun mult :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> abc_prog"

    40   where

    41   "mult m1 m2 n p e = [Dec m1 e]@ plus m2 n p 1"

    42 

    43 fun expo :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> abc_prog"

    44   where

    45   "expo n m1 m2 p e = [Inc n, Dec m1 e] @ mult m2 n n p 2"