equal
deleted
inserted
replaced
231 |
231 |
232 lemma tm_comp_length: |
232 lemma tm_comp_length: |
233 shows "length (A |+| B) = length A + length B" |
233 shows "length (A |+| B) = length A + length B" |
234 by auto |
234 by auto |
235 |
235 |
|
236 lemma tm_comp_wf[intro]: |
|
237 "\<lbrakk>tm_wf (A, 0); tm_wf (B, 0)\<rbrakk> \<Longrightarrow> tm_wf (A |+| B, 0)" |
|
238 by (auto simp: tm_wf.simps shift.simps adjust.simps tm_comp_length tm_comp.simps) |
|
239 |
|
240 |
236 lemma tm_comp_step: |
241 lemma tm_comp_step: |
237 assumes unfinal: "\<not> is_final (step0 c A)" |
242 assumes unfinal: "\<not> is_final (step0 c A)" |
238 shows "step0 c (A |+| B) = step0 c A" |
243 shows "step0 c (A |+| B) = step0 c A" |
239 proof - |
244 proof - |
240 obtain s l r where eq: "c = (s, l, r)" by (metis is_final.cases) |
245 obtain s l r where eq: "c = (s, l, r)" by (metis is_final.cases) |