[STATEMENT]
lemma i_Exec_Stream_nth_gr0_calc: "
  0 < n \<Longrightarrow>
  (i_Exec_Comp_Stream trans_fun input c) n =
  trans_fun (input n) ((i_Exec_Comp_Stream trans_fun input c) (n - 1))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < n \<Longrightarrow> i_Exec_Comp_Stream trans_fun input c n = trans_fun (input n) (i_Exec_Comp_Stream trans_fun input c (n - 1))
[PROOF STEP]
by (simp add: i_Exec_Stream_nth i_take_Suc_conv_app_nth f_Exec_append)


[STATEMENT]
lemma i_Exec_Stream_nth_calc_Previous: "
  i_Exec_Comp_Stream trans_fun input c n =
  trans_fun (input n) ((i_Exec_Comp_Stream trans_fun input c)\<^bsup>\<leftarrow> c\<^esup> n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i_Exec_Comp_Stream trans_fun input c n = trans_fun (input n) ((i_Exec_Comp_Stream trans_fun input c)\<^bsup>\<leftarrow> c\<^esup> n)
[PROOF STEP]
by (simp add: i_Exec_Stream_nth ilist_Previous_nth_if i_take_first i_take_Suc_conv_app_nth f_Exec_append)


[STATEMENT]
lemma f_Exec_Stream_Init_nth_Suc_calc: "
  n < length xs \<Longrightarrow>
  f_Exec_Comp_Stream_Init trans_fun xs c ! Suc n =
  trans_fun (xs ! n) (f_Exec_Comp_Stream_Init trans_fun xs c ! n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n < length xs \<Longrightarrow> f_Exec_Comp_Stream_Init trans_fun xs c ! Suc n = trans_fun (xs ! n) (f_Exec_Comp_Stream_Init trans_fun xs c ! n)
[PROOF STEP]
by (simp add: f_Exec_Stream_Init_eq_f_Exec_Stream_Cons f_Exec_Stream_nth nth_Cons' length_greater_0_conv[THEN iffD1, OF gr_implies_gr0] take_Suc_conv_app_nth f_Exec_append)


[STATEMENT]
lemma f_Exec_Stream_Init_nth_Plus1_calc: "
  n < length xs \<Longrightarrow>
  f_Exec_Comp_Stream_Init trans_fun xs c ! (n + 1)=
  trans_fun (xs ! n) (f_Exec_Comp_Stream_Init trans_fun xs c ! n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n < length xs \<Longrightarrow> f_Exec_Comp_Stream_Init trans_fun xs c ! (n + 1) = trans_fun (xs ! n) (f_Exec_Comp_Stream_Init trans_fun xs c ! n)
[PROOF STEP]
by (simp add: f_Exec_Stream_Init_nth_Suc_calc)


[STATEMENT]
lemma f_Exec_Stream_Init_nth_gr0_calc: "
  \<lbrakk> n \<le> length xs; 0 < n \<rbrakk> \<Longrightarrow>
  f_Exec_Comp_Stream_Init trans_fun xs c ! n =
  trans_fun (xs ! (n - 1)) (f_Exec_Comp_Stream_Init trans_fun xs c ! (n - 1))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n \<le> length xs; 0 < n\<rbrakk> \<Longrightarrow> f_Exec_Comp_Stream_Init trans_fun xs c ! n = trans_fun (xs ! (n - 1)) (f_Exec_Comp_Stream_Init trans_fun xs c ! (n - 1))
[PROOF STEP]
by (clarsimp simp: gr0_conv_Suc f_Exec_Stream_Init_nth_Suc_calc)


[STATEMENT]
lemma i_Exec_Stream_Init_nth_Suc_calc: "
  i_Exec_Comp_Stream_Init trans_fun input c (Suc n) =
  trans_fun (input n) (i_Exec_Comp_Stream_Init trans_fun input c n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i_Exec_Comp_Stream_Init trans_fun input c (Suc n) = trans_fun (input n) (i_Exec_Comp_Stream_Init trans_fun input c n)
[PROOF STEP]
by (simp add: i_Exec_Stream_Init_nth i_take_Suc_conv_app_nth f_Exec_append)


[STATEMENT]
lemma i_Exec_Stream_Init_nth_Plus1_calc: "
  i_Exec_Comp_Stream_Init trans_fun input c (n + 1) =
  trans_fun (input n) (i_Exec_Comp_Stream_Init trans_fun input c n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i_Exec_Comp_Stream_Init trans_fun input c (n + 1) = trans_fun (input n) (i_Exec_Comp_Stream_Init trans_fun input c n)
[PROOF STEP]
by (simp add: i_Exec_Stream_Init_nth_Suc_calc)


[STATEMENT]
lemma i_Exec_Stream_Init_nth_gr0_calc: "
  0 < n \<Longrightarrow>
  i_Exec_Comp_Stream_Init trans_fun input c n =
  trans_fun (input (n - 1)) (i_Exec_Comp_Stream_Init trans_fun input c (n - 1))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < n \<Longrightarrow> i_Exec_Comp_Stream_Init trans_fun input c n = trans_fun (input (n - 1)) (i_Exec_Comp_Stream_Init trans_fun input c (n - 1))
[PROOF STEP]
by (clarsimp simp: gr0_conv_Suc i_Exec_Stream_Init_nth_Suc_calc)


[STATEMENT]
lemma f_Exec_Stream_Pre_Post1: "
  \<lbrakk> n < length xs;
    c_n = (f_Exec_Comp_Stream trans_fun xs c)\<^bsup>\<leftarrow>' c\<^esup> n; x_n = xs ! n \<rbrakk> \<Longrightarrow>
  (P1 x_n \<and> P2 c_n \<longrightarrow> Q (f_Exec_Comp_Stream trans_fun xs c ! n)) =
  (P1 x_n \<and> P2 c_n \<longrightarrow> Q (trans_fun x_n c_n))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n < length xs; c_n = (f_Exec_Comp_Stream trans_fun xs c)\<^bsup>\<leftarrow>' c\<^esup> n; x_n = xs ! n\<rbrakk> \<Longrightarrow> (P1 x_n \<and> P2 c_n \<longrightarrow> Q (f_Exec_Comp_Stream trans_fun xs c ! n)) = (P1 x_n \<and> P2 c_n \<longrightarrow> Q (trans_fun x_n c_n))
[PROOF STEP]
by (simp add: f_Exec_Stream_nth_calc_Previous)


[STATEMENT]
lemma f_Exec_Stream_Pre_Post2: "
  \<lbrakk> n < length xs;
    c_n = (f_Exec_Comp_Stream trans_fun xs c)\<^bsup>\<leftarrow>' c\<^esup> n; x_n = xs ! n \<rbrakk> \<Longrightarrow>
  (P c_n \<longrightarrow> Q (xs ! n) (f_Exec_Comp_Stream trans_fun xs c ! n)) =
  (P c_n \<longrightarrow> Q x_n (trans_fun x_n c_n))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n < length xs; c_n = (f_Exec_Comp_Stream trans_fun xs c)\<^bsup>\<leftarrow>' c\<^esup> n; x_n = xs ! n\<rbrakk> \<Longrightarrow> (P c_n \<longrightarrow> Q (xs ! n) (f_Exec_Comp_Stream trans_fun xs c ! n)) = (P c_n \<longrightarrow> Q x_n (trans_fun x_n c_n))
[PROOF STEP]
by (simp add: f_Exec_Stream_nth_calc_Previous)


[STATEMENT]
lemma f_Exec_Stream_Pre_Post2_Suc: "
  \<lbrakk> Suc n < length xs;
    c_n = f_Exec_Comp_Stream trans_fun xs c ! n; x_n1 = xs ! Suc n \<rbrakk> \<Longrightarrow>
  (P c_n \<longrightarrow> Q (xs ! Suc n) (f_Exec_Comp_Stream trans_fun xs c ! Suc n)) =
  (P c_n \<longrightarrow> Q x_n1 (trans_fun x_n1 c_n))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Suc n < length xs; c_n = f_Exec_Comp_Stream trans_fun xs c ! n; x_n1 = xs ! Suc n\<rbrakk> \<Longrightarrow> (P c_n \<longrightarrow> Q (xs ! Suc n) (f_Exec_Comp_Stream trans_fun xs c ! Suc n)) = (P c_n \<longrightarrow> Q x_n1 (trans_fun x_n1 c_n))
[PROOF STEP]
by (simp add: f_Exec_Stream_nth_gr0_calc)


[STATEMENT]
lemma f_Exec_Stream_Init_Pre_Post1: "
  \<lbrakk> n < length xs;
    c_n = f_Exec_Comp_Stream_Init trans_fun xs c ! n; x_n = xs ! n \<rbrakk> \<Longrightarrow>
  (P1 x_n \<and> P2 c_n \<longrightarrow> Q (f_Exec_Comp_Stream_Init trans_fun xs c ! Suc n)) =
  (P1 x_n \<and> P2 c_n \<longrightarrow> Q (trans_fun x_n c_n))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n < length xs; c_n = f_Exec_Comp_Stream_Init trans_fun xs c ! n; x_n = xs ! n\<rbrakk> \<Longrightarrow> (P1 x_n \<and> P2 c_n \<longrightarrow> Q (f_Exec_Comp_Stream_Init trans_fun xs c ! Suc n)) = (P1 x_n \<and> P2 c_n \<longrightarrow> Q (trans_fun x_n c_n))
[PROOF STEP]
by (simp add: f_Exec_Stream_Init_nth_Suc_calc)


[STATEMENT]
lemma f_Exec_Stream_Init_Pre_Post2: "
  \<lbrakk> n < length xs;
    c_n = f_Exec_Comp_Stream_Init trans_fun xs c ! n; x_n = xs ! n \<rbrakk> \<Longrightarrow>
  (P (xs ! n) (f_Exec_Comp_Stream_Init trans_fun xs c ! n) \<longrightarrow>
     Q (f_Exec_Comp_Stream_Init trans_fun xs c ! Suc n)) =
  (P x_n c_n \<longrightarrow> Q (trans_fun x_n c_n))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n < length xs; c_n = f_Exec_Comp_Stream_Init trans_fun xs c ! n; x_n = xs ! n\<rbrakk> \<Longrightarrow> (P (xs ! n) (f_Exec_Comp_Stream_Init trans_fun xs c ! n) \<longrightarrow> Q (f_Exec_Comp_Stream_Init trans_fun xs c ! Suc n)) = (P x_n c_n \<longrightarrow> Q (trans_fun x_n c_n))
[PROOF STEP]
by (simp add: f_Exec_Stream_Init_nth_Suc_calc)


[STATEMENT]
lemma i_Exec_Stream_Pre_Post1: "
  \<lbrakk> c_n = (i_Exec_Comp_Stream trans_fun input c)\<^bsup>\<leftarrow> c\<^esup> n; x_n = input n \<rbrakk> \<Longrightarrow>
  (P1 x_n \<and> P2 c_n \<longrightarrow> Q (i_Exec_Comp_Stream trans_fun input c n)) =
  (P1 x_n \<and> P2 c_n \<longrightarrow> Q (trans_fun x_n c_n))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>c_n = (i_Exec_Comp_Stream trans_fun input c)\<^bsup>\<leftarrow> c\<^esup> n; x_n = input n\<rbrakk> \<Longrightarrow> (P1 x_n \<and> P2 c_n \<longrightarrow> Q (i_Exec_Comp_Stream trans_fun input c n)) = (P1 x_n \<and> P2 c_n \<longrightarrow> Q (trans_fun x_n c_n))
[PROOF STEP]
by (simp add: i_Exec_Stream_nth_calc_Previous)


[STATEMENT]
lemma i_Exec_Stream_Pre_Post2: "
  \<lbrakk> c_n = (i_Exec_Comp_Stream trans_fun input c)\<^bsup>\<leftarrow> c\<^esup> n; x_n = input n \<rbrakk> \<Longrightarrow>
  (P c_n \<longrightarrow> Q (input n) (i_Exec_Comp_Stream trans_fun input c n)) =
  (P c_n \<longrightarrow> Q x_n (trans_fun x_n c_n))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>c_n = (i_Exec_Comp_Stream trans_fun input c)\<^bsup>\<leftarrow> c\<^esup> n; x_n = input n\<rbrakk> \<Longrightarrow> (P c_n \<longrightarrow> Q (input n) (i_Exec_Comp_Stream trans_fun input c n)) = (P c_n \<longrightarrow> Q x_n (trans_fun x_n c_n))
[PROOF STEP]
by (simp add: i_Exec_Stream_nth_calc_Previous)


[STATEMENT]
lemma i_Exec_Stream_Pre_Post2_Suc: "
  \<lbrakk> c_n = i_Exec_Comp_Stream trans_fun input c n; x_n1 = input (Suc n) \<rbrakk> \<Longrightarrow>
  (P c_n \<longrightarrow> Q (input (Suc n)) (i_Exec_Comp_Stream trans_fun input c (Suc n))) =
  (P c_n \<longrightarrow> Q x_n1 (trans_fun x_n1 c_n))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>c_n = i_Exec_Comp_Stream trans_fun input c n; x_n1 = input (Suc n)\<rbrakk> \<Longrightarrow> (P c_n \<longrightarrow> Q (input (Suc n)) (i_Exec_Comp_Stream trans_fun input c (Suc n))) = (P c_n \<longrightarrow> Q x_n1 (trans_fun x_n1 c_n))
[PROOF STEP]
by (simp add: i_Exec_Stream_nth_gr0_calc)


[STATEMENT]
lemma i_Exec_Stream_Init_Pre_Post1: "
  \<lbrakk> c_n = i_Exec_Comp_Stream_Init trans_fun input c n; x_n = input n \<rbrakk> \<Longrightarrow>
  (P1 x_n \<and> P2 c_n \<longrightarrow> Q (i_Exec_Comp_Stream_Init trans_fun input c (Suc n))) =
  (P1 x_n \<and> P2 c_n \<longrightarrow> Q (trans_fun x_n c_n))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>c_n = i_Exec_Comp_Stream_Init trans_fun input c n; x_n = input n\<rbrakk> \<Longrightarrow> (P1 x_n \<and> P2 c_n \<longrightarrow> Q (i_Exec_Comp_Stream_Init trans_fun input c (Suc n))) = (P1 x_n \<and> P2 c_n \<longrightarrow> Q (trans_fun x_n c_n))
[PROOF STEP]
by (simp add: i_Exec_Stream_Init_nth_Suc_calc)


[STATEMENT]
lemma i_Exec_Stream_Init_Pre_Post2: "
  \<lbrakk> c_n = i_Exec_Comp_Stream_Init trans_fun input c n; x_n = input n \<rbrakk> \<Longrightarrow>
  (P (input n) (i_Exec_Comp_Stream_Init trans_fun input c n) \<longrightarrow>
     Q (i_Exec_Comp_Stream_Init trans_fun input c (Suc n))) =
  (P x_n c_n \<longrightarrow> Q (trans_fun x_n c_n))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>c_n = i_Exec_Comp_Stream_Init trans_fun input c n; x_n = input n\<rbrakk> \<Longrightarrow> (P (input n) (i_Exec_Comp_Stream_Init trans_fun input c n) \<longrightarrow> Q (i_Exec_Comp_Stream_Init trans_fun input c (Suc n))) = (P x_n c_n \<longrightarrow> Q (trans_fun x_n c_n))
[PROOF STEP]
by (simp add: i_Exec_Stream_Init_nth_Suc_calc)


[STATEMENT]
lemma f_Exec_Stream_prefix: "
  prefix xs ys \<Longrightarrow>
  prefix (f_Exec_Comp_Stream trans_fun xs c)
         (f_Exec_Comp_Stream trans_fun ys c)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prefix xs ys \<Longrightarrow> prefix (f_Exec_Comp_Stream trans_fun xs c) (f_Exec_Comp_Stream trans_fun ys c)
[PROOF STEP]
by (clarsimp simp: prefix_def f_Exec_Stream_append)


[STATEMENT]
lemma i_Exec_Stream_prefix: "
 xs \<sqsubseteq> input \<Longrightarrow>
  f_Exec_Comp_Stream trans_fun xs c \<sqsubseteq>
  i_Exec_Comp_Stream trans_fun input c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. xs \<sqsubseteq> input \<Longrightarrow> f_Exec_Comp_Stream trans_fun xs c \<sqsubseteq> i_Exec_Comp_Stream trans_fun input c
[PROOF STEP]
by (simp add: iprefix_eq_iprefix_take i_Exec_Stream_take)


[STATEMENT]
lemma f_Exec_N_prefix: "
  \<lbrakk> n \<le> length xs; prefix xs ys \<rbrakk> \<Longrightarrow>
  f_Exec_Comp_N trans_fun n xs c =
  f_Exec_Comp_N trans_fun n ys c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n \<le> length xs; prefix xs ys\<rbrakk> \<Longrightarrow> f_Exec_Comp_N trans_fun n xs c = f_Exec_Comp_N trans_fun n ys c
[PROOF STEP]
by (simp add: f_Exec_Comp_N_def prefix_imp_take_eq)


[STATEMENT]
theorem f_Exec_Stream_prefix_causal[rule_format]:"
  n \<le> length (xs \<sqinter> ys) \<Longrightarrow>
  f_Exec_Comp_Stream trans_fun xs c \<down> n =
  f_Exec_Comp_Stream trans_fun ys c \<down> n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n \<le> length (xs \<sqinter> ys) \<Longrightarrow> f_Exec_Comp_Stream trans_fun xs c \<down> n = f_Exec_Comp_Stream trans_fun ys c \<down> n
[PROOF STEP]
by (rule f_Exec_Stream_causal, rule inf_prefix_take_correct)


[STATEMENT]
lemma f_Exec_Stream_Init_prefix:"
  prefix xs ys \<Longrightarrow>
  prefix (f_Exec_Comp_Stream_Init trans_fun xs c)
         (f_Exec_Comp_Stream_Init trans_fun ys c)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prefix xs ys \<Longrightarrow> prefix (f_Exec_Comp_Stream_Init trans_fun xs c) (f_Exec_Comp_Stream_Init trans_fun ys c)
[PROOF STEP]
by (clarsimp simp: prefix_def f_Exec_Stream_Init_append)


[STATEMENT]
lemma i_Exec_Stream_Init_prefix: "
 xs \<sqsubseteq> input \<Longrightarrow>
  f_Exec_Comp_Stream_Init trans_fun xs c \<sqsubseteq>
  i_Exec_Comp_Stream_Init trans_fun input c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. xs \<sqsubseteq> input \<Longrightarrow> f_Exec_Comp_Stream_Init trans_fun xs c \<sqsubseteq> i_Exec_Comp_Stream_Init trans_fun input c
[PROOF STEP]
by (simp add: iprefix_eq_iprefix_take i_Exec_Stream_Init_take)


[STATEMENT]
theorem f_Exec_Stream_Init_prefix_strictly_causal[rule_format]:"
  n \<le> length (xs \<sqinter> ys) \<Longrightarrow>
  f_Exec_Comp_Stream_Init trans_fun xs c \<down> Suc n =
  f_Exec_Comp_Stream_Init trans_fun ys c \<down> Suc n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n \<le> length (xs \<sqinter> ys) \<Longrightarrow> f_Exec_Comp_Stream_Init trans_fun xs c \<down> Suc n = f_Exec_Comp_Stream_Init trans_fun ys c \<down> Suc n
[PROOF STEP]
by (rule f_Exec_Stream_Init_strictly_causal, rule inf_prefix_take_correct)


[STATEMENT]
lemma Deterministic_f_Exec: "
  \<lbrakk> Deterministic_Trans_Fun trans_fun localState; localState c1 = localState c2; xs \<noteq> [] \<rbrakk> \<Longrightarrow>
  f_Exec_Comp trans_fun xs c1 = f_Exec_Comp trans_fun xs c2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Deterministic_Trans_Fun trans_fun localState; localState c1 = localState c2; xs \<noteq> []\<rbrakk> \<Longrightarrow> f_Exec_Comp trans_fun xs c1 = f_Exec_Comp trans_fun xs c2
[PROOF STEP]
apply (unfold Deterministic_Trans_Fun_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>c1 c2 x. localState c1 = localState c2 \<longrightarrow> trans_fun x c1 = trans_fun x c2; localState c1 = localState c2; xs \<noteq> []\<rbrakk> \<Longrightarrow> f_Exec_Comp trans_fun xs c1 = f_Exec_Comp trans_fun xs c2
[PROOF STEP]
apply (case_tac xs, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a list. \<lbrakk>\<forall>c1 c2 x. localState c1 = localState c2 \<longrightarrow> trans_fun x c1 = trans_fun x c2; localState c1 = localState c2; xs \<noteq> []; xs = a # list\<rbrakk> \<Longrightarrow> f_Exec_Comp trans_fun xs c1 = f_Exec_Comp trans_fun xs c2
[PROOF STEP]
apply (rename_tac y ys)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>y ys. \<lbrakk>\<forall>c1 c2 x. localState c1 = localState c2 \<longrightarrow> trans_fun x c1 = trans_fun x c2; localState c1 = localState c2; xs \<noteq> []; xs = y # ys\<rbrakk> \<Longrightarrow> f_Exec_Comp trans_fun xs c1 = f_Exec_Comp trans_fun xs c2
[PROOF STEP]
apply (drule_tac x=c1 in spec)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>y ys. \<lbrakk>localState c1 = localState c2; xs \<noteq> []; xs = y # ys; \<forall>c2 x. localState c1 = localState c2 \<longrightarrow> trans_fun x c1 = trans_fun x c2\<rbrakk> \<Longrightarrow> f_Exec_Comp trans_fun xs c1 = f_Exec_Comp trans_fun xs c2
[PROOF STEP]
apply (drule_tac x=c2 in spec)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>y ys. \<lbrakk>localState c1 = localState c2; xs \<noteq> []; xs = y # ys; \<forall>x. localState c1 = localState c2 \<longrightarrow> trans_fun x c1 = trans_fun x c2\<rbrakk> \<Longrightarrow> f_Exec_Comp trans_fun xs c1 = f_Exec_Comp trans_fun xs c2
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma Deterministic_f_Exec_Stream: "
  \<lbrakk> Deterministic_Trans_Fun trans_fun localState; localState c1 = localState c2 \<rbrakk> \<Longrightarrow>
  f_Exec_Comp_Stream trans_fun xs c1 = f_Exec_Comp_Stream trans_fun xs c2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Deterministic_Trans_Fun trans_fun localState; localState c1 = localState c2\<rbrakk> \<Longrightarrow> f_Exec_Comp_Stream trans_fun xs c1 = f_Exec_Comp_Stream trans_fun xs c2
[PROOF STEP]
apply (clarsimp simp: list_eq_iff f_Exec_Stream_nth)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i. \<lbrakk>Deterministic_Trans_Fun trans_fun localState; localState c1 = localState c2; i < length xs\<rbrakk> \<Longrightarrow> f_Exec_Comp trans_fun (xs \<down> Suc i) c1 = f_Exec_Comp trans_fun (xs \<down> Suc i) c2
[PROOF STEP]
apply (rule Deterministic_f_Exec)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>i. \<lbrakk>Deterministic_Trans_Fun trans_fun localState; localState c1 = localState c2; i < length xs\<rbrakk> \<Longrightarrow> Deterministic_Trans_Fun trans_fun (?localState5 i)
 2. \<And>i. \<lbrakk>Deterministic_Trans_Fun trans_fun localState; localState c1 = localState c2; i < length xs\<rbrakk> \<Longrightarrow> ?localState5 i c1 = ?localState5 i c2
 3. \<And>i. \<lbrakk>Deterministic_Trans_Fun trans_fun localState; localState c1 = localState c2; i < length xs\<rbrakk> \<Longrightarrow> xs \<down> Suc i \<noteq> []
[PROOF STEP]
apply (simp add: length_greater_0_conv[THEN iffD1, OF gr_implies_gr0])+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma Deterministic_i_Exec_Stream: "
  \<lbrakk> Deterministic_Trans_Fun trans_fun localState; localState c1 = localState c2 \<rbrakk> \<Longrightarrow>
  i_Exec_Comp_Stream trans_fun input c1 = i_Exec_Comp_Stream trans_fun input c2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Deterministic_Trans_Fun trans_fun localState; localState c1 = localState c2\<rbrakk> \<Longrightarrow> i_Exec_Comp_Stream trans_fun input c1 = i_Exec_Comp_Stream trans_fun input c2
[PROOF STEP]
apply (clarsimp simp: ilist_eq_iff i_Exec_Stream_nth)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>Deterministic_Trans_Fun trans_fun localState; localState c1 = localState c2\<rbrakk> \<Longrightarrow> f_Exec_Comp trans_fun (input \<Down> Suc x) c1 = f_Exec_Comp trans_fun (input \<Down> Suc x) c2
[PROOF STEP]
apply (rule Deterministic_f_Exec)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>Deterministic_Trans_Fun trans_fun localState; localState c1 = localState c2\<rbrakk> \<Longrightarrow> Deterministic_Trans_Fun trans_fun (?localState1 x)
 2. \<And>x. \<lbrakk>Deterministic_Trans_Fun trans_fun localState; localState c1 = localState c2\<rbrakk> \<Longrightarrow> ?localState1 x c1 = ?localState1 x c2
 3. \<And>x. \<lbrakk>Deterministic_Trans_Fun trans_fun localState; localState c1 = localState c2\<rbrakk> \<Longrightarrow> input \<Down> Suc x \<noteq> []
[PROOF STEP]
apply simp+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma f_Streams_Connected_imp_not_empty: "f_Streams_Connected outS inS \<Longrightarrow> inS \<noteq> []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f_Streams_Connected outS inS \<Longrightarrow> inS \<noteq> []
[PROOF STEP]
by (simp add: f_Streams_Connected_def)


[STATEMENT]
lemma f_Streams_Connected_nth_conv: "
  f_Streams_Connected outS inS =
  (length inS = Suc (length outS) \<and>
  (\<forall>i<length inS. inS ! i = (case i of 0 \<Rightarrow> \<NoMsg> | Suc k \<Rightarrow> outS ! k)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f_Streams_Connected outS inS = (length inS = Suc (length outS) \<and> (\<forall>i<length inS. inS ! i = (case i of 0 \<Rightarrow> NoMsg | Suc k \<Rightarrow> outS ! k)))
[PROOF STEP]
by (simp add: f_Streams_Connected_def list_eq_iff nth_Cons)


[STATEMENT]
lemma f_Streams_Connected_nth_conv_if: "
  f_Streams_Connected outS inS =
  (length inS = Suc (length outS) \<and>
  (\<forall>i<length inS. inS ! i = (if i = 0 then \<NoMsg> else outS ! (i - Suc 0))))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f_Streams_Connected outS inS = (length inS = Suc (length outS) \<and> (\<forall>i<length inS. inS ! i = (if i = 0 then NoMsg else outS ! (i - Suc 0))))
[PROOF STEP]
apply (subst f_Streams_Connected_nth_conv)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (length inS = Suc (length outS) \<and> (\<forall>i<length inS. inS ! i = (case i of 0 \<Rightarrow> NoMsg | Suc x \<Rightarrow> outS ! x))) = (length inS = Suc (length outS) \<and> (\<forall>i<length inS. inS ! i = (if i = 0 then NoMsg else outS ! (i - Suc 0))))
[PROOF STEP]
apply (rule conj_cong, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length inS = Suc (length outS) \<Longrightarrow> (\<forall>i<length inS. inS ! i = (case i of 0 \<Rightarrow> NoMsg | Suc x \<Rightarrow> outS ! x)) = (\<forall>i<length inS. inS ! i = (if i = 0 then NoMsg else outS ! (i - Suc 0)))
[PROOF STEP]
apply (rule all_imp_eqI, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i. \<lbrakk>length inS = Suc (length outS); i < length inS\<rbrakk> \<Longrightarrow> (inS ! i = (case i of 0 \<Rightarrow> NoMsg | Suc x \<Rightarrow> outS ! x)) = (inS ! i = (if i = 0 then NoMsg else outS ! (i - Suc 0)))
[PROOF STEP]
apply (rename_tac i, case_tac i, simp+)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma i_Streams_Connected_nth_conv: "
  i_Streams_Connected outS inS =
  (\<forall>i. inS i = (case i of 0 \<Rightarrow> \<NoMsg> | Suc k \<Rightarrow> outS k))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i_Streams_Connected outS inS = (\<forall>i. inS i = (case i of 0 \<Rightarrow> NoMsg | Suc k \<Rightarrow> outS k))
[PROOF STEP]
by (simp add: i_Streams_Connected_def ilist_eq_iff i_append_nth_Cons)


[STATEMENT]
lemma i_Streams_Connected_nth_conv_if: "
  i_Streams_Connected outS inS =
  (\<forall>i. inS i = (if i = 0 then \<NoMsg> else outS (i - Suc 0)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i_Streams_Connected outS inS = (\<forall>i. inS i = (if i = 0 then NoMsg else outS (i - Suc 0)))
[PROOF STEP]
apply (subst i_Streams_Connected_nth_conv)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>i. inS i = (case i of 0 \<Rightarrow> NoMsg | Suc x \<Rightarrow> outS x)) = (\<forall>i. inS i = (if i = 0 then NoMsg else outS (i - Suc 0)))
[PROOF STEP]
apply (rule all_eqI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i. (inS i = (case i of 0 \<Rightarrow> NoMsg | Suc x \<Rightarrow> outS x)) = (inS i = (if i = 0 then NoMsg else outS (i - Suc 0)))
[PROOF STEP]
apply (rename_tac i, case_tac i, simp+)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma f_Exec_Stream_Init_eq_output_channel: "
  \<lbrakk> output_fun c = \<NoMsg>;
    f_Streams_Connected
      (map output_fun (f_Exec_Comp_Stream trans_fun xs c))
      channel \<rbrakk> \<Longrightarrow>
  map output_fun (f_Exec_Comp_Stream_Init trans_fun xs c) = channel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>output_fun c = NoMsg; f_Streams_Connected (map output_fun (f_Exec_Comp_Stream trans_fun xs c)) channel\<rbrakk> \<Longrightarrow> map output_fun (f_Exec_Comp_Stream_Init trans_fun xs c) = channel
[PROOF STEP]
by (simp add: f_Streams_Connected_def f_Exec_Stream_Init_eq_f_Exec_Stream_Cons)


[STATEMENT]
lemma i_Exec_Stream_Init_eq_output_channel: "
  \<lbrakk> output_fun c = \<NoMsg>;
    i_Streams_Connected
      (output_fun \<circ> (i_Exec_Comp_Stream trans_fun input c))
      channel \<rbrakk> \<Longrightarrow>
  output_fun \<circ> (i_Exec_Comp_Stream_Init trans_fun input c) = channel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>output_fun c = NoMsg; i_Streams_Connected (output_fun \<circ> i_Exec_Comp_Stream trans_fun input c) channel\<rbrakk> \<Longrightarrow> output_fun \<circ> i_Exec_Comp_Stream_Init trans_fun input c = channel
[PROOF STEP]
by (simp add: i_Streams_Connected_def i_Exec_Stream_Init_eq_i_Exec_Stream_Cons)


[STATEMENT]
lemma f_Exec_Stream_output_causal: "
  \<lbrakk> xs \<down> n = ys \<down> n;
    output1 = map output_fun (f_Exec_Comp_Stream trans_fun xs c);
    output2 = map output_fun (f_Exec_Comp_Stream trans_fun ys c) \<rbrakk> \<Longrightarrow>
  output1 \<down> n = output2 \<down> n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>xs \<down> n = ys \<down> n; output1 = map output_fun (f_Exec_Comp_Stream trans_fun xs c); output2 = map output_fun (f_Exec_Comp_Stream trans_fun ys c)\<rbrakk> \<Longrightarrow> output1 \<down> n = output2 \<down> n
[PROOF STEP]
by (simp add: take_map f_Exec_Stream_causal[of n xs])


[STATEMENT]
lemma f_Exec_Stream_Init_output_strictly_causal: "
  \<lbrakk> xs \<down> n = ys \<down> n;
    output1 = map output_fun (f_Exec_Comp_Stream_Init trans_fun xs c);
    output2 = map output_fun (f_Exec_Comp_Stream_Init trans_fun ys c) \<rbrakk> \<Longrightarrow>
  output1 \<down> Suc n = output2 \<down> Suc n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>xs \<down> n = ys \<down> n; output1 = map output_fun (f_Exec_Comp_Stream_Init trans_fun xs c); output2 = map output_fun (f_Exec_Comp_Stream_Init trans_fun ys c)\<rbrakk> \<Longrightarrow> output1 \<down> Suc n = output2 \<down> Suc n
[PROOF STEP]
by (simp add: take_map f_Exec_Stream_Init_strictly_causal[of n xs])


[STATEMENT]
lemma i_Exec_Stream_output_causal: "
  \<lbrakk> input1 \<Down> n = input2 \<Down> n;
    output1 = output_fun \<circ> i_Exec_Comp_Stream trans_fun input1 c;
    output2 = output_fun \<circ> i_Exec_Comp_Stream trans_fun input2 c \<rbrakk> \<Longrightarrow>
  output1 \<Down> n = output2 \<Down> n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>input1 \<Down> n = input2 \<Down> n; output1 = output_fun \<circ> i_Exec_Comp_Stream trans_fun input1 c; output2 = output_fun \<circ> i_Exec_Comp_Stream trans_fun input2 c\<rbrakk> \<Longrightarrow> output1 \<Down> n = output2 \<Down> n
[PROOF STEP]
by (simp add: i_Exec_Stream_causal[of n input1])


[STATEMENT]
lemma i_Exec_Stream_Init_output_strictly_causal: "
  \<lbrakk> input1 \<Down> n = input2 \<Down> n;
    output1 = output_fun \<circ> i_Exec_Comp_Stream_Init trans_fun input1 c;
    output2 = output_fun \<circ> i_Exec_Comp_Stream_Init trans_fun input2 c \<rbrakk> \<Longrightarrow>
  output1 \<Down> Suc n = output2 \<Down> Suc n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>input1 \<Down> n = input2 \<Down> n; output1 = output_fun \<circ> i_Exec_Comp_Stream_Init trans_fun input1 c; output2 = output_fun \<circ> i_Exec_Comp_Stream_Init trans_fun input2 c\<rbrakk> \<Longrightarrow> output1 \<Down> Suc n = output2 \<Down> Suc n
[PROOF STEP]
by (simp add: i_Exec_Stream_Init_strictly_causal[of n input1])


[STATEMENT]
lemma f_Exec_Stream_Connected_strictly_causal: "
  \<lbrakk> xs \<down> n = ys \<down> n;
    f_Streams_Connected
      (map output_fun (f_Exec_Comp_Stream trans_fun xs c))
      channel1;
    f_Streams_Connected
      (map output_fun (f_Exec_Comp_Stream trans_fun ys c))
      channel2 \<rbrakk> \<Longrightarrow>
  channel1 \<down> Suc n = channel2 \<down> Suc n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>xs \<down> n = ys \<down> n; f_Streams_Connected (map output_fun (f_Exec_Comp_Stream trans_fun xs c)) channel1; f_Streams_Connected (map output_fun (f_Exec_Comp_Stream trans_fun ys c)) channel2\<rbrakk> \<Longrightarrow> channel1 \<down> Suc n = channel2 \<down> Suc n
[PROOF STEP]
by (simp add: f_Streams_Connected_def take_map f_Exec_Stream_take)


[STATEMENT]
lemma i_Exec_Stream_Connected_strictly_causal: "
  \<lbrakk> input1 \<Down> n = input2 \<Down> n;
    i_Streams_Connected
      (portOutput \<circ> (i_Exec_Comp_Stream trans_fun input1 c))
      channel1;
    i_Streams_Connected
      (portOutput \<circ> (i_Exec_Comp_Stream trans_fun input2 c))
      channel2 \<rbrakk> \<Longrightarrow>
  channel1 \<Down> Suc n = channel2 \<Down> Suc n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>input1 \<Down> n = input2 \<Down> n; i_Streams_Connected (portOutput \<circ> i_Exec_Comp_Stream trans_fun input1 c) channel1; i_Streams_Connected (portOutput \<circ> i_Exec_Comp_Stream trans_fun input2 c) channel2\<rbrakk> \<Longrightarrow> channel1 \<Down> Suc n = channel2 \<Down> Suc n
[PROOF STEP]
by (simp add: i_Streams_Connected_def i_take_Suc_Cons i_Exec_Stream_take)


[STATEMENT]
lemma f_Streams_Connected_Init_nth_conv: "
  f_Streams_Connected_Init outS inS =
  (length inS = length outS \<and> (\<forall>i<length inS. inS ! i = outS ! i))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f_Streams_Connected_Init outS inS = (length inS = length outS \<and> (\<forall>i<length inS. inS ! i = outS ! i))
[PROOF STEP]
by (simp add: f_Streams_Connected_Init_def list_eq_iff)


[STATEMENT]
lemma i_Streams_Connected_Init_nth_conv: "
  i_Streams_Connected_Init outS inS =
  (\<forall>i. inS i = outS i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i_Streams_Connected_Init outS inS = (\<forall>i. inS i = outS i)
[PROOF STEP]
by (simp add: i_Streams_Connected_Init_def ilist_eq_iff)


[STATEMENT]
lemma f_Exec_Stream_Init_eq_output_channel2: "
  \<lbrakk> output_fun c = \<NoMsg>;
    f_Streams_Connected_Init
      (map output_fun (f_Exec_Comp_Stream_Init trans_fun xs c))
      channel \<rbrakk> \<Longrightarrow>
  map output_fun (f_Exec_Comp_Stream_Init trans_fun xs c) = channel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>output_fun c = NoMsg; f_Streams_Connected_Init (map output_fun (f_Exec_Comp_Stream_Init trans_fun xs c)) channel\<rbrakk> \<Longrightarrow> map output_fun (f_Exec_Comp_Stream_Init trans_fun xs c) = channel
[PROOF STEP]
by (simp add: f_Streams_Connected_Init_def f_Exec_Stream_Init_eq_f_Exec_Stream_Cons)


[STATEMENT]
lemma i_Exec_Stream_Init_eq_output_channel2: "
  \<lbrakk> output_fun c = \<NoMsg>;
    i_Streams_Connected_Init
      (output_fun \<circ> (i_Exec_Comp_Stream_Init trans_fun input c))
      channel \<rbrakk> \<Longrightarrow>
  output_fun \<circ> (i_Exec_Comp_Stream_Init trans_fun input c) = channel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>output_fun c = NoMsg; i_Streams_Connected_Init (output_fun \<circ> i_Exec_Comp_Stream_Init trans_fun input c) channel\<rbrakk> \<Longrightarrow> output_fun \<circ> i_Exec_Comp_Stream_Init trans_fun input c = channel
[PROOF STEP]
by (simp add: i_Streams_Connected_Init_def i_Exec_Stream_Init_eq_i_Exec_Stream_Cons)


[STATEMENT]
lemma f_Exec_Stream_Connected_Init_strictly_causal: "
  \<lbrakk> xs \<down> n = ys \<down> n;
    f_Streams_Connected_Init
      (map output_fun (f_Exec_Comp_Stream_Init trans_fun xs c))
      channel1;
    f_Streams_Connected_Init
      (map output_fun (f_Exec_Comp_Stream_Init trans_fun ys c))
      channel2 \<rbrakk> \<Longrightarrow>
  channel1 \<down> Suc n = channel2 \<down> Suc n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>xs \<down> n = ys \<down> n; f_Streams_Connected_Init (map output_fun (f_Exec_Comp_Stream_Init trans_fun xs c)) channel1; f_Streams_Connected_Init (map output_fun (f_Exec_Comp_Stream_Init trans_fun ys c)) channel2\<rbrakk> \<Longrightarrow> channel1 \<down> Suc n = channel2 \<down> Suc n
[PROOF STEP]
by (simp add: f_Streams_Connected_Init_def f_Exec_Stream_Init_eq_f_Exec_Stream_Cons take_map f_Exec_Stream_take)


[STATEMENT]
lemma i_Exec_Stream_Connected_Init_strictly_causal: "
  \<lbrakk> input1 \<Down> n = input2 \<Down> n;
    i_Streams_Connected_Init
      (portOutput \<circ> (i_Exec_Comp_Stream_Init trans_fun input1 c))
      channel1;
    i_Streams_Connected_Init
      (portOutput \<circ> (i_Exec_Comp_Stream_Init trans_fun input2 c))
      channel2 \<rbrakk> \<Longrightarrow>
  channel1 \<Down> Suc n = channel2 \<Down> Suc n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>input1 \<Down> n = input2 \<Down> n; i_Streams_Connected_Init (portOutput \<circ> i_Exec_Comp_Stream_Init trans_fun input1 c) channel1; i_Streams_Connected_Init (portOutput \<circ> i_Exec_Comp_Stream_Init trans_fun input2 c) channel2\<rbrakk> \<Longrightarrow> channel1 \<Down> Suc n = channel2 \<Down> Suc n
[PROOF STEP]
by (simp add: i_Streams_Connected_Init_def i_Exec_Stream_Init_eq_i_Exec_Stream_Cons i_Exec_Stream_take)


[STATEMENT]
lemma f_State_Change_exists_set: "
  \<lbrakk> n1 \<le> n2; n1 \<in> I; n2 \<in> I;
    \<not> P (f_Exec_Comp trans_fun (input \<down> n1) c);
    P (f_Exec_Comp trans_fun (input \<down> n2) c) \<rbrakk> \<Longrightarrow>
  \<exists>n\<in>I. n1 \<le> n \<and> n < n2 \<and>
    \<not> P (f_Exec_Comp trans_fun (input \<down> n) c) \<and>
    P (f_Exec_Comp trans_fun (input \<down> (inext n I)) c)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n1 \<le> n2; n1 \<in> I; n2 \<in> I; \<not> P (f_Exec_Comp trans_fun (input \<down> n1) c); P (f_Exec_Comp trans_fun (input \<down> n2) c)\<rbrakk> \<Longrightarrow> \<exists>n\<in>I. n1 \<le> n \<and> n < n2 \<and> \<not> P (f_Exec_Comp trans_fun (input \<down> n) c) \<and> P (f_Exec_Comp trans_fun (input \<down> inext n I) c)
[PROOF STEP]
by (rule inext_predicate_change_exists)


[STATEMENT]
lemma f_State_Change_exists: "
  \<lbrakk> n1 \<le> n2;
    \<not> P (f_Exec_Comp trans_fun (input \<down> n1) c);
    P (f_Exec_Comp trans_fun (input \<down> n2) c) \<rbrakk> \<Longrightarrow>
  \<exists>n\<ge>n1. n < n2 \<and>
    \<not> P (f_Exec_Comp trans_fun (input \<down> n) c) \<and>
    P (f_Exec_Comp trans_fun (input \<down> (Suc n)) c)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n1 \<le> n2; \<not> P (f_Exec_Comp trans_fun (input \<down> n1) c); P (f_Exec_Comp trans_fun (input \<down> n2) c)\<rbrakk> \<Longrightarrow> \<exists>n\<ge>n1. n < n2 \<and> \<not> P (f_Exec_Comp trans_fun (input \<down> n) c) \<and> P (f_Exec_Comp trans_fun (input \<down> Suc n) c)
[PROOF STEP]
by (rule nat_Suc_predicate_change_exists)


[STATEMENT]
lemma i_State_Change_exists_set: "
  \<lbrakk> n1 \<le> n2; n1 \<in> I; n2 \<in> I;
    \<not> P (i_Exec_Comp_Stream trans_fun input c n1);
    P (i_Exec_Comp_Stream trans_fun input c n2) \<rbrakk> \<Longrightarrow>
  \<exists>n\<in>I. n1 \<le> n \<and> n < n2 \<and>
    \<not> P (i_Exec_Comp_Stream trans_fun input c n) \<and>
    P (i_Exec_Comp_Stream trans_fun input c (inext n I))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n1 \<le> n2; n1 \<in> I; n2 \<in> I; \<not> P (i_Exec_Comp_Stream trans_fun input c n1); P (i_Exec_Comp_Stream trans_fun input c n2)\<rbrakk> \<Longrightarrow> \<exists>n\<in>I. n1 \<le> n \<and> n < n2 \<and> \<not> P (i_Exec_Comp_Stream trans_fun input c n) \<and> P (i_Exec_Comp_Stream trans_fun input c (inext n I))
[PROOF STEP]
by (rule inext_predicate_change_exists)


[STATEMENT]
lemma i_State_Change_exists: "
  \<lbrakk> n1 \<le> n2;
    \<not> P (i_Exec_Comp_Stream trans_fun input c n1);
    P (i_Exec_Comp_Stream trans_fun input c n2) \<rbrakk> \<Longrightarrow>
  \<exists>n\<ge>n1. n < n2 \<and>
    \<not> P (i_Exec_Comp_Stream trans_fun input c n) \<and>
    P (i_Exec_Comp_Stream trans_fun input c (Suc n))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n1 \<le> n2; \<not> P (i_Exec_Comp_Stream trans_fun input c n1); P (i_Exec_Comp_Stream trans_fun input c n2)\<rbrakk> \<Longrightarrow> \<exists>n\<ge>n1. n < n2 \<and> \<not> P (i_Exec_Comp_Stream trans_fun input c n) \<and> P (i_Exec_Comp_Stream trans_fun input c (Suc n))
[PROOF STEP]
by (rule nat_Suc_predicate_change_exists)


[STATEMENT]
lemma i_State_Change_Init_exists_set: "
  \<lbrakk> n1 \<le> n2; n1 \<in> I; n2 \<in> I;
    \<not> P (i_Exec_Comp_Stream_Init trans_fun input c n1);
    P (i_Exec_Comp_Stream_Init trans_fun input c n2) \<rbrakk> \<Longrightarrow>
  \<exists>n\<in>I. n1 \<le> n \<and> n < n2 \<and>
    \<not> P (i_Exec_Comp_Stream_Init trans_fun input c n) \<and>
    P (i_Exec_Comp_Stream_Init trans_fun input c (inext n I))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n1 \<le> n2; n1 \<in> I; n2 \<in> I; \<not> P (i_Exec_Comp_Stream_Init trans_fun input c n1); P (i_Exec_Comp_Stream_Init trans_fun input c n2)\<rbrakk> \<Longrightarrow> \<exists>n\<in>I. n1 \<le> n \<and> n < n2 \<and> \<not> P (i_Exec_Comp_Stream_Init trans_fun input c n) \<and> P (i_Exec_Comp_Stream_Init trans_fun input c (inext n I))
[PROOF STEP]
by (rule inext_predicate_change_exists)


[STATEMENT]
lemma i_State_Change_Init_exists: "
  \<lbrakk> n1 \<le> n2;
    \<not> P (i_Exec_Comp_Stream_Init trans_fun input c n1);
    P (i_Exec_Comp_Stream_Init trans_fun input c n2) \<rbrakk> \<Longrightarrow>
  \<exists>n\<ge>n1. n < n2 \<and>
    \<not> P (i_Exec_Comp_Stream_Init trans_fun input c n) \<and>
    P (i_Exec_Comp_Stream_Init trans_fun input c (Suc n))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n1 \<le> n2; \<not> P (i_Exec_Comp_Stream_Init trans_fun input c n1); P (i_Exec_Comp_Stream_Init trans_fun input c n2)\<rbrakk> \<Longrightarrow> \<exists>n\<ge>n1. n < n2 \<and> \<not> P (i_Exec_Comp_Stream_Init trans_fun input c n) \<and> P (i_Exec_Comp_Stream_Init trans_fun input c (Suc n))
[PROOF STEP]
by (rule nat_Suc_predicate_change_exists)


[STATEMENT]
lemma Equiv_Exec_equiv_statesI: "
  \<lbrakk> equiv_states (localState1 c1) (localState2 c2);
    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 (input_fun1 m # \<NoMsg>\<^bsup>k1 - Suc 0\<^esup>) c1))
    (localState2 (f_Exec_Comp trans_fun2 (input_fun2 m # \<NoMsg>\<^bsup>k2 - Suc 0\<^esup>) c2))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>equiv_states (localState1 c1) (localState2 c2); 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 (input_fun1 m # NoMsg\<^bsup>k1 - Suc 0\<^esup>) c1)) (localState2 (f_Exec_Comp trans_fun2 (input_fun2 m # NoMsg\<^bsup>k2 - Suc 0\<^esup>) c2))
[PROOF STEP]
by (simp add: Equiv_Exec_def)


[STATEMENT]
lemma Equiv_Exec_output_eqI: "
  \<lbrakk> equiv_states (localState1 c1) (localState2 c2);
    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>
  last_message (map output_fun1 (
    f_Exec_Comp_Stream trans_fun1 (input_fun1 m # \<NoMsg>\<^bsup>k1 - Suc 0\<^esup>) c1)) =
  last_message (map output_fun2 (
    f_Exec_Comp_Stream trans_fun2 (input_fun2 m # \<NoMsg>\<^bsup>k2 - Suc 0\<^esup>) c2))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>equiv_states (localState1 c1) (localState2 c2); 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> last_message (map output_fun1 (f_Exec_Comp_Stream trans_fun1 (input_fun1 m # NoMsg\<^bsup>k1 - Suc 0\<^esup>) c1)) = last_message (map output_fun2 (f_Exec_Comp_Stream trans_fun2 (input_fun2 m # NoMsg\<^bsup>k2 - Suc 0\<^esup>) c2))
[PROOF STEP]
by (simp add: Equiv_Exec_def)


[STATEMENT]
lemma Equiv_Exec_equiv_statesI': "
  \<lbrakk> equiv_states (localState1 c1) (localState2 c2);
    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 m) c1)))
   (localState2 (f_Exec_Comp trans_fun2 NoMsg\<^bsup>k2 - Suc 0\<^esup> (trans_fun2 (input_fun2 m) c2)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>equiv_states (localState1 c1) (localState2 c2); 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 m) c1))) (localState2 (f_Exec_Comp trans_fun2 NoMsg\<^bsup>k2 - Suc 0\<^esup> (trans_fun2 (input_fun2 m) c2)))
[PROOF STEP]
by (simp add: Equiv_Exec_def)


[STATEMENT]
lemma Equiv_Exec_le1: "
  \<lbrakk> k1 \<le> Suc 0; k2 \<le> Suc 0;
    equiv_states (localState1 c1) (localState2 c2);
    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>
  output_fun1 (trans_fun1 (input_fun1 m) c1) =
  output_fun2 (trans_fun2 (input_fun2 m) c2) \<and>
  equiv_states
    (localState1 (trans_fun1 (input_fun1 m) c1))
    (localState2 (trans_fun2 (input_fun2 m) c2))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>k1 \<le> Suc 0; k2 \<le> Suc 0; equiv_states (localState1 c1) (localState2 c2); 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> output_fun1 (trans_fun1 (input_fun1 m) c1) = output_fun2 (trans_fun2 (input_fun2 m) c2) \<and> equiv_states (localState1 (trans_fun1 (input_fun1 m) c1)) (localState2 (trans_fun2 (input_fun2 m) c2))
[PROOF STEP]
by (simp add: Equiv_Exec_def)


[STATEMENT]
lemma Equiv_Exec_stable_set_UNIV: "
  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 =
  Equiv_Exec_stable
    equiv_states
    localState1 localState2 input_fun1 input_fun2 output_fun1 output_fun2
    trans_fun1 trans_fun2 k1 k2 c1 c2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 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 = Equiv_Exec_stable equiv_states localState1 localState2 input_fun1 input_fun2 output_fun1 output_fun2 trans_fun1 trans_fun2 k1 k2 c1 c2
[PROOF STEP]
by (simp add: Equiv_Exec_stable_set_def Equiv_Exec_stable_def)


[STATEMENT]
lemma Equiv_Exec_stable_setI: "
  \<lbrakk> 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; 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 input \<odot>\<^sub>f k1) c1)
        (f_Exec_Comp trans_fun2 (map input_fun2 input \<odot>\<^sub>f k2) c2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>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; 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 input \<odot> k1) c1) (f_Exec_Comp trans_fun2 (map input_fun2 input \<odot> k2) c2)
[PROOF STEP]
by (simp add: Equiv_Exec_stable_set_def)


[STATEMENT]
lemma Equiv_Exec_stableI: "
  Equiv_Exec_stable
    equiv_states localState1 localState2 input_fun1 input_fun2 output_fun1 output_fun2
    trans_fun1 trans_fun2 k1 k2 c1 c2 \<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>\<^sub>f k1) c1)
    (f_Exec_Comp trans_fun2 (map input_fun2 input \<odot>\<^sub>f k2) c2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Equiv_Exec_stable equiv_states localState1 localState2 input_fun1 input_fun2 output_fun1 output_fun2 trans_fun1 trans_fun2 k1 k2 c1 c2 \<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)
[PROOF STEP]
by (simp add: Equiv_Exec_stable_def)


[STATEMENT]
lemma Equiv_Exec_refl: "
  \<lbrakk> \<And>c. equiv_states (localState c) (localState c) \<rbrakk> \<Longrightarrow>
  Equiv_Exec
    m equiv_states
    localState localState input_fun input_fun output_fun output_fun
    trans_fun trans_fun k k c c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>c. equiv_states (localState c) (localState c)) \<Longrightarrow> Equiv_Exec m equiv_states localState localState input_fun input_fun output_fun output_fun trans_fun trans_fun k k c c
[PROOF STEP]
by (simp add: Equiv_Exec_def)


[STATEMENT]
lemma Equiv_Exec_sym[rule_format]: "
  \<lbrakk> \<forall>c1 c2.
      equiv_states (localState1 c1) (localState2 c2) =
      equiv_states (localState2 c2) (localState1 c1) \<rbrakk> \<Longrightarrow>
  Equiv_Exec
    m equiv_states
    localState1 localState2 input_fun1 input_fun2 output_fun1 output_fun2
    trans_fun1 trans_fun2 k1 k2 c1 c2 =
  Equiv_Exec
    m equiv_states
    localState2 localState1 input_fun2 input_fun1 output_fun2 output_fun1
    trans_fun2 trans_fun1 k2 k1 c2 c1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>c1 c2. equiv_states (localState1 c1) (localState2 c2) = equiv_states (localState2 c2) (localState1 c1) \<Longrightarrow> Equiv_Exec m equiv_states localState1 localState2 input_fun1 input_fun2 output_fun1 output_fun2 trans_fun1 trans_fun2 k1 k2 c1 c2 = Equiv_Exec m equiv_states localState2 localState1 input_fun2 input_fun1 output_fun2 output_fun1 trans_fun2 trans_fun1 k2 k1 c2 c1
[PROOF STEP]
by (fastforce simp: Equiv_Exec_def)


[STATEMENT]
lemma Equiv_Exec_sym2: "
  \<lbrakk> equiv_states_sym = (\<lambda>s1 s2. equiv_states s2 s1) \<rbrakk> \<Longrightarrow>
  Equiv_Exec
    m equiv_states
    localState1 localState2 input_fun1 input_fun2 output_fun1 output_fun2
    trans_fun1 trans_fun2 k1 k2 c1 c2 =
  Equiv_Exec
    m equiv_states_sym
    localState2 localState1 input_fun2 input_fun1 output_fun2 output_fun1
    trans_fun2 trans_fun1 k2 k1 c2 c1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. equiv_states_sym = (\<lambda>s1 s2. equiv_states s2 s1) \<Longrightarrow> Equiv_Exec m equiv_states localState1 localState2 input_fun1 input_fun2 output_fun1 output_fun2 trans_fun1 trans_fun2 k1 k2 c1 c2 = Equiv_Exec m equiv_states_sym localState2 localState1 input_fun2 input_fun1 output_fun2 output_fun1 trans_fun2 trans_fun1 k2 k1 c2 c1
[PROOF STEP]
by (fastforce simp: Equiv_Exec_def)


[STATEMENT]
lemma Equiv_Exec_sym2_ex: "
  \<exists>equiv_states_sym.
    Equiv_Exec
      m equiv_states
      localState1 localState2 input_fun1 input_fun2 output_fun1 output_fun2
      trans_fun1 trans_fun2 k1 k2 c1 c2 =
    Equiv_Exec
      m equiv_states_sym
      localState2 localState1 input_fun2 input_fun1 output_fun2 output_fun1
      trans_fun2 trans_fun1 k2 k1 c2 c1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>equiv_states_sym. Equiv_Exec m equiv_states localState1 localState2 input_fun1 input_fun2 output_fun1 output_fun2 trans_fun1 trans_fun2 k1 k2 c1 c2 = Equiv_Exec m equiv_states_sym localState2 localState1 input_fun2 input_fun1 output_fun2 output_fun1 trans_fun2 trans_fun1 k2 k1 c2 c1
[PROOF STEP]
by (rule exI, rule Equiv_Exec_sym2, simp)


[STATEMENT]
lemma Equiv_Exec_trans: "
  \<lbrakk> Equiv_Exec
      m equiv_states12
      localState1 localState2 input_fun1 input_fun2 output_fun1 output_fun2
      trans_fun1 trans_fun2 k1 k2 c1 c2;
    Equiv_Exec
      m equiv_states23
      localState2 localState3 input_fun2 input_fun3 output_fun2 output_fun3
      trans_fun2 trans_fun3 k2 k3 c2 c3;
    equiv_states13 = (\<lambda>s1 s3. (
      if s1 = localState1 c1 \<and> s3 = localState3 c3 then
        equiv_states12 s1 (localState2 c2) \<and>
        equiv_states23 (localState2 c2) s3
      else
        equiv_states12 s1 (
          localState2 (f_Exec_Comp trans_fun2 (input_fun2 m # \<NoMsg>\<^bsup>k2 - Suc 0\<^esup>) c2))) \<and>
        equiv_states23 (
          localState2 (f_Exec_Comp trans_fun2 (input_fun2 m # \<NoMsg>\<^bsup>k2 - Suc 0\<^esup>) c2)) s3) \<rbrakk> \<Longrightarrow>
    Equiv_Exec
      m equiv_states13
      localState1 localState3 input_fun1 input_fun3 output_fun1 output_fun3
      trans_fun1 trans_fun3 k1 k3 c1 c3"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Equiv_Exec m equiv_states12 localState1 localState2 input_fun1 input_fun2 output_fun1 output_fun2 trans_fun1 trans_fun2 k1 k2 c1 c2; Equiv_Exec m equiv_states23 localState2 localState3 input_fun2 input_fun3 output_fun2 output_fun3 trans_fun2 trans_fun3 k2 k3 c2 c3; equiv_states13 = (\<lambda>s1 s3. (if s1 = localState1 c1 \<and> s3 = localState3 c3 then equiv_states12 s1 (localState2 c2) \<and> equiv_states23 (localState2 c2) s3 else equiv_states12 s1 (localState2 (f_Exec_Comp trans_fun2 (input_fun2 m # NoMsg\<^bsup>k2 - Suc 0\<^esup>) c2))) \<and> equiv_states23 (localState2 (f_Exec_Comp trans_fun2 (input_fun2 m # NoMsg\<^bsup>k2 - Suc 0\<^esup>) c2)) s3)\<rbrakk> \<Longrightarrow> Equiv_Exec m equiv_states13 localState1 localState3 input_fun1 input_fun3 output_fun1 output_fun3 trans_fun1 trans_fun3 k1 k3 c1 c3
[PROOF STEP]
by (fastforce simp: Equiv_Exec_def)


[STATEMENT]
lemma Equiv_Exec_trans_ex: "
  \<lbrakk> Equiv_Exec
      m equiv_states12
      localState1 localState2 input_fun1 input_fun2 output_fun1 output_fun2
      trans_fun1 trans_fun2 k1 k2 c1 c2;
    Equiv_Exec
      m equiv_states23
      localState2 localState3 input_fun2 input_fun3 output_fun2 output_fun3
      trans_fun2 trans_fun3 k2 k3 c2 c3 \<rbrakk> \<Longrightarrow>
    \<exists>equiv_states13. Equiv_Exec
      m equiv_states13
      localState1 localState3 input_fun1 input_fun3 output_fun1 output_fun3
      trans_fun1 trans_fun3 k1 k3 c1 c3"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Equiv_Exec m equiv_states12 localState1 localState2 input_fun1 input_fun2 output_fun1 output_fun2 trans_fun1 trans_fun2 k1 k2 c1 c2; Equiv_Exec m equiv_states23 localState2 localState3 input_fun2 input_fun3 output_fun2 output_fun3 trans_fun2 trans_fun3 k2 k3 c2 c3\<rbrakk> \<Longrightarrow> \<exists>equiv_states13. Equiv_Exec m equiv_states13 localState1 localState3 input_fun1 input_fun3 output_fun1 output_fun3 trans_fun1 trans_fun3 k1 k3 c1 c3
[PROOF STEP]
by (blast intro: Equiv_Exec_trans)


[STATEMENT]
lemma Exec_Equal_StateD: "
  \<lbrakk> Exec_Equal_State localState trans_fun;
    localState c1 = localState c2 \<rbrakk> \<Longrightarrow>
  trans_fun m c1 = trans_fun m c2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Exec_Equal_State localState trans_fun; localState c1 = localState c2\<rbrakk> \<Longrightarrow> trans_fun m c1 = trans_fun m c2
[PROOF STEP]
by (unfold Exec_Equal_State_def, blast)


[STATEMENT]
lemma Exec_Equal_StateD': "
  Exec_Equal_State localState trans_fun \<Longrightarrow>
  \<forall>c1 c2 m. localState c1 = localState c2 \<longrightarrow> trans_fun m c1 = trans_fun m c2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Exec_Equal_State localState trans_fun \<Longrightarrow> \<forall>c1 c2 m. localState c1 = localState c2 \<longrightarrow> trans_fun m c1 = trans_fun m c2
[PROOF STEP]
by (unfold Exec_Equal_State_def, blast)


[STATEMENT]
lemma Exec_Equal_StateI: "
  (\<And>c1 c2 m. localState c1 = localState c2 \<Longrightarrow> trans_fun m c1 = trans_fun m c2)
  \<Longrightarrow> Exec_Equal_State localState trans_fun"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>c1 c2 m. localState c1 = localState c2 \<Longrightarrow> trans_fun m c1 = trans_fun m c2) \<Longrightarrow> Exec_Equal_State localState trans_fun
[PROOF STEP]
by (unfold Exec_Equal_State_def, blast)


[STATEMENT]
lemma f_Exec_Equal_State: "\<And>c1 c2.
  \<lbrakk> Exec_Equal_State localState trans_fun;
    localState c1 = localState c2; xs \<noteq> [] \<rbrakk> \<Longrightarrow>
  f_Exec_Comp trans_fun xs c1 = f_Exec_Comp trans_fun xs c2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>c1 c2. \<lbrakk>Exec_Equal_State localState trans_fun; localState c1 = localState c2; xs \<noteq> []\<rbrakk> \<Longrightarrow> f_Exec_Comp trans_fun xs c1 = f_Exec_Comp trans_fun xs c2
[PROOF STEP]
apply (induct xs, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a xs c1 c2. \<lbrakk>\<And>c1 c2. \<lbrakk>Exec_Equal_State localState trans_fun; localState c1 = localState c2; xs \<noteq> []\<rbrakk> \<Longrightarrow> f_Exec_Comp trans_fun xs c1 = f_Exec_Comp trans_fun xs c2; Exec_Equal_State localState trans_fun; localState c1 = localState c2; a # xs \<noteq> []\<rbrakk> \<Longrightarrow> f_Exec_Comp trans_fun (a # xs) c1 = f_Exec_Comp trans_fun (a # xs) c2
[PROOF STEP]
apply (case_tac "xs = []")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a xs c1 c2. \<lbrakk>\<And>c1 c2. \<lbrakk>Exec_Equal_State localState trans_fun; localState c1 = localState c2; xs \<noteq> []\<rbrakk> \<Longrightarrow> f_Exec_Comp trans_fun xs c1 = f_Exec_Comp trans_fun xs c2; Exec_Equal_State localState trans_fun; localState c1 = localState c2; a # xs \<noteq> []; xs = []\<rbrakk> \<Longrightarrow> f_Exec_Comp trans_fun (a # xs) c1 = f_Exec_Comp trans_fun (a # xs) c2
 2. \<And>a xs c1 c2. \<lbrakk>\<And>c1 c2. \<lbrakk>Exec_Equal_State localState trans_fun; localState c1 = localState c2; xs \<noteq> []\<rbrakk> \<Longrightarrow> f_Exec_Comp trans_fun xs c1 = f_Exec_Comp trans_fun xs c2; Exec_Equal_State localState trans_fun; localState c1 = localState c2; a # xs \<noteq> []; xs \<noteq> []\<rbrakk> \<Longrightarrow> f_Exec_Comp trans_fun (a # xs) c1 = f_Exec_Comp trans_fun (a # xs) c2
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a xs c1 c2. \<lbrakk>Exec_Equal_State localState trans_fun; localState c1 = localState c2; xs = []\<rbrakk> \<Longrightarrow> trans_fun a c1 = trans_fun a c2
 2. \<And>a xs c1 c2. \<lbrakk>\<And>c1 c2. \<lbrakk>Exec_Equal_State localState trans_fun; localState c1 = localState c2; xs \<noteq> []\<rbrakk> \<Longrightarrow> f_Exec_Comp trans_fun xs c1 = f_Exec_Comp trans_fun xs c2; Exec_Equal_State localState trans_fun; localState c1 = localState c2; a # xs \<noteq> []; xs \<noteq> []\<rbrakk> \<Longrightarrow> f_Exec_Comp trans_fun (a # xs) c1 = f_Exec_Comp trans_fun (a # xs) c2
[PROOF STEP]
apply (rule Exec_Equal_StateD, assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a xs c1 c2. \<lbrakk>\<And>c1 c2. \<lbrakk>Exec_Equal_State localState trans_fun; localState c1 = localState c2; xs \<noteq> []\<rbrakk> \<Longrightarrow> f_Exec_Comp trans_fun xs c1 = f_Exec_Comp trans_fun xs c2; Exec_Equal_State localState trans_fun; localState c1 = localState c2; a # xs \<noteq> []; xs \<noteq> []\<rbrakk> \<Longrightarrow> f_Exec_Comp trans_fun (a # xs) c1 = f_Exec_Comp trans_fun (a # xs) c2
[PROOF STEP]
apply (drule_tac x="trans_fun a c1" in meta_spec)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a xs c1 c2. \<lbrakk>Exec_Equal_State localState trans_fun; localState c1 = localState c2; a # xs \<noteq> []; xs \<noteq> []; \<And>c2. \<lbrakk>Exec_Equal_State localState trans_fun; localState (trans_fun a c1) = localState c2; xs \<noteq> []\<rbrakk> \<Longrightarrow> f_Exec_Comp trans_fun xs (trans_fun a c1) = f_Exec_Comp trans_fun xs c2\<rbrakk> \<Longrightarrow> f_Exec_Comp trans_fun (a # xs) c1 = f_Exec_Comp trans_fun (a # xs) c2
[PROOF STEP]
apply (drule_tac x="trans_fun a c2" in meta_spec)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a xs c1 c2. \<lbrakk>Exec_Equal_State localState trans_fun; localState c1 = localState c2; a # xs \<noteq> []; xs \<noteq> []; \<lbrakk>Exec_Equal_State localState trans_fun; localState (trans_fun a c1) = localState (trans_fun a c2); xs \<noteq> []\<rbrakk> \<Longrightarrow> f_Exec_Comp trans_fun xs (trans_fun a c1) = f_Exec_Comp trans_fun xs (trans_fun a c2)\<rbrakk> \<Longrightarrow> f_Exec_Comp trans_fun (a # xs) c1 = f_Exec_Comp trans_fun (a # xs) c2
[PROOF STEP]
apply (drule_tac ?c1.0=c1 and ?c2.0=c2 and m=a in Exec_Equal_StateD, assumption)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a xs c1 c2. \<lbrakk>localState c1 = localState c2; a # xs \<noteq> []; xs \<noteq> []; \<lbrakk>Exec_Equal_State localState trans_fun; localState (trans_fun a c1) = localState (trans_fun a c2); xs \<noteq> []\<rbrakk> \<Longrightarrow> f_Exec_Comp trans_fun xs (trans_fun a c1) = f_Exec_Comp trans_fun xs (trans_fun a c2); trans_fun a c1 = trans_fun a c2\<rbrakk> \<Longrightarrow> f_Exec_Comp trans_fun (a # xs) c1 = f_Exec_Comp trans_fun (a # xs) c2
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma f_Exec_Stream_Equal_State: "
  \<lbrakk> Exec_Equal_State localState trans_fun;
    localState c1 = localState c2 \<rbrakk> \<Longrightarrow>
  f_Exec_Comp_Stream trans_fun xs c1 =
  f_Exec_Comp_Stream trans_fun xs c2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Exec_Equal_State localState trans_fun; localState c1 = localState c2\<rbrakk> \<Longrightarrow> f_Exec_Comp_Stream trans_fun xs c1 = f_Exec_Comp_Stream trans_fun xs c2
[PROOF STEP]
apply (clarsimp simp: list_eq_iff f_Exec_Stream_nth)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i. \<lbrakk>Exec_Equal_State localState trans_fun; localState c1 = localState c2; i < length xs\<rbrakk> \<Longrightarrow> f_Exec_Comp trans_fun (xs \<down> Suc i) c1 = f_Exec_Comp trans_fun (xs \<down> Suc i) c2
[PROOF STEP]
apply (drule gr_implies_gr0)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i. \<lbrakk>Exec_Equal_State localState trans_fun; localState c1 = localState c2; 0 < length xs\<rbrakk> \<Longrightarrow> f_Exec_Comp trans_fun (xs \<down> Suc i) c1 = f_Exec_Comp trans_fun (xs \<down> Suc i) c2
[PROOF STEP]
apply (rule f_Exec_Equal_State)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>i. \<lbrakk>Exec_Equal_State localState trans_fun; localState c1 = localState c2; 0 < length xs\<rbrakk> \<Longrightarrow> Exec_Equal_State (?localState7 i) trans_fun
 2. \<And>i. \<lbrakk>Exec_Equal_State localState trans_fun; localState c1 = localState c2; 0 < length xs\<rbrakk> \<Longrightarrow> ?localState7 i c1 = ?localState7 i c2
 3. \<And>i. \<lbrakk>Exec_Equal_State localState trans_fun; localState c1 = localState c2; 0 < length xs\<rbrakk> \<Longrightarrow> xs \<down> Suc i \<noteq> []
[PROOF STEP]
apply simp+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma i_Exec_Stream_Equal_State: "
  \<lbrakk> Exec_Equal_State localState trans_fun;
    localState c1 = localState c2 \<rbrakk> \<Longrightarrow>
  i_Exec_Comp_Stream trans_fun input c1 =
  i_Exec_Comp_Stream trans_fun input c2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Exec_Equal_State localState trans_fun; localState c1 = localState c2\<rbrakk> \<Longrightarrow> i_Exec_Comp_Stream trans_fun input c1 = i_Exec_Comp_Stream trans_fun input c2
[PROOF STEP]
apply (clarsimp simp: ilist_eq_iff i_Exec_Stream_nth)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>Exec_Equal_State localState trans_fun; localState c1 = localState c2\<rbrakk> \<Longrightarrow> f_Exec_Comp trans_fun (input \<Down> Suc x) c1 = f_Exec_Comp trans_fun (input \<Down> Suc x) c2
[PROOF STEP]
apply (rule f_Exec_Equal_State)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>Exec_Equal_State localState trans_fun; localState c1 = localState c2\<rbrakk> \<Longrightarrow> Exec_Equal_State (?localState1 x) trans_fun
 2. \<And>x. \<lbrakk>Exec_Equal_State localState trans_fun; localState c1 = localState c2\<rbrakk> \<Longrightarrow> ?localState1 x c1 = ?localState1 x c2
 3. \<And>x. \<lbrakk>Exec_Equal_State localState trans_fun; localState c1 = localState c2\<rbrakk> \<Longrightarrow> input \<Down> Suc x \<noteq> []
[PROOF STEP]
apply simp+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma State_IdleD: "
  \<lbrakk> State_Idle localState output_fun trans_fun state;
    localState c = state \<rbrakk> \<Longrightarrow>
  localState (trans_fun \<NoMsg> c) = state \<and>
  output_fun (trans_fun \<NoMsg> c) = \<NoMsg>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>State_Idle localState output_fun trans_fun state; localState c = state\<rbrakk> \<Longrightarrow> localState (trans_fun NoMsg c) = state \<and> output_fun (trans_fun NoMsg c) = NoMsg
[PROOF STEP]
by (unfold State_Idle_def, blast)


[STATEMENT]
lemma State_IdleD': "
  State_Idle localState output_fun trans_fun state \<Longrightarrow>
  \<forall>c. localState c = state \<longrightarrow>
  localState (trans_fun \<NoMsg> c) = state \<and>
  output_fun (trans_fun \<NoMsg> c) = \<NoMsg>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. State_Idle localState output_fun trans_fun state \<Longrightarrow> \<forall>c. localState c = state \<longrightarrow> localState (trans_fun NoMsg c) = state \<and> output_fun (trans_fun NoMsg c) = NoMsg
[PROOF STEP]
by (unfold State_Idle_def, blast)


[STATEMENT]
lemma State_IdleI: "
  \<lbrakk> \<And>c. localState c = state \<Longrightarrow>
    localState (trans_fun \<NoMsg> c) = state \<and>
    output_fun (trans_fun \<NoMsg> c) = \<NoMsg> \<rbrakk> \<Longrightarrow>
  State_Idle localState output_fun trans_fun state"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>c. localState c = state \<Longrightarrow> localState (trans_fun NoMsg c) = state \<and> output_fun (trans_fun NoMsg c) = NoMsg) \<Longrightarrow> State_Idle localState output_fun trans_fun state
[PROOF STEP]
by (unfold State_Idle_def, blast)


[STATEMENT]
lemma State_Idle_step[rule_format]: "
  \<lbrakk> State_Idle localState output_fun trans_fun (localState c) \<rbrakk> \<Longrightarrow>
  State_Idle localState output_fun trans_fun (localState (trans_fun \<NoMsg> c))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. State_Idle localState output_fun trans_fun (localState c) \<Longrightarrow> State_Idle localState output_fun trans_fun (localState (trans_fun NoMsg c))
[PROOF STEP]
apply (frule State_IdleD[OF _ refl], erule conjE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>State_Idle localState output_fun trans_fun (localState c); localState (trans_fun NoMsg c) = localState c; output_fun (trans_fun NoMsg c) = NoMsg\<rbrakk> \<Longrightarrow> State_Idle localState output_fun trans_fun (localState (trans_fun NoMsg c))
[PROOF STEP]
apply (rule State_IdleI, rename_tac c0)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>c0. \<lbrakk>State_Idle localState output_fun trans_fun (localState c); localState (trans_fun NoMsg c) = localState c; output_fun (trans_fun NoMsg c) = NoMsg; localState c0 = localState (trans_fun NoMsg c)\<rbrakk> \<Longrightarrow> localState (trans_fun NoMsg c0) = localState (trans_fun NoMsg c) \<and> output_fun (trans_fun NoMsg c0) = NoMsg
[PROOF STEP]
apply (drule_tac c=c0 in State_IdleD)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>c0. \<lbrakk>localState (trans_fun NoMsg c) = localState c; output_fun (trans_fun NoMsg c) = NoMsg; localState c0 = localState (trans_fun NoMsg c)\<rbrakk> \<Longrightarrow> localState c0 = localState c
 2. \<And>c0. \<lbrakk>localState (trans_fun NoMsg c) = localState c; output_fun (trans_fun NoMsg c) = NoMsg; localState c0 = localState (trans_fun NoMsg c); localState (trans_fun NoMsg c0) = localState c \<and> output_fun (trans_fun NoMsg c0) = NoMsg\<rbrakk> \<Longrightarrow> localState (trans_fun NoMsg c0) = localState (trans_fun NoMsg c) \<and> output_fun (trans_fun NoMsg c0) = NoMsg
[PROOF STEP]
apply simp+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma f_Exec_State_Idle_replicate_NoMsg_state[rule_format]: "
  \<And>c. State_Idle localState output_fun trans_fun (localState c) \<Longrightarrow>
  localState (f_Exec_Comp trans_fun \<NoMsg>\<^bsup>n\<^esup> c) = localState c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>c. State_Idle localState output_fun trans_fun (localState c) \<Longrightarrow> localState (f_Exec_Comp trans_fun NoMsg\<^bsup>n\<^esup> c) = localState c
[PROOF STEP]
apply (induct n, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n c. \<lbrakk>\<And>c. State_Idle localState output_fun trans_fun (localState c) \<Longrightarrow> localState (f_Exec_Comp trans_fun NoMsg\<^bsup>n\<^esup> c) = localState c; State_Idle localState output_fun trans_fun (localState c)\<rbrakk> \<Longrightarrow> localState (f_Exec_Comp trans_fun NoMsg\<^bsup>Suc n\<^esup> c) = localState c
[PROOF STEP]
apply (frule State_Idle_step)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n c. \<lbrakk>\<And>c. State_Idle localState output_fun trans_fun (localState c) \<Longrightarrow> localState (f_Exec_Comp trans_fun NoMsg\<^bsup>n\<^esup> c) = localState c; State_Idle localState output_fun trans_fun (localState c); State_Idle localState output_fun trans_fun (localState (trans_fun NoMsg c))\<rbrakk> \<Longrightarrow> localState (f_Exec_Comp trans_fun NoMsg\<^bsup>Suc n\<^esup> c) = localState c
[PROOF STEP]
apply (drule_tac c=c in State_IdleD, rule refl)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n c. \<lbrakk>\<And>c. State_Idle localState output_fun trans_fun (localState c) \<Longrightarrow> localState (f_Exec_Comp trans_fun NoMsg\<^bsup>n\<^esup> c) = localState c; State_Idle localState output_fun trans_fun (localState (trans_fun NoMsg c)); localState (trans_fun NoMsg c) = localState c \<and> output_fun (trans_fun NoMsg c) = NoMsg\<rbrakk> \<Longrightarrow> localState (f_Exec_Comp trans_fun NoMsg\<^bsup>Suc n\<^esup> c) = localState c
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma f_Exec_State_Idle_replicate_NoMsg_gr0_output[rule_format]: "\<And>c.
  \<lbrakk> State_Idle localState output_fun trans_fun (localState c); 0 < n \<rbrakk> \<Longrightarrow>
  output_fun (f_Exec_Comp trans_fun \<NoMsg>\<^bsup>n\<^esup> c) = \<NoMsg>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>c. \<lbrakk>State_Idle localState output_fun trans_fun (localState c); 0 < n\<rbrakk> \<Longrightarrow> output_fun (f_Exec_Comp trans_fun NoMsg\<^bsup>n\<^esup> c) = NoMsg
[PROOF STEP]
apply (induct n, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n c. \<lbrakk>\<And>c. \<lbrakk>State_Idle localState output_fun trans_fun (localState c); 0 < n\<rbrakk> \<Longrightarrow> output_fun (f_Exec_Comp trans_fun NoMsg\<^bsup>n\<^esup> c) = NoMsg; State_Idle localState output_fun trans_fun (localState c); 0 < Suc n\<rbrakk> \<Longrightarrow> output_fun (f_Exec_Comp trans_fun NoMsg\<^bsup>Suc n\<^esup> c) = NoMsg
[PROOF STEP]
apply (case_tac "n = 0")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>n c. \<lbrakk>\<And>c. \<lbrakk>State_Idle localState output_fun trans_fun (localState c); 0 < n\<rbrakk> \<Longrightarrow> output_fun (f_Exec_Comp trans_fun NoMsg\<^bsup>n\<^esup> c) = NoMsg; State_Idle localState output_fun trans_fun (localState c); 0 < Suc n; n = 0\<rbrakk> \<Longrightarrow> output_fun (f_Exec_Comp trans_fun NoMsg\<^bsup>Suc n\<^esup> c) = NoMsg
 2. \<And>n c. \<lbrakk>\<And>c. \<lbrakk>State_Idle localState output_fun trans_fun (localState c); 0 < n\<rbrakk> \<Longrightarrow> output_fun (f_Exec_Comp trans_fun NoMsg\<^bsup>n\<^esup> c) = NoMsg; State_Idle localState output_fun trans_fun (localState c); 0 < Suc n; n \<noteq> 0\<rbrakk> \<Longrightarrow> output_fun (f_Exec_Comp trans_fun NoMsg\<^bsup>Suc n\<^esup> c) = NoMsg
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>n c. \<lbrakk>State_Idle localState output_fun trans_fun (localState c); n = 0\<rbrakk> \<Longrightarrow> output_fun (trans_fun NoMsg c) = NoMsg
 2. \<And>n c. \<lbrakk>\<And>c. \<lbrakk>State_Idle localState output_fun trans_fun (localState c); 0 < n\<rbrakk> \<Longrightarrow> output_fun (f_Exec_Comp trans_fun NoMsg\<^bsup>n\<^esup> c) = NoMsg; State_Idle localState output_fun trans_fun (localState c); 0 < Suc n; n \<noteq> 0\<rbrakk> \<Longrightarrow> output_fun (f_Exec_Comp trans_fun NoMsg\<^bsup>Suc n\<^esup> c) = NoMsg
[PROOF STEP]
apply (rule State_IdleD[THEN conjunct2], assumption, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n c. \<lbrakk>\<And>c. \<lbrakk>State_Idle localState output_fun trans_fun (localState c); 0 < n\<rbrakk> \<Longrightarrow> output_fun (f_Exec_Comp trans_fun NoMsg\<^bsup>n\<^esup> c) = NoMsg; State_Idle localState output_fun trans_fun (localState c); 0 < Suc n; n \<noteq> 0\<rbrakk> \<Longrightarrow> output_fun (f_Exec_Comp trans_fun NoMsg\<^bsup>Suc n\<^esup> c) = NoMsg
[PROOF STEP]
apply (drule State_Idle_step)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n c. \<lbrakk>\<And>c. \<lbrakk>State_Idle localState output_fun trans_fun (localState c); 0 < n\<rbrakk> \<Longrightarrow> output_fun (f_Exec_Comp trans_fun NoMsg\<^bsup>n\<^esup> c) = NoMsg; 0 < Suc n; n \<noteq> 0; State_Idle localState output_fun trans_fun (localState (trans_fun NoMsg c))\<rbrakk> \<Longrightarrow> output_fun (f_Exec_Comp trans_fun NoMsg\<^bsup>Suc n\<^esup> c) = NoMsg
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma f_Exec_State_Idle_replicate_NoMsg_output[rule_format]: "
  \<lbrakk> State_Idle localState output_fun trans_fun (localState c);
    output_fun c = \<NoMsg> \<rbrakk> \<Longrightarrow>
  output_fun (f_Exec_Comp trans_fun \<NoMsg>\<^bsup>n\<^esup> c) = \<NoMsg>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>State_Idle localState output_fun trans_fun (localState c); output_fun c = NoMsg\<rbrakk> \<Longrightarrow> output_fun (f_Exec_Comp trans_fun NoMsg\<^bsup>n\<^esup> c) = NoMsg
[PROOF STEP]
apply (case_tac "n = 0", simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>State_Idle localState output_fun trans_fun (localState c); output_fun c = NoMsg; n \<noteq> 0\<rbrakk> \<Longrightarrow> output_fun (f_Exec_Comp trans_fun NoMsg\<^bsup>n\<^esup> c) = NoMsg
[PROOF STEP]
apply (simp add: f_Exec_State_Idle_replicate_NoMsg_gr0_output)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma f_Exec_Stream_State_Idle_replicate_NoMsg_output[rule_format]: "
  \<lbrakk> State_Idle localState output_fun trans_fun (localState c) \<rbrakk> \<Longrightarrow>
  map output_fun (f_Exec_Comp_Stream trans_fun \<NoMsg>\<^bsup>n\<^esup> c) = \<NoMsg>\<^bsup>n\<^esup>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. State_Idle localState output_fun trans_fun (localState c) \<Longrightarrow> map output_fun (f_Exec_Comp_Stream trans_fun NoMsg\<^bsup>n\<^esup> c) = NoMsg\<^bsup>n\<^esup>
[PROOF STEP]
by (simp add: list_eq_iff f_Exec_Stream_nth min_eqL f_Exec_State_Idle_replicate_NoMsg_gr0_output del: replicate.simps)


[STATEMENT]
lemma State_Idle_append_replicate_NoMsg_output_last_message: "
  \<lbrakk> State_Idle localState output_fun trans_fun (
      localState (f_Exec_Comp trans_fun xs c)) \<rbrakk> \<Longrightarrow>
  last_message (map output_fun (f_Exec_Comp_Stream trans_fun (xs @ \<NoMsg>\<^bsup>n\<^esup>) c)) =
  last_message (map output_fun (f_Exec_Comp_Stream trans_fun xs c))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun xs c)) \<Longrightarrow> last_message (map output_fun (f_Exec_Comp_Stream trans_fun (xs @ NoMsg\<^bsup>n\<^esup>) c)) = last_message (map output_fun (f_Exec_Comp_Stream trans_fun xs c))
[PROOF STEP]
by (simp add: f_Exec_Stream_State_Idle_append_replicate_NoMsg_gr0_output last_message_append_replicate_NoMsg)


[STATEMENT]
lemma State_Idle_append_replicate_NoMsg_output_Msg_eq_last_message: "
  \<lbrakk> State_Idle localState output_fun trans_fun (
      localState (f_Exec_Comp trans_fun xs c));
    output_fun (f_Exec_Comp trans_fun xs c) \<noteq> \<NoMsg>;
    xs \<noteq> [] \<rbrakk> \<Longrightarrow>
  last_message (map output_fun (f_Exec_Comp_Stream trans_fun (xs @ \<NoMsg>\<^bsup>n\<^esup>) c)) =
  output_fun (f_Exec_Comp trans_fun xs c)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun xs c)); output_fun (f_Exec_Comp trans_fun xs c) \<noteq> NoMsg; xs \<noteq> []\<rbrakk> \<Longrightarrow> last_message (map output_fun (f_Exec_Comp_Stream trans_fun (xs @ NoMsg\<^bsup>n\<^esup>) c)) = output_fun (f_Exec_Comp trans_fun xs c)
[PROOF STEP]
apply (simp add: State_Idle_append_replicate_NoMsg_output_last_message f_Exec_eq_f_Exec_Stream_last2 )
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>State_Idle localState output_fun trans_fun (localState (last (f_Exec_Comp_Stream trans_fun xs c))); output_fun (last (f_Exec_Comp_Stream trans_fun xs c)) \<noteq> NoMsg; xs \<noteq> []\<rbrakk> \<Longrightarrow> last_message (map output_fun (f_Exec_Comp_Stream trans_fun xs c)) = output_fun (last (f_Exec_Comp_Stream trans_fun xs c))
[PROOF STEP]
apply (subst last_message_Msg_eq_last)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>State_Idle localState output_fun trans_fun (localState (last (f_Exec_Comp_Stream trans_fun xs c))); output_fun (last (f_Exec_Comp_Stream trans_fun xs c)) \<noteq> NoMsg; xs \<noteq> []\<rbrakk> \<Longrightarrow> map output_fun (f_Exec_Comp_Stream trans_fun xs c) \<noteq> []
 2. \<lbrakk>State_Idle localState output_fun trans_fun (localState (last (f_Exec_Comp_Stream trans_fun xs c))); output_fun (last (f_Exec_Comp_Stream trans_fun xs c)) \<noteq> NoMsg; xs \<noteq> []\<rbrakk> \<Longrightarrow> last (map output_fun (f_Exec_Comp_Stream trans_fun xs c)) \<noteq> NoMsg
 3. \<lbrakk>State_Idle localState output_fun trans_fun (localState (last (f_Exec_Comp_Stream trans_fun xs c))); output_fun (last (f_Exec_Comp_Stream trans_fun xs c)) \<noteq> NoMsg; xs \<noteq> []\<rbrakk> \<Longrightarrow> last (map output_fun (f_Exec_Comp_Stream trans_fun xs c)) = output_fun (last (f_Exec_Comp_Stream trans_fun xs c))
[PROOF STEP]
apply (simp add: map_last f_Exec_Stream_not_empty_conv)+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma State_Idle_imp_exists_state_change: "
  \<lbrakk> \<not> State_Idle localState output_fun trans_fun (localState c);
    State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun \<NoMsg>\<^bsup>n\<^esup> c)) \<rbrakk> \<Longrightarrow>
  \<exists>i<n. (
    \<not> State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun \<NoMsg>\<^bsup>i\<^esup> c)) \<and> (
    \<forall>j\<le>n. i < j \<longrightarrow> State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun \<NoMsg>\<^bsup>j\<^esup> c))))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> State_Idle localState output_fun trans_fun (localState c); State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun NoMsg\<^bsup>n\<^esup> c))\<rbrakk> \<Longrightarrow> \<exists>i<n. \<not> State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun NoMsg\<^bsup>i\<^esup> c)) \<and> (\<forall>j\<le>n. i < j \<longrightarrow> State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun NoMsg\<^bsup>j\<^esup> c)))
[PROOF STEP]
apply (cut_tac
  a=0 and b=n and
  P="\<lambda>x. State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun NoMsg\<^bsup>x\<^esup> c))"
  in nat_Suc_predicate_change_exists, simp+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> State_Idle localState output_fun trans_fun (localState c); State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun NoMsg\<^bsup>n\<^esup> c)); \<exists>na<n. \<not> State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun NoMsg\<^bsup>na\<^esup> c)) \<and> State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun NoMsg\<^bsup>na\<^esup> (trans_fun NoMsg c)))\<rbrakk> \<Longrightarrow> \<exists>i<n. \<not> State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun NoMsg\<^bsup>i\<^esup> c)) \<and> (\<forall>j\<le>n. i < j \<longrightarrow> State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun NoMsg\<^bsup>j\<^esup> c)))
[PROOF STEP]
apply (clarify, rename_tac n1)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n1. \<lbrakk>\<not> State_Idle localState output_fun trans_fun (localState c); State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun NoMsg\<^bsup>n\<^esup> c)); n1 < n; \<not> State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun NoMsg\<^bsup>n1\<^esup> c)); State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun NoMsg\<^bsup>n1\<^esup> (trans_fun NoMsg c)))\<rbrakk> \<Longrightarrow> \<exists>i<n. \<not> State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun NoMsg\<^bsup>i\<^esup> c)) \<and> (\<forall>j\<le>n. i < j \<longrightarrow> State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun NoMsg\<^bsup>j\<^esup> c)))
[PROOF STEP]
apply (rule_tac x=n1 in exI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n1. \<lbrakk>\<not> State_Idle localState output_fun trans_fun (localState c); State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun NoMsg\<^bsup>n\<^esup> c)); n1 < n; \<not> State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun NoMsg\<^bsup>n1\<^esup> c)); State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun NoMsg\<^bsup>n1\<^esup> (trans_fun NoMsg c)))\<rbrakk> \<Longrightarrow> n1 < n \<and> \<not> State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun NoMsg\<^bsup>n1\<^esup> c)) \<and> (\<forall>j\<le>n. n1 < j \<longrightarrow> State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun NoMsg\<^bsup>j\<^esup> c)))
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n1 j. \<lbrakk>\<not> State_Idle localState output_fun trans_fun (localState c); State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun NoMsg\<^bsup>n\<^esup> c)); \<not> State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun NoMsg\<^bsup>n1\<^esup> c)); State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun NoMsg\<^bsup>n1\<^esup> (trans_fun NoMsg c))); j \<le> n; n1 < j\<rbrakk> \<Longrightarrow> State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun NoMsg\<^bsup>j\<^esup> c))
[PROOF STEP]
apply (rule_tac t="j" and s="Suc n1 + (j - Suc n1)" in subst, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n1 j. \<lbrakk>\<not> State_Idle localState output_fun trans_fun (localState c); State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun NoMsg\<^bsup>n\<^esup> c)); \<not> State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun NoMsg\<^bsup>n1\<^esup> c)); State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun NoMsg\<^bsup>n1\<^esup> (trans_fun NoMsg c))); j \<le> n; n1 < j\<rbrakk> \<Longrightarrow> State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun NoMsg\<^bsup>Suc n1 + (j - Suc n1)\<^esup> c))
[PROOF STEP]
apply (subst replicate_add)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n1 j. \<lbrakk>\<not> State_Idle localState output_fun trans_fun (localState c); State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun NoMsg\<^bsup>n\<^esup> c)); \<not> State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun NoMsg\<^bsup>n1\<^esup> c)); State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun NoMsg\<^bsup>n1\<^esup> (trans_fun NoMsg c))); j \<le> n; n1 < j\<rbrakk> \<Longrightarrow> State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun (NoMsg\<^bsup>Suc n1\<^esup> @ NoMsg\<^bsup>j - Suc n1\<^esup>) c))
[PROOF STEP]
apply (simp add: replicate_add f_Exec_State_Idle_append_replicate_NoMsg_state)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma State_Idle_imp_exists_state_change2: "
  \<lbrakk> \<not> State_Idle localState output_fun trans_fun (localState c);
    State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun \<NoMsg>\<^bsup>n\<^esup> c)) \<rbrakk> \<Longrightarrow>
  \<exists>i<n. (
    (\<forall>j\<le>i. \<not> State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun \<NoMsg>\<^bsup>i\<^esup> c))) \<and>
    (\<forall>j\<le>n. i < j \<longrightarrow> State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun \<NoMsg>\<^bsup>j\<^esup> c))))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> State_Idle localState output_fun trans_fun (localState c); State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun NoMsg\<^bsup>n\<^esup> c))\<rbrakk> \<Longrightarrow> \<exists>i<n. (\<forall>j\<le>i. \<not> State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun NoMsg\<^bsup>i\<^esup> c))) \<and> (\<forall>j\<le>n. i < j \<longrightarrow> State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun NoMsg\<^bsup>j\<^esup> c)))
