[STATEMENT]
lemma R_update :
  "R M q q' pP (p@[t]) = (if (target q (p@[t]) = q')
                          then insert (pP@p@[t]) (R M q q' pP p)
                          else (R M q q' pP p))"
  (is "?R1 = ?R2")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. R M q q' pP (p @ [t]) = (if target q (p @ [t]) = q' then insert (pP @ p @ [t]) (R M q q' pP p) else R M q q' pP p)
[PROOF STEP]
proof (cases "(target q (p@[t]) = q')")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. target q (p @ [t]) = q' \<Longrightarrow> R M q q' pP (p @ [t]) = (if target q (p @ [t]) = q' then insert (pP @ p @ [t]) (R M q q' pP p) else R M q q' pP p)
 2. target q (p @ [t]) \<noteq> q' \<Longrightarrow> R M q q' pP (p @ [t]) = (if target q (p @ [t]) = q' then insert (pP @ p @ [t]) (R M q q' pP p) else R M q q' pP p)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
target q (p @ [t]) = q'

goal (2 subgoals):
 1. target q (p @ [t]) = q' \<Longrightarrow> R M q q' pP (p @ [t]) = (if target q (p @ [t]) = q' then insert (pP @ p @ [t]) (R M q q' pP p) else R M q q' pP p)
 2. target q (p @ [t]) \<noteq> q' \<Longrightarrow> R M q q' pP (p @ [t]) = (if target q (p @ [t]) = q' then insert (pP @ p @ [t]) (R M q q' pP p) else R M q q' pP p)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
target q (p @ [t]) = q'
[PROOF STEP]
have *: "?R2 = insert (pP@p@[t]) (R M q q' pP p)"
[PROOF STATE]
proof (prove)
using this:
target q (p @ [t]) = q'

goal (1 subgoal):
 1. (if target q (p @ [t]) = q' then insert (pP @ p @ [t]) (R M q q' pP p) else R M q q' pP p) = insert (pP @ p @ [t]) (R M q q' pP p)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(if target q (p @ [t]) = q' then insert (pP @ p @ [t]) (R M q q' pP p) else R M q q' pP p) = insert (pP @ p @ [t]) (R M q q' pP p)

goal (2 subgoals):
 1. target q (p @ [t]) = q' \<Longrightarrow> R M q q' pP (p @ [t]) = (if target q (p @ [t]) = q' then insert (pP @ p @ [t]) (R M q q' pP p) else R M q q' pP p)
 2. target q (p @ [t]) \<noteq> q' \<Longrightarrow> R M q q' pP (p @ [t]) = (if target q (p @ [t]) = q' then insert (pP @ p @ [t]) (R M q q' pP p) else R M q q' pP p)
[PROOF STEP]
have "\<And> p' . p' \<in> R M q q' pP (p@[t]) \<Longrightarrow> p' \<in> insert (pP@p@[t]) (R M q q' pP p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>p'. p' \<in> R M q q' pP (p @ [t]) \<Longrightarrow> p' \<in> insert (pP @ p @ [t]) (R M q q' pP p)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>p'. p' \<in> R M q q' pP (p @ [t]) \<Longrightarrow> p' \<in> insert (pP @ p @ [t]) (R M q q' pP p)
[PROOF STEP]
fix p'
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>p'. p' \<in> R M q q' pP (p @ [t]) \<Longrightarrow> p' \<in> insert (pP @ p @ [t]) (R M q q' pP p)
[PROOF STEP]
assume "p' \<in> R M q q' pP (p@[t])"
[PROOF STATE]
proof (state)
this:
p' \<in> R M q q' pP (p @ [t])

goal (1 subgoal):
 1. \<And>p'. p' \<in> R M q q' pP (p @ [t]) \<Longrightarrow> p' \<in> insert (pP @ p @ [t]) (R M q q' pP p)
[PROOF STEP]
obtain p'' where "p' = pP @ p''"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>p''. p' = pP @ p'' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using R_component_ob[OF \<open>p' \<in> R M q q' pP (p@[t])\<close>]
[PROOF STATE]
proof (prove)
using this:
(\<And>pR. p' = pP @ pR \<Longrightarrow> ?thesis) \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. (\<And>p''. p' = pP @ p'' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
p' = pP @ p''

goal (1 subgoal):
 1. \<And>p'. p' \<in> R M q q' pP (p @ [t]) \<Longrightarrow> p' \<in> insert (pP @ p @ [t]) (R M q q' pP p)
[PROOF STEP]
obtain p''' where "p'' \<noteq> []" and "target q p'' = q'" and "p @ [t] = p'' @ p'''"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>p'''. \<lbrakk>p'' \<noteq> []; target q p'' = q'; p @ [t] = p'' @ p'''\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using \<open>p' \<in> R M q q' pP (p@[t])\<close>
[PROOF STATE]
proof (prove)
using this:
p' \<in> R M q q' pP (p @ [t])

goal (1 subgoal):
 1. (\<And>p'''. \<lbrakk>p'' \<noteq> []; target q p'' = q'; p @ [t] = p'' @ p'''\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding R_def \<open>p' = pP @ p''\<close>
[PROOF STATE]
proof (prove)
using this:
pP @ p'' \<in> {pP @ p' |p'. p' \<noteq> [] \<and> target q p' = q' \<and> (\<exists>p''. p @ [t] = p' @ p'')}

goal (1 subgoal):
 1. (\<And>p'''. \<lbrakk>p'' \<noteq> []; target q p'' = q'; p @ [t] = p'' @ p'''\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
p'' \<noteq> []
target q p'' = q'
p @ [t] = p'' @ p'''

goal (1 subgoal):
 1. \<And>p'. p' \<in> R M q q' pP (p @ [t]) \<Longrightarrow> p' \<in> insert (pP @ p @ [t]) (R M q q' pP p)
[PROOF STEP]
show "p' \<in> insert (pP@p@[t]) (R M q q' pP p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p' \<in> insert (pP @ p @ [t]) (R M q q' pP p)
[PROOF STEP]
proof (cases p''' rule: rev_cases)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. p''' = [] \<Longrightarrow> p' \<in> insert (pP @ p @ [t]) (R M q q' pP p)
 2. \<And>ys y. p''' = ys @ [y] \<Longrightarrow> p' \<in> insert (pP @ p @ [t]) (R M q q' pP p)
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
p''' = []

goal (2 subgoals):
 1. p''' = [] \<Longrightarrow> p' \<in> insert (pP @ p @ [t]) (R M q q' pP p)
 2. \<And>ys y. p''' = ys @ [y] \<Longrightarrow> p' \<in> insert (pP @ p @ [t]) (R M q q' pP p)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
p''' = []
[PROOF STEP]
have "p' = pP@(p@[t])"
[PROOF STATE]
proof (prove)
using this:
p''' = []

goal (1 subgoal):
 1. p' = pP @ p @ [t]
[PROOF STEP]
using \<open>p' = pP @ p''\<close> \<open>p @ [t] = p'' @ p'''\<close>
[PROOF STATE]
proof (prove)
using this:
p''' = []
p' = pP @ p''
p @ [t] = p'' @ p'''

goal (1 subgoal):
 1. p' = pP @ p @ [t]
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
p' = pP @ p @ [t]

goal (2 subgoals):
 1. p''' = [] \<Longrightarrow> p' \<in> insert (pP @ p @ [t]) (R M q q' pP p)
 2. \<And>ys y. p''' = ys @ [y] \<Longrightarrow> p' \<in> insert (pP @ p @ [t]) (R M q q' pP p)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
p' = pP @ p @ [t]
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
p' = pP @ p @ [t]

goal (1 subgoal):
 1. p' \<in> insert (pP @ p @ [t]) (R M q q' pP p)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
