[STATEMENT]
lemma expandLeft:
  fixes P   :: pi
  and   Q   :: pi
  and   R   :: pi
  and   Rel :: "(pi \<times> pi) set"

  assumes Exp: "(R, expandSet P Q) \<in> sumComposeSet"
  and     Phnf: "hnf P"
  and     Qhnf: "hnf Q"
  and     Id: "Id \<subseteq> Rel"

  shows "P \<parallel> Q \<leadsto>[Rel] R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<parallel> Q \<leadsto>[Rel] R
[PROOF STEP]
proof(induct rule: simCases)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>a y Q'. \<lbrakk>R \<longmapsto> a\<guillemotleft>y\<guillemotright> \<prec> Q'; y \<sharp> P \<parallel> Q\<rbrakk> \<Longrightarrow> \<exists>P'. P \<parallel> Q \<longmapsto> a\<guillemotleft>y\<guillemotright> \<prec> P' \<and> derivative P' Q' a y Rel
 2. \<And>\<alpha> Q'. R \<longmapsto> \<alpha> \<prec> Q' \<Longrightarrow> \<exists>P'. P \<parallel> Q \<longmapsto> \<alpha> \<prec> P' \<and> (P', Q') \<in> Rel
[PROOF STEP]
case(Bound a x R')
[PROOF STATE]
proof (state)
this:
R \<longmapsto> a\<guillemotleft>x\<guillemotright> \<prec> R'
x \<sharp> P \<parallel> Q

goal (2 subgoals):
 1. \<And>a y Q'. \<lbrakk>R \<longmapsto> a\<guillemotleft>y\<guillemotright> \<prec> Q'; y \<sharp> P \<parallel> Q\<rbrakk> \<Longrightarrow> \<exists>P'. P \<parallel> Q \<longmapsto> a\<guillemotleft>y\<guillemotright> \<prec> P' \<and> derivative P' Q' a y Rel
 2. \<And>\<alpha> Q'. R \<longmapsto> \<alpha> \<prec> Q' \<Longrightarrow> \<exists>P'. P \<parallel> Q \<longmapsto> \<alpha> \<prec> P' \<and> (P', Q') \<in> Rel
[PROOF STEP]
have "R \<longmapsto>a\<guillemotleft>x\<guillemotright> \<prec> R'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. R \<longmapsto> a\<guillemotleft>x\<guillemotright> \<prec> R'
[PROOF STEP]
by fact
[PROOF STATE]
proof (state)
this:
R \<longmapsto> a\<guillemotleft>x\<guillemotright> \<prec> R'

goal (2 subgoals):
 1. \<And>a y Q'. \<lbrakk>R \<longmapsto> a\<guillemotleft>y\<guillemotright> \<prec> Q'; y \<sharp> P \<parallel> Q\<rbrakk> \<Longrightarrow> \<exists>P'. P \<parallel> Q \<longmapsto> a\<guillemotleft>y\<guillemotright> \<prec> P' \<and> derivative P' Q' a y Rel
 2. \<And>\<alpha> Q'. R \<longmapsto> \<alpha> \<prec> Q' \<Longrightarrow> \<exists>P'. P \<parallel> Q \<longmapsto> \<alpha> \<prec> P' \<and> (P', Q') \<in> Rel
[PROOF STEP]
with Exp Phnf Qhnf
[PROOF STATE]
proof (chain)
picking this:
(R, expandSet P Q) \<in> sumComposeSet
hnf P
hnf Q
R \<longmapsto> a\<guillemotleft>x\<guillemotright> \<prec> R'
[PROOF STEP]
have "P \<parallel> Q \<longmapsto>a\<guillemotleft>x\<guillemotright> \<prec> R'"
[PROOF STATE]
proof (prove)
using this:
(R, expandSet P Q) \<in> sumComposeSet
hnf P
hnf Q
R \<longmapsto> a\<guillemotleft>x\<guillemotright> \<prec> R'

goal (1 subgoal):
 1. P \<parallel> Q \<longmapsto> a\<guillemotleft>x\<guillemotright> \<prec> R'
[PROOF STEP]
by(cases a, auto simp add: expandTrans)
[PROOF STATE]
proof (state)
this:
P \<parallel> Q \<longmapsto> a\<guillemotleft>x\<guillemotright> \<prec> R'

goal (2 subgoals):
 1. \<And>a y Q'. \<lbrakk>R \<longmapsto> a\<guillemotleft>y\<guillemotright> \<prec> Q'; y \<sharp> P \<parallel> Q\<rbrakk> \<Longrightarrow> \<exists>P'. P \<parallel> Q \<longmapsto> a\<guillemotleft>y\<guillemotright> \<prec> P' \<and> derivative P' Q' a y Rel
 2. \<And>\<alpha> Q'. R \<longmapsto> \<alpha> \<prec> Q' \<Longrightarrow> \<exists>P'. P \<parallel> Q \<longmapsto> \<alpha> \<prec> P' \<and> (P', Q') \<in> Rel
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
P \<parallel> Q \<longmapsto> a\<guillemotleft>x\<guillemotright> \<prec> R'

goal (2 subgoals):
 1. \<And>a y Q'. \<lbrakk>R \<longmapsto> a\<guillemotleft>y\<guillemotright> \<prec> Q'; y \<sharp> P \<parallel> Q\<rbrakk> \<Longrightarrow> \<exists>P'. P \<parallel> Q \<longmapsto> a\<guillemotleft>y\<guillemotright> \<prec> P' \<and> derivative P' Q' a y Rel
 2. \<And>\<alpha> Q'. R \<longmapsto> \<alpha> \<prec> Q' \<Longrightarrow> \<exists>P'. P \<parallel> Q \<longmapsto> \<alpha> \<prec> P' \<and> (P', Q') \<in> Rel
[PROOF STEP]
from Id
[PROOF STATE]
proof (chain)
picking this:
Id \<subseteq> Rel
[PROOF STEP]
have "derivative R' R' a x Rel"
[PROOF STATE]
proof (prove)
using this:
Id \<subseteq> Rel

goal (1 subgoal):
 1. derivative R' R' a x Rel
[PROOF STEP]
by(cases a, auto simp add: derivative_def)
[PROOF STATE]
proof (state)
this:
derivative R' R' a x Rel

goal (2 subgoals):
 1. \<And>a y Q'. \<lbrakk>R \<longmapsto> a\<guillemotleft>y\<guillemotright> \<prec> Q'; y \<sharp> P \<parallel> Q\<rbrakk> \<Longrightarrow> \<exists>P'. P \<parallel> Q \<longmapsto> a\<guillemotleft>y\<guillemotright> \<prec> P' \<and> derivative P' Q' a y Rel
 2. \<And>\<alpha> Q'. R \<longmapsto> \<alpha> \<prec> Q' \<Longrightarrow> \<exists>P'. P \<parallel> Q \<longmapsto> \<alpha> \<prec> P' \<and> (P', Q') \<in> Rel
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
P \<parallel> Q \<longmapsto> a\<guillemotleft>x\<guillemotright> \<prec> R'
derivative R' R' a x Rel
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
P \<parallel> Q \<longmapsto> a\<guillemotleft>x\<guillemotright> \<prec> R'
derivative R' R' a x Rel

goal (1 subgoal):
 1. \<exists>P'. P \<parallel> Q \<longmapsto> a\<guillemotleft>x\<guillemotright> \<prec> P' \<and> derivative P' R' a x Rel
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>P'. P \<parallel> Q \<longmapsto> a\<guillemotleft>x\<guillemotright> \<prec> P' \<and> derivative P' R' a x Rel

goal (1 subgoal):
 1. \<And>\<alpha> Q'. R \<longmapsto> \<alpha> \<prec> Q' \<Longrightarrow> \<exists>P'. P \<parallel> Q \<longmapsto> \<alpha> \<prec> P' \<and> (P', Q') \<in> Rel
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>\<alpha> Q'. R \<longmapsto> \<alpha> \<prec> Q' \<Longrightarrow> \<exists>P'. P \<parallel> Q \<longmapsto> \<alpha> \<prec> P' \<and> (P', Q') \<in> Rel
[PROOF STEP]
case(Free \<alpha> R')
[PROOF STATE]
proof (state)
this:
R \<longmapsto> \<alpha> \<prec> R'

goal (1 subgoal):
 1. \<And>\<alpha> Q'. R \<longmapsto> \<alpha> \<prec> Q' \<Longrightarrow> \<exists>P'. P \<parallel> Q \<longmapsto> \<alpha> \<prec> P' \<and> (P', Q') \<in> Rel
[PROOF STEP]
have "R \<longmapsto>\<alpha> \<prec> R'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. R \<longmapsto> \<alpha> \<prec> R'
[PROOF STEP]
by fact
[PROOF STATE]
proof (state)
this:
R \<longmapsto> \<alpha> \<prec> R'

goal (1 subgoal):
 1. \<And>\<alpha> Q'. R \<longmapsto> \<alpha> \<prec> Q' \<Longrightarrow> \<exists>P'. P \<parallel> Q \<longmapsto> \<alpha> \<prec> P' \<and> (P', Q') \<in> Rel
[PROOF STEP]
with Exp Phnf Qhnf
[PROOF STATE]
proof (chain)
picking this:
(R, expandSet P Q) \<in> sumComposeSet
hnf P
hnf Q
R \<longmapsto> \<alpha> \<prec> R'
[PROOF STEP]
have "P \<parallel> Q \<longmapsto>\<alpha> \<prec> R'"
[PROOF STATE]
proof (prove)
using this:
(R, expandSet P Q) \<in> sumComposeSet
hnf P
hnf Q
R \<longmapsto> \<alpha> \<prec> R'

goal (1 subgoal):
 1. P \<parallel> Q \<longmapsto> \<alpha> \<prec> R'
[PROOF STEP]
by(cases \<alpha>, auto simp add: expandTrans)
[PROOF STATE]
proof (state)
this:
P \<parallel> Q \<longmapsto> \<alpha> \<prec> R'

goal (1 subgoal):
 1. \<And>\<alpha> Q'. R \<longmapsto> \<alpha> \<prec> Q' \<Longrightarrow> \<exists>P'. P \<parallel> Q \<longmapsto> \<alpha> \<prec> P' \<and> (P', Q') \<in> Rel
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
P \<parallel> Q \<longmapsto> \<alpha> \<prec> R'

goal (1 subgoal):
 1. \<And>\<alpha> Q'. R \<longmapsto> \<alpha> \<prec> Q' \<Longrightarrow> \<exists>P'. P \<parallel> Q \<longmapsto> \<alpha> \<prec> P' \<and> (P', Q') \<in> Rel
[PROOF STEP]
from Id
[PROOF STATE]
proof (chain)
picking this:
Id \<subseteq> Rel
[PROOF STEP]
have "(R', R') \<in> Rel"
[PROOF STATE]
proof (prove)
using this:
Id \<subseteq> Rel

goal (1 subgoal):
 1. (R', R') \<in> Rel
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(R', R') \<in> Rel

goal (1 subgoal):
 1. \<And>\<alpha> Q'. R \<longmapsto> \<alpha> \<prec> Q' \<Longrightarrow> \<exists>P'. P \<parallel> Q \<longmapsto> \<alpha> \<prec> P' \<and> (P', Q') \<in> Rel
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
P \<parallel> Q \<longmapsto> \<alpha> \<prec> R'
(R', R') \<in> Rel
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
P \<parallel> Q \<longmapsto> \<alpha> \<prec> R'
(R', R') \<in> Rel

goal (1 subgoal):
 1. \<exists>P'. P \<parallel> Q \<longmapsto> \<alpha> \<prec> P' \<and> (P', R') \<in> Rel
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>P'. P \<parallel> Q \<longmapsto> \<alpha> \<prec> P' \<and> (P', R') \<in> Rel

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma expandRight:
  fixes P   :: pi
  and   Q   :: pi
  and   R   :: pi
  and   Rel :: "(pi \<times> pi) set"

  assumes Exp: "(R, expandSet P Q) \<in> sumComposeSet"
  and     Phnf: "hnf P"
  and     Qhnf: "hnf Q"
  and     Id: "Id \<subseteq> Rel"

  shows "R \<leadsto>[Rel] P \<parallel> Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. R \<leadsto>[Rel] P \<parallel> Q
[PROOF STEP]
proof(induct rule: simCases)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>a y Q'. \<lbrakk>P \<parallel> Q \<longmapsto> a\<guillemotleft>y\<guillemotright> \<prec> Q'; y \<sharp> R\<rbrakk> \<Longrightarrow> \<exists>P'. R \<longmapsto> a\<guillemotleft>y\<guillemotright> \<prec> P' \<and> derivative P' Q' a y Rel
 2. \<And>\<alpha> Q'. P \<parallel> Q \<longmapsto> \<alpha> \<prec> Q' \<Longrightarrow> \<exists>P'. R \<longmapsto> \<alpha> \<prec> P' \<and> (P', Q') \<in> Rel
[PROOF STEP]
case(Bound a x R')
[PROOF STATE]
proof (state)
this:
P \<parallel> Q \<longmapsto> a\<guillemotleft>x\<guillemotright> \<prec> R'
x \<sharp> R

goal (2 subgoals):
 1. \<And>a y Q'. \<lbrakk>P \<parallel> Q \<longmapsto> a\<guillemotleft>y\<guillemotright> \<prec> Q'; y \<sharp> R\<rbrakk> \<Longrightarrow> \<exists>P'. R \<longmapsto> a\<guillemotleft>y\<guillemotright> \<prec> P' \<and> derivative P' Q' a y Rel
 2. \<And>\<alpha> Q'. P \<parallel> Q \<longmapsto> \<alpha> \<prec> Q' \<Longrightarrow> \<exists>P'. R \<longmapsto> \<alpha> \<prec> P' \<and> (P', Q') \<in> Rel
[PROOF STEP]
have "P \<parallel> Q \<longmapsto>a\<guillemotleft>x\<guillemotright> \<prec> R'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<parallel> Q \<longmapsto> a\<guillemotleft>x\<guillemotright> \<prec> R'
[PROOF STEP]
by fact
[PROOF STATE]
proof (state)
this:
P \<parallel> Q \<longmapsto> a\<guillemotleft>x\<guillemotright> \<prec> R'

goal (2 subgoals):
 1. \<And>a y Q'. \<lbrakk>P \<parallel> Q \<longmapsto> a\<guillemotleft>y\<guillemotright> \<prec> Q'; y \<sharp> R\<rbrakk> \<Longrightarrow> \<exists>P'. R \<longmapsto> a\<guillemotleft>y\<guillemotright> \<prec> P' \<and> derivative P' Q' a y Rel
 2. \<And>\<alpha> Q'. P \<parallel> Q \<longmapsto> \<alpha> \<prec> Q' \<Longrightarrow> \<exists>P'. R \<longmapsto> \<alpha> \<prec> P' \<and> (P', Q') \<in> Rel
[PROOF STEP]
with Exp Phnf Qhnf
[PROOF STATE]
proof (chain)
picking this:
(R, expandSet P Q) \<in> sumComposeSet
hnf P
hnf Q
P \<parallel> Q \<longmapsto> a\<guillemotleft>x\<guillemotright> \<prec> R'
[PROOF STEP]
have "R \<longmapsto>a\<guillemotleft>x\<guillemotright> \<prec> R'"
[PROOF STATE]
proof (prove)
using this:
(R, expandSet P Q) \<in> sumComposeSet
hnf P
hnf Q
P \<parallel> Q \<longmapsto> a\<guillemotleft>x\<guillemotright> \<prec> R'

goal (1 subgoal):
 1. R \<longmapsto> a\<guillemotleft>x\<guillemotright> \<prec> R'
[PROOF STEP]
by(cases a, auto simp add: expandTrans)
[PROOF STATE]
proof (state)
this:
R \<longmapsto> a\<guillemotleft>x\<guillemotright> \<prec> R'

goal (2 subgoals):
 1. \<And>a y Q'. \<lbrakk>P \<parallel> Q \<longmapsto> a\<guillemotleft>y\<guillemotright> \<prec> Q'; y \<sharp> R\<rbrakk> \<Longrightarrow> \<exists>P'. R \<longmapsto> a\<guillemotleft>y\<guillemotright> \<prec> P' \<and> derivative P' Q' a y Rel
 2. \<And>\<alpha> Q'. P \<parallel> Q \<longmapsto> \<alpha> \<prec> Q' \<Longrightarrow> \<exists>P'. R \<longmapsto> \<alpha> \<prec> P' \<and> (P', Q') \<in> Rel
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
R \<longmapsto> a\<guillemotleft>x\<guillemotright> \<prec> R'

goal (2 subgoals):
 1. \<And>a y Q'. \<lbrakk>P \<parallel> Q \<longmapsto> a\<guillemotleft>y\<guillemotright> \<prec> Q'; y \<sharp> R\<rbrakk> \<Longrightarrow> \<exists>P'. R \<longmapsto> a\<guillemotleft>y\<guillemotright> \<prec> P' \<and> derivative P' Q' a y Rel
 2. \<And>\<alpha> Q'. P \<parallel> Q \<longmapsto> \<alpha> \<prec> Q' \<Longrightarrow> \<exists>P'. R \<longmapsto> \<alpha> \<prec> P' \<and> (P', Q') \<in> Rel
[PROOF STEP]
from Id
[PROOF STATE]
proof (chain)
picking this:
Id \<subseteq> Rel
[PROOF STEP]
have "derivative R' R' a x Rel"
[PROOF STATE]
proof (prove)
using this:
Id \<subseteq> Rel

goal (1 subgoal):
 1. derivative R' R' a x Rel
[PROOF STEP]
by(cases a, auto simp add: derivative_def)
[PROOF STATE]
proof (state)
this:
derivative R' R' a x Rel

goal (2 subgoals):
 1. \<And>a y Q'. \<lbrakk>P \<parallel> Q \<longmapsto> a\<guillemotleft>y\<guillemotright> \<prec> Q'; y \<sharp> R\<rbrakk> \<Longrightarrow> \<exists>P'. R \<longmapsto> a\<guillemotleft>y\<guillemotright> \<prec> P' \<and> derivative P' Q' a y Rel
 2. \<And>\<alpha> Q'. P \<parallel> Q \<longmapsto> \<alpha> \<prec> Q' \<Longrightarrow> \<exists>P'. R \<longmapsto> \<alpha> \<prec> P' \<and> (P', Q') \<in> Rel
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
R \<longmapsto> a\<guillemotleft>x\<guillemotright> \<prec> R'
derivative R' R' a x Rel
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
R \<longmapsto> a\<guillemotleft>x\<guillemotright> \<prec> R'
derivative R' R' a x Rel

goal (1 subgoal):
 1. \<exists>P'. R \<longmapsto> a\<guillemotleft>x\<guillemotright> \<prec> P' \<and> derivative P' R' a x Rel
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>P'. R \<longmapsto> a\<guillemotleft>x\<guillemotright> \<prec> P' \<and> derivative P' R' a x Rel

goal (1 subgoal):
 1. \<And>\<alpha> Q'. P \<parallel> Q \<longmapsto> \<alpha> \<prec> Q' \<Longrightarrow> \<exists>P'. R \<longmapsto> \<alpha> \<prec> P' \<and> (P', Q') \<in> Rel
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>\<alpha> Q'. P \<parallel> Q \<longmapsto> \<alpha> \<prec> Q' \<Longrightarrow> \<exists>P'. R \<longmapsto> \<alpha> \<prec> P' \<and> (P', Q') \<in> Rel
[PROOF STEP]
case(Free \<alpha> R')
[PROOF STATE]
proof (state)
this:
P \<parallel> Q \<longmapsto> \<alpha> \<prec> R'

goal (1 subgoal):
 1. \<And>\<alpha> Q'. P \<parallel> Q \<longmapsto> \<alpha> \<prec> Q' \<Longrightarrow> \<exists>P'. R \<longmapsto> \<alpha> \<prec> P' \<and> (P', Q') \<in> Rel
[PROOF STEP]
have "P \<parallel> Q \<longmapsto>\<alpha> \<prec> R'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<parallel> Q \<longmapsto> \<alpha> \<prec> R'
[PROOF STEP]
by fact
[PROOF STATE]
proof (state)
this:
P \<parallel> Q \<longmapsto> \<alpha> \<prec> R'

goal (1 subgoal):
 1. \<And>\<alpha> Q'. P \<parallel> Q \<longmapsto> \<alpha> \<prec> Q' \<Longrightarrow> \<exists>P'. R \<longmapsto> \<alpha> \<prec> P' \<and> (P', Q') \<in> Rel
[PROOF STEP]
with Exp Phnf Qhnf
[PROOF STATE]
proof (chain)
picking this:
(R, expandSet P Q) \<in> sumComposeSet
hnf P
hnf Q
P \<parallel> Q \<longmapsto> \<alpha> \<prec> R'
[PROOF STEP]
have "R \<longmapsto>\<alpha> \<prec> R'"
[PROOF STATE]
proof (prove)
using this:
(R, expandSet P Q) \<in> sumComposeSet
hnf P
hnf Q
P \<parallel> Q \<longmapsto> \<alpha> \<prec> R'

goal (1 subgoal):
 1. R \<longmapsto> \<alpha> \<prec> R'
[PROOF STEP]
by(cases \<alpha>, auto simp add: expandTrans)
[PROOF STATE]
proof (state)
this:
R \<longmapsto> \<alpha> \<prec> R'

goal (1 subgoal):
 1. \<And>\<alpha> Q'. P \<parallel> Q \<longmapsto> \<alpha> \<prec> Q' \<Longrightarrow> \<exists>P'. R \<longmapsto> \<alpha> \<prec> P' \<and> (P', Q') \<in> Rel
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
R \<longmapsto> \<alpha> \<prec> R'

goal (1 subgoal):
 1. \<And>\<alpha> Q'. P \<parallel> Q \<longmapsto> \<alpha> \<prec> Q' \<Longrightarrow> \<exists>P'. R \<longmapsto> \<alpha> \<prec> P' \<and> (P', Q') \<in> Rel
[PROOF STEP]
from Id
[PROOF STATE]
proof (chain)
picking this:
Id \<subseteq> Rel
[PROOF STEP]
have "(R', R') \<in> Rel"
[PROOF STATE]
proof (prove)
using this:
Id \<subseteq> Rel

goal (1 subgoal):
 1. (R', R') \<in> Rel
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(R', R') \<in> Rel

goal (1 subgoal):
 1. \<And>\<alpha> Q'. P \<parallel> Q \<longmapsto> \<alpha> \<prec> Q' \<Longrightarrow> \<exists>P'. R \<longmapsto> \<alpha> \<prec> P' \<and> (P', Q') \<in> Rel
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
R \<longmapsto> \<alpha> \<prec> R'
(R', R') \<in> Rel
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
R \<longmapsto> \<alpha> \<prec> R'
(R', R') \<in> Rel

goal (1 subgoal):
 1. \<exists>P'. R \<longmapsto> \<alpha> \<prec> P' \<and> (P', R') \<in> Rel
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>P'. R \<longmapsto> \<alpha> \<prec> P' \<and> (P', R') \<in> Rel

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma expandSC:
  fixes P :: pi
  and   Q :: pi
  and   R :: pi

  assumes "(R, expandSet P Q) \<in> sumComposeSet"
  and     "hnf P"
  and     "hnf Q"

  shows "P \<parallel> Q \<sim> R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<parallel> Q \<sim> R
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. P \<parallel> Q \<sim> R
[PROOF STEP]
let ?X = "{(P \<parallel> Q, R) | P Q R. (R, expandSet P Q) \<in> sumComposeSet \<and> hnf P \<and> hnf Q} \<union> {(R, P \<parallel> Q) | P Q R. (R, expandSet P Q) \<in> sumComposeSet \<and> hnf P \<and> hnf Q}"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. P \<parallel> Q \<sim> R
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
(R, expandSet P Q) \<in> sumComposeSet
hnf P
hnf Q
[PROOF STEP]
have "(P \<parallel> Q, R) \<in> ?X"
[PROOF STATE]
proof (prove)
using this:
(R, expandSet P Q) \<in> sumComposeSet
hnf P
hnf Q

goal (1 subgoal):
 1. (P \<parallel> Q, R) \<in> {(P \<parallel> Q, R) |P Q R. (R, expandSet P Q) \<in> sumComposeSet \<and> hnf P \<and> hnf Q} \<union> {(R, P \<parallel> Q) |P Q R. (R, expandSet P Q) \<in> sumComposeSet \<and> hnf P \<and> hnf Q}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(P \<parallel> Q, R) \<in> {(P \<parallel> Q, R) |P Q R. (R, expandSet P Q) \<in> sumComposeSet \<and> hnf P \<and> hnf Q} \<union> {(R, P \<parallel> Q) |P Q R. (R, expandSet P Q) \<in> sumComposeSet \<and> hnf P \<and> hnf Q}

goal (1 subgoal):
 1. P \<parallel> Q \<sim> R
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
(P \<parallel> Q, R) \<in> {(P \<parallel> Q, R) |P Q R. (R, expandSet P Q) \<in> sumComposeSet \<and> hnf P \<and> hnf Q} \<union> {(R, P \<parallel> Q) |P Q R. (R, expandSet P Q) \<in> sumComposeSet \<and> hnf P \<and> hnf Q}

goal (1 subgoal):
 1. P \<parallel> Q \<sim> R
[PROOF STEP]
proof(coinduct rule: bisimCoinduct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>R S. (R, S) \<in> {(P \<parallel> Q, R) |P Q R. (R, expandSet P Q) \<in> sumComposeSet \<and> hnf P \<and> hnf Q} \<union> {(R, P \<parallel> Q) |P Q R. (R, expandSet P Q) \<in> sumComposeSet \<and> hnf P \<and> hnf Q} \<Longrightarrow> R \<leadsto>[({(P \<parallel> Q, R) |P Q R. (R, expandSet P Q) \<in> sumComposeSet \<and> hnf P \<and> hnf Q} \<union> {(R, P \<parallel> Q) |P Q R. (R, expandSet P Q) \<in> sumComposeSet \<and> hnf P \<and> hnf Q} \<union> bisim)] S
 2. \<And>R S. (R, S) \<in> {(P \<parallel> Q, R) |P Q R. (R, expandSet P Q) \<in> sumComposeSet \<and> hnf P \<and> hnf Q} \<union> {(R, P \<parallel> Q) |P Q R. (R, expandSet P Q) \<in> sumComposeSet \<and> hnf P \<and> hnf Q} \<Longrightarrow> (S, R) \<in> {(P \<parallel> Q, R) |P Q R. (R, expandSet P Q) \<in> sumComposeSet \<and> hnf P \<and> hnf Q} \<union> {(R, P \<parallel> Q) |P Q R. (R, expandSet P Q) \<in> sumComposeSet \<and> hnf P \<and> hnf Q}
[PROOF STEP]
case(cSim P Q)
[PROOF STATE]
proof (state)
this:
(P, Q) \<in> {(P \<parallel> Q, R) |P Q R. (R, expandSet P Q) \<in> sumComposeSet \<and> hnf P \<and> hnf Q} \<union> {(R, P \<parallel> Q) |P Q R. (R, expandSet P Q) \<in> sumComposeSet \<and> hnf P \<and> hnf Q}

goal (2 subgoals):
 1. \<And>R S. (R, S) \<in> {(P \<parallel> Q, R) |P Q R. (R, expandSet P Q) \<in> sumComposeSet \<and> hnf P \<and> hnf Q} \<union> {(R, P \<parallel> Q) |P Q R. (R, expandSet P Q) \<in> sumComposeSet \<and> hnf P \<and> hnf Q} \<Longrightarrow> R \<leadsto>[({(P \<parallel> Q, R) |P Q R. (R, expandSet P Q) \<in> sumComposeSet \<and> hnf P \<and> hnf Q} \<union> {(R, P \<parallel> Q) |P Q R. (R, expandSet P Q) \<in> sumComposeSet \<and> hnf P \<and> hnf Q} \<union> bisim)] S
 2. \<And>R S. (R, S) \<in> {(P \<parallel> Q, R) |P Q R. (R, expandSet P Q) \<in> sumComposeSet \<and> hnf P \<and> hnf Q} \<union> {(R, P \<parallel> Q) |P Q R. (R, expandSet P Q) \<in> sumComposeSet \<and> hnf P \<and> hnf Q} \<Longrightarrow> (S, R) \<in> {(P \<parallel> Q, R) |P Q R. (R, expandSet P Q) \<in> sumComposeSet \<and> hnf P \<and> hnf Q} \<union> {(R, P \<parallel> Q) |P Q R. (R, expandSet P Q) \<in> sumComposeSet \<and> hnf P \<and> hnf Q}
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
(P, Q) \<in> {(P \<parallel> Q, R) |P Q R. (R, expandSet P Q) \<in> sumComposeSet \<and> hnf P \<and> hnf Q} \<union> {(R, P \<parallel> Q) |P Q R. (R, expandSet P Q) \<in> sumComposeSet \<and> hnf P \<and> hnf Q}

goal (1 subgoal):
 1. P \<leadsto>[({(P \<parallel> Q, R) |P Q R. (R, expandSet P Q) \<in> sumComposeSet \<and> hnf P \<and> hnf Q} \<union> {(R, P \<parallel> Q) |P Q R. (R, expandSet P Q) \<in> sumComposeSet \<and> hnf P \<and> hnf Q} \<union> bisim)] Q
[PROOF STEP]
by(blast intro: reflexive expandLeft expandRight)
[PROOF STATE]
proof (state)
this:
P \<leadsto>[({(P \<parallel> Q, R) |P Q R. (R, expandSet P Q) \<in> sumComposeSet \<and> hnf P \<and> hnf Q} \<union> {(R, P \<parallel> Q) |P Q R. (R, expandSet P Q) \<in> sumComposeSet \<and> hnf P \<and> hnf Q} \<union> bisim)] Q

goal (1 subgoal):
 1. \<And>R S. (R, S) \<in> {(P \<parallel> Q, R) |P Q R. (R, expandSet P Q) \<in> sumComposeSet \<and> hnf P \<and> hnf Q} \<union> {(R, P \<parallel> Q) |P Q R. (R, expandSet P Q) \<in> sumComposeSet \<and> hnf P \<and> hnf Q} \<Longrightarrow> (S, R) \<in> {(P \<parallel> Q, R) |P Q R. (R, expandSet P Q) \<in> sumComposeSet \<and> hnf P \<and> hnf Q} \<union> {(R, P \<parallel> Q) |P Q R. (R, expandSet P Q) \<in> sumComposeSet \<and> hnf P \<and> hnf Q}
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>R S. (R, S) \<in> {(P \<parallel> Q, R) |P Q R. (R, expandSet P Q) \<in> sumComposeSet \<and> hnf P \<and> hnf Q} \<union> {(R, P \<parallel> Q) |P Q R. (R, expandSet P Q) \<in> sumComposeSet \<and> hnf P \<and> hnf Q} \<Longrightarrow> (S, R) \<in> {(P \<parallel> Q, R) |P Q R. (R, expandSet P Q) \<in> sumComposeSet \<and> hnf P \<and> hnf Q} \<union> {(R, P \<parallel> Q) |P Q R. (R, expandSet P Q) \<in> sumComposeSet \<and> hnf P \<and> hnf Q}
[PROOF STEP]
case(cSym P Q)
[PROOF STATE]
proof (state)
this:
(P, Q) \<in> {(P \<parallel> Q, R) |P Q R. (R, expandSet P Q) \<in> sumComposeSet \<and> hnf P \<and> hnf Q} \<union> {(R, P \<parallel> Q) |P Q R. (R, expandSet P Q) \<in> sumComposeSet \<and> hnf P \<and> hnf Q}

goal (1 subgoal):
 1. \<And>R S. (R, S) \<in> {(P \<parallel> Q, R) |P Q R. (R, expandSet P Q) \<in> sumComposeSet \<and> hnf P \<and> hnf Q} \<union> {(R, P \<parallel> Q) |P Q R. (R, expandSet P Q) \<in> sumComposeSet \<and> hnf P \<and> hnf Q} \<Longrightarrow> (S, R) \<in> {(P \<parallel> Q, R) |P Q R. (R, expandSet P Q) \<in> sumComposeSet \<and> hnf P \<and> hnf Q} \<union> {(R, P \<parallel> Q) |P Q R. (R, expandSet P Q) \<in> sumComposeSet \<and> hnf P \<and> hnf Q}
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
(P, Q) \<in> {(P \<parallel> Q, R) |P Q R. (R, expandSet P Q) \<in> sumComposeSet \<and> hnf P \<and> hnf Q} \<union> {(R, P \<parallel> Q) |P Q R. (R, expandSet P Q) \<in> sumComposeSet \<and> hnf P \<and> hnf Q}

goal (1 subgoal):
 1. (Q, P) \<in> {(P \<parallel> Q, R) |P Q R. (R, expandSet P Q) \<in> sumComposeSet \<and> hnf P \<and> hnf Q} \<union> {(R, P \<parallel> Q) |P Q R. (R, expandSet P Q) \<in> sumComposeSet \<and> hnf P \<and> hnf Q}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(Q, P) \<in> {(P \<parallel> Q, R) |P Q R. (R, expandSet P Q) \<in> sumComposeSet \<and> hnf P \<and> hnf Q} \<union> {(R, P \<parallel> Q) |P Q R. (R, expandSet P Q) \<in> sumComposeSet \<and> hnf P \<and> hnf Q}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
P \<parallel> Q \<sim> R

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma the_enat_mono[simp]:
  assumes "m \<noteq> \<infinity>"
    and "n \<le> m"
  shows "the_enat n \<le> the_enat m"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. the_enat n \<le> the_enat m
[PROOF STEP]
using assms(1) assms(2) enat_ile
[PROOF STATE]
proof (prove)
using this:
m \<noteq> \<infinity>
n \<le> m
?n \<le> enat ?m \<Longrightarrow> \<exists>k. ?n = enat k

goal (1 subgoal):
 1. the_enat n \<le> the_enat m
[PROOF STEP]
by fastforce


[STATEMENT]
lemma llength_geq_enat_lfiniteD: "llength xs \<le> enat n \<Longrightarrow> lfinite xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. llength xs \<le> enat n \<Longrightarrow> lfinite xs
[PROOF STEP]
using not_lfinite_llength
[PROOF STATE]
proof (prove)
using this:
\<not> lfinite ?xs \<Longrightarrow> llength ?xs = \<infinity>

goal (1 subgoal):
 1. llength xs \<le> enat n \<Longrightarrow> lfinite xs
[PROOF STEP]
by force


[STATEMENT]
lemma validCI_act[simp]:
  assumes "\<exists>i\<ge>n. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>"
    and "\<gamma> (lnth ((\<pi>\<^bsub>cid\<^esub>(inf_llist t)) @\<^sub>l (inf_llist t'))) (the_enat(\<langle>cid #\<^bsub>n\<^esub> inf_llist t\<rangle>))"
  shows "eval cid t t' n \<gamma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval cid t t' n \<gamma>
[PROOF STEP]
using assms eval_def
[PROOF STATE]
proof (prove)
using this:
\<exists>i\<ge>n. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>
\<gamma> (lnth (\<pi>\<^bsub>cid\<^esub>inf_llist t @\<^sub>l inf_llist t')) (the_enat \<langle>cid #\<^bsub>enat n\<^esub>inf_llist t\<rangle>)
eval ?cid ?t ?t' ?n ?\<gamma> \<equiv> (\<exists>i\<ge>?n. \<parallel>?cid\<parallel>\<^bsub>?t i\<^esub>) \<and> ?\<gamma> (lnth (\<pi>\<^bsub>?cid\<^esub>inf_llist ?t @\<^sub>l inf_llist ?t')) (the_enat \<langle>?cid #\<^bsub>enat ?n\<^esub>inf_llist ?t\<rangle>) \<or> (\<exists>i. \<parallel>?cid\<parallel>\<^bsub>?t i\<^esub>) \<and> \<not> (\<exists>i'\<ge>?n. \<parallel>?cid\<parallel>\<^bsub>?t i'\<^esub>) \<and> ?\<gamma> (lnth (\<pi>\<^bsub>?cid\<^esub>inf_llist ?t @\<^sub>l inf_llist ?t')) (\<^bsub>?cid\<^esub>\<down>\<^bsub>?t\<^esub>?n) \<or> (\<nexists>i. \<parallel>?cid\<parallel>\<^bsub>?t i\<^esub>) \<and> ?\<gamma> (lnth (\<pi>\<^bsub>?cid\<^esub>inf_llist ?t @\<^sub>l inf_llist ?t')) ?n

goal (1 subgoal):
 1. eval cid t t' n \<gamma>
[PROOF STEP]
by simp


[STATEMENT]
lemma validCI_cont[simp]:
  assumes "\<exists>i. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>"
    and "\<nexists>i'. i'\<ge>n \<and> \<parallel>cid\<parallel>\<^bsub>t i'\<^esub>"
    and "\<gamma> (lnth ((\<pi>\<^bsub>cid\<^esub>(inf_llist t)) @\<^sub>l (inf_llist t'))) (\<^bsub>cid\<^esub>\<down>\<^bsub>t\<^esub>(n))"
  shows "eval cid t t' n \<gamma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval cid t t' n \<gamma>
[PROOF STEP]
using assms eval_def
[PROOF STATE]
proof (prove)
using this:
\<exists>i. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>
\<not> (\<exists>i'\<ge>n. \<parallel>cid\<parallel>\<^bsub>t i'\<^esub>)
\<gamma> (lnth (\<pi>\<^bsub>cid\<^esub>inf_llist t @\<^sub>l inf_llist t')) (\<^bsub>cid\<^esub>\<down>\<^bsub>t\<^esub>n)
eval ?cid ?t ?t' ?n ?\<gamma> \<equiv> (\<exists>i\<ge>?n. \<parallel>?cid\<parallel>\<^bsub>?t i\<^esub>) \<and> ?\<gamma> (lnth (\<pi>\<^bsub>?cid\<^esub>inf_llist ?t @\<^sub>l inf_llist ?t')) (the_enat \<langle>?cid #\<^bsub>enat ?n\<^esub>inf_llist ?t\<rangle>) \<or> (\<exists>i. \<parallel>?cid\<parallel>\<^bsub>?t i\<^esub>) \<and> \<not> (\<exists>i'\<ge>?n. \<parallel>?cid\<parallel>\<^bsub>?t i'\<^esub>) \<and> ?\<gamma> (lnth (\<pi>\<^bsub>?cid\<^esub>inf_llist ?t @\<^sub>l inf_llist ?t')) (\<^bsub>?cid\<^esub>\<down>\<^bsub>?t\<^esub>?n) \<or> (\<nexists>i. \<parallel>?cid\<parallel>\<^bsub>?t i\<^esub>) \<and> ?\<gamma> (lnth (\<pi>\<^bsub>?cid\<^esub>inf_llist ?t @\<^sub>l inf_llist ?t')) ?n

goal (1 subgoal):
 1. eval cid t t' n \<gamma>
[PROOF STEP]
by simp


[STATEMENT]
lemma validCI_not_act[simp]:
  assumes "\<nexists>i. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>"
    and "\<gamma> (lnth ((\<pi>\<^bsub>cid\<^esub>(inf_llist t)) @\<^sub>l (inf_llist t'))) n"
  shows "eval cid t t' n \<gamma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval cid t t' n \<gamma>
[PROOF STEP]
using assms eval_def
[PROOF STATE]
proof (prove)
using this:
\<nexists>i. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>
\<gamma> (lnth (\<pi>\<^bsub>cid\<^esub>inf_llist t @\<^sub>l inf_llist t')) n
eval ?cid ?t ?t' ?n ?\<gamma> \<equiv> (\<exists>i\<ge>?n. \<parallel>?cid\<parallel>\<^bsub>?t i\<^esub>) \<and> ?\<gamma> (lnth (\<pi>\<^bsub>?cid\<^esub>inf_llist ?t @\<^sub>l inf_llist ?t')) (the_enat \<langle>?cid #\<^bsub>enat ?n\<^esub>inf_llist ?t\<rangle>) \<or> (\<exists>i. \<parallel>?cid\<parallel>\<^bsub>?t i\<^esub>) \<and> \<not> (\<exists>i'\<ge>?n. \<parallel>?cid\<parallel>\<^bsub>?t i'\<^esub>) \<and> ?\<gamma> (lnth (\<pi>\<^bsub>?cid\<^esub>inf_llist ?t @\<^sub>l inf_llist ?t')) (\<^bsub>?cid\<^esub>\<down>\<^bsub>?t\<^esub>?n) \<or> (\<nexists>i. \<parallel>?cid\<parallel>\<^bsub>?t i\<^esub>) \<and> ?\<gamma> (lnth (\<pi>\<^bsub>?cid\<^esub>inf_llist ?t @\<^sub>l inf_llist ?t')) ?n

goal (1 subgoal):
 1. eval cid t t' n \<gamma>
[PROOF STEP]
by simp


[STATEMENT]
lemma validCE_act[simp]:
  assumes "\<exists>i\<ge>n. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>"
    and "eval cid t t' n \<gamma>"
  shows "\<gamma> (lnth ((\<pi>\<^bsub>cid\<^esub>(inf_llist t)) @\<^sub>l (inf_llist t'))) (the_enat(\<langle>cid #\<^bsub>n\<^esub> inf_llist t\<rangle>))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<gamma> (lnth (\<pi>\<^bsub>cid\<^esub>inf_llist t @\<^sub>l inf_llist t')) (the_enat \<langle>cid #\<^bsub>enat n\<^esub>inf_llist t\<rangle>)
[PROOF STEP]
using assms eval_def
[PROOF STATE]
proof (prove)
using this:
\<exists>i\<ge>n. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>
eval cid t t' n \<gamma>
eval ?cid ?t ?t' ?n ?\<gamma> \<equiv> (\<exists>i\<ge>?n. \<parallel>?cid\<parallel>\<^bsub>?t i\<^esub>) \<and> ?\<gamma> (lnth (\<pi>\<^bsub>?cid\<^esub>inf_llist ?t @\<^sub>l inf_llist ?t')) (the_enat \<langle>?cid #\<^bsub>enat ?n\<^esub>inf_llist ?t\<rangle>) \<or> (\<exists>i. \<parallel>?cid\<parallel>\<^bsub>?t i\<^esub>) \<and> \<not> (\<exists>i'\<ge>?n. \<parallel>?cid\<parallel>\<^bsub>?t i'\<^esub>) \<and> ?\<gamma> (lnth (\<pi>\<^bsub>?cid\<^esub>inf_llist ?t @\<^sub>l inf_llist ?t')) (\<^bsub>?cid\<^esub>\<down>\<^bsub>?t\<^esub>?n) \<or> (\<nexists>i. \<parallel>?cid\<parallel>\<^bsub>?t i\<^esub>) \<and> ?\<gamma> (lnth (\<pi>\<^bsub>?cid\<^esub>inf_llist ?t @\<^sub>l inf_llist ?t')) ?n

goal (1 subgoal):
 1. \<gamma> (lnth (\<pi>\<^bsub>cid\<^esub>inf_llist t @\<^sub>l inf_llist t')) (the_enat \<langle>cid #\<^bsub>enat n\<^esub>inf_llist t\<rangle>)
[PROOF STEP]
by auto


[STATEMENT]
lemma validCE_cont[simp]:
  assumes "\<exists>i. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>"
    and "\<nexists>i'. i'\<ge>n \<and> \<parallel>cid\<parallel>\<^bsub>t i'\<^esub>"
    and "eval cid t t' n \<gamma>"
  shows "\<gamma> (lnth ((\<pi>\<^bsub>cid\<^esub>(inf_llist t)) @\<^sub>l (inf_llist t'))) (\<^bsub>cid\<^esub>\<down>\<^bsub>t\<^esub>(n))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<gamma> (lnth (\<pi>\<^bsub>cid\<^esub>inf_llist t @\<^sub>l inf_llist t')) (\<^bsub>cid\<^esub>\<down>\<^bsub>t\<^esub>n)
[PROOF STEP]
using assms eval_def
[PROOF STATE]
proof (prove)
using this:
\<exists>i. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>
\<not> (\<exists>i'\<ge>n. \<parallel>cid\<parallel>\<^bsub>t i'\<^esub>)
eval cid t t' n \<gamma>
eval ?cid ?t ?t' ?n ?\<gamma> \<equiv> (\<exists>i\<ge>?n. \<parallel>?cid\<parallel>\<^bsub>?t i\<^esub>) \<and> ?\<gamma> (lnth (\<pi>\<^bsub>?cid\<^esub>inf_llist ?t @\<^sub>l inf_llist ?t')) (the_enat \<langle>?cid #\<^bsub>enat ?n\<^esub>inf_llist ?t\<rangle>) \<or> (\<exists>i. \<parallel>?cid\<parallel>\<^bsub>?t i\<^esub>) \<and> \<not> (\<exists>i'\<ge>?n. \<parallel>?cid\<parallel>\<^bsub>?t i'\<^esub>) \<and> ?\<gamma> (lnth (\<pi>\<^bsub>?cid\<^esub>inf_llist ?t @\<^sub>l inf_llist ?t')) (\<^bsub>?cid\<^esub>\<down>\<^bsub>?t\<^esub>?n) \<or> (\<nexists>i. \<parallel>?cid\<parallel>\<^bsub>?t i\<^esub>) \<and> ?\<gamma> (lnth (\<pi>\<^bsub>?cid\<^esub>inf_llist ?t @\<^sub>l inf_llist ?t')) ?n

goal (1 subgoal):
 1. \<gamma> (lnth (\<pi>\<^bsub>cid\<^esub>inf_llist t @\<^sub>l inf_llist t')) (\<^bsub>cid\<^esub>\<down>\<^bsub>t\<^esub>n)
[PROOF STEP]
by auto


[STATEMENT]
lemma validCE_not_act[simp]:
  assumes "\<nexists>i. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>"
    and "eval cid t t' n \<gamma>"
  shows "\<gamma> (lnth ((\<pi>\<^bsub>cid\<^esub>(inf_llist t)) @\<^sub>l (inf_llist t'))) n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<gamma> (lnth (\<pi>\<^bsub>cid\<^esub>inf_llist t @\<^sub>l inf_llist t')) n
[PROOF STEP]
using assms eval_def
[PROOF STATE]
proof (prove)
using this:
\<nexists>i. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>
eval cid t t' n \<gamma>
eval ?cid ?t ?t' ?n ?\<gamma> \<equiv> (\<exists>i\<ge>?n. \<parallel>?cid\<parallel>\<^bsub>?t i\<^esub>) \<and> ?\<gamma> (lnth (\<pi>\<^bsub>?cid\<^esub>inf_llist ?t @\<^sub>l inf_llist ?t')) (the_enat \<langle>?cid #\<^bsub>enat ?n\<^esub>inf_llist ?t\<rangle>) \<or> (\<exists>i. \<parallel>?cid\<parallel>\<^bsub>?t i\<^esub>) \<and> \<not> (\<exists>i'\<ge>?n. \<parallel>?cid\<parallel>\<^bsub>?t i'\<^esub>) \<and> ?\<gamma> (lnth (\<pi>\<^bsub>?cid\<^esub>inf_llist ?t @\<^sub>l inf_llist ?t')) (\<^bsub>?cid\<^esub>\<down>\<^bsub>?t\<^esub>?n) \<or> (\<nexists>i. \<parallel>?cid\<parallel>\<^bsub>?t i\<^esub>) \<and> ?\<gamma> (lnth (\<pi>\<^bsub>?cid\<^esub>inf_llist ?t @\<^sub>l inf_llist ?t')) ?n

goal (1 subgoal):
 1. \<gamma> (lnth (\<pi>\<^bsub>cid\<^esub>inf_llist t @\<^sub>l inf_llist t')) n
[PROOF STEP]
by auto


[STATEMENT]
lemma predI[intro]:
  fixes cid t t' n P
  assumes "P"
  shows "eval cid t t' n (pred P)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval cid t t' n (pred P)
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> eval cid t t' n (pred P)
 2. \<not> ?P \<Longrightarrow> eval cid t t' n (pred P)
[PROOF STEP]
assume "(\<exists>i. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>)"
[PROOF STATE]
proof (state)
this:
\<exists>i. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>

goal (2 subgoals):
 1. ?P \<Longrightarrow> eval cid t t' n (pred P)
 2. \<not> ?P \<Longrightarrow> eval cid t t' n (pred P)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval cid t t' n (pred P)
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> eval cid t t' n (pred P)
 2. \<not> ?P \<Longrightarrow> eval cid t t' n (pred P)
[PROOF STEP]
assume "\<exists>i\<ge>n. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>"
[PROOF STATE]
proof (state)
this:
\<exists>i\<ge>n. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>

goal (2 subgoals):
 1. ?P \<Longrightarrow> eval cid t t' n (pred P)
 2. \<not> ?P \<Longrightarrow> eval cid t t' n (pred P)
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
P
\<exists>i\<ge>n. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
P
\<exists>i\<ge>n. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>

goal (1 subgoal):
 1. eval cid t t' n (pred P)
[PROOF STEP]
using eval_def pred_def
[PROOF STATE]
proof (prove)
using this:
P
\<exists>i\<ge>n. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>
eval ?cid ?t ?t' ?n ?\<gamma> \<equiv> (\<exists>i\<ge>?n. \<parallel>?cid\<parallel>\<^bsub>?t i\<^esub>) \<and> ?\<gamma> (lnth (\<pi>\<^bsub>?cid\<^esub>inf_llist ?t @\<^sub>l inf_llist ?t')) (the_enat \<langle>?cid #\<^bsub>enat ?n\<^esub>inf_llist ?t\<rangle>) \<or> (\<exists>i. \<parallel>?cid\<parallel>\<^bsub>?t i\<^esub>) \<and> \<not> (\<exists>i'\<ge>?n. \<parallel>?cid\<parallel>\<^bsub>?t i'\<^esub>) \<and> ?\<gamma> (lnth (\<pi>\<^bsub>?cid\<^esub>inf_llist ?t @\<^sub>l inf_llist ?t')) (\<^bsub>?cid\<^esub>\<down>\<^bsub>?t\<^esub>?n) \<or> (\<nexists>i. \<parallel>?cid\<parallel>\<^bsub>?t i\<^esub>) \<and> ?\<gamma> (lnth (\<pi>\<^bsub>?cid\<^esub>inf_llist ?t @\<^sub>l inf_llist ?t')) ?n
pred ?P \<equiv> \<lambda>t n. ?P

goal (1 subgoal):
 1. eval cid t t' n (pred P)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
eval cid t t' n (pred P)

goal (1 subgoal):
 1. \<not> (\<exists>i\<ge>n. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>) \<Longrightarrow> eval cid t t' n (pred P)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> (\<exists>i\<ge>n. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>) \<Longrightarrow> eval cid t t' n (pred P)
[PROOF STEP]
assume "\<not> (\<exists>i\<ge>n. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>)"
[PROOF STATE]
proof (state)
this:
\<not> (\<exists>i\<ge>n. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>)

goal (1 subgoal):
 1. \<not> (\<exists>i\<ge>n. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>) \<Longrightarrow> eval cid t t' n (pred P)
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
P
\<not> (\<exists>i\<ge>n. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
P
\<not> (\<exists>i\<ge>n. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>)

goal (1 subgoal):
 1. eval cid t t' n (pred P)
[PROOF STEP]
using eval_def pred_def
[PROOF STATE]
proof (prove)
using this:
P
\<not> (\<exists>i\<ge>n. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>)
eval ?cid ?t ?t' ?n ?\<gamma> \<equiv> (\<exists>i\<ge>?n. \<parallel>?cid\<parallel>\<^bsub>?t i\<^esub>) \<and> ?\<gamma> (lnth (\<pi>\<^bsub>?cid\<^esub>inf_llist ?t @\<^sub>l inf_llist ?t')) (the_enat \<langle>?cid #\<^bsub>enat ?n\<^esub>inf_llist ?t\<rangle>) \<or> (\<exists>i. \<parallel>?cid\<parallel>\<^bsub>?t i\<^esub>) \<and> \<not> (\<exists>i'\<ge>?n. \<parallel>?cid\<parallel>\<^bsub>?t i'\<^esub>) \<and> ?\<gamma> (lnth (\<pi>\<^bsub>?cid\<^esub>inf_llist ?t @\<^sub>l inf_llist ?t')) (\<^bsub>?cid\<^esub>\<down>\<^bsub>?t\<^esub>?n) \<or> (\<nexists>i. \<parallel>?cid\<parallel>\<^bsub>?t i\<^esub>) \<and> ?\<gamma> (lnth (\<pi>\<^bsub>?cid\<^esub>inf_llist ?t @\<^sub>l inf_llist ?t')) ?n
pred ?P \<equiv> \<lambda>t n. ?P

goal (1 subgoal):
 1. eval cid t t' n (pred P)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
eval cid t t' n (pred P)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
eval cid t t' n (pred P)

goal (1 subgoal):
 1. \<nexists>i. \<parallel>cid\<parallel>\<^bsub>t i\<^esub> \<Longrightarrow> eval cid t t' n (pred P)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<nexists>i. \<parallel>cid\<parallel>\<^bsub>t i\<^esub> \<Longrightarrow> eval cid t t' n (pred P)
[PROOF STEP]
assume "\<not>(\<exists>i. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>)"
[PROOF STATE]
proof (state)
this:
\<nexists>i. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>

goal (1 subgoal):
 1. \<nexists>i. \<parallel>cid\<parallel>\<^bsub>t i\<^esub> \<Longrightarrow> eval cid t t' n (pred P)
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
P
\<nexists>i. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
P
\<nexists>i. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>

goal (1 subgoal):
 1. eval cid t t' n (pred P)
[PROOF STEP]
using eval_def pred_def
[PROOF STATE]
proof (prove)
using this:
P
\<nexists>i. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>
eval ?cid ?t ?t' ?n ?\<gamma> \<equiv> (\<exists>i\<ge>?n. \<parallel>?cid\<parallel>\<^bsub>?t i\<^esub>) \<and> ?\<gamma> (lnth (\<pi>\<^bsub>?cid\<^esub>inf_llist ?t @\<^sub>l inf_llist ?t')) (the_enat \<langle>?cid #\<^bsub>enat ?n\<^esub>inf_llist ?t\<rangle>) \<or> (\<exists>i. \<parallel>?cid\<parallel>\<^bsub>?t i\<^esub>) \<and> \<not> (\<exists>i'\<ge>?n. \<parallel>?cid\<parallel>\<^bsub>?t i'\<^esub>) \<and> ?\<gamma> (lnth (\<pi>\<^bsub>?cid\<^esub>inf_llist ?t @\<^sub>l inf_llist ?t')) (\<^bsub>?cid\<^esub>\<down>\<^bsub>?t\<^esub>?n) \<or> (\<nexists>i. \<parallel>?cid\<parallel>\<^bsub>?t i\<^esub>) \<and> ?\<gamma> (lnth (\<pi>\<^bsub>?cid\<^esub>inf_llist ?t @\<^sub>l inf_llist ?t')) ?n
pred ?P \<equiv> \<lambda>t n. ?P

goal (1 subgoal):
 1. eval cid t t' n (pred P)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
eval cid t t' n (pred P)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma predE[elim]:
  fixes cid t t' n P
  assumes "eval cid t t' n (pred P)"
  shows "P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> P
 2. \<not> ?P \<Longrightarrow> P
[PROOF STEP]
assume "(\<exists>i. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>)"
[PROOF STATE]
proof (state)
this:
\<exists>i. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>

goal (2 subgoals):
 1. ?P \<Longrightarrow> P
 2. \<not> ?P \<Longrightarrow> P
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> P
 2. \<not> ?P \<Longrightarrow> P
[PROOF STEP]
assume "\<exists>i\<ge>n. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>"
[PROOF STATE]
proof (state)
this:
\<exists>i\<ge>n. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>

goal (2 subgoals):
 1. ?P \<Longrightarrow> P
 2. \<not> ?P \<Longrightarrow> P
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
eval cid t t' n (pred P)
\<exists>i\<ge>n. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
eval cid t t' n (pred P)
\<exists>i\<ge>n. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>

goal (1 subgoal):
 1. P
[PROOF STEP]
using eval_def pred_def
[PROOF STATE]
proof (prove)
using this:
eval cid t t' n (pred P)
\<exists>i\<ge>n. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>
eval ?cid ?t ?t' ?n ?\<gamma> \<equiv> (\<exists>i\<ge>?n. \<parallel>?cid\<parallel>\<^bsub>?t i\<^esub>) \<and> ?\<gamma> (lnth (\<pi>\<^bsub>?cid\<^esub>inf_llist ?t @\<^sub>l inf_llist ?t')) (the_enat \<langle>?cid #\<^bsub>enat ?n\<^esub>inf_llist ?t\<rangle>) \<or> (\<exists>i. \<parallel>?cid\<parallel>\<^bsub>?t i\<^esub>) \<and> \<not> (\<exists>i'\<ge>?n. \<parallel>?cid\<parallel>\<^bsub>?t i'\<^esub>) \<and> ?\<gamma> (lnth (\<pi>\<^bsub>?cid\<^esub>inf_llist ?t @\<^sub>l inf_llist ?t')) (\<^bsub>?cid\<^esub>\<down>\<^bsub>?t\<^esub>?n) \<or> (\<nexists>i. \<parallel>?cid\<parallel>\<^bsub>?t i\<^esub>) \<and> ?\<gamma> (lnth (\<pi>\<^bsub>?cid\<^esub>inf_llist ?t @\<^sub>l inf_llist ?t')) ?n
pred ?P \<equiv> \<lambda>t n. ?P

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

goal (1 subgoal):
 1. \<not> (\<exists>i\<ge>n. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>) \<Longrightarrow> P
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> (\<exists>i\<ge>n. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>) \<Longrightarrow> P
[PROOF STEP]
assume "\<not> (\<exists>i\<ge>n. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>)"
[PROOF STATE]
proof (state)
this:
\<not> (\<exists>i\<ge>n. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>)

goal (1 subgoal):
 1. \<not> (\<exists>i\<ge>n. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>) \<Longrightarrow> P
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
eval cid t t' n (pred P)
\<not> (\<exists>i\<ge>n. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
eval cid t t' n (pred P)
\<not> (\<exists>i\<ge>n. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>)

goal (1 subgoal):
 1. P
[PROOF STEP]
using eval_def pred_def
[PROOF STATE]
proof (prove)
using this:
eval cid t t' n (pred P)
\<not> (\<exists>i\<ge>n. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>)
eval ?cid ?t ?t' ?n ?\<gamma> \<equiv> (\<exists>i\<ge>?n. \<parallel>?cid\<parallel>\<^bsub>?t i\<^esub>) \<and> ?\<gamma> (lnth (\<pi>\<^bsub>?cid\<^esub>inf_llist ?t @\<^sub>l inf_llist ?t')) (the_enat \<langle>?cid #\<^bsub>enat ?n\<^esub>inf_llist ?t\<rangle>) \<or> (\<exists>i. \<parallel>?cid\<parallel>\<^bsub>?t i\<^esub>) \<and> \<not> (\<exists>i'\<ge>?n. \<parallel>?cid\<parallel>\<^bsub>?t i'\<^esub>) \<and> ?\<gamma> (lnth (\<pi>\<^bsub>?cid\<^esub>inf_llist ?t @\<^sub>l inf_llist ?t')) (\<^bsub>?cid\<^esub>\<down>\<^bsub>?t\<^esub>?n) \<or> (\<nexists>i. \<parallel>?cid\<parallel>\<^bsub>?t i\<^esub>) \<and> ?\<gamma> (lnth (\<pi>\<^bsub>?cid\<^esub>inf_llist ?t @\<^sub>l inf_llist ?t')) ?n
pred ?P \<equiv> \<lambda>t n. ?P

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

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

goal (1 subgoal):
 1. \<nexists>i. \<parallel>cid\<parallel>\<^bsub>t i\<^esub> \<Longrightarrow> P
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<nexists>i. \<parallel>cid\<parallel>\<^bsub>t i\<^esub> \<Longrightarrow> P
[PROOF STEP]
assume "\<not>(\<exists>i. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>)"
[PROOF STATE]
proof (state)
this:
\<nexists>i. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>

goal (1 subgoal):
 1. \<nexists>i. \<parallel>cid\<parallel>\<^bsub>t i\<^esub> \<Longrightarrow> P
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
eval cid t t' n (pred P)
\<nexists>i. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
eval cid t t' n (pred P)
\<nexists>i. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>

goal (1 subgoal):
 1. P
[PROOF STEP]
using eval_def pred_def
[PROOF STATE]
proof (prove)
using this:
eval cid t t' n (pred P)
\<nexists>i. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>
eval ?cid ?t ?t' ?n ?\<gamma> \<equiv> (\<exists>i\<ge>?n. \<parallel>?cid\<parallel>\<^bsub>?t i\<^esub>) \<and> ?\<gamma> (lnth (\<pi>\<^bsub>?cid\<^esub>inf_llist ?t @\<^sub>l inf_llist ?t')) (the_enat \<langle>?cid #\<^bsub>enat ?n\<^esub>inf_llist ?t\<rangle>) \<or> (\<exists>i. \<parallel>?cid\<parallel>\<^bsub>?t i\<^esub>) \<and> \<not> (\<exists>i'\<ge>?n. \<parallel>?cid\<parallel>\<^bsub>?t i'\<^esub>) \<and> ?\<gamma> (lnth (\<pi>\<^bsub>?cid\<^esub>inf_llist ?t @\<^sub>l inf_llist ?t')) (\<^bsub>?cid\<^esub>\<down>\<^bsub>?t\<^esub>?n) \<or> (\<nexists>i. \<parallel>?cid\<parallel>\<^bsub>?t i\<^esub>) \<and> ?\<gamma> (lnth (\<pi>\<^bsub>?cid\<^esub>inf_llist ?t @\<^sub>l inf_llist ?t')) ?n
pred ?P \<equiv> \<lambda>t n. ?P

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma impI[intro!]:
  assumes "eval cid t t' n \<gamma> \<longrightarrow> eval cid t t' n \<gamma>'"
  shows "eval cid t t' n (\<gamma> \<longrightarrow>\<^sup>b \<gamma>')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval cid t t' n (\<gamma> \<longrightarrow>\<^sup>b \<gamma>')
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> eval cid t t' n (\<gamma> \<longrightarrow>\<^sup>b \<gamma>')
 2. \<not> ?P \<Longrightarrow> eval cid t t' n (\<gamma> \<longrightarrow>\<^sup>b \<gamma>')
[PROOF STEP]
assume "\<exists>i. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>"
[PROOF STATE]
proof (state)
this:
\<exists>i. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>

goal (2 subgoals):
 1. ?P \<Longrightarrow> eval cid t t' n (\<gamma> \<longrightarrow>\<^sup>b \<gamma>')
 2. \<not> ?P \<Longrightarrow> eval cid t t' n (\<gamma> \<longrightarrow>\<^sup>b \<gamma>')
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval cid t t' n (\<gamma> \<longrightarrow>\<^sup>b \<gamma>')
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> eval cid t t' n (\<gamma> \<longrightarrow>\<^sup>b \<gamma>')
 2. \<not> ?P \<Longrightarrow> eval cid t t' n (\<gamma> \<longrightarrow>\<^sup>b \<gamma>')