[PROOF STEP]
apply (frule State_Idle_imp_exists_state_change, assumption)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> State_Idle localState output_fun trans_fun (localState c); State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun NoMsg\<^bsup>n\<^esup> c)); \<exists>i<n. \<not> State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun NoMsg\<^bsup>i\<^esup> c)) \<and> (\<forall>j\<le>n. i < j \<longrightarrow> State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun NoMsg\<^bsup>j\<^esup> c)))\<rbrakk> \<Longrightarrow> \<exists>i<n. (\<forall>j\<le>i. \<not> State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun NoMsg\<^bsup>i\<^esup> c))) \<and> (\<forall>j\<le>n. i < j \<longrightarrow> State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun NoMsg\<^bsup>j\<^esup> c)))
[PROOF STEP]
apply (clarify, rename_tac i)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i. \<lbrakk>\<not> State_Idle localState output_fun trans_fun (localState c); State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun NoMsg\<^bsup>n\<^esup> c)); i < n; \<not> State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun NoMsg\<^bsup>i\<^esup> c)); \<forall>j\<le>n. i < j \<longrightarrow> State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun NoMsg\<^bsup>j\<^esup> c))\<rbrakk> \<Longrightarrow> \<exists>i<n. (\<forall>j\<le>i. \<not> State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun NoMsg\<^bsup>i\<^esup> c))) \<and> (\<forall>j\<le>n. i < j \<longrightarrow> State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun NoMsg\<^bsup>j\<^esup> c)))
[PROOF STEP]
apply (rule_tac x=i in exI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i. \<lbrakk>\<not> State_Idle localState output_fun trans_fun (localState c); State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun NoMsg\<^bsup>n\<^esup> c)); i < n; \<not> State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun NoMsg\<^bsup>i\<^esup> c)); \<forall>j\<le>n. i < j \<longrightarrow> State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun NoMsg\<^bsup>j\<^esup> c))\<rbrakk> \<Longrightarrow> i < n \<and> (\<forall>j\<le>i. \<not> State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun NoMsg\<^bsup>i\<^esup> c))) \<and> (\<forall>j\<le>n. i < j \<longrightarrow> State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun NoMsg\<^bsup>j\<^esup> c)))
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma f_Exec_Stream_Acc_Output_length[simp]: "
  0 < k \<Longrightarrow>
  length (f_Exec_Comp_Stream_Acc_Output k output_fun trans_fun xs c) = length xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < k \<Longrightarrow> length (f_Exec_Comp_Stream_Acc_Output k output_fun trans_fun xs c) = length xs
