[STATEMENT]
lemma flatten_sigma_2_correct:
  "w \<Turnstile>\<^sub>n \<phi>[\<G>\<F> \<phi> w]\<^sub>\<Sigma>\<^sub>2 \<longleftrightarrow> w \<Turnstile>\<^sub>n \<phi>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. w \<Turnstile>\<^sub>n \<phi>[\<G>\<F> \<phi> w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>
[PROOF STEP]
proof (induction \<phi> arbitrary: w)
[PROOF STATE]
proof (state)
goal (11 subgoals):
 1. \<And>w. w \<Turnstile>\<^sub>n true\<^sub>n[\<G>\<F> true\<^sub>n w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n true\<^sub>n
 2. \<And>w. w \<Turnstile>\<^sub>n false\<^sub>n[\<G>\<F> false\<^sub>n w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n false\<^sub>n
 3. \<And>x w. w \<Turnstile>\<^sub>n prop\<^sub>n(x)[\<G>\<F> prop\<^sub>n(x) w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n prop\<^sub>n(x)
 4. \<And>x w. w \<Turnstile>\<^sub>n nprop\<^sub>n(x)[\<G>\<F> nprop\<^sub>n(x) w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n nprop\<^sub>n(x)
 5. \<And>\<phi>1 \<phi>2 w. \<lbrakk>\<And>w. w \<Turnstile>\<^sub>n \<phi>1[\<G>\<F> \<phi>1 w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>1; \<And>w. w \<Turnstile>\<^sub>n \<phi>2[\<G>\<F> \<phi>2 w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>2\<rbrakk> \<Longrightarrow> w \<Turnstile>\<^sub>n \<phi>1 and\<^sub>n \<phi>2[\<G>\<F> (\<phi>1 and\<^sub>n \<phi>2) w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>1 and\<^sub>n \<phi>2
 6. \<And>\<phi>1 \<phi>2 w. \<lbrakk>\<And>w. w \<Turnstile>\<^sub>n \<phi>1[\<G>\<F> \<phi>1 w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>1; \<And>w. w \<Turnstile>\<^sub>n \<phi>2[\<G>\<F> \<phi>2 w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>2\<rbrakk> \<Longrightarrow> w \<Turnstile>\<^sub>n \<phi>1 or\<^sub>n \<phi>2[\<G>\<F> (\<phi>1 or\<^sub>n \<phi>2) w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>1 or\<^sub>n \<phi>2
 7. \<And>\<phi> w. (\<And>w. w \<Turnstile>\<^sub>n \<phi>[\<G>\<F> \<phi> w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>) \<Longrightarrow> w \<Turnstile>\<^sub>n X\<^sub>n \<phi>[\<G>\<F> (X\<^sub>n \<phi>) w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n X\<^sub>n \<phi>
 8. \<And>\<phi>1 \<phi>2 w. \<lbrakk>\<And>w. w \<Turnstile>\<^sub>n \<phi>1[\<G>\<F> \<phi>1 w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>1; \<And>w. w \<Turnstile>\<^sub>n \<phi>2[\<G>\<F> \<phi>2 w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>2\<rbrakk> \<Longrightarrow> w \<Turnstile>\<^sub>n \<phi>1 U\<^sub>n \<phi>2[\<G>\<F> (\<phi>1 U\<^sub>n \<phi>2) w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>1 U\<^sub>n \<phi>2
 9. \<And>\<phi>1 \<phi>2 w. \<lbrakk>\<And>w. w \<Turnstile>\<^sub>n \<phi>1[\<G>\<F> \<phi>1 w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>1; \<And>w. w \<Turnstile>\<^sub>n \<phi>2[\<G>\<F> \<phi>2 w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>2\<rbrakk> \<Longrightarrow> w \<Turnstile>\<^sub>n \<phi>1 R\<^sub>n \<phi>2[\<G>\<F> (\<phi>1 R\<^sub>n \<phi>2) w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>1 R\<^sub>n \<phi>2
 10. \<And>\<phi>1 \<phi>2 w. \<lbrakk>\<And>w. w \<Turnstile>\<^sub>n \<phi>1[\<G>\<F> \<phi>1 w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>1; \<And>w. w \<Turnstile>\<^sub>n \<phi>2[\<G>\<F> \<phi>2 w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>2\<rbrakk> \<Longrightarrow> w \<Turnstile>\<^sub>n \<phi>1 W\<^sub>n \<phi>2[\<G>\<F> (\<phi>1 W\<^sub>n \<phi>2) w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>1 W\<^sub>n \<phi>2
A total of 11 subgoals...
[PROOF STEP]
case (And_ltln \<phi>1 \<phi>2)
[PROOF STATE]
proof (state)
this:
?w \<Turnstile>\<^sub>n \<phi>1[\<G>\<F> \<phi>1 ?w]\<^sub>\<Sigma>\<^sub>2 = ?w \<Turnstile>\<^sub>n \<phi>1
?w \<Turnstile>\<^sub>n \<phi>2[\<G>\<F> \<phi>2 ?w]\<^sub>\<Sigma>\<^sub>2 = ?w \<Turnstile>\<^sub>n \<phi>2

goal (11 subgoals):
 1. \<And>w. w \<Turnstile>\<^sub>n true\<^sub>n[\<G>\<F> true\<^sub>n w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n true\<^sub>n
 2. \<And>w. w \<Turnstile>\<^sub>n false\<^sub>n[\<G>\<F> false\<^sub>n w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n false\<^sub>n
 3. \<And>x w. w \<Turnstile>\<^sub>n prop\<^sub>n(x)[\<G>\<F> prop\<^sub>n(x) w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n prop\<^sub>n(x)
 4. \<And>x w. w \<Turnstile>\<^sub>n nprop\<^sub>n(x)[\<G>\<F> nprop\<^sub>n(x) w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n nprop\<^sub>n(x)
 5. \<And>\<phi>1 \<phi>2 w. \<lbrakk>\<And>w. w \<Turnstile>\<^sub>n \<phi>1[\<G>\<F> \<phi>1 w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>1; \<And>w. w \<Turnstile>\<^sub>n \<phi>2[\<G>\<F> \<phi>2 w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>2\<rbrakk> \<Longrightarrow> w \<Turnstile>\<^sub>n \<phi>1 and\<^sub>n \<phi>2[\<G>\<F> (\<phi>1 and\<^sub>n \<phi>2) w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>1 and\<^sub>n \<phi>2
 6. \<And>\<phi>1 \<phi>2 w. \<lbrakk>\<And>w. w \<Turnstile>\<^sub>n \<phi>1[\<G>\<F> \<phi>1 w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>1; \<And>w. w \<Turnstile>\<^sub>n \<phi>2[\<G>\<F> \<phi>2 w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>2\<rbrakk> \<Longrightarrow> w \<Turnstile>\<^sub>n \<phi>1 or\<^sub>n \<phi>2[\<G>\<F> (\<phi>1 or\<^sub>n \<phi>2) w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>1 or\<^sub>n \<phi>2
 7. \<And>\<phi> w. (\<And>w. w \<Turnstile>\<^sub>n \<phi>[\<G>\<F> \<phi> w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>) \<Longrightarrow> w \<Turnstile>\<^sub>n X\<^sub>n \<phi>[\<G>\<F> (X\<^sub>n \<phi>) w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n X\<^sub>n \<phi>
 8. \<And>\<phi>1 \<phi>2 w. \<lbrakk>\<And>w. w \<Turnstile>\<^sub>n \<phi>1[\<G>\<F> \<phi>1 w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>1; \<And>w. w \<Turnstile>\<^sub>n \<phi>2[\<G>\<F> \<phi>2 w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>2\<rbrakk> \<Longrightarrow> w \<Turnstile>\<^sub>n \<phi>1 U\<^sub>n \<phi>2[\<G>\<F> (\<phi>1 U\<^sub>n \<phi>2) w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>1 U\<^sub>n \<phi>2
 9. \<And>\<phi>1 \<phi>2 w. \<lbrakk>\<And>w. w \<Turnstile>\<^sub>n \<phi>1[\<G>\<F> \<phi>1 w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>1; \<And>w. w \<Turnstile>\<^sub>n \<phi>2[\<G>\<F> \<phi>2 w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>2\<rbrakk> \<Longrightarrow> w \<Turnstile>\<^sub>n \<phi>1 R\<^sub>n \<phi>2[\<G>\<F> (\<phi>1 R\<^sub>n \<phi>2) w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>1 R\<^sub>n \<phi>2
 10. \<And>\<phi>1 \<phi>2 w. \<lbrakk>\<And>w. w \<Turnstile>\<^sub>n \<phi>1[\<G>\<F> \<phi>1 w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>1; \<And>w. w \<Turnstile>\<^sub>n \<phi>2[\<G>\<F> \<phi>2 w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>2\<rbrakk> \<Longrightarrow> w \<Turnstile>\<^sub>n \<phi>1 W\<^sub>n \<phi>2[\<G>\<F> (\<phi>1 W\<^sub>n \<phi>2) w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>1 W\<^sub>n \<phi>2
A total of 11 subgoals...
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
?w \<Turnstile>\<^sub>n \<phi>1[\<G>\<F> \<phi>1 ?w]\<^sub>\<Sigma>\<^sub>2 = ?w \<Turnstile>\<^sub>n \<phi>1
?w \<Turnstile>\<^sub>n \<phi>2[\<G>\<F> \<phi>2 ?w]\<^sub>\<Sigma>\<^sub>2 = ?w \<Turnstile>\<^sub>n \<phi>2
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
?w \<Turnstile>\<^sub>n \<phi>1[\<G>\<F> \<phi>1 ?w]\<^sub>\<Sigma>\<^sub>2 = ?w \<Turnstile>\<^sub>n \<phi>1
?w \<Turnstile>\<^sub>n \<phi>2[\<G>\<F> \<phi>2 ?w]\<^sub>\<Sigma>\<^sub>2 = ?w \<Turnstile>\<^sub>n \<phi>2

goal (1 subgoal):
 1. w \<Turnstile>\<^sub>n \<phi>1 and\<^sub>n \<phi>2[\<G>\<F> (\<phi>1 and\<^sub>n \<phi>2) w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>1 and\<^sub>n \<phi>2
[PROOF STEP]
using flatten_sigma_2_IH_lifting[of _ "\<phi>1 and\<^sub>n \<phi>2" 0]
[PROOF STATE]
proof (prove)
using this:
?w \<Turnstile>\<^sub>n \<phi>1[\<G>\<F> \<phi>1 ?w]\<^sub>\<Sigma>\<^sub>2 = ?w \<Turnstile>\<^sub>n \<phi>1
?w \<Turnstile>\<^sub>n \<phi>2[\<G>\<F> \<phi>2 ?w]\<^sub>\<Sigma>\<^sub>2 = ?w \<Turnstile>\<^sub>n \<phi>2
\<lbrakk>?\<psi> \<in> subfrmlsn (\<phi>1 and\<^sub>n \<phi>2); suffix 0 ?w \<Turnstile>\<^sub>n ?\<psi>[\<G>\<F> ?\<psi> (suffix 0 ?w)]\<^sub>\<Sigma>\<^sub>2 = suffix 0 ?w \<Turnstile>\<^sub>n ?\<psi>\<rbrakk> \<Longrightarrow> suffix 0 ?w \<Turnstile>\<^sub>n ?\<psi>[\<G>\<F> (\<phi>1 and\<^sub>n \<phi>2) ?w]\<^sub>\<Sigma>\<^sub>2 = suffix 0 ?w \<Turnstile>\<^sub>n ?\<psi>

goal (1 subgoal):
 1. w \<Turnstile>\<^sub>n \<phi>1 and\<^sub>n \<phi>2[\<G>\<F> (\<phi>1 and\<^sub>n \<phi>2) w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>1 and\<^sub>n \<phi>2
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
w \<Turnstile>\<^sub>n \<phi>1 and\<^sub>n \<phi>2[\<G>\<F> (\<phi>1 and\<^sub>n \<phi>2) w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>1 and\<^sub>n \<phi>2

goal (10 subgoals):
 1. \<And>w. w \<Turnstile>\<^sub>n true\<^sub>n[\<G>\<F> true\<^sub>n w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n true\<^sub>n
 2. \<And>w. w \<Turnstile>\<^sub>n false\<^sub>n[\<G>\<F> false\<^sub>n w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n false\<^sub>n
 3. \<And>x w. w \<Turnstile>\<^sub>n prop\<^sub>n(x)[\<G>\<F> prop\<^sub>n(x) w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n prop\<^sub>n(x)
 4. \<And>x w. w \<Turnstile>\<^sub>n nprop\<^sub>n(x)[\<G>\<F> nprop\<^sub>n(x) w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n nprop\<^sub>n(x)
 5. \<And>\<phi>1 \<phi>2 w. \<lbrakk>\<And>w. w \<Turnstile>\<^sub>n \<phi>1[\<G>\<F> \<phi>1 w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>1; \<And>w. w \<Turnstile>\<^sub>n \<phi>2[\<G>\<F> \<phi>2 w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>2\<rbrakk> \<Longrightarrow> w \<Turnstile>\<^sub>n \<phi>1 or\<^sub>n \<phi>2[\<G>\<F> (\<phi>1 or\<^sub>n \<phi>2) w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>1 or\<^sub>n \<phi>2
 6. \<And>\<phi> w. (\<And>w. w \<Turnstile>\<^sub>n \<phi>[\<G>\<F> \<phi> w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>) \<Longrightarrow> w \<Turnstile>\<^sub>n X\<^sub>n \<phi>[\<G>\<F> (X\<^sub>n \<phi>) w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n X\<^sub>n \<phi>
 7. \<And>\<phi>1 \<phi>2 w. \<lbrakk>\<And>w. w \<Turnstile>\<^sub>n \<phi>1[\<G>\<F> \<phi>1 w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>1; \<And>w. w \<Turnstile>\<^sub>n \<phi>2[\<G>\<F> \<phi>2 w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>2\<rbrakk> \<Longrightarrow> w \<Turnstile>\<^sub>n \<phi>1 U\<^sub>n \<phi>2[\<G>\<F> (\<phi>1 U\<^sub>n \<phi>2) w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>1 U\<^sub>n \<phi>2
 8. \<And>\<phi>1 \<phi>2 w. \<lbrakk>\<And>w. w \<Turnstile>\<^sub>n \<phi>1[\<G>\<F> \<phi>1 w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>1; \<And>w. w \<Turnstile>\<^sub>n \<phi>2[\<G>\<F> \<phi>2 w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>2\<rbrakk> \<Longrightarrow> w \<Turnstile>\<^sub>n \<phi>1 R\<^sub>n \<phi>2[\<G>\<F> (\<phi>1 R\<^sub>n \<phi>2) w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>1 R\<^sub>n \<phi>2
 9. \<And>\<phi>1 \<phi>2 w. \<lbrakk>\<And>w. w \<Turnstile>\<^sub>n \<phi>1[\<G>\<F> \<phi>1 w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>1; \<And>w. w \<Turnstile>\<^sub>n \<phi>2[\<G>\<F> \<phi>2 w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>2\<rbrakk> \<Longrightarrow> w \<Turnstile>\<^sub>n \<phi>1 W\<^sub>n \<phi>2[\<G>\<F> (\<phi>1 W\<^sub>n \<phi>2) w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>1 W\<^sub>n \<phi>2
 10. \<And>\<phi>1 \<phi>2 w. \<lbrakk>\<And>w. w \<Turnstile>\<^sub>n \<phi>1[\<G>\<F> \<phi>1 w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>1; \<And>w. w \<Turnstile>\<^sub>n \<phi>2[\<G>\<F> \<phi>2 w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>2\<rbrakk> \<Longrightarrow> w \<Turnstile>\<^sub>n \<phi>1 M\<^sub>n \<phi>2[\<G>\<F> (\<phi>1 M\<^sub>n \<phi>2) w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>1 M\<^sub>n \<phi>2
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (10 subgoals):
 1. \<And>w. w \<Turnstile>\<^sub>n true\<^sub>n[\<G>\<F> true\<^sub>n w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n true\<^sub>n
 2. \<And>w. w \<Turnstile>\<^sub>n false\<^sub>n[\<G>\<F> false\<^sub>n w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n false\<^sub>n
 3. \<And>x w. w \<Turnstile>\<^sub>n prop\<^sub>n(x)[\<G>\<F> prop\<^sub>n(x) w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n prop\<^sub>n(x)
 4. \<And>x w. w \<Turnstile>\<^sub>n nprop\<^sub>n(x)[\<G>\<F> nprop\<^sub>n(x) w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n nprop\<^sub>n(x)
 5. \<And>\<phi>1 \<phi>2 w. \<lbrakk>\<And>w. w \<Turnstile>\<^sub>n \<phi>1[\<G>\<F> \<phi>1 w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>1; \<And>w. w \<Turnstile>\<^sub>n \<phi>2[\<G>\<F> \<phi>2 w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>2\<rbrakk> \<Longrightarrow> w \<Turnstile>\<^sub>n \<phi>1 or\<^sub>n \<phi>2[\<G>\<F> (\<phi>1 or\<^sub>n \<phi>2) w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>1 or\<^sub>n \<phi>2
 6. \<And>\<phi> w. (\<And>w. w \<Turnstile>\<^sub>n \<phi>[\<G>\<F> \<phi> w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>) \<Longrightarrow> w \<Turnstile>\<^sub>n X\<^sub>n \<phi>[\<G>\<F> (X\<^sub>n \<phi>) w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n X\<^sub>n \<phi>
 7. \<And>\<phi>1 \<phi>2 w. \<lbrakk>\<And>w. w \<Turnstile>\<^sub>n \<phi>1[\<G>\<F> \<phi>1 w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>1; \<And>w. w \<Turnstile>\<^sub>n \<phi>2[\<G>\<F> \<phi>2 w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>2\<rbrakk> \<Longrightarrow> w \<Turnstile>\<^sub>n \<phi>1 U\<^sub>n \<phi>2[\<G>\<F> (\<phi>1 U\<^sub>n \<phi>2) w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>1 U\<^sub>n \<phi>2
 8. \<And>\<phi>1 \<phi>2 w. \<lbrakk>\<And>w. w \<Turnstile>\<^sub>n \<phi>1[\<G>\<F> \<phi>1 w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>1; \<And>w. w \<Turnstile>\<^sub>n \<phi>2[\<G>\<F> \<phi>2 w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>2\<rbrakk> \<Longrightarrow> w \<Turnstile>\<^sub>n \<phi>1 R\<^sub>n \<phi>2[\<G>\<F> (\<phi>1 R\<^sub>n \<phi>2) w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>1 R\<^sub>n \<phi>2
 9. \<And>\<phi>1 \<phi>2 w. \<lbrakk>\<And>w. w \<Turnstile>\<^sub>n \<phi>1[\<G>\<F> \<phi>1 w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>1; \<And>w. w \<Turnstile>\<^sub>n \<phi>2[\<G>\<F> \<phi>2 w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>2\<rbrakk> \<Longrightarrow> w \<Turnstile>\<^sub>n \<phi>1 W\<^sub>n \<phi>2[\<G>\<F> (\<phi>1 W\<^sub>n \<phi>2) w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>1 W\<^sub>n \<phi>2
 10. \<And>\<phi>1 \<phi>2 w. \<lbrakk>\<And>w. w \<Turnstile>\<^sub>n \<phi>1[\<G>\<F> \<phi>1 w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>1; \<And>w. w \<Turnstile>\<^sub>n \<phi>2[\<G>\<F> \<phi>2 w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>2\<rbrakk> \<Longrightarrow> w \<Turnstile>\<^sub>n \<phi>1 M\<^sub>n \<phi>2[\<G>\<F> (\<phi>1 M\<^sub>n \<phi>2) w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>1 M\<^sub>n \<phi>2
[PROOF STEP]
case (Or_ltln \<phi>1 \<phi>2)
[PROOF STATE]
proof (state)
this:
?w \<Turnstile>\<^sub>n \<phi>1[\<G>\<F> \<phi>1 ?w]\<^sub>\<Sigma>\<^sub>2 = ?w \<Turnstile>\<^sub>n \<phi>1
?w \<Turnstile>\<^sub>n \<phi>2[\<G>\<F> \<phi>2 ?w]\<^sub>\<Sigma>\<^sub>2 = ?w \<Turnstile>\<^sub>n \<phi>2

goal (10 subgoals):
 1. \<And>w. w \<Turnstile>\<^sub>n true\<^sub>n[\<G>\<F> true\<^sub>n w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n true\<^sub>n
 2. \<And>w. w \<Turnstile>\<^sub>n false\<^sub>n[\<G>\<F> false\<^sub>n w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n false\<^sub>n
 3. \<And>x w. w \<Turnstile>\<^sub>n prop\<^sub>n(x)[\<G>\<F> prop\<^sub>n(x) w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n prop\<^sub>n(x)
 4. \<And>x w. w \<Turnstile>\<^sub>n nprop\<^sub>n(x)[\<G>\<F> nprop\<^sub>n(x) w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n nprop\<^sub>n(x)
 5. \<And>\<phi>1 \<phi>2 w. \<lbrakk>\<And>w. w \<Turnstile>\<^sub>n \<phi>1[\<G>\<F> \<phi>1 w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>1; \<And>w. w \<Turnstile>\<^sub>n \<phi>2[\<G>\<F> \<phi>2 w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>2\<rbrakk> \<Longrightarrow> w \<Turnstile>\<^sub>n \<phi>1 or\<^sub>n \<phi>2[\<G>\<F> (\<phi>1 or\<^sub>n \<phi>2) w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>1 or\<^sub>n \<phi>2
 6. \<And>\<phi> w. (\<And>w. w \<Turnstile>\<^sub>n \<phi>[\<G>\<F> \<phi> w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>) \<Longrightarrow> w \<Turnstile>\<^sub>n X\<^sub>n \<phi>[\<G>\<F> (X\<^sub>n \<phi>) w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n X\<^sub>n \<phi>
 7. \<And>\<phi>1 \<phi>2 w. \<lbrakk>\<And>w. w \<Turnstile>\<^sub>n \<phi>1[\<G>\<F> \<phi>1 w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>1; \<And>w. w \<Turnstile>\<^sub>n \<phi>2[\<G>\<F> \<phi>2 w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>2\<rbrakk> \<Longrightarrow> w \<Turnstile>\<^sub>n \<phi>1 U\<^sub>n \<phi>2[\<G>\<F> (\<phi>1 U\<^sub>n \<phi>2) w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>1 U\<^sub>n \<phi>2
 8. \<And>\<phi>1 \<phi>2 w. \<lbrakk>\<And>w. w \<Turnstile>\<^sub>n \<phi>1[\<G>\<F> \<phi>1 w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>1; \<And>w. w \<Turnstile>\<^sub>n \<phi>2[\<G>\<F> \<phi>2 w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>2\<rbrakk> \<Longrightarrow> w \<Turnstile>\<^sub>n \<phi>1 R\<^sub>n \<phi>2[\<G>\<F> (\<phi>1 R\<^sub>n \<phi>2) w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>1 R\<^sub>n \<phi>2
 9. \<And>\<phi>1 \<phi>2 w. \<lbrakk>\<And>w. w \<Turnstile>\<^sub>n \<phi>1[\<G>\<F> \<phi>1 w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>1; \<And>w. w \<Turnstile>\<^sub>n \<phi>2[\<G>\<F> \<phi>2 w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>2\<rbrakk> \<Longrightarrow> w \<Turnstile>\<^sub>n \<phi>1 W\<^sub>n \<phi>2[\<G>\<F> (\<phi>1 W\<^sub>n \<phi>2) w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>1 W\<^sub>n \<phi>2
 10. \<And>\<phi>1 \<phi>2 w. \<lbrakk>\<And>w. w \<Turnstile>\<^sub>n \<phi>1[\<G>\<F> \<phi>1 w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>1; \<And>w. w \<Turnstile>\<^sub>n \<phi>2[\<G>\<F> \<phi>2 w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>2\<rbrakk> \<Longrightarrow> w \<Turnstile>\<^sub>n \<phi>1 M\<^sub>n \<phi>2[\<G>\<F> (\<phi>1 M\<^sub>n \<phi>2) w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>1 M\<^sub>n \<phi>2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
?w \<Turnstile>\<^sub>n \<phi>1[\<G>\<F> \<phi>1 ?w]\<^sub>\<Sigma>\<^sub>2 = ?w \<Turnstile>\<^sub>n \<phi>1
?w \<Turnstile>\<^sub>n \<phi>2[\<G>\<F> \<phi>2 ?w]\<^sub>\<Sigma>\<^sub>2 = ?w \<Turnstile>\<^sub>n \<phi>2
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
?w \<Turnstile>\<^sub>n \<phi>1[\<G>\<F> \<phi>1 ?w]\<^sub>\<Sigma>\<^sub>2 = ?w \<Turnstile>\<^sub>n \<phi>1
?w \<Turnstile>\<^sub>n \<phi>2[\<G>\<F> \<phi>2 ?w]\<^sub>\<Sigma>\<^sub>2 = ?w \<Turnstile>\<^sub>n \<phi>2

goal (1 subgoal):
 1. w \<Turnstile>\<^sub>n \<phi>1 or\<^sub>n \<phi>2[\<G>\<F> (\<phi>1 or\<^sub>n \<phi>2) w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>1 or\<^sub>n \<phi>2
[PROOF STEP]
using flatten_sigma_2_IH_lifting[of _ "\<phi>1 or\<^sub>n \<phi>2" 0]
[PROOF STATE]
proof (prove)
using this:
?w \<Turnstile>\<^sub>n \<phi>1[\<G>\<F> \<phi>1 ?w]\<^sub>\<Sigma>\<^sub>2 = ?w \<Turnstile>\<^sub>n \<phi>1
?w \<Turnstile>\<^sub>n \<phi>2[\<G>\<F> \<phi>2 ?w]\<^sub>\<Sigma>\<^sub>2 = ?w \<Turnstile>\<^sub>n \<phi>2
\<lbrakk>?\<psi> \<in> subfrmlsn (\<phi>1 or\<^sub>n \<phi>2); suffix 0 ?w \<Turnstile>\<^sub>n ?\<psi>[\<G>\<F> ?\<psi> (suffix 0 ?w)]\<^sub>\<Sigma>\<^sub>2 = suffix 0 ?w \<Turnstile>\<^sub>n ?\<psi>\<rbrakk> \<Longrightarrow> suffix 0 ?w \<Turnstile>\<^sub>n ?\<psi>[\<G>\<F> (\<phi>1 or\<^sub>n \<phi>2) ?w]\<^sub>\<Sigma>\<^sub>2 = suffix 0 ?w \<Turnstile>\<^sub>n ?\<psi>

goal (1 subgoal):
 1. w \<Turnstile>\<^sub>n \<phi>1 or\<^sub>n \<phi>2[\<G>\<F> (\<phi>1 or\<^sub>n \<phi>2) w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>1 or\<^sub>n \<phi>2
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
w \<Turnstile>\<^sub>n \<phi>1 or\<^sub>n \<phi>2[\<G>\<F> (\<phi>1 or\<^sub>n \<phi>2) w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>1 or\<^sub>n \<phi>2

goal (9 subgoals):
 1. \<And>w. w \<Turnstile>\<^sub>n true\<^sub>n[\<G>\<F> true\<^sub>n w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n true\<^sub>n
 2. \<And>w. w \<Turnstile>\<^sub>n false\<^sub>n[\<G>\<F> false\<^sub>n w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n false\<^sub>n
 3. \<And>x w. w \<Turnstile>\<^sub>n prop\<^sub>n(x)[\<G>\<F> prop\<^sub>n(x) w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n prop\<^sub>n(x)
 4. \<And>x w. w \<Turnstile>\<^sub>n nprop\<^sub>n(x)[\<G>\<F> nprop\<^sub>n(x) w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n nprop\<^sub>n(x)
 5. \<And>\<phi> w. (\<And>w. w \<Turnstile>\<^sub>n \<phi>[\<G>\<F> \<phi> w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>) \<Longrightarrow> w \<Turnstile>\<^sub>n X\<^sub>n \<phi>[\<G>\<F> (X\<^sub>n \<phi>) w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n X\<^sub>n \<phi>
 6. \<And>\<phi>1 \<phi>2 w. \<lbrakk>\<And>w. w \<Turnstile>\<^sub>n \<phi>1[\<G>\<F> \<phi>1 w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>1; \<And>w. w \<Turnstile>\<^sub>n \<phi>2[\<G>\<F> \<phi>2 w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>2\<rbrakk> \<Longrightarrow> w \<Turnstile>\<^sub>n \<phi>1 U\<^sub>n \<phi>2[\<G>\<F> (\<phi>1 U\<^sub>n \<phi>2) w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>1 U\<^sub>n \<phi>2
 7. \<And>\<phi>1 \<phi>2 w. \<lbrakk>\<And>w. w \<Turnstile>\<^sub>n \<phi>1[\<G>\<F> \<phi>1 w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>1; \<And>w. w \<Turnstile>\<^sub>n \<phi>2[\<G>\<F> \<phi>2 w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>2\<rbrakk> \<Longrightarrow> w \<Turnstile>\<^sub>n \<phi>1 R\<^sub>n \<phi>2[\<G>\<F> (\<phi>1 R\<^sub>n \<phi>2) w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>1 R\<^sub>n \<phi>2
 8. \<And>\<phi>1 \<phi>2 w. \<lbrakk>\<And>w. w \<Turnstile>\<^sub>n \<phi>1[\<G>\<F> \<phi>1 w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>1; \<And>w. w \<Turnstile>\<^sub>n \<phi>2[\<G>\<F> \<phi>2 w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>2\<rbrakk> \<Longrightarrow> w \<Turnstile>\<^sub>n \<phi>1 W\<^sub>n \<phi>2[\<G>\<F> (\<phi>1 W\<^sub>n \<phi>2) w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>1 W\<^sub>n \<phi>2
 9. \<And>\<phi>1 \<phi>2 w. \<lbrakk>\<And>w. w \<Turnstile>\<^sub>n \<phi>1[\<G>\<F> \<phi>1 w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>1; \<And>w. w \<Turnstile>\<^sub>n \<phi>2[\<G>\<F> \<phi>2 w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>2\<rbrakk> \<Longrightarrow> w \<Turnstile>\<^sub>n \<phi>1 M\<^sub>n \<phi>2[\<G>\<F> (\<phi>1 M\<^sub>n \<phi>2) w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>1 M\<^sub>n \<phi>2
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (9 subgoals):
 1. \<And>w. w \<Turnstile>\<^sub>n true\<^sub>n[\<G>\<F> true\<^sub>n w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n true\<^sub>n
 2. \<And>w. w \<Turnstile>\<^sub>n false\<^sub>n[\<G>\<F> false\<^sub>n w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n false\<^sub>n
 3. \<And>x w. w \<Turnstile>\<^sub>n prop\<^sub>n(x)[\<G>\<F> prop\<^sub>n(x) w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n prop\<^sub>n(x)
 4. \<And>x w. w \<Turnstile>\<^sub>n nprop\<^sub>n(x)[\<G>\<F> nprop\<^sub>n(x) w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n nprop\<^sub>n(x)
 5. \<And>\<phi> w. (\<And>w. w \<Turnstile>\<^sub>n \<phi>[\<G>\<F> \<phi> w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>) \<Longrightarrow> w \<Turnstile>\<^sub>n X\<^sub>n \<phi>[\<G>\<F> (X\<^sub>n \<phi>) w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n X\<^sub>n \<phi>
 6. \<And>\<phi>1 \<phi>2 w. \<lbrakk>\<And>w. w \<Turnstile>\<^sub>n \<phi>1[\<G>\<F> \<phi>1 w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>1; \<And>w. w \<Turnstile>\<^sub>n \<phi>2[\<G>\<F> \<phi>2 w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>2\<rbrakk> \<Longrightarrow> w \<Turnstile>\<^sub>n \<phi>1 U\<^sub>n \<phi>2[\<G>\<F> (\<phi>1 U\<^sub>n \<phi>2) w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>1 U\<^sub>n \<phi>2
 7. \<And>\<phi>1 \<phi>2 w. \<lbrakk>\<And>w. w \<Turnstile>\<^sub>n \<phi>1[\<G>\<F> \<phi>1 w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>1; \<And>w. w \<Turnstile>\<^sub>n \<phi>2[\<G>\<F> \<phi>2 w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>2\<rbrakk> \<Longrightarrow> w \<Turnstile>\<^sub>n \<phi>1 R\<^sub>n \<phi>2[\<G>\<F> (\<phi>1 R\<^sub>n \<phi>2) w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>1 R\<^sub>n \<phi>2
 8. \<And>\<phi>1 \<phi>2 w. \<lbrakk>\<And>w. w \<Turnstile>\<^sub>n \<phi>1[\<G>\<F> \<phi>1 w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>1; \<And>w. w \<Turnstile>\<^sub>n \<phi>2[\<G>\<F> \<phi>2 w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>2\<rbrakk> \<Longrightarrow> w \<Turnstile>\<^sub>n \<phi>1 W\<^sub>n \<phi>2[\<G>\<F> (\<phi>1 W\<^sub>n \<phi>2) w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>1 W\<^sub>n \<phi>2
 9. \<And>\<phi>1 \<phi>2 w. \<lbrakk>\<And>w. w \<Turnstile>\<^sub>n \<phi>1[\<G>\<F> \<phi>1 w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>1; \<And>w. w \<Turnstile>\<^sub>n \<phi>2[\<G>\<F> \<phi>2 w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>2\<rbrakk> \<Longrightarrow> w \<Turnstile>\<^sub>n \<phi>1 M\<^sub>n \<phi>2[\<G>\<F> (\<phi>1 M\<^sub>n \<phi>2) w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>1 M\<^sub>n \<phi>2
[PROOF STEP]
case (Next_ltln \<phi>)
[PROOF STATE]
proof (state)
this:
?w \<Turnstile>\<^sub>n \<phi>[\<G>\<F> \<phi> ?w]\<^sub>\<Sigma>\<^sub>2 = ?w \<Turnstile>\<^sub>n \<phi>

goal (9 subgoals):
 1. \<And>w. w \<Turnstile>\<^sub>n true\<^sub>n[\<G>\<F> true\<^sub>n w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n true\<^sub>n
 2. \<And>w. w \<Turnstile>\<^sub>n false\<^sub>n[\<G>\<F> false\<^sub>n w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n false\<^sub>n
 3. \<And>x w. w \<Turnstile>\<^sub>n prop\<^sub>n(x)[\<G>\<F> prop\<^sub>n(x) w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n prop\<^sub>n(x)
 4. \<And>x w. w \<Turnstile>\<^sub>n nprop\<^sub>n(x)[\<G>\<F> nprop\<^sub>n(x) w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n nprop\<^sub>n(x)
 5. \<And>\<phi> w. (\<And>w. w \<Turnstile>\<^sub>n \<phi>[\<G>\<F> \<phi> w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>) \<Longrightarrow> w \<Turnstile>\<^sub>n X\<^sub>n \<phi>[\<G>\<F> (X\<^sub>n \<phi>) w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n X\<^sub>n \<phi>
 6. \<And>\<phi>1 \<phi>2 w. \<lbrakk>\<And>w. w \<Turnstile>\<^sub>n \<phi>1[\<G>\<F> \<phi>1 w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>1; \<And>w. w \<Turnstile>\<^sub>n \<phi>2[\<G>\<F> \<phi>2 w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>2\<rbrakk> \<Longrightarrow> w \<Turnstile>\<^sub>n \<phi>1 U\<^sub>n \<phi>2[\<G>\<F> (\<phi>1 U\<^sub>n \<phi>2) w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>1 U\<^sub>n \<phi>2
 7. \<And>\<phi>1 \<phi>2 w. \<lbrakk>\<And>w. w \<Turnstile>\<^sub>n \<phi>1[\<G>\<F> \<phi>1 w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>1; \<And>w. w \<Turnstile>\<^sub>n \<phi>2[\<G>\<F> \<phi>2 w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>2\<rbrakk> \<Longrightarrow> w \<Turnstile>\<^sub>n \<phi>1 R\<^sub>n \<phi>2[\<G>\<F> (\<phi>1 R\<^sub>n \<phi>2) w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>1 R\<^sub>n \<phi>2
 8. \<And>\<phi>1 \<phi>2 w. \<lbrakk>\<And>w. w \<Turnstile>\<^sub>n \<phi>1[\<G>\<F> \<phi>1 w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>1; \<And>w. w \<Turnstile>\<^sub>n \<phi>2[\<G>\<F> \<phi>2 w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>2\<rbrakk> \<Longrightarrow> w \<Turnstile>\<^sub>n \<phi>1 W\<^sub>n \<phi>2[\<G>\<F> (\<phi>1 W\<^sub>n \<phi>2) w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>1 W\<^sub>n \<phi>2
 9. \<And>\<phi>1 \<phi>2 w. \<lbrakk>\<And>w. w \<Turnstile>\<^sub>n \<phi>1[\<G>\<F> \<phi>1 w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>1; \<And>w. w \<Turnstile>\<^sub>n \<phi>2[\<G>\<F> \<phi>2 w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>2\<rbrakk> \<Longrightarrow> w \<Turnstile>\<^sub>n \<phi>1 M\<^sub>n \<phi>2[\<G>\<F> (\<phi>1 M\<^sub>n \<phi>2) w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>1 M\<^sub>n \<phi>2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
?w \<Turnstile>\<^sub>n \<phi>[\<G>\<F> \<phi> ?w]\<^sub>\<Sigma>\<^sub>2 = ?w \<Turnstile>\<^sub>n \<phi>
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
?w \<Turnstile>\<^sub>n \<phi>[\<G>\<F> \<phi> ?w]\<^sub>\<Sigma>\<^sub>2 = ?w \<Turnstile>\<^sub>n \<phi>

goal (1 subgoal):
 1. w \<Turnstile>\<^sub>n X\<^sub>n \<phi>[\<G>\<F> (X\<^sub>n \<phi>) w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n X\<^sub>n \<phi>
[PROOF STEP]
using flatten_sigma_2_IH_lifting[of _ "X\<^sub>n \<phi>" 1]
[PROOF STATE]
proof (prove)
using this:
?w \<Turnstile>\<^sub>n \<phi>[\<G>\<F> \<phi> ?w]\<^sub>\<Sigma>\<^sub>2 = ?w \<Turnstile>\<^sub>n \<phi>
\<lbrakk>?\<psi> \<in> subfrmlsn (X\<^sub>n \<phi>); suffix 1 ?w \<Turnstile>\<^sub>n ?\<psi>[\<G>\<F> ?\<psi> (suffix 1 ?w)]\<^sub>\<Sigma>\<^sub>2 = suffix 1 ?w \<Turnstile>\<^sub>n ?\<psi>\<rbrakk> \<Longrightarrow> suffix 1 ?w \<Turnstile>\<^sub>n ?\<psi>[\<G>\<F> (X\<^sub>n \<phi>) ?w]\<^sub>\<Sigma>\<^sub>2 = suffix 1 ?w \<Turnstile>\<^sub>n ?\<psi>

goal (1 subgoal):
 1. w \<Turnstile>\<^sub>n X\<^sub>n \<phi>[\<G>\<F> (X\<^sub>n \<phi>) w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n X\<^sub>n \<phi>
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
w \<Turnstile>\<^sub>n X\<^sub>n \<phi>[\<G>\<F> (X\<^sub>n \<phi>) w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n X\<^sub>n \<phi>

goal (8 subgoals):
 1. \<And>w. w \<Turnstile>\<^sub>n true\<^sub>n[\<G>\<F> true\<^sub>n w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n true\<^sub>n
 2. \<And>w. w \<Turnstile>\<^sub>n false\<^sub>n[\<G>\<F> false\<^sub>n w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n false\<^sub>n
 3. \<And>x w. w \<Turnstile>\<^sub>n prop\<^sub>n(x)[\<G>\<F> prop\<^sub>n(x) w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n prop\<^sub>n(x)
 4. \<And>x w. w \<Turnstile>\<^sub>n nprop\<^sub>n(x)[\<G>\<F> nprop\<^sub>n(x) w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n nprop\<^sub>n(x)
 5. \<And>\<phi>1 \<phi>2 w. \<lbrakk>\<And>w. w \<Turnstile>\<^sub>n \<phi>1[\<G>\<F> \<phi>1 w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>1; \<And>w. w \<Turnstile>\<^sub>n \<phi>2[\<G>\<F> \<phi>2 w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>2\<rbrakk> \<Longrightarrow> w \<Turnstile>\<^sub>n \<phi>1 U\<^sub>n \<phi>2[\<G>\<F> (\<phi>1 U\<^sub>n \<phi>2) w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>1 U\<^sub>n \<phi>2
 6. \<And>\<phi>1 \<phi>2 w. \<lbrakk>\<And>w. w \<Turnstile>\<^sub>n \<phi>1[\<G>\<F> \<phi>1 w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>1; \<And>w. w \<Turnstile>\<^sub>n \<phi>2[\<G>\<F> \<phi>2 w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>2\<rbrakk> \<Longrightarrow> w \<Turnstile>\<^sub>n \<phi>1 R\<^sub>n \<phi>2[\<G>\<F> (\<phi>1 R\<^sub>n \<phi>2) w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>1 R\<^sub>n \<phi>2
 7. \<And>\<phi>1 \<phi>2 w. \<lbrakk>\<And>w. w \<Turnstile>\<^sub>n \<phi>1[\<G>\<F> \<phi>1 w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>1; \<And>w. w \<Turnstile>\<^sub>n \<phi>2[\<G>\<F> \<phi>2 w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>2\<rbrakk> \<Longrightarrow> w \<Turnstile>\<^sub>n \<phi>1 W\<^sub>n \<phi>2[\<G>\<F> (\<phi>1 W\<^sub>n \<phi>2) w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>1 W\<^sub>n \<phi>2
 8. \<And>\<phi>1 \<phi>2 w. \<lbrakk>\<And>w. w \<Turnstile>\<^sub>n \<phi>1[\<G>\<F> \<phi>1 w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>1; \<And>w. w \<Turnstile>\<^sub>n \<phi>2[\<G>\<F> \<phi>2 w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>2\<rbrakk> \<Longrightarrow> w \<Turnstile>\<^sub>n \<phi>1 M\<^sub>n \<phi>2[\<G>\<F> (\<phi>1 M\<^sub>n \<phi>2) w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>1 M\<^sub>n \<phi>2
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (8 subgoals):
 1. \<And>w. w \<Turnstile>\<^sub>n true\<^sub>n[\<G>\<F> true\<^sub>n w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n true\<^sub>n
 2. \<And>w. w \<Turnstile>\<^sub>n false\<^sub>n[\<G>\<F> false\<^sub>n w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n false\<^sub>n
 3. \<And>x w. w \<Turnstile>\<^sub>n prop\<^sub>n(x)[\<G>\<F> prop\<^sub>n(x) w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n prop\<^sub>n(x)
 4. \<And>x w. w \<Turnstile>\<^sub>n nprop\<^sub>n(x)[\<G>\<F> nprop\<^sub>n(x) w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n nprop\<^sub>n(x)
 5. \<And>\<phi>1 \<phi>2 w. \<lbrakk>\<And>w. w \<Turnstile>\<^sub>n \<phi>1[\<G>\<F> \<phi>1 w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>1; \<And>w. w \<Turnstile>\<^sub>n \<phi>2[\<G>\<F> \<phi>2 w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>2\<rbrakk> \<Longrightarrow> w \<Turnstile>\<^sub>n \<phi>1 U\<^sub>n \<phi>2[\<G>\<F> (\<phi>1 U\<^sub>n \<phi>2) w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>1 U\<^sub>n \<phi>2
 6. \<And>\<phi>1 \<phi>2 w. \<lbrakk>\<And>w. w \<Turnstile>\<^sub>n \<phi>1[\<G>\<F> \<phi>1 w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>1; \<And>w. w \<Turnstile>\<^sub>n \<phi>2[\<G>\<F> \<phi>2 w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>2\<rbrakk> \<Longrightarrow> w \<Turnstile>\<^sub>n \<phi>1 R\<^sub>n \<phi>2[\<G>\<F> (\<phi>1 R\<^sub>n \<phi>2) w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>1 R\<^sub>n \<phi>2
 7. \<And>\<phi>1 \<phi>2 w. \<lbrakk>\<And>w. w \<Turnstile>\<^sub>n \<phi>1[\<G>\<F> \<phi>1 w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>1; \<And>w. w \<Turnstile>\<^sub>n \<phi>2[\<G>\<F> \<phi>2 w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>2\<rbrakk> \<Longrightarrow> w \<Turnstile>\<^sub>n \<phi>1 W\<^sub>n \<phi>2[\<G>\<F> (\<phi>1 W\<^sub>n \<phi>2) w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>1 W\<^sub>n \<phi>2
 8. \<And>\<phi>1 \<phi>2 w. \<lbrakk>\<And>w. w \<Turnstile>\<^sub>n \<phi>1[\<G>\<F> \<phi>1 w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>1; \<And>w. w \<Turnstile>\<^sub>n \<phi>2[\<G>\<F> \<phi>2 w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>2\<rbrakk> \<Longrightarrow> w \<Turnstile>\<^sub>n \<phi>1 M\<^sub>n \<phi>2[\<G>\<F> (\<phi>1 M\<^sub>n \<phi>2) w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>1 M\<^sub>n \<phi>2
[PROOF STEP]
case (Until_ltln \<phi>1 \<phi>2)
[PROOF STATE]
proof (state)
this:
?w \<Turnstile>\<^sub>n \<phi>1[\<G>\<F> \<phi>1 ?w]\<^sub>\<Sigma>\<^sub>2 = ?w \<Turnstile>\<^sub>n \<phi>1
?w \<Turnstile>\<^sub>n \<phi>2[\<G>\<F> \<phi>2 ?w]\<^sub>\<Sigma>\<^sub>2 = ?w \<Turnstile>\<^sub>n \<phi>2

goal (8 subgoals):
 1. \<And>w. w \<Turnstile>\<^sub>n true\<^sub>n[\<G>\<F> true\<^sub>n w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n true\<^sub>n
 2. \<And>w. w \<Turnstile>\<^sub>n false\<^sub>n[\<G>\<F> false\<^sub>n w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n false\<^sub>n
 3. \<And>x w. w \<Turnstile>\<^sub>n prop\<^sub>n(x)[\<G>\<F> prop\<^sub>n(x) w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n prop\<^sub>n(x)
 4. \<And>x w. w \<Turnstile>\<^sub>n nprop\<^sub>n(x)[\<G>\<F> nprop\<^sub>n(x) w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n nprop\<^sub>n(x)
 5. \<And>\<phi>1 \<phi>2 w. \<lbrakk>\<And>w. w \<Turnstile>\<^sub>n \<phi>1[\<G>\<F> \<phi>1 w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>1; \<And>w. w \<Turnstile>\<^sub>n \<phi>2[\<G>\<F> \<phi>2 w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>2\<rbrakk> \<Longrightarrow> w \<Turnstile>\<^sub>n \<phi>1 U\<^sub>n \<phi>2[\<G>\<F> (\<phi>1 U\<^sub>n \<phi>2) w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>1 U\<^sub>n \<phi>2
 6. \<And>\<phi>1 \<phi>2 w. \<lbrakk>\<And>w. w \<Turnstile>\<^sub>n \<phi>1[\<G>\<F> \<phi>1 w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>1; \<And>w. w \<Turnstile>\<^sub>n \<phi>2[\<G>\<F> \<phi>2 w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>2\<rbrakk> \<Longrightarrow> w \<Turnstile>\<^sub>n \<phi>1 R\<^sub>n \<phi>2[\<G>\<F> (\<phi>1 R\<^sub>n \<phi>2) w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>1 R\<^sub>n \<phi>2
 7. \<And>\<phi>1 \<phi>2 w. \<lbrakk>\<And>w. w \<Turnstile>\<^sub>n \<phi>1[\<G>\<F> \<phi>1 w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>1; \<And>w. w \<Turnstile>\<^sub>n \<phi>2[\<G>\<F> \<phi>2 w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>2\<rbrakk> \<Longrightarrow> w \<Turnstile>\<^sub>n \<phi>1 W\<^sub>n \<phi>2[\<G>\<F> (\<phi>1 W\<^sub>n \<phi>2) w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>1 W\<^sub>n \<phi>2
 8. \<And>\<phi>1 \<phi>2 w. \<lbrakk>\<And>w. w \<Turnstile>\<^sub>n \<phi>1[\<G>\<F> \<phi>1 w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>1; \<And>w. w \<Turnstile>\<^sub>n \<phi>2[\<G>\<F> \<phi>2 w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>2\<rbrakk> \<Longrightarrow> w \<Turnstile>\<^sub>n \<phi>1 M\<^sub>n \<phi>2[\<G>\<F> (\<phi>1 M\<^sub>n \<phi>2) w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>1 M\<^sub>n \<phi>2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
?w \<Turnstile>\<^sub>n \<phi>1[\<G>\<F> \<phi>1 ?w]\<^sub>\<Sigma>\<^sub>2 = ?w \<Turnstile>\<^sub>n \<phi>1
?w \<Turnstile>\<^sub>n \<phi>2[\<G>\<F> \<phi>2 ?w]\<^sub>\<Sigma>\<^sub>2 = ?w \<Turnstile>\<^sub>n \<phi>2
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
?w \<Turnstile>\<^sub>n \<phi>1[\<G>\<F> \<phi>1 ?w]\<^sub>\<Sigma>\<^sub>2 = ?w \<Turnstile>\<^sub>n \<phi>1
?w \<Turnstile>\<^sub>n \<phi>2[\<G>\<F> \<phi>2 ?w]\<^sub>\<Sigma>\<^sub>2 = ?w \<Turnstile>\<^sub>n \<phi>2

goal (1 subgoal):
 1. w \<Turnstile>\<^sub>n \<phi>1 U\<^sub>n \<phi>2[\<G>\<F> (\<phi>1 U\<^sub>n \<phi>2) w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>1 U\<^sub>n \<phi>2
[PROOF STEP]
using flatten_sigma_2_IH_lifting[of _ "\<phi>1 U\<^sub>n \<phi>2"]
[PROOF STATE]
proof (prove)
using this:
?w \<Turnstile>\<^sub>n \<phi>1[\<G>\<F> \<phi>1 ?w]\<^sub>\<Sigma>\<^sub>2 = ?w \<Turnstile>\<^sub>n \<phi>1
?w \<Turnstile>\<^sub>n \<phi>2[\<G>\<F> \<phi>2 ?w]\<^sub>\<Sigma>\<^sub>2 = ?w \<Turnstile>\<^sub>n \<phi>2
\<lbrakk>?\<psi> \<in> subfrmlsn (\<phi>1 U\<^sub>n \<phi>2); suffix ?i ?w \<Turnstile>\<^sub>n ?\<psi>[\<G>\<F> ?\<psi> (suffix ?i ?w)]\<^sub>\<Sigma>\<^sub>2 = suffix ?i ?w \<Turnstile>\<^sub>n ?\<psi>\<rbrakk> \<Longrightarrow> suffix ?i ?w \<Turnstile>\<^sub>n ?\<psi>[\<G>\<F> (\<phi>1 U\<^sub>n \<phi>2) ?w]\<^sub>\<Sigma>\<^sub>2 = suffix ?i ?w \<Turnstile>\<^sub>n ?\<psi>

goal (1 subgoal):
 1. w \<Turnstile>\<^sub>n \<phi>1 U\<^sub>n \<phi>2[\<G>\<F> (\<phi>1 U\<^sub>n \<phi>2) w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>1 U\<^sub>n \<phi>2
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
w \<Turnstile>\<^sub>n \<phi>1 U\<^sub>n \<phi>2[\<G>\<F> (\<phi>1 U\<^sub>n \<phi>2) w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>1 U\<^sub>n \<phi>2

goal (7 subgoals):
 1. \<And>w. w \<Turnstile>\<^sub>n true\<^sub>n[\<G>\<F> true\<^sub>n w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n true\<^sub>n
 2. \<And>w. w \<Turnstile>\<^sub>n false\<^sub>n[\<G>\<F> false\<^sub>n w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n false\<^sub>n
 3. \<And>x w. w \<Turnstile>\<^sub>n prop\<^sub>n(x)[\<G>\<F> prop\<^sub>n(x) w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n prop\<^sub>n(x)
 4. \<And>x w. w \<Turnstile>\<^sub>n nprop\<^sub>n(x)[\<G>\<F> nprop\<^sub>n(x) w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n nprop\<^sub>n(x)
 5. \<And>\<phi>1 \<phi>2 w. \<lbrakk>\<And>w. w \<Turnstile>\<^sub>n \<phi>1[\<G>\<F> \<phi>1 w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>1; \<And>w. w \<Turnstile>\<^sub>n \<phi>2[\<G>\<F> \<phi>2 w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>2\<rbrakk> \<Longrightarrow> w \<Turnstile>\<^sub>n \<phi>1 R\<^sub>n \<phi>2[\<G>\<F> (\<phi>1 R\<^sub>n \<phi>2) w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>1 R\<^sub>n \<phi>2
 6. \<And>\<phi>1 \<phi>2 w. \<lbrakk>\<And>w. w \<Turnstile>\<^sub>n \<phi>1[\<G>\<F> \<phi>1 w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>1; \<And>w. w \<Turnstile>\<^sub>n \<phi>2[\<G>\<F> \<phi>2 w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>2\<rbrakk> \<Longrightarrow> w \<Turnstile>\<^sub>n \<phi>1 W\<^sub>n \<phi>2[\<G>\<F> (\<phi>1 W\<^sub>n \<phi>2) w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>1 W\<^sub>n \<phi>2
 7. \<And>\<phi>1 \<phi>2 w. \<lbrakk>\<And>w. w \<Turnstile>\<^sub>n \<phi>1[\<G>\<F> \<phi>1 w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>1; \<And>w. w \<Turnstile>\<^sub>n \<phi>2[\<G>\<F> \<phi>2 w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>2\<rbrakk> \<Longrightarrow> w \<Turnstile>\<^sub>n \<phi>1 M\<^sub>n \<phi>2[\<G>\<F> (\<phi>1 M\<^sub>n \<phi>2) w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>1 M\<^sub>n \<phi>2
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (7 subgoals):
 1. \<And>w. w \<Turnstile>\<^sub>n true\<^sub>n[\<G>\<F> true\<^sub>n w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n true\<^sub>n
 2. \<And>w. w \<Turnstile>\<^sub>n false\<^sub>n[\<G>\<F> false\<^sub>n w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n false\<^sub>n
 3. \<And>x w. w \<Turnstile>\<^sub>n prop\<^sub>n(x)[\<G>\<F> prop\<^sub>n(x) w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n prop\<^sub>n(x)
 4. \<And>x w. w \<Turnstile>\<^sub>n nprop\<^sub>n(x)[\<G>\<F> nprop\<^sub>n(x) w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n nprop\<^sub>n(x)
 5. \<And>\<phi>1 \<phi>2 w. \<lbrakk>\<And>w. w \<Turnstile>\<^sub>n \<phi>1[\<G>\<F> \<phi>1 w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>1; \<And>w. w \<Turnstile>\<^sub>n \<phi>2[\<G>\<F> \<phi>2 w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>2\<rbrakk> \<Longrightarrow> w \<Turnstile>\<^sub>n \<phi>1 R\<^sub>n \<phi>2[\<G>\<F> (\<phi>1 R\<^sub>n \<phi>2) w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>1 R\<^sub>n \<phi>2
 6. \<And>\<phi>1 \<phi>2 w. \<lbrakk>\<And>w. w \<Turnstile>\<^sub>n \<phi>1[\<G>\<F> \<phi>1 w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>1; \<And>w. w \<Turnstile>\<^sub>n \<phi>2[\<G>\<F> \<phi>2 w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>2\<rbrakk> \<Longrightarrow> w \<Turnstile>\<^sub>n \<phi>1 W\<^sub>n \<phi>2[\<G>\<F> (\<phi>1 W\<^sub>n \<phi>2) w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>1 W\<^sub>n \<phi>2
 7. \<And>\<phi>1 \<phi>2 w. \<lbrakk>\<And>w. w \<Turnstile>\<^sub>n \<phi>1[\<G>\<F> \<phi>1 w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>1; \<And>w. w \<Turnstile>\<^sub>n \<phi>2[\<G>\<F> \<phi>2 w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>2\<rbrakk> \<Longrightarrow> w \<Turnstile>\<^sub>n \<phi>1 M\<^sub>n \<phi>2[\<G>\<F> (\<phi>1 M\<^sub>n \<phi>2) w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>1 M\<^sub>n \<phi>2
[PROOF STEP]
case (Release_ltln \<phi>1 \<phi>2)
[PROOF STATE]
proof (state)
this:
?w \<Turnstile>\<^sub>n \<phi>1[\<G>\<F> \<phi>1 ?w]\<^sub>\<Sigma>\<^sub>2 = ?w \<Turnstile>\<^sub>n \<phi>1
?w \<Turnstile>\<^sub>n \<phi>2[\<G>\<F> \<phi>2 ?w]\<^sub>\<Sigma>\<^sub>2 = ?w \<Turnstile>\<^sub>n \<phi>2

goal (7 subgoals):
 1. \<And>w. w \<Turnstile>\<^sub>n true\<^sub>n[\<G>\<F> true\<^sub>n w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n true\<^sub>n
 2. \<And>w. w \<Turnstile>\<^sub>n false\<^sub>n[\<G>\<F> false\<^sub>n w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n false\<^sub>n
 3. \<And>x w. w \<Turnstile>\<^sub>n prop\<^sub>n(x)[\<G>\<F> prop\<^sub>n(x) w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n prop\<^sub>n(x)
 4. \<And>x w. w \<Turnstile>\<^sub>n nprop\<^sub>n(x)[\<G>\<F> nprop\<^sub>n(x) w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n nprop\<^sub>n(x)
 5. \<And>\<phi>1 \<phi>2 w. \<lbrakk>\<And>w. w \<Turnstile>\<^sub>n \<phi>1[\<G>\<F> \<phi>1 w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>1; \<And>w. w \<Turnstile>\<^sub>n \<phi>2[\<G>\<F> \<phi>2 w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>2\<rbrakk> \<Longrightarrow> w \<Turnstile>\<^sub>n \<phi>1 R\<^sub>n \<phi>2[\<G>\<F> (\<phi>1 R\<^sub>n \<phi>2) w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>1 R\<^sub>n \<phi>2
 6. \<And>\<phi>1 \<phi>2 w. \<lbrakk>\<And>w. w \<Turnstile>\<^sub>n \<phi>1[\<G>\<F> \<phi>1 w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>1; \<And>w. w \<Turnstile>\<^sub>n \<phi>2[\<G>\<F> \<phi>2 w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>2\<rbrakk> \<Longrightarrow> w \<Turnstile>\<^sub>n \<phi>1 W\<^sub>n \<phi>2[\<G>\<F> (\<phi>1 W\<^sub>n \<phi>2) w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>1 W\<^sub>n \<phi>2
 7. \<And>\<phi>1 \<phi>2 w. \<lbrakk>\<And>w. w \<Turnstile>\<^sub>n \<phi>1[\<G>\<F> \<phi>1 w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>1; \<And>w. w \<Turnstile>\<^sub>n \<phi>2[\<G>\<F> \<phi>2 w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>2\<rbrakk> \<Longrightarrow> w \<Turnstile>\<^sub>n \<phi>1 M\<^sub>n \<phi>2[\<G>\<F> (\<phi>1 M\<^sub>n \<phi>2) w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>1 M\<^sub>n \<phi>2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
?w \<Turnstile>\<^sub>n \<phi>1[\<G>\<F> \<phi>1 ?w]\<^sub>\<Sigma>\<^sub>2 = ?w \<Turnstile>\<^sub>n \<phi>1
?w \<Turnstile>\<^sub>n \<phi>2[\<G>\<F> \<phi>2 ?w]\<^sub>\<Sigma>\<^sub>2 = ?w \<Turnstile>\<^sub>n \<phi>2
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
?w \<Turnstile>\<^sub>n \<phi>1[\<G>\<F> \<phi>1 ?w]\<^sub>\<Sigma>\<^sub>2 = ?w \<Turnstile>\<^sub>n \<phi>1
?w \<Turnstile>\<^sub>n \<phi>2[\<G>\<F> \<phi>2 ?w]\<^sub>\<Sigma>\<^sub>2 = ?w \<Turnstile>\<^sub>n \<phi>2

goal (1 subgoal):
 1. w \<Turnstile>\<^sub>n \<phi>1 R\<^sub>n \<phi>2[\<G>\<F> (\<phi>1 R\<^sub>n \<phi>2) w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>1 R\<^sub>n \<phi>2
[PROOF STEP]
unfolding ltln_weak_strong_stable_words
[PROOF STATE]
proof (prove)
using this:
?w \<Turnstile>\<^sub>n \<phi>1[\<G>\<F> \<phi>1 ?w]\<^sub>\<Sigma>\<^sub>2 = ?w \<Turnstile>\<^sub>n \<phi>1
?w \<Turnstile>\<^sub>n \<phi>2[\<G>\<F> \<phi>2 ?w]\<^sub>\<Sigma>\<^sub>2 = ?w \<Turnstile>\<^sub>n \<phi>2

goal (1 subgoal):
 1. w \<Turnstile>\<^sub>n \<phi>1 R\<^sub>n \<phi>2[\<G>\<F> (\<phi>1 R\<^sub>n \<phi>2) w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n (\<phi>1 or\<^sub>n G\<^sub>n \<phi>2[\<G>\<F> (\<phi>1 R\<^sub>n \<phi>2) w]\<^sub>\<Pi>\<^sub>1) M\<^sub>n \<phi>2
[PROOF STEP]
using flatten_sigma_2_IH_lifting[of _ "\<phi>1 R\<^sub>n \<phi>2"]
[PROOF STATE]
proof (prove)
using this:
?w \<Turnstile>\<^sub>n \<phi>1[\<G>\<F> \<phi>1 ?w]\<^sub>\<Sigma>\<^sub>2 = ?w \<Turnstile>\<^sub>n \<phi>1
?w \<Turnstile>\<^sub>n \<phi>2[\<G>\<F> \<phi>2 ?w]\<^sub>\<Sigma>\<^sub>2 = ?w \<Turnstile>\<^sub>n \<phi>2
\<lbrakk>?\<psi> \<in> subfrmlsn (\<phi>1 R\<^sub>n \<phi>2); suffix ?i ?w \<Turnstile>\<^sub>n ?\<psi>[\<G>\<F> ?\<psi> (suffix ?i ?w)]\<^sub>\<Sigma>\<^sub>2 = suffix ?i ?w \<Turnstile>\<^sub>n ?\<psi>\<rbrakk> \<Longrightarrow> suffix ?i ?w \<Turnstile>\<^sub>n ?\<psi>[\<G>\<F> (\<phi>1 R\<^sub>n \<phi>2) ?w]\<^sub>\<Sigma>\<^sub>2 = suffix ?i ?w \<Turnstile>\<^sub>n ?\<psi>

goal (1 subgoal):
 1. w \<Turnstile>\<^sub>n \<phi>1 R\<^sub>n \<phi>2[\<G>\<F> (\<phi>1 R\<^sub>n \<phi>2) w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n (\<phi>1 or\<^sub>n G\<^sub>n \<phi>2[\<G>\<F> (\<phi>1 R\<^sub>n \<phi>2) w]\<^sub>\<Pi>\<^sub>1) M\<^sub>n \<phi>2
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
w \<Turnstile>\<^sub>n \<phi>1 R\<^sub>n \<phi>2[\<G>\<F> (\<phi>1 R\<^sub>n \<phi>2) w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>1 R\<^sub>n \<phi>2

goal (6 subgoals):
 1. \<And>w. w \<Turnstile>\<^sub>n true\<^sub>n[\<G>\<F> true\<^sub>n w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n true\<^sub>n
 2. \<And>w. w \<Turnstile>\<^sub>n false\<^sub>n[\<G>\<F> false\<^sub>n w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n false\<^sub>n
 3. \<And>x w. w \<Turnstile>\<^sub>n prop\<^sub>n(x)[\<G>\<F> prop\<^sub>n(x) w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n prop\<^sub>n(x)
 4. \<And>x w. w \<Turnstile>\<^sub>n nprop\<^sub>n(x)[\<G>\<F> nprop\<^sub>n(x) w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n nprop\<^sub>n(x)
 5. \<And>\<phi>1 \<phi>2 w. \<lbrakk>\<And>w. w \<Turnstile>\<^sub>n \<phi>1[\<G>\<F> \<phi>1 w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>1; \<And>w. w \<Turnstile>\<^sub>n \<phi>2[\<G>\<F> \<phi>2 w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>2\<rbrakk> \<Longrightarrow> w \<Turnstile>\<^sub>n \<phi>1 W\<^sub>n \<phi>2[\<G>\<F> (\<phi>1 W\<^sub>n \<phi>2) w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>1 W\<^sub>n \<phi>2
 6. \<And>\<phi>1 \<phi>2 w. \<lbrakk>\<And>w. w \<Turnstile>\<^sub>n \<phi>1[\<G>\<F> \<phi>1 w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>1; \<And>w. w \<Turnstile>\<^sub>n \<phi>2[\<G>\<F> \<phi>2 w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>2\<rbrakk> \<Longrightarrow> w \<Turnstile>\<^sub>n \<phi>1 M\<^sub>n \<phi>2[\<G>\<F> (\<phi>1 M\<^sub>n \<phi>2) w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>1 M\<^sub>n \<phi>2
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (6 subgoals):
 1. \<And>w. w \<Turnstile>\<^sub>n true\<^sub>n[\<G>\<F> true\<^sub>n w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n true\<^sub>n
 2. \<And>w. w \<Turnstile>\<^sub>n false\<^sub>n[\<G>\<F> false\<^sub>n w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n false\<^sub>n
 3. \<And>x w. w \<Turnstile>\<^sub>n prop\<^sub>n(x)[\<G>\<F> prop\<^sub>n(x) w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n prop\<^sub>n(x)
 4. \<And>x w. w \<Turnstile>\<^sub>n nprop\<^sub>n(x)[\<G>\<F> nprop\<^sub>n(x) w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n nprop\<^sub>n(x)
 5. \<And>\<phi>1 \<phi>2 w. \<lbrakk>\<And>w. w \<Turnstile>\<^sub>n \<phi>1[\<G>\<F> \<phi>1 w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>1; \<And>w. w \<Turnstile>\<^sub>n \<phi>2[\<G>\<F> \<phi>2 w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>2\<rbrakk> \<Longrightarrow> w \<Turnstile>\<^sub>n \<phi>1 W\<^sub>n \<phi>2[\<G>\<F> (\<phi>1 W\<^sub>n \<phi>2) w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>1 W\<^sub>n \<phi>2
 6. \<And>\<phi>1 \<phi>2 w. \<lbrakk>\<And>w. w \<Turnstile>\<^sub>n \<phi>1[\<G>\<F> \<phi>1 w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>1; \<And>w. w \<Turnstile>\<^sub>n \<phi>2[\<G>\<F> \<phi>2 w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>2\<rbrakk> \<Longrightarrow> w \<Turnstile>\<^sub>n \<phi>1 M\<^sub>n \<phi>2[\<G>\<F> (\<phi>1 M\<^sub>n \<phi>2) w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>1 M\<^sub>n \<phi>2
[PROOF STEP]
case (WeakUntil_ltln \<phi>1 \<phi>2)
[PROOF STATE]
proof (state)
this:
?w \<Turnstile>\<^sub>n \<phi>1[\<G>\<F> \<phi>1 ?w]\<^sub>\<Sigma>\<^sub>2 = ?w \<Turnstile>\<^sub>n \<phi>1
?w \<Turnstile>\<^sub>n \<phi>2[\<G>\<F> \<phi>2 ?w]\<^sub>\<Sigma>\<^sub>2 = ?w \<Turnstile>\<^sub>n \<phi>2

goal (6 subgoals):
 1. \<And>w. w \<Turnstile>\<^sub>n true\<^sub>n[\<G>\<F> true\<^sub>n w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n true\<^sub>n
 2. \<And>w. w \<Turnstile>\<^sub>n false\<^sub>n[\<G>\<F> false\<^sub>n w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n false\<^sub>n
 3. \<And>x w. w \<Turnstile>\<^sub>n prop\<^sub>n(x)[\<G>\<F> prop\<^sub>n(x) w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n prop\<^sub>n(x)
 4. \<And>x w. w \<Turnstile>\<^sub>n nprop\<^sub>n(x)[\<G>\<F> nprop\<^sub>n(x) w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n nprop\<^sub>n(x)
 5. \<And>\<phi>1 \<phi>2 w. \<lbrakk>\<And>w. w \<Turnstile>\<^sub>n \<phi>1[\<G>\<F> \<phi>1 w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>1; \<And>w. w \<Turnstile>\<^sub>n \<phi>2[\<G>\<F> \<phi>2 w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>2\<rbrakk> \<Longrightarrow> w \<Turnstile>\<^sub>n \<phi>1 W\<^sub>n \<phi>2[\<G>\<F> (\<phi>1 W\<^sub>n \<phi>2) w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>1 W\<^sub>n \<phi>2
 6. \<And>\<phi>1 \<phi>2 w. \<lbrakk>\<And>w. w \<Turnstile>\<^sub>n \<phi>1[\<G>\<F> \<phi>1 w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>1; \<And>w. w \<Turnstile>\<^sub>n \<phi>2[\<G>\<F> \<phi>2 w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>2\<rbrakk> \<Longrightarrow> w \<Turnstile>\<^sub>n \<phi>1 M\<^sub>n \<phi>2[\<G>\<F> (\<phi>1 M\<^sub>n \<phi>2) w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>1 M\<^sub>n \<phi>2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
?w \<Turnstile>\<^sub>n \<phi>1[\<G>\<F> \<phi>1 ?w]\<^sub>\<Sigma>\<^sub>2 = ?w \<Turnstile>\<^sub>n \<phi>1
?w \<Turnstile>\<^sub>n \<phi>2[\<G>\<F> \<phi>2 ?w]\<^sub>\<Sigma>\<^sub>2 = ?w \<Turnstile>\<^sub>n \<phi>2
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
?w \<Turnstile>\<^sub>n \<phi>1[\<G>\<F> \<phi>1 ?w]\<^sub>\<Sigma>\<^sub>2 = ?w \<Turnstile>\<^sub>n \<phi>1
?w \<Turnstile>\<^sub>n \<phi>2[\<G>\<F> \<phi>2 ?w]\<^sub>\<Sigma>\<^sub>2 = ?w \<Turnstile>\<^sub>n \<phi>2

goal (1 subgoal):
 1. w \<Turnstile>\<^sub>n \<phi>1 W\<^sub>n \<phi>2[\<G>\<F> (\<phi>1 W\<^sub>n \<phi>2) w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>1 W\<^sub>n \<phi>2
[PROOF STEP]
unfolding ltln_weak_strong_stable_words
[PROOF STATE]
proof (prove)
using this:
?w \<Turnstile>\<^sub>n \<phi>1[\<G>\<F> \<phi>1 ?w]\<^sub>\<Sigma>\<^sub>2 = ?w \<Turnstile>\<^sub>n \<phi>1
?w \<Turnstile>\<^sub>n \<phi>2[\<G>\<F> \<phi>2 ?w]\<^sub>\<Sigma>\<^sub>2 = ?w \<Turnstile>\<^sub>n \<phi>2

goal (1 subgoal):
 1. w \<Turnstile>\<^sub>n \<phi>1 W\<^sub>n \<phi>2[\<G>\<F> (\<phi>1 W\<^sub>n \<phi>2) w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>1 U\<^sub>n (\<phi>2 or\<^sub>n G\<^sub>n \<phi>1[\<G>\<F> (\<phi>1 W\<^sub>n \<phi>2) w]\<^sub>\<Pi>\<^sub>1)
[PROOF STEP]
using flatten_sigma_2_IH_lifting[of _ "\<phi>1 W\<^sub>n \<phi>2"]
[PROOF STATE]
proof (prove)
using this:
?w \<Turnstile>\<^sub>n \<phi>1[\<G>\<F> \<phi>1 ?w]\<^sub>\<Sigma>\<^sub>2 = ?w \<Turnstile>\<^sub>n \<phi>1
?w \<Turnstile>\<^sub>n \<phi>2[\<G>\<F> \<phi>2 ?w]\<^sub>\<Sigma>\<^sub>2 = ?w \<Turnstile>\<^sub>n \<phi>2
\<lbrakk>?\<psi> \<in> subfrmlsn (\<phi>1 W\<^sub>n \<phi>2); suffix ?i ?w \<Turnstile>\<^sub>n ?\<psi>[\<G>\<F> ?\<psi> (suffix ?i ?w)]\<^sub>\<Sigma>\<^sub>2 = suffix ?i ?w \<Turnstile>\<^sub>n ?\<psi>\<rbrakk> \<Longrightarrow> suffix ?i ?w \<Turnstile>\<^sub>n ?\<psi>[\<G>\<F> (\<phi>1 W\<^sub>n \<phi>2) ?w]\<^sub>\<Sigma>\<^sub>2 = suffix ?i ?w \<Turnstile>\<^sub>n ?\<psi>

goal (1 subgoal):
 1. w \<Turnstile>\<^sub>n \<phi>1 W\<^sub>n \<phi>2[\<G>\<F> (\<phi>1 W\<^sub>n \<phi>2) w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>1 U\<^sub>n (\<phi>2 or\<^sub>n G\<^sub>n \<phi>1[\<G>\<F> (\<phi>1 W\<^sub>n \<phi>2) w]\<^sub>\<Pi>\<^sub>1)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
w \<Turnstile>\<^sub>n \<phi>1 W\<^sub>n \<phi>2[\<G>\<F> (\<phi>1 W\<^sub>n \<phi>2) w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>1 W\<^sub>n \<phi>2

goal (5 subgoals):
 1. \<And>w. w \<Turnstile>\<^sub>n true\<^sub>n[\<G>\<F> true\<^sub>n w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n true\<^sub>n
 2. \<And>w. w \<Turnstile>\<^sub>n false\<^sub>n[\<G>\<F> false\<^sub>n w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n false\<^sub>n
 3. \<And>x w. w \<Turnstile>\<^sub>n prop\<^sub>n(x)[\<G>\<F> prop\<^sub>n(x) w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n prop\<^sub>n(x)
 4. \<And>x w. w \<Turnstile>\<^sub>n nprop\<^sub>n(x)[\<G>\<F> nprop\<^sub>n(x) w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n nprop\<^sub>n(x)
 5. \<And>\<phi>1 \<phi>2 w. \<lbrakk>\<And>w. w \<Turnstile>\<^sub>n \<phi>1[\<G>\<F> \<phi>1 w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>1; \<And>w. w \<Turnstile>\<^sub>n \<phi>2[\<G>\<F> \<phi>2 w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>2\<rbrakk> \<Longrightarrow> w \<Turnstile>\<^sub>n \<phi>1 M\<^sub>n \<phi>2[\<G>\<F> (\<phi>1 M\<^sub>n \<phi>2) w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>1 M\<^sub>n \<phi>2
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>w. w \<Turnstile>\<^sub>n true\<^sub>n[\<G>\<F> true\<^sub>n w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n true\<^sub>n
 2. \<And>w. w \<Turnstile>\<^sub>n false\<^sub>n[\<G>\<F> false\<^sub>n w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n false\<^sub>n
 3. \<And>x w. w \<Turnstile>\<^sub>n prop\<^sub>n(x)[\<G>\<F> prop\<^sub>n(x) w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n prop\<^sub>n(x)
 4. \<And>x w. w \<Turnstile>\<^sub>n nprop\<^sub>n(x)[\<G>\<F> nprop\<^sub>n(x) w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n nprop\<^sub>n(x)
 5. \<And>\<phi>1 \<phi>2 w. \<lbrakk>\<And>w. w \<Turnstile>\<^sub>n \<phi>1[\<G>\<F> \<phi>1 w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>1; \<And>w. w \<Turnstile>\<^sub>n \<phi>2[\<G>\<F> \<phi>2 w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>2\<rbrakk> \<Longrightarrow> w \<Turnstile>\<^sub>n \<phi>1 M\<^sub>n \<phi>2[\<G>\<F> (\<phi>1 M\<^sub>n \<phi>2) w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>1 M\<^sub>n \<phi>2
[PROOF STEP]
case (StrongRelease_ltln \<phi>1 \<phi>2)
[PROOF STATE]
proof (state)
this:
?w \<Turnstile>\<^sub>n \<phi>1[\<G>\<F> \<phi>1 ?w]\<^sub>\<Sigma>\<^sub>2 = ?w \<Turnstile>\<^sub>n \<phi>1
?w \<Turnstile>\<^sub>n \<phi>2[\<G>\<F> \<phi>2 ?w]\<^sub>\<Sigma>\<^sub>2 = ?w \<Turnstile>\<^sub>n \<phi>2

goal (5 subgoals):
 1. \<And>w. w \<Turnstile>\<^sub>n true\<^sub>n[\<G>\<F> true\<^sub>n w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n true\<^sub>n
 2. \<And>w. w \<Turnstile>\<^sub>n false\<^sub>n[\<G>\<F> false\<^sub>n w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n false\<^sub>n
 3. \<And>x w. w \<Turnstile>\<^sub>n prop\<^sub>n(x)[\<G>\<F> prop\<^sub>n(x) w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n prop\<^sub>n(x)
 4. \<And>x w. w \<Turnstile>\<^sub>n nprop\<^sub>n(x)[\<G>\<F> nprop\<^sub>n(x) w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n nprop\<^sub>n(x)
 5. \<And>\<phi>1 \<phi>2 w. \<lbrakk>\<And>w. w \<Turnstile>\<^sub>n \<phi>1[\<G>\<F> \<phi>1 w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>1; \<And>w. w \<Turnstile>\<^sub>n \<phi>2[\<G>\<F> \<phi>2 w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>2\<rbrakk> \<Longrightarrow> w \<Turnstile>\<^sub>n \<phi>1 M\<^sub>n \<phi>2[\<G>\<F> (\<phi>1 M\<^sub>n \<phi>2) w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>1 M\<^sub>n \<phi>2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
?w \<Turnstile>\<^sub>n \<phi>1[\<G>\<F> \<phi>1 ?w]\<^sub>\<Sigma>\<^sub>2 = ?w \<Turnstile>\<^sub>n \<phi>1
?w \<Turnstile>\<^sub>n \<phi>2[\<G>\<F> \<phi>2 ?w]\<^sub>\<Sigma>\<^sub>2 = ?w \<Turnstile>\<^sub>n \<phi>2
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
?w \<Turnstile>\<^sub>n \<phi>1[\<G>\<F> \<phi>1 ?w]\<^sub>\<Sigma>\<^sub>2 = ?w \<Turnstile>\<^sub>n \<phi>1
?w \<Turnstile>\<^sub>n \<phi>2[\<G>\<F> \<phi>2 ?w]\<^sub>\<Sigma>\<^sub>2 = ?w \<Turnstile>\<^sub>n \<phi>2

goal (1 subgoal):
 1. w \<Turnstile>\<^sub>n \<phi>1 M\<^sub>n \<phi>2[\<G>\<F> (\<phi>1 M\<^sub>n \<phi>2) w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>1 M\<^sub>n \<phi>2
[PROOF STEP]
using flatten_sigma_2_IH_lifting[of _ "\<phi>1 M\<^sub>n \<phi>2"]
[PROOF STATE]
proof (prove)
using this:
?w \<Turnstile>\<^sub>n \<phi>1[\<G>\<F> \<phi>1 ?w]\<^sub>\<Sigma>\<^sub>2 = ?w \<Turnstile>\<^sub>n \<phi>1
?w \<Turnstile>\<^sub>n \<phi>2[\<G>\<F> \<phi>2 ?w]\<^sub>\<Sigma>\<^sub>2 = ?w \<Turnstile>\<^sub>n \<phi>2
\<lbrakk>?\<psi> \<in> subfrmlsn (\<phi>1 M\<^sub>n \<phi>2); suffix ?i ?w \<Turnstile>\<^sub>n ?\<psi>[\<G>\<F> ?\<psi> (suffix ?i ?w)]\<^sub>\<Sigma>\<^sub>2 = suffix ?i ?w \<Turnstile>\<^sub>n ?\<psi>\<rbrakk> \<Longrightarrow> suffix ?i ?w \<Turnstile>\<^sub>n ?\<psi>[\<G>\<F> (\<phi>1 M\<^sub>n \<phi>2) ?w]\<^sub>\<Sigma>\<^sub>2 = suffix ?i ?w \<Turnstile>\<^sub>n ?\<psi>

goal (1 subgoal):
 1. w \<Turnstile>\<^sub>n \<phi>1 M\<^sub>n \<phi>2[\<G>\<F> (\<phi>1 M\<^sub>n \<phi>2) w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>1 M\<^sub>n \<phi>2
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
w \<Turnstile>\<^sub>n \<phi>1 M\<^sub>n \<phi>2[\<G>\<F> (\<phi>1 M\<^sub>n \<phi>2) w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>1 M\<^sub>n \<phi>2

goal (4 subgoals):
 1. \<And>w. w \<Turnstile>\<^sub>n true\<^sub>n[\<G>\<F> true\<^sub>n w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n true\<^sub>n
 2. \<And>w. w \<Turnstile>\<^sub>n false\<^sub>n[\<G>\<F> false\<^sub>n w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n false\<^sub>n
 3. \<And>x w. w \<Turnstile>\<^sub>n prop\<^sub>n(x)[\<G>\<F> prop\<^sub>n(x) w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n prop\<^sub>n(x)
 4. \<And>x w. w \<Turnstile>\<^sub>n nprop\<^sub>n(x)[\<G>\<F> nprop\<^sub>n(x) w]\<^sub>\<Sigma>\<^sub>2 = w \<Turnstile>\<^sub>n nprop\<^sub>n(x)
[PROOF STEP]
qed auto


[STATEMENT]
lemma ltln_strong_weak_stable_words_1:
  "w \<Turnstile>\<^sub>n \<phi> U\<^sub>n \<psi> \<longleftrightarrow> w \<Turnstile>\<^sub>n (\<phi> and\<^sub>n (F\<^sub>n \<psi>[\<F>\<G> \<psi> w]\<^sub>\<Sigma>\<^sub>1)) W\<^sub>n \<psi>" (is "?lhs \<longleftrightarrow> ?rhs")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. w \<Turnstile>\<^sub>n \<phi> U\<^sub>n \<psi> = w \<Turnstile>\<^sub>n (\<phi> and\<^sub>n F\<^sub>n \<psi>[\<F>\<G> \<psi> w]\<^sub>\<Sigma>\<^sub>1) W\<^sub>n \<psi>
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. w \<Turnstile>\<^sub>n \<phi> U\<^sub>n \<psi> \<Longrightarrow> w \<Turnstile>\<^sub>n (\<phi> and\<^sub>n F\<^sub>n \<psi>[\<F>\<G> \<psi> w]\<^sub>\<Sigma>\<^sub>1) W\<^sub>n \<psi>
 2. w \<Turnstile>\<^sub>n (\<phi> and\<^sub>n F\<^sub>n \<psi>[\<F>\<G> \<psi> w]\<^sub>\<Sigma>\<^sub>1) W\<^sub>n \<psi> \<Longrightarrow> w \<Turnstile>\<^sub>n \<phi> U\<^sub>n \<psi>
[PROOF STEP]
assume ?rhs
[PROOF STATE]
proof (state)
this:
w \<Turnstile>\<^sub>n (\<phi> and\<^sub>n F\<^sub>n \<psi>[\<F>\<G> \<psi> w]\<^sub>\<Sigma>\<^sub>1) W\<^sub>n \<psi>

goal (2 subgoals):
 1. w \<Turnstile>\<^sub>n \<phi> U\<^sub>n \<psi> \<Longrightarrow> w \<Turnstile>\<^sub>n (\<phi> and\<^sub>n F\<^sub>n \<psi>[\<F>\<G> \<psi> w]\<^sub>\<Sigma>\<^sub>1) W\<^sub>n \<psi>
 2. w \<Turnstile>\<^sub>n (\<phi> and\<^sub>n F\<^sub>n \<psi>[\<F>\<G> \<psi> w]\<^sub>\<Sigma>\<^sub>1) W\<^sub>n \<psi> \<Longrightarrow> w \<Turnstile>\<^sub>n \<phi> U\<^sub>n \<psi>
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
w \<Turnstile>\<^sub>n (\<phi> and\<^sub>n F\<^sub>n \<psi>[\<F>\<G> \<psi> w]\<^sub>\<Sigma>\<^sub>1) W\<^sub>n \<psi>

goal (2 subgoals):
 1. w \<Turnstile>\<^sub>n \<phi> U\<^sub>n \<psi> \<Longrightarrow> w \<Turnstile>\<^sub>n (\<phi> and\<^sub>n F\<^sub>n \<psi>[\<F>\<G> \<psi> w]\<^sub>\<Sigma>\<^sub>1) W\<^sub>n \<psi>
 2. w \<Turnstile>\<^sub>n (\<phi> and\<^sub>n F\<^sub>n \<psi>[\<F>\<G> \<psi> w]\<^sub>\<Sigma>\<^sub>1) W\<^sub>n \<psi> \<Longrightarrow> w \<Turnstile>\<^sub>n \<phi> U\<^sub>n \<psi>
[PROOF STEP]
obtain i where "\<nu>_stable \<psi> (suffix i w)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>i. \<nu>_stable \<psi> (suffix i w) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis MOST_nat less_Suc_eq suffix_\<nu>_stable)
[PROOF STATE]
proof (state)
this:
\<nu>_stable \<psi> (suffix i w)

goal (2 subgoals):
 1. w \<Turnstile>\<^sub>n \<phi> U\<^sub>n \<psi> \<Longrightarrow> w \<Turnstile>\<^sub>n (\<phi> and\<^sub>n F\<^sub>n \<psi>[\<F>\<G> \<psi> w]\<^sub>\<Sigma>\<^sub>1) W\<^sub>n \<psi>
 2. w \<Turnstile>\<^sub>n (\<phi> and\<^sub>n F\<^sub>n \<psi>[\<F>\<G> \<psi> w]\<^sub>\<Sigma>\<^sub>1) W\<^sub>n \<psi> \<Longrightarrow> w \<Turnstile>\<^sub>n \<phi> U\<^sub>n \<psi>
[PROOF STEP]
hence "\<forall>\<psi> \<in> \<F>\<G> \<psi> w. suffix i w \<Turnstile>\<^sub>n G\<^sub>n \<psi>"
[PROOF STATE]
proof (prove)
using this:
\<nu>_stable \<psi> (suffix i w)

goal (1 subgoal):
 1. \<forall>\<psi>\<in>\<F>\<G> \<psi> w. suffix i w \<Turnstile>\<^sub>n G\<^sub>n \<psi>
[PROOF STEP]
using \<F>\<G>_suffix \<G>_elim \<nu>_stable_def
[PROOF STATE]
proof (prove)
using this:
\<nu>_stable \<psi> (suffix i w)
\<F>\<G> ?\<phi> (suffix ?i ?w) = \<F>\<G> ?\<phi> ?w
?\<psi> \<in> \<G> ?\<phi> ?w \<Longrightarrow> ?w \<Turnstile>\<^sub>n G\<^sub>n ?\<psi>
\<nu>_stable ?\<phi> ?w = (\<F>\<G> ?\<phi> ?w = \<G> ?\<phi> ?w)

goal (1 subgoal):
 1. \<forall>\<psi>\<in>\<F>\<G> \<psi> w. suffix i w \<Turnstile>\<^sub>n G\<^sub>n \<psi>
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<forall>\<psi>\<in>\<F>\<G> \<psi> w. suffix i w \<Turnstile>\<^sub>n G\<^sub>n \<psi>

goal (2 subgoals):
 1. w \<Turnstile>\<^sub>n \<phi> U\<^sub>n \<psi> \<Longrightarrow> w \<Turnstile>\<^sub>n (\<phi> and\<^sub>n F\<^sub>n \<psi>[\<F>\<G> \<psi> w]\<^sub>\<Sigma>\<^sub>1) W\<^sub>n \<psi>
 2. w \<Turnstile>\<^sub>n (\<phi> and\<^sub>n F\<^sub>n \<psi>[\<F>\<G> \<psi> w]\<^sub>\<Sigma>\<^sub>1) W\<^sub>n \<psi> \<Longrightarrow> w \<Turnstile>\<^sub>n \<phi> U\<^sub>n \<psi>
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
\<forall>\<psi>\<in>\<F>\<G> \<psi> w. suffix i w \<Turnstile>\<^sub>n G\<^sub>n \<psi>

goal (2 subgoals):
 1. w \<Turnstile>\<^sub>n \<phi> U\<^sub>n \<psi> \<Longrightarrow> w \<Turnstile>\<^sub>n (\<phi> and\<^sub>n F\<^sub>n \<psi>[\<F>\<G> \<psi> w]\<^sub>\<Sigma>\<^sub>1) W\<^sub>n \<psi>
 2. w \<Turnstile>\<^sub>n (\<phi> and\<^sub>n F\<^sub>n \<psi>[\<F>\<G> \<psi> w]\<^sub>\<Sigma>\<^sub>1) W\<^sub>n \<psi> \<Longrightarrow> w \<Turnstile>\<^sub>n \<phi> U\<^sub>n \<psi>
[PROOF STEP]
assume assm: "w \<Turnstile>\<^sub>n G\<^sub>n (\<phi> and\<^sub>n (F\<^sub>n \<psi>[\<F>\<G> \<psi> w]\<^sub>\<Sigma>\<^sub>1))"
[PROOF STATE]
proof (state)
this:
w \<Turnstile>\<^sub>n G\<^sub>n (\<phi> and\<^sub>n F\<^sub>n \<psi>[\<F>\<G> \<psi> w]\<^sub>\<Sigma>\<^sub>1)

goal (2 subgoals):
 1. w \<Turnstile>\<^sub>n \<phi> U\<^sub>n \<psi> \<Longrightarrow> w \<Turnstile>\<^sub>n (\<phi> and\<^sub>n F\<^sub>n \<psi>[\<F>\<G> \<psi> w]\<^sub>\<Sigma>\<^sub>1) W\<^sub>n \<psi>
 2. w \<Turnstile>\<^sub>n (\<phi> and\<^sub>n F\<^sub>n \<psi>[\<F>\<G> \<psi> w]\<^sub>\<Sigma>\<^sub>1) W\<^sub>n \<psi> \<Longrightarrow> w \<Turnstile>\<^sub>n \<phi> U\<^sub>n \<psi>
[PROOF STEP]
hence "suffix i w \<Turnstile>\<^sub>n (F\<^sub>n \<psi>)[\<F>\<G> \<psi> w]\<^sub>\<Sigma>\<^sub>1"
[PROOF STATE]
proof (prove)
using this:
w \<Turnstile>\<^sub>n G\<^sub>n (\<phi> and\<^sub>n F\<^sub>n \<psi>[\<F>\<G> \<psi> w]\<^sub>\<Sigma>\<^sub>1)

goal (1 subgoal):
 1. suffix i w \<Turnstile>\<^sub>n (F\<^sub>n \<psi>)[\<F>\<G> \<psi> w]\<^sub>\<Sigma>\<^sub>1
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
suffix i w \<Turnstile>\<^sub>n (F\<^sub>n \<psi>)[\<F>\<G> \<psi> w]\<^sub>\<Sigma>\<^sub>1

goal (2 subgoals):
 1. w \<Turnstile>\<^sub>n \<phi> U\<^sub>n \<psi> \<Longrightarrow> w \<Turnstile>\<^sub>n (\<phi> and\<^sub>n F\<^sub>n \<psi>[\<F>\<G> \<psi> w]\<^sub>\<Sigma>\<^sub>1) W\<^sub>n \<psi>
 2. w \<Turnstile>\<^sub>n (\<phi> and\<^sub>n F\<^sub>n \<psi>[\<F>\<G> \<psi> w]\<^sub>\<Sigma>\<^sub>1) W\<^sub>n \<psi> \<Longrightarrow> w \<Turnstile>\<^sub>n \<phi> U\<^sub>n \<psi>
[PROOF STEP]
hence "suffix i w \<Turnstile>\<^sub>n F\<^sub>n \<psi>"
[PROOF STATE]
proof (prove)
using this:
suffix i w \<Turnstile>\<^sub>n (F\<^sub>n \<psi>)[\<F>\<G> \<psi> w]\<^sub>\<Sigma>\<^sub>1

goal (1 subgoal):
 1. suffix i w \<Turnstile>\<^sub>n F\<^sub>n \<psi>
[PROOF STEP]
by (blast dest: FG_advice_b2_helper[OF \<open>\<forall>\<psi> \<in> \<F>\<G> \<psi> w. suffix i w \<Turnstile>\<^sub>n G\<^sub>n \<psi>\<close>])
[PROOF STATE]
proof (state)
this:
suffix i w \<Turnstile>\<^sub>n F\<^sub>n \<psi>

goal (2 subgoals):
 1. w \<Turnstile>\<^sub>n \<phi> U\<^sub>n \<psi> \<Longrightarrow> w \<Turnstile>\<^sub>n (\<phi> and\<^sub>n F\<^sub>n \<psi>[\<F>\<G> \<psi> w]\<^sub>\<Sigma>\<^sub>1) W\<^sub>n \<psi>
 2. w \<Turnstile>\<^sub>n (\<phi> and\<^sub>n F\<^sub>n \<psi>[\<F>\<G> \<psi> w]\<^sub>\<Sigma>\<^sub>1) W\<^sub>n \<psi> \<Longrightarrow> w \<Turnstile>\<^sub>n \<phi> U\<^sub>n \<psi>
[PROOF STEP]
hence "w \<Turnstile>\<^sub>n \<phi> U\<^sub>n \<psi>"
[PROOF STATE]
proof (prove)
using this:
suffix i w \<Turnstile>\<^sub>n F\<^sub>n \<psi>

goal (1 subgoal):
 1. w \<Turnstile>\<^sub>n \<phi> U\<^sub>n \<psi>
[PROOF STEP]
using assm
[PROOF STATE]
proof (prove)
using this:
suffix i w \<Turnstile>\<^sub>n F\<^sub>n \<psi>
w \<Turnstile>\<^sub>n G\<^sub>n (\<phi> and\<^sub>n F\<^sub>n \<psi>[\<F>\<G> \<psi> w]\<^sub>\<Sigma>\<^sub>1)

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

goal (2 subgoals):
 1. w \<Turnstile>\<^sub>n \<phi> U\<^sub>n \<psi> \<Longrightarrow> w \<Turnstile>\<^sub>n (\<phi> and\<^sub>n F\<^sub>n \<psi>[\<F>\<G> \<psi> w]\<^sub>\<Sigma>\<^sub>1) W\<^sub>n \<psi>
 2. w \<Turnstile>\<^sub>n (\<phi> and\<^sub>n F\<^sub>n \<psi>[\<F>\<G> \<psi> w]\<^sub>\<Sigma>\<^sub>1) W\<^sub>n \<psi> \<Longrightarrow> w \<Turnstile>\<^sub>n \<phi> U\<^sub>n \<psi>
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
w \<Turnstile>\<^sub>n G\<^sub>n (\<phi> and\<^sub>n F\<^sub>n \<psi>[\<F>\<G> \<psi> w]\<^sub>\<Sigma>\<^sub>1) \<Longrightarrow> w \<Turnstile>\<^sub>n \<phi> U\<^sub>n \<psi>

goal (2 subgoals):
 1. w \<Turnstile>\<^sub>n \<phi> U\<^sub>n \<psi> \<Longrightarrow> w \<Turnstile>\<^sub>n (\<phi> and\<^sub>n F\<^sub>n \<psi>[\<F>\<G> \<psi> w]\<^sub>\<Sigma>\<^sub>1) W\<^sub>n \<psi>
 2. w \<Turnstile>\<^sub>n (\<phi> and\<^sub>n F\<^sub>n \<psi>[\<F>\<G> \<psi> w]\<^sub>\<Sigma>\<^sub>1) W\<^sub>n \<psi> \<Longrightarrow> w \<Turnstile>\<^sub>n \<phi> U\<^sub>n \<psi>
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
w \<Turnstile>\<^sub>n (\<phi> and\<^sub>n F\<^sub>n \<psi>[\<F>\<G> \<psi> w]\<^sub>\<Sigma>\<^sub>1) W\<^sub>n \<psi>
w \<Turnstile>\<^sub>n G\<^sub>n (\<phi> and\<^sub>n F\<^sub>n \<psi>[\<F>\<G> \<psi> w]\<^sub>\<Sigma>\<^sub>1) \<Longrightarrow> w \<Turnstile>\<^sub>n \<phi> U\<^sub>n \<psi>
[PROOF STEP]
show ?lhs
[PROOF STATE]
proof (prove)
using this:
w \<Turnstile>\<^sub>n (\<phi> and\<^sub>n F\<^sub>n \<psi>[\<F>\<G> \<psi> w]\<^sub>\<Sigma>\<^sub>1) W\<^sub>n \<psi>
w \<Turnstile>\<^sub>n G\<^sub>n (\<phi> and\<^sub>n F\<^sub>n \<psi>[\<F>\<G> \<psi> w]\<^sub>\<Sigma>\<^sub>1) \<Longrightarrow> w \<Turnstile>\<^sub>n \<phi> U\<^sub>n \<psi>

goal (1 subgoal):
 1. w \<Turnstile>\<^sub>n \<phi> U\<^sub>n \<psi>
[PROOF STEP]
by (meson ltln_weak_to_strong(1) semantics_ltln.simps(5) until_and_left_distrib)
[PROOF STATE]
proof (state)
this:
w \<Turnstile>\<^sub>n \<phi> U\<^sub>n \<psi>

goal (1 subgoal):
 1. w \<Turnstile>\<^sub>n \<phi> U\<^sub>n \<psi> \<Longrightarrow> w \<Turnstile>\<^sub>n (\<phi> and\<^sub>n F\<^sub>n \<psi>[\<F>\<G> \<psi> w]\<^sub>\<Sigma>\<^sub>1) W\<^sub>n \<psi>
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. w \<Turnstile>\<^sub>n \<phi> U\<^sub>n \<psi> \<Longrightarrow> w \<Turnstile>\<^sub>n (\<phi> and\<^sub>n F\<^sub>n \<psi>[\<F>\<G> \<psi> w]\<^sub>\<Sigma>\<^sub>1) W\<^sub>n \<psi>
[PROOF STEP]
assume ?lhs
[PROOF STATE]
proof (state)
this:
w \<Turnstile>\<^sub>n \<phi> U\<^sub>n \<psi>

goal (1 subgoal):
 1. w \<Turnstile>\<^sub>n \<phi> U\<^sub>n \<psi> \<Longrightarrow> w \<Turnstile>\<^sub>n (\<phi> and\<^sub>n F\<^sub>n \<psi>[\<F>\<G> \<psi> w]\<^sub>\<Sigma>\<^sub>1) W\<^sub>n \<psi>
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
w \<Turnstile>\<^sub>n \<phi> U\<^sub>n \<psi>

goal (1 subgoal):
 1. w \<Turnstile>\<^sub>n \<phi> U\<^sub>n \<psi> \<Longrightarrow> w \<Turnstile>\<^sub>n (\<phi> and\<^sub>n F\<^sub>n \<psi>[\<F>\<G> \<psi> w]\<^sub>\<Sigma>\<^sub>1) W\<^sub>n \<psi>
[PROOF STEP]
have "\<And>i. suffix i w \<Turnstile>\<^sub>n \<psi> \<Longrightarrow> suffix i w \<Turnstile>\<^sub>n \<psi>[\<F>\<G> \<psi> w]\<^sub>\<Sigma>\<^sub>1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i. suffix i w \<Turnstile>\<^sub>n \<psi> \<Longrightarrow> suffix i w \<Turnstile>\<^sub>n \<psi>[\<F>\<G> \<psi> w]\<^sub>\<Sigma>\<^sub>1
[PROOF STEP]
using \<F>\<G>_suffix
[PROOF STATE]
proof (prove)
using this:
\<F>\<G> ?\<phi> (suffix ?i ?w) = \<F>\<G> ?\<phi> ?w

goal (1 subgoal):
 1. \<And>i. suffix i w \<Turnstile>\<^sub>n \<psi> \<Longrightarrow> suffix i w \<Turnstile>\<^sub>n \<psi>[\<F>\<G> \<psi> w]\<^sub>\<Sigma>\<^sub>1
[PROOF STEP]
by (blast intro: FG_advice_b1)
[PROOF STATE]
proof (state)
this:
suffix ?i w \<Turnstile>\<^sub>n \<psi> \<Longrightarrow> suffix ?i w \<Turnstile>\<^sub>n \<psi>[\<F>\<G> \<psi> w]\<^sub>\<Sigma>\<^sub>1

goal (1 subgoal):
 1. w \<Turnstile>\<^sub>n \<phi> U\<^sub>n \<psi> \<Longrightarrow> w \<Turnstile>\<^sub>n (\<phi> and\<^sub>n F\<^sub>n \<psi>[\<F>\<G> \<psi> w]\<^sub>\<Sigma>\<^sub>1) W\<^sub>n \<psi>
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
w \<Turnstile>\<^sub>n \<phi> U\<^sub>n \<psi>
suffix ?i w \<Turnstile>\<^sub>n \<psi> \<Longrightarrow> suffix ?i w \<Turnstile>\<^sub>n \<psi>[\<F>\<G> \<psi> w]\<^sub>\<Sigma>\<^sub>1
[PROOF STEP]
show "?rhs"
[PROOF STATE]
proof (prove)
using this:
w \<Turnstile>\<^sub>n \<phi> U\<^sub>n \<psi>
suffix ?i w \<Turnstile>\<^sub>n \<psi> \<Longrightarrow> suffix ?i w \<Turnstile>\<^sub>n \<psi>[\<F>\<G> \<psi> w]\<^sub>\<Sigma>\<^sub>1

goal (1 subgoal):
 1. w \<Turnstile>\<^sub>n (\<phi> and\<^sub>n F\<^sub>n \<psi>[\<F>\<G> \<psi> w]\<^sub>\<Sigma>\<^sub>1) W\<^sub>n \<psi>
[PROOF STEP]
unfolding ltln_strong_weak_2
[PROOF STATE]
proof (prove)
using this:
w \<Turnstile>\<^sub>n (\<phi> and\<^sub>n F\<^sub>n \<psi>) W\<^sub>n \<psi>
suffix ?i w \<Turnstile>\<^sub>n \<psi> \<Longrightarrow> suffix ?i w \<Turnstile>\<^sub>n \<psi>[\<F>\<G> \<psi> w]\<^sub>\<Sigma>\<^sub>1

goal (1 subgoal):
 1. w \<Turnstile>\<^sub>n (\<phi> and\<^sub>n F\<^sub>n \<psi>[\<F>\<G> \<psi> w]\<^sub>\<Sigma>\<^sub>1) W\<^sub>n \<psi>
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
w \<Turnstile>\<^sub>n (\<phi> and\<^sub>n F\<^sub>n \<psi>[\<F>\<G> \<psi> w]\<^sub>\<Sigma>\<^sub>1) W\<^sub>n \<psi>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ltln_strong_weak_stable_words_2:
  "w \<Turnstile>\<^sub>n \<phi> M\<^sub>n \<psi> \<longleftrightarrow> w \<Turnstile>\<^sub>n \<phi> R\<^sub>n (\<psi> and\<^sub>n (F\<^sub>n \<phi>[\<F>\<G> \<phi> w]\<^sub>\<Sigma>\<^sub>1))" (is "?lhs \<longleftrightarrow> ?rhs")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. w \<Turnstile>\<^sub>n \<phi> M\<^sub>n \<psi> = w \<Turnstile>\<^sub>n \<phi> R\<^sub>n (\<psi> and\<^sub>n F\<^sub>n \<phi>[\<F>\<G> \<phi> w]\<^sub>\<Sigma>\<^sub>1)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. w \<Turnstile>\<^sub>n \<phi> M\<^sub>n \<psi> \<Longrightarrow> w \<Turnstile>\<^sub>n \<phi> R\<^sub>n (\<psi> and\<^sub>n F\<^sub>n \<phi>[\<F>\<G> \<phi> w]\<^sub>\<Sigma>\<^sub>1)
 2. w \<Turnstile>\<^sub>n \<phi> R\<^sub>n (\<psi> and\<^sub>n F\<^sub>n \<phi>[\<F>\<G> \<phi> w]\<^sub>\<Sigma>\<^sub>1) \<Longrightarrow> w \<Turnstile>\<^sub>n \<phi> M\<^sub>n \<psi>
[PROOF STEP]
assume ?rhs
[PROOF STATE]
proof (state)
this:
w \<Turnstile>\<^sub>n \<phi> R\<^sub>n (\<psi> and\<^sub>n F\<^sub>n \<phi>[\<F>\<G> \<phi> w]\<^sub>\<Sigma>\<^sub>1)

goal (2 subgoals):
 1. w \<Turnstile>\<^sub>n \<phi> M\<^sub>n \<psi> \<Longrightarrow> w \<Turnstile>\<^sub>n \<phi> R\<^sub>n (\<psi> and\<^sub>n F\<^sub>n \<phi>[\<F>\<G> \<phi> w]\<^sub>\<Sigma>\<^sub>1)
 2. w \<Turnstile>\<^sub>n \<phi> R\<^sub>n (\<psi> and\<^sub>n F\<^sub>n \<phi>[\<F>\<G> \<phi> w]\<^sub>\<Sigma>\<^sub>1) \<Longrightarrow> w \<Turnstile>\<^sub>n \<phi> M\<^sub>n \<psi>
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
w \<Turnstile>\<^sub>n \<phi> R\<^sub>n (\<psi> and\<^sub>n F\<^sub>n \<phi>[\<F>\<G> \<phi> w]\<^sub>\<Sigma>\<^sub>1)

goal (2 subgoals):
 1. w \<Turnstile>\<^sub>n \<phi> M\<^sub>n \<psi> \<Longrightarrow> w \<Turnstile>\<^sub>n \<phi> R\<^sub>n (\<psi> and\<^sub>n F\<^sub>n \<phi>[\<F>\<G> \<phi> w]\<^sub>\<Sigma>\<^sub>1)
 2. w \<Turnstile>\<^sub>n \<phi> R\<^sub>n (\<psi> and\<^sub>n F\<^sub>n \<phi>[\<F>\<G> \<phi> w]\<^sub>\<Sigma>\<^sub>1) \<Longrightarrow> w \<Turnstile>\<^sub>n \<phi> M\<^sub>n \<psi>
[PROOF STEP]
obtain i where "\<nu>_stable \<phi> (suffix i w)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>i. \<nu>_stable \<phi> (suffix i w) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis MOST_nat less_Suc_eq suffix_\<nu>_stable)
[PROOF STATE]
proof (state)
this:
\<nu>_stable \<phi> (suffix i w)

goal (2 subgoals):
 1. w \<Turnstile>\<^sub>n \<phi> M\<^sub>n \<psi> \<Longrightarrow> w \<Turnstile>\<^sub>n \<phi> R\<^sub>n (\<psi> and\<^sub>n F\<^sub>n \<phi>[\<F>\<G> \<phi> w]\<^sub>\<Sigma>\<^sub>1)
 2. w \<Turnstile>\<^sub>n \<phi> R\<^sub>n (\<psi> and\<^sub>n F\<^sub>n \<phi>[\<F>\<G> \<phi> w]\<^sub>\<Sigma>\<^sub>1) \<Longrightarrow> w \<Turnstile>\<^sub>n \<phi> M\<^sub>n \<psi>
[PROOF STEP]
hence "\<forall>\<psi> \<in> \<F>\<G> \<phi> w. suffix i w \<Turnstile>\<^sub>n G\<^sub>n \<psi>"
[PROOF STATE]
proof (prove)
using this:
\<nu>_stable \<phi> (suffix i w)

goal (1 subgoal):
 1. \<forall>\<psi>\<in>\<F>\<G> \<phi> w. suffix i w \<Turnstile>\<^sub>n G\<^sub>n \<psi>
[PROOF STEP]
using \<F>\<G>_suffix \<G>_elim \<nu>_stable_def
[PROOF STATE]
proof (prove)
using this:
\<nu>_stable \<phi> (suffix i w)
\<F>\<G> ?\<phi> (suffix ?i ?w) = \<F>\<G> ?\<phi> ?w
?\<psi> \<in> \<G> ?\<phi> ?w \<Longrightarrow> ?w \<Turnstile>\<^sub>n G\<^sub>n ?\<psi>
\<nu>_stable ?\<phi> ?w = (\<F>\<G> ?\<phi> ?w = \<G> ?\<phi> ?w)

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

goal (2 subgoals):
 1. w \<Turnstile>\<^sub>n \<phi> M\<^sub>n \<psi> \<Longrightarrow> w \<Turnstile>\<^sub>n \<phi> R\<^sub>n (\<psi> and\<^sub>n F\<^sub>n \<phi>[\<F>\<G> \<phi> w]\<^sub>\<Sigma>\<^sub>1)
 2. w \<Turnstile>\<^sub>n \<phi> R\<^sub>n (\<psi> and\<^sub>n F\<^sub>n \<phi>[\<F>\<G> \<phi> w]\<^sub>\<Sigma>\<^sub>1) \<Longrightarrow> w \<Turnstile>\<^sub>n \<phi> M\<^sub>n \<psi>
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
\<forall>\<psi>\<in>\<F>\<G> \<phi> w. suffix i w \<Turnstile>\<^sub>n G\<^sub>n \<psi>

goal (2 subgoals):
 1. w \<Turnstile>\<^sub>n \<phi> M\<^sub>n \<psi> \<Longrightarrow> w \<Turnstile>\<^sub>n \<phi> R\<^sub>n (\<psi> and\<^sub>n F\<^sub>n \<phi>[\<F>\<G> \<phi> w]\<^sub>\<Sigma>\<^sub>1)
 2. w \<Turnstile>\<^sub>n \<phi> R\<^sub>n (\<psi> and\<^sub>n F\<^sub>n \<phi>[\<F>\<G> \<phi> w]\<^sub>\<Sigma>\<^sub>1) \<Longrightarrow> w \<Turnstile>\<^sub>n \<phi> M\<^sub>n \<psi>
[PROOF STEP]
assume assm: "w \<Turnstile>\<^sub>n G\<^sub>n (\<psi> and\<^sub>n (F\<^sub>n \<phi>[\<F>\<G> \<phi> w]\<^sub>\<Sigma>\<^sub>1))"
[PROOF STATE]
proof (state)
this:
w \<Turnstile>\<^sub>n G\<^sub>n (\<psi> and\<^sub>n F\<^sub>n \<phi>[\<F>\<G> \<phi> w]\<^sub>\<Sigma>\<^sub>1)

goal (2 subgoals):
 1. w \<Turnstile>\<^sub>n \<phi> M\<^sub>n \<psi> \<Longrightarrow> w \<Turnstile>\<^sub>n \<phi> R\<^sub>n (\<psi> and\<^sub>n F\<^sub>n \<phi>[\<F>\<G> \<phi> w]\<^sub>\<Sigma>\<^sub>1)
 2. w \<Turnstile>\<^sub>n \<phi> R\<^sub>n (\<psi> and\<^sub>n F\<^sub>n \<phi>[\<F>\<G> \<phi> w]\<^sub>\<Sigma>\<^sub>1) \<Longrightarrow> w \<Turnstile>\<^sub>n \<phi> M\<^sub>n \<psi>
[PROOF STEP]
hence "suffix i w \<Turnstile>\<^sub>n (F\<^sub>n \<phi>)[\<F>\<G> \<phi> w]\<^sub>\<Sigma>\<^sub>1"
[PROOF STATE]
proof (prove)
using this:
w \<Turnstile>\<^sub>n G\<^sub>n (\<psi> and\<^sub>n F\<^sub>n \<phi>[\<F>\<G> \<phi> w]\<^sub>\<Sigma>\<^sub>1)

goal (1 subgoal):
 1. suffix i w \<Turnstile>\<^sub>n (F\<^sub>n \<phi>)[\<F>\<G> \<phi> w]\<^sub>\<Sigma>\<^sub>1
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
suffix i w \<Turnstile>\<^sub>n (F\<^sub>n \<phi>)[\<F>\<G> \<phi> w]\<^sub>\<Sigma>\<^sub>1

goal (2 subgoals):
 1. w \<Turnstile>\<^sub>n \<phi> M\<^sub>n \<psi> \<Longrightarrow> w \<Turnstile>\<^sub>n \<phi> R\<^sub>n (\<psi> and\<^sub>n F\<^sub>n \<phi>[\<F>\<G> \<phi> w]\<^sub>\<Sigma>\<^sub>1)
 2. w \<Turnstile>\<^sub>n \<phi> R\<^sub>n (\<psi> and\<^sub>n F\<^sub>n \<phi>[\<F>\<G> \<phi> w]\<^sub>\<Sigma>\<^sub>1) \<Longrightarrow> w \<Turnstile>\<^sub>n \<phi> M\<^sub>n \<psi>
[PROOF STEP]
hence "suffix i w \<Turnstile>\<^sub>n F\<^sub>n \<phi>"
[PROOF STATE]
proof (prove)
using this:
suffix i w \<Turnstile>\<^sub>n (F\<^sub>n \<phi>)[\<F>\<G> \<phi> w]\<^sub>\<Sigma>\<^sub>1

goal (1 subgoal):
 1. suffix i w \<Turnstile>\<^sub>n F\<^sub>n \<phi>
[PROOF STEP]
by (blast dest: FG_advice_b2_helper[OF \<open>\<forall>\<psi> \<in> \<F>\<G> \<phi> w. suffix i w \<Turnstile>\<^sub>n G\<^sub>n \<psi>\<close>])
[PROOF STATE]
proof (state)
this:
suffix i w \<Turnstile>\<^sub>n F\<^sub>n \<phi>

goal (2 subgoals):
 1. w \<Turnstile>\<^sub>n \<phi> M\<^sub>n \<psi> \<Longrightarrow> w \<Turnstile>\<^sub>n \<phi> R\<^sub>n (\<psi> and\<^sub>n F\<^sub>n \<phi>[\<F>\<G> \<phi> w]\<^sub>\<Sigma>\<^sub>1)
 2. w \<Turnstile>\<^sub>n \<phi> R\<^sub>n (\<psi> and\<^sub>n F\<^sub>n \<phi>[\<F>\<G> \<phi> w]\<^sub>\<Sigma>\<^sub>1) \<Longrightarrow> w \<Turnstile>\<^sub>n \<phi> M\<^sub>n \<psi>
[PROOF STEP]
hence "w \<Turnstile>\<^sub>n \<phi> M\<^sub>n \<psi>"
[PROOF STATE]
proof (prove)
using this:
suffix i w \<Turnstile>\<^sub>n F\<^sub>n \<phi>

goal (1 subgoal):
 1. w \<Turnstile>\<^sub>n \<phi> M\<^sub>n \<psi>
[PROOF STEP]
using assm
[PROOF STATE]
proof (prove)
using this:
suffix i w \<Turnstile>\<^sub>n F\<^sub>n \<phi>
w \<Turnstile>\<^sub>n G\<^sub>n (\<psi> and\<^sub>n F\<^sub>n \<phi>[\<F>\<G> \<phi> w]\<^sub>\<Sigma>\<^sub>1)

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

goal (2 subgoals):
 1. w \<Turnstile>\<^sub>n \<phi> M\<^sub>n \<psi> \<Longrightarrow> w \<Turnstile>\<^sub>n \<phi> R\<^sub>n (\<psi> and\<^sub>n F\<^sub>n \<phi>[\<F>\<G> \<phi> w]\<^sub>\<Sigma>\<^sub>1)
 2. w \<Turnstile>\<^sub>n \<phi> R\<^sub>n (\<psi> and\<^sub>n F\<^sub>n \<phi>[\<F>\<G> \<phi> w]\<^sub>\<Sigma>\<^sub>1) \<Longrightarrow> w \<Turnstile>\<^sub>n \<phi> M\<^sub>n \<psi>
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
w \<Turnstile>\<^sub>n G\<^sub>n (\<psi> and\<^sub>n F\<^sub>n \<phi>[\<F>\<G> \<phi> w]\<^sub>\<Sigma>\<^sub>1) \<Longrightarrow> w \<Turnstile>\<^sub>n \<phi> M\<^sub>n \<psi>

goal (2 subgoals):
 1. w \<Turnstile>\<^sub>n \<phi> M\<^sub>n \<psi> \<Longrightarrow> w \<Turnstile>\<^sub>n \<phi> R\<^sub>n (\<psi> and\<^sub>n F\<^sub>n \<phi>[\<F>\<G> \<phi> w]\<^sub>\<Sigma>\<^sub>1)
 2. w \<Turnstile>\<^sub>n \<phi> R\<^sub>n (\<psi> and\<^sub>n F\<^sub>n \<phi>[\<F>\<G> \<phi> w]\<^sub>\<Sigma>\<^sub>1) \<Longrightarrow> w \<Turnstile>\<^sub>n \<phi> M\<^sub>n \<psi>
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
w \<Turnstile>\<^sub>n \<phi> R\<^sub>n (\<psi> and\<^sub>n F\<^sub>n \<phi>[\<F>\<G> \<phi> w]\<^sub>\<Sigma>\<^sub>1)
w \<Turnstile>\<^sub>n G\<^sub>n (\<psi> and\<^sub>n F\<^sub>n \<phi>[\<F>\<G> \<phi> w]\<^sub>\<Sigma>\<^sub>1) \<Longrightarrow> w \<Turnstile>\<^sub>n \<phi> M\<^sub>n \<psi>
[PROOF STEP]
show ?lhs
[PROOF STATE]
proof (prove)
using this:
w \<Turnstile>\<^sub>n \<phi> R\<^sub>n (\<psi> and\<^sub>n F\<^sub>n \<phi>[\<F>\<G> \<phi> w]\<^sub>\<Sigma>\<^sub>1)
w \<Turnstile>\<^sub>n G\<^sub>n (\<psi> and\<^sub>n F\<^sub>n \<phi>[\<F>\<G> \<phi> w]\<^sub>\<Sigma>\<^sub>1) \<Longrightarrow> w \<Turnstile>\<^sub>n \<phi> M\<^sub>n \<psi>

goal (1 subgoal):
 1. w \<Turnstile>\<^sub>n \<phi> M\<^sub>n \<psi>
[PROOF STEP]
using ltln_weak_to_strong(3) semantics_ltln.simps(5) strong_release_and_right_distrib
[PROOF STATE]
proof (prove)
using this:
w \<Turnstile>\<^sub>n \<phi> R\<^sub>n (\<psi> and\<^sub>n F\<^sub>n \<phi>[\<F>\<G> \<phi> w]\<^sub>\<Sigma>\<^sub>1)
w \<Turnstile>\<^sub>n G\<^sub>n (\<psi> and\<^sub>n F\<^sub>n \<phi>[\<F>\<G> \<phi> w]\<^sub>\<Sigma>\<^sub>1) \<Longrightarrow> w \<Turnstile>\<^sub>n \<phi> M\<^sub>n \<psi>
\<lbrakk>?w \<Turnstile>\<^sub>n ?\<phi> R\<^sub>n ?\<psi>; \<not> ?w \<Turnstile>\<^sub>n G\<^sub>n ?\<psi>\<rbrakk> \<Longrightarrow> ?w \<Turnstile>\<^sub>n ?\<phi> M\<^sub>n ?\<psi>
?\<xi> \<Turnstile>\<^sub>n ?\<phi> and\<^sub>n ?\<psi> = (?\<xi> \<Turnstile>\<^sub>n ?\<phi> \<and> ?\<xi> \<Turnstile>\<^sub>n ?\<psi>)
?w \<Turnstile>\<^sub>n ?\<phi> M\<^sub>n (?\<psi>\<^sub>1 and\<^sub>n ?\<psi>\<^sub>2) = ?w \<Turnstile>\<^sub>n ?\<phi> M\<^sub>n ?\<psi>\<^sub>1 and\<^sub>n ?\<phi> M\<^sub>n ?\<psi>\<^sub>2

goal (1 subgoal):
 1. w \<Turnstile>\<^sub>n \<phi> M\<^sub>n \<psi>
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
w \<Turnstile>\<^sub>n \<phi> M\<^sub>n \<psi>

goal (1 subgoal):
 1. w \<Turnstile>\<^sub>n \<phi> M\<^sub>n \<psi> \<Longrightarrow> w \<Turnstile>\<^sub>n \<phi> R\<^sub>n (\<psi> and\<^sub>n F\<^sub>n \<phi>[\<F>\<G> \<phi> w]\<^sub>\<Sigma>\<^sub>1)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. w \<Turnstile>\<^sub>n \<phi> M\<^sub>n \<psi> \<Longrightarrow> w \<Turnstile>\<^sub>n \<phi> R\<^sub>n (\<psi> and\<^sub>n F\<^sub>n \<phi>[\<F>\<G> \<phi> w]\<^sub>\<Sigma>\<^sub>1)
[PROOF STEP]
assume ?lhs
[PROOF STATE]
proof (state)
this:
w \<Turnstile>\<^sub>n \<phi> M\<^sub>n \<psi>

goal (1 subgoal):
 1. w \<Turnstile>\<^sub>n \<phi> M\<^sub>n \<psi> \<Longrightarrow> w \<Turnstile>\<^sub>n \<phi> R\<^sub>n (\<psi> and\<^sub>n F\<^sub>n \<phi>[\<F>\<G> \<phi> w]\<^sub>\<Sigma>\<^sub>1)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
w \<Turnstile>\<^sub>n \<phi> M\<^sub>n \<psi>

goal (1 subgoal):
 1. w \<Turnstile>\<^sub>n \<phi> M\<^sub>n \<psi> \<Longrightarrow> w \<Turnstile>\<^sub>n \<phi> R\<^sub>n (\<psi> and\<^sub>n F\<^sub>n \<phi>[\<F>\<G> \<phi> w]\<^sub>\<Sigma>\<^sub>1)
[PROOF STEP]
have "\<And>i. suffix i w \<Turnstile>\<^sub>n \<phi> \<Longrightarrow> suffix i w \<Turnstile>\<^sub>n \<phi>[\<F>\<G> \<phi> w]\<^sub>\<Sigma>\<^sub>1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i. suffix i w \<Turnstile>\<^sub>n \<phi> \<Longrightarrow> suffix i w \<Turnstile>\<^sub>n \<phi>[\<F>\<G> \<phi> w]\<^sub>\<Sigma>\<^sub>1
[PROOF STEP]
using \<F>\<G>_suffix
[PROOF STATE]
proof (prove)
using this:
\<F>\<G> ?\<phi> (suffix ?i ?w) = \<F>\<G> ?\<phi> ?w

goal (1 subgoal):
 1. \<And>i. suffix i w \<Turnstile>\<^sub>n \<phi> \<Longrightarrow> suffix i w \<Turnstile>\<^sub>n \<phi>[\<F>\<G> \<phi> w]\<^sub>\<Sigma>\<^sub>1
[PROOF STEP]
by (blast intro: FG_advice_b1)
[PROOF STATE]
proof (state)
this:
suffix ?i w \<Turnstile>\<^sub>n \<phi> \<Longrightarrow> suffix ?i w \<Turnstile>\<^sub>n \<phi>[\<F>\<G> \<phi> w]\<^sub>\<Sigma>\<^sub>1

goal (1 subgoal):
 1. w \<Turnstile>\<^sub>n \<phi> M\<^sub>n \<psi> \<Longrightarrow> w \<Turnstile>\<^sub>n \<phi> R\<^sub>n (\<psi> and\<^sub>n F\<^sub>n \<phi>[\<F>\<G> \<phi> w]\<^sub>\<Sigma>\<^sub>1)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
w \<Turnstile>\<^sub>n \<phi> M\<^sub>n \<psi>
suffix ?i w \<Turnstile>\<^sub>n \<phi> \<Longrightarrow> suffix ?i w \<Turnstile>\<^sub>n \<phi>[\<F>\<G> \<phi> w]\<^sub>\<Sigma>\<^sub>1
[PROOF STEP]
show "?rhs"
[PROOF STATE]
proof (prove)
using this:
w \<Turnstile>\<^sub>n \<phi> M\<^sub>n \<psi>
suffix ?i w \<Turnstile>\<^sub>n \<phi> \<Longrightarrow> suffix ?i w \<Turnstile>\<^sub>n \<phi>[\<F>\<G> \<phi> w]\<^sub>\<Sigma>\<^sub>1

goal (1 subgoal):
 1. w \<Turnstile>\<^sub>n \<phi> R\<^sub>n (\<psi> and\<^sub>n F\<^sub>n \<phi>[\<F>\<G> \<phi> w]\<^sub>\<Sigma>\<^sub>1)
[PROOF STEP]
unfolding ltln_strong_weak_2
[PROOF STATE]
proof (prove)
using this:
w \<Turnstile>\<^sub>n \<phi> R\<^sub>n (\<psi> and\<^sub>n F\<^sub>n \<phi>)
suffix ?i w \<Turnstile>\<^sub>n \<phi> \<Longrightarrow> suffix ?i w \<Turnstile>\<^sub>n \<phi>[\<F>\<G> \<phi> w]\<^sub>\<Sigma>\<^sub>1

goal (1 subgoal):
 1. w \<Turnstile>\<^sub>n \<phi> R\<^sub>n (\<psi> and\<^sub>n F\<^sub>n \<phi>[\<F>\<G> \<phi> w]\<^sub>\<Sigma>\<^sub>1)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
w \<Turnstile>\<^sub>n \<phi> R\<^sub>n (\<psi> and\<^sub>n F\<^sub>n \<phi>[\<F>\<G> \<phi> w]\<^sub>\<Sigma>\<^sub>1)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ltln_strong_weak_stable_words:
  "w \<Turnstile>\<^sub>n \<phi> U\<^sub>n \<psi> \<longleftrightarrow> w \<Turnstile>\<^sub>n (\<phi> and\<^sub>n (F\<^sub>n \<psi>[\<F>\<G> (\<phi> U\<^sub>n \<psi>) w]\<^sub>\<Sigma>\<^sub>1)) W\<^sub>n \<psi>"
  "w \<Turnstile>\<^sub>n \<phi> M\<^sub>n \<psi> \<longleftrightarrow> w \<Turnstile>\<^sub>n \<phi> R\<^sub>n (\<psi> and\<^sub>n (F\<^sub>n \<phi>[\<F>\<G> (\<phi> M\<^sub>n \<psi>) w]\<^sub>\<Sigma>\<^sub>1))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. w \<Turnstile>\<^sub>n \<phi> U\<^sub>n \<psi> = w \<Turnstile>\<^sub>n (\<phi> and\<^sub>n F\<^sub>n \<psi>[\<F>\<G> (\<phi> U\<^sub>n \<psi>) w]\<^sub>\<Sigma>\<^sub>1) W\<^sub>n \<psi> &&& w \<Turnstile>\<^sub>n \<phi> M\<^sub>n \<psi> = w \<Turnstile>\<^sub>n \<phi> R\<^sub>n (\<psi> and\<^sub>n F\<^sub>n \<phi>[\<F>\<G> (\<phi> M\<^sub>n \<psi>) w]\<^sub>\<Sigma>\<^sub>1)
[PROOF STEP]
unfolding ltln_strong_weak_stable_words_1 ltln_strong_weak_stable_words_2 FG_advice_restriction
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. w \<Turnstile>\<^sub>n (\<phi> and\<^sub>n F\<^sub>n \<psi>[\<F>\<G> \<psi> w]\<^sub>\<Sigma>\<^sub>1) W\<^sub>n \<psi> = w \<Turnstile>\<^sub>n (\<phi> and\<^sub>n F\<^sub>n \<psi>[\<F>\<G> \<psi> w]\<^sub>\<Sigma>\<^sub>1) W\<^sub>n \<psi> &&& w \<Turnstile>\<^sub>n \<phi> R\<^sub>n (\<psi> and\<^sub>n F\<^sub>n \<phi>[\<F>\<G> \<phi> w]\<^sub>\<Sigma>\<^sub>1) = w \<Turnstile>\<^sub>n \<phi> R\<^sub>n (\<psi> and\<^sub>n F\<^sub>n \<phi>[\<F>\<G> \<phi> w]\<^sub>\<Sigma>\<^sub>1)
[PROOF STEP]
by simp+


[STATEMENT]
lemma flatten_pi_2_IH_lifting:
  assumes "\<psi> \<in> subfrmlsn \<phi>"
  assumes "suffix i w \<Turnstile>\<^sub>n \<psi>[\<F>\<G> \<psi> (suffix i w)]\<^sub>\<Pi>\<^sub>2 = suffix i w \<Turnstile>\<^sub>n \<psi>"
  shows "suffix i w \<Turnstile>\<^sub>n \<psi>[\<F>\<G> \<phi> w]\<^sub>\<Pi>\<^sub>2 = suffix i w \<Turnstile>\<^sub>n \<psi>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. suffix i w \<Turnstile>\<^sub>n \<psi>[\<F>\<G> \<phi> w]\<^sub>\<Pi>\<^sub>2 = suffix i w \<Turnstile>\<^sub>n \<psi>
[PROOF STEP]
by (metis (no_types, lifting) inf.absorb_iff2 inf_assoc inf_commute assms(2) \<F>\<G>_suffix flatten_pi_2_intersection_eq[of "\<F>\<G> \<phi> w" \<psi> "\<F>\<G> \<psi> w"] \<F>\<G>_semantics' subformulas\<^sub>\<nu>_subset[OF assms(1)])