[STATEMENT]
lemma f_Exec_Stream_Acc_LocalState__State_Idle_nth[rule_format]: "
  \<And>c i.
  \<lbrakk> 0 < l; l \<le> k; Exec_Equal_State localState trans_fun;
    \<forall>n\<le>i. State_Idle localState output_fun trans_fun (
      f_Exec_Comp_Stream_Acc_LocalState l localState trans_fun xs c ! n);
    i < length xs \<rbrakk> \<Longrightarrow>
  f_Exec_Comp_Stream_Acc_LocalState k localState trans_fun xs c ! i =
  f_Exec_Comp_Stream_Acc_LocalState l localState trans_fun xs c ! i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>c i. \<lbrakk>0 < l; l \<le> k; Exec_Equal_State localState trans_fun; \<forall>n\<le>i. State_Idle localState output_fun trans_fun (f_Exec_Comp_Stream_Acc_LocalState l localState trans_fun xs c ! n); i < length xs\<rbrakk> \<Longrightarrow> f_Exec_Comp_Stream_Acc_LocalState k localState trans_fun xs c ! i = f_Exec_Comp_Stream_Acc_LocalState l localState trans_fun xs c ! i
[PROOF STEP]
apply (frule length_greater_0_conv[THEN iffD1, OF gr_implies_gr0])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>c i. \<lbrakk>0 < l; l \<le> k; Exec_Equal_State localState trans_fun; \<forall>n\<le>i. State_Idle localState output_fun trans_fun (f_Exec_Comp_Stream_Acc_LocalState l localState trans_fun xs c ! n); i < length xs; xs \<noteq> []\<rbrakk> \<Longrightarrow> f_Exec_Comp_Stream_Acc_LocalState k localState trans_fun xs c ! i = f_Exec_Comp_Stream_Acc_LocalState l localState trans_fun xs c ! i
[PROOF STEP]
apply (simp only: f_Exec_Stream_Acc_LocalState_nth take_Suc_conv_app_nth)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>c i. \<lbrakk>0 < l; l \<le> k; Exec_Equal_State localState trans_fun; \<forall>n\<le>i. State_Idle localState output_fun trans_fun (f_Exec_Comp_Stream_Acc_LocalState l localState trans_fun xs c ! n); i < length xs; xs \<noteq> []\<rbrakk> \<Longrightarrow> localState (f_Exec_Comp trans_fun ((xs \<down> i @ [xs ! i]) \<odot> k) c) = localState (f_Exec_Comp trans_fun ((xs \<down> i @ [xs ! i]) \<odot> l) c)
[PROOF STEP]
apply (simp only: f_expand_snoc f_Exec_append)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>c i. \<lbrakk>0 < l; l \<le> k; Exec_Equal_State localState trans_fun; \<forall>n\<le>i. State_Idle localState output_fun trans_fun (f_Exec_Comp_Stream_Acc_LocalState l localState trans_fun xs c ! n); i < length xs; xs \<noteq> []\<rbrakk> \<Longrightarrow> localState (f_Exec_Comp trans_fun (xs ! i # NoMsg\<^bsup>k - Suc 0\<^esup>) (f_Exec_Comp trans_fun (xs \<down> i \<odot> k) c)) = localState (f_Exec_Comp trans_fun (xs ! i # NoMsg\<^bsup>l - Suc 0\<^esup>) (f_Exec_Comp trans_fun (xs \<down> i \<odot> l) c))
[PROOF STEP]
apply (rule_tac s="\<NoMsg>\<^bsup>l - Suc 0\<^esup> @ \<NoMsg>\<^bsup>k-l\<^esup>" and t="\<NoMsg>\<^bsup>k - Suc 0\<^esup>" in subst)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>c i. \<lbrakk>0 < l; l \<le> k; Exec_Equal_State localState trans_fun; \<forall>n\<le>i. State_Idle localState output_fun trans_fun (f_Exec_Comp_Stream_Acc_LocalState l localState trans_fun xs c ! n); i < length xs; xs \<noteq> []\<rbrakk> \<Longrightarrow> NoMsg\<^bsup>l - Suc 0\<^esup> @ NoMsg\<^bsup>k - l\<^esup> = NoMsg\<^bsup>k - Suc 0\<^esup>
 2. \<And>c i. \<lbrakk>0 < l; l \<le> k; Exec_Equal_State localState trans_fun; \<forall>n\<le>i. State_Idle localState output_fun trans_fun (f_Exec_Comp_Stream_Acc_LocalState l localState trans_fun xs c ! n); i < length xs; xs \<noteq> []\<rbrakk> \<Longrightarrow> localState (f_Exec_Comp trans_fun (xs ! i # NoMsg\<^bsup>l - Suc 0\<^esup> @ NoMsg\<^bsup>k - l\<^esup>) (f_Exec_Comp trans_fun (xs \<down> i \<odot> k) c)) = localState (f_Exec_Comp trans_fun (xs ! i # NoMsg\<^bsup>l - Suc 0\<^esup>) (f_Exec_Comp trans_fun (xs \<down> i \<odot> l) c))
[PROOF STEP]
apply (simp add: replicate_le_diff2)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>c i. \<lbrakk>0 < l; l \<le> k; Exec_Equal_State localState trans_fun; \<forall>n\<le>i. State_Idle localState output_fun trans_fun (f_Exec_Comp_Stream_Acc_LocalState l localState trans_fun xs c ! n); i < length xs; xs \<noteq> []\<rbrakk> \<Longrightarrow> localState (f_Exec_Comp trans_fun (xs ! i # NoMsg\<^bsup>l - Suc 0\<^esup> @ NoMsg\<^bsup>k - l\<^esup>) (f_Exec_Comp trans_fun (xs \<down> i \<odot> k) c)) = localState (f_Exec_Comp trans_fun (xs ! i # NoMsg\<^bsup>l - Suc 0\<^esup>) (f_Exec_Comp trans_fun (xs \<down> i \<odot> l) c))
[PROOF STEP]
apply (subst append_Cons[symmetric])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>c i. \<lbrakk>0 < l; l \<le> k; Exec_Equal_State localState trans_fun; \<forall>n\<le>i. State_Idle localState output_fun trans_fun (f_Exec_Comp_Stream_Acc_LocalState l localState trans_fun xs c ! n); i < length xs; xs \<noteq> []\<rbrakk> \<Longrightarrow> localState (f_Exec_Comp trans_fun ((xs ! i # NoMsg\<^bsup>l - Suc 0\<^esup>) @ NoMsg\<^bsup>k - l\<^esup>) (f_Exec_Comp trans_fun (xs \<down> i \<odot> k) c)) = localState (f_Exec_Comp trans_fun (xs ! i # NoMsg\<^bsup>l - Suc 0\<^esup>) (f_Exec_Comp trans_fun (xs \<down> i \<odot> l) c))
[PROOF STEP]
apply (induct xs, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a xs c i. \<lbrakk>\<And>c i. \<lbrakk>0 < l; l \<le> k; Exec_Equal_State localState trans_fun; \<forall>n\<le>i. State_Idle localState output_fun trans_fun (f_Exec_Comp_Stream_Acc_LocalState l localState trans_fun xs c ! n); i < length xs; xs \<noteq> []\<rbrakk> \<Longrightarrow> localState (f_Exec_Comp trans_fun ((xs ! i # NoMsg\<^bsup>l - Suc 0\<^esup>) @ NoMsg\<^bsup>k - l\<^esup>) (f_Exec_Comp trans_fun (xs \<down> i \<odot> k) c)) = localState (f_Exec_Comp trans_fun (xs ! i # NoMsg\<^bsup>l - Suc 0\<^esup>) (f_Exec_Comp trans_fun (xs \<down> i \<odot> l) c)); 0 < l; l \<le> k; Exec_Equal_State localState trans_fun; \<forall>n\<le>i. State_Idle localState output_fun trans_fun (f_Exec_Comp_Stream_Acc_LocalState l localState trans_fun (a # xs) c ! n); i < length (a # xs); a # xs \<noteq> []\<rbrakk> \<Longrightarrow> localState (f_Exec_Comp trans_fun (((a # xs) ! i # NoMsg\<^bsup>l - Suc 0\<^esup>) @ NoMsg\<^bsup>k - l\<^esup>) (f_Exec_Comp trans_fun ((a # xs) \<down> i \<odot> k) c)) = localState (f_Exec_Comp trans_fun ((a # xs) ! i # NoMsg\<^bsup>l - Suc 0\<^esup>) (f_Exec_Comp trans_fun ((a # xs) \<down> i \<odot> l) c))
[PROOF STEP]
apply (case_tac i)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a xs c i. \<lbrakk>\<And>c i. \<lbrakk>0 < l; l \<le> k; Exec_Equal_State localState trans_fun; \<forall>n\<le>i. State_Idle localState output_fun trans_fun (f_Exec_Comp_Stream_Acc_LocalState l localState trans_fun xs c ! n); i < length xs; xs \<noteq> []\<rbrakk> \<Longrightarrow> localState (f_Exec_Comp trans_fun ((xs ! i # NoMsg\<^bsup>l - Suc 0\<^esup>) @ NoMsg\<^bsup>k - l\<^esup>) (f_Exec_Comp trans_fun (xs \<down> i \<odot> k) c)) = localState (f_Exec_Comp trans_fun (xs ! i # NoMsg\<^bsup>l - Suc 0\<^esup>) (f_Exec_Comp trans_fun (xs \<down> i \<odot> l) c)); 0 < l; l \<le> k; Exec_Equal_State localState trans_fun; \<forall>n\<le>i. State_Idle localState output_fun trans_fun (f_Exec_Comp_Stream_Acc_LocalState l localState trans_fun (a # xs) c ! n); i < length (a # xs); a # xs \<noteq> []; i = 0\<rbrakk> \<Longrightarrow> localState (f_Exec_Comp trans_fun (((a # xs) ! i # NoMsg\<^bsup>l - Suc 0\<^esup>) @ NoMsg\<^bsup>k - l\<^esup>) (f_Exec_Comp trans_fun ((a # xs) \<down> i \<odot> k) c)) = localState (f_Exec_Comp trans_fun ((a # xs) ! i # NoMsg\<^bsup>l - Suc 0\<^esup>) (f_Exec_Comp trans_fun ((a # xs) \<down> i \<odot> l) c))
 2. \<And>a xs c i nat. \<lbrakk>\<And>c i. \<lbrakk>0 < l; l \<le> k; Exec_Equal_State localState trans_fun; \<forall>n\<le>i. State_Idle localState output_fun trans_fun (f_Exec_Comp_Stream_Acc_LocalState l localState trans_fun xs c ! n); i < length xs; xs \<noteq> []\<rbrakk> \<Longrightarrow> localState (f_Exec_Comp trans_fun ((xs ! i # NoMsg\<^bsup>l - Suc 0\<^esup>) @ NoMsg\<^bsup>k - l\<^esup>) (f_Exec_Comp trans_fun (xs \<down> i \<odot> k) c)) = localState (f_Exec_Comp trans_fun (xs ! i # NoMsg\<^bsup>l - Suc 0\<^esup>) (f_Exec_Comp trans_fun (xs \<down> i \<odot> l) c)); 0 < l; l \<le> k; Exec_Equal_State localState trans_fun; \<forall>n\<le>i. State_Idle localState output_fun trans_fun (f_Exec_Comp_Stream_Acc_LocalState l localState trans_fun (a # xs) c ! n); i < length (a # xs); a # xs \<noteq> []; i = Suc nat\<rbrakk> \<Longrightarrow> localState (f_Exec_Comp trans_fun (((a # xs) ! i # NoMsg\<^bsup>l - Suc 0\<^esup>) @ NoMsg\<^bsup>k - l\<^esup>) (f_Exec_Comp trans_fun ((a # xs) \<down> i \<odot> k) c)) = localState (f_Exec_Comp trans_fun ((a # xs) ! i # NoMsg\<^bsup>l - Suc 0\<^esup>) (f_Exec_Comp trans_fun ((a # xs) \<down> i \<odot> l) c))
[PROOF STEP]
apply (simp add: f_Exec_Stream_Acc_LocalState_Cons f_Exec_State_Idle_append_replicate_NoMsg_state)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a xs c i nat. \<lbrakk>\<And>c i. \<lbrakk>0 < l; l \<le> k; Exec_Equal_State localState trans_fun; \<forall>n\<le>i. State_Idle localState output_fun trans_fun (f_Exec_Comp_Stream_Acc_LocalState l localState trans_fun xs c ! n); i < length xs; xs \<noteq> []\<rbrakk> \<Longrightarrow> localState (f_Exec_Comp trans_fun ((xs ! i # NoMsg\<^bsup>l - Suc 0\<^esup>) @ NoMsg\<^bsup>k - l\<^esup>) (f_Exec_Comp trans_fun (xs \<down> i \<odot> k) c)) = localState (f_Exec_Comp trans_fun (xs ! i # NoMsg\<^bsup>l - Suc 0\<^esup>) (f_Exec_Comp trans_fun (xs \<down> i \<odot> l) c)); 0 < l; l \<le> k; Exec_Equal_State localState trans_fun; \<forall>n\<le>i. State_Idle localState output_fun trans_fun (f_Exec_Comp_Stream_Acc_LocalState l localState trans_fun (a # xs) c ! n); i < length (a # xs); a # xs \<noteq> []; i = Suc nat\<rbrakk> \<Longrightarrow> localState (f_Exec_Comp trans_fun (((a # xs) ! i # NoMsg\<^bsup>l - Suc 0\<^esup>) @ NoMsg\<^bsup>k - l\<^esup>) (f_Exec_Comp trans_fun ((a # xs) \<down> i \<odot> k) c)) = localState (f_Exec_Comp trans_fun ((a # xs) ! i # NoMsg\<^bsup>l - Suc 0\<^esup>) (f_Exec_Comp trans_fun ((a # xs) \<down> i \<odot> l) c))
[PROOF STEP]
apply (rename_tac n)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a xs c i n. \<lbrakk>\<And>c i. \<lbrakk>0 < l; l \<le> k; Exec_Equal_State localState trans_fun; \<forall>n\<le>i. State_Idle localState output_fun trans_fun (f_Exec_Comp_Stream_Acc_LocalState l localState trans_fun xs c ! n); i < length xs; xs \<noteq> []\<rbrakk> \<Longrightarrow> localState (f_Exec_Comp trans_fun ((xs ! i # NoMsg\<^bsup>l - Suc 0\<^esup>) @ NoMsg\<^bsup>k - l\<^esup>) (f_Exec_Comp trans_fun (xs \<down> i \<odot> k) c)) = localState (f_Exec_Comp trans_fun (xs ! i # NoMsg\<^bsup>l - Suc 0\<^esup>) (f_Exec_Comp trans_fun (xs \<down> i \<odot> l) c)); 0 < l; l \<le> k; Exec_Equal_State localState trans_fun; \<forall>n\<le>i. State_Idle localState output_fun trans_fun (f_Exec_Comp_Stream_Acc_LocalState l localState trans_fun (a # xs) c ! n); i < length (a # xs); a # xs \<noteq> []; i = Suc n\<rbrakk> \<Longrightarrow> localState (f_Exec_Comp trans_fun (((a # xs) ! i # NoMsg\<^bsup>l - Suc 0\<^esup>) @ NoMsg\<^bsup>k - l\<^esup>) (f_Exec_Comp trans_fun ((a # xs) \<down> i \<odot> k) c)) = localState (f_Exec_Comp trans_fun ((a # xs) ! i # NoMsg\<^bsup>l - Suc 0\<^esup>) (f_Exec_Comp trans_fun ((a # xs) \<down> i \<odot> l) c))
[PROOF STEP]
apply (drule_tac x="f_Exec_Comp trans_fun (a # \<NoMsg>\<^bsup>l - Suc 0\<^esup>) c" in meta_spec)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a xs c i n. \<lbrakk>0 < l; l \<le> k; Exec_Equal_State localState trans_fun; \<forall>n\<le>i. State_Idle localState output_fun trans_fun (f_Exec_Comp_Stream_Acc_LocalState l localState trans_fun (a # xs) c ! n); i < length (a # xs); a # xs \<noteq> []; i = Suc n; \<And>i. \<lbrakk>0 < l; l \<le> k; Exec_Equal_State localState trans_fun; \<forall>n\<le>i. State_Idle localState output_fun trans_fun (f_Exec_Comp_Stream_Acc_LocalState l localState trans_fun xs (f_Exec_Comp trans_fun (a # NoMsg\<^bsup>l - Suc 0\<^esup>) c) ! n); i < length xs; xs \<noteq> []\<rbrakk> \<Longrightarrow> localState (f_Exec_Comp trans_fun ((xs ! i # NoMsg\<^bsup>l - Suc 0\<^esup>) @ NoMsg\<^bsup>k - l\<^esup>) (f_Exec_Comp trans_fun (xs \<down> i \<odot> k) (f_Exec_Comp trans_fun (a # NoMsg\<^bsup>l - Suc 0\<^esup>) c))) = localState (f_Exec_Comp trans_fun (xs ! i # NoMsg\<^bsup>l - Suc 0\<^esup>) (f_Exec_Comp trans_fun (xs \<down> i \<odot> l) (f_Exec_Comp trans_fun (a # NoMsg\<^bsup>l - Suc 0\<^esup>) c)))\<rbrakk> \<Longrightarrow> localState (f_Exec_Comp trans_fun (((a # xs) ! i # NoMsg\<^bsup>l - Suc 0\<^esup>) @ NoMsg\<^bsup>k - l\<^esup>) (f_Exec_Comp trans_fun ((a # xs) \<down> i \<odot> k) c)) = localState (f_Exec_Comp trans_fun ((a # xs) ! i # NoMsg\<^bsup>l - Suc 0\<^esup>) (f_Exec_Comp trans_fun ((a # xs) \<down> i \<odot> l) c))
[PROOF STEP]
apply (drule_tac x=n in meta_spec)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a xs c i n. \<lbrakk>0 < l; l \<le> k; Exec_Equal_State localState trans_fun; \<forall>n\<le>i. State_Idle localState output_fun trans_fun (f_Exec_Comp_Stream_Acc_LocalState l localState trans_fun (a # xs) c ! n); i < length (a # xs); a # xs \<noteq> []; i = Suc n; \<lbrakk>0 < l; l \<le> k; Exec_Equal_State localState trans_fun; \<forall>na\<le>n. State_Idle localState output_fun trans_fun (f_Exec_Comp_Stream_Acc_LocalState l localState trans_fun xs (f_Exec_Comp trans_fun (a # NoMsg\<^bsup>l - Suc 0\<^esup>) c) ! na); n < length xs; xs \<noteq> []\<rbrakk> \<Longrightarrow> localState (f_Exec_Comp trans_fun ((xs ! n # NoMsg\<^bsup>l - Suc 0\<^esup>) @ NoMsg\<^bsup>k - l\<^esup>) (f_Exec_Comp trans_fun (xs \<down> n \<odot> k) (f_Exec_Comp trans_fun (a # NoMsg\<^bsup>l - Suc 0\<^esup>) c))) = localState (f_Exec_Comp trans_fun (xs ! n # NoMsg\<^bsup>l - Suc 0\<^esup>) (f_Exec_Comp trans_fun (xs \<down> n \<odot> l) (f_Exec_Comp trans_fun (a # NoMsg\<^bsup>l - Suc 0\<^esup>) c)))\<rbrakk> \<Longrightarrow> localState (f_Exec_Comp trans_fun (((a # xs) ! i # NoMsg\<^bsup>l - Suc 0\<^esup>) @ NoMsg\<^bsup>k - l\<^esup>) (f_Exec_Comp trans_fun ((a # xs) \<down> i \<odot> k) c)) = localState (f_Exec_Comp trans_fun ((a # xs) ! i # NoMsg\<^bsup>l - Suc 0\<^esup>) (f_Exec_Comp trans_fun ((a # xs) \<down> i \<odot> l) c))
[PROOF STEP]
apply (simp del: f_Exec_Cons)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a xs c i n. \<lbrakk>0 < l; l \<le> k; Exec_Equal_State localState trans_fun; \<forall>na\<le>Suc n. State_Idle localState output_fun trans_fun (f_Exec_Comp_Stream_Acc_LocalState l localState trans_fun (a # xs) c ! na); n < length xs; i = Suc n; \<lbrakk>\<forall>na\<le>n. State_Idle localState output_fun trans_fun (f_Exec_Comp_Stream_Acc_LocalState l localState trans_fun xs (f_Exec_Comp trans_fun (a # NoMsg\<^bsup>l - Suc 0\<^esup>) c) ! na); xs \<noteq> []\<rbrakk> \<Longrightarrow> localState (f_Exec_Comp trans_fun (xs ! n # NoMsg\<^bsup>l - Suc 0\<^esup> @ NoMsg\<^bsup>k - l\<^esup>) (f_Exec_Comp trans_fun (xs \<down> n \<odot> k) (f_Exec_Comp trans_fun (a # NoMsg\<^bsup>l - Suc 0\<^esup>) c))) = localState (f_Exec_Comp trans_fun (xs ! n # NoMsg\<^bsup>l - Suc 0\<^esup>) (f_Exec_Comp trans_fun (xs \<down> n \<odot> l) (f_Exec_Comp trans_fun (a # NoMsg\<^bsup>l - Suc 0\<^esup>) c)))\<rbrakk> \<Longrightarrow> localState (f_Exec_Comp trans_fun (xs ! n # NoMsg\<^bsup>l - Suc 0\<^esup> @ NoMsg\<^bsup>k - l\<^esup>) (f_Exec_Comp trans_fun (a # NoMsg\<^bsup>k - Suc 0\<^esup> @ xs \<down> n \<odot> k) c)) = localState (f_Exec_Comp trans_fun (xs ! n # NoMsg\<^bsup>l - Suc 0\<^esup>) (f_Exec_Comp trans_fun (a # NoMsg\<^bsup>l - Suc 0\<^esup> @ xs \<down> n \<odot> l) c))
[PROOF STEP]
apply (frule length_greater_imp_not_empty)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a xs c i n. \<lbrakk>0 < l; l \<le> k; Exec_Equal_State localState trans_fun; \<forall>na\<le>Suc n. State_Idle localState output_fun trans_fun (f_Exec_Comp_Stream_Acc_LocalState l localState trans_fun (a # xs) c ! na); n < length xs; i = Suc n; \<lbrakk>\<forall>na\<le>n. State_Idle localState output_fun trans_fun (f_Exec_Comp_Stream_Acc_LocalState l localState trans_fun xs (f_Exec_Comp trans_fun (a # NoMsg\<^bsup>l - Suc 0\<^esup>) c) ! na); xs \<noteq> []\<rbrakk> \<Longrightarrow> localState (f_Exec_Comp trans_fun (xs ! n # NoMsg\<^bsup>l - Suc 0\<^esup> @ NoMsg\<^bsup>k - l\<^esup>) (f_Exec_Comp trans_fun (xs \<down> n \<odot> k) (f_Exec_Comp trans_fun (a # NoMsg\<^bsup>l - Suc 0\<^esup>) c))) = localState (f_Exec_Comp trans_fun (xs ! n # NoMsg\<^bsup>l - Suc 0\<^esup>) (f_Exec_Comp trans_fun (xs \<down> n \<odot> l) (f_Exec_Comp trans_fun (a # NoMsg\<^bsup>l - Suc 0\<^esup>) c))); xs \<noteq> []\<rbrakk> \<Longrightarrow> localState (f_Exec_Comp trans_fun (xs ! n # NoMsg\<^bsup>l - Suc 0\<^esup> @ NoMsg\<^bsup>k - l\<^esup>) (f_Exec_Comp trans_fun (a # NoMsg\<^bsup>k - Suc 0\<^esup> @ xs \<down> n \<odot> k) c)) = localState (f_Exec_Comp trans_fun (xs ! n # NoMsg\<^bsup>l - Suc 0\<^esup>) (f_Exec_Comp trans_fun (a # NoMsg\<^bsup>l - Suc 0\<^esup> @ xs \<down> n \<odot> l) c))
[PROOF STEP]
apply (drule meta_mp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a xs c i n. \<lbrakk>0 < l; l \<le> k; Exec_Equal_State localState trans_fun; \<forall>na\<le>Suc n. State_Idle localState output_fun trans_fun (f_Exec_Comp_Stream_Acc_LocalState l localState trans_fun (a # xs) c ! na); n < length xs; i = Suc n; xs \<noteq> []\<rbrakk> \<Longrightarrow> \<forall>na\<le>n. State_Idle localState output_fun trans_fun (f_Exec_Comp_Stream_Acc_LocalState l localState trans_fun xs (f_Exec_Comp trans_fun (a # NoMsg\<^bsup>l - Suc 0\<^esup>) c) ! na)
 2. \<And>a xs c i n. \<lbrakk>0 < l; l \<le> k; Exec_Equal_State localState trans_fun; \<forall>na\<le>Suc n. State_Idle localState output_fun trans_fun (f_Exec_Comp_Stream_Acc_LocalState l localState trans_fun (a # xs) c ! na); n < length xs; i = Suc n; xs \<noteq> []; xs \<noteq> [] \<Longrightarrow> localState (f_Exec_Comp trans_fun (xs ! n # NoMsg\<^bsup>l - Suc 0\<^esup> @ NoMsg\<^bsup>k - l\<^esup>) (f_Exec_Comp trans_fun (xs \<down> n \<odot> k) (f_Exec_Comp trans_fun (a # NoMsg\<^bsup>l - Suc 0\<^esup>) c))) = localState (f_Exec_Comp trans_fun (xs ! n # NoMsg\<^bsup>l - Suc 0\<^esup>) (f_Exec_Comp trans_fun (xs \<down> n \<odot> l) (f_Exec_Comp trans_fun (a # NoMsg\<^bsup>l - Suc 0\<^esup>) c)))\<rbrakk> \<Longrightarrow> localState (f_Exec_Comp trans_fun (xs ! n # NoMsg\<^bsup>l - Suc 0\<^esup> @ NoMsg\<^bsup>k - l\<^esup>) (f_Exec_Comp trans_fun (a # NoMsg\<^bsup>k - Suc 0\<^esup> @ xs \<down> n \<odot> k) c)) = localState (f_Exec_Comp trans_fun (xs ! n # NoMsg\<^bsup>l - Suc 0\<^esup>) (f_Exec_Comp trans_fun (a # NoMsg\<^bsup>l - Suc 0\<^esup> @ xs \<down> n \<odot> l) c))
[PROOF STEP]
apply (simp add: f_Exec_Stream_Acc_LocalState_nth f_Exec_append)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a xs c i n. \<lbrakk>0 < l; l \<le> k; Exec_Equal_State localState trans_fun; \<forall>na\<le>Suc n. State_Idle localState output_fun trans_fun (f_Exec_Comp_Stream_Acc_LocalState l localState trans_fun (a # xs) c ! na); n < length xs; i = Suc n; xs \<noteq> []; xs \<noteq> [] \<Longrightarrow> localState (f_Exec_Comp trans_fun (xs ! n # NoMsg\<^bsup>l - Suc 0\<^esup> @ NoMsg\<^bsup>k - l\<^esup>) (f_Exec_Comp trans_fun (xs \<down> n \<odot> k) (f_Exec_Comp trans_fun (a # NoMsg\<^bsup>l - Suc 0\<^esup>) c))) = localState (f_Exec_Comp trans_fun (xs ! n # NoMsg\<^bsup>l - Suc 0\<^esup>) (f_Exec_Comp trans_fun (xs \<down> n \<odot> l) (f_Exec_Comp trans_fun (a # NoMsg\<^bsup>l - Suc 0\<^esup>) c)))\<rbrakk> \<Longrightarrow> localState (f_Exec_Comp trans_fun (xs ! n # NoMsg\<^bsup>l - Suc 0\<^esup> @ NoMsg\<^bsup>k - l\<^esup>) (f_Exec_Comp trans_fun (a # NoMsg\<^bsup>k - Suc 0\<^esup> @ xs \<down> n \<odot> k) c)) = localState (f_Exec_Comp trans_fun (xs ! n # NoMsg\<^bsup>l - Suc 0\<^esup>) (f_Exec_Comp trans_fun (a # NoMsg\<^bsup>l - Suc 0\<^esup> @ xs \<down> n \<odot> l) c))
[PROOF STEP]
apply (simp add: append_Cons[symmetric] f_expand_Cons f_Exec_append del: append_Cons)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a xs c i n. \<lbrakk>0 < l; l \<le> k; Exec_Equal_State localState trans_fun; \<forall>na\<le>Suc n. State_Idle localState output_fun trans_fun (f_Exec_Comp_Stream_Acc_LocalState l localState trans_fun (a # xs) c ! na); n < length xs; i = Suc n; xs \<noteq> []; localState (f_Exec_Comp trans_fun NoMsg\<^bsup>k - l\<^esup> (f_Exec_Comp trans_fun NoMsg\<^bsup>l - Suc 0\<^esup> (trans_fun (xs ! n) (f_Exec_Comp trans_fun (xs \<down> n \<odot> k) (f_Exec_Comp trans_fun NoMsg\<^bsup>l - Suc 0\<^esup> (trans_fun a c)))))) = localState (f_Exec_Comp trans_fun NoMsg\<^bsup>l - Suc 0\<^esup> (trans_fun (xs ! n) (f_Exec_Comp trans_fun (xs \<down> n \<odot> l) (f_Exec_Comp trans_fun NoMsg\<^bsup>l - Suc 0\<^esup> (trans_fun a c)))))\<rbrakk> \<Longrightarrow> localState (f_Exec_Comp trans_fun NoMsg\<^bsup>k - l\<^esup> (f_Exec_Comp trans_fun NoMsg\<^bsup>l - Suc 0\<^esup> (trans_fun (xs ! n) (f_Exec_Comp trans_fun (xs \<down> n \<odot> k) (f_Exec_Comp trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun a c)))))) = localState (f_Exec_Comp trans_fun NoMsg\<^bsup>l - Suc 0\<^esup> (trans_fun (xs ! n) (f_Exec_Comp trans_fun (xs \<down> n \<odot> l) (f_Exec_Comp trans_fun NoMsg\<^bsup>l - Suc 0\<^esup> (trans_fun a c)))))
[PROOF STEP]
apply (subgoal_tac "
  localState (f_Exec_Comp trans_fun (a # NoMsg\<^bsup>k - Suc 0\<^esup>) c) =
  localState (f_Exec_Comp trans_fun (a # NoMsg\<^bsup>l - Suc 0\<^esup>) c)")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a xs c i n. \<lbrakk>0 < l; l \<le> k; Exec_Equal_State localState trans_fun; \<forall>na\<le>Suc n. State_Idle localState output_fun trans_fun (f_Exec_Comp_Stream_Acc_LocalState l localState trans_fun (a # xs) c ! na); n < length xs; i = Suc n; xs \<noteq> []; localState (f_Exec_Comp trans_fun NoMsg\<^bsup>k - l\<^esup> (f_Exec_Comp trans_fun NoMsg\<^bsup>l - Suc 0\<^esup> (trans_fun (xs ! n) (f_Exec_Comp trans_fun (xs \<down> n \<odot> k) (f_Exec_Comp trans_fun NoMsg\<^bsup>l - Suc 0\<^esup> (trans_fun a c)))))) = localState (f_Exec_Comp trans_fun NoMsg\<^bsup>l - Suc 0\<^esup> (trans_fun (xs ! n) (f_Exec_Comp trans_fun (xs \<down> n \<odot> l) (f_Exec_Comp trans_fun NoMsg\<^bsup>l - Suc 0\<^esup> (trans_fun a c))))); localState (f_Exec_Comp trans_fun (a # NoMsg\<^bsup>k - Suc 0\<^esup>) c) = localState (f_Exec_Comp trans_fun (a # NoMsg\<^bsup>l - Suc 0\<^esup>) c)\<rbrakk> \<Longrightarrow> localState (f_Exec_Comp trans_fun NoMsg\<^bsup>k - l\<^esup> (f_Exec_Comp trans_fun NoMsg\<^bsup>l - Suc 0\<^esup> (trans_fun (xs ! n) (f_Exec_Comp trans_fun (xs \<down> n \<odot> k) (f_Exec_Comp trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun a c)))))) = localState (f_Exec_Comp trans_fun NoMsg\<^bsup>l - Suc 0\<^esup> (trans_fun (xs ! n) (f_Exec_Comp trans_fun (xs \<down> n \<odot> l) (f_Exec_Comp trans_fun NoMsg\<^bsup>l - Suc 0\<^esup> (trans_fun a c)))))
 2. \<And>a xs c i n. \<lbrakk>0 < l; l \<le> k; Exec_Equal_State localState trans_fun; \<forall>na\<le>Suc n. State_Idle localState output_fun trans_fun (f_Exec_Comp_Stream_Acc_LocalState l localState trans_fun (a # xs) c ! na); n < length xs; i = Suc n; xs \<noteq> []; localState (f_Exec_Comp trans_fun NoMsg\<^bsup>k - l\<^esup> (f_Exec_Comp trans_fun NoMsg\<^bsup>l - Suc 0\<^esup> (trans_fun (xs ! n) (f_Exec_Comp trans_fun (xs \<down> n \<odot> k) (f_Exec_Comp trans_fun NoMsg\<^bsup>l - Suc 0\<^esup> (trans_fun a c)))))) = localState (f_Exec_Comp trans_fun NoMsg\<^bsup>l - Suc 0\<^esup> (trans_fun (xs ! n) (f_Exec_Comp trans_fun (xs \<down> n \<odot> l) (f_Exec_Comp trans_fun NoMsg\<^bsup>l - Suc 0\<^esup> (trans_fun a c)))))\<rbrakk> \<Longrightarrow> localState (f_Exec_Comp trans_fun (a # NoMsg\<^bsup>k - Suc 0\<^esup>) c) = localState (f_Exec_Comp trans_fun (a # NoMsg\<^bsup>l - Suc 0\<^esup>) c)
[PROOF STEP]
prefer 2
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a xs c i n. \<lbrakk>0 < l; l \<le> k; Exec_Equal_State localState trans_fun; \<forall>na\<le>Suc n. State_Idle localState output_fun trans_fun (f_Exec_Comp_Stream_Acc_LocalState l localState trans_fun (a # xs) c ! na); n < length xs; i = Suc n; xs \<noteq> []; localState (f_Exec_Comp trans_fun NoMsg\<^bsup>k - l\<^esup> (f_Exec_Comp trans_fun NoMsg\<^bsup>l - Suc 0\<^esup> (trans_fun (xs ! n) (f_Exec_Comp trans_fun (xs \<down> n \<odot> k) (f_Exec_Comp trans_fun NoMsg\<^bsup>l - Suc 0\<^esup> (trans_fun a c)))))) = localState (f_Exec_Comp trans_fun NoMsg\<^bsup>l - Suc 0\<^esup> (trans_fun (xs ! n) (f_Exec_Comp trans_fun (xs \<down> n \<odot> l) (f_Exec_Comp trans_fun NoMsg\<^bsup>l - Suc 0\<^esup> (trans_fun a c)))))\<rbrakk> \<Longrightarrow> localState (f_Exec_Comp trans_fun (a # NoMsg\<^bsup>k - Suc 0\<^esup>) c) = localState (f_Exec_Comp trans_fun (a # NoMsg\<^bsup>l - Suc 0\<^esup>) c)
 2. \<And>a xs c i n. \<lbrakk>0 < l; l \<le> k; Exec_Equal_State localState trans_fun; \<forall>na\<le>Suc n. State_Idle localState output_fun trans_fun (f_Exec_Comp_Stream_Acc_LocalState l localState trans_fun (a # xs) c ! na); n < length xs; i = Suc n; xs \<noteq> []; localState (f_Exec_Comp trans_fun NoMsg\<^bsup>k - l\<^esup> (f_Exec_Comp trans_fun NoMsg\<^bsup>l - Suc 0\<^esup> (trans_fun (xs ! n) (f_Exec_Comp trans_fun (xs \<down> n \<odot> k) (f_Exec_Comp trans_fun NoMsg\<^bsup>l - Suc 0\<^esup> (trans_fun a c)))))) = localState (f_Exec_Comp trans_fun NoMsg\<^bsup>l - Suc 0\<^esup> (trans_fun (xs ! n) (f_Exec_Comp trans_fun (xs \<down> n \<odot> l) (f_Exec_Comp trans_fun NoMsg\<^bsup>l - Suc 0\<^esup> (trans_fun a c))))); localState (f_Exec_Comp trans_fun (a # NoMsg\<^bsup>k - Suc 0\<^esup>) c) = localState (f_Exec_Comp trans_fun (a # NoMsg\<^bsup>l - Suc 0\<^esup>) c)\<rbrakk> \<Longrightarrow> localState (f_Exec_Comp trans_fun NoMsg\<^bsup>k - l\<^esup> (f_Exec_Comp trans_fun NoMsg\<^bsup>l - Suc 0\<^esup> (trans_fun (xs ! n) (f_Exec_Comp trans_fun (xs \<down> n \<odot> k) (f_Exec_Comp trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun a c)))))) = localState (f_Exec_Comp trans_fun NoMsg\<^bsup>l - Suc 0\<^esup> (trans_fun (xs ! n) (f_Exec_Comp trans_fun (xs \<down> n \<odot> l) (f_Exec_Comp trans_fun NoMsg\<^bsup>l - Suc 0\<^esup> (trans_fun a c)))))
[PROOF STEP]
apply (drule_tac x=0 in spec)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a xs c i n. \<lbrakk>0 < l; l \<le> k; Exec_Equal_State localState trans_fun; n < length xs; i = Suc n; xs \<noteq> []; localState (f_Exec_Comp trans_fun NoMsg\<^bsup>k - l\<^esup> (f_Exec_Comp trans_fun NoMsg\<^bsup>l - Suc 0\<^esup> (trans_fun (xs ! n) (f_Exec_Comp trans_fun (xs \<down> n \<odot> k) (f_Exec_Comp trans_fun NoMsg\<^bsup>l - Suc 0\<^esup> (trans_fun a c)))))) = localState (f_Exec_Comp trans_fun NoMsg\<^bsup>l - Suc 0\<^esup> (trans_fun (xs ! n) (f_Exec_Comp trans_fun (xs \<down> n \<odot> l) (f_Exec_Comp trans_fun NoMsg\<^bsup>l - Suc 0\<^esup> (trans_fun a c))))); 0 \<le> Suc n \<longrightarrow> State_Idle localState output_fun trans_fun (f_Exec_Comp_Stream_Acc_LocalState l localState trans_fun (a # xs) c ! 0)\<rbrakk> \<Longrightarrow> localState (f_Exec_Comp trans_fun (a # NoMsg\<^bsup>k - Suc 0\<^esup>) c) = localState (f_Exec_Comp trans_fun (a # NoMsg\<^bsup>l - Suc 0\<^esup>) c)
 2. \<And>a xs c i n. \<lbrakk>0 < l; l \<le> k; Exec_Equal_State localState trans_fun; \<forall>na\<le>Suc n. State_Idle localState output_fun trans_fun (f_Exec_Comp_Stream_Acc_LocalState l localState trans_fun (a # xs) c ! na); n < length xs; i = Suc n; xs \<noteq> []; localState (f_Exec_Comp trans_fun NoMsg\<^bsup>k - l\<^esup> (f_Exec_Comp trans_fun NoMsg\<^bsup>l - Suc 0\<^esup> (trans_fun (xs ! n) (f_Exec_Comp trans_fun (xs \<down> n \<odot> k) (f_Exec_Comp trans_fun NoMsg\<^bsup>l - Suc 0\<^esup> (trans_fun a c)))))) = localState (f_Exec_Comp trans_fun NoMsg\<^bsup>l - Suc 0\<^esup> (trans_fun (xs ! n) (f_Exec_Comp trans_fun (xs \<down> n \<odot> l) (f_Exec_Comp trans_fun NoMsg\<^bsup>l - Suc 0\<^esup> (trans_fun a c))))); localState (f_Exec_Comp trans_fun (a # NoMsg\<^bsup>k - Suc 0\<^esup>) c) = localState (f_Exec_Comp trans_fun (a # NoMsg\<^bsup>l - Suc 0\<^esup>) c)\<rbrakk> \<Longrightarrow> localState (f_Exec_Comp trans_fun NoMsg\<^bsup>k - l\<^esup> (f_Exec_Comp trans_fun NoMsg\<^bsup>l - Suc 0\<^esup> (trans_fun (xs ! n) (f_Exec_Comp trans_fun (xs \<down> n \<odot> k) (f_Exec_Comp trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun a c)))))) = localState (f_Exec_Comp trans_fun NoMsg\<^bsup>l - Suc 0\<^esup> (trans_fun (xs ! n) (f_Exec_Comp trans_fun (xs \<down> n \<odot> l) (f_Exec_Comp trans_fun NoMsg\<^bsup>l - Suc 0\<^esup> (trans_fun a c)))))
[PROOF STEP]
apply (simp add: f_Exec_Stream_Acc_LocalState_Cons)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a xs c i n. \<lbrakk>0 < l; l \<le> k; Exec_Equal_State localState trans_fun; n < length xs; i = Suc n; xs \<noteq> []; localState (f_Exec_Comp trans_fun NoMsg\<^bsup>k - l\<^esup> (f_Exec_Comp trans_fun NoMsg\<^bsup>l - Suc 0\<^esup> (trans_fun (xs ! n) (f_Exec_Comp trans_fun (xs \<down> n \<odot> k) (f_Exec_Comp trans_fun NoMsg\<^bsup>l - Suc 0\<^esup> (trans_fun a c)))))) = localState (f_Exec_Comp trans_fun NoMsg\<^bsup>l - Suc 0\<^esup> (trans_fun (xs ! n) (f_Exec_Comp trans_fun (xs \<down> n \<odot> l) (f_Exec_Comp trans_fun NoMsg\<^bsup>l - Suc 0\<^esup> (trans_fun a c))))); State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun NoMsg\<^bsup>l - Suc 0\<^esup> (trans_fun a c)))\<rbrakk> \<Longrightarrow> localState (f_Exec_Comp trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun a c)) = localState (f_Exec_Comp trans_fun NoMsg\<^bsup>l - Suc 0\<^esup> (trans_fun a c))
 2. \<And>a xs c i n. \<lbrakk>0 < l; l \<le> k; Exec_Equal_State localState trans_fun; \<forall>na\<le>Suc n. State_Idle localState output_fun trans_fun (f_Exec_Comp_Stream_Acc_LocalState l localState trans_fun (a # xs) c ! na); n < length xs; i = Suc n; xs \<noteq> []; localState (f_Exec_Comp trans_fun NoMsg\<^bsup>k - l\<^esup> (f_Exec_Comp trans_fun NoMsg\<^bsup>l - Suc 0\<^esup> (trans_fun (xs ! n) (f_Exec_Comp trans_fun (xs \<down> n \<odot> k) (f_Exec_Comp trans_fun NoMsg\<^bsup>l - Suc 0\<^esup> (trans_fun a c)))))) = localState (f_Exec_Comp trans_fun NoMsg\<^bsup>l - Suc 0\<^esup> (trans_fun (xs ! n) (f_Exec_Comp trans_fun (xs \<down> n \<odot> l) (f_Exec_Comp trans_fun NoMsg\<^bsup>l - Suc 0\<^esup> (trans_fun a c))))); localState (f_Exec_Comp trans_fun (a # NoMsg\<^bsup>k - Suc 0\<^esup>) c) = localState (f_Exec_Comp trans_fun (a # NoMsg\<^bsup>l - Suc 0\<^esup>) c)\<rbrakk> \<Longrightarrow> localState (f_Exec_Comp trans_fun NoMsg\<^bsup>k - l\<^esup> (f_Exec_Comp trans_fun NoMsg\<^bsup>l - Suc 0\<^esup> (trans_fun (xs ! n) (f_Exec_Comp trans_fun (xs \<down> n \<odot> k) (f_Exec_Comp trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun a c)))))) = localState (f_Exec_Comp trans_fun NoMsg\<^bsup>l - Suc 0\<^esup> (trans_fun (xs ! n) (f_Exec_Comp trans_fun (xs \<down> n \<odot> l) (f_Exec_Comp trans_fun NoMsg\<^bsup>l - Suc 0\<^esup> (trans_fun a c)))))
[PROOF STEP]
apply (subst replicate_le_diff2[OF Suc_leI, symmetric], assumption+)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a xs c i n. \<lbrakk>0 < l; l \<le> k; Exec_Equal_State localState trans_fun; n < length xs; i = Suc n; xs \<noteq> []; localState (f_Exec_Comp trans_fun NoMsg\<^bsup>k - l\<^esup> (f_Exec_Comp trans_fun NoMsg\<^bsup>l - Suc 0\<^esup> (trans_fun (xs ! n) (f_Exec_Comp trans_fun (xs \<down> n \<odot> k) (f_Exec_Comp trans_fun NoMsg\<^bsup>l - Suc 0\<^esup> (trans_fun a c)))))) = localState (f_Exec_Comp trans_fun NoMsg\<^bsup>l - Suc 0\<^esup> (trans_fun (xs ! n) (f_Exec_Comp trans_fun (xs \<down> n \<odot> l) (f_Exec_Comp trans_fun NoMsg\<^bsup>l - Suc 0\<^esup> (trans_fun a c))))); State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun NoMsg\<^bsup>l - Suc 0\<^esup> (trans_fun a c)))\<rbrakk> \<Longrightarrow> localState (f_Exec_Comp trans_fun (NoMsg\<^bsup>l - Suc 0\<^esup> @ NoMsg\<^bsup>k - l\<^esup>) (trans_fun a c)) = localState (f_Exec_Comp trans_fun NoMsg\<^bsup>l - Suc 0\<^esup> (trans_fun a c))
 2. \<And>a xs c i n. \<lbrakk>0 < l; l \<le> k; Exec_Equal_State localState trans_fun; \<forall>na\<le>Suc n. State_Idle localState output_fun trans_fun (f_Exec_Comp_Stream_Acc_LocalState l localState trans_fun (a # xs) c ! na); n < length xs; i = Suc n; xs \<noteq> []; localState (f_Exec_Comp trans_fun NoMsg\<^bsup>k - l\<^esup> (f_Exec_Comp trans_fun NoMsg\<^bsup>l - Suc 0\<^esup> (trans_fun (xs ! n) (f_Exec_Comp trans_fun (xs \<down> n \<odot> k) (f_Exec_Comp trans_fun NoMsg\<^bsup>l - Suc 0\<^esup> (trans_fun a c)))))) = localState (f_Exec_Comp trans_fun NoMsg\<^bsup>l - Suc 0\<^esup> (trans_fun (xs ! n) (f_Exec_Comp trans_fun (xs \<down> n \<odot> l) (f_Exec_Comp trans_fun NoMsg\<^bsup>l - Suc 0\<^esup> (trans_fun a c))))); localState (f_Exec_Comp trans_fun (a # NoMsg\<^bsup>k - Suc 0\<^esup>) c) = localState (f_Exec_Comp trans_fun (a # NoMsg\<^bsup>l - Suc 0\<^esup>) c)\<rbrakk> \<Longrightarrow> localState (f_Exec_Comp trans_fun NoMsg\<^bsup>k - l\<^esup> (f_Exec_Comp trans_fun NoMsg\<^bsup>l - Suc 0\<^esup> (trans_fun (xs ! n) (f_Exec_Comp trans_fun (xs \<down> n \<odot> k) (f_Exec_Comp trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun a c)))))) = localState (f_Exec_Comp trans_fun NoMsg\<^bsup>l - Suc 0\<^esup> (trans_fun (xs ! n) (f_Exec_Comp trans_fun (xs \<down> n \<odot> l) (f_Exec_Comp trans_fun NoMsg\<^bsup>l - Suc 0\<^esup> (trans_fun a c)))))
[PROOF STEP]
apply (simp add: append_Cons[symmetric] f_Exec_append del: append_Cons)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a xs c i n. \<lbrakk>0 < l; l \<le> k; Exec_Equal_State localState trans_fun; n < length xs; i = Suc n; xs \<noteq> []; localState (f_Exec_Comp trans_fun NoMsg\<^bsup>k - l\<^esup> (f_Exec_Comp trans_fun NoMsg\<^bsup>l - Suc 0\<^esup> (trans_fun (xs ! n) (f_Exec_Comp trans_fun (xs \<down> n \<odot> k) (f_Exec_Comp trans_fun NoMsg\<^bsup>l - Suc 0\<^esup> (trans_fun a c)))))) = localState (f_Exec_Comp trans_fun NoMsg\<^bsup>l - Suc 0\<^esup> (trans_fun (xs ! n) (f_Exec_Comp trans_fun (xs \<down> n \<odot> l) (f_Exec_Comp trans_fun NoMsg\<^bsup>l - Suc 0\<^esup> (trans_fun a c))))); State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun NoMsg\<^bsup>l - Suc 0\<^esup> (trans_fun a c)))\<rbrakk> \<Longrightarrow> localState (f_Exec_Comp trans_fun NoMsg\<^bsup>k - l\<^esup> (f_Exec_Comp trans_fun NoMsg\<^bsup>l - Suc 0\<^esup> (trans_fun a c))) = localState (f_Exec_Comp trans_fun NoMsg\<^bsup>l - Suc 0\<^esup> (trans_fun a c))
 2. \<And>a xs c i n. \<lbrakk>0 < l; l \<le> k; Exec_Equal_State localState trans_fun; \<forall>na\<le>Suc n. State_Idle localState output_fun trans_fun (f_Exec_Comp_Stream_Acc_LocalState l localState trans_fun (a # xs) c ! na); n < length xs; i = Suc n; xs \<noteq> []; localState (f_Exec_Comp trans_fun NoMsg\<^bsup>k - l\<^esup> (f_Exec_Comp trans_fun NoMsg\<^bsup>l - Suc 0\<^esup> (trans_fun (xs ! n) (f_Exec_Comp trans_fun (xs \<down> n \<odot> k) (f_Exec_Comp trans_fun NoMsg\<^bsup>l - Suc 0\<^esup> (trans_fun a c)))))) = localState (f_Exec_Comp trans_fun NoMsg\<^bsup>l - Suc 0\<^esup> (trans_fun (xs ! n) (f_Exec_Comp trans_fun (xs \<down> n \<odot> l) (f_Exec_Comp trans_fun NoMsg\<^bsup>l - Suc 0\<^esup> (trans_fun a c))))); localState (f_Exec_Comp trans_fun (a # NoMsg\<^bsup>k - Suc 0\<^esup>) c) = localState (f_Exec_Comp trans_fun (a # NoMsg\<^bsup>l - Suc 0\<^esup>) c)\<rbrakk> \<Longrightarrow> localState (f_Exec_Comp trans_fun NoMsg\<^bsup>k - l\<^esup> (f_Exec_Comp trans_fun NoMsg\<^bsup>l - Suc 0\<^esup> (trans_fun (xs ! n) (f_Exec_Comp trans_fun (xs \<down> n \<odot> k) (f_Exec_Comp trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun a c)))))) = localState (f_Exec_Comp trans_fun NoMsg\<^bsup>l - Suc 0\<^esup> (trans_fun (xs ! n) (f_Exec_Comp trans_fun (xs \<down> n \<odot> l) (f_Exec_Comp trans_fun NoMsg\<^bsup>l - Suc 0\<^esup> (trans_fun a c)))))
[PROOF STEP]
apply (rule f_Exec_State_Idle_replicate_NoMsg_state, assumption)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a xs c i n. \<lbrakk>0 < l; l \<le> k; Exec_Equal_State localState trans_fun; \<forall>na\<le>Suc n. State_Idle localState output_fun trans_fun (f_Exec_Comp_Stream_Acc_LocalState l localState trans_fun (a # xs) c ! na); n < length xs; i = Suc n; xs \<noteq> []; localState (f_Exec_Comp trans_fun NoMsg\<^bsup>k - l\<^esup> (f_Exec_Comp trans_fun NoMsg\<^bsup>l - Suc 0\<^esup> (trans_fun (xs ! n) (f_Exec_Comp trans_fun (xs \<down> n \<odot> k) (f_Exec_Comp trans_fun NoMsg\<^bsup>l - Suc 0\<^esup> (trans_fun a c)))))) = localState (f_Exec_Comp trans_fun NoMsg\<^bsup>l - Suc 0\<^esup> (trans_fun (xs ! n) (f_Exec_Comp trans_fun (xs \<down> n \<odot> l) (f_Exec_Comp trans_fun NoMsg\<^bsup>l - Suc 0\<^esup> (trans_fun a c))))); localState (f_Exec_Comp trans_fun (a # NoMsg\<^bsup>k - Suc 0\<^esup>) c) = localState (f_Exec_Comp trans_fun (a # NoMsg\<^bsup>l - Suc 0\<^esup>) c)\<rbrakk> \<Longrightarrow> localState (f_Exec_Comp trans_fun NoMsg\<^bsup>k - l\<^esup> (f_Exec_Comp trans_fun NoMsg\<^bsup>l - Suc 0\<^esup> (trans_fun (xs ! n) (f_Exec_Comp trans_fun (xs \<down> n \<odot> k) (f_Exec_Comp trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun a c)))))) = localState (f_Exec_Comp trans_fun NoMsg\<^bsup>l - Suc 0\<^esup> (trans_fun (xs ! n) (f_Exec_Comp trans_fun (xs \<down> n \<odot> l) (f_Exec_Comp trans_fun NoMsg\<^bsup>l - Suc 0\<^esup> (trans_fun a c)))))
[PROOF STEP]
apply (case_tac "n = 0")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a xs c i n. \<lbrakk>0 < l; l \<le> k; Exec_Equal_State localState trans_fun; \<forall>na\<le>Suc n. State_Idle localState output_fun trans_fun (f_Exec_Comp_Stream_Acc_LocalState l localState trans_fun (a # xs) c ! na); n < length xs; i = Suc n; xs \<noteq> []; localState (f_Exec_Comp trans_fun NoMsg\<^bsup>k - l\<^esup> (f_Exec_Comp trans_fun NoMsg\<^bsup>l - Suc 0\<^esup> (trans_fun (xs ! n) (f_Exec_Comp trans_fun (xs \<down> n \<odot> k) (f_Exec_Comp trans_fun NoMsg\<^bsup>l - Suc 0\<^esup> (trans_fun a c)))))) = localState (f_Exec_Comp trans_fun NoMsg\<^bsup>l - Suc 0\<^esup> (trans_fun (xs ! n) (f_Exec_Comp trans_fun (xs \<down> n \<odot> l) (f_Exec_Comp trans_fun NoMsg\<^bsup>l - Suc 0\<^esup> (trans_fun a c))))); localState (f_Exec_Comp trans_fun (a # NoMsg\<^bsup>k - Suc 0\<^esup>) c) = localState (f_Exec_Comp trans_fun (a # NoMsg\<^bsup>l - Suc 0\<^esup>) c); n = 0\<rbrakk> \<Longrightarrow> localState (f_Exec_Comp trans_fun NoMsg\<^bsup>k - l\<^esup> (f_Exec_Comp trans_fun NoMsg\<^bsup>l - Suc 0\<^esup> (trans_fun (xs ! n) (f_Exec_Comp trans_fun (xs \<down> n \<odot> k) (f_Exec_Comp trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun a c)))))) = localState (f_Exec_Comp trans_fun NoMsg\<^bsup>l - Suc 0\<^esup> (trans_fun (xs ! n) (f_Exec_Comp trans_fun (xs \<down> n \<odot> l) (f_Exec_Comp trans_fun NoMsg\<^bsup>l - Suc 0\<^esup> (trans_fun a c)))))
 2. \<And>a xs c i n. \<lbrakk>0 < l; l \<le> k; Exec_Equal_State localState trans_fun; \<forall>na\<le>Suc n. State_Idle localState output_fun trans_fun (f_Exec_Comp_Stream_Acc_LocalState l localState trans_fun (a # xs) c ! na); n < length xs; i = Suc n; xs \<noteq> []; localState (f_Exec_Comp trans_fun NoMsg\<^bsup>k - l\<^esup> (f_Exec_Comp trans_fun NoMsg\<^bsup>l - Suc 0\<^esup> (trans_fun (xs ! n) (f_Exec_Comp trans_fun (xs \<down> n \<odot> k) (f_Exec_Comp trans_fun NoMsg\<^bsup>l - Suc 0\<^esup> (trans_fun a c)))))) = localState (f_Exec_Comp trans_fun NoMsg\<^bsup>l - Suc 0\<^esup> (trans_fun (xs ! n) (f_Exec_Comp trans_fun (xs \<down> n \<odot> l) (f_Exec_Comp trans_fun NoMsg\<^bsup>l - Suc 0\<^esup> (trans_fun a c))))); localState (f_Exec_Comp trans_fun (a # NoMsg\<^bsup>k - Suc 0\<^esup>) c) = localState (f_Exec_Comp trans_fun (a # NoMsg\<^bsup>l - Suc 0\<^esup>) c); n \<noteq> 0\<rbrakk> \<Longrightarrow> localState (f_Exec_Comp trans_fun NoMsg\<^bsup>k - l\<^esup> (f_Exec_Comp trans_fun NoMsg\<^bsup>l - Suc 0\<^esup> (trans_fun (xs ! n) (f_Exec_Comp trans_fun (xs \<down> n \<odot> k) (f_Exec_Comp trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun a c)))))) = localState (f_Exec_Comp trans_fun NoMsg\<^bsup>l - Suc 0\<^esup> (trans_fun (xs ! n) (f_Exec_Comp trans_fun (xs \<down> n \<odot> l) (f_Exec_Comp trans_fun NoMsg\<^bsup>l - Suc 0\<^esup> (trans_fun a c)))))
[PROOF STEP]
apply (frule_tac
   ?c1.0="f_Exec_Comp trans_fun (a # NoMsg\<^bsup>k - Suc 0\<^esup>) c" and
   xs = "xs ! 0 # NoMsg\<^bsup>l - Suc 0\<^esup>" in f_Exec_Equal_State)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>a xs c i n. \<lbrakk>0 < l; l \<le> k; Exec_Equal_State localState trans_fun; \<forall>na\<le>Suc n. State_Idle localState output_fun trans_fun (f_Exec_Comp_Stream_Acc_LocalState l localState trans_fun (a # xs) c ! na); n < length xs; i = Suc n; xs \<noteq> []; localState (f_Exec_Comp trans_fun NoMsg\<^bsup>k - l\<^esup> (f_Exec_Comp trans_fun NoMsg\<^bsup>l - Suc 0\<^esup> (trans_fun (xs ! n) (f_Exec_Comp trans_fun (xs \<down> n \<odot> k) (f_Exec_Comp trans_fun NoMsg\<^bsup>l - Suc 0\<^esup> (trans_fun a c)))))) = localState (f_Exec_Comp trans_fun NoMsg\<^bsup>l - Suc 0\<^esup> (trans_fun (xs ! n) (f_Exec_Comp trans_fun (xs \<down> n \<odot> l) (f_Exec_Comp trans_fun NoMsg\<^bsup>l - Suc 0\<^esup> (trans_fun a c))))); localState (f_Exec_Comp trans_fun (a # NoMsg\<^bsup>k - Suc 0\<^esup>) c) = localState (f_Exec_Comp trans_fun (a # NoMsg\<^bsup>l - Suc 0\<^esup>) c); n = 0\<rbrakk> \<Longrightarrow> localState (f_Exec_Comp trans_fun (a # NoMsg\<^bsup>k - Suc 0\<^esup>) c) = localState (?c2.28 a xs c i n)
 2. \<And>a xs c i n. \<lbrakk>0 < l; l \<le> k; Exec_Equal_State localState trans_fun; \<forall>na\<le>Suc n. State_Idle localState output_fun trans_fun (f_Exec_Comp_Stream_Acc_LocalState l localState trans_fun (a # xs) c ! na); n < length xs; i = Suc n; xs \<noteq> []; localState (f_Exec_Comp trans_fun NoMsg\<^bsup>k - l\<^esup> (f_Exec_Comp trans_fun NoMsg\<^bsup>l - Suc 0\<^esup> (trans_fun (xs ! n) (f_Exec_Comp trans_fun (xs \<down> n \<odot> k) (f_Exec_Comp trans_fun NoMsg\<^bsup>l - Suc 0\<^esup> (trans_fun a c)))))) = localState (f_Exec_Comp trans_fun NoMsg\<^bsup>l - Suc 0\<^esup> (trans_fun (xs ! n) (f_Exec_Comp trans_fun (xs \<down> n \<odot> l) (f_Exec_Comp trans_fun NoMsg\<^bsup>l - Suc 0\<^esup> (trans_fun a c))))); localState (f_Exec_Comp trans_fun (a # NoMsg\<^bsup>k - Suc 0\<^esup>) c) = localState (f_Exec_Comp trans_fun (a # NoMsg\<^bsup>l - Suc 0\<^esup>) c); n = 0\<rbrakk> \<Longrightarrow> xs ! 0 # NoMsg\<^bsup>l - Suc 0\<^esup> \<noteq> []
 3. \<And>a xs c i n. \<lbrakk>0 < l; l \<le> k; Exec_Equal_State localState trans_fun; \<forall>na\<le>Suc n. State_Idle localState output_fun trans_fun (f_Exec_Comp_Stream_Acc_LocalState l localState trans_fun (a # xs) c ! na); n < length xs; i = Suc n; xs \<noteq> []; localState (f_Exec_Comp trans_fun NoMsg\<^bsup>k - l\<^esup> (f_Exec_Comp trans_fun NoMsg\<^bsup>l - Suc 0\<^esup> (trans_fun (xs ! n) (f_Exec_Comp trans_fun (xs \<down> n \<odot> k) (f_Exec_Comp trans_fun NoMsg\<^bsup>l - Suc 0\<^esup> (trans_fun a c)))))) = localState (f_Exec_Comp trans_fun NoMsg\<^bsup>l - Suc 0\<^esup> (trans_fun (xs ! n) (f_Exec_Comp trans_fun (xs \<down> n \<odot> l) (f_Exec_Comp trans_fun NoMsg\<^bsup>l - Suc 0\<^esup> (trans_fun a c))))); localState (f_Exec_Comp trans_fun (a # NoMsg\<^bsup>k - Suc 0\<^esup>) c) = localState (f_Exec_Comp trans_fun (a # NoMsg\<^bsup>l - Suc 0\<^esup>) c); n = 0; f_Exec_Comp trans_fun (xs ! 0 # NoMsg\<^bsup>l - Suc 0\<^esup>) (f_Exec_Comp trans_fun (a # NoMsg\<^bsup>k - Suc 0\<^esup>) c) = f_Exec_Comp trans_fun (xs ! 0 # NoMsg\<^bsup>l - Suc 0\<^esup>) (?c2.28 a xs c i n)\<rbrakk> \<Longrightarrow> localState (f_Exec_Comp trans_fun NoMsg\<^bsup>k - l\<^esup> (f_Exec_Comp trans_fun NoMsg\<^bsup>l - Suc 0\<^esup> (trans_fun (xs ! n) (f_Exec_Comp trans_fun (xs \<down> n \<odot> k) (f_Exec_Comp trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun a c)))))) = localState (f_Exec_Comp trans_fun NoMsg\<^bsup>l - Suc 0\<^esup> (trans_fun (xs ! n) (f_Exec_Comp trans_fun (xs \<down> n \<odot> l) (f_Exec_Comp trans_fun NoMsg\<^bsup>l - Suc 0\<^esup> (trans_fun a c)))))
 4. \<And>a xs c i n. \<lbrakk>0 < l; l \<le> k; Exec_Equal_State localState trans_fun; \<forall>na\<le>Suc n. State_Idle localState output_fun trans_fun (f_Exec_Comp_Stream_Acc_LocalState l localState trans_fun (a # xs) c ! na); n < length xs; i = Suc n; xs \<noteq> []; localState (f_Exec_Comp trans_fun NoMsg\<^bsup>k - l\<^esup> (f_Exec_Comp trans_fun NoMsg\<^bsup>l - Suc 0\<^esup> (trans_fun (xs ! n) (f_Exec_Comp trans_fun (xs \<down> n \<odot> k) (f_Exec_Comp trans_fun NoMsg\<^bsup>l - Suc 0\<^esup> (trans_fun a c)))))) = localState (f_Exec_Comp trans_fun NoMsg\<^bsup>l - Suc 0\<^esup> (trans_fun (xs ! n) (f_Exec_Comp trans_fun (xs \<down> n \<odot> l) (f_Exec_Comp trans_fun NoMsg\<^bsup>l - Suc 0\<^esup> (trans_fun a c))))); localState (f_Exec_Comp trans_fun (a # NoMsg\<^bsup>k - Suc 0\<^esup>) c) = localState (f_Exec_Comp trans_fun (a # NoMsg\<^bsup>l - Suc 0\<^esup>) c); n \<noteq> 0\<rbrakk> \<Longrightarrow> localState (f_Exec_Comp trans_fun NoMsg\<^bsup>k - l\<^esup> (f_Exec_Comp trans_fun NoMsg\<^bsup>l - Suc 0\<^esup> (trans_fun (xs ! n) (f_Exec_Comp trans_fun (xs \<down> n \<odot> k) (f_Exec_Comp trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun a c)))))) = localState (f_Exec_Comp trans_fun NoMsg\<^bsup>l - Suc 0\<^esup> (trans_fun (xs ! n) (f_Exec_Comp trans_fun (xs \<down> n \<odot> l) (f_Exec_Comp trans_fun NoMsg\<^bsup>l - Suc 0\<^esup> (trans_fun a c)))))
[PROOF STEP]
apply simp+
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a xs c i n. \<lbrakk>0 < l; l \<le> k; Exec_Equal_State localState trans_fun; \<forall>na\<le>Suc n. State_Idle localState output_fun trans_fun (f_Exec_Comp_Stream_Acc_LocalState l localState trans_fun (a # xs) c ! na); n < length xs; i = Suc n; xs \<noteq> []; localState (f_Exec_Comp trans_fun NoMsg\<^bsup>k - l\<^esup> (f_Exec_Comp trans_fun NoMsg\<^bsup>l - Suc 0\<^esup> (trans_fun (xs ! n) (f_Exec_Comp trans_fun (xs \<down> n \<odot> k) (f_Exec_Comp trans_fun NoMsg\<^bsup>l - Suc 0\<^esup> (trans_fun a c)))))) = localState (f_Exec_Comp trans_fun NoMsg\<^bsup>l - Suc 0\<^esup> (trans_fun (xs ! n) (f_Exec_Comp trans_fun (xs \<down> n \<odot> l) (f_Exec_Comp trans_fun NoMsg\<^bsup>l - Suc 0\<^esup> (trans_fun a c))))); localState (f_Exec_Comp trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun a c)) = localState (f_Exec_Comp trans_fun NoMsg\<^bsup>l - Suc 0\<^esup> (trans_fun a c)); 0 < n\<rbrakk> \<Longrightarrow> localState (f_Exec_Comp trans_fun NoMsg\<^bsup>k - l\<^esup> (f_Exec_Comp trans_fun NoMsg\<^bsup>l - Suc 0\<^esup> (trans_fun (xs ! n) (f_Exec_Comp trans_fun (xs \<down> n \<odot> k) (f_Exec_Comp trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun a c)))))) = localState (f_Exec_Comp trans_fun NoMsg\<^bsup>l - Suc 0\<^esup> (trans_fun (xs ! n) (f_Exec_Comp trans_fun (xs \<down> n \<odot> l) (f_Exec_Comp trans_fun NoMsg\<^bsup>l - Suc 0\<^esup> (trans_fun a c)))))
[PROOF STEP]
apply (frule_tac
  ?c1.0="f_Exec_Comp trans_fun (a # NoMsg\<^bsup>k - Suc 0\<^esup>) c" and
  xs = "xs \<down> n \<odot>\<^sub>f k" in f_Exec_Equal_State)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>a xs c i n. \<lbrakk>0 < l; l \<le> k; Exec_Equal_State localState trans_fun; \<forall>na\<le>Suc n. State_Idle localState output_fun trans_fun (f_Exec_Comp_Stream_Acc_LocalState l localState trans_fun (a # xs) c ! na); n < length xs; i = Suc n; xs \<noteq> []; localState (f_Exec_Comp trans_fun NoMsg\<^bsup>k - l\<^esup> (f_Exec_Comp trans_fun NoMsg\<^bsup>l - Suc 0\<^esup> (trans_fun (xs ! n) (f_Exec_Comp trans_fun (xs \<down> n \<odot> k) (f_Exec_Comp trans_fun NoMsg\<^bsup>l - Suc 0\<^esup> (trans_fun a c)))))) = localState (f_Exec_Comp trans_fun NoMsg\<^bsup>l - Suc 0\<^esup> (trans_fun (xs ! n) (f_Exec_Comp trans_fun (xs \<down> n \<odot> l) (f_Exec_Comp trans_fun NoMsg\<^bsup>l - Suc 0\<^esup> (trans_fun a c))))); localState (f_Exec_Comp trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun a c)) = localState (f_Exec_Comp trans_fun NoMsg\<^bsup>l - Suc 0\<^esup> (trans_fun a c)); 0 < n\<rbrakk> \<Longrightarrow> localState (f_Exec_Comp trans_fun (a # NoMsg\<^bsup>k - Suc 0\<^esup>) c) = localState (?c2.33 a xs c i n)
 2. \<And>a xs c i n. \<lbrakk>0 < l; l \<le> k; Exec_Equal_State localState trans_fun; \<forall>na\<le>Suc n. State_Idle localState output_fun trans_fun (f_Exec_Comp_Stream_Acc_LocalState l localState trans_fun (a # xs) c ! na); n < length xs; i = Suc n; xs \<noteq> []; localState (f_Exec_Comp trans_fun NoMsg\<^bsup>k - l\<^esup> (f_Exec_Comp trans_fun NoMsg\<^bsup>l - Suc 0\<^esup> (trans_fun (xs ! n) (f_Exec_Comp trans_fun (xs \<down> n \<odot> k) (f_Exec_Comp trans_fun NoMsg\<^bsup>l - Suc 0\<^esup> (trans_fun a c)))))) = localState (f_Exec_Comp trans_fun NoMsg\<^bsup>l - Suc 0\<^esup> (trans_fun (xs ! n) (f_Exec_Comp trans_fun (xs \<down> n \<odot> l) (f_Exec_Comp trans_fun NoMsg\<^bsup>l - Suc 0\<^esup> (trans_fun a c))))); localState (f_Exec_Comp trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun a c)) = localState (f_Exec_Comp trans_fun NoMsg\<^bsup>l - Suc 0\<^esup> (trans_fun a c)); 0 < n\<rbrakk> \<Longrightarrow> xs \<down> n \<odot> k \<noteq> []
 3. \<And>a xs c i n. \<lbrakk>0 < l; l \<le> k; Exec_Equal_State localState trans_fun; \<forall>na\<le>Suc n. State_Idle localState output_fun trans_fun (f_Exec_Comp_Stream_Acc_LocalState l localState trans_fun (a # xs) c ! na); n < length xs; i = Suc n; xs \<noteq> []; localState (f_Exec_Comp trans_fun NoMsg\<^bsup>k - l\<^esup> (f_Exec_Comp trans_fun NoMsg\<^bsup>l - Suc 0\<^esup> (trans_fun (xs ! n) (f_Exec_Comp trans_fun (xs \<down> n \<odot> k) (f_Exec_Comp trans_fun NoMsg\<^bsup>l - Suc 0\<^esup> (trans_fun a c)))))) = localState (f_Exec_Comp trans_fun NoMsg\<^bsup>l - Suc 0\<^esup> (trans_fun (xs ! n) (f_Exec_Comp trans_fun (xs \<down> n \<odot> l) (f_Exec_Comp trans_fun NoMsg\<^bsup>l - Suc 0\<^esup> (trans_fun a c))))); localState (f_Exec_Comp trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun a c)) = localState (f_Exec_Comp trans_fun NoMsg\<^bsup>l - Suc 0\<^esup> (trans_fun a c)); 0 < n; f_Exec_Comp trans_fun (xs \<down> n \<odot> k) (f_Exec_Comp trans_fun (a # NoMsg\<^bsup>k - Suc 0\<^esup>) c) = f_Exec_Comp trans_fun (xs \<down> n \<odot> k) (?c2.33 a xs c i n)\<rbrakk> \<Longrightarrow> localState (f_Exec_Comp trans_fun NoMsg\<^bsup>k - l\<^esup> (f_Exec_Comp trans_fun NoMsg\<^bsup>l - Suc 0\<^esup> (trans_fun (xs ! n) (f_Exec_Comp trans_fun (xs \<down> n \<odot> k) (f_Exec_Comp trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun a c)))))) = localState (f_Exec_Comp trans_fun NoMsg\<^bsup>l - Suc 0\<^esup> (trans_fun (xs ! n) (f_Exec_Comp trans_fun (xs \<down> n \<odot> l) (f_Exec_Comp trans_fun NoMsg\<^bsup>l - Suc 0\<^esup> (trans_fun a c)))))
[PROOF STEP]
apply (simp add: f_expand_not_empty_conv)+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma i_Exec_Stream_Acc_LocalState__State_Idle_nth[rule_format]: "
  \<lbrakk> 0 < l; l \<le> k; Exec_Equal_State localState trans_fun;
    \<forall>n\<le>i. State_Idle localState output_fun trans_fun (
      i_Exec_Comp_Stream_Acc_LocalState l localState trans_fun input c n) \<rbrakk> \<Longrightarrow>
  i_Exec_Comp_Stream_Acc_LocalState k localState trans_fun input c i =
  i_Exec_Comp_Stream_Acc_LocalState l localState trans_fun input c i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < l; l \<le> k; Exec_Equal_State localState trans_fun; \<forall>n\<le>i. State_Idle localState output_fun trans_fun (i_Exec_Comp_Stream_Acc_LocalState l localState trans_fun input c n)\<rbrakk> \<Longrightarrow> i_Exec_Comp_Stream_Acc_LocalState k localState trans_fun input c i = i_Exec_Comp_Stream_Acc_LocalState l localState trans_fun input c i
[PROOF STEP]
apply (simp only: f_Exec_Stream_Acc_LocalState_nth_eq_i_nth[of _ _ "Suc i", symmetric])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < l; l \<le> k; Exec_Equal_State localState trans_fun; \<forall>n\<le>i. State_Idle localState output_fun trans_fun (i_Exec_Comp_Stream_Acc_LocalState l localState trans_fun input c n)\<rbrakk> \<Longrightarrow> f_Exec_Comp_Stream_Acc_LocalState k localState trans_fun (input \<Down> Suc i) c ! i = f_Exec_Comp_Stream_Acc_LocalState l localState trans_fun (input \<Down> Suc i) c ! i
[PROOF STEP]
apply (rule f_Exec_Stream_Acc_LocalState__State_Idle_nth)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<lbrakk>0 < l; l \<le> k; Exec_Equal_State localState trans_fun; \<forall>n\<le>i. State_Idle localState output_fun trans_fun (i_Exec_Comp_Stream_Acc_LocalState l localState trans_fun input c n)\<rbrakk> \<Longrightarrow> 0 < l
 2. \<lbrakk>0 < l; l \<le> k; Exec_Equal_State localState trans_fun; \<forall>n\<le>i. State_Idle localState output_fun trans_fun (i_Exec_Comp_Stream_Acc_LocalState l localState trans_fun input c n)\<rbrakk> \<Longrightarrow> l \<le> k
 3. \<lbrakk>0 < l; l \<le> k; Exec_Equal_State localState trans_fun; \<forall>n\<le>i. State_Idle localState output_fun trans_fun (i_Exec_Comp_Stream_Acc_LocalState l localState trans_fun input c n)\<rbrakk> \<Longrightarrow> Exec_Equal_State localState trans_fun
 4. \<And>n. \<lbrakk>0 < l; l \<le> k; Exec_Equal_State localState trans_fun; \<forall>n\<le>i. State_Idle localState output_fun trans_fun (i_Exec_Comp_Stream_Acc_LocalState l localState trans_fun input c n); n \<le> i\<rbrakk> \<Longrightarrow> State_Idle localState ?output_fun16 trans_fun (f_Exec_Comp_Stream_Acc_LocalState l localState trans_fun (input \<Down> Suc i) c ! n)
 5. \<lbrakk>0 < l; l \<le> k; Exec_Equal_State localState trans_fun; \<forall>n\<le>i. State_Idle localState output_fun trans_fun (i_Exec_Comp_Stream_Acc_LocalState l localState trans_fun input c n)\<rbrakk> \<Longrightarrow> i < length (input \<Down> Suc i)
[PROOF STEP]
apply simp_all
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>0 < l; l \<le> k; Exec_Equal_State localState trans_fun; \<forall>n\<le>i. State_Idle localState output_fun trans_fun (i_Exec_Comp_Stream_Acc_LocalState l localState trans_fun input c n); n \<le> i\<rbrakk> \<Longrightarrow> State_Idle localState ?output_fun16 trans_fun (f_Exec_Comp_Stream_Acc_LocalState l localState trans_fun (input \<Down> Suc i) c ! n)
[PROOF STEP]
apply (drule_tac x=n in spec)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>0 < l; l \<le> k; Exec_Equal_State localState trans_fun; n \<le> i; n \<le> i \<longrightarrow> State_Idle localState output_fun trans_fun (i_Exec_Comp_Stream_Acc_LocalState l localState trans_fun input c n)\<rbrakk> \<Longrightarrow> State_Idle localState ?output_fun16 trans_fun (f_Exec_Comp_Stream_Acc_LocalState l localState trans_fun (input \<Down> Suc i) c ! n)
[PROOF STEP]
apply (simp add: f_Exec_Stream_Acc_LocalState_nth_eq_i_nth)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done