[STATEMENT]
lemma f_Exec_Stream_Acc_Output__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 (
      f_Exec_Comp_Stream_Acc_LocalState l localState trans_fun xs c ! n);
    i < length xs \<rbrakk> \<Longrightarrow>
  f_Exec_Comp_Stream_Acc_Output k output_fun trans_fun xs c ! i =
  f_Exec_Comp_Stream_Acc_Output l output_fun trans_fun xs 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 (f_Exec_Comp_Stream_Acc_LocalState l localState trans_fun xs c ! n); i < length xs\<rbrakk> \<Longrightarrow> f_Exec_Comp_Stream_Acc_Output k output_fun trans_fun xs c ! i = f_Exec_Comp_Stream_Acc_Output l output_fun trans_fun xs c ! i
[PROOF STEP]
apply (drule order_le_less[THEN iffD1], erule disjE)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>0 < l; 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; l < k\<rbrakk> \<Longrightarrow> f_Exec_Comp_Stream_Acc_Output k output_fun trans_fun xs c ! i = f_Exec_Comp_Stream_Acc_Output l output_fun trans_fun xs c ! i
 2. \<lbrakk>0 < l; 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; l = k\<rbrakk> \<Longrightarrow> f_Exec_Comp_Stream_Acc_Output k output_fun trans_fun xs c ! i = f_Exec_Comp_Stream_Acc_Output l output_fun trans_fun xs c ! i