[PROOF STEP]
by (simp add: f_Exec_Comp_Stream_Acc_Output_def f_shrink_length)


[STATEMENT]
lemma f_Exec_Stream_Acc_LocalState_length[simp]: "
  0 < k \<Longrightarrow>
  length (f_Exec_Comp_Stream_Acc_LocalState k localState trans_fun xs c) = length xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < k \<Longrightarrow> length (f_Exec_Comp_Stream_Acc_LocalState k localState trans_fun xs c) = length xs
[PROOF STEP]
by (simp add: f_Exec_Comp_Stream_Acc_LocalState_def f_shrink_last_length)


[STATEMENT]
lemma f_Exec_Stream_Acc_Output_Nil[simp]: "
  f_Exec_Comp_Stream_Acc_Output k output_fun trans_fun [] c = []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f_Exec_Comp_Stream_Acc_Output k output_fun trans_fun [] c = []
[PROOF STEP]
by (simp add: f_Exec_Comp_Stream_Acc_Output_def)


[STATEMENT]
lemma f_Exec_Stream_Acc_LocalState_Nil[simp]: "
  f_Exec_Comp_Stream_Acc_LocalState k localState trans_fun [] c = []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f_Exec_Comp_Stream_Acc_LocalState k localState trans_fun [] c = []
