[STATEMENT]
lemma rtrancl_beta_UpdL:
  "\<lbrakk> t \<rightarrow>\<^sub>\<beta>\<^sup>* t'; body u \<rbrakk> \<Longrightarrow> Upd t l u \<rightarrow>\<^sub>\<beta>\<^sup>* Upd t' l u"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>t ->> t'; body u\<rbrakk> \<Longrightarrow> Upd t l u ->> Upd t' l u
[PROOF STEP]
proof (induct t t' rule: rtranclp.induct, simp)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a b c. \<lbrakk>a ->> b; body u \<Longrightarrow> Upd a l u ->> Upd b l u; b -> c; body u\<rbrakk> \<Longrightarrow> Upd a l u ->> Upd c l u
[PROOF STEP]
case (rtrancl_into_rtrancl a b c)
[PROOF STATE]
proof (state)
this:
a ->> b
body u \<Longrightarrow> Upd a l u ->> Upd b l u
b -> c
body u

goal (1 subgoal):
 1. \<And>a b c. \<lbrakk>a ->> b; body u \<Longrightarrow> Upd a l u ->> Upd b l u; b -> c; body u\<rbrakk> \<Longrightarrow> Upd a l u ->> Upd c l u
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
a ->> b
body u \<Longrightarrow> Upd a l u ->> Upd b l u
b -> c
body u

goal (1 subgoal):
 1. Upd a l u ->> Upd c l u
[PROOF STEP]
proof (auto)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>a ->> b; Upd a l u ->> Upd b l u; b -> c; body u\<rbrakk> \<Longrightarrow> Upd a l u ->> Upd c l u
[PROOF STEP]
from \<open>b \<rightarrow>\<^sub>\<beta> c\<close> \<open>body u\<close>
[PROOF STATE]
proof (chain)
picking this:
b -> c
body u
[PROOF STEP]
have "Upd b l u \<rightarrow>\<^sub>\<beta> Upd c l u"
[PROOF STATE]
proof (prove)
using this:
b -> c
body u

goal (1 subgoal):
 1. Upd b l u -> Upd c l u
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Upd b l u -> Upd c l u

goal (1 subgoal):
 1. \<lbrakk>a ->> b; Upd a l u ->> Upd b l u; b -> c; body u\<rbrakk> \<Longrightarrow> Upd a l u ->> Upd c l u
[PROOF STEP]
with rtrancl_into_rtrancl(2)[OF \<open>body u\<close>]
[PROOF STATE]
proof (chain)
picking this:
Upd a l u ->> Upd b l u
Upd b l u -> Upd c l u
[PROOF STEP]
show "Upd a l u \<rightarrow>\<^sub>\<beta>\<^sup>* Upd c l u"
[PROOF STATE]
proof (prove)
using this:
Upd a l u ->> Upd b l u
Upd b l u -> Upd c l u

goal (1 subgoal):
 1. Upd a l u ->> Upd c l u
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Upd a l u ->> Upd c l u

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
Upd a l u ->> Upd c l u

goal:
No subgoals!
[PROOF STEP]
qed