p' \<in> insert (pP @ p @ [t]) (R M q q' pP p)

goal (1 subgoal):
 1. \<And>ys y. p''' = ys @ [y] \<Longrightarrow> p' \<in> insert (pP @ p @ [t]) (R M q q' pP p)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>ys y. p''' = ys @ [y] \<Longrightarrow> p' \<in> insert (pP @ p @ [t]) (R M q q' pP p)
[PROOF STEP]
case (snoc p'''' t')
[PROOF STATE]
proof (state)
this:
p''' = p'''' @ [t']

goal (1 subgoal):
 1. \<And>ys y. p''' = ys @ [y] \<Longrightarrow> p' \<in> insert (pP @ p @ [t]) (R M q q' pP p)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
p''' = p'''' @ [t']
[PROOF STEP]
have "p = p'' @ p''''"
[PROOF STATE]
proof (prove)
using this:
p''' = p'''' @ [t']

goal (1 subgoal):
 1. p = p'' @ p''''
[PROOF STEP]
using \<open>p @ [t] = p'' @ p'''\<close>
[PROOF STATE]
proof (prove)
using this:
p''' = p'''' @ [t']
p @ [t] = p'' @ p'''

goal (1 subgoal):
 1. p = p'' @ p''''
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
p = p'' @ p''''

goal (1 subgoal):
 1. \<And>ys y. p''' = ys @ [y] \<Longrightarrow> p' \<in> insert (pP @ p @ [t]) (R M q q' pP p)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
p = p'' @ p''''
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
p = p'' @ p''''

goal (1 subgoal):
 1. p' \<in> insert (pP @ p @ [t]) (R M q q' pP p)
[PROOF STEP]
unfolding R_def
[PROOF STATE]
proof (prove)
using this:
p = p'' @ p''''

goal (1 subgoal):
 1. p' \<in> insert (pP @ p @ [t]) {pP @ p' |p'. p' \<noteq> [] \<and> target q p' = q' \<and> (\<exists>p''. p = p' @ p'')}
[PROOF STEP]
using \<open>p'' \<noteq> []\<close> \<open>target q p'' = q'\<close>
[PROOF STATE]
proof (prove)
using this:
p = p'' @ p''''
p'' \<noteq> []
target q p'' = q'

goal (1 subgoal):
 1. p' \<in> insert (pP @ p @ [t]) {pP @ p' |p'. p' \<noteq> [] \<and> target q p' = q' \<and> (\<exists>p''. p = p' @ p'')}
[PROOF STEP]
by (simp add: \<open>p' = pP @ p''\<close>)
[PROOF STATE]
proof (state)
this:
p' \<in> insert (pP @ p @ [t]) (R M q q' pP p)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
p' \<in> insert (pP @ p @ [t]) (R M q q' pP p)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
?p' \<in> R M q q' pP (p @ [t]) \<Longrightarrow> ?p' \<in> insert (pP @ p @ [t]) (R M q q' pP p)

goal (2 subgoals):
 1. target q (p @ [t]) = q' \<Longrightarrow> R M q q' pP (p @ [t]) = (if target q (p @ [t]) = q' then insert (pP @ p @ [t]) (R M q q' pP p) else R M q q' pP p)
 2. target q (p @ [t]) \<noteq> q' \<Longrightarrow> R M q q' pP (p @ [t]) = (if target q (p @ [t]) = q' then insert (pP @ p @ [t]) (R M q q' pP p) else R M q q' pP p)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
?p' \<in> R M q q' pP (p @ [t]) \<Longrightarrow> ?p' \<in> insert (pP @ p @ [t]) (R M q q' pP p)

goal (2 subgoals):
 1. target q (p @ [t]) = q' \<Longrightarrow> R M q q' pP (p @ [t]) = (if target q (p @ [t]) = q' then insert (pP @ p @ [t]) (R M q q' pP p) else R M q q' pP p)
 2. target q (p @ [t]) \<noteq> q' \<Longrightarrow> R M q q' pP (p @ [t]) = (if target q (p @ [t]) = q' then insert (pP @ p @ [t]) (R M q q' pP p) else R M q q' pP p)
[PROOF STEP]
have "\<And> p' . p' \<in> insert (pP@p@[t]) (R M q q' pP p) \<Longrightarrow> p' \<in> R M q q' pP (p@[t])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>p'. p' \<in> insert (pP @ p @ [t]) (R M q q' pP p) \<Longrightarrow> p' \<in> R M q q' pP (p @ [t])
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>p'. p' \<in> insert (pP @ p @ [t]) (R M q q' pP p) \<Longrightarrow> p' \<in> R M q q' pP (p @ [t])
[PROOF STEP]
fix p'
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>p'. p' \<in> insert (pP @ p @ [t]) (R M q q' pP p) \<Longrightarrow> p' \<in> R M q q' pP (p @ [t])
[PROOF STEP]
assume "p' \<in> insert (pP@p@[t]) (R M q q' pP p)"
[PROOF STATE]
proof (state)
this:
p' \<in> insert (pP @ p @ [t]) (R M q q' pP p)

goal (1 subgoal):
 1. \<And>p'. p' \<in> insert (pP @ p @ [t]) (R M q q' pP p) \<Longrightarrow> p' \<in> R M q q' pP (p @ [t])
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
p' \<in> insert (pP @ p @ [t]) (R M q q' pP p)
[PROOF STEP]
consider (a) "p' = (pP@p@[t])" | (b) "p' \<in> (R M q q' pP p)"
[PROOF STATE]
proof (prove)
using this:
p' \<in> insert (pP @ p @ [t]) (R M q q' pP p)