[PROOF STEP]
by (simp add: f_Exec_Comp_Stream_Acc_LocalState_def)


[STATEMENT]
lemma f_Exec_Stream_Acc_Output_0[simp]: "
  f_Exec_Comp_Stream_Acc_Output 0 output_fun trans_fun xs c = []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f_Exec_Comp_Stream_Acc_Output 0 output_fun trans_fun xs c = []
[PROOF STEP]
by (simp add: f_Exec_Comp_Stream_Acc_Output_def)


[STATEMENT]
lemma f_Exec_Stream_Acc_LocalState_0[simp]: "
  f_Exec_Comp_Stream_Acc_LocalState 0 localState trans_fun xs c = []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f_Exec_Comp_Stream_Acc_LocalState 0 localState trans_fun xs c = []
[PROOF STEP]
by (simp add: f_Exec_Comp_Stream_Acc_LocalState_def)


[STATEMENT]
lemma f_Exec_Stream_Acc_Output_1[simp]: "
  f_Exec_Comp_Stream_Acc_Output (Suc 0) output_fun trans_fun xs c =
  map output_fun (f_Exec_Comp_Stream trans_fun xs c)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f_Exec_Comp_Stream_Acc_Output (Suc 0) output_fun trans_fun xs c = map output_fun (f_Exec_Comp_Stream trans_fun xs c)
