[STATEMENT]
lemma f_Equiv_Exec_Stream_expand_shrink_equiv_state_set[rule_format]: "
  \<And>c1 c2 i. \<lbrakk>
   0 < k1; 0 < k2;
   equiv_states (localState1 c1) (localState2 c2);
   \<forall>input0. set input0 \<subseteq> A \<longrightarrow> (\<forall>m\<in>A.
      Equiv_Exec m equiv_states
      localState1 localState2 input_fun1 input_fun2 output_fun1 output_fun2
      trans_fun1 trans_fun2 k1 k2
      (f_Exec_Comp trans_fun1 (map input_fun1 input0 \<odot>\<^sub>f k1) c1)
      (f_Exec_Comp trans_fun2 (map input_fun2 input0 \<odot>\<^sub>f k2) c2));
      \<comment> \<open>\<open>equiv_states\<close> relation implies equivalent executions\<close>
      \<comment> \<open>not only at the beginning but also after processing an input\<close>
   set input \<subseteq> A; i < length input \<rbrakk> \<Longrightarrow>
   equiv_states
     (localState1 ((f_Exec_Comp_Stream trans_fun1 (map input_fun1 input \<odot>\<^sub>f k1) c1) \<div>\<^bsub>fl\<^esub> k1 ! i))
     (localState2 ((f_Exec_Comp_Stream trans_fun2 (map input_fun2 input \<odot>\<^sub>f k2) c2) \<div>\<^bsub>fl\<^esub> k2 ! i))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>c1 c2 i. \<lbrakk>0 < k1; 0 < k2; equiv_states (localState1 c1) (localState2 c2); \<forall>input0. set input0 \<subseteq> A \<longrightarrow> (\<forall>m\<in>A. Equiv_Exec m equiv_states localState1 localState2 input_fun1 input_fun2 output_fun1 output_fun2 trans_fun1 trans_fun2 k1 k2 (f_Exec_Comp trans_fun1 (map input_fun1 input0 \<odot> k1) c1) (f_Exec_Comp trans_fun2 (map input_fun2 input0 \<odot> k2) c2)); set input \<subseteq> A; i < length input\<rbrakk> \<Longrightarrow> equiv_states (localState1 (f_Exec_Comp_Stream trans_fun1 (map input_fun1 input \<odot> k1) c1 \<div>\<^sub>l k1 ! i)) (localState2 (f_Exec_Comp_Stream trans_fun2 (map input_fun2 input \<odot> k2) c2 \<div>\<^sub>l k2 ! i))