goal (1 subgoal):
 1. \<lbrakk>p' = pP @ p @ [t] \<Longrightarrow> thesis; p' \<in> R M q q' pP p \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<lbrakk>p' = pP @ p @ [t] \<Longrightarrow> ?thesis; p' \<in> R M q q' pP p \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. \<And>p'. p' \<in> insert (pP @ p @ [t]) (R M q q' pP p) \<Longrightarrow> p' \<in> R M q q' pP (p @ [t])
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>p' = pP @ p @ [t] \<Longrightarrow> ?thesis; p' \<in> R M q q' pP p \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis
[PROOF STEP]
show "p' \<in> R M q q' pP (p@[t])"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>p' = pP @ p @ [t] \<Longrightarrow> ?thesis; p' \<in> R M q q' pP p \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. p' \<in> R M q q' pP (p @ [t])
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. p' = pP @ p @ [t] \<Longrightarrow> p' \<in> R M q q' pP (p @ [t])
 2. p' \<in> R M q q' pP p \<Longrightarrow> p' \<in> R M q q' pP (p @ [t])
[PROOF STEP]
case a
[PROOF STATE]
proof (state)
this:
p' = pP @ p @ [t]

goal (2 subgoals):
 1. p' = pP @ p @ [t] \<Longrightarrow> p' \<in> R M q q' pP (p @ [t])
 2. p' \<in> R M q q' pP p \<Longrightarrow> p' \<in> R M q q' pP (p @ [t])
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
p' = pP @ p @ [t]
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
p' = pP @ p @ [t]

goal (1 subgoal):
 1. p' \<in> R M q q' pP (p @ [t])
[PROOF STEP]
using True
[PROOF STATE]
proof (prove)
using this:
p' = pP @ p @ [t]
target q (p @ [t]) = q'

goal (1 subgoal):
 1. p' \<in> R M q q' pP (p @ [t])
[PROOF STEP]
unfolding R_def
[PROOF STATE]
proof (prove)
using this:
p' = pP @ p @ [t]
target q (p @ [t]) = q'

goal (1 subgoal):
 1. p' \<in> {pP @ p' |p'. p' \<noteq> [] \<and> target q p' = q' \<and> (\<exists>p''. p @ [t] = p' @ p'')}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
p' \<in> R M q q' pP (p @ [t])

goal (1 subgoal):
 1. p' \<in> R M q q' pP p \<Longrightarrow> p' \<in> R M q q' pP (p @ [t])
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. p' \<in> R M q q' pP p \<Longrightarrow> p' \<in> R M q q' pP (p @ [t])
[PROOF STEP]
case b
[PROOF STATE]
proof (state)
this:
p' \<in> R M q q' pP p

goal (1 subgoal):
 1. p' \<in> R M q q' pP p \<Longrightarrow> p' \<in> R M q q' pP (p @ [t])
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
p' \<in> R M q q' pP p
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
p' \<in> R M q q' pP p

goal (1 subgoal):
 1. p' \<in> R M q q' pP (p @ [t])
[PROOF STEP]
unfolding R_def
[PROOF STATE]
proof (prove)
using this:
p' \<in> {pP @ p' |p'. p' \<noteq> [] \<and> target q p' = q' \<and> (\<exists>p''. p = p' @ p'')}

goal (1 subgoal):
 1. p' \<in> {pP @ p' |p'. p' \<noteq> [] \<and> target q p' = q' \<and> (\<exists>p''. p @ [t] = p' @ p'')}
[PROOF STEP]
using append.assoc
[PROOF STATE]
proof (prove)
using this:
p' \<in> {pP @ p' |p'. p' \<noteq> [] \<and> target q p' = q' \<and> (\<exists>p''. p = p' @ p'')}
(?a @ ?b) @ ?c = ?a @ ?b @ ?c

goal (1 subgoal):
 1. p' \<in> {pP @ p' |p'. p' \<noteq> [] \<and> target q p' = q' \<and> (\<exists>p''. p @ [t] = p' @ p'')}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
p' \<in> R M q q' pP (p @ [t])

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
p' \<in> R M q q' pP (p @ [t])

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
?p' \<in> insert (pP @ p @ [t]) (R M q q' pP p) \<Longrightarrow> ?p' \<in> R M q q' pP (p @ [t])

goal (2 subgoals):
 1. target q (p @ [t]) = q' \<Longrightarrow> R M q q' pP (p @ [t]) = (if target q (p @ [t]) = q' then insert (pP @ p @ [t]) (R M q q' pP p) else R M q q' pP p)
 2. target q (p @ [t]) \<noteq> q' \<Longrightarrow> R M q q' pP (p @ [t]) = (if target q (p @ [t]) = q' then insert (pP @ p @ [t]) (R M q q' pP p) else R M q q' pP p)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
?p' \<in> R M q q' pP (p @ [t]) \<Longrightarrow> ?p' \<in> insert (pP @ p @ [t]) (R M q q' pP p)
?p' \<in> insert (pP @ p @ [t]) (R M q q' pP p) \<Longrightarrow> ?p' \<in> R M q q' pP (p @ [t])
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
?p' \<in> R M q q' pP (p @ [t]) \<Longrightarrow> ?p' \<in> insert (pP @ p @ [t]) (R M q q' pP p)
?p' \<in> insert (pP @ p @ [t]) (R M q q' pP p) \<Longrightarrow> ?p' \<in> R M q q' pP (p @ [t])

goal (1 subgoal):
 1. R M q q' pP (p @ [t]) = (if target q (p @ [t]) = q' then insert (pP @ p @ [t]) (R M q q' pP p) else R M q q' pP p)
[PROOF STEP]
unfolding *
[PROOF STATE]
proof (prove)
using this:
?p' \<in> R M q q' pP (p @ [t]) \<Longrightarrow> ?p' \<in> insert (pP @ p @ [t]) (R M q q' pP p)
?p' \<in> insert (pP @ p @ [t]) (R M q q' pP p) \<Longrightarrow> ?p' \<in> R M q q' pP (p @ [t])

goal (1 subgoal):
 1. R M q q' pP (p @ [t]) = insert (pP @ p @ [t]) (R M q q' pP p)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
R M q q' pP (p @ [t]) = (if target q (p @ [t]) = q' then insert (pP @ p @ [t]) (R M q q' pP p) else R M q q' pP p)

goal (1 subgoal):
 1. target q (p @ [t]) \<noteq> q' \<Longrightarrow> R M q q' pP (p @ [t]) = (if target q (p @ [t]) = q' then insert (pP @ p @ [t]) (R M q q' pP p) else R M q q' pP p)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. target q (p @ [t]) \<noteq> q' \<Longrightarrow> R M q q' pP (p @ [t]) = (if target q (p @ [t]) = q' then insert (pP @ p @ [t]) (R M q q' pP p) else R M q q' pP p)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
target q (p @ [t]) \<noteq> q'

goal (1 subgoal):
 1. target q (p @ [t]) \<noteq> q' \<Longrightarrow> R M q q' pP (p @ [t]) = (if target q (p @ [t]) = q' then insert (pP @ p @ [t]) (R M q q' pP p) else R M q q' pP p)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
target q (p @ [t]) \<noteq> q'
[PROOF STEP]
have *: "?R2 = (R M q q' pP p)"
[PROOF STATE]
proof (prove)
using this:
target q (p @ [t]) \<noteq> q'

goal (1 subgoal):
 1. (if target q (p @ [t]) = q' then insert (pP @ p @ [t]) (R M q q' pP p) else R M q q' pP p) = R M q q' pP p
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(if target q (p @ [t]) = q' then insert (pP @ p @ [t]) (R M q q' pP p) else R M q q' pP p) = R M q q' pP p

goal (1 subgoal):
 1. target q (p @ [t]) \<noteq> q' \<Longrightarrow> R M q q' pP (p @ [t]) = (if target q (p @ [t]) = q' then insert (pP @ p @ [t]) (R M q q' pP p) else R M q q' pP p)
[PROOF STEP]
have "\<And> p' . p' \<in> R M q q' pP (p@[t]) \<Longrightarrow> p' \<in> (R M q q' pP p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>p'. p' \<in> R M q q' pP (p @ [t]) \<Longrightarrow> p' \<in> R M q q' pP p
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>p'. p' \<in> R M q q' pP (p @ [t]) \<Longrightarrow> p' \<in> R M q q' pP p
[PROOF STEP]
fix p'
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>p'. p' \<in> R M q q' pP (p @ [t]) \<Longrightarrow> p' \<in> R M q q' pP p
[PROOF STEP]
assume "p' \<in> R M q q' pP (p@[t])"
[PROOF STATE]
proof (state)
this:
p' \<in> R M q q' pP (p @ [t])

goal (1 subgoal):
 1. \<And>p'. p' \<in> R M q q' pP (p @ [t]) \<Longrightarrow> p' \<in> R M q q' pP p