[PROOF STEP]
by (simp add: f_Exec_Comp_Stream_Acc_Output_def)


[STATEMENT]
lemma f_Exec_Stream_Acc_LocalState_1[simp]: "
  f_Exec_Comp_Stream_Acc_LocalState (Suc 0) localState trans_fun xs c =
  map localState (f_Exec_Comp_Stream trans_fun xs c)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f_Exec_Comp_Stream_Acc_LocalState (Suc 0) localState trans_fun xs c = map localState (f_Exec_Comp_Stream trans_fun xs c)
[PROOF STEP]
by (simp add: f_Exec_Comp_Stream_Acc_LocalState_def)


[STATEMENT]
lemma i_Exec_Stream_Acc_Output_1[simp]: "
  i_Exec_Comp_Stream_Acc_Output (Suc 0) output_fun trans_fun input c =
  output_fun \<circ> (i_Exec_Comp_Stream trans_fun input c)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i_Exec_Comp_Stream_Acc_Output (Suc 0) output_fun trans_fun input c = output_fun \<circ> i_Exec_Comp_Stream trans_fun input c
[PROOF STEP]
by (simp add: i_Exec_Comp_Stream_Acc_Output_def)


[STATEMENT]
lemma i_Exec_Stream_Acc_LocalState_1[simp]: "
  i_Exec_Comp_Stream_Acc_LocalState (Suc 0) localState trans_fun input c =
  localState \<circ> (i_Exec_Comp_Stream trans_fun input c)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i_Exec_Comp_Stream_Acc_LocalState (Suc 0) localState trans_fun input c = localState \<circ> i_Exec_Comp_Stream trans_fun input c
