[STATEMENT]
lemma max_pos_imp_Interp:
  assumes "C \<in> N" and "C \<noteq> {#}" and "Max_mset C = Pos A" and "S C = {#}"
  shows "Interp C \<Turnstile> C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Interp C \<Turnstile> C
[PROOF STEP]
proof (cases "productive C")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. production C \<noteq> {} \<Longrightarrow> Interp C \<Turnstile> C
 2. \<not> production C \<noteq> {} \<Longrightarrow> Interp C \<Turnstile> C
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
production C \<noteq> {}

goal (2 subgoals):
 1. production C \<noteq> {} \<Longrightarrow> Interp C \<Turnstile> C
 2. \<not> production C \<noteq> {} \<Longrightarrow> Interp C \<Turnstile> C
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
production C \<noteq> {}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
production C \<noteq> {}

goal (1 subgoal):
 1. Interp C \<Turnstile> C
[PROOF STEP]
by (fast intro: productive_imp_Interp)
[PROOF STATE]
proof (state)
this:
Interp C \<Turnstile> C

goal (1 subgoal):
 1. \<not> production C \<noteq> {} \<Longrightarrow> Interp C \<Turnstile> C
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> production C \<noteq> {} \<Longrightarrow> Interp C \<Turnstile> C
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> production C \<noteq> {}

goal (1 subgoal):
 1. \<not> production C \<noteq> {} \<Longrightarrow> Interp C \<Turnstile> C
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> production C \<noteq> {}
[PROOF STEP]
have "interp C \<Turnstile> C"
[PROOF STATE]
proof (prove)
using this:
\<not> production C \<noteq> {}

goal (1 subgoal):
 1. interp C \<Turnstile> C
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<not> production C \<noteq> {}
C \<in> N
C \<noteq> {#}
Max_mset C = Pos A
S C = {#}

goal (1 subgoal):
 1. interp C \<Turnstile> C
[PROOF STEP]
unfolding production_unfold
[PROOF STATE]
proof (prove)
using this:
\<not> {A. C \<in> N \<and> C \<noteq> {#} \<and> Max_mset C = Pos A \<and> \<not> interp C \<Turnstile> C \<and> S C = {#}} \<noteq> {}
C \<in> N
C \<noteq> {#}
Max_mset C = Pos A
S C = {#}

goal (1 subgoal):
 1. interp C \<Turnstile> C
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
interp C \<Turnstile> C

goal (1 subgoal):
 1. \<not> production C \<noteq> {} \<Longrightarrow> Interp C \<Turnstile> C
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
interp C \<Turnstile> C
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
interp C \<Turnstile> C

goal (1 subgoal):
 1. Interp C \<Turnstile> C
[PROOF STEP]
unfolding Interp_def
[PROOF STATE]
proof (prove)
using this:
interp C \<Turnstile> C

goal (1 subgoal):
 1. interp C \<union> production C \<Turnstile> C
[PROOF STEP]
using False
[PROOF STATE]
proof (prove)
using this:
interp C \<Turnstile> C
\<not> production C \<noteq> {}

goal (1 subgoal):
 1. interp C \<union> production C \<Turnstile> C
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Interp C \<Turnstile> C

goal:
No subgoals!
[PROOF STEP]
qed