[PROOF STEP]
obtain p'' where "p' = pP @ p''"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>p''. p' = pP @ p'' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using R_component_ob[OF \<open>p' \<in> R M q q' pP (p@[t])\<close>]
[PROOF STATE]
proof (prove)
using this:
(\<And>pR. p' = pP @ pR \<Longrightarrow> ?thesis) \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. (\<And>p''. p' = pP @ p'' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
p' = pP @ p''

goal (1 subgoal):
 1. \<And>p'. p' \<in> R M q q' pP (p @ [t]) \<Longrightarrow> p' \<in> R M q q' pP p
[PROOF STEP]
obtain p''' where "p'' \<noteq> []" and "target q p'' = q'" and "p @ [t] = p'' @ p'''"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>p'''. \<lbrakk>p'' \<noteq> []; target q p'' = q'; p @ [t] = p'' @ p'''\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using \<open>p' \<in> R M q q' pP (p@[t])\<close>
[PROOF STATE]
proof (prove)
using this:
p' \<in> R M q q' pP (p @ [t])

goal (1 subgoal):
 1. (\<And>p'''. \<lbrakk>p'' \<noteq> []; target q p'' = q'; p @ [t] = p'' @ p'''\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding R_def \<open>p' = pP @ p''\<close>
[PROOF STATE]
proof (prove)
using this:
pP @ p'' \<in> {pP @ p' |p'. p' \<noteq> [] \<and> target q p' = q' \<and> (\<exists>p''. p @ [t] = p' @ p'')}

goal (1 subgoal):
 1. (\<And>p'''. \<lbrakk>p'' \<noteq> []; target q p'' = q'; p @ [t] = p'' @ p'''\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
p'' \<noteq> []
target q p'' = q'
p @ [t] = p'' @ p'''

goal (1 subgoal):
 1. \<And>p'. p' \<in> R M q q' pP (p @ [t]) \<Longrightarrow> p' \<in> R M q q' pP p
[PROOF STEP]
show "p' \<in> (R M q q' pP p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p' \<in> R M q q' pP p
[PROOF STEP]
proof (cases p''' rule: rev_cases)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. p''' = [] \<Longrightarrow> p' \<in> R M q q' pP p
 2. \<And>ys y. p''' = ys @ [y] \<Longrightarrow> p' \<in> R M q q' pP p
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
p''' = []

goal (2 subgoals):
 1. p''' = [] \<Longrightarrow> p' \<in> R M q q' pP p
 2. \<And>ys y. p''' = ys @ [y] \<Longrightarrow> p' \<in> R M q q' pP p
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
p''' = []
[PROOF STEP]
have "p' = pP@(p@[t])"
[PROOF STATE]
proof (prove)
using this:
p''' = []

goal (1 subgoal):
 1. p' = pP @ p @ [t]
[PROOF STEP]
using \<open>p' = pP @ p''\<close> \<open>p @ [t] = p'' @ p'''\<close>
[PROOF STATE]
proof (prove)
using this:
p''' = []
p' = pP @ p''
p @ [t] = p'' @ p'''

goal (1 subgoal):
 1. p' = pP @ p @ [t]
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
p' = pP @ p @ [t]

goal (2 subgoals):
 1. p''' = [] \<Longrightarrow> p' \<in> R M q q' pP p
 2. \<And>ys y. p''' = ys @ [y] \<Longrightarrow> p' \<in> R M q q' pP p
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
p' = pP @ p @ [t]
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
p' = pP @ p @ [t]

goal (1 subgoal):
 1. p' \<in> R M q q' pP p
[PROOF STEP]
using False \<open>p @ [t] = p'' @ p'''\<close> \<open>target q p'' = q'\<close> local.Nil
[PROOF STATE]
proof (prove)
using this:
p' = pP @ p @ [t]
target q (p @ [t]) \<noteq> q'
p @ [t] = p'' @ p'''
target q p'' = q'
p''' = []

goal (1 subgoal):
 1. p' \<in> R M q q' pP p
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
p' \<in> R M q q' pP p

goal (1 subgoal):
 1. \<And>ys y. p''' = ys @ [y] \<Longrightarrow> p' \<in> R M q q' pP p
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>ys y. p''' = ys @ [y] \<Longrightarrow> p' \<in> R M q q' pP p
[PROOF STEP]
case (snoc p'''' t')
[PROOF STATE]
proof (state)
this:
p''' = p'''' @ [t']

goal (1 subgoal):
 1. \<And>ys y. p''' = ys @ [y] \<Longrightarrow> p' \<in> R M q q' pP p
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
p''' = p'''' @ [t']
[PROOF STEP]
have "p = p'' @ p''''"
[PROOF STATE]
proof (prove)
using this:
p''' = p'''' @ [t']

goal (1 subgoal):
 1. p = p'' @ p''''
[PROOF STEP]
using \<open>p @ [t] = p'' @ p'''\<close>
[PROOF STATE]
proof (prove)
using this:
p''' = p'''' @ [t']
p @ [t] = p'' @ p'''

goal (1 subgoal):
 1. p = p'' @ p''''
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
p = p'' @ p''''

goal (1 subgoal):
 1. \<And>ys y. p''' = ys @ [y] \<Longrightarrow> p' \<in> R M q q' pP p
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
p = p'' @ p''''
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
p = p'' @ p''''

goal (1 subgoal):
 1. p' \<in> R M q q' pP p
[PROOF STEP]
unfolding R_def
[PROOF STATE]
proof (prove)
using this:
p = p'' @ p''''

goal (1 subgoal):
 1. p' \<in> {pP @ p' |p'. p' \<noteq> [] \<and> target q p' = q' \<and> (\<exists>p''. p = p' @ p'')}
[PROOF STEP]
using \<open>p'' \<noteq> []\<close> \<open>target q p'' = q'\<close>
[PROOF STATE]
proof (prove)
using this:
p = p'' @ p''''
p'' \<noteq> []
target q p'' = q'

