[STATEMENT]
lemma af_implies_af\<^sub>G:
  "S \<Turnstile>\<^sub>P af \<phi> w \<Longrightarrow> S \<Turnstile>\<^sub>P af\<^sub>G \<phi> w"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. S \<Turnstile>\<^sub>P af \<phi> w \<Longrightarrow> S \<Turnstile>\<^sub>P af\<^sub>G \<phi> w
[PROOF STEP]
proof (induction w arbitrary: S rule: rev_induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>S. S \<Turnstile>\<^sub>P af \<phi> [] \<Longrightarrow> S \<Turnstile>\<^sub>P af\<^sub>G \<phi> []
 2. \<And>x xs S. \<lbrakk>\<And>S. S \<Turnstile>\<^sub>P af \<phi> xs \<Longrightarrow> S \<Turnstile>\<^sub>P af\<^sub>G \<phi> xs; S \<Turnstile>\<^sub>P af \<phi> (xs @ [x])\<rbrakk> \<Longrightarrow> S \<Turnstile>\<^sub>P af\<^sub>G \<phi> (xs @ [x])
[PROOF STEP]
case (snoc x xs)
[PROOF STATE]
proof (state)
this:
?S \<Turnstile>\<^sub>P af \<phi> xs \<Longrightarrow> ?S \<Turnstile>\<^sub>P af\<^sub>G \<phi> xs
S \<Turnstile>\<^sub>P af \<phi> (xs @ [x])

goal (2 subgoals):
 1. \<And>S. S \<Turnstile>\<^sub>P af \<phi> [] \<Longrightarrow> S \<Turnstile>\<^sub>P af\<^sub>G \<phi> []
 2. \<And>x xs S. \<lbrakk>\<And>S. S \<Turnstile>\<^sub>P af \<phi> xs \<Longrightarrow> S \<Turnstile>\<^sub>P af\<^sub>G \<phi> xs; S \<Turnstile>\<^sub>P af \<phi> (xs @ [x])\<rbrakk> \<Longrightarrow> S \<Turnstile>\<^sub>P af\<^sub>G \<phi> (xs @ [x])
[PROOF STEP]
hence "S \<Turnstile>\<^sub>P af_letter (af \<phi> xs) x"
[PROOF STATE]
proof (prove)
using this:
?S \<Turnstile>\<^sub>P af \<phi> xs \<Longrightarrow> ?S \<Turnstile>\<^sub>P af\<^sub>G \<phi> xs
S \<Turnstile>\<^sub>P af \<phi> (xs @ [x])

goal (1 subgoal):
 1. S \<Turnstile>\<^sub>P af_letter (af \<phi> xs) x
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
S \<Turnstile>\<^sub>P af_letter (af \<phi> xs) x

goal (2 subgoals):
 1. \<And>S. S \<Turnstile>\<^sub>P af \<phi> [] \<Longrightarrow> S \<Turnstile>\<^sub>P af\<^sub>G \<phi> []
 2. \<And>x xs S. \<lbrakk>\<And>S. S \<Turnstile>\<^sub>P af \<phi> xs \<Longrightarrow> S \<Turnstile>\<^sub>P af\<^sub>G \<phi> xs; S \<Turnstile>\<^sub>P af \<phi> (xs @ [x])\<rbrakk> \<Longrightarrow> S \<Turnstile>\<^sub>P af\<^sub>G \<phi> (xs @ [x])
[PROOF STEP]
hence "S \<Turnstile>\<^sub>P af_letter (af\<^sub>G \<phi> xs) x"
[PROOF STATE]
proof (prove)
using this:
S \<Turnstile>\<^sub>P af_letter (af \<phi> xs) x

goal (1 subgoal):
 1. S \<Turnstile>\<^sub>P af_letter (af\<^sub>G \<phi> xs) x
[PROOF STEP]
using af_respectfulness(1) snoc.IH
[PROOF STATE]
proof (prove)
using this:
S \<Turnstile>\<^sub>P af_letter (af \<phi> xs) x
?\<phi> \<longrightarrow>\<^sub>P ?\<psi> \<Longrightarrow> af_letter ?\<phi> ?\<nu> \<longrightarrow>\<^sub>P af_letter ?\<psi> ?\<nu>
?S \<Turnstile>\<^sub>P af \<phi> xs \<Longrightarrow> ?S \<Turnstile>\<^sub>P af\<^sub>G \<phi> xs

goal (1 subgoal):
 1. S \<Turnstile>\<^sub>P af_letter (af\<^sub>G \<phi> xs) x
[PROOF STEP]
unfolding ltl_prop_implies_def
[PROOF STATE]
proof (prove)
using this:
S \<Turnstile>\<^sub>P af_letter (af \<phi> xs) x
\<forall>\<A>. \<A> \<Turnstile>\<^sub>P ?\<phi> \<longrightarrow> \<A> \<Turnstile>\<^sub>P ?\<psi> \<Longrightarrow> \<forall>\<A>. \<A> \<Turnstile>\<^sub>P af_letter ?\<phi> ?\<nu> \<longrightarrow> \<A> \<Turnstile>\<^sub>P af_letter ?\<psi> ?\<nu>
?S \<Turnstile>\<^sub>P af \<phi> xs \<Longrightarrow> ?S \<Turnstile>\<^sub>P af\<^sub>G \<phi> xs

goal (1 subgoal):
 1. S \<Turnstile>\<^sub>P af_letter (af\<^sub>G \<phi> xs) x
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
S \<Turnstile>\<^sub>P af_letter (af\<^sub>G \<phi> xs) x

goal (2 subgoals):
 1. \<And>S. S \<Turnstile>\<^sub>P af \<phi> [] \<Longrightarrow> S \<Turnstile>\<^sub>P af\<^sub>G \<phi> []
 2. \<And>x xs S. \<lbrakk>\<And>S. S \<Turnstile>\<^sub>P af \<phi> xs \<Longrightarrow> S \<Turnstile>\<^sub>P af\<^sub>G \<phi> xs; S \<Turnstile>\<^sub>P af \<phi> (xs @ [x])\<rbrakk> \<Longrightarrow> S \<Turnstile>\<^sub>P af\<^sub>G \<phi> (xs @ [x])
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
S \<Turnstile>\<^sub>P af_letter (af\<^sub>G \<phi> xs) x

goal (2 subgoals):
 1. \<And>S. S \<Turnstile>\<^sub>P af \<phi> [] \<Longrightarrow> S \<Turnstile>\<^sub>P af\<^sub>G \<phi> []
 2. \<And>x xs S. \<lbrakk>\<And>S. S \<Turnstile>\<^sub>P af \<phi> xs \<Longrightarrow> S \<Turnstile>\<^sub>P af\<^sub>G \<phi> xs; S \<Turnstile>\<^sub>P af \<phi> (xs @ [x])\<rbrakk> \<Longrightarrow> S \<Turnstile>\<^sub>P af\<^sub>G \<phi> (xs @ [x])
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
S \<Turnstile>\<^sub>P af_letter (af\<^sub>G \<phi> xs) x

goal (2 subgoals):
 1. \<And>S. S \<Turnstile>\<^sub>P af \<phi> [] \<Longrightarrow> S \<Turnstile>\<^sub>P af\<^sub>G \<phi> []
 2. \<And>x xs S. \<lbrakk>\<And>S. S \<Turnstile>\<^sub>P af \<phi> xs \<Longrightarrow> S \<Turnstile>\<^sub>P af\<^sub>G \<phi> xs; S \<Turnstile>\<^sub>P af \<phi> (xs @ [x])\<rbrakk> \<Longrightarrow> S \<Turnstile>\<^sub>P af\<^sub>G \<phi> (xs @ [x])
[PROOF STEP]
fix \<phi>
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>S. S \<Turnstile>\<^sub>P af \<phi> [] \<Longrightarrow> S \<Turnstile>\<^sub>P af\<^sub>G \<phi> []
 2. \<And>x xs S. \<lbrakk>\<And>S. S \<Turnstile>\<^sub>P af \<phi> xs \<Longrightarrow> S \<Turnstile>\<^sub>P af\<^sub>G \<phi> xs; S \<Turnstile>\<^sub>P af \<phi> (xs @ [x])\<rbrakk> \<Longrightarrow> S \<Turnstile>\<^sub>P af\<^sub>G \<phi> (xs @ [x])
[PROOF STEP]
have "\<And>\<nu>. S \<Turnstile>\<^sub>P af_letter \<phi> \<nu> \<Longrightarrow> S \<Turnstile>\<^sub>P af_G_letter \<phi> \<nu>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>\<nu>. S \<Turnstile>\<^sub>P af_letter \<phi> \<nu> \<Longrightarrow> S \<Turnstile>\<^sub>P af_G_letter \<phi> \<nu>
[PROOF STEP]
by (induction \<phi>) auto
[PROOF STATE]
proof (state)
this:
S \<Turnstile>\<^sub>P af_letter \<phi> ?\<nu> \<Longrightarrow> S \<Turnstile>\<^sub>P af_G_letter \<phi> ?\<nu>

goal (2 subgoals):
 1. \<And>S. S \<Turnstile>\<^sub>P af \<phi> [] \<Longrightarrow> S \<Turnstile>\<^sub>P af\<^sub>G \<phi> []
 2. \<And>x xs S. \<lbrakk>\<And>S. S \<Turnstile>\<^sub>P af \<phi> xs \<Longrightarrow> S \<Turnstile>\<^sub>P af\<^sub>G \<phi> xs; S \<Turnstile>\<^sub>P af \<phi> (xs @ [x])\<rbrakk> \<Longrightarrow> S \<Turnstile>\<^sub>P af\<^sub>G \<phi> (xs @ [x])
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
S \<Turnstile>\<^sub>P af_letter ?\<phi>'3 ?\<nu> \<Longrightarrow> S \<Turnstile>\<^sub>P af_G_letter ?\<phi>'3 ?\<nu>

goal (2 subgoals):
 1. \<And>S. S \<Turnstile>\<^sub>P af \<phi> [] \<Longrightarrow> S \<Turnstile>\<^sub>P af\<^sub>G \<phi> []
 2. \<And>x xs S. \<lbrakk>\<And>S. S \<Turnstile>\<^sub>P af \<phi> xs \<Longrightarrow> S \<Turnstile>\<^sub>P af\<^sub>G \<phi> xs; S \<Turnstile>\<^sub>P af \<phi> (xs @ [x])\<rbrakk> \<Longrightarrow> S \<Turnstile>\<^sub>P af\<^sub>G \<phi> (xs @ [x])
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
S \<Turnstile>\<^sub>P af_letter (af\<^sub>G \<phi> xs) x
S \<Turnstile>\<^sub>P af_letter ?\<phi>'3 ?\<nu> \<Longrightarrow> S \<Turnstile>\<^sub>P af_G_letter ?\<phi>'3 ?\<nu>
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
S \<Turnstile>\<^sub>P af_letter (af\<^sub>G \<phi> xs) x
S \<Turnstile>\<^sub>P af_letter ?\<phi>'3 ?\<nu> \<Longrightarrow> S \<Turnstile>\<^sub>P af_G_letter ?\<phi>'3 ?\<nu>

goal (1 subgoal):
 1. S \<Turnstile>\<^sub>P af\<^sub>G \<phi> (xs @ [x])
[PROOF STEP]
using snoc.prems foldl_append
[PROOF STATE]
proof (prove)
using this:
S \<Turnstile>\<^sub>P af_letter (af\<^sub>G \<phi> xs) x
S \<Turnstile>\<^sub>P af_letter ?\<phi>'3 ?\<nu> \<Longrightarrow> S \<Turnstile>\<^sub>P af_G_letter ?\<phi>'3 ?\<nu>
S \<Turnstile>\<^sub>P af \<phi> (xs @ [x])
foldl ?f ?a (?xs @ ?ys) = foldl ?f (foldl ?f ?a ?xs) ?ys

goal (1 subgoal):
 1. S \<Turnstile>\<^sub>P af\<^sub>G \<phi> (xs @ [x])
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
S \<Turnstile>\<^sub>P af\<^sub>G \<phi> (xs @ [x])

goal (1 subgoal):
 1. \<And>S. S \<Turnstile>\<^sub>P af \<phi> [] \<Longrightarrow> S \<Turnstile>\<^sub>P af\<^sub>G \<phi> []
[PROOF STEP]
qed simp


[STATEMENT]
lemma af_implies_af\<^sub>G_2:
  "w \<Turnstile> af \<phi> xs \<Longrightarrow> w \<Turnstile> af\<^sub>G \<phi> xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. w \<Turnstile> af \<phi> xs \<Longrightarrow> w \<Turnstile> af\<^sub>G \<phi> xs
[PROOF STEP]
by (metis ltl_prop_implication_implies_ltl_implication af_implies_af\<^sub>G ltl_prop_implies_def)