[STATEMENT]
lemma reach_lreach:
assumes "reach s"
obtains "lreach nid (s nid)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (lreach nid (s nid) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (lreach nid (s nid) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
interpret Node: Transition_System "istate nid" "validTrans nid" "srcOf nid" "tgtOf nid"
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
.
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (Node.reach (s nid) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from assms that
[PROOF STATE]
proof (chain)
picking this:
reach s
Node.reach (s nid) \<Longrightarrow> thesis
[PROOF STEP]
show thesis
[PROOF STATE]
proof (prove)
using this:
reach s
Node.reach (s nid) \<Longrightarrow> thesis

goal (1 subgoal):
 1. thesis
[PROOF STEP]
proof induction
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. (Node.reach (istate nid) \<Longrightarrow> thesis) \<Longrightarrow> thesis
 2. \<And>s trn s'. \<lbrakk>reach s; (Node.reach (s nid) \<Longrightarrow> thesis) \<Longrightarrow> thesis; nValidTrans trn; nSrcOf trn = s; nTgtOf trn = s'; Node.reach (s' nid) \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
case Istate
[PROOF STATE]
proof (state)
this:
Node.reach (istate nid) \<Longrightarrow> thesis

goal (2 subgoals):
 1. (Node.reach (istate nid) \<Longrightarrow> thesis) \<Longrightarrow> thesis
 2. \<And>s trn s'. \<lbrakk>reach s; (Node.reach (s nid) \<Longrightarrow> thesis) \<Longrightarrow> thesis; nValidTrans trn; nSrcOf trn = s; nTgtOf trn = s'; Node.reach (s' nid) \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Node.reach (istate nid) \<Longrightarrow> thesis
[PROOF STEP]
show thesis
[PROOF STATE]
proof (prove)
using this:
Node.reach (istate nid) \<Longrightarrow> thesis

goal (1 subgoal):
 1. thesis
[PROOF STEP]
using Node.reach.Istate
[PROOF STATE]
proof (prove)
using this:
Node.reach (istate nid) \<Longrightarrow> thesis
Node.reach (istate nid)

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

goal (1 subgoal):
 1. \<And>s trn s'. \<lbrakk>reach s; (Node.reach (s nid) \<Longrightarrow> thesis) \<Longrightarrow> thesis; nValidTrans trn; nSrcOf trn = s; nTgtOf trn = s'; Node.reach (s' nid) \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>s trn s'. \<lbrakk>reach s; (Node.reach (s nid) \<Longrightarrow> thesis) \<Longrightarrow> thesis; nValidTrans trn; nSrcOf trn = s; nTgtOf trn = s'; Node.reach (s' nid) \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
case (Step s trn s')
[PROOF STATE]
proof (state)
this:
reach s
nValidTrans trn
nSrcOf trn = s
nTgtOf trn = s'
(Node.reach (s nid) \<Longrightarrow> thesis) \<Longrightarrow> thesis
Node.reach (s' nid) \<Longrightarrow> thesis

goal (1 subgoal):
 1. \<And>s trn s'. \<lbrakk>reach s; (Node.reach (s nid) \<Longrightarrow> thesis) \<Longrightarrow> thesis; nValidTrans trn; nSrcOf trn = s; nTgtOf trn = s'; Node.reach (s' nid) \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
show thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. thesis
[PROOF STEP]
proof (rule Step.IH)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Node.reach (s nid) \<Longrightarrow> thesis
[PROOF STEP]
assume "Node.reach (s nid)"
[PROOF STATE]
proof (state)
this:
Node.reach (s nid)

goal (1 subgoal):
 1. Node.reach (s nid) \<Longrightarrow> thesis
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Node.reach (s nid)
[PROOF STEP]
show thesis
[PROOF STATE]
proof (prove)
using this:
Node.reach (s nid)

goal (1 subgoal):
 1. thesis
[PROOF STEP]
using Step.hyps Node.reach.Step[of "s nid" _ "s' nid"]
[PROOF STATE]
proof (prove)
using this:
Node.reach (s nid)
reach s
nValidTrans trn
nSrcOf trn = s
nTgtOf trn = s'
\<lbrakk>Node.reach (s nid); validTrans nid ?trn; srcOf nid ?trn = s nid; tgtOf nid ?trn = s' nid\<rbrakk> \<Longrightarrow> Node.reach (s' nid)

goal (1 subgoal):
 1. thesis
[PROOF STEP]
by (intro Step.prems, cases trn) (auto)
[PROOF STATE]
proof (state)
this:
thesis

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

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

goal:
No subgoals!
[PROOF STEP]
qed