[PROOF STEP]
apply (induct input, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a input c1 c2 i. \<lbrakk>\<And>c1 c2 i. \<lbrakk>0 < k1; 0 < k2; equiv_states (localState1 c1) (localState2 c2); \<forall>input0. set input0 \<subseteq> A \<longrightarrow> (\<forall>m\<in>A. Equiv_Exec m equiv_states localState1 localState2 input_fun1 input_fun2 output_fun1 output_fun2 trans_fun1 trans_fun2 k1 k2 (f_Exec_Comp trans_fun1 (map input_fun1 input0 \<odot> k1) c1) (f_Exec_Comp trans_fun2 (map input_fun2 input0 \<odot> k2) c2)); set input \<subseteq> A; i < length input\<rbrakk> \<Longrightarrow> equiv_states (localState1 (f_Exec_Comp_Stream trans_fun1 (map input_fun1 input \<odot> k1) c1 \<div>\<^sub>l k1 ! i)) (localState2 (f_Exec_Comp_Stream trans_fun2 (map input_fun2 input \<odot> k2) c2 \<div>\<^sub>l k2 ! i)); 0 < k1; 0 < k2; equiv_states (localState1 c1) (localState2 c2); \<forall>input0. set input0 \<subseteq> A \<longrightarrow> (\<forall>m\<in>A. Equiv_Exec m equiv_states localState1 localState2 input_fun1 input_fun2 output_fun1 output_fun2 trans_fun1 trans_fun2 k1 k2 (f_Exec_Comp trans_fun1 (map input_fun1 input0 \<odot> k1) c1) (f_Exec_Comp trans_fun2 (map input_fun2 input0 \<odot> k2) c2)); set (a # input) \<subseteq> A; i < length (a # input)\<rbrakk> \<Longrightarrow> equiv_states (localState1 (f_Exec_Comp_Stream trans_fun1 (map input_fun1 (a # input) \<odot> k1) c1 \<div>\<^sub>l k1 ! i)) (localState2 (f_Exec_Comp_Stream trans_fun2 (map input_fun2 (a # input) \<odot> k2) c2 \<div>\<^sub>l k2 ! i))
[PROOF STEP]
apply (clarsimp simp: append_Cons[symmetric] f_Exec_Stream_append_if f_shrink_last_Cons nth_Cons simp del: last.simps f_Exec_Stream_Cons append_Cons)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a input c1 c2 i. \<lbrakk>\<And>c1 c2 i. \<lbrakk>equiv_states (localState1 c1) (localState2 c2); \<forall>input0. set input0 \<subseteq> A \<longrightarrow> (\<forall>m\<in>A. Equiv_Exec m equiv_states localState1 localState2 input_fun1 input_fun2 output_fun1 output_fun2 trans_fun1 trans_fun2 k1 k2 (f_Exec_Comp trans_fun1 (map input_fun1 input0 \<odot> k1) c1) (f_Exec_Comp trans_fun2 (map input_fun2 input0 \<odot> k2) c2)); i < length input\<rbrakk> \<Longrightarrow> equiv_states (localState1 (f_Exec_Comp_Stream trans_fun1 (map input_fun1 input \<odot> k1) c1 \<div>\<^sub>l k1 ! i)) (localState2 (f_Exec_Comp_Stream trans_fun2 (map input_fun2 input \<odot> k2) c2 \<div>\<^sub>l k2 ! i)); 0 < k1; 0 < k2; equiv_states (localState1 c1) (localState2 c2); \<forall>input0. set input0 \<subseteq> A \<longrightarrow> (\<forall>m\<in>A. Equiv_Exec m equiv_states localState1 localState2 input_fun1 input_fun2 output_fun1 output_fun2 trans_fun1 trans_fun2 k1 k2 (f_Exec_Comp trans_fun1 (map input_fun1 input0 \<odot> k1) c1) (f_Exec_Comp trans_fun2 (map input_fun2 input0 \<odot> k2) c2)); i < Suc (length input); a \<in> A; set input \<subseteq> A\<rbrakk> \<Longrightarrow> equiv_states (localState1 (case i of 0 \<Rightarrow> last (f_Exec_Comp_Stream trans_fun1 (input_fun1 a # NoMsg\<^bsup>k1 - Suc 0\<^esup>) c1) | Suc k \<Rightarrow> f_Exec_Comp_Stream trans_fun1 (map input_fun1 input \<odot> k1) (last (f_Exec_Comp_Stream trans_fun1 (input_fun1 a # NoMsg\<^bsup>k1 - Suc 0\<^esup>) c1)) \<div>\<^sub>l k1 ! k)) (localState2 (case i of 0 \<Rightarrow> last (f_Exec_Comp_Stream trans_fun2 (input_fun2 a # NoMsg\<^bsup>k2 - Suc 0\<^esup>) c2) | Suc k \<Rightarrow> f_Exec_Comp_Stream trans_fun2 (map input_fun2 input \<odot> k2) (last (f_Exec_Comp_Stream trans_fun2 (input_fun2 a # NoMsg\<^bsup>k2 - Suc 0\<^esup>) c2)) \<div>\<^sub>l k2 ! k))
[PROOF STEP]
apply (case_tac i)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a input c1 c2 i. \<lbrakk>\<And>c1 c2 i. \<lbrakk>equiv_states (localState1 c1) (localState2 c2); \<forall>input0. set input0 \<subseteq> A \<longrightarrow> (\<forall>m\<in>A. Equiv_Exec m equiv_states localState1 localState2 input_fun1 input_fun2 output_fun1 output_fun2 trans_fun1 trans_fun2 k1 k2 (f_Exec_Comp trans_fun1 (map input_fun1 input0 \<odot> k1) c1) (f_Exec_Comp trans_fun2 (map input_fun2 input0 \<odot> k2) c2)); i < length input\<rbrakk> \<Longrightarrow> equiv_states (localState1 (f_Exec_Comp_Stream trans_fun1 (map input_fun1 input \<odot> k1) c1 \<div>\<^sub>l k1 ! i)) (localState2 (f_Exec_Comp_Stream trans_fun2 (map input_fun2 input \<odot> k2) c2 \<div>\<^sub>l k2 ! i)); 0 < k1; 0 < k2; equiv_states (localState1 c1) (localState2 c2); \<forall>input0. set input0 \<subseteq> A \<longrightarrow> (\<forall>m\<in>A. Equiv_Exec m equiv_states localState1 localState2 input_fun1 input_fun2 output_fun1 output_fun2 trans_fun1 trans_fun2 k1 k2 (f_Exec_Comp trans_fun1 (map input_fun1 input0 \<odot> k1) c1) (f_Exec_Comp trans_fun2 (map input_fun2 input0 \<odot> k2) c2)); i < Suc (length input); a \<in> A; set input \<subseteq> A; i = 0\<rbrakk> \<Longrightarrow> equiv_states (localState1 (case i of 0 \<Rightarrow> last (f_Exec_Comp_Stream trans_fun1 (input_fun1 a # NoMsg\<^bsup>k1 - Suc 0\<^esup>) c1) | Suc k \<Rightarrow> f_Exec_Comp_Stream trans_fun1 (map input_fun1 input \<odot> k1) (last (f_Exec_Comp_Stream trans_fun1 (input_fun1 a # NoMsg\<^bsup>k1 - Suc 0\<^esup>) c1)) \<div>\<^sub>l k1 ! k)) (localState2 (case i of 0 \<Rightarrow> last (f_Exec_Comp_Stream trans_fun2 (input_fun2 a # NoMsg\<^bsup>k2 - Suc 0\<^esup>) c2) | Suc k \<Rightarrow> f_Exec_Comp_Stream trans_fun2 (map input_fun2 input \<odot> k2) (last (f_Exec_Comp_Stream trans_fun2 (input_fun2 a # NoMsg\<^bsup>k2 - Suc 0\<^esup>) c2)) \<div>\<^sub>l k2 ! k))
 2. \<And>a input c1 c2 i nat. \<lbrakk>\<And>c1 c2 i. \<lbrakk>equiv_states (localState1 c1) (localState2 c2); \<forall>input0. set input0 \<subseteq> A \<longrightarrow> (\<forall>m\<in>A. Equiv_Exec m equiv_states localState1 localState2 input_fun1 input_fun2 output_fun1 output_fun2 trans_fun1 trans_fun2 k1 k2 (f_Exec_Comp trans_fun1 (map input_fun1 input0 \<odot> k1) c1) (f_Exec_Comp trans_fun2 (map input_fun2 input0 \<odot> k2) c2)); i < length input\<rbrakk> \<Longrightarrow> equiv_states (localState1 (f_Exec_Comp_Stream trans_fun1 (map input_fun1 input \<odot> k1) c1 \<div>\<^sub>l k1 ! i)) (localState2 (f_Exec_Comp_Stream trans_fun2 (map input_fun2 input \<odot> k2) c2 \<div>\<^sub>l k2 ! i)); 0 < k1; 0 < k2; equiv_states (localState1 c1) (localState2 c2); \<forall>input0. set input0 \<subseteq> A \<longrightarrow> (\<forall>m\<in>A. Equiv_Exec m equiv_states localState1 localState2 input_fun1 input_fun2 output_fun1 output_fun2 trans_fun1 trans_fun2 k1 k2 (f_Exec_Comp trans_fun1 (map input_fun1 input0 \<odot> k1) c1) (f_Exec_Comp trans_fun2 (map input_fun2 input0 \<odot> k2) c2)); i < Suc (length input); a \<in> A; set input \<subseteq> A; i = Suc nat\<rbrakk> \<Longrightarrow> equiv_states (localState1 (case i of 0 \<Rightarrow> last (f_Exec_Comp_Stream trans_fun1 (input_fun1 a # NoMsg\<^bsup>k1 - Suc 0\<^esup>) c1) | Suc k \<Rightarrow> f_Exec_Comp_Stream trans_fun1 (map input_fun1 input \<odot> k1) (last (f_Exec_Comp_Stream trans_fun1 (input_fun1 a # NoMsg\<^bsup>k1 - Suc 0\<^esup>) c1)) \<div>\<^sub>l k1 ! k)) (localState2 (case i of 0 \<Rightarrow> last (f_Exec_Comp_Stream trans_fun2 (input_fun2 a # NoMsg\<^bsup>k2 - Suc 0\<^esup>) c2) | Suc k \<Rightarrow> f_Exec_Comp_Stream trans_fun2 (map input_fun2 input \<odot> k2) (last (f_Exec_Comp_Stream trans_fun2 (input_fun2 a # NoMsg\<^bsup>k2 - Suc 0\<^esup>) c2)) \<div>\<^sub>l k2 ! k))
[PROOF STEP]
apply (drule_tac x="[]" in spec)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a input c1 c2 i. \<lbrakk>\<And>c1 c2 i. \<lbrakk>equiv_states (localState1 c1) (localState2 c2); \<forall>input0. set input0 \<subseteq> A \<longrightarrow> (\<forall>m\<in>A. Equiv_Exec m equiv_states localState1 localState2 input_fun1 input_fun2 output_fun1 output_fun2 trans_fun1 trans_fun2 k1 k2 (f_Exec_Comp trans_fun1 (map input_fun1 input0 \<odot> k1) c1) (f_Exec_Comp trans_fun2 (map input_fun2 input0 \<odot> k2) c2)); i < length input\<rbrakk> \<Longrightarrow> equiv_states (localState1 (f_Exec_Comp_Stream trans_fun1 (map input_fun1 input \<odot> k1) c1 \<div>\<^sub>l k1 ! i)) (localState2 (f_Exec_Comp_Stream trans_fun2 (map input_fun2 input \<odot> k2) c2 \<div>\<^sub>l k2 ! i)); 0 < k1; 0 < k2; equiv_states (localState1 c1) (localState2 c2); i < Suc (length input); a \<in> A; set input \<subseteq> A; i = 0; set [] \<subseteq> A \<longrightarrow> (\<forall>m\<in>A. Equiv_Exec m equiv_states localState1 localState2 input_fun1 input_fun2 output_fun1 output_fun2 trans_fun1 trans_fun2 k1 k2 (f_Exec_Comp trans_fun1 (map input_fun1 [] \<odot> k1) c1) (f_Exec_Comp trans_fun2 (map input_fun2 [] \<odot> k2) c2))\<rbrakk> \<Longrightarrow> equiv_states (localState1 (case i of 0 \<Rightarrow> last (f_Exec_Comp_Stream trans_fun1 (input_fun1 a # NoMsg\<^bsup>k1 - Suc 0\<^esup>) c1) | Suc k \<Rightarrow> f_Exec_Comp_Stream trans_fun1 (map input_fun1 input \<odot> k1) (last (f_Exec_Comp_Stream trans_fun1 (input_fun1 a # NoMsg\<^bsup>k1 - Suc 0\<^esup>) c1)) \<div>\<^sub>l k1 ! k)) (localState2 (case i of 0 \<Rightarrow> last (f_Exec_Comp_Stream trans_fun2 (input_fun2 a # NoMsg\<^bsup>k2 - Suc 0\<^esup>) c2) | Suc k \<Rightarrow> f_Exec_Comp_Stream trans_fun2 (map input_fun2 input \<odot> k2) (last (f_Exec_Comp_Stream trans_fun2 (input_fun2 a # NoMsg\<^bsup>k2 - Suc 0\<^esup>) c2)) \<div>\<^sub>l k2 ! k))
 2. \<And>a input c1 c2 i nat. \<lbrakk>\<And>c1 c2 i. \<lbrakk>equiv_states (localState1 c1) (localState2 c2); \<forall>input0. set input0 \<subseteq> A \<longrightarrow> (\<forall>m\<in>A. Equiv_Exec m equiv_states localState1 localState2 input_fun1 input_fun2 output_fun1 output_fun2 trans_fun1 trans_fun2 k1 k2 (f_Exec_Comp trans_fun1 (map input_fun1 input0 \<odot> k1) c1) (f_Exec_Comp trans_fun2 (map input_fun2 input0 \<odot> k2) c2)); i < length input\<rbrakk> \<Longrightarrow> equiv_states (localState1 (f_Exec_Comp_Stream trans_fun1 (map input_fun1 input \<odot> k1) c1 \<div>\<^sub>l k1 ! i)) (localState2 (f_Exec_Comp_Stream trans_fun2 (map input_fun2 input \<odot> k2) c2 \<div>\<^sub>l k2 ! i)); 0 < k1; 0 < k2; equiv_states (localState1 c1) (localState2 c2); \<forall>input0. set input0 \<subseteq> A \<longrightarrow> (\<forall>m\<in>A. Equiv_Exec m equiv_states localState1 localState2 input_fun1 input_fun2 output_fun1 output_fun2 trans_fun1 trans_fun2 k1 k2 (f_Exec_Comp trans_fun1 (map input_fun1 input0 \<odot> k1) c1) (f_Exec_Comp trans_fun2 (map input_fun2 input0 \<odot> k2) c2)); i < Suc (length input); a \<in> A; set input \<subseteq> A; i = Suc nat\<rbrakk> \<Longrightarrow> equiv_states (localState1 (case i of 0 \<Rightarrow> last (f_Exec_Comp_Stream trans_fun1 (input_fun1 a # NoMsg\<^bsup>k1 - Suc 0\<^esup>) c1) | Suc k \<Rightarrow> f_Exec_Comp_Stream trans_fun1 (map input_fun1 input \<odot> k1) (last (f_Exec_Comp_Stream trans_fun1 (input_fun1 a # NoMsg\<^bsup>k1 - Suc 0\<^esup>) c1)) \<div>\<^sub>l k1 ! k)) (localState2 (case i of 0 \<Rightarrow> last (f_Exec_Comp_Stream trans_fun2 (input_fun2 a # NoMsg\<^bsup>k2 - Suc 0\<^esup>) c2) | Suc k \<Rightarrow> f_Exec_Comp_Stream trans_fun2 (map input_fun2 input \<odot> k2) (last (f_Exec_Comp_Stream trans_fun2 (input_fun2 a # NoMsg\<^bsup>k2 - Suc 0\<^esup>) c2)) \<div>\<^sub>l k2 ! k))
[PROOF STEP]
apply (drule mp, simp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a input c1 c2 i. \<lbrakk>\<And>c1 c2 i. \<lbrakk>equiv_states (localState1 c1) (localState2 c2); \<forall>input0. set input0 \<subseteq> A \<longrightarrow> (\<forall>m\<in>A. Equiv_Exec m equiv_states localState1 localState2 input_fun1 input_fun2 output_fun1 output_fun2 trans_fun1 trans_fun2 k1 k2 (f_Exec_Comp trans_fun1 (map input_fun1 input0 \<odot> k1) c1) (f_Exec_Comp trans_fun2 (map input_fun2 input0 \<odot> k2) c2)); i < length input\<rbrakk> \<Longrightarrow> equiv_states (localState1 (f_Exec_Comp_Stream trans_fun1 (map input_fun1 input \<odot> k1) c1 \<div>\<^sub>l k1 ! i)) (localState2 (f_Exec_Comp_Stream trans_fun2 (map input_fun2 input \<odot> k2) c2 \<div>\<^sub>l k2 ! i)); 0 < k1; 0 < k2; equiv_states (localState1 c1) (localState2 c2); i < Suc (length input); a \<in> A; set input \<subseteq> A; i = 0; \<forall>m\<in>A. Equiv_Exec m equiv_states localState1 localState2 input_fun1 input_fun2 output_fun1 output_fun2 trans_fun1 trans_fun2 k1 k2 (f_Exec_Comp trans_fun1 (map input_fun1 [] \<odot> k1) c1) (f_Exec_Comp trans_fun2 (map input_fun2 [] \<odot> k2) c2)\<rbrakk> \<Longrightarrow> equiv_states (localState1 (case i of 0 \<Rightarrow> last (f_Exec_Comp_Stream trans_fun1 (input_fun1 a # NoMsg\<^bsup>k1 - Suc 0\<^esup>) c1) | Suc k \<Rightarrow> f_Exec_Comp_Stream trans_fun1 (map input_fun1 input \<odot> k1) (last (f_Exec_Comp_Stream trans_fun1 (input_fun1 a # NoMsg\<^bsup>k1 - Suc 0\<^esup>) c1)) \<div>\<^sub>l k1 ! k)) (localState2 (case i of 0 \<Rightarrow> last (f_Exec_Comp_Stream trans_fun2 (input_fun2 a # NoMsg\<^bsup>k2 - Suc 0\<^esup>) c2) | Suc k \<Rightarrow> f_Exec_Comp_Stream trans_fun2 (map input_fun2 input \<odot> k2) (last (f_Exec_Comp_Stream trans_fun2 (input_fun2 a # NoMsg\<^bsup>k2 - Suc 0\<^esup>) c2)) \<div>\<^sub>l k2 ! k))
 2. \<And>a input c1 c2 i nat. \<lbrakk>\<And>c1 c2 i. \<lbrakk>equiv_states (localState1 c1) (localState2 c2); \<forall>input0. set input0 \<subseteq> A \<longrightarrow> (\<forall>m\<in>A. Equiv_Exec m equiv_states localState1 localState2 input_fun1 input_fun2 output_fun1 output_fun2 trans_fun1 trans_fun2 k1 k2 (f_Exec_Comp trans_fun1 (map input_fun1 input0 \<odot> k1) c1) (f_Exec_Comp trans_fun2 (map input_fun2 input0 \<odot> k2) c2)); i < length input\<rbrakk> \<Longrightarrow> equiv_states (localState1 (f_Exec_Comp_Stream trans_fun1 (map input_fun1 input \<odot> k1) c1 \<div>\<^sub>l k1 ! i)) (localState2 (f_Exec_Comp_Stream trans_fun2 (map input_fun2 input \<odot> k2) c2 \<div>\<^sub>l k2 ! i)); 0 < k1; 0 < k2; equiv_states (localState1 c1) (localState2 c2); \<forall>input0. set input0 \<subseteq> A \<longrightarrow> (\<forall>m\<in>A. Equiv_Exec m equiv_states localState1 localState2 input_fun1 input_fun2 output_fun1 output_fun2 trans_fun1 trans_fun2 k1 k2 (f_Exec_Comp trans_fun1 (map input_fun1 input0 \<odot> k1) c1) (f_Exec_Comp trans_fun2 (map input_fun2 input0 \<odot> k2) c2)); i < Suc (length input); a \<in> A; set input \<subseteq> A; i = Suc nat\<rbrakk> \<Longrightarrow> equiv_states (localState1 (case i of 0 \<Rightarrow> last (f_Exec_Comp_Stream trans_fun1 (input_fun1 a # NoMsg\<^bsup>k1 - Suc 0\<^esup>) c1) | Suc k \<Rightarrow> f_Exec_Comp_Stream trans_fun1 (map input_fun1 input \<odot> k1) (last (f_Exec_Comp_Stream trans_fun1 (input_fun1 a # NoMsg\<^bsup>k1 - Suc 0\<^esup>) c1)) \<div>\<^sub>l k1 ! k)) (localState2 (case i of 0 \<Rightarrow> last (f_Exec_Comp_Stream trans_fun2 (input_fun2 a # NoMsg\<^bsup>k2 - Suc 0\<^esup>) c2) | Suc k \<Rightarrow> f_Exec_Comp_Stream trans_fun2 (map input_fun2 input \<odot> k2) (last (f_Exec_Comp_Stream trans_fun2 (input_fun2 a # NoMsg\<^bsup>k2 - Suc 0\<^esup>) c2)) \<div>\<^sub>l k2 ! k))
[PROOF STEP]
apply (drule_tac x=a in bspec, assumption)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a input c1 c2 i. \<lbrakk>\<And>c1 c2 i. \<lbrakk>equiv_states (localState1 c1) (localState2 c2); \<forall>input0. set input0 \<subseteq> A \<longrightarrow> (\<forall>m\<in>A. Equiv_Exec m equiv_states localState1 localState2 input_fun1 input_fun2 output_fun1 output_fun2 trans_fun1 trans_fun2 k1 k2 (f_Exec_Comp trans_fun1 (map input_fun1 input0 \<odot> k1) c1) (f_Exec_Comp trans_fun2 (map input_fun2 input0 \<odot> k2) c2)); i < length input\<rbrakk> \<Longrightarrow> equiv_states (localState1 (f_Exec_Comp_Stream trans_fun1 (map input_fun1 input \<odot> k1) c1 \<div>\<^sub>l k1 ! i)) (localState2 (f_Exec_Comp_Stream trans_fun2 (map input_fun2 input \<odot> k2) c2 \<div>\<^sub>l k2 ! i)); 0 < k1; 0 < k2; equiv_states (localState1 c1) (localState2 c2); i < Suc (length input); a \<in> A; set input \<subseteq> A; i = 0; Equiv_Exec a equiv_states localState1 localState2 input_fun1 input_fun2 output_fun1 output_fun2 trans_fun1 trans_fun2 k1 k2 (f_Exec_Comp trans_fun1 (map input_fun1 [] \<odot> k1) c1) (f_Exec_Comp trans_fun2 (map input_fun2 [] \<odot> k2) c2)\<rbrakk> \<Longrightarrow> equiv_states (localState1 (case i of 0 \<Rightarrow> last (f_Exec_Comp_Stream trans_fun1 (input_fun1 a # NoMsg\<^bsup>k1 - Suc 0\<^esup>) c1) | Suc k \<Rightarrow> f_Exec_Comp_Stream trans_fun1 (map input_fun1 input \<odot> k1) (last (f_Exec_Comp_Stream trans_fun1 (input_fun1 a # NoMsg\<^bsup>k1 - Suc 0\<^esup>) c1)) \<div>\<^sub>l k1 ! k)) (localState2 (case i of 0 \<Rightarrow> last (f_Exec_Comp_Stream trans_fun2 (input_fun2 a # NoMsg\<^bsup>k2 - Suc 0\<^esup>) c2) | Suc k \<Rightarrow> f_Exec_Comp_Stream trans_fun2 (map input_fun2 input \<odot> k2) (last (f_Exec_Comp_Stream trans_fun2 (input_fun2 a # NoMsg\<^bsup>k2 - Suc 0\<^esup>) c2)) \<div>\<^sub>l k2 ! k))
 2. \<And>a input c1 c2 i nat. \<lbrakk>\<And>c1 c2 i. \<lbrakk>equiv_states (localState1 c1) (localState2 c2); \<forall>input0. set input0 \<subseteq> A \<longrightarrow> (\<forall>m\<in>A. Equiv_Exec m equiv_states localState1 localState2 input_fun1 input_fun2 output_fun1 output_fun2 trans_fun1 trans_fun2 k1 k2 (f_Exec_Comp trans_fun1 (map input_fun1 input0 \<odot> k1) c1) (f_Exec_Comp trans_fun2 (map input_fun2 input0 \<odot> k2) c2)); i < length input\<rbrakk> \<Longrightarrow> equiv_states (localState1 (f_Exec_Comp_Stream trans_fun1 (map input_fun1 input \<odot> k1) c1 \<div>\<^sub>l k1 ! i)) (localState2 (f_Exec_Comp_Stream trans_fun2 (map input_fun2 input \<odot> k2) c2 \<div>\<^sub>l k2 ! i)); 0 < k1; 0 < k2; equiv_states (localState1 c1) (localState2 c2); \<forall>input0. set input0 \<subseteq> A \<longrightarrow> (\<forall>m\<in>A. Equiv_Exec m equiv_states localState1 localState2 input_fun1 input_fun2 output_fun1 output_fun2 trans_fun1 trans_fun2 k1 k2 (f_Exec_Comp trans_fun1 (map input_fun1 input0 \<odot> k1) c1) (f_Exec_Comp trans_fun2 (map input_fun2 input0 \<odot> k2) c2)); i < Suc (length input); a \<in> A; set input \<subseteq> A; i = Suc nat\<rbrakk> \<Longrightarrow> equiv_states (localState1 (case i of 0 \<Rightarrow> last (f_Exec_Comp_Stream trans_fun1 (input_fun1 a # NoMsg\<^bsup>k1 - Suc 0\<^esup>) c1) | Suc k \<Rightarrow> f_Exec_Comp_Stream trans_fun1 (map input_fun1 input \<odot> k1) (last (f_Exec_Comp_Stream trans_fun1 (input_fun1 a # NoMsg\<^bsup>k1 - Suc 0\<^esup>) c1)) \<div>\<^sub>l k1 ! k)) (localState2 (case i of 0 \<Rightarrow> last (f_Exec_Comp_Stream trans_fun2 (input_fun2 a # NoMsg\<^bsup>k2 - Suc 0\<^esup>) c2) | Suc k \<Rightarrow> f_Exec_Comp_Stream trans_fun2 (map input_fun2 input \<odot> k2) (last (f_Exec_Comp_Stream trans_fun2 (input_fun2 a # NoMsg\<^bsup>k2 - Suc 0\<^esup>) c2)) \<div>\<^sub>l k2 ! k))
[PROOF STEP]
apply (simp del: last.simps f_Exec_Stream_Cons)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a input c1 c2 i. \<lbrakk>\<And>c1 c2 i. \<lbrakk>equiv_states (localState1 c1) (localState2 c2); \<forall>input0. set input0 \<subseteq> A \<longrightarrow> (\<forall>m\<in>A. Equiv_Exec m equiv_states localState1 localState2 input_fun1 input_fun2 output_fun1 output_fun2 trans_fun1 trans_fun2 k1 k2 (f_Exec_Comp trans_fun1 (map input_fun1 input0 \<odot> k1) c1) (f_Exec_Comp trans_fun2 (map input_fun2 input0 \<odot> k2) c2)); i < length input\<rbrakk> \<Longrightarrow> equiv_states (localState1 (f_Exec_Comp_Stream trans_fun1 (map input_fun1 input \<odot> k1) c1 \<div>\<^sub>l k1 ! i)) (localState2 (f_Exec_Comp_Stream trans_fun2 (map input_fun2 input \<odot> k2) c2 \<div>\<^sub>l k2 ! i)); 0 < k1; 0 < k2; equiv_states (localState1 c1) (localState2 c2); a \<in> A; set input \<subseteq> A; i = 0; Equiv_Exec a equiv_states localState1 localState2 input_fun1 input_fun2 output_fun1 output_fun2 trans_fun1 trans_fun2 k1 k2 c1 c2\<rbrakk> \<Longrightarrow> equiv_states (localState1 (last (f_Exec_Comp_Stream trans_fun1 (input_fun1 a # NoMsg\<^bsup>k1 - Suc 0\<^esup>) c1))) (localState2 (last (f_Exec_Comp_Stream trans_fun2 (input_fun2 a # NoMsg\<^bsup>k2 - Suc 0\<^esup>) c2)))
 2. \<And>a input c1 c2 i nat. \<lbrakk>\<And>c1 c2 i. \<lbrakk>equiv_states (localState1 c1) (localState2 c2); \<forall>input0. set input0 \<subseteq> A \<longrightarrow> (\<forall>m\<in>A. Equiv_Exec m equiv_states localState1 localState2 input_fun1 input_fun2 output_fun1 output_fun2 trans_fun1 trans_fun2 k1 k2 (f_Exec_Comp trans_fun1 (map input_fun1 input0 \<odot> k1) c1) (f_Exec_Comp trans_fun2 (map input_fun2 input0 \<odot> k2) c2)); i < length input\<rbrakk> \<Longrightarrow> equiv_states (localState1 (f_Exec_Comp_Stream trans_fun1 (map input_fun1 input \<odot> k1) c1 \<div>\<^sub>l k1 ! i)) (localState2 (f_Exec_Comp_Stream trans_fun2 (map input_fun2 input \<odot> k2) c2 \<div>\<^sub>l k2 ! i)); 0 < k1; 0 < k2; equiv_states (localState1 c1) (localState2 c2); \<forall>input0. set input0 \<subseteq> A \<longrightarrow> (\<forall>m\<in>A. Equiv_Exec m equiv_states localState1 localState2 input_fun1 input_fun2 output_fun1 output_fun2 trans_fun1 trans_fun2 k1 k2 (f_Exec_Comp trans_fun1 (map input_fun1 input0 \<odot> k1) c1) (f_Exec_Comp trans_fun2 (map input_fun2 input0 \<odot> k2) c2)); i < Suc (length input); a \<in> A; set input \<subseteq> A; i = Suc nat\<rbrakk> \<Longrightarrow> equiv_states (localState1 (case i of 0 \<Rightarrow> last (f_Exec_Comp_Stream trans_fun1 (input_fun1 a # NoMsg\<^bsup>k1 - Suc 0\<^esup>) c1) | Suc k \<Rightarrow> f_Exec_Comp_Stream trans_fun1 (map input_fun1 input \<odot> k1) (last (f_Exec_Comp_Stream trans_fun1 (input_fun1 a # NoMsg\<^bsup>k1 - Suc 0\<^esup>) c1)) \<div>\<^sub>l k1 ! k)) (localState2 (case i of 0 \<Rightarrow> last (f_Exec_Comp_Stream trans_fun2 (input_fun2 a # NoMsg\<^bsup>k2 - Suc 0\<^esup>) c2) | Suc k \<Rightarrow> f_Exec_Comp_Stream trans_fun2 (map input_fun2 input \<odot> k2) (last (f_Exec_Comp_Stream trans_fun2 (input_fun2 a # NoMsg\<^bsup>k2 - Suc 0\<^esup>) c2)) \<div>\<^sub>l k2 ! k))
[PROOF STEP]
apply (subst f_Exec_eq_f_Exec_Stream_last2[symmetric], simp)+
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a input c1 c2 i. \<lbrakk>\<And>c1 c2 i. \<lbrakk>equiv_states (localState1 c1) (localState2 c2); \<forall>input0. set input0 \<subseteq> A \<longrightarrow> (\<forall>m\<in>A. Equiv_Exec m equiv_states localState1 localState2 input_fun1 input_fun2 output_fun1 output_fun2 trans_fun1 trans_fun2 k1 k2 (f_Exec_Comp trans_fun1 (map input_fun1 input0 \<odot> k1) c1) (f_Exec_Comp trans_fun2 (map input_fun2 input0 \<odot> k2) c2)); i < length input\<rbrakk> \<Longrightarrow> equiv_states (localState1 (f_Exec_Comp_Stream trans_fun1 (map input_fun1 input \<odot> k1) c1 \<div>\<^sub>l k1 ! i)) (localState2 (f_Exec_Comp_Stream trans_fun2 (map input_fun2 input \<odot> k2) c2 \<div>\<^sub>l k2 ! i)); 0 < k1; 0 < k2; equiv_states (localState1 c1) (localState2 c2); a \<in> A; set input \<subseteq> A; i = 0; Equiv_Exec a equiv_states localState1 localState2 input_fun1 input_fun2 output_fun1 output_fun2 trans_fun1 trans_fun2 k1 k2 c1 c2\<rbrakk> \<Longrightarrow> equiv_states (localState1 (f_Exec_Comp trans_fun1 (input_fun1 a # NoMsg\<^bsup>k1 - Suc 0\<^esup>) c1)) (localState2 (f_Exec_Comp trans_fun2 (input_fun2 a # NoMsg\<^bsup>k2 - Suc 0\<^esup>) c2))
 2. \<And>a input c1 c2 i nat. \<lbrakk>\<And>c1 c2 i. \<lbrakk>equiv_states (localState1 c1) (localState2 c2); \<forall>input0. set input0 \<subseteq> A \<longrightarrow> (\<forall>m\<in>A. Equiv_Exec m equiv_states localState1 localState2 input_fun1 input_fun2 output_fun1 output_fun2 trans_fun1 trans_fun2 k1 k2 (f_Exec_Comp trans_fun1 (map input_fun1 input0 \<odot> k1) c1) (f_Exec_Comp trans_fun2 (map input_fun2 input0 \<odot> k2) c2)); i < length input\<rbrakk> \<Longrightarrow> equiv_states (localState1 (f_Exec_Comp_Stream trans_fun1 (map input_fun1 input \<odot> k1) c1 \<div>\<^sub>l k1 ! i)) (localState2 (f_Exec_Comp_Stream trans_fun2 (map input_fun2 input \<odot> k2) c2 \<div>\<^sub>l k2 ! i)); 0 < k1; 0 < k2; equiv_states (localState1 c1) (localState2 c2); \<forall>input0. set input0 \<subseteq> A \<longrightarrow> (\<forall>m\<in>A. Equiv_Exec m equiv_states localState1 localState2 input_fun1 input_fun2 output_fun1 output_fun2 trans_fun1 trans_fun2 k1 k2 (f_Exec_Comp trans_fun1 (map input_fun1 input0 \<odot> k1) c1) (f_Exec_Comp trans_fun2 (map input_fun2 input0 \<odot> k2) c2)); i < Suc (length input); a \<in> A; set input \<subseteq> A; i = Suc nat\<rbrakk> \<Longrightarrow> equiv_states (localState1 (case i of 0 \<Rightarrow> last (f_Exec_Comp_Stream trans_fun1 (input_fun1 a # NoMsg\<^bsup>k1 - Suc 0\<^esup>) c1) | Suc k \<Rightarrow> f_Exec_Comp_Stream trans_fun1 (map input_fun1 input \<odot> k1) (last (f_Exec_Comp_Stream trans_fun1 (input_fun1 a # NoMsg\<^bsup>k1 - Suc 0\<^esup>) c1)) \<div>\<^sub>l k1 ! k)) (localState2 (case i of 0 \<Rightarrow> last (f_Exec_Comp_Stream trans_fun2 (input_fun2 a # NoMsg\<^bsup>k2 - Suc 0\<^esup>) c2) | Suc k \<Rightarrow> f_Exec_Comp_Stream trans_fun2 (map input_fun2 input \<odot> k2) (last (f_Exec_Comp_Stream trans_fun2 (input_fun2 a # NoMsg\<^bsup>k2 - Suc 0\<^esup>) c2)) \<div>\<^sub>l k2 ! k))
[PROOF STEP]
apply (rule Equiv_Exec_equiv_statesI[of equiv_states localState1 _ localState2 _ _ input_fun1], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a input c1 c2 i nat. \<lbrakk>\<And>c1 c2 i. \<lbrakk>equiv_states (localState1 c1) (localState2 c2); \<forall>input0. set input0 \<subseteq> A \<longrightarrow> (\<forall>m\<in>A. Equiv_Exec m equiv_states localState1 localState2 input_fun1 input_fun2 output_fun1 output_fun2 trans_fun1 trans_fun2 k1 k2 (f_Exec_Comp trans_fun1 (map input_fun1 input0 \<odot> k1) c1) (f_Exec_Comp trans_fun2 (map input_fun2 input0 \<odot> k2) c2)); i < length input\<rbrakk> \<Longrightarrow> equiv_states (localState1 (f_Exec_Comp_Stream trans_fun1 (map input_fun1 input \<odot> k1) c1 \<div>\<^sub>l k1 ! i)) (localState2 (f_Exec_Comp_Stream trans_fun2 (map input_fun2 input \<odot> k2) c2 \<div>\<^sub>l k2 ! i)); 0 < k1; 0 < k2; equiv_states (localState1 c1) (localState2 c2); \<forall>input0. set input0 \<subseteq> A \<longrightarrow> (\<forall>m\<in>A. Equiv_Exec m equiv_states localState1 localState2 input_fun1 input_fun2 output_fun1 output_fun2 trans_fun1 trans_fun2 k1 k2 (f_Exec_Comp trans_fun1 (map input_fun1 input0 \<odot> k1) c1) (f_Exec_Comp trans_fun2 (map input_fun2 input0 \<odot> k2) c2)); i < Suc (length input); a \<in> A; set input \<subseteq> A; i = Suc nat\<rbrakk> \<Longrightarrow> equiv_states (localState1 (case i of 0 \<Rightarrow> last (f_Exec_Comp_Stream trans_fun1 (input_fun1 a # NoMsg\<^bsup>k1 - Suc 0\<^esup>) c1) | Suc k \<Rightarrow> f_Exec_Comp_Stream trans_fun1 (map input_fun1 input \<odot> k1) (last (f_Exec_Comp_Stream trans_fun1 (input_fun1 a # NoMsg\<^bsup>k1 - Suc 0\<^esup>) c1)) \<div>\<^sub>l k1 ! k)) (localState2 (case i of 0 \<Rightarrow> last (f_Exec_Comp_Stream trans_fun2 (input_fun2 a # NoMsg\<^bsup>k2 - Suc 0\<^esup>) c2) | Suc k \<Rightarrow> f_Exec_Comp_Stream trans_fun2 (map input_fun2 input \<odot> k2) (last (f_Exec_Comp_Stream trans_fun2 (input_fun2 a # NoMsg\<^bsup>k2 - Suc 0\<^esup>) c2)) \<div>\<^sub>l k2 ! k))
[PROOF STEP]
apply (rename_tac i')
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a input c1 c2 i i'. \<lbrakk>\<And>c1 c2 i. \<lbrakk>equiv_states (localState1 c1) (localState2 c2); \<forall>input0. set input0 \<subseteq> A \<longrightarrow> (\<forall>m\<in>A. Equiv_Exec m equiv_states localState1 localState2 input_fun1 input_fun2 output_fun1 output_fun2 trans_fun1 trans_fun2 k1 k2 (f_Exec_Comp trans_fun1 (map input_fun1 input0 \<odot> k1) c1) (f_Exec_Comp trans_fun2 (map input_fun2 input0 \<odot> k2) c2)); i < length input\<rbrakk> \<Longrightarrow> equiv_states (localState1 (f_Exec_Comp_Stream trans_fun1 (map input_fun1 input \<odot> k1) c1 \<div>\<^sub>l k1 ! i)) (localState2 (f_Exec_Comp_Stream trans_fun2 (map input_fun2 input \<odot> k2) c2 \<div>\<^sub>l k2 ! i)); 0 < k1; 0 < k2; equiv_states (localState1 c1) (localState2 c2); \<forall>input0. set input0 \<subseteq> A \<longrightarrow> (\<forall>m\<in>A. Equiv_Exec m equiv_states localState1 localState2 input_fun1 input_fun2 output_fun1 output_fun2 trans_fun1 trans_fun2 k1 k2 (f_Exec_Comp trans_fun1 (map input_fun1 input0 \<odot> k1) c1) (f_Exec_Comp trans_fun2 (map input_fun2 input0 \<odot> k2) c2)); i < Suc (length input); a \<in> A; set input \<subseteq> A; i = Suc i'\<rbrakk> \<Longrightarrow> equiv_states (localState1 (case i of 0 \<Rightarrow> last (f_Exec_Comp_Stream trans_fun1 (input_fun1 a # NoMsg\<^bsup>k1 - Suc 0\<^esup>) c1) | Suc k \<Rightarrow> f_Exec_Comp_Stream trans_fun1 (map input_fun1 input \<odot> k1) (last (f_Exec_Comp_Stream trans_fun1 (input_fun1 a # NoMsg\<^bsup>k1 - Suc 0\<^esup>) c1)) \<div>\<^sub>l k1 ! k)) (localState2 (case i of 0 \<Rightarrow> last (f_Exec_Comp_Stream trans_fun2 (input_fun2 a # NoMsg\<^bsup>k2 - Suc 0\<^esup>) c2) | Suc k \<Rightarrow> f_Exec_Comp_Stream trans_fun2 (map input_fun2 input \<odot> k2) (last (f_Exec_Comp_Stream trans_fun2 (input_fun2 a # NoMsg\<^bsup>k2 - Suc 0\<^esup>) c2)) \<div>\<^sub>l k2 ! k))
[PROOF STEP]
apply (subst f_Exec_eq_f_Exec_Stream_last2[symmetric], simp)+
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a input c1 c2 i i'. \<lbrakk>\<And>c1 c2 i. \<lbrakk>equiv_states (localState1 c1) (localState2 c2); \<forall>input0. set input0 \<subseteq> A \<longrightarrow> (\<forall>m\<in>A. Equiv_Exec m equiv_states localState1 localState2 input_fun1 input_fun2 output_fun1 output_fun2 trans_fun1 trans_fun2 k1 k2 (f_Exec_Comp trans_fun1 (map input_fun1 input0 \<odot> k1) c1) (f_Exec_Comp trans_fun2 (map input_fun2 input0 \<odot> k2) c2)); i < length input\<rbrakk> \<Longrightarrow> equiv_states (localState1 (f_Exec_Comp_Stream trans_fun1 (map input_fun1 input \<odot> k1) c1 \<div>\<^sub>l k1 ! i)) (localState2 (f_Exec_Comp_Stream trans_fun2 (map input_fun2 input \<odot> k2) c2 \<div>\<^sub>l k2 ! i)); 0 < k1; 0 < k2; equiv_states (localState1 c1) (localState2 c2); \<forall>input0. set input0 \<subseteq> A \<longrightarrow> (\<forall>m\<in>A. Equiv_Exec m equiv_states localState1 localState2 input_fun1 input_fun2 output_fun1 output_fun2 trans_fun1 trans_fun2 k1 k2 (f_Exec_Comp trans_fun1 (map input_fun1 input0 \<odot> k1) c1) (f_Exec_Comp trans_fun2 (map input_fun2 input0 \<odot> k2) c2)); i < Suc (length input); a \<in> A; set input \<subseteq> A; i = Suc i'\<rbrakk> \<Longrightarrow> equiv_states (localState1 (case i of 0 \<Rightarrow> f_Exec_Comp trans_fun1 (input_fun1 a # NoMsg\<^bsup>k1 - Suc 0\<^esup>) c1 | Suc x \<Rightarrow> f_Exec_Comp_Stream trans_fun1 (map input_fun1 input \<odot> k1) (f_Exec_Comp trans_fun1 (input_fun1 a # NoMsg\<^bsup>k1 - Suc 0\<^esup>) c1) \<div>\<^sub>l k1 ! x)) (localState2 (case i of 0 \<Rightarrow> f_Exec_Comp trans_fun2 (input_fun2 a # NoMsg\<^bsup>k2 - Suc 0\<^esup>) c2 | Suc x \<Rightarrow> f_Exec_Comp_Stream trans_fun2 (map input_fun2 input \<odot> k2) (f_Exec_Comp trans_fun2 (input_fun2 a # NoMsg\<^bsup>k2 - Suc 0\<^esup>) c2) \<div>\<^sub>l k2 ! x))
[PROOF STEP]
apply (drule_tac x="f_Exec_Comp trans_fun1 (input_fun1 a # \<NoMsg>\<^bsup>k1 - Suc 0\<^esup>) c1" in meta_spec)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a input c1 c2 i i'. \<lbrakk>0 < k1; 0 < k2; equiv_states (localState1 c1) (localState2 c2); \<forall>input0. set input0 \<subseteq> A \<longrightarrow> (\<forall>m\<in>A. Equiv_Exec m equiv_states localState1 localState2 input_fun1 input_fun2 output_fun1 output_fun2 trans_fun1 trans_fun2 k1 k2 (f_Exec_Comp trans_fun1 (map input_fun1 input0 \<odot> k1) c1) (f_Exec_Comp trans_fun2 (map input_fun2 input0 \<odot> k2) c2)); i < Suc (length input); a \<in> A; set input \<subseteq> A; i = Suc i'; \<And>c2 i. \<lbrakk>equiv_states (localState1 (f_Exec_Comp trans_fun1 (input_fun1 a # NoMsg\<^bsup>k1 - Suc 0\<^esup>) c1)) (localState2 c2); \<forall>input0. set input0 \<subseteq> A \<longrightarrow> (\<forall>m\<in>A. Equiv_Exec m equiv_states localState1 localState2 input_fun1 input_fun2 output_fun1 output_fun2 trans_fun1 trans_fun2 k1 k2 (f_Exec_Comp trans_fun1 (map input_fun1 input0 \<odot> k1) (f_Exec_Comp trans_fun1 (input_fun1 a # NoMsg\<^bsup>k1 - Suc 0\<^esup>) c1)) (f_Exec_Comp trans_fun2 (map input_fun2 input0 \<odot> k2) c2)); i < length input\<rbrakk> \<Longrightarrow> equiv_states (localState1 (f_Exec_Comp_Stream trans_fun1 (map input_fun1 input \<odot> k1) (f_Exec_Comp trans_fun1 (input_fun1 a # NoMsg\<^bsup>k1 - Suc 0\<^esup>) c1) \<div>\<^sub>l k1 ! i)) (localState2 (f_Exec_Comp_Stream trans_fun2 (map input_fun2 input \<odot> k2) c2 \<div>\<^sub>l k2 ! i))\<rbrakk> \<Longrightarrow> equiv_states (localState1 (case i of 0 \<Rightarrow> f_Exec_Comp trans_fun1 (input_fun1 a # NoMsg\<^bsup>k1 - Suc 0\<^esup>) c1 | Suc x \<Rightarrow> f_Exec_Comp_Stream trans_fun1 (map input_fun1 input \<odot> k1) (f_Exec_Comp trans_fun1 (input_fun1 a # NoMsg\<^bsup>k1 - Suc 0\<^esup>) c1) \<div>\<^sub>l k1 ! x)) (localState2 (case i of 0 \<Rightarrow> f_Exec_Comp trans_fun2 (input_fun2 a # NoMsg\<^bsup>k2 - Suc 0\<^esup>) c2 | Suc x \<Rightarrow> f_Exec_Comp_Stream trans_fun2 (map input_fun2 input \<odot> k2) (f_Exec_Comp trans_fun2 (input_fun2 a # NoMsg\<^bsup>k2 - Suc 0\<^esup>) c2) \<div>\<^sub>l k2 ! x))
[PROOF STEP]
apply (drule_tac x="f_Exec_Comp trans_fun2 (input_fun2 a # \<NoMsg>\<^bsup>k2 - Suc 0\<^esup>) c2" in meta_spec)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a input c1 c2 i i'. \<lbrakk>0 < k1; 0 < k2; equiv_states (localState1 c1) (localState2 c2); \<forall>input0. set input0 \<subseteq> A \<longrightarrow> (\<forall>m\<in>A. Equiv_Exec m equiv_states localState1 localState2 input_fun1 input_fun2 output_fun1 output_fun2 trans_fun1 trans_fun2 k1 k2 (f_Exec_Comp trans_fun1 (map input_fun1 input0 \<odot> k1) c1) (f_Exec_Comp trans_fun2 (map input_fun2 input0 \<odot> k2) c2)); i < Suc (length input); a \<in> A; set input \<subseteq> A; i = Suc i'; \<And>i. \<lbrakk>equiv_states (localState1 (f_Exec_Comp trans_fun1 (input_fun1 a # NoMsg\<^bsup>k1 - Suc 0\<^esup>) c1)) (localState2 (f_Exec_Comp trans_fun2 (input_fun2 a # NoMsg\<^bsup>k2 - Suc 0\<^esup>) c2)); \<forall>input0. set input0 \<subseteq> A \<longrightarrow> (\<forall>m\<in>A. Equiv_Exec m equiv_states localState1 localState2 input_fun1 input_fun2 output_fun1 output_fun2 trans_fun1 trans_fun2 k1 k2 (f_Exec_Comp trans_fun1 (map input_fun1 input0 \<odot> k1) (f_Exec_Comp trans_fun1 (input_fun1 a # NoMsg\<^bsup>k1 - Suc 0\<^esup>) c1)) (f_Exec_Comp trans_fun2 (map input_fun2 input0 \<odot> k2) (f_Exec_Comp trans_fun2 (input_fun2 a # NoMsg\<^bsup>k2 - Suc 0\<^esup>) c2))); i < length input\<rbrakk> \<Longrightarrow> equiv_states (localState1 (f_Exec_Comp_Stream trans_fun1 (map input_fun1 input \<odot> k1) (f_Exec_Comp trans_fun1 (input_fun1 a # NoMsg\<^bsup>k1 - Suc 0\<^esup>) c1) \<div>\<^sub>l k1 ! i)) (localState2 (f_Exec_Comp_Stream trans_fun2 (map input_fun2 input \<odot> k2) (f_Exec_Comp trans_fun2 (input_fun2 a # NoMsg\<^bsup>k2 - Suc 0\<^esup>) c2) \<div>\<^sub>l k2 ! i))\<rbrakk> \<Longrightarrow> equiv_states (localState1 (case i of 0 \<Rightarrow> f_Exec_Comp trans_fun1 (input_fun1 a # NoMsg\<^bsup>k1 - Suc 0\<^esup>) c1 | Suc x \<Rightarrow> f_Exec_Comp_Stream trans_fun1 (map input_fun1 input \<odot> k1) (f_Exec_Comp trans_fun1 (input_fun1 a # NoMsg\<^bsup>k1 - Suc 0\<^esup>) c1) \<div>\<^sub>l k1 ! x)) (localState2 (case i of 0 \<Rightarrow> f_Exec_Comp trans_fun2 (input_fun2 a # NoMsg\<^bsup>k2 - Suc 0\<^esup>) c2 | Suc x \<Rightarrow> f_Exec_Comp_Stream trans_fun2 (map input_fun2 input \<odot> k2) (f_Exec_Comp trans_fun2 (input_fun2 a # NoMsg\<^bsup>k2 - Suc 0\<^esup>) c2) \<div>\<^sub>l k2 ! x))
[PROOF STEP]
apply (drule_tac x=i' in meta_spec)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a input c1 c2 i i'. \<lbrakk>0 < k1; 0 < k2; equiv_states (localState1 c1) (localState2 c2); \<forall>input0. set input0 \<subseteq> A \<longrightarrow> (\<forall>m\<in>A. Equiv_Exec m equiv_states localState1 localState2 input_fun1 input_fun2 output_fun1 output_fun2 trans_fun1 trans_fun2 k1 k2 (f_Exec_Comp trans_fun1 (map input_fun1 input0 \<odot> k1) c1) (f_Exec_Comp trans_fun2 (map input_fun2 input0 \<odot> k2) c2)); i < Suc (length input); a \<in> A; set input \<subseteq> A; i = Suc i'; \<lbrakk>equiv_states (localState1 (f_Exec_Comp trans_fun1 (input_fun1 a # NoMsg\<^bsup>k1 - Suc 0\<^esup>) c1)) (localState2 (f_Exec_Comp trans_fun2 (input_fun2 a # NoMsg\<^bsup>k2 - Suc 0\<^esup>) c2)); \<forall>input0. set input0 \<subseteq> A \<longrightarrow> (\<forall>m\<in>A. Equiv_Exec m equiv_states localState1 localState2 input_fun1 input_fun2 output_fun1 output_fun2 trans_fun1 trans_fun2 k1 k2 (f_Exec_Comp trans_fun1 (map input_fun1 input0 \<odot> k1) (f_Exec_Comp trans_fun1 (input_fun1 a # NoMsg\<^bsup>k1 - Suc 0\<^esup>) c1)) (f_Exec_Comp trans_fun2 (map input_fun2 input0 \<odot> k2) (f_Exec_Comp trans_fun2 (input_fun2 a # NoMsg\<^bsup>k2 - Suc 0\<^esup>) c2))); i' < length input\<rbrakk> \<Longrightarrow> equiv_states (localState1 (f_Exec_Comp_Stream trans_fun1 (map input_fun1 input \<odot> k1) (f_Exec_Comp trans_fun1 (input_fun1 a # NoMsg\<^bsup>k1 - Suc 0\<^esup>) c1) \<div>\<^sub>l k1 ! i')) (localState2 (f_Exec_Comp_Stream trans_fun2 (map input_fun2 input \<odot> k2) (f_Exec_Comp trans_fun2 (input_fun2 a # NoMsg\<^bsup>k2 - Suc 0\<^esup>) c2) \<div>\<^sub>l k2 ! i'))\<rbrakk> \<Longrightarrow> equiv_states (localState1 (case i of 0 \<Rightarrow> f_Exec_Comp trans_fun1 (input_fun1 a # NoMsg\<^bsup>k1 - Suc 0\<^esup>) c1 | Suc x \<Rightarrow> f_Exec_Comp_Stream trans_fun1 (map input_fun1 input \<odot> k1) (f_Exec_Comp trans_fun1 (input_fun1 a # NoMsg\<^bsup>k1 - Suc 0\<^esup>) c1) \<div>\<^sub>l k1 ! x)) (localState2 (case i of 0 \<Rightarrow> f_Exec_Comp trans_fun2 (input_fun2 a # NoMsg\<^bsup>k2 - Suc 0\<^esup>) c2 | Suc x \<Rightarrow> f_Exec_Comp_Stream trans_fun2 (map input_fun2 input \<odot> k2) (f_Exec_Comp trans_fun2 (input_fun2 a # NoMsg\<^bsup>k2 - Suc 0\<^esup>) c2) \<div>\<^sub>l k2 ! x))
[PROOF STEP]
apply (drule meta_mp, simp)+
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a input c1 c2 i i'. \<lbrakk>0 < k1; 0 < k2; equiv_states (localState1 c1) (localState2 c2); \<forall>input0. set input0 \<subseteq> A \<longrightarrow> (\<forall>m\<in>A. Equiv_Exec m equiv_states localState1 localState2 input_fun1 input_fun2 output_fun1 output_fun2 trans_fun1 trans_fun2 k1 k2 (f_Exec_Comp trans_fun1 (map input_fun1 input0 \<odot> k1) c1) (f_Exec_Comp trans_fun2 (map input_fun2 input0 \<odot> k2) c2)); i' < length input; a \<in> A; set input \<subseteq> A; i = Suc i'\<rbrakk> \<Longrightarrow> equiv_states (localState1 (f_Exec_Comp trans_fun1 NoMsg\<^bsup>k1 - Suc 0\<^esup> (trans_fun1 (input_fun1 a) c1))) (localState2 (f_Exec_Comp trans_fun2 NoMsg\<^bsup>k2 - Suc 0\<^esup> (trans_fun2 (input_fun2 a) c2)))
 2. \<And>a input c1 c2 i i'. \<lbrakk>0 < k1; 0 < k2; equiv_states (localState1 c1) (localState2 c2); \<forall>input0. set input0 \<subseteq> A \<longrightarrow> (\<forall>m\<in>A. Equiv_Exec m equiv_states localState1 localState2 input_fun1 input_fun2 output_fun1 output_fun2 trans_fun1 trans_fun2 k1 k2 (f_Exec_Comp trans_fun1 (map input_fun1 input0 \<odot> k1) c1) (f_Exec_Comp trans_fun2 (map input_fun2 input0 \<odot> k2) c2)); i < Suc (length input); a \<in> A; set input \<subseteq> A; i = Suc i'; \<lbrakk>\<forall>input0. set input0 \<subseteq> A \<longrightarrow> (\<forall>m\<in>A. Equiv_Exec m equiv_states localState1 localState2 input_fun1 input_fun2 output_fun1 output_fun2 trans_fun1 trans_fun2 k1 k2 (f_Exec_Comp trans_fun1 (map input_fun1 input0 \<odot> k1) (f_Exec_Comp trans_fun1 (input_fun1 a # NoMsg\<^bsup>k1 - Suc 0\<^esup>) c1)) (f_Exec_Comp trans_fun2 (map input_fun2 input0 \<odot> k2) (f_Exec_Comp trans_fun2 (input_fun2 a # NoMsg\<^bsup>k2 - Suc 0\<^esup>) c2))); i' < length input\<rbrakk> \<Longrightarrow> equiv_states (localState1 (f_Exec_Comp_Stream trans_fun1 (map input_fun1 input \<odot> k1) (f_Exec_Comp trans_fun1 (input_fun1 a # NoMsg\<^bsup>k1 - Suc 0\<^esup>) c1) \<div>\<^sub>l k1 ! i')) (localState2 (f_Exec_Comp_Stream trans_fun2 (map input_fun2 input \<odot> k2) (f_Exec_Comp trans_fun2 (input_fun2 a # NoMsg\<^bsup>k2 - Suc 0\<^esup>) c2) \<div>\<^sub>l k2 ! i'))\<rbrakk> \<Longrightarrow> equiv_states (localState1 (case i of 0 \<Rightarrow> f_Exec_Comp trans_fun1 (input_fun1 a # NoMsg\<^bsup>k1 - Suc 0\<^esup>) c1 | Suc x \<Rightarrow> f_Exec_Comp_Stream trans_fun1 (map input_fun1 input \<odot> k1) (f_Exec_Comp trans_fun1 (input_fun1 a # NoMsg\<^bsup>k1 - Suc 0\<^esup>) c1) \<div>\<^sub>l k1 ! x)) (localState2 (case i of 0 \<Rightarrow> f_Exec_Comp trans_fun2 (input_fun2 a # NoMsg\<^bsup>k2 - Suc 0\<^esup>) c2 | Suc x \<Rightarrow> f_Exec_Comp_Stream trans_fun2 (map input_fun2 input \<odot> k2) (f_Exec_Comp trans_fun2 (input_fun2 a # NoMsg\<^bsup>k2 - Suc 0\<^esup>) c2) \<div>\<^sub>l k2 ! x))
[PROOF STEP]
apply (drule_tac x="[]" in spec, simp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a input c1 c2 i i'. \<lbrakk>0 < k1; 0 < k2; equiv_states (localState1 c1) (localState2 c2); i' < length input; a \<in> A; set input \<subseteq> A; i = Suc i'; \<forall>m\<in>A. Equiv_Exec m equiv_states localState1 localState2 input_fun1 input_fun2 output_fun1 output_fun2 trans_fun1 trans_fun2 k1 k2 c1 c2\<rbrakk> \<Longrightarrow> equiv_states (localState1 (f_Exec_Comp trans_fun1 NoMsg\<^bsup>k1 - Suc 0\<^esup> (trans_fun1 (input_fun1 a) c1))) (localState2 (f_Exec_Comp trans_fun2 NoMsg\<^bsup>k2 - Suc 0\<^esup> (trans_fun2 (input_fun2 a) c2)))
 2. \<And>a input c1 c2 i i'. \<lbrakk>0 < k1; 0 < k2; equiv_states (localState1 c1) (localState2 c2); \<forall>input0. set input0 \<subseteq> A \<longrightarrow> (\<forall>m\<in>A. Equiv_Exec m equiv_states localState1 localState2 input_fun1 input_fun2 output_fun1 output_fun2 trans_fun1 trans_fun2 k1 k2 (f_Exec_Comp trans_fun1 (map input_fun1 input0 \<odot> k1) c1) (f_Exec_Comp trans_fun2 (map input_fun2 input0 \<odot> k2) c2)); i < Suc (length input); a \<in> A; set input \<subseteq> A; i = Suc i'; \<lbrakk>\<forall>input0. set input0 \<subseteq> A \<longrightarrow> (\<forall>m\<in>A. Equiv_Exec m equiv_states localState1 localState2 input_fun1 input_fun2 output_fun1 output_fun2 trans_fun1 trans_fun2 k1 k2 (f_Exec_Comp trans_fun1 (map input_fun1 input0 \<odot> k1) (f_Exec_Comp trans_fun1 (input_fun1 a # NoMsg\<^bsup>k1 - Suc 0\<^esup>) c1)) (f_Exec_Comp trans_fun2 (map input_fun2 input0 \<odot> k2) (f_Exec_Comp trans_fun2 (input_fun2 a # NoMsg\<^bsup>k2 - Suc 0\<^esup>) c2))); i' < length input\<rbrakk> \<Longrightarrow> equiv_states (localState1 (f_Exec_Comp_Stream trans_fun1 (map input_fun1 input \<odot> k1) (f_Exec_Comp trans_fun1 (input_fun1 a # NoMsg\<^bsup>k1 - Suc 0\<^esup>) c1) \<div>\<^sub>l k1 ! i')) (localState2 (f_Exec_Comp_Stream trans_fun2 (map input_fun2 input \<odot> k2) (f_Exec_Comp trans_fun2 (input_fun2 a # NoMsg\<^bsup>k2 - Suc 0\<^esup>) c2) \<div>\<^sub>l k2 ! i'))\<rbrakk> \<Longrightarrow> equiv_states (localState1 (case i of 0 \<Rightarrow> f_Exec_Comp trans_fun1 (input_fun1 a # NoMsg\<^bsup>k1 - Suc 0\<^esup>) c1 | Suc x \<Rightarrow> f_Exec_Comp_Stream trans_fun1 (map input_fun1 input \<odot> k1) (f_Exec_Comp trans_fun1 (input_fun1 a # NoMsg\<^bsup>k1 - Suc 0\<^esup>) c1) \<div>\<^sub>l k1 ! x)) (localState2 (case i of 0 \<Rightarrow> f_Exec_Comp trans_fun2 (input_fun2 a # NoMsg\<^bsup>k2 - Suc 0\<^esup>) c2 | Suc x \<Rightarrow> f_Exec_Comp_Stream trans_fun2 (map input_fun2 input \<odot> k2) (f_Exec_Comp trans_fun2 (input_fun2 a # NoMsg\<^bsup>k2 - Suc 0\<^esup>) c2) \<div>\<^sub>l k2 ! x))
[PROOF STEP]
apply (drule_tac x=a in bspec, assumption)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a input c1 c2 i i'. \<lbrakk>0 < k1; 0 < k2; equiv_states (localState1 c1) (localState2 c2); i' < length input; a \<in> A; set input \<subseteq> A; i = Suc i'; Equiv_Exec a equiv_states localState1 localState2 input_fun1 input_fun2 output_fun1 output_fun2 trans_fun1 trans_fun2 k1 k2 c1 c2\<rbrakk> \<Longrightarrow> equiv_states (localState1 (f_Exec_Comp trans_fun1 NoMsg\<^bsup>k1 - Suc 0\<^esup> (trans_fun1 (input_fun1 a) c1))) (localState2 (f_Exec_Comp trans_fun2 NoMsg\<^bsup>k2 - Suc 0\<^esup> (trans_fun2 (input_fun2 a) c2)))
 2. \<And>a input c1 c2 i i'. \<lbrakk>0 < k1; 0 < k2; equiv_states (localState1 c1) (localState2 c2); \<forall>input0. set input0 \<subseteq> A \<longrightarrow> (\<forall>m\<in>A. Equiv_Exec m equiv_states localState1 localState2 input_fun1 input_fun2 output_fun1 output_fun2 trans_fun1 trans_fun2 k1 k2 (f_Exec_Comp trans_fun1 (map input_fun1 input0 \<odot> k1) c1) (f_Exec_Comp trans_fun2 (map input_fun2 input0 \<odot> k2) c2)); i < Suc (length input); a \<in> A; set input \<subseteq> A; i = Suc i'; \<lbrakk>\<forall>input0. set input0 \<subseteq> A \<longrightarrow> (\<forall>m\<in>A. Equiv_Exec m equiv_states localState1 localState2 input_fun1 input_fun2 output_fun1 output_fun2 trans_fun1 trans_fun2 k1 k2 (f_Exec_Comp trans_fun1 (map input_fun1 input0 \<odot> k1) (f_Exec_Comp trans_fun1 (input_fun1 a # NoMsg\<^bsup>k1 - Suc 0\<^esup>) c1)) (f_Exec_Comp trans_fun2 (map input_fun2 input0 \<odot> k2) (f_Exec_Comp trans_fun2 (input_fun2 a # NoMsg\<^bsup>k2 - Suc 0\<^esup>) c2))); i' < length input\<rbrakk> \<Longrightarrow> equiv_states (localState1 (f_Exec_Comp_Stream trans_fun1 (map input_fun1 input \<odot> k1) (f_Exec_Comp trans_fun1 (input_fun1 a # NoMsg\<^bsup>k1 - Suc 0\<^esup>) c1) \<div>\<^sub>l k1 ! i')) (localState2 (f_Exec_Comp_Stream trans_fun2 (map input_fun2 input \<odot> k2) (f_Exec_Comp trans_fun2 (input_fun2 a # NoMsg\<^bsup>k2 - Suc 0\<^esup>) c2) \<div>\<^sub>l k2 ! i'))\<rbrakk> \<Longrightarrow> equiv_states (localState1 (case i of 0 \<Rightarrow> f_Exec_Comp trans_fun1 (input_fun1 a # NoMsg\<^bsup>k1 - Suc 0\<^esup>) c1 | Suc x \<Rightarrow> f_Exec_Comp_Stream trans_fun1 (map input_fun1 input \<odot> k1) (f_Exec_Comp trans_fun1 (input_fun1 a # NoMsg\<^bsup>k1 - Suc 0\<^esup>) c1) \<div>\<^sub>l k1 ! x)) (localState2 (case i of 0 \<Rightarrow> f_Exec_Comp trans_fun2 (input_fun2 a # NoMsg\<^bsup>k2 - Suc 0\<^esup>) c2 | Suc x \<Rightarrow> f_Exec_Comp_Stream trans_fun2 (map input_fun2 input \<odot> k2) (f_Exec_Comp trans_fun2 (input_fun2 a # NoMsg\<^bsup>k2 - Suc 0\<^esup>) c2) \<div>\<^sub>l k2 ! x))
[PROOF STEP]
apply (rule Equiv_Exec_equiv_statesI'[of equiv_states localState1 _ localState2 _ _ input_fun1], simp+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a input c1 c2 i i'. \<lbrakk>0 < k1; 0 < k2; equiv_states (localState1 c1) (localState2 c2); \<forall>input0. set input0 \<subseteq> A \<longrightarrow> (\<forall>m\<in>A. Equiv_Exec m equiv_states localState1 localState2 input_fun1 input_fun2 output_fun1 output_fun2 trans_fun1 trans_fun2 k1 k2 (f_Exec_Comp trans_fun1 (map input_fun1 input0 \<odot> k1) c1) (f_Exec_Comp trans_fun2 (map input_fun2 input0 \<odot> k2) c2)); i' < length input; a \<in> A; set input \<subseteq> A; i = Suc i'; \<forall>input0. set input0 \<subseteq> A \<longrightarrow> (\<forall>m\<in>A. Equiv_Exec m equiv_states localState1 localState2 input_fun1 input_fun2 output_fun1 output_fun2 trans_fun1 trans_fun2 k1 k2 (f_Exec_Comp trans_fun1 (map input_fun1 input0 \<odot> k1) (f_Exec_Comp trans_fun1 NoMsg\<^bsup>k1 - Suc 0\<^esup> (trans_fun1 (input_fun1 a) c1))) (f_Exec_Comp trans_fun2 (map input_fun2 input0 \<odot> k2) (f_Exec_Comp trans_fun2 NoMsg\<^bsup>k2 - Suc 0\<^esup> (trans_fun2 (input_fun2 a) c2)))) \<Longrightarrow> equiv_states (localState1 (f_Exec_Comp_Stream trans_fun1 (map input_fun1 input \<odot> k1) (f_Exec_Comp trans_fun1 NoMsg\<^bsup>k1 - Suc 0\<^esup> (trans_fun1 (input_fun1 a) c1)) \<div>\<^sub>l k1 ! i')) (localState2 (f_Exec_Comp_Stream trans_fun2 (map input_fun2 input \<odot> k2) (f_Exec_Comp trans_fun2 NoMsg\<^bsup>k2 - Suc 0\<^esup> (trans_fun2 (input_fun2 a) c2)) \<div>\<^sub>l k2 ! i'))\<rbrakk> \<Longrightarrow> equiv_states (localState1 (f_Exec_Comp_Stream trans_fun1 (map input_fun1 input \<odot> k1) (f_Exec_Comp trans_fun1 NoMsg\<^bsup>k1 - Suc 0\<^esup> (trans_fun1 (input_fun1 a) c1)) \<div>\<^sub>l k1 ! i')) (localState2 (f_Exec_Comp_Stream trans_fun2 (map input_fun2 input \<odot> k2) (f_Exec_Comp trans_fun2 NoMsg\<^bsup>k2 - Suc 0\<^esup> (trans_fun2 (input_fun2 a) c2)) \<div>\<^sub>l k2 ! i'))
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a input c1 c2 i'. \<lbrakk>0 < k1; 0 < k2; equiv_states (localState1 c1) (localState2 c2); \<forall>input0. set input0 \<subseteq> A \<longrightarrow> (\<forall>m\<in>A. Equiv_Exec m equiv_states localState1 localState2 input_fun1 input_fun2 output_fun1 output_fun2 trans_fun1 trans_fun2 k1 k2 (f_Exec_Comp trans_fun1 (map input_fun1 input0 \<odot> k1) c1) (f_Exec_Comp trans_fun2 (map input_fun2 input0 \<odot> k2) c2)); i' < length input; a \<in> A; set input \<subseteq> A; \<forall>input0. set input0 \<subseteq> A \<longrightarrow> (\<forall>m\<in>A. Equiv_Exec m equiv_states localState1 localState2 input_fun1 input_fun2 output_fun1 output_fun2 trans_fun1 trans_fun2 k1 k2 (f_Exec_Comp trans_fun1 (map input_fun1 input0 \<odot> k1) (f_Exec_Comp trans_fun1 NoMsg\<^bsup>k1 - Suc 0\<^esup> (trans_fun1 (input_fun1 a) c1))) (f_Exec_Comp trans_fun2 (map input_fun2 input0 \<odot> k2) (f_Exec_Comp trans_fun2 NoMsg\<^bsup>k2 - Suc 0\<^esup> (trans_fun2 (input_fun2 a) c2)))) \<Longrightarrow> equiv_states (localState1 (f_Exec_Comp_Stream trans_fun1 (map input_fun1 input \<odot> k1) (f_Exec_Comp trans_fun1 NoMsg\<^bsup>k1 - Suc 0\<^esup> (trans_fun1 (input_fun1 a) c1)) \<div>\<^sub>l k1 ! i')) (localState2 (f_Exec_Comp_Stream trans_fun2 (map input_fun2 input \<odot> k2) (f_Exec_Comp trans_fun2 NoMsg\<^bsup>k2 - Suc 0\<^esup> (trans_fun2 (input_fun2 a) c2)) \<div>\<^sub>l k2 ! i'))\<rbrakk> \<Longrightarrow> equiv_states (localState1 (f_Exec_Comp_Stream trans_fun1 (map input_fun1 input \<odot> k1) (f_Exec_Comp trans_fun1 NoMsg\<^bsup>k1 - Suc 0\<^esup> (trans_fun1 (input_fun1 a) c1)) \<div>\<^sub>l k1 ! i')) (localState2 (f_Exec_Comp_Stream trans_fun2 (map input_fun2 input \<odot> k2) (f_Exec_Comp trans_fun2 NoMsg\<^bsup>k2 - Suc 0\<^esup> (trans_fun2 (input_fun2 a) c2)) \<div>\<^sub>l k2 ! i'))
[PROOF STEP]
apply (drule meta_mp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a input c1 c2 i'. \<lbrakk>0 < k1; 0 < k2; equiv_states (localState1 c1) (localState2 c2); \<forall>input0. set input0 \<subseteq> A \<longrightarrow> (\<forall>m\<in>A. Equiv_Exec m equiv_states localState1 localState2 input_fun1 input_fun2 output_fun1 output_fun2 trans_fun1 trans_fun2 k1 k2 (f_Exec_Comp trans_fun1 (map input_fun1 input0 \<odot> k1) c1) (f_Exec_Comp trans_fun2 (map input_fun2 input0 \<odot> k2) c2)); i' < length input; a \<in> A; set input \<subseteq> A\<rbrakk> \<Longrightarrow> \<forall>input0. set input0 \<subseteq> A \<longrightarrow> (\<forall>m\<in>A. Equiv_Exec m equiv_states localState1 localState2 input_fun1 input_fun2 output_fun1 output_fun2 trans_fun1 trans_fun2 k1 k2 (f_Exec_Comp trans_fun1 (map input_fun1 input0 \<odot> k1) (f_Exec_Comp trans_fun1 NoMsg\<^bsup>k1 - Suc 0\<^esup> (trans_fun1 (input_fun1 a) c1))) (f_Exec_Comp trans_fun2 (map input_fun2 input0 \<odot> k2) (f_Exec_Comp trans_fun2 NoMsg\<^bsup>k2 - Suc 0\<^esup> (trans_fun2 (input_fun2 a) c2))))
 2. \<And>a input c1 c2 i'. \<lbrakk>0 < k1; 0 < k2; equiv_states (localState1 c1) (localState2 c2); \<forall>input0. set input0 \<subseteq> A \<longrightarrow> (\<forall>m\<in>A. Equiv_Exec m equiv_states localState1 localState2 input_fun1 input_fun2 output_fun1 output_fun2 trans_fun1 trans_fun2 k1 k2 (f_Exec_Comp trans_fun1 (map input_fun1 input0 \<odot> k1) c1) (f_Exec_Comp trans_fun2 (map input_fun2 input0 \<odot> k2) c2)); i' < length input; a \<in> A; set input \<subseteq> A; equiv_states (localState1 (f_Exec_Comp_Stream trans_fun1 (map input_fun1 input \<odot> k1) (f_Exec_Comp trans_fun1 NoMsg\<^bsup>k1 - Suc 0\<^esup> (trans_fun1 (input_fun1 a) c1)) \<div>\<^sub>l k1 ! i')) (localState2 (f_Exec_Comp_Stream trans_fun2 (map input_fun2 input \<odot> k2) (f_Exec_Comp trans_fun2 NoMsg\<^bsup>k2 - Suc 0\<^esup> (trans_fun2 (input_fun2 a) c2)) \<div>\<^sub>l k2 ! i'))\<rbrakk> \<Longrightarrow> equiv_states (localState1 (f_Exec_Comp_Stream trans_fun1 (map input_fun1 input \<odot> k1) (f_Exec_Comp trans_fun1 NoMsg\<^bsup>k1 - Suc 0\<^esup> (trans_fun1 (input_fun1 a) c1)) \<div>\<^sub>l k1 ! i')) (localState2 (f_Exec_Comp_Stream trans_fun2 (map input_fun2 input \<odot> k2) (f_Exec_Comp trans_fun2 NoMsg\<^bsup>k2 - Suc 0\<^esup> (trans_fun2 (input_fun2 a) c2)) \<div>\<^sub>l k2 ! i'))
[PROOF STEP]
apply clarify
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a input c1 c2 i' input0 m. \<lbrakk>0 < k1; 0 < k2; equiv_states (localState1 c1) (localState2 c2); \<forall>input0. set input0 \<subseteq> A \<longrightarrow> (\<forall>m\<in>A. Equiv_Exec m equiv_states localState1 localState2 input_fun1 input_fun2 output_fun1 output_fun2 trans_fun1 trans_fun2 k1 k2 (f_Exec_Comp trans_fun1 (map input_fun1 input0 \<odot> k1) c1) (f_Exec_Comp trans_fun2 (map input_fun2 input0 \<odot> k2) c2)); i' < length input; a \<in> A; set input \<subseteq> A; set input0 \<subseteq> A; m \<in> A\<rbrakk> \<Longrightarrow> Equiv_Exec m equiv_states localState1 localState2 input_fun1 input_fun2 output_fun1 output_fun2 trans_fun1 trans_fun2 k1 k2 (f_Exec_Comp trans_fun1 (map input_fun1 input0 \<odot> k1) (f_Exec_Comp trans_fun1 NoMsg\<^bsup>k1 - Suc 0\<^esup> (trans_fun1 (input_fun1 a) c1))) (f_Exec_Comp trans_fun2 (map input_fun2 input0 \<odot> k2) (f_Exec_Comp trans_fun2 NoMsg\<^bsup>k2 - Suc 0\<^esup> (trans_fun2 (input_fun2 a) c2)))
 2. \<And>a input c1 c2 i'. \<lbrakk>0 < k1; 0 < k2; equiv_states (localState1 c1) (localState2 c2); \<forall>input0. set input0 \<subseteq> A \<longrightarrow> (\<forall>m\<in>A. Equiv_Exec m equiv_states localState1 localState2 input_fun1 input_fun2 output_fun1 output_fun2 trans_fun1 trans_fun2 k1 k2 (f_Exec_Comp trans_fun1 (map input_fun1 input0 \<odot> k1) c1) (f_Exec_Comp trans_fun2 (map input_fun2 input0 \<odot> k2) c2)); i' < length input; a \<in> A; set input \<subseteq> A; equiv_states (localState1 (f_Exec_Comp_Stream trans_fun1 (map input_fun1 input \<odot> k1) (f_Exec_Comp trans_fun1 NoMsg\<^bsup>k1 - Suc 0\<^esup> (trans_fun1 (input_fun1 a) c1)) \<div>\<^sub>l k1 ! i')) (localState2 (f_Exec_Comp_Stream trans_fun2 (map input_fun2 input \<odot> k2) (f_Exec_Comp trans_fun2 NoMsg\<^bsup>k2 - Suc 0\<^esup> (trans_fun2 (input_fun2 a) c2)) \<div>\<^sub>l k2 ! i'))\<rbrakk> \<Longrightarrow> equiv_states (localState1 (f_Exec_Comp_Stream trans_fun1 (map input_fun1 input \<odot> k1) (f_Exec_Comp trans_fun1 NoMsg\<^bsup>k1 - Suc 0\<^esup> (trans_fun1 (input_fun1 a) c1)) \<div>\<^sub>l k1 ! i')) (localState2 (f_Exec_Comp_Stream trans_fun2 (map input_fun2 input \<odot> k2) (f_Exec_Comp trans_fun2 NoMsg\<^bsup>k2 - Suc 0\<^esup> (trans_fun2 (input_fun2 a) c2)) \<div>\<^sub>l k2 ! i'))
[PROOF STEP]
apply (drule_tac x="a # input0" in spec)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a input c1 c2 i' input0 m. \<lbrakk>0 < k1; 0 < k2; equiv_states (localState1 c1) (localState2 c2); i' < length input; a \<in> A; set input \<subseteq> A; set input0 \<subseteq> A; m \<in> A; set (a # input0) \<subseteq> A \<longrightarrow> (\<forall>m\<in>A. Equiv_Exec m equiv_states localState1 localState2 input_fun1 input_fun2 output_fun1 output_fun2 trans_fun1 trans_fun2 k1 k2 (f_Exec_Comp trans_fun1 (map input_fun1 (a # input0) \<odot> k1) c1) (f_Exec_Comp trans_fun2 (map input_fun2 (a # input0) \<odot> k2) c2))\<rbrakk> \<Longrightarrow> Equiv_Exec m equiv_states localState1 localState2 input_fun1 input_fun2 output_fun1 output_fun2 trans_fun1 trans_fun2 k1 k2 (f_Exec_Comp trans_fun1 (map input_fun1 input0 \<odot> k1) (f_Exec_Comp trans_fun1 NoMsg\<^bsup>k1 - Suc 0\<^esup> (trans_fun1 (input_fun1 a) c1))) (f_Exec_Comp trans_fun2 (map input_fun2 input0 \<odot> k2) (f_Exec_Comp trans_fun2 NoMsg\<^bsup>k2 - Suc 0\<^esup> (trans_fun2 (input_fun2 a) c2)))
 2. \<And>a input c1 c2 i'. \<lbrakk>0 < k1; 0 < k2; equiv_states (localState1 c1) (localState2 c2); \<forall>input0. set input0 \<subseteq> A \<longrightarrow> (\<forall>m\<in>A. Equiv_Exec m equiv_states localState1 localState2 input_fun1 input_fun2 output_fun1 output_fun2 trans_fun1 trans_fun2 k1 k2 (f_Exec_Comp trans_fun1 (map input_fun1 input0 \<odot> k1) c1) (f_Exec_Comp trans_fun2 (map input_fun2 input0 \<odot> k2) c2)); i' < length input; a \<in> A; set input \<subseteq> A; equiv_states (localState1 (f_Exec_Comp_Stream trans_fun1 (map input_fun1 input \<odot> k1) (f_Exec_Comp trans_fun1 NoMsg\<^bsup>k1 - Suc 0\<^esup> (trans_fun1 (input_fun1 a) c1)) \<div>\<^sub>l k1 ! i')) (localState2 (f_Exec_Comp_Stream trans_fun2 (map input_fun2 input \<odot> k2) (f_Exec_Comp trans_fun2 NoMsg\<^bsup>k2 - Suc 0\<^esup> (trans_fun2 (input_fun2 a) c2)) \<div>\<^sub>l k2 ! i'))\<rbrakk> \<Longrightarrow> equiv_states (localState1 (f_Exec_Comp_Stream trans_fun1 (map input_fun1 input \<odot> k1) (f_Exec_Comp trans_fun1 NoMsg\<^bsup>k1 - Suc 0\<^esup> (trans_fun1 (input_fun1 a) c1)) \<div>\<^sub>l k1 ! i')) (localState2 (f_Exec_Comp_Stream trans_fun2 (map input_fun2 input \<odot> k2) (f_Exec_Comp trans_fun2 NoMsg\<^bsup>k2 - Suc 0\<^esup> (trans_fun2 (input_fun2 a) c2)) \<div>\<^sub>l k2 ! i'))
[PROOF STEP]
apply (simp add: f_Exec_append)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a input c1 c2 i'. \<lbrakk>0 < k1; 0 < k2; equiv_states (localState1 c1) (localState2 c2); \<forall>input0. set input0 \<subseteq> A \<longrightarrow> (\<forall>m\<in>A. Equiv_Exec m equiv_states localState1 localState2 input_fun1 input_fun2 output_fun1 output_fun2 trans_fun1 trans_fun2 k1 k2 (f_Exec_Comp trans_fun1 (map input_fun1 input0 \<odot> k1) c1) (f_Exec_Comp trans_fun2 (map input_fun2 input0 \<odot> k2) c2)); i' < length input; a \<in> A; set input \<subseteq> A; equiv_states (localState1 (f_Exec_Comp_Stream trans_fun1 (map input_fun1 input \<odot> k1) (f_Exec_Comp trans_fun1 NoMsg\<^bsup>k1 - Suc 0\<^esup> (trans_fun1 (input_fun1 a) c1)) \<div>\<^sub>l k1 ! i')) (localState2 (f_Exec_Comp_Stream trans_fun2 (map input_fun2 input \<odot> k2) (f_Exec_Comp trans_fun2 NoMsg\<^bsup>k2 - Suc 0\<^esup> (trans_fun2 (input_fun2 a) c2)) \<div>\<^sub>l k2 ! i'))\<rbrakk> \<Longrightarrow> equiv_states (localState1 (f_Exec_Comp_Stream trans_fun1 (map input_fun1 input \<odot> k1) (f_Exec_Comp trans_fun1 NoMsg\<^bsup>k1 - Suc 0\<^esup> (trans_fun1 (input_fun1 a) c1)) \<div>\<^sub>l k1 ! i')) (localState2 (f_Exec_Comp_Stream trans_fun2 (map input_fun2 input \<odot> k2) (f_Exec_Comp trans_fun2 NoMsg\<^bsup>k2 - Suc 0\<^esup> (trans_fun2 (input_fun2 a) c2)) \<div>\<^sub>l k2 ! i'))
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma f_Equiv_Exec_expand_shrink_equiv_state_set:"
  \<lbrakk> 0 < k1; 0 < k2; equiv_states (localState1 c1) (localState2 c2);
    \<And>input0 m. \<lbrakk>set input0 \<subseteq> A; m \<in> A\<rbrakk> \<Longrightarrow>
       Equiv_Exec
         m equiv_states localState1 localState2
         input_fun1 input_fun2 output_fun1 output_fun2 trans_fun1 trans_fun2 k1 k2
         (f_Exec_Comp trans_fun1 (map input_fun1 input0 \<odot>\<^sub>f k1) c1)
         (f_Exec_Comp trans_fun2 (map input_fun2 input0 \<odot>\<^sub>f k2) c2);
    set input \<subseteq> A \<rbrakk> \<Longrightarrow>
  equiv_states
    (localState1 (f_Exec_Comp trans_fun1 (map input_fun1 input \<odot>\<^sub>f k1) c1))
    (localState2 (f_Exec_Comp trans_fun2 (map input_fun2 input \<odot>\<^sub>f k2) c2))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < k1; 0 < k2; equiv_states (localState1 c1) (localState2 c2); \<And>input0 m. \<lbrakk>set input0 \<subseteq> A; m \<in> A\<rbrakk> \<Longrightarrow> Equiv_Exec m equiv_states localState1 localState2 input_fun1 input_fun2 output_fun1 output_fun2 trans_fun1 trans_fun2 k1 k2 (f_Exec_Comp trans_fun1 (map input_fun1 input0 \<odot> k1) c1) (f_Exec_Comp trans_fun2 (map input_fun2 input0 \<odot> k2) c2); set input \<subseteq> A\<rbrakk> \<Longrightarrow> equiv_states (localState1 (f_Exec_Comp trans_fun1 (map input_fun1 input \<odot> k1) c1)) (localState2 (f_Exec_Comp trans_fun2 (map input_fun2 input \<odot> k2) c2))
[PROOF STEP]
apply (case_tac "input = []", simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < k1; 0 < k2; equiv_states (localState1 c1) (localState2 c2); \<And>input0 m. \<lbrakk>set input0 \<subseteq> A; m \<in> A\<rbrakk> \<Longrightarrow> Equiv_Exec m equiv_states localState1 localState2 input_fun1 input_fun2 output_fun1 output_fun2 trans_fun1 trans_fun2 k1 k2 (f_Exec_Comp trans_fun1 (map input_fun1 input0 \<odot> k1) c1) (f_Exec_Comp trans_fun2 (map input_fun2 input0 \<odot> k2) c2); set input \<subseteq> A; input \<noteq> []\<rbrakk> \<Longrightarrow> equiv_states (localState1 (f_Exec_Comp trans_fun1 (map input_fun1 input \<odot> k1) c1)) (localState2 (f_Exec_Comp trans_fun2 (map input_fun2 input \<odot> k2) c2))
[PROOF STEP]
apply (subgoal_tac "map input_fun1 input \<odot>\<^sub>f k1 \<noteq> [] \<and> map input_fun2 input \<odot>\<^sub>f k2 \<noteq> []")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>0 < k1; 0 < k2; equiv_states (localState1 c1) (localState2 c2); \<And>input0 m. \<lbrakk>set input0 \<subseteq> A; m \<in> A\<rbrakk> \<Longrightarrow> Equiv_Exec m equiv_states localState1 localState2 input_fun1 input_fun2 output_fun1 output_fun2 trans_fun1 trans_fun2 k1 k2 (f_Exec_Comp trans_fun1 (map input_fun1 input0 \<odot> k1) c1) (f_Exec_Comp trans_fun2 (map input_fun2 input0 \<odot> k2) c2); set input \<subseteq> A; input \<noteq> []; map input_fun1 input \<odot> k1 \<noteq> [] \<and> map input_fun2 input \<odot> k2 \<noteq> []\<rbrakk> \<Longrightarrow> equiv_states (localState1 (f_Exec_Comp trans_fun1 (map input_fun1 input \<odot> k1) c1)) (localState2 (f_Exec_Comp trans_fun2 (map input_fun2 input \<odot> k2) c2))
 2. \<lbrakk>0 < k1; 0 < k2; equiv_states (localState1 c1) (localState2 c2); \<And>input0 m. \<lbrakk>set input0 \<subseteq> A; m \<in> A\<rbrakk> \<Longrightarrow> Equiv_Exec m equiv_states localState1 localState2 input_fun1 input_fun2 output_fun1 output_fun2 trans_fun1 trans_fun2 k1 k2 (f_Exec_Comp trans_fun1 (map input_fun1 input0 \<odot> k1) c1) (f_Exec_Comp trans_fun2 (map input_fun2 input0 \<odot> k2) c2); set input \<subseteq> A; input \<noteq> []\<rbrakk> \<Longrightarrow> map input_fun1 input \<odot> k1 \<noteq> [] \<and> map input_fun2 input \<odot> k2 \<noteq> []
[PROOF STEP]
prefer 2
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>0 < k1; 0 < k2; equiv_states (localState1 c1) (localState2 c2); \<And>input0 m. \<lbrakk>set input0 \<subseteq> A; m \<in> A\<rbrakk> \<Longrightarrow> Equiv_Exec m equiv_states localState1 localState2 input_fun1 input_fun2 output_fun1 output_fun2 trans_fun1 trans_fun2 k1 k2 (f_Exec_Comp trans_fun1 (map input_fun1 input0 \<odot> k1) c1) (f_Exec_Comp trans_fun2 (map input_fun2 input0 \<odot> k2) c2); set input \<subseteq> A; input \<noteq> []\<rbrakk> \<Longrightarrow> map input_fun1 input \<odot> k1 \<noteq> [] \<and> map input_fun2 input \<odot> k2 \<noteq> []
 2. \<lbrakk>0 < k1; 0 < k2; equiv_states (localState1 c1) (localState2 c2); \<And>input0 m. \<lbrakk>set input0 \<subseteq> A; m \<in> A\<rbrakk> \<Longrightarrow> Equiv_Exec m equiv_states localState1 localState2 input_fun1 input_fun2 output_fun1 output_fun2 trans_fun1 trans_fun2 k1 k2 (f_Exec_Comp trans_fun1 (map input_fun1 input0 \<odot> k1) c1) (f_Exec_Comp trans_fun2 (map input_fun2 input0 \<odot> k2) c2); set input \<subseteq> A; input \<noteq> []; map input_fun1 input \<odot> k1 \<noteq> [] \<and> map input_fun2 input \<odot> k2 \<noteq> []\<rbrakk> \<Longrightarrow> equiv_states (localState1 (f_Exec_Comp trans_fun1 (map input_fun1 input \<odot> k1) c1)) (localState2 (f_Exec_Comp trans_fun2 (map input_fun2 input \<odot> k2) c2))
[PROOF STEP]
apply (simp add: length_greater_0_conv[symmetric] del: length_greater_0_conv)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < k1; 0 < k2; equiv_states (localState1 c1) (localState2 c2); \<And>input0 m. \<lbrakk>set input0 \<subseteq> A; m \<in> A\<rbrakk> \<Longrightarrow> Equiv_Exec m equiv_states localState1 localState2 input_fun1 input_fun2 output_fun1 output_fun2 trans_fun1 trans_fun2 k1 k2 (f_Exec_Comp trans_fun1 (map input_fun1 input0 \<odot> k1) c1) (f_Exec_Comp trans_fun2 (map input_fun2 input0 \<odot> k2) c2); set input \<subseteq> A; input \<noteq> []; map input_fun1 input \<odot> k1 \<noteq> [] \<and> map input_fun2 input \<odot> k2 \<noteq> []\<rbrakk> \<Longrightarrow> equiv_states (localState1 (f_Exec_Comp trans_fun1 (map input_fun1 input \<odot> k1) c1)) (localState2 (f_Exec_Comp trans_fun2 (map input_fun2 input \<odot> k2) c2))
[PROOF STEP]
apply (simp add: f_Exec_eq_f_Exec_Stream_last2 last_nth f_Exec_Stream_not_empty_conv)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < k1; 0 < k2; equiv_states (localState1 c1) (localState2 c2); \<And>input0 m. \<lbrakk>set input0 \<subseteq> A; m \<in> A\<rbrakk> \<Longrightarrow> Equiv_Exec m equiv_states localState1 localState2 input_fun1 input_fun2 output_fun1 output_fun2 trans_fun1 trans_fun2 k1 k2 (f_Exec_Comp trans_fun1 (map input_fun1 input0 \<odot> k1) c1) (f_Exec_Comp trans_fun2 (map input_fun2 input0 \<odot> k2) c2); set input \<subseteq> A; input \<noteq> []; map input_fun1 input \<odot> k1 \<noteq> [] \<and> map input_fun2 input \<odot> k2 \<noteq> []\<rbrakk> \<Longrightarrow> equiv_states (localState1 (f_Exec_Comp_Stream trans_fun1 (map input_fun1 input \<odot> k1) c1 ! (length input * k1 - Suc 0))) (localState2 (f_Exec_Comp_Stream trans_fun2 (map input_fun2 input \<odot> k2) c2 ! (length input * k2 - Suc 0)))
[PROOF STEP]
apply (insert f_shrink_last_nth[of "length input - Suc 0" "f_Exec_Comp_Stream trans_fun1 (map input_fun1 input \<odot>\<^sub>f k1) c1" k1, symmetric])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < k1; 0 < k2; equiv_states (localState1 c1) (localState2 c2); \<And>input0 m. \<lbrakk>set input0 \<subseteq> A; m \<in> A\<rbrakk> \<Longrightarrow> Equiv_Exec m equiv_states localState1 localState2 input_fun1 input_fun2 output_fun1 output_fun2 trans_fun1 trans_fun2 k1 k2 (f_Exec_Comp trans_fun1 (map input_fun1 input0 \<odot> k1) c1) (f_Exec_Comp trans_fun2 (map input_fun2 input0 \<odot> k2) c2); set input \<subseteq> A; input \<noteq> []; map input_fun1 input \<odot> k1 \<noteq> [] \<and> map input_fun2 input \<odot> k2 \<noteq> []; length input - Suc 0 < length (f_Exec_Comp_Stream trans_fun1 (map input_fun1 input \<odot> k1) c1) div k1 \<Longrightarrow> f_Exec_Comp_Stream trans_fun1 (map input_fun1 input \<odot> k1) c1 ! ((length input - Suc 0) * k1 + k1 - Suc 0) = f_Exec_Comp_Stream trans_fun1 (map input_fun1 input \<odot> k1) c1 \<div>\<^sub>l k1 ! (length input - Suc 0)\<rbrakk> \<Longrightarrow> equiv_states (localState1 (f_Exec_Comp_Stream trans_fun1 (map input_fun1 input \<odot> k1) c1 ! (length input * k1 - Suc 0))) (localState2 (f_Exec_Comp_Stream trans_fun2 (map input_fun2 input \<odot> k2) c2 ! (length input * k2 - Suc 0)))
[PROOF STEP]
apply (insert f_shrink_last_nth[of "length input - Suc 0" "f_Exec_Comp_Stream trans_fun2 (map input_fun2 input \<odot>\<^sub>f k2) c2" k2, symmetric])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < k1; 0 < k2; equiv_states (localState1 c1) (localState2 c2); \<And>input0 m. \<lbrakk>set input0 \<subseteq> A; m \<in> A\<rbrakk> \<Longrightarrow> Equiv_Exec m equiv_states localState1 localState2 input_fun1 input_fun2 output_fun1 output_fun2 trans_fun1 trans_fun2 k1 k2 (f_Exec_Comp trans_fun1 (map input_fun1 input0 \<odot> k1) c1) (f_Exec_Comp trans_fun2 (map input_fun2 input0 \<odot> k2) c2); set input \<subseteq> A; input \<noteq> []; map input_fun1 input \<odot> k1 \<noteq> [] \<and> map input_fun2 input \<odot> k2 \<noteq> []; length input - Suc 0 < length (f_Exec_Comp_Stream trans_fun1 (map input_fun1 input \<odot> k1) c1) div k1 \<Longrightarrow> f_Exec_Comp_Stream trans_fun1 (map input_fun1 input \<odot> k1) c1 ! ((length input - Suc 0) * k1 + k1 - Suc 0) = f_Exec_Comp_Stream trans_fun1 (map input_fun1 input \<odot> k1) c1 \<div>\<^sub>l k1 ! (length input - Suc 0); length input - Suc 0 < length (f_Exec_Comp_Stream trans_fun2 (map input_fun2 input \<odot> k2) c2) div k2 \<Longrightarrow> f_Exec_Comp_Stream trans_fun2 (map input_fun2 input \<odot> k2) c2 ! ((length input - Suc 0) * k2 + k2 - Suc 0) = f_Exec_Comp_Stream trans_fun2 (map input_fun2 input \<odot> k2) c2 \<div>\<^sub>l k2 ! (length input - Suc 0)\<rbrakk> \<Longrightarrow> equiv_states (localState1 (f_Exec_Comp_Stream trans_fun1 (map input_fun1 input \<odot> k1) c1 ! (length input * k1 - Suc 0))) (localState2 (f_Exec_Comp_Stream trans_fun2 (map input_fun2 input \<odot> k2) c2 ! (length input * k2 - Suc 0)))
[PROOF STEP]
apply (simp add: diff_mult_distrib gr0_imp_self_le_mult2)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < k1; 0 < k2; equiv_states (localState1 c1) (localState2 c2); \<And>input0 m. \<lbrakk>set input0 \<subseteq> A; m \<in> A\<rbrakk> \<Longrightarrow> Equiv_Exec m equiv_states localState1 localState2 input_fun1 input_fun2 output_fun1 output_fun2 trans_fun1 trans_fun2 k1 k2 (f_Exec_Comp trans_fun1 (map input_fun1 input0 \<odot> k1) c1) (f_Exec_Comp trans_fun2 (map input_fun2 input0 \<odot> k2) c2); set input \<subseteq> A; input \<noteq> []; map input_fun1 input \<odot> k1 \<noteq> [] \<and> map input_fun2 input \<odot> k2 \<noteq> []; f_Exec_Comp_Stream trans_fun1 (map input_fun1 input \<odot> k1) c1 ! (length input * k1 - Suc 0) = f_Exec_Comp_Stream trans_fun1 (map input_fun1 input \<odot> k1) c1 \<div>\<^sub>l k1 ! (length input - Suc 0); f_Exec_Comp_Stream trans_fun2 (map input_fun2 input \<odot> k2) c2 ! (length input * k2 - Suc 0) = f_Exec_Comp_Stream trans_fun2 (map input_fun2 input \<odot> k2) c2 \<div>\<^sub>l k2 ! (length input - Suc 0)\<rbrakk> \<Longrightarrow> equiv_states (localState1 (f_Exec_Comp_Stream trans_fun1 (map input_fun1 input \<odot> k1) c1 \<div>\<^sub>l k1 ! (length input - Suc 0))) (localState2 (f_Exec_Comp_Stream trans_fun2 (map input_fun2 input \<odot> k2) c2 \<div>\<^sub>l k2 ! (length input - Suc 0)))
[PROOF STEP]
apply (rule f_Equiv_Exec_Stream_expand_shrink_equiv_state_set[of k1 k2 equiv_states localState1 _ localState2 _ A input_fun1 input_fun2 output_fun1 output_fun2])
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<lbrakk>0 < k1; 0 < k2; equiv_states (localState1 c1) (localState2 c2); \<And>input0 m. \<lbrakk>set input0 \<subseteq> A; m \<in> A\<rbrakk> \<Longrightarrow> Equiv_Exec m equiv_states localState1 localState2 input_fun1 input_fun2 output_fun1 output_fun2 trans_fun1 trans_fun2 k1 k2 (f_Exec_Comp trans_fun1 (map input_fun1 input0 \<odot> k1) c1) (f_Exec_Comp trans_fun2 (map input_fun2 input0 \<odot> k2) c2); set input \<subseteq> A; input \<noteq> []; map input_fun1 input \<odot> k1 \<noteq> [] \<and> map input_fun2 input \<odot> k2 \<noteq> []; f_Exec_Comp_Stream trans_fun1 (map input_fun1 input \<odot> k1) c1 ! (length input * k1 - Suc 0) = f_Exec_Comp_Stream trans_fun1 (map input_fun1 input \<odot> k1) c1 \<div>\<^sub>l k1 ! (length input - Suc 0); f_Exec_Comp_Stream trans_fun2 (map input_fun2 input \<odot> k2) c2 ! (length input * k2 - Suc 0) = f_Exec_Comp_Stream trans_fun2 (map input_fun2 input \<odot> k2) c2 \<div>\<^sub>l k2 ! (length input - Suc 0)\<rbrakk> \<Longrightarrow> 0 < k1
 2. \<lbrakk>0 < k1; 0 < k2; equiv_states (localState1 c1) (localState2 c2); \<And>input0 m. \<lbrakk>set input0 \<subseteq> A; m \<in> A\<rbrakk> \<Longrightarrow> Equiv_Exec m equiv_states localState1 localState2 input_fun1 input_fun2 output_fun1 output_fun2 trans_fun1 trans_fun2 k1 k2 (f_Exec_Comp trans_fun1 (map input_fun1 input0 \<odot> k1) c1) (f_Exec_Comp trans_fun2 (map input_fun2 input0 \<odot> k2) c2); set input \<subseteq> A; input \<noteq> []; map input_fun1 input \<odot> k1 \<noteq> [] \<and> map input_fun2 input \<odot> k2 \<noteq> []; f_Exec_Comp_Stream trans_fun1 (map input_fun1 input \<odot> k1) c1 ! (length input * k1 - Suc 0) = f_Exec_Comp_Stream trans_fun1 (map input_fun1 input \<odot> k1) c1 \<div>\<^sub>l k1 ! (length input - Suc 0); f_Exec_Comp_Stream trans_fun2 (map input_fun2 input \<odot> k2) c2 ! (length input * k2 - Suc 0) = f_Exec_Comp_Stream trans_fun2 (map input_fun2 input \<odot> k2) c2 \<div>\<^sub>l k2 ! (length input - Suc 0)\<rbrakk> \<Longrightarrow> 0 < k2
 3. \<lbrakk>0 < k1; 0 < k2; equiv_states (localState1 c1) (localState2 c2); \<And>input0 m. \<lbrakk>set input0 \<subseteq> A; m \<in> A\<rbrakk> \<Longrightarrow> Equiv_Exec m equiv_states localState1 localState2 input_fun1 input_fun2 output_fun1 output_fun2 trans_fun1 trans_fun2 k1 k2 (f_Exec_Comp trans_fun1 (map input_fun1 input0 \<odot> k1) c1) (f_Exec_Comp trans_fun2 (map input_fun2 input0 \<odot> k2) c2); set input \<subseteq> A; input \<noteq> []; map input_fun1 input \<odot> k1 \<noteq> [] \<and> map input_fun2 input \<odot> k2 \<noteq> []; f_Exec_Comp_Stream trans_fun1 (map input_fun1 input \<odot> k1) c1 ! (length input * k1 - Suc 0) = f_Exec_Comp_Stream trans_fun1 (map input_fun1 input \<odot> k1) c1 \<div>\<^sub>l k1 ! (length input - Suc 0); f_Exec_Comp_Stream trans_fun2 (map input_fun2 input \<odot> k2) c2 ! (length input * k2 - Suc 0) = f_Exec_Comp_Stream trans_fun2 (map input_fun2 input \<odot> k2) c2 \<div>\<^sub>l k2 ! (length input - Suc 0)\<rbrakk> \<Longrightarrow> equiv_states (localState1 c1) (localState2 c2)
 4. \<And>input0 m. \<lbrakk>0 < k1; 0 < k2; equiv_states (localState1 c1) (localState2 c2); \<And>input0 m. \<lbrakk>set input0 \<subseteq> A; m \<in> A\<rbrakk> \<Longrightarrow> Equiv_Exec m equiv_states localState1 localState2 input_fun1 input_fun2 output_fun1 output_fun2 trans_fun1 trans_fun2 k1 k2 (f_Exec_Comp trans_fun1 (map input_fun1 input0 \<odot> k1) c1) (f_Exec_Comp trans_fun2 (map input_fun2 input0 \<odot> k2) c2); set input \<subseteq> A; input \<noteq> []; map input_fun1 input \<odot> k1 \<noteq> [] \<and> map input_fun2 input \<odot> k2 \<noteq> []; f_Exec_Comp_Stream trans_fun1 (map input_fun1 input \<odot> k1) c1 ! (length input * k1 - Suc 0) = f_Exec_Comp_Stream trans_fun1 (map input_fun1 input \<odot> k1) c1 \<div>\<^sub>l k1 ! (length input - Suc 0); f_Exec_Comp_Stream trans_fun2 (map input_fun2 input \<odot> k2) c2 ! (length input * k2 - Suc 0) = f_Exec_Comp_Stream trans_fun2 (map input_fun2 input \<odot> k2) c2 \<div>\<^sub>l k2 ! (length input - Suc 0); set input0 \<subseteq> A; m \<in> A\<rbrakk> \<Longrightarrow> Equiv_Exec m equiv_states localState1 localState2 input_fun1 input_fun2 output_fun1 output_fun2 trans_fun1 trans_fun2 k1 k2 (f_Exec_Comp trans_fun1 (map input_fun1 input0 \<odot> k1) c1) (f_Exec_Comp trans_fun2 (map input_fun2 input0 \<odot> k2) c2)
 5. \<lbrakk>0 < k1; 0 < k2; equiv_states (localState1 c1) (localState2 c2); \<And>input0 m. \<lbrakk>set input0 \<subseteq> A; m \<in> A\<rbrakk> \<Longrightarrow> Equiv_Exec m equiv_states localState1 localState2 input_fun1 input_fun2 output_fun1 output_fun2 trans_fun1 trans_fun2 k1 k2 (f_Exec_Comp trans_fun1 (map input_fun1 input0 \<odot> k1) c1) (f_Exec_Comp trans_fun2 (map input_fun2 input0 \<odot> k2) c2); set input \<subseteq> A; input \<noteq> []; map input_fun1 input \<odot> k1 \<noteq> [] \<and> map input_fun2 input \<odot> k2 \<noteq> []; f_Exec_Comp_Stream trans_fun1 (map input_fun1 input \<odot> k1) c1 ! (length input * k1 - Suc 0) = f_Exec_Comp_Stream trans_fun1 (map input_fun1 input \<odot> k1) c1 \<div>\<^sub>l k1 ! (length input - Suc 0); f_Exec_Comp_Stream trans_fun2 (map input_fun2 input \<odot> k2) c2 ! (length input * k2 - Suc 0) = f_Exec_Comp_Stream trans_fun2 (map input_fun2 input \<odot> k2) c2 \<div>\<^sub>l k2 ! (length input - Suc 0)\<rbrakk> \<Longrightarrow> set input \<subseteq> A
 6. \<lbrakk>0 < k1; 0 < k2; equiv_states (localState1 c1) (localState2 c2); \<And>input0 m. \<lbrakk>set input0 \<subseteq> A; m \<in> A\<rbrakk> \<Longrightarrow> Equiv_Exec m equiv_states localState1 localState2 input_fun1 input_fun2 output_fun1 output_fun2 trans_fun1 trans_fun2 k1 k2 (f_Exec_Comp trans_fun1 (map input_fun1 input0 \<odot> k1) c1) (f_Exec_Comp trans_fun2 (map input_fun2 input0 \<odot> k2) c2); set input \<subseteq> A; input \<noteq> []; map input_fun1 input \<odot> k1 \<noteq> [] \<and> map input_fun2 input \<odot> k2 \<noteq> []; f_Exec_Comp_Stream trans_fun1 (map input_fun1 input \<odot> k1) c1 ! (length input * k1 - Suc 0) = f_Exec_Comp_Stream trans_fun1 (map input_fun1 input \<odot> k1) c1 \<div>\<^sub>l k1 ! (length input - Suc 0); f_Exec_Comp_Stream trans_fun2 (map input_fun2 input \<odot> k2) c2 ! (length input * k2 - Suc 0) = f_Exec_Comp_Stream trans_fun2 (map input_fun2 input \<odot> k2) c2 \<div>\<^sub>l k2 ! (length input - Suc 0)\<rbrakk> \<Longrightarrow> length input - Suc 0 < length input
[PROOF STEP]
apply simp+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma f_Equiv_Exec_expand_shrink_equiv_state:"
  \<lbrakk> 0 < k1; 0 < k2; equiv_states (localState1 c1) (localState2 c2);
    \<And>input0 m.
       Equiv_Exec
         m equiv_states localState1 localState2
         input_fun1 input_fun2 output_fun1 output_fun2 trans_fun1 trans_fun2 k1 k2
         (f_Exec_Comp trans_fun1 (map input_fun1 input0 \<odot>\<^sub>f k1) c1)
         (f_Exec_Comp trans_fun2 (map input_fun2 input0 \<odot>\<^sub>f k2) c2) \<rbrakk> \<Longrightarrow>
  equiv_states
    (localState1 (f_Exec_Comp trans_fun1 (map input_fun1 input \<odot>\<^sub>f k1) c1))
    (localState2 (f_Exec_Comp trans_fun2 (map input_fun2 input \<odot>\<^sub>f k2) c2))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < k1; 0 < k2; equiv_states (localState1 c1) (localState2 c2); \<And>input0 m. Equiv_Exec m equiv_states localState1 localState2 input_fun1 input_fun2 output_fun1 output_fun2 trans_fun1 trans_fun2 k1 k2 (f_Exec_Comp trans_fun1 (map input_fun1 input0 \<odot> k1) c1) (f_Exec_Comp trans_fun2 (map input_fun2 input0 \<odot> k2) c2)\<rbrakk> \<Longrightarrow> equiv_states (localState1 (f_Exec_Comp trans_fun1 (map input_fun1 input \<odot> k1) c1)) (localState2 (f_Exec_Comp trans_fun2 (map input_fun2 input \<odot> k2) c2))
[PROOF STEP]
by (rule f_Equiv_Exec_expand_shrink_equiv_state_set[of k1 k2 equiv_states localState1 _ localState2 _ UNIV input_fun1 input_fun2 output_fun1 output_fun2], simp+)


[STATEMENT]
lemma i_Equiv_Exec_Stream_expand_shrink_equiv_state_set[rule_format]: "
  \<lbrakk> 0 < k1; 0 < k2; equiv_states (localState1 c1) (localState2 c2);
    \<And>input0 m. \<lbrakk>set input0 \<subseteq> A; m \<in> A\<rbrakk> \<Longrightarrow>
       Equiv_Exec
        m equiv_states localState1 localState2
        input_fun1 input_fun2 output_fun1 output_fun2 trans_fun1 trans_fun2 k1 k2
       (f_Exec_Comp trans_fun1 (map input_fun1 input0 \<odot>\<^sub>f k1) c1)
       (f_Exec_Comp trans_fun2 (map input_fun2 input0 \<odot>\<^sub>f k2) c2);
    range input \<subseteq> A \<rbrakk> \<Longrightarrow>
  equiv_states
    (localState1 ((i_Exec_Comp_Stream trans_fun1 ((input_fun1 \<circ> input) \<odot>\<^sub>i k1) c1 \<div>\<^bsub>il\<^esub> k1) i))
    (localState2 ((i_Exec_Comp_Stream trans_fun2 ((input_fun2 \<circ> input) \<odot>\<^sub>i k2) c2 \<div>\<^bsub>il\<^esub> k2) i))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < k1; 0 < k2; equiv_states (localState1 c1) (localState2 c2); \<And>input0 m. \<lbrakk>set input0 \<subseteq> A; m \<in> A\<rbrakk> \<Longrightarrow> Equiv_Exec m equiv_states localState1 localState2 input_fun1 input_fun2 output_fun1 output_fun2 trans_fun1 trans_fun2 k1 k2 (f_Exec_Comp trans_fun1 (map input_fun1 input0 \<odot> k1) c1) (f_Exec_Comp trans_fun2 (map input_fun2 input0 \<odot> k2) c2); range input \<subseteq> A\<rbrakk> \<Longrightarrow> equiv_states (localState1 ((i_Exec_Comp_Stream trans_fun1 ((input_fun1 \<circ> input) \<odot> k1) c1 \<div>\<^sub>l k1) i)) (localState2 ((i_Exec_Comp_Stream trans_fun2 ((input_fun2 \<circ> input) \<odot> k2) c2 \<div>\<^sub>l k2) i))
[PROOF STEP]
apply (simp add: i_shrink_last_nth i_Exec_Stream_nth i_expand_i_take_mod)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < k1; 0 < k2; equiv_states (localState1 c1) (localState2 c2); \<And>input0 m. \<lbrakk>set input0 \<subseteq> A; m \<in> A\<rbrakk> \<Longrightarrow> Equiv_Exec m equiv_states localState1 localState2 input_fun1 input_fun2 output_fun1 output_fun2 trans_fun1 trans_fun2 k1 k2 (f_Exec_Comp trans_fun1 (map input_fun1 input0 \<odot> k1) c1) (f_Exec_Comp trans_fun2 (map input_fun2 input0 \<odot> k2) c2); range input \<subseteq> A\<rbrakk> \<Longrightarrow> equiv_states (localState1 (f_Exec_Comp trans_fun1 (map input_fun1 (input \<Down> Suc i) \<odot> k1) c1)) (localState2 (f_Exec_Comp trans_fun2 (map input_fun2 (input \<Down> Suc i) \<odot> k2) c2))
[PROOF STEP]
apply (rule f_Equiv_Exec_expand_shrink_equiv_state_set[of
  k1 k2 equiv_states localState1 c1 localState2 c2 A input_fun1 input_fun2 output_fun1 output_fun2])
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<lbrakk>0 < k1; 0 < k2; equiv_states (localState1 c1) (localState2 c2); \<And>input0 m. \<lbrakk>set input0 \<subseteq> A; m \<in> A\<rbrakk> \<Longrightarrow> Equiv_Exec m equiv_states localState1 localState2 input_fun1 input_fun2 output_fun1 output_fun2 trans_fun1 trans_fun2 k1 k2 (f_Exec_Comp trans_fun1 (map input_fun1 input0 \<odot> k1) c1) (f_Exec_Comp trans_fun2 (map input_fun2 input0 \<odot> k2) c2); range input \<subseteq> A\<rbrakk> \<Longrightarrow> 0 < k1
 2. \<lbrakk>0 < k1; 0 < k2; equiv_states (localState1 c1) (localState2 c2); \<And>input0 m. \<lbrakk>set input0 \<subseteq> A; m \<in> A\<rbrakk> \<Longrightarrow> Equiv_Exec m equiv_states localState1 localState2 input_fun1 input_fun2 output_fun1 output_fun2 trans_fun1 trans_fun2 k1 k2 (f_Exec_Comp trans_fun1 (map input_fun1 input0 \<odot> k1) c1) (f_Exec_Comp trans_fun2 (map input_fun2 input0 \<odot> k2) c2); range input \<subseteq> A\<rbrakk> \<Longrightarrow> 0 < k2
 3. \<lbrakk>0 < k1; 0 < k2; equiv_states (localState1 c1) (localState2 c2); \<And>input0 m. \<lbrakk>set input0 \<subseteq> A; m \<in> A\<rbrakk> \<Longrightarrow> Equiv_Exec m equiv_states localState1 localState2 input_fun1 input_fun2 output_fun1 output_fun2 trans_fun1 trans_fun2 k1 k2 (f_Exec_Comp trans_fun1 (map input_fun1 input0 \<odot> k1) c1) (f_Exec_Comp trans_fun2 (map input_fun2 input0 \<odot> k2) c2); range input \<subseteq> A\<rbrakk> \<Longrightarrow> equiv_states (localState1 c1) (localState2 c2)
 4. \<And>input0 m. \<lbrakk>0 < k1; 0 < k2; equiv_states (localState1 c1) (localState2 c2); \<And>input0 m. \<lbrakk>set input0 \<subseteq> A; m \<in> A\<rbrakk> \<Longrightarrow> Equiv_Exec m equiv_states localState1 localState2 input_fun1 input_fun2 output_fun1 output_fun2 trans_fun1 trans_fun2 k1 k2 (f_Exec_Comp trans_fun1 (map input_fun1 input0 \<odot> k1) c1) (f_Exec_Comp trans_fun2 (map input_fun2 input0 \<odot> k2) c2); range input \<subseteq> A; set input0 \<subseteq> A; m \<in> A\<rbrakk> \<Longrightarrow> Equiv_Exec m equiv_states localState1 localState2 input_fun1 input_fun2 output_fun1 output_fun2 trans_fun1 trans_fun2 k1 k2 (f_Exec_Comp trans_fun1 (map input_fun1 input0 \<odot> k1) c1) (f_Exec_Comp trans_fun2 (map input_fun2 input0 \<odot> k2) c2)
 5. \<lbrakk>0 < k1; 0 < k2; equiv_states (localState1 c1) (localState2 c2); \<And>input0 m. \<lbrakk>set input0 \<subseteq> A; m \<in> A\<rbrakk> \<Longrightarrow> Equiv_Exec m equiv_states localState1 localState2 input_fun1 input_fun2 output_fun1 output_fun2 trans_fun1 trans_fun2 k1 k2 (f_Exec_Comp trans_fun1 (map input_fun1 input0 \<odot> k1) c1) (f_Exec_Comp trans_fun2 (map input_fun2 input0 \<odot> k2) c2); range input \<subseteq> A\<rbrakk> \<Longrightarrow> set (input \<Down> Suc i) \<subseteq> A
[PROOF STEP]
apply (simp add: subset_trans[OF set_i_take_subset])+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma i_Equiv_Exec_Stream_expand_shrink_equiv_state: "
  \<lbrakk> 0 < k1; 0 < k2; equiv_states (localState1 c1) (localState2 c2);
    \<And>input0 m.
       Equiv_Exec
        m equiv_states localState1 localState2
        input_fun1 input_fun2 output_fun1 output_fun2 trans_fun1 trans_fun2 k1 k2
       (f_Exec_Comp trans_fun1 (map input_fun1 input0 \<odot>\<^sub>f k1) c1)
       (f_Exec_Comp trans_fun2 (map input_fun2 input0 \<odot>\<^sub>f k2) c2) \<rbrakk> \<Longrightarrow>
  equiv_states
    (localState1 ((i_Exec_Comp_Stream trans_fun1 ((input_fun1 \<circ> input) \<odot>\<^sub>i k1) c1 \<div>\<^bsub>il\<^esub> k1) i))
    (localState2 ((i_Exec_Comp_Stream trans_fun2 ((input_fun2 \<circ> input) \<odot>\<^sub>i k2) c2 \<div>\<^bsub>il\<^esub> k2) i))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < k1; 0 < k2; equiv_states (localState1 c1) (localState2 c2); \<And>input0 m. Equiv_Exec m equiv_states localState1 localState2 input_fun1 input_fun2 output_fun1 output_fun2 trans_fun1 trans_fun2 k1 k2 (f_Exec_Comp trans_fun1 (map input_fun1 input0 \<odot> k1) c1) (f_Exec_Comp trans_fun2 (map input_fun2 input0 \<odot> k2) c2)\<rbrakk> \<Longrightarrow> equiv_states (localState1 ((i_Exec_Comp_Stream trans_fun1 ((input_fun1 \<circ> input) \<odot> k1) c1 \<div>\<^sub>l k1) i)) (localState2 ((i_Exec_Comp_Stream trans_fun2 ((input_fun2 \<circ> input) \<odot> k2) c2 \<div>\<^sub>l k2) i))
[PROOF STEP]
by (rule i_Equiv_Exec_Stream_expand_shrink_equiv_state_set[of k1 k2 equiv_states localState1 c1 localState2 c2 UNIV input_fun1 input_fun2 output_fun1 output_fun2], simp+)