[STATEMENT]
lemma Delay_L3:
 assumes h1:"\<forall>t1 \<le> t. y t1 = []"
        and h2:"Delay y i1 d x i2"
        and h3:"t2 \<le> t + d"
   shows "x t2 = []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x t2 = []
[PROOF STEP]
proof (cases "t2 < d")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. t2 < d \<Longrightarrow> x t2 = []
 2. \<not> t2 < d \<Longrightarrow> x t2 = []
[PROOF STEP]
assume a1:"t2 < d"
[PROOF STATE]
proof (state)
this:
t2 < d

goal (2 subgoals):
 1. t2 < d \<Longrightarrow> x t2 = []
 2. \<not> t2 < d \<Longrightarrow> x t2 = []
[PROOF STEP]
from h2
[PROOF STATE]
proof (chain)
picking this:
Delay y i1 d x i2
[PROOF STEP]
have sg1:"t2 < d \<longrightarrow> x t2 = []"
[PROOF STATE]
proof (prove)
using this:
Delay y i1 d x i2

goal (1 subgoal):
 1. t2 < d \<longrightarrow> x t2 = []
[PROOF STEP]
by (simp add: Delay_def)
[PROOF STATE]
proof (state)
this:
t2 < d \<longrightarrow> x t2 = []

goal (2 subgoals):
 1. t2 < d \<Longrightarrow> x t2 = []
 2. \<not> t2 < d \<Longrightarrow> x t2 = []
[PROOF STEP]
from sg1 and a1
[PROOF STATE]
proof (chain)
picking this:
t2 < d \<longrightarrow> x t2 = []
t2 < d
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
t2 < d \<longrightarrow> x t2 = []
t2 < d

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

goal (1 subgoal):
 1. \<not> t2 < d \<Longrightarrow> x t2 = []
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> t2 < d \<Longrightarrow> x t2 = []
[PROOF STEP]
assume a2:"\<not> t2 < d"
[PROOF STATE]
proof (state)
this:
\<not> t2 < d

goal (1 subgoal):
 1. \<not> t2 < d \<Longrightarrow> x t2 = []
[PROOF STEP]
from h2
[PROOF STATE]
proof (chain)
picking this:
Delay y i1 d x i2
[PROOF STEP]
have sg2:"d \<le> t2 \<longrightarrow> x t2 = y (t2 - d)"
[PROOF STATE]
proof (prove)
using this:
Delay y i1 d x i2

goal (1 subgoal):
 1. d \<le> t2 \<longrightarrow> x t2 = y (t2 - d)
[PROOF STEP]
by (simp add: Delay_def)
[PROOF STATE]
proof (state)
this:
d \<le> t2 \<longrightarrow> x t2 = y (t2 - d)

goal (1 subgoal):
 1. \<not> t2 < d \<Longrightarrow> x t2 = []
[PROOF STEP]
from a2 and sg2
[PROOF STATE]
proof (chain)
picking this:
\<not> t2 < d
d \<le> t2 \<longrightarrow> x t2 = y (t2 - d)
[PROOF STEP]
have sg3:"x t2 = y (t2 - d)"
[PROOF STATE]
proof (prove)
using this:
\<not> t2 < d
d \<le> t2 \<longrightarrow> x t2 = y (t2 - d)

goal (1 subgoal):
 1. x t2 = y (t2 - d)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
x t2 = y (t2 - d)

goal (1 subgoal):
 1. \<not> t2 < d \<Longrightarrow> x t2 = []
[PROOF STEP]
from h1 and a2 and h3 and sg3
[PROOF STATE]
proof (chain)
picking this:
\<forall>t1\<le>t. y t1 = []
\<not> t2 < d
t2 \<le> t + d
x t2 = y (t2 - d)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>t1\<le>t. y t1 = []
\<not> t2 < d
t2 \<le> t + d
x t2 = y (t2 - d)

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

goal:
No subgoals!
[PROOF STEP]
qed