[PROOF STEP]
assume "\<exists>i\<ge>n. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>"
[PROOF STATE]
proof (state)
this:
\<exists>i\<ge>n. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>

goal (2 subgoals):
 1. ?P \<Longrightarrow> eval cid t t' n (\<gamma> \<longrightarrow>\<^sup>b \<gamma>')
 2. \<not> ?P \<Longrightarrow> eval cid t t' n (\<gamma> \<longrightarrow>\<^sup>b \<gamma>')
[PROOF STEP]
with \<open>eval cid t t' n \<gamma> \<longrightarrow> eval cid t t' n \<gamma>'\<close>
[PROOF STATE]
proof (chain)
picking this:
eval cid t t' n \<gamma> \<longrightarrow> eval cid t t' n \<gamma>'
\<exists>i\<ge>n. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>
[PROOF STEP]
have "\<gamma> (lnth (\<pi>\<^bsub>cid\<^esub>inf_llist t @\<^sub>l inf_llist t')) (the_enat \<langle>cid #\<^bsub>enat n\<^esub>inf_llist t\<rangle>)
      \<longrightarrow> \<gamma>' (lnth (\<pi>\<^bsub>cid\<^esub>inf_llist t @\<^sub>l inf_llist t')) (the_enat \<langle>cid #\<^bsub>enat n\<^esub>inf_llist t\<rangle>)"
[PROOF STATE]
proof (prove)
using this:
eval cid t t' n \<gamma> \<longrightarrow> eval cid t t' n \<gamma>'
\<exists>i\<ge>n. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>

goal (1 subgoal):
 1. \<gamma> (lnth (\<pi>\<^bsub>cid\<^esub>inf_llist t @\<^sub>l inf_llist t')) (the_enat \<langle>cid #\<^bsub>enat n\<^esub>inf_llist t\<rangle>) \<longrightarrow> \<gamma>' (lnth (\<pi>\<^bsub>cid\<^esub>inf_llist t @\<^sub>l inf_llist t')) (the_enat \<langle>cid #\<^bsub>enat n\<^esub>inf_llist t\<rangle>)
[PROOF STEP]
using eval_def
[PROOF STATE]
proof (prove)
using this:
eval cid t t' n \<gamma> \<longrightarrow> eval cid t t' n \<gamma>'
\<exists>i\<ge>n. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>
eval ?cid ?t ?t' ?n ?\<gamma> \<equiv> (\<exists>i\<ge>?n. \<parallel>?cid\<parallel>\<^bsub>?t i\<^esub>) \<and> ?\<gamma> (lnth (\<pi>\<^bsub>?cid\<^esub>inf_llist ?t @\<^sub>l inf_llist ?t')) (the_enat \<langle>?cid #\<^bsub>enat ?n\<^esub>inf_llist ?t\<rangle>) \<or> (\<exists>i. \<parallel>?cid\<parallel>\<^bsub>?t i\<^esub>) \<and> \<not> (\<exists>i'\<ge>?n. \<parallel>?cid\<parallel>\<^bsub>?t i'\<^esub>) \<and> ?\<gamma> (lnth (\<pi>\<^bsub>?cid\<^esub>inf_llist ?t @\<^sub>l inf_llist ?t')) (\<^bsub>?cid\<^esub>\<down>\<^bsub>?t\<^esub>?n) \<or> (\<nexists>i. \<parallel>?cid\<parallel>\<^bsub>?t i\<^esub>) \<and> ?\<gamma> (lnth (\<pi>\<^bsub>?cid\<^esub>inf_llist ?t @\<^sub>l inf_llist ?t')) ?n

goal (1 subgoal):
 1. \<gamma> (lnth (\<pi>\<^bsub>cid\<^esub>inf_llist t @\<^sub>l inf_llist t')) (the_enat \<langle>cid #\<^bsub>enat n\<^esub>inf_llist t\<rangle>) \<longrightarrow> \<gamma>' (lnth (\<pi>\<^bsub>cid\<^esub>inf_llist t @\<^sub>l inf_llist t')) (the_enat \<langle>cid #\<^bsub>enat n\<^esub>inf_llist t\<rangle>)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<gamma> (lnth (\<pi>\<^bsub>cid\<^esub>inf_llist t @\<^sub>l inf_llist t')) (the_enat \<langle>cid #\<^bsub>enat n\<^esub>inf_llist t\<rangle>) \<longrightarrow> \<gamma>' (lnth (\<pi>\<^bsub>cid\<^esub>inf_llist t @\<^sub>l inf_llist t')) (the_enat \<langle>cid #\<^bsub>enat n\<^esub>inf_llist t\<rangle>)

goal (2 subgoals):
 1. ?P \<Longrightarrow> eval cid t t' n (\<gamma> \<longrightarrow>\<^sup>b \<gamma>')
 2. \<not> ?P \<Longrightarrow> eval cid t t' n (\<gamma> \<longrightarrow>\<^sup>b \<gamma>')
[PROOF STEP]
with \<open>\<exists>i\<ge>n. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>\<close>
[PROOF STATE]
proof (chain)
picking this:
\<exists>i\<ge>n. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>
\<gamma> (lnth (\<pi>\<^bsub>cid\<^esub>inf_llist t @\<^sub>l inf_llist t')) (the_enat \<langle>cid #\<^bsub>enat n\<^esub>inf_llist t\<rangle>) \<longrightarrow> \<gamma>' (lnth (\<pi>\<^bsub>cid\<^esub>inf_llist t @\<^sub>l inf_llist t')) (the_enat \<langle>cid #\<^bsub>enat n\<^esub>inf_llist t\<rangle>)
[PROOF STEP]
have "eval cid t t' n (\<lambda>t n. \<gamma> t n \<longrightarrow> \<gamma>' t n)"
[PROOF STATE]
proof (prove)
using this:
\<exists>i\<ge>n. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>
\<gamma> (lnth (\<pi>\<^bsub>cid\<^esub>inf_llist t @\<^sub>l inf_llist t')) (the_enat \<langle>cid #\<^bsub>enat n\<^esub>inf_llist t\<rangle>) \<longrightarrow> \<gamma>' (lnth (\<pi>\<^bsub>cid\<^esub>inf_llist t @\<^sub>l inf_llist t')) (the_enat \<langle>cid #\<^bsub>enat n\<^esub>inf_llist t\<rangle>)

goal (1 subgoal):
 1. eval cid t t' n (\<lambda>t n. \<gamma> t n \<longrightarrow> \<gamma>' t n)
[PROOF STEP]
using validCI_act[where \<gamma>="\<lambda> t n. \<gamma> t n \<longrightarrow> \<gamma>' t n"]
[PROOF STATE]
proof (prove)
using this:
\<exists>i\<ge>n. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>
\<gamma> (lnth (\<pi>\<^bsub>cid\<^esub>inf_llist t @\<^sub>l inf_llist t')) (the_enat \<langle>cid #\<^bsub>enat n\<^esub>inf_llist t\<rangle>) \<longrightarrow> \<gamma>' (lnth (\<pi>\<^bsub>cid\<^esub>inf_llist t @\<^sub>l inf_llist t')) (the_enat \<langle>cid #\<^bsub>enat n\<^esub>inf_llist t\<rangle>)
\<lbrakk>\<exists>i\<ge>?n. \<parallel>?cid\<parallel>\<^bsub>?t i\<^esub>; \<gamma> (lnth (\<pi>\<^bsub>?cid\<^esub>inf_llist ?t @\<^sub>l inf_llist ?t')) (the_enat \<langle>?cid #\<^bsub>enat ?n\<^esub>inf_llist ?t\<rangle>) \<longrightarrow> \<gamma>' (lnth (\<pi>\<^bsub>?cid\<^esub>inf_llist ?t @\<^sub>l inf_llist ?t')) (the_enat \<langle>?cid #\<^bsub>enat ?n\<^esub>inf_llist ?t\<rangle>)\<rbrakk> \<Longrightarrow> eval ?cid ?t ?t' ?n (\<lambda>t n. \<gamma> t n \<longrightarrow> \<gamma>' t n)

goal (1 subgoal):
 1. eval cid t t' n (\<lambda>t n. \<gamma> t n \<longrightarrow> \<gamma>' t n)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
eval cid t t' n (\<lambda>t n. \<gamma> t n \<longrightarrow> \<gamma>' t n)

goal (2 subgoals):
 1. ?P \<Longrightarrow> eval cid t t' n (\<gamma> \<longrightarrow>\<^sup>b \<gamma>')
 2. \<not> ?P \<Longrightarrow> eval cid t t' n (\<gamma> \<longrightarrow>\<^sup>b \<gamma>')
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
eval cid t t' n (\<lambda>t n. \<gamma> t n \<longrightarrow> \<gamma>' t n)

goal (1 subgoal):
 1. eval cid t t' n (\<gamma> \<longrightarrow>\<^sup>b \<gamma>')
[PROOF STEP]
using imp_def
[PROOF STATE]
proof (prove)
using this:
eval cid t t' n (\<lambda>t n. \<gamma> t n \<longrightarrow> \<gamma>' t n)
?\<gamma> \<longrightarrow>\<^sup>b ?\<gamma>' \<equiv> \<lambda>t n. ?\<gamma> t n \<longrightarrow> ?\<gamma>' t n

goal (1 subgoal):
 1. eval cid t t' n (\<gamma> \<longrightarrow>\<^sup>b \<gamma>')
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
eval cid t t' n (\<gamma> \<longrightarrow>\<^sup>b \<gamma>')

goal (1 subgoal):
 1. \<not> (\<exists>i\<ge>n. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>) \<Longrightarrow> eval cid t t' n (\<gamma> \<longrightarrow>\<^sup>b \<gamma>')
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> (\<exists>i\<ge>n. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>) \<Longrightarrow> eval cid t t' n (\<gamma> \<longrightarrow>\<^sup>b \<gamma>')
[PROOF STEP]
assume "\<not> (\<exists>i\<ge>n. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>)"
[PROOF STATE]
proof (state)
this:
\<not> (\<exists>i\<ge>n. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>)

goal (1 subgoal):
 1. \<not> (\<exists>i\<ge>n. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>) \<Longrightarrow> eval cid t t' n (\<gamma> \<longrightarrow>\<^sup>b \<gamma>')
[PROOF STEP]
with \<open>\<exists>i. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>\<close> \<open>eval cid t t' n \<gamma> \<longrightarrow> eval cid t t' n \<gamma>'\<close>
[PROOF STATE]
proof (chain)
picking this:
\<exists>i. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>
eval cid t t' n \<gamma> \<longrightarrow> eval cid t t' n \<gamma>'
\<not> (\<exists>i\<ge>n. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>)
[PROOF STEP]
have "\<gamma> (lnth (\<pi>\<^bsub>cid\<^esub>inf_llist t @\<^sub>l inf_llist t')) (\<^bsub>cid\<^esub>\<down>\<^bsub>t\<^esub>n)
      \<longrightarrow> \<gamma>' (lnth (\<pi>\<^bsub>cid\<^esub>inf_llist t @\<^sub>l inf_llist t')) (\<^bsub>cid\<^esub>\<down>\<^bsub>t\<^esub>n)"
[PROOF STATE]
proof (prove)
using this:
\<exists>i. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>
eval cid t t' n \<gamma> \<longrightarrow> eval cid t t' n \<gamma>'
\<not> (\<exists>i\<ge>n. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>)

goal (1 subgoal):
 1. \<gamma> (lnth (\<pi>\<^bsub>cid\<^esub>inf_llist t @\<^sub>l inf_llist t')) (\<^bsub>cid\<^esub>\<down>\<^bsub>t\<^esub>n) \<longrightarrow> \<gamma>' (lnth (\<pi>\<^bsub>cid\<^esub>inf_llist t @\<^sub>l inf_llist t')) (\<^bsub>cid\<^esub>\<down>\<^bsub>t\<^esub>n)
[PROOF STEP]
using eval_def
[PROOF STATE]
proof (prove)
using this:
\<exists>i. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>
eval cid t t' n \<gamma> \<longrightarrow> eval cid t t' n \<gamma>'
\<not> (\<exists>i\<ge>n. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>)
eval ?cid ?t ?t' ?n ?\<gamma> \<equiv> (\<exists>i\<ge>?n. \<parallel>?cid\<parallel>\<^bsub>?t i\<^esub>) \<and> ?\<gamma> (lnth (\<pi>\<^bsub>?cid\<^esub>inf_llist ?t @\<^sub>l inf_llist ?t')) (the_enat \<langle>?cid #\<^bsub>enat ?n\<^esub>inf_llist ?t\<rangle>) \<or> (\<exists>i. \<parallel>?cid\<parallel>\<^bsub>?t i\<^esub>) \<and> \<not> (\<exists>i'\<ge>?n. \<parallel>?cid\<parallel>\<^bsub>?t i'\<^esub>) \<and> ?\<gamma> (lnth (\<pi>\<^bsub>?cid\<^esub>inf_llist ?t @\<^sub>l inf_llist ?t')) (\<^bsub>?cid\<^esub>\<down>\<^bsub>?t\<^esub>?n) \<or> (\<nexists>i. \<parallel>?cid\<parallel>\<^bsub>?t i\<^esub>) \<and> ?\<gamma> (lnth (\<pi>\<^bsub>?cid\<^esub>inf_llist ?t @\<^sub>l inf_llist ?t')) ?n

goal (1 subgoal):
 1. \<gamma> (lnth (\<pi>\<^bsub>cid\<^esub>inf_llist t @\<^sub>l inf_llist t')) (\<^bsub>cid\<^esub>\<down>\<^bsub>t\<^esub>n) \<longrightarrow> \<gamma>' (lnth (\<pi>\<^bsub>cid\<^esub>inf_llist t @\<^sub>l inf_llist t')) (\<^bsub>cid\<^esub>\<down>\<^bsub>t\<^esub>n)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<gamma> (lnth (\<pi>\<^bsub>cid\<^esub>inf_llist t @\<^sub>l inf_llist t')) (\<^bsub>cid\<^esub>\<down>\<^bsub>t\<^esub>n) \<longrightarrow> \<gamma>' (lnth (\<pi>\<^bsub>cid\<^esub>inf_llist t @\<^sub>l inf_llist t')) (\<^bsub>cid\<^esub>\<down>\<^bsub>t\<^esub>n)

goal (1 subgoal):
 1. \<not> (\<exists>i\<ge>n. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>) \<Longrightarrow> eval cid t t' n (\<gamma> \<longrightarrow>\<^sup>b \<gamma>')
[PROOF STEP]
with \<open>\<exists>i. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>\<close> \<open>\<not> (\<exists>i\<ge>n. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>)\<close>
[PROOF STATE]
proof (chain)
picking this:
\<exists>i. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>
\<not> (\<exists>i\<ge>n. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>)
\<gamma> (lnth (\<pi>\<^bsub>cid\<^esub>inf_llist t @\<^sub>l inf_llist t')) (\<^bsub>cid\<^esub>\<down>\<^bsub>t\<^esub>n) \<longrightarrow> \<gamma>' (lnth (\<pi>\<^bsub>cid\<^esub>inf_llist t @\<^sub>l inf_llist t')) (\<^bsub>cid\<^esub>\<down>\<^bsub>t\<^esub>n)
[PROOF STEP]
have "eval cid t t' n (\<lambda>t n. \<gamma> t n \<longrightarrow> \<gamma>' t n)"
[PROOF STATE]
proof (prove)
using this:
\<exists>i. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>
\<not> (\<exists>i\<ge>n. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>)
\<gamma> (lnth (\<pi>\<^bsub>cid\<^esub>inf_llist t @\<^sub>l inf_llist t')) (\<^bsub>cid\<^esub>\<down>\<^bsub>t\<^esub>n) \<longrightarrow> \<gamma>' (lnth (\<pi>\<^bsub>cid\<^esub>inf_llist t @\<^sub>l inf_llist t')) (\<^bsub>cid\<^esub>\<down>\<^bsub>t\<^esub>n)

goal (1 subgoal):
 1. eval cid t t' n (\<lambda>t n. \<gamma> t n \<longrightarrow> \<gamma>' t n)
[PROOF STEP]
using validCI_cont[where \<gamma>="\<lambda> t n. \<gamma> t n \<longrightarrow> \<gamma>' t n"]
[PROOF STATE]
proof (prove)
using this:
\<exists>i. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>
\<not> (\<exists>i\<ge>n. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>)
\<gamma> (lnth (\<pi>\<^bsub>cid\<^esub>inf_llist t @\<^sub>l inf_llist t')) (\<^bsub>cid\<^esub>\<down>\<^bsub>t\<^esub>n) \<longrightarrow> \<gamma>' (lnth (\<pi>\<^bsub>cid\<^esub>inf_llist t @\<^sub>l inf_llist t')) (\<^bsub>cid\<^esub>\<down>\<^bsub>t\<^esub>n)
\<lbrakk>\<exists>i. \<parallel>?cid\<parallel>\<^bsub>?t i\<^esub>; \<not> (\<exists>i'\<ge>?n. \<parallel>?cid\<parallel>\<^bsub>?t i'\<^esub>); \<gamma> (lnth (\<pi>\<^bsub>?cid\<^esub>inf_llist ?t @\<^sub>l inf_llist ?t')) (\<^bsub>?cid\<^esub>\<down>\<^bsub>?t\<^esub>?n) \<longrightarrow> \<gamma>' (lnth (\<pi>\<^bsub>?cid\<^esub>inf_llist ?t @\<^sub>l inf_llist ?t')) (\<^bsub>?cid\<^esub>\<down>\<^bsub>?t\<^esub>?n)\<rbrakk> \<Longrightarrow> eval ?cid ?t ?t' ?n (\<lambda>t n. \<gamma> t n \<longrightarrow> \<gamma>' t n)

goal (1 subgoal):
 1. eval cid t t' n (\<lambda>t n. \<gamma> t n \<longrightarrow> \<gamma>' t n)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
eval cid t t' n (\<lambda>t n. \<gamma> t n \<longrightarrow> \<gamma>' t n)

goal (1 subgoal):
 1. \<not> (\<exists>i\<ge>n. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>) \<Longrightarrow> eval cid t t' n (\<gamma> \<longrightarrow>\<^sup>b \<gamma>')
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
eval cid t t' n (\<lambda>t n. \<gamma> t n \<longrightarrow> \<gamma>' t n)

goal (1 subgoal):
 1. eval cid t t' n (\<gamma> \<longrightarrow>\<^sup>b \<gamma>')
[PROOF STEP]
using imp_def
[PROOF STATE]
proof (prove)
using this:
eval cid t t' n (\<lambda>t n. \<gamma> t n \<longrightarrow> \<gamma>' t n)
?\<gamma> \<longrightarrow>\<^sup>b ?\<gamma>' \<equiv> \<lambda>t n. ?\<gamma> t n \<longrightarrow> ?\<gamma>' t n

goal (1 subgoal):
 1. eval cid t t' n (\<gamma> \<longrightarrow>\<^sup>b \<gamma>')
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
eval cid t t' n (\<gamma> \<longrightarrow>\<^sup>b \<gamma>')

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
eval cid t t' n (\<gamma> \<longrightarrow>\<^sup>b \<gamma>')

goal (1 subgoal):
 1. \<nexists>i. \<parallel>cid\<parallel>\<^bsub>t i\<^esub> \<Longrightarrow> eval cid t t' n (\<gamma> \<longrightarrow>\<^sup>b \<gamma>')
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<nexists>i. \<parallel>cid\<parallel>\<^bsub>t i\<^esub> \<Longrightarrow> eval cid t t' n (\<gamma> \<longrightarrow>\<^sup>b \<gamma>')
[PROOF STEP]
assume "\<not>(\<exists>i. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>)"
[PROOF STATE]
proof (state)
this:
\<nexists>i. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>

goal (1 subgoal):
 1. \<nexists>i. \<parallel>cid\<parallel>\<^bsub>t i\<^esub> \<Longrightarrow> eval cid t t' n (\<gamma> \<longrightarrow>\<^sup>b \<gamma>')
[PROOF STEP]
with \<open>eval cid t t' n \<gamma> \<longrightarrow> eval cid t t' n \<gamma>'\<close>
[PROOF STATE]
proof (chain)
picking this:
eval cid t t' n \<gamma> \<longrightarrow> eval cid t t' n \<gamma>'
\<nexists>i. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>
[PROOF STEP]
have "\<gamma> (lnth (\<pi>\<^bsub>cid\<^esub>inf_llist t @\<^sub>l inf_llist t')) n \<longrightarrow> \<gamma>' (lnth (\<pi>\<^bsub>cid\<^esub>inf_llist t @\<^sub>l inf_llist t')) n"
[PROOF STATE]
proof (prove)
using this:
eval cid t t' n \<gamma> \<longrightarrow> eval cid t t' n \<gamma>'
\<nexists>i. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>

goal (1 subgoal):
 1. \<gamma> (lnth (\<pi>\<^bsub>cid\<^esub>inf_llist t @\<^sub>l inf_llist t')) n \<longrightarrow> \<gamma>' (lnth (\<pi>\<^bsub>cid\<^esub>inf_llist t @\<^sub>l inf_llist t')) n
[PROOF STEP]
using eval_def
[PROOF STATE]
proof (prove)
using this:
eval cid t t' n \<gamma> \<longrightarrow> eval cid t t' n \<gamma>'
\<nexists>i. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>
eval ?cid ?t ?t' ?n ?\<gamma> \<equiv> (\<exists>i\<ge>?n. \<parallel>?cid\<parallel>\<^bsub>?t i\<^esub>) \<and> ?\<gamma> (lnth (\<pi>\<^bsub>?cid\<^esub>inf_llist ?t @\<^sub>l inf_llist ?t')) (the_enat \<langle>?cid #\<^bsub>enat ?n\<^esub>inf_llist ?t\<rangle>) \<or> (\<exists>i. \<parallel>?cid\<parallel>\<^bsub>?t i\<^esub>) \<and> \<not> (\<exists>i'\<ge>?n. \<parallel>?cid\<parallel>\<^bsub>?t i'\<^esub>) \<and> ?\<gamma> (lnth (\<pi>\<^bsub>?cid\<^esub>inf_llist ?t @\<^sub>l inf_llist ?t')) (\<^bsub>?cid\<^esub>\<down>\<^bsub>?t\<^esub>?n) \<or> (\<nexists>i. \<parallel>?cid\<parallel>\<^bsub>?t i\<^esub>) \<and> ?\<gamma> (lnth (\<pi>\<^bsub>?cid\<^esub>inf_llist ?t @\<^sub>l inf_llist ?t')) ?n

goal (1 subgoal):
 1. \<gamma> (lnth (\<pi>\<^bsub>cid\<^esub>inf_llist t @\<^sub>l inf_llist t')) n \<longrightarrow> \<gamma>' (lnth (\<pi>\<^bsub>cid\<^esub>inf_llist t @\<^sub>l inf_llist t')) n
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<gamma> (lnth (\<pi>\<^bsub>cid\<^esub>inf_llist t @\<^sub>l inf_llist t')) n \<longrightarrow> \<gamma>' (lnth (\<pi>\<^bsub>cid\<^esub>inf_llist t @\<^sub>l inf_llist t')) n

goal (1 subgoal):
 1. \<nexists>i. \<parallel>cid\<parallel>\<^bsub>t i\<^esub> \<Longrightarrow> eval cid t t' n (\<gamma> \<longrightarrow>\<^sup>b \<gamma>')
[PROOF STEP]
with \<open>\<not>(\<exists>i. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>)\<close>
[PROOF STATE]
proof (chain)
picking this:
\<nexists>i. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>
\<gamma> (lnth (\<pi>\<^bsub>cid\<^esub>inf_llist t @\<^sub>l inf_llist t')) n \<longrightarrow> \<gamma>' (lnth (\<pi>\<^bsub>cid\<^esub>inf_llist t @\<^sub>l inf_llist t')) n
[PROOF STEP]
have "eval cid t t' n (\<lambda>t n. \<gamma> t n \<longrightarrow> \<gamma>' t n)"
[PROOF STATE]
proof (prove)
using this:
\<nexists>i. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>
\<gamma> (lnth (\<pi>\<^bsub>cid\<^esub>inf_llist t @\<^sub>l inf_llist t')) n \<longrightarrow> \<gamma>' (lnth (\<pi>\<^bsub>cid\<^esub>inf_llist t @\<^sub>l inf_llist t')) n

goal (1 subgoal):
 1. eval cid t t' n (\<lambda>t n. \<gamma> t n \<longrightarrow> \<gamma>' t n)
[PROOF STEP]
using validCI_not_act[where \<gamma>="\<lambda> t n. \<gamma> t n \<longrightarrow> \<gamma>' t n"]
[PROOF STATE]
proof (prove)
using this:
\<nexists>i. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>
\<gamma> (lnth (\<pi>\<^bsub>cid\<^esub>inf_llist t @\<^sub>l inf_llist t')) n \<longrightarrow> \<gamma>' (lnth (\<pi>\<^bsub>cid\<^esub>inf_llist t @\<^sub>l inf_llist t')) n
\<lbrakk>\<nexists>i. \<parallel>?cid\<parallel>\<^bsub>?t i\<^esub>; \<gamma> (lnth (\<pi>\<^bsub>?cid\<^esub>inf_llist ?t @\<^sub>l inf_llist ?t')) ?n \<longrightarrow> \<gamma>' (lnth (\<pi>\<^bsub>?cid\<^esub>inf_llist ?t @\<^sub>l inf_llist ?t')) ?n\<rbrakk> \<Longrightarrow> eval ?cid ?t ?t' ?n (\<lambda>t n. \<gamma> t n \<longrightarrow> \<gamma>' t n)

goal (1 subgoal):
 1. eval cid t t' n (\<lambda>t n. \<gamma> t n \<longrightarrow> \<gamma>' t n)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
eval cid t t' n (\<lambda>t n. \<gamma> t n \<longrightarrow> \<gamma>' t n)

goal (1 subgoal):
 1. \<nexists>i. \<parallel>cid\<parallel>\<^bsub>t i\<^esub> \<Longrightarrow> eval cid t t' n (\<gamma> \<longrightarrow>\<^sup>b \<gamma>')
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
eval cid t t' n (\<lambda>t n. \<gamma> t n \<longrightarrow> \<gamma>' t n)

goal (1 subgoal):
 1. eval cid t t' n (\<gamma> \<longrightarrow>\<^sup>b \<gamma>')
[PROOF STEP]
using imp_def
[PROOF STATE]
proof (prove)
using this:
eval cid t t' n (\<lambda>t n. \<gamma> t n \<longrightarrow> \<gamma>' t n)
?\<gamma> \<longrightarrow>\<^sup>b ?\<gamma>' \<equiv> \<lambda>t n. ?\<gamma> t n \<longrightarrow> ?\<gamma>' t n

goal (1 subgoal):
 1. eval cid t t' n (\<gamma> \<longrightarrow>\<^sup>b \<gamma>')
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
eval cid t t' n (\<gamma> \<longrightarrow>\<^sup>b \<gamma>')

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma impE[elim!]:
  assumes "eval cid t t' n (\<gamma> \<longrightarrow>\<^sup>b \<gamma>')"
  shows "eval cid t t' n \<gamma> \<longrightarrow> eval cid t t' n \<gamma>'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval cid t t' n \<gamma> \<longrightarrow> eval cid t t' n \<gamma>'
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> eval cid t t' n \<gamma> \<longrightarrow> eval cid t t' n \<gamma>'
 2. \<not> ?P \<Longrightarrow> eval cid t t' n \<gamma> \<longrightarrow> eval cid t t' n \<gamma>'
[PROOF STEP]
assume "(\<exists>i. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>)"
[PROOF STATE]
proof (state)
this:
\<exists>i. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>

goal (2 subgoals):
 1. ?P \<Longrightarrow> eval cid t t' n \<gamma> \<longrightarrow> eval cid t t' n \<gamma>'
 2. \<not> ?P \<Longrightarrow> eval cid t t' n \<gamma> \<longrightarrow> eval cid t t' n \<gamma>'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval cid t t' n \<gamma> \<longrightarrow> eval cid t t' n \<gamma>'
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> eval cid t t' n \<gamma> \<longrightarrow> eval cid t t' n \<gamma>'
 2. \<not> ?P \<Longrightarrow> eval cid t t' n \<gamma> \<longrightarrow> eval cid t t' n \<gamma>'
[PROOF STEP]
assume "\<exists>i\<ge>n. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>"
[PROOF STATE]
proof (state)
this:
\<exists>i\<ge>n. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>

goal (2 subgoals):
 1. ?P \<Longrightarrow> eval cid t t' n \<gamma> \<longrightarrow> eval cid t t' n \<gamma>'
 2. \<not> ?P \<Longrightarrow> eval cid t t' n \<gamma> \<longrightarrow> eval cid t t' n \<gamma>'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<exists>i\<ge>n. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>

goal (2 subgoals):
 1. ?P \<Longrightarrow> eval cid t t' n \<gamma> \<longrightarrow> eval cid t t' n \<gamma>'
 2. \<not> ?P \<Longrightarrow> eval cid t t' n \<gamma> \<longrightarrow> eval cid t t' n \<gamma>'
[PROOF STEP]
from \<open>eval cid t t' n (\<gamma> \<longrightarrow>\<^sup>b \<gamma>')\<close>
[PROOF STATE]
proof (chain)
picking this:
eval cid t t' n (\<gamma> \<longrightarrow>\<^sup>b \<gamma>')
[PROOF STEP]
have "eval cid t t' n (\<lambda>t n. \<gamma> t n \<longrightarrow> \<gamma>' t n)"
[PROOF STATE]
proof (prove)
using this:
eval cid t t' n (\<gamma> \<longrightarrow>\<^sup>b \<gamma>')

goal (1 subgoal):
 1. eval cid t t' n (\<lambda>t n. \<gamma> t n \<longrightarrow> \<gamma>' t n)
[PROOF STEP]
using imp_def
[PROOF STATE]
proof (prove)
using this:
eval cid t t' n (\<gamma> \<longrightarrow>\<^sup>b \<gamma>')
?\<gamma> \<longrightarrow>\<^sup>b ?\<gamma>' \<equiv> \<lambda>t n. ?\<gamma> t n \<longrightarrow> ?\<gamma>' t n

goal (1 subgoal):
 1. eval cid t t' n (\<lambda>t n. \<gamma> t n \<longrightarrow> \<gamma>' t n)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
eval cid t t' n (\<lambda>t n. \<gamma> t n \<longrightarrow> \<gamma>' t n)

goal (2 subgoals):
 1. ?P \<Longrightarrow> eval cid t t' n \<gamma> \<longrightarrow> eval cid t t' n \<gamma>'
 2. \<not> ?P \<Longrightarrow> eval cid t t' n \<gamma> \<longrightarrow> eval cid t t' n \<gamma>'
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<exists>i\<ge>n. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>
eval cid t t' n (\<lambda>t n. \<gamma> t n \<longrightarrow> \<gamma>' t n)
[PROOF STEP]
have "\<gamma> (lnth (\<pi>\<^bsub>cid\<^esub>inf_llist t @\<^sub>l inf_llist t')) (the_enat \<langle>cid #\<^bsub>enat n\<^esub>inf_llist t\<rangle>)
      \<longrightarrow> \<gamma>' (lnth (\<pi>\<^bsub>cid\<^esub>inf_llist t @\<^sub>l inf_llist t')) (the_enat \<langle>cid #\<^bsub>enat n\<^esub>inf_llist t\<rangle>)"
[PROOF STATE]
proof (prove)
using this:
\<exists>i\<ge>n. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>
eval cid t t' n (\<lambda>t n. \<gamma> t n \<longrightarrow> \<gamma>' t n)

goal (1 subgoal):
 1. \<gamma> (lnth (\<pi>\<^bsub>cid\<^esub>inf_llist t @\<^sub>l inf_llist t')) (the_enat \<langle>cid #\<^bsub>enat n\<^esub>inf_llist t\<rangle>) \<longrightarrow> \<gamma>' (lnth (\<pi>\<^bsub>cid\<^esub>inf_llist t @\<^sub>l inf_llist t')) (the_enat \<langle>cid #\<^bsub>enat n\<^esub>inf_llist t\<rangle>)
[PROOF STEP]
using validCE_act[where \<gamma>="\<lambda> t n. \<gamma> t n \<longrightarrow> \<gamma>' t n"]
[PROOF STATE]
proof (prove)
using this:
\<exists>i\<ge>n. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>
eval cid t t' n (\<lambda>t n. \<gamma> t n \<longrightarrow> \<gamma>' t n)
\<lbrakk>\<exists>i\<ge>?n. \<parallel>?cid\<parallel>\<^bsub>?t i\<^esub>; eval ?cid ?t ?t' ?n (\<lambda>t n. \<gamma> t n \<longrightarrow> \<gamma>' t n)\<rbrakk> \<Longrightarrow> \<gamma> (lnth (\<pi>\<^bsub>?cid\<^esub>inf_llist ?t @\<^sub>l inf_llist ?t')) (the_enat \<langle>?cid #\<^bsub>enat ?n\<^esub>inf_llist ?t\<rangle>) \<longrightarrow> \<gamma>' (lnth (\<pi>\<^bsub>?cid\<^esub>inf_llist ?t @\<^sub>l inf_llist ?t')) (the_enat \<langle>?cid #\<^bsub>enat ?n\<^esub>inf_llist ?t\<rangle>)

goal (1 subgoal):
 1. \<gamma> (lnth (\<pi>\<^bsub>cid\<^esub>inf_llist t @\<^sub>l inf_llist t')) (the_enat \<langle>cid #\<^bsub>enat n\<^esub>inf_llist t\<rangle>) \<longrightarrow> \<gamma>' (lnth (\<pi>\<^bsub>cid\<^esub>inf_llist t @\<^sub>l inf_llist t')) (the_enat \<langle>cid #\<^bsub>enat n\<^esub>inf_llist t\<rangle>)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<gamma> (lnth (\<pi>\<^bsub>cid\<^esub>inf_llist t @\<^sub>l inf_llist t')) (the_enat \<langle>cid #\<^bsub>enat n\<^esub>inf_llist t\<rangle>) \<longrightarrow> \<gamma>' (lnth (\<pi>\<^bsub>cid\<^esub>inf_llist t @\<^sub>l inf_llist t')) (the_enat \<langle>cid #\<^bsub>enat n\<^esub>inf_llist t\<rangle>)

goal (2 subgoals):
 1. ?P \<Longrightarrow> eval cid t t' n \<gamma> \<longrightarrow> eval cid t t' n \<gamma>'
 2. \<not> ?P \<Longrightarrow> eval cid t t' n \<gamma> \<longrightarrow> eval cid t t' n \<gamma>'
[PROOF STEP]
with \<open>\<exists>i\<ge>n. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>\<close>
[PROOF STATE]
proof (chain)
picking this:
\<exists>i\<ge>n. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>
\<gamma> (lnth (\<pi>\<^bsub>cid\<^esub>inf_llist t @\<^sub>l inf_llist t')) (the_enat \<langle>cid #\<^bsub>enat n\<^esub>inf_llist t\<rangle>) \<longrightarrow> \<gamma>' (lnth (\<pi>\<^bsub>cid\<^esub>inf_llist t @\<^sub>l inf_llist t')) (the_enat \<langle>cid #\<^bsub>enat n\<^esub>inf_llist t\<rangle>)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<exists>i\<ge>n. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>
\<gamma> (lnth (\<pi>\<^bsub>cid\<^esub>inf_llist t @\<^sub>l inf_llist t')) (the_enat \<langle>cid #\<^bsub>enat n\<^esub>inf_llist t\<rangle>) \<longrightarrow> \<gamma>' (lnth (\<pi>\<^bsub>cid\<^esub>inf_llist t @\<^sub>l inf_llist t')) (the_enat \<langle>cid #\<^bsub>enat n\<^esub>inf_llist t\<rangle>)

goal (1 subgoal):
 1. eval cid t t' n \<gamma> \<longrightarrow> eval cid t t' n \<gamma>'
[PROOF STEP]
using eval_def
[PROOF STATE]
proof (prove)
using this:
\<exists>i\<ge>n. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>
\<gamma> (lnth (\<pi>\<^bsub>cid\<^esub>inf_llist t @\<^sub>l inf_llist t')) (the_enat \<langle>cid #\<^bsub>enat n\<^esub>inf_llist t\<rangle>) \<longrightarrow> \<gamma>' (lnth (\<pi>\<^bsub>cid\<^esub>inf_llist t @\<^sub>l inf_llist t')) (the_enat \<langle>cid #\<^bsub>enat n\<^esub>inf_llist t\<rangle>)
eval ?cid ?t ?t' ?n ?\<gamma> \<equiv> (\<exists>i\<ge>?n. \<parallel>?cid\<parallel>\<^bsub>?t i\<^esub>) \<and> ?\<gamma> (lnth (\<pi>\<^bsub>?cid\<^esub>inf_llist ?t @\<^sub>l inf_llist ?t')) (the_enat \<langle>?cid #\<^bsub>enat ?n\<^esub>inf_llist ?t\<rangle>) \<or> (\<exists>i. \<parallel>?cid\<parallel>\<^bsub>?t i\<^esub>) \<and> \<not> (\<exists>i'\<ge>?n. \<parallel>?cid\<parallel>\<^bsub>?t i'\<^esub>) \<and> ?\<gamma> (lnth (\<pi>\<^bsub>?cid\<^esub>inf_llist ?t @\<^sub>l inf_llist ?t')) (\<^bsub>?cid\<^esub>\<down>\<^bsub>?t\<^esub>?n) \<or> (\<nexists>i. \<parallel>?cid\<parallel>\<^bsub>?t i\<^esub>) \<and> ?\<gamma> (lnth (\<pi>\<^bsub>?cid\<^esub>inf_llist ?t @\<^sub>l inf_llist ?t')) ?n

goal (1 subgoal):
 1. eval cid t t' n \<gamma> \<longrightarrow> eval cid t t' n \<gamma>'
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
eval cid t t' n \<gamma> \<longrightarrow> eval cid t t' n \<gamma>'

goal (1 subgoal):
 1. \<not> (\<exists>i\<ge>n. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>) \<Longrightarrow> eval cid t t' n \<gamma> \<longrightarrow> eval cid t t' n \<gamma>'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> (\<exists>i\<ge>n. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>) \<Longrightarrow> eval cid t t' n \<gamma> \<longrightarrow> eval cid t t' n \<gamma>'
[PROOF STEP]
assume "\<not> (\<exists>i\<ge>n. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>)"
[PROOF STATE]
proof (state)
this:
\<not> (\<exists>i\<ge>n. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>)

goal (1 subgoal):
 1. \<not> (\<exists>i\<ge>n. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>) \<Longrightarrow> eval cid t t' n \<gamma> \<longrightarrow> eval cid t t' n \<gamma>'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<not> (\<exists>i\<ge>n. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>)

goal (1 subgoal):
 1. \<not> (\<exists>i\<ge>n. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>) \<Longrightarrow> eval cid t t' n \<gamma> \<longrightarrow> eval cid t t' n \<gamma>'
[PROOF STEP]
from \<open>eval cid t t' n (\<gamma> \<longrightarrow>\<^sup>b \<gamma>')\<close>
[PROOF STATE]
proof (chain)
picking this:
eval cid t t' n (\<gamma> \<longrightarrow>\<^sup>b \<gamma>')
[PROOF STEP]
have "eval cid t t' n (\<lambda>t n. \<gamma> t n \<longrightarrow> \<gamma>' t n)"
[PROOF STATE]
proof (prove)
using this:
eval cid t t' n (\<gamma> \<longrightarrow>\<^sup>b \<gamma>')

goal (1 subgoal):
 1. eval cid t t' n (\<lambda>t n. \<gamma> t n \<longrightarrow> \<gamma>' t n)
[PROOF STEP]
using imp_def
[PROOF STATE]
proof (prove)
using this:
eval cid t t' n (\<gamma> \<longrightarrow>\<^sup>b \<gamma>')
?\<gamma> \<longrightarrow>\<^sup>b ?\<gamma>' \<equiv> \<lambda>t n. ?\<gamma> t n \<longrightarrow> ?\<gamma>' t n

goal (1 subgoal):
 1. eval cid t t' n (\<lambda>t n. \<gamma> t n \<longrightarrow> \<gamma>' t n)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
eval cid t t' n (\<lambda>t n. \<gamma> t n \<longrightarrow> \<gamma>' t n)

goal (1 subgoal):
 1. \<not> (\<exists>i\<ge>n. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>) \<Longrightarrow> eval cid t t' n \<gamma> \<longrightarrow> eval cid t t' n \<gamma>'
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<not> (\<exists>i\<ge>n. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>)
eval cid t t' n (\<lambda>t n. \<gamma> t n \<longrightarrow> \<gamma>' t n)
[PROOF STEP]
have "\<gamma> (lnth (\<pi>\<^bsub>cid\<^esub>inf_llist t @\<^sub>l inf_llist t')) (\<^bsub>cid\<^esub>\<down>\<^bsub>t\<^esub>n)
      \<longrightarrow> \<gamma>' (lnth (\<pi>\<^bsub>cid\<^esub>inf_llist t @\<^sub>l inf_llist t')) (\<^bsub>cid\<^esub>\<down>\<^bsub>t\<^esub>n)"
[PROOF STATE]
proof (prove)
using this:
\<not> (\<exists>i\<ge>n. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>)
eval cid t t' n (\<lambda>t n. \<gamma> t n \<longrightarrow> \<gamma>' t n)

goal (1 subgoal):
 1. \<gamma> (lnth (\<pi>\<^bsub>cid\<^esub>inf_llist t @\<^sub>l inf_llist t')) (\<^bsub>cid\<^esub>\<down>\<^bsub>t\<^esub>n) \<longrightarrow> \<gamma>' (lnth (\<pi>\<^bsub>cid\<^esub>inf_llist t @\<^sub>l inf_llist t')) (\<^bsub>cid\<^esub>\<down>\<^bsub>t\<^esub>n)
[PROOF STEP]
using validCE_cont[where \<gamma>="\<lambda> t n. \<gamma> t n \<longrightarrow> \<gamma>' t n"] \<open>\<exists>i. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>\<close>
[PROOF STATE]
proof (prove)
using this:
\<not> (\<exists>i\<ge>n. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>)
eval cid t t' n (\<lambda>t n. \<gamma> t n \<longrightarrow> \<gamma>' t n)
\<lbrakk>\<exists>i. \<parallel>?cid\<parallel>\<^bsub>?t i\<^esub>; \<not> (\<exists>i'\<ge>?n. \<parallel>?cid\<parallel>\<^bsub>?t i'\<^esub>); eval ?cid ?t ?t' ?n (\<lambda>t n. \<gamma> t n \<longrightarrow> \<gamma>' t n)\<rbrakk> \<Longrightarrow> \<gamma> (lnth (\<pi>\<^bsub>?cid\<^esub>inf_llist ?t @\<^sub>l inf_llist ?t')) (\<^bsub>?cid\<^esub>\<down>\<^bsub>?t\<^esub>?n) \<longrightarrow> \<gamma>' (lnth (\<pi>\<^bsub>?cid\<^esub>inf_llist ?t @\<^sub>l inf_llist ?t')) (\<^bsub>?cid\<^esub>\<down>\<^bsub>?t\<^esub>?n)
\<exists>i. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>

goal (1 subgoal):
 1. \<gamma> (lnth (\<pi>\<^bsub>cid\<^esub>inf_llist t @\<^sub>l inf_llist t')) (\<^bsub>cid\<^esub>\<down>\<^bsub>t\<^esub>n) \<longrightarrow> \<gamma>' (lnth (\<pi>\<^bsub>cid\<^esub>inf_llist t @\<^sub>l inf_llist t')) (\<^bsub>cid\<^esub>\<down>\<^bsub>t\<^esub>n)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<gamma> (lnth (\<pi>\<^bsub>cid\<^esub>inf_llist t @\<^sub>l inf_llist t')) (\<^bsub>cid\<^esub>\<down>\<^bsub>t\<^esub>n) \<longrightarrow> \<gamma>' (lnth (\<pi>\<^bsub>cid\<^esub>inf_llist t @\<^sub>l inf_llist t')) (\<^bsub>cid\<^esub>\<down>\<^bsub>t\<^esub>n)

goal (1 subgoal):
 1. \<not> (\<exists>i\<ge>n. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>) \<Longrightarrow> eval cid t t' n \<gamma> \<longrightarrow> eval cid t t' n \<gamma>'
[PROOF STEP]
with \<open>\<not> (\<exists>i\<ge>n. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>)\<close> \<open>\<exists>i. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>\<close>
[PROOF STATE]
proof (chain)
picking this:
\<not> (\<exists>i\<ge>n. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>)
\<exists>i. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>
\<gamma> (lnth (\<pi>\<^bsub>cid\<^esub>inf_llist t @\<^sub>l inf_llist t')) (\<^bsub>cid\<^esub>\<down>\<^bsub>t\<^esub>n) \<longrightarrow> \<gamma>' (lnth (\<pi>\<^bsub>cid\<^esub>inf_llist t @\<^sub>l inf_llist t')) (\<^bsub>cid\<^esub>\<down>\<^bsub>t\<^esub>n)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<not> (\<exists>i\<ge>n. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>)
\<exists>i. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>
\<gamma> (lnth (\<pi>\<^bsub>cid\<^esub>inf_llist t @\<^sub>l inf_llist t')) (\<^bsub>cid\<^esub>\<down>\<^bsub>t\<^esub>n) \<longrightarrow> \<gamma>' (lnth (\<pi>\<^bsub>cid\<^esub>inf_llist t @\<^sub>l inf_llist t')) (\<^bsub>cid\<^esub>\<down>\<^bsub>t\<^esub>n)

goal (1 subgoal):
 1. eval cid t t' n \<gamma> \<longrightarrow> eval cid t t' n \<gamma>'
[PROOF STEP]
using eval_def
[PROOF STATE]
proof (prove)
using this:
\<not> (\<exists>i\<ge>n. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>)
\<exists>i. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>
\<gamma> (lnth (\<pi>\<^bsub>cid\<^esub>inf_llist t @\<^sub>l inf_llist t')) (\<^bsub>cid\<^esub>\<down>\<^bsub>t\<^esub>n) \<longrightarrow> \<gamma>' (lnth (\<pi>\<^bsub>cid\<^esub>inf_llist t @\<^sub>l inf_llist t')) (\<^bsub>cid\<^esub>\<down>\<^bsub>t\<^esub>n)
eval ?cid ?t ?t' ?n ?\<gamma> \<equiv> (\<exists>i\<ge>?n. \<parallel>?cid\<parallel>\<^bsub>?t i\<^esub>) \<and> ?\<gamma> (lnth (\<pi>\<^bsub>?cid\<^esub>inf_llist ?t @\<^sub>l inf_llist ?t')) (the_enat \<langle>?cid #\<^bsub>enat ?n\<^esub>inf_llist ?t\<rangle>) \<or> (\<exists>i. \<parallel>?cid\<parallel>\<^bsub>?t i\<^esub>) \<and> \<not> (\<exists>i'\<ge>?n. \<parallel>?cid\<parallel>\<^bsub>?t i'\<^esub>) \<and> ?\<gamma> (lnth (\<pi>\<^bsub>?cid\<^esub>inf_llist ?t @\<^sub>l inf_llist ?t')) (\<^bsub>?cid\<^esub>\<down>\<^bsub>?t\<^esub>?n) \<or> (\<nexists>i. \<parallel>?cid\<parallel>\<^bsub>?t i\<^esub>) \<and> ?\<gamma> (lnth (\<pi>\<^bsub>?cid\<^esub>inf_llist ?t @\<^sub>l inf_llist ?t')) ?n

goal (1 subgoal):
 1. eval cid t t' n \<gamma> \<longrightarrow> eval cid t t' n \<gamma>'
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
eval cid t t' n \<gamma> \<longrightarrow> eval cid t t' n \<gamma>'

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
eval cid t t' n \<gamma> \<longrightarrow> eval cid t t' n \<gamma>'

goal (1 subgoal):
 1. \<nexists>i. \<parallel>cid\<parallel>\<^bsub>t i\<^esub> \<Longrightarrow> eval cid t t' n \<gamma> \<longrightarrow> eval cid t t' n \<gamma>'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<nexists>i. \<parallel>cid\<parallel>\<^bsub>t i\<^esub> \<Longrightarrow> eval cid t t' n \<gamma> \<longrightarrow> eval cid t t' n \<gamma>'
[PROOF STEP]
assume "\<not>(\<exists>i. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>)"
[PROOF STATE]
proof (state)
this:
\<nexists>i. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>

goal (1 subgoal):
 1. \<nexists>i. \<parallel>cid\<parallel>\<^bsub>t i\<^esub> \<Longrightarrow> eval cid t t' n \<gamma> \<longrightarrow> eval cid t t' n \<gamma>'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<nexists>i. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>

goal (1 subgoal):
 1. \<nexists>i. \<parallel>cid\<parallel>\<^bsub>t i\<^esub> \<Longrightarrow> eval cid t t' n \<gamma> \<longrightarrow> eval cid t t' n \<gamma>'
[PROOF STEP]
from \<open>eval cid t t' n (\<gamma> \<longrightarrow>\<^sup>b \<gamma>')\<close>
[PROOF STATE]
proof (chain)
picking this:
eval cid t t' n (\<gamma> \<longrightarrow>\<^sup>b \<gamma>')
[PROOF STEP]
have "eval cid t t' n (\<lambda>t n. \<gamma> t n \<longrightarrow> \<gamma>' t n)"
[PROOF STATE]
proof (prove)
using this:
eval cid t t' n (\<gamma> \<longrightarrow>\<^sup>b \<gamma>')

goal (1 subgoal):
 1. eval cid t t' n (\<lambda>t n. \<gamma> t n \<longrightarrow> \<gamma>' t n)
[PROOF STEP]
using imp_def
[PROOF STATE]
proof (prove)
using this:
eval cid t t' n (\<gamma> \<longrightarrow>\<^sup>b \<gamma>')
?\<gamma> \<longrightarrow>\<^sup>b ?\<gamma>' \<equiv> \<lambda>t n. ?\<gamma> t n \<longrightarrow> ?\<gamma>' t n

goal (1 subgoal):
 1. eval cid t t' n (\<lambda>t n. \<gamma> t n \<longrightarrow> \<gamma>' t n)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
eval cid t t' n (\<lambda>t n. \<gamma> t n \<longrightarrow> \<gamma>' t n)

goal (1 subgoal):
 1. \<nexists>i. \<parallel>cid\<parallel>\<^bsub>t i\<^esub> \<Longrightarrow> eval cid t t' n \<gamma> \<longrightarrow> eval cid t t' n \<gamma>'
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<nexists>i. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>
eval cid t t' n (\<lambda>t n. \<gamma> t n \<longrightarrow> \<gamma>' t n)
[PROOF STEP]
have "\<gamma> (lnth (\<pi>\<^bsub>cid\<^esub>inf_llist t @\<^sub>l inf_llist t')) n
    \<longrightarrow> \<gamma>' (lnth (\<pi>\<^bsub>cid\<^esub>inf_llist t @\<^sub>l inf_llist t')) n"
[PROOF STATE]
proof (prove)
using this:
\<nexists>i. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>
eval cid t t' n (\<lambda>t n. \<gamma> t n \<longrightarrow> \<gamma>' t n)

goal (1 subgoal):
 1. \<gamma> (lnth (\<pi>\<^bsub>cid\<^esub>inf_llist t @\<^sub>l inf_llist t')) n \<longrightarrow> \<gamma>' (lnth (\<pi>\<^bsub>cid\<^esub>inf_llist t @\<^sub>l inf_llist t')) n
[PROOF STEP]
using validCE_not_act[where \<gamma>="\<lambda> t n. \<gamma> t n \<longrightarrow> \<gamma>' t n"]
[PROOF STATE]
proof (prove)
using this:
\<nexists>i. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>
eval cid t t' n (\<lambda>t n. \<gamma> t n \<longrightarrow> \<gamma>' t n)
\<lbrakk>\<nexists>i. \<parallel>?cid\<parallel>\<^bsub>?t i\<^esub>; eval ?cid ?t ?t' ?n (\<lambda>t n. \<gamma> t n \<longrightarrow> \<gamma>' t n)\<rbrakk> \<Longrightarrow> \<gamma> (lnth (\<pi>\<^bsub>?cid\<^esub>inf_llist ?t @\<^sub>l inf_llist ?t')) ?n \<longrightarrow> \<gamma>' (lnth (\<pi>\<^bsub>?cid\<^esub>inf_llist ?t @\<^sub>l inf_llist ?t')) ?n

goal (1 subgoal):
 1. \<gamma> (lnth (\<pi>\<^bsub>cid\<^esub>inf_llist t @\<^sub>l inf_llist t')) n \<longrightarrow> \<gamma>' (lnth (\<pi>\<^bsub>cid\<^esub>inf_llist t @\<^sub>l inf_llist t')) n
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<gamma> (lnth (\<pi>\<^bsub>cid\<^esub>inf_llist t @\<^sub>l inf_llist t')) n \<longrightarrow> \<gamma>' (lnth (\<pi>\<^bsub>cid\<^esub>inf_llist t @\<^sub>l inf_llist t')) n

goal (1 subgoal):
 1. \<nexists>i. \<parallel>cid\<parallel>\<^bsub>t i\<^esub> \<Longrightarrow> eval cid t t' n \<gamma> \<longrightarrow> eval cid t t' n \<gamma>'
[PROOF STEP]
with \<open>\<not>(\<exists>i. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>)\<close>
[PROOF STATE]
proof (chain)
picking this:
\<nexists>i. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>
\<gamma> (lnth (\<pi>\<^bsub>cid\<^esub>inf_llist t @\<^sub>l inf_llist t')) n \<longrightarrow> \<gamma>' (lnth (\<pi>\<^bsub>cid\<^esub>inf_llist t @\<^sub>l inf_llist t')) n
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<nexists>i. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>
\<gamma> (lnth (\<pi>\<^bsub>cid\<^esub>inf_llist t @\<^sub>l inf_llist t')) n \<longrightarrow> \<gamma>' (lnth (\<pi>\<^bsub>cid\<^esub>inf_llist t @\<^sub>l inf_llist t')) n

goal (1 subgoal):
 1. eval cid t t' n \<gamma> \<longrightarrow> eval cid t t' n \<gamma>'
[PROOF STEP]
using eval_def
[PROOF STATE]
proof (prove)
using this:
\<nexists>i. \<parallel>cid\<parallel>\<^bsub>t i\<^esub>
\<gamma> (lnth (\<pi>\<^bsub>cid\<^esub>inf_llist t @\<^sub>l inf_llist t')) n \<longrightarrow> \<gamma>' (lnth (\<pi>\<^bsub>cid\<^esub>inf_llist t @\<^sub>l inf_llist t')) n
eval ?cid ?t ?t' ?n ?\<gamma> \<equiv> (\<exists>i\<ge>?n. \<parallel>?cid\<parallel>\<^bsub>?t i\<^esub>) \<and> ?\<gamma> (lnth (\<pi>\<^bsub>?cid\<^esub>inf_llist ?t @\<^sub>l inf_llist ?t')) (the_enat \<langle>?cid #\<^bsub>enat ?n\<^esub>inf_llist ?t\<rangle>) \<or> (\<exists>i. \<parallel>?cid\<parallel>\<^bsub>?t i\<^esub>) \<and> \<not> (\<exists>i'\<ge>?n. \<parallel>?cid\<parallel>\<^bsub>?t i'\<^esub>) \<and> ?\<gamma> (lnth (\<pi>\<^bsub>?cid\<^esub>inf_llist ?t @\<^sub>l inf_llist ?t')) (\<^bsub>?cid\<^esub>\<down>\<^bsub>?t\<^esub>?n) \<or> (\<nexists>i. \<parallel>?cid\<parallel>\<^bsub>?t i\<^esub>) \<and> ?\<gamma> (lnth (\<pi>\<^bsub>?cid\<^esub>inf_llist ?t @\<^sub>l inf_llist ?t')) ?n

goal (1 subgoal):
 1. eval cid t t' n \<gamma> \<longrightarrow> eval cid t t' n \<gamma>'
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
eval cid t t' n \<gamma> \<longrightarrow> eval cid t t' n \<gamma>'

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma disjI[intro!]:
  assumes "eval cid t t' n \<gamma> \<or> eval cid t t' n \<gamma>'"
  shows "eval cid t t' n (\<gamma> \<or>\<^sup>b \<gamma>')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval cid t t' n (\<gamma> \<or>\<^sup>b \<gamma>')
[PROOF STEP]
using assms disj_def eval_def
[PROOF STATE]
proof (prove)
using this:
eval cid t t' n \<gamma> \<or> eval cid t t' n \<gamma>'
?\<gamma> \<or>\<^sup>b ?\<gamma>' \<equiv> \<lambda>t n. ?\<gamma> t n \<or> ?\<gamma>' t n
eval ?cid ?t ?t' ?n ?\<gamma> \<equiv> (\<exists>i\<ge>?n. \<parallel>?cid\<parallel>\<^bsub>?t i\<^esub>) \<and> ?\<gamma> (lnth (\<pi>\<^bsub>?cid\<^esub>inf_llist ?t @\<^sub>l inf_llist ?t')) (the_enat \<langle>?cid #\<^bsub>enat ?n\<^esub>inf_llist ?t\<rangle>) \<or> (\<exists>i. \<parallel>?cid\<parallel>\<^bsub>?t i\<^esub>) \<and> \<not> (\<exists>i'\<ge>?n. \<parallel>?cid\<parallel>\<^bsub>?t i'\<^esub>) \<and> ?\<gamma> (lnth (\<pi>\<^bsub>?cid\<^esub>inf_llist ?t @\<^sub>l inf_llist ?t')) (\<^bsub>?cid\<^esub>\<down>\<^bsub>?t\<^esub>?n) \<or> (\<nexists>i. \<parallel>?cid\<parallel>\<^bsub>?t i\<^esub>) \<and> ?\<gamma> (lnth (\<pi>\<^bsub>?cid\<^esub>inf_llist ?t @\<^sub>l inf_llist ?t')) ?n

goal (1 subgoal):
 1. eval cid t t' n (\<gamma> \<or>\<^sup>b \<gamma>')
[PROOF STEP]
by auto