[PROOF STEP]
by (simp add: i_Exec_Comp_Stream_Acc_LocalState_def)


[STATEMENT]
lemma f_Exec_Stream_Acc_Output_eq_last_message_hold: "
  f_Exec_Comp_Stream_Acc_Output k output_fun trans_fun xs c =
  (map output_fun (f_Exec_Comp_Stream trans_fun (xs \<odot>\<^sub>f k) c)) \<longmapsto>\<^sub>f k \<div>\<^bsub>fl\<^esub> k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f_Exec_Comp_Stream_Acc_Output k output_fun trans_fun xs c = map output_fun (f_Exec_Comp_Stream trans_fun (xs \<odot> k) c) \<longmapsto> k \<div>\<^sub>l k
[PROOF STEP]
by (simp add: f_Exec_Comp_Stream_Acc_Output_def f_shrink_eq_f_last_message_hold_shrink_last)


[STATEMENT]
lemma i_Exec_Stream_Acc_Output_eq_last_message_hold: "0 < k \<Longrightarrow>
  i_Exec_Comp_Stream_Acc_Output k output_fun trans_fun input c =
  (output_fun \<circ> (i_Exec_Comp_Stream trans_fun (input \<odot>\<^sub>i k) c)) \<longmapsto>\<^sub>i k \<div>\<^bsub>il\<^esub> k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < k \<Longrightarrow> i_Exec_Comp_Stream_Acc_Output k output_fun trans_fun input c = (output_fun \<circ> i_Exec_Comp_Stream trans_fun (input \<odot> k) c) \<longmapsto> k \<div>\<^sub>l k
