[STATEMENT]
lemma closed_\<G>\<^sub>F\<^sub>G:
  "closed (\<G>\<^sub>F\<^sub>G \<phi> w) w"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. closed (\<G>\<^sub>F\<^sub>G \<phi> w) w
[PROOF STEP]
proof (induction \<phi>)
[PROOF STATE]
proof (state)
goal (10 subgoals):
 1. closed (\<G>\<^sub>F\<^sub>G true w) w
 2. closed (\<G>\<^sub>F\<^sub>G false w) w
 3. \<And>x. closed (\<G>\<^sub>F\<^sub>G p(x) w) w
 4. \<And>x. closed (\<G>\<^sub>F\<^sub>G (np(x)) w) w
 5. \<And>\<phi>1 \<phi>2. \<lbrakk>closed (\<G>\<^sub>F\<^sub>G \<phi>1 w) w; closed (\<G>\<^sub>F\<^sub>G \<phi>2 w) w\<rbrakk> \<Longrightarrow> closed (\<G>\<^sub>F\<^sub>G (\<phi>1 and \<phi>2) w) w
 6. \<And>\<phi>1 \<phi>2. \<lbrakk>closed (\<G>\<^sub>F\<^sub>G \<phi>1 w) w; closed (\<G>\<^sub>F\<^sub>G \<phi>2 w) w\<rbrakk> \<Longrightarrow> closed (\<G>\<^sub>F\<^sub>G (\<phi>1 or \<phi>2) w) w
 7. \<And>\<phi>. closed (\<G>\<^sub>F\<^sub>G \<phi> w) w \<Longrightarrow> closed (\<G>\<^sub>F\<^sub>G (X \<phi>) w) w
 8. \<And>\<phi>. closed (\<G>\<^sub>F\<^sub>G \<phi> w) w \<Longrightarrow> closed (\<G>\<^sub>F\<^sub>G (G \<phi>) w) w
 9. \<And>\<phi>. closed (\<G>\<^sub>F\<^sub>G \<phi> w) w \<Longrightarrow> closed (\<G>\<^sub>F\<^sub>G (F \<phi>) w) w
 10. \<And>\<phi>1 \<phi>2. \<lbrakk>closed (\<G>\<^sub>F\<^sub>G \<phi>1 w) w; closed (\<G>\<^sub>F\<^sub>G \<phi>2 w) w\<rbrakk> \<Longrightarrow> closed (\<G>\<^sub>F\<^sub>G (\<phi>1 U \<phi>2) w) w
[PROOF STEP]
case (LTLGlobal \<phi>)
[PROOF STATE]
proof (state)
this:
closed (\<G>\<^sub>F\<^sub>G \<phi> w) w

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

goal (1 subgoal):
 1. closed (\<G>\<^sub>F\<^sub>G (G \<phi>) w) w
[PROOF STEP]
proof (cases "w \<Turnstile> F G \<phi>")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>closed (\<G>\<^sub>F\<^sub>G \<phi> w) w; w \<Turnstile> F G \<phi>\<rbrakk> \<Longrightarrow> closed (\<G>\<^sub>F\<^sub>G (G \<phi>) w) w
 2. \<lbrakk>closed (\<G>\<^sub>F\<^sub>G \<phi> w) w; \<not> w \<Turnstile> F G \<phi>\<rbrakk> \<Longrightarrow> closed (\<G>\<^sub>F\<^sub>G (G \<phi>) w) w
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
w \<Turnstile> F G \<phi>

goal (2 subgoals):
 1. \<lbrakk>closed (\<G>\<^sub>F\<^sub>G \<phi> w) w; w \<Turnstile> F G \<phi>\<rbrakk> \<Longrightarrow> closed (\<G>\<^sub>F\<^sub>G (G \<phi>) w) w
 2. \<lbrakk>closed (\<G>\<^sub>F\<^sub>G \<phi> w) w; \<not> w \<Turnstile> F G \<phi>\<rbrakk> \<Longrightarrow> closed (\<G>\<^sub>F\<^sub>G (G \<phi>) w) w
[PROOF STEP]
hence "\<forall>\<^sub>\<infinity>i. suffix i w \<Turnstile> \<phi>"
[PROOF STATE]
proof (prove)
using this:
w \<Turnstile> F G \<phi>

goal (1 subgoal):
 1. \<forall>\<^sub>\<infinity>i. suffix i w \<Turnstile> \<phi>
[PROOF STEP]
using LTL_FG_almost_all_suffixes
[PROOF STATE]
proof (prove)
using this:
w \<Turnstile> F G \<phi>
?w \<Turnstile> F G ?\<phi> = (\<forall>\<^sub>\<infinity>i. suffix i ?w \<Turnstile> ?\<phi>)

