237 using final

   237 using final

   238 apply(case_tac "A = []")

   238 apply(case_tac "A = []")

   239 apply(rule_tac x = 0 in exI, simp add: abc_steps_l.simps abc_exec_null)

   239 apply(rule_tac x = 0 in exI, simp add: abc_steps_l.simps abc_exec_null)

   240 apply(rule_tac abc_comp_frist_steps_halt_eq', simp_all)

   240 apply(rule_tac abc_comp_frist_steps_halt_eq', simp_all)

   241 done

   241 done

   242 

   243 

   243 lemma abc_comp_second_step_eq: 

   244 lemma abc_comp_second_step_eq: 

   244   assumes exec: "abc_step_l (s, lm) (abc_fetch s B) = (sa, lma)"

   245   assumes exec: "abc_step_l (s, lm) (abc_fetch s B) = (sa, lma)"

   245   shows "abc_step_l (s + length A, lm) (abc_fetch (s + length A) (A [+] B))

   246   shows "abc_step_l (s + length A, lm) (abc_fetch (s + length A) (A [+] B))

   246          = (sa + length A, lma)"

   247          = (sa + length A, lma)"