[PROOF STEP]
prefer 2
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>0 < l; 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; l = k\<rbrakk> \<Longrightarrow> f_Exec_Comp_Stream_Acc_Output k output_fun trans_fun xs c ! i = f_Exec_Comp_Stream_Acc_Output l output_fun trans_fun xs c ! i
 2. \<lbrakk>0 < l; 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; l < k\<rbrakk> \<Longrightarrow> f_Exec_Comp_Stream_Acc_Output k output_fun trans_fun xs c ! i = f_Exec_Comp_Stream_Acc_Output l output_fun trans_fun xs c ! i
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < l; 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; l < k\<rbrakk> \<Longrightarrow> f_Exec_Comp_Stream_Acc_Output k output_fun trans_fun xs c ! i = f_Exec_Comp_Stream_Acc_Output l output_fun trans_fun xs c ! i
[PROOF STEP]
apply (frule zero_less_diff[of k l, THEN iffD2])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < l; 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; l < k; 0 < k - l\<rbrakk> \<Longrightarrow> f_Exec_Comp_Stream_Acc_Output k output_fun trans_fun xs c ! i = f_Exec_Comp_Stream_Acc_Output l output_fun trans_fun xs c ! i
[PROOF STEP]
apply (frule length_greater_imp_not_empty)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < l; 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; l < k; 0 < k - l; xs \<noteq> []\<rbrakk> \<Longrightarrow> f_Exec_Comp_Stream_Acc_Output k output_fun trans_fun xs c ! i = f_Exec_Comp_Stream_Acc_Output l output_fun trans_fun xs c ! i
[PROOF STEP]
apply (simp add: f_Exec_Stream_Acc_Output_nth del: f_Exec_Stream_Cons)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < l; 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; l < k; xs \<noteq> []\<rbrakk> \<Longrightarrow> last_message (map output_fun (f_Exec_Comp_Stream trans_fun (xs ! i # NoMsg\<^bsup>k - Suc 0\<^esup>) (f_Exec_Comp trans_fun (xs \<down> i \<odot> k) c))) = last_message (map output_fun (f_Exec_Comp_Stream 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 replicate_le_diff2[OF Suc_leI, symmetric])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>0 < l; 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; l < k; xs \<noteq> []\<rbrakk> \<Longrightarrow> 0 < ?m9
 2. \<lbrakk>0 < l; 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; l < k; xs \<noteq> []\<rbrakk> \<Longrightarrow> ?m9 \<le> k
 3. \<lbrakk>0 < l; 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; l < k; xs \<noteq> []\<rbrakk> \<Longrightarrow> last_message (map output_fun (f_Exec_Comp_Stream trans_fun (xs ! i # NoMsg\<^bsup>?m9 - Suc 0\<^esup> @ NoMsg\<^bsup>k - ?m9\<^esup>) (f_Exec_Comp trans_fun (xs \<down> i \<odot> k) c))) = last_message (map output_fun (f_Exec_Comp_Stream 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 del: f_Exec_Stream_Cons)+
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < l; 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; l < k; xs \<noteq> []\<rbrakk> \<Longrightarrow> last_message (map output_fun (f_Exec_Comp_Stream 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))) = last_message (map output_fun (f_Exec_Comp_Stream 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. \<lbrakk>0 < l; 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; l < k; xs \<noteq> []\<rbrakk> \<Longrightarrow> last_message (map output_fun (f_Exec_Comp_Stream 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))) = last_message (map output_fun (f_Exec_Comp_Stream trans_fun (xs ! i # NoMsg\<^bsup>l - Suc 0\<^esup>) (f_Exec_Comp trans_fun (xs \<down> i \<odot> l) c)))
[PROOF STEP]
apply (case_tac i)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>0 < l; 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; l < k; xs \<noteq> []; i = 0\<rbrakk> \<Longrightarrow> last_message (map output_fun (f_Exec_Comp_Stream 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))) = last_message (map output_fun (f_Exec_Comp_Stream trans_fun (xs ! i # NoMsg\<^bsup>l - Suc 0\<^esup>) (f_Exec_Comp trans_fun (xs \<down> i \<odot> l) c)))
 2. \<And>nat. \<lbrakk>0 < l; 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; l < k; xs \<noteq> []; i = Suc nat\<rbrakk> \<Longrightarrow> last_message (map output_fun (f_Exec_Comp_Stream 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))) = last_message (map output_fun (f_Exec_Comp_Stream trans_fun (xs ! i # NoMsg\<^bsup>l - Suc 0\<^esup>) (f_Exec_Comp trans_fun (xs \<down> i \<odot> l) c)))
[PROOF STEP]
apply (drule_tac x=0 in spec)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>0 < l; Exec_Equal_State localState trans_fun; i < length xs; l < k; xs \<noteq> []; i = 0; 0 \<le> i \<longrightarrow> State_Idle localState output_fun trans_fun (f_Exec_Comp_Stream_Acc_LocalState l localState trans_fun xs c ! 0)\<rbrakk> \<Longrightarrow> last_message (map output_fun (f_Exec_Comp_Stream 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))) = last_message (map output_fun (f_Exec_Comp_Stream trans_fun (xs ! i # NoMsg\<^bsup>l - Suc 0\<^esup>) (f_Exec_Comp trans_fun (xs \<down> i \<odot> l) c)))
 2. \<And>nat. \<lbrakk>0 < l; 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; l < k; xs \<noteq> []; i = Suc nat\<rbrakk> \<Longrightarrow> last_message (map output_fun (f_Exec_Comp_Stream 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))) = last_message (map output_fun (f_Exec_Comp_Stream 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: f_Exec_Stream_Acc_LocalState_nth take_first f_expand_one del: last.simps f_Exec_Cons f_Exec_Stream_Cons append_Cons replicate.simps)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>0 < l; Exec_Equal_State localState trans_fun; l < k; xs \<noteq> []; i = 0; State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun (xs ! 0 # NoMsg\<^bsup>l - Suc 0\<^esup>) c))\<rbrakk> \<Longrightarrow> last_message (map output_fun (f_Exec_Comp_Stream trans_fun ((xs ! 0 # NoMsg\<^bsup>l - Suc 0\<^esup>) @ NoMsg\<^bsup>k - l\<^esup>) c)) = last_message (map output_fun (f_Exec_Comp_Stream trans_fun (xs ! 0 # NoMsg\<^bsup>l - Suc 0\<^esup>) c))
 2. \<And>nat. \<lbrakk>0 < l; 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; l < k; xs \<noteq> []; i = Suc nat\<rbrakk> \<Longrightarrow> last_message (map output_fun (f_Exec_Comp_Stream 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))) = last_message (map output_fun (f_Exec_Comp_Stream 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 only: f_Exec_Stream_append map_append last_message_append)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>0 < l; Exec_Equal_State localState trans_fun; l < k; xs \<noteq> []; i = 0; State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun (xs ! 0 # NoMsg\<^bsup>l - Suc 0\<^esup>) c))\<rbrakk> \<Longrightarrow> (if last_message (map output_fun (f_Exec_Comp_Stream trans_fun NoMsg\<^bsup>k - l\<^esup> (f_Exec_Comp trans_fun (xs ! 0 # NoMsg\<^bsup>l - Suc 0\<^esup>) c))) = NoMsg then last_message (map output_fun (f_Exec_Comp_Stream trans_fun (xs ! 0 # NoMsg\<^bsup>l - Suc 0\<^esup>) c)) else last_message (map output_fun (f_Exec_Comp_Stream trans_fun NoMsg\<^bsup>k - l\<^esup> (f_Exec_Comp trans_fun (xs ! 0 # NoMsg\<^bsup>l - Suc 0\<^esup>) c)))) = last_message (map output_fun (f_Exec_Comp_Stream trans_fun (xs ! 0 # NoMsg\<^bsup>l - Suc 0\<^esup>) c))
 2. \<And>nat. \<lbrakk>0 < l; 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; l < k; xs \<noteq> []; i = Suc nat\<rbrakk> \<Longrightarrow> last_message (map output_fun (f_Exec_Comp_Stream 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))) = last_message (map output_fun (f_Exec_Comp_Stream 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 if_P')
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>0 < l; Exec_Equal_State localState trans_fun; l < k; xs \<noteq> []; i = 0; State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun (xs ! 0 # NoMsg\<^bsup>l - Suc 0\<^esup>) c))\<rbrakk> \<Longrightarrow> last_message (map output_fun (f_Exec_Comp_Stream trans_fun NoMsg\<^bsup>k - l\<^esup> (f_Exec_Comp trans_fun (xs ! 0 # NoMsg\<^bsup>l - Suc 0\<^esup>) c))) = NoMsg
 2. \<lbrakk>0 < l; Exec_Equal_State localState trans_fun; l < k; xs \<noteq> []; i = 0; State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun (xs ! 0 # NoMsg\<^bsup>l - Suc 0\<^esup>) c))\<rbrakk> \<Longrightarrow> last_message (map output_fun (f_Exec_Comp_Stream trans_fun (xs ! 0 # NoMsg\<^bsup>l - Suc 0\<^esup>) c)) = last_message (map output_fun (f_Exec_Comp_Stream trans_fun (xs ! 0 # NoMsg\<^bsup>l - Suc 0\<^esup>) c))
 3. \<And>nat. \<lbrakk>0 < l; 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; l < k; xs \<noteq> []; i = Suc nat\<rbrakk> \<Longrightarrow> last_message (map output_fun (f_Exec_Comp_Stream 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))) = last_message (map output_fun (f_Exec_Comp_Stream trans_fun (xs ! i # NoMsg\<^bsup>l - Suc 0\<^esup>) (f_Exec_Comp trans_fun (xs \<down> i \<odot> l) c)))
[PROOF STEP]
apply (clarsimp simp: last_message_NoMsg_conv f_Exec_Stream_nth min_eqL simp del: last.simps f_Exec_Comp.simps append_Cons replicate.simps)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>ia. \<lbrakk>0 < l; Exec_Equal_State localState trans_fun; l < k; xs \<noteq> []; i = 0; State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun (xs ! 0 # NoMsg\<^bsup>l - Suc 0\<^esup>) c)); ia < k - l\<rbrakk> \<Longrightarrow> output_fun (f_Exec_Comp trans_fun NoMsg\<^bsup>Suc ia\<^esup> (f_Exec_Comp trans_fun (xs ! 0 # NoMsg\<^bsup>l - Suc 0\<^esup>) c)) = NoMsg
 2. \<lbrakk>0 < l; Exec_Equal_State localState trans_fun; l < k; xs \<noteq> []; i = 0; State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun (xs ! 0 # NoMsg\<^bsup>l - Suc 0\<^esup>) c))\<rbrakk> \<Longrightarrow> last_message (map output_fun (f_Exec_Comp_Stream trans_fun (xs ! 0 # NoMsg\<^bsup>l - Suc 0\<^esup>) c)) = last_message (map output_fun (f_Exec_Comp_Stream trans_fun (xs ! 0 # NoMsg\<^bsup>l - Suc 0\<^esup>) c))
 3. \<And>nat. \<lbrakk>0 < l; 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; l < k; xs \<noteq> []; i = Suc nat\<rbrakk> \<Longrightarrow> last_message (map output_fun (f_Exec_Comp_Stream 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))) = last_message (map output_fun (f_Exec_Comp_Stream 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 f_Exec_State_Idle_replicate_NoMsg_gr0_output)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>ia. \<lbrakk>0 < l; Exec_Equal_State localState trans_fun; l < k; xs \<noteq> []; i = 0; State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun (xs ! 0 # NoMsg\<^bsup>l - Suc 0\<^esup>) c)); ia < k - l\<rbrakk> \<Longrightarrow> State_Idle (?localState21 ia) output_fun trans_fun (?localState21 ia (f_Exec_Comp trans_fun (xs ! 0 # NoMsg\<^bsup>l - Suc 0\<^esup>) c))
 2. \<And>ia. \<lbrakk>0 < l; Exec_Equal_State localState trans_fun; l < k; xs \<noteq> []; i = 0; State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun (xs ! 0 # NoMsg\<^bsup>l - Suc 0\<^esup>) c)); ia < k - l\<rbrakk> \<Longrightarrow> 0 < Suc ia
 3. \<lbrakk>0 < l; Exec_Equal_State localState trans_fun; l < k; xs \<noteq> []; i = 0; State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun (xs ! 0 # NoMsg\<^bsup>l - Suc 0\<^esup>) c))\<rbrakk> \<Longrightarrow> last_message (map output_fun (f_Exec_Comp_Stream trans_fun (xs ! 0 # NoMsg\<^bsup>l - Suc 0\<^esup>) c)) = last_message (map output_fun (f_Exec_Comp_Stream trans_fun (xs ! 0 # NoMsg\<^bsup>l - Suc 0\<^esup>) c))
 4. \<And>nat. \<lbrakk>0 < l; 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; l < k; xs \<noteq> []; i = Suc nat\<rbrakk> \<Longrightarrow> last_message (map output_fun (f_Exec_Comp_Stream 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))) = last_message (map output_fun (f_Exec_Comp_Stream 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 del: last.simps f_Exec_Comp_Stream.simps append_Cons)+
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>nat. \<lbrakk>0 < l; Exec_Equal_State localState trans_fun; \<forall>n\<le>Suc nat. State_Idle localState output_fun trans_fun (f_Exec_Comp_Stream_Acc_LocalState l localState trans_fun xs c ! n); Suc nat < length xs; l < k; xs \<noteq> []; i = Suc nat\<rbrakk> \<Longrightarrow> last_message (map output_fun (f_Exec_Comp_Stream trans_fun ((xs ! Suc nat # NoMsg\<^bsup>l - Suc 0\<^esup>) @ NoMsg\<^bsup>k - l\<^esup>) (f_Exec_Comp trans_fun (xs \<down> Suc nat \<odot> k) c))) = last_message (map output_fun (f_Exec_Comp_Stream trans_fun (xs ! Suc nat # NoMsg\<^bsup>l - Suc 0\<^esup>) (f_Exec_Comp trans_fun (xs \<down> Suc nat \<odot> l) c)))
[PROOF STEP]
apply (rename_tac n)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>0 < l; 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 xs c ! na); Suc n < length xs; l < k; xs \<noteq> []; i = Suc n\<rbrakk> \<Longrightarrow> last_message (map output_fun (f_Exec_Comp_Stream trans_fun ((xs ! Suc n # NoMsg\<^bsup>l - Suc 0\<^esup>) @ NoMsg\<^bsup>k - l\<^esup>) (f_Exec_Comp trans_fun (xs \<down> Suc n \<odot> k) c))) = last_message (map output_fun (f_Exec_Comp_Stream trans_fun (xs ! Suc n # NoMsg\<^bsup>l - Suc 0\<^esup>) (f_Exec_Comp trans_fun (xs \<down> Suc n \<odot> l) c)))
[PROOF STEP]
apply (simp only: f_Exec_Stream_append map_append last_message_append)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>0 < l; 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 xs c ! na); Suc n < length xs; l < k; xs \<noteq> []; i = Suc n\<rbrakk> \<Longrightarrow> (if last_message (map output_fun (f_Exec_Comp_Stream trans_fun NoMsg\<^bsup>k - l\<^esup> (f_Exec_Comp trans_fun (xs ! Suc n # NoMsg\<^bsup>l - Suc 0\<^esup>) (f_Exec_Comp trans_fun (xs \<down> Suc n \<odot> k) c)))) = NoMsg then last_message (map output_fun (f_Exec_Comp_Stream trans_fun (xs ! Suc n # NoMsg\<^bsup>l - Suc 0\<^esup>) (f_Exec_Comp trans_fun (xs \<down> Suc n \<odot> k) c))) else last_message (map output_fun (f_Exec_Comp_Stream trans_fun NoMsg\<^bsup>k - l\<^esup> (f_Exec_Comp trans_fun (xs ! Suc n # NoMsg\<^bsup>l - Suc 0\<^esup>) (f_Exec_Comp trans_fun (xs \<down> Suc n \<odot> k) c))))) = last_message (map output_fun (f_Exec_Comp_Stream trans_fun (xs ! Suc n # NoMsg\<^bsup>l - Suc 0\<^esup>) (f_Exec_Comp trans_fun (xs \<down> Suc n \<odot> l) c)))
[PROOF STEP]
apply (subgoal_tac "
  localState (f_Exec_Comp trans_fun (xs \<down> Suc n \<odot>\<^sub>f k) c) =
  localState (f_Exec_Comp trans_fun (xs \<down> Suc n \<odot>\<^sub>f l) c)")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>n. \<lbrakk>0 < l; 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 xs c ! na); Suc n < length xs; l < k; xs \<noteq> []; i = Suc n; localState (f_Exec_Comp trans_fun (xs \<down> Suc n \<odot> k) c) = localState (f_Exec_Comp trans_fun (xs \<down> Suc n \<odot> l) c)\<rbrakk> \<Longrightarrow> (if last_message (map output_fun (f_Exec_Comp_Stream trans_fun NoMsg\<^bsup>k - l\<^esup> (f_Exec_Comp trans_fun (xs ! Suc n # NoMsg\<^bsup>l - Suc 0\<^esup>) (f_Exec_Comp trans_fun (xs \<down> Suc n \<odot> k) c)))) = NoMsg then last_message (map output_fun (f_Exec_Comp_Stream trans_fun (xs ! Suc n # NoMsg\<^bsup>l - Suc 0\<^esup>) (f_Exec_Comp trans_fun (xs \<down> Suc n \<odot> k) c))) else last_message (map output_fun (f_Exec_Comp_Stream trans_fun NoMsg\<^bsup>k - l\<^esup> (f_Exec_Comp trans_fun (xs ! Suc n # NoMsg\<^bsup>l - Suc 0\<^esup>) (f_Exec_Comp trans_fun (xs \<down> Suc n \<odot> k) c))))) = last_message (map output_fun (f_Exec_Comp_Stream trans_fun (xs ! Suc n # NoMsg\<^bsup>l - Suc 0\<^esup>) (f_Exec_Comp trans_fun (xs \<down> Suc n \<odot> l) c)))
 2. \<And>n. \<lbrakk>0 < l; 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 xs c ! na); Suc n < length xs; l < k; xs \<noteq> []; i = Suc n\<rbrakk> \<Longrightarrow> localState (f_Exec_Comp trans_fun (xs \<down> Suc n \<odot> k) c) = localState (f_Exec_Comp trans_fun (xs \<down> Suc n \<odot> l) c)
[PROOF STEP]
prefer 2
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>n. \<lbrakk>0 < l; 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 xs c ! na); Suc n < length xs; l < k; xs \<noteq> []; i = Suc n\<rbrakk> \<Longrightarrow> localState (f_Exec_Comp trans_fun (xs \<down> Suc n \<odot> k) c) = localState (f_Exec_Comp trans_fun (xs \<down> Suc n \<odot> l) c)
 2. \<And>n. \<lbrakk>0 < l; 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 xs c ! na); Suc n < length xs; l < k; xs \<noteq> []; i = Suc n; localState (f_Exec_Comp trans_fun (xs \<down> Suc n \<odot> k) c) = localState (f_Exec_Comp trans_fun (xs \<down> Suc n \<odot> l) c)\<rbrakk> \<Longrightarrow> (if last_message (map output_fun (f_Exec_Comp_Stream trans_fun NoMsg\<^bsup>k - l\<^esup> (f_Exec_Comp trans_fun (xs ! Suc n # NoMsg\<^bsup>l - Suc 0\<^esup>) (f_Exec_Comp trans_fun (xs \<down> Suc n \<odot> k) c)))) = NoMsg then last_message (map output_fun (f_Exec_Comp_Stream trans_fun (xs ! Suc n # NoMsg\<^bsup>l - Suc 0\<^esup>) (f_Exec_Comp trans_fun (xs \<down> Suc n \<odot> k) c))) else last_message (map output_fun (f_Exec_Comp_Stream trans_fun NoMsg\<^bsup>k - l\<^esup> (f_Exec_Comp trans_fun (xs ! Suc n # NoMsg\<^bsup>l - Suc 0\<^esup>) (f_Exec_Comp trans_fun (xs \<down> Suc n \<odot> k) c))))) = last_message (map output_fun (f_Exec_Comp_Stream trans_fun (xs ! Suc n # NoMsg\<^bsup>l - Suc 0\<^esup>) (f_Exec_Comp trans_fun (xs \<down> Suc n \<odot> l) c)))
[PROOF STEP]
apply (simp add: f_Exec_Stream_Acc_LocalState_nth[symmetric])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>n. \<lbrakk>0 < l; 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 xs c ! na); Suc n < length xs; l < k; xs \<noteq> []; i = Suc n\<rbrakk> \<Longrightarrow> f_Exec_Comp_Stream_Acc_LocalState k localState trans_fun xs c ! n = f_Exec_Comp_Stream_Acc_LocalState l localState trans_fun xs c ! n
 2. \<And>n. \<lbrakk>0 < l; 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 xs c ! na); Suc n < length xs; l < k; xs \<noteq> []; i = Suc n; localState (f_Exec_Comp trans_fun (xs \<down> Suc n \<odot> k) c) = localState (f_Exec_Comp trans_fun (xs \<down> Suc n \<odot> l) c)\<rbrakk> \<Longrightarrow> (if last_message (map output_fun (f_Exec_Comp_Stream trans_fun NoMsg\<^bsup>k - l\<^esup> (f_Exec_Comp trans_fun (xs ! Suc n # NoMsg\<^bsup>l - Suc 0\<^esup>) (f_Exec_Comp trans_fun (xs \<down> Suc n \<odot> k) c)))) = NoMsg then last_message (map output_fun (f_Exec_Comp_Stream trans_fun (xs ! Suc n # NoMsg\<^bsup>l - Suc 0\<^esup>) (f_Exec_Comp trans_fun (xs \<down> Suc n \<odot> k) c))) else last_message (map output_fun (f_Exec_Comp_Stream trans_fun NoMsg\<^bsup>k - l\<^esup> (f_Exec_Comp trans_fun (xs ! Suc n # NoMsg\<^bsup>l - Suc 0\<^esup>) (f_Exec_Comp trans_fun (xs \<down> Suc n \<odot> k) c))))) = last_message (map output_fun (f_Exec_Comp_Stream trans_fun (xs ! Suc n # NoMsg\<^bsup>l - Suc 0\<^esup>) (f_Exec_Comp trans_fun (xs \<down> Suc n \<odot> l) c)))
[PROOF STEP]
apply (rule f_Exec_Stream_Acc_LocalState__State_Idle_nth)
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<And>n. \<lbrakk>0 < l; 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 xs c ! na); Suc n < length xs; l < k; xs \<noteq> []; i = Suc n\<rbrakk> \<Longrightarrow> 0 < l
 2. \<And>n. \<lbrakk>0 < l; 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 xs c ! na); Suc n < length xs; l < k; xs \<noteq> []; i = Suc n\<rbrakk> \<Longrightarrow> l \<le> k
 3. \<And>n. \<lbrakk>0 < l; 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 xs c ! na); Suc n < length xs; l < k; xs \<noteq> []; i = Suc n\<rbrakk> \<Longrightarrow> Exec_Equal_State localState trans_fun
 4. \<And>n na. \<lbrakk>0 < l; 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 xs c ! na); Suc n < length xs; l < k; xs \<noteq> []; i = Suc n; na \<le> n\<rbrakk> \<Longrightarrow> State_Idle localState (?output_fun25 n) trans_fun (f_Exec_Comp_Stream_Acc_LocalState l localState trans_fun xs c ! na)
 5. \<And>n. \<lbrakk>0 < l; 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 xs c ! na); Suc n < length xs; l < k; xs \<noteq> []; i = Suc n\<rbrakk> \<Longrightarrow> n < length xs
 6. \<And>n. \<lbrakk>0 < l; 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 xs c ! na); Suc n < length xs; l < k; xs \<noteq> []; i = Suc n; localState (f_Exec_Comp trans_fun (xs \<down> Suc n \<odot> k) c) = localState (f_Exec_Comp trans_fun (xs \<down> Suc n \<odot> l) c)\<rbrakk> \<Longrightarrow> (if last_message (map output_fun (f_Exec_Comp_Stream trans_fun NoMsg\<^bsup>k - l\<^esup> (f_Exec_Comp trans_fun (xs ! Suc n # NoMsg\<^bsup>l - Suc 0\<^esup>) (f_Exec_Comp trans_fun (xs \<down> Suc n \<odot> k) c)))) = NoMsg then last_message (map output_fun (f_Exec_Comp_Stream trans_fun (xs ! Suc n # NoMsg\<^bsup>l - Suc 0\<^esup>) (f_Exec_Comp trans_fun (xs \<down> Suc n \<odot> k) c))) else last_message (map output_fun (f_Exec_Comp_Stream trans_fun NoMsg\<^bsup>k - l\<^esup> (f_Exec_Comp trans_fun (xs ! Suc n # NoMsg\<^bsup>l - Suc 0\<^esup>) (f_Exec_Comp trans_fun (xs \<down> Suc n \<odot> k) c))))) = last_message (map output_fun (f_Exec_Comp_Stream trans_fun (xs ! Suc n # NoMsg\<^bsup>l - Suc 0\<^esup>) (f_Exec_Comp trans_fun (xs \<down> Suc n \<odot> l) c)))
[PROOF STEP]
apply simp+
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>n na. \<lbrakk>0 < l; 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 xs c ! na); Suc n < length xs; l < k; xs \<noteq> []; i = Suc n; na \<le> n\<rbrakk> \<Longrightarrow> State_Idle localState (?output_fun25 n) trans_fun (f_Exec_Comp_Stream_Acc_LocalState l localState trans_fun xs c ! na)
 2. \<And>n. \<lbrakk>0 < l; 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 xs c ! na); Suc n < length xs; l < k; xs \<noteq> []; i = Suc n\<rbrakk> \<Longrightarrow> n < length xs
 3. \<And>n. \<lbrakk>0 < l; 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 xs c ! na); Suc n < length xs; l < k; xs \<noteq> []; i = Suc n; localState (f_Exec_Comp trans_fun (xs \<down> Suc n \<odot> k) c) = localState (f_Exec_Comp trans_fun (xs \<down> Suc n \<odot> l) c)\<rbrakk> \<Longrightarrow> (if last_message (map output_fun (f_Exec_Comp_Stream trans_fun NoMsg\<^bsup>k - l\<^esup> (f_Exec_Comp trans_fun (xs ! Suc n # NoMsg\<^bsup>l - Suc 0\<^esup>) (f_Exec_Comp trans_fun (xs \<down> Suc n \<odot> k) c)))) = NoMsg then last_message (map output_fun (f_Exec_Comp_Stream trans_fun (xs ! Suc n # NoMsg\<^bsup>l - Suc 0\<^esup>) (f_Exec_Comp trans_fun (xs \<down> Suc n \<odot> k) c))) else last_message (map output_fun (f_Exec_Comp_Stream trans_fun NoMsg\<^bsup>k - l\<^esup> (f_Exec_Comp trans_fun (xs ! Suc n # NoMsg\<^bsup>l - Suc 0\<^esup>) (f_Exec_Comp trans_fun (xs \<down> Suc n \<odot> k) c))))) = last_message (map output_fun (f_Exec_Comp_Stream trans_fun (xs ! Suc n # NoMsg\<^bsup>l - Suc 0\<^esup>) (f_Exec_Comp trans_fun (xs \<down> Suc n \<odot> l) c)))
[PROOF STEP]
apply (rename_tac n, drule_tac x=n in spec, simp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>n. \<lbrakk>0 < l; 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 xs c ! na); Suc n < length xs; l < k; xs \<noteq> []; i = Suc n\<rbrakk> \<Longrightarrow> n < length xs
 2. \<And>n. \<lbrakk>0 < l; 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 xs c ! na); Suc n < length xs; l < k; xs \<noteq> []; i = Suc n; localState (f_Exec_Comp trans_fun (xs \<down> Suc n \<odot> k) c) = localState (f_Exec_Comp trans_fun (xs \<down> Suc n \<odot> l) c)\<rbrakk> \<Longrightarrow> (if last_message (map output_fun (f_Exec_Comp_Stream trans_fun NoMsg\<^bsup>k - l\<^esup> (f_Exec_Comp trans_fun (xs ! Suc n # NoMsg\<^bsup>l - Suc 0\<^esup>) (f_Exec_Comp trans_fun (xs \<down> Suc n \<odot> k) c)))) = NoMsg then last_message (map output_fun (f_Exec_Comp_Stream trans_fun (xs ! Suc n # NoMsg\<^bsup>l - Suc 0\<^esup>) (f_Exec_Comp trans_fun (xs \<down> Suc n \<odot> k) c))) else last_message (map output_fun (f_Exec_Comp_Stream trans_fun NoMsg\<^bsup>k - l\<^esup> (f_Exec_Comp trans_fun (xs ! Suc n # NoMsg\<^bsup>l - Suc 0\<^esup>) (f_Exec_Comp trans_fun (xs \<down> Suc n \<odot> k) c))))) = last_message (map output_fun (f_Exec_Comp_Stream trans_fun (xs ! Suc n # NoMsg\<^bsup>l - Suc 0\<^esup>) (f_Exec_Comp trans_fun (xs \<down> Suc n \<odot> l) c)))
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>0 < l; 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 xs c ! na); Suc n < length xs; l < k; xs \<noteq> []; i = Suc n; localState (f_Exec_Comp trans_fun (xs \<down> Suc n \<odot> k) c) = localState (f_Exec_Comp trans_fun (xs \<down> Suc n \<odot> l) c)\<rbrakk> \<Longrightarrow> (if last_message (map output_fun (f_Exec_Comp_Stream trans_fun NoMsg\<^bsup>k - l\<^esup> (f_Exec_Comp trans_fun (xs ! Suc n # NoMsg\<^bsup>l - Suc 0\<^esup>) (f_Exec_Comp trans_fun (xs \<down> Suc n \<odot> k) c)))) = NoMsg then last_message (map output_fun (f_Exec_Comp_Stream trans_fun (xs ! Suc n # NoMsg\<^bsup>l - Suc 0\<^esup>) (f_Exec_Comp trans_fun (xs \<down> Suc n \<odot> k) c))) else last_message (map output_fun (f_Exec_Comp_Stream trans_fun NoMsg\<^bsup>k - l\<^esup> (f_Exec_Comp trans_fun (xs ! Suc n # NoMsg\<^bsup>l - Suc 0\<^esup>) (f_Exec_Comp trans_fun (xs \<down> Suc n \<odot> k) c))))) = last_message (map output_fun (f_Exec_Comp_Stream trans_fun (xs ! Suc n # NoMsg\<^bsup>l - Suc 0\<^esup>) (f_Exec_Comp trans_fun (xs \<down> Suc n \<odot> l) c)))
[PROOF STEP]
apply (rule if_P')
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>n. \<lbrakk>0 < l; 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 xs c ! na); Suc n < length xs; l < k; xs \<noteq> []; i = Suc n; localState (f_Exec_Comp trans_fun (xs \<down> Suc n \<odot> k) c) = localState (f_Exec_Comp trans_fun (xs \<down> Suc n \<odot> l) c)\<rbrakk> \<Longrightarrow> last_message (map output_fun (f_Exec_Comp_Stream trans_fun NoMsg\<^bsup>k - l\<^esup> (f_Exec_Comp trans_fun (xs ! Suc n # NoMsg\<^bsup>l - Suc 0\<^esup>) (f_Exec_Comp trans_fun (xs \<down> Suc n \<odot> k) c)))) = NoMsg
 2. \<And>n. \<lbrakk>0 < l; 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 xs c ! na); Suc n < length xs; l < k; xs \<noteq> []; i = Suc n; localState (f_Exec_Comp trans_fun (xs \<down> Suc n \<odot> k) c) = localState (f_Exec_Comp trans_fun (xs \<down> Suc n \<odot> l) c)\<rbrakk> \<Longrightarrow> last_message (map output_fun (f_Exec_Comp_Stream trans_fun (xs ! Suc n # NoMsg\<^bsup>l - Suc 0\<^esup>) (f_Exec_Comp trans_fun (xs \<down> Suc n \<odot> k) c))) = last_message (map output_fun (f_Exec_Comp_Stream trans_fun (xs ! Suc n # NoMsg\<^bsup>l - Suc 0\<^esup>) (f_Exec_Comp trans_fun (xs \<down> Suc n \<odot> l) c)))
[PROOF STEP]
apply (simp add: last_message_NoMsg_conv f_Exec_Stream_nth min_eqL del: f_Exec_Comp.simps replicate.simps)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>n. \<lbrakk>0 < l; 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 xs c ! na); Suc n < length xs; l < k; xs \<noteq> []; i = Suc n; localState (f_Exec_Comp trans_fun (xs \<down> Suc n \<odot> k) c) = localState (f_Exec_Comp trans_fun (xs \<down> Suc n \<odot> l) c)\<rbrakk> \<Longrightarrow> \<forall>i<k - l. output_fun (f_Exec_Comp trans_fun NoMsg\<^bsup>Suc i\<^esup> (f_Exec_Comp trans_fun (xs ! Suc n # NoMsg\<^bsup>l - Suc 0\<^esup>) (f_Exec_Comp trans_fun (xs \<down> Suc n \<odot> k) c))) = NoMsg
 2. \<And>n. \<lbrakk>0 < l; 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 xs c ! na); Suc n < length xs; l < k; xs \<noteq> []; i = Suc n; localState (f_Exec_Comp trans_fun (xs \<down> Suc n \<odot> k) c) = localState (f_Exec_Comp trans_fun (xs \<down> Suc n \<odot> l) c)\<rbrakk> \<Longrightarrow> last_message (map output_fun (f_Exec_Comp_Stream trans_fun (xs ! Suc n # NoMsg\<^bsup>l - Suc 0\<^esup>) (f_Exec_Comp trans_fun (xs \<down> Suc n \<odot> k) c))) = last_message (map output_fun (f_Exec_Comp_Stream trans_fun (xs ! Suc n # NoMsg\<^bsup>l - Suc 0\<^esup>) (f_Exec_Comp trans_fun (xs \<down> Suc n \<odot> l) c)))
[PROOF STEP]
apply (clarify, rename_tac j)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>n j. \<lbrakk>0 < l; 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 xs c ! na); Suc n < length xs; l < k; xs \<noteq> []; i = Suc n; localState (f_Exec_Comp trans_fun (xs \<down> Suc n \<odot> k) c) = localState (f_Exec_Comp trans_fun (xs \<down> Suc n \<odot> l) c); j < k - l\<rbrakk> \<Longrightarrow> output_fun (f_Exec_Comp trans_fun NoMsg\<^bsup>Suc j\<^esup> (f_Exec_Comp trans_fun (xs ! Suc n # NoMsg\<^bsup>l - Suc 0\<^esup>) (f_Exec_Comp trans_fun (xs \<down> Suc n \<odot> k) c))) = NoMsg
 2. \<And>n. \<lbrakk>0 < l; 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 xs c ! na); Suc n < length xs; l < k; xs \<noteq> []; i = Suc n; localState (f_Exec_Comp trans_fun (xs \<down> Suc n \<odot> k) c) = localState (f_Exec_Comp trans_fun (xs \<down> Suc n \<odot> l) c)\<rbrakk> \<Longrightarrow> last_message (map output_fun (f_Exec_Comp_Stream trans_fun (xs ! Suc n # NoMsg\<^bsup>l - Suc 0\<^esup>) (f_Exec_Comp trans_fun (xs \<down> Suc n \<odot> k) c))) = last_message (map output_fun (f_Exec_Comp_Stream trans_fun (xs ! Suc n # NoMsg\<^bsup>l - Suc 0\<^esup>) (f_Exec_Comp trans_fun (xs \<down> Suc n \<odot> l) c)))
[PROOF STEP]
apply (frule_tac x="Suc n" in spec)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>n j. \<lbrakk>0 < l; 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 xs c ! na); Suc n < length xs; l < k; xs \<noteq> []; i = Suc n; localState (f_Exec_Comp trans_fun (xs \<down> Suc n \<odot> k) c) = localState (f_Exec_Comp trans_fun (xs \<down> Suc n \<odot> l) c); j < k - l; Suc n \<le> Suc n \<longrightarrow> State_Idle localState output_fun trans_fun (f_Exec_Comp_Stream_Acc_LocalState l localState trans_fun xs c ! Suc n)\<rbrakk> \<Longrightarrow> output_fun (f_Exec_Comp trans_fun NoMsg\<^bsup>Suc j\<^esup> (f_Exec_Comp trans_fun (xs ! Suc n # NoMsg\<^bsup>l - Suc 0\<^esup>) (f_Exec_Comp trans_fun (xs \<down> Suc n \<odot> k) c))) = NoMsg
 2. \<And>n. \<lbrakk>0 < l; 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 xs c ! na); Suc n < length xs; l < k; xs \<noteq> []; i = Suc n; localState (f_Exec_Comp trans_fun (xs \<down> Suc n \<odot> k) c) = localState (f_Exec_Comp trans_fun (xs \<down> Suc n \<odot> l) c)\<rbrakk> \<Longrightarrow> last_message (map output_fun (f_Exec_Comp_Stream trans_fun (xs ! Suc n # NoMsg\<^bsup>l - Suc 0\<^esup>) (f_Exec_Comp trans_fun (xs \<down> Suc n \<odot> k) c))) = last_message (map output_fun (f_Exec_Comp_Stream trans_fun (xs ! Suc n # NoMsg\<^bsup>l - Suc 0\<^esup>) (f_Exec_Comp trans_fun (xs \<down> Suc n \<odot> l) c)))
[PROOF STEP]
apply (simp only: f_Exec_Stream_Acc_LocalState_nth)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>n j. \<lbrakk>0 < l; 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 xs c ! na); Suc n < length xs; l < k; xs \<noteq> []; i = Suc n; localState (f_Exec_Comp trans_fun (xs \<down> Suc n \<odot> k) c) = localState (f_Exec_Comp trans_fun (xs \<down> Suc n \<odot> l) c); j < k - l; Suc n \<le> Suc n \<longrightarrow> State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun (xs \<down> Suc (Suc n) \<odot> l) c))\<rbrakk> \<Longrightarrow> output_fun (f_Exec_Comp trans_fun NoMsg\<^bsup>Suc j\<^esup> (f_Exec_Comp trans_fun (xs ! Suc n # NoMsg\<^bsup>l - Suc 0\<^esup>) (f_Exec_Comp trans_fun (xs \<down> Suc n \<odot> k) c))) = NoMsg
 2. \<And>n. \<lbrakk>0 < l; 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 xs c ! na); Suc n < length xs; l < k; xs \<noteq> []; i = Suc n; localState (f_Exec_Comp trans_fun (xs \<down> Suc n \<odot> k) c) = localState (f_Exec_Comp trans_fun (xs \<down> Suc n \<odot> l) c)\<rbrakk> \<Longrightarrow> last_message (map output_fun (f_Exec_Comp_Stream trans_fun (xs ! Suc n # NoMsg\<^bsup>l - Suc 0\<^esup>) (f_Exec_Comp trans_fun (xs \<down> Suc n \<odot> k) c))) = last_message (map output_fun (f_Exec_Comp_Stream trans_fun (xs ! Suc n # NoMsg\<^bsup>l - Suc 0\<^esup>) (f_Exec_Comp trans_fun (xs \<down> Suc n \<odot> l) c)))
[PROOF STEP]
apply (rule_tac
   ?c1.0="f_Exec_Comp trans_fun (xs \<down> Suc n \<odot>\<^sub>f l) c"
   and ?c2.0="f_Exec_Comp trans_fun (xs \<down> Suc n \<odot>\<^sub>f k) c"
   in subst[OF f_Exec_Equal_State, rule_format])
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>n j. \<lbrakk>0 < l; 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 xs c ! na); Suc n < length xs; l < k; xs \<noteq> []; i = Suc n; localState (f_Exec_Comp trans_fun (xs \<down> Suc n \<odot> k) c) = localState (f_Exec_Comp trans_fun (xs \<down> Suc n \<odot> l) c); j < k - l; Suc n \<le> Suc n \<longrightarrow> State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun (xs \<down> Suc (Suc n) \<odot> l) c))\<rbrakk> \<Longrightarrow> Exec_Equal_State (?localState42 n j) trans_fun
 2. \<And>n j. \<lbrakk>0 < l; 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 xs c ! na); Suc n < length xs; l < k; xs \<noteq> []; i = Suc n; localState (f_Exec_Comp trans_fun (xs \<down> Suc n \<odot> k) c) = localState (f_Exec_Comp trans_fun (xs \<down> Suc n \<odot> l) c); j < k - l; Suc n \<le> Suc n \<longrightarrow> State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun (xs \<down> Suc (Suc n) \<odot> l) c))\<rbrakk> \<Longrightarrow> ?localState42 n j (f_Exec_Comp trans_fun (xs \<down> Suc n \<odot> l) c) = ?localState42 n j (f_Exec_Comp trans_fun (xs \<down> Suc n \<odot> k) c)
 3. \<And>n j. \<lbrakk>0 < l; 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 xs c ! na); Suc n < length xs; l < k; xs \<noteq> []; i = Suc n; localState (f_Exec_Comp trans_fun (xs \<down> Suc n \<odot> k) c) = localState (f_Exec_Comp trans_fun (xs \<down> Suc n \<odot> l) c); j < k - l; Suc n \<le> Suc n \<longrightarrow> State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun (xs \<down> Suc (Suc n) \<odot> l) c))\<rbrakk> \<Longrightarrow> xs ! Suc n # NoMsg\<^bsup>l - Suc 0\<^esup> \<noteq> []
 4. \<And>n j. \<lbrakk>0 < l; 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 xs c ! na); Suc n < length xs; l < k; xs \<noteq> []; i = Suc n; localState (f_Exec_Comp trans_fun (xs \<down> Suc n \<odot> k) c) = localState (f_Exec_Comp trans_fun (xs \<down> Suc n \<odot> l) c); j < k - l; Suc n \<le> Suc n \<longrightarrow> State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun (xs \<down> Suc (Suc n) \<odot> l) c))\<rbrakk> \<Longrightarrow> output_fun (f_Exec_Comp trans_fun NoMsg\<^bsup>Suc j\<^esup> (f_Exec_Comp trans_fun (xs ! Suc n # NoMsg\<^bsup>l - Suc 0\<^esup>) (f_Exec_Comp trans_fun (xs \<down> Suc n \<odot> l) c))) = NoMsg
 5. \<And>n. \<lbrakk>0 < l; 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 xs c ! na); Suc n < length xs; l < k; xs \<noteq> []; i = Suc n; localState (f_Exec_Comp trans_fun (xs \<down> Suc n \<odot> k) c) = localState (f_Exec_Comp trans_fun (xs \<down> Suc n \<odot> l) c)\<rbrakk> \<Longrightarrow> last_message (map output_fun (f_Exec_Comp_Stream trans_fun (xs ! Suc n # NoMsg\<^bsup>l - Suc 0\<^esup>) (f_Exec_Comp trans_fun (xs \<down> Suc n \<odot> k) c))) = last_message (map output_fun (f_Exec_Comp_Stream trans_fun (xs ! Suc n # NoMsg\<^bsup>l - Suc 0\<^esup>) (f_Exec_Comp trans_fun (xs \<down> Suc n \<odot> l) c)))
[PROOF STEP]
apply (simp del: f_Exec_Comp.simps replicate.simps)+
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>n j. \<lbrakk>0 < l; 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 xs c ! na); Suc n < length xs; l < k; xs \<noteq> []; i = Suc n; localState (f_Exec_Comp trans_fun (xs \<down> Suc n \<odot> k) c) = localState (f_Exec_Comp trans_fun (xs \<down> Suc n \<odot> l) c); j < k - l; State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun (xs \<down> Suc (Suc n) \<odot> l) c))\<rbrakk> \<Longrightarrow> output_fun (f_Exec_Comp trans_fun NoMsg\<^bsup>Suc j\<^esup> (f_Exec_Comp trans_fun (xs ! Suc n # NoMsg\<^bsup>l - Suc 0\<^esup>) (f_Exec_Comp trans_fun (xs \<down> Suc n \<odot> l) c))) = NoMsg
 2. \<And>n. \<lbrakk>0 < l; 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 xs c ! na); Suc n < length xs; l < k; xs \<noteq> []; i = Suc n; localState (f_Exec_Comp trans_fun (xs \<down> Suc n \<odot> k) c) = localState (f_Exec_Comp trans_fun (xs \<down> Suc n \<odot> l) c)\<rbrakk> \<Longrightarrow> last_message (map output_fun (f_Exec_Comp_Stream trans_fun (xs ! Suc n # NoMsg\<^bsup>l - Suc 0\<^esup>) (f_Exec_Comp trans_fun (xs \<down> Suc n \<odot> k) c))) = last_message (map output_fun (f_Exec_Comp_Stream trans_fun (xs ! Suc n # NoMsg\<^bsup>l - Suc 0\<^esup>) (f_Exec_Comp trans_fun (xs \<down> Suc n \<odot> l) c)))
[PROOF STEP]
apply (simp only: take_Suc_conv_app_nth f_expand_snoc f_Exec_append)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>n j. \<lbrakk>0 < l; 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 xs c ! na); Suc n < length xs; l < k; xs \<noteq> []; i = Suc n; localState (f_Exec_Comp trans_fun (xs ! n # NoMsg\<^bsup>k - Suc 0\<^esup>) (f_Exec_Comp trans_fun (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 (xs \<down> n \<odot> l) c)); j < k - l; State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun (xs ! Suc n # NoMsg\<^bsup>l - Suc 0\<^esup>) (f_Exec_Comp trans_fun (xs ! n # NoMsg\<^bsup>l - Suc 0\<^esup>) (f_Exec_Comp trans_fun (xs \<down> n \<odot> l) c))))\<rbrakk> \<Longrightarrow> output_fun (f_Exec_Comp trans_fun NoMsg\<^bsup>Suc j\<^esup> (f_Exec_Comp trans_fun (xs ! Suc n # NoMsg\<^bsup>l - Suc 0\<^esup>) (f_Exec_Comp trans_fun (xs ! n # NoMsg\<^bsup>l - Suc 0\<^esup>) (f_Exec_Comp trans_fun (xs \<down> n \<odot> l) c)))) = NoMsg
 2. \<And>n. \<lbrakk>0 < l; 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 xs c ! na); Suc n < length xs; l < k; xs \<noteq> []; i = Suc n; localState (f_Exec_Comp trans_fun (xs \<down> Suc n \<odot> k) c) = localState (f_Exec_Comp trans_fun (xs \<down> Suc n \<odot> l) c)\<rbrakk> \<Longrightarrow> last_message (map output_fun (f_Exec_Comp_Stream trans_fun (xs ! Suc n # NoMsg\<^bsup>l - Suc 0\<^esup>) (f_Exec_Comp trans_fun (xs \<down> Suc n \<odot> k) c))) = last_message (map output_fun (f_Exec_Comp_Stream trans_fun (xs ! Suc n # NoMsg\<^bsup>l - Suc 0\<^esup>) (f_Exec_Comp trans_fun (xs \<down> Suc n \<odot> l) c)))
[PROOF STEP]
apply (rule f_Exec_State_Idle_replicate_NoMsg_gr0_output, assumption)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>n j. \<lbrakk>0 < l; 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 xs c ! na); Suc n < length xs; l < k; xs \<noteq> []; i = Suc n; localState (f_Exec_Comp trans_fun (xs ! n # NoMsg\<^bsup>k - Suc 0\<^esup>) (f_Exec_Comp trans_fun (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 (xs \<down> n \<odot> l) c)); j < k - l; State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun (xs ! Suc n # NoMsg\<^bsup>l - Suc 0\<^esup>) (f_Exec_Comp trans_fun (xs ! n # NoMsg\<^bsup>l - Suc 0\<^esup>) (f_Exec_Comp trans_fun (xs \<down> n \<odot> l) c))))\<rbrakk> \<Longrightarrow> 0 < Suc j
 2. \<And>n. \<lbrakk>0 < l; 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 xs c ! na); Suc n < length xs; l < k; xs \<noteq> []; i = Suc n; localState (f_Exec_Comp trans_fun (xs \<down> Suc n \<odot> k) c) = localState (f_Exec_Comp trans_fun (xs \<down> Suc n \<odot> l) c)\<rbrakk> \<Longrightarrow> last_message (map output_fun (f_Exec_Comp_Stream trans_fun (xs ! Suc n # NoMsg\<^bsup>l - Suc 0\<^esup>) (f_Exec_Comp trans_fun (xs \<down> Suc n \<odot> k) c))) = last_message (map output_fun (f_Exec_Comp_Stream trans_fun (xs ! Suc n # NoMsg\<^bsup>l - Suc 0\<^esup>) (f_Exec_Comp trans_fun (xs \<down> Suc n \<odot> l) c)))
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>0 < l; 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 xs c ! na); Suc n < length xs; l < k; xs \<noteq> []; i = Suc n; localState (f_Exec_Comp trans_fun (xs \<down> Suc n \<odot> k) c) = localState (f_Exec_Comp trans_fun (xs \<down> Suc n \<odot> l) c)\<rbrakk> \<Longrightarrow> last_message (map output_fun (f_Exec_Comp_Stream trans_fun (xs ! Suc n # NoMsg\<^bsup>l - Suc 0\<^esup>) (f_Exec_Comp trans_fun (xs \<down> Suc n \<odot> k) c))) = last_message (map output_fun (f_Exec_Comp_Stream trans_fun (xs ! Suc n # NoMsg\<^bsup>l - Suc 0\<^esup>) (f_Exec_Comp trans_fun (xs \<down> Suc n \<odot> l) c)))
[PROOF STEP]
apply (rule arg_cong[where f="\<lambda>x. last_message (map output_fun x)"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>0 < l; 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 xs c ! na); Suc n < length xs; l < k; xs \<noteq> []; i = Suc n; localState (f_Exec_Comp trans_fun (xs \<down> Suc n \<odot> k) c) = localState (f_Exec_Comp trans_fun (xs \<down> Suc n \<odot> l) c)\<rbrakk> \<Longrightarrow> f_Exec_Comp_Stream trans_fun (xs ! Suc n # NoMsg\<^bsup>l - Suc 0\<^esup>) (f_Exec_Comp trans_fun (xs \<down> Suc n \<odot> k) c) = f_Exec_Comp_Stream trans_fun (xs ! Suc n # NoMsg\<^bsup>l - Suc 0\<^esup>) (f_Exec_Comp trans_fun (xs \<down> Suc n \<odot> l) c)
[PROOF STEP]
apply (rule f_Exec_Stream_Equal_State, assumption+)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma f_Exec_Stream_Acc_Output__State_Idle_eq[rule_format]: "
  \<lbrakk> 0 < l; l \<le> k; Exec_Equal_State localState trans_fun;
    \<forall>n<length xs. State_Idle localState output_fun trans_fun (
      f_Exec_Comp_Stream_Acc_LocalState l localState trans_fun xs c ! n) \<rbrakk> \<Longrightarrow>
  f_Exec_Comp_Stream_Acc_Output k output_fun trans_fun xs c =
  f_Exec_Comp_Stream_Acc_Output l output_fun trans_fun xs c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < l; l \<le> k; Exec_Equal_State localState trans_fun; \<forall>n<length xs. State_Idle localState output_fun trans_fun (f_Exec_Comp_Stream_Acc_LocalState l localState trans_fun xs c ! n)\<rbrakk> \<Longrightarrow> f_Exec_Comp_Stream_Acc_Output k output_fun trans_fun xs c = f_Exec_Comp_Stream_Acc_Output l output_fun trans_fun xs c
[PROOF STEP]
apply (clarsimp simp: list_eq_iff)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i. \<lbrakk>0 < l; l \<le> k; Exec_Equal_State localState trans_fun; \<forall>n<length xs. 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_Output k output_fun trans_fun xs c ! i = f_Exec_Comp_Stream_Acc_Output l output_fun trans_fun xs c ! i
[PROOF STEP]
apply (rule f_Exec_Stream_Acc_Output__State_Idle_nth)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>i. \<lbrakk>0 < l; l \<le> k; Exec_Equal_State localState trans_fun; \<forall>n<length xs. 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> 0 < l
 2. \<And>i. \<lbrakk>0 < l; l \<le> k; Exec_Equal_State localState trans_fun; \<forall>n<length xs. 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> l \<le> k
 3. \<And>i. \<lbrakk>0 < l; l \<le> k; Exec_Equal_State localState trans_fun; \<forall>n<length xs. 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> Exec_Equal_State (?localState12 i) trans_fun
 4. \<And>i n. \<lbrakk>0 < l; l \<le> k; Exec_Equal_State localState trans_fun; \<forall>n<length xs. State_Idle localState output_fun trans_fun (f_Exec_Comp_Stream_Acc_LocalState l localState trans_fun xs c ! n); i < length xs; n \<le> i\<rbrakk> \<Longrightarrow> State_Idle (?localState12 i) output_fun trans_fun (f_Exec_Comp_Stream_Acc_LocalState l (?localState12 i) trans_fun xs c ! n)
 5. \<And>i. \<lbrakk>0 < l; l \<le> k; Exec_Equal_State localState trans_fun; \<forall>n<length xs. 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> i < length xs
[PROOF STEP]
apply simp_all
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i n. \<lbrakk>0 < l; l \<le> k; Exec_Equal_State localState trans_fun; \<forall>n<length xs. State_Idle localState output_fun trans_fun (f_Exec_Comp_Stream_Acc_LocalState l localState trans_fun xs c ! n); i < length xs; n \<le> i\<rbrakk> \<Longrightarrow> State_Idle localState output_fun trans_fun (f_Exec_Comp_Stream_Acc_LocalState l localState trans_fun xs c ! n)
[PROOF STEP]
apply (drule_tac x=n in spec)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i n. \<lbrakk>0 < l; l \<le> k; Exec_Equal_State localState trans_fun; i < length xs; n \<le> i; n < length xs \<longrightarrow> State_Idle localState output_fun trans_fun (f_Exec_Comp_Stream_Acc_LocalState l localState trans_fun xs c ! n)\<rbrakk> \<Longrightarrow> State_Idle localState output_fun trans_fun (f_Exec_Comp_Stream_Acc_LocalState l localState trans_fun xs c ! n)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma i_Exec_Stream_Acc_Output__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_Output k output_fun trans_fun input c i =
  i_Exec_Comp_Stream_Acc_Output l output_fun 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_Output k output_fun trans_fun input c i = i_Exec_Comp_Stream_Acc_Output l output_fun trans_fun input c i
[PROOF STEP]
apply (simp only: i_Exec_Stream_Acc_Output_nth_f_nth)
[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_Output k output_fun trans_fun (input \<Down> Suc i) c ! i = f_Exec_Comp_Stream_Acc_Output l output_fun trans_fun (input \<Down> Suc i) c ! i
[PROOF STEP]
apply (rule f_Exec_Stream_Acc_Output__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 ?localState8 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 ?localState8 output_fun trans_fun (f_Exec_Comp_Stream_Acc_LocalState l ?localState8 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_fun 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_fun 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


[STATEMENT]
lemma i_Exec_Stream_Acc_Output__State_Idle_eq[rule_format]: "
  \<lbrakk> 0 < l; l \<le> k; Exec_Equal_State localState trans_fun;
    \<forall>n. 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_Output k output_fun trans_fun input c =
  i_Exec_Comp_Stream_Acc_Output l output_fun trans_fun input c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < l; l \<le> k; Exec_Equal_State localState trans_fun; \<forall>n. 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_Output k output_fun trans_fun input c = i_Exec_Comp_Stream_Acc_Output l output_fun trans_fun input c
[PROOF STEP]
apply (clarsimp simp: ilist_eq_iff)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>0 < l; l \<le> k; Exec_Equal_State localState trans_fun; \<forall>n. 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_Output k output_fun trans_fun input c x = i_Exec_Comp_Stream_Acc_Output l output_fun trans_fun input c x
[PROOF STEP]
apply (rule i_Exec_Stream_Acc_Output__State_Idle_nth)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>x. \<lbrakk>0 < l; l \<le> k; Exec_Equal_State localState trans_fun; \<forall>n. 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. \<And>x. \<lbrakk>0 < l; l \<le> k; Exec_Equal_State localState trans_fun; \<forall>n. 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. \<And>x. \<lbrakk>0 < l; l \<le> k; Exec_Equal_State localState trans_fun; \<forall>n. 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 (?localState1 x) trans_fun
 4. \<And>x n. \<lbrakk>0 < l; l \<le> k; Exec_Equal_State localState trans_fun; \<forall>n. State_Idle localState output_fun trans_fun (i_Exec_Comp_Stream_Acc_LocalState l localState trans_fun input c n); n \<le> x\<rbrakk> \<Longrightarrow> State_Idle (?localState1 x) output_fun trans_fun (i_Exec_Comp_Stream_Acc_LocalState l (?localState1 x) trans_fun input c n)
[PROOF STEP]
apply simp_all
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x n. \<lbrakk>0 < l; l \<le> k; Exec_Equal_State localState trans_fun; \<forall>n. State_Idle localState output_fun trans_fun (i_Exec_Comp_Stream_Acc_LocalState l localState trans_fun input c n); n \<le> x\<rbrakk> \<Longrightarrow> State_Idle localState output_fun trans_fun (i_Exec_Comp_Stream_Acc_LocalState l localState trans_fun input c n)
[PROOF STEP]
apply (drule_tac x=n in spec)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x n. \<lbrakk>0 < l; l \<le> k; Exec_Equal_State localState trans_fun; n \<le> x; 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_fun trans_fun (i_Exec_Comp_Stream_Acc_LocalState l localState trans_fun input c n)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma f_Exec_Stream_Acc_LocalState__State_Idle_all[rule_format]: "
  \<And>c xs. \<lbrakk> 0 < l; l \<le> k;
    State_Idle localState output_fun trans_fun (localState c);
    \<forall>c m. State_Idle localState output_fun trans_fun (localState c) \<longrightarrow>
      State_Idle localState output_fun trans_fun (
        localState (f_Exec_Comp trans_fun (m # \<NoMsg>\<^bsup>l - Suc 0\<^esup>) c));
    i < length xs \<rbrakk> \<Longrightarrow>
  State_Idle localState output_fun trans_fun (
    f_Exec_Comp_Stream_Acc_LocalState k localState trans_fun xs c ! i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>c xs. \<lbrakk>0 < l; l \<le> k; State_Idle localState output_fun trans_fun (localState c); \<forall>c m. State_Idle localState output_fun trans_fun (localState c) \<longrightarrow> State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun (m # NoMsg\<^bsup>l - Suc 0\<^esup>) c)); i < length xs\<rbrakk> \<Longrightarrow> State_Idle localState output_fun trans_fun (f_Exec_Comp_Stream_Acc_LocalState k localState trans_fun xs c ! i)
[PROOF STEP]
apply (frule length_greater_imp_not_empty)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>c xs. \<lbrakk>0 < l; l \<le> k; State_Idle localState output_fun trans_fun (localState c); \<forall>c m. State_Idle localState output_fun trans_fun (localState c) \<longrightarrow> State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun (m # NoMsg\<^bsup>l - Suc 0\<^esup>) c)); i < length xs; xs \<noteq> []\<rbrakk> \<Longrightarrow> State_Idle localState output_fun trans_fun (f_Exec_Comp_Stream_Acc_LocalState k localState trans_fun xs c ! i)
[PROOF STEP]
apply (subgoal_tac "
  State_Idle localState output_fun trans_fun (
    localState (f_Exec_Comp trans_fun (hd xs # NoMsg\<^bsup>k - Suc 0\<^esup>) c))")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>c xs. \<lbrakk>0 < l; l \<le> k; State_Idle localState output_fun trans_fun (localState c); \<forall>c m. State_Idle localState output_fun trans_fun (localState c) \<longrightarrow> State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun (m # NoMsg\<^bsup>l - Suc 0\<^esup>) c)); i < length xs; xs \<noteq> []; State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun (hd xs # NoMsg\<^bsup>k - Suc 0\<^esup>) c))\<rbrakk> \<Longrightarrow> State_Idle localState output_fun trans_fun (f_Exec_Comp_Stream_Acc_LocalState k localState trans_fun xs c ! i)
 2. \<And>c xs. \<lbrakk>0 < l; l \<le> k; State_Idle localState output_fun trans_fun (localState c); \<forall>c m. State_Idle localState output_fun trans_fun (localState c) \<longrightarrow> State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun (m # NoMsg\<^bsup>l - Suc 0\<^esup>) c)); i < length xs; xs \<noteq> []\<rbrakk> \<Longrightarrow> State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun (hd xs # NoMsg\<^bsup>k - Suc 0\<^esup>) c))
[PROOF STEP]
prefer 2
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>c xs. \<lbrakk>0 < l; l \<le> k; State_Idle localState output_fun trans_fun (localState c); \<forall>c m. State_Idle localState output_fun trans_fun (localState c) \<longrightarrow> State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun (m # NoMsg\<^bsup>l - Suc 0\<^esup>) c)); i < length xs; xs \<noteq> []\<rbrakk> \<Longrightarrow> State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun (hd xs # NoMsg\<^bsup>k - Suc 0\<^esup>) c))
 2. \<And>c xs. \<lbrakk>0 < l; l \<le> k; State_Idle localState output_fun trans_fun (localState c); \<forall>c m. State_Idle localState output_fun trans_fun (localState c) \<longrightarrow> State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun (m # NoMsg\<^bsup>l - Suc 0\<^esup>) c)); i < length xs; xs \<noteq> []; State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun (hd xs # NoMsg\<^bsup>k - Suc 0\<^esup>) c))\<rbrakk> \<Longrightarrow> State_Idle localState output_fun trans_fun (f_Exec_Comp_Stream_Acc_LocalState k localState trans_fun xs c ! i)
[PROOF STEP]
apply (drule_tac x=c in spec, drule_tac x="hd xs" in spec)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>c xs. \<lbrakk>0 < l; l \<le> k; State_Idle localState output_fun trans_fun (localState c); i < length xs; xs \<noteq> []; State_Idle localState output_fun trans_fun (localState c) \<longrightarrow> State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun (hd xs # NoMsg\<^bsup>l - Suc 0\<^esup>) c))\<rbrakk> \<Longrightarrow> State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun (hd xs # NoMsg\<^bsup>k - Suc 0\<^esup>) c))
 2. \<And>c xs. \<lbrakk>0 < l; l \<le> k; State_Idle localState output_fun trans_fun (localState c); \<forall>c m. State_Idle localState output_fun trans_fun (localState c) \<longrightarrow> State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun (m # NoMsg\<^bsup>l - Suc 0\<^esup>) c)); i < length xs; xs \<noteq> []; State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun (hd xs # NoMsg\<^bsup>k - Suc 0\<^esup>) c))\<rbrakk> \<Longrightarrow> State_Idle localState output_fun trans_fun (f_Exec_Comp_Stream_Acc_LocalState k localState trans_fun xs c ! i)
[PROOF STEP]
apply (rule subst[OF replicate_le_diff2[OF Suc_leI], of 0 l k], assumption+)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>c xs. \<lbrakk>0 < l; l \<le> k; State_Idle localState output_fun trans_fun (localState c); i < length xs; xs \<noteq> []; State_Idle localState output_fun trans_fun (localState c) \<longrightarrow> State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun (hd xs # NoMsg\<^bsup>l - Suc 0\<^esup>) c))\<rbrakk> \<Longrightarrow> State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun (hd xs # NoMsg\<^bsup>l - Suc 0\<^esup> @ NoMsg\<^bsup>k - l\<^esup>) c))
 2. \<And>c xs. \<lbrakk>0 < l; l \<le> k; State_Idle localState output_fun trans_fun (localState c); \<forall>c m. State_Idle localState output_fun trans_fun (localState c) \<longrightarrow> State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun (m # NoMsg\<^bsup>l - Suc 0\<^esup>) c)); i < length xs; xs \<noteq> []; State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun (hd xs # NoMsg\<^bsup>k - Suc 0\<^esup>) c))\<rbrakk> \<Longrightarrow> State_Idle localState output_fun trans_fun (f_Exec_Comp_Stream_Acc_LocalState k localState trans_fun xs c ! i)
[PROOF STEP]
apply (simp add: f_Exec_append f_Exec_State_Idle_replicate_NoMsg_state)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>c xs. \<lbrakk>0 < l; l \<le> k; State_Idle localState output_fun trans_fun (localState c); \<forall>c m. State_Idle localState output_fun trans_fun (localState c) \<longrightarrow> State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun (m # NoMsg\<^bsup>l - Suc 0\<^esup>) c)); i < length xs; xs \<noteq> []; State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun (hd xs # NoMsg\<^bsup>k - Suc 0\<^esup>) c))\<rbrakk> \<Longrightarrow> State_Idle localState output_fun trans_fun (f_Exec_Comp_Stream_Acc_LocalState k localState trans_fun xs c ! i)
[PROOF STEP]
apply (induct i)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>c xs. \<lbrakk>0 < l; l \<le> k; State_Idle localState output_fun trans_fun (localState c); \<forall>c m. State_Idle localState output_fun trans_fun (localState c) \<longrightarrow> State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun (m # NoMsg\<^bsup>l - Suc 0\<^esup>) c)); 0 < length xs; xs \<noteq> []; State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun (hd xs # NoMsg\<^bsup>k - Suc 0\<^esup>) c))\<rbrakk> \<Longrightarrow> State_Idle localState output_fun trans_fun (f_Exec_Comp_Stream_Acc_LocalState k localState trans_fun xs c ! 0)
 2. \<And>i c xs. \<lbrakk>\<And>c xs. \<lbrakk>0 < l; l \<le> k; State_Idle localState output_fun trans_fun (localState c); \<forall>c m. State_Idle localState output_fun trans_fun (localState c) \<longrightarrow> State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun (m # NoMsg\<^bsup>l - Suc 0\<^esup>) c)); i < length xs; xs \<noteq> []; State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun (hd xs # NoMsg\<^bsup>k - Suc 0\<^esup>) c))\<rbrakk> \<Longrightarrow> State_Idle localState output_fun trans_fun (f_Exec_Comp_Stream_Acc_LocalState k localState trans_fun xs c ! i); 0 < l; l \<le> k; State_Idle localState output_fun trans_fun (localState c); \<forall>c m. State_Idle localState output_fun trans_fun (localState c) \<longrightarrow> State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun (m # NoMsg\<^bsup>l - Suc 0\<^esup>) c)); Suc i < length xs; xs \<noteq> []; State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun (hd xs # NoMsg\<^bsup>k - Suc 0\<^esup>) c))\<rbrakk> \<Longrightarrow> State_Idle localState output_fun trans_fun (f_Exec_Comp_Stream_Acc_LocalState k localState trans_fun xs c ! Suc i)
[PROOF STEP]
apply (simp add: f_Exec_Stream_Acc_LocalState_nth take_first hd_eq_first)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i c xs. \<lbrakk>\<And>c xs. \<lbrakk>0 < l; l \<le> k; State_Idle localState output_fun trans_fun (localState c); \<forall>c m. State_Idle localState output_fun trans_fun (localState c) \<longrightarrow> State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun (m # NoMsg\<^bsup>l - Suc 0\<^esup>) c)); i < length xs; xs \<noteq> []; State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun (hd xs # NoMsg\<^bsup>k - Suc 0\<^esup>) c))\<rbrakk> \<Longrightarrow> State_Idle localState output_fun trans_fun (f_Exec_Comp_Stream_Acc_LocalState k localState trans_fun xs c ! i); 0 < l; l \<le> k; State_Idle localState output_fun trans_fun (localState c); \<forall>c m. State_Idle localState output_fun trans_fun (localState c) \<longrightarrow> State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun (m # NoMsg\<^bsup>l - Suc 0\<^esup>) c)); Suc i < length xs; xs \<noteq> []; State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun (hd xs # NoMsg\<^bsup>k - Suc 0\<^esup>) c))\<rbrakk> \<Longrightarrow> State_Idle localState output_fun trans_fun (f_Exec_Comp_Stream_Acc_LocalState k localState trans_fun xs c ! Suc i)
[PROOF STEP]
apply (drule_tac x="f_Exec_Comp trans_fun (hd xs # NoMsg\<^bsup>k - Suc 0\<^esup>) c" in meta_spec)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i c xs. \<lbrakk>0 < l; l \<le> k; State_Idle localState output_fun trans_fun (localState c); \<forall>c m. State_Idle localState output_fun trans_fun (localState c) \<longrightarrow> State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun (m # NoMsg\<^bsup>l - Suc 0\<^esup>) c)); Suc i < length xs; xs \<noteq> []; State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun (hd xs # NoMsg\<^bsup>k - Suc 0\<^esup>) c)); \<And>xsa. \<lbrakk>0 < l; l \<le> k; State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun (hd xs # NoMsg\<^bsup>k - Suc 0\<^esup>) c)); \<forall>c m. State_Idle localState output_fun trans_fun (localState c) \<longrightarrow> State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun (m # NoMsg\<^bsup>l - Suc 0\<^esup>) c)); i < length xsa; xsa \<noteq> []; State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun (hd xsa # NoMsg\<^bsup>k - Suc 0\<^esup>) (f_Exec_Comp trans_fun (hd xs # NoMsg\<^bsup>k - Suc 0\<^esup>) c)))\<rbrakk> \<Longrightarrow> State_Idle localState output_fun trans_fun (f_Exec_Comp_Stream_Acc_LocalState k localState trans_fun xsa (f_Exec_Comp trans_fun (hd xs # NoMsg\<^bsup>k - Suc 0\<^esup>) c) ! i)\<rbrakk> \<Longrightarrow> State_Idle localState output_fun trans_fun (f_Exec_Comp_Stream_Acc_LocalState k localState trans_fun xs c ! Suc i)
[PROOF STEP]
apply (drule_tac x="tl xs" in meta_spec)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i c xs. \<lbrakk>0 < l; l \<le> k; State_Idle localState output_fun trans_fun (localState c); \<forall>c m. State_Idle localState output_fun trans_fun (localState c) \<longrightarrow> State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun (m # NoMsg\<^bsup>l - Suc 0\<^esup>) c)); Suc i < length xs; xs \<noteq> []; State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun (hd xs # NoMsg\<^bsup>k - Suc 0\<^esup>) c)); \<lbrakk>0 < l; l \<le> k; State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun (hd xs # NoMsg\<^bsup>k - Suc 0\<^esup>) c)); \<forall>c m. State_Idle localState output_fun trans_fun (localState c) \<longrightarrow> State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun (m # NoMsg\<^bsup>l - Suc 0\<^esup>) c)); i < length (tl xs); tl xs \<noteq> []; State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun (hd (tl xs) # NoMsg\<^bsup>k - Suc 0\<^esup>) (f_Exec_Comp trans_fun (hd xs # NoMsg\<^bsup>k - Suc 0\<^esup>) c)))\<rbrakk> \<Longrightarrow> State_Idle localState output_fun trans_fun (f_Exec_Comp_Stream_Acc_LocalState k localState trans_fun (tl xs) (f_Exec_Comp trans_fun (hd xs # NoMsg\<^bsup>k - Suc 0\<^esup>) c) ! i)\<rbrakk> \<Longrightarrow> State_Idle localState output_fun trans_fun (f_Exec_Comp_Stream_Acc_LocalState k localState trans_fun xs c ! Suc i)
[PROOF STEP]
apply (subgoal_tac "i < length (tl xs) \<and> tl xs \<noteq> []", elim conjE)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>i c xs. \<lbrakk>0 < l; l \<le> k; State_Idle localState output_fun trans_fun (localState c); \<forall>c m. State_Idle localState output_fun trans_fun (localState c) \<longrightarrow> State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun (m # NoMsg\<^bsup>l - Suc 0\<^esup>) c)); Suc i < length xs; xs \<noteq> []; State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun (hd xs # NoMsg\<^bsup>k - Suc 0\<^esup>) c)); \<lbrakk>0 < l; l \<le> k; State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun (hd xs # NoMsg\<^bsup>k - Suc 0\<^esup>) c)); \<forall>c m. State_Idle localState output_fun trans_fun (localState c) \<longrightarrow> State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun (m # NoMsg\<^bsup>l - Suc 0\<^esup>) c)); i < length (tl xs); tl xs \<noteq> []; State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun (hd (tl xs) # NoMsg\<^bsup>k - Suc 0\<^esup>) (f_Exec_Comp trans_fun (hd xs # NoMsg\<^bsup>k - Suc 0\<^esup>) c)))\<rbrakk> \<Longrightarrow> State_Idle localState output_fun trans_fun (f_Exec_Comp_Stream_Acc_LocalState k localState trans_fun (tl xs) (f_Exec_Comp trans_fun (hd xs # NoMsg\<^bsup>k - Suc 0\<^esup>) c) ! i); i < length (tl xs); tl xs \<noteq> []\<rbrakk> \<Longrightarrow> State_Idle localState output_fun trans_fun (f_Exec_Comp_Stream_Acc_LocalState k localState trans_fun xs c ! Suc i)
 2. \<And>i c xs. \<lbrakk>0 < l; l \<le> k; State_Idle localState output_fun trans_fun (localState c); \<forall>c m. State_Idle localState output_fun trans_fun (localState c) \<longrightarrow> State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun (m # NoMsg\<^bsup>l - Suc 0\<^esup>) c)); Suc i < length xs; xs \<noteq> []; State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun (hd xs # NoMsg\<^bsup>k - Suc 0\<^esup>) c)); \<lbrakk>0 < l; l \<le> k; State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun (hd xs # NoMsg\<^bsup>k - Suc 0\<^esup>) c)); \<forall>c m. State_Idle localState output_fun trans_fun (localState c) \<longrightarrow> State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun (m # NoMsg\<^bsup>l - Suc 0\<^esup>) c)); i < length (tl xs); tl xs \<noteq> []; State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun (hd (tl xs) # NoMsg\<^bsup>k - Suc 0\<^esup>) (f_Exec_Comp trans_fun (hd xs # NoMsg\<^bsup>k - Suc 0\<^esup>) c)))\<rbrakk> \<Longrightarrow> State_Idle localState output_fun trans_fun (f_Exec_Comp_Stream_Acc_LocalState k localState trans_fun (tl xs) (f_Exec_Comp trans_fun (hd xs # NoMsg\<^bsup>k - Suc 0\<^esup>) c) ! i)\<rbrakk> \<Longrightarrow> i < length (tl xs) \<and> tl xs \<noteq> []
[PROOF STEP]
prefer 2
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>i c xs. \<lbrakk>0 < l; l \<le> k; State_Idle localState output_fun trans_fun (localState c); \<forall>c m. State_Idle localState output_fun trans_fun (localState c) \<longrightarrow> State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun (m # NoMsg\<^bsup>l - Suc 0\<^esup>) c)); Suc i < length xs; xs \<noteq> []; State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun (hd xs # NoMsg\<^bsup>k - Suc 0\<^esup>) c)); \<lbrakk>0 < l; l \<le> k; State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun (hd xs # NoMsg\<^bsup>k - Suc 0\<^esup>) c)); \<forall>c m. State_Idle localState output_fun trans_fun (localState c) \<longrightarrow> State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun (m # NoMsg\<^bsup>l - Suc 0\<^esup>) c)); i < length (tl xs); tl xs \<noteq> []; State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun (hd (tl xs) # NoMsg\<^bsup>k - Suc 0\<^esup>) (f_Exec_Comp trans_fun (hd xs # NoMsg\<^bsup>k - Suc 0\<^esup>) c)))\<rbrakk> \<Longrightarrow> State_Idle localState output_fun trans_fun (f_Exec_Comp_Stream_Acc_LocalState k localState trans_fun (tl xs) (f_Exec_Comp trans_fun (hd xs # NoMsg\<^bsup>k - Suc 0\<^esup>) c) ! i)\<rbrakk> \<Longrightarrow> i < length (tl xs) \<and> tl xs \<noteq> []
 2. \<And>i c xs. \<lbrakk>0 < l; l \<le> k; State_Idle localState output_fun trans_fun (localState c); \<forall>c m. State_Idle localState output_fun trans_fun (localState c) \<longrightarrow> State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun (m # NoMsg\<^bsup>l - Suc 0\<^esup>) c)); Suc i < length xs; xs \<noteq> []; State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun (hd xs # NoMsg\<^bsup>k - Suc 0\<^esup>) c)); \<lbrakk>0 < l; l \<le> k; State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun (hd xs # NoMsg\<^bsup>k - Suc 0\<^esup>) c)); \<forall>c m. State_Idle localState output_fun trans_fun (localState c) \<longrightarrow> State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun (m # NoMsg\<^bsup>l - Suc 0\<^esup>) c)); i < length (tl xs); tl xs \<noteq> []; State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun (hd (tl xs) # NoMsg\<^bsup>k - Suc 0\<^esup>) (f_Exec_Comp trans_fun (hd xs # NoMsg\<^bsup>k - Suc 0\<^esup>) c)))\<rbrakk> \<Longrightarrow> State_Idle localState output_fun trans_fun (f_Exec_Comp_Stream_Acc_LocalState k localState trans_fun (tl xs) (f_Exec_Comp trans_fun (hd xs # NoMsg\<^bsup>k - Suc 0\<^esup>) c) ! i); i < length (tl xs); tl xs \<noteq> []\<rbrakk> \<Longrightarrow> State_Idle localState output_fun trans_fun (f_Exec_Comp_Stream_Acc_LocalState k localState trans_fun xs c ! Suc i)
[PROOF STEP]
apply (simp add: length_greater_0_conv[symmetric] del: length_greater_0_conv)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i c xs. \<lbrakk>0 < l; l \<le> k; State_Idle localState output_fun trans_fun (localState c); \<forall>c m. State_Idle localState output_fun trans_fun (localState c) \<longrightarrow> State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun (m # NoMsg\<^bsup>l - Suc 0\<^esup>) c)); Suc i < length xs; xs \<noteq> []; State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun (hd xs # NoMsg\<^bsup>k - Suc 0\<^esup>) c)); \<lbrakk>0 < l; l \<le> k; State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun (hd xs # NoMsg\<^bsup>k - Suc 0\<^esup>) c)); \<forall>c m. State_Idle localState output_fun trans_fun (localState c) \<longrightarrow> State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun (m # NoMsg\<^bsup>l - Suc 0\<^esup>) c)); i < length (tl xs); tl xs \<noteq> []; State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun (hd (tl xs) # NoMsg\<^bsup>k - Suc 0\<^esup>) (f_Exec_Comp trans_fun (hd xs # NoMsg\<^bsup>k - Suc 0\<^esup>) c)))\<rbrakk> \<Longrightarrow> State_Idle localState output_fun trans_fun (f_Exec_Comp_Stream_Acc_LocalState k localState trans_fun (tl xs) (f_Exec_Comp trans_fun (hd xs # NoMsg\<^bsup>k - Suc 0\<^esup>) c) ! i); i < length (tl xs); tl xs \<noteq> []\<rbrakk> \<Longrightarrow> State_Idle localState output_fun trans_fun (f_Exec_Comp_Stream_Acc_LocalState k localState trans_fun xs c ! Suc i)
[PROOF STEP]
apply (simp add: f_Exec_Stream_Acc_LocalState_nth)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i c xs. \<lbrakk>0 < l; l \<le> k; State_Idle localState output_fun trans_fun (localState c); \<forall>c. State_Idle localState output_fun trans_fun (localState c) \<longrightarrow> (\<forall>m. State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun NoMsg\<^bsup>l - Suc 0\<^esup> (trans_fun m c)))); Suc i < length xs; xs \<noteq> []; State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun (hd xs) c))); State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun (hd (tl xs)) (f_Exec_Comp trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun (hd xs) c))))) \<Longrightarrow> State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun (tl xs \<down> Suc i \<odot> k) (f_Exec_Comp trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun (hd xs) c)))); i < length xs - Suc 0; tl xs \<noteq> []\<rbrakk> \<Longrightarrow> State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun (xs \<down> Suc (Suc i) \<odot> k) c))
[PROOF STEP]
apply (rule_tac n="Suc i" in ssubst[OF take_Suc, rule_format], assumption)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i c xs. \<lbrakk>0 < l; l \<le> k; State_Idle localState output_fun trans_fun (localState c); \<forall>c. State_Idle localState output_fun trans_fun (localState c) \<longrightarrow> (\<forall>m. State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun NoMsg\<^bsup>l - Suc 0\<^esup> (trans_fun m c)))); Suc i < length xs; xs \<noteq> []; State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun (hd xs) c))); State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun (hd (tl xs)) (f_Exec_Comp trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun (hd xs) c))))) \<Longrightarrow> State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun (tl xs \<down> Suc i \<odot> k) (f_Exec_Comp trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun (hd xs) c)))); i < length xs - Suc 0; tl xs \<noteq> []\<rbrakk> \<Longrightarrow> State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun ((hd xs # tl xs \<down> Suc i) \<odot> k) c))
[PROOF STEP]
apply (simp add: append_Cons[symmetric] f_Exec_append del: append_Cons)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i c xs. \<lbrakk>0 < l; l \<le> k; State_Idle localState output_fun trans_fun (localState c); \<forall>c. State_Idle localState output_fun trans_fun (localState c) \<longrightarrow> (\<forall>m. State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun NoMsg\<^bsup>l - Suc 0\<^esup> (trans_fun m c)))); Suc i < length xs; xs \<noteq> []; State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun (hd xs) c))); State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun (hd (tl xs)) (f_Exec_Comp trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun (hd xs) c))))) \<Longrightarrow> State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun (tl xs \<down> Suc i \<odot> k) (f_Exec_Comp trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun (hd xs) c)))); i < length xs - Suc 0; tl xs \<noteq> []\<rbrakk> \<Longrightarrow> State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun (tl xs \<down> Suc i \<odot> k) (f_Exec_Comp trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun (hd xs) c))))
[PROOF STEP]
apply (drule meta_mp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>i c xs. \<lbrakk>0 < l; l \<le> k; State_Idle localState output_fun trans_fun (localState c); \<forall>c. State_Idle localState output_fun trans_fun (localState c) \<longrightarrow> (\<forall>m. State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun NoMsg\<^bsup>l - Suc 0\<^esup> (trans_fun m c)))); Suc i < length xs; xs \<noteq> []; State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun (hd xs) c))); i < length xs - Suc 0; tl xs \<noteq> []\<rbrakk> \<Longrightarrow> State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun (hd (tl xs)) (f_Exec_Comp trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun (hd xs) c)))))
 2. \<And>i c xs. \<lbrakk>0 < l; l \<le> k; State_Idle localState output_fun trans_fun (localState c); \<forall>c. State_Idle localState output_fun trans_fun (localState c) \<longrightarrow> (\<forall>m. State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun NoMsg\<^bsup>l - Suc 0\<^esup> (trans_fun m c)))); Suc i < length xs; xs \<noteq> []; State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun (hd xs) c))); i < length xs - Suc 0; tl xs \<noteq> []; State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun (tl xs \<down> Suc i \<odot> k) (f_Exec_Comp trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun (hd xs) c))))\<rbrakk> \<Longrightarrow> State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun (tl xs \<down> Suc i \<odot> k) (f_Exec_Comp trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun (hd xs) c))))
[PROOF STEP]
apply (drule_tac x="f_Exec_Comp trans_fun (hd xs # NoMsg\<^bsup>k - Suc 0\<^esup>) c" in spec)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>i c xs. \<lbrakk>0 < l; l \<le> k; State_Idle localState output_fun trans_fun (localState c); Suc i < length xs; xs \<noteq> []; State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun (hd xs) c))); i < length xs - Suc 0; tl xs \<noteq> []; State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun (hd xs # NoMsg\<^bsup>k - Suc 0\<^esup>) c)) \<longrightarrow> (\<forall>m. State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun NoMsg\<^bsup>l - Suc 0\<^esup> (trans_fun m (f_Exec_Comp trans_fun (hd xs # NoMsg\<^bsup>k - Suc 0\<^esup>) c)))))\<rbrakk> \<Longrightarrow> State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun (hd (tl xs)) (f_Exec_Comp trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun (hd xs) c)))))
 2. \<And>i c xs. \<lbrakk>0 < l; l \<le> k; State_Idle localState output_fun trans_fun (localState c); \<forall>c. State_Idle localState output_fun trans_fun (localState c) \<longrightarrow> (\<forall>m. State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun NoMsg\<^bsup>l - Suc 0\<^esup> (trans_fun m c)))); Suc i < length xs; xs \<noteq> []; State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun (hd xs) c))); i < length xs - Suc 0; tl xs \<noteq> []; State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun (tl xs \<down> Suc i \<odot> k) (f_Exec_Comp trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun (hd xs) c))))\<rbrakk> \<Longrightarrow> State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun (tl xs \<down> Suc i \<odot> k) (f_Exec_Comp trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun (hd xs) c))))
[PROOF STEP]
apply (drule mp, simp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>i c xs. \<lbrakk>0 < l; l \<le> k; State_Idle localState output_fun trans_fun (localState c); Suc i < length xs; xs \<noteq> []; State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun (hd xs) c))); i < length xs - Suc 0; tl xs \<noteq> []; \<forall>m. State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun NoMsg\<^bsup>l - Suc 0\<^esup> (trans_fun m (f_Exec_Comp trans_fun (hd xs # NoMsg\<^bsup>k - Suc 0\<^esup>) c))))\<rbrakk> \<Longrightarrow> State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun (hd (tl xs)) (f_Exec_Comp trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun (hd xs) c)))))
 2. \<And>i c xs. \<lbrakk>0 < l; l \<le> k; State_Idle localState output_fun trans_fun (localState c); \<forall>c. State_Idle localState output_fun trans_fun (localState c) \<longrightarrow> (\<forall>m. State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun NoMsg\<^bsup>l - Suc 0\<^esup> (trans_fun m c)))); Suc i < length xs; xs \<noteq> []; State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun (hd xs) c))); i < length xs - Suc 0; tl xs \<noteq> []; State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun (tl xs \<down> Suc i \<odot> k) (f_Exec_Comp trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun (hd xs) c))))\<rbrakk> \<Longrightarrow> State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun (tl xs \<down> Suc i \<odot> k) (f_Exec_Comp trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun (hd xs) c))))
[PROOF STEP]
apply (drule_tac x="hd (tl xs)" in spec)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>i c xs. \<lbrakk>0 < l; l \<le> k; State_Idle localState output_fun trans_fun (localState c); Suc i < length xs; xs \<noteq> []; State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun (hd xs) c))); i < length xs - Suc 0; tl xs \<noteq> []; State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun NoMsg\<^bsup>l - Suc 0\<^esup> (trans_fun (hd (tl xs)) (f_Exec_Comp trans_fun (hd xs # NoMsg\<^bsup>k - Suc 0\<^esup>) c))))\<rbrakk> \<Longrightarrow> State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun (hd (tl xs)) (f_Exec_Comp trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun (hd xs) c)))))
 2. \<And>i c xs. \<lbrakk>0 < l; l \<le> k; State_Idle localState output_fun trans_fun (localState c); \<forall>c. State_Idle localState output_fun trans_fun (localState c) \<longrightarrow> (\<forall>m. State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun NoMsg\<^bsup>l - Suc 0\<^esup> (trans_fun m c)))); Suc i < length xs; xs \<noteq> []; State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun (hd xs) c))); i < length xs - Suc 0; tl xs \<noteq> []; State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun (tl xs \<down> Suc i \<odot> k) (f_Exec_Comp trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun (hd xs) c))))\<rbrakk> \<Longrightarrow> State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun (tl xs \<down> Suc i \<odot> k) (f_Exec_Comp trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun (hd xs) c))))
[PROOF STEP]
apply (subst replicate_le_diff2[OF Suc_leI, of 0 l k, symmetric], simp+)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>i c xs. \<lbrakk>0 < l; l \<le> k; State_Idle localState output_fun trans_fun (localState c); Suc i < length xs; xs \<noteq> []; State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun (hd xs) c))); i < length xs - Suc 0; tl xs \<noteq> []; State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun NoMsg\<^bsup>l - Suc 0\<^esup> (trans_fun (hd (tl xs)) (f_Exec_Comp trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun (hd xs) c)))))\<rbrakk> \<Longrightarrow> State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun (NoMsg\<^bsup>l - Suc 0\<^esup> @ NoMsg\<^bsup>k - l\<^esup>) (trans_fun (hd (tl xs)) (f_Exec_Comp trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun (hd xs) c)))))
 2. \<And>i c xs. \<lbrakk>0 < l; l \<le> k; State_Idle localState output_fun trans_fun (localState c); \<forall>c. State_Idle localState output_fun trans_fun (localState c) \<longrightarrow> (\<forall>m. State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun NoMsg\<^bsup>l - Suc 0\<^esup> (trans_fun m c)))); Suc i < length xs; xs \<noteq> []; State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun (hd xs) c))); i < length xs - Suc 0; tl xs \<noteq> []; State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun (tl xs \<down> Suc i \<odot> k) (f_Exec_Comp trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun (hd xs) c))))\<rbrakk> \<Longrightarrow> State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun (tl xs \<down> Suc i \<odot> k) (f_Exec_Comp trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun (hd xs) c))))
[PROOF STEP]
apply (simp add: f_Exec_append f_Exec_State_Idle_replicate_NoMsg_state)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i c xs. \<lbrakk>0 < l; l \<le> k; State_Idle localState output_fun trans_fun (localState c); \<forall>c. State_Idle localState output_fun trans_fun (localState c) \<longrightarrow> (\<forall>m. State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun NoMsg\<^bsup>l - Suc 0\<^esup> (trans_fun m c)))); Suc i < length xs; xs \<noteq> []; State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun (hd xs) c))); i < length xs - Suc 0; tl xs \<noteq> []; State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun (tl xs \<down> Suc i \<odot> k) (f_Exec_Comp trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun (hd xs) c))))\<rbrakk> \<Longrightarrow> State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun (tl xs \<down> Suc i \<odot> k) (f_Exec_Comp trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun (hd xs) c))))
[PROOF STEP]
apply (simp add: f_Exec_Stream_Acc_LocalState_nth)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done