[STATEMENT]
lemma transitions_cons_eq:
  "root \<Midarrow>(x # xs)\<Rightarrow> root'' \<longleftrightarrow> (\<exists>root'. root \<midarrow>x\<rightarrow> root' \<and> root' \<Midarrow>xs\<Rightarrow> root'')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. root \<Midarrow>(x # xs)\<Rightarrow> root'' = (\<exists>root'. root \<midarrow>x\<rightarrow> root' \<and> root' \<Midarrow>xs\<Rightarrow> root'')
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. root \<Midarrow>(x # xs)\<Rightarrow> root'' \<Longrightarrow> \<exists>root'. root \<midarrow>x\<rightarrow> root' \<and> root' \<Midarrow>xs\<Rightarrow> root''
 2. \<exists>root'. root \<midarrow>x\<rightarrow> root' \<and> root' \<Midarrow>xs\<Rightarrow> root'' \<Longrightarrow> root \<Midarrow>(x # xs)\<Rightarrow> root''
[PROOF STEP]
assume "root \<Midarrow>(x # xs)\<Rightarrow> root''"
[PROOF STATE]
proof (state)
this:
root \<Midarrow>(x # xs)\<Rightarrow> root''

goal (2 subgoals):
 1. root \<Midarrow>(x # xs)\<Rightarrow> root'' \<Longrightarrow> \<exists>root'. root \<midarrow>x\<rightarrow> root' \<and> root' \<Midarrow>xs\<Rightarrow> root''
 2. \<exists>root'. root \<midarrow>x\<rightarrow> root' \<and> root' \<Midarrow>xs\<Rightarrow> root'' \<Longrightarrow> root \<Midarrow>(x # xs)\<Rightarrow> root''
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
root \<Midarrow>(x # xs)\<Rightarrow> root''
[PROOF STEP]
show "\<exists>root'. root \<midarrow>x\<rightarrow> root' \<and> root' \<Midarrow>xs\<Rightarrow> root''"
[PROOF STATE]
proof (prove)
using this:
root \<Midarrow>(x # xs)\<Rightarrow> root''

goal (1 subgoal):
 1. \<exists>root'. root \<midarrow>x\<rightarrow> root' \<and> root' \<Midarrow>xs\<Rightarrow> root''
[PROOF STEP]
by cases auto
[PROOF STATE]
proof (state)
this:
\<exists>root'. root \<midarrow>x\<rightarrow> root' \<and> root' \<Midarrow>xs\<Rightarrow> root''

goal (1 subgoal):
 1. \<exists>root'. root \<midarrow>x\<rightarrow> root' \<and> root' \<Midarrow>xs\<Rightarrow> root'' \<Longrightarrow> root \<Midarrow>(x # xs)\<Rightarrow> root''
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>root'. root \<midarrow>x\<rightarrow> root' \<and> root' \<Midarrow>xs\<Rightarrow> root'' \<Longrightarrow> root \<Midarrow>(x # xs)\<Rightarrow> root''
[PROOF STEP]
assume "\<exists>root'. root \<midarrow>x\<rightarrow> root' \<and> root' \<Midarrow>xs\<Rightarrow> root''"
[PROOF STATE]
proof (state)
this:
\<exists>root'. root \<midarrow>x\<rightarrow> root' \<and> root' \<Midarrow>xs\<Rightarrow> root''

goal (1 subgoal):
 1. \<exists>root'. root \<midarrow>x\<rightarrow> root' \<and> root' \<Midarrow>xs\<Rightarrow> root'' \<Longrightarrow> root \<Midarrow>(x # xs)\<Rightarrow> root''
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>root'. root \<midarrow>x\<rightarrow> root' \<and> root' \<Midarrow>xs\<Rightarrow> root''
[PROOF STEP]
show "root \<Midarrow>(x # xs)\<Rightarrow> root''"
[PROOF STATE]
proof (prove)
using this:
\<exists>root'. root \<midarrow>x\<rightarrow> root' \<and> root' \<Midarrow>xs\<Rightarrow> root''

goal (1 subgoal):
 1. root \<Midarrow>(x # xs)\<Rightarrow> root''
[PROOF STEP]
by (blast intro: transitions.cons)
[PROOF STATE]
proof (state)
this:
root \<Midarrow>(x # xs)\<Rightarrow> root''

goal:
No subgoals!
[PROOF STEP]
qed