[STATEMENT]
lemma aType_empty: 
  assumes h1:"msg (Suc 0) a"
         and h2: "a t \<noteq> [sc_ack]"
  shows       "a t = []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a t = []
[PROOF STEP]
proof (cases "a t")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. a t = [] \<Longrightarrow> a t = []
 2. \<And>aa list. a t = aa # list \<Longrightarrow> a t = []
[PROOF STEP]
assume a1:"a t = []"
[PROOF STATE]
proof (state)
this:
a t = []

goal (2 subgoals):
 1. a t = [] \<Longrightarrow> a t = []
 2. \<And>aa list. a t = aa # list \<Longrightarrow> a t = []
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
a t = []
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
a t = []

goal (1 subgoal):
 1. a t = []
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
a t = []

goal (1 subgoal):
 1. \<And>aa list. a t = aa # list \<Longrightarrow> a t = []
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>aa list. a t = aa # list \<Longrightarrow> a t = []
[PROOF STEP]
fix aa l
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>aa list. a t = aa # list \<Longrightarrow> a t = []
[PROOF STEP]
assume a2:"a t = aa # l"
[PROOF STATE]
proof (state)
this:
a t = aa # l

goal (1 subgoal):
 1. \<And>aa list. a t = aa # list \<Longrightarrow> a t = []
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a t = []
[PROOF STEP]
proof (cases "aa")
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. aa = sc_ack \<Longrightarrow> a t = []
[PROOF STEP]
assume a3:"aa = sc_ack"
[PROOF STATE]
proof (state)
this:
aa = sc_ack

goal (1 subgoal):
 1. aa = sc_ack \<Longrightarrow> a t = []
[PROOF STEP]
from h1
[PROOF STATE]
proof (chain)
picking this:
msg (Suc 0) a
[PROOF STEP]
have sg1:"length (a t) \<le> Suc 0"
[PROOF STATE]
proof (prove)
using this:
msg (Suc 0) a

goal (1 subgoal):
 1. length (a t) \<le> Suc 0
[PROOF STEP]
by (simp add: msg_def)
[PROOF STATE]
proof (state)
this:
length (a t) \<le> Suc 0

goal (1 subgoal):
 1. aa = sc_ack \<Longrightarrow> a t = []
[PROOF STEP]
from this and assms and a2 and a3
[PROOF STATE]
proof (chain)
picking this:
length (a t) \<le> Suc 0
msg (Suc 0) a
a t \<noteq> [sc_ack]
a t = aa # l
aa = sc_ack
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
length (a t) \<le> Suc 0
msg (Suc 0) a
a t \<noteq> [sc_ack]
a t = aa # l
aa = sc_ack

goal (1 subgoal):
 1. a t = []
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
a t = []

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
a t = []

goal:
No subgoals!
[PROOF STEP]
qed