[STATEMENT]
lemma is_generalised_output_of_does_not_subsume:
  "is_generalised_output_of t' t r p \<Longrightarrow>
   p < length (Outputs t) \<Longrightarrow>
   nth (Outputs t) p = L v \<Longrightarrow>
   c $ r \<noteq> Some v \<Longrightarrow>
   \<exists>i. can_take_transition t i c \<Longrightarrow>
   \<not>subsumes t' c t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_generalised_output_of t' t r p; p < length (Outputs t); Outputs t ! p = L v; c $ r \<noteq> Some v; \<exists>i. can_take_transition t i c\<rbrakk> \<Longrightarrow> \<not> subsumes t' c t
[PROOF STEP]
apply (rule bad_outputs)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_generalised_output_of t' t r p; p < length (Outputs t); Outputs t ! p = L v; c $ r \<noteq> Some v; \<exists>i. can_take_transition t i c\<rbrakk> \<Longrightarrow> \<exists>i. can_take_transition t i c \<and> evaluate_outputs t i c \<noteq> evaluate_outputs t' i c
[PROOF STEP]
apply clarify
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i. \<lbrakk>is_generalised_output_of t' t r p; p < length (Outputs t); Outputs t ! p = L v; c $ r \<noteq> Some v; can_take_transition t i c\<rbrakk> \<Longrightarrow> \<exists>i. can_take_transition t i c \<and> evaluate_outputs t i c \<noteq> evaluate_outputs t' i c
[PROOF STEP]
subgoal for i
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_generalised_output_of t' t r p; p < length (Outputs t); Outputs t ! p = L v; c $ r \<noteq> Some v; can_take_transition t i c\<rbrakk> \<Longrightarrow> \<exists>i. can_take_transition t i c \<and> evaluate_outputs t i c \<noteq> evaluate_outputs t' i c
[PROOF STEP]
apply (rule_tac x=i in exI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_generalised_output_of t' t r p; p < length (Outputs t); Outputs t ! p = L v; c $ r \<noteq> Some v; can_take_transition t i c\<rbrakk> \<Longrightarrow> can_take_transition t i c \<and> evaluate_outputs t i c \<noteq> evaluate_outputs t' i c
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_generalised_output_of t' t r p; p < length (Outputs t); Outputs t ! p = L v; c $ r \<noteq> Some v; can_take_transition t i c\<rbrakk> \<Longrightarrow> evaluate_outputs t i c \<noteq> evaluate_outputs t' i c
[PROOF STEP]
apply (rule lists_neq_if)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_generalised_output_of t' t r p; p < length (Outputs t); Outputs t ! p = L v; c $ r \<noteq> Some v; can_take_transition t i c\<rbrakk> \<Longrightarrow> \<exists>ia. evaluate_outputs t i c ! ia \<noteq> evaluate_outputs t' i c ! ia
[PROOF STEP]
apply (rule_tac x=p in exI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_generalised_output_of t' t r p; p < length (Outputs t); Outputs t ! p = L v; c $ r \<noteq> Some v; can_take_transition t i c\<rbrakk> \<Longrightarrow> evaluate_outputs t i c ! p \<noteq> evaluate_outputs t' i c ! p
[PROOF STEP]
by (simp add: is_generalised_output_of_def generalise_output_def apply_outputs_nth join_ir_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done