[STATEMENT]
lemma f_Exec_Stream_Acc_LocalState_Cons: "
  0 < k \<Longrightarrow>
  f_Exec_Comp_Stream_Acc_LocalState k localState trans_fun (x # xs) c =
  localState (f_Exec_Comp trans_fun (x #  \<NoMsg>\<^bsup>k - Suc 0\<^esup>) c) #
  f_Exec_Comp_Stream_Acc_LocalState k localState 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_LocalState k localState trans_fun (x # xs) c = localState (f_Exec_Comp trans_fun (x # NoMsg\<^bsup>k - Suc 0\<^esup>) c) # f_Exec_Comp_Stream_Acc_LocalState k localState trans_fun xs (f_Exec_Comp trans_fun (x # NoMsg\<^bsup>k - Suc 0\<^esup>) c)
[PROOF STEP]
apply (unfold f_Exec_Comp_Stream_Acc_LocalState_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < k \<Longrightarrow> map localState (f_Exec_Comp_Stream trans_fun ((x # xs) \<odot> k) c) \<div>\<^sub>l k = localState (f_Exec_Comp trans_fun (x # NoMsg\<^bsup>k - Suc 0\<^esup>) c) # map localState (f_Exec_Comp_Stream trans_fun (xs \<odot> k) (f_Exec_Comp trans_fun (x # NoMsg\<^bsup>k - Suc 0\<^esup>) c)) \<div>\<^sub>l k
[PROOF STEP]
apply (simp only: f_shrink_last_map f_expand_Cons append_Cons[symmetric])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < k \<Longrightarrow> map localState (f_Exec_Comp_Stream trans_fun ((x # NoMsg\<^bsup>k - Suc 0\<^esup>) @ xs \<odot> k) c \<div>\<^sub>l k) = localState (f_Exec_Comp trans_fun (x # NoMsg\<^bsup>k - Suc 0\<^esup>) c) # map localState (f_Exec_Comp_Stream trans_fun (xs \<odot> k) (f_Exec_Comp trans_fun (x # NoMsg\<^bsup>k - Suc 0\<^esup>) c) \<div>\<^sub>l k)
[PROOF STEP]
apply (simp add: f_Exec_Stream_append replicate_pred_Cons_length f_shrink_last_Cons del: f_Exec_Stream_Cons append_Cons)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < k \<Longrightarrow> localState (last (f_Exec_Comp_Stream trans_fun (x # NoMsg\<^bsup>k - Suc 0\<^esup>) c)) = localState (f_Exec_Comp trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun x c))
[PROOF STEP]
apply (simp add: f_Exec_eq_f_Exec_Stream_last2[symmetric] f_Exec_Stream_empty_conv)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma f_Exec_Stream_Acc_LocalState_one: "
  0 < k \<Longrightarrow>
  f_Exec_Comp_Stream_Acc_LocalState k localState trans_fun [x] c =
  [localState (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_LocalState k localState trans_fun [x] c = [localState (f_Exec_Comp trans_fun (x # NoMsg\<^bsup>k - Suc 0\<^esup>) c)]
[PROOF STEP]
by (simp add: f_Exec_Stream_Acc_LocalState_Cons)


[STATEMENT]
lemma f_Exec_Stream_Acc_LocalState_snoc: "
  0 < k \<Longrightarrow>
  f_Exec_Comp_Stream_Acc_LocalState k localState trans_fun (xs @ [x]) c =
  f_Exec_Comp_Stream_Acc_LocalState k localState trans_fun xs c @
  [localState (f_Exec_Comp trans_fun ((xs @ [x]) \<odot>\<^sub>f k) c)]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < k \<Longrightarrow> f_Exec_Comp_Stream_Acc_LocalState k localState trans_fun (xs @ [x]) c = f_Exec_Comp_Stream_Acc_LocalState k localState trans_fun xs c @ [localState (f_Exec_Comp trans_fun ((xs @ [x]) \<odot> k) c)]
[PROOF STEP]
by (simp add: f_Exec_Stream_Acc_LocalState_append f_Exec_Stream_Acc_LocalState_Cons f_Exec_append)


[STATEMENT]
lemma i_Exec_Stream_Acc_LocalState_append: "
  i_Exec_Comp_Stream_Acc_LocalState k localState trans_fun (xs \<frown> input) c =
  f_Exec_Comp_Stream_Acc_LocalState k localState trans_fun xs c \<frown>
  i_Exec_Comp_Stream_Acc_LocalState k localState 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_LocalState k localState trans_fun (xs \<frown> input) c = f_Exec_Comp_Stream_Acc_LocalState k localState trans_fun xs c \<frown> i_Exec_Comp_Stream_Acc_LocalState k localState trans_fun input (f_Exec_Comp trans_fun (xs \<odot> k) 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_map_aggregate_append)


[STATEMENT]
lemma i_Exec_Stream_Acc_LocalState_Cons: "
  0 < k \<Longrightarrow>
  i_Exec_Comp_Stream_Acc_LocalState k localState trans_fun ([x] \<frown> input) c =
  [localState (f_Exec_Comp trans_fun (x #  \<NoMsg>\<^bsup>k - Suc 0\<^esup>) c)] \<frown>
  i_Exec_Comp_Stream_Acc_LocalState k localState 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_LocalState k localState trans_fun ([x] \<frown> input) c = [localState (f_Exec_Comp trans_fun (x # NoMsg\<^bsup>k - Suc 0\<^esup>) c)] \<frown> i_Exec_Comp_Stream_Acc_LocalState k localState 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_LocalState_append f_Exec_Stream_Acc_LocalState_one f_expand_one)


[STATEMENT]
lemma f_Exec_Stream_Acc_Output_nth: "
  \<lbrakk> 0 < k; n < length xs \<rbrakk> \<Longrightarrow>
  f_Exec_Comp_Stream_Acc_Output k output_fun trans_fun xs c ! n =
  last_message (map output_fun (
    f_Exec_Comp_Stream trans_fun (xs ! n # \<NoMsg>\<^bsup>k - Suc 0\<^esup>) (
      f_Exec_Comp trans_fun (xs \<down> n \<odot>\<^sub>f k) c)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < k; n < length xs\<rbrakk> \<Longrightarrow> f_Exec_Comp_Stream_Acc_Output k output_fun trans_fun xs c ! n = last_message (map output_fun (f_Exec_Comp_Stream trans_fun (xs ! n # NoMsg\<^bsup>k - Suc 0\<^esup>) (f_Exec_Comp trans_fun (xs \<down> n \<odot> k) c)))
[PROOF STEP]
by (unfold f_Exec_Comp_Stream_Acc_Output_def f_shrink_def, rule f_Exec_Stream_expand_aggregate_map_nth)


[STATEMENT]
lemma f_Exec_Stream_Acc_Output_nth_eq_i_nth: "
  \<lbrakk> 0 < k; n < n' \<rbrakk> \<Longrightarrow>
  f_Exec_Comp_Stream_Acc_Output k output_fun trans_fun (input \<Down> n') c ! n =
  i_Exec_Comp_Stream_Acc_Output k output_fun trans_fun input c n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < k; n < n'\<rbrakk> \<Longrightarrow> f_Exec_Comp_Stream_Acc_Output k output_fun trans_fun (input \<Down> n') c ! n = i_Exec_Comp_Stream_Acc_Output k output_fun trans_fun input c n
[PROOF STEP]
by (unfold f_Exec_Comp_Stream_Acc_Output_def i_Exec_Comp_Stream_Acc_Output_def f_shrink_def i_shrink_def, rule f_Exec_Stream_expand_aggregate_map_nth_eq_i_nth)


[STATEMENT]
lemma i_Exec_Stream_Acc_Output_nth: "
  0 < k \<Longrightarrow>
  i_Exec_Comp_Stream_Acc_Output k output_fun trans_fun input c n =
  last_message (map output_fun (
    f_Exec_Comp_Stream trans_fun (input n # \<NoMsg>\<^bsup>k - Suc 0\<^esup>) (
      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 n = last_message (map output_fun (f_Exec_Comp_Stream trans_fun (input n # NoMsg\<^bsup>k - Suc 0\<^esup>) (f_Exec_Comp trans_fun (input \<Down> n \<odot> k) c)))
[PROOF STEP]
by (unfold i_Exec_Comp_Stream_Acc_Output_def i_shrink_def, rule i_Exec_Stream_expand_aggregate_map_nth)


[STATEMENT]
lemma f_Exec_Stream_Acc_LocalState_nth: "
  \<lbrakk> 0 < k; n < length xs \<rbrakk> \<Longrightarrow>
  f_Exec_Comp_Stream_Acc_LocalState k localState trans_fun xs c ! n =
  localState (f_Exec_Comp trans_fun (xs \<down> Suc n \<odot>\<^sub>f k) c)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < k; n < length xs\<rbrakk> \<Longrightarrow> f_Exec_Comp_Stream_Acc_LocalState k localState trans_fun xs c ! n = localState (f_Exec_Comp trans_fun (xs \<down> Suc n \<odot> k) c)
[PROOF STEP]
apply (simp add: f_Exec_Comp_Stream_Acc_LocalState_def f_shrink_last_map)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < k; n < length xs\<rbrakk> \<Longrightarrow> map localState (f_Exec_Comp_Stream trans_fun (xs \<odot> k) c \<div>\<^sub>l k) ! n = localState (f_Exec_Comp trans_fun (xs \<down> Suc n \<odot> k) c)
[PROOF STEP]
apply (simp add: f_shrink_last_nth' f_shrink_last_length del: mult_Suc)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < k; n < length xs\<rbrakk> \<Longrightarrow> localState (f_Exec_Comp_Stream trans_fun (xs \<odot> k) c ! (Suc n * k - Suc 0)) = localState (f_Exec_Comp trans_fun (xs \<down> Suc n \<odot> k) c)
[PROOF STEP]
apply (simp add: f_Exec_Stream_nth less_imp_Suc_mult_pred_less f_expand_take_mod del: mult_Suc)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma f_Exec_Stream_Acc_LocalState_nth_eq_i_nth: "
  \<lbrakk> 0 < k; n < n' \<rbrakk> \<Longrightarrow>
  f_Exec_Comp_Stream_Acc_LocalState k localState trans_fun (input \<Down> n') c ! n =
  i_Exec_Comp_Stream_Acc_LocalState k localState trans_fun input c n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < k; n < n'\<rbrakk> \<Longrightarrow> f_Exec_Comp_Stream_Acc_LocalState k localState trans_fun (input \<Down> n') c ! n = i_Exec_Comp_Stream_Acc_LocalState k localState trans_fun input c n
[PROOF STEP]
by (unfold f_Exec_Comp_Stream_Acc_LocalState_def i_Exec_Comp_Stream_Acc_LocalState_def f_shrink_last_def i_shrink_last_def, rule f_Exec_Stream_expand_aggregate_map_nth_eq_i_nth)


[STATEMENT]
lemma i_Exec_Stream_Acc_LocalState_nth: "
  0 < k \<Longrightarrow>
  i_Exec_Comp_Stream_Acc_LocalState k localState trans_fun input c n =
  localState (f_Exec_Comp trans_fun (input \<Down> Suc 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 n = localState (f_Exec_Comp trans_fun (input \<Down> Suc n \<odot> k) c)
[PROOF STEP]
by (simp add: i_Exec_Stream_Acc_LocalState_nth_f_nth f_Exec_Stream_Acc_LocalState_nth)


[STATEMENT]
lemma f_Exec_Stream_Acc_Output_causal: "
  xs \<down> n = ys \<down> n \<Longrightarrow>
  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 ys c \<down> n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. xs \<down> n = ys \<down> n \<Longrightarrow> 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 ys c \<down> n
[PROOF STEP]
by (simp add: f_Exec_Stream_Acc_Output_take)


[STATEMENT]
lemma i_Exec_Stream_Acc_Output_causal: "
  input1 \<Down> n = input2 \<Down> n \<Longrightarrow>
  i_Exec_Comp_Stream_Acc_Output k output_fun trans_fun input1 c \<Down> n =
  i_Exec_Comp_Stream_Acc_Output k output_fun trans_fun input2 c \<Down> n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. input1 \<Down> n = input2 \<Down> n \<Longrightarrow> i_Exec_Comp_Stream_Acc_Output k output_fun trans_fun input1 c \<Down> n = i_Exec_Comp_Stream_Acc_Output k output_fun trans_fun input2 c \<Down> n
[PROOF STEP]
apply (case_tac "k = 0")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>input1 \<Down> n = input2 \<Down> n; k = 0\<rbrakk> \<Longrightarrow> i_Exec_Comp_Stream_Acc_Output k output_fun trans_fun input1 c \<Down> n = i_Exec_Comp_Stream_Acc_Output k output_fun trans_fun input2 c \<Down> n
 2. \<lbrakk>input1 \<Down> n = input2 \<Down> n; k \<noteq> 0\<rbrakk> \<Longrightarrow> i_Exec_Comp_Stream_Acc_Output k output_fun trans_fun input1 c \<Down> n = i_Exec_Comp_Stream_Acc_Output k output_fun trans_fun input2 c \<Down> n
[PROOF STEP]
apply (simp add: i_Exec_Comp_Stream_Acc_Output_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>input1 \<Down> n = input2 \<Down> n; k \<noteq> 0\<rbrakk> \<Longrightarrow> i_Exec_Comp_Stream_Acc_Output k output_fun trans_fun input1 c \<Down> n = i_Exec_Comp_Stream_Acc_Output k output_fun trans_fun input2 c \<Down> n
[PROOF STEP]
apply (simp add: i_Exec_Stream_Acc_Output_take)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma f_Exec_Stream_Acc_Output_Connected_strictly_causal: "
  \<lbrakk> xs \<down> n = ys \<down> n;
    f_Streams_Connected
      (f_Exec_Comp_Stream_Acc_Output k output_fun trans_fun xs c)
      channel1;
    f_Streams_Connected
      (f_Exec_Comp_Stream_Acc_Output k output_fun 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 (f_Exec_Comp_Stream_Acc_Output k output_fun trans_fun xs c) channel1; f_Streams_Connected (f_Exec_Comp_Stream_Acc_Output k output_fun trans_fun ys c) channel2\<rbrakk> \<Longrightarrow> channel1 \<down> Suc n = channel2 \<down> Suc n
[PROOF STEP]
by (simp add: f_Streams_Connected_def f_Exec_Stream_Acc_Output_take)


[STATEMENT]
lemma i_Exec_Stream_Acc_Output_Connected_strictly_causal: "
  \<lbrakk> input1 \<Down> n = input2 \<Down> n;
    i_Streams_Connected
      (i_Exec_Comp_Stream_Acc_Output k output_fun trans_fun input1 c)
      channel1;
    i_Streams_Connected
      (i_Exec_Comp_Stream_Acc_Output k output_fun 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 (i_Exec_Comp_Stream_Acc_Output k output_fun trans_fun input1 c) channel1; i_Streams_Connected (i_Exec_Comp_Stream_Acc_Output k output_fun trans_fun input2 c) channel2\<rbrakk> \<Longrightarrow> channel1 \<Down> Suc n = channel2 \<Down> Suc n
[PROOF STEP]
apply (unfold i_Streams_Connected_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>input1 \<Down> n = input2 \<Down> n; channel1 = [NoMsg] \<frown> i_Exec_Comp_Stream_Acc_Output k output_fun trans_fun input1 c; channel2 = [NoMsg] \<frown> i_Exec_Comp_Stream_Acc_Output k output_fun trans_fun input2 c\<rbrakk> \<Longrightarrow> channel1 \<Down> Suc n = channel2 \<Down> Suc n
[PROOF STEP]
apply (case_tac "k = 0")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>input1 \<Down> n = input2 \<Down> n; channel1 = [NoMsg] \<frown> i_Exec_Comp_Stream_Acc_Output k output_fun trans_fun input1 c; channel2 = [NoMsg] \<frown> i_Exec_Comp_Stream_Acc_Output k output_fun trans_fun input2 c; k = 0\<rbrakk> \<Longrightarrow> channel1 \<Down> Suc n = channel2 \<Down> Suc n
 2. \<lbrakk>input1 \<Down> n = input2 \<Down> n; channel1 = [NoMsg] \<frown> i_Exec_Comp_Stream_Acc_Output k output_fun trans_fun input1 c; channel2 = [NoMsg] \<frown> i_Exec_Comp_Stream_Acc_Output k output_fun trans_fun input2 c; k \<noteq> 0\<rbrakk> \<Longrightarrow> channel1 \<Down> Suc n = channel2 \<Down> Suc n
[PROOF STEP]
apply (simp add: i_Exec_Comp_Stream_Acc_Output_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>input1 \<Down> n = input2 \<Down> n; channel1 = [NoMsg] \<frown> i_Exec_Comp_Stream_Acc_Output k output_fun trans_fun input1 c; channel2 = [NoMsg] \<frown> i_Exec_Comp_Stream_Acc_Output k output_fun trans_fun input2 c; k \<noteq> 0\<rbrakk> \<Longrightarrow> channel1 \<Down> Suc n = channel2 \<Down> Suc n
[PROOF STEP]
apply (simp add: i_Exec_Stream_Acc_Output_take)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma Deterministic_trans_fun_imp_acc_trans_fun:
  "Deterministic_Trans_Fun trans_fun localState \<Longrightarrow>
    Deterministic_Trans_Fun (Acc_Trans_Fun_Step k trans_fun pointwise_shrink) localState"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Deterministic_Trans_Fun trans_fun localState \<Longrightarrow> Deterministic_Trans_Fun (Acc_Trans_Fun_Step k trans_fun pointwise_shrink) localState
[PROOF STEP]
apply (simp (no_asm) only: Deterministic_Trans_Fun_def Acc_Trans_Fun_Step_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Deterministic_Trans_Fun trans_fun localState \<Longrightarrow> \<forall>c1 c2 x. localState c1 = localState c2 \<longrightarrow> pointwise_shrink (f_Exec_Comp_Stream trans_fun (x # NoMsg\<^bsup>k - Suc 0\<^esup>) c1) = pointwise_shrink (f_Exec_Comp_Stream trans_fun (x # NoMsg\<^bsup>k - Suc 0\<^esup>) c2)
[PROOF STEP]
apply clarify
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>c1 c2 x. \<lbrakk>Deterministic_Trans_Fun trans_fun localState; localState c1 = localState c2\<rbrakk> \<Longrightarrow> pointwise_shrink (f_Exec_Comp_Stream trans_fun (x # NoMsg\<^bsup>k - Suc 0\<^esup>) c1) = pointwise_shrink (f_Exec_Comp_Stream trans_fun (x # NoMsg\<^bsup>k - Suc 0\<^esup>) c2)
[PROOF STEP]
apply (subst Deterministic_f_Exec_Stream, simp+)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma is_Pointwise_Output_Shrink_list_imp_is_Pointwise_Output_Shrink:
  "\<lbrakk> is_Pointwise_Output_Shrink_list pointwise_shrink fs; output_fun \<in> set fs \<rbrakk> \<Longrightarrow>
    is_Pointwise_Output_Shrink pointwise_shrink output_fun"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_Pointwise_Output_Shrink_list pointwise_shrink fs; output_fun \<in> set fs\<rbrakk> \<Longrightarrow> is_Pointwise_Output_Shrink pointwise_shrink output_fun
[PROOF STEP]
apply (induct fs, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a fs. \<lbrakk>\<lbrakk>is_Pointwise_Output_Shrink_list pointwise_shrink fs; output_fun \<in> set fs\<rbrakk> \<Longrightarrow> is_Pointwise_Output_Shrink pointwise_shrink output_fun; is_Pointwise_Output_Shrink_list pointwise_shrink (a # fs); output_fun \<in> set (a # fs)\<rbrakk> \<Longrightarrow> is_Pointwise_Output_Shrink pointwise_shrink output_fun
[PROOF STEP]
apply fastforce
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma is_Pointwise_Output_Shrink_list_eq_is_Pointwise_Output_Shrink_all:
  "(is_Pointwise_Output_Shrink_list pointwise_shrink fs) =
    (\<forall>output_fun \<in> set fs. is_Pointwise_Output_Shrink pointwise_shrink output_fun)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_Pointwise_Output_Shrink_list pointwise_shrink fs = (\<forall>output_fun\<in>set fs. is_Pointwise_Output_Shrink pointwise_shrink output_fun)
[PROOF STEP]
apply (rule iffI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. is_Pointwise_Output_Shrink_list pointwise_shrink fs \<Longrightarrow> \<forall>output_fun\<in>set fs. is_Pointwise_Output_Shrink pointwise_shrink output_fun
 2. \<forall>output_fun\<in>set fs. is_Pointwise_Output_Shrink pointwise_shrink output_fun \<Longrightarrow> is_Pointwise_Output_Shrink_list pointwise_shrink fs
[PROOF STEP]
apply (rule ballI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>output_fun. \<lbrakk>is_Pointwise_Output_Shrink_list pointwise_shrink fs; output_fun \<in> set fs\<rbrakk> \<Longrightarrow> is_Pointwise_Output_Shrink pointwise_shrink output_fun
 2. \<forall>output_fun\<in>set fs. is_Pointwise_Output_Shrink pointwise_shrink output_fun \<Longrightarrow> is_Pointwise_Output_Shrink_list pointwise_shrink fs
[PROOF STEP]
apply (rule is_Pointwise_Output_Shrink_list_imp_is_Pointwise_Output_Shrink)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>output_fun. \<lbrakk>is_Pointwise_Output_Shrink_list pointwise_shrink fs; output_fun \<in> set fs\<rbrakk> \<Longrightarrow> is_Pointwise_Output_Shrink_list pointwise_shrink (?fs5 output_fun)
 2. \<And>output_fun. \<lbrakk>is_Pointwise_Output_Shrink_list pointwise_shrink fs; output_fun \<in> set fs\<rbrakk> \<Longrightarrow> output_fun \<in> set (?fs5 output_fun)
 3. \<forall>output_fun\<in>set fs. is_Pointwise_Output_Shrink pointwise_shrink output_fun \<Longrightarrow> is_Pointwise_Output_Shrink_list pointwise_shrink fs
[PROOF STEP]
apply (simp add: member_def)+
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>output_fun\<in>set fs. is_Pointwise_Output_Shrink pointwise_shrink output_fun \<Longrightarrow> is_Pointwise_Output_Shrink_list pointwise_shrink fs
[PROOF STEP]
apply (induct fs, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a fs. \<lbrakk>Ball (set fs) (is_Pointwise_Output_Shrink pointwise_shrink) \<Longrightarrow> is_Pointwise_Output_Shrink_list pointwise_shrink fs; Ball (set (a # fs)) (is_Pointwise_Output_Shrink pointwise_shrink)\<rbrakk> \<Longrightarrow> is_Pointwise_Output_Shrink_list pointwise_shrink (a # fs)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma is_Pointwise_Output_Shrink_subset:
  "\<lbrakk> is_Pointwise_Output_Shrink_list pointwise_shrink fs; set fs' \<subseteq> set fs \<rbrakk> \<Longrightarrow>
    is_Pointwise_Output_Shrink_list pointwise_shrink fs'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_Pointwise_Output_Shrink_list pointwise_shrink fs; set fs' \<subseteq> set fs\<rbrakk> \<Longrightarrow> is_Pointwise_Output_Shrink_list pointwise_shrink fs'
[PROOF STEP]
by (fastforce simp: is_Pointwise_Output_Shrink_list_eq_is_Pointwise_Output_Shrink_all)


[STATEMENT]
lemma f_Exec_Stream_Acc_LocalState_eq_Acc_Trans_Fun_Step_LocalState: "\<And>c.
  \<lbrakk> 0 < k;
    Deterministic_Trans_Fun trans_fun localState;
    is_correct_localState_Pointwise_Output_Shrink pointwise_shrink localState \<rbrakk> \<Longrightarrow>
  f_Exec_Comp_Stream_Acc_LocalState k localState trans_fun xs c =
  map localState (f_Exec_Comp_Stream (Acc_Trans_Fun_Step k trans_fun pointwise_shrink) xs c)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>c. \<lbrakk>0 < k; Deterministic_Trans_Fun trans_fun localState; is_correct_localState_Pointwise_Output_Shrink pointwise_shrink localState\<rbrakk> \<Longrightarrow> f_Exec_Comp_Stream_Acc_LocalState k localState trans_fun xs c = map localState (f_Exec_Comp_Stream (Acc_Trans_Fun_Step k trans_fun pointwise_shrink) xs c)
[PROOF STEP]
apply (drule Deterministic_trans_fun_imp_acc_trans_fun[of trans_fun localState k pointwise_shrink])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>c. \<lbrakk>0 < k; is_correct_localState_Pointwise_Output_Shrink pointwise_shrink localState; Deterministic_Trans_Fun (Acc_Trans_Fun_Step k trans_fun pointwise_shrink) localState\<rbrakk> \<Longrightarrow> f_Exec_Comp_Stream_Acc_LocalState k localState trans_fun xs c = map localState (f_Exec_Comp_Stream (Acc_Trans_Fun_Step k trans_fun pointwise_shrink) xs c)
[PROOF STEP]
apply (clarsimp simp: list_eq_iff)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>c i. \<lbrakk>0 < k; is_correct_localState_Pointwise_Output_Shrink pointwise_shrink localState; Deterministic_Trans_Fun (Acc_Trans_Fun_Step k trans_fun pointwise_shrink) localState; i < length xs\<rbrakk> \<Longrightarrow> f_Exec_Comp_Stream_Acc_LocalState k localState trans_fun xs c ! i = localState (f_Exec_Comp_Stream (Acc_Trans_Fun_Step k trans_fun pointwise_shrink) xs c ! i)
[PROOF STEP]
apply (simp add: f_Exec_Stream_Acc_LocalState_nth f_Exec_Stream_nth)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>c i. \<lbrakk>0 < k; is_correct_localState_Pointwise_Output_Shrink pointwise_shrink localState; Deterministic_Trans_Fun (Acc_Trans_Fun_Step k trans_fun pointwise_shrink) localState; i < length xs\<rbrakk> \<Longrightarrow> localState (f_Exec_Comp trans_fun (xs \<down> Suc i \<odot> k) c) = localState (f_Exec_Comp (Acc_Trans_Fun_Step k trans_fun pointwise_shrink) (xs \<down> Suc i) c)
[PROOF STEP]
apply (induct xs, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a xs c i. \<lbrakk>\<And>c i. \<lbrakk>0 < k; is_correct_localState_Pointwise_Output_Shrink pointwise_shrink localState; Deterministic_Trans_Fun (Acc_Trans_Fun_Step k trans_fun pointwise_shrink) localState; i < length xs\<rbrakk> \<Longrightarrow> localState (f_Exec_Comp trans_fun (xs \<down> Suc i \<odot> k) c) = localState (f_Exec_Comp (Acc_Trans_Fun_Step k trans_fun pointwise_shrink) (xs \<down> Suc i) c); 0 < k; is_correct_localState_Pointwise_Output_Shrink pointwise_shrink localState; Deterministic_Trans_Fun (Acc_Trans_Fun_Step k trans_fun pointwise_shrink) localState; i < length (a # xs)\<rbrakk> \<Longrightarrow> localState (f_Exec_Comp trans_fun ((a # xs) \<down> Suc i \<odot> k) c) = localState (f_Exec_Comp (Acc_Trans_Fun_Step k trans_fun pointwise_shrink) ((a # xs) \<down> Suc i) c)
[PROOF STEP]
apply (rename_tac x xs c i)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x xs c i. \<lbrakk>\<And>c i. \<lbrakk>0 < k; is_correct_localState_Pointwise_Output_Shrink pointwise_shrink localState; Deterministic_Trans_Fun (Acc_Trans_Fun_Step k trans_fun pointwise_shrink) localState; i < length xs\<rbrakk> \<Longrightarrow> localState (f_Exec_Comp trans_fun (xs \<down> Suc i \<odot> k) c) = localState (f_Exec_Comp (Acc_Trans_Fun_Step k trans_fun pointwise_shrink) (xs \<down> Suc i) c); 0 < k; is_correct_localState_Pointwise_Output_Shrink pointwise_shrink localState; Deterministic_Trans_Fun (Acc_Trans_Fun_Step k trans_fun pointwise_shrink) localState; i < length (x # xs)\<rbrakk> \<Longrightarrow> localState (f_Exec_Comp trans_fun ((x # xs) \<down> Suc i \<odot> k) c) = localState (f_Exec_Comp (Acc_Trans_Fun_Step k trans_fun pointwise_shrink) ((x # xs) \<down> Suc i) c)
[PROOF STEP]
apply (simp add: Acc_Trans_Fun_Step_def f_expand_Cons f_Exec_append)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x xs c i. \<lbrakk>\<And>c i. i < length xs \<Longrightarrow> localState (f_Exec_Comp trans_fun (xs \<down> Suc i \<odot> k) c) = localState (f_Exec_Comp (Acc_Trans_Fun_Step k trans_fun pointwise_shrink) (xs \<down> Suc i) c); 0 < k; is_correct_localState_Pointwise_Output_Shrink pointwise_shrink localState; Deterministic_Trans_Fun (Acc_Trans_Fun_Step k trans_fun pointwise_shrink) localState; i < Suc (length xs)\<rbrakk> \<Longrightarrow> localState (f_Exec_Comp trans_fun (xs \<down> i \<odot> k) (f_Exec_Comp trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun x c))) = localState (f_Exec_Comp (Acc_Trans_Fun_Step k trans_fun pointwise_shrink) (xs \<down> i) (pointwise_shrink (trans_fun x c # f_Exec_Comp_Stream trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun x c))))
[PROOF STEP]
apply (case_tac i)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x xs c i. \<lbrakk>\<And>c i. i < length xs \<Longrightarrow> localState (f_Exec_Comp trans_fun (xs \<down> Suc i \<odot> k) c) = localState (f_Exec_Comp (Acc_Trans_Fun_Step k trans_fun pointwise_shrink) (xs \<down> Suc i) c); 0 < k; is_correct_localState_Pointwise_Output_Shrink pointwise_shrink localState; Deterministic_Trans_Fun (Acc_Trans_Fun_Step k trans_fun pointwise_shrink) localState; i < Suc (length xs); i = 0\<rbrakk> \<Longrightarrow> localState (f_Exec_Comp trans_fun (xs \<down> i \<odot> k) (f_Exec_Comp trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun x c))) = localState (f_Exec_Comp (Acc_Trans_Fun_Step k trans_fun pointwise_shrink) (xs \<down> i) (pointwise_shrink (trans_fun x c # f_Exec_Comp_Stream trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun x c))))
 2. \<And>x xs c i nat. \<lbrakk>\<And>c i. i < length xs \<Longrightarrow> localState (f_Exec_Comp trans_fun (xs \<down> Suc i \<odot> k) c) = localState (f_Exec_Comp (Acc_Trans_Fun_Step k trans_fun pointwise_shrink) (xs \<down> Suc i) c); 0 < k; is_correct_localState_Pointwise_Output_Shrink pointwise_shrink localState; Deterministic_Trans_Fun (Acc_Trans_Fun_Step k trans_fun pointwise_shrink) localState; i < Suc (length xs); i = Suc nat\<rbrakk> \<Longrightarrow> localState (f_Exec_Comp trans_fun (xs \<down> i \<odot> k) (f_Exec_Comp trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun x c))) = localState (f_Exec_Comp (Acc_Trans_Fun_Step k trans_fun pointwise_shrink) (xs \<down> i) (pointwise_shrink (trans_fun x c # f_Exec_Comp_Stream trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun x c))))
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x xs c i. \<lbrakk>\<And>c i. i < length xs \<Longrightarrow> localState (f_Exec_Comp trans_fun (xs \<down> Suc i \<odot> k) c) = localState (f_Exec_Comp (Acc_Trans_Fun_Step k trans_fun pointwise_shrink) (xs \<down> Suc i) c); 0 < k; is_correct_localState_Pointwise_Output_Shrink pointwise_shrink localState; Deterministic_Trans_Fun (Acc_Trans_Fun_Step k trans_fun pointwise_shrink) localState; i = 0\<rbrakk> \<Longrightarrow> localState (f_Exec_Comp trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun x c)) = localState (pointwise_shrink (trans_fun x c # f_Exec_Comp_Stream trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun x c)))
 2. \<And>x xs c i nat. \<lbrakk>\<And>c i. i < length xs \<Longrightarrow> localState (f_Exec_Comp trans_fun (xs \<down> Suc i \<odot> k) c) = localState (f_Exec_Comp (Acc_Trans_Fun_Step k trans_fun pointwise_shrink) (xs \<down> Suc i) c); 0 < k; is_correct_localState_Pointwise_Output_Shrink pointwise_shrink localState; Deterministic_Trans_Fun (Acc_Trans_Fun_Step k trans_fun pointwise_shrink) localState; i < Suc (length xs); i = Suc nat\<rbrakk> \<Longrightarrow> localState (f_Exec_Comp trans_fun (xs \<down> i \<odot> k) (f_Exec_Comp trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun x c))) = localState (f_Exec_Comp (Acc_Trans_Fun_Step k trans_fun pointwise_shrink) (xs \<down> i) (pointwise_shrink (trans_fun x c # f_Exec_Comp_Stream trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun x c))))
[PROOF STEP]
apply (simp only: is_correct_localState_Pointwise_Output_Shrink_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x xs c i. \<lbrakk>\<And>c i. i < length xs \<Longrightarrow> localState (f_Exec_Comp trans_fun (xs \<down> Suc i \<odot> k) c) = localState (f_Exec_Comp (Acc_Trans_Fun_Step k trans_fun pointwise_shrink) (xs \<down> Suc i) c); 0 < k; \<forall>cs. cs \<noteq> [] \<longrightarrow> localState (pointwise_shrink cs) = localState (last cs); Deterministic_Trans_Fun (Acc_Trans_Fun_Step k trans_fun pointwise_shrink) localState; i = 0\<rbrakk> \<Longrightarrow> localState (f_Exec_Comp trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun x c)) = localState (pointwise_shrink (trans_fun x c # f_Exec_Comp_Stream trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun x c)))
 2. \<And>x xs c i nat. \<lbrakk>\<And>c i. i < length xs \<Longrightarrow> localState (f_Exec_Comp trans_fun (xs \<down> Suc i \<odot> k) c) = localState (f_Exec_Comp (Acc_Trans_Fun_Step k trans_fun pointwise_shrink) (xs \<down> Suc i) c); 0 < k; is_correct_localState_Pointwise_Output_Shrink pointwise_shrink localState; Deterministic_Trans_Fun (Acc_Trans_Fun_Step k trans_fun pointwise_shrink) localState; i < Suc (length xs); i = Suc nat\<rbrakk> \<Longrightarrow> localState (f_Exec_Comp trans_fun (xs \<down> i \<odot> k) (f_Exec_Comp trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun x c))) = localState (f_Exec_Comp (Acc_Trans_Fun_Step k trans_fun pointwise_shrink) (xs \<down> i) (pointwise_shrink (trans_fun x c # f_Exec_Comp_Stream trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun x c))))
[PROOF STEP]
apply (drule_tac x="f_Exec_Comp_Stream trans_fun (x # NoMsg\<^bsup>k - Suc 0\<^esup>) c" in spec)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x xs c i. \<lbrakk>\<And>c i. i < length xs \<Longrightarrow> localState (f_Exec_Comp trans_fun (xs \<down> Suc i \<odot> k) c) = localState (f_Exec_Comp (Acc_Trans_Fun_Step k trans_fun pointwise_shrink) (xs \<down> Suc i) c); 0 < k; Deterministic_Trans_Fun (Acc_Trans_Fun_Step k trans_fun pointwise_shrink) localState; i = 0; f_Exec_Comp_Stream trans_fun (x # NoMsg\<^bsup>k - Suc 0\<^esup>) c \<noteq> [] \<longrightarrow> localState (pointwise_shrink (f_Exec_Comp_Stream trans_fun (x # NoMsg\<^bsup>k - Suc 0\<^esup>) c)) = localState (last (f_Exec_Comp_Stream trans_fun (x # NoMsg\<^bsup>k - Suc 0\<^esup>) c))\<rbrakk> \<Longrightarrow> localState (f_Exec_Comp trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun x c)) = localState (pointwise_shrink (trans_fun x c # f_Exec_Comp_Stream trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun x c)))
 2. \<And>x xs c i nat. \<lbrakk>\<And>c i. i < length xs \<Longrightarrow> localState (f_Exec_Comp trans_fun (xs \<down> Suc i \<odot> k) c) = localState (f_Exec_Comp (Acc_Trans_Fun_Step k trans_fun pointwise_shrink) (xs \<down> Suc i) c); 0 < k; is_correct_localState_Pointwise_Output_Shrink pointwise_shrink localState; Deterministic_Trans_Fun (Acc_Trans_Fun_Step k trans_fun pointwise_shrink) localState; i < Suc (length xs); i = Suc nat\<rbrakk> \<Longrightarrow> localState (f_Exec_Comp trans_fun (xs \<down> i \<odot> k) (f_Exec_Comp trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun x c))) = localState (f_Exec_Comp (Acc_Trans_Fun_Step k trans_fun pointwise_shrink) (xs \<down> i) (pointwise_shrink (trans_fun x c # f_Exec_Comp_Stream trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun x c))))
[PROOF STEP]
apply (simp add: f_Exec_Stream_not_empty_conv f_Exec_eq_f_Exec_Stream_last)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x xs c i nat. \<lbrakk>\<And>c i. i < length xs \<Longrightarrow> localState (f_Exec_Comp trans_fun (xs \<down> Suc i \<odot> k) c) = localState (f_Exec_Comp (Acc_Trans_Fun_Step k trans_fun pointwise_shrink) (xs \<down> Suc i) c); 0 < k; is_correct_localState_Pointwise_Output_Shrink pointwise_shrink localState; Deterministic_Trans_Fun (Acc_Trans_Fun_Step k trans_fun pointwise_shrink) localState; i < Suc (length xs); i = Suc nat\<rbrakk> \<Longrightarrow> localState (f_Exec_Comp trans_fun (xs \<down> i \<odot> k) (f_Exec_Comp trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun x c))) = localState (f_Exec_Comp (Acc_Trans_Fun_Step k trans_fun pointwise_shrink) (xs \<down> i) (pointwise_shrink (trans_fun x c # f_Exec_Comp_Stream trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun x c))))
[PROOF STEP]
apply (rename_tac i2)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x xs c i i2. \<lbrakk>\<And>c i. i < length xs \<Longrightarrow> localState (f_Exec_Comp trans_fun (xs \<down> Suc i \<odot> k) c) = localState (f_Exec_Comp (Acc_Trans_Fun_Step k trans_fun pointwise_shrink) (xs \<down> Suc i) c); 0 < k; is_correct_localState_Pointwise_Output_Shrink pointwise_shrink localState; Deterministic_Trans_Fun (Acc_Trans_Fun_Step k trans_fun pointwise_shrink) localState; i < Suc (length xs); i = Suc i2\<rbrakk> \<Longrightarrow> localState (f_Exec_Comp trans_fun (xs \<down> i \<odot> k) (f_Exec_Comp trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun x c))) = localState (f_Exec_Comp (Acc_Trans_Fun_Step k trans_fun pointwise_shrink) (xs \<down> i) (pointwise_shrink (trans_fun x c # f_Exec_Comp_Stream trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun x c))))
[PROOF STEP]
apply (drule_tac x="f_Exec_Comp trans_fun \<NoMsg>\<^bsup>k - Suc 0\<^esup> (trans_fun x c)" in meta_spec)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x xs c i i2. \<lbrakk>0 < k; is_correct_localState_Pointwise_Output_Shrink pointwise_shrink localState; Deterministic_Trans_Fun (Acc_Trans_Fun_Step k trans_fun pointwise_shrink) localState; i < Suc (length xs); i = Suc i2; \<And>i. i < length xs \<Longrightarrow> localState (f_Exec_Comp trans_fun (xs \<down> Suc i \<odot> k) (f_Exec_Comp trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun x c))) = localState (f_Exec_Comp (Acc_Trans_Fun_Step k trans_fun pointwise_shrink) (xs \<down> Suc i) (f_Exec_Comp trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun x c)))\<rbrakk> \<Longrightarrow> localState (f_Exec_Comp trans_fun (xs \<down> i \<odot> k) (f_Exec_Comp trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun x c))) = localState (f_Exec_Comp (Acc_Trans_Fun_Step k trans_fun pointwise_shrink) (xs \<down> i) (pointwise_shrink (trans_fun x c # f_Exec_Comp_Stream trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun x c))))
[PROOF STEP]
apply (drule_tac x=i2 in meta_spec)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x xs c i i2. \<lbrakk>0 < k; is_correct_localState_Pointwise_Output_Shrink pointwise_shrink localState; Deterministic_Trans_Fun (Acc_Trans_Fun_Step k trans_fun pointwise_shrink) localState; i < Suc (length xs); i = Suc i2; i2 < length xs \<Longrightarrow> localState (f_Exec_Comp trans_fun (xs \<down> Suc i2 \<odot> k) (f_Exec_Comp trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun x c))) = localState (f_Exec_Comp (Acc_Trans_Fun_Step k trans_fun pointwise_shrink) (xs \<down> Suc i2) (f_Exec_Comp trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun x c)))\<rbrakk> \<Longrightarrow> localState (f_Exec_Comp trans_fun (xs \<down> i \<odot> k) (f_Exec_Comp trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun x c))) = localState (f_Exec_Comp (Acc_Trans_Fun_Step k trans_fun pointwise_shrink) (xs \<down> i) (pointwise_shrink (trans_fun x c # f_Exec_Comp_Stream trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun x c))))
[PROOF STEP]
apply (simp add: is_correct_localState_Pointwise_Output_Shrink_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x xs c i i2. \<lbrakk>0 < k; \<forall>cs. cs \<noteq> [] \<longrightarrow> localState (pointwise_shrink cs) = localState (last cs); Deterministic_Trans_Fun (Acc_Trans_Fun_Step k trans_fun pointwise_shrink) localState; i2 < length xs; i = Suc i2; localState (f_Exec_Comp trans_fun (xs \<down> Suc i2 \<odot> k) (f_Exec_Comp trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun x c))) = localState (f_Exec_Comp (Acc_Trans_Fun_Step k trans_fun pointwise_shrink) (xs \<down> Suc i2) (f_Exec_Comp trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun x c)))\<rbrakk> \<Longrightarrow> localState (f_Exec_Comp (Acc_Trans_Fun_Step k trans_fun pointwise_shrink) (xs \<down> Suc i2) (f_Exec_Comp trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun x c))) = localState (f_Exec_Comp (Acc_Trans_Fun_Step k trans_fun pointwise_shrink) (xs \<down> Suc i2) (pointwise_shrink (trans_fun x c # f_Exec_Comp_Stream trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun x c))))
[PROOF STEP]
apply (drule_tac x="f_Exec_Comp_Stream trans_fun (x # NoMsg\<^bsup>k - Suc 0\<^esup>) c" in spec)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x xs c i i2. \<lbrakk>0 < k; Deterministic_Trans_Fun (Acc_Trans_Fun_Step k trans_fun pointwise_shrink) localState; i2 < length xs; i = Suc i2; localState (f_Exec_Comp trans_fun (xs \<down> Suc i2 \<odot> k) (f_Exec_Comp trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun x c))) = localState (f_Exec_Comp (Acc_Trans_Fun_Step k trans_fun pointwise_shrink) (xs \<down> Suc i2) (f_Exec_Comp trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun x c))); f_Exec_Comp_Stream trans_fun (x # NoMsg\<^bsup>k - Suc 0\<^esup>) c \<noteq> [] \<longrightarrow> localState (pointwise_shrink (f_Exec_Comp_Stream trans_fun (x # NoMsg\<^bsup>k - Suc 0\<^esup>) c)) = localState (last (f_Exec_Comp_Stream trans_fun (x # NoMsg\<^bsup>k - Suc 0\<^esup>) c))\<rbrakk> \<Longrightarrow> localState (f_Exec_Comp (Acc_Trans_Fun_Step k trans_fun pointwise_shrink) (xs \<down> Suc i2) (f_Exec_Comp trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun x c))) = localState (f_Exec_Comp (Acc_Trans_Fun_Step k trans_fun pointwise_shrink) (xs \<down> Suc i2) (pointwise_shrink (trans_fun x c # f_Exec_Comp_Stream trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun x c))))
[PROOF STEP]
apply (simp add: f_Exec_Stream_not_empty_conv)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x xs c i i2. \<lbrakk>0 < k; Deterministic_Trans_Fun (Acc_Trans_Fun_Step k trans_fun pointwise_shrink) localState; i2 < length xs; i = Suc i2; localState (f_Exec_Comp trans_fun (xs \<down> Suc i2 \<odot> k) (f_Exec_Comp trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun x c))) = localState (f_Exec_Comp (Acc_Trans_Fun_Step k trans_fun pointwise_shrink) (xs \<down> Suc i2) (f_Exec_Comp trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun x c))); localState (pointwise_shrink (trans_fun x c # f_Exec_Comp_Stream trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun x c))) = localState (if f_Exec_Comp_Stream trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun x c) = [] then trans_fun x c else last (f_Exec_Comp_Stream trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun x c)))\<rbrakk> \<Longrightarrow> localState (f_Exec_Comp (Acc_Trans_Fun_Step k trans_fun pointwise_shrink) (xs \<down> Suc i2) (f_Exec_Comp trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun x c))) = localState (f_Exec_Comp (Acc_Trans_Fun_Step k trans_fun pointwise_shrink) (xs \<down> Suc i2) (pointwise_shrink (trans_fun x c # f_Exec_Comp_Stream trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun x c))))
[PROOF STEP]
apply (rule arg_cong[where f=localState])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x xs c i i2. \<lbrakk>0 < k; Deterministic_Trans_Fun (Acc_Trans_Fun_Step k trans_fun pointwise_shrink) localState; i2 < length xs; i = Suc i2; localState (f_Exec_Comp trans_fun (xs \<down> Suc i2 \<odot> k) (f_Exec_Comp trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun x c))) = localState (f_Exec_Comp (Acc_Trans_Fun_Step k trans_fun pointwise_shrink) (xs \<down> Suc i2) (f_Exec_Comp trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun x c))); localState (pointwise_shrink (trans_fun x c # f_Exec_Comp_Stream trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun x c))) = localState (if f_Exec_Comp_Stream trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun x c) = [] then trans_fun x c else last (f_Exec_Comp_Stream trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun x c)))\<rbrakk> \<Longrightarrow> f_Exec_Comp (Acc_Trans_Fun_Step k trans_fun pointwise_shrink) (xs \<down> Suc i2) (f_Exec_Comp trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun x c)) = f_Exec_Comp (Acc_Trans_Fun_Step k trans_fun pointwise_shrink) (xs \<down> Suc i2) (pointwise_shrink (trans_fun x c # f_Exec_Comp_Stream trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun x c)))
[PROOF STEP]
apply (rule Deterministic_f_Exec)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x xs c i i2. \<lbrakk>0 < k; Deterministic_Trans_Fun (Acc_Trans_Fun_Step k trans_fun pointwise_shrink) localState; i2 < length xs; i = Suc i2; localState (f_Exec_Comp trans_fun (xs \<down> Suc i2 \<odot> k) (f_Exec_Comp trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun x c))) = localState (f_Exec_Comp (Acc_Trans_Fun_Step k trans_fun pointwise_shrink) (xs \<down> Suc i2) (f_Exec_Comp trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun x c))); localState (pointwise_shrink (trans_fun x c # f_Exec_Comp_Stream trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun x c))) = localState (if f_Exec_Comp_Stream trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun x c) = [] then trans_fun x c else last (f_Exec_Comp_Stream trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun x c)))\<rbrakk> \<Longrightarrow> Deterministic_Trans_Fun (Acc_Trans_Fun_Step k trans_fun pointwise_shrink) (?localState13 x xs c i i2)
 2. \<And>x xs c i i2. \<lbrakk>0 < k; Deterministic_Trans_Fun (Acc_Trans_Fun_Step k trans_fun pointwise_shrink) localState; i2 < length xs; i = Suc i2; localState (f_Exec_Comp trans_fun (xs \<down> Suc i2 \<odot> k) (f_Exec_Comp trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun x c))) = localState (f_Exec_Comp (Acc_Trans_Fun_Step k trans_fun pointwise_shrink) (xs \<down> Suc i2) (f_Exec_Comp trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun x c))); localState (pointwise_shrink (trans_fun x c # f_Exec_Comp_Stream trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun x c))) = localState (if f_Exec_Comp_Stream trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun x c) = [] then trans_fun x c else last (f_Exec_Comp_Stream trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun x c)))\<rbrakk> \<Longrightarrow> ?localState13 x xs c i i2 (f_Exec_Comp trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun x c)) = ?localState13 x xs c i i2 (pointwise_shrink (trans_fun x c # f_Exec_Comp_Stream trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun x c)))
 3. \<And>x xs c i i2. \<lbrakk>0 < k; Deterministic_Trans_Fun (Acc_Trans_Fun_Step k trans_fun pointwise_shrink) localState; i2 < length xs; i = Suc i2; localState (f_Exec_Comp trans_fun (xs \<down> Suc i2 \<odot> k) (f_Exec_Comp trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun x c))) = localState (f_Exec_Comp (Acc_Trans_Fun_Step k trans_fun pointwise_shrink) (xs \<down> Suc i2) (f_Exec_Comp trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun x c))); localState (pointwise_shrink (trans_fun x c # f_Exec_Comp_Stream trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun x c))) = localState (if f_Exec_Comp_Stream trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun x c) = [] then trans_fun x c else last (f_Exec_Comp_Stream trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun x c)))\<rbrakk> \<Longrightarrow> xs \<down> Suc i2 \<noteq> []
[PROOF STEP]
apply assumption
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x xs c i i2. \<lbrakk>0 < k; Deterministic_Trans_Fun (Acc_Trans_Fun_Step k trans_fun pointwise_shrink) localState; i2 < length xs; i = Suc i2; localState (f_Exec_Comp trans_fun (xs \<down> Suc i2 \<odot> k) (f_Exec_Comp trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun x c))) = localState (f_Exec_Comp (Acc_Trans_Fun_Step k trans_fun pointwise_shrink) (xs \<down> Suc i2) (f_Exec_Comp trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun x c))); localState (pointwise_shrink (trans_fun x c # f_Exec_Comp_Stream trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun x c))) = localState (if f_Exec_Comp_Stream trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun x c) = [] then trans_fun x c else last (f_Exec_Comp_Stream trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun x c)))\<rbrakk> \<Longrightarrow> localState (f_Exec_Comp trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun x c)) = localState (pointwise_shrink (trans_fun x c # f_Exec_Comp_Stream trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun x c)))
 2. \<And>x xs c i i2. \<lbrakk>0 < k; Deterministic_Trans_Fun (Acc_Trans_Fun_Step k trans_fun pointwise_shrink) localState; i2 < length xs; i = Suc i2; localState (f_Exec_Comp trans_fun (xs \<down> Suc i2 \<odot> k) (f_Exec_Comp trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun x c))) = localState (f_Exec_Comp (Acc_Trans_Fun_Step k trans_fun pointwise_shrink) (xs \<down> Suc i2) (f_Exec_Comp trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun x c))); localState (pointwise_shrink (trans_fun x c # f_Exec_Comp_Stream trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun x c))) = localState (if f_Exec_Comp_Stream trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun x c) = [] then trans_fun x c else last (f_Exec_Comp_Stream trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun x c)))\<rbrakk> \<Longrightarrow> xs \<down> Suc i2 \<noteq> []
[PROOF STEP]
apply (simp add: f_Exec_eq_f_Exec_Stream_last)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x xs c i i2. \<lbrakk>0 < k; Deterministic_Trans_Fun (Acc_Trans_Fun_Step k trans_fun pointwise_shrink) localState; i2 < length xs; i = Suc i2; localState (f_Exec_Comp trans_fun (xs \<down> Suc i2 \<odot> k) (f_Exec_Comp trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun x c))) = localState (f_Exec_Comp (Acc_Trans_Fun_Step k trans_fun pointwise_shrink) (xs \<down> Suc i2) (f_Exec_Comp trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun x c))); localState (pointwise_shrink (trans_fun x c # f_Exec_Comp_Stream trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun x c))) = localState (if f_Exec_Comp_Stream trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun x c) = [] then trans_fun x c else last (f_Exec_Comp_Stream trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun x c)))\<rbrakk> \<Longrightarrow> xs \<down> Suc i2 \<noteq> []
[PROOF STEP]
apply (simp add: length_greater_0_conv[symmetric] del: length_greater_0_conv)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma f_Exec_Stream_Acc_Output_eq_Acc_Trans_Fun_Step_Output: "\<And>c.
  \<lbrakk> 0 < k;
    Deterministic_Trans_Fun trans_fun localState;
    is_correct_localState_Pointwise_Output_Shrink pointwise_shrink localState;
    is_Pointwise_Output_Shrink pointwise_shrink output_fun \<rbrakk> \<Longrightarrow>
  f_Exec_Comp_Stream_Acc_Output k output_fun trans_fun xs c =
  map output_fun (f_Exec_Comp_Stream (Acc_Trans_Fun_Step k trans_fun pointwise_shrink) xs c)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>c. \<lbrakk>0 < k; Deterministic_Trans_Fun trans_fun localState; is_correct_localState_Pointwise_Output_Shrink pointwise_shrink localState; is_Pointwise_Output_Shrink pointwise_shrink output_fun\<rbrakk> \<Longrightarrow> f_Exec_Comp_Stream_Acc_Output k output_fun trans_fun xs c = map output_fun (f_Exec_Comp_Stream (Acc_Trans_Fun_Step k trans_fun pointwise_shrink) xs c)
[PROOF STEP]
apply (drule Deterministic_trans_fun_imp_acc_trans_fun[of trans_fun localState k pointwise_shrink])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>c. \<lbrakk>0 < k; is_correct_localState_Pointwise_Output_Shrink pointwise_shrink localState; is_Pointwise_Output_Shrink pointwise_shrink output_fun; Deterministic_Trans_Fun (Acc_Trans_Fun_Step k trans_fun pointwise_shrink) localState\<rbrakk> \<Longrightarrow> f_Exec_Comp_Stream_Acc_Output k output_fun trans_fun xs c = map output_fun (f_Exec_Comp_Stream (Acc_Trans_Fun_Step k trans_fun pointwise_shrink) xs c)
[PROOF STEP]
apply (clarsimp simp: list_eq_iff)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>c i. \<lbrakk>0 < k; is_correct_localState_Pointwise_Output_Shrink pointwise_shrink localState; is_Pointwise_Output_Shrink pointwise_shrink output_fun; Deterministic_Trans_Fun (Acc_Trans_Fun_Step k trans_fun pointwise_shrink) localState; i < length xs\<rbrakk> \<Longrightarrow> f_Exec_Comp_Stream_Acc_Output k output_fun trans_fun xs c ! i = output_fun (f_Exec_Comp_Stream (Acc_Trans_Fun_Step k trans_fun pointwise_shrink) xs c ! i)
[PROOF STEP]
apply (simp add: f_Exec_Stream_Acc_Output_nth f_Exec_Stream_nth del: f_Exec_Stream_Cons)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>c i. \<lbrakk>0 < k; is_correct_localState_Pointwise_Output_Shrink pointwise_shrink localState; is_Pointwise_Output_Shrink pointwise_shrink output_fun; Deterministic_Trans_Fun (Acc_Trans_Fun_Step k trans_fun pointwise_shrink) localState; i < length xs\<rbrakk> \<Longrightarrow> last_message (map output_fun (f_Exec_Comp_Stream trans_fun (xs ! i # NoMsg\<^bsup>k - Suc 0\<^esup>) (f_Exec_Comp trans_fun (xs \<down> i \<odot> k) c))) = output_fun (f_Exec_Comp (Acc_Trans_Fun_Step k trans_fun pointwise_shrink) (xs \<down> Suc i) c)
[PROOF STEP]
apply (induct xs, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a xs c i. \<lbrakk>\<And>c i. \<lbrakk>0 < k; is_correct_localState_Pointwise_Output_Shrink pointwise_shrink localState; is_Pointwise_Output_Shrink pointwise_shrink output_fun; Deterministic_Trans_Fun (Acc_Trans_Fun_Step k trans_fun pointwise_shrink) localState; i < length xs\<rbrakk> \<Longrightarrow> last_message (map output_fun (f_Exec_Comp_Stream trans_fun (xs ! i # NoMsg\<^bsup>k - Suc 0\<^esup>) (f_Exec_Comp trans_fun (xs \<down> i \<odot> k) c))) = output_fun (f_Exec_Comp (Acc_Trans_Fun_Step k trans_fun pointwise_shrink) (xs \<down> Suc i) c); 0 < k; is_correct_localState_Pointwise_Output_Shrink pointwise_shrink localState; is_Pointwise_Output_Shrink pointwise_shrink output_fun; Deterministic_Trans_Fun (Acc_Trans_Fun_Step k trans_fun pointwise_shrink) localState; i < length (a # xs)\<rbrakk> \<Longrightarrow> last_message (map output_fun (f_Exec_Comp_Stream trans_fun ((a # xs) ! i # NoMsg\<^bsup>k - Suc 0\<^esup>) (f_Exec_Comp trans_fun ((a # xs) \<down> i \<odot> k) c))) = output_fun (f_Exec_Comp (Acc_Trans_Fun_Step k trans_fun pointwise_shrink) ((a # xs) \<down> Suc i) c)
[PROOF STEP]
apply (rename_tac x xs c i)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x xs c i. \<lbrakk>\<And>c i. \<lbrakk>0 < k; is_correct_localState_Pointwise_Output_Shrink pointwise_shrink localState; is_Pointwise_Output_Shrink pointwise_shrink output_fun; Deterministic_Trans_Fun (Acc_Trans_Fun_Step k trans_fun pointwise_shrink) localState; i < length xs\<rbrakk> \<Longrightarrow> last_message (map output_fun (f_Exec_Comp_Stream trans_fun (xs ! i # NoMsg\<^bsup>k - Suc 0\<^esup>) (f_Exec_Comp trans_fun (xs \<down> i \<odot> k) c))) = output_fun (f_Exec_Comp (Acc_Trans_Fun_Step k trans_fun pointwise_shrink) (xs \<down> Suc i) c); 0 < k; is_correct_localState_Pointwise_Output_Shrink pointwise_shrink localState; is_Pointwise_Output_Shrink pointwise_shrink output_fun; Deterministic_Trans_Fun (Acc_Trans_Fun_Step k trans_fun pointwise_shrink) localState; i < length (x # xs)\<rbrakk> \<Longrightarrow> last_message (map output_fun (f_Exec_Comp_Stream trans_fun ((x # xs) ! i # NoMsg\<^bsup>k - Suc 0\<^esup>) (f_Exec_Comp trans_fun ((x # xs) \<down> i \<odot> k) c))) = output_fun (f_Exec_Comp (Acc_Trans_Fun_Step k trans_fun pointwise_shrink) ((x # xs) \<down> Suc i) c)
[PROOF STEP]
apply (simp add: Acc_Trans_Fun_Step_def del: f_Exec_Stream_Cons)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x xs c i. \<lbrakk>\<And>c i. i < length xs \<Longrightarrow> last_message (map output_fun (f_Exec_Comp_Stream trans_fun (xs ! i # NoMsg\<^bsup>k - Suc 0\<^esup>) (f_Exec_Comp trans_fun (xs \<down> i \<odot> k) c))) = output_fun (f_Exec_Comp (Acc_Trans_Fun_Step k trans_fun pointwise_shrink) (xs \<down> Suc i) c); 0 < k; is_correct_localState_Pointwise_Output_Shrink pointwise_shrink localState; is_Pointwise_Output_Shrink pointwise_shrink output_fun; Deterministic_Trans_Fun (Acc_Trans_Fun_Step k trans_fun pointwise_shrink) localState; i < Suc (length xs)\<rbrakk> \<Longrightarrow> last_message (map output_fun (f_Exec_Comp_Stream trans_fun ((x # xs) ! i # NoMsg\<^bsup>k - Suc 0\<^esup>) (f_Exec_Comp trans_fun ((x # xs) \<down> i \<odot> k) c))) = output_fun (f_Exec_Comp (Acc_Trans_Fun_Step k trans_fun pointwise_shrink) (xs \<down> i) (pointwise_shrink (f_Exec_Comp_Stream trans_fun (x # NoMsg\<^bsup>k - Suc 0\<^esup>) c)))
[PROOF STEP]
apply (case_tac i)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x xs c i. \<lbrakk>\<And>c i. i < length xs \<Longrightarrow> last_message (map output_fun (f_Exec_Comp_Stream trans_fun (xs ! i # NoMsg\<^bsup>k - Suc 0\<^esup>) (f_Exec_Comp trans_fun (xs \<down> i \<odot> k) c))) = output_fun (f_Exec_Comp (Acc_Trans_Fun_Step k trans_fun pointwise_shrink) (xs \<down> Suc i) c); 0 < k; is_correct_localState_Pointwise_Output_Shrink pointwise_shrink localState; is_Pointwise_Output_Shrink pointwise_shrink output_fun; Deterministic_Trans_Fun (Acc_Trans_Fun_Step k trans_fun pointwise_shrink) localState; i < Suc (length xs); i = 0\<rbrakk> \<Longrightarrow> last_message (map output_fun (f_Exec_Comp_Stream trans_fun ((x # xs) ! i # NoMsg\<^bsup>k - Suc 0\<^esup>) (f_Exec_Comp trans_fun ((x # xs) \<down> i \<odot> k) c))) = output_fun (f_Exec_Comp (Acc_Trans_Fun_Step k trans_fun pointwise_shrink) (xs \<down> i) (pointwise_shrink (f_Exec_Comp_Stream trans_fun (x # NoMsg\<^bsup>k - Suc 0\<^esup>) c)))
 2. \<And>x xs c i nat. \<lbrakk>\<And>c i. i < length xs \<Longrightarrow> last_message (map output_fun (f_Exec_Comp_Stream trans_fun (xs ! i # NoMsg\<^bsup>k - Suc 0\<^esup>) (f_Exec_Comp trans_fun (xs \<down> i \<odot> k) c))) = output_fun (f_Exec_Comp (Acc_Trans_Fun_Step k trans_fun pointwise_shrink) (xs \<down> Suc i) c); 0 < k; is_correct_localState_Pointwise_Output_Shrink pointwise_shrink localState; is_Pointwise_Output_Shrink pointwise_shrink output_fun; Deterministic_Trans_Fun (Acc_Trans_Fun_Step k trans_fun pointwise_shrink) localState; i < Suc (length xs); i = Suc nat\<rbrakk> \<Longrightarrow> last_message (map output_fun (f_Exec_Comp_Stream trans_fun ((x # xs) ! i # NoMsg\<^bsup>k - Suc 0\<^esup>) (f_Exec_Comp trans_fun ((x # xs) \<down> i \<odot> k) c))) = output_fun (f_Exec_Comp (Acc_Trans_Fun_Step k trans_fun pointwise_shrink) (xs \<down> i) (pointwise_shrink (f_Exec_Comp_Stream trans_fun (x # NoMsg\<^bsup>k - Suc 0\<^esup>) c)))
[PROOF STEP]
apply (simp add: is_Pointwise_Output_Shrink_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x xs c i nat. \<lbrakk>\<And>c i. i < length xs \<Longrightarrow> last_message (map output_fun (f_Exec_Comp_Stream trans_fun (xs ! i # NoMsg\<^bsup>k - Suc 0\<^esup>) (f_Exec_Comp trans_fun (xs \<down> i \<odot> k) c))) = output_fun (f_Exec_Comp (Acc_Trans_Fun_Step k trans_fun pointwise_shrink) (xs \<down> Suc i) c); 0 < k; is_correct_localState_Pointwise_Output_Shrink pointwise_shrink localState; is_Pointwise_Output_Shrink pointwise_shrink output_fun; Deterministic_Trans_Fun (Acc_Trans_Fun_Step k trans_fun pointwise_shrink) localState; i < Suc (length xs); i = Suc nat\<rbrakk> \<Longrightarrow> last_message (map output_fun (f_Exec_Comp_Stream trans_fun ((x # xs) ! i # NoMsg\<^bsup>k - Suc 0\<^esup>) (f_Exec_Comp trans_fun ((x # xs) \<down> i \<odot> k) c))) = output_fun (f_Exec_Comp (Acc_Trans_Fun_Step k trans_fun pointwise_shrink) (xs \<down> i) (pointwise_shrink (f_Exec_Comp_Stream trans_fun (x # NoMsg\<^bsup>k - Suc 0\<^esup>) c)))
[PROOF STEP]
apply (rename_tac i2)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x xs c i i2. \<lbrakk>\<And>c i. i < length xs \<Longrightarrow> last_message (map output_fun (f_Exec_Comp_Stream trans_fun (xs ! i # NoMsg\<^bsup>k - Suc 0\<^esup>) (f_Exec_Comp trans_fun (xs \<down> i \<odot> k) c))) = output_fun (f_Exec_Comp (Acc_Trans_Fun_Step k trans_fun pointwise_shrink) (xs \<down> Suc i) c); 0 < k; is_correct_localState_Pointwise_Output_Shrink pointwise_shrink localState; is_Pointwise_Output_Shrink pointwise_shrink output_fun; Deterministic_Trans_Fun (Acc_Trans_Fun_Step k trans_fun pointwise_shrink) localState; i < Suc (length xs); i = Suc i2\<rbrakk> \<Longrightarrow> last_message (map output_fun (f_Exec_Comp_Stream trans_fun ((x # xs) ! i # NoMsg\<^bsup>k - Suc 0\<^esup>) (f_Exec_Comp trans_fun ((x # xs) \<down> i \<odot> k) c))) = output_fun (f_Exec_Comp (Acc_Trans_Fun_Step k trans_fun pointwise_shrink) (xs \<down> i) (pointwise_shrink (f_Exec_Comp_Stream trans_fun (x # NoMsg\<^bsup>k - Suc 0\<^esup>) c)))
[PROOF STEP]
apply (simp add: f_Exec_append)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x xs c i i2. \<lbrakk>\<And>c i. i < length xs \<Longrightarrow> (if last_message (map output_fun (f_Exec_Comp_Stream trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun (xs ! i) (f_Exec_Comp trans_fun (xs \<down> i \<odot> k) c)))) = NoMsg then output_fun (trans_fun (xs ! i) (f_Exec_Comp trans_fun (xs \<down> i \<odot> k) c)) else last_message (map output_fun (f_Exec_Comp_Stream trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun (xs ! i) (f_Exec_Comp trans_fun (xs \<down> i \<odot> k) c))))) = output_fun (f_Exec_Comp (Acc_Trans_Fun_Step k trans_fun pointwise_shrink) (xs \<down> Suc i) c); 0 < k; is_correct_localState_Pointwise_Output_Shrink pointwise_shrink localState; is_Pointwise_Output_Shrink pointwise_shrink output_fun; Deterministic_Trans_Fun (Acc_Trans_Fun_Step k trans_fun pointwise_shrink) localState; i2 < length xs; i = Suc i2\<rbrakk> \<Longrightarrow> output_fun (f_Exec_Comp (Acc_Trans_Fun_Step k trans_fun pointwise_shrink) (xs \<down> Suc i2) (f_Exec_Comp trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun x c))) = output_fun (f_Exec_Comp (Acc_Trans_Fun_Step k trans_fun pointwise_shrink) (xs \<down> Suc i2) (pointwise_shrink (trans_fun x c # f_Exec_Comp_Stream trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun x c))))
[PROOF STEP]
apply (drule_tac x="f_Exec_Comp trans_fun \<NoMsg>\<^bsup>k - Suc 0\<^esup> (trans_fun x c)" in meta_spec)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x xs c i i2. \<lbrakk>0 < k; is_correct_localState_Pointwise_Output_Shrink pointwise_shrink localState; is_Pointwise_Output_Shrink pointwise_shrink output_fun; Deterministic_Trans_Fun (Acc_Trans_Fun_Step k trans_fun pointwise_shrink) localState; i2 < length xs; i = Suc i2; \<And>i. i < length xs \<Longrightarrow> (if last_message (map output_fun (f_Exec_Comp_Stream trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun (xs ! i) (f_Exec_Comp trans_fun (xs \<down> i \<odot> k) (f_Exec_Comp trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun x c)))))) = NoMsg then output_fun (trans_fun (xs ! i) (f_Exec_Comp trans_fun (xs \<down> i \<odot> k) (f_Exec_Comp trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun x c)))) else last_message (map output_fun (f_Exec_Comp_Stream trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun (xs ! i) (f_Exec_Comp trans_fun (xs \<down> i \<odot> k) (f_Exec_Comp trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun x c))))))) = output_fun (f_Exec_Comp (Acc_Trans_Fun_Step k trans_fun pointwise_shrink) (xs \<down> Suc i) (f_Exec_Comp trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun x c)))\<rbrakk> \<Longrightarrow> output_fun (f_Exec_Comp (Acc_Trans_Fun_Step k trans_fun pointwise_shrink) (xs \<down> Suc i2) (f_Exec_Comp trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun x c))) = output_fun (f_Exec_Comp (Acc_Trans_Fun_Step k trans_fun pointwise_shrink) (xs \<down> Suc i2) (pointwise_shrink (trans_fun x c # f_Exec_Comp_Stream trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun x c))))
[PROOF STEP]
apply (drule_tac x=i2 in meta_spec)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x xs c i i2. \<lbrakk>0 < k; is_correct_localState_Pointwise_Output_Shrink pointwise_shrink localState; is_Pointwise_Output_Shrink pointwise_shrink output_fun; Deterministic_Trans_Fun (Acc_Trans_Fun_Step k trans_fun pointwise_shrink) localState; i2 < length xs; i = Suc i2; i2 < length xs \<Longrightarrow> (if last_message (map output_fun (f_Exec_Comp_Stream trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun (xs ! i2) (f_Exec_Comp trans_fun (xs \<down> i2 \<odot> k) (f_Exec_Comp trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun x c)))))) = NoMsg then output_fun (trans_fun (xs ! i2) (f_Exec_Comp trans_fun (xs \<down> i2 \<odot> k) (f_Exec_Comp trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun x c)))) else last_message (map output_fun (f_Exec_Comp_Stream trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun (xs ! i2) (f_Exec_Comp trans_fun (xs \<down> i2 \<odot> k) (f_Exec_Comp trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun x c))))))) = output_fun (f_Exec_Comp (Acc_Trans_Fun_Step k trans_fun pointwise_shrink) (xs \<down> Suc i2) (f_Exec_Comp trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun x c)))\<rbrakk> \<Longrightarrow> output_fun (f_Exec_Comp (Acc_Trans_Fun_Step k trans_fun pointwise_shrink) (xs \<down> Suc i2) (f_Exec_Comp trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun x c))) = output_fun (f_Exec_Comp (Acc_Trans_Fun_Step k trans_fun pointwise_shrink) (xs \<down> Suc i2) (pointwise_shrink (trans_fun x c # f_Exec_Comp_Stream trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun x c))))
[PROOF STEP]
apply (simp add: is_correct_localState_Pointwise_Output_Shrink_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x xs c i i2. \<lbrakk>0 < k; \<forall>cs. cs \<noteq> [] \<longrightarrow> localState (pointwise_shrink cs) = localState (last cs); is_Pointwise_Output_Shrink pointwise_shrink output_fun; Deterministic_Trans_Fun (Acc_Trans_Fun_Step k trans_fun pointwise_shrink) localState; i2 < length xs; i = Suc i2; (if last_message (map output_fun (f_Exec_Comp_Stream trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun (xs ! i2) (f_Exec_Comp trans_fun (xs \<down> i2 \<odot> k) (f_Exec_Comp trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun x c)))))) = NoMsg then output_fun (trans_fun (xs ! i2) (f_Exec_Comp trans_fun (xs \<down> i2 \<odot> k) (f_Exec_Comp trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun x c)))) else last_message (map output_fun (f_Exec_Comp_Stream trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun (xs ! i2) (f_Exec_Comp trans_fun (xs \<down> i2 \<odot> k) (f_Exec_Comp trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun x c))))))) = output_fun (f_Exec_Comp (Acc_Trans_Fun_Step k trans_fun pointwise_shrink) (xs \<down> Suc i2) (f_Exec_Comp trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun x c)))\<rbrakk> \<Longrightarrow> output_fun (f_Exec_Comp (Acc_Trans_Fun_Step k trans_fun pointwise_shrink) (xs \<down> Suc i2) (f_Exec_Comp trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun x c))) = output_fun (f_Exec_Comp (Acc_Trans_Fun_Step k trans_fun pointwise_shrink) (xs \<down> Suc i2) (pointwise_shrink (trans_fun x c # f_Exec_Comp_Stream trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun x c))))
[PROOF STEP]
apply (drule_tac x="f_Exec_Comp_Stream trans_fun (x # NoMsg\<^bsup>k - Suc 0\<^esup>) c" in spec)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x xs c i i2. \<lbrakk>0 < k; is_Pointwise_Output_Shrink pointwise_shrink output_fun; Deterministic_Trans_Fun (Acc_Trans_Fun_Step k trans_fun pointwise_shrink) localState; i2 < length xs; i = Suc i2; (if last_message (map output_fun (f_Exec_Comp_Stream trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun (xs ! i2) (f_Exec_Comp trans_fun (xs \<down> i2 \<odot> k) (f_Exec_Comp trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun x c)))))) = NoMsg then output_fun (trans_fun (xs ! i2) (f_Exec_Comp trans_fun (xs \<down> i2 \<odot> k) (f_Exec_Comp trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun x c)))) else last_message (map output_fun (f_Exec_Comp_Stream trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun (xs ! i2) (f_Exec_Comp trans_fun (xs \<down> i2 \<odot> k) (f_Exec_Comp trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun x c))))))) = output_fun (f_Exec_Comp (Acc_Trans_Fun_Step k trans_fun pointwise_shrink) (xs \<down> Suc i2) (f_Exec_Comp trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun x c))); f_Exec_Comp_Stream trans_fun (x # NoMsg\<^bsup>k - Suc 0\<^esup>) c \<noteq> [] \<longrightarrow> localState (pointwise_shrink (f_Exec_Comp_Stream trans_fun (x # NoMsg\<^bsup>k - Suc 0\<^esup>) c)) = localState (last (f_Exec_Comp_Stream trans_fun (x # NoMsg\<^bsup>k - Suc 0\<^esup>) c))\<rbrakk> \<Longrightarrow> output_fun (f_Exec_Comp (Acc_Trans_Fun_Step k trans_fun pointwise_shrink) (xs \<down> Suc i2) (f_Exec_Comp trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun x c))) = output_fun (f_Exec_Comp (Acc_Trans_Fun_Step k trans_fun pointwise_shrink) (xs \<down> Suc i2) (pointwise_shrink (trans_fun x c # f_Exec_Comp_Stream trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun x c))))
[PROOF STEP]
apply (simp add: f_Exec_Stream_not_empty_conv)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x xs c i i2. \<lbrakk>0 < k; is_Pointwise_Output_Shrink pointwise_shrink output_fun; Deterministic_Trans_Fun (Acc_Trans_Fun_Step k trans_fun pointwise_shrink) localState; i2 < length xs; i = Suc i2; (if last_message (map output_fun (f_Exec_Comp_Stream trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun (xs ! i2) (f_Exec_Comp trans_fun (xs \<down> i2 \<odot> k) (f_Exec_Comp trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun x c)))))) = NoMsg then output_fun (trans_fun (xs ! i2) (f_Exec_Comp trans_fun (xs \<down> i2 \<odot> k) (f_Exec_Comp trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun x c)))) else last_message (map output_fun (f_Exec_Comp_Stream trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun (xs ! i2) (f_Exec_Comp trans_fun (xs \<down> i2 \<odot> k) (f_Exec_Comp trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun x c))))))) = output_fun (f_Exec_Comp (Acc_Trans_Fun_Step k trans_fun pointwise_shrink) (xs \<down> Suc i2) (f_Exec_Comp trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun x c))); localState (pointwise_shrink (trans_fun x c # f_Exec_Comp_Stream trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun x c))) = localState (if f_Exec_Comp_Stream trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun x c) = [] then trans_fun x c else last (f_Exec_Comp_Stream trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun x c)))\<rbrakk> \<Longrightarrow> output_fun (f_Exec_Comp (Acc_Trans_Fun_Step k trans_fun pointwise_shrink) (xs \<down> Suc i2) (f_Exec_Comp trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun x c))) = output_fun (f_Exec_Comp (Acc_Trans_Fun_Step k trans_fun pointwise_shrink) (xs \<down> Suc i2) (pointwise_shrink (trans_fun x c # f_Exec_Comp_Stream trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun x c))))
[PROOF STEP]
apply (rule arg_cong[where f=output_fun])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x xs c i i2. \<lbrakk>0 < k; is_Pointwise_Output_Shrink pointwise_shrink output_fun; Deterministic_Trans_Fun (Acc_Trans_Fun_Step k trans_fun pointwise_shrink) localState; i2 < length xs; i = Suc i2; (if last_message (map output_fun (f_Exec_Comp_Stream trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun (xs ! i2) (f_Exec_Comp trans_fun (xs \<down> i2 \<odot> k) (f_Exec_Comp trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun x c)))))) = NoMsg then output_fun (trans_fun (xs ! i2) (f_Exec_Comp trans_fun (xs \<down> i2 \<odot> k) (f_Exec_Comp trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun x c)))) else last_message (map output_fun (f_Exec_Comp_Stream trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun (xs ! i2) (f_Exec_Comp trans_fun (xs \<down> i2 \<odot> k) (f_Exec_Comp trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun x c))))))) = output_fun (f_Exec_Comp (Acc_Trans_Fun_Step k trans_fun pointwise_shrink) (xs \<down> Suc i2) (f_Exec_Comp trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun x c))); localState (pointwise_shrink (trans_fun x c # f_Exec_Comp_Stream trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun x c))) = localState (if f_Exec_Comp_Stream trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun x c) = [] then trans_fun x c else last (f_Exec_Comp_Stream trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun x c)))\<rbrakk> \<Longrightarrow> f_Exec_Comp (Acc_Trans_Fun_Step k trans_fun pointwise_shrink) (xs \<down> Suc i2) (f_Exec_Comp trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun x c)) = f_Exec_Comp (Acc_Trans_Fun_Step k trans_fun pointwise_shrink) (xs \<down> Suc i2) (pointwise_shrink (trans_fun x c # f_Exec_Comp_Stream trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun x c)))
[PROOF STEP]
apply (rule Deterministic_f_Exec)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x xs c i i2. \<lbrakk>0 < k; is_Pointwise_Output_Shrink pointwise_shrink output_fun; Deterministic_Trans_Fun (Acc_Trans_Fun_Step k trans_fun pointwise_shrink) localState; i2 < length xs; i = Suc i2; (if last_message (map output_fun (f_Exec_Comp_Stream trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun (xs ! i2) (f_Exec_Comp trans_fun (xs \<down> i2 \<odot> k) (f_Exec_Comp trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun x c)))))) = NoMsg then output_fun (trans_fun (xs ! i2) (f_Exec_Comp trans_fun (xs \<down> i2 \<odot> k) (f_Exec_Comp trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun x c)))) else last_message (map output_fun (f_Exec_Comp_Stream trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun (xs ! i2) (f_Exec_Comp trans_fun (xs \<down> i2 \<odot> k) (f_Exec_Comp trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun x c))))))) = output_fun (f_Exec_Comp (Acc_Trans_Fun_Step k trans_fun pointwise_shrink) (xs \<down> Suc i2) (f_Exec_Comp trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun x c))); localState (pointwise_shrink (trans_fun x c # f_Exec_Comp_Stream trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun x c))) = localState (if f_Exec_Comp_Stream trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun x c) = [] then trans_fun x c else last (f_Exec_Comp_Stream trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun x c)))\<rbrakk> \<Longrightarrow> Deterministic_Trans_Fun (Acc_Trans_Fun_Step k trans_fun pointwise_shrink) (?localState11 x xs c i i2)
 2. \<And>x xs c i i2. \<lbrakk>0 < k; is_Pointwise_Output_Shrink pointwise_shrink output_fun; Deterministic_Trans_Fun (Acc_Trans_Fun_Step k trans_fun pointwise_shrink) localState; i2 < length xs; i = Suc i2; (if last_message (map output_fun (f_Exec_Comp_Stream trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun (xs ! i2) (f_Exec_Comp trans_fun (xs \<down> i2 \<odot> k) (f_Exec_Comp trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun x c)))))) = NoMsg then output_fun (trans_fun (xs ! i2) (f_Exec_Comp trans_fun (xs \<down> i2 \<odot> k) (f_Exec_Comp trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun x c)))) else last_message (map output_fun (f_Exec_Comp_Stream trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun (xs ! i2) (f_Exec_Comp trans_fun (xs \<down> i2 \<odot> k) (f_Exec_Comp trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun x c))))))) = output_fun (f_Exec_Comp (Acc_Trans_Fun_Step k trans_fun pointwise_shrink) (xs \<down> Suc i2) (f_Exec_Comp trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun x c))); localState (pointwise_shrink (trans_fun x c # f_Exec_Comp_Stream trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun x c))) = localState (if f_Exec_Comp_Stream trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun x c) = [] then trans_fun x c else last (f_Exec_Comp_Stream trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun x c)))\<rbrakk> \<Longrightarrow> ?localState11 x xs c i i2 (f_Exec_Comp trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun x c)) = ?localState11 x xs c i i2 (pointwise_shrink (trans_fun x c # f_Exec_Comp_Stream trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun x c)))
 3. \<And>x xs c i i2. \<lbrakk>0 < k; is_Pointwise_Output_Shrink pointwise_shrink output_fun; Deterministic_Trans_Fun (Acc_Trans_Fun_Step k trans_fun pointwise_shrink) localState; i2 < length xs; i = Suc i2; (if last_message (map output_fun (f_Exec_Comp_Stream trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun (xs ! i2) (f_Exec_Comp trans_fun (xs \<down> i2 \<odot> k) (f_Exec_Comp trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun x c)))))) = NoMsg then output_fun (trans_fun (xs ! i2) (f_Exec_Comp trans_fun (xs \<down> i2 \<odot> k) (f_Exec_Comp trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun x c)))) else last_message (map output_fun (f_Exec_Comp_Stream trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun (xs ! i2) (f_Exec_Comp trans_fun (xs \<down> i2 \<odot> k) (f_Exec_Comp trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun x c))))))) = output_fun (f_Exec_Comp (Acc_Trans_Fun_Step k trans_fun pointwise_shrink) (xs \<down> Suc i2) (f_Exec_Comp trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun x c))); localState (pointwise_shrink (trans_fun x c # f_Exec_Comp_Stream trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun x c))) = localState (if f_Exec_Comp_Stream trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun x c) = [] then trans_fun x c else last (f_Exec_Comp_Stream trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun x c)))\<rbrakk> \<Longrightarrow> xs \<down> Suc i2 \<noteq> []
[PROOF STEP]
apply assumption
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x xs c i i2. \<lbrakk>0 < k; is_Pointwise_Output_Shrink pointwise_shrink output_fun; Deterministic_Trans_Fun (Acc_Trans_Fun_Step k trans_fun pointwise_shrink) localState; i2 < length xs; i = Suc i2; (if last_message (map output_fun (f_Exec_Comp_Stream trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun (xs ! i2) (f_Exec_Comp trans_fun (xs \<down> i2 \<odot> k) (f_Exec_Comp trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun x c)))))) = NoMsg then output_fun (trans_fun (xs ! i2) (f_Exec_Comp trans_fun (xs \<down> i2 \<odot> k) (f_Exec_Comp trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun x c)))) else last_message (map output_fun (f_Exec_Comp_Stream trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun (xs ! i2) (f_Exec_Comp trans_fun (xs \<down> i2 \<odot> k) (f_Exec_Comp trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun x c))))))) = output_fun (f_Exec_Comp (Acc_Trans_Fun_Step k trans_fun pointwise_shrink) (xs \<down> Suc i2) (f_Exec_Comp trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun x c))); localState (pointwise_shrink (trans_fun x c # f_Exec_Comp_Stream trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun x c))) = localState (if f_Exec_Comp_Stream trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun x c) = [] then trans_fun x c else last (f_Exec_Comp_Stream trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun x c)))\<rbrakk> \<Longrightarrow> localState (f_Exec_Comp trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun x c)) = localState (pointwise_shrink (trans_fun x c # f_Exec_Comp_Stream trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun x c)))
 2. \<And>x xs c i i2. \<lbrakk>0 < k; is_Pointwise_Output_Shrink pointwise_shrink output_fun; Deterministic_Trans_Fun (Acc_Trans_Fun_Step k trans_fun pointwise_shrink) localState; i2 < length xs; i = Suc i2; (if last_message (map output_fun (f_Exec_Comp_Stream trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun (xs ! i2) (f_Exec_Comp trans_fun (xs \<down> i2 \<odot> k) (f_Exec_Comp trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun x c)))))) = NoMsg then output_fun (trans_fun (xs ! i2) (f_Exec_Comp trans_fun (xs \<down> i2 \<odot> k) (f_Exec_Comp trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun x c)))) else last_message (map output_fun (f_Exec_Comp_Stream trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun (xs ! i2) (f_Exec_Comp trans_fun (xs \<down> i2 \<odot> k) (f_Exec_Comp trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun x c))))))) = output_fun (f_Exec_Comp (Acc_Trans_Fun_Step k trans_fun pointwise_shrink) (xs \<down> Suc i2) (f_Exec_Comp trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun x c))); localState (pointwise_shrink (trans_fun x c # f_Exec_Comp_Stream trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun x c))) = localState (if f_Exec_Comp_Stream trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun x c) = [] then trans_fun x c else last (f_Exec_Comp_Stream trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun x c)))\<rbrakk> \<Longrightarrow> xs \<down> Suc i2 \<noteq> []
[PROOF STEP]
apply (simp add: f_Exec_eq_f_Exec_Stream_last)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x xs c i i2. \<lbrakk>0 < k; is_Pointwise_Output_Shrink pointwise_shrink output_fun; Deterministic_Trans_Fun (Acc_Trans_Fun_Step k trans_fun pointwise_shrink) localState; i2 < length xs; i = Suc i2; (if last_message (map output_fun (f_Exec_Comp_Stream trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun (xs ! i2) (f_Exec_Comp trans_fun (xs \<down> i2 \<odot> k) (f_Exec_Comp trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun x c)))))) = NoMsg then output_fun (trans_fun (xs ! i2) (f_Exec_Comp trans_fun (xs \<down> i2 \<odot> k) (f_Exec_Comp trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun x c)))) else last_message (map output_fun (f_Exec_Comp_Stream trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun (xs ! i2) (f_Exec_Comp trans_fun (xs \<down> i2 \<odot> k) (f_Exec_Comp trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun x c))))))) = output_fun (f_Exec_Comp (Acc_Trans_Fun_Step k trans_fun pointwise_shrink) (xs \<down> Suc i2) (f_Exec_Comp trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun x c))); localState (pointwise_shrink (trans_fun x c # f_Exec_Comp_Stream trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun x c))) = localState (if f_Exec_Comp_Stream trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun x c) = [] then trans_fun x c else last (f_Exec_Comp_Stream trans_fun NoMsg\<^bsup>k - Suc 0\<^esup> (trans_fun x c)))\<rbrakk> \<Longrightarrow> xs \<down> Suc i2 \<noteq> []
[PROOF STEP]
apply (simp add: length_greater_0_conv[symmetric] del: length_greater_0_conv)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma i_Exec_Stream_Acc_LocalState_eq_Acc_Trans_Fun_Step_LocalState: "\<And>c.
  \<lbrakk> 0 < k;
    Deterministic_Trans_Fun trans_fun localState;
    is_correct_localState_Pointwise_Output_Shrink pointwise_shrink localState \<rbrakk> \<Longrightarrow>
  i_Exec_Comp_Stream_Acc_LocalState k localState trans_fun input c =
  localState \<circ> (i_Exec_Comp_Stream (Acc_Trans_Fun_Step k trans_fun pointwise_shrink) input c)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>c. \<lbrakk>0 < k; Deterministic_Trans_Fun trans_fun localState; is_correct_localState_Pointwise_Output_Shrink pointwise_shrink localState\<rbrakk> \<Longrightarrow> i_Exec_Comp_Stream_Acc_LocalState k localState trans_fun input c = localState \<circ> i_Exec_Comp_Stream (Acc_Trans_Fun_Step k trans_fun pointwise_shrink) input c
[PROOF STEP]
apply (rule ilist_i_take_eq_conv[THEN iffD2], rule allI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>c n. \<lbrakk>0 < k; Deterministic_Trans_Fun trans_fun localState; is_correct_localState_Pointwise_Output_Shrink pointwise_shrink localState\<rbrakk> \<Longrightarrow> i_Exec_Comp_Stream_Acc_LocalState k localState trans_fun input c \<Down> n = (localState \<circ> i_Exec_Comp_Stream (Acc_Trans_Fun_Step k trans_fun pointwise_shrink) input c) \<Down> n
[PROOF STEP]
apply (simp add: i_Exec_Stream_Acc_LocalState_take i_Exec_Stream_take f_Exec_Stream_Acc_LocalState_eq_Acc_Trans_Fun_Step_LocalState)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma i_Exec_Stream_Acc_Output_eq_Acc_Trans_Fun_Step_Output: "\<And>c.
  \<lbrakk> 0 < k;
    Deterministic_Trans_Fun trans_fun localState;
    is_correct_localState_Pointwise_Output_Shrink pointwise_shrink localState;
    is_Pointwise_Output_Shrink pointwise_shrink output_fun \<rbrakk> \<Longrightarrow>
  i_Exec_Comp_Stream_Acc_Output k output_fun trans_fun input c =
  output_fun \<circ> (i_Exec_Comp_Stream (Acc_Trans_Fun_Step k trans_fun pointwise_shrink) input c)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>c. \<lbrakk>0 < k; Deterministic_Trans_Fun trans_fun localState; is_correct_localState_Pointwise_Output_Shrink pointwise_shrink localState; is_Pointwise_Output_Shrink pointwise_shrink output_fun\<rbrakk> \<Longrightarrow> i_Exec_Comp_Stream_Acc_Output k output_fun trans_fun input c = output_fun \<circ> i_Exec_Comp_Stream (Acc_Trans_Fun_Step k trans_fun pointwise_shrink) input c
[PROOF STEP]
apply (rule ilist_i_take_eq_conv[THEN iffD2], rule allI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>c n. \<lbrakk>0 < k; Deterministic_Trans_Fun trans_fun localState; is_correct_localState_Pointwise_Output_Shrink pointwise_shrink localState; is_Pointwise_Output_Shrink pointwise_shrink output_fun\<rbrakk> \<Longrightarrow> i_Exec_Comp_Stream_Acc_Output k output_fun trans_fun input c \<Down> n = (output_fun \<circ> i_Exec_Comp_Stream (Acc_Trans_Fun_Step k trans_fun pointwise_shrink) input c) \<Down> n
[PROOF STEP]
apply (simp add: i_Exec_Stream_Acc_Output_take i_Exec_Stream_take f_Exec_Stream_Acc_Output_eq_Acc_Trans_Fun_Step_Output)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


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


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


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


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


[STATEMENT]
lemma f_Exec_Stream_Acc_Output_Init_1: "
  f_Exec_Comp_Stream_Acc_Output_Init (Suc 0) output_fun trans_fun xs c =
  map output_fun (f_Exec_Comp_Stream_Init trans_fun xs c)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f_Exec_Comp_Stream_Acc_Output_Init (Suc 0) output_fun trans_fun xs c = map output_fun (f_Exec_Comp_Stream_Init trans_fun xs c)
[PROOF STEP]
by (simp add: f_Exec_Comp_Stream_Acc_Output_Init_def f_Exec_Stream_Init_eq_f_Exec_Stream_Cons)


[STATEMENT]
lemma f_Exec_Stream_Acc_LocalState_Init_1: "
  f_Exec_Comp_Stream_Acc_LocalState_Init (Suc 0) localState trans_fun xs c =
  map localState (f_Exec_Comp_Stream_Init trans_fun xs c)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f_Exec_Comp_Stream_Acc_LocalState_Init (Suc 0) localState trans_fun xs c = map localState (f_Exec_Comp_Stream_Init trans_fun xs c)
[PROOF STEP]
by (simp add: f_Exec_Comp_Stream_Acc_LocalState_Init_def f_Exec_Stream_Init_eq_f_Exec_Stream_Cons)


[STATEMENT]
lemma i_Exec_Stream_Acc_Output_Init_1: "
  i_Exec_Comp_Stream_Acc_Output_Init (Suc 0) output_fun trans_fun input c =
  output_fun \<circ> (i_Exec_Comp_Stream_Init trans_fun input c)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i_Exec_Comp_Stream_Acc_Output_Init (Suc 0) output_fun trans_fun input c = output_fun \<circ> i_Exec_Comp_Stream_Init trans_fun input c
[PROOF STEP]
by (simp add: i_Exec_Comp_Stream_Acc_Output_Init_def i_Exec_Stream_Init_eq_i_Exec_Stream_Cons)


[STATEMENT]
lemma i_Exec_Stream_Acc_LocalState_Init_1: "
  i_Exec_Comp_Stream_Acc_LocalState_Init (Suc 0) localState trans_fun input c =
  localState \<circ> (i_Exec_Comp_Stream_Init trans_fun input c)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i_Exec_Comp_Stream_Acc_LocalState_Init (Suc 0) localState trans_fun input c = localState \<circ> i_Exec_Comp_Stream_Init trans_fun input c
[PROOF STEP]
by (simp add: i_Exec_Comp_Stream_Acc_LocalState_Init_def i_Exec_Stream_Init_eq_i_Exec_Stream_Cons)


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


[STATEMENT]
lemma f_Exec_Stream_Acc_Output_Init_drop': "
  \<lbrakk> 0 < k; n < length xs \<rbrakk> \<Longrightarrow>
  f_Exec_Comp_Stream_Acc_Output_Init k output_fun trans_fun xs c \<up> Suc n =
  f_Exec_Comp_Stream_Acc_Output k output_fun trans_fun xs c \<up> n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < k; n < length xs\<rbrakk> \<Longrightarrow> f_Exec_Comp_Stream_Acc_Output_Init k output_fun trans_fun xs c \<up> Suc n = f_Exec_Comp_Stream_Acc_Output k output_fun trans_fun xs c \<up> n
[PROOF STEP]
by (simp add: f_Exec_Comp_Stream_Acc_Output_Init_def)


[STATEMENT]
lemma i_Exec_Stream_Acc_Output_Init_take: "
  0 < k \<Longrightarrow>
  i_Exec_Comp_Stream_Acc_Output_Init k output_fun trans_fun input c \<Down> (Suc n) =
  f_Exec_Comp_Stream_Acc_Output_Init 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_Init k output_fun trans_fun input c \<Down> Suc n = f_Exec_Comp_Stream_Acc_Output_Init k output_fun trans_fun (input \<Down> n) c
[PROOF STEP]
by (simp add: f_Exec_Comp_Stream_Acc_Output_Init_def i_Exec_Comp_Stream_Acc_Output_Init_def i_Exec_Stream_Acc_Output_take)


[STATEMENT]
lemma i_Exec_Stream_Acc_Output_Init_drop': "
  0 < k \<Longrightarrow>
  i_Exec_Comp_Stream_Acc_Output_Init k output_fun trans_fun xs c \<Up> Suc n =
  i_Exec_Comp_Stream_Acc_Output k output_fun trans_fun xs c \<Up> n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < k \<Longrightarrow> i_Exec_Comp_Stream_Acc_Output_Init k output_fun trans_fun xs c \<Up> Suc n = i_Exec_Comp_Stream_Acc_Output k output_fun trans_fun xs c \<Up> n
[PROOF STEP]
by (simp add: i_Exec_Comp_Stream_Acc_Output_Init_def)


[STATEMENT]
lemma f_Exec_Stream_Acc_Output_Init_strictly_causal: "
  xs \<down> n = ys \<down> n \<Longrightarrow>
  f_Exec_Comp_Stream_Acc_Output_Init k output_fun trans_fun xs c \<down> Suc n =
  f_Exec_Comp_Stream_Acc_Output_Init k output_fun trans_fun ys c \<down> Suc n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. xs \<down> n = ys \<down> n \<Longrightarrow> f_Exec_Comp_Stream_Acc_Output_Init k output_fun trans_fun xs c \<down> Suc n = f_Exec_Comp_Stream_Acc_Output_Init k output_fun trans_fun ys c \<down> Suc n
[PROOF STEP]
by (simp add: f_Exec_Comp_Stream_Acc_Output_Init_def, rule f_Exec_Stream_Acc_Output_causal)


[STATEMENT]
lemma i_Exec_Stream_Acc_Output_Init_strictly_causal: "
  input1 \<Down> n = input2 \<Down> n \<Longrightarrow>
  i_Exec_Comp_Stream_Acc_Output_Init k output_fun trans_fun input1 c \<Down> Suc n =
  i_Exec_Comp_Stream_Acc_Output_Init k output_fun trans_fun input2 c \<Down> Suc n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. input1 \<Down> n = input2 \<Down> n \<Longrightarrow> i_Exec_Comp_Stream_Acc_Output_Init k output_fun trans_fun input1 c \<Down> Suc n = i_Exec_Comp_Stream_Acc_Output_Init k output_fun trans_fun input2 c \<Down> Suc n
[PROOF STEP]
by (simp add: i_Exec_Comp_Stream_Acc_Output_Init_def, rule i_Exec_Stream_Acc_Output_causal)


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


[STATEMENT]
lemma f_Exec_Stream_Acc_Output_Init_eq_f_Exec_Stream_Acc_Output_Cons_output: "
  output_fun c = \<NoMsg> \<Longrightarrow>
  f_Exec_Comp_Stream_Acc_Output_Init k output_fun trans_fun xs c =
  \<NoMsg> # f_Exec_Comp_Stream_Acc_Output k output_fun trans_fun xs c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. output_fun c = NoMsg \<Longrightarrow> f_Exec_Comp_Stream_Acc_Output_Init k output_fun trans_fun xs c = NoMsg # f_Exec_Comp_Stream_Acc_Output k output_fun trans_fun xs c
[PROOF STEP]
by (simp add: f_Exec_Stream_Acc_Output_Init_eq_f_Exec_Stream_Acc_Output_Cons)


[STATEMENT]
lemma f_Exec_Stream__Acc_OutputInit_tl_eq_f_Exec_Stream_Acc_Output: "
  tl (f_Exec_Comp_Stream_Acc_Output_Init k output_fun trans_fun xs c) =
  f_Exec_Comp_Stream_Acc_Output k output_fun trans_fun xs c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. tl (f_Exec_Comp_Stream_Acc_Output_Init k output_fun trans_fun xs c) = f_Exec_Comp_Stream_Acc_Output k output_fun trans_fun xs c
[PROOF STEP]
by (simp add: f_Exec_Stream_Acc_Output_Init_eq_f_Exec_Stream_Acc_Output_Cons)


[STATEMENT]
lemma f_Exec_Stream_Previous_f_Exec_Stream_Acc_Output_Init: "
  f_Exec_Comp_Stream_Acc_Output_Init k output_fun trans_fun xs c ! n =
  (f_Exec_Comp_Stream_Acc_Output k output_fun trans_fun xs c)\<^bsup>\<leftarrow>' output_fun c\<^esup> n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f_Exec_Comp_Stream_Acc_Output_Init k output_fun trans_fun xs c ! n = (f_Exec_Comp_Stream_Acc_Output k output_fun trans_fun xs c)\<^bsup>\<leftarrow>' output_fun c\<^esup> n
[PROOF STEP]
by (simp add: f_Exec_Stream_Acc_Output_Init_eq_f_Exec_Stream_Acc_Output_Cons list_Previous_nth_if nth_Cons')


[STATEMENT]
lemma f_Exec_Stream_Acc_Output_Init_eq_output_channel: "
  \<lbrakk> output_fun c = \<NoMsg>;
    f_Streams_Connected
      (f_Exec_Comp_Stream_Acc_Output k output_fun trans_fun xs c)
      channel \<rbrakk> \<Longrightarrow>
  f_Exec_Comp_Stream_Acc_Output_Init k output_fun trans_fun xs c = channel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>output_fun c = NoMsg; f_Streams_Connected (f_Exec_Comp_Stream_Acc_Output k output_fun trans_fun xs c) channel\<rbrakk> \<Longrightarrow> f_Exec_Comp_Stream_Acc_Output_Init k output_fun trans_fun xs c = channel
[PROOF STEP]
by (simp add: f_Streams_Connected_def f_Exec_Stream_Acc_Output_Init_eq_f_Exec_Stream_Acc_Output_Cons_output)


[STATEMENT]
lemma i_Exec_Stream_Acc_Output_Init_eq_i_Exec_Stream_Acc_Output_Cons: "
  i_Exec_Comp_Stream_Acc_Output_Init k output_fun trans_fun input c =
  [output_fun c] \<frown> i_Exec_Comp_Stream_Acc_Output k output_fun trans_fun input c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i_Exec_Comp_Stream_Acc_Output_Init k output_fun trans_fun input c = [output_fun c] \<frown> i_Exec_Comp_Stream_Acc_Output k output_fun trans_fun input c
[PROOF STEP]
by (simp add: i_Exec_Comp_Stream_Acc_Output_def i_Exec_Comp_Stream_Acc_Output_Init_def)


[STATEMENT]
lemma i_Exec_Stream_Acc_Output_Init_eq_i_Exec_Stream_Acc_Output_Cons_output: "
  output_fun c = \<NoMsg> \<Longrightarrow>
  i_Exec_Comp_Stream_Acc_Output_Init k output_fun trans_fun input c =
  [\<NoMsg> ] \<frown> i_Exec_Comp_Stream_Acc_Output k output_fun trans_fun input c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. output_fun c = NoMsg \<Longrightarrow> i_Exec_Comp_Stream_Acc_Output_Init k output_fun trans_fun input c = [NoMsg] \<frown> i_Exec_Comp_Stream_Acc_Output k output_fun trans_fun input c
[PROOF STEP]
by (simp add: i_Exec_Stream_Acc_Output_Init_eq_i_Exec_Stream_Acc_Output_Cons)


[STATEMENT]
lemma i_Exec_Stream_Previous_i_Exec_Stream_Acc_Output_Init: "
  i_Exec_Comp_Stream_Acc_Output_Init k output_fun trans_fun input c n =
  (i_Exec_Comp_Stream_Acc_Output k output_fun trans_fun input c)\<^bsup>\<leftarrow> output_fun c\<^esup> n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i_Exec_Comp_Stream_Acc_Output_Init k output_fun trans_fun input c n = (i_Exec_Comp_Stream_Acc_Output k output_fun trans_fun input c)\<^bsup>\<leftarrow> output_fun c\<^esup> n
[PROOF STEP]
by (simp add: i_Exec_Stream_Acc_Output_Init_eq_i_Exec_Stream_Acc_Output_Cons ilist_Previous_nth_if)


[STATEMENT]
lemma i_Exec_Stream_Acc_Output_Init_eq_output_channel: "
  \<lbrakk> output_fun c = \<NoMsg>;
    i_Streams_Connected
      (i_Exec_Comp_Stream_Acc_Output k output_fun trans_fun input c)
      channel \<rbrakk> \<Longrightarrow>
  i_Exec_Comp_Stream_Acc_Output_Init k output_fun trans_fun input c = channel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>output_fun c = NoMsg; i_Streams_Connected (i_Exec_Comp_Stream_Acc_Output k output_fun trans_fun input c) channel\<rbrakk> \<Longrightarrow> i_Exec_Comp_Stream_Acc_Output_Init k output_fun trans_fun input c = channel
[PROOF STEP]
by (simp add: i_Streams_Connected_def i_Exec_Stream_Acc_Output_Init_eq_i_Exec_Stream_Acc_Output_Cons_output)