equal
deleted
inserted
replaced
161 and "layout_of ((Inc R\<iota>)#is) = (2 * R\<iota> + 9)#(layout_of is)" |
161 and "layout_of ((Inc R\<iota>)#is) = (2 * R\<iota> + 9)#(layout_of is)" |
162 and "layout_of ((Dec R\<iota> l)#is) = (2 * R\<iota> + 16)#(layout_of is)" |
162 and "layout_of ((Dec R\<iota> l)#is) = (2 * R\<iota> + 16)#(layout_of is)" |
163 and "layout_of ((Goto l)#is) = 1#(layout_of is)" |
163 and "layout_of ((Goto l)#is) = 1#(layout_of is)" |
164 by(auto simp add: layout_of.simps length_of.simps) |
164 by(auto simp add: layout_of.simps length_of.simps) |
165 |
165 |
166 |
166 fun clear :: "nat \<Rightarrow> nat \<Rightarrow> abc_prog" |
|
167 where |
|
168 "clear n e = [Dec n e, Goto 0]" |
167 (*>*) |
169 (*>*) |
168 |
170 |
169 section {* Introduction *} |
171 section {* Introduction *} |
170 |
172 |
171 |
173 |