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

  assumes PSimQ: "P \<leadsto>[Rel] Q"
  and     QSimR: "Q \<leadsto>[Rel'] R"
  and     Eqvt': "eqvt Rel''"
  and     Trans: "Rel O Rel' \<subseteq> Rel''"

  shows "P \<leadsto>[Rel''] R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<leadsto>[Rel''] R
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. P \<leadsto>[Rel''] R
[PROOF STEP]
from Eqvt'
[PROOF STATE]
proof (chain)
picking this:
eqvt Rel''
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
eqvt Rel''

goal (1 subgoal):
 1. P \<leadsto>[Rel''] R
[PROOF STEP]
proof(induct rule: simCasesCont[where C=Q])
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>a y Q'. \<lbrakk>R \<longmapsto> a<\<nu>y> \<prec> Q'; y \<sharp> P; y \<sharp> R; y \<sharp> Q\<rbrakk> \<Longrightarrow> \<exists>P'. P \<longmapsto> a<\<nu>y> \<prec> P' \<and> (P', Q') \<in> Rel''
 2. \<And>\<alpha> Q'. R \<longmapsto> \<alpha> \<prec> Q' \<Longrightarrow> \<exists>P'. P \<longmapsto> \<alpha> \<prec> P' \<and> (P', Q') \<in> Rel''