goal (1 subgoal):
 1. p' \<in> {pP @ p' |p'. p' \<noteq> [] \<and> target q p' = q' \<and> (\<exists>p''. p = p' @ p'')}
[PROOF STEP]
by (simp add: \<open>p' = pP @ p''\<close>)
[PROOF STATE]
proof (state)
this:
p' \<in> R M q q' pP p

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
p' \<in> R M q q' pP p

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
?p' \<in> R M q q' pP (p @ [t]) \<Longrightarrow> ?p' \<in> R M q q' pP p

goal (1 subgoal):
 1. target q (p @ [t]) \<noteq> q' \<Longrightarrow> R M q q' pP (p @ [t]) = (if target q (p @ [t]) = q' then insert (pP @ p @ [t]) (R M q q' pP p) else R M q q' pP p)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
?p' \<in> R M q q' pP (p @ [t]) \<Longrightarrow> ?p' \<in> R M q q' pP p

goal (1 subgoal):
 1. target q (p @ [t]) \<noteq> q' \<Longrightarrow> R M q q' pP (p @ [t]) = (if target q (p @ [t]) = q' then insert (pP @ p @ [t]) (R M q q' pP p) else R M q q' pP p)
[PROOF STEP]
have "\<And> p' . p' \<in> (R M q q' pP p) \<Longrightarrow> p' \<in> R M q q' pP (p@[t])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>p'. p' \<in> R M q q' pP p \<Longrightarrow> p' \<in> R M q q' pP (p @ [t])
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>p'. p' \<in> R M q q' pP p \<Longrightarrow> p' \<in> R M q q' pP (p @ [t])
[PROOF STEP]
fix p'
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>p'. p' \<in> R M q q' pP p \<Longrightarrow> p' \<in> R M q q' pP (p @ [t])
[PROOF STEP]
assume "p' \<in> (R M q q' pP p)"
[PROOF STATE]
proof (state)
this:
p' \<in> R M q q' pP p

goal (1 subgoal):
 1. \<And>p'. p' \<in> R M q q' pP p \<Longrightarrow> p' \<in> R M q q' pP (p @ [t])
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
p' \<in> R M q q' pP p
[PROOF STEP]
show "p' \<in> R M q q' pP (p@[t])"
[PROOF STATE]
proof (prove)
using this:
p' \<in> R M q q' pP p

goal (1 subgoal):
 1. p' \<in> R M q q' pP (p @ [t])
[PROOF STEP]
unfolding R_def
[PROOF STATE]
proof (prove)
using this:
p' \<in> {pP @ p' |p'. p' \<noteq> [] \<and> target q p' = q' \<and> (\<exists>p''. p = p' @ p'')}

goal (1 subgoal):
 1. p' \<in> {pP @ p' |p'. p' \<noteq> [] \<and> target q p' = q' \<and> (\<exists>p''. p @ [t] = p' @ p'')}
[PROOF STEP]
using append.assoc
[PROOF STATE]
proof (prove)
using this:
p' \<in> {pP @ p' |p'. p' \<noteq> [] \<and> target q p' = q' \<and> (\<exists>p''. p = p' @ p'')}
(?a @ ?b) @ ?c = ?a @ ?b @ ?c

goal (1 subgoal):
 1. p' \<in> {pP @ p' |p'. p' \<noteq> [] \<and> target q p' = q' \<and> (\<exists>p''. p @ [t] = p' @ p'')}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
p' \<in> R M q q' pP (p @ [t])

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
?p' \<in> R M q q' pP p \<Longrightarrow> ?p' \<in> R M q q' pP (p @ [t])

goal (1 subgoal):
 1. target q (p @ [t]) \<noteq> q' \<Longrightarrow> R M q q' pP (p @ [t]) = (if target q (p @ [t]) = q' then insert (pP @ p @ [t]) (R M q q' pP p) else R M q q' pP p)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
?p' \<in> R M q q' pP (p @ [t]) \<Longrightarrow> ?p' \<in> R M q q' pP p
?p' \<in> R M q q' pP p \<Longrightarrow> ?p' \<in> R M q q' pP (p @ [t])
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
?p' \<in> R M q q' pP (p @ [t]) \<Longrightarrow> ?p' \<in> R M q q' pP p
?p' \<in> R M q q' pP p \<Longrightarrow> ?p' \<in> R M q q' pP (p @ [t])

goal (1 subgoal):
 1. R M q q' pP (p @ [t]) = (if target q (p @ [t]) = q' then insert (pP @ p @ [t]) (R M q q' pP p) else R M q q' pP p)
[PROOF STEP]
unfolding *
[PROOF STATE]
proof (prove)
using this:
?p' \<in> R M q q' pP (p @ [t]) \<Longrightarrow> ?p' \<in> R M q q' pP p
?p' \<in> R M q q' pP p \<Longrightarrow> ?p' \<in> R M q q' pP (p @ [t])

goal (1 subgoal):
 1. R M q q' pP (p @ [t]) = R M q q' pP p
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
R M q q' pP (p @ [t]) = (if target q (p @ [t]) = q' then insert (pP @ p @ [t]) (R M q q' pP p) else R M q q' pP p)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma R_union_card_is_suffix_length :
  assumes "path M (initial M) pP"
  and     "path M (target (initial M) pP) p"
shows "(\<Sum> q \<in> states M . card (R M (target (initial M) pP) q pP p)) = length p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>q\<in>FSM.states M. card (R M (target (FSM.initial M) pP) q pP p)) = length p
[PROOF STEP]
using assms(2)
[PROOF STATE]
proof (prove)
using this:
path M (target (FSM.initial M) pP) p

goal (1 subgoal):
 1. (\<Sum>q\<in>FSM.states M. card (R M (target (FSM.initial M) pP) q pP p)) = length p
[PROOF STEP]
proof (induction p rule: rev_induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. path M (target (FSM.initial M) pP) [] \<Longrightarrow> (\<Sum>q\<in>FSM.states M. card (R M (target (FSM.initial M) pP) q pP [])) = length []
 2. \<And>x xs. \<lbrakk>path M (target (FSM.initial M) pP) xs \<Longrightarrow> (\<Sum>q\<in>FSM.states M. card (R M (target (FSM.initial M) pP) q pP xs)) = length xs; path M (target (FSM.initial M) pP) (xs @ [x])\<rbrakk> \<Longrightarrow> (\<Sum>q\<in>FSM.states M. card (R M (target (FSM.initial M) pP) q pP (xs @ [x]))) = length (xs @ [x])
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
path M (target (FSM.initial M) pP) []

goal (2 subgoals):
 1. path M (target (FSM.initial M) pP) [] \<Longrightarrow> (\<Sum>q\<in>FSM.states M. card (R M (target (FSM.initial M) pP) q pP [])) = length []
 2. \<And>x xs. \<lbrakk>path M (target (FSM.initial M) pP) xs \<Longrightarrow> (\<Sum>q\<in>FSM.states M. card (R M (target (FSM.initial M) pP) q pP xs)) = length xs; path M (target (FSM.initial M) pP) (xs @ [x])\<rbrakk> \<Longrightarrow> (\<Sum>q\<in>FSM.states M. card (R M (target (FSM.initial M) pP) q pP (xs @ [x]))) = length (xs @ [x])
[PROOF STEP]
have "\<And> q' . R M (target (initial M) pP) q' pP [] = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>q'. R M (target (FSM.initial M) pP) q' pP [] = {}
[PROOF STEP]
unfolding R_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>q'. {pP @ p' |p'. p' \<noteq> [] \<and> target (target (FSM.initial M) pP) p' = q' \<and> (\<exists>p''. [] = p' @ p'')} = {}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
R M (target (FSM.initial M) pP) ?q' pP [] = {}

goal (2 subgoals):
 1. path M (target (FSM.initial M) pP) [] \<Longrightarrow> (\<Sum>q\<in>FSM.states M. card (R M (target (FSM.initial M) pP) q pP [])) = length []
 2. \<And>x xs. \<lbrakk>path M (target (FSM.initial M) pP) xs \<Longrightarrow> (\<Sum>q\<in>FSM.states M. card (R M (target (FSM.initial M) pP) q pP xs)) = length xs; path M (target (FSM.initial M) pP) (xs @ [x])\<rbrakk> \<Longrightarrow> (\<Sum>q\<in>FSM.states M. card (R M (target (FSM.initial M) pP) q pP (xs @ [x]))) = length (xs @ [x])
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
R M (target (FSM.initial M) pP) ?q' pP [] = {}
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
R M (target (FSM.initial M) pP) ?q' pP [] = {}

goal (1 subgoal):
 1. (\<Sum>q\<in>FSM.states M. card (R M (target (FSM.initial M) pP) q pP [])) = length []
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<Sum>q\<in>FSM.states M. card (R M (target (FSM.initial M) pP) q pP [])) = length []

goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>path M (target (FSM.initial M) pP) xs \<Longrightarrow> (\<Sum>q\<in>FSM.states M. card (R M (target (FSM.initial M) pP) q pP xs)) = length xs; path M (target (FSM.initial M) pP) (xs @ [x])\<rbrakk> \<Longrightarrow> (\<Sum>q\<in>FSM.states M. card (R M (target (FSM.initial M) pP) q pP (xs @ [x]))) = length (xs @ [x])
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>path M (target (FSM.initial M) pP) xs \<Longrightarrow> (\<Sum>q\<in>FSM.states M. card (R M (target (FSM.initial M) pP) q pP xs)) = length xs; path M (target (FSM.initial M) pP) (xs @ [x])\<rbrakk> \<Longrightarrow> (\<Sum>q\<in>FSM.states M. card (R M (target (FSM.initial M) pP) q pP (xs @ [x]))) = length (xs @ [x])
[PROOF STEP]
case (snoc t p)
[PROOF STATE]
proof (state)
this:
path M (target (FSM.initial M) pP) p \<Longrightarrow> (\<Sum>q\<in>FSM.states M. card (R M (target (FSM.initial M) pP) q pP p)) = length p
path M (target (FSM.initial M) pP) (p @ [t])

goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>path M (target (FSM.initial M) pP) xs \<Longrightarrow> (\<Sum>q\<in>FSM.states M. card (R M (target (FSM.initial M) pP) q pP xs)) = length xs; path M (target (FSM.initial M) pP) (xs @ [x])\<rbrakk> \<Longrightarrow> (\<Sum>q\<in>FSM.states M. card (R M (target (FSM.initial M) pP) q pP (xs @ [x]))) = length (xs @ [x])
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
path M (target (FSM.initial M) pP) p \<Longrightarrow> (\<Sum>q\<in>FSM.states M. card (R M (target (FSM.initial M) pP) q pP p)) = length p
path M (target (FSM.initial M) pP) (p @ [t])
[PROOF STEP]
have "path M (target (initial M) pP) p"
[PROOF STATE]
proof (prove)
using this:
path M (target (FSM.initial M) pP) p \<Longrightarrow> (\<Sum>q\<in>FSM.states M. card (R M (target (FSM.initial M) pP) q pP p)) = length p
path M (target (FSM.initial M) pP) (p @ [t])

goal (1 subgoal):
 1. path M (target (FSM.initial M) pP) p
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
path M (target (FSM.initial M) pP) p

goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>path M (target (FSM.initial M) pP) xs \<Longrightarrow> (\<Sum>q\<in>FSM.states M. card (R M (target (FSM.initial M) pP) q pP xs)) = length xs; path M (target (FSM.initial M) pP) (xs @ [x])\<rbrakk> \<Longrightarrow> (\<Sum>q\<in>FSM.states M. card (R M (target (FSM.initial M) pP) q pP (xs @ [x]))) = length (xs @ [x])
[PROOF STEP]
let ?q = "(target (initial M) pP)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>path M (target (FSM.initial M) pP) xs \<Longrightarrow> (\<Sum>q\<in>FSM.states M. card (R M (target (FSM.initial M) pP) q pP xs)) = length xs; path M (target (FSM.initial M) pP) (xs @ [x])\<rbrakk> \<Longrightarrow> (\<Sum>q\<in>FSM.states M. card (R M (target (FSM.initial M) pP) q pP (xs @ [x]))) = length (xs @ [x])
[PROOF STEP]
let ?q' = "target ?q (p @ [t])"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>path M (target (FSM.initial M) pP) xs \<Longrightarrow> (\<Sum>q\<in>FSM.states M. card (R M (target (FSM.initial M) pP) q pP xs)) = length xs; path M (target (FSM.initial M) pP) (xs @ [x])\<rbrakk> \<Longrightarrow> (\<Sum>q\<in>FSM.states M. card (R M (target (FSM.initial M) pP) q pP (xs @ [x]))) = length (xs @ [x])
[PROOF STEP]
have "\<And> q . q \<noteq> ?q' \<Longrightarrow> R M ?q q pP (p@[t]) = R M ?q q pP p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>q. q \<noteq> target (target (FSM.initial M) pP) (p @ [t]) \<Longrightarrow> R M (target (FSM.initial M) pP) q pP (p @ [t]) = R M (target (FSM.initial M) pP) q pP p
[PROOF STEP]
using R_update[of M ?q _ pP p t]
[PROOF STATE]
proof (prove)
using this:
R M (target (FSM.initial M) pP) ?q' pP (p @ [t]) = (if target (target (FSM.initial M) pP) (p @ [t]) = ?q' then insert (pP @ p @ [t]) (R M (target (FSM.initial M) pP) ?q' pP p) else R M (target (FSM.initial M) pP) ?q' pP p)

goal (1 subgoal):
 1. \<And>q. q \<noteq> target (target (FSM.initial M) pP) (p @ [t]) \<Longrightarrow> R M (target (FSM.initial M) pP) q pP (p @ [t]) = R M (target (FSM.initial M) pP) q pP p
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
?q \<noteq> target (target (FSM.initial M) pP) (p @ [t]) \<Longrightarrow> R M (target (FSM.initial M) pP) ?q pP (p @ [t]) = R M (target (FSM.initial M) pP) ?q pP p

goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>path M (target (FSM.initial M) pP) xs \<Longrightarrow> (\<Sum>q\<in>FSM.states M. card (R M (target (FSM.initial M) pP) q pP xs)) = length xs; path M (target (FSM.initial M) pP) (xs @ [x])\<rbrakk> \<Longrightarrow> (\<Sum>q\<in>FSM.states M. card (R M (target (FSM.initial M) pP) q pP (xs @ [x]))) = length (xs @ [x])
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
?q \<noteq> target (target (FSM.initial M) pP) (p @ [t]) \<Longrightarrow> R M (target (FSM.initial M) pP) ?q pP (p @ [t]) = R M (target (FSM.initial M) pP) ?q pP p
[PROOF STEP]
have *: "(\<Sum> q \<in> states M - {?q'} . card (R M (target (initial M) pP) q pP (p@[t])))
                  = (\<Sum> q \<in> states M - {?q'} . card (R M (target (initial M) pP) q pP p))"
[PROOF STATE]
proof (prove)
using this:
?q \<noteq> target (target (FSM.initial M) pP) (p @ [t]) \<Longrightarrow> R M (target (FSM.initial M) pP) ?q pP (p @ [t]) = R M (target (FSM.initial M) pP) ?q pP p

goal (1 subgoal):
 1. (\<Sum>q\<in>FSM.states M - {target (target (FSM.initial M) pP) (p @ [t])}. card (R M (target (FSM.initial M) pP) q pP (p @ [t]))) = (\<Sum>q\<in>FSM.states M - {target (target (FSM.initial M) pP) (p @ [t])}. card (R M (target (FSM.initial M) pP) q pP p))
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
(\<Sum>q\<in>FSM.states M - {target (target (FSM.initial M) pP) (p @ [t])}. card (R M (target (FSM.initial M) pP) q pP (p @ [t]))) = (\<Sum>q\<in>FSM.states M - {target (target (FSM.initial M) pP) (p @ [t])}. card (R M (target (FSM.initial M) pP) q pP p))

goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>path M (target (FSM.initial M) pP) xs \<Longrightarrow> (\<Sum>q\<in>FSM.states M. card (R M (target (FSM.initial M) pP) q pP xs)) = length xs; path M (target (FSM.initial M) pP) (xs @ [x])\<rbrakk> \<Longrightarrow> (\<Sum>q\<in>FSM.states M. card (R M (target (FSM.initial M) pP) q pP (xs @ [x]))) = length (xs @ [x])
[PROOF STEP]
have "R M ?q ?q' pP (p@[t]) = insert (pP@p@[t]) (R M ?q ?q' pP p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. R M (target (FSM.initial M) pP) (target (target (FSM.initial M) pP) (p @ [t])) pP (p @ [t]) = insert (pP @ p @ [t]) (R M (target (FSM.initial M) pP) (target (target (FSM.initial M) pP) (p @ [t])) pP p)
[PROOF STEP]
using R_update[of M ?q ?q' pP p t]
[PROOF STATE]
proof (prove)
using this:
R M (target (FSM.initial M) pP) (target (target (FSM.initial M) pP) (p @ [t])) pP (p @ [t]) = (if target (target (FSM.initial M) pP) (p @ [t]) = target (target (FSM.initial M) pP) (p @ [t]) then insert (pP @ p @ [t]) (R M (target (FSM.initial M) pP) (target (target (FSM.initial M) pP) (p @ [t])) pP p) else R M (target (FSM.initial M) pP) (target (target (FSM.initial M) pP) (p @ [t])) pP p)

goal (1 subgoal):
 1. R M (target (FSM.initial M) pP) (target (target (FSM.initial M) pP) (p @ [t])) pP (p @ [t]) = insert (pP @ p @ [t]) (R M (target (FSM.initial M) pP) (target (target (FSM.initial M) pP) (p @ [t])) pP p)
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
R M (target (FSM.initial M) pP) (target (target (FSM.initial M) pP) (p @ [t])) pP (p @ [t]) = insert (pP @ p @ [t]) (R M (target (FSM.initial M) pP) (target (target (FSM.initial M) pP) (p @ [t])) pP p)

goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>path M (target (FSM.initial M) pP) xs \<Longrightarrow> (\<Sum>q\<in>FSM.states M. card (R M (target (FSM.initial M) pP) q pP xs)) = length xs; path M (target (FSM.initial M) pP) (xs @ [x])\<rbrakk> \<Longrightarrow> (\<Sum>q\<in>FSM.states M. card (R M (target (FSM.initial M) pP) q pP (xs @ [x]))) = length (xs @ [x])
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
R M (target (FSM.initial M) pP) (target (target (FSM.initial M) pP) (p @ [t])) pP (p @ [t]) = insert (pP @ p @ [t]) (R M (target (FSM.initial M) pP) (target (target (FSM.initial M) pP) (p @ [t])) pP p)

goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>path M (target (FSM.initial M) pP) xs \<Longrightarrow> (\<Sum>q\<in>FSM.states M. card (R M (target (FSM.initial M) pP) q pP xs)) = length xs; path M (target (FSM.initial M) pP) (xs @ [x])\<rbrakk> \<Longrightarrow> (\<Sum>q\<in>FSM.states M. card (R M (target (FSM.initial M) pP) q pP (xs @ [x]))) = length (xs @ [x])
[PROOF STEP]
have "(pP@p@[t]) \<notin> (R M ?q ?q' pP p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pP @ p @ [t] \<notin> R M (target (FSM.initial M) pP) (target (target (FSM.initial M) pP) (p @ [t])) pP p
[PROOF STEP]
unfolding R_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pP @ p @ [t] \<notin> {pP @ p' |p'. p' \<noteq> [] \<and> target (target (FSM.initial M) pP) p' = target (target (FSM.initial M) pP) (p @ [t]) \<and> (\<exists>p''. p = p' @ p'')}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
pP @ p @ [t] \<notin> R M (target (FSM.initial M) pP) (target (target (FSM.initial M) pP) (p @ [t])) pP p

goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>path M (target (FSM.initial M) pP) xs \<Longrightarrow> (\<Sum>q\<in>FSM.states M. card (R M (target (FSM.initial M) pP) q pP xs)) = length xs; path M (target (FSM.initial M) pP) (xs @ [x])\<rbrakk> \<Longrightarrow> (\<Sum>q\<in>FSM.states M. card (R M (target (FSM.initial M) pP) q pP (xs @ [x]))) = length (xs @ [x])
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
R M (target (FSM.initial M) pP) (target (target (FSM.initial M) pP) (p @ [t])) pP (p @ [t]) = insert (pP @ p @ [t]) (R M (target (FSM.initial M) pP) (target (target (FSM.initial M) pP) (p @ [t])) pP p)
pP @ p @ [t] \<notin> R M (target (FSM.initial M) pP) (target (target (FSM.initial M) pP) (p @ [t])) pP p
[PROOF STEP]
have **: "card (R M (target (initial M) pP) ?q' pP (p@[t])) = Suc (card (R M (target (initial M) pP) ?q' pP p))"
[PROOF STATE]
proof (prove)
using this:
R M (target (FSM.initial M) pP) (target (target (FSM.initial M) pP) (p @ [t])) pP (p @ [t]) = insert (pP @ p @ [t]) (R M (target (FSM.initial M) pP) (target (target (FSM.initial M) pP) (p @ [t])) pP p)
pP @ p @ [t] \<notin> R M (target (FSM.initial M) pP) (target (target (FSM.initial M) pP) (p @ [t])) pP p

goal (1 subgoal):
 1. card (R M (target (FSM.initial M) pP) (target (target (FSM.initial M) pP) (p @ [t])) pP (p @ [t])) = Suc (card (R M (target (FSM.initial M) pP) (target (target (FSM.initial M) pP) (p @ [t])) pP p))
[PROOF STEP]
using finite_R[OF \<open>path M (target (initial M) pP) (p@[t])\<close>] finite_R[OF \<open>path M (target (initial M) pP) p\<close>]
[PROOF STATE]
proof (prove)
using this:
R M (target (FSM.initial M) pP) (target (target (FSM.initial M) pP) (p @ [t])) pP (p @ [t]) = insert (pP @ p @ [t]) (R M (target (FSM.initial M) pP) (target (target (FSM.initial M) pP) (p @ [t])) pP p)
pP @ p @ [t] \<notin> R M (target (FSM.initial M) pP) (target (target (FSM.initial M) pP) (p @ [t])) pP p
finite (R M (target (FSM.initial M) pP) ?q' ?pP (p @ [t]))
finite (R M (target (FSM.initial M) pP) ?q' ?pP p)

goal (1 subgoal):
 1. card (R M (target (FSM.initial M) pP) (target (target (FSM.initial M) pP) (p @ [t])) pP (p @ [t])) = Suc (card (R M (target (FSM.initial M) pP) (target (target (FSM.initial M) pP) (p @ [t])) pP p))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
card (R M (target (FSM.initial M) pP) (target (target (FSM.initial M) pP) (p @ [t])) pP (p @ [t])) = Suc (card (R M (target (FSM.initial M) pP) (target (target (FSM.initial M) pP) (p @ [t])) pP p))

goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>path M (target (FSM.initial M) pP) xs \<Longrightarrow> (\<Sum>q\<in>FSM.states M. card (R M (target (FSM.initial M) pP) q pP xs)) = length xs; path M (target (FSM.initial M) pP) (xs @ [x])\<rbrakk> \<Longrightarrow> (\<Sum>q\<in>FSM.states M. card (R M (target (FSM.initial M) pP) q pP (xs @ [x]))) = length (xs @ [x])
[PROOF STEP]
have "?q' \<in> states M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. target (target (FSM.initial M) pP) (p @ [t]) \<in> FSM.states M
[PROOF STEP]
using path_target_is_state[OF \<open>path M (target (FSM.initial M) pP) (p @ [t])\<close>]
[PROOF STATE]
proof (prove)
using this:
target (target (FSM.initial M) pP) (p @ [t]) \<in> FSM.states M

goal (1 subgoal):
 1. target (target (FSM.initial M) pP) (p @ [t]) \<in> FSM.states M
[PROOF STEP]
by assumption
[PROOF STATE]
proof (state)
this:
target (target (FSM.initial M) pP) (p @ [t]) \<in> FSM.states M

goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>path M (target (FSM.initial M) pP) xs \<Longrightarrow> (\<Sum>q\<in>FSM.states M. card (R M (target (FSM.initial M) pP) q pP xs)) = length xs; path M (target (FSM.initial M) pP) (xs @ [x])\<rbrakk> \<Longrightarrow> (\<Sum>q\<in>FSM.states M. card (R M (target (FSM.initial M) pP) q pP (xs @ [x]))) = length (xs @ [x])
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
target (target (FSM.initial M) pP) (p @ [t]) \<in> FSM.states M
[PROOF STEP]
have ***: "(\<Sum> q \<in> states M . card (R M (target (initial M) pP) q pP (p@[t])))
                    = (\<Sum> q \<in> states M - {?q'} . card (R M (target (initial M) pP) q pP (p@[t]))) + (card (R M (target (initial M) pP) ?q' pP (p@[t])))"
       and ****: "(\<Sum> q \<in> states M . card (R M (target (initial M) pP) q pP p))
                    = (\<Sum> q \<in> states M - {?q'} . card (R M (target (initial M) pP) q pP p)) + (card (R M (target (initial M) pP) ?q' pP p))"
[PROOF STATE]
proof (prove)
using this:
target (target (FSM.initial M) pP) (p @ [t]) \<in> FSM.states M

goal (1 subgoal):
 1. (\<Sum>q\<in>FSM.states M. card (R M (target (FSM.initial M) pP) q pP (p @ [t]))) = (\<Sum>q\<in>FSM.states M - {target (target (FSM.initial M) pP) (p @ [t])}. card (R M (target (FSM.initial M) pP) q pP (p @ [t]))) + card (R M (target (FSM.initial M) pP) (target (target (FSM.initial M) pP) (p @ [t])) pP (p @ [t])) &&& (\<Sum>q\<in>FSM.states M. card (R M (target (FSM.initial M) pP) q pP p)) = (\<Sum>q\<in>FSM.states M - {target (target (FSM.initial M) pP) (p @ [t])}. card (R M (target (FSM.initial M) pP) q pP p)) + card (R M (target (FSM.initial M) pP) (target (target (FSM.initial M) pP) (p @ [t])) pP p)
[PROOF STEP]
by (metis (no_types, lifting) Diff_insert_absorb add.commute finite_Diff fsm_states_finite mk_disjoint_insert sum.insert)+
[PROOF STATE]
proof (state)
this:
(\<Sum>q\<in>FSM.states M. card (R M (target (FSM.initial M) pP) q pP (p @ [t]))) = (\<Sum>q\<in>FSM.states M - {target (target (FSM.initial M) pP) (p @ [t])}. card (R M (target (FSM.initial M) pP) q pP (p @ [t]))) + card (R M (target (FSM.initial M) pP) (target (target (FSM.initial M) pP) (p @ [t])) pP (p @ [t]))
(\<Sum>q\<in>FSM.states M. card (R M (target (FSM.initial M) pP) q pP p)) = (\<Sum>q\<in>FSM.states M - {target (target (FSM.initial M) pP) (p @ [t])}. card (R M (target (FSM.initial M) pP) q pP p)) + card (R M (target (FSM.initial M) pP) (target (target (FSM.initial M) pP) (p @ [t])) pP p)

goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>path M (target (FSM.initial M) pP) xs \<Longrightarrow> (\<Sum>q\<in>FSM.states M. card (R M (target (FSM.initial M) pP) q pP xs)) = length xs; path M (target (FSM.initial M) pP) (xs @ [x])\<rbrakk> \<Longrightarrow> (\<Sum>q\<in>FSM.states M. card (R M (target (FSM.initial M) pP) q pP (xs @ [x]))) = length (xs @ [x])
[PROOF STEP]
have "(\<Sum> q \<in> states M . card (R M (target (initial M) pP) q pP (p@[t]))) = Suc (\<Sum> q \<in> states M . card (R M (target (initial M) pP) q pP p))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>q\<in>FSM.states M. card (R M (target (FSM.initial M) pP) q pP (p @ [t]))) = Suc (\<Sum>q\<in>FSM.states M. card (R M (target (FSM.initial M) pP) q pP p))
[PROOF STEP]
unfolding **** *** ** *
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>q\<in>FSM.states M - {target (target (FSM.initial M) pP) (p @ [t])}. card (R M (target (FSM.initial M) pP) q pP p)) + Suc (card (R M (target (FSM.initial M) pP) (target (target (FSM.initial M) pP) (p @ [t])) pP p)) = Suc ((\<Sum>q\<in>FSM.states M - {target (target (FSM.initial M) pP) (p @ [t])}. card (R M (target (FSM.initial M) pP) q pP p)) + card (R M (target (FSM.initial M) pP) (target (target (FSM.initial M) pP) (p @ [t])) pP p))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<Sum>q\<in>FSM.states M. card (R M (target (FSM.initial M) pP) q pP (p @ [t]))) = Suc (\<Sum>q\<in>FSM.states M. card (R M (target (FSM.initial M) pP) q pP p))

goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>path M (target (FSM.initial M) pP) xs \<Longrightarrow> (\<Sum>q\<in>FSM.states M. card (R M (target (FSM.initial M) pP) q pP xs)) = length xs; path M (target (FSM.initial M) pP) (xs @ [x])\<rbrakk> \<Longrightarrow> (\<Sum>q\<in>FSM.states M. card (R M (target (FSM.initial M) pP) q pP (xs @ [x]))) = length (xs @ [x])
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(\<Sum>q\<in>FSM.states M. card (R M (target (FSM.initial M) pP) q pP (p @ [t]))) = Suc (\<Sum>q\<in>FSM.states M. card (R M (target (FSM.initial M) pP) q pP p))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
(\<Sum>q\<in>FSM.states M. card (R M (target (FSM.initial M) pP) q pP (p @ [t]))) = Suc (\<Sum>q\<in>FSM.states M. card (R M (target (FSM.initial M) pP) q pP p))

goal (1 subgoal):
 1. (\<Sum>q\<in>FSM.states M. card (R M (target (FSM.initial M) pP) q pP (p @ [t]))) = length (p @ [t])
[PROOF STEP]
unfolding snoc.IH[OF \<open>path M (target (initial M) pP) p\<close>]
[PROOF STATE]
proof (prove)
using this:
(\<Sum>q\<in>FSM.states M. card (R M (target (FSM.initial M) pP) q pP (p @ [t]))) = Suc (length p)

goal (1 subgoal):
 1. (\<Sum>q\<in>FSM.states M. card (R M (target (FSM.initial M) pP) q pP (p @ [t]))) = length (p @ [t])
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<Sum>q\<in>FSM.states M. card (R M (target (FSM.initial M) pP) q pP (p @ [t]))) = length (p @ [t])

goal:
No subgoals!
[PROOF STEP]
qed