[STATEMENT]
lemma f_Equiv_Exec_Stream_expand_shrink_output_set_eq: "
  \<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>
  (map output_fun1 (
    f_Exec_Comp_Stream trans_fun1 (map input_fun1 input \<odot>\<^sub>f k1) c1)) \<div>\<^sub>f k1 =
  (map output_fun2 (
    f_Exec_Comp_Stream trans_fun2 (map input_fun2 input \<odot>\<^sub>f k2) c2)) \<div>\<^sub>f k2"
[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> map output_fun1 (f_Exec_Comp_Stream trans_fun1 (map input_fun1 input \<odot> k1) c1) \<div> k1 = map output_fun2 (f_Exec_Comp_Stream trans_fun2 (map input_fun2 input \<odot> k2) c2) \<div> k2
[PROOF STEP]
apply (subst list_eq_iff)
[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> length (map output_fun1 (f_Exec_Comp_Stream trans_fun1 (map input_fun1 input \<odot> k1) c1) \<div> k1) = length (map output_fun2 (f_Exec_Comp_Stream trans_fun2 (map input_fun2 input \<odot> k2) c2) \<div> k2) \<and> (\<forall>i<length (map output_fun1 (f_Exec_Comp_Stream trans_fun1 (map input_fun1 input \<odot> k1) c1) \<div> k1). map output_fun1 (f_Exec_Comp_Stream trans_fun1 (map input_fun1 input \<odot> k1) c1) \<div> k1 ! i = map output_fun2 (f_Exec_Comp_Stream trans_fun2 (map input_fun2 input \<odot> k2) c2) \<div> k2 ! i)
[PROOF STEP]
apply (clarsimp simp: f_shrink_length)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i. \<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; i < length input\<rbrakk> \<Longrightarrow> map output_fun1 (f_Exec_Comp_Stream trans_fun1 (map input_fun1 input \<odot> k1) c1) \<div> k1 ! i = map output_fun2 (f_Exec_Comp_Stream trans_fun2 (map input_fun2 input \<odot> k2) c2) \<div> k2 ! i
[PROOF STEP]
apply (simp del: last.simps f_Exec_Stream_Cons add: f_shrink_nth take_map drop_map f_Exec_Stream_take f_Exec_Stream_drop f_expand_take_mod f_expand_drop_mod take_first)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i. \<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; i < length input\<rbrakk> \<Longrightarrow> last_message (map output_fun1 (f_Exec_Comp_Stream trans_fun1 (input_fun1 (input ! i) # NoMsg\<^bsup>k1 - Suc 0\<^esup>) (f_Exec_Comp trans_fun1 (map input_fun1 (input \<down> i) \<odot> k1) c1))) = last_message (map output_fun2 (f_Exec_Comp_Stream trans_fun2 (input_fun2 (input ! i) # NoMsg\<^bsup>k2 - Suc 0\<^esup>) (f_Exec_Comp trans_fun2 (map input_fun2 (input \<down> i) \<odot> k2) c2)))
[PROOF STEP]
apply (frule_tac n=i in subset_trans[OF set_take_subset, rule_format])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i. \<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; i < length input; set (input \<down> i) \<subseteq> A\<rbrakk> \<Longrightarrow> last_message (map output_fun1 (f_Exec_Comp_Stream trans_fun1 (input_fun1 (input ! i) # NoMsg\<^bsup>k1 - Suc 0\<^esup>) (f_Exec_Comp trans_fun1 (map input_fun1 (input \<down> i) \<odot> k1) c1))) = last_message (map output_fun2 (f_Exec_Comp_Stream trans_fun2 (input_fun2 (input ! i) # NoMsg\<^bsup>k2 - Suc 0\<^esup>) (f_Exec_Comp trans_fun2 (map input_fun2 (input \<down> i) \<odot> k2) c2)))
[PROOF STEP]
apply (unfold atomize_all atomize_imp, intro allI impI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i. \<lbrakk>0 < k1; 0 < k2; equiv_states (localState1 c1) (localState2 c2); \<forall>input0 m. set input0 \<subseteq> A \<longrightarrow> m \<in> A \<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; i < length input; set (input \<down> i) \<subseteq> A\<rbrakk> \<Longrightarrow> last_message (map output_fun1 (f_Exec_Comp_Stream trans_fun1 (input_fun1 (input ! i) # NoMsg\<^bsup>k1 - Suc 0\<^esup>) (f_Exec_Comp trans_fun1 (map input_fun1 (input \<down> i) \<odot> k1) c1))) = last_message (map output_fun2 (f_Exec_Comp_Stream trans_fun2 (input_fun2 (input ! i) # NoMsg\<^bsup>k2 - Suc 0\<^esup>) (f_Exec_Comp trans_fun2 (map input_fun2 (input \<down> i) \<odot> k2) c2)))
[PROOF STEP]
apply (frule_tac x="take i input" in spec)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i. \<lbrakk>0 < k1; 0 < k2; equiv_states (localState1 c1) (localState2 c2); \<forall>input0 m. set input0 \<subseteq> A \<longrightarrow> m \<in> A \<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; i < length input; set (input \<down> i) \<subseteq> A; \<forall>m. set (input \<down> i) \<subseteq> A \<longrightarrow> m \<in> A \<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 (input \<down> i) \<odot> k1) c1) (f_Exec_Comp trans_fun2 (map input_fun2 (input \<down> i) \<odot> k2) c2)\<rbrakk> \<Longrightarrow> last_message (map output_fun1 (f_Exec_Comp_Stream trans_fun1 (input_fun1 (input ! i) # NoMsg\<^bsup>k1 - Suc 0\<^esup>) (f_Exec_Comp trans_fun1 (map input_fun1 (input \<down> i) \<odot> k1) c1))) = last_message (map output_fun2 (f_Exec_Comp_Stream trans_fun2 (input_fun2 (input ! i) # NoMsg\<^bsup>k2 - Suc 0\<^esup>) (f_Exec_Comp trans_fun2 (map input_fun2 (input \<down> i) \<odot> k2) c2)))
[PROOF STEP]
apply (drule_tac x="input ! i" in spec)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i. \<lbrakk>0 < k1; 0 < k2; equiv_states (localState1 c1) (localState2 c2); \<forall>input0 m. set input0 \<subseteq> A \<longrightarrow> m \<in> A \<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; i < length input; set (input \<down> i) \<subseteq> A; set (input \<down> i) \<subseteq> A \<longrightarrow> input ! i \<in> A \<longrightarrow> Equiv_Exec (input ! i) 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 (input \<down> i) \<odot> k1) c1) (f_Exec_Comp trans_fun2 (map input_fun2 (input \<down> i) \<odot> k2) c2)\<rbrakk> \<Longrightarrow> last_message (map output_fun1 (f_Exec_Comp_Stream trans_fun1 (input_fun1 (input ! i) # NoMsg\<^bsup>k1 - Suc 0\<^esup>) (f_Exec_Comp trans_fun1 (map input_fun1 (input \<down> i) \<odot> k1) c1))) = last_message (map output_fun2 (f_Exec_Comp_Stream trans_fun2 (input_fun2 (input ! i) # NoMsg\<^bsup>k2 - Suc 0\<^esup>) (f_Exec_Comp trans_fun2 (map input_fun2 (input \<down> i) \<odot> k2) c2)))
[PROOF STEP]
apply (erule impE, assumption)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i. \<lbrakk>0 < k1; 0 < k2; equiv_states (localState1 c1) (localState2 c2); \<forall>input0 m. set input0 \<subseteq> A \<longrightarrow> m \<in> A \<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; i < length input; set (input \<down> i) \<subseteq> A; input ! i \<in> A \<longrightarrow> Equiv_Exec (input ! i) 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 (input \<down> i) \<odot> k1) c1) (f_Exec_Comp trans_fun2 (map input_fun2 (input \<down> i) \<odot> k2) c2)\<rbrakk> \<Longrightarrow> last_message (map output_fun1 (f_Exec_Comp_Stream trans_fun1 (input_fun1 (input ! i) # NoMsg\<^bsup>k1 - Suc 0\<^esup>) (f_Exec_Comp trans_fun1 (map input_fun1 (input \<down> i) \<odot> k1) c1))) = last_message (map output_fun2 (f_Exec_Comp_Stream trans_fun2 (input_fun2 (input ! i) # NoMsg\<^bsup>k2 - Suc 0\<^esup>) (f_Exec_Comp trans_fun2 (map input_fun2 (input \<down> i) \<odot> k2) c2)))
[PROOF STEP]
apply (erule impE)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>i. \<lbrakk>0 < k1; 0 < k2; equiv_states (localState1 c1) (localState2 c2); \<forall>input0 m. set input0 \<subseteq> A \<longrightarrow> m \<in> A \<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; i < length input; set (input \<down> i) \<subseteq> A\<rbrakk> \<Longrightarrow> input ! i \<in> A
 2. \<And>i. \<lbrakk>0 < k1; 0 < k2; equiv_states (localState1 c1) (localState2 c2); \<forall>input0 m. set input0 \<subseteq> A \<longrightarrow> m \<in> A \<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; i < length input; set (input \<down> i) \<subseteq> A; Equiv_Exec (input ! i) 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 (input \<down> i) \<odot> k1) c1) (f_Exec_Comp trans_fun2 (map input_fun2 (input \<down> i) \<odot> k2) c2)\<rbrakk> \<Longrightarrow> last_message (map output_fun1 (f_Exec_Comp_Stream trans_fun1 (input_fun1 (input ! i) # NoMsg\<^bsup>k1 - Suc 0\<^esup>) (f_Exec_Comp trans_fun1 (map input_fun1 (input \<down> i) \<odot> k1) c1))) = last_message (map output_fun2 (f_Exec_Comp_Stream trans_fun2 (input_fun2 (input ! i) # NoMsg\<^bsup>k2 - Suc 0\<^esup>) (f_Exec_Comp trans_fun2 (map input_fun2 (input \<down> i) \<odot> k2) c2)))
[PROOF STEP]
apply (blast intro: nth_mem)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i. \<lbrakk>0 < k1; 0 < k2; equiv_states (localState1 c1) (localState2 c2); \<forall>input0 m. set input0 \<subseteq> A \<longrightarrow> m \<in> A \<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; i < length input; set (input \<down> i) \<subseteq> A; Equiv_Exec (input ! i) 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 (input \<down> i) \<odot> k1) c1) (f_Exec_Comp trans_fun2 (map input_fun2 (input \<down> i) \<odot> k2) c2)\<rbrakk> \<Longrightarrow> last_message (map output_fun1 (f_Exec_Comp_Stream trans_fun1 (input_fun1 (input ! i) # NoMsg\<^bsup>k1 - Suc 0\<^esup>) (f_Exec_Comp trans_fun1 (map input_fun1 (input \<down> i) \<odot> k1) c1))) = last_message (map output_fun2 (f_Exec_Comp_Stream trans_fun2 (input_fun2 (input ! i) # NoMsg\<^bsup>k2 - Suc 0\<^esup>) (f_Exec_Comp trans_fun2 (map input_fun2 (input \<down> i) \<odot> k2) c2)))
[PROOF STEP]
apply (simp del: last.simps f_Exec_Stream_Cons)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i. \<lbrakk>0 < k1; 0 < k2; equiv_states (localState1 c1) (localState2 c2); \<forall>input0. set input0 \<subseteq> A \<longrightarrow> (\<forall>m. m \<in> A \<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; i < length input; set (input \<down> i) \<subseteq> A; Equiv_Exec (input ! i) 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 (input \<down> i) \<odot> k1) c1) (f_Exec_Comp trans_fun2 (map input_fun2 (input \<down> i) \<odot> k2) c2)\<rbrakk> \<Longrightarrow> last_message (map output_fun1 (f_Exec_Comp_Stream trans_fun1 (input_fun1 (input ! i) # NoMsg\<^bsup>k1 - Suc 0\<^esup>) (f_Exec_Comp trans_fun1 (map input_fun1 (input \<down> i) \<odot> k1) c1))) = last_message (map output_fun2 (f_Exec_Comp_Stream trans_fun2 (input_fun2 (input ! i) # NoMsg\<^bsup>k2 - Suc 0\<^esup>) (f_Exec_Comp trans_fun2 (map input_fun2 (input \<down> i) \<odot> k2) c2)))
[PROOF STEP]
apply (rule Equiv_Exec_output_eqI[of equiv_states localState1 _ localState2 _ _ input_fun1 input_fun2])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>i. \<lbrakk>0 < k1; 0 < k2; equiv_states (localState1 c1) (localState2 c2); \<forall>input0. set input0 \<subseteq> A \<longrightarrow> (\<forall>m. m \<in> A \<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; i < length input; set (input \<down> i) \<subseteq> A; Equiv_Exec (input ! i) 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 (input \<down> i) \<odot> k1) c1) (f_Exec_Comp trans_fun2 (map input_fun2 (input \<down> i) \<odot> k2) c2)\<rbrakk> \<Longrightarrow> equiv_states (localState1 (f_Exec_Comp trans_fun1 (map input_fun1 (input \<down> i) \<odot> k1) c1)) (localState2 (f_Exec_Comp trans_fun2 (map input_fun2 (input \<down> i) \<odot> k2) c2))
 2. \<And>i. \<lbrakk>0 < k1; 0 < k2; equiv_states (localState1 c1) (localState2 c2); \<forall>input0. set input0 \<subseteq> A \<longrightarrow> (\<forall>m. m \<in> A \<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; i < length input; set (input \<down> i) \<subseteq> A; Equiv_Exec (input ! i) 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 (input \<down> i) \<odot> k1) c1) (f_Exec_Comp trans_fun2 (map input_fun2 (input \<down> i) \<odot> k2) c2)\<rbrakk> \<Longrightarrow> Equiv_Exec (input ! i) 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 (input \<down> i) \<odot> k1) c1) (f_Exec_Comp trans_fun2 (map input_fun2 (input \<down> i) \<odot> k2) c2)
[PROOF STEP]
apply (case_tac i, simp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>i nat. \<lbrakk>0 < k1; 0 < k2; equiv_states (localState1 c1) (localState2 c2); \<forall>input0. set input0 \<subseteq> A \<longrightarrow> (\<forall>m. m \<in> A \<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; i < length input; set (input \<down> i) \<subseteq> A; Equiv_Exec (input ! i) 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 (input \<down> i) \<odot> k1) c1) (f_Exec_Comp trans_fun2 (map input_fun2 (input \<down> i) \<odot> k2) c2); i = Suc nat\<rbrakk> \<Longrightarrow> equiv_states (localState1 (f_Exec_Comp trans_fun1 (map input_fun1 (input \<down> i) \<odot> k1) c1)) (localState2 (f_Exec_Comp trans_fun2 (map input_fun2 (input \<down> i) \<odot> k2) c2))
 2. \<And>i. \<lbrakk>0 < k1; 0 < k2; equiv_states (localState1 c1) (localState2 c2); \<forall>input0. set input0 \<subseteq> A \<longrightarrow> (\<forall>m. m \<in> A \<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; i < length input; set (input \<down> i) \<subseteq> A; Equiv_Exec (input ! i) 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 (input \<down> i) \<odot> k1) c1) (f_Exec_Comp trans_fun2 (map input_fun2 (input \<down> i) \<odot> k2) c2)\<rbrakk> \<Longrightarrow> Equiv_Exec (input ! i) 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 (input \<down> i) \<odot> k1) c1) (f_Exec_Comp trans_fun2 (map input_fun2 (input \<down> i) \<odot> k2) c2)
[PROOF STEP]
apply (simp add: take_map[symmetric] f_Exec_Stream_expand_shrink_last_nth_eq_f_Exec_Comp[symmetric])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>i nat. \<lbrakk>0 < k1; 0 < k2; equiv_states (localState1 c1) (localState2 c2); \<forall>input0. set input0 \<subseteq> A \<longrightarrow> (\<forall>m. m \<in> A \<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; Suc nat < length input; set (input \<down> Suc nat) \<subseteq> A; Equiv_Exec (input ! Suc nat) equiv_states localState1 localState2 input_fun1 input_fun2 output_fun1 output_fun2 trans_fun1 trans_fun2 k1 k2 (f_Exec_Comp_Stream trans_fun1 (map input_fun1 input \<odot> k1) c1 \<div>\<^sub>l k1 ! nat) (f_Exec_Comp_Stream trans_fun2 (map input_fun2 input \<odot> k2) c2 \<div>\<^sub>l k2 ! nat); i = Suc nat\<rbrakk> \<Longrightarrow> equiv_states (localState1 (f_Exec_Comp_Stream trans_fun1 (map input_fun1 input \<odot> k1) c1 \<div>\<^sub>l k1 ! nat)) (localState2 (f_Exec_Comp_Stream trans_fun2 (map input_fun2 input \<odot> k2) c2 \<div>\<^sub>l k2 ! nat))
 2. \<And>i. \<lbrakk>0 < k1; 0 < k2; equiv_states (localState1 c1) (localState2 c2); \<forall>input0. set input0 \<subseteq> A \<longrightarrow> (\<forall>m. m \<in> A \<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; i < length input; set (input \<down> i) \<subseteq> A; Equiv_Exec (input ! i) 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 (input \<down> i) \<odot> k1) c1) (f_Exec_Comp trans_fun2 (map input_fun2 (input \<down> i) \<odot> k2) c2)\<rbrakk> \<Longrightarrow> Equiv_Exec (input ! i) 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 (input \<down> i) \<odot> k1) c1) (f_Exec_Comp trans_fun2 (map input_fun2 (input \<down> i) \<odot> k2) c2)
[PROOF STEP]
apply (frule Suc_lessD)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>i nat. \<lbrakk>0 < k1; 0 < k2; equiv_states (localState1 c1) (localState2 c2); \<forall>input0. set input0 \<subseteq> A \<longrightarrow> (\<forall>m. m \<in> A \<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; Suc nat < length input; set (input \<down> Suc nat) \<subseteq> A; Equiv_Exec (input ! Suc nat) equiv_states localState1 localState2 input_fun1 input_fun2 output_fun1 output_fun2 trans_fun1 trans_fun2 k1 k2 (f_Exec_Comp_Stream trans_fun1 (map input_fun1 input \<odot> k1) c1 \<div>\<^sub>l k1 ! nat) (f_Exec_Comp_Stream trans_fun2 (map input_fun2 input \<odot> k2) c2 \<div>\<^sub>l k2 ! nat); i = Suc nat; nat < length input\<rbrakk> \<Longrightarrow> equiv_states (localState1 (f_Exec_Comp_Stream trans_fun1 (map input_fun1 input \<odot> k1) c1 \<div>\<^sub>l k1 ! nat)) (localState2 (f_Exec_Comp_Stream trans_fun2 (map input_fun2 input \<odot> k2) c2 \<div>\<^sub>l k2 ! nat))
 2. \<And>i. \<lbrakk>0 < k1; 0 < k2; equiv_states (localState1 c1) (localState2 c2); \<forall>input0. set input0 \<subseteq> A \<longrightarrow> (\<forall>m. m \<in> A \<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; i < length input; set (input \<down> i) \<subseteq> A; Equiv_Exec (input ! i) 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 (input \<down> i) \<odot> k1) c1) (f_Exec_Comp trans_fun2 (map input_fun2 (input \<down> i) \<odot> k2) c2)\<rbrakk> \<Longrightarrow> Equiv_Exec (input ! i) 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 (input \<down> i) \<odot> k1) c1) (f_Exec_Comp trans_fun2 (map input_fun2 (input \<down> i) \<odot> k2) c2)
[PROOF STEP]
apply (simp add: 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 (1 subgoal):
 1. \<And>i. \<lbrakk>0 < k1; 0 < k2; equiv_states (localState1 c1) (localState2 c2); \<forall>input0. set input0 \<subseteq> A \<longrightarrow> (\<forall>m. m \<in> A \<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; i < length input; set (input \<down> i) \<subseteq> A; Equiv_Exec (input ! i) 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 (input \<down> i) \<odot> k1) c1) (f_Exec_Comp trans_fun2 (map input_fun2 (input \<down> i) \<odot> k2) c2)\<rbrakk> \<Longrightarrow> Equiv_Exec (input ! i) 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 (input \<down> i) \<odot> k1) c1) (f_Exec_Comp trans_fun2 (map input_fun2 (input \<down> i) \<odot> k2) c2)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma f_Equiv_Exec_Stream_expand_shrink_output_eq: "
  \<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>
  (map output_fun1 (
    f_Exec_Comp_Stream trans_fun1 (map input_fun1 input \<odot>\<^sub>f k1) c1)) \<div>\<^sub>f k1 =
  (map output_fun2 (
    f_Exec_Comp_Stream trans_fun2 (map input_fun2 input \<odot>\<^sub>f k2) c2)) \<div>\<^sub>f k2"
[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> map output_fun1 (f_Exec_Comp_Stream trans_fun1 (map input_fun1 input \<odot> k1) c1) \<div> k1 = map output_fun2 (f_Exec_Comp_Stream trans_fun2 (map input_fun2 input \<odot> k2) c2) \<div> k2
[PROOF STEP]
by (rule f_Equiv_Exec_Stream_expand_shrink_output_set_eq[of k1 k2 equiv_states localState1 _ localState2 _ UNIV], simp+)


[STATEMENT]
lemma i_Equiv_Exec_Stream_expand_shrink_output_set_eq: "
  \<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>
  (output_fun1 \<circ>
    i_Exec_Comp_Stream trans_fun1 ((input_fun1 \<circ> input) \<odot>\<^sub>i k1) c1) \<div>\<^sub>i k1 =
  (output_fun2 \<circ>
    i_Exec_Comp_Stream trans_fun2 ((input_fun2 \<circ> input) \<odot>\<^sub>i k2) c2) \<div>\<^sub>i k2"
[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> (output_fun1 \<circ> i_Exec_Comp_Stream trans_fun1 ((input_fun1 \<circ> input) \<odot> k1) c1) \<div> k1 = (output_fun2 \<circ> i_Exec_Comp_Stream trans_fun2 ((input_fun2 \<circ> input) \<odot> k2) c2) \<div> k2
[PROOF STEP]
apply (clarsimp simp: ilist_eq_iff, rename_tac i)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i. \<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> ((output_fun1 \<circ> i_Exec_Comp_Stream trans_fun1 ((input_fun1 \<circ> input) \<odot> k1) c1) \<div> k1) i = ((output_fun2 \<circ> i_Exec_Comp_Stream trans_fun2 ((input_fun2 \<circ> input) \<odot> k2) c2) \<div> k2) i
[PROOF STEP]
apply (simp del: last.simps f_Exec_Stream_Cons add: i_shrink_nth i_Exec_Stream_take i_Exec_Stream_drop i_expand_i_take_mod i_expand_i_drop_mod i_take_first map_one f_expand_one)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i. \<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> last_message (map output_fun1 (f_Exec_Comp_Stream trans_fun1 (input_fun1 (input i) # NoMsg\<^bsup>k1 - Suc 0\<^esup>) (f_Exec_Comp trans_fun1 (map input_fun1 (input \<Down> i) \<odot> k1) c1))) = last_message (map output_fun2 (f_Exec_Comp_Stream trans_fun2 (input_fun2 (input i) # NoMsg\<^bsup>k2 - Suc 0\<^esup>) (f_Exec_Comp trans_fun2 (map input_fun2 (input \<Down> i) \<odot> k2) c2)))
[PROOF STEP]
apply (rule Equiv_Exec_output_eqI[of
  equiv_states localState1 _ localState2 _ _
  input_fun1 input_fun2 output_fun1 output_fun2 trans_fun1 trans_fun2 k1 k2])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>i. \<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> i) \<odot> k1) c1)) (localState2 (f_Exec_Comp trans_fun2 (map input_fun2 (input \<Down> i) \<odot> k2) c2))
 2. \<And>i. \<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_Exec (input i) 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 (input \<Down> i) \<odot> k1) c1) (f_Exec_Comp trans_fun2 (map input_fun2 (input \<Down> i) \<odot> k2) c2)
[PROOF STEP]
apply (rule f_Equiv_Exec_expand_shrink_equiv_state_set[of
  k1 k2 equiv_states localState1 _ localState2 _ A
  input_fun1 input_fun2 output_fun1 output_fun2 trans_fun1 trans_fun2])
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<And>i. \<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. \<And>i. \<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. \<And>i. \<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>i 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. \<And>i. \<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> i) \<subseteq> A
 6. \<And>i. \<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_Exec (input i) 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 (input \<Down> i) \<odot> k1) c1) (f_Exec_Comp trans_fun2 (map input_fun2 (input \<Down> i) \<odot> k2) c2)
[PROOF STEP]
apply (simp add: subset_trans[OF set_i_take_subset] subsetD[OF _ rangeI])+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma i_Equiv_Exec_Stream_expand_shrink_output_eq: "
  \<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>
  (output_fun1 \<circ>
    i_Exec_Comp_Stream trans_fun1 ((input_fun1 \<circ> input) \<odot>\<^sub>i k1) c1) \<div>\<^sub>i k1 =
  (output_fun2 \<circ>
    i_Exec_Comp_Stream trans_fun2 ((input_fun2 \<circ> input) \<odot>\<^sub>i k2) c2) \<div>\<^sub>i k2"
[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> (output_fun1 \<circ> i_Exec_Comp_Stream trans_fun1 ((input_fun1 \<circ> input) \<odot> k1) c1) \<div> k1 = (output_fun2 \<circ> i_Exec_Comp_Stream trans_fun2 ((input_fun2 \<circ> input) \<odot> k2) c2) \<div> k2
[PROOF STEP]
apply (rule i_Equiv_Exec_Stream_expand_shrink_output_set_eq[of
  k1 k2 equiv_states localState1 c1 localState2 c2 UNIV
  input_fun1 input_fun2 output_fun1 output_fun2 trans_fun1 trans_fun2])
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 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> 0 < k1
 2. \<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> 0 < k2
 3. \<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 c1) (localState2 c2)
 4. \<And>input0 m. \<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); set input0 \<subseteq> UNIV; m \<in> UNIV\<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. 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> range input \<subseteq> UNIV
[PROOF STEP]
apply simp+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma f_Equiv_Exec_Stream_Acc_LocalState_set: "
  \<lbrakk> 0 < k1; 0 < k2;
    equiv_states (localState1 c1) (localState2 c2);
    Equiv_Exec_stable_set A
      equiv_states localState1 localState2
      input_fun1 input_fun2 output_fun1 output_fun2
      trans_fun1 trans_fun2 k1 k2 c1 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
    (f_Exec_Comp_Stream_Acc_LocalState k1 localState1 trans_fun1 (map input_fun1 input) c1 ! i)
    (f_Exec_Comp_Stream_Acc_LocalState k2 localState2 trans_fun2 (map input_fun2 input) c2 ! i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < k1; 0 < k2; equiv_states (localState1 c1) (localState2 c2); Equiv_Exec_stable_set A equiv_states localState1 localState2 input_fun1 input_fun2 output_fun1 output_fun2 trans_fun1 trans_fun2 k1 k2 c1 c2; set input \<subseteq> A; i < length input\<rbrakk> \<Longrightarrow> equiv_states (f_Exec_Comp_Stream_Acc_LocalState k1 localState1 trans_fun1 (map input_fun1 input) c1 ! i) (f_Exec_Comp_Stream_Acc_LocalState k2 localState2 trans_fun2 (map input_fun2 input) c2 ! i)
[PROOF STEP]
apply (unfold f_Exec_Comp_Stream_Acc_LocalState_def Equiv_Exec_stable_set_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < k1; 0 < k2; equiv_states (localState1 c1) (localState2 c2); \<forall>input m. set input \<subseteq> A \<and> m \<in> A \<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 input \<odot> k1) c1) (f_Exec_Comp trans_fun2 (map input_fun2 input \<odot> k2) c2); set input \<subseteq> A; i < length input\<rbrakk> \<Longrightarrow> equiv_states (map localState1 (f_Exec_Comp_Stream trans_fun1 (map input_fun1 input \<odot> k1) c1) \<div>\<^sub>l k1 ! i) (map localState2 (f_Exec_Comp_Stream trans_fun2 (map input_fun2 input \<odot> k2) c2) \<div>\<^sub>l k2 ! i)
[PROOF STEP]
apply (simp add: f_shrink_last_map f_shrink_last_length)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < k1; 0 < k2; equiv_states (localState1 c1) (localState2 c2); \<forall>input m. set input \<subseteq> A \<and> m \<in> A \<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 input \<odot> k1) c1) (f_Exec_Comp trans_fun2 (map input_fun2 input \<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 (rule f_Equiv_Exec_Stream_expand_shrink_equiv_state_set[of
  k1 k2 equiv_states localState1 c1 localState2 c2 A
  input_fun1 input_fun2 output_fun1 output_fun2 trans_fun1 trans_fun2 input, rule_format])
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<lbrakk>0 < k1; 0 < k2; equiv_states (localState1 c1) (localState2 c2); \<forall>input m. set input \<subseteq> A \<and> m \<in> A \<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 input \<odot> k1) c1) (f_Exec_Comp trans_fun2 (map input_fun2 input \<odot> k2) c2); set input \<subseteq> A; i < length input\<rbrakk> \<Longrightarrow> 0 < k1
 2. \<lbrakk>0 < k1; 0 < k2; equiv_states (localState1 c1) (localState2 c2); \<forall>input m. set input \<subseteq> A \<and> m \<in> A \<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 input \<odot> k1) c1) (f_Exec_Comp trans_fun2 (map input_fun2 input \<odot> k2) c2); set input \<subseteq> A; i < length input\<rbrakk> \<Longrightarrow> 0 < k2
 3. \<lbrakk>0 < k1; 0 < k2; equiv_states (localState1 c1) (localState2 c2); \<forall>input m. set input \<subseteq> A \<and> m \<in> A \<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 input \<odot> k1) c1) (f_Exec_Comp trans_fun2 (map input_fun2 input \<odot> k2) c2); set input \<subseteq> A; i < length input\<rbrakk> \<Longrightarrow> equiv_states (localState1 c1) (localState2 c2)
 4. \<And>input0 m. \<lbrakk>0 < k1; 0 < k2; equiv_states (localState1 c1) (localState2 c2); \<forall>input m. set input \<subseteq> A \<and> m \<in> A \<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 input \<odot> k1) c1) (f_Exec_Comp trans_fun2 (map input_fun2 input \<odot> k2) c2); set input \<subseteq> A; i < length input; 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); \<forall>input m. set input \<subseteq> A \<and> m \<in> A \<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 input \<odot> k1) c1) (f_Exec_Comp trans_fun2 (map input_fun2 input \<odot> k2) c2); set input \<subseteq> A; i < length input\<rbrakk> \<Longrightarrow> set input \<subseteq> A
 6. \<lbrakk>0 < k1; 0 < k2; equiv_states (localState1 c1) (localState2 c2); \<forall>input m. set input \<subseteq> A \<and> m \<in> A \<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 input \<odot> k1) c1) (f_Exec_Comp trans_fun2 (map input_fun2 input \<odot> k2) c2); set input \<subseteq> A; i < length input\<rbrakk> \<Longrightarrow> i < length input
