[STATEMENT]
lemma af\<^sub>G_implies_af_eval\<^sub>G:
  assumes "S \<Turnstile>\<^sub>P eval\<^sub>G \<G> (af\<^sub>G \<phi> (w [0\<rightarrow>j]))"
  assumes "\<And>\<psi>. G \<psi> \<in> \<G> \<Longrightarrow> S \<Turnstile>\<^sub>P G \<psi>"
  assumes "\<And>\<psi> i. G \<psi> \<in> \<G> \<Longrightarrow> i \<le> j \<Longrightarrow> S \<Turnstile>\<^sub>P eval\<^sub>G \<G> (af\<^sub>G \<psi> (w [i \<rightarrow> j]))"
  shows "S \<Turnstile>\<^sub>P af \<phi> (w [0\<rightarrow>j])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. S \<Turnstile>\<^sub>P af \<phi> (prefix j w)
[PROOF STEP]
using af\<^sub>G_implies_af_eval\<^sub>G'[OF assms(1-2), unfolded subsequence_length subsequence_drop] assms(3)
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<And>\<psi>. G \<psi> \<in> \<G> \<Longrightarrow> G \<psi> \<in> \<G>; \<And>\<psi> i. \<lbrakk>G \<psi> \<in> \<G>; i < j - 0\<rbrakk> \<Longrightarrow> S \<Turnstile>\<^sub>P eval\<^sub>G \<G> (af\<^sub>G \<psi> (w [0 + i \<rightarrow> j]))\<rbrakk> \<Longrightarrow> S \<Turnstile>\<^sub>P af \<phi> (prefix j w)
\<lbrakk>G ?\<psi> \<in> \<G>; ?i \<le> j\<rbrakk> \<Longrightarrow> S \<Turnstile>\<^sub>P eval\<^sub>G \<G> (af\<^sub>G ?\<psi> (w [?i \<rightarrow> j]))

goal (1 subgoal):
 1. S \<Turnstile>\<^sub>P af \<phi> (prefix j w)
[PROOF STEP]
by force