goal (1 subgoal):
 1. \<forall>\<^sub>\<infinity>i. suffix i w \<Turnstile> \<phi>
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<forall>\<^sub>\<infinity>i. suffix i w \<Turnstile> \<phi>

goal (2 subgoals):
 1. \<lbrakk>closed (\<G>\<^sub>F\<^sub>G \<phi> w) w; w \<Turnstile> F G \<phi>\<rbrakk> \<Longrightarrow> closed (\<G>\<^sub>F\<^sub>G (G \<phi>) w) w
 2. \<lbrakk>closed (\<G>\<^sub>F\<^sub>G \<phi> w) w; \<not> w \<Turnstile> F G \<phi>\<rbrakk> \<Longrightarrow> closed (\<G>\<^sub>F\<^sub>G (G \<phi>) w) w
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>\<^sub>\<infinity>i. suffix i w \<Turnstile> \<phi>
[PROOF STEP]
obtain i where "\<forall>j \<ge> i. suffix j w \<Turnstile> \<phi>"
[PROOF STATE]
proof (prove)
using this:
\<forall>\<^sub>\<infinity>i. suffix i w \<Turnstile> \<phi>

goal (1 subgoal):
 1. (\<And>i. \<forall>j\<ge>i. suffix j w \<Turnstile> \<phi> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding MOST_nat_le
[PROOF STATE]
proof (prove)
using this:
\<exists>m. \<forall>n\<ge>m. suffix n w \<Turnstile> \<phi>

goal (1 subgoal):
 1. (\<And>i. \<forall>j\<ge>i. suffix j w \<Turnstile> \<phi> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<forall>j\<ge>i. suffix j w \<Turnstile> \<phi>

goal (2 subgoals):
 1. \<lbrakk>closed (\<G>\<^sub>F\<^sub>G \<phi> w) w; w \<Turnstile> F G \<phi>\<rbrakk> \<Longrightarrow> closed (\<G>\<^sub>F\<^sub>G (G \<phi>) w) w
 2. \<lbrakk>closed (\<G>\<^sub>F\<^sub>G \<phi> w) w; \<not> w \<Turnstile> F G \<phi>\<rbrakk> \<Longrightarrow> closed (\<G>\<^sub>F\<^sub>G (G \<phi>) w) w
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
\<forall>j\<ge>i. suffix j w \<Turnstile> \<phi>

goal (2 subgoals):
 1. \<lbrakk>closed (\<G>\<^sub>F\<^sub>G \<phi> w) w; w \<Turnstile> F G \<phi>\<rbrakk> \<Longrightarrow> closed (\<G>\<^sub>F\<^sub>G (G \<phi>) w) w
 2. \<lbrakk>closed (\<G>\<^sub>F\<^sub>G \<phi> w) w; \<not> w \<Turnstile> F G \<phi>\<rbrakk> \<Longrightarrow> closed (\<G>\<^sub>F\<^sub>G (G \<phi>) w) w
[PROOF STEP]
fix k
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>closed (\<G>\<^sub>F\<^sub>G \<phi> w) w; w \<Turnstile> F G \<phi>\<rbrakk> \<Longrightarrow> closed (\<G>\<^sub>F\<^sub>G (G \<phi>) w) w
 2. \<lbrakk>closed (\<G>\<^sub>F\<^sub>G \<phi> w) w; \<not> w \<Turnstile> F G \<phi>\<rbrakk> \<Longrightarrow> closed (\<G>\<^sub>F\<^sub>G (G \<phi>) w) w
[PROOF STEP]
assume "k \<ge> i"
[PROOF STATE]
proof (state)
this:
i \<le> k

goal (2 subgoals):
 1. \<lbrakk>closed (\<G>\<^sub>F\<^sub>G \<phi> w) w; w \<Turnstile> F G \<phi>\<rbrakk> \<Longrightarrow> closed (\<G>\<^sub>F\<^sub>G (G \<phi>) w) w
 2. \<lbrakk>closed (\<G>\<^sub>F\<^sub>G \<phi> w) w; \<not> w \<Turnstile> F G \<phi>\<rbrakk> \<Longrightarrow> closed (\<G>\<^sub>F\<^sub>G (G \<phi>) w) w
[PROOF STEP]
hence "suffix k w \<Turnstile> \<phi>"
[PROOF STATE]
proof (prove)
using this:
i \<le> k

goal (1 subgoal):
 1. suffix k w \<Turnstile> \<phi>
[PROOF STEP]
using \<open>\<forall>j\<ge>i. suffix j w \<Turnstile> \<phi>\<close>
[PROOF STATE]
proof (prove)
using this:
i \<le> k
\<forall>j\<ge>i. suffix j w \<Turnstile> \<phi>

goal (1 subgoal):
 1. suffix k w \<Turnstile> \<phi>
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
suffix k w \<Turnstile> \<phi>

goal (2 subgoals):
 1. \<lbrakk>closed (\<G>\<^sub>F\<^sub>G \<phi> w) w; w \<Turnstile> F G \<phi>\<rbrakk> \<Longrightarrow> closed (\<G>\<^sub>F\<^sub>G (G \<phi>) w) w
 2. \<lbrakk>closed (\<G>\<^sub>F\<^sub>G \<phi> w) w; \<not> w \<Turnstile> F G \<phi>\<rbrakk> \<Longrightarrow> closed (\<G>\<^sub>F\<^sub>G (G \<phi>) w) w
[PROOF STEP]
hence "\<PP> \<phi> {G \<psi> |\<psi>. w \<Turnstile> F G \<psi>} (suffix k w) 0"
[PROOF STATE]
proof (prove)
using this:
suffix k w \<Turnstile> \<phi>

goal (1 subgoal):
 1. \<exists>j. {G \<psi> |\<psi>. w \<Turnstile> F G \<psi>} \<Turnstile>\<^sub>P af\<^sub>G \<phi> (prefix j (suffix k w))
[PROOF STEP]
using LTL_FG_suffix
[PROOF STATE]
proof (prove)
using this:
suffix k w \<Turnstile> \<phi>
suffix ?i ?w \<Turnstile> F G ?\<phi> = ?w \<Turnstile> F G ?\<phi>

goal (1 subgoal):
 1. \<exists>j. {G \<psi> |\<psi>. w \<Turnstile> F G \<psi>} \<Turnstile>\<^sub>P af\<^sub>G \<phi> (prefix j (suffix k w))
[PROOF STEP]
by (blast dest: ltl_implies_provable[unfolded \<G>\<^sub>F\<^sub>G_alt_def])
[PROOF STATE]
proof (state)
this:
\<exists>j. {G \<psi> |\<psi>. w \<Turnstile> F G \<psi>} \<Turnstile>\<^sub>P af\<^sub>G \<phi> (prefix j (suffix k w))

goal (2 subgoals):
 1. \<lbrakk>closed (\<G>\<^sub>F\<^sub>G \<phi> w) w; w \<Turnstile> F G \<phi>\<rbrakk> \<Longrightarrow> closed (\<G>\<^sub>F\<^sub>G (G \<phi>) w) w
 2. \<lbrakk>closed (\<G>\<^sub>F\<^sub>G \<phi> w) w; \<not> w \<Turnstile> F G \<phi>\<rbrakk> \<Longrightarrow> closed (\<G>\<^sub>F\<^sub>G (G \<phi>) w) w
[PROOF STEP]
hence "\<PP> \<phi> {G \<psi> |\<psi>. w \<Turnstile> F G \<psi>} w k"
[PROOF STATE]
proof (prove)
using this:
\<exists>j. {G \<psi> |\<psi>. w \<Turnstile> F G \<psi>} \<Turnstile>\<^sub>P af\<^sub>G \<phi> (prefix j (suffix k w))

goal (1 subgoal):
 1. \<PP> \<phi> {G \<psi> |\<psi>. w \<Turnstile> F G \<psi>} w k
[PROOF STEP]
unfolding subsequence_shift
[PROOF STATE]
proof (prove)
using this:
\<exists>j. {G \<psi> |\<psi>. w \<Turnstile> F G \<psi>} \<Turnstile>\<^sub>P af\<^sub>G \<phi> (w [k + 0 \<rightarrow> k + j])

goal (1 subgoal):
 1. \<PP> \<phi> {G \<psi> |\<psi>. w \<Turnstile> F G \<psi>} w k
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<PP> \<phi> {G \<psi> |\<psi>. w \<Turnstile> F G \<psi>} w k

goal (2 subgoals):
 1. \<lbrakk>closed (\<G>\<^sub>F\<^sub>G \<phi> w) w; w \<Turnstile> F G \<phi>\<rbrakk> \<Longrightarrow> closed (\<G>\<^sub>F\<^sub>G (G \<phi>) w) w
 2. \<lbrakk>closed (\<G>\<^sub>F\<^sub>G \<phi> w) w; \<not> w \<Turnstile> F G \<phi>\<rbrakk> \<Longrightarrow> closed (\<G>\<^sub>F\<^sub>G (G \<phi>) w) w
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
i \<le> ?k2 \<Longrightarrow> \<PP> \<phi> {G \<psi> |\<psi>. w \<Turnstile> F G \<psi>} w ?k2

goal (2 subgoals):
 1. \<lbrakk>closed (\<G>\<^sub>F\<^sub>G \<phi> w) w; w \<Turnstile> F G \<phi>\<rbrakk> \<Longrightarrow> closed (\<G>\<^sub>F\<^sub>G (G \<phi>) w) w
 2. \<lbrakk>closed (\<G>\<^sub>F\<^sub>G \<phi> w) w; \<not> w \<Turnstile> F G \<phi>\<rbrakk> \<Longrightarrow> closed (\<G>\<^sub>F\<^sub>G (G \<phi>) w) w
[PROOF STEP]
hence "\<PP>\<^sub>\<infinity> \<phi> {G \<psi> | \<psi>. w \<Turnstile> F G \<psi>} w"
[PROOF STATE]
proof (prove)
using this:
i \<le> ?k2 \<Longrightarrow> \<PP> \<phi> {G \<psi> |\<psi>. w \<Turnstile> F G \<psi>} w ?k2

goal (1 subgoal):
 1. \<PP>\<^sub>\<infinity> \<phi> {G \<psi> |\<psi>. w \<Turnstile> F G \<psi>} w
[PROOF STEP]
using almost_all_eventually_provable_def[of \<phi> _ w]
[PROOF STATE]
proof (prove)
using this:
i \<le> ?k2 \<Longrightarrow> \<PP> \<phi> {G \<psi> |\<psi>. w \<Turnstile> F G \<psi>} w ?k2
\<PP>\<^sub>\<infinity> \<phi> ?\<G> w \<equiv> \<forall>\<^sub>\<infinity>i. \<PP> \<phi> ?\<G> w i

goal (1 subgoal):
 1. \<PP>\<^sub>\<infinity> \<phi> {G \<psi> |\<psi>. w \<Turnstile> F G \<psi>} w
[PROOF STEP]
unfolding MOST_nat_le
[PROOF STATE]
proof (prove)
using this:
i \<le> ?k2 \<Longrightarrow> \<PP> \<phi> {G \<psi> |\<psi>. w \<Turnstile> F G \<psi>} w ?k2
\<PP>\<^sub>\<infinity> \<phi> ?\<G> w \<equiv> \<exists>m. \<forall>n\<ge>m. \<PP> \<phi> ?\<G> w n

goal (1 subgoal):
 1. \<PP>\<^sub>\<infinity> \<phi> {G \<psi> |\<psi>. w \<Turnstile> F G \<psi>} w
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<PP>\<^sub>\<infinity> \<phi> {G \<psi> |\<psi>. w \<Turnstile> F G \<psi>} w

goal (2 subgoals):
 1. \<lbrakk>closed (\<G>\<^sub>F\<^sub>G \<phi> w) w; w \<Turnstile> F G \<phi>\<rbrakk> \<Longrightarrow> closed (\<G>\<^sub>F\<^sub>G (G \<phi>) w) w
 2. \<lbrakk>closed (\<G>\<^sub>F\<^sub>G \<phi> w) w; \<not> w \<Turnstile> F G \<phi>\<rbrakk> \<Longrightarrow> closed (\<G>\<^sub>F\<^sub>G (G \<phi>) w) w
[PROOF STEP]
hence "\<PP>\<^sub>\<infinity> \<phi> (\<G>\<^sub>F\<^sub>G \<phi> w) w"
[PROOF STATE]
proof (prove)
using this:
\<PP>\<^sub>\<infinity> \<phi> {G \<psi> |\<psi>. w \<Turnstile> F G \<psi>} w

goal (1 subgoal):
 1. \<PP>\<^sub>\<infinity> \<phi> (\<G>\<^sub>F\<^sub>G \<phi> w) w
[PROOF STEP]
unfolding \<G>\<^sub>F\<^sub>G_alt_def
[PROOF STATE]
proof (prove)
using this:
\<PP>\<^sub>\<infinity> \<phi> {G \<psi> |\<psi>. w \<Turnstile> F G \<psi>} w

goal (1 subgoal):
 1. \<PP>\<^sub>\<infinity> \<phi> {G \<psi> |\<psi>. G \<psi> \<in> \<^bold>G \<phi> \<and> w \<Turnstile> F G \<psi>} w
[PROOF STEP]
using almost_all_eventually_provable_restrict_to_G
[PROOF STATE]
proof (prove)
using this:
\<PP>\<^sub>\<infinity> \<phi> {G \<psi> |\<psi>. w \<Turnstile> F G \<psi>} w
\<lbrakk>\<PP>\<^sub>\<infinity> ?\<phi> ?\<G> ?w; Only_G ?\<G>\<rbrakk> \<Longrightarrow> \<PP>\<^sub>\<infinity> ?\<phi> (?\<G> \<inter> \<^bold>G ?\<phi>) ?w

goal (1 subgoal):
 1. \<PP>\<^sub>\<infinity> \<phi> {G \<psi> |\<psi>. G \<psi> \<in> \<^bold>G \<phi> \<and> w \<Turnstile> F G \<psi>} w
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<PP>\<^sub>\<infinity> \<phi> (\<G>\<^sub>F\<^sub>G \<phi> w) w

goal (2 subgoals):
 1. \<lbrakk>closed (\<G>\<^sub>F\<^sub>G \<phi> w) w; w \<Turnstile> F G \<phi>\<rbrakk> \<Longrightarrow> closed (\<G>\<^sub>F\<^sub>G (G \<phi>) w) w
 2. \<lbrakk>closed (\<G>\<^sub>F\<^sub>G \<phi> w) w; \<not> w \<Turnstile> F G \<phi>\<rbrakk> \<Longrightarrow> closed (\<G>\<^sub>F\<^sub>G (G \<phi>) w) w
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<PP>\<^sub>\<infinity> \<phi> (\<G>\<^sub>F\<^sub>G \<phi> w) w

goal (1 subgoal):
 1. closed (\<G>\<^sub>F\<^sub>G (G \<phi>) w) w
[PROOF STEP]
using LTLGlobal insert
[PROOF STATE]
proof (prove)
using this:
\<PP>\<^sub>\<infinity> \<phi> (\<G>\<^sub>F\<^sub>G \<phi> w) w
closed (\<G>\<^sub>F\<^sub>G \<phi> w) w
ListMem ?x ?xs \<Longrightarrow> ListMem ?x (?y # ?xs)

goal (1 subgoal):
 1. closed (\<G>\<^sub>F\<^sub>G (G \<phi>) w) w
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
closed (\<G>\<^sub>F\<^sub>G (G \<phi>) w) w

goal (1 subgoal):
 1. \<lbrakk>closed (\<G>\<^sub>F\<^sub>G \<phi> w) w; \<not> w \<Turnstile> F G \<phi>\<rbrakk> \<Longrightarrow> closed (\<G>\<^sub>F\<^sub>G (G \<phi>) w) w
[PROOF STEP]
qed auto
[PROOF STATE]
proof (state)
this:
closed (\<G>\<^sub>F\<^sub>G (G \<phi>) w) w

goal (9 subgoals):
 1. closed (\<G>\<^sub>F\<^sub>G true w) w
 2. closed (\<G>\<^sub>F\<^sub>G false w) w
 3. \<And>x. closed (\<G>\<^sub>F\<^sub>G p(x) w) w
 4. \<And>x. closed (\<G>\<^sub>F\<^sub>G (np(x)) w) w
 5. \<And>\<phi>1 \<phi>2. \<lbrakk>closed (\<G>\<^sub>F\<^sub>G \<phi>1 w) w; closed (\<G>\<^sub>F\<^sub>G \<phi>2 w) w\<rbrakk> \<Longrightarrow> closed (\<G>\<^sub>F\<^sub>G (\<phi>1 and \<phi>2) w) w
 6. \<And>\<phi>1 \<phi>2. \<lbrakk>closed (\<G>\<^sub>F\<^sub>G \<phi>1 w) w; closed (\<G>\<^sub>F\<^sub>G \<phi>2 w) w\<rbrakk> \<Longrightarrow> closed (\<G>\<^sub>F\<^sub>G (\<phi>1 or \<phi>2) w) w
 7. \<And>\<phi>. closed (\<G>\<^sub>F\<^sub>G \<phi> w) w \<Longrightarrow> closed (\<G>\<^sub>F\<^sub>G (X \<phi>) w) w
 8. \<And>\<phi>. closed (\<G>\<^sub>F\<^sub>G \<phi> w) w \<Longrightarrow> closed (\<G>\<^sub>F\<^sub>G (F \<phi>) w) w
 9. \<And>\<phi>1 \<phi>2. \<lbrakk>closed (\<G>\<^sub>F\<^sub>G \<phi>1 w) w; closed (\<G>\<^sub>F\<^sub>G \<phi>2 w) w\<rbrakk> \<Longrightarrow> closed (\<G>\<^sub>F\<^sub>G (\<phi>1 U \<phi>2) w) w
[PROOF STEP]
qed auto