[PROOF STEP]
apply simp+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma f_Equiv_Exec_Stream_Acc_LocalState: "
  \<lbrakk> 0 < k1; 0 < k2;
    equiv_states (localState1 c1) (localState2 c2);
    Equiv_Exec_stable
      equiv_states localState1 localState2
      input_fun1 input_fun2 output_fun1 output_fun2
      trans_fun1 trans_fun2 k1 k2 c1 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>
    i < length input \<rbrakk> \<Longrightarrow>
  equiv_states
    (f_Exec_Comp_Stream_Acc_LocalState k1 localState1 trans_fun1 (map input_fun1 input) c1 ! i)
    (f_Exec_Comp_Stream_Acc_LocalState k2 localState2 trans_fun2 (map input_fun2 input) c2 ! i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < k1; 0 < k2; equiv_states (localState1 c1) (localState2 c2); Equiv_Exec_stable equiv_states localState1 localState2 input_fun1 input_fun2 output_fun1 output_fun2 trans_fun1 trans_fun2 k1 k2 c1 c2; i < length input\<rbrakk> \<Longrightarrow> equiv_states (f_Exec_Comp_Stream_Acc_LocalState k1 localState1 trans_fun1 (map input_fun1 input) c1 ! i) (f_Exec_Comp_Stream_Acc_LocalState k2 localState2 trans_fun2 (map input_fun2 input) c2 ! i)
[PROOF STEP]
apply (rule f_Equiv_Exec_Stream_Acc_LocalState_set[where A=UNIV])
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<lbrakk>0 < k1; 0 < k2; equiv_states (localState1 c1) (localState2 c2); Equiv_Exec_stable equiv_states localState1 localState2 input_fun1 input_fun2 output_fun1 output_fun2 trans_fun1 trans_fun2 k1 k2 c1 c2; i < length input\<rbrakk> \<Longrightarrow> 0 < k1
 2. \<lbrakk>0 < k1; 0 < k2; equiv_states (localState1 c1) (localState2 c2); Equiv_Exec_stable equiv_states localState1 localState2 input_fun1 input_fun2 output_fun1 output_fun2 trans_fun1 trans_fun2 k1 k2 c1 c2; i < length input\<rbrakk> \<Longrightarrow> 0 < k2
 3. \<lbrakk>0 < k1; 0 < k2; equiv_states (localState1 c1) (localState2 c2); Equiv_Exec_stable equiv_states localState1 localState2 input_fun1 input_fun2 output_fun1 output_fun2 trans_fun1 trans_fun2 k1 k2 c1 c2; i < length input\<rbrakk> \<Longrightarrow> equiv_states (localState1 c1) (localState2 c2)
 4. \<lbrakk>0 < k1; 0 < k2; equiv_states (localState1 c1) (localState2 c2); Equiv_Exec_stable equiv_states localState1 localState2 input_fun1 input_fun2 output_fun1 output_fun2 trans_fun1 trans_fun2 k1 k2 c1 c2; i < length input\<rbrakk> \<Longrightarrow> Equiv_Exec_stable_set UNIV equiv_states localState1 localState2 input_fun1 input_fun2 ?output_fun1.0 ?output_fun2.0 trans_fun1 trans_fun2 k1 k2 c1 c2
 5. \<lbrakk>0 < k1; 0 < k2; equiv_states (localState1 c1) (localState2 c2); Equiv_Exec_stable equiv_states localState1 localState2 input_fun1 input_fun2 output_fun1 output_fun2 trans_fun1 trans_fun2 k1 k2 c1 c2; i < length input\<rbrakk> \<Longrightarrow> set input \<subseteq> UNIV
 6. \<lbrakk>0 < k1; 0 < k2; equiv_states (localState1 c1) (localState2 c2); Equiv_Exec_stable equiv_states localState1 localState2 input_fun1 input_fun2 output_fun1 output_fun2 trans_fun1 trans_fun2 k1 k2 c1 c2; i < length input\<rbrakk> \<Longrightarrow> i < length input
[PROOF STEP]
apply (simp add: Equiv_Exec_stable_set_UNIV)+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma f_Equiv_Exec_Stream_Acc_Output_set_eq: "
  \<lbrakk> 0 < k1; 0 < k2;
    equiv_states (localState1 c1) (localState2 c2);
    Equiv_Exec_stable_set A
      equiv_states localState1 localState2
      input_fun1 input_fun2 output_fun1 output_fun2 trans_fun1 trans_fun2 k1 k2 c1 c2;
    set input \<subseteq> A \<rbrakk> \<Longrightarrow>
  f_Exec_Comp_Stream_Acc_Output k1 output_fun1 trans_fun1 (map input_fun1 input) c1 =
  f_Exec_Comp_Stream_Acc_Output k2 output_fun2 trans_fun2 (map input_fun2 input) c2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < k1; 0 < k2; equiv_states (localState1 c1) (localState2 c2); Equiv_Exec_stable_set A equiv_states localState1 localState2 input_fun1 input_fun2 output_fun1 output_fun2 trans_fun1 trans_fun2 k1 k2 c1 c2; set input \<subseteq> A\<rbrakk> \<Longrightarrow> f_Exec_Comp_Stream_Acc_Output k1 output_fun1 trans_fun1 (map input_fun1 input) c1 = f_Exec_Comp_Stream_Acc_Output k2 output_fun2 trans_fun2 (map input_fun2 input) c2
[PROOF STEP]
apply (unfold f_Exec_Comp_Stream_Acc_Output_def Equiv_Exec_stable_set_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < k1; 0 < k2; equiv_states (localState1 c1) (localState2 c2); \<forall>input m. set input \<subseteq> A \<and> m \<in> A \<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 input \<odot> k1) c1) (f_Exec_Comp trans_fun2 (map input_fun2 input \<odot> k2) c2); set input \<subseteq> A\<rbrakk> \<Longrightarrow> map output_fun1 (f_Exec_Comp_Stream trans_fun1 (map input_fun1 input \<odot> k1) c1) \<div> k1 = map output_fun2 (f_Exec_Comp_Stream trans_fun2 (map input_fun2 input \<odot> k2) c2) \<div> k2
[PROOF STEP]
apply (rule f_Equiv_Exec_Stream_expand_shrink_output_set_eq[of
  k1 k2 equiv_states localState1 c1 localState2 c2
  A input_fun1 input_fun2 output_fun1 output_fun2 trans_fun1 trans_fun2 input])
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<lbrakk>0 < k1; 0 < k2; equiv_states (localState1 c1) (localState2 c2); \<forall>input m. set input \<subseteq> A \<and> m \<in> A \<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 input \<odot> k1) c1) (f_Exec_Comp trans_fun2 (map input_fun2 input \<odot> k2) c2); set input \<subseteq> A\<rbrakk> \<Longrightarrow> 0 < k1
 2. \<lbrakk>0 < k1; 0 < k2; equiv_states (localState1 c1) (localState2 c2); \<forall>input m. set input \<subseteq> A \<and> m \<in> A \<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 input \<odot> k1) c1) (f_Exec_Comp trans_fun2 (map input_fun2 input \<odot> k2) c2); set input \<subseteq> A\<rbrakk> \<Longrightarrow> 0 < k2
 3. \<lbrakk>0 < k1; 0 < k2; equiv_states (localState1 c1) (localState2 c2); \<forall>input m. set input \<subseteq> A \<and> m \<in> A \<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 input \<odot> k1) c1) (f_Exec_Comp trans_fun2 (map input_fun2 input \<odot> k2) c2); set 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); \<forall>input m. set input \<subseteq> A \<and> m \<in> A \<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 input \<odot> k1) c1) (f_Exec_Comp trans_fun2 (map input_fun2 input \<odot> k2) c2); 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) 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); \<forall>input m. set input \<subseteq> A \<and> m \<in> A \<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 input \<odot> k1) c1) (f_Exec_Comp trans_fun2 (map input_fun2 input \<odot> k2) c2); set input \<subseteq> A\<rbrakk> \<Longrightarrow> set input \<subseteq> A