[STATEMENT]
lemma af_ltl_continuation:
  "(w \<frown> w') \<Turnstile> \<phi> \<longleftrightarrow> w' \<Turnstile> af \<phi> w"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (w \<frown> w') \<Turnstile> \<phi> = w' \<Turnstile> af \<phi> w
[PROOF STEP]
proof (induction w arbitrary: \<phi> w')
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>\<phi> w'. ([] \<frown> w') \<Turnstile> \<phi> = w' \<Turnstile> af \<phi> []
 2. \<And>a w \<phi> w'. (\<And>\<phi> w'. (w \<frown> w') \<Turnstile> \<phi> = w' \<Turnstile> af \<phi> w) \<Longrightarrow> ((a # w) \<frown> w') \<Turnstile> \<phi> = w' \<Turnstile> af \<phi> (a # w)
[PROOF STEP]
case (Cons x xs)
[PROOF STATE]
proof (state)
this:
(xs \<frown> ?w') \<Turnstile> ?\<phi> = ?w' \<Turnstile> af ?\<phi> xs

goal (2 subgoals):
 1. \<And>\<phi> w'. ([] \<frown> w') \<Turnstile> \<phi> = w' \<Turnstile> af \<phi> []
 2. \<And>a w \<phi> w'. (\<And>\<phi> w'. (w \<frown> w') \<Turnstile> \<phi> = w' \<Turnstile> af \<phi> w) \<Longrightarrow> ((a # w) \<frown> w') \<Turnstile> \<phi> = w' \<Turnstile> af \<phi> (a # w)
[PROOF STEP]
have "((x # xs) \<frown> w') 0 = x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((x # xs) \<frown> w') 0 = x
[PROOF STEP]
unfolding conc_def nth_Cons_0
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (if 0 < length (x # xs) then x else w' (0 - length (x # xs))) = x
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
((x # xs) \<frown> w') 0 = x

goal (2 subgoals):
 1. \<And>\<phi> w'. ([] \<frown> w') \<Turnstile> \<phi> = w' \<Turnstile> af \<phi> []
 2. \<And>a w \<phi> w'. (\<And>\<phi> w'. (w \<frown> w') \<Turnstile> \<phi> = w' \<Turnstile> af \<phi> w) \<Longrightarrow> ((a # w) \<frown> w') \<Turnstile> \<phi> = w' \<Turnstile> af \<phi> (a # w)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
((x # xs) \<frown> w') 0 = x

goal (2 subgoals):
 1. \<And>\<phi> w'. ([] \<frown> w') \<Turnstile> \<phi> = w' \<Turnstile> af \<phi> []
 2. \<And>a w \<phi> w'. (\<And>\<phi> w'. (w \<frown> w') \<Turnstile> \<phi> = w' \<Turnstile> af \<phi> w) \<Longrightarrow> ((a # w) \<frown> w') \<Turnstile> \<phi> = w' \<Turnstile> af \<phi> (a # w)
[PROOF STEP]
have "suffix 1 ((x # xs) \<frown> w') = xs \<frown> w'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. suffix 1 ((x # xs) \<frown> w') = xs \<frown> w'
[PROOF STEP]
unfolding suffix_def conc_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>n. if 1 + n < length (x # xs) then (x # xs) ! (1 + n) else w' (1 + n - length (x # xs))) = (\<lambda>n. if n < length xs then xs ! n else w' (n - length xs))
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
suffix 1 ((x # xs) \<frown> w') = xs \<frown> w'

goal (2 subgoals):
 1. \<And>\<phi> w'. ([] \<frown> w') \<Turnstile> \<phi> = w' \<Turnstile> af \<phi> []
 2. \<And>a w \<phi> w'. (\<And>\<phi> w'. (w \<frown> w') \<Turnstile> \<phi> = w' \<Turnstile> af \<phi> w) \<Longrightarrow> ((a # w) \<frown> w') \<Turnstile> \<phi> = w' \<Turnstile> af \<phi> (a # w)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
suffix 1 ((x # xs) \<frown> w') = xs \<frown> w'

goal (2 subgoals):
 1. \<And>\<phi> w'. ([] \<frown> w') \<Turnstile> \<phi> = w' \<Turnstile> af \<phi> []
 2. \<And>a w \<phi> w'. (\<And>\<phi> w'. (w \<frown> w') \<Turnstile> \<phi> = w' \<Turnstile> af \<phi> w) \<Longrightarrow> ((a # w) \<frown> w') \<Turnstile> \<phi> = w' \<Turnstile> af \<phi> (a # w)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
suffix 1 ((x # xs) \<frown> w') = xs \<frown> w'

goal (2 subgoals):
 1. \<And>\<phi> w'. ([] \<frown> w') \<Turnstile> \<phi> = w' \<Turnstile> af \<phi> []
 2. \<And>a w \<phi> w'. (\<And>\<phi> w'. (w \<frown> w') \<Turnstile> \<phi> = w' \<Turnstile> af \<phi> w) \<Longrightarrow> ((a # w) \<frown> w') \<Turnstile> \<phi> = w' \<Turnstile> af \<phi> (a # w)
[PROOF STEP]
fix \<phi> :: "'a ltl"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>\<phi> w'. ([] \<frown> w') \<Turnstile> \<phi> = w' \<Turnstile> af \<phi> []
 2. \<And>a w \<phi> w'. (\<And>\<phi> w'. (w \<frown> w') \<Turnstile> \<phi> = w' \<Turnstile> af \<phi> w) \<Longrightarrow> ((a # w) \<frown> w') \<Turnstile> \<phi> = w' \<Turnstile> af \<phi> (a # w)
[PROOF STEP]
have "\<And>w. w \<Turnstile> \<phi> \<longleftrightarrow> suffix 1 w \<Turnstile> af_letter \<phi> (w 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>w. w \<Turnstile> \<phi> = suffix 1 w \<Turnstile> af_letter \<phi> (w 0)
[PROOF STEP]
by (induction \<phi>) ((unfold LTL_F_one_step_unfolding LTL_G_one_step_unfolding LTL_U_one_step_unfolding)?, auto)
[PROOF STATE]
proof (state)
this:
?w \<Turnstile> \<phi> = suffix 1 ?w \<Turnstile> af_letter \<phi> (?w 0)

goal (2 subgoals):
 1. \<And>\<phi> w'. ([] \<frown> w') \<Turnstile> \<phi> = w' \<Turnstile> af \<phi> []
 2. \<And>a w \<phi> w'. (\<And>\<phi> w'. (w \<frown> w') \<Turnstile> \<phi> = w' \<Turnstile> af \<phi> w) \<Longrightarrow> ((a # w) \<frown> w') \<Turnstile> \<phi> = w' \<Turnstile> af \<phi> (a # w)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?w \<Turnstile> ?\<phi>''3 = suffix 1 ?w \<Turnstile> af_letter ?\<phi>''3 (?w 0)

goal (2 subgoals):
 1. \<And>\<phi> w'. ([] \<frown> w') \<Turnstile> \<phi> = w' \<Turnstile> af \<phi> []
 2. \<And>a w \<phi> w'. (\<And>\<phi> w'. (w \<frown> w') \<Turnstile> \<phi> = w' \<Turnstile> af \<phi> w) \<Longrightarrow> ((a # w) \<frown> w') \<Turnstile> \<phi> = w' \<Turnstile> af \<phi> (a # w)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
((x # xs) \<frown> w') 0 = x
suffix 1 ((x # xs) \<frown> w') = xs \<frown> w'
?w \<Turnstile> ?\<phi>''3 = suffix 1 ?w \<Turnstile> af_letter ?\<phi>''3 (?w 0)
[PROOF STEP]
have "((x # xs) \<frown> w') \<Turnstile> \<phi> \<longleftrightarrow> (xs \<frown> w') \<Turnstile> af_letter \<phi> x"
[PROOF STATE]
proof (prove)
using this:
((x # xs) \<frown> w') 0 = x
suffix 1 ((x # xs) \<frown> w') = xs \<frown> w'
?w \<Turnstile> ?\<phi>''3 = suffix 1 ?w \<Turnstile> af_letter ?\<phi>''3 (?w 0)

goal (1 subgoal):
 1. ((x # xs) \<frown> w') \<Turnstile> \<phi> = (xs \<frown> w') \<Turnstile> af_letter \<phi> x
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
((x # xs) \<frown> w') \<Turnstile> \<phi> = (xs \<frown> w') \<Turnstile> af_letter \<phi> x

goal (2 subgoals):
 1. \<And>\<phi> w'. ([] \<frown> w') \<Turnstile> \<phi> = w' \<Turnstile> af \<phi> []
 2. \<And>a w \<phi> w'. (\<And>\<phi> w'. (w \<frown> w') \<Turnstile> \<phi> = w' \<Turnstile> af \<phi> w) \<Longrightarrow> ((a # w) \<frown> w') \<Turnstile> \<phi> = w' \<Turnstile> af \<phi> (a # w)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
((x # xs) \<frown> w') \<Turnstile> \<phi> = (xs \<frown> w') \<Turnstile> af_letter \<phi> x

goal (2 subgoals):
 1. \<And>\<phi> w'. ([] \<frown> w') \<Turnstile> \<phi> = w' \<Turnstile> af \<phi> []
 2. \<And>a w \<phi> w'. (\<And>\<phi> w'. (w \<frown> w') \<Turnstile> \<phi> = w' \<Turnstile> af \<phi> w) \<Longrightarrow> ((a # w) \<frown> w') \<Turnstile> \<phi> = w' \<Turnstile> af \<phi> (a # w)
[PROOF STEP]
have "\<dots> \<longleftrightarrow> w' \<Turnstile> af \<phi> (x#xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (xs \<frown> w') \<Turnstile> af_letter \<phi> x = w' \<Turnstile> af \<phi> (x # xs)
[PROOF STEP]
using Cons.IH
[PROOF STATE]
proof (prove)
using this:
(xs \<frown> ?w') \<Turnstile> ?\<phi> = ?w' \<Turnstile> af ?\<phi> xs

goal (1 subgoal):
 1. (xs \<frown> w') \<Turnstile> af_letter \<phi> x = w' \<Turnstile> af \<phi> (x # xs)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(xs \<frown> w') \<Turnstile> af_letter \<phi> x = w' \<Turnstile> af \<phi> (x # xs)

goal (2 subgoals):
 1. \<And>\<phi> w'. ([] \<frown> w') \<Turnstile> \<phi> = w' \<Turnstile> af \<phi> []
 2. \<And>a w \<phi> w'. (\<And>\<phi> w'. (w \<frown> w') \<Turnstile> \<phi> = w' \<Turnstile> af \<phi> w) \<Longrightarrow> ((a # w) \<frown> w') \<Turnstile> \<phi> = w' \<Turnstile> af \<phi> (a # w)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
((x # xs) \<frown> w') \<Turnstile> \<phi> = w' \<Turnstile> af \<phi> (x # xs)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
((x # xs) \<frown> w') \<Turnstile> \<phi> = w' \<Turnstile> af \<phi> (x # xs)

goal (1 subgoal):
 1. ((x # xs) \<frown> w') \<Turnstile> \<phi> = w' \<Turnstile> af \<phi> (x # xs)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
((x # xs) \<frown> w') \<Turnstile> \<phi> = w' \<Turnstile> af \<phi> (x # xs)

goal (1 subgoal):
 1. \<And>\<phi> w'. ([] \<frown> w') \<Turnstile> \<phi> = w' \<Turnstile> af \<phi> []
[PROOF STEP]
qed simp


[STATEMENT]
lemma af_ltl_continuation_suffix:
  "w \<Turnstile> \<phi> \<longleftrightarrow> suffix i w \<Turnstile> af \<phi> (w[0 \<rightarrow> i])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. w \<Turnstile> \<phi> = suffix i w \<Turnstile> af \<phi> (prefix i w)
[PROOF STEP]
using af_ltl_continuation prefix_suffix subsequence_def
[PROOF STATE]
proof (prove)
using this:
(?w \<frown> ?w') \<Turnstile> ?\<phi> = ?w' \<Turnstile> af ?\<phi> ?w
?x = prefix ?n ?x \<frown> suffix ?n ?x
?w [?i \<rightarrow> ?j] \<equiv> map ?w [?i..<?j]

goal (1 subgoal):
 1. w \<Turnstile> \<phi> = suffix i w \<Turnstile> af \<phi> (prefix i w)
[PROOF STEP]
by metis


[STATEMENT]
lemma af_G_ltl_continuation:
  "\<forall>\<psi> \<in> \<^bold>G \<phi>. w' \<Turnstile> \<psi> = (w \<frown> w') \<Turnstile> \<psi> \<Longrightarrow> (w \<frown> w') \<Turnstile> \<phi> \<longleftrightarrow> w' \<Turnstile> af\<^sub>G \<phi> w"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>\<psi>\<in>\<^bold>G \<phi>. w' \<Turnstile> \<psi> = (w \<frown> w') \<Turnstile> \<psi> \<Longrightarrow> (w \<frown> w') \<Turnstile> \<phi> = w' \<Turnstile> af\<^sub>G \<phi> w
[PROOF STEP]
proof (induction w arbitrary: w' \<phi>)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>w' \<phi>. \<forall>\<psi>\<in>\<^bold>G \<phi>. w' \<Turnstile> \<psi> = ([] \<frown> w') \<Turnstile> \<psi> \<Longrightarrow> ([] \<frown> w') \<Turnstile> \<phi> = w' \<Turnstile> af\<^sub>G \<phi> []
 2. \<And>a w w' \<phi>. \<lbrakk>\<And>w' \<phi>. \<forall>\<psi>\<in>\<^bold>G \<phi>. w' \<Turnstile> \<psi> = (w \<frown> w') \<Turnstile> \<psi> \<Longrightarrow> (w \<frown> w') \<Turnstile> \<phi> = w' \<Turnstile> af\<^sub>G \<phi> w; \<forall>\<psi>\<in>\<^bold>G \<phi>. w' \<Turnstile> \<psi> = ((a # w) \<frown> w') \<Turnstile> \<psi>\<rbrakk> \<Longrightarrow> ((a # w) \<frown> w') \<Turnstile> \<phi> = w' \<Turnstile> af\<^sub>G \<phi> (a # w)
[PROOF STEP]
case (Cons x xs)
[PROOF STATE]
proof (state)
this:
\<forall>\<psi>\<in>\<^bold>G ?\<phi>. ?w' \<Turnstile> \<psi> = (xs \<frown> ?w') \<Turnstile> \<psi> \<Longrightarrow> (xs \<frown> ?w') \<Turnstile> ?\<phi> = ?w' \<Turnstile> af\<^sub>G ?\<phi> xs
\<forall>\<psi>\<in>\<^bold>G \<phi>. w' \<Turnstile> \<psi> = ((x # xs) \<frown> w') \<Turnstile> \<psi>

goal (2 subgoals):
 1. \<And>w' \<phi>. \<forall>\<psi>\<in>\<^bold>G \<phi>. w' \<Turnstile> \<psi> = ([] \<frown> w') \<Turnstile> \<psi> \<Longrightarrow> ([] \<frown> w') \<Turnstile> \<phi> = w' \<Turnstile> af\<^sub>G \<phi> []
 2. \<And>a w w' \<phi>. \<lbrakk>\<And>w' \<phi>. \<forall>\<psi>\<in>\<^bold>G \<phi>. w' \<Turnstile> \<psi> = (w \<frown> w') \<Turnstile> \<psi> \<Longrightarrow> (w \<frown> w') \<Turnstile> \<phi> = w' \<Turnstile> af\<^sub>G \<phi> w; \<forall>\<psi>\<in>\<^bold>G \<phi>. w' \<Turnstile> \<psi> = ((a # w) \<frown> w') \<Turnstile> \<psi>\<rbrakk> \<Longrightarrow> ((a # w) \<frown> w') \<Turnstile> \<phi> = w' \<Turnstile> af\<^sub>G \<phi> (a # w)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
\<forall>\<psi>\<in>\<^bold>G ?\<phi>. ?w' \<Turnstile> \<psi> = (xs \<frown> ?w') \<Turnstile> \<psi> \<Longrightarrow> (xs \<frown> ?w') \<Turnstile> ?\<phi> = ?w' \<Turnstile> af\<^sub>G ?\<phi> xs
\<forall>\<psi>\<in>\<^bold>G \<phi>. w' \<Turnstile> \<psi> = ((x # xs) \<frown> w') \<Turnstile> \<psi>

goal (2 subgoals):
 1. \<And>w' \<phi>. \<forall>\<psi>\<in>\<^bold>G \<phi>. w' \<Turnstile> \<psi> = ([] \<frown> w') \<Turnstile> \<psi> \<Longrightarrow> ([] \<frown> w') \<Turnstile> \<phi> = w' \<Turnstile> af\<^sub>G \<phi> []
 2. \<And>a w w' \<phi>. \<lbrakk>\<And>w' \<phi>. \<forall>\<psi>\<in>\<^bold>G \<phi>. w' \<Turnstile> \<psi> = (w \<frown> w') \<Turnstile> \<psi> \<Longrightarrow> (w \<frown> w') \<Turnstile> \<phi> = w' \<Turnstile> af\<^sub>G \<phi> w; \<forall>\<psi>\<in>\<^bold>G \<phi>. w' \<Turnstile> \<psi> = ((a # w) \<frown> w') \<Turnstile> \<psi>\<rbrakk> \<Longrightarrow> ((a # w) \<frown> w') \<Turnstile> \<phi> = w' \<Turnstile> af\<^sub>G \<phi> (a # w)
[PROOF STEP]
fix \<psi> :: "'a ltl"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>w' \<phi>. \<forall>\<psi>\<in>\<^bold>G \<phi>. w' \<Turnstile> \<psi> = ([] \<frown> w') \<Turnstile> \<psi> \<Longrightarrow> ([] \<frown> w') \<Turnstile> \<phi> = w' \<Turnstile> af\<^sub>G \<phi> []
 2. \<And>a w w' \<phi>. \<lbrakk>\<And>w' \<phi>. \<forall>\<psi>\<in>\<^bold>G \<phi>. w' \<Turnstile> \<psi> = (w \<frown> w') \<Turnstile> \<psi> \<Longrightarrow> (w \<frown> w') \<Turnstile> \<phi> = w' \<Turnstile> af\<^sub>G \<phi> w; \<forall>\<psi>\<in>\<^bold>G \<phi>. w' \<Turnstile> \<psi> = ((a # w) \<frown> w') \<Turnstile> \<psi>\<rbrakk> \<Longrightarrow> ((a # w) \<frown> w') \<Turnstile> \<phi> = w' \<Turnstile> af\<^sub>G \<phi> (a # w)
[PROOF STEP]
fix  w w' w''
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>w' \<phi>. \<forall>\<psi>\<in>\<^bold>G \<phi>. w' \<Turnstile> \<psi> = ([] \<frown> w') \<Turnstile> \<psi> \<Longrightarrow> ([] \<frown> w') \<Turnstile> \<phi> = w' \<Turnstile> af\<^sub>G \<phi> []
 2. \<And>a w w' \<phi>. \<lbrakk>\<And>w' \<phi>. \<forall>\<psi>\<in>\<^bold>G \<phi>. w' \<Turnstile> \<psi> = (w \<frown> w') \<Turnstile> \<psi> \<Longrightarrow> (w \<frown> w') \<Turnstile> \<phi> = w' \<Turnstile> af\<^sub>G \<phi> w; \<forall>\<psi>\<in>\<^bold>G \<phi>. w' \<Turnstile> \<psi> = ((a # w) \<frown> w') \<Turnstile> \<psi>\<rbrakk> \<Longrightarrow> ((a # w) \<frown> w') \<Turnstile> \<phi> = w' \<Turnstile> af\<^sub>G \<phi> (a # w)
[PROOF STEP]
assume "w'' \<Turnstile> G \<psi> = ((w @ w') \<frown> w'') \<Turnstile> G \<psi>"
[PROOF STATE]
proof (state)
this:
w'' \<Turnstile> G \<psi> = ((w @ w') \<frown> w'') \<Turnstile> G \<psi>

goal (2 subgoals):
 1. \<And>w' \<phi>. \<forall>\<psi>\<in>\<^bold>G \<phi>. w' \<Turnstile> \<psi> = ([] \<frown> w') \<Turnstile> \<psi> \<Longrightarrow> ([] \<frown> w') \<Turnstile> \<phi> = w' \<Turnstile> af\<^sub>G \<phi> []
 2. \<And>a w w' \<phi>. \<lbrakk>\<And>w' \<phi>. \<forall>\<psi>\<in>\<^bold>G \<phi>. w' \<Turnstile> \<psi> = (w \<frown> w') \<Turnstile> \<psi> \<Longrightarrow> (w \<frown> w') \<Turnstile> \<phi> = w' \<Turnstile> af\<^sub>G \<phi> w; \<forall>\<psi>\<in>\<^bold>G \<phi>. w' \<Turnstile> \<psi> = ((a # w) \<frown> w') \<Turnstile> \<psi>\<rbrakk> \<Longrightarrow> ((a # w) \<frown> w') \<Turnstile> \<phi> = w' \<Turnstile> af\<^sub>G \<phi> (a # w)
[PROOF STEP]
hence "w'' \<Turnstile> G \<psi> = (w' \<frown>  w'') \<Turnstile> G \<psi>" and "(w' \<frown> w'') \<Turnstile> G \<psi> = ((w @ w') \<frown> w'') \<Turnstile> G \<psi>"
[PROOF STATE]
proof (prove)
using this:
w'' \<Turnstile> G \<psi> = ((w @ w') \<frown> w'') \<Turnstile> G \<psi>

goal (1 subgoal):
 1. w'' \<Turnstile> G \<psi> = (w' \<frown> w'') \<Turnstile> G \<psi> &&& (w' \<frown> w'') \<Turnstile> G \<psi> = ((w @ w') \<frown> w'') \<Turnstile> G \<psi>
[PROOF STEP]
by (induction w' arbitrary: w) (metis LTL_suffix_G suffix_conc_length conc_conc)+
[PROOF STATE]
proof (state)
this:
w'' \<Turnstile> G \<psi> = (w' \<frown> w'') \<Turnstile> G \<psi>
(w' \<frown> w'') \<Turnstile> G \<psi> = ((w @ w') \<frown> w'') \<Turnstile> G \<psi>

goal (2 subgoals):
 1. \<And>w' \<phi>. \<forall>\<psi>\<in>\<^bold>G \<phi>. w' \<Turnstile> \<psi> = ([] \<frown> w') \<Turnstile> \<psi> \<Longrightarrow> ([] \<frown> w') \<Turnstile> \<phi> = w' \<Turnstile> af\<^sub>G \<phi> []
 2. \<And>a w w' \<phi>. \<lbrakk>\<And>w' \<phi>. \<forall>\<psi>\<in>\<^bold>G \<phi>. w' \<Turnstile> \<psi> = (w \<frown> w') \<Turnstile> \<psi> \<Longrightarrow> (w \<frown> w') \<Turnstile> \<phi> = w' \<Turnstile> af\<^sub>G \<phi> w; \<forall>\<psi>\<in>\<^bold>G \<phi>. w' \<Turnstile> \<psi> = ((a # w) \<frown> w') \<Turnstile> \<psi>\<rbrakk> \<Longrightarrow> ((a # w) \<frown> w') \<Turnstile> \<phi> = w' \<Turnstile> af\<^sub>G \<phi> (a # w)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?w''2 \<Turnstile> G ?\<psi>2 = ((?wa2 @ ?w'b2) \<frown> ?w''2) \<Turnstile> G ?\<psi>2 \<Longrightarrow> ?w''2 \<Turnstile> G ?\<psi>2 = (?w'b2 \<frown> ?w''2) \<Turnstile> G ?\<psi>2
?w''2 \<Turnstile> G ?\<psi>2 = ((?wa2 @ ?w'b2) \<frown> ?w''2) \<Turnstile> G ?\<psi>2 \<Longrightarrow> (?w'b2 \<frown> ?w''2) \<Turnstile> G ?\<psi>2 = ((?wa2 @ ?w'b2) \<frown> ?w''2) \<Turnstile> G ?\<psi>2

goal (2 subgoals):
 1. \<And>w' \<phi>. \<forall>\<psi>\<in>\<^bold>G \<phi>. w' \<Turnstile> \<psi> = ([] \<frown> w') \<Turnstile> \<psi> \<Longrightarrow> ([] \<frown> w') \<Turnstile> \<phi> = w' \<Turnstile> af\<^sub>G \<phi> []
 2. \<And>a w w' \<phi>. \<lbrakk>\<And>w' \<phi>. \<forall>\<psi>\<in>\<^bold>G \<phi>. w' \<Turnstile> \<psi> = (w \<frown> w') \<Turnstile> \<psi> \<Longrightarrow> (w \<frown> w') \<Turnstile> \<phi> = w' \<Turnstile> af\<^sub>G \<phi> w; \<forall>\<psi>\<in>\<^bold>G \<phi>. w' \<Turnstile> \<psi> = ((a # w) \<frown> w') \<Turnstile> \<psi>\<rbrakk> \<Longrightarrow> ((a # w) \<frown> w') \<Turnstile> \<phi> = w' \<Turnstile> af\<^sub>G \<phi> (a # w)
[PROOF STEP]
note G_stable = this
[PROOF STATE]
proof (state)
this:
?w''2 \<Turnstile> G ?\<psi>2 = ((?wa2 @ ?w'b2) \<frown> ?w''2) \<Turnstile> G ?\<psi>2 \<Longrightarrow> ?w''2 \<Turnstile> G ?\<psi>2 = (?w'b2 \<frown> ?w''2) \<Turnstile> G ?\<psi>2
?w''2 \<Turnstile> G ?\<psi>2 = ((?wa2 @ ?w'b2) \<frown> ?w''2) \<Turnstile> G ?\<psi>2 \<Longrightarrow> (?w'b2 \<frown> ?w''2) \<Turnstile> G ?\<psi>2 = ((?wa2 @ ?w'b2) \<frown> ?w''2) \<Turnstile> G ?\<psi>2

goal (2 subgoals):
 1. \<And>w' \<phi>. \<forall>\<psi>\<in>\<^bold>G \<phi>. w' \<Turnstile> \<psi> = ([] \<frown> w') \<Turnstile> \<psi> \<Longrightarrow> ([] \<frown> w') \<Turnstile> \<phi> = w' \<Turnstile> af\<^sub>G \<phi> []
 2. \<And>a w w' \<phi>. \<lbrakk>\<And>w' \<phi>. \<forall>\<psi>\<in>\<^bold>G \<phi>. w' \<Turnstile> \<psi> = (w \<frown> w') \<Turnstile> \<psi> \<Longrightarrow> (w \<frown> w') \<Turnstile> \<phi> = w' \<Turnstile> af\<^sub>G \<phi> w; \<forall>\<psi>\<in>\<^bold>G \<phi>. w' \<Turnstile> \<psi> = ((a # w) \<frown> w') \<Turnstile> \<psi>\<rbrakk> \<Longrightarrow> ((a # w) \<frown> w') \<Turnstile> \<phi> = w' \<Turnstile> af\<^sub>G \<phi> (a # w)
[PROOF STEP]
have A: "\<forall>\<psi>\<in>\<^bold>G (af\<^sub>G \<phi> [x]). w' \<Turnstile> \<psi> = (xs \<frown> w') \<Turnstile> \<psi>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>\<psi>\<in>\<^bold>G (af\<^sub>G \<phi> [x]). w' \<Turnstile> \<psi> = (xs \<frown> w') \<Turnstile> \<psi>
[PROOF STEP]
using G_stable(1)[of w' _ "[x]"] Cons.prems
[PROOF STATE]
proof (prove)
using this:
w' \<Turnstile> G ?\<psi>2 = (([x] @ ?w'b2) \<frown> w') \<Turnstile> G ?\<psi>2 \<Longrightarrow> w' \<Turnstile> G ?\<psi>2 = (?w'b2 \<frown> w') \<Turnstile> G ?\<psi>2
\<forall>\<psi>\<in>\<^bold>G \<phi>. w' \<Turnstile> \<psi> = ((x # xs) \<frown> w') \<Turnstile> \<psi>

goal (1 subgoal):
 1. \<forall>\<psi>\<in>\<^bold>G (af\<^sub>G \<phi> [x]). w' \<Turnstile> \<psi> = (xs \<frown> w') \<Turnstile> \<psi>
[PROOF STEP]
unfolding G_af\<^sub>G_simp conc_conc append.simps
[PROOF STATE]
proof (prove)
using this:
w' \<Turnstile> G ?\<psi>2 = ((x # ?w'b2) \<frown> w') \<Turnstile> G ?\<psi>2 \<Longrightarrow> w' \<Turnstile> G ?\<psi>2 = (?w'b2 \<frown> w') \<Turnstile> G ?\<psi>2
\<forall>\<psi>\<in>\<^bold>G \<phi>. w' \<Turnstile> \<psi> = ((x # xs) \<frown> w') \<Turnstile> \<psi>

goal (1 subgoal):
 1. \<forall>\<psi>\<in>\<^bold>G \<phi>. w' \<Turnstile> \<psi> = (xs \<frown> w') \<Turnstile> \<psi>
[PROOF STEP]
unfolding G_nested_propos_alt_def
[PROOF STATE]
proof (prove)
using this:
w' \<Turnstile> G ?\<psi>2 = ((x # ?w'b2) \<frown> w') \<Turnstile> G ?\<psi>2 \<Longrightarrow> w' \<Turnstile> G ?\<psi>2 = (?w'b2 \<frown> w') \<Turnstile> G ?\<psi>2
\<forall>\<psi>\<in>nested_propos \<phi> \<inter> {\<psi>. \<exists>x. \<psi> = G x}. w' \<Turnstile> \<psi> = ((x # xs) \<frown> w') \<Turnstile> \<psi>

goal (1 subgoal):
 1. \<forall>\<psi>\<in>nested_propos \<phi> \<inter> {\<psi>. \<exists>x. \<psi> = G x}. w' \<Turnstile> \<psi> = (xs \<frown> w') \<Turnstile> \<psi>
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<forall>\<psi>\<in>\<^bold>G (af\<^sub>G \<phi> [x]). w' \<Turnstile> \<psi> = (xs \<frown> w') \<Turnstile> \<psi>

goal (2 subgoals):
 1. \<And>w' \<phi>. \<forall>\<psi>\<in>\<^bold>G \<phi>. w' \<Turnstile> \<psi> = ([] \<frown> w') \<Turnstile> \<psi> \<Longrightarrow> ([] \<frown> w') \<Turnstile> \<phi> = w' \<Turnstile> af\<^sub>G \<phi> []
 2. \<And>a w w' \<phi>. \<lbrakk>\<And>w' \<phi>. \<forall>\<psi>\<in>\<^bold>G \<phi>. w' \<Turnstile> \<psi> = (w \<frown> w') \<Turnstile> \<psi> \<Longrightarrow> (w \<frown> w') \<Turnstile> \<phi> = w' \<Turnstile> af\<^sub>G \<phi> w; \<forall>\<psi>\<in>\<^bold>G \<phi>. w' \<Turnstile> \<psi> = ((a # w) \<frown> w') \<Turnstile> \<psi>\<rbrakk> \<Longrightarrow> ((a # w) \<frown> w') \<Turnstile> \<phi> = w' \<Turnstile> af\<^sub>G \<phi> (a # w)
[PROOF STEP]
have B: "\<forall>\<psi>\<in>\<^bold>G \<phi>. ([x] \<frown> xs \<frown> w') \<Turnstile> \<psi> = (xs \<frown> w') \<Turnstile> \<psi>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>\<psi>\<in>\<^bold>G \<phi>. ([x] \<frown> xs \<frown> w') \<Turnstile> \<psi> = (xs \<frown> w') \<Turnstile> \<psi>
[PROOF STEP]
using G_stable(2)[of w' _ "[x]"] Cons.prems
[PROOF STATE]
proof (prove)
using this:
w' \<Turnstile> G ?\<psi>2 = (([x] @ ?w'b2) \<frown> w') \<Turnstile> G ?\<psi>2 \<Longrightarrow> (?w'b2 \<frown> w') \<Turnstile> G ?\<psi>2 = (([x] @ ?w'b2) \<frown> w') \<Turnstile> G ?\<psi>2
\<forall>\<psi>\<in>\<^bold>G \<phi>. w' \<Turnstile> \<psi> = ((x # xs) \<frown> w') \<Turnstile> \<psi>

goal (1 subgoal):
 1. \<forall>\<psi>\<in>\<^bold>G \<phi>. ([x] \<frown> xs \<frown> w') \<Turnstile> \<psi> = (xs \<frown> w') \<Turnstile> \<psi>
[PROOF STEP]
unfolding conc_conc append.simps
[PROOF STATE]
proof (prove)
using this:
w' \<Turnstile> G ?\<psi>2 = ((x # ?w'b2) \<frown> w') \<Turnstile> G ?\<psi>2 \<Longrightarrow> (?w'b2 \<frown> w') \<Turnstile> G ?\<psi>2 = ((x # ?w'b2) \<frown> w') \<Turnstile> G ?\<psi>2
\<forall>\<psi>\<in>\<^bold>G \<phi>. w' \<Turnstile> \<psi> = ((x # xs) \<frown> w') \<Turnstile> \<psi>

goal (1 subgoal):
 1. \<forall>\<psi>\<in>\<^bold>G \<phi>. ((x # xs) \<frown> w') \<Turnstile> \<psi> = (xs \<frown> w') \<Turnstile> \<psi>
[PROOF STEP]
unfolding G_nested_propos_alt_def
[PROOF STATE]
proof (prove)
using this:
w' \<Turnstile> G ?\<psi>2 = ((x # ?w'b2) \<frown> w') \<Turnstile> G ?\<psi>2 \<Longrightarrow> (?w'b2 \<frown> w') \<Turnstile> G ?\<psi>2 = ((x # ?w'b2) \<frown> w') \<Turnstile> G ?\<psi>2
\<forall>\<psi>\<in>nested_propos \<phi> \<inter> {\<psi>. \<exists>x. \<psi> = G x}. w' \<Turnstile> \<psi> = ((x # xs) \<frown> w') \<Turnstile> \<psi>

goal (1 subgoal):
 1. \<forall>\<psi>\<in>nested_propos \<phi> \<inter> {\<psi>. \<exists>x. \<psi> = G x}. ((x # xs) \<frown> w') \<Turnstile> \<psi> = (xs \<frown> w') \<Turnstile> \<psi>
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<forall>\<psi>\<in>\<^bold>G \<phi>. ([x] \<frown> xs \<frown> w') \<Turnstile> \<psi> = (xs \<frown> w') \<Turnstile> \<psi>

goal (2 subgoals):
 1. \<And>w' \<phi>. \<forall>\<psi>\<in>\<^bold>G \<phi>. w' \<Turnstile> \<psi> = ([] \<frown> w') \<Turnstile> \<psi> \<Longrightarrow> ([] \<frown> w') \<Turnstile> \<phi> = w' \<Turnstile> af\<^sub>G \<phi> []
 2. \<And>a w w' \<phi>. \<lbrakk>\<And>w' \<phi>. \<forall>\<psi>\<in>\<^bold>G \<phi>. w' \<Turnstile> \<psi> = (w \<frown> w') \<Turnstile> \<psi> \<Longrightarrow> (w \<frown> w') \<Turnstile> \<phi> = w' \<Turnstile> af\<^sub>G \<phi> w; \<forall>\<psi>\<in>\<^bold>G \<phi>. w' \<Turnstile> \<psi> = ((a # w) \<frown> w') \<Turnstile> \<psi>\<rbrakk> \<Longrightarrow> ((a # w) \<frown> w') \<Turnstile> \<phi> = w' \<Turnstile> af\<^sub>G \<phi> (a # w)
[PROOF STEP]
hence "([x] \<frown> xs \<frown> w') \<Turnstile> \<phi> = (xs \<frown> w') \<Turnstile> af\<^sub>G \<phi> [x]"
[PROOF STATE]
proof (prove)
using this:
\<forall>\<psi>\<in>\<^bold>G \<phi>. ([x] \<frown> xs \<frown> w') \<Turnstile> \<psi> = (xs \<frown> w') \<Turnstile> \<psi>

goal (1 subgoal):
 1. ([x] \<frown> xs \<frown> w') \<Turnstile> \<phi> = (xs \<frown> w') \<Turnstile> af\<^sub>G \<phi> [x]
[PROOF STEP]
proof (induction \<phi>)
[PROOF STATE]
proof (state)
goal (10 subgoals):
 1. \<forall>\<psi>\<in>\<^bold>G true. ([x] \<frown> xs \<frown> w') \<Turnstile> \<psi> = (xs \<frown> w') \<Turnstile> \<psi> \<Longrightarrow> ([x] \<frown> xs \<frown> w') \<Turnstile> true = (xs \<frown> w') \<Turnstile> af\<^sub>G true [x]
 2. \<forall>\<psi>\<in>\<^bold>G false. ([x] \<frown> xs \<frown> w') \<Turnstile> \<psi> = (xs \<frown> w') \<Turnstile> \<psi> \<Longrightarrow> ([x] \<frown> xs \<frown> w') \<Turnstile> false = (xs \<frown> w') \<Turnstile> af\<^sub>G false [x]
 3. \<And>xa. \<forall>\<psi>\<in>\<^bold>G p(xa). ([x] \<frown> xs \<frown> w') \<Turnstile> \<psi> = (xs \<frown> w') \<Turnstile> \<psi> \<Longrightarrow> ([x] \<frown> xs \<frown> w') \<Turnstile> p(xa) = (xs \<frown> w') \<Turnstile> af\<^sub>G p(xa) [x]
 4. \<And>xa. \<forall>\<psi>\<in>\<^bold>G (np(xa)). ([x] \<frown> xs \<frown> w') \<Turnstile> \<psi> = (xs \<frown> w') \<Turnstile> \<psi> \<Longrightarrow> ([x] \<frown> xs \<frown> w') \<Turnstile> np(xa) = (xs \<frown> w') \<Turnstile> af\<^sub>G (np(xa)) [x]
 5. \<And>\<phi>1 \<phi>2. \<lbrakk>\<forall>\<psi>\<in>\<^bold>G \<phi>1. ([x] \<frown> xs \<frown> w') \<Turnstile> \<psi> = (xs \<frown> w') \<Turnstile> \<psi> \<Longrightarrow> ([x] \<frown> xs \<frown> w') \<Turnstile> \<phi>1 = (xs \<frown> w') \<Turnstile> af\<^sub>G \<phi>1 [x]; \<forall>\<psi>\<in>\<^bold>G \<phi>2. ([x] \<frown> xs \<frown> w') \<Turnstile> \<psi> = (xs \<frown> w') \<Turnstile> \<psi> \<Longrightarrow> ([x] \<frown> xs \<frown> w') \<Turnstile> \<phi>2 = (xs \<frown> w') \<Turnstile> af\<^sub>G \<phi>2 [x]; \<forall>\<psi>\<in>\<^bold>G (\<phi>1 and \<phi>2). ([x] \<frown> xs \<frown> w') \<Turnstile> \<psi> = (xs \<frown> w') \<Turnstile> \<psi>\<rbrakk> \<Longrightarrow> ([x] \<frown> xs \<frown> w') \<Turnstile> \<phi>1 and \<phi>2 = (xs \<frown> w') \<Turnstile> af\<^sub>G (\<phi>1 and \<phi>2) [x]
 6. \<And>\<phi>1 \<phi>2. \<lbrakk>\<forall>\<psi>\<in>\<^bold>G \<phi>1. ([x] \<frown> xs \<frown> w') \<Turnstile> \<psi> = (xs \<frown> w') \<Turnstile> \<psi> \<Longrightarrow> ([x] \<frown> xs \<frown> w') \<Turnstile> \<phi>1 = (xs \<frown> w') \<Turnstile> af\<^sub>G \<phi>1 [x]; \<forall>\<psi>\<in>\<^bold>G \<phi>2. ([x] \<frown> xs \<frown> w') \<Turnstile> \<psi> = (xs \<frown> w') \<Turnstile> \<psi> \<Longrightarrow> ([x] \<frown> xs \<frown> w') \<Turnstile> \<phi>2 = (xs \<frown> w') \<Turnstile> af\<^sub>G \<phi>2 [x]; \<forall>\<psi>\<in>\<^bold>G (\<phi>1 or \<phi>2). ([x] \<frown> xs \<frown> w') \<Turnstile> \<psi> = (xs \<frown> w') \<Turnstile> \<psi>\<rbrakk> \<Longrightarrow> ([x] \<frown> xs \<frown> w') \<Turnstile> \<phi>1 or \<phi>2 = (xs \<frown> w') \<Turnstile> af\<^sub>G (\<phi>1 or \<phi>2) [x]
 7. \<And>\<phi>. \<lbrakk>\<forall>\<psi>\<in>\<^bold>G \<phi>. ([x] \<frown> xs \<frown> w') \<Turnstile> \<psi> = (xs \<frown> w') \<Turnstile> \<psi> \<Longrightarrow> ([x] \<frown> xs \<frown> w') \<Turnstile> \<phi> = (xs \<frown> w') \<Turnstile> af\<^sub>G \<phi> [x]; \<forall>\<psi>\<in>\<^bold>G (X \<phi>). ([x] \<frown> xs \<frown> w') \<Turnstile> \<psi> = (xs \<frown> w') \<Turnstile> \<psi>\<rbrakk> \<Longrightarrow> ([x] \<frown> xs \<frown> w') \<Turnstile> X \<phi> = (xs \<frown> w') \<Turnstile> af\<^sub>G (X \<phi>) [x]
 8. \<And>\<phi>. \<lbrakk>\<forall>\<psi>\<in>\<^bold>G \<phi>. ([x] \<frown> xs \<frown> w') \<Turnstile> \<psi> = (xs \<frown> w') \<Turnstile> \<psi> \<Longrightarrow> ([x] \<frown> xs \<frown> w') \<Turnstile> \<phi> = (xs \<frown> w') \<Turnstile> af\<^sub>G \<phi> [x]; \<forall>\<psi>\<in>\<^bold>G (G \<phi>). ([x] \<frown> xs \<frown> w') \<Turnstile> \<psi> = (xs \<frown> w') \<Turnstile> \<psi>\<rbrakk> \<Longrightarrow> ([x] \<frown> xs \<frown> w') \<Turnstile> G \<phi> = (xs \<frown> w') \<Turnstile> af\<^sub>G (G \<phi>) [x]
 9. \<And>\<phi>. \<lbrakk>\<forall>\<psi>\<in>\<^bold>G \<phi>. ([x] \<frown> xs \<frown> w') \<Turnstile> \<psi> = (xs \<frown> w') \<Turnstile> \<psi> \<Longrightarrow> ([x] \<frown> xs \<frown> w') \<Turnstile> \<phi> = (xs \<frown> w') \<Turnstile> af\<^sub>G \<phi> [x]; \<forall>\<psi>\<in>\<^bold>G (F \<phi>). ([x] \<frown> xs \<frown> w') \<Turnstile> \<psi> = (xs \<frown> w') \<Turnstile> \<psi>\<rbrakk> \<Longrightarrow> ([x] \<frown> xs \<frown> w') \<Turnstile> F \<phi> = (xs \<frown> w') \<Turnstile> af\<^sub>G (F \<phi>) [x]
 10. \<And>\<phi>1 \<phi>2. \<lbrakk>\<forall>\<psi>\<in>\<^bold>G \<phi>1. ([x] \<frown> xs \<frown> w') \<Turnstile> \<psi> = (xs \<frown> w') \<Turnstile> \<psi> \<Longrightarrow> ([x] \<frown> xs \<frown> w') \<Turnstile> \<phi>1 = (xs \<frown> w') \<Turnstile> af\<^sub>G \<phi>1 [x]; \<forall>\<psi>\<in>\<^bold>G \<phi>2. ([x] \<frown> xs \<frown> w') \<Turnstile> \<psi> = (xs \<frown> w') \<Turnstile> \<psi> \<Longrightarrow> ([x] \<frown> xs \<frown> w') \<Turnstile> \<phi>2 = (xs \<frown> w') \<Turnstile> af\<^sub>G \<phi>2 [x]; \<forall>\<psi>\<in>\<^bold>G (\<phi>1 U \<phi>2). ([x] \<frown> xs \<frown> w') \<Turnstile> \<psi> = (xs \<frown> w') \<Turnstile> \<psi>\<rbrakk> \<Longrightarrow> ([x] \<frown> xs \<frown> w') \<Turnstile> \<phi>1 U \<phi>2 = (xs \<frown> w') \<Turnstile> af\<^sub>G (\<phi>1 U \<phi>2) [x]
[PROOF STEP]
case (LTLFinal \<phi>)
[PROOF STATE]
proof (state)
this:
\<forall>\<psi>\<in>\<^bold>G \<phi>. ([x] \<frown> xs \<frown> w') \<Turnstile> \<psi> = (xs \<frown> w') \<Turnstile> \<psi> \<Longrightarrow> ([x] \<frown> xs \<frown> w') \<Turnstile> \<phi> = (xs \<frown> w') \<Turnstile> af\<^sub>G \<phi> [x]
\<forall>\<psi>\<in>\<^bold>G (F \<phi>). ([x] \<frown> xs \<frown> w') \<Turnstile> \<psi> = (xs \<frown> w') \<Turnstile> \<psi>

goal (10 subgoals):
 1. \<forall>\<psi>\<in>\<^bold>G true. ([x] \<frown> xs \<frown> w') \<Turnstile> \<psi> = (xs \<frown> w') \<Turnstile> \<psi> \<Longrightarrow> ([x] \<frown> xs \<frown> w') \<Turnstile> true = (xs \<frown> w') \<Turnstile> af\<^sub>G true [x]
 2. \<forall>\<psi>\<in>\<^bold>G false. ([x] \<frown> xs \<frown> w') \<Turnstile> \<psi> = (xs \<frown> w') \<Turnstile> \<psi> \<Longrightarrow> ([x] \<frown> xs \<frown> w') \<Turnstile> false = (xs \<frown> w') \<Turnstile> af\<^sub>G false [x]
 3. \<And>xa. \<forall>\<psi>\<in>\<^bold>G p(xa). ([x] \<frown> xs \<frown> w') \<Turnstile> \<psi> = (xs \<frown> w') \<Turnstile> \<psi> \<Longrightarrow> ([x] \<frown> xs \<frown> w') \<Turnstile> p(xa) = (xs \<frown> w') \<Turnstile> af\<^sub>G p(xa) [x]
 4. \<And>xa. \<forall>\<psi>\<in>\<^bold>G (np(xa)). ([x] \<frown> xs \<frown> w') \<Turnstile> \<psi> = (xs \<frown> w') \<Turnstile> \<psi> \<Longrightarrow> ([x] \<frown> xs \<frown> w') \<Turnstile> np(xa) = (xs \<frown> w') \<Turnstile> af\<^sub>G (np(xa)) [x]
 5. \<And>\<phi>1 \<phi>2. \<lbrakk>\<forall>\<psi>\<in>\<^bold>G \<phi>1. ([x] \<frown> xs \<frown> w') \<Turnstile> \<psi> = (xs \<frown> w') \<Turnstile> \<psi> \<Longrightarrow> ([x] \<frown> xs \<frown> w') \<Turnstile> \<phi>1 = (xs \<frown> w') \<Turnstile> af\<^sub>G \<phi>1 [x]; \<forall>\<psi>\<in>\<^bold>G \<phi>2. ([x] \<frown> xs \<frown> w') \<Turnstile> \<psi> = (xs \<frown> w') \<Turnstile> \<psi> \<Longrightarrow> ([x] \<frown> xs \<frown> w') \<Turnstile> \<phi>2 = (xs \<frown> w') \<Turnstile> af\<^sub>G \<phi>2 [x]; \<forall>\<psi>\<in>\<^bold>G (\<phi>1 and \<phi>2). ([x] \<frown> xs \<frown> w') \<Turnstile> \<psi> = (xs \<frown> w') \<Turnstile> \<psi>\<rbrakk> \<Longrightarrow> ([x] \<frown> xs \<frown> w') \<Turnstile> \<phi>1 and \<phi>2 = (xs \<frown> w') \<Turnstile> af\<^sub>G (\<phi>1 and \<phi>2) [x]
 6. \<And>\<phi>1 \<phi>2. \<lbrakk>\<forall>\<psi>\<in>\<^bold>G \<phi>1. ([x] \<frown> xs \<frown> w') \<Turnstile> \<psi> = (xs \<frown> w') \<Turnstile> \<psi> \<Longrightarrow> ([x] \<frown> xs \<frown> w') \<Turnstile> \<phi>1 = (xs \<frown> w') \<Turnstile> af\<^sub>G \<phi>1 [x]; \<forall>\<psi>\<in>\<^bold>G \<phi>2. ([x] \<frown> xs \<frown> w') \<Turnstile> \<psi> = (xs \<frown> w') \<Turnstile> \<psi> \<Longrightarrow> ([x] \<frown> xs \<frown> w') \<Turnstile> \<phi>2 = (xs \<frown> w') \<Turnstile> af\<^sub>G \<phi>2 [x]; \<forall>\<psi>\<in>\<^bold>G (\<phi>1 or \<phi>2). ([x] \<frown> xs \<frown> w') \<Turnstile> \<psi> = (xs \<frown> w') \<Turnstile> \<psi>\<rbrakk> \<Longrightarrow> ([x] \<frown> xs \<frown> w') \<Turnstile> \<phi>1 or \<phi>2 = (xs \<frown> w') \<Turnstile> af\<^sub>G (\<phi>1 or \<phi>2) [x]
 7. \<And>\<phi>. \<lbrakk>\<forall>\<psi>\<in>\<^bold>G \<phi>. ([x] \<frown> xs \<frown> w') \<Turnstile> \<psi> = (xs \<frown> w') \<Turnstile> \<psi> \<Longrightarrow> ([x] \<frown> xs \<frown> w') \<Turnstile> \<phi> = (xs \<frown> w') \<Turnstile> af\<^sub>G \<phi> [x]; \<forall>\<psi>\<in>\<^bold>G (X \<phi>). ([x] \<frown> xs \<frown> w') \<Turnstile> \<psi> = (xs \<frown> w') \<Turnstile> \<psi>\<rbrakk> \<Longrightarrow> ([x] \<frown> xs \<frown> w') \<Turnstile> X \<phi> = (xs \<frown> w') \<Turnstile> af\<^sub>G (X \<phi>) [x]
 8. \<And>\<phi>. \<lbrakk>\<forall>\<psi>\<in>\<^bold>G \<phi>. ([x] \<frown> xs \<frown> w') \<Turnstile> \<psi> = (xs \<frown> w') \<Turnstile> \<psi> \<Longrightarrow> ([x] \<frown> xs \<frown> w') \<Turnstile> \<phi> = (xs \<frown> w') \<Turnstile> af\<^sub>G \<phi> [x]; \<forall>\<psi>\<in>\<^bold>G (G \<phi>). ([x] \<frown> xs \<frown> w') \<Turnstile> \<psi> = (xs \<frown> w') \<Turnstile> \<psi>\<rbrakk> \<Longrightarrow> ([x] \<frown> xs \<frown> w') \<Turnstile> G \<phi> = (xs \<frown> w') \<Turnstile> af\<^sub>G (G \<phi>) [x]
 9. \<And>\<phi>. \<lbrakk>\<forall>\<psi>\<in>\<^bold>G \<phi>. ([x] \<frown> xs \<frown> w') \<Turnstile> \<psi> = (xs \<frown> w') \<Turnstile> \<psi> \<Longrightarrow> ([x] \<frown> xs \<frown> w') \<Turnstile> \<phi> = (xs \<frown> w') \<Turnstile> af\<^sub>G \<phi> [x]; \<forall>\<psi>\<in>\<^bold>G (F \<phi>). ([x] \<frown> xs \<frown> w') \<Turnstile> \<psi> = (xs \<frown> w') \<Turnstile> \<psi>\<rbrakk> \<Longrightarrow> ([x] \<frown> xs \<frown> w') \<Turnstile> F \<phi> = (xs \<frown> w') \<Turnstile> af\<^sub>G (F \<phi>) [x]
 10. \<And>\<phi>1 \<phi>2. \<lbrakk>\<forall>\<psi>\<in>\<^bold>G \<phi>1. ([x] \<frown> xs \<frown> w') \<Turnstile> \<psi> = (xs \<frown> w') \<Turnstile> \<psi> \<Longrightarrow> ([x] \<frown> xs \<frown> w') \<Turnstile> \<phi>1 = (xs \<frown> w') \<Turnstile> af\<^sub>G \<phi>1 [x]; \<forall>\<psi>\<in>\<^bold>G \<phi>2. ([x] \<frown> xs \<frown> w') \<Turnstile> \<psi> = (xs \<frown> w') \<Turnstile> \<psi> \<Longrightarrow> ([x] \<frown> xs \<frown> w') \<Turnstile> \<phi>2 = (xs \<frown> w') \<Turnstile> af\<^sub>G \<phi>2 [x]; \<forall>\<psi>\<in>\<^bold>G (\<phi>1 U \<phi>2). ([x] \<frown> xs \<frown> w') \<Turnstile> \<psi> = (xs \<frown> w') \<Turnstile> \<psi>\<rbrakk> \<Longrightarrow> ([x] \<frown> xs \<frown> w') \<Turnstile> \<phi>1 U \<phi>2 = (xs \<frown> w') \<Turnstile> af\<^sub>G (\<phi>1 U \<phi>2) [x]
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
\<forall>\<psi>\<in>\<^bold>G \<phi>. ([x] \<frown> xs \<frown> w') \<Turnstile> \<psi> = (xs \<frown> w') \<Turnstile> \<psi> \<Longrightarrow> ([x] \<frown> xs \<frown> w') \<Turnstile> \<phi> = (xs \<frown> w') \<Turnstile> af\<^sub>G \<phi> [x]
\<forall>\<psi>\<in>\<^bold>G (F \<phi>). ([x] \<frown> xs \<frown> w') \<Turnstile> \<psi> = (xs \<frown> w') \<Turnstile> \<psi>

goal (1 subgoal):
 1. ([x] \<frown> xs \<frown> w') \<Turnstile> F \<phi> = (xs \<frown> w') \<Turnstile> af\<^sub>G (F \<phi>) [x]
[PROOF STEP]
unfolding LTL_F_one_step_unfolding
[PROOF STATE]
proof (prove)
using this:
\<forall>\<psi>\<in>\<^bold>G \<phi>. ([x] \<frown> xs \<frown> w') \<Turnstile> \<psi> = (xs \<frown> w') \<Turnstile> \<psi> \<Longrightarrow> ([x] \<frown> xs \<frown> w') \<Turnstile> \<phi> = (xs \<frown> w') \<Turnstile> af\<^sub>G \<phi> [x]
\<forall>\<psi>\<in>\<^bold>G (F \<phi>). ([x] \<frown> xs \<frown> w') \<Turnstile> \<psi> = (xs \<frown> w') \<Turnstile> \<psi>

goal (1 subgoal):
 1. (([x] \<frown> xs \<frown> w') \<Turnstile> \<phi> \<or> ([x] \<frown> xs \<frown> w') \<Turnstile> X (F \<phi>)) = (xs \<frown> w') \<Turnstile> af\<^sub>G (F \<phi>) [x]
[PROOF STEP]
by (auto simp add: suffix_conc_length[of "[x]", simplified])
[PROOF STATE]
proof (state)
this:
([x] \<frown> xs \<frown> w') \<Turnstile> F \<phi> = (xs \<frown> w') \<Turnstile> af\<^sub>G (F \<phi>) [x]

goal (9 subgoals):
 1. \<forall>\<psi>\<in>\<^bold>G true. ([x] \<frown> xs \<frown> w') \<Turnstile> \<psi> = (xs \<frown> w') \<Turnstile> \<psi> \<Longrightarrow> ([x] \<frown> xs \<frown> w') \<Turnstile> true = (xs \<frown> w') \<Turnstile> af\<^sub>G true [x]
 2. \<forall>\<psi>\<in>\<^bold>G false. ([x] \<frown> xs \<frown> w') \<Turnstile> \<psi> = (xs \<frown> w') \<Turnstile> \<psi> \<Longrightarrow> ([x] \<frown> xs \<frown> w') \<Turnstile> false = (xs \<frown> w') \<Turnstile> af\<^sub>G false [x]
 3. \<And>xa. \<forall>\<psi>\<in>\<^bold>G p(xa). ([x] \<frown> xs \<frown> w') \<Turnstile> \<psi> = (xs \<frown> w') \<Turnstile> \<psi> \<Longrightarrow> ([x] \<frown> xs \<frown> w') \<Turnstile> p(xa) = (xs \<frown> w') \<Turnstile> af\<^sub>G p(xa) [x]
 4. \<And>xa. \<forall>\<psi>\<in>\<^bold>G (np(xa)). ([x] \<frown> xs \<frown> w') \<Turnstile> \<psi> = (xs \<frown> w') \<Turnstile> \<psi> \<Longrightarrow> ([x] \<frown> xs \<frown> w') \<Turnstile> np(xa) = (xs \<frown> w') \<Turnstile> af\<^sub>G (np(xa)) [x]
 5. \<And>\<phi>1 \<phi>2. \<lbrakk>\<forall>\<psi>\<in>\<^bold>G \<phi>1. ([x] \<frown> xs \<frown> w') \<Turnstile> \<psi> = (xs \<frown> w') \<Turnstile> \<psi> \<Longrightarrow> ([x] \<frown> xs \<frown> w') \<Turnstile> \<phi>1 = (xs \<frown> w') \<Turnstile> af\<^sub>G \<phi>1 [x]; \<forall>\<psi>\<in>\<^bold>G \<phi>2. ([x] \<frown> xs \<frown> w') \<Turnstile> \<psi> = (xs \<frown> w') \<Turnstile> \<psi> \<Longrightarrow> ([x] \<frown> xs \<frown> w') \<Turnstile> \<phi>2 = (xs \<frown> w') \<Turnstile> af\<^sub>G \<phi>2 [x]; \<forall>\<psi>\<in>\<^bold>G (\<phi>1 and \<phi>2). ([x] \<frown> xs \<frown> w') \<Turnstile> \<psi> = (xs \<frown> w') \<Turnstile> \<psi>\<rbrakk> \<Longrightarrow> ([x] \<frown> xs \<frown> w') \<Turnstile> \<phi>1 and \<phi>2 = (xs \<frown> w') \<Turnstile> af\<^sub>G (\<phi>1 and \<phi>2) [x]
 6. \<And>\<phi>1 \<phi>2. \<lbrakk>\<forall>\<psi>\<in>\<^bold>G \<phi>1. ([x] \<frown> xs \<frown> w') \<Turnstile> \<psi> = (xs \<frown> w') \<Turnstile> \<psi> \<Longrightarrow> ([x] \<frown> xs \<frown> w') \<Turnstile> \<phi>1 = (xs \<frown> w') \<Turnstile> af\<^sub>G \<phi>1 [x]; \<forall>\<psi>\<in>\<^bold>G \<phi>2. ([x] \<frown> xs \<frown> w') \<Turnstile> \<psi> = (xs \<frown> w') \<Turnstile> \<psi> \<Longrightarrow> ([x] \<frown> xs \<frown> w') \<Turnstile> \<phi>2 = (xs \<frown> w') \<Turnstile> af\<^sub>G \<phi>2 [x]; \<forall>\<psi>\<in>\<^bold>G (\<phi>1 or \<phi>2). ([x] \<frown> xs \<frown> w') \<Turnstile> \<psi> = (xs \<frown> w') \<Turnstile> \<psi>\<rbrakk> \<Longrightarrow> ([x] \<frown> xs \<frown> w') \<Turnstile> \<phi>1 or \<phi>2 = (xs \<frown> w') \<Turnstile> af\<^sub>G (\<phi>1 or \<phi>2) [x]
 7. \<And>\<phi>. \<lbrakk>\<forall>\<psi>\<in>\<^bold>G \<phi>. ([x] \<frown> xs \<frown> w') \<Turnstile> \<psi> = (xs \<frown> w') \<Turnstile> \<psi> \<Longrightarrow> ([x] \<frown> xs \<frown> w') \<Turnstile> \<phi> = (xs \<frown> w') \<Turnstile> af\<^sub>G \<phi> [x]; \<forall>\<psi>\<in>\<^bold>G (X \<phi>). ([x] \<frown> xs \<frown> w') \<Turnstile> \<psi> = (xs \<frown> w') \<Turnstile> \<psi>\<rbrakk> \<Longrightarrow> ([x] \<frown> xs \<frown> w') \<Turnstile> X \<phi> = (xs \<frown> w') \<Turnstile> af\<^sub>G (X \<phi>) [x]
 8. \<And>\<phi>. \<lbrakk>\<forall>\<psi>\<in>\<^bold>G \<phi>. ([x] \<frown> xs \<frown> w') \<Turnstile> \<psi> = (xs \<frown> w') \<Turnstile> \<psi> \<Longrightarrow> ([x] \<frown> xs \<frown> w') \<Turnstile> \<phi> = (xs \<frown> w') \<Turnstile> af\<^sub>G \<phi> [x]; \<forall>\<psi>\<in>\<^bold>G (G \<phi>). ([x] \<frown> xs \<frown> w') \<Turnstile> \<psi> = (xs \<frown> w') \<Turnstile> \<psi>\<rbrakk> \<Longrightarrow> ([x] \<frown> xs \<frown> w') \<Turnstile> G \<phi> = (xs \<frown> w') \<Turnstile> af\<^sub>G (G \<phi>) [x]
 9. \<And>\<phi>1 \<phi>2. \<lbrakk>\<forall>\<psi>\<in>\<^bold>G \<phi>1. ([x] \<frown> xs \<frown> w') \<Turnstile> \<psi> = (xs \<frown> w') \<Turnstile> \<psi> \<Longrightarrow> ([x] \<frown> xs \<frown> w') \<Turnstile> \<phi>1 = (xs \<frown> w') \<Turnstile> af\<^sub>G \<phi>1 [x]; \<forall>\<psi>\<in>\<^bold>G \<phi>2. ([x] \<frown> xs \<frown> w') \<Turnstile> \<psi> = (xs \<frown> w') \<Turnstile> \<psi> \<Longrightarrow> ([x] \<frown> xs \<frown> w') \<Turnstile> \<phi>2 = (xs \<frown> w') \<Turnstile> af\<^sub>G \<phi>2 [x]; \<forall>\<psi>\<in>\<^bold>G (\<phi>1 U \<phi>2). ([x] \<frown> xs \<frown> w') \<Turnstile> \<psi> = (xs \<frown> w') \<Turnstile> \<psi>\<rbrakk> \<Longrightarrow> ([x] \<frown> xs \<frown> w') \<Turnstile> \<phi>1 U \<phi>2 = (xs \<frown> w') \<Turnstile> af\<^sub>G (\<phi>1 U \<phi>2) [x]
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (9 subgoals):
 1. \<forall>\<psi>\<in>\<^bold>G true. ([x] \<frown> xs \<frown> w') \<Turnstile> \<psi> = (xs \<frown> w') \<Turnstile> \<psi> \<Longrightarrow> ([x] \<frown> xs \<frown> w') \<Turnstile> true = (xs \<frown> w') \<Turnstile> af\<^sub>G true [x]
 2. \<forall>\<psi>\<in>\<^bold>G false. ([x] \<frown> xs \<frown> w') \<Turnstile> \<psi> = (xs \<frown> w') \<Turnstile> \<psi> \<Longrightarrow> ([x] \<frown> xs \<frown> w') \<Turnstile> false = (xs \<frown> w') \<Turnstile> af\<^sub>G false [x]
 3. \<And>xa. \<forall>\<psi>\<in>\<^bold>G p(xa). ([x] \<frown> xs \<frown> w') \<Turnstile> \<psi> = (xs \<frown> w') \<Turnstile> \<psi> \<Longrightarrow> ([x] \<frown> xs \<frown> w') \<Turnstile> p(xa) = (xs \<frown> w') \<Turnstile> af\<^sub>G p(xa) [x]
 4. \<And>xa. \<forall>\<psi>\<in>\<^bold>G (np(xa)). ([x] \<frown> xs \<frown> w') \<Turnstile> \<psi> = (xs \<frown> w') \<Turnstile> \<psi> \<Longrightarrow> ([x] \<frown> xs \<frown> w') \<Turnstile> np(xa) = (xs \<frown> w') \<Turnstile> af\<^sub>G (np(xa)) [x]
 5. \<And>\<phi>1 \<phi>2. \<lbrakk>\<forall>\<psi>\<in>\<^bold>G \<phi>1. ([x] \<frown> xs \<frown> w') \<Turnstile> \<psi> = (xs \<frown> w') \<Turnstile> \<psi> \<Longrightarrow> ([x] \<frown> xs \<frown> w') \<Turnstile> \<phi>1 = (xs \<frown> w') \<Turnstile> af\<^sub>G \<phi>1 [x]; \<forall>\<psi>\<in>\<^bold>G \<phi>2. ([x] \<frown> xs \<frown> w') \<Turnstile> \<psi> = (xs \<frown> w') \<Turnstile> \<psi> \<Longrightarrow> ([x] \<frown> xs \<frown> w') \<Turnstile> \<phi>2 = (xs \<frown> w') \<Turnstile> af\<^sub>G \<phi>2 [x]; \<forall>\<psi>\<in>\<^bold>G (\<phi>1 and \<phi>2). ([x] \<frown> xs \<frown> w') \<Turnstile> \<psi> = (xs \<frown> w') \<Turnstile> \<psi>\<rbrakk> \<Longrightarrow> ([x] \<frown> xs \<frown> w') \<Turnstile> \<phi>1 and \<phi>2 = (xs \<frown> w') \<Turnstile> af\<^sub>G (\<phi>1 and \<phi>2) [x]
 6. \<And>\<phi>1 \<phi>2. \<lbrakk>\<forall>\<psi>\<in>\<^bold>G \<phi>1. ([x] \<frown> xs \<frown> w') \<Turnstile> \<psi> = (xs \<frown> w') \<Turnstile> \<psi> \<Longrightarrow> ([x] \<frown> xs \<frown> w') \<Turnstile> \<phi>1 = (xs \<frown> w') \<Turnstile> af\<^sub>G \<phi>1 [x]; \<forall>\<psi>\<in>\<^bold>G \<phi>2. ([x] \<frown> xs \<frown> w') \<Turnstile> \<psi> = (xs \<frown> w') \<Turnstile> \<psi> \<Longrightarrow> ([x] \<frown> xs \<frown> w') \<Turnstile> \<phi>2 = (xs \<frown> w') \<Turnstile> af\<^sub>G \<phi>2 [x]; \<forall>\<psi>\<in>\<^bold>G (\<phi>1 or \<phi>2). ([x] \<frown> xs \<frown> w') \<Turnstile> \<psi> = (xs \<frown> w') \<Turnstile> \<psi>\<rbrakk> \<Longrightarrow> ([x] \<frown> xs \<frown> w') \<Turnstile> \<phi>1 or \<phi>2 = (xs \<frown> w') \<Turnstile> af\<^sub>G (\<phi>1 or \<phi>2) [x]
 7. \<And>\<phi>. \<lbrakk>\<forall>\<psi>\<in>\<^bold>G \<phi>. ([x] \<frown> xs \<frown> w') \<Turnstile> \<psi> = (xs \<frown> w') \<Turnstile> \<psi> \<Longrightarrow> ([x] \<frown> xs \<frown> w') \<Turnstile> \<phi> = (xs \<frown> w') \<Turnstile> af\<^sub>G \<phi> [x]; \<forall>\<psi>\<in>\<^bold>G (X \<phi>). ([x] \<frown> xs \<frown> w') \<Turnstile> \<psi> = (xs \<frown> w') \<Turnstile> \<psi>\<rbrakk> \<Longrightarrow> ([x] \<frown> xs \<frown> w') \<Turnstile> X \<phi> = (xs \<frown> w') \<Turnstile> af\<^sub>G (X \<phi>) [x]
 8. \<And>\<phi>. \<lbrakk>\<forall>\<psi>\<in>\<^bold>G \<phi>. ([x] \<frown> xs \<frown> w') \<Turnstile> \<psi> = (xs \<frown> w') \<Turnstile> \<psi> \<Longrightarrow> ([x] \<frown> xs \<frown> w') \<Turnstile> \<phi> = (xs \<frown> w') \<Turnstile> af\<^sub>G \<phi> [x]; \<forall>\<psi>\<in>\<^bold>G (G \<phi>). ([x] \<frown> xs \<frown> w') \<Turnstile> \<psi> = (xs \<frown> w') \<Turnstile> \<psi>\<rbrakk> \<Longrightarrow> ([x] \<frown> xs \<frown> w') \<Turnstile> G \<phi> = (xs \<frown> w') \<Turnstile> af\<^sub>G (G \<phi>) [x]
 9. \<And>\<phi>1 \<phi>2. \<lbrakk>\<forall>\<psi>\<in>\<^bold>G \<phi>1. ([x] \<frown> xs \<frown> w') \<Turnstile> \<psi> = (xs \<frown> w') \<Turnstile> \<psi> \<Longrightarrow> ([x] \<frown> xs \<frown> w') \<Turnstile> \<phi>1 = (xs \<frown> w') \<Turnstile> af\<^sub>G \<phi>1 [x]; \<forall>\<psi>\<in>\<^bold>G \<phi>2. ([x] \<frown> xs \<frown> w') \<Turnstile> \<psi> = (xs \<frown> w') \<Turnstile> \<psi> \<Longrightarrow> ([x] \<frown> xs \<frown> w') \<Turnstile> \<phi>2 = (xs \<frown> w') \<Turnstile> af\<^sub>G \<phi>2 [x]; \<forall>\<psi>\<in>\<^bold>G (\<phi>1 U \<phi>2). ([x] \<frown> xs \<frown> w') \<Turnstile> \<psi> = (xs \<frown> w') \<Turnstile> \<psi>\<rbrakk> \<Longrightarrow> ([x] \<frown> xs \<frown> w') \<Turnstile> \<phi>1 U \<phi>2 = (xs \<frown> w') \<Turnstile> af\<^sub>G (\<phi>1 U \<phi>2) [x]
[PROOF STEP]
case (LTLUntil \<phi> \<psi>)
[PROOF STATE]
proof (state)
this:
\<forall>\<psi>\<in>\<^bold>G \<phi>. ([x] \<frown> xs \<frown> w') \<Turnstile> \<psi> = (xs \<frown> w') \<Turnstile> \<psi> \<Longrightarrow> ([x] \<frown> xs \<frown> w') \<Turnstile> \<phi> = (xs \<frown> w') \<Turnstile> af\<^sub>G \<phi> [x]
\<forall>\<psi>\<in>\<^bold>G \<psi>. ([x] \<frown> xs \<frown> w') \<Turnstile> \<psi> = (xs \<frown> w') \<Turnstile> \<psi> \<Longrightarrow> ([x] \<frown> xs \<frown> w') \<Turnstile> \<psi> = (xs \<frown> w') \<Turnstile> af\<^sub>G \<psi> [x]
\<forall>\<psi>\<in>\<^bold>G (\<phi> U \<psi>). ([x] \<frown> xs \<frown> w') \<Turnstile> \<psi> = (xs \<frown> w') \<Turnstile> \<psi>

goal (9 subgoals):
 1. \<forall>\<psi>\<in>\<^bold>G true. ([x] \<frown> xs \<frown> w') \<Turnstile> \<psi> = (xs \<frown> w') \<Turnstile> \<psi> \<Longrightarrow> ([x] \<frown> xs \<frown> w') \<Turnstile> true = (xs \<frown> w') \<Turnstile> af\<^sub>G true [x]
 2. \<forall>\<psi>\<in>\<^bold>G false. ([x] \<frown> xs \<frown> w') \<Turnstile> \<psi> = (xs \<frown> w') \<Turnstile> \<psi> \<Longrightarrow> ([x] \<frown> xs \<frown> w') \<Turnstile> false = (xs \<frown> w') \<Turnstile> af\<^sub>G false [x]
 3. \<And>xa. \<forall>\<psi>\<in>\<^bold>G p(xa). ([x] \<frown> xs \<frown> w') \<Turnstile> \<psi> = (xs \<frown> w') \<Turnstile> \<psi> \<Longrightarrow> ([x] \<frown> xs \<frown> w') \<Turnstile> p(xa) = (xs \<frown> w') \<Turnstile> af\<^sub>G p(xa) [x]
 4. \<And>xa. \<forall>\<psi>\<in>\<^bold>G (np(xa)). ([x] \<frown> xs \<frown> w') \<Turnstile> \<psi> = (xs \<frown> w') \<Turnstile> \<psi> \<Longrightarrow> ([x] \<frown> xs \<frown> w') \<Turnstile> np(xa) = (xs \<frown> w') \<Turnstile> af\<^sub>G (np(xa)) [x]
 5. \<And>\<phi>1 \<phi>2. \<lbrakk>\<forall>\<psi>\<in>\<^bold>G \<phi>1. ([x] \<frown> xs \<frown> w') \<Turnstile> \<psi> = (xs \<frown> w') \<Turnstile> \<psi> \<Longrightarrow> ([x] \<frown> xs \<frown> w') \<Turnstile> \<phi>1 = (xs \<frown> w') \<Turnstile> af\<^sub>G \<phi>1 [x]; \<forall>\<psi>\<in>\<^bold>G \<phi>2. ([x] \<frown> xs \<frown> w') \<Turnstile> \<psi> = (xs \<frown> w') \<Turnstile> \<psi> \<Longrightarrow> ([x] \<frown> xs \<frown> w') \<Turnstile> \<phi>2 = (xs \<frown> w') \<Turnstile> af\<^sub>G \<phi>2 [x]; \<forall>\<psi>\<in>\<^bold>G (\<phi>1 and \<phi>2). ([x] \<frown> xs \<frown> w') \<Turnstile> \<psi> = (xs \<frown> w') \<Turnstile> \<psi>\<rbrakk> \<Longrightarrow> ([x] \<frown> xs \<frown> w') \<Turnstile> \<phi>1 and \<phi>2 = (xs \<frown> w') \<Turnstile> af\<^sub>G (\<phi>1 and \<phi>2) [x]
 6. \<And>\<phi>1 \<phi>2. \<lbrakk>\<forall>\<psi>\<in>\<^bold>G \<phi>1. ([x] \<frown> xs \<frown> w') \<Turnstile> \<psi> = (xs \<frown> w') \<Turnstile> \<psi> \<Longrightarrow> ([x] \<frown> xs \<frown> w') \<Turnstile> \<phi>1 = (xs \<frown> w') \<Turnstile> af\<^sub>G \<phi>1 [x]; \<forall>\<psi>\<in>\<^bold>G \<phi>2. ([x] \<frown> xs \<frown> w') \<Turnstile> \<psi> = (xs \<frown> w') \<Turnstile> \<psi> \<Longrightarrow> ([x] \<frown> xs \<frown> w') \<Turnstile> \<phi>2 = (xs \<frown> w') \<Turnstile> af\<^sub>G \<phi>2 [x]; \<forall>\<psi>\<in>\<^bold>G (\<phi>1 or \<phi>2). ([x] \<frown> xs \<frown> w') \<Turnstile> \<psi> = (xs \<frown> w') \<Turnstile> \<psi>\<rbrakk> \<Longrightarrow> ([x] \<frown> xs \<frown> w') \<Turnstile> \<phi>1 or \<phi>2 = (xs \<frown> w') \<Turnstile> af\<^sub>G (\<phi>1 or \<phi>2) [x]
 7. \<And>\<phi>. \<lbrakk>\<forall>\<psi>\<in>\<^bold>G \<phi>. ([x] \<frown> xs \<frown> w') \<Turnstile> \<psi> = (xs \<frown> w') \<Turnstile> \<psi> \<Longrightarrow> ([x] \<frown> xs \<frown> w') \<Turnstile> \<phi> = (xs \<frown> w') \<Turnstile> af\<^sub>G \<phi> [x]; \<forall>\<psi>\<in>\<^bold>G (X \<phi>). ([x] \<frown> xs \<frown> w') \<Turnstile> \<psi> = (xs \<frown> w') \<Turnstile> \<psi>\<rbrakk> \<Longrightarrow> ([x] \<frown> xs \<frown> w') \<Turnstile> X \<phi> = (xs \<frown> w') \<Turnstile> af\<^sub>G (X \<phi>) [x]
 8. \<And>\<phi>. \<lbrakk>\<forall>\<psi>\<in>\<^bold>G \<phi>. ([x] \<frown> xs \<frown> w') \<Turnstile> \<psi> = (xs \<frown> w') \<Turnstile> \<psi> \<Longrightarrow> ([x] \<frown> xs \<frown> w') \<Turnstile> \<phi> = (xs \<frown> w') \<Turnstile> af\<^sub>G \<phi> [x]; \<forall>\<psi>\<in>\<^bold>G (G \<phi>). ([x] \<frown> xs \<frown> w') \<Turnstile> \<psi> = (xs \<frown> w') \<Turnstile> \<psi>\<rbrakk> \<Longrightarrow> ([x] \<frown> xs \<frown> w') \<Turnstile> G \<phi> = (xs \<frown> w') \<Turnstile> af\<^sub>G (G \<phi>) [x]
 9. \<And>\<phi>1 \<phi>2. \<lbrakk>\<forall>\<psi>\<in>\<^bold>G \<phi>1. ([x] \<frown> xs \<frown> w') \<Turnstile> \<psi> = (xs \<frown> w') \<Turnstile> \<psi> \<Longrightarrow> ([x] \<frown> xs \<frown> w') \<Turnstile> \<phi>1 = (xs \<frown> w') \<Turnstile> af\<^sub>G \<phi>1 [x]; \<forall>\<psi>\<in>\<^bold>G \<phi>2. ([x] \<frown> xs \<frown> w') \<Turnstile> \<psi> = (xs \<frown> w') \<Turnstile> \<psi> \<Longrightarrow> ([x] \<frown> xs \<frown> w') \<Turnstile> \<phi>2 = (xs \<frown> w') \<Turnstile> af\<^sub>G \<phi>2 [x]; \<forall>\<psi>\<in>\<^bold>G (\<phi>1 U \<phi>2). ([x] \<frown> xs \<frown> w') \<Turnstile> \<psi> = (xs \<frown> w') \<Turnstile> \<psi>\<rbrakk> \<Longrightarrow> ([x] \<frown> xs \<frown> w') \<Turnstile> \<phi>1 U \<phi>2 = (xs \<frown> w') \<Turnstile> af\<^sub>G (\<phi>1 U \<phi>2) [x]
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
\<forall>\<psi>\<in>\<^bold>G \<phi>. ([x] \<frown> xs \<frown> w') \<Turnstile> \<psi> = (xs \<frown> w') \<Turnstile> \<psi> \<Longrightarrow> ([x] \<frown> xs \<frown> w') \<Turnstile> \<phi> = (xs \<frown> w') \<Turnstile> af\<^sub>G \<phi> [x]
\<forall>\<psi>\<in>\<^bold>G \<psi>. ([x] \<frown> xs \<frown> w') \<Turnstile> \<psi> = (xs \<frown> w') \<Turnstile> \<psi> \<Longrightarrow> ([x] \<frown> xs \<frown> w') \<Turnstile> \<psi> = (xs \<frown> w') \<Turnstile> af\<^sub>G \<psi> [x]
\<forall>\<psi>\<in>\<^bold>G (\<phi> U \<psi>). ([x] \<frown> xs \<frown> w') \<Turnstile> \<psi> = (xs \<frown> w') \<Turnstile> \<psi>

goal (1 subgoal):
 1. ([x] \<frown> xs \<frown> w') \<Turnstile> \<phi> U \<psi> = (xs \<frown> w') \<Turnstile> af\<^sub>G (\<phi> U \<psi>) [x]
[PROOF STEP]
unfolding LTL_U_one_step_unfolding
[PROOF STATE]
proof (prove)
using this:
\<forall>\<psi>\<in>\<^bold>G \<phi>. ([x] \<frown> xs \<frown> w') \<Turnstile> \<psi> = (xs \<frown> w') \<Turnstile> \<psi> \<Longrightarrow> ([x] \<frown> xs \<frown> w') \<Turnstile> \<phi> = (xs \<frown> w') \<Turnstile> af\<^sub>G \<phi> [x]
\<forall>\<psi>\<in>\<^bold>G \<psi>. ([x] \<frown> xs \<frown> w') \<Turnstile> \<psi> = (xs \<frown> w') \<Turnstile> \<psi> \<Longrightarrow> ([x] \<frown> xs \<frown> w') \<Turnstile> \<psi> = (xs \<frown> w') \<Turnstile> af\<^sub>G \<psi> [x]
\<forall>\<psi>\<in>\<^bold>G (\<phi> U \<psi>). ([x] \<frown> xs \<frown> w') \<Turnstile> \<psi> = (xs \<frown> w') \<Turnstile> \<psi>

goal (1 subgoal):
 1. (([x] \<frown> xs \<frown> w') \<Turnstile> \<psi> \<or> ([x] \<frown> xs \<frown> w') \<Turnstile> \<phi> \<and> ([x] \<frown> xs \<frown> w') \<Turnstile> X (\<phi> U \<psi>)) = (xs \<frown> w') \<Turnstile> af\<^sub>G (\<phi> U \<psi>) [x]
[PROOF STEP]
by (auto simp add: suffix_conc_length[of "[x]", simplified])
[PROOF STATE]
proof (state)
this:
([x] \<frown> xs \<frown> w') \<Turnstile> \<phi> U \<psi> = (xs \<frown> w') \<Turnstile> af\<^sub>G (\<phi> U \<psi>) [x]

goal (8 subgoals):
 1. \<forall>\<psi>\<in>\<^bold>G true. ([x] \<frown> xs \<frown> w') \<Turnstile> \<psi> = (xs \<frown> w') \<Turnstile> \<psi> \<Longrightarrow> ([x] \<frown> xs \<frown> w') \<Turnstile> true = (xs \<frown> w') \<Turnstile> af\<^sub>G true [x]
 2. \<forall>\<psi>\<in>\<^bold>G false. ([x] \<frown> xs \<frown> w') \<Turnstile> \<psi> = (xs \<frown> w') \<Turnstile> \<psi> \<Longrightarrow> ([x] \<frown> xs \<frown> w') \<Turnstile> false = (xs \<frown> w') \<Turnstile> af\<^sub>G false [x]
 3. \<And>xa. \<forall>\<psi>\<in>\<^bold>G p(xa). ([x] \<frown> xs \<frown> w') \<Turnstile> \<psi> = (xs \<frown> w') \<Turnstile> \<psi> \<Longrightarrow> ([x] \<frown> xs \<frown> w') \<Turnstile> p(xa) = (xs \<frown> w') \<Turnstile> af\<^sub>G p(xa) [x]
 4. \<And>xa. \<forall>\<psi>\<in>\<^bold>G (np(xa)). ([x] \<frown> xs \<frown> w') \<Turnstile> \<psi> = (xs \<frown> w') \<Turnstile> \<psi> \<Longrightarrow> ([x] \<frown> xs \<frown> w') \<Turnstile> np(xa) = (xs \<frown> w') \<Turnstile> af\<^sub>G (np(xa)) [x]
 5. \<And>\<phi>1 \<phi>2. \<lbrakk>\<forall>\<psi>\<in>\<^bold>G \<phi>1. ([x] \<frown> xs \<frown> w') \<Turnstile> \<psi> = (xs \<frown> w') \<Turnstile> \<psi> \<Longrightarrow> ([x] \<frown> xs \<frown> w') \<Turnstile> \<phi>1 = (xs \<frown> w') \<Turnstile> af\<^sub>G \<phi>1 [x]; \<forall>\<psi>\<in>\<^bold>G \<phi>2. ([x] \<frown> xs \<frown> w') \<Turnstile> \<psi> = (xs \<frown> w') \<Turnstile> \<psi> \<Longrightarrow> ([x] \<frown> xs \<frown> w') \<Turnstile> \<phi>2 = (xs \<frown> w') \<Turnstile> af\<^sub>G \<phi>2 [x]; \<forall>\<psi>\<in>\<^bold>G (\<phi>1 and \<phi>2). ([x] \<frown> xs \<frown> w') \<Turnstile> \<psi> = (xs \<frown> w') \<Turnstile> \<psi>\<rbrakk> \<Longrightarrow> ([x] \<frown> xs \<frown> w') \<Turnstile> \<phi>1 and \<phi>2 = (xs \<frown> w') \<Turnstile> af\<^sub>G (\<phi>1 and \<phi>2) [x]
 6. \<And>\<phi>1 \<phi>2. \<lbrakk>\<forall>\<psi>\<in>\<^bold>G \<phi>1. ([x] \<frown> xs \<frown> w') \<Turnstile> \<psi> = (xs \<frown> w') \<Turnstile> \<psi> \<Longrightarrow> ([x] \<frown> xs \<frown> w') \<Turnstile> \<phi>1 = (xs \<frown> w') \<Turnstile> af\<^sub>G \<phi>1 [x]; \<forall>\<psi>\<in>\<^bold>G \<phi>2. ([x] \<frown> xs \<frown> w') \<Turnstile> \<psi> = (xs \<frown> w') \<Turnstile> \<psi> \<Longrightarrow> ([x] \<frown> xs \<frown> w') \<Turnstile> \<phi>2 = (xs \<frown> w') \<Turnstile> af\<^sub>G \<phi>2 [x]; \<forall>\<psi>\<in>\<^bold>G (\<phi>1 or \<phi>2). ([x] \<frown> xs \<frown> w') \<Turnstile> \<psi> = (xs \<frown> w') \<Turnstile> \<psi>\<rbrakk> \<Longrightarrow> ([x] \<frown> xs \<frown> w') \<Turnstile> \<phi>1 or \<phi>2 = (xs \<frown> w') \<Turnstile> af\<^sub>G (\<phi>1 or \<phi>2) [x]
 7. \<And>\<phi>. \<lbrakk>\<forall>\<psi>\<in>\<^bold>G \<phi>. ([x] \<frown> xs \<frown> w') \<Turnstile> \<psi> = (xs \<frown> w') \<Turnstile> \<psi> \<Longrightarrow> ([x] \<frown> xs \<frown> w') \<Turnstile> \<phi> = (xs \<frown> w') \<Turnstile> af\<^sub>G \<phi> [x]; \<forall>\<psi>\<in>\<^bold>G (X \<phi>). ([x] \<frown> xs \<frown> w') \<Turnstile> \<psi> = (xs \<frown> w') \<Turnstile> \<psi>\<rbrakk> \<Longrightarrow> ([x] \<frown> xs \<frown> w') \<Turnstile> X \<phi> = (xs \<frown> w') \<Turnstile> af\<^sub>G (X \<phi>) [x]
 8. \<And>\<phi>. \<lbrakk>\<forall>\<psi>\<in>\<^bold>G \<phi>. ([x] \<frown> xs \<frown> w') \<Turnstile> \<psi> = (xs \<frown> w') \<Turnstile> \<psi> \<Longrightarrow> ([x] \<frown> xs \<frown> w') \<Turnstile> \<phi> = (xs \<frown> w') \<Turnstile> af\<^sub>G \<phi> [x]; \<forall>\<psi>\<in>\<^bold>G (G \<phi>). ([x] \<frown> xs \<frown> w') \<Turnstile> \<psi> = (xs \<frown> w') \<Turnstile> \<psi>\<rbrakk> \<Longrightarrow> ([x] \<frown> xs \<frown> w') \<Turnstile> G \<phi> = (xs \<frown> w') \<Turnstile> af\<^sub>G (G \<phi>) [x]
[PROOF STEP]
qed (auto simp add: conc_fst[of 0 "[x]"] suffix_conc_length[of "[x]", simplified])
[PROOF STATE]
proof (state)
this:
([x] \<frown> xs \<frown> w') \<Turnstile> \<phi> = (xs \<frown> w') \<Turnstile> af\<^sub>G \<phi> [x]

goal (2 subgoals):
 1. \<And>w' \<phi>. \<forall>\<psi>\<in>\<^bold>G \<phi>. w' \<Turnstile> \<psi> = ([] \<frown> w') \<Turnstile> \<psi> \<Longrightarrow> ([] \<frown> w') \<Turnstile> \<phi> = w' \<Turnstile> af\<^sub>G \<phi> []
 2. \<And>a w w' \<phi>. \<lbrakk>\<And>w' \<phi>. \<forall>\<psi>\<in>\<^bold>G \<phi>. w' \<Turnstile> \<psi> = (w \<frown> w') \<Turnstile> \<psi> \<Longrightarrow> (w \<frown> w') \<Turnstile> \<phi> = w' \<Turnstile> af\<^sub>G \<phi> w; \<forall>\<psi>\<in>\<^bold>G \<phi>. w' \<Turnstile> \<psi> = ((a # w) \<frown> w') \<Turnstile> \<psi>\<rbrakk> \<Longrightarrow> ((a # w) \<frown> w') \<Turnstile> \<phi> = w' \<Turnstile> af\<^sub>G \<phi> (a # w)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
([x] \<frown> xs \<frown> w') \<Turnstile> \<phi> = (xs \<frown> w') \<Turnstile> af\<^sub>G \<phi> [x]

goal (2 subgoals):
 1. \<And>w' \<phi>. \<forall>\<psi>\<in>\<^bold>G \<phi>. w' \<Turnstile> \<psi> = ([] \<frown> w') \<Turnstile> \<psi> \<Longrightarrow> ([] \<frown> w') \<Turnstile> \<phi> = w' \<Turnstile> af\<^sub>G \<phi> []
 2. \<And>a w w' \<phi>. \<lbrakk>\<And>w' \<phi>. \<forall>\<psi>\<in>\<^bold>G \<phi>. w' \<Turnstile> \<psi> = (w \<frown> w') \<Turnstile> \<psi> \<Longrightarrow> (w \<frown> w') \<Turnstile> \<phi> = w' \<Turnstile> af\<^sub>G \<phi> w; \<forall>\<psi>\<in>\<^bold>G \<phi>. w' \<Turnstile> \<psi> = ((a # w) \<frown> w') \<Turnstile> \<psi>\<rbrakk> \<Longrightarrow> ((a # w) \<frown> w') \<Turnstile> \<phi> = w' \<Turnstile> af\<^sub>G \<phi> (a # w)
[PROOF STEP]
have "... = w' \<Turnstile> af\<^sub>G \<phi> (x # xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (xs \<frown> w') \<Turnstile> af\<^sub>G \<phi> [x] = w' \<Turnstile> af\<^sub>G \<phi> (x # xs)
[PROOF STEP]
using Cons.IH[of "af\<^sub>G \<phi> [x]" w'] A
[PROOF STATE]
proof (prove)
using this:
\<forall>\<psi>\<in>\<^bold>G (af\<^sub>G \<phi> [x]). w' \<Turnstile> \<psi> = (xs \<frown> w') \<Turnstile> \<psi> \<Longrightarrow> (xs \<frown> w') \<Turnstile> af\<^sub>G \<phi> [x] = w' \<Turnstile> af\<^sub>G (af\<^sub>G \<phi> [x]) xs
\<forall>\<psi>\<in>\<^bold>G (af\<^sub>G \<phi> [x]). w' \<Turnstile> \<psi> = (xs \<frown> w') \<Turnstile> \<psi>

goal (1 subgoal):
 1. (xs \<frown> w') \<Turnstile> af\<^sub>G \<phi> [x] = w' \<Turnstile> af\<^sub>G \<phi> (x # xs)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(xs \<frown> w') \<Turnstile> af\<^sub>G \<phi> [x] = w' \<Turnstile> af\<^sub>G \<phi> (x # xs)

goal (2 subgoals):
 1. \<And>w' \<phi>. \<forall>\<psi>\<in>\<^bold>G \<phi>. w' \<Turnstile> \<psi> = ([] \<frown> w') \<Turnstile> \<psi> \<Longrightarrow> ([] \<frown> w') \<Turnstile> \<phi> = w' \<Turnstile> af\<^sub>G \<phi> []
 2. \<And>a w w' \<phi>. \<lbrakk>\<And>w' \<phi>. \<forall>\<psi>\<in>\<^bold>G \<phi>. w' \<Turnstile> \<psi> = (w \<frown> w') \<Turnstile> \<psi> \<Longrightarrow> (w \<frown> w') \<Turnstile> \<phi> = w' \<Turnstile> af\<^sub>G \<phi> w; \<forall>\<psi>\<in>\<^bold>G \<phi>. w' \<Turnstile> \<psi> = ((a # w) \<frown> w') \<Turnstile> \<psi>\<rbrakk> \<Longrightarrow> ((a # w) \<frown> w') \<Turnstile> \<phi> = w' \<Turnstile> af\<^sub>G \<phi> (a # w)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
([x] \<frown> xs \<frown> w') \<Turnstile> \<phi> = w' \<Turnstile> af\<^sub>G \<phi> (x # xs)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
([x] \<frown> xs \<frown> w') \<Turnstile> \<phi> = w' \<Turnstile> af\<^sub>G \<phi> (x # xs)

goal (1 subgoal):
 1. ((x # xs) \<frown> w') \<Turnstile> \<phi> = w' \<Turnstile> af\<^sub>G \<phi> (x # xs)
[PROOF STEP]
unfolding conc_conc
[PROOF STATE]
proof (prove)
using this:
(([x] @ xs) \<frown> w') \<Turnstile> \<phi> = w' \<Turnstile> af\<^sub>G \<phi> (x # xs)

goal (1 subgoal):
 1. ((x # xs) \<frown> w') \<Turnstile> \<phi> = w' \<Turnstile> af\<^sub>G \<phi> (x # xs)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
((x # xs) \<frown> w') \<Turnstile> \<phi> = w' \<Turnstile> af\<^sub>G \<phi> (x # xs)

goal (1 subgoal):
 1. \<And>w' \<phi>. \<forall>\<psi>\<in>\<^bold>G \<phi>. w' \<Turnstile> \<psi> = ([] \<frown> w') \<Turnstile> \<psi> \<Longrightarrow> ([] \<frown> w') \<Turnstile> \<phi> = w' \<Turnstile> af\<^sub>G \<phi> []
[PROOF STEP]
qed simp


[STATEMENT]
lemma af\<^sub>G_ltl_continuation_suffix:
  "\<forall>\<psi> \<in> \<^bold>G \<phi>. w \<Turnstile> \<psi> = (suffix i w) \<Turnstile> \<psi> \<Longrightarrow> w \<Turnstile> \<phi> \<longleftrightarrow> suffix i w \<Turnstile> af\<^sub>G \<phi> (w [0 \<rightarrow> i])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>\<psi>\<in>\<^bold>G \<phi>. w \<Turnstile> \<psi> = suffix i w \<Turnstile> \<psi> \<Longrightarrow> w \<Turnstile> \<phi> = suffix i w \<Turnstile> af\<^sub>G \<phi> (prefix i w)
[PROOF STEP]
by (metis af_G_ltl_continuation[of \<phi> "suffix i w"] prefix_suffix subsequence_def)


[STATEMENT]
lemma af_letter_alt_def:
  "af_letter \<phi> \<nu> = step (Unf \<phi>) \<nu>"
  "af_G_letter \<phi> \<nu> = step (Unf\<^sub>G \<phi>) \<nu>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. af_letter \<phi> \<nu> = step (Unf \<phi>) \<nu> &&& af_G_letter \<phi> \<nu> = step (Unf\<^sub>G \<phi>) \<nu>
[PROOF STEP]
by (induction \<phi>) simp_all


[STATEMENT]
lemma af_to_af_opt:
  "Unf (af \<phi> w) = af\<^sub>\<UU> (Unf \<phi>) w"
  "Unf\<^sub>G (af\<^sub>G \<phi> w) = af\<^sub>G\<^sub>\<UU> (Unf\<^sub>G \<phi>) w"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Unf (af \<phi> w) = af\<^sub>\<UU> (Unf \<phi>) w &&& Unf\<^sub>G (af\<^sub>G \<phi> w) = af\<^sub>G\<^sub>\<UU> (Unf\<^sub>G \<phi>) w
[PROOF STEP]
by (induction w arbitrary: \<phi>)
     (simp_all add: af_letter_alt_def)


[STATEMENT]
lemma af_equiv:
  "af \<phi> (w @ [\<nu>]) = step (af\<^sub>\<UU> (Unf \<phi>) w) \<nu>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. af \<phi> (w @ [\<nu>]) = step (af\<^sub>\<UU> (Unf \<phi>) w) \<nu>
[PROOF STEP]
using af_to_af_opt(1)
[PROOF STATE]
proof (prove)
using this:
Unf (af ?\<phi> ?w) = af\<^sub>\<UU> (Unf ?\<phi>) ?w

goal (1 subgoal):
 1. af \<phi> (w @ [\<nu>]) = step (af\<^sub>\<UU> (Unf \<phi>) w) \<nu>
[PROOF STEP]
by (metis af_letter_alt_def(1) foldl_Cons foldl_Nil foldl_append)


[STATEMENT]
lemma af_equiv':
  "af \<phi> (w [0 \<rightarrow> Suc i]) = step (af\<^sub>\<UU> (Unf \<phi>) (w [0 \<rightarrow> i])) (w i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. af \<phi> (prefix (Suc i) w) = step (af\<^sub>\<UU> (Unf \<phi>) (prefix i w)) (w i)
[PROOF STEP]
using af_equiv
[PROOF STATE]
proof (prove)
using this:
af ?\<phi> (?w @ [?\<nu>]) = step (af\<^sub>\<UU> (Unf ?\<phi>) ?w) ?\<nu>

goal (1 subgoal):
 1. af \<phi> (prefix (Suc i) w) = step (af\<^sub>\<UU> (Unf \<phi>) (prefix i w)) (w i)
[PROOF STEP]
unfolding subsequence_def
[PROOF STATE]
proof (prove)
using this:
af ?\<phi> (?w @ [?\<nu>]) = step (af\<^sub>\<UU> (Unf ?\<phi>) ?w) ?\<nu>

goal (1 subgoal):
 1. af \<phi> (map w [0..<Suc i]) = step (af\<^sub>\<UU> (Unf \<phi>) (map w [0..<i])) (w i)
[PROOF STEP]
by auto


[STATEMENT]
lemma respectfulness:
  "\<phi> \<longrightarrow>\<^sub>P \<psi> \<Longrightarrow> af_letter_opt \<phi> \<nu> \<longrightarrow>\<^sub>P af_letter_opt \<psi> \<nu>"
  "\<phi> \<equiv>\<^sub>P \<psi> \<Longrightarrow> af_letter_opt \<phi> \<nu> \<equiv>\<^sub>P af_letter_opt \<psi> \<nu>"
  "\<phi> \<longrightarrow>\<^sub>P \<psi> \<Longrightarrow> af_G_letter_opt \<phi> \<nu> \<longrightarrow>\<^sub>P af_G_letter_opt \<psi> \<nu>"
  "\<phi> \<equiv>\<^sub>P \<psi> \<Longrightarrow> af_G_letter_opt \<phi> \<nu> \<equiv>\<^sub>P af_G_letter_opt \<psi> \<nu>"
  "\<phi> \<longrightarrow>\<^sub>P \<psi> \<Longrightarrow> step \<phi> \<nu> \<longrightarrow>\<^sub>P step \<psi> \<nu>"
  "\<phi> \<equiv>\<^sub>P \<psi> \<Longrightarrow> step \<phi> \<nu> \<equiv>\<^sub>P step \<psi> \<nu>"
  "\<phi> \<longrightarrow>\<^sub>P \<psi> \<Longrightarrow> Unf \<phi> \<longrightarrow>\<^sub>P Unf \<psi>"
  "\<phi> \<equiv>\<^sub>P \<psi> \<Longrightarrow> Unf \<phi> \<equiv>\<^sub>P Unf \<psi>"
  "\<phi> \<longrightarrow>\<^sub>P \<psi> \<Longrightarrow> Unf\<^sub>G \<phi> \<longrightarrow>\<^sub>P Unf\<^sub>G \<psi>"
  "\<phi> \<equiv>\<^sub>P \<psi> \<Longrightarrow> Unf\<^sub>G \<phi> \<equiv>\<^sub>P Unf\<^sub>G \<psi>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (((\<phi> \<longrightarrow>\<^sub>P \<psi> \<Longrightarrow> af_letter_opt \<phi> \<nu> \<longrightarrow>\<^sub>P af_letter_opt \<psi> \<nu>) &&& (\<phi> \<equiv>\<^sub>P \<psi> \<Longrightarrow> af_letter_opt \<phi> \<nu> \<equiv>\<^sub>P af_letter_opt \<psi> \<nu>)) &&& (\<phi> \<longrightarrow>\<^sub>P \<psi> \<Longrightarrow> af_G_letter_opt \<phi> \<nu> \<longrightarrow>\<^sub>P af_G_letter_opt \<psi> \<nu>) &&& (\<phi> \<equiv>\<^sub>P \<psi> \<Longrightarrow> af_G_letter_opt \<phi> \<nu> \<equiv>\<^sub>P af_G_letter_opt \<psi> \<nu>) &&& (\<phi> \<longrightarrow>\<^sub>P \<psi> \<Longrightarrow> step \<phi> \<nu> \<longrightarrow>\<^sub>P step \<psi> \<nu>)) &&& ((\<phi> \<equiv>\<^sub>P \<psi> \<Longrightarrow> step \<phi> \<nu> \<equiv>\<^sub>P step \<psi> \<nu>) &&& (\<phi> \<longrightarrow>\<^sub>P \<psi> \<Longrightarrow> Unf \<phi> \<longrightarrow>\<^sub>P Unf \<psi>)) &&& (\<phi> \<equiv>\<^sub>P \<psi> \<Longrightarrow> Unf \<phi> \<equiv>\<^sub>P Unf \<psi>) &&& (\<phi> \<longrightarrow>\<^sub>P \<psi> \<Longrightarrow> Unf\<^sub>G \<phi> \<longrightarrow>\<^sub>P Unf\<^sub>G \<psi>) &&& (\<phi> \<equiv>\<^sub>P \<psi> \<Longrightarrow> Unf\<^sub>G \<phi> \<equiv>\<^sub>P Unf\<^sub>G \<psi>)
[PROOF STEP]
using decomposable_function_subst[of "\<lambda>\<chi>. af_letter_opt \<chi> \<nu>", simplified] af_letter_opt.simps
[PROOF STATE]
proof (prove)
using this:
Unf (step ?\<phi> \<nu>) = subst ?\<phi> (\<lambda>\<chi>. Some (Unf (step \<chi> \<nu>)))
af_letter_opt ?\<phi> ?\<nu> = Unf (step ?\<phi> ?\<nu>)

goal (1 subgoal):
 1. (((\<phi> \<longrightarrow>\<^sub>P \<psi> \<Longrightarrow> af_letter_opt \<phi> \<nu> \<longrightarrow>\<^sub>P af_letter_opt \<psi> \<nu>) &&& (\<phi> \<equiv>\<^sub>P \<psi> \<Longrightarrow> af_letter_opt \<phi> \<nu> \<equiv>\<^sub>P af_letter_opt \<psi> \<nu>)) &&& (\<phi> \<longrightarrow>\<^sub>P \<psi> \<Longrightarrow> af_G_letter_opt \<phi> \<nu> \<longrightarrow>\<^sub>P af_G_letter_opt \<psi> \<nu>) &&& (\<phi> \<equiv>\<^sub>P \<psi> \<Longrightarrow> af_G_letter_opt \<phi> \<nu> \<equiv>\<^sub>P af_G_letter_opt \<psi> \<nu>) &&& (\<phi> \<longrightarrow>\<^sub>P \<psi> \<Longrightarrow> step \<phi> \<nu> \<longrightarrow>\<^sub>P step \<psi> \<nu>)) &&& ((\<phi> \<equiv>\<^sub>P \<psi> \<Longrightarrow> step \<phi> \<nu> \<equiv>\<^sub>P step \<psi> \<nu>) &&& (\<phi> \<longrightarrow>\<^sub>P \<psi> \<Longrightarrow> Unf \<phi> \<longrightarrow>\<^sub>P Unf \<psi>)) &&& (\<phi> \<equiv>\<^sub>P \<psi> \<Longrightarrow> Unf \<phi> \<equiv>\<^sub>P Unf \<psi>) &&& (\<phi> \<longrightarrow>\<^sub>P \<psi> \<Longrightarrow> Unf\<^sub>G \<phi> \<longrightarrow>\<^sub>P Unf\<^sub>G \<psi>) &&& (\<phi> \<equiv>\<^sub>P \<psi> \<Longrightarrow> Unf\<^sub>G \<phi> \<equiv>\<^sub>P Unf\<^sub>G \<psi>)
[PROOF STEP]
using decomposable_function_subst[of "\<lambda>\<chi>. af_G_letter_opt \<chi> \<nu>", simplified] af_G_letter_opt.simps
[PROOF STATE]
proof (prove)
using this:
Unf (step ?\<phi> \<nu>) = subst ?\<phi> (\<lambda>\<chi>. Some (Unf (step \<chi> \<nu>)))
af_letter_opt ?\<phi> ?\<nu> = Unf (step ?\<phi> ?\<nu>)
Unf\<^sub>G (step ?\<phi> \<nu>) = subst ?\<phi> (\<lambda>\<chi>. Some (Unf\<^sub>G (step \<chi> \<nu>)))
af_G_letter_opt ?\<phi> ?\<nu> = Unf\<^sub>G (step ?\<phi> ?\<nu>)

goal (1 subgoal):
 1. (((\<phi> \<longrightarrow>\<^sub>P \<psi> \<Longrightarrow> af_letter_opt \<phi> \<nu> \<longrightarrow>\<^sub>P af_letter_opt \<psi> \<nu>) &&& (\<phi> \<equiv>\<^sub>P \<psi> \<Longrightarrow> af_letter_opt \<phi> \<nu> \<equiv>\<^sub>P af_letter_opt \<psi> \<nu>)) &&& (\<phi> \<longrightarrow>\<^sub>P \<psi> \<Longrightarrow> af_G_letter_opt \<phi> \<nu> \<longrightarrow>\<^sub>P af_G_letter_opt \<psi> \<nu>) &&& (\<phi> \<equiv>\<^sub>P \<psi> \<Longrightarrow> af_G_letter_opt \<phi> \<nu> \<equiv>\<^sub>P af_G_letter_opt \<psi> \<nu>) &&& (\<phi> \<longrightarrow>\<^sub>P \<psi> \<Longrightarrow> step \<phi> \<nu> \<longrightarrow>\<^sub>P step \<psi> \<nu>)) &&& ((\<phi> \<equiv>\<^sub>P \<psi> \<Longrightarrow> step \<phi> \<nu> \<equiv>\<^sub>P step \<psi> \<nu>) &&& (\<phi> \<longrightarrow>\<^sub>P \<psi> \<Longrightarrow> Unf \<phi> \<longrightarrow>\<^sub>P Unf \<psi>)) &&& (\<phi> \<equiv>\<^sub>P \<psi> \<Longrightarrow> Unf \<phi> \<equiv>\<^sub>P Unf \<psi>) &&& (\<phi> \<longrightarrow>\<^sub>P \<psi> \<Longrightarrow> Unf\<^sub>G \<phi> \<longrightarrow>\<^sub>P Unf\<^sub>G \<psi>) &&& (\<phi> \<equiv>\<^sub>P \<psi> \<Longrightarrow> Unf\<^sub>G \<phi> \<equiv>\<^sub>P Unf\<^sub>G \<psi>)
[PROOF STEP]
using decomposable_function_subst[of "\<lambda>\<chi>. step \<chi> \<nu>", simplified]
[PROOF STATE]
proof (prove)
using this:
Unf (step ?\<phi> \<nu>) = subst ?\<phi> (\<lambda>\<chi>. Some (Unf (step \<chi> \<nu>)))
af_letter_opt ?\<phi> ?\<nu> = Unf (step ?\<phi> ?\<nu>)
Unf\<^sub>G (step ?\<phi> \<nu>) = subst ?\<phi> (\<lambda>\<chi>. Some (Unf\<^sub>G (step \<chi> \<nu>)))
af_G_letter_opt ?\<phi> ?\<nu> = Unf\<^sub>G (step ?\<phi> ?\<nu>)
step ?\<phi> \<nu> = subst ?\<phi> (\<lambda>\<chi>. Some (step \<chi> \<nu>))

goal (1 subgoal):
 1. (((\<phi> \<longrightarrow>\<^sub>P \<psi> \<Longrightarrow> af_letter_opt \<phi> \<nu> \<longrightarrow>\<^sub>P af_letter_opt \<psi> \<nu>) &&& (\<phi> \<equiv>\<^sub>P \<psi> \<Longrightarrow> af_letter_opt \<phi> \<nu> \<equiv>\<^sub>P af_letter_opt \<psi> \<nu>)) &&& (\<phi> \<longrightarrow>\<^sub>P \<psi> \<Longrightarrow> af_G_letter_opt \<phi> \<nu> \<longrightarrow>\<^sub>P af_G_letter_opt \<psi> \<nu>) &&& (\<phi> \<equiv>\<^sub>P \<psi> \<Longrightarrow> af_G_letter_opt \<phi> \<nu> \<equiv>\<^sub>P af_G_letter_opt \<psi> \<nu>) &&& (\<phi> \<longrightarrow>\<^sub>P \<psi> \<Longrightarrow> step \<phi> \<nu> \<longrightarrow>\<^sub>P step \<psi> \<nu>)) &&& ((\<phi> \<equiv>\<^sub>P \<psi> \<Longrightarrow> step \<phi> \<nu> \<equiv>\<^sub>P step \<psi> \<nu>) &&& (\<phi> \<longrightarrow>\<^sub>P \<psi> \<Longrightarrow> Unf \<phi> \<longrightarrow>\<^sub>P Unf \<psi>)) &&& (\<phi> \<equiv>\<^sub>P \<psi> \<Longrightarrow> Unf \<phi> \<equiv>\<^sub>P Unf \<psi>) &&& (\<phi> \<longrightarrow>\<^sub>P \<psi> \<Longrightarrow> Unf\<^sub>G \<phi> \<longrightarrow>\<^sub>P Unf\<^sub>G \<psi>) &&& (\<phi> \<equiv>\<^sub>P \<psi> \<Longrightarrow> Unf\<^sub>G \<phi> \<equiv>\<^sub>P Unf\<^sub>G \<psi>)
[PROOF STEP]
using decomposable_function_subst[of Unf, simplified]
[PROOF STATE]
proof (prove)
using this:
Unf (step ?\<phi> \<nu>) = subst ?\<phi> (\<lambda>\<chi>. Some (Unf (step \<chi> \<nu>)))
af_letter_opt ?\<phi> ?\<nu> = Unf (step ?\<phi> ?\<nu>)
Unf\<^sub>G (step ?\<phi> \<nu>) = subst ?\<phi> (\<lambda>\<chi>. Some (Unf\<^sub>G (step \<chi> \<nu>)))
af_G_letter_opt ?\<phi> ?\<nu> = Unf\<^sub>G (step ?\<phi> ?\<nu>)
step ?\<phi> \<nu> = subst ?\<phi> (\<lambda>\<chi>. Some (step \<chi> \<nu>))
Unf ?\<phi> = subst ?\<phi> (\<lambda>\<chi>. Some (Unf \<chi>))

goal (1 subgoal):
 1. (((\<phi> \<longrightarrow>\<^sub>P \<psi> \<Longrightarrow> af_letter_opt \<phi> \<nu> \<longrightarrow>\<^sub>P af_letter_opt \<psi> \<nu>) &&& (\<phi> \<equiv>\<^sub>P \<psi> \<Longrightarrow> af_letter_opt \<phi> \<nu> \<equiv>\<^sub>P af_letter_opt \<psi> \<nu>)) &&& (\<phi> \<longrightarrow>\<^sub>P \<psi> \<Longrightarrow> af_G_letter_opt \<phi> \<nu> \<longrightarrow>\<^sub>P af_G_letter_opt \<psi> \<nu>) &&& (\<phi> \<equiv>\<^sub>P \<psi> \<Longrightarrow> af_G_letter_opt \<phi> \<nu> \<equiv>\<^sub>P af_G_letter_opt \<psi> \<nu>) &&& (\<phi> \<longrightarrow>\<^sub>P \<psi> \<Longrightarrow> step \<phi> \<nu> \<longrightarrow>\<^sub>P step \<psi> \<nu>)) &&& ((\<phi> \<equiv>\<^sub>P \<psi> \<Longrightarrow> step \<phi> \<nu> \<equiv>\<^sub>P step \<psi> \<nu>) &&& (\<phi> \<longrightarrow>\<^sub>P \<psi> \<Longrightarrow> Unf \<phi> \<longrightarrow>\<^sub>P Unf \<psi>)) &&& (\<phi> \<equiv>\<^sub>P \<psi> \<Longrightarrow> Unf \<phi> \<equiv>\<^sub>P Unf \<psi>) &&& (\<phi> \<longrightarrow>\<^sub>P \<psi> \<Longrightarrow> Unf\<^sub>G \<phi> \<longrightarrow>\<^sub>P Unf\<^sub>G \<psi>) &&& (\<phi> \<equiv>\<^sub>P \<psi> \<Longrightarrow> Unf\<^sub>G \<phi> \<equiv>\<^sub>P Unf\<^sub>G \<psi>)
[PROOF STEP]
using decomposable_function_subst[of Unf\<^sub>G, simplified]
[PROOF STATE]
proof (prove)
using this:
Unf (step ?\<phi> \<nu>) = subst ?\<phi> (\<lambda>\<chi>. Some (Unf (step \<chi> \<nu>)))
af_letter_opt ?\<phi> ?\<nu> = Unf (step ?\<phi> ?\<nu>)
Unf\<^sub>G (step ?\<phi> \<nu>) = subst ?\<phi> (\<lambda>\<chi>. Some (Unf\<^sub>G (step \<chi> \<nu>)))
af_G_letter_opt ?\<phi> ?\<nu> = Unf\<^sub>G (step ?\<phi> ?\<nu>)
step ?\<phi> \<nu> = subst ?\<phi> (\<lambda>\<chi>. Some (step \<chi> \<nu>))
Unf ?\<phi> = subst ?\<phi> (\<lambda>\<chi>. Some (Unf \<chi>))
Unf\<^sub>G ?\<phi> = subst ?\<phi> (\<lambda>\<chi>. Some (Unf\<^sub>G \<chi>))

goal (1 subgoal):
 1. (((\<phi> \<longrightarrow>\<^sub>P \<psi> \<Longrightarrow> af_letter_opt \<phi> \<nu> \<longrightarrow>\<^sub>P af_letter_opt \<psi> \<nu>) &&& (\<phi> \<equiv>\<^sub>P \<psi> \<Longrightarrow> af_letter_opt \<phi> \<nu> \<equiv>\<^sub>P af_letter_opt \<psi> \<nu>)) &&& (\<phi> \<longrightarrow>\<^sub>P \<psi> \<Longrightarrow> af_G_letter_opt \<phi> \<nu> \<longrightarrow>\<^sub>P af_G_letter_opt \<psi> \<nu>) &&& (\<phi> \<equiv>\<^sub>P \<psi> \<Longrightarrow> af_G_letter_opt \<phi> \<nu> \<equiv>\<^sub>P af_G_letter_opt \<psi> \<nu>) &&& (\<phi> \<longrightarrow>\<^sub>P \<psi> \<Longrightarrow> step \<phi> \<nu> \<longrightarrow>\<^sub>P step \<psi> \<nu>)) &&& ((\<phi> \<equiv>\<^sub>P \<psi> \<Longrightarrow> step \<phi> \<nu> \<equiv>\<^sub>P step \<psi> \<nu>) &&& (\<phi> \<longrightarrow>\<^sub>P \<psi> \<Longrightarrow> Unf \<phi> \<longrightarrow>\<^sub>P Unf \<psi>)) &&& (\<phi> \<equiv>\<^sub>P \<psi> \<Longrightarrow> Unf \<phi> \<equiv>\<^sub>P Unf \<psi>) &&& (\<phi> \<longrightarrow>\<^sub>P \<psi> \<Longrightarrow> Unf\<^sub>G \<phi> \<longrightarrow>\<^sub>P Unf\<^sub>G \<psi>) &&& (\<phi> \<equiv>\<^sub>P \<psi> \<Longrightarrow> Unf\<^sub>G \<phi> \<equiv>\<^sub>P Unf\<^sub>G \<psi>)
[PROOF STEP]
using subst_respects_ltl_prop_entailment
[PROOF STATE]
proof (prove)
using this:
Unf (step ?\<phi> \<nu>) = subst ?\<phi> (\<lambda>\<chi>. Some (Unf (step \<chi> \<nu>)))
af_letter_opt ?\<phi> ?\<nu> = Unf (step ?\<phi> ?\<nu>)
Unf\<^sub>G (step ?\<phi> \<nu>) = subst ?\<phi> (\<lambda>\<chi>. Some (Unf\<^sub>G (step \<chi> \<nu>)))
af_G_letter_opt ?\<phi> ?\<nu> = Unf\<^sub>G (step ?\<phi> ?\<nu>)
step ?\<phi> \<nu> = subst ?\<phi> (\<lambda>\<chi>. Some (step \<chi> \<nu>))
Unf ?\<phi> = subst ?\<phi> (\<lambda>\<chi>. Some (Unf \<chi>))
Unf\<^sub>G ?\<phi> = subst ?\<phi> (\<lambda>\<chi>. Some (Unf\<^sub>G \<chi>))
?\<phi> \<longrightarrow>\<^sub>P ?\<psi> \<Longrightarrow> subst ?\<phi> ?m \<longrightarrow>\<^sub>P subst ?\<psi> ?m
?\<phi> \<equiv>\<^sub>P ?\<psi> \<Longrightarrow> subst ?\<phi> ?m \<equiv>\<^sub>P subst ?\<psi> ?m

goal (1 subgoal):
 1. (((\<phi> \<longrightarrow>\<^sub>P \<psi> \<Longrightarrow> af_letter_opt \<phi> \<nu> \<longrightarrow>\<^sub>P af_letter_opt \<psi> \<nu>) &&& (\<phi> \<equiv>\<^sub>P \<psi> \<Longrightarrow> af_letter_opt \<phi> \<nu> \<equiv>\<^sub>P af_letter_opt \<psi> \<nu>)) &&& (\<phi> \<longrightarrow>\<^sub>P \<psi> \<Longrightarrow> af_G_letter_opt \<phi> \<nu> \<longrightarrow>\<^sub>P af_G_letter_opt \<psi> \<nu>) &&& (\<phi> \<equiv>\<^sub>P \<psi> \<Longrightarrow> af_G_letter_opt \<phi> \<nu> \<equiv>\<^sub>P af_G_letter_opt \<psi> \<nu>) &&& (\<phi> \<longrightarrow>\<^sub>P \<psi> \<Longrightarrow> step \<phi> \<nu> \<longrightarrow>\<^sub>P step \<psi> \<nu>)) &&& ((\<phi> \<equiv>\<^sub>P \<psi> \<Longrightarrow> step \<phi> \<nu> \<equiv>\<^sub>P step \<psi> \<nu>) &&& (\<phi> \<longrightarrow>\<^sub>P \<psi> \<Longrightarrow> Unf \<phi> \<longrightarrow>\<^sub>P Unf \<psi>)) &&& (\<phi> \<equiv>\<^sub>P \<psi> \<Longrightarrow> Unf \<phi> \<equiv>\<^sub>P Unf \<psi>) &&& (\<phi> \<longrightarrow>\<^sub>P \<psi> \<Longrightarrow> Unf\<^sub>G \<phi> \<longrightarrow>\<^sub>P Unf\<^sub>G \<psi>) &&& (\<phi> \<equiv>\<^sub>P \<psi> \<Longrightarrow> Unf\<^sub>G \<phi> \<equiv>\<^sub>P Unf\<^sub>G \<psi>)
[PROOF STEP]
by metis+


[STATEMENT]
lemma nested_propos:
  "nested_propos (step \<phi> \<nu>) \<subseteq> nested_propos \<phi>"
  "nested_propos (Unf \<phi>) \<subseteq> nested_propos \<phi>"
  "nested_propos (Unf\<^sub>G \<phi>) \<subseteq> nested_propos \<phi>"
  "nested_propos (af_letter_opt \<phi> \<nu>) \<subseteq> nested_propos \<phi>"
  "nested_propos (af_G_letter_opt \<phi> \<nu>) \<subseteq> nested_propos \<phi>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (nested_propos (step \<phi> \<nu>) \<subseteq> nested_propos \<phi> &&& nested_propos (Unf \<phi>) \<subseteq> nested_propos \<phi>) &&& nested_propos (Unf\<^sub>G \<phi>) \<subseteq> nested_propos \<phi> &&& nested_propos (af_letter_opt \<phi> \<nu>) \<subseteq> nested_propos \<phi> &&& nested_propos (af_G_letter_opt \<phi> \<nu>) \<subseteq> nested_propos \<phi>
[PROOF STEP]
by (induction \<phi>) auto


[STATEMENT]
lemma af_G_letter_opt_sat_core:
  "Only_G \<G> \<Longrightarrow> \<G> \<Turnstile>\<^sub>P \<phi> \<Longrightarrow> \<G> \<Turnstile>\<^sub>P af_G_letter_opt \<phi> \<nu>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Only_G \<G>; \<G> \<Turnstile>\<^sub>P \<phi>\<rbrakk> \<Longrightarrow> \<G> \<Turnstile>\<^sub>P af_G_letter_opt \<phi> \<nu>
[PROOF STEP]
by (induction \<phi>) auto


[STATEMENT]
lemma af_G_letter_sat_core_lifted:
  "Only_G \<G> \<Longrightarrow> \<G> \<Turnstile>\<^sub>P Rep \<phi> \<Longrightarrow> \<G> \<Turnstile>\<^sub>P Rep (af_G_letter_abs \<phi> \<nu>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Only_G \<G>; \<G> \<Turnstile>\<^sub>P Rep \<phi>\<rbrakk> \<Longrightarrow> \<G> \<Turnstile>\<^sub>P Rep (\<up>af\<^sub>G \<phi> \<nu>)
[PROOF STEP]
by (metis af_G_letter_sat_core Quotient_ltl_prop_equiv_quotient[THEN Quotient_rep_abs] Quotient3_ltl_prop_equiv_quotient[THEN Quotient3_abs_rep] af_G_abs.f_abs.abs_eq ltl_prop_equiv_def af_G_letter_abs_def)


[STATEMENT]
lemma af_G_letter_opt_sat_core_lifted:
  "Only_G \<G> \<Longrightarrow> \<G> \<Turnstile>\<^sub>P Rep \<phi> \<Longrightarrow> \<G> \<Turnstile>\<^sub>P Rep (\<up>af\<^sub>G\<^sub>\<UU> \<phi> \<nu>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Only_G \<G>; \<G> \<Turnstile>\<^sub>P Rep \<phi>\<rbrakk> \<Longrightarrow> \<G> \<Turnstile>\<^sub>P Rep (\<up>af\<^sub>G\<^sub>\<UU> \<phi> \<nu>)
[PROOF STEP]
unfolding af_G_letter_abs_opt_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Only_G \<G>; \<G> \<Turnstile>\<^sub>P Rep \<phi>\<rbrakk> \<Longrightarrow> \<G> \<Turnstile>\<^sub>P Rep (af_G_abs_opt.f_abs \<phi> \<nu>)
[PROOF STEP]
by (metis af_G_letter_opt_sat_core Quotient_ltl_prop_equiv_quotient[THEN Quotient_rep_abs] Quotient3_ltl_prop_equiv_quotient[THEN Quotient3_abs_rep] af_G_abs_opt.f_abs.abs_eq ltl_prop_equiv_def)


[STATEMENT]
lemma af_G_letter_abs_opt_split:
  "\<up>Unf\<^sub>G (\<up>step \<Phi> \<nu>) = \<up>af\<^sub>G\<^sub>\<UU> \<Phi> \<nu>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<up>Unf\<^sub>G (\<up>step \<Phi> \<nu>) = \<up>af\<^sub>G\<^sub>\<UU> \<Phi> \<nu>
[PROOF STEP]
unfolding af_G_letter_abs_opt_def step_abs_def comp_def af_G_abs_opt.f_abs_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<up>Unf\<^sub>G (map_fun Rep (map_fun id Abs) step \<Phi> \<nu>) = map_fun Rep (map_fun id Abs) af_G_letter_opt \<Phi> \<nu>
[PROOF STEP]
using map_fun_apply Unf\<^sub>G_abs.abs_eq af_G_letter_opt.simps
[PROOF STATE]
proof (prove)
using this:
map_fun ?f ?g ?h ?x = ?g (?h (?f ?x))
\<up>Unf\<^sub>G (Abs ?x) = Abs (Unf\<^sub>G ?x)
af_G_letter_opt ?\<phi> ?\<nu> = Unf\<^sub>G (step ?\<phi> ?\<nu>)

goal (1 subgoal):
 1. \<up>Unf\<^sub>G (map_fun Rep (map_fun id Abs) step \<Phi> \<nu>) = map_fun Rep (map_fun id Abs) af_G_letter_opt \<Phi> \<nu>
[PROOF STEP]
by auto


[STATEMENT]
lemma af_unfold:
  "\<up>af = (\<lambda>\<phi> \<nu>. \<up>step (\<up>Unf \<phi>) \<nu>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<up>af = (\<lambda>\<phi>. \<up>step (\<up>Unf \<phi>))
[PROOF STEP]
by (metis Unf_abs_def af_abs.f_abs.abs_eq af_letter_abs_def af_letter_alt_def(1) ltl\<^sub>P_abs_rep map_fun_apply step_abs.abs_eq)


[STATEMENT]
lemma af_opt_unfold:
  "\<up>af\<^sub>\<UU> = (\<lambda>\<phi> \<nu>. \<up>Unf (\<up>step \<phi> \<nu>))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<up>af\<^sub>\<UU> = (\<lambda>\<phi> \<nu>. \<up>Unf (\<up>step \<phi> \<nu>))
[PROOF STEP]
by (metis (no_types, lifting) Quotient3_abs_rep Quotient3_ltl_prop_equiv_quotient Unf_abs.abs_eq af_abs_opt.f_abs.abs_eq af_letter_abs_opt_def af_letter_opt.elims id_apply map_fun_apply  step_abs_def)


[STATEMENT]
lemma af_abs_equiv:
  "foldl \<up>af \<psi> (xs @ [x]) = \<up>step (foldl \<up>af\<^sub>\<UU> (\<up>Unf \<psi>) xs) x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. foldl \<up>af \<psi> (xs @ [x]) = \<up>step (foldl \<up>af\<^sub>\<UU> (\<up>Unf \<psi>) xs) x
[PROOF STEP]
unfolding af_unfold af_opt_unfold
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. foldl (\<lambda>\<phi>. \<up>step (\<up>Unf \<phi>)) \<psi> (xs @ [x]) = \<up>step (foldl (\<lambda>\<phi> \<nu>. \<up>Unf (\<up>step \<phi> \<nu>)) (\<up>Unf \<psi>) xs) x
[PROOF STEP]
by (induction xs arbitrary: x \<psi> rule: rev_induct) simp+


[STATEMENT]
lemma Rep_Abs_equiv:
  "Rep (Abs \<phi>) \<equiv>\<^sub>P \<phi>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Rep (Abs \<phi>) \<equiv>\<^sub>P \<phi>
[PROOF STEP]
using Rep_Abs_prop_entailment
[PROOF STATE]
proof (prove)
using this:
?A \<Turnstile>\<^sub>P Rep (Abs ?\<phi>) = ?A \<Turnstile>\<^sub>P ?\<phi>

goal (1 subgoal):
 1. Rep (Abs \<phi>) \<equiv>\<^sub>P \<phi>
[PROOF STEP]
unfolding ltl_prop_equiv_def
[PROOF STATE]
proof (prove)
using this:
?A \<Turnstile>\<^sub>P Rep (Abs ?\<phi>) = ?A \<Turnstile>\<^sub>P ?\<phi>

goal (1 subgoal):
 1. \<forall>\<A>. \<A> \<Turnstile>\<^sub>P Rep (Abs \<phi>) = \<A> \<Turnstile>\<^sub>P \<phi>
[PROOF STEP]
by auto


[STATEMENT]
lemma Rep_step:
  "Rep (\<up>step \<Phi> \<nu>) \<equiv>\<^sub>P step (Rep \<Phi>) \<nu>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Rep (\<up>step \<Phi> \<nu>) \<equiv>\<^sub>P step (Rep \<Phi>) \<nu>
[PROOF STEP]
by (metis Quotient3_abs_rep Quotient3_ltl_prop_equiv_quotient ltl_prop_equiv_quotient.abs_eq_iff step_abs.abs_eq)


[STATEMENT]
lemma step_\<G>:
  "Only_G \<G> \<Longrightarrow> \<G> \<Turnstile>\<^sub>P \<phi> \<Longrightarrow> \<G> \<Turnstile>\<^sub>P step \<phi> \<nu>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Only_G \<G>; \<G> \<Turnstile>\<^sub>P \<phi>\<rbrakk> \<Longrightarrow> \<G> \<Turnstile>\<^sub>P step \<phi> \<nu>
[PROOF STEP]
by (induction \<phi>) auto


[STATEMENT]
lemma Unf\<^sub>G_\<G>:
  "Only_G \<G> \<Longrightarrow> \<G> \<Turnstile>\<^sub>P \<phi> \<Longrightarrow> \<G> \<Turnstile>\<^sub>P Unf\<^sub>G \<phi>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Only_G \<G>; \<G> \<Turnstile>\<^sub>P \<phi>\<rbrakk> \<Longrightarrow> \<G> \<Turnstile>\<^sub>P Unf\<^sub>G \<phi>
[PROOF STEP]
by (induction \<phi>) auto


[STATEMENT]
lemma Abs_lst1_fcb:
  fixes x y :: "'a :: at"
    and S T :: "'b :: fs"
  assumes e: "[[atom x]]lst. T = [[atom y]]lst. S"
  and f1: "\<lbrakk>x \<noteq> y; atom y \<sharp> T; atom x \<sharp> (y \<leftrightarrow> x) \<bullet> T\<rbrakk> \<Longrightarrow> atom x \<sharp> f x T"
  and f2: "\<lbrakk>x \<noteq> y; atom y \<sharp> T; atom x \<sharp> (y \<leftrightarrow> x) \<bullet> T\<rbrakk> \<Longrightarrow> atom y \<sharp> f x T"
  and p: "\<lbrakk>S = (x \<leftrightarrow> y) \<bullet> T; x \<noteq> y; atom y \<sharp> T; atom x \<sharp> S\<rbrakk>
    \<Longrightarrow> (x \<leftrightarrow> y) \<bullet> (f x T) = f y S"
  shows "f x T = f y S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f x T = f y S
[PROOF STEP]
using e
[PROOF STATE]
proof (prove)
using this:
[[atom x]]lst. T = [[atom y]]lst. S

goal (1 subgoal):
 1. f x T = f y S
[PROOF STEP]
apply(case_tac "atom x \<sharp> S")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>[[atom x]]lst. T = [[atom y]]lst. S; atom x \<sharp> S\<rbrakk> \<Longrightarrow> f x T = f y S
 2. \<lbrakk>[[atom x]]lst. T = [[atom y]]lst. S; \<not> atom x \<sharp> S\<rbrakk> \<Longrightarrow> f x T = f y S
[PROOF STEP]
apply(simp add: Abs1_eq_iff')
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>x = y \<and> T = S \<or> x \<noteq> y \<and> (y \<leftrightarrow> x) \<bullet> T = S \<and> atom y \<sharp> T; atom x \<sharp> S\<rbrakk> \<Longrightarrow> f x T = f y S
 2. \<lbrakk>[[atom x]]lst. T = [[atom y]]lst. S; \<not> atom x \<sharp> S\<rbrakk> \<Longrightarrow> f x T = f y S
[PROOF STEP]
apply(elim conjE disjE)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>atom x \<sharp> S; x = y; T = S\<rbrakk> \<Longrightarrow> f x T = f y S
 2. \<lbrakk>atom x \<sharp> S; x \<noteq> y; (y \<leftrightarrow> x) \<bullet> T = S; atom y \<sharp> T\<rbrakk> \<Longrightarrow> f x T = f y S
 3. \<lbrakk>[[atom x]]lst. T = [[atom y]]lst. S; \<not> atom x \<sharp> S\<rbrakk> \<Longrightarrow> f x T = f y S
[PROOF STEP]
apply(simp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>atom x \<sharp> S; x \<noteq> y; (y \<leftrightarrow> x) \<bullet> T = S; atom y \<sharp> T\<rbrakk> \<Longrightarrow> f x T = f y S
 2. \<lbrakk>[[atom x]]lst. T = [[atom y]]lst. S; \<not> atom x \<sharp> S\<rbrakk> \<Longrightarrow> f x T = f y S
[PROOF STEP]
apply(rule trans)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>atom x \<sharp> S; x \<noteq> y; (y \<leftrightarrow> x) \<bullet> T = S; atom y \<sharp> T\<rbrakk> \<Longrightarrow> f x T = ?s6
 2. \<lbrakk>atom x \<sharp> S; x \<noteq> y; (y \<leftrightarrow> x) \<bullet> T = S; atom y \<sharp> T\<rbrakk> \<Longrightarrow> ?s6 = f y S
 3. \<lbrakk>[[atom x]]lst. T = [[atom y]]lst. S; \<not> atom x \<sharp> S\<rbrakk> \<Longrightarrow> f x T = f y S
[PROOF STEP]
apply(rule_tac p="(x \<leftrightarrow> y)" in supp_perm_eq[symmetric])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>atom x \<sharp> S; x \<noteq> y; (y \<leftrightarrow> x) \<bullet> T = S; atom y \<sharp> T\<rbrakk> \<Longrightarrow> supp (f x T) \<sharp>* (x \<leftrightarrow> y)
 2. \<lbrakk>atom x \<sharp> S; x \<noteq> y; (y \<leftrightarrow> x) \<bullet> T = S; atom y \<sharp> T\<rbrakk> \<Longrightarrow> (x \<leftrightarrow> y) \<bullet> f x T = f y S
 3. \<lbrakk>[[atom x]]lst. T = [[atom y]]lst. S; \<not> atom x \<sharp> S\<rbrakk> \<Longrightarrow> f x T = f y S
[PROOF STEP]
apply(rule fresh_star_supp_conv)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>atom x \<sharp> S; x \<noteq> y; (y \<leftrightarrow> x) \<bullet> T = S; atom y \<sharp> T\<rbrakk> \<Longrightarrow> supp (x \<leftrightarrow> y) \<sharp>* f x T
 2. \<lbrakk>atom x \<sharp> S; x \<noteq> y; (y \<leftrightarrow> x) \<bullet> T = S; atom y \<sharp> T\<rbrakk> \<Longrightarrow> (x \<leftrightarrow> y) \<bullet> f x T = f y S
 3. \<lbrakk>[[atom x]]lst. T = [[atom y]]lst. S; \<not> atom x \<sharp> S\<rbrakk> \<Longrightarrow> f x T = f y S
[PROOF STEP]
apply(simp add: flip_def supp_swap fresh_star_def f1 f2)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>atom x \<sharp> S; x \<noteq> y; (y \<leftrightarrow> x) \<bullet> T = S; atom y \<sharp> T\<rbrakk> \<Longrightarrow> (x \<leftrightarrow> y) \<bullet> f x T = f y S
 2. \<lbrakk>[[atom x]]lst. T = [[atom y]]lst. S; \<not> atom x \<sharp> S\<rbrakk> \<Longrightarrow> f x T = f y S
[PROOF STEP]
apply(simp add: flip_commute p)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>[[atom x]]lst. T = [[atom y]]lst. S; \<not> atom x \<sharp> S\<rbrakk> \<Longrightarrow> f x T = f y S
[PROOF STEP]
apply(simp add: Abs1_eq_iff)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done