544 by arith

   544 by arith

   545 

   545 

   546 lemma compile_mod2: "length (concat (take n (tms_of ap))) mod 2 = 0"

   546 lemma compile_mod2: "length (concat (take n (tms_of ap))) mod 2 = 0"

   547 apply(induct n, auto)

   547 apply(induct n, auto)

   548 apply(case_tac "n < length (tms_of ap)", simp add: take_Suc_conv_app_nth, auto)

   548 apply(case_tac "n < length (tms_of ap)", simp add: take_Suc_conv_app_nth, auto)

   550 apply arith

   550 apply arith

   551 by auto

   551 by auto

   552 

   554 

   553 lemma tpa_states:

   555 lemma tpa_states:

   554   "\<lbrakk>tp = concat (take as (tms_of ap));

   556   "\<lbrakk>tp = concat (take as (tms_of ap));

   555   as \<le> length ap\<rbrakk> \<Longrightarrow> 

   557   as \<le> length ap\<rbrakk> \<Longrightarrow> 

   556   start_of (layout_of ap) as = Suc (length tp div 2)"

   558   start_of (layout_of ap) as = Suc (length tp div 2)"