[PROOF STEP]
case(Bound a y R')
[PROOF STATE]
proof (state)
this:
R \<longmapsto> a<\<nu>y> \<prec> R'
y \<sharp> P
y \<sharp> R
y \<sharp> Q

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

goal (2 subgoals):
 1. \<And>a y Q'. \<lbrakk>R \<longmapsto> a<\<nu>y> \<prec> Q'; y \<sharp> P; y \<sharp> R; y \<sharp> Q\<rbrakk> \<Longrightarrow> \<exists>P'. P \<longmapsto> a<\<nu>y> \<prec> P' \<and> (P', Q') \<in> Rel''
 2. \<And>\<alpha> Q'. R \<longmapsto> \<alpha> \<prec> Q' \<Longrightarrow> \<exists>P'. P \<longmapsto> \<alpha> \<prec> P' \<and> (P', Q') \<in> Rel''
[PROOF STEP]
from QSimR RTrans \<open>y \<sharp> Q\<close>
[PROOF STATE]
proof (chain)
picking this:
Q \<leadsto>[Rel'] R
R \<longmapsto> a<\<nu>y> \<prec> R'
y \<sharp> Q
[PROOF STEP]
have "\<exists>Q'. Q \<longmapsto> a<\<nu>y> \<prec> Q' \<and> (Q', R') \<in> Rel'"
[PROOF STATE]
proof (prove)
using this:
Q \<leadsto>[Rel'] R
R \<longmapsto> a<\<nu>y> \<prec> R'
y \<sharp> Q

goal (1 subgoal):
 1. \<exists>Q'. Q \<longmapsto> a<\<nu>y> \<prec> Q' \<and> (Q', R') \<in> Rel'
[PROOF STEP]
by(rule elim)
[PROOF STATE]
proof (state)
this:
\<exists>Q'. Q \<longmapsto> a<\<nu>y> \<prec> Q' \<and> (Q', R') \<in> Rel'

goal (2 subgoals):
 1. \<And>a y Q'. \<lbrakk>R \<longmapsto> a<\<nu>y> \<prec> Q'; y \<sharp> P; y \<sharp> R; y \<sharp> Q\<rbrakk> \<Longrightarrow> \<exists>P'. P \<longmapsto> a<\<nu>y> \<prec> P' \<and> (P', Q') \<in> Rel''
 2. \<And>\<alpha> Q'. R \<longmapsto> \<alpha> \<prec> Q' \<Longrightarrow> \<exists>P'. P \<longmapsto> \<alpha> \<prec> P' \<and> (P', Q') \<in> Rel''
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>Q'. Q \<longmapsto> a<\<nu>y> \<prec> Q' \<and> (Q', R') \<in> Rel'
[PROOF STEP]
obtain Q' where QTrans: "Q \<longmapsto> a<\<nu>y> \<prec> Q'" and Q'Rel'R': "(Q', R') \<in> Rel'"
[PROOF STATE]
proof (prove)
using this:
\<exists>Q'. Q \<longmapsto> a<\<nu>y> \<prec> Q' \<and> (Q', R') \<in> Rel'

goal (1 subgoal):
 1. (\<And>Q'. \<lbrakk>Q \<longmapsto> a<\<nu>y> \<prec> Q'; (Q', R') \<in> Rel'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Q \<longmapsto> a<\<nu>y> \<prec> Q'
(Q', R') \<in> Rel'

goal (2 subgoals):
 1. \<And>a y Q'. \<lbrakk>R \<longmapsto> a<\<nu>y> \<prec> Q'; y \<sharp> P; y \<sharp> R; y \<sharp> Q\<rbrakk> \<Longrightarrow> \<exists>P'. P \<longmapsto> a<\<nu>y> \<prec> P' \<and> (P', Q') \<in> Rel''
 2. \<And>\<alpha> Q'. R \<longmapsto> \<alpha> \<prec> Q' \<Longrightarrow> \<exists>P'. P \<longmapsto> \<alpha> \<prec> P' \<and> (P', Q') \<in> Rel''
[PROOF STEP]
from PSimQ QTrans \<open>y \<sharp> P\<close>
[PROOF STATE]
proof (chain)
picking this:
P \<leadsto>[Rel] Q
Q \<longmapsto> a<\<nu>y> \<prec> Q'
y \<sharp> P
[PROOF STEP]
have "\<exists>P'. P \<longmapsto> a<\<nu>y> \<prec> P' \<and> (P', Q') \<in> Rel"
[PROOF STATE]
proof (prove)
using this:
P \<leadsto>[Rel] Q
Q \<longmapsto> a<\<nu>y> \<prec> Q'
y \<sharp> P

goal (1 subgoal):
 1. \<exists>P'. P \<longmapsto> a<\<nu>y> \<prec> P' \<and> (P', Q') \<in> Rel
[PROOF STEP]
by(rule elim)
[PROOF STATE]
proof (state)
this:
\<exists>P'. P \<longmapsto> a<\<nu>y> \<prec> P' \<and> (P', Q') \<in> Rel

goal (2 subgoals):
 1. \<And>a y Q'. \<lbrakk>R \<longmapsto> a<\<nu>y> \<prec> Q'; y \<sharp> P; y \<sharp> R; y \<sharp> Q\<rbrakk> \<Longrightarrow> \<exists>P'. P \<longmapsto> a<\<nu>y> \<prec> P' \<and> (P', Q') \<in> Rel''
 2. \<And>\<alpha> Q'. R \<longmapsto> \<alpha> \<prec> Q' \<Longrightarrow> \<exists>P'. P \<longmapsto> \<alpha> \<prec> P' \<and> (P', Q') \<in> Rel''
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>P'. P \<longmapsto> a<\<nu>y> \<prec> P' \<and> (P', Q') \<in> Rel
[PROOF STEP]
obtain P' where PTrans: "P \<longmapsto> a<\<nu>y> \<prec> P'" and P'RelQ': "(P', Q') \<in> Rel"
[PROOF STATE]
proof (prove)
using this:
\<exists>P'. P \<longmapsto> a<\<nu>y> \<prec> P' \<and> (P', Q') \<in> Rel

goal (1 subgoal):
 1. (\<And>P'. \<lbrakk>P \<longmapsto> a<\<nu>y> \<prec> P'; (P', Q') \<in> Rel\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
P \<longmapsto> a<\<nu>y> \<prec> P'
(P', Q') \<in> Rel

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

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

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

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

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

goal (1 subgoal):
 1. \<And>\<alpha> Q'. R \<longmapsto> \<alpha> \<prec> Q' \<Longrightarrow> \<exists>P'. P \<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 \<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 \<longmapsto> \<alpha> \<prec> P' \<and> (P', Q') \<in> Rel''
[PROOF STEP]
have RTrans: "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 \<longmapsto> \<alpha> \<prec> P' \<and> (P', Q') \<in> Rel''
[PROOF STEP]
with QSimR
[PROOF STATE]
proof (chain)
picking this:
Q \<leadsto>[Rel'] R
R \<longmapsto> \<alpha> \<prec> R'
[PROOF STEP]
have "\<exists>Q'. Q \<longmapsto> \<alpha> \<prec> Q' \<and> (Q', R') \<in> Rel'"
[PROOF STATE]
proof (prove)
using this:
Q \<leadsto>[Rel'] R
R \<longmapsto> \<alpha> \<prec> R'

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

goal (1 subgoal):
 1. \<And>\<alpha> Q'. R \<longmapsto> \<alpha> \<prec> Q' \<Longrightarrow> \<exists>P'. P \<longmapsto> \<alpha> \<prec> P' \<and> (P', Q') \<in> Rel''
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>Q'. Q \<longmapsto> \<alpha> \<prec> Q' \<and> (Q', R') \<in> Rel'
[PROOF STEP]
obtain Q' where QTrans: "Q \<longmapsto> \<alpha> \<prec> Q'" and Q'RelR': "(Q', R') \<in> Rel'"
[PROOF STATE]
proof (prove)
using this:
\<exists>Q'. Q \<longmapsto> \<alpha> \<prec> Q' \<and> (Q', R') \<in> Rel'

goal (1 subgoal):
 1. (\<And>Q'. \<lbrakk>Q \<longmapsto> \<alpha> \<prec> Q'; (Q', R') \<in> Rel'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Q \<longmapsto> \<alpha> \<prec> Q'
(Q', R') \<in> Rel'

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

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

goal (1 subgoal):
 1. \<And>\<alpha> Q'. R \<longmapsto> \<alpha> \<prec> Q' \<Longrightarrow> \<exists>P'. P \<longmapsto> \<alpha> \<prec> P' \<and> (P', Q') \<in> Rel''
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>P'. P \<longmapsto> \<alpha> \<prec> P' \<and> (P', Q') \<in> Rel
[PROOF STEP]
obtain P' where PTrans: "P \<longmapsto> \<alpha> \<prec> P'" and P'RelQ': "(P', Q') \<in> Rel"
[PROOF STATE]
proof (prove)
using this:
\<exists>P'. P \<longmapsto> \<alpha> \<prec> P' \<and> (P', Q') \<in> Rel

goal (1 subgoal):
 1. (\<And>P'. \<lbrakk>P \<longmapsto> \<alpha> \<prec> P'; (P', Q') \<in> Rel\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
P \<longmapsto> \<alpha> \<prec> P'
(P', Q') \<in> Rel

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

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

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

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
P \<leadsto>[Rel''] R

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma fold_graph_OR: "finite \<Phi> \<Longrightarrow> fold_graph Or_ltlp False_ltlp \<Phi> (OR \<Phi>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite \<Phi> \<Longrightarrow> fold_graph Or_ltlp false\<^sub>p \<Phi> (OR \<Phi>)
[PROOF STEP]
unfolding OR_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite \<Phi> \<Longrightarrow> fold_graph Or_ltlp false\<^sub>p \<Phi> (SOME \<phi>. fold_graph Or_ltlp false\<^sub>p \<Phi> \<phi>)
[PROOF STEP]
by (rule someI2_ex[OF finite_imp_fold_graph])


[STATEMENT]
lemma fold_graph_AND: "finite \<Phi> \<Longrightarrow> fold_graph And_ltlp True_ltlp \<Phi> (AND \<Phi>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite \<Phi> \<Longrightarrow> fold_graph And_ltlp true\<^sub>p \<Phi> (AND \<Phi>)
[PROOF STEP]
unfolding AND_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite \<Phi> \<Longrightarrow> fold_graph And_ltlp true\<^sub>p \<Phi> (SOME \<phi>. fold_graph And_ltlp true\<^sub>p \<Phi> \<phi>)
[PROOF STEP]
by (rule someI2_ex[OF finite_imp_fold_graph])


[STATEMENT]
lemma holds_of_OR [simp]:
  assumes fin: "finite (\<Phi>::'a pltl set)"
  shows "(\<sigma> \<Turnstile>\<^sub>p OR \<Phi>) = (\<exists>\<phi>\<in>\<Phi>. \<sigma> \<Turnstile>\<^sub>p \<phi>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<sigma> \<Turnstile>\<^sub>p OR \<Phi> = (\<exists>\<phi>\<in>\<Phi>. \<sigma> \<Turnstile>\<^sub>p \<phi>)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<sigma> \<Turnstile>\<^sub>p OR \<Phi> = (\<exists>\<phi>\<in>\<Phi>. \<sigma> \<Turnstile>\<^sub>p \<phi>)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<sigma> \<Turnstile>\<^sub>p OR \<Phi> = (\<exists>\<phi>\<in>\<Phi>. \<sigma> \<Turnstile>\<^sub>p \<phi>)
[PROOF STEP]
fix \<psi>::"'a pltl"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<sigma> \<Turnstile>\<^sub>p OR \<Phi> = (\<exists>\<phi>\<in>\<Phi>. \<sigma> \<Turnstile>\<^sub>p \<phi>)
[PROOF STEP]
assume "fold_graph Or_ltlp False_ltlp \<Phi> \<psi>"
[PROOF STATE]
proof (state)
this:
fold_graph Or_ltlp false\<^sub>p \<Phi> \<psi>

goal (1 subgoal):
 1. \<sigma> \<Turnstile>\<^sub>p OR \<Phi> = (\<exists>\<phi>\<in>\<Phi>. \<sigma> \<Turnstile>\<^sub>p \<phi>)
[PROOF STEP]
hence "(\<sigma> \<Turnstile>\<^sub>p \<psi>) = (\<exists>\<phi>\<in>\<Phi>. \<sigma> \<Turnstile>\<^sub>p \<phi>)"
[PROOF STATE]
proof (prove)
using this:
fold_graph Or_ltlp false\<^sub>p \<Phi> \<psi>

goal (1 subgoal):
 1. \<sigma> \<Turnstile>\<^sub>p \<psi> = (\<exists>\<phi>\<in>\<Phi>. \<sigma> \<Turnstile>\<^sub>p \<phi>)
[PROOF STEP]
by (rule fold_graph.induct) auto
[PROOF STATE]
proof (state)
this:
\<sigma> \<Turnstile>\<^sub>p \<psi> = (\<exists>\<phi>\<in>\<Phi>. \<sigma> \<Turnstile>\<^sub>p \<phi>)

goal (1 subgoal):
 1. \<sigma> \<Turnstile>\<^sub>p OR \<Phi> = (\<exists>\<phi>\<in>\<Phi>. \<sigma> \<Turnstile>\<^sub>p \<phi>)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
fold_graph Or_ltlp false\<^sub>p \<Phi> ?\<psi>2 \<Longrightarrow> \<sigma> \<Turnstile>\<^sub>p ?\<psi>2 = (\<exists>\<phi>\<in>\<Phi>. \<sigma> \<Turnstile>\<^sub>p \<phi>)

goal (1 subgoal):
 1. \<sigma> \<Turnstile>\<^sub>p OR \<Phi> = (\<exists>\<phi>\<in>\<Phi>. \<sigma> \<Turnstile>\<^sub>p \<phi>)
[PROOF STEP]
with fold_graph_OR[OF fin]
[PROOF STATE]
proof (chain)
picking this:
fold_graph Or_ltlp false\<^sub>p \<Phi> (OR \<Phi>)
fold_graph Or_ltlp false\<^sub>p \<Phi> ?\<psi>2 \<Longrightarrow> \<sigma> \<Turnstile>\<^sub>p ?\<psi>2 = (\<exists>\<phi>\<in>\<Phi>. \<sigma> \<Turnstile>\<^sub>p \<phi>)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
fold_graph Or_ltlp false\<^sub>p \<Phi> (OR \<Phi>)
fold_graph Or_ltlp false\<^sub>p \<Phi> ?\<psi>2 \<Longrightarrow> \<sigma> \<Turnstile>\<^sub>p ?\<psi>2 = (\<exists>\<phi>\<in>\<Phi>. \<sigma> \<Turnstile>\<^sub>p \<phi>)

goal (1 subgoal):
 1. \<sigma> \<Turnstile>\<^sub>p OR \<Phi> = (\<exists>\<phi>\<in>\<Phi>. \<sigma> \<Turnstile>\<^sub>p \<phi>)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<sigma> \<Turnstile>\<^sub>p OR \<Phi> = (\<exists>\<phi>\<in>\<Phi>. \<sigma> \<Turnstile>\<^sub>p \<phi>)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma holds_of_AND [simp]:
  assumes fin: "finite (\<Phi>::'a pltl set)"
  shows "(\<sigma> \<Turnstile>\<^sub>p AND \<Phi>) = (\<forall>\<phi>\<in>\<Phi>. \<sigma> \<Turnstile>\<^sub>p \<phi>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<sigma> \<Turnstile>\<^sub>p AND \<Phi> = (\<forall>\<phi>\<in>\<Phi>. \<sigma> \<Turnstile>\<^sub>p \<phi>)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<sigma> \<Turnstile>\<^sub>p AND \<Phi> = (\<forall>\<phi>\<in>\<Phi>. \<sigma> \<Turnstile>\<^sub>p \<phi>)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<sigma> \<Turnstile>\<^sub>p AND \<Phi> = (\<forall>\<phi>\<in>\<Phi>. \<sigma> \<Turnstile>\<^sub>p \<phi>)
[PROOF STEP]
fix \<psi>::"'a pltl"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<sigma> \<Turnstile>\<^sub>p AND \<Phi> = (\<forall>\<phi>\<in>\<Phi>. \<sigma> \<Turnstile>\<^sub>p \<phi>)
[PROOF STEP]
assume "fold_graph And_ltlp True_ltlp \<Phi> \<psi>"
[PROOF STATE]
proof (state)
this:
fold_graph And_ltlp true\<^sub>p \<Phi> \<psi>

goal (1 subgoal):
 1. \<sigma> \<Turnstile>\<^sub>p AND \<Phi> = (\<forall>\<phi>\<in>\<Phi>. \<sigma> \<Turnstile>\<^sub>p \<phi>)
[PROOF STEP]
hence "(\<sigma> \<Turnstile>\<^sub>p \<psi>) = (\<forall>\<phi>\<in>\<Phi>. \<sigma> \<Turnstile>\<^sub>p \<phi>)"
[PROOF STATE]
proof (prove)
using this:
fold_graph And_ltlp true\<^sub>p \<Phi> \<psi>

goal (1 subgoal):
 1. \<sigma> \<Turnstile>\<^sub>p \<psi> = (\<forall>\<phi>\<in>\<Phi>. \<sigma> \<Turnstile>\<^sub>p \<phi>)
[PROOF STEP]
by (rule fold_graph.induct) auto
[PROOF STATE]
proof (state)
this:
\<sigma> \<Turnstile>\<^sub>p \<psi> = (\<forall>\<phi>\<in>\<Phi>. \<sigma> \<Turnstile>\<^sub>p \<phi>)

goal (1 subgoal):
 1. \<sigma> \<Turnstile>\<^sub>p AND \<Phi> = (\<forall>\<phi>\<in>\<Phi>. \<sigma> \<Turnstile>\<^sub>p \<phi>)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
fold_graph And_ltlp true\<^sub>p \<Phi> ?\<psi>2 \<Longrightarrow> \<sigma> \<Turnstile>\<^sub>p ?\<psi>2 = (\<forall>\<phi>\<in>\<Phi>. \<sigma> \<Turnstile>\<^sub>p \<phi>)

goal (1 subgoal):
 1. \<sigma> \<Turnstile>\<^sub>p AND \<Phi> = (\<forall>\<phi>\<in>\<Phi>. \<sigma> \<Turnstile>\<^sub>p \<phi>)
[PROOF STEP]
with fold_graph_AND[OF fin]
[PROOF STATE]
proof (chain)
picking this:
fold_graph And_ltlp true\<^sub>p \<Phi> (AND \<Phi>)
fold_graph And_ltlp true\<^sub>p \<Phi> ?\<psi>2 \<Longrightarrow> \<sigma> \<Turnstile>\<^sub>p ?\<psi>2 = (\<forall>\<phi>\<in>\<Phi>. \<sigma> \<Turnstile>\<^sub>p \<phi>)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
fold_graph And_ltlp true\<^sub>p \<Phi> (AND \<Phi>)
fold_graph And_ltlp true\<^sub>p \<Phi> ?\<psi>2 \<Longrightarrow> \<sigma> \<Turnstile>\<^sub>p ?\<psi>2 = (\<forall>\<phi>\<in>\<Phi>. \<sigma> \<Turnstile>\<^sub>p \<phi>)

goal (1 subgoal):
 1. \<sigma> \<Turnstile>\<^sub>p AND \<Phi> = (\<forall>\<phi>\<in>\<Phi>. \<sigma> \<Turnstile>\<^sub>p \<phi>)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<sigma> \<Turnstile>\<^sub>p AND \<Phi> = (\<forall>\<phi>\<in>\<Phi>. \<sigma> \<Turnstile>\<^sub>p \<phi>)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma next_free_not [simp]:
  "next_free (not\<^sub>p \<phi>) = next_free \<phi>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. next_free (not\<^sub>p \<phi>) = next_free \<phi>
[PROOF STEP]
by (simp add: Not_ltlp_def)


[STATEMENT]
lemma next_free_true [simp]:
  "next_free true\<^sub>p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. next_free true\<^sub>p
[PROOF STEP]
by (simp add: True_ltlp_def)


[STATEMENT]
lemma next_free_or [simp]:
  "next_free (\<phi> or\<^sub>p \<psi>) = (next_free \<phi> \<and> next_free \<psi>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. next_free (\<phi> or\<^sub>p \<psi>) = (next_free \<phi> \<and> next_free \<psi>)
[PROOF STEP]
by (simp add: Or_ltlp_def)


[STATEMENT]
lemma next_free_and [simp]: "next_free (\<phi> and\<^sub>p \<psi>) = (next_free \<phi> \<and> next_free \<psi>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. next_free (\<phi> and\<^sub>p \<psi>) = (next_free \<phi> \<and> next_free \<psi>)
[PROOF STEP]
by (simp add: And_ltlp_def)


[STATEMENT]
lemma next_free_eventually [simp]:
  "next_free (F\<^sub>p \<phi>) = next_free \<phi>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. next_free (F\<^sub>p \<phi>) = next_free \<phi>
[PROOF STEP]
by (simp add: Eventually_ltlp_def)


[STATEMENT]
lemma next_free_always [simp]:
  "next_free (G\<^sub>p \<phi>) = next_free \<phi>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. next_free (G\<^sub>p \<phi>) = next_free \<phi>
[PROOF STEP]
by (simp add: Always_ltlp_def)


[STATEMENT]
lemma next_free_release [simp]:
  "next_free (\<phi> R\<^sub>p \<psi>) = (next_free \<phi> \<and> next_free \<psi>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. next_free (\<phi> R\<^sub>p \<psi>) = (next_free \<phi> \<and> next_free \<psi>)
[PROOF STEP]
by (simp add: Release_ltlp_def)


[STATEMENT]
lemma next_free_strong_release [simp]:
  "next_free (\<phi> M\<^sub>p \<psi>) = (next_free \<phi> \<and> next_free \<psi>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. next_free (\<phi> M\<^sub>p \<psi>) = (next_free \<phi> \<and> next_free \<psi>)
[PROOF STEP]
by (auto simp: StrongRelease_ltlp_def)


[STATEMENT]
lemma next_free_OR [simp]:
  assumes fin: "finite (\<Phi>::'a pltl set)"
  shows "next_free (OR \<Phi>) = (\<forall>\<phi>\<in>\<Phi>. next_free \<phi>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. next_free (OR \<Phi>) = (\<forall>\<phi>\<in>\<Phi>. next_free \<phi>)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. next_free (OR \<Phi>) = (\<forall>\<phi>\<in>\<Phi>. next_free \<phi>)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. next_free (OR \<Phi>) = (\<forall>\<phi>\<in>\<Phi>. next_free \<phi>)
[PROOF STEP]
fix \<psi>::"'a pltl"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. next_free (OR \<Phi>) = (\<forall>\<phi>\<in>\<Phi>. next_free \<phi>)
[PROOF STEP]
assume "fold_graph Or_ltlp False_ltlp \<Phi> \<psi>"
[PROOF STATE]
proof (state)
this:
fold_graph Or_ltlp false\<^sub>p \<Phi> \<psi>

goal (1 subgoal):
 1. next_free (OR \<Phi>) = (\<forall>\<phi>\<in>\<Phi>. next_free \<phi>)
[PROOF STEP]
hence "next_free \<psi> = (\<forall>\<phi>\<in>\<Phi>. next_free \<phi>)"
[PROOF STATE]
proof (prove)
using this:
fold_graph Or_ltlp false\<^sub>p \<Phi> \<psi>

goal (1 subgoal):
 1. next_free \<psi> = (\<forall>\<phi>\<in>\<Phi>. next_free \<phi>)
[PROOF STEP]
by (rule fold_graph.induct) auto
[PROOF STATE]
proof (state)
this:
next_free \<psi> = (\<forall>\<phi>\<in>\<Phi>. next_free \<phi>)

goal (1 subgoal):
 1. next_free (OR \<Phi>) = (\<forall>\<phi>\<in>\<Phi>. next_free \<phi>)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
fold_graph Or_ltlp false\<^sub>p \<Phi> ?\<psi>2 \<Longrightarrow> next_free ?\<psi>2 = (\<forall>\<phi>\<in>\<Phi>. next_free \<phi>)

goal (1 subgoal):
 1. next_free (OR \<Phi>) = (\<forall>\<phi>\<in>\<Phi>. next_free \<phi>)
[PROOF STEP]
with fold_graph_OR[OF fin]
[PROOF STATE]
proof (chain)
picking this:
fold_graph Or_ltlp false\<^sub>p \<Phi> (OR \<Phi>)
fold_graph Or_ltlp false\<^sub>p \<Phi> ?\<psi>2 \<Longrightarrow> next_free ?\<psi>2 = (\<forall>\<phi>\<in>\<Phi>. next_free \<phi>)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
fold_graph Or_ltlp false\<^sub>p \<Phi> (OR \<Phi>)
fold_graph Or_ltlp false\<^sub>p \<Phi> ?\<psi>2 \<Longrightarrow> next_free ?\<psi>2 = (\<forall>\<phi>\<in>\<Phi>. next_free \<phi>)

goal (1 subgoal):
 1. next_free (OR \<Phi>) = (\<forall>\<phi>\<in>\<Phi>. next_free \<phi>)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
next_free (OR \<Phi>) = (\<forall>\<phi>\<in>\<Phi>. next_free \<phi>)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma next_free_AND [simp]:
  assumes fin: "finite (\<Phi>::'a pltl set)"
  shows "next_free (AND \<Phi>) = (\<forall>\<phi>\<in>\<Phi>. next_free \<phi>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. next_free (AND \<Phi>) = (\<forall>\<phi>\<in>\<Phi>. next_free \<phi>)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. next_free (AND \<Phi>) = (\<forall>\<phi>\<in>\<Phi>. next_free \<phi>)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. next_free (AND \<Phi>) = (\<forall>\<phi>\<in>\<Phi>. next_free \<phi>)
[PROOF STEP]
fix \<psi>::"'a pltl"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. next_free (AND \<Phi>) = (\<forall>\<phi>\<in>\<Phi>. next_free \<phi>)
[PROOF STEP]
assume "fold_graph And_ltlp True_ltlp \<Phi> \<psi>"
[PROOF STATE]
proof (state)
this:
fold_graph And_ltlp true\<^sub>p \<Phi> \<psi>

goal (1 subgoal):
 1. next_free (AND \<Phi>) = (\<forall>\<phi>\<in>\<Phi>. next_free \<phi>)
[PROOF STEP]
hence "next_free \<psi> = (\<forall>\<phi>\<in>\<Phi>. next_free \<phi>)"
[PROOF STATE]
proof (prove)
using this:
fold_graph And_ltlp true\<^sub>p \<Phi> \<psi>

goal (1 subgoal):
 1. next_free \<psi> = (\<forall>\<phi>\<in>\<Phi>. next_free \<phi>)
[PROOF STEP]
by (rule fold_graph.induct) auto
[PROOF STATE]
proof (state)
this:
next_free \<psi> = (\<forall>\<phi>\<in>\<Phi>. next_free \<phi>)

goal (1 subgoal):
 1. next_free (AND \<Phi>) = (\<forall>\<phi>\<in>\<Phi>. next_free \<phi>)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
fold_graph And_ltlp true\<^sub>p \<Phi> ?\<psi>2 \<Longrightarrow> next_free ?\<psi>2 = (\<forall>\<phi>\<in>\<Phi>. next_free \<phi>)

goal (1 subgoal):
 1. next_free (AND \<Phi>) = (\<forall>\<phi>\<in>\<Phi>. next_free \<phi>)
[PROOF STEP]
with fold_graph_AND[OF fin]
[PROOF STATE]
proof (chain)
picking this:
fold_graph And_ltlp true\<^sub>p \<Phi> (AND \<Phi>)
fold_graph And_ltlp true\<^sub>p \<Phi> ?\<psi>2 \<Longrightarrow> next_free ?\<psi>2 = (\<forall>\<phi>\<in>\<Phi>. next_free \<phi>)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
fold_graph And_ltlp true\<^sub>p \<Phi> (AND \<Phi>)
fold_graph And_ltlp true\<^sub>p \<Phi> ?\<psi>2 \<Longrightarrow> next_free ?\<psi>2 = (\<forall>\<phi>\<in>\<Phi>. next_free \<phi>)

goal (1 subgoal):
 1. next_free (AND \<Phi>) = (\<forall>\<phi>\<in>\<Phi>. next_free \<phi>)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
next_free (AND \<Phi>) = (\<forall>\<phi>\<in>\<Phi>. next_free \<phi>)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma stutter_invariantI [intro!]:
  assumes "\<And>\<sigma> \<tau>. \<lbrakk>\<sigma> \<approx> \<tau>; \<sigma> \<Turnstile>\<^sub>p \<phi>\<rbrakk> \<Longrightarrow> \<tau> \<Turnstile>\<^sub>p \<phi>"
  shows "stutter_invariant \<phi>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. stutter_invariant \<phi>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. stutter_invariant \<phi>
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. stutter_invariant \<phi>
[PROOF STEP]
fix \<sigma> \<tau>
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. stutter_invariant \<phi>
[PROOF STEP]
assume st: "\<sigma> \<approx> \<tau>" and f: "\<sigma> \<Turnstile>\<^sub>p \<phi>"
[PROOF STATE]
proof (state)
this:
\<sigma> \<approx> \<tau>
\<sigma> \<Turnstile>\<^sub>p \<phi>

goal (1 subgoal):
 1. stutter_invariant \<phi>
[PROOF STEP]
hence "\<tau> \<Turnstile>\<^sub>p \<phi>"
[PROOF STATE]
proof (prove)
using this:
\<sigma> \<approx> \<tau>
\<sigma> \<Turnstile>\<^sub>p \<phi>

goal (1 subgoal):
 1. \<tau> \<Turnstile>\<^sub>p \<phi>
[PROOF STEP]
by (rule assms)
[PROOF STATE]
proof (state)
this:
\<tau> \<Turnstile>\<^sub>p \<phi>

goal (1 subgoal):
 1. stutter_invariant \<phi>
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>?\<sigma>2 \<approx> ?\<tau>2; ?\<sigma>2 \<Turnstile>\<^sub>p \<phi>\<rbrakk> \<Longrightarrow> ?\<tau>2 \<Turnstile>\<^sub>p \<phi>

goal (1 subgoal):
 1. stutter_invariant \<phi>
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<lbrakk>?\<sigma>2 \<approx> ?\<tau>2; ?\<sigma>2 \<Turnstile>\<^sub>p \<phi>\<rbrakk> \<Longrightarrow> ?\<tau>2 \<Turnstile>\<^sub>p \<phi>

goal (1 subgoal):
 1. stutter_invariant \<phi>
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
\<lbrakk>?\<sigma>2 \<approx> ?\<tau>2; ?\<sigma>2 \<Turnstile>\<^sub>p \<phi>\<rbrakk> \<Longrightarrow> ?\<tau>2 \<Turnstile>\<^sub>p \<phi>

goal (1 subgoal):
 1. stutter_invariant \<phi>
[PROOF STEP]
fix \<sigma> \<tau>
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. stutter_invariant \<phi>
[PROOF STEP]
assume st: "\<sigma> \<approx> \<tau>" and f: "\<tau> \<Turnstile>\<^sub>p \<phi>"
[PROOF STATE]
proof (state)
this:
\<sigma> \<approx> \<tau>
\<tau> \<Turnstile>\<^sub>p \<phi>

goal (1 subgoal):
 1. stutter_invariant \<phi>
[PROOF STEP]
from st
[PROOF STATE]
proof (chain)
picking this:
\<sigma> \<approx> \<tau>
[PROOF STEP]
have "\<tau> \<approx> \<sigma>"
[PROOF STATE]
proof (prove)
using this:
\<sigma> \<approx> \<tau>

goal (1 subgoal):
 1. \<tau> \<approx> \<sigma>
[PROOF STEP]
by (rule stutter_equiv_sym)
[PROOF STATE]
proof (state)
this:
\<tau> \<approx> \<sigma>

goal (1 subgoal):
 1. stutter_invariant \<phi>
[PROOF STEP]
from this f
[PROOF STATE]
proof (chain)
picking this:
\<tau> \<approx> \<sigma>
\<tau> \<Turnstile>\<^sub>p \<phi>
[PROOF STEP]
have "\<sigma> \<Turnstile>\<^sub>p \<phi>"
[PROOF STATE]
proof (prove)
using this:
\<tau> \<approx> \<sigma>
\<tau> \<Turnstile>\<^sub>p \<phi>

goal (1 subgoal):
 1. \<sigma> \<Turnstile>\<^sub>p \<phi>
[PROOF STEP]
by (rule assms)
[PROOF STATE]
proof (state)
this:
\<sigma> \<Turnstile>\<^sub>p \<phi>

goal (1 subgoal):
 1. stutter_invariant \<phi>
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>?\<sigma>2 \<approx> ?\<tau>2; ?\<tau>2 \<Turnstile>\<^sub>p \<phi>\<rbrakk> \<Longrightarrow> ?\<sigma>2 \<Turnstile>\<^sub>p \<phi>

goal (1 subgoal):
 1. stutter_invariant \<phi>
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>?\<sigma>2 \<approx> ?\<tau>2; ?\<sigma>2 \<Turnstile>\<^sub>p \<phi>\<rbrakk> \<Longrightarrow> ?\<tau>2 \<Turnstile>\<^sub>p \<phi>
\<lbrakk>?\<sigma>2 \<approx> ?\<tau>2; ?\<tau>2 \<Turnstile>\<^sub>p \<phi>\<rbrakk> \<Longrightarrow> ?\<sigma>2 \<Turnstile>\<^sub>p \<phi>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?\<sigma>2 \<approx> ?\<tau>2; ?\<sigma>2 \<Turnstile>\<^sub>p \<phi>\<rbrakk> \<Longrightarrow> ?\<tau>2 \<Turnstile>\<^sub>p \<phi>
\<lbrakk>?\<sigma>2 \<approx> ?\<tau>2; ?\<tau>2 \<Turnstile>\<^sub>p \<phi>\<rbrakk> \<Longrightarrow> ?\<sigma>2 \<Turnstile>\<^sub>p \<phi>

goal (1 subgoal):
 1. stutter_invariant \<phi>
[PROOF STEP]
by (auto simp: stutter_invariant_def)
[PROOF STATE]
proof (state)
this:
stutter_invariant \<phi>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma stutter_invariantD [dest]:
  assumes "stutter_invariant \<phi>" and "\<sigma> \<approx> \<tau>"
  shows "(\<sigma> \<Turnstile>\<^sub>p \<phi>) = (\<tau> \<Turnstile>\<^sub>p \<phi>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<sigma> \<Turnstile>\<^sub>p \<phi> = \<tau> \<Turnstile>\<^sub>p \<phi>
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
stutter_invariant \<phi>
\<sigma> \<approx> \<tau>

goal (1 subgoal):
 1. \<sigma> \<Turnstile>\<^sub>p \<phi> = \<tau> \<Turnstile>\<^sub>p \<phi>
[PROOF STEP]
by (auto simp: stutter_invariant_def)


[STATEMENT]
theorem next_free_stutter_invariant:
  "next_free \<phi> \<Longrightarrow> stutter_invariant (\<phi>::'a pltl)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. next_free \<phi> \<Longrightarrow> stutter_invariant \<phi>
[PROOF STEP]
proof (induct "\<phi>")
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. next_free false\<^sub>p \<Longrightarrow> stutter_invariant false\<^sub>p
 2. \<And>x. next_free atom\<^sub>p(x) \<Longrightarrow> stutter_invariant atom\<^sub>p(x)
 3. \<And>\<phi>1 \<phi>2. \<lbrakk>next_free \<phi>1 \<Longrightarrow> stutter_invariant \<phi>1; next_free \<phi>2 \<Longrightarrow> stutter_invariant \<phi>2; next_free (\<phi>1 implies\<^sub>p \<phi>2)\<rbrakk> \<Longrightarrow> stutter_invariant (\<phi>1 implies\<^sub>p \<phi>2)
 4. \<And>\<phi>. \<lbrakk>next_free \<phi> \<Longrightarrow> stutter_invariant \<phi>; next_free (X\<^sub>p \<phi>)\<rbrakk> \<Longrightarrow> stutter_invariant (X\<^sub>p \<phi>)
 5. \<And>\<phi>1 \<phi>2. \<lbrakk>next_free \<phi>1 \<Longrightarrow> stutter_invariant \<phi>1; next_free \<phi>2 \<Longrightarrow> stutter_invariant \<phi>2; next_free (\<phi>1 U\<^sub>p \<phi>2)\<rbrakk> \<Longrightarrow> stutter_invariant (\<phi>1 U\<^sub>p \<phi>2)
[PROOF STEP]
show "stutter_invariant false\<^sub>p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. stutter_invariant false\<^sub>p
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
stutter_invariant false\<^sub>p

goal (4 subgoals):
 1. \<And>x. next_free atom\<^sub>p(x) \<Longrightarrow> stutter_invariant atom\<^sub>p(x)
 2. \<And>\<phi>1 \<phi>2. \<lbrakk>next_free \<phi>1 \<Longrightarrow> stutter_invariant \<phi>1; next_free \<phi>2 \<Longrightarrow> stutter_invariant \<phi>2; next_free (\<phi>1 implies\<^sub>p \<phi>2)\<rbrakk> \<Longrightarrow> stutter_invariant (\<phi>1 implies\<^sub>p \<phi>2)
 3. \<And>\<phi>. \<lbrakk>next_free \<phi> \<Longrightarrow> stutter_invariant \<phi>; next_free (X\<^sub>p \<phi>)\<rbrakk> \<Longrightarrow> stutter_invariant (X\<^sub>p \<phi>)
 4. \<And>\<phi>1 \<phi>2. \<lbrakk>next_free \<phi>1 \<Longrightarrow> stutter_invariant \<phi>1; next_free \<phi>2 \<Longrightarrow> stutter_invariant \<phi>2; next_free (\<phi>1 U\<^sub>p \<phi>2)\<rbrakk> \<Longrightarrow> stutter_invariant (\<phi>1 U\<^sub>p \<phi>2)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>x. next_free atom\<^sub>p(x) \<Longrightarrow> stutter_invariant atom\<^sub>p(x)
 2. \<And>\<phi>1 \<phi>2. \<lbrakk>next_free \<phi>1 \<Longrightarrow> stutter_invariant \<phi>1; next_free \<phi>2 \<Longrightarrow> stutter_invariant \<phi>2; next_free (\<phi>1 implies\<^sub>p \<phi>2)\<rbrakk> \<Longrightarrow> stutter_invariant (\<phi>1 implies\<^sub>p \<phi>2)
 3. \<And>\<phi>. \<lbrakk>next_free \<phi> \<Longrightarrow> stutter_invariant \<phi>; next_free (X\<^sub>p \<phi>)\<rbrakk> \<Longrightarrow> stutter_invariant (X\<^sub>p \<phi>)
 4. \<And>\<phi>1 \<phi>2. \<lbrakk>next_free \<phi>1 \<Longrightarrow> stutter_invariant \<phi>1; next_free \<phi>2 \<Longrightarrow> stutter_invariant \<phi>2; next_free (\<phi>1 U\<^sub>p \<phi>2)\<rbrakk> \<Longrightarrow> stutter_invariant (\<phi>1 U\<^sub>p \<phi>2)
[PROOF STEP]
fix p :: "'a \<Rightarrow> bool"
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>x. next_free atom\<^sub>p(x) \<Longrightarrow> stutter_invariant atom\<^sub>p(x)
 2. \<And>\<phi>1 \<phi>2. \<lbrakk>next_free \<phi>1 \<Longrightarrow> stutter_invariant \<phi>1; next_free \<phi>2 \<Longrightarrow> stutter_invariant \<phi>2; next_free (\<phi>1 implies\<^sub>p \<phi>2)\<rbrakk> \<Longrightarrow> stutter_invariant (\<phi>1 implies\<^sub>p \<phi>2)
 3. \<And>\<phi>. \<lbrakk>next_free \<phi> \<Longrightarrow> stutter_invariant \<phi>; next_free (X\<^sub>p \<phi>)\<rbrakk> \<Longrightarrow> stutter_invariant (X\<^sub>p \<phi>)
 4. \<And>\<phi>1 \<phi>2. \<lbrakk>next_free \<phi>1 \<Longrightarrow> stutter_invariant \<phi>1; next_free \<phi>2 \<Longrightarrow> stutter_invariant \<phi>2; next_free (\<phi>1 U\<^sub>p \<phi>2)\<rbrakk> \<Longrightarrow> stutter_invariant (\<phi>1 U\<^sub>p \<phi>2)
[PROOF STEP]
show "stutter_invariant (atom\<^sub>p(p))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. stutter_invariant atom\<^sub>p(p)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>\<sigma> \<tau>. \<lbrakk>\<sigma> \<approx> \<tau>; \<sigma> \<Turnstile>\<^sub>p atom\<^sub>p(p)\<rbrakk> \<Longrightarrow> \<tau> \<Turnstile>\<^sub>p atom\<^sub>p(p)
[PROOF STEP]
fix \<sigma> \<tau>
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>\<sigma> \<tau>. \<lbrakk>\<sigma> \<approx> \<tau>; \<sigma> \<Turnstile>\<^sub>p atom\<^sub>p(p)\<rbrakk> \<Longrightarrow> \<tau> \<Turnstile>\<^sub>p atom\<^sub>p(p)
[PROOF STEP]
assume "\<sigma> \<approx> \<tau>" "\<sigma> \<Turnstile>\<^sub>p atom\<^sub>p(p)"
[PROOF STATE]
proof (state)
this:
\<sigma> \<approx> \<tau>
\<sigma> \<Turnstile>\<^sub>p atom\<^sub>p(p)

goal (1 subgoal):
 1. \<And>\<sigma> \<tau>. \<lbrakk>\<sigma> \<approx> \<tau>; \<sigma> \<Turnstile>\<^sub>p atom\<^sub>p(p)\<rbrakk> \<Longrightarrow> \<tau> \<Turnstile>\<^sub>p atom\<^sub>p(p)
[PROOF STEP]
thus "\<tau> \<Turnstile>\<^sub>p atom\<^sub>p(p)"
[PROOF STATE]
proof (prove)
using this:
\<sigma> \<approx> \<tau>
\<sigma> \<Turnstile>\<^sub>p atom\<^sub>p(p)

goal (1 subgoal):
 1. \<tau> \<Turnstile>\<^sub>p atom\<^sub>p(p)
[PROOF STEP]
by (simp add: stutter_equiv_0)
[PROOF STATE]
proof (state)
this:
\<tau> \<Turnstile>\<^sub>p atom\<^sub>p(p)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
stutter_invariant atom\<^sub>p(p)

goal (3 subgoals):
 1. \<And>\<phi>1 \<phi>2. \<lbrakk>next_free \<phi>1 \<Longrightarrow> stutter_invariant \<phi>1; next_free \<phi>2 \<Longrightarrow> stutter_invariant \<phi>2; next_free (\<phi>1 implies\<^sub>p \<phi>2)\<rbrakk> \<Longrightarrow> stutter_invariant (\<phi>1 implies\<^sub>p \<phi>2)
 2. \<And>\<phi>. \<lbrakk>next_free \<phi> \<Longrightarrow> stutter_invariant \<phi>; next_free (X\<^sub>p \<phi>)\<rbrakk> \<Longrightarrow> stutter_invariant (X\<^sub>p \<phi>)
 3. \<And>\<phi>1 \<phi>2. \<lbrakk>next_free \<phi>1 \<Longrightarrow> stutter_invariant \<phi>1; next_free \<phi>2 \<Longrightarrow> stutter_invariant \<phi>2; next_free (\<phi>1 U\<^sub>p \<phi>2)\<rbrakk> \<Longrightarrow> stutter_invariant (\<phi>1 U\<^sub>p \<phi>2)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>\<phi>1 \<phi>2. \<lbrakk>next_free \<phi>1 \<Longrightarrow> stutter_invariant \<phi>1; next_free \<phi>2 \<Longrightarrow> stutter_invariant \<phi>2; next_free (\<phi>1 implies\<^sub>p \<phi>2)\<rbrakk> \<Longrightarrow> stutter_invariant (\<phi>1 implies\<^sub>p \<phi>2)
 2. \<And>\<phi>. \<lbrakk>next_free \<phi> \<Longrightarrow> stutter_invariant \<phi>; next_free (X\<^sub>p \<phi>)\<rbrakk> \<Longrightarrow> stutter_invariant (X\<^sub>p \<phi>)
 3. \<And>\<phi>1 \<phi>2. \<lbrakk>next_free \<phi>1 \<Longrightarrow> stutter_invariant \<phi>1; next_free \<phi>2 \<Longrightarrow> stutter_invariant \<phi>2; next_free (\<phi>1 U\<^sub>p \<phi>2)\<rbrakk> \<Longrightarrow> stutter_invariant (\<phi>1 U\<^sub>p \<phi>2)
[PROOF STEP]
fix \<phi> \<psi> :: "'a pltl"
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>\<phi>1 \<phi>2. \<lbrakk>next_free \<phi>1 \<Longrightarrow> stutter_invariant \<phi>1; next_free \<phi>2 \<Longrightarrow> stutter_invariant \<phi>2; next_free (\<phi>1 implies\<^sub>p \<phi>2)\<rbrakk> \<Longrightarrow> stutter_invariant (\<phi>1 implies\<^sub>p \<phi>2)
 2. \<And>\<phi>. \<lbrakk>next_free \<phi> \<Longrightarrow> stutter_invariant \<phi>; next_free (X\<^sub>p \<phi>)\<rbrakk> \<Longrightarrow> stutter_invariant (X\<^sub>p \<phi>)
 3. \<And>\<phi>1 \<phi>2. \<lbrakk>next_free \<phi>1 \<Longrightarrow> stutter_invariant \<phi>1; next_free \<phi>2 \<Longrightarrow> stutter_invariant \<phi>2; next_free (\<phi>1 U\<^sub>p \<phi>2)\<rbrakk> \<Longrightarrow> stutter_invariant (\<phi>1 U\<^sub>p \<phi>2)
[PROOF STEP]
assume ih: "next_free \<phi> \<Longrightarrow> stutter_invariant \<phi>"
             "next_free \<psi> \<Longrightarrow> stutter_invariant \<psi>"
[PROOF STATE]
proof (state)
this:
next_free \<phi> \<Longrightarrow> stutter_invariant \<phi>
next_free \<psi> \<Longrightarrow> stutter_invariant \<psi>

goal (3 subgoals):
 1. \<And>\<phi>1 \<phi>2. \<lbrakk>next_free \<phi>1 \<Longrightarrow> stutter_invariant \<phi>1; next_free \<phi>2 \<Longrightarrow> stutter_invariant \<phi>2; next_free (\<phi>1 implies\<^sub>p \<phi>2)\<rbrakk> \<Longrightarrow> stutter_invariant (\<phi>1 implies\<^sub>p \<phi>2)
 2. \<And>\<phi>. \<lbrakk>next_free \<phi> \<Longrightarrow> stutter_invariant \<phi>; next_free (X\<^sub>p \<phi>)\<rbrakk> \<Longrightarrow> stutter_invariant (X\<^sub>p \<phi>)
 3. \<And>\<phi>1 \<phi>2. \<lbrakk>next_free \<phi>1 \<Longrightarrow> stutter_invariant \<phi>1; next_free \<phi>2 \<Longrightarrow> stutter_invariant \<phi>2; next_free (\<phi>1 U\<^sub>p \<phi>2)\<rbrakk> \<Longrightarrow> stutter_invariant (\<phi>1 U\<^sub>p \<phi>2)
[PROOF STEP]
assume "next_free (\<phi> implies\<^sub>p \<psi>)"
[PROOF STATE]
proof (state)
this:
next_free (\<phi> implies\<^sub>p \<psi>)

goal (3 subgoals):
 1. \<And>\<phi>1 \<phi>2. \<lbrakk>next_free \<phi>1 \<Longrightarrow> stutter_invariant \<phi>1; next_free \<phi>2 \<Longrightarrow> stutter_invariant \<phi>2; next_free (\<phi>1 implies\<^sub>p \<phi>2)\<rbrakk> \<Longrightarrow> stutter_invariant (\<phi>1 implies\<^sub>p \<phi>2)
 2. \<And>\<phi>. \<lbrakk>next_free \<phi> \<Longrightarrow> stutter_invariant \<phi>; next_free (X\<^sub>p \<phi>)\<rbrakk> \<Longrightarrow> stutter_invariant (X\<^sub>p \<phi>)
 3. \<And>\<phi>1 \<phi>2. \<lbrakk>next_free \<phi>1 \<Longrightarrow> stutter_invariant \<phi>1; next_free \<phi>2 \<Longrightarrow> stutter_invariant \<phi>2; next_free (\<phi>1 U\<^sub>p \<phi>2)\<rbrakk> \<Longrightarrow> stutter_invariant (\<phi>1 U\<^sub>p \<phi>2)
[PROOF STEP]
with ih
[PROOF STATE]
proof (chain)
picking this:
next_free \<phi> \<Longrightarrow> stutter_invariant \<phi>
next_free \<psi> \<Longrightarrow> stutter_invariant \<psi>
next_free (\<phi> implies\<^sub>p \<psi>)
[PROOF STEP]
show "stutter_invariant (\<phi> implies\<^sub>p \<psi>)"
[PROOF STATE]
proof (prove)
using this:
next_free \<phi> \<Longrightarrow> stutter_invariant \<phi>
next_free \<psi> \<Longrightarrow> stutter_invariant \<psi>
next_free (\<phi> implies\<^sub>p \<psi>)

goal (1 subgoal):
 1. stutter_invariant (\<phi> implies\<^sub>p \<psi>)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
stutter_invariant (\<phi> implies\<^sub>p \<psi>)

goal (2 subgoals):
 1. \<And>\<phi>. \<lbrakk>next_free \<phi> \<Longrightarrow> stutter_invariant \<phi>; next_free (X\<^sub>p \<phi>)\<rbrakk> \<Longrightarrow> stutter_invariant (X\<^sub>p \<phi>)
 2. \<And>\<phi>1 \<phi>2. \<lbrakk>next_free \<phi>1 \<Longrightarrow> stutter_invariant \<phi>1; next_free \<phi>2 \<Longrightarrow> stutter_invariant \<phi>2; next_free (\<phi>1 U\<^sub>p \<phi>2)\<rbrakk> \<Longrightarrow> stutter_invariant (\<phi>1 U\<^sub>p \<phi>2)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>\<phi>. \<lbrakk>next_free \<phi> \<Longrightarrow> stutter_invariant \<phi>; next_free (X\<^sub>p \<phi>)\<rbrakk> \<Longrightarrow> stutter_invariant (X\<^sub>p \<phi>)
 2. \<And>\<phi>1 \<phi>2. \<lbrakk>next_free \<phi>1 \<Longrightarrow> stutter_invariant \<phi>1; next_free \<phi>2 \<Longrightarrow> stutter_invariant \<phi>2; next_free (\<phi>1 U\<^sub>p \<phi>2)\<rbrakk> \<Longrightarrow> stutter_invariant (\<phi>1 U\<^sub>p \<phi>2)
[PROOF STEP]
fix \<phi> :: "'a pltl"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>\<phi>. \<lbrakk>next_free \<phi> \<Longrightarrow> stutter_invariant \<phi>; next_free (X\<^sub>p \<phi>)\<rbrakk> \<Longrightarrow> stutter_invariant (X\<^sub>p \<phi>)
 2. \<And>\<phi>1 \<phi>2. \<lbrakk>next_free \<phi>1 \<Longrightarrow> stutter_invariant \<phi>1; next_free \<phi>2 \<Longrightarrow> stutter_invariant \<phi>2; next_free (\<phi>1 U\<^sub>p \<phi>2)\<rbrakk> \<Longrightarrow> stutter_invariant (\<phi>1 U\<^sub>p \<phi>2)
[PROOF STEP]
assume "next_free (X\<^sub>p \<phi>)"  \<comment> \<open>hence contradiction\<close>
[PROOF STATE]
proof (state)
this:
next_free (X\<^sub>p \<phi>)

goal (2 subgoals):
 1. \<And>\<phi>. \<lbrakk>next_free \<phi> \<Longrightarrow> stutter_invariant \<phi>; next_free (X\<^sub>p \<phi>)\<rbrakk> \<Longrightarrow> stutter_invariant (X\<^sub>p \<phi>)
 2. \<And>\<phi>1 \<phi>2. \<lbrakk>next_free \<phi>1 \<Longrightarrow> stutter_invariant \<phi>1; next_free \<phi>2 \<Longrightarrow> stutter_invariant \<phi>2; next_free (\<phi>1 U\<^sub>p \<phi>2)\<rbrakk> \<Longrightarrow> stutter_invariant (\<phi>1 U\<^sub>p \<phi>2)
[PROOF STEP]
thus "stutter_invariant (X\<^sub>p \<phi>)"
[PROOF STATE]
proof (prove)
using this:
next_free (X\<^sub>p \<phi>)

goal (1 subgoal):
 1. stutter_invariant (X\<^sub>p \<phi>)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
stutter_invariant (X\<^sub>p \<phi>)

goal (1 subgoal):
 1. \<And>\<phi>1 \<phi>2. \<lbrakk>next_free \<phi>1 \<Longrightarrow> stutter_invariant \<phi>1; next_free \<phi>2 \<Longrightarrow> stutter_invariant \<phi>2; next_free (\<phi>1 U\<^sub>p \<phi>2)\<rbrakk> \<Longrightarrow> stutter_invariant (\<phi>1 U\<^sub>p \<phi>2)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>\<phi>1 \<phi>2. \<lbrakk>next_free \<phi>1 \<Longrightarrow> stutter_invariant \<phi>1; next_free \<phi>2 \<Longrightarrow> stutter_invariant \<phi>2; next_free (\<phi>1 U\<^sub>p \<phi>2)\<rbrakk> \<Longrightarrow> stutter_invariant (\<phi>1 U\<^sub>p \<phi>2)
[PROOF STEP]
fix \<phi> \<psi> :: "'a pltl"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>\<phi>1 \<phi>2. \<lbrakk>next_free \<phi>1 \<Longrightarrow> stutter_invariant \<phi>1; next_free \<phi>2 \<Longrightarrow> stutter_invariant \<phi>2; next_free (\<phi>1 U\<^sub>p \<phi>2)\<rbrakk> \<Longrightarrow> stutter_invariant (\<phi>1 U\<^sub>p \<phi>2)
[PROOF STEP]
assume ih: "next_free \<phi> \<Longrightarrow> stutter_invariant \<phi>"
             "next_free \<psi> \<Longrightarrow> stutter_invariant \<psi>"
[PROOF STATE]
proof (state)
this:
next_free \<phi> \<Longrightarrow> stutter_invariant \<phi>
next_free \<psi> \<Longrightarrow> stutter_invariant \<psi>

goal (1 subgoal):
 1. \<And>\<phi>1 \<phi>2. \<lbrakk>next_free \<phi>1 \<Longrightarrow> stutter_invariant \<phi>1; next_free \<phi>2 \<Longrightarrow> stutter_invariant \<phi>2; next_free (\<phi>1 U\<^sub>p \<phi>2)\<rbrakk> \<Longrightarrow> stutter_invariant (\<phi>1 U\<^sub>p \<phi>2)
[PROOF STEP]
assume "next_free (\<phi> U\<^sub>p \<psi>)"
[PROOF STATE]
proof (state)
this:
next_free (\<phi> U\<^sub>p \<psi>)

goal (1 subgoal):
 1. \<And>\<phi>1 \<phi>2. \<lbrakk>next_free \<phi>1 \<Longrightarrow> stutter_invariant \<phi>1; next_free \<phi>2 \<Longrightarrow> stutter_invariant \<phi>2; next_free (\<phi>1 U\<^sub>p \<phi>2)\<rbrakk> \<Longrightarrow> stutter_invariant (\<phi>1 U\<^sub>p \<phi>2)
[PROOF STEP]
with ih
[PROOF STATE]
proof (chain)
picking this:
next_free \<phi> \<Longrightarrow> stutter_invariant \<phi>
next_free \<psi> \<Longrightarrow> stutter_invariant \<psi>
next_free (\<phi> U\<^sub>p \<psi>)
[PROOF STEP]
have stinv: "stutter_invariant \<phi>" "stutter_invariant \<psi>"
[PROOF STATE]
proof (prove)
using this:
next_free \<phi> \<Longrightarrow> stutter_invariant \<phi>
next_free \<psi> \<Longrightarrow> stutter_invariant \<psi>
next_free (\<phi> U\<^sub>p \<psi>)

goal (1 subgoal):
 1. stutter_invariant \<phi> &&& stutter_invariant \<psi>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
stutter_invariant \<phi>
stutter_invariant \<psi>

goal (1 subgoal):
 1. \<And>\<phi>1 \<phi>2. \<lbrakk>next_free \<phi>1 \<Longrightarrow> stutter_invariant \<phi>1; next_free \<phi>2 \<Longrightarrow> stutter_invariant \<phi>2; next_free (\<phi>1 U\<^sub>p \<phi>2)\<rbrakk> \<Longrightarrow> stutter_invariant (\<phi>1 U\<^sub>p \<phi>2)
[PROOF STEP]
show "stutter_invariant (\<phi> U\<^sub>p \<psi>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. stutter_invariant (\<phi> U\<^sub>p \<psi>)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>\<sigma> \<tau>. \<lbrakk>\<sigma> \<approx> \<tau>; \<sigma> \<Turnstile>\<^sub>p \<phi> U\<^sub>p \<psi>\<rbrakk> \<Longrightarrow> \<tau> \<Turnstile>\<^sub>p \<phi> U\<^sub>p \<psi>
[PROOF STEP]
fix \<sigma> \<tau>
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>\<sigma> \<tau>. \<lbrakk>\<sigma> \<approx> \<tau>; \<sigma> \<Turnstile>\<^sub>p \<phi> U\<^sub>p \<psi>\<rbrakk> \<Longrightarrow> \<tau> \<Turnstile>\<^sub>p \<phi> U\<^sub>p \<psi>
[PROOF STEP]
assume st: "\<sigma> \<approx> \<tau>" and unt: "\<sigma> \<Turnstile>\<^sub>p \<phi> U\<^sub>p \<psi>"
[PROOF STATE]
proof (state)
this:
\<sigma> \<approx> \<tau>
\<sigma> \<Turnstile>\<^sub>p \<phi> U\<^sub>p \<psi>

goal (1 subgoal):
 1. \<And>\<sigma> \<tau>. \<lbrakk>\<sigma> \<approx> \<tau>; \<sigma> \<Turnstile>\<^sub>p \<phi> U\<^sub>p \<psi>\<rbrakk> \<Longrightarrow> \<tau> \<Turnstile>\<^sub>p \<phi> U\<^sub>p \<psi>
[PROOF STEP]
from unt
[PROOF STATE]
proof (chain)
picking this:
\<sigma> \<Turnstile>\<^sub>p \<phi> U\<^sub>p \<psi>
[PROOF STEP]
obtain m
      where 1: "\<sigma>[m..] \<Turnstile>\<^sub>p \<psi>" and 2: "\<forall>j<m. (\<sigma>[j..] \<Turnstile>\<^sub>p \<phi>)"
[PROOF STATE]
proof (prove)
using this:
\<sigma> \<Turnstile>\<^sub>p \<phi> U\<^sub>p \<psi>

goal (1 subgoal):
 1. (\<And>m. \<lbrakk>\<sigma> [m..] \<Turnstile>\<^sub>p \<psi>; \<forall>j<m. \<sigma> [j..] \<Turnstile>\<^sub>p \<phi>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<sigma> [m..] \<Turnstile>\<^sub>p \<psi>
\<forall>j<m. \<sigma> [j..] \<Turnstile>\<^sub>p \<phi>

goal (1 subgoal):
 1. \<And>\<sigma> \<tau>. \<lbrakk>\<sigma> \<approx> \<tau>; \<sigma> \<Turnstile>\<^sub>p \<phi> U\<^sub>p \<psi>\<rbrakk> \<Longrightarrow> \<tau> \<Turnstile>\<^sub>p \<phi> U\<^sub>p \<psi>
[PROOF STEP]
from st
[PROOF STATE]
proof (chain)
picking this:
\<sigma> \<approx> \<tau>
[PROOF STEP]
obtain n
      where 3: "(\<sigma>[m..]) \<approx> (\<tau>[n..])" and 4: "\<forall>i<n. \<exists>j<m. (\<sigma>[j..]) \<approx> (\<tau>[i..])"
[PROOF STATE]
proof (prove)
using this:
\<sigma> \<approx> \<tau>

goal (1 subgoal):
 1. (\<And>n. \<lbrakk>\<sigma> [m..] \<approx> \<tau> [n..]; \<forall>i<n. \<exists>j<m. \<sigma> [j..] \<approx> \<tau> [i..]\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (rule stutter_equiv_suffixes_right)
[PROOF STATE]
proof (state)
this:
\<sigma> [m..] \<approx> \<tau> [n..]
\<forall>i<n. \<exists>j<m. \<sigma> [j..] \<approx> \<tau> [i..]

goal (1 subgoal):
 1. \<And>\<sigma> \<tau>. \<lbrakk>\<sigma> \<approx> \<tau>; \<sigma> \<Turnstile>\<^sub>p \<phi> U\<^sub>p \<psi>\<rbrakk> \<Longrightarrow> \<tau> \<Turnstile>\<^sub>p \<phi> U\<^sub>p \<psi>
[PROOF STEP]
from 1 3 stinv
[PROOF STATE]
proof (chain)
picking this:
\<sigma> [m..] \<Turnstile>\<^sub>p \<psi>
\<sigma> [m..] \<approx> \<tau> [n..]
stutter_invariant \<phi>
stutter_invariant \<psi>
[PROOF STEP]
have "\<tau>[n..] \<Turnstile>\<^sub>p \<psi>"
[PROOF STATE]
proof (prove)
using this:
\<sigma> [m..] \<Turnstile>\<^sub>p \<psi>
\<sigma> [m..] \<approx> \<tau> [n..]
stutter_invariant \<phi>
stutter_invariant \<psi>

goal (1 subgoal):
 1. \<tau> [n..] \<Turnstile>\<^sub>p \<psi>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<tau> [n..] \<Turnstile>\<^sub>p \<psi>

goal (1 subgoal):
 1. \<And>\<sigma> \<tau>. \<lbrakk>\<sigma> \<approx> \<tau>; \<sigma> \<Turnstile>\<^sub>p \<phi> U\<^sub>p \<psi>\<rbrakk> \<Longrightarrow> \<tau> \<Turnstile>\<^sub>p \<phi> U\<^sub>p \<psi>
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<tau> [n..] \<Turnstile>\<^sub>p \<psi>

goal (1 subgoal):
 1. \<And>\<sigma> \<tau>. \<lbrakk>\<sigma> \<approx> \<tau>; \<sigma> \<Turnstile>\<^sub>p \<phi> U\<^sub>p \<psi>\<rbrakk> \<Longrightarrow> \<tau> \<Turnstile>\<^sub>p \<phi> U\<^sub>p \<psi>
[PROOF STEP]
from 2 4 stinv
[PROOF STATE]
proof (chain)
picking this:
\<forall>j<m. \<sigma> [j..] \<Turnstile>\<^sub>p \<phi>
\<forall>i<n. \<exists>j<m. \<sigma> [j..] \<approx> \<tau> [i..]
stutter_invariant \<phi>
stutter_invariant \<psi>
[PROOF STEP]
have "\<forall>i<n. (\<tau>[i..] \<Turnstile>\<^sub>p \<phi>)"
[PROOF STATE]
proof (prove)
using this:
\<forall>j<m. \<sigma> [j..] \<Turnstile>\<^sub>p \<phi>
\<forall>i<n. \<exists>j<m. \<sigma> [j..] \<approx> \<tau> [i..]
stutter_invariant \<phi>
stutter_invariant \<psi>

goal (1 subgoal):
 1. \<forall>i<n. \<tau> [i..] \<Turnstile>\<^sub>p \<phi>
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
\<forall>i<n. \<tau> [i..] \<Turnstile>\<^sub>p \<phi>

goal (1 subgoal):
 1. \<And>\<sigma> \<tau>. \<lbrakk>\<sigma> \<approx> \<tau>; \<sigma> \<Turnstile>\<^sub>p \<phi> U\<^sub>p \<psi>\<rbrakk> \<Longrightarrow> \<tau> \<Turnstile>\<^sub>p \<phi> U\<^sub>p \<psi>
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<tau> [n..] \<Turnstile>\<^sub>p \<psi>
\<forall>i<n. \<tau> [i..] \<Turnstile>\<^sub>p \<phi>
[PROOF STEP]
show "\<tau> \<Turnstile>\<^sub>p \<phi> U\<^sub>p \<psi>"
[PROOF STATE]
proof (prove)
using this:
\<tau> [n..] \<Turnstile>\<^sub>p \<psi>
\<forall>i<n. \<tau> [i..] \<Turnstile>\<^sub>p \<phi>

goal (1 subgoal):
 1. \<tau> \<Turnstile>\<^sub>p \<phi> U\<^sub>p \<psi>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<tau> \<Turnstile>\<^sub>p \<phi> U\<^sub>p \<psi>

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
stutter_invariant (\<phi> U\<^sub>p \<psi>)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma atoms_pltl_OR [simp]:
  assumes fin: "finite (\<Phi>::'a pltl set)"
  shows "atoms_pltl (OR \<Phi>) = (\<Union>\<phi>\<in>\<Phi>. atoms_pltl \<phi>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. atoms_pltl (OR \<Phi>) = \<Union> (atoms_pltl ` \<Phi>)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. atoms_pltl (OR \<Phi>) = \<Union> (atoms_pltl ` \<Phi>)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. atoms_pltl (OR \<Phi>) = \<Union> (atoms_pltl ` \<Phi>)
[PROOF STEP]
fix \<psi>::"'a pltl"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. atoms_pltl (OR \<Phi>) = \<Union> (atoms_pltl ` \<Phi>)
[PROOF STEP]
assume "fold_graph Or_ltlp False_ltlp \<Phi> \<psi>"
[PROOF STATE]
proof (state)
this:
fold_graph Or_ltlp false\<^sub>p \<Phi> \<psi>

goal (1 subgoal):
 1. atoms_pltl (OR \<Phi>) = \<Union> (atoms_pltl ` \<Phi>)
[PROOF STEP]
hence "atoms_pltl \<psi> = (\<Union>\<phi>\<in>\<Phi>. atoms_pltl \<phi>)"
[PROOF STATE]
proof (prove)
using this:
fold_graph Or_ltlp false\<^sub>p \<Phi> \<psi>

goal (1 subgoal):
 1. atoms_pltl \<psi> = \<Union> (atoms_pltl ` \<Phi>)
[PROOF STEP]
by (rule fold_graph.induct) auto
[PROOF STATE]
proof (state)
this:
atoms_pltl \<psi> = \<Union> (atoms_pltl ` \<Phi>)

goal (1 subgoal):
 1. atoms_pltl (OR \<Phi>) = \<Union> (atoms_pltl ` \<Phi>)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
fold_graph Or_ltlp false\<^sub>p \<Phi> ?\<psi>2 \<Longrightarrow> atoms_pltl ?\<psi>2 = \<Union> (atoms_pltl ` \<Phi>)

goal (1 subgoal):
 1. atoms_pltl (OR \<Phi>) = \<Union> (atoms_pltl ` \<Phi>)
[PROOF STEP]
with fold_graph_OR[OF fin]
[PROOF STATE]
proof (chain)
picking this:
fold_graph Or_ltlp false\<^sub>p \<Phi> (OR \<Phi>)
fold_graph Or_ltlp false\<^sub>p \<Phi> ?\<psi>2 \<Longrightarrow> atoms_pltl ?\<psi>2 = \<Union> (atoms_pltl ` \<Phi>)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
fold_graph Or_ltlp false\<^sub>p \<Phi> (OR \<Phi>)
fold_graph Or_ltlp false\<^sub>p \<Phi> ?\<psi>2 \<Longrightarrow> atoms_pltl ?\<psi>2 = \<Union> (atoms_pltl ` \<Phi>)

goal (1 subgoal):
 1. atoms_pltl (OR \<Phi>) = \<Union> (atoms_pltl ` \<Phi>)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
atoms_pltl (OR \<Phi>) = \<Union> (atoms_pltl ` \<Phi>)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma atoms_pltl_AND [simp]:
  assumes fin: "finite (\<Phi>::'a pltl set)"
  shows "atoms_pltl (AND \<Phi>) = (\<Union>\<phi>\<in>\<Phi>. atoms_pltl \<phi>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. atoms_pltl (AND \<Phi>) = \<Union> (atoms_pltl ` \<Phi>)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. atoms_pltl (AND \<Phi>) = \<Union> (atoms_pltl ` \<Phi>)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. atoms_pltl (AND \<Phi>) = \<Union> (atoms_pltl ` \<Phi>)
[PROOF STEP]
fix \<psi>::"'a pltl"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. atoms_pltl (AND \<Phi>) = \<Union> (atoms_pltl ` \<Phi>)
[PROOF STEP]
assume "fold_graph And_ltlp True_ltlp \<Phi> \<psi>"
[PROOF STATE]
proof (state)
this:
fold_graph And_ltlp true\<^sub>p \<Phi> \<psi>

goal (1 subgoal):
 1. atoms_pltl (AND \<Phi>) = \<Union> (atoms_pltl ` \<Phi>)
[PROOF STEP]
hence "atoms_pltl \<psi> = (\<Union>\<phi>\<in>\<Phi>. atoms_pltl \<phi>)"
[PROOF STATE]
proof (prove)
using this:
fold_graph And_ltlp true\<^sub>p \<Phi> \<psi>

goal (1 subgoal):
 1. atoms_pltl \<psi> = \<Union> (atoms_pltl ` \<Phi>)
[PROOF STEP]
by (rule fold_graph.induct) auto
[PROOF STATE]
proof (state)
this:
atoms_pltl \<psi> = \<Union> (atoms_pltl ` \<Phi>)

goal (1 subgoal):
 1. atoms_pltl (AND \<Phi>) = \<Union> (atoms_pltl ` \<Phi>)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
fold_graph And_ltlp true\<^sub>p \<Phi> ?\<psi>2 \<Longrightarrow> atoms_pltl ?\<psi>2 = \<Union> (atoms_pltl ` \<Phi>)

goal (1 subgoal):
 1. atoms_pltl (AND \<Phi>) = \<Union> (atoms_pltl ` \<Phi>)
[PROOF STEP]
with fold_graph_AND[OF fin]
[PROOF STATE]
proof (chain)
picking this:
fold_graph And_ltlp true\<^sub>p \<Phi> (AND \<Phi>)
fold_graph And_ltlp true\<^sub>p \<Phi> ?\<psi>2 \<Longrightarrow> atoms_pltl ?\<psi>2 = \<Union> (atoms_pltl ` \<Phi>)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
fold_graph And_ltlp true\<^sub>p \<Phi> (AND \<Phi>)
fold_graph And_ltlp true\<^sub>p \<Phi> ?\<psi>2 \<Longrightarrow> atoms_pltl ?\<psi>2 = \<Union> (atoms_pltl ` \<Phi>)

goal (1 subgoal):
 1. atoms_pltl (AND \<Phi>) = \<Union> (atoms_pltl ` \<Phi>)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
atoms_pltl (AND \<Phi>) = \<Union> (atoms_pltl ` \<Phi>)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma state_sim_refl [simp]: "s ~A~ s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s ~A~ s
[PROOF STEP]
by (simp add: state_sim_def)


[STATEMENT]
lemma state_sim_sym: "s ~A~ t \<Longrightarrow> t ~A~ s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s ~A~ t \<Longrightarrow> t ~A~ s
[PROOF STEP]
by (auto simp: state_sim_def)


[STATEMENT]
lemma state_sim_trans[trans]: "s ~A~ t \<Longrightarrow> t ~A~ u \<Longrightarrow> s ~A~ u"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>s ~A~ t; t ~A~ u\<rbrakk> \<Longrightarrow> s ~A~ u
[PROOF STEP]
unfolding state_sim_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>p\<in>A. p s = p t; \<forall>p\<in>A. p t = p u\<rbrakk> \<Longrightarrow> \<forall>p\<in>A. p s = p u
[PROOF STEP]
by blast


[STATEMENT]
lemma state_sim_mono:
  assumes "s ~A~ t" and "B \<subseteq> A"
  shows "s ~B~ t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s ~B~ t
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
s ~A~ t
B \<subseteq> A

goal (1 subgoal):
 1. s ~B~ t
[PROOF STEP]
unfolding state_sim_def
[PROOF STATE]
proof (prove)
using this:
\<forall>p\<in>A. p s = p t
B \<subseteq> A

goal (1 subgoal):
 1. \<forall>p\<in>B. p s = p t
[PROOF STEP]
by auto


[STATEMENT]
lemma seq_sim_refl [simp]: "\<sigma> \<simeq>A\<simeq> \<sigma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<sigma> \<simeq>A\<simeq> \<sigma>
[PROOF STEP]
by (simp add: seq_sim_def)


[STATEMENT]
lemma seq_sim_sym: "\<sigma> \<simeq>A\<simeq> \<tau> \<Longrightarrow> \<tau> \<simeq>A\<simeq> \<sigma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<sigma> \<simeq>A\<simeq> \<tau> \<Longrightarrow> \<tau> \<simeq>A\<simeq> \<sigma>
[PROOF STEP]
by (auto simp: seq_sim_def state_sim_sym)


[STATEMENT]
lemma seq_sim_trans[trans]: "\<rho> \<simeq>A\<simeq> \<sigma> \<Longrightarrow> \<sigma> \<simeq>A\<simeq> \<tau> \<Longrightarrow> \<rho> \<simeq>A\<simeq> \<tau>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<rho> \<simeq>A\<simeq> \<sigma>; \<sigma> \<simeq>A\<simeq> \<tau>\<rbrakk> \<Longrightarrow> \<rho> \<simeq>A\<simeq> \<tau>
[PROOF STEP]
unfolding seq_sim_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>n. \<rho> n ~A~ \<sigma> n; \<forall>n. \<sigma> n ~A~ \<tau> n\<rbrakk> \<Longrightarrow> \<forall>n. \<rho> n ~A~ \<tau> n
[PROOF STEP]
by (blast intro: state_sim_trans)


[STATEMENT]
lemma seq_sim_mono:
  assumes "\<sigma> \<simeq>A\<simeq> \<tau>" and "B \<subseteq> A"
  shows "\<sigma> \<simeq>B\<simeq> \<tau>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<sigma> \<simeq>B\<simeq> \<tau>
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<sigma> \<simeq>A\<simeq> \<tau>
B \<subseteq> A

goal (1 subgoal):
 1. \<sigma> \<simeq>B\<simeq> \<tau>
[PROOF STEP]
unfolding seq_sim_def
[PROOF STATE]
proof (prove)
using this:
\<forall>n. \<sigma> n ~A~ \<tau> n
B \<subseteq> A

goal (1 subgoal):
 1. \<forall>n. \<sigma> n ~B~ \<tau> n
[PROOF STEP]
by (blast intro: state_sim_mono)