[PROOF STEP]
by (simp add: i_Exec_Comp_Stream_Acc_Output_def i_shrink_eq_i_last_message_hold_shrink_last)


[STATEMENT]
lemma f_Exec_Stream_Acc_Output_take: "
  f_Exec_Comp_Stream_Acc_Output k output_fun trans_fun xs c \<down> n =
  f_Exec_Comp_Stream_Acc_Output k output_fun trans_fun (xs \<down> n) c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f_Exec_Comp_Stream_Acc_Output k output_fun trans_fun xs c \<down> n = f_Exec_Comp_Stream_Acc_Output k output_fun trans_fun (xs \<down> n) c
[PROOF STEP]
by (simp add: f_Exec_Comp_Stream_Acc_Output_def f_shrink_def f_Exec_Stream_expand_aggregate_map_take)


[STATEMENT]
lemma f_Exec_Stream_Acc_Output_drop: "
  f_Exec_Comp_Stream_Acc_Output k output_fun trans_fun xs c \<up> n =
  f_Exec_Comp_Stream_Acc_Output k output_fun trans_fun (xs \<up> n) (
    f_Exec_Comp trans_fun (xs \<down> n \<odot>\<^sub>f k) c)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f_Exec_Comp_Stream_Acc_Output k output_fun trans_fun xs c \<up> n = f_Exec_Comp_Stream_Acc_Output k output_fun trans_fun (xs \<up> n) (f_Exec_Comp trans_fun (xs \<down> n \<odot> k) c)