[PROOF STEP]
apply simp+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma f_Equiv_Exec_Stream_Acc_Output_eq: "
  \<lbrakk> 0 < k1; 0 < k2;
    equiv_states (localState1 c1) (localState2 c2);
    Equiv_Exec_stable
      equiv_states localState1 localState2
      input_fun1 input_fun2 output_fun1 output_fun2 trans_fun1 trans_fun2 k1 k2 c1 c2 \<rbrakk> \<Longrightarrow>
  f_Exec_Comp_Stream_Acc_Output k1 output_fun1 trans_fun1 (map input_fun1 input) c1 =
  f_Exec_Comp_Stream_Acc_Output k2 output_fun2 trans_fun2 (map input_fun2 input) c2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < k1; 0 < k2; equiv_states (localState1 c1) (localState2 c2); Equiv_Exec_stable equiv_states localState1 localState2 input_fun1 input_fun2 output_fun1 output_fun2 trans_fun1 trans_fun2 k1 k2 c1 c2\<rbrakk> \<Longrightarrow> f_Exec_Comp_Stream_Acc_Output k1 output_fun1 trans_fun1 (map input_fun1 input) c1 = f_Exec_Comp_Stream_Acc_Output k2 output_fun2 trans_fun2 (map input_fun2 input) c2
