equal
deleted
inserted
replaced
36 "plus m n p e = [Dec m 4, Inc n, Inc p, |
36 "plus m n p e = [Dec m 4, Inc n, Inc p, |
37 Goto 0, Dec p e, Inc m, Goto 4]" |
37 Goto 0, Dec p e, Inc m, Goto 4]" |
38 |
38 |
39 fun mult :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> abc_prog" |
39 fun mult :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> abc_prog" |
40 where |
40 where |
41 "mult m1 m2 n p e = [Dec m1 e]@ plus m1 m2 p 1" |
41 "mult m1 m2 n p e = [Dec m1 e]@ plus m2 n p 1" |
42 |
42 |
43 fun expo :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> abc_prog" |
43 fun expo :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> abc_prog" |
44 where |
44 where |
45 "expo n m1 m2 p e = [Inc n, Dec m1 e] @ mult m2 n n p 2" |
45 "expo n m1 m2 p e = [Inc n, Dec m1 e] @ mult m2 n n p 2" |
46 |
46 |