[PROOF STEP]
by (simp add: f_Exec_Comp_Stream_Acc_Output_def f_shrink_def f_Exec_Stream_expand_aggregate_map_drop)


[STATEMENT]
lemma i_Exec_Stream_Acc_Output_take: "
  0 < k \<Longrightarrow>
  i_Exec_Comp_Stream_Acc_Output k output_fun trans_fun input c \<Down> n =
  f_Exec_Comp_Stream_Acc_Output k output_fun trans_fun (input \<Down> n) c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < k \<Longrightarrow> i_Exec_Comp_Stream_Acc_Output k output_fun trans_fun input c \<Down> n = f_Exec_Comp_Stream_Acc_Output k output_fun trans_fun (input \<Down> n) c
[PROOF STEP]
by (simp add: f_Exec_Comp_Stream_Acc_Output_def i_Exec_Comp_Stream_Acc_Output_def
  f_shrink_def i_shrink_def i_Exec_Stream_expand_aggregate_map_take)


[STATEMENT]
lemma i_Exec_Stream_Acc_Output_drop: "
  0 < k \<Longrightarrow>
  i_Exec_Comp_Stream_Acc_Output k output_fun trans_fun input c \<Up> n =
  i_Exec_Comp_Stream_Acc_Output k output_fun trans_fun (input \<Up> n) (
    f_Exec_Comp trans_fun (input \<Down> n \<odot>\<^sub>f k) c)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < k \<Longrightarrow> i_Exec_Comp_Stream_Acc_Output k output_fun trans_fun input c \<Up> n = i_Exec_Comp_Stream_Acc_Output k output_fun trans_fun (input \<Up> n) (f_Exec_Comp trans_fun (input \<Down> n \<odot> k) c)
[PROOF STEP]
by (simp add: i_Exec_Comp_Stream_Acc_Output_def i_shrink_def i_Exec_Stream_expand_aggregate_map_drop)


[STATEMENT]
lemma i_Exec_Stream_Acc_LocalState_take: "
  0 < k \<Longrightarrow>
  i_Exec_Comp_Stream_Acc_LocalState k localState trans_fun input c \<Down> n =
  f_Exec_Comp_Stream_Acc_LocalState k localState trans_fun (input \<Down> n) c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < k \<Longrightarrow> i_Exec_Comp_Stream_Acc_LocalState k localState trans_fun input c \<Down> n = f_Exec_Comp_Stream_Acc_LocalState k localState trans_fun (input \<Down> n) c
[PROOF STEP]
by (simp add: f_Exec_Comp_Stream_Acc_LocalState_def i_Exec_Comp_Stream_Acc_LocalState_def
  f_shrink_last_def i_shrink_last_def i_Exec_Stream_expand_aggregate_map_take)


[STATEMENT]
lemma i_Exec_Stream_Acc_LocalState_drop: "
  0 < k \<Longrightarrow>
  i_Exec_Comp_Stream_Acc_LocalState k localState trans_fun input c \<Up> n =
  i_Exec_Comp_Stream_Acc_LocalState k localState trans_fun (input \<Up> n) (
    f_Exec_Comp trans_fun (input \<Down> n \<odot>\<^sub>f k) c)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < k \<Longrightarrow> i_Exec_Comp_Stream_Acc_LocalState k localState trans_fun input c \<Up> n = i_Exec_Comp_Stream_Acc_LocalState k localState trans_fun (input \<Up> n) (f_Exec_Comp trans_fun (input \<Down> n \<odot> k) c)
[PROOF STEP]
by (simp add: i_Exec_Comp_Stream_Acc_LocalState_def i_shrink_last_def i_Exec_Stream_expand_aggregate_map_drop)


[STATEMENT]
lemma f_Exec_Stream_Acc_Output_append: "
  f_Exec_Comp_Stream_Acc_Output k output_fun trans_fun (xs @ ys) c =
  f_Exec_Comp_Stream_Acc_Output k output_fun trans_fun xs c @
  f_Exec_Comp_Stream_Acc_Output k output_fun trans_fun ys (
    f_Exec_Comp trans_fun (xs \<odot>\<^sub>f k) c)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f_Exec_Comp_Stream_Acc_Output k output_fun trans_fun (xs @ ys) c = f_Exec_Comp_Stream_Acc_Output k output_fun trans_fun xs c @ f_Exec_Comp_Stream_Acc_Output k output_fun trans_fun ys (f_Exec_Comp trans_fun (xs \<odot> k) c)
[PROOF STEP]
by (simp only: f_Exec_Comp_Stream_Acc_Output_def f_shrink_def f_Exec_Stream_expand_map_aggregate_append)


[STATEMENT]
lemma f_Exec_Stream_Acc_Output_Cons: "
  0 < k \<Longrightarrow>
  f_Exec_Comp_Stream_Acc_Output k output_fun trans_fun (x # xs) c =
  last_message (map output_fun (f_Exec_Comp_Stream trans_fun (x # \<NoMsg>\<^bsup>k - Suc 0\<^esup>) c)) #
  f_Exec_Comp_Stream_Acc_Output k output_fun trans_fun xs (
    f_Exec_Comp trans_fun (x # \<NoMsg>\<^bsup>k - Suc 0\<^esup>) c)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < k \<Longrightarrow> f_Exec_Comp_Stream_Acc_Output k output_fun trans_fun (x # xs) c = last_message (map output_fun (f_Exec_Comp_Stream trans_fun (x # NoMsg\<^bsup>k - Suc 0\<^esup>) c)) # f_Exec_Comp_Stream_Acc_Output k output_fun trans_fun xs (f_Exec_Comp trans_fun (x # NoMsg\<^bsup>k - Suc 0\<^esup>) c)
[PROOF STEP]
by (simp only: f_Exec_Comp_Stream_Acc_Output_def f_shrink_def f_Exec_Stream_expand_map_aggregate_Cons)


[STATEMENT]
lemma f_Exec_Stream_Acc_Output_one: "
  0 < k \<Longrightarrow>
  f_Exec_Comp_Stream_Acc_Output k output_fun trans_fun [x] c =
  [last_message (map output_fun (f_Exec_Comp_Stream trans_fun (x # \<NoMsg>\<^bsup>k - Suc 0\<^esup>) c))]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < k \<Longrightarrow> f_Exec_Comp_Stream_Acc_Output k output_fun trans_fun [x] c = [last_message (map output_fun (f_Exec_Comp_Stream trans_fun (x # NoMsg\<^bsup>k - Suc 0\<^esup>) c))]
[PROOF STEP]
by (simp add: f_Exec_Stream_Acc_Output_Cons)


[STATEMENT]
lemma f_Exec_Stream_Acc_Output_snoc: "
  0 < k \<Longrightarrow>
  f_Exec_Comp_Stream_Acc_Output k output_fun trans_fun (xs @ [x]) c =
  f_Exec_Comp_Stream_Acc_Output k output_fun trans_fun xs c @
  [last_message (map output_fun (f_Exec_Comp_Stream trans_fun (x # \<NoMsg>\<^bsup>k - Suc 0\<^esup>) (
    f_Exec_Comp trans_fun (xs \<odot>\<^sub>f k) c)))]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < k \<Longrightarrow> f_Exec_Comp_Stream_Acc_Output k output_fun trans_fun (xs @ [x]) c = f_Exec_Comp_Stream_Acc_Output k output_fun trans_fun xs c @ [last_message (map output_fun (f_Exec_Comp_Stream trans_fun (x # NoMsg\<^bsup>k - Suc 0\<^esup>) (f_Exec_Comp trans_fun (xs \<odot> k) c)))]
[PROOF STEP]
by (simp add: f_Exec_Stream_Acc_Output_append f_Exec_Stream_Acc_Output_one)


[STATEMENT]
lemma i_Exec_Stream_Acc_Output_append: "
  i_Exec_Comp_Stream_Acc_Output k output_fun trans_fun (xs \<frown> input) c =
  f_Exec_Comp_Stream_Acc_Output k output_fun trans_fun xs c \<frown>
  i_Exec_Comp_Stream_Acc_Output k output_fun trans_fun input (
    f_Exec_Comp trans_fun (xs \<odot>\<^sub>f k) c)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i_Exec_Comp_Stream_Acc_Output k output_fun trans_fun (xs \<frown> input) c = f_Exec_Comp_Stream_Acc_Output k output_fun trans_fun xs c \<frown> i_Exec_Comp_Stream_Acc_Output k output_fun trans_fun input (f_Exec_Comp trans_fun (xs \<odot> k) c)
[PROOF STEP]
by (simp add: f_Exec_Comp_Stream_Acc_Output_def i_Exec_Comp_Stream_Acc_Output_def f_shrink_def i_shrink_def i_Exec_Stream_expand_map_aggregate_append)


[STATEMENT]
lemma i_Exec_Stream_Acc_Output_Cons: "
  0 < k \<Longrightarrow>
  i_Exec_Comp_Stream_Acc_Output k output_fun trans_fun ([x] \<frown> input) c =
  [last_message (map output_fun (f_Exec_Comp_Stream trans_fun (x # \<NoMsg>\<^bsup>k - Suc 0\<^esup>) c))] \<frown>
  i_Exec_Comp_Stream_Acc_Output k output_fun trans_fun input (
    f_Exec_Comp trans_fun (x # \<NoMsg>\<^bsup>k - Suc 0\<^esup>) c)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < k \<Longrightarrow> i_Exec_Comp_Stream_Acc_Output k output_fun trans_fun ([x] \<frown> input) c = [last_message (map output_fun (f_Exec_Comp_Stream trans_fun (x # NoMsg\<^bsup>k - Suc 0\<^esup>) c))] \<frown> i_Exec_Comp_Stream_Acc_Output k output_fun trans_fun input (f_Exec_Comp trans_fun (x # NoMsg\<^bsup>k - Suc 0\<^esup>) c)
[PROOF STEP]
by (simp add: i_Exec_Stream_Acc_Output_append f_Exec_Stream_Acc_Output_one)


[STATEMENT]
lemma f_Exec_Stream_Acc_LocalState_append: "
  f_Exec_Comp_Stream_Acc_LocalState k localState trans_fun (xs @ ys) c =
  f_Exec_Comp_Stream_Acc_LocalState k localState trans_fun xs c @
  f_Exec_Comp_Stream_Acc_LocalState k localState trans_fun ys (
    f_Exec_Comp trans_fun (xs \<odot>\<^sub>f k) c)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f_Exec_Comp_Stream_Acc_LocalState k localState trans_fun (xs @ ys) c = f_Exec_Comp_Stream_Acc_LocalState k localState trans_fun xs c @ f_Exec_Comp_Stream_Acc_LocalState k localState trans_fun ys (f_Exec_Comp trans_fun (xs \<odot> k) c)
[PROOF STEP]
by (simp only: f_Exec_Comp_Stream_Acc_LocalState_def f_shrink_last_def f_Exec_Stream_expand_map_aggregate_append)