[PROOF STEP]
apply (rule f_Equiv_Exec_Stream_Acc_Output_set_eq[of k1 k2 equiv_states localState1 c1 localState2 c2 UNIV])
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<lbrakk>0 < k1; 0 < k2; equiv_states (localState1 c1) (localState2 c2); Equiv_Exec_stable equiv_states localState1 localState2 input_fun1 input_fun2 output_fun1 output_fun2 trans_fun1 trans_fun2 k1 k2 c1 c2\<rbrakk> \<Longrightarrow> 0 < k1
 2. \<lbrakk>0 < k1; 0 < k2; equiv_states (localState1 c1) (localState2 c2); Equiv_Exec_stable equiv_states localState1 localState2 input_fun1 input_fun2 output_fun1 output_fun2 trans_fun1 trans_fun2 k1 k2 c1 c2\<rbrakk> \<Longrightarrow> 0 < k2
 3. \<lbrakk>0 < k1; 0 < k2; equiv_states (localState1 c1) (localState2 c2); Equiv_Exec_stable 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 c1) (localState2 c2)
 4. \<lbrakk>0 < k1; 0 < k2; equiv_states (localState1 c1) (localState2 c2); Equiv_Exec_stable equiv_states localState1 localState2 input_fun1 input_fun2 output_fun1 output_fun2 trans_fun1 trans_fun2 k1 k2 c1 c2\<rbrakk> \<Longrightarrow> Equiv_Exec_stable_set UNIV equiv_states localState1 localState2 input_fun1 input_fun2 output_fun1 output_fun2 trans_fun1 trans_fun2 k1 k2 c1 c2
 5. \<lbrakk>0 < k1; 0 < k2; equiv_states (localState1 c1) (localState2 c2); Equiv_Exec_stable equiv_states localState1 localState2 input_fun1 input_fun2 output_fun1 output_fun2 trans_fun1 trans_fun2 k1 k2 c1 c2\<rbrakk> \<Longrightarrow> set input \<subseteq> UNIV
[PROOF STEP]
apply (simp add: Equiv_Exec_stable_set_UNIV)+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma i_Equiv_Exec_Stream_Acc_LocalState_set: "
  \<lbrakk> 0 < k1; 0 < k2;
    equiv_states (localState1 c1) (localState2 c2);
    Equiv_Exec_stable_set A
      equiv_states localState1 localState2 input_fun1 input_fun2 output_fun1 output_fun2
      trans_fun1 trans_fun2 k1 k2 c1 c2;
    range input \<subseteq> A \<rbrakk> \<Longrightarrow>
  equiv_states
    (i_Exec_Comp_Stream_Acc_LocalState k1 localState1 trans_fun1 (input_fun1 \<circ> input) c1 i)
    (i_Exec_Comp_Stream_Acc_LocalState k2 localState2 trans_fun2 (input_fun2 \<circ> input) c2 i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < k1; 0 < k2; equiv_states (localState1 c1) (localState2 c2); Equiv_Exec_stable_set A equiv_states localState1 localState2 input_fun1 input_fun2 output_fun1 output_fun2 trans_fun1 trans_fun2 k1 k2 c1 c2; range input \<subseteq> A\<rbrakk> \<Longrightarrow> equiv_states (i_Exec_Comp_Stream_Acc_LocalState k1 localState1 trans_fun1 (input_fun1 \<circ> input) c1 i) (i_Exec_Comp_Stream_Acc_LocalState k2 localState2 trans_fun2 (input_fun2 \<circ> input) c2 i)
[PROOF STEP]
apply (simp add: i_Exec_Stream_Acc_LocalState_nth_f_nth)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < k1; 0 < k2; equiv_states (localState1 c1) (localState2 c2); Equiv_Exec_stable_set A equiv_states localState1 localState2 input_fun1 input_fun2 output_fun1 output_fun2 trans_fun1 trans_fun2 k1 k2 c1 c2; range input \<subseteq> A\<rbrakk> \<Longrightarrow> equiv_states (f_Exec_Comp_Stream_Acc_LocalState k1 localState1 trans_fun1 (map input_fun1 (input \<Down> Suc i)) c1 ! i) (f_Exec_Comp_Stream_Acc_LocalState k2 localState2 trans_fun2 (map input_fun2 (input \<Down> Suc i)) c2 ! i)
[PROOF STEP]
apply (rule f_Equiv_Exec_Stream_Acc_LocalState_set)
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<lbrakk>0 < k1; 0 < k2; equiv_states (localState1 c1) (localState2 c2); Equiv_Exec_stable_set A equiv_states localState1 localState2 input_fun1 input_fun2 output_fun1 output_fun2 trans_fun1 trans_fun2 k1 k2 c1 c2; range input \<subseteq> A\<rbrakk> \<Longrightarrow> 0 < k1
 2. \<lbrakk>0 < k1; 0 < k2; equiv_states (localState1 c1) (localState2 c2); Equiv_Exec_stable_set A equiv_states localState1 localState2 input_fun1 input_fun2 output_fun1 output_fun2 trans_fun1 trans_fun2 k1 k2 c1 c2; range input \<subseteq> A\<rbrakk> \<Longrightarrow> 0 < k2
 3. \<lbrakk>0 < k1; 0 < k2; equiv_states (localState1 c1) (localState2 c2); Equiv_Exec_stable_set A equiv_states localState1 localState2 input_fun1 input_fun2 output_fun1 output_fun2 trans_fun1 trans_fun2 k1 k2 c1 c2; range input \<subseteq> A\<rbrakk> \<Longrightarrow> equiv_states (localState1 c1) (localState2 c2)
 4. \<lbrakk>0 < k1; 0 < k2; equiv_states (localState1 c1) (localState2 c2); Equiv_Exec_stable_set A equiv_states localState1 localState2 input_fun1 input_fun2 output_fun1 output_fun2 trans_fun1 trans_fun2 k1 k2 c1 c2; range input \<subseteq> A\<rbrakk> \<Longrightarrow> Equiv_Exec_stable_set ?A6 equiv_states localState1 localState2 input_fun1 input_fun2 ?output_fun1.6 ?output_fun2.6 trans_fun1 trans_fun2 k1 k2 c1 c2
 5. \<lbrakk>0 < k1; 0 < k2; equiv_states (localState1 c1) (localState2 c2); Equiv_Exec_stable_set A equiv_states localState1 localState2 input_fun1 input_fun2 output_fun1 output_fun2 trans_fun1 trans_fun2 k1 k2 c1 c2; range input \<subseteq> A\<rbrakk> \<Longrightarrow> set (input \<Down> Suc i) \<subseteq> ?A6
 6. \<lbrakk>0 < k1; 0 < k2; equiv_states (localState1 c1) (localState2 c2); Equiv_Exec_stable_set A equiv_states localState1 localState2 input_fun1 input_fun2 output_fun1 output_fun2 trans_fun1 trans_fun2 k1 k2 c1 c2; range input \<subseteq> A\<rbrakk> \<Longrightarrow> i < length (input \<Down> Suc i)
[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_Acc_LocalState: "
  \<lbrakk> 0 < k1; 0 < k2;
    equiv_states (localState1 c1) (localState2 c2);
    Equiv_Exec_stable
      equiv_states localState1 localState2
      input_fun1 input_fun2 output_fun1 output_fun2
      trans_fun1 trans_fun2 k1 k2 c1 c2 \<rbrakk> \<Longrightarrow>
  equiv_states
    (i_Exec_Comp_Stream_Acc_LocalState k1 localState1 trans_fun1 (input_fun1 \<circ> input) c1 i)
    (i_Exec_Comp_Stream_Acc_LocalState k2 localState2 trans_fun2 (input_fun2 \<circ> input) c2 i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < k1; 0 < k2; equiv_states (localState1 c1) (localState2 c2); Equiv_Exec_stable equiv_states localState1 localState2 input_fun1 input_fun2 output_fun1 output_fun2 trans_fun1 trans_fun2 k1 k2 c1 c2\<rbrakk> \<Longrightarrow> equiv_states (i_Exec_Comp_Stream_Acc_LocalState k1 localState1 trans_fun1 (input_fun1 \<circ> input) c1 i) (i_Exec_Comp_Stream_Acc_LocalState k2 localState2 trans_fun2 (input_fun2 \<circ> input) c2 i)
[PROOF STEP]
apply (rule i_Equiv_Exec_Stream_Acc_LocalState_set[where A=UNIV])
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<lbrakk>0 < k1; 0 < k2; equiv_states (localState1 c1) (localState2 c2); Equiv_Exec_stable equiv_states localState1 localState2 input_fun1 input_fun2 output_fun1 output_fun2 trans_fun1 trans_fun2 k1 k2 c1 c2\<rbrakk> \<Longrightarrow> 0 < k1
 2. \<lbrakk>0 < k1; 0 < k2; equiv_states (localState1 c1) (localState2 c2); Equiv_Exec_stable equiv_states localState1 localState2 input_fun1 input_fun2 output_fun1 output_fun2 trans_fun1 trans_fun2 k1 k2 c1 c2\<rbrakk> \<Longrightarrow> 0 < k2
 3. \<lbrakk>0 < k1; 0 < k2; equiv_states (localState1 c1) (localState2 c2); Equiv_Exec_stable 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 c1) (localState2 c2)
 4. \<lbrakk>0 < k1; 0 < k2; equiv_states (localState1 c1) (localState2 c2); Equiv_Exec_stable equiv_states localState1 localState2 input_fun1 input_fun2 output_fun1 output_fun2 trans_fun1 trans_fun2 k1 k2 c1 c2\<rbrakk> \<Longrightarrow> Equiv_Exec_stable_set UNIV equiv_states localState1 localState2 input_fun1 input_fun2 ?output_fun1.0 ?output_fun2.0 trans_fun1 trans_fun2 k1 k2 c1 c2
 5. \<lbrakk>0 < k1; 0 < k2; equiv_states (localState1 c1) (localState2 c2); Equiv_Exec_stable equiv_states localState1 localState2 input_fun1 input_fun2 output_fun1 output_fun2 trans_fun1 trans_fun2 k1 k2 c1 c2\<rbrakk> \<Longrightarrow> range input \<subseteq> UNIV
[PROOF STEP]
apply (simp add: Equiv_Exec_stable_set_UNIV)+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma i_Equiv_Exec_Stream_Acc_Output_set_eq: "
  \<lbrakk> 0 < k1; 0 < k2;
    equiv_states (localState1 c1) (localState2 c2);
    Equiv_Exec_stable_set A
      equiv_states localState1 localState2
      input_fun1 input_fun2 output_fun1 output_fun2 trans_fun1 trans_fun2 k1 k2 c1 c2;
    range input \<subseteq> A \<rbrakk> \<Longrightarrow>
  i_Exec_Comp_Stream_Acc_Output k1 output_fun1 trans_fun1 (input_fun1 \<circ> input) c1 =
  i_Exec_Comp_Stream_Acc_Output k2 output_fun2 trans_fun2 (input_fun2 \<circ> input) c2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < k1; 0 < k2; equiv_states (localState1 c1) (localState2 c2); Equiv_Exec_stable_set A equiv_states localState1 localState2 input_fun1 input_fun2 output_fun1 output_fun2 trans_fun1 trans_fun2 k1 k2 c1 c2; range input \<subseteq> A\<rbrakk> \<Longrightarrow> i_Exec_Comp_Stream_Acc_Output k1 output_fun1 trans_fun1 (input_fun1 \<circ> input) c1 = i_Exec_Comp_Stream_Acc_Output k2 output_fun2 trans_fun2 (input_fun2 \<circ> input) c2
[PROOF STEP]
apply (clarsimp simp: ilist_eq_iff i_Exec_Stream_Acc_Output_nth_f_nth, rename_tac i)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i. \<lbrakk>0 < k1; 0 < k2; equiv_states (localState1 c1) (localState2 c2); Equiv_Exec_stable_set A equiv_states localState1 localState2 input_fun1 input_fun2 output_fun1 output_fun2 trans_fun1 trans_fun2 k1 k2 c1 c2; range input \<subseteq> A\<rbrakk> \<Longrightarrow> f_Exec_Comp_Stream_Acc_Output k1 output_fun1 trans_fun1 (map input_fun1 (input \<Down> Suc i)) c1 ! i = f_Exec_Comp_Stream_Acc_Output k2 output_fun2 trans_fun2 (map input_fun2 (input \<Down> Suc i)) c2 ! i
[PROOF STEP]
apply (drule_tac n="Suc i" in subset_trans[OF set_i_take_subset, rule_format])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i. \<lbrakk>0 < k1; 0 < k2; equiv_states (localState1 c1) (localState2 c2); Equiv_Exec_stable_set A equiv_states localState1 localState2 input_fun1 input_fun2 output_fun1 output_fun2 trans_fun1 trans_fun2 k1 k2 c1 c2; set (input \<Down> Suc i) \<subseteq> A\<rbrakk> \<Longrightarrow> f_Exec_Comp_Stream_Acc_Output k1 output_fun1 trans_fun1 (map input_fun1 (input \<Down> Suc i)) c1 ! i = f_Exec_Comp_Stream_Acc_Output k2 output_fun2 trans_fun2 (map input_fun2 (input \<Down> Suc i)) c2 ! i
[PROOF STEP]
apply (simp add: f_Equiv_Exec_Stream_Acc_Output_set_eq[where equiv_states=equiv_states])
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma i_Equiv_Exec_Stream_Acc_Output_eq: "
  \<lbrakk> 0 < k1; 0 < k2;
    equiv_states (localState1 c1) (localState2 c2);
    Equiv_Exec_stable
      equiv_states localState1 localState2
      input_fun1 input_fun2 output_fun1 output_fun2 trans_fun1 trans_fun2 k1 k2 c1 c2 \<rbrakk> \<Longrightarrow>
  i_Exec_Comp_Stream_Acc_Output k1 output_fun1 trans_fun1 (input_fun1 \<circ> input) c1 =
  i_Exec_Comp_Stream_Acc_Output k2 output_fun2 trans_fun2 (input_fun2 \<circ> input) c2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < k1; 0 < k2; equiv_states (localState1 c1) (localState2 c2); Equiv_Exec_stable equiv_states localState1 localState2 input_fun1 input_fun2 output_fun1 output_fun2 trans_fun1 trans_fun2 k1 k2 c1 c2\<rbrakk> \<Longrightarrow> i_Exec_Comp_Stream_Acc_Output k1 output_fun1 trans_fun1 (input_fun1 \<circ> input) c1 = i_Exec_Comp_Stream_Acc_Output k2 output_fun2 trans_fun2 (input_fun2 \<circ> input) c2
[PROOF STEP]
apply (rule i_Equiv_Exec_Stream_Acc_Output_set_eq[of k1 k2 equiv_states localState1 c1 localState2 c2 UNIV])
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<lbrakk>0 < k1; 0 < k2; equiv_states (localState1 c1) (localState2 c2); Equiv_Exec_stable equiv_states localState1 localState2 input_fun1 input_fun2 output_fun1 output_fun2 trans_fun1 trans_fun2 k1 k2 c1 c2\<rbrakk> \<Longrightarrow> 0 < k1
 2. \<lbrakk>0 < k1; 0 < k2; equiv_states (localState1 c1) (localState2 c2); Equiv_Exec_stable equiv_states localState1 localState2 input_fun1 input_fun2 output_fun1 output_fun2 trans_fun1 trans_fun2 k1 k2 c1 c2\<rbrakk> \<Longrightarrow> 0 < k2
 3. \<lbrakk>0 < k1; 0 < k2; equiv_states (localState1 c1) (localState2 c2); Equiv_Exec_stable 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 c1) (localState2 c2)
 4. \<lbrakk>0 < k1; 0 < k2; equiv_states (localState1 c1) (localState2 c2); Equiv_Exec_stable equiv_states localState1 localState2 input_fun1 input_fun2 output_fun1 output_fun2 trans_fun1 trans_fun2 k1 k2 c1 c2\<rbrakk> \<Longrightarrow> Equiv_Exec_stable_set UNIV equiv_states localState1 localState2 input_fun1 input_fun2 output_fun1 output_fun2 trans_fun1 trans_fun2 k1 k2 c1 c2
 5. \<lbrakk>0 < k1; 0 < k2; equiv_states (localState1 c1) (localState2 c2); Equiv_Exec_stable equiv_states localState1 localState2 input_fun1 input_fun2 output_fun1 output_fun2 trans_fun1 trans_fun2 k1 k2 c1 c2\<rbrakk> \<Longrightarrow> range input \<subseteq> UNIV
[PROOF STEP]
apply (simp add: Equiv_Exec_stable_set_UNIV)+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done