[STATEMENT]
lemma flatten_pi_2_correct:
  "w \<Turnstile>\<^sub>n \<phi>[\<F>\<G> \<phi> w]\<^sub>\<Pi>\<^sub>2 \<longleftrightarrow> w \<Turnstile>\<^sub>n \<phi>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. w \<Turnstile>\<^sub>n \<phi>[\<F>\<G> \<phi> w]\<^sub>\<Pi>\<^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[\<F>\<G> true\<^sub>n w]\<^sub>\<Pi>\<^sub>2 = w \<Turnstile>\<^sub>n true\<^sub>n
 2. \<And>w. w \<Turnstile>\<^sub>n false\<^sub>n[\<F>\<G> false\<^sub>n w]\<^sub>\<Pi>\<^sub>2 = w \<Turnstile>\<^sub>n false\<^sub>n
 3. \<And>x w. w \<Turnstile>\<^sub>n prop\<^sub>n(x)[\<F>\<G> prop\<^sub>n(x) w]\<^sub>\<Pi>\<^sub>2 = w \<Turnstile>\<^sub>n prop\<^sub>n(x)
 4. \<And>x w. w \<Turnstile>\<^sub>n nprop\<^sub>n(x)[\<F>\<G> nprop\<^sub>n(x) w]\<^sub>\<Pi>\<^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[\<F>\<G> \<phi>1 w]\<^sub>\<Pi>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>1; \<And>w. w \<Turnstile>\<^sub>n \<phi>2[\<F>\<G> \<phi>2 w]\<^sub>\<Pi>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>2\<rbrakk> \<Longrightarrow> w \<Turnstile>\<^sub>n \<phi>1 and\<^sub>n \<phi>2[\<F>\<G> (\<phi>1 and\<^sub>n \<phi>2) w]\<^sub>\<Pi>\<^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[\<F>\<G> \<phi>1 w]\<^sub>\<Pi>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>1; \<And>w. w \<Turnstile>\<^sub>n \<phi>2[\<F>\<G> \<phi>2 w]\<^sub>\<Pi>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>2\<rbrakk> \<Longrightarrow> w \<Turnstile>\<^sub>n \<phi>1 or\<^sub>n \<phi>2[\<F>\<G> (\<phi>1 or\<^sub>n \<phi>2) w]\<^sub>\<Pi>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>1 or\<^sub>n \<phi>2
 7. \<And>\<phi> w. (\<And>w. w \<Turnstile>\<^sub>n \<phi>[\<F>\<G> \<phi> w]\<^sub>\<Pi>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>) \<Longrightarrow> w \<Turnstile>\<^sub>n X\<^sub>n \<phi>[\<F>\<G> (X\<^sub>n \<phi>) w]\<^sub>\<Pi>\<^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[\<F>\<G> \<phi>1 w]\<^sub>\<Pi>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>1; \<And>w. w \<Turnstile>\<^sub>n \<phi>2[\<F>\<G> \<phi>2 w]\<^sub>\<Pi>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>2\<rbrakk> \<Longrightarrow> w \<Turnstile>\<^sub>n \<phi>1 U\<^sub>n \<phi>2[\<F>\<G> (\<phi>1 U\<^sub>n \<phi>2) w]\<^sub>\<Pi>\<^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[\<F>\<G> \<phi>1 w]\<^sub>\<Pi>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>1; \<And>w. w \<Turnstile>\<^sub>n \<phi>2[\<F>\<G> \<phi>2 w]\<^sub>\<Pi>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>2\<rbrakk> \<Longrightarrow> w \<Turnstile>\<^sub>n \<phi>1 R\<^sub>n \<phi>2[\<F>\<G> (\<phi>1 R\<^sub>n \<phi>2) w]\<^sub>\<Pi>\<^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[\<F>\<G> \<phi>1 w]\<^sub>\<Pi>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>1; \<And>w. w \<Turnstile>\<^sub>n \<phi>2[\<F>\<G> \<phi>2 w]\<^sub>\<Pi>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>2\<rbrakk> \<Longrightarrow> w \<Turnstile>\<^sub>n \<phi>1 W\<^sub>n \<phi>2[\<F>\<G> (\<phi>1 W\<^sub>n \<phi>2) w]\<^sub>\<Pi>\<^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[\<F>\<G> \<phi>1 ?w]\<^sub>\<Pi>\<^sub>2 = ?w \<Turnstile>\<^sub>n \<phi>1
?w \<Turnstile>\<^sub>n \<phi>2[\<F>\<G> \<phi>2 ?w]\<^sub>\<Pi>\<^sub>2 = ?w \<Turnstile>\<^sub>n \<phi>2

goal (11 subgoals):
 1. \<And>w. w \<Turnstile>\<^sub>n true\<^sub>n[\<F>\<G> true\<^sub>n w]\<^sub>\<Pi>\<^sub>2 = w \<Turnstile>\<^sub>n true\<^sub>n
 2. \<And>w. w \<Turnstile>\<^sub>n false\<^sub>n[\<F>\<G> false\<^sub>n w]\<^sub>\<Pi>\<^sub>2 = w \<Turnstile>\<^sub>n false\<^sub>n
 3. \<And>x w. w \<Turnstile>\<^sub>n prop\<^sub>n(x)[\<F>\<G> prop\<^sub>n(x) w]\<^sub>\<Pi>\<^sub>2 = w \<Turnstile>\<^sub>n prop\<^sub>n(x)
 4. \<And>x w. w \<Turnstile>\<^sub>n nprop\<^sub>n(x)[\<F>\<G> nprop\<^sub>n(x) w]\<^sub>\<Pi>\<^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[\<F>\<G> \<phi>1 w]\<^sub>\<Pi>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>1; \<And>w. w \<Turnstile>\<^sub>n \<phi>2[\<F>\<G> \<phi>2 w]\<^sub>\<Pi>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>2\<rbrakk> \<Longrightarrow> w \<Turnstile>\<^sub>n \<phi>1 and\<^sub>n \<phi>2[\<F>\<G> (\<phi>1 and\<^sub>n \<phi>2) w]\<^sub>\<Pi>\<^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[\<F>\<G> \<phi>1 w]\<^sub>\<Pi>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>1; \<And>w. w \<Turnstile>\<^sub>n \<phi>2[\<F>\<G> \<phi>2 w]\<^sub>\<Pi>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>2\<rbrakk> \<Longrightarrow> w \<Turnstile>\<^sub>n \<phi>1 or\<^sub>n \<phi>2[\<F>\<G> (\<phi>1 or\<^sub>n \<phi>2) w]\<^sub>\<Pi>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>1 or\<^sub>n \<phi>2
 7. \<And>\<phi> w. (\<And>w. w \<Turnstile>\<^sub>n \<phi>[\<F>\<G> \<phi> w]\<^sub>\<Pi>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>) \<Longrightarrow> w \<Turnstile>\<^sub>n X\<^sub>n \<phi>[\<F>\<G> (X\<^sub>n \<phi>) w]\<^sub>\<Pi>\<^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[\<F>\<G> \<phi>1 w]\<^sub>\<Pi>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>1; \<And>w. w \<Turnstile>\<^sub>n \<phi>2[\<F>\<G> \<phi>2 w]\<^sub>\<Pi>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>2\<rbrakk> \<Longrightarrow> w \<Turnstile>\<^sub>n \<phi>1 U\<^sub>n \<phi>2[\<F>\<G> (\<phi>1 U\<^sub>n \<phi>2) w]\<^sub>\<Pi>\<^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[\<F>\<G> \<phi>1 w]\<^sub>\<Pi>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>1; \<And>w. w \<Turnstile>\<^sub>n \<phi>2[\<F>\<G> \<phi>2 w]\<^sub>\<Pi>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>2\<rbrakk> \<Longrightarrow> w \<Turnstile>\<^sub>n \<phi>1 R\<^sub>n \<phi>2[\<F>\<G> (\<phi>1 R\<^sub>n \<phi>2) w]\<^sub>\<Pi>\<^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[\<F>\<G> \<phi>1 w]\<^sub>\<Pi>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>1; \<And>w. w \<Turnstile>\<^sub>n \<phi>2[\<F>\<G> \<phi>2 w]\<^sub>\<Pi>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>2\<rbrakk> \<Longrightarrow> w \<Turnstile>\<^sub>n \<phi>1 W\<^sub>n \<phi>2[\<F>\<G> (\<phi>1 W\<^sub>n \<phi>2) w]\<^sub>\<Pi>\<^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[\<F>\<G> \<phi>1 ?w]\<^sub>\<Pi>\<^sub>2 = ?w \<Turnstile>\<^sub>n \<phi>1
?w \<Turnstile>\<^sub>n \<phi>2[\<F>\<G> \<phi>2 ?w]\<^sub>\<Pi>\<^sub>2 = ?w \<Turnstile>\<^sub>n \<phi>2
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
?w \<Turnstile>\<^sub>n \<phi>1[\<F>\<G> \<phi>1 ?w]\<^sub>\<Pi>\<^sub>2 = ?w \<Turnstile>\<^sub>n \<phi>1
?w \<Turnstile>\<^sub>n \<phi>2[\<F>\<G> \<phi>2 ?w]\<^sub>\<Pi>\<^sub>2 = ?w \<Turnstile>\<^sub>n \<phi>2

goal (1 subgoal):
 1. w \<Turnstile>\<^sub>n \<phi>1 and\<^sub>n \<phi>2[\<F>\<G> (\<phi>1 and\<^sub>n \<phi>2) w]\<^sub>\<Pi>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>1 and\<^sub>n \<phi>2
[PROOF STEP]
using flatten_pi_2_IH_lifting[of _ "\<phi>1 and\<^sub>n \<phi>2" 0]
[PROOF STATE]
proof (prove)
using this:
?w \<Turnstile>\<^sub>n \<phi>1[\<F>\<G> \<phi>1 ?w]\<^sub>\<Pi>\<^sub>2 = ?w \<Turnstile>\<^sub>n \<phi>1
?w \<Turnstile>\<^sub>n \<phi>2[\<F>\<G> \<phi>2 ?w]\<^sub>\<Pi>\<^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>[\<F>\<G> ?\<psi> (suffix 0 ?w)]\<^sub>\<Pi>\<^sub>2 = suffix 0 ?w \<Turnstile>\<^sub>n ?\<psi>\<rbrakk> \<Longrightarrow> suffix 0 ?w \<Turnstile>\<^sub>n ?\<psi>[\<F>\<G> (\<phi>1 and\<^sub>n \<phi>2) ?w]\<^sub>\<Pi>\<^sub>2 = suffix 0 ?w \<Turnstile>\<^sub>n ?\<psi>

goal (1 subgoal):
 1. w \<Turnstile>\<^sub>n \<phi>1 and\<^sub>n \<phi>2[\<F>\<G> (\<phi>1 and\<^sub>n \<phi>2) w]\<^sub>\<Pi>\<^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[\<F>\<G> (\<phi>1 and\<^sub>n \<phi>2) w]\<^sub>\<Pi>\<^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[\<F>\<G> true\<^sub>n w]\<^sub>\<Pi>\<^sub>2 = w \<Turnstile>\<^sub>n true\<^sub>n
 2. \<And>w. w \<Turnstile>\<^sub>n false\<^sub>n[\<F>\<G> false\<^sub>n w]\<^sub>\<Pi>\<^sub>2 = w \<Turnstile>\<^sub>n false\<^sub>n
 3. \<And>x w. w \<Turnstile>\<^sub>n prop\<^sub>n(x)[\<F>\<G> prop\<^sub>n(x) w]\<^sub>\<Pi>\<^sub>2 = w \<Turnstile>\<^sub>n prop\<^sub>n(x)
 4. \<And>x w. w \<Turnstile>\<^sub>n nprop\<^sub>n(x)[\<F>\<G> nprop\<^sub>n(x) w]\<^sub>\<Pi>\<^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[\<F>\<G> \<phi>1 w]\<^sub>\<Pi>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>1; \<And>w. w \<Turnstile>\<^sub>n \<phi>2[\<F>\<G> \<phi>2 w]\<^sub>\<Pi>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>2\<rbrakk> \<Longrightarrow> w \<Turnstile>\<^sub>n \<phi>1 or\<^sub>n \<phi>2[\<F>\<G> (\<phi>1 or\<^sub>n \<phi>2) w]\<^sub>\<Pi>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>1 or\<^sub>n \<phi>2
 6. \<And>\<phi> w. (\<And>w. w \<Turnstile>\<^sub>n \<phi>[\<F>\<G> \<phi> w]\<^sub>\<Pi>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>) \<Longrightarrow> w \<Turnstile>\<^sub>n X\<^sub>n \<phi>[\<F>\<G> (X\<^sub>n \<phi>) w]\<^sub>\<Pi>\<^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[\<F>\<G> \<phi>1 w]\<^sub>\<Pi>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>1; \<And>w. w \<Turnstile>\<^sub>n \<phi>2[\<F>\<G> \<phi>2 w]\<^sub>\<Pi>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>2\<rbrakk> \<Longrightarrow> w \<Turnstile>\<^sub>n \<phi>1 U\<^sub>n \<phi>2[\<F>\<G> (\<phi>1 U\<^sub>n \<phi>2) w]\<^sub>\<Pi>\<^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[\<F>\<G> \<phi>1 w]\<^sub>\<Pi>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>1; \<And>w. w \<Turnstile>\<^sub>n \<phi>2[\<F>\<G> \<phi>2 w]\<^sub>\<Pi>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>2\<rbrakk> \<Longrightarrow> w \<Turnstile>\<^sub>n \<phi>1 R\<^sub>n \<phi>2[\<F>\<G> (\<phi>1 R\<^sub>n \<phi>2) w]\<^sub>\<Pi>\<^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[\<F>\<G> \<phi>1 w]\<^sub>\<Pi>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>1; \<And>w. w \<Turnstile>\<^sub>n \<phi>2[\<F>\<G> \<phi>2 w]\<^sub>\<Pi>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>2\<rbrakk> \<Longrightarrow> w \<Turnstile>\<^sub>n \<phi>1 W\<^sub>n \<phi>2[\<F>\<G> (\<phi>1 W\<^sub>n \<phi>2) w]\<^sub>\<Pi>\<^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[\<F>\<G> \<phi>1 w]\<^sub>\<Pi>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>1; \<And>w. w \<Turnstile>\<^sub>n \<phi>2[\<F>\<G> \<phi>2 w]\<^sub>\<Pi>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>2\<rbrakk> \<Longrightarrow> w \<Turnstile>\<^sub>n \<phi>1 M\<^sub>n \<phi>2[\<F>\<G> (\<phi>1 M\<^sub>n \<phi>2) w]\<^sub>\<Pi>\<^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[\<F>\<G> true\<^sub>n w]\<^sub>\<Pi>\<^sub>2 = w \<Turnstile>\<^sub>n true\<^sub>n
 2. \<And>w. w \<Turnstile>\<^sub>n false\<^sub>n[\<F>\<G> false\<^sub>n w]\<^sub>\<Pi>\<^sub>2 = w \<Turnstile>\<^sub>n false\<^sub>n
 3. \<And>x w. w \<Turnstile>\<^sub>n prop\<^sub>n(x)[\<F>\<G> prop\<^sub>n(x) w]\<^sub>\<Pi>\<^sub>2 = w \<Turnstile>\<^sub>n prop\<^sub>n(x)
 4. \<And>x w. w \<Turnstile>\<^sub>n nprop\<^sub>n(x)[\<F>\<G> nprop\<^sub>n(x) w]\<^sub>\<Pi>\<^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[\<F>\<G> \<phi>1 w]\<^sub>\<Pi>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>1; \<And>w. w \<Turnstile>\<^sub>n \<phi>2[\<F>\<G> \<phi>2 w]\<^sub>\<Pi>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>2\<rbrakk> \<Longrightarrow> w \<Turnstile>\<^sub>n \<phi>1 or\<^sub>n \<phi>2[\<F>\<G> (\<phi>1 or\<^sub>n \<phi>2) w]\<^sub>\<Pi>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>1 or\<^sub>n \<phi>2
 6. \<And>\<phi> w. (\<And>w. w \<Turnstile>\<^sub>n \<phi>[\<F>\<G> \<phi> w]\<^sub>\<Pi>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>) \<Longrightarrow> w \<Turnstile>\<^sub>n X\<^sub>n \<phi>[\<F>\<G> (X\<^sub>n \<phi>) w]\<^sub>\<Pi>\<^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[\<F>\<G> \<phi>1 w]\<^sub>\<Pi>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>1; \<And>w. w \<Turnstile>\<^sub>n \<phi>2[\<F>\<G> \<phi>2 w]\<^sub>\<Pi>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>2\<rbrakk> \<Longrightarrow> w \<Turnstile>\<^sub>n \<phi>1 U\<^sub>n \<phi>2[\<F>\<G> (\<phi>1 U\<^sub>n \<phi>2) w]\<^sub>\<Pi>\<^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[\<F>\<G> \<phi>1 w]\<^sub>\<Pi>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>1; \<And>w. w \<Turnstile>\<^sub>n \<phi>2[\<F>\<G> \<phi>2 w]\<^sub>\<Pi>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>2\<rbrakk> \<Longrightarrow> w \<Turnstile>\<^sub>n \<phi>1 R\<^sub>n \<phi>2[\<F>\<G> (\<phi>1 R\<^sub>n \<phi>2) w]\<^sub>\<Pi>\<^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[\<F>\<G> \<phi>1 w]\<^sub>\<Pi>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>1; \<And>w. w \<Turnstile>\<^sub>n \<phi>2[\<F>\<G> \<phi>2 w]\<^sub>\<Pi>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>2\<rbrakk> \<Longrightarrow> w \<Turnstile>\<^sub>n \<phi>1 W\<^sub>n \<phi>2[\<F>\<G> (\<phi>1 W\<^sub>n \<phi>2) w]\<^sub>\<Pi>\<^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[\<F>\<G> \<phi>1 w]\<^sub>\<Pi>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>1; \<And>w. w \<Turnstile>\<^sub>n \<phi>2[\<F>\<G> \<phi>2 w]\<^sub>\<Pi>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>2\<rbrakk> \<Longrightarrow> w \<Turnstile>\<^sub>n \<phi>1 M\<^sub>n \<phi>2[\<F>\<G> (\<phi>1 M\<^sub>n \<phi>2) w]\<^sub>\<Pi>\<^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[\<F>\<G> \<phi>1 ?w]\<^sub>\<Pi>\<^sub>2 = ?w \<Turnstile>\<^sub>n \<phi>1
?w \<Turnstile>\<^sub>n \<phi>2[\<F>\<G> \<phi>2 ?w]\<^sub>\<Pi>\<^sub>2 = ?w \<Turnstile>\<^sub>n \<phi>2

goal (10 subgoals):
 1. \<And>w. w \<Turnstile>\<^sub>n true\<^sub>n[\<F>\<G> true\<^sub>n w]\<^sub>\<Pi>\<^sub>2 = w \<Turnstile>\<^sub>n true\<^sub>n
 2. \<And>w. w \<Turnstile>\<^sub>n false\<^sub>n[\<F>\<G> false\<^sub>n w]\<^sub>\<Pi>\<^sub>2 = w \<Turnstile>\<^sub>n false\<^sub>n
 3. \<And>x w. w \<Turnstile>\<^sub>n prop\<^sub>n(x)[\<F>\<G> prop\<^sub>n(x) w]\<^sub>\<Pi>\<^sub>2 = w \<Turnstile>\<^sub>n prop\<^sub>n(x)
 4. \<And>x w. w \<Turnstile>\<^sub>n nprop\<^sub>n(x)[\<F>\<G> nprop\<^sub>n(x) w]\<^sub>\<Pi>\<^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[\<F>\<G> \<phi>1 w]\<^sub>\<Pi>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>1; \<And>w. w \<Turnstile>\<^sub>n \<phi>2[\<F>\<G> \<phi>2 w]\<^sub>\<Pi>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>2\<rbrakk> \<Longrightarrow> w \<Turnstile>\<^sub>n \<phi>1 or\<^sub>n \<phi>2[\<F>\<G> (\<phi>1 or\<^sub>n \<phi>2) w]\<^sub>\<Pi>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>1 or\<^sub>n \<phi>2
 6. \<And>\<phi> w. (\<And>w. w \<Turnstile>\<^sub>n \<phi>[\<F>\<G> \<phi> w]\<^sub>\<Pi>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>) \<Longrightarrow> w \<Turnstile>\<^sub>n X\<^sub>n \<phi>[\<F>\<G> (X\<^sub>n \<phi>) w]\<^sub>\<Pi>\<^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[\<F>\<G> \<phi>1 w]\<^sub>\<Pi>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>1; \<And>w. w \<Turnstile>\<^sub>n \<phi>2[\<F>\<G> \<phi>2 w]\<^sub>\<Pi>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>2\<rbrakk> \<Longrightarrow> w \<Turnstile>\<^sub>n \<phi>1 U\<^sub>n \<phi>2[\<F>\<G> (\<phi>1 U\<^sub>n \<phi>2) w]\<^sub>\<Pi>\<^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[\<F>\<G> \<phi>1 w]\<^sub>\<Pi>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>1; \<And>w. w \<Turnstile>\<^sub>n \<phi>2[\<F>\<G> \<phi>2 w]\<^sub>\<Pi>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>2\<rbrakk> \<Longrightarrow> w \<Turnstile>\<^sub>n \<phi>1 R\<^sub>n \<phi>2[\<F>\<G> (\<phi>1 R\<^sub>n \<phi>2) w]\<^sub>\<Pi>\<^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[\<F>\<G> \<phi>1 w]\<^sub>\<Pi>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>1; \<And>w. w \<Turnstile>\<^sub>n \<phi>2[\<F>\<G> \<phi>2 w]\<^sub>\<Pi>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>2\<rbrakk> \<Longrightarrow> w \<Turnstile>\<^sub>n \<phi>1 W\<^sub>n \<phi>2[\<F>\<G> (\<phi>1 W\<^sub>n \<phi>2) w]\<^sub>\<Pi>\<^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[\<F>\<G> \<phi>1 w]\<^sub>\<Pi>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>1; \<And>w. w \<Turnstile>\<^sub>n \<phi>2[\<F>\<G> \<phi>2 w]\<^sub>\<Pi>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>2\<rbrakk> \<Longrightarrow> w \<Turnstile>\<^sub>n \<phi>1 M\<^sub>n \<phi>2[\<F>\<G> (\<phi>1 M\<^sub>n \<phi>2) w]\<^sub>\<Pi>\<^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[\<F>\<G> \<phi>1 ?w]\<^sub>\<Pi>\<^sub>2 = ?w \<Turnstile>\<^sub>n \<phi>1
?w \<Turnstile>\<^sub>n \<phi>2[\<F>\<G> \<phi>2 ?w]\<^sub>\<Pi>\<^sub>2 = ?w \<Turnstile>\<^sub>n \<phi>2
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
?w \<Turnstile>\<^sub>n \<phi>1[\<F>\<G> \<phi>1 ?w]\<^sub>\<Pi>\<^sub>2 = ?w \<Turnstile>\<^sub>n \<phi>1
?w \<Turnstile>\<^sub>n \<phi>2[\<F>\<G> \<phi>2 ?w]\<^sub>\<Pi>\<^sub>2 = ?w \<Turnstile>\<^sub>n \<phi>2

goal (1 subgoal):
 1. w \<Turnstile>\<^sub>n \<phi>1 or\<^sub>n \<phi>2[\<F>\<G> (\<phi>1 or\<^sub>n \<phi>2) w]\<^sub>\<Pi>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>1 or\<^sub>n \<phi>2
[PROOF STEP]
using flatten_pi_2_IH_lifting[of _ "\<phi>1 or\<^sub>n \<phi>2" 0]
[PROOF STATE]
proof (prove)
using this:
?w \<Turnstile>\<^sub>n \<phi>1[\<F>\<G> \<phi>1 ?w]\<^sub>\<Pi>\<^sub>2 = ?w \<Turnstile>\<^sub>n \<phi>1
?w \<Turnstile>\<^sub>n \<phi>2[\<F>\<G> \<phi>2 ?w]\<^sub>\<Pi>\<^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>[\<F>\<G> ?\<psi> (suffix 0 ?w)]\<^sub>\<Pi>\<^sub>2 = suffix 0 ?w \<Turnstile>\<^sub>n ?\<psi>\<rbrakk> \<Longrightarrow> suffix 0 ?w \<Turnstile>\<^sub>n ?\<psi>[\<F>\<G> (\<phi>1 or\<^sub>n \<phi>2) ?w]\<^sub>\<Pi>\<^sub>2 = suffix 0 ?w \<Turnstile>\<^sub>n ?\<psi>

goal (1 subgoal):
 1. w \<Turnstile>\<^sub>n \<phi>1 or\<^sub>n \<phi>2[\<F>\<G> (\<phi>1 or\<^sub>n \<phi>2) w]\<^sub>\<Pi>\<^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[\<F>\<G> (\<phi>1 or\<^sub>n \<phi>2) w]\<^sub>\<Pi>\<^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[\<F>\<G> true\<^sub>n w]\<^sub>\<Pi>\<^sub>2 = w \<Turnstile>\<^sub>n true\<^sub>n
 2. \<And>w. w \<Turnstile>\<^sub>n false\<^sub>n[\<F>\<G> false\<^sub>n w]\<^sub>\<Pi>\<^sub>2 = w \<Turnstile>\<^sub>n false\<^sub>n
 3. \<And>x w. w \<Turnstile>\<^sub>n prop\<^sub>n(x)[\<F>\<G> prop\<^sub>n(x) w]\<^sub>\<Pi>\<^sub>2 = w \<Turnstile>\<^sub>n prop\<^sub>n(x)
 4. \<And>x w. w \<Turnstile>\<^sub>n nprop\<^sub>n(x)[\<F>\<G> nprop\<^sub>n(x) w]\<^sub>\<Pi>\<^sub>2 = w \<Turnstile>\<^sub>n nprop\<^sub>n(x)
 5. \<And>\<phi> w. (\<And>w. w \<Turnstile>\<^sub>n \<phi>[\<F>\<G> \<phi> w]\<^sub>\<Pi>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>) \<Longrightarrow> w \<Turnstile>\<^sub>n X\<^sub>n \<phi>[\<F>\<G> (X\<^sub>n \<phi>) w]\<^sub>\<Pi>\<^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[\<F>\<G> \<phi>1 w]\<^sub>\<Pi>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>1; \<And>w. w \<Turnstile>\<^sub>n \<phi>2[\<F>\<G> \<phi>2 w]\<^sub>\<Pi>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>2\<rbrakk> \<Longrightarrow> w \<Turnstile>\<^sub>n \<phi>1 U\<^sub>n \<phi>2[\<F>\<G> (\<phi>1 U\<^sub>n \<phi>2) w]\<^sub>\<Pi>\<^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[\<F>\<G> \<phi>1 w]\<^sub>\<Pi>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>1; \<And>w. w \<Turnstile>\<^sub>n \<phi>2[\<F>\<G> \<phi>2 w]\<^sub>\<Pi>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>2\<rbrakk> \<Longrightarrow> w \<Turnstile>\<^sub>n \<phi>1 R\<^sub>n \<phi>2[\<F>\<G> (\<phi>1 R\<^sub>n \<phi>2) w]\<^sub>\<Pi>\<^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[\<F>\<G> \<phi>1 w]\<^sub>\<Pi>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>1; \<And>w. w \<Turnstile>\<^sub>n \<phi>2[\<F>\<G> \<phi>2 w]\<^sub>\<Pi>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>2\<rbrakk> \<Longrightarrow> w \<Turnstile>\<^sub>n \<phi>1 W\<^sub>n \<phi>2[\<F>\<G> (\<phi>1 W\<^sub>n \<phi>2) w]\<^sub>\<Pi>\<^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[\<F>\<G> \<phi>1 w]\<^sub>\<Pi>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>1; \<And>w. w \<Turnstile>\<^sub>n \<phi>2[\<F>\<G> \<phi>2 w]\<^sub>\<Pi>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>2\<rbrakk> \<Longrightarrow> w \<Turnstile>\<^sub>n \<phi>1 M\<^sub>n \<phi>2[\<F>\<G> (\<phi>1 M\<^sub>n \<phi>2) w]\<^sub>\<Pi>\<^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[\<F>\<G> true\<^sub>n w]\<^sub>\<Pi>\<^sub>2 = w \<Turnstile>\<^sub>n true\<^sub>n
 2. \<And>w. w \<Turnstile>\<^sub>n false\<^sub>n[\<F>\<G> false\<^sub>n w]\<^sub>\<Pi>\<^sub>2 = w \<Turnstile>\<^sub>n false\<^sub>n
 3. \<And>x w. w \<Turnstile>\<^sub>n prop\<^sub>n(x)[\<F>\<G> prop\<^sub>n(x) w]\<^sub>\<Pi>\<^sub>2 = w \<Turnstile>\<^sub>n prop\<^sub>n(x)
 4. \<And>x w. w \<Turnstile>\<^sub>n nprop\<^sub>n(x)[\<F>\<G> nprop\<^sub>n(x) w]\<^sub>\<Pi>\<^sub>2 = w \<Turnstile>\<^sub>n nprop\<^sub>n(x)
 5. \<And>\<phi> w. (\<And>w. w \<Turnstile>\<^sub>n \<phi>[\<F>\<G> \<phi> w]\<^sub>\<Pi>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>) \<Longrightarrow> w \<Turnstile>\<^sub>n X\<^sub>n \<phi>[\<F>\<G> (X\<^sub>n \<phi>) w]\<^sub>\<Pi>\<^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[\<F>\<G> \<phi>1 w]\<^sub>\<Pi>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>1; \<And>w. w \<Turnstile>\<^sub>n \<phi>2[\<F>\<G> \<phi>2 w]\<^sub>\<Pi>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>2\<rbrakk> \<Longrightarrow> w \<Turnstile>\<^sub>n \<phi>1 U\<^sub>n \<phi>2[\<F>\<G> (\<phi>1 U\<^sub>n \<phi>2) w]\<^sub>\<Pi>\<^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[\<F>\<G> \<phi>1 w]\<^sub>\<Pi>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>1; \<And>w. w \<Turnstile>\<^sub>n \<phi>2[\<F>\<G> \<phi>2 w]\<^sub>\<Pi>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>2\<rbrakk> \<Longrightarrow> w \<Turnstile>\<^sub>n \<phi>1 R\<^sub>n \<phi>2[\<F>\<G> (\<phi>1 R\<^sub>n \<phi>2) w]\<^sub>\<Pi>\<^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[\<F>\<G> \<phi>1 w]\<^sub>\<Pi>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>1; \<And>w. w \<Turnstile>\<^sub>n \<phi>2[\<F>\<G> \<phi>2 w]\<^sub>\<Pi>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>2\<rbrakk> \<Longrightarrow> w \<Turnstile>\<^sub>n \<phi>1 W\<^sub>n \<phi>2[\<F>\<G> (\<phi>1 W\<^sub>n \<phi>2) w]\<^sub>\<Pi>\<^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[\<F>\<G> \<phi>1 w]\<^sub>\<Pi>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>1; \<And>w. w \<Turnstile>\<^sub>n \<phi>2[\<F>\<G> \<phi>2 w]\<^sub>\<Pi>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>2\<rbrakk> \<Longrightarrow> w \<Turnstile>\<^sub>n \<phi>1 M\<^sub>n \<phi>2[\<F>\<G> (\<phi>1 M\<^sub>n \<phi>2) w]\<^sub>\<Pi>\<^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>[\<F>\<G> \<phi> ?w]\<^sub>\<Pi>\<^sub>2 = ?w \<Turnstile>\<^sub>n \<phi>

goal (9 subgoals):
 1. \<And>w. w \<Turnstile>\<^sub>n true\<^sub>n[\<F>\<G> true\<^sub>n w]\<^sub>\<Pi>\<^sub>2 = w \<Turnstile>\<^sub>n true\<^sub>n
 2. \<And>w. w \<Turnstile>\<^sub>n false\<^sub>n[\<F>\<G> false\<^sub>n w]\<^sub>\<Pi>\<^sub>2 = w \<Turnstile>\<^sub>n false\<^sub>n
 3. \<And>x w. w \<Turnstile>\<^sub>n prop\<^sub>n(x)[\<F>\<G> prop\<^sub>n(x) w]\<^sub>\<Pi>\<^sub>2 = w \<Turnstile>\<^sub>n prop\<^sub>n(x)
 4. \<And>x w. w \<Turnstile>\<^sub>n nprop\<^sub>n(x)[\<F>\<G> nprop\<^sub>n(x) w]\<^sub>\<Pi>\<^sub>2 = w \<Turnstile>\<^sub>n nprop\<^sub>n(x)
 5. \<And>\<phi> w. (\<And>w. w \<Turnstile>\<^sub>n \<phi>[\<F>\<G> \<phi> w]\<^sub>\<Pi>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>) \<Longrightarrow> w \<Turnstile>\<^sub>n X\<^sub>n \<phi>[\<F>\<G> (X\<^sub>n \<phi>) w]\<^sub>\<Pi>\<^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[\<F>\<G> \<phi>1 w]\<^sub>\<Pi>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>1; \<And>w. w \<Turnstile>\<^sub>n \<phi>2[\<F>\<G> \<phi>2 w]\<^sub>\<Pi>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>2\<rbrakk> \<Longrightarrow> w \<Turnstile>\<^sub>n \<phi>1 U\<^sub>n \<phi>2[\<F>\<G> (\<phi>1 U\<^sub>n \<phi>2) w]\<^sub>\<Pi>\<^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[\<F>\<G> \<phi>1 w]\<^sub>\<Pi>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>1; \<And>w. w \<Turnstile>\<^sub>n \<phi>2[\<F>\<G> \<phi>2 w]\<^sub>\<Pi>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>2\<rbrakk> \<Longrightarrow> w \<Turnstile>\<^sub>n \<phi>1 R\<^sub>n \<phi>2[\<F>\<G> (\<phi>1 R\<^sub>n \<phi>2) w]\<^sub>\<Pi>\<^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[\<F>\<G> \<phi>1 w]\<^sub>\<Pi>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>1; \<And>w. w \<Turnstile>\<^sub>n \<phi>2[\<F>\<G> \<phi>2 w]\<^sub>\<Pi>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>2\<rbrakk> \<Longrightarrow> w \<Turnstile>\<^sub>n \<phi>1 W\<^sub>n \<phi>2[\<F>\<G> (\<phi>1 W\<^sub>n \<phi>2) w]\<^sub>\<Pi>\<^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[\<F>\<G> \<phi>1 w]\<^sub>\<Pi>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>1; \<And>w. w \<Turnstile>\<^sub>n \<phi>2[\<F>\<G> \<phi>2 w]\<^sub>\<Pi>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>2\<rbrakk> \<Longrightarrow> w \<Turnstile>\<^sub>n \<phi>1 M\<^sub>n \<phi>2[\<F>\<G> (\<phi>1 M\<^sub>n \<phi>2) w]\<^sub>\<Pi>\<^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>[\<F>\<G> \<phi> ?w]\<^sub>\<Pi>\<^sub>2 = ?w \<Turnstile>\<^sub>n \<phi>
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
?w \<Turnstile>\<^sub>n \<phi>[\<F>\<G> \<phi> ?w]\<^sub>\<Pi>\<^sub>2 = ?w \<Turnstile>\<^sub>n \<phi>

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

goal (1 subgoal):
 1. w \<Turnstile>\<^sub>n X\<^sub>n \<phi>[\<F>\<G> (X\<^sub>n \<phi>) w]\<^sub>\<Pi>\<^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>[\<F>\<G> (X\<^sub>n \<phi>) w]\<^sub>\<Pi>\<^sub>2 = w \<Turnstile>\<^sub>n X\<^sub>n \<phi>

goal (8 subgoals):
 1. \<And>w. w \<Turnstile>\<^sub>n true\<^sub>n[\<F>\<G> true\<^sub>n w]\<^sub>\<Pi>\<^sub>2 = w \<Turnstile>\<^sub>n true\<^sub>n
 2. \<And>w. w \<Turnstile>\<^sub>n false\<^sub>n[\<F>\<G> false\<^sub>n w]\<^sub>\<Pi>\<^sub>2 = w \<Turnstile>\<^sub>n false\<^sub>n
 3. \<And>x w. w \<Turnstile>\<^sub>n prop\<^sub>n(x)[\<F>\<G> prop\<^sub>n(x) w]\<^sub>\<Pi>\<^sub>2 = w \<Turnstile>\<^sub>n prop\<^sub>n(x)
 4. \<And>x w. w \<Turnstile>\<^sub>n nprop\<^sub>n(x)[\<F>\<G> nprop\<^sub>n(x) w]\<^sub>\<Pi>\<^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[\<F>\<G> \<phi>1 w]\<^sub>\<Pi>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>1; \<And>w. w \<Turnstile>\<^sub>n \<phi>2[\<F>\<G> \<phi>2 w]\<^sub>\<Pi>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>2\<rbrakk> \<Longrightarrow> w \<Turnstile>\<^sub>n \<phi>1 U\<^sub>n \<phi>2[\<F>\<G> (\<phi>1 U\<^sub>n \<phi>2) w]\<^sub>\<Pi>\<^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[\<F>\<G> \<phi>1 w]\<^sub>\<Pi>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>1; \<And>w. w \<Turnstile>\<^sub>n \<phi>2[\<F>\<G> \<phi>2 w]\<^sub>\<Pi>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>2\<rbrakk> \<Longrightarrow> w \<Turnstile>\<^sub>n \<phi>1 R\<^sub>n \<phi>2[\<F>\<G> (\<phi>1 R\<^sub>n \<phi>2) w]\<^sub>\<Pi>\<^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[\<F>\<G> \<phi>1 w]\<^sub>\<Pi>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>1; \<And>w. w \<Turnstile>\<^sub>n \<phi>2[\<F>\<G> \<phi>2 w]\<^sub>\<Pi>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>2\<rbrakk> \<Longrightarrow> w \<Turnstile>\<^sub>n \<phi>1 W\<^sub>n \<phi>2[\<F>\<G> (\<phi>1 W\<^sub>n \<phi>2) w]\<^sub>\<Pi>\<^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[\<F>\<G> \<phi>1 w]\<^sub>\<Pi>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>1; \<And>w. w \<Turnstile>\<^sub>n \<phi>2[\<F>\<G> \<phi>2 w]\<^sub>\<Pi>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>2\<rbrakk> \<Longrightarrow> w \<Turnstile>\<^sub>n \<phi>1 M\<^sub>n \<phi>2[\<F>\<G> (\<phi>1 M\<^sub>n \<phi>2) w]\<^sub>\<Pi>\<^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[\<F>\<G> true\<^sub>n w]\<^sub>\<Pi>\<^sub>2 = w \<Turnstile>\<^sub>n true\<^sub>n
 2. \<And>w. w \<Turnstile>\<^sub>n false\<^sub>n[\<F>\<G> false\<^sub>n w]\<^sub>\<Pi>\<^sub>2 = w \<Turnstile>\<^sub>n false\<^sub>n
 3. \<And>x w. w \<Turnstile>\<^sub>n prop\<^sub>n(x)[\<F>\<G> prop\<^sub>n(x) w]\<^sub>\<Pi>\<^sub>2 = w \<Turnstile>\<^sub>n prop\<^sub>n(x)
 4. \<And>x w. w \<Turnstile>\<^sub>n nprop\<^sub>n(x)[\<F>\<G> nprop\<^sub>n(x) w]\<^sub>\<Pi>\<^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[\<F>\<G> \<phi>1 w]\<^sub>\<Pi>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>1; \<And>w. w \<Turnstile>\<^sub>n \<phi>2[\<F>\<G> \<phi>2 w]\<^sub>\<Pi>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>2\<rbrakk> \<Longrightarrow> w \<Turnstile>\<^sub>n \<phi>1 U\<^sub>n \<phi>2[\<F>\<G> (\<phi>1 U\<^sub>n \<phi>2) w]\<^sub>\<Pi>\<^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[\<F>\<G> \<phi>1 w]\<^sub>\<Pi>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>1; \<And>w. w \<Turnstile>\<^sub>n \<phi>2[\<F>\<G> \<phi>2 w]\<^sub>\<Pi>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>2\<rbrakk> \<Longrightarrow> w \<Turnstile>\<^sub>n \<phi>1 R\<^sub>n \<phi>2[\<F>\<G> (\<phi>1 R\<^sub>n \<phi>2) w]\<^sub>\<Pi>\<^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[\<F>\<G> \<phi>1 w]\<^sub>\<Pi>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>1; \<And>w. w \<Turnstile>\<^sub>n \<phi>2[\<F>\<G> \<phi>2 w]\<^sub>\<Pi>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>2\<rbrakk> \<Longrightarrow> w \<Turnstile>\<^sub>n \<phi>1 W\<^sub>n \<phi>2[\<F>\<G> (\<phi>1 W\<^sub>n \<phi>2) w]\<^sub>\<Pi>\<^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[\<F>\<G> \<phi>1 w]\<^sub>\<Pi>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>1; \<And>w. w \<Turnstile>\<^sub>n \<phi>2[\<F>\<G> \<phi>2 w]\<^sub>\<Pi>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>2\<rbrakk> \<Longrightarrow> w \<Turnstile>\<^sub>n \<phi>1 M\<^sub>n \<phi>2[\<F>\<G> (\<phi>1 M\<^sub>n \<phi>2) w]\<^sub>\<Pi>\<^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[\<F>\<G> \<phi>1 ?w]\<^sub>\<Pi>\<^sub>2 = ?w \<Turnstile>\<^sub>n \<phi>1
?w \<Turnstile>\<^sub>n \<phi>2[\<F>\<G> \<phi>2 ?w]\<^sub>\<Pi>\<^sub>2 = ?w \<Turnstile>\<^sub>n \<phi>2

goal (8 subgoals):
 1. \<And>w. w \<Turnstile>\<^sub>n true\<^sub>n[\<F>\<G> true\<^sub>n w]\<^sub>\<Pi>\<^sub>2 = w \<Turnstile>\<^sub>n true\<^sub>n
 2. \<And>w. w \<Turnstile>\<^sub>n false\<^sub>n[\<F>\<G> false\<^sub>n w]\<^sub>\<Pi>\<^sub>2 = w \<Turnstile>\<^sub>n false\<^sub>n
 3. \<And>x w. w \<Turnstile>\<^sub>n prop\<^sub>n(x)[\<F>\<G> prop\<^sub>n(x) w]\<^sub>\<Pi>\<^sub>2 = w \<Turnstile>\<^sub>n prop\<^sub>n(x)
 4. \<And>x w. w \<Turnstile>\<^sub>n nprop\<^sub>n(x)[\<F>\<G> nprop\<^sub>n(x) w]\<^sub>\<Pi>\<^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[\<F>\<G> \<phi>1 w]\<^sub>\<Pi>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>1; \<And>w. w \<Turnstile>\<^sub>n \<phi>2[\<F>\<G> \<phi>2 w]\<^sub>\<Pi>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>2\<rbrakk> \<Longrightarrow> w \<Turnstile>\<^sub>n \<phi>1 U\<^sub>n \<phi>2[\<F>\<G> (\<phi>1 U\<^sub>n \<phi>2) w]\<^sub>\<Pi>\<^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[\<F>\<G> \<phi>1 w]\<^sub>\<Pi>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>1; \<And>w. w \<Turnstile>\<^sub>n \<phi>2[\<F>\<G> \<phi>2 w]\<^sub>\<Pi>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>2\<rbrakk> \<Longrightarrow> w \<Turnstile>\<^sub>n \<phi>1 R\<^sub>n \<phi>2[\<F>\<G> (\<phi>1 R\<^sub>n \<phi>2) w]\<^sub>\<Pi>\<^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[\<F>\<G> \<phi>1 w]\<^sub>\<Pi>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>1; \<And>w. w \<Turnstile>\<^sub>n \<phi>2[\<F>\<G> \<phi>2 w]\<^sub>\<Pi>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>2\<rbrakk> \<Longrightarrow> w \<Turnstile>\<^sub>n \<phi>1 W\<^sub>n \<phi>2[\<F>\<G> (\<phi>1 W\<^sub>n \<phi>2) w]\<^sub>\<Pi>\<^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[\<F>\<G> \<phi>1 w]\<^sub>\<Pi>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>1; \<And>w. w \<Turnstile>\<^sub>n \<phi>2[\<F>\<G> \<phi>2 w]\<^sub>\<Pi>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>2\<rbrakk> \<Longrightarrow> w \<Turnstile>\<^sub>n \<phi>1 M\<^sub>n \<phi>2[\<F>\<G> (\<phi>1 M\<^sub>n \<phi>2) w]\<^sub>\<Pi>\<^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[\<F>\<G> \<phi>1 ?w]\<^sub>\<Pi>\<^sub>2 = ?w \<Turnstile>\<^sub>n \<phi>1
?w \<Turnstile>\<^sub>n \<phi>2[\<F>\<G> \<phi>2 ?w]\<^sub>\<Pi>\<^sub>2 = ?w \<Turnstile>\<^sub>n \<phi>2
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
?w \<Turnstile>\<^sub>n \<phi>1[\<F>\<G> \<phi>1 ?w]\<^sub>\<Pi>\<^sub>2 = ?w \<Turnstile>\<^sub>n \<phi>1
?w \<Turnstile>\<^sub>n \<phi>2[\<F>\<G> \<phi>2 ?w]\<^sub>\<Pi>\<^sub>2 = ?w \<Turnstile>\<^sub>n \<phi>2

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

goal (1 subgoal):
 1. w \<Turnstile>\<^sub>n \<phi>1 U\<^sub>n \<phi>2[\<F>\<G> (\<phi>1 U\<^sub>n \<phi>2) w]\<^sub>\<Pi>\<^sub>2 = w \<Turnstile>\<^sub>n (\<phi>1 and\<^sub>n F\<^sub>n \<phi>2[\<F>\<G> (\<phi>1 U\<^sub>n \<phi>2) w]\<^sub>\<Sigma>\<^sub>1) W\<^sub>n \<phi>2
[PROOF STEP]
using flatten_pi_2_IH_lifting[of _ "\<phi>1 U\<^sub>n \<phi>2"]
[PROOF STATE]
proof (prove)
using this:
?w \<Turnstile>\<^sub>n \<phi>1[\<F>\<G> \<phi>1 ?w]\<^sub>\<Pi>\<^sub>2 = ?w \<Turnstile>\<^sub>n \<phi>1
?w \<Turnstile>\<^sub>n \<phi>2[\<F>\<G> \<phi>2 ?w]\<^sub>\<Pi>\<^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>[\<F>\<G> ?\<psi> (suffix ?i ?w)]\<^sub>\<Pi>\<^sub>2 = suffix ?i ?w \<Turnstile>\<^sub>n ?\<psi>\<rbrakk> \<Longrightarrow> suffix ?i ?w \<Turnstile>\<^sub>n ?\<psi>[\<F>\<G> (\<phi>1 U\<^sub>n \<phi>2) ?w]\<^sub>\<Pi>\<^sub>2 = suffix ?i ?w \<Turnstile>\<^sub>n ?\<psi>

goal (1 subgoal):
 1. w \<Turnstile>\<^sub>n \<phi>1 U\<^sub>n \<phi>2[\<F>\<G> (\<phi>1 U\<^sub>n \<phi>2) w]\<^sub>\<Pi>\<^sub>2 = w \<Turnstile>\<^sub>n (\<phi>1 and\<^sub>n F\<^sub>n \<phi>2[\<F>\<G> (\<phi>1 U\<^sub>n \<phi>2) w]\<^sub>\<Sigma>\<^sub>1) W\<^sub>n \<phi>2
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
w \<Turnstile>\<^sub>n \<phi>1 U\<^sub>n \<phi>2[\<F>\<G> (\<phi>1 U\<^sub>n \<phi>2) w]\<^sub>\<Pi>\<^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[\<F>\<G> true\<^sub>n w]\<^sub>\<Pi>\<^sub>2 = w \<Turnstile>\<^sub>n true\<^sub>n
 2. \<And>w. w \<Turnstile>\<^sub>n false\<^sub>n[\<F>\<G> false\<^sub>n w]\<^sub>\<Pi>\<^sub>2 = w \<Turnstile>\<^sub>n false\<^sub>n
 3. \<And>x w. w \<Turnstile>\<^sub>n prop\<^sub>n(x)[\<F>\<G> prop\<^sub>n(x) w]\<^sub>\<Pi>\<^sub>2 = w \<Turnstile>\<^sub>n prop\<^sub>n(x)
 4. \<And>x w. w \<Turnstile>\<^sub>n nprop\<^sub>n(x)[\<F>\<G> nprop\<^sub>n(x) w]\<^sub>\<Pi>\<^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[\<F>\<G> \<phi>1 w]\<^sub>\<Pi>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>1; \<And>w. w \<Turnstile>\<^sub>n \<phi>2[\<F>\<G> \<phi>2 w]\<^sub>\<Pi>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>2\<rbrakk> \<Longrightarrow> w \<Turnstile>\<^sub>n \<phi>1 R\<^sub>n \<phi>2[\<F>\<G> (\<phi>1 R\<^sub>n \<phi>2) w]\<^sub>\<Pi>\<^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[\<F>\<G> \<phi>1 w]\<^sub>\<Pi>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>1; \<And>w. w \<Turnstile>\<^sub>n \<phi>2[\<F>\<G> \<phi>2 w]\<^sub>\<Pi>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>2\<rbrakk> \<Longrightarrow> w \<Turnstile>\<^sub>n \<phi>1 W\<^sub>n \<phi>2[\<F>\<G> (\<phi>1 W\<^sub>n \<phi>2) w]\<^sub>\<Pi>\<^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[\<F>\<G> \<phi>1 w]\<^sub>\<Pi>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>1; \<And>w. w \<Turnstile>\<^sub>n \<phi>2[\<F>\<G> \<phi>2 w]\<^sub>\<Pi>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>2\<rbrakk> \<Longrightarrow> w \<Turnstile>\<^sub>n \<phi>1 M\<^sub>n \<phi>2[\<F>\<G> (\<phi>1 M\<^sub>n \<phi>2) w]\<^sub>\<Pi>\<^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[\<F>\<G> true\<^sub>n w]\<^sub>\<Pi>\<^sub>2 = w \<Turnstile>\<^sub>n true\<^sub>n
 2. \<And>w. w \<Turnstile>\<^sub>n false\<^sub>n[\<F>\<G> false\<^sub>n w]\<^sub>\<Pi>\<^sub>2 = w \<Turnstile>\<^sub>n false\<^sub>n
 3. \<And>x w. w \<Turnstile>\<^sub>n prop\<^sub>n(x)[\<F>\<G> prop\<^sub>n(x) w]\<^sub>\<Pi>\<^sub>2 = w \<Turnstile>\<^sub>n prop\<^sub>n(x)
 4. \<And>x w. w \<Turnstile>\<^sub>n nprop\<^sub>n(x)[\<F>\<G> nprop\<^sub>n(x) w]\<^sub>\<Pi>\<^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[\<F>\<G> \<phi>1 w]\<^sub>\<Pi>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>1; \<And>w. w \<Turnstile>\<^sub>n \<phi>2[\<F>\<G> \<phi>2 w]\<^sub>\<Pi>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>2\<rbrakk> \<Longrightarrow> w \<Turnstile>\<^sub>n \<phi>1 R\<^sub>n \<phi>2[\<F>\<G> (\<phi>1 R\<^sub>n \<phi>2) w]\<^sub>\<Pi>\<^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[\<F>\<G> \<phi>1 w]\<^sub>\<Pi>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>1; \<And>w. w \<Turnstile>\<^sub>n \<phi>2[\<F>\<G> \<phi>2 w]\<^sub>\<Pi>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>2\<rbrakk> \<Longrightarrow> w \<Turnstile>\<^sub>n \<phi>1 W\<^sub>n \<phi>2[\<F>\<G> (\<phi>1 W\<^sub>n \<phi>2) w]\<^sub>\<Pi>\<^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[\<F>\<G> \<phi>1 w]\<^sub>\<Pi>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>1; \<And>w. w \<Turnstile>\<^sub>n \<phi>2[\<F>\<G> \<phi>2 w]\<^sub>\<Pi>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>2\<rbrakk> \<Longrightarrow> w \<Turnstile>\<^sub>n \<phi>1 M\<^sub>n \<phi>2[\<F>\<G> (\<phi>1 M\<^sub>n \<phi>2) w]\<^sub>\<Pi>\<^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[\<F>\<G> \<phi>1 ?w]\<^sub>\<Pi>\<^sub>2 = ?w \<Turnstile>\<^sub>n \<phi>1
?w \<Turnstile>\<^sub>n \<phi>2[\<F>\<G> \<phi>2 ?w]\<^sub>\<Pi>\<^sub>2 = ?w \<Turnstile>\<^sub>n \<phi>2

goal (7 subgoals):
 1. \<And>w. w \<Turnstile>\<^sub>n true\<^sub>n[\<F>\<G> true\<^sub>n w]\<^sub>\<Pi>\<^sub>2 = w \<Turnstile>\<^sub>n true\<^sub>n
 2. \<And>w. w \<Turnstile>\<^sub>n false\<^sub>n[\<F>\<G> false\<^sub>n w]\<^sub>\<Pi>\<^sub>2 = w \<Turnstile>\<^sub>n false\<^sub>n
 3. \<And>x w. w \<Turnstile>\<^sub>n prop\<^sub>n(x)[\<F>\<G> prop\<^sub>n(x) w]\<^sub>\<Pi>\<^sub>2 = w \<Turnstile>\<^sub>n prop\<^sub>n(x)
 4. \<And>x w. w \<Turnstile>\<^sub>n nprop\<^sub>n(x)[\<F>\<G> nprop\<^sub>n(x) w]\<^sub>\<Pi>\<^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[\<F>\<G> \<phi>1 w]\<^sub>\<Pi>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>1; \<And>w. w \<Turnstile>\<^sub>n \<phi>2[\<F>\<G> \<phi>2 w]\<^sub>\<Pi>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>2\<rbrakk> \<Longrightarrow> w \<Turnstile>\<^sub>n \<phi>1 R\<^sub>n \<phi>2[\<F>\<G> (\<phi>1 R\<^sub>n \<phi>2) w]\<^sub>\<Pi>\<^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[\<F>\<G> \<phi>1 w]\<^sub>\<Pi>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>1; \<And>w. w \<Turnstile>\<^sub>n \<phi>2[\<F>\<G> \<phi>2 w]\<^sub>\<Pi>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>2\<rbrakk> \<Longrightarrow> w \<Turnstile>\<^sub>n \<phi>1 W\<^sub>n \<phi>2[\<F>\<G> (\<phi>1 W\<^sub>n \<phi>2) w]\<^sub>\<Pi>\<^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[\<F>\<G> \<phi>1 w]\<^sub>\<Pi>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>1; \<And>w. w \<Turnstile>\<^sub>n \<phi>2[\<F>\<G> \<phi>2 w]\<^sub>\<Pi>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>2\<rbrakk> \<Longrightarrow> w \<Turnstile>\<^sub>n \<phi>1 M\<^sub>n \<phi>2[\<F>\<G> (\<phi>1 M\<^sub>n \<phi>2) w]\<^sub>\<Pi>\<^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[\<F>\<G> \<phi>1 ?w]\<^sub>\<Pi>\<^sub>2 = ?w \<Turnstile>\<^sub>n \<phi>1
?w \<Turnstile>\<^sub>n \<phi>2[\<F>\<G> \<phi>2 ?w]\<^sub>\<Pi>\<^sub>2 = ?w \<Turnstile>\<^sub>n \<phi>2
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
?w \<Turnstile>\<^sub>n \<phi>1[\<F>\<G> \<phi>1 ?w]\<^sub>\<Pi>\<^sub>2 = ?w \<Turnstile>\<^sub>n \<phi>1
?w \<Turnstile>\<^sub>n \<phi>2[\<F>\<G> \<phi>2 ?w]\<^sub>\<Pi>\<^sub>2 = ?w \<Turnstile>\<^sub>n \<phi>2

goal (1 subgoal):
 1. w \<Turnstile>\<^sub>n \<phi>1 R\<^sub>n \<phi>2[\<F>\<G> (\<phi>1 R\<^sub>n \<phi>2) w]\<^sub>\<Pi>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>1 R\<^sub>n \<phi>2
[PROOF STEP]
using flatten_pi_2_IH_lifting[of _ "\<phi>1 R\<^sub>n \<phi>2"]
[PROOF STATE]
proof (prove)
using this:
?w \<Turnstile>\<^sub>n \<phi>1[\<F>\<G> \<phi>1 ?w]\<^sub>\<Pi>\<^sub>2 = ?w \<Turnstile>\<^sub>n \<phi>1
?w \<Turnstile>\<^sub>n \<phi>2[\<F>\<G> \<phi>2 ?w]\<^sub>\<Pi>\<^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>[\<F>\<G> ?\<psi> (suffix ?i ?w)]\<^sub>\<Pi>\<^sub>2 = suffix ?i ?w \<Turnstile>\<^sub>n ?\<psi>\<rbrakk> \<Longrightarrow> suffix ?i ?w \<Turnstile>\<^sub>n ?\<psi>[\<F>\<G> (\<phi>1 R\<^sub>n \<phi>2) ?w]\<^sub>\<Pi>\<^sub>2 = suffix ?i ?w \<Turnstile>\<^sub>n ?\<psi>

goal (1 subgoal):
 1. w \<Turnstile>\<^sub>n \<phi>1 R\<^sub>n \<phi>2[\<F>\<G> (\<phi>1 R\<^sub>n \<phi>2) w]\<^sub>\<Pi>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>1 R\<^sub>n \<phi>2
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
w \<Turnstile>\<^sub>n \<phi>1 R\<^sub>n \<phi>2[\<F>\<G> (\<phi>1 R\<^sub>n \<phi>2) w]\<^sub>\<Pi>\<^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[\<F>\<G> true\<^sub>n w]\<^sub>\<Pi>\<^sub>2 = w \<Turnstile>\<^sub>n true\<^sub>n
 2. \<And>w. w \<Turnstile>\<^sub>n false\<^sub>n[\<F>\<G> false\<^sub>n w]\<^sub>\<Pi>\<^sub>2 = w \<Turnstile>\<^sub>n false\<^sub>n
 3. \<And>x w. w \<Turnstile>\<^sub>n prop\<^sub>n(x)[\<F>\<G> prop\<^sub>n(x) w]\<^sub>\<Pi>\<^sub>2 = w \<Turnstile>\<^sub>n prop\<^sub>n(x)
 4. \<And>x w. w \<Turnstile>\<^sub>n nprop\<^sub>n(x)[\<F>\<G> nprop\<^sub>n(x) w]\<^sub>\<Pi>\<^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[\<F>\<G> \<phi>1 w]\<^sub>\<Pi>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>1; \<And>w. w \<Turnstile>\<^sub>n \<phi>2[\<F>\<G> \<phi>2 w]\<^sub>\<Pi>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>2\<rbrakk> \<Longrightarrow> w \<Turnstile>\<^sub>n \<phi>1 W\<^sub>n \<phi>2[\<F>\<G> (\<phi>1 W\<^sub>n \<phi>2) w]\<^sub>\<Pi>\<^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[\<F>\<G> \<phi>1 w]\<^sub>\<Pi>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>1; \<And>w. w \<Turnstile>\<^sub>n \<phi>2[\<F>\<G> \<phi>2 w]\<^sub>\<Pi>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>2\<rbrakk> \<Longrightarrow> w \<Turnstile>\<^sub>n \<phi>1 M\<^sub>n \<phi>2[\<F>\<G> (\<phi>1 M\<^sub>n \<phi>2) w]\<^sub>\<Pi>\<^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[\<F>\<G> true\<^sub>n w]\<^sub>\<Pi>\<^sub>2 = w \<Turnstile>\<^sub>n true\<^sub>n
 2. \<And>w. w \<Turnstile>\<^sub>n false\<^sub>n[\<F>\<G> false\<^sub>n w]\<^sub>\<Pi>\<^sub>2 = w \<Turnstile>\<^sub>n false\<^sub>n
 3. \<And>x w. w \<Turnstile>\<^sub>n prop\<^sub>n(x)[\<F>\<G> prop\<^sub>n(x) w]\<^sub>\<Pi>\<^sub>2 = w \<Turnstile>\<^sub>n prop\<^sub>n(x)
 4. \<And>x w. w \<Turnstile>\<^sub>n nprop\<^sub>n(x)[\<F>\<G> nprop\<^sub>n(x) w]\<^sub>\<Pi>\<^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[\<F>\<G> \<phi>1 w]\<^sub>\<Pi>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>1; \<And>w. w \<Turnstile>\<^sub>n \<phi>2[\<F>\<G> \<phi>2 w]\<^sub>\<Pi>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>2\<rbrakk> \<Longrightarrow> w \<Turnstile>\<^sub>n \<phi>1 W\<^sub>n \<phi>2[\<F>\<G> (\<phi>1 W\<^sub>n \<phi>2) w]\<^sub>\<Pi>\<^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[\<F>\<G> \<phi>1 w]\<^sub>\<Pi>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>1; \<And>w. w \<Turnstile>\<^sub>n \<phi>2[\<F>\<G> \<phi>2 w]\<^sub>\<Pi>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>2\<rbrakk> \<Longrightarrow> w \<Turnstile>\<^sub>n \<phi>1 M\<^sub>n \<phi>2[\<F>\<G> (\<phi>1 M\<^sub>n \<phi>2) w]\<^sub>\<Pi>\<^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[\<F>\<G> \<phi>1 ?w]\<^sub>\<Pi>\<^sub>2 = ?w \<Turnstile>\<^sub>n \<phi>1
?w \<Turnstile>\<^sub>n \<phi>2[\<F>\<G> \<phi>2 ?w]\<^sub>\<Pi>\<^sub>2 = ?w \<Turnstile>\<^sub>n \<phi>2

goal (6 subgoals):
 1. \<And>w. w \<Turnstile>\<^sub>n true\<^sub>n[\<F>\<G> true\<^sub>n w]\<^sub>\<Pi>\<^sub>2 = w \<Turnstile>\<^sub>n true\<^sub>n
 2. \<And>w. w \<Turnstile>\<^sub>n false\<^sub>n[\<F>\<G> false\<^sub>n w]\<^sub>\<Pi>\<^sub>2 = w \<Turnstile>\<^sub>n false\<^sub>n
 3. \<And>x w. w \<Turnstile>\<^sub>n prop\<^sub>n(x)[\<F>\<G> prop\<^sub>n(x) w]\<^sub>\<Pi>\<^sub>2 = w \<Turnstile>\<^sub>n prop\<^sub>n(x)
 4. \<And>x w. w \<Turnstile>\<^sub>n nprop\<^sub>n(x)[\<F>\<G> nprop\<^sub>n(x) w]\<^sub>\<Pi>\<^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[\<F>\<G> \<phi>1 w]\<^sub>\<Pi>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>1; \<And>w. w \<Turnstile>\<^sub>n \<phi>2[\<F>\<G> \<phi>2 w]\<^sub>\<Pi>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>2\<rbrakk> \<Longrightarrow> w \<Turnstile>\<^sub>n \<phi>1 W\<^sub>n \<phi>2[\<F>\<G> (\<phi>1 W\<^sub>n \<phi>2) w]\<^sub>\<Pi>\<^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[\<F>\<G> \<phi>1 w]\<^sub>\<Pi>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>1; \<And>w. w \<Turnstile>\<^sub>n \<phi>2[\<F>\<G> \<phi>2 w]\<^sub>\<Pi>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>2\<rbrakk> \<Longrightarrow> w \<Turnstile>\<^sub>n \<phi>1 M\<^sub>n \<phi>2[\<F>\<G> (\<phi>1 M\<^sub>n \<phi>2) w]\<^sub>\<Pi>\<^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[\<F>\<G> \<phi>1 ?w]\<^sub>\<Pi>\<^sub>2 = ?w \<Turnstile>\<^sub>n \<phi>1
?w \<Turnstile>\<^sub>n \<phi>2[\<F>\<G> \<phi>2 ?w]\<^sub>\<Pi>\<^sub>2 = ?w \<Turnstile>\<^sub>n \<phi>2
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
?w \<Turnstile>\<^sub>n \<phi>1[\<F>\<G> \<phi>1 ?w]\<^sub>\<Pi>\<^sub>2 = ?w \<Turnstile>\<^sub>n \<phi>1
?w \<Turnstile>\<^sub>n \<phi>2[\<F>\<G> \<phi>2 ?w]\<^sub>\<Pi>\<^sub>2 = ?w \<Turnstile>\<^sub>n \<phi>2

goal (1 subgoal):
 1. w \<Turnstile>\<^sub>n \<phi>1 W\<^sub>n \<phi>2[\<F>\<G> (\<phi>1 W\<^sub>n \<phi>2) w]\<^sub>\<Pi>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>1 W\<^sub>n \<phi>2
[PROOF STEP]
using flatten_pi_2_IH_lifting[of _ "\<phi>1 W\<^sub>n \<phi>2"]
[PROOF STATE]
proof (prove)
using this:
?w \<Turnstile>\<^sub>n \<phi>1[\<F>\<G> \<phi>1 ?w]\<^sub>\<Pi>\<^sub>2 = ?w \<Turnstile>\<^sub>n \<phi>1
?w \<Turnstile>\<^sub>n \<phi>2[\<F>\<G> \<phi>2 ?w]\<^sub>\<Pi>\<^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>[\<F>\<G> ?\<psi> (suffix ?i ?w)]\<^sub>\<Pi>\<^sub>2 = suffix ?i ?w \<Turnstile>\<^sub>n ?\<psi>\<rbrakk> \<Longrightarrow> suffix ?i ?w \<Turnstile>\<^sub>n ?\<psi>[\<F>\<G> (\<phi>1 W\<^sub>n \<phi>2) ?w]\<^sub>\<Pi>\<^sub>2 = suffix ?i ?w \<Turnstile>\<^sub>n ?\<psi>

goal (1 subgoal):
 1. w \<Turnstile>\<^sub>n \<phi>1 W\<^sub>n \<phi>2[\<F>\<G> (\<phi>1 W\<^sub>n \<phi>2) w]\<^sub>\<Pi>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>1 W\<^sub>n \<phi>2
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
w \<Turnstile>\<^sub>n \<phi>1 W\<^sub>n \<phi>2[\<F>\<G> (\<phi>1 W\<^sub>n \<phi>2) w]\<^sub>\<Pi>\<^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[\<F>\<G> true\<^sub>n w]\<^sub>\<Pi>\<^sub>2 = w \<Turnstile>\<^sub>n true\<^sub>n
 2. \<And>w. w \<Turnstile>\<^sub>n false\<^sub>n[\<F>\<G> false\<^sub>n w]\<^sub>\<Pi>\<^sub>2 = w \<Turnstile>\<^sub>n false\<^sub>n
 3. \<And>x w. w \<Turnstile>\<^sub>n prop\<^sub>n(x)[\<F>\<G> prop\<^sub>n(x) w]\<^sub>\<Pi>\<^sub>2 = w \<Turnstile>\<^sub>n prop\<^sub>n(x)
 4. \<And>x w. w \<Turnstile>\<^sub>n nprop\<^sub>n(x)[\<F>\<G> nprop\<^sub>n(x) w]\<^sub>\<Pi>\<^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[\<F>\<G> \<phi>1 w]\<^sub>\<Pi>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>1; \<And>w. w \<Turnstile>\<^sub>n \<phi>2[\<F>\<G> \<phi>2 w]\<^sub>\<Pi>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>2\<rbrakk> \<Longrightarrow> w \<Turnstile>\<^sub>n \<phi>1 M\<^sub>n \<phi>2[\<F>\<G> (\<phi>1 M\<^sub>n \<phi>2) w]\<^sub>\<Pi>\<^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[\<F>\<G> true\<^sub>n w]\<^sub>\<Pi>\<^sub>2 = w \<Turnstile>\<^sub>n true\<^sub>n
 2. \<And>w. w \<Turnstile>\<^sub>n false\<^sub>n[\<F>\<G> false\<^sub>n w]\<^sub>\<Pi>\<^sub>2 = w \<Turnstile>\<^sub>n false\<^sub>n
 3. \<And>x w. w \<Turnstile>\<^sub>n prop\<^sub>n(x)[\<F>\<G> prop\<^sub>n(x) w]\<^sub>\<Pi>\<^sub>2 = w \<Turnstile>\<^sub>n prop\<^sub>n(x)
 4. \<And>x w. w \<Turnstile>\<^sub>n nprop\<^sub>n(x)[\<F>\<G> nprop\<^sub>n(x) w]\<^sub>\<Pi>\<^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[\<F>\<G> \<phi>1 w]\<^sub>\<Pi>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>1; \<And>w. w \<Turnstile>\<^sub>n \<phi>2[\<F>\<G> \<phi>2 w]\<^sub>\<Pi>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>2\<rbrakk> \<Longrightarrow> w \<Turnstile>\<^sub>n \<phi>1 M\<^sub>n \<phi>2[\<F>\<G> (\<phi>1 M\<^sub>n \<phi>2) w]\<^sub>\<Pi>\<^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[\<F>\<G> \<phi>1 ?w]\<^sub>\<Pi>\<^sub>2 = ?w \<Turnstile>\<^sub>n \<phi>1
?w \<Turnstile>\<^sub>n \<phi>2[\<F>\<G> \<phi>2 ?w]\<^sub>\<Pi>\<^sub>2 = ?w \<Turnstile>\<^sub>n \<phi>2

goal (5 subgoals):
 1. \<And>w. w \<Turnstile>\<^sub>n true\<^sub>n[\<F>\<G> true\<^sub>n w]\<^sub>\<Pi>\<^sub>2 = w \<Turnstile>\<^sub>n true\<^sub>n
 2. \<And>w. w \<Turnstile>\<^sub>n false\<^sub>n[\<F>\<G> false\<^sub>n w]\<^sub>\<Pi>\<^sub>2 = w \<Turnstile>\<^sub>n false\<^sub>n
 3. \<And>x w. w \<Turnstile>\<^sub>n prop\<^sub>n(x)[\<F>\<G> prop\<^sub>n(x) w]\<^sub>\<Pi>\<^sub>2 = w \<Turnstile>\<^sub>n prop\<^sub>n(x)
 4. \<And>x w. w \<Turnstile>\<^sub>n nprop\<^sub>n(x)[\<F>\<G> nprop\<^sub>n(x) w]\<^sub>\<Pi>\<^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[\<F>\<G> \<phi>1 w]\<^sub>\<Pi>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>1; \<And>w. w \<Turnstile>\<^sub>n \<phi>2[\<F>\<G> \<phi>2 w]\<^sub>\<Pi>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>2\<rbrakk> \<Longrightarrow> w \<Turnstile>\<^sub>n \<phi>1 M\<^sub>n \<phi>2[\<F>\<G> (\<phi>1 M\<^sub>n \<phi>2) w]\<^sub>\<Pi>\<^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[\<F>\<G> \<phi>1 ?w]\<^sub>\<Pi>\<^sub>2 = ?w \<Turnstile>\<^sub>n \<phi>1
?w \<Turnstile>\<^sub>n \<phi>2[\<F>\<G> \<phi>2 ?w]\<^sub>\<Pi>\<^sub>2 = ?w \<Turnstile>\<^sub>n \<phi>2
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
?w \<Turnstile>\<^sub>n \<phi>1[\<F>\<G> \<phi>1 ?w]\<^sub>\<Pi>\<^sub>2 = ?w \<Turnstile>\<^sub>n \<phi>1
?w \<Turnstile>\<^sub>n \<phi>2[\<F>\<G> \<phi>2 ?w]\<^sub>\<Pi>\<^sub>2 = ?w \<Turnstile>\<^sub>n \<phi>2

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

goal (1 subgoal):
 1. w \<Turnstile>\<^sub>n \<phi>1 M\<^sub>n \<phi>2[\<F>\<G> (\<phi>1 M\<^sub>n \<phi>2) w]\<^sub>\<Pi>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>1 R\<^sub>n (\<phi>2 and\<^sub>n F\<^sub>n \<phi>1[\<F>\<G> (\<phi>1 M\<^sub>n \<phi>2) w]\<^sub>\<Sigma>\<^sub>1)
[PROOF STEP]
using flatten_pi_2_IH_lifting[of _ "\<phi>1 M\<^sub>n \<phi>2"]
[PROOF STATE]
proof (prove)
using this:
?w \<Turnstile>\<^sub>n \<phi>1[\<F>\<G> \<phi>1 ?w]\<^sub>\<Pi>\<^sub>2 = ?w \<Turnstile>\<^sub>n \<phi>1
?w \<Turnstile>\<^sub>n \<phi>2[\<F>\<G> \<phi>2 ?w]\<^sub>\<Pi>\<^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>[\<F>\<G> ?\<psi> (suffix ?i ?w)]\<^sub>\<Pi>\<^sub>2 = suffix ?i ?w \<Turnstile>\<^sub>n ?\<psi>\<rbrakk> \<Longrightarrow> suffix ?i ?w \<Turnstile>\<^sub>n ?\<psi>[\<F>\<G> (\<phi>1 M\<^sub>n \<phi>2) ?w]\<^sub>\<Pi>\<^sub>2 = suffix ?i ?w \<Turnstile>\<^sub>n ?\<psi>

goal (1 subgoal):
 1. w \<Turnstile>\<^sub>n \<phi>1 M\<^sub>n \<phi>2[\<F>\<G> (\<phi>1 M\<^sub>n \<phi>2) w]\<^sub>\<Pi>\<^sub>2 = w \<Turnstile>\<^sub>n \<phi>1 R\<^sub>n (\<phi>2 and\<^sub>n F\<^sub>n \<phi>1[\<F>\<G> (\<phi>1 M\<^sub>n \<phi>2) w]\<^sub>\<Sigma>\<^sub>1)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
w \<Turnstile>\<^sub>n \<phi>1 M\<^sub>n \<phi>2[\<F>\<G> (\<phi>1 M\<^sub>n \<phi>2) w]\<^sub>\<Pi>\<^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[\<F>\<G> true\<^sub>n w]\<^sub>\<Pi>\<^sub>2 = w \<Turnstile>\<^sub>n true\<^sub>n
 2. \<And>w. w \<Turnstile>\<^sub>n false\<^sub>n[\<F>\<G> false\<^sub>n w]\<^sub>\<Pi>\<^sub>2 = w \<Turnstile>\<^sub>n false\<^sub>n
 3. \<And>x w. w \<Turnstile>\<^sub>n prop\<^sub>n(x)[\<F>\<G> prop\<^sub>n(x) w]\<^sub>\<Pi>\<^sub>2 = w \<Turnstile>\<^sub>n prop\<^sub>n(x)
 4. \<And>x w. w \<Turnstile>\<^sub>n nprop\<^sub>n(x)[\<F>\<G> nprop\<^sub>n(x) w]\<^sub>\<Pi>\<^sub>2 = w \<Turnstile>\<^sub>n nprop\<^sub>n(x)
[PROOF STEP]
qed auto


[STATEMENT]
theorem normal_form_with_flatten_sigma_2:
  "w \<Turnstile>\<^sub>n \<phi> \<longleftrightarrow>
    (\<exists>M \<subseteq> subformulas\<^sub>\<mu> \<phi>. \<exists>N \<subseteq> subformulas\<^sub>\<nu> \<phi>.
      w \<Turnstile>\<^sub>n \<phi>[M]\<^sub>\<Sigma>\<^sub>2 \<and> (\<forall>\<psi> \<in> M. w \<Turnstile>\<^sub>n G\<^sub>n (F\<^sub>n \<psi>[N]\<^sub>\<Sigma>\<^sub>1)) \<and> (\<forall>\<psi> \<in> N. w \<Turnstile>\<^sub>n F\<^sub>n (G\<^sub>n \<psi>[M]\<^sub>\<Pi>\<^sub>1)))" (is "?lhs \<longleftrightarrow> ?rhs")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. w \<Turnstile>\<^sub>n \<phi> = (\<exists>M\<subseteq>subformulas\<^sub>\<mu> \<phi>. \<exists>N\<subseteq>subformulas\<^sub>\<nu> \<phi>. w \<Turnstile>\<^sub>n \<phi>[M]\<^sub>\<Sigma>\<^sub>2 \<and> (\<forall>\<psi>\<in>M. w \<Turnstile>\<^sub>n G\<^sub>n (F\<^sub>n \<psi>[N]\<^sub>\<Sigma>\<^sub>1)) \<and> (\<forall>\<psi>\<in>N. w \<Turnstile>\<^sub>n F\<^sub>n (G\<^sub>n \<psi>[M]\<^sub>\<Pi>\<^sub>1)))
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. w \<Turnstile>\<^sub>n \<phi> \<Longrightarrow> \<exists>M\<subseteq>subformulas\<^sub>\<mu> \<phi>. \<exists>N\<subseteq>subformulas\<^sub>\<nu> \<phi>. w \<Turnstile>\<^sub>n \<phi>[M]\<^sub>\<Sigma>\<^sub>2 \<and> (\<forall>\<psi>\<in>M. w \<Turnstile>\<^sub>n G\<^sub>n (F\<^sub>n \<psi>[N]\<^sub>\<Sigma>\<^sub>1)) \<and> (\<forall>\<psi>\<in>N. w \<Turnstile>\<^sub>n F\<^sub>n (G\<^sub>n \<psi>[M]\<^sub>\<Pi>\<^sub>1))
 2. \<exists>M\<subseteq>subformulas\<^sub>\<mu> \<phi>. \<exists>N\<subseteq>subformulas\<^sub>\<nu> \<phi>. w \<Turnstile>\<^sub>n \<phi>[M]\<^sub>\<Sigma>\<^sub>2 \<and> (\<forall>\<psi>\<in>M. w \<Turnstile>\<^sub>n G\<^sub>n (F\<^sub>n \<psi>[N]\<^sub>\<Sigma>\<^sub>1)) \<and> (\<forall>\<psi>\<in>N. w \<Turnstile>\<^sub>n F\<^sub>n (G\<^sub>n \<psi>[M]\<^sub>\<Pi>\<^sub>1)) \<Longrightarrow> w \<Turnstile>\<^sub>n \<phi>
[PROOF STEP]
assume ?lhs
[PROOF STATE]
proof (state)
this:
w \<Turnstile>\<^sub>n \<phi>

goal (2 subgoals):
 1. w \<Turnstile>\<^sub>n \<phi> \<Longrightarrow> \<exists>M\<subseteq>subformulas\<^sub>\<mu> \<phi>. \<exists>N\<subseteq>subformulas\<^sub>\<nu> \<phi>. w \<Turnstile>\<^sub>n \<phi>[M]\<^sub>\<Sigma>\<^sub>2 \<and> (\<forall>\<psi>\<in>M. w \<Turnstile>\<^sub>n G\<^sub>n (F\<^sub>n \<psi>[N]\<^sub>\<Sigma>\<^sub>1)) \<and> (\<forall>\<psi>\<in>N. w \<Turnstile>\<^sub>n F\<^sub>n (G\<^sub>n \<psi>[M]\<^sub>\<Pi>\<^sub>1))
 2. \<exists>M\<subseteq>subformulas\<^sub>\<mu> \<phi>. \<exists>N\<subseteq>subformulas\<^sub>\<nu> \<phi>. w \<Turnstile>\<^sub>n \<phi>[M]\<^sub>\<Sigma>\<^sub>2 \<and> (\<forall>\<psi>\<in>M. w \<Turnstile>\<^sub>n G\<^sub>n (F\<^sub>n \<psi>[N]\<^sub>\<Sigma>\<^sub>1)) \<and> (\<forall>\<psi>\<in>N. w \<Turnstile>\<^sub>n F\<^sub>n (G\<^sub>n \<psi>[M]\<^sub>\<Pi>\<^sub>1)) \<Longrightarrow> w \<Turnstile>\<^sub>n \<phi>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
w \<Turnstile>\<^sub>n \<phi>
[PROOF STEP]
have "w \<Turnstile>\<^sub>n \<phi>[\<G>\<F> \<phi> w]\<^sub>\<Sigma>\<^sub>2"
[PROOF STATE]
proof (prove)
using this:
w \<Turnstile>\<^sub>n \<phi>

goal (1 subgoal):
 1. w \<Turnstile>\<^sub>n \<phi>[\<G>\<F> \<phi> w]\<^sub>\<Sigma>\<^sub>2
[PROOF STEP]
using flatten_sigma_2_correct
[PROOF STATE]
proof (prove)
using this:
w \<Turnstile>\<^sub>n \<phi>
?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 \<phi>[\<G>\<F> \<phi> w]\<^sub>\<Sigma>\<^sub>2
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
w \<Turnstile>\<^sub>n \<phi>[\<G>\<F> \<phi> w]\<^sub>\<Sigma>\<^sub>2

goal (2 subgoals):
 1. w \<Turnstile>\<^sub>n \<phi> \<Longrightarrow> \<exists>M\<subseteq>subformulas\<^sub>\<mu> \<phi>. \<exists>N\<subseteq>subformulas\<^sub>\<nu> \<phi>. w \<Turnstile>\<^sub>n \<phi>[M]\<^sub>\<Sigma>\<^sub>2 \<and> (\<forall>\<psi>\<in>M. w \<Turnstile>\<^sub>n G\<^sub>n (F\<^sub>n \<psi>[N]\<^sub>\<Sigma>\<^sub>1)) \<and> (\<forall>\<psi>\<in>N. w \<Turnstile>\<^sub>n F\<^sub>n (G\<^sub>n \<psi>[M]\<^sub>\<Pi>\<^sub>1))
 2. \<exists>M\<subseteq>subformulas\<^sub>\<mu> \<phi>. \<exists>N\<subseteq>subformulas\<^sub>\<nu> \<phi>. w \<Turnstile>\<^sub>n \<phi>[M]\<^sub>\<Sigma>\<^sub>2 \<and> (\<forall>\<psi>\<in>M. w \<Turnstile>\<^sub>n G\<^sub>n (F\<^sub>n \<psi>[N]\<^sub>\<Sigma>\<^sub>1)) \<and> (\<forall>\<psi>\<in>N. w \<Turnstile>\<^sub>n F\<^sub>n (G\<^sub>n \<psi>[M]\<^sub>\<Pi>\<^sub>1)) \<Longrightarrow> w \<Turnstile>\<^sub>n \<phi>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
w \<Turnstile>\<^sub>n \<phi>[\<G>\<F> \<phi> w]\<^sub>\<Sigma>\<^sub>2
[PROOF STEP]
show ?rhs
[PROOF STATE]
proof (prove)
using this:
w \<Turnstile>\<^sub>n \<phi>[\<G>\<F> \<phi> w]\<^sub>\<Sigma>\<^sub>2

goal (1 subgoal):
 1. \<exists>M\<subseteq>subformulas\<^sub>\<mu> \<phi>. \<exists>N\<subseteq>subformulas\<^sub>\<nu> \<phi>. w \<Turnstile>\<^sub>n \<phi>[M]\<^sub>\<Sigma>\<^sub>2 \<and> (\<forall>\<psi>\<in>M. w \<Turnstile>\<^sub>n G\<^sub>n (F\<^sub>n \<psi>[N]\<^sub>\<Sigma>\<^sub>1)) \<and> (\<forall>\<psi>\<in>N. w \<Turnstile>\<^sub>n F\<^sub>n (G\<^sub>n \<psi>[M]\<^sub>\<Pi>\<^sub>1))
[PROOF STEP]
using \<G>\<F>_subformulas\<^sub>\<mu> \<F>\<G>_subformulas\<^sub>\<nu> \<G>\<F>_implies_GF \<F>\<G>_implies_FG
[PROOF STATE]
proof (prove)
using this:
w \<Turnstile>\<^sub>n \<phi>[\<G>\<F> \<phi> w]\<^sub>\<Sigma>\<^sub>2
\<G>\<F> ?\<phi> ?w \<subseteq> subformulas\<^sub>\<mu> ?\<phi>
\<F>\<G> ?\<phi> ?w \<subseteq> subformulas\<^sub>\<nu> ?\<phi>
\<forall>\<psi>\<in>\<G>\<F> ?\<phi> ?w. ?w \<Turnstile>\<^sub>n G\<^sub>n (F\<^sub>n \<psi>[\<F>\<G> ?\<phi> ?w]\<^sub>\<Sigma>\<^sub>1)
\<forall>\<psi>\<in>\<F>\<G> ?\<phi> ?w. ?w \<Turnstile>\<^sub>n F\<^sub>n (G\<^sub>n \<psi>[\<G>\<F> ?\<phi> ?w]\<^sub>\<Pi>\<^sub>1)

goal (1 subgoal):
 1. \<exists>M\<subseteq>subformulas\<^sub>\<mu> \<phi>. \<exists>N\<subseteq>subformulas\<^sub>\<nu> \<phi>. w \<Turnstile>\<^sub>n \<phi>[M]\<^sub>\<Sigma>\<^sub>2 \<and> (\<forall>\<psi>\<in>M. w \<Turnstile>\<^sub>n G\<^sub>n (F\<^sub>n \<psi>[N]\<^sub>\<Sigma>\<^sub>1)) \<and> (\<forall>\<psi>\<in>N. w \<Turnstile>\<^sub>n F\<^sub>n (G\<^sub>n \<psi>[M]\<^sub>\<Pi>\<^sub>1))
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
\<exists>M\<subseteq>subformulas\<^sub>\<mu> \<phi>. \<exists>N\<subseteq>subformulas\<^sub>\<nu> \<phi>. w \<Turnstile>\<^sub>n \<phi>[M]\<^sub>\<Sigma>\<^sub>2 \<and> (\<forall>\<psi>\<in>M. w \<Turnstile>\<^sub>n G\<^sub>n (F\<^sub>n \<psi>[N]\<^sub>\<Sigma>\<^sub>1)) \<and> (\<forall>\<psi>\<in>N. w \<Turnstile>\<^sub>n F\<^sub>n (G\<^sub>n \<psi>[M]\<^sub>\<Pi>\<^sub>1))

goal (1 subgoal):
 1. \<exists>M\<subseteq>subformulas\<^sub>\<mu> \<phi>. \<exists>N\<subseteq>subformulas\<^sub>\<nu> \<phi>. w \<Turnstile>\<^sub>n \<phi>[M]\<^sub>\<Sigma>\<^sub>2 \<and> (\<forall>\<psi>\<in>M. w \<Turnstile>\<^sub>n G\<^sub>n (F\<^sub>n \<psi>[N]\<^sub>\<Sigma>\<^sub>1)) \<and> (\<forall>\<psi>\<in>N. w \<Turnstile>\<^sub>n F\<^sub>n (G\<^sub>n \<psi>[M]\<^sub>\<Pi>\<^sub>1)) \<Longrightarrow> w \<Turnstile>\<^sub>n \<phi>
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>M\<subseteq>subformulas\<^sub>\<mu> \<phi>. \<exists>N\<subseteq>subformulas\<^sub>\<nu> \<phi>. w \<Turnstile>\<^sub>n \<phi>[M]\<^sub>\<Sigma>\<^sub>2 \<and> (\<forall>\<psi>\<in>M. w \<Turnstile>\<^sub>n G\<^sub>n (F\<^sub>n \<psi>[N]\<^sub>\<Sigma>\<^sub>1)) \<and> (\<forall>\<psi>\<in>N. w \<Turnstile>\<^sub>n F\<^sub>n (G\<^sub>n \<psi>[M]\<^sub>\<Pi>\<^sub>1)) \<Longrightarrow> w \<Turnstile>\<^sub>n \<phi>
[PROOF STEP]
assume ?rhs
[PROOF STATE]
proof (state)
this:
\<exists>M\<subseteq>subformulas\<^sub>\<mu> \<phi>. \<exists>N\<subseteq>subformulas\<^sub>\<nu> \<phi>. w \<Turnstile>\<^sub>n \<phi>[M]\<^sub>\<Sigma>\<^sub>2 \<and> (\<forall>\<psi>\<in>M. w \<Turnstile>\<^sub>n G\<^sub>n (F\<^sub>n \<psi>[N]\<^sub>\<Sigma>\<^sub>1)) \<and> (\<forall>\<psi>\<in>N. w \<Turnstile>\<^sub>n F\<^sub>n (G\<^sub>n \<psi>[M]\<^sub>\<Pi>\<^sub>1))

goal (1 subgoal):
 1. \<exists>M\<subseteq>subformulas\<^sub>\<mu> \<phi>. \<exists>N\<subseteq>subformulas\<^sub>\<nu> \<phi>. w \<Turnstile>\<^sub>n \<phi>[M]\<^sub>\<Sigma>\<^sub>2 \<and> (\<forall>\<psi>\<in>M. w \<Turnstile>\<^sub>n G\<^sub>n (F\<^sub>n \<psi>[N]\<^sub>\<Sigma>\<^sub>1)) \<and> (\<forall>\<psi>\<in>N. w \<Turnstile>\<^sub>n F\<^sub>n (G\<^sub>n \<psi>[M]\<^sub>\<Pi>\<^sub>1)) \<Longrightarrow> w \<Turnstile>\<^sub>n \<phi>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>M\<subseteq>subformulas\<^sub>\<mu> \<phi>. \<exists>N\<subseteq>subformulas\<^sub>\<nu> \<phi>. w \<Turnstile>\<^sub>n \<phi>[M]\<^sub>\<Sigma>\<^sub>2 \<and> (\<forall>\<psi>\<in>M. w \<Turnstile>\<^sub>n G\<^sub>n (F\<^sub>n \<psi>[N]\<^sub>\<Sigma>\<^sub>1)) \<and> (\<forall>\<psi>\<in>N. w \<Turnstile>\<^sub>n F\<^sub>n (G\<^sub>n \<psi>[M]\<^sub>\<Pi>\<^sub>1))
[PROOF STEP]
obtain M N where "w \<Turnstile>\<^sub>n \<phi>[M]\<^sub>\<Sigma>\<^sub>2" and "M \<subseteq> \<G>\<F> \<phi> w" and "N \<subseteq> \<F>\<G> \<phi> w"
[PROOF STATE]
proof (prove)
using this:
\<exists>M\<subseteq>subformulas\<^sub>\<mu> \<phi>. \<exists>N\<subseteq>subformulas\<^sub>\<nu> \<phi>. w \<Turnstile>\<^sub>n \<phi>[M]\<^sub>\<Sigma>\<^sub>2 \<and> (\<forall>\<psi>\<in>M. w \<Turnstile>\<^sub>n G\<^sub>n (F\<^sub>n \<psi>[N]\<^sub>\<Sigma>\<^sub>1)) \<and> (\<forall>\<psi>\<in>N. w \<Turnstile>\<^sub>n F\<^sub>n (G\<^sub>n \<psi>[M]\<^sub>\<Pi>\<^sub>1))

goal (1 subgoal):
 1. (\<And>M N. \<lbrakk>w \<Turnstile>\<^sub>n \<phi>[M]\<^sub>\<Sigma>\<^sub>2; M \<subseteq> \<G>\<F> \<phi> w; N \<subseteq> \<F>\<G> \<phi> w\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using X_\<G>\<F>_Y_\<F>\<G>
[PROOF STATE]
proof (prove)
using this:
\<exists>M\<subseteq>subformulas\<^sub>\<mu> \<phi>. \<exists>N\<subseteq>subformulas\<^sub>\<nu> \<phi>. w \<Turnstile>\<^sub>n \<phi>[M]\<^sub>\<Sigma>\<^sub>2 \<and> (\<forall>\<psi>\<in>M. w \<Turnstile>\<^sub>n G\<^sub>n (F\<^sub>n \<psi>[N]\<^sub>\<Sigma>\<^sub>1)) \<and> (\<forall>\<psi>\<in>N. w \<Turnstile>\<^sub>n F\<^sub>n (G\<^sub>n \<psi>[M]\<^sub>\<Pi>\<^sub>1))
\<lbrakk>?X \<subseteq> subformulas\<^sub>\<mu> ?\<phi>; ?Y \<subseteq> subformulas\<^sub>\<nu> ?\<phi>; \<forall>\<psi>\<in>?X. ?w \<Turnstile>\<^sub>n G\<^sub>n (F\<^sub>n \<psi>[?Y]\<^sub>\<Sigma>\<^sub>1); \<forall>\<psi>\<in>?Y. ?w \<Turnstile>\<^sub>n F\<^sub>n (G\<^sub>n \<psi>[?X]\<^sub>\<Pi>\<^sub>1)\<rbrakk> \<Longrightarrow> ?X \<subseteq> \<G>\<F> ?\<phi> ?w \<and> ?Y \<subseteq> \<F>\<G> ?\<phi> ?w

goal (1 subgoal):
 1. (\<And>M N. \<lbrakk>w \<Turnstile>\<^sub>n \<phi>[M]\<^sub>\<Sigma>\<^sub>2; M \<subseteq> \<G>\<F> \<phi> w; N \<subseteq> \<F>\<G> \<phi> w\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
w \<Turnstile>\<^sub>n \<phi>[M]\<^sub>\<Sigma>\<^sub>2
M \<subseteq> \<G>\<F> \<phi> w
N \<subseteq> \<F>\<G> \<phi> w

goal (1 subgoal):
 1. \<exists>M\<subseteq>subformulas\<^sub>\<mu> \<phi>. \<exists>N\<subseteq>subformulas\<^sub>\<nu> \<phi>. w \<Turnstile>\<^sub>n \<phi>[M]\<^sub>\<Sigma>\<^sub>2 \<and> (\<forall>\<psi>\<in>M. w \<Turnstile>\<^sub>n G\<^sub>n (F\<^sub>n \<psi>[N]\<^sub>\<Sigma>\<^sub>1)) \<and> (\<forall>\<psi>\<in>N. w \<Turnstile>\<^sub>n F\<^sub>n (G\<^sub>n \<psi>[M]\<^sub>\<Pi>\<^sub>1)) \<Longrightarrow> w \<Turnstile>\<^sub>n \<phi>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
w \<Turnstile>\<^sub>n \<phi>[M]\<^sub>\<Sigma>\<^sub>2
M \<subseteq> \<G>\<F> \<phi> w
N \<subseteq> \<F>\<G> \<phi> w
[PROOF STEP]
have "w \<Turnstile>\<^sub>n \<phi>[\<G>\<F> \<phi> w]\<^sub>\<Sigma>\<^sub>2"
[PROOF STATE]
proof (prove)
using this:
w \<Turnstile>\<^sub>n \<phi>[M]\<^sub>\<Sigma>\<^sub>2
M \<subseteq> \<G>\<F> \<phi> w
N \<subseteq> \<F>\<G> \<phi> w

goal (1 subgoal):
 1. w \<Turnstile>\<^sub>n \<phi>[\<G>\<F> \<phi> w]\<^sub>\<Sigma>\<^sub>2
[PROOF STEP]
using flatten_sigma_2_monotone
[PROOF STATE]
proof (prove)
using this:
w \<Turnstile>\<^sub>n \<phi>[M]\<^sub>\<Sigma>\<^sub>2
M \<subseteq> \<G>\<F> \<phi> w
N \<subseteq> \<F>\<G> \<phi> w
\<lbrakk>?w \<Turnstile>\<^sub>n ?\<phi>[?M]\<^sub>\<Sigma>\<^sub>2; ?M \<subseteq> ?M'\<rbrakk> \<Longrightarrow> ?w \<Turnstile>\<^sub>n ?\<phi>[?M']\<^sub>\<Sigma>\<^sub>2

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

goal (1 subgoal):
 1. \<exists>M\<subseteq>subformulas\<^sub>\<mu> \<phi>. \<exists>N\<subseteq>subformulas\<^sub>\<nu> \<phi>. w \<Turnstile>\<^sub>n \<phi>[M]\<^sub>\<Sigma>\<^sub>2 \<and> (\<forall>\<psi>\<in>M. w \<Turnstile>\<^sub>n G\<^sub>n (F\<^sub>n \<psi>[N]\<^sub>\<Sigma>\<^sub>1)) \<and> (\<forall>\<psi>\<in>N. w \<Turnstile>\<^sub>n F\<^sub>n (G\<^sub>n \<psi>[M]\<^sub>\<Pi>\<^sub>1)) \<Longrightarrow> w \<Turnstile>\<^sub>n \<phi>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
w \<Turnstile>\<^sub>n \<phi>[\<G>\<F> \<phi> w]\<^sub>\<Sigma>\<^sub>2
[PROOF STEP]
show ?lhs
[PROOF STATE]
proof (prove)
using this:
w \<Turnstile>\<^sub>n \<phi>[\<G>\<F> \<phi> w]\<^sub>\<Sigma>\<^sub>2

goal (1 subgoal):
 1. w \<Turnstile>\<^sub>n \<phi>
[PROOF STEP]
using flatten_sigma_2_correct
[PROOF STATE]
proof (prove)
using this:
w \<Turnstile>\<^sub>n \<phi>[\<G>\<F> \<phi> w]\<^sub>\<Sigma>\<^sub>2
?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 \<phi>
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
w \<Turnstile>\<^sub>n \<phi>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem normal_form_with_flatten_pi_2:
  "w \<Turnstile>\<^sub>n \<phi> \<longleftrightarrow>
    (\<exists>M \<subseteq> subformulas\<^sub>\<mu> \<phi>. \<exists>N \<subseteq> subformulas\<^sub>\<nu> \<phi>.
      w \<Turnstile>\<^sub>n \<phi>[N]\<^sub>\<Pi>\<^sub>2 \<and> (\<forall>\<psi> \<in> M. w \<Turnstile>\<^sub>n G\<^sub>n (F\<^sub>n \<psi>[N]\<^sub>\<Sigma>\<^sub>1)) \<and> (\<forall>\<psi> \<in> N. w \<Turnstile>\<^sub>n F\<^sub>n (G\<^sub>n \<psi>[M]\<^sub>\<Pi>\<^sub>1)))" (is "?lhs \<longleftrightarrow> ?rhs")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. w \<Turnstile>\<^sub>n \<phi> = (\<exists>M\<subseteq>subformulas\<^sub>\<mu> \<phi>. \<exists>N\<subseteq>subformulas\<^sub>\<nu> \<phi>. w \<Turnstile>\<^sub>n \<phi>[N]\<^sub>\<Pi>\<^sub>2 \<and> (\<forall>\<psi>\<in>M. w \<Turnstile>\<^sub>n G\<^sub>n (F\<^sub>n \<psi>[N]\<^sub>\<Sigma>\<^sub>1)) \<and> (\<forall>\<psi>\<in>N. w \<Turnstile>\<^sub>n F\<^sub>n (G\<^sub>n \<psi>[M]\<^sub>\<Pi>\<^sub>1)))
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. w \<Turnstile>\<^sub>n \<phi> \<Longrightarrow> \<exists>M\<subseteq>subformulas\<^sub>\<mu> \<phi>. \<exists>N\<subseteq>subformulas\<^sub>\<nu> \<phi>. w \<Turnstile>\<^sub>n \<phi>[N]\<^sub>\<Pi>\<^sub>2 \<and> (\<forall>\<psi>\<in>M. w \<Turnstile>\<^sub>n G\<^sub>n (F\<^sub>n \<psi>[N]\<^sub>\<Sigma>\<^sub>1)) \<and> (\<forall>\<psi>\<in>N. w \<Turnstile>\<^sub>n F\<^sub>n (G\<^sub>n \<psi>[M]\<^sub>\<Pi>\<^sub>1))
 2. \<exists>M\<subseteq>subformulas\<^sub>\<mu> \<phi>. \<exists>N\<subseteq>subformulas\<^sub>\<nu> \<phi>. w \<Turnstile>\<^sub>n \<phi>[N]\<^sub>\<Pi>\<^sub>2 \<and> (\<forall>\<psi>\<in>M. w \<Turnstile>\<^sub>n G\<^sub>n (F\<^sub>n \<psi>[N]\<^sub>\<Sigma>\<^sub>1)) \<and> (\<forall>\<psi>\<in>N. w \<Turnstile>\<^sub>n F\<^sub>n (G\<^sub>n \<psi>[M]\<^sub>\<Pi>\<^sub>1)) \<Longrightarrow> w \<Turnstile>\<^sub>n \<phi>
[PROOF STEP]
assume ?lhs
[PROOF STATE]
proof (state)
this:
w \<Turnstile>\<^sub>n \<phi>

goal (2 subgoals):
 1. w \<Turnstile>\<^sub>n \<phi> \<Longrightarrow> \<exists>M\<subseteq>subformulas\<^sub>\<mu> \<phi>. \<exists>N\<subseteq>subformulas\<^sub>\<nu> \<phi>. w \<Turnstile>\<^sub>n \<phi>[N]\<^sub>\<Pi>\<^sub>2 \<and> (\<forall>\<psi>\<in>M. w \<Turnstile>\<^sub>n G\<^sub>n (F\<^sub>n \<psi>[N]\<^sub>\<Sigma>\<^sub>1)) \<and> (\<forall>\<psi>\<in>N. w \<Turnstile>\<^sub>n F\<^sub>n (G\<^sub>n \<psi>[M]\<^sub>\<Pi>\<^sub>1))
 2. \<exists>M\<subseteq>subformulas\<^sub>\<mu> \<phi>. \<exists>N\<subseteq>subformulas\<^sub>\<nu> \<phi>. w \<Turnstile>\<^sub>n \<phi>[N]\<^sub>\<Pi>\<^sub>2 \<and> (\<forall>\<psi>\<in>M. w \<Turnstile>\<^sub>n G\<^sub>n (F\<^sub>n \<psi>[N]\<^sub>\<Sigma>\<^sub>1)) \<and> (\<forall>\<psi>\<in>N. w \<Turnstile>\<^sub>n F\<^sub>n (G\<^sub>n \<psi>[M]\<^sub>\<Pi>\<^sub>1)) \<Longrightarrow> w \<Turnstile>\<^sub>n \<phi>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
w \<Turnstile>\<^sub>n \<phi>
[PROOF STEP]
have "w \<Turnstile>\<^sub>n \<phi>[\<F>\<G> \<phi> w]\<^sub>\<Pi>\<^sub>2"
[PROOF STATE]
proof (prove)
using this:
w \<Turnstile>\<^sub>n \<phi>

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

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

goal (2 subgoals):
 1. w \<Turnstile>\<^sub>n \<phi> \<Longrightarrow> \<exists>M\<subseteq>subformulas\<^sub>\<mu> \<phi>. \<exists>N\<subseteq>subformulas\<^sub>\<nu> \<phi>. w \<Turnstile>\<^sub>n \<phi>[N]\<^sub>\<Pi>\<^sub>2 \<and> (\<forall>\<psi>\<in>M. w \<Turnstile>\<^sub>n G\<^sub>n (F\<^sub>n \<psi>[N]\<^sub>\<Sigma>\<^sub>1)) \<and> (\<forall>\<psi>\<in>N. w \<Turnstile>\<^sub>n F\<^sub>n (G\<^sub>n \<psi>[M]\<^sub>\<Pi>\<^sub>1))
 2. \<exists>M\<subseteq>subformulas\<^sub>\<mu> \<phi>. \<exists>N\<subseteq>subformulas\<^sub>\<nu> \<phi>. w \<Turnstile>\<^sub>n \<phi>[N]\<^sub>\<Pi>\<^sub>2 \<and> (\<forall>\<psi>\<in>M. w \<Turnstile>\<^sub>n G\<^sub>n (F\<^sub>n \<psi>[N]\<^sub>\<Sigma>\<^sub>1)) \<and> (\<forall>\<psi>\<in>N. w \<Turnstile>\<^sub>n F\<^sub>n (G\<^sub>n \<psi>[M]\<^sub>\<Pi>\<^sub>1)) \<Longrightarrow> w \<Turnstile>\<^sub>n \<phi>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
w \<Turnstile>\<^sub>n \<phi>[\<F>\<G> \<phi> w]\<^sub>\<Pi>\<^sub>2
[PROOF STEP]
show ?rhs
[PROOF STATE]
proof (prove)
using this:
w \<Turnstile>\<^sub>n \<phi>[\<F>\<G> \<phi> w]\<^sub>\<Pi>\<^sub>2

goal (1 subgoal):
 1. \<exists>M\<subseteq>subformulas\<^sub>\<mu> \<phi>. \<exists>N\<subseteq>subformulas\<^sub>\<nu> \<phi>. w \<Turnstile>\<^sub>n \<phi>[N]\<^sub>\<Pi>\<^sub>2 \<and> (\<forall>\<psi>\<in>M. w \<Turnstile>\<^sub>n G\<^sub>n (F\<^sub>n \<psi>[N]\<^sub>\<Sigma>\<^sub>1)) \<and> (\<forall>\<psi>\<in>N. w \<Turnstile>\<^sub>n F\<^sub>n (G\<^sub>n \<psi>[M]\<^sub>\<Pi>\<^sub>1))
[PROOF STEP]
using \<G>\<F>_subformulas\<^sub>\<mu> \<F>\<G>_subformulas\<^sub>\<nu> \<G>\<F>_implies_GF \<F>\<G>_implies_FG
[PROOF STATE]
proof (prove)
using this:
w \<Turnstile>\<^sub>n \<phi>[\<F>\<G> \<phi> w]\<^sub>\<Pi>\<^sub>2
\<G>\<F> ?\<phi> ?w \<subseteq> subformulas\<^sub>\<mu> ?\<phi>
\<F>\<G> ?\<phi> ?w \<subseteq> subformulas\<^sub>\<nu> ?\<phi>
\<forall>\<psi>\<in>\<G>\<F> ?\<phi> ?w. ?w \<Turnstile>\<^sub>n G\<^sub>n (F\<^sub>n \<psi>[\<F>\<G> ?\<phi> ?w]\<^sub>\<Sigma>\<^sub>1)
\<forall>\<psi>\<in>\<F>\<G> ?\<phi> ?w. ?w \<Turnstile>\<^sub>n F\<^sub>n (G\<^sub>n \<psi>[\<G>\<F> ?\<phi> ?w]\<^sub>\<Pi>\<^sub>1)

goal (1 subgoal):
 1. \<exists>M\<subseteq>subformulas\<^sub>\<mu> \<phi>. \<exists>N\<subseteq>subformulas\<^sub>\<nu> \<phi>. w \<Turnstile>\<^sub>n \<phi>[N]\<^sub>\<Pi>\<^sub>2 \<and> (\<forall>\<psi>\<in>M. w \<Turnstile>\<^sub>n G\<^sub>n (F\<^sub>n \<psi>[N]\<^sub>\<Sigma>\<^sub>1)) \<and> (\<forall>\<psi>\<in>N. w \<Turnstile>\<^sub>n F\<^sub>n (G\<^sub>n \<psi>[M]\<^sub>\<Pi>\<^sub>1))
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
\<exists>M\<subseteq>subformulas\<^sub>\<mu> \<phi>. \<exists>N\<subseteq>subformulas\<^sub>\<nu> \<phi>. w \<Turnstile>\<^sub>n \<phi>[N]\<^sub>\<Pi>\<^sub>2 \<and> (\<forall>\<psi>\<in>M. w \<Turnstile>\<^sub>n G\<^sub>n (F\<^sub>n \<psi>[N]\<^sub>\<Sigma>\<^sub>1)) \<and> (\<forall>\<psi>\<in>N. w \<Turnstile>\<^sub>n F\<^sub>n (G\<^sub>n \<psi>[M]\<^sub>\<Pi>\<^sub>1))

goal (1 subgoal):
 1. \<exists>M\<subseteq>subformulas\<^sub>\<mu> \<phi>. \<exists>N\<subseteq>subformulas\<^sub>\<nu> \<phi>. w \<Turnstile>\<^sub>n \<phi>[N]\<^sub>\<Pi>\<^sub>2 \<and> (\<forall>\<psi>\<in>M. w \<Turnstile>\<^sub>n G\<^sub>n (F\<^sub>n \<psi>[N]\<^sub>\<Sigma>\<^sub>1)) \<and> (\<forall>\<psi>\<in>N. w \<Turnstile>\<^sub>n F\<^sub>n (G\<^sub>n \<psi>[M]\<^sub>\<Pi>\<^sub>1)) \<Longrightarrow> w \<Turnstile>\<^sub>n \<phi>
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>M\<subseteq>subformulas\<^sub>\<mu> \<phi>. \<exists>N\<subseteq>subformulas\<^sub>\<nu> \<phi>. w \<Turnstile>\<^sub>n \<phi>[N]\<^sub>\<Pi>\<^sub>2 \<and> (\<forall>\<psi>\<in>M. w \<Turnstile>\<^sub>n G\<^sub>n (F\<^sub>n \<psi>[N]\<^sub>\<Sigma>\<^sub>1)) \<and> (\<forall>\<psi>\<in>N. w \<Turnstile>\<^sub>n F\<^sub>n (G\<^sub>n \<psi>[M]\<^sub>\<Pi>\<^sub>1)) \<Longrightarrow> w \<Turnstile>\<^sub>n \<phi>
[PROOF STEP]
assume ?rhs
[PROOF STATE]
proof (state)
this:
\<exists>M\<subseteq>subformulas\<^sub>\<mu> \<phi>. \<exists>N\<subseteq>subformulas\<^sub>\<nu> \<phi>. w \<Turnstile>\<^sub>n \<phi>[N]\<^sub>\<Pi>\<^sub>2 \<and> (\<forall>\<psi>\<in>M. w \<Turnstile>\<^sub>n G\<^sub>n (F\<^sub>n \<psi>[N]\<^sub>\<Sigma>\<^sub>1)) \<and> (\<forall>\<psi>\<in>N. w \<Turnstile>\<^sub>n F\<^sub>n (G\<^sub>n \<psi>[M]\<^sub>\<Pi>\<^sub>1))

goal (1 subgoal):
 1. \<exists>M\<subseteq>subformulas\<^sub>\<mu> \<phi>. \<exists>N\<subseteq>subformulas\<^sub>\<nu> \<phi>. w \<Turnstile>\<^sub>n \<phi>[N]\<^sub>\<Pi>\<^sub>2 \<and> (\<forall>\<psi>\<in>M. w \<Turnstile>\<^sub>n G\<^sub>n (F\<^sub>n \<psi>[N]\<^sub>\<Sigma>\<^sub>1)) \<and> (\<forall>\<psi>\<in>N. w \<Turnstile>\<^sub>n F\<^sub>n (G\<^sub>n \<psi>[M]\<^sub>\<Pi>\<^sub>1)) \<Longrightarrow> w \<Turnstile>\<^sub>n \<phi>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>M\<subseteq>subformulas\<^sub>\<mu> \<phi>. \<exists>N\<subseteq>subformulas\<^sub>\<nu> \<phi>. w \<Turnstile>\<^sub>n \<phi>[N]\<^sub>\<Pi>\<^sub>2 \<and> (\<forall>\<psi>\<in>M. w \<Turnstile>\<^sub>n G\<^sub>n (F\<^sub>n \<psi>[N]\<^sub>\<Sigma>\<^sub>1)) \<and> (\<forall>\<psi>\<in>N. w \<Turnstile>\<^sub>n F\<^sub>n (G\<^sub>n \<psi>[M]\<^sub>\<Pi>\<^sub>1))
[PROOF STEP]
obtain M N where "w \<Turnstile>\<^sub>n \<phi>[N]\<^sub>\<Pi>\<^sub>2" and "M \<subseteq> \<G>\<F> \<phi> w" and "N \<subseteq> \<F>\<G> \<phi> w"
[PROOF STATE]
proof (prove)
using this:
\<exists>M\<subseteq>subformulas\<^sub>\<mu> \<phi>. \<exists>N\<subseteq>subformulas\<^sub>\<nu> \<phi>. w \<Turnstile>\<^sub>n \<phi>[N]\<^sub>\<Pi>\<^sub>2 \<and> (\<forall>\<psi>\<in>M. w \<Turnstile>\<^sub>n G\<^sub>n (F\<^sub>n \<psi>[N]\<^sub>\<Sigma>\<^sub>1)) \<and> (\<forall>\<psi>\<in>N. w \<Turnstile>\<^sub>n F\<^sub>n (G\<^sub>n \<psi>[M]\<^sub>\<Pi>\<^sub>1))

goal (1 subgoal):
 1. (\<And>N M. \<lbrakk>w \<Turnstile>\<^sub>n \<phi>[N]\<^sub>\<Pi>\<^sub>2; M \<subseteq> \<G>\<F> \<phi> w; N \<subseteq> \<F>\<G> \<phi> w\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using X_\<G>\<F>_Y_\<F>\<G>
[PROOF STATE]
proof (prove)
using this:
\<exists>M\<subseteq>subformulas\<^sub>\<mu> \<phi>. \<exists>N\<subseteq>subformulas\<^sub>\<nu> \<phi>. w \<Turnstile>\<^sub>n \<phi>[N]\<^sub>\<Pi>\<^sub>2 \<and> (\<forall>\<psi>\<in>M. w \<Turnstile>\<^sub>n G\<^sub>n (F\<^sub>n \<psi>[N]\<^sub>\<Sigma>\<^sub>1)) \<and> (\<forall>\<psi>\<in>N. w \<Turnstile>\<^sub>n F\<^sub>n (G\<^sub>n \<psi>[M]\<^sub>\<Pi>\<^sub>1))
\<lbrakk>?X \<subseteq> subformulas\<^sub>\<mu> ?\<phi>; ?Y \<subseteq> subformulas\<^sub>\<nu> ?\<phi>; \<forall>\<psi>\<in>?X. ?w \<Turnstile>\<^sub>n G\<^sub>n (F\<^sub>n \<psi>[?Y]\<^sub>\<Sigma>\<^sub>1); \<forall>\<psi>\<in>?Y. ?w \<Turnstile>\<^sub>n F\<^sub>n (G\<^sub>n \<psi>[?X]\<^sub>\<Pi>\<^sub>1)\<rbrakk> \<Longrightarrow> ?X \<subseteq> \<G>\<F> ?\<phi> ?w \<and> ?Y \<subseteq> \<F>\<G> ?\<phi> ?w

goal (1 subgoal):
 1. (\<And>N M. \<lbrakk>w \<Turnstile>\<^sub>n \<phi>[N]\<^sub>\<Pi>\<^sub>2; M \<subseteq> \<G>\<F> \<phi> w; N \<subseteq> \<F>\<G> \<phi> w\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
w \<Turnstile>\<^sub>n \<phi>[N]\<^sub>\<Pi>\<^sub>2
M \<subseteq> \<G>\<F> \<phi> w
N \<subseteq> \<F>\<G> \<phi> w

goal (1 subgoal):
 1. \<exists>M\<subseteq>subformulas\<^sub>\<mu> \<phi>. \<exists>N\<subseteq>subformulas\<^sub>\<nu> \<phi>. w \<Turnstile>\<^sub>n \<phi>[N]\<^sub>\<Pi>\<^sub>2 \<and> (\<forall>\<psi>\<in>M. w \<Turnstile>\<^sub>n G\<^sub>n (F\<^sub>n \<psi>[N]\<^sub>\<Sigma>\<^sub>1)) \<and> (\<forall>\<psi>\<in>N. w \<Turnstile>\<^sub>n F\<^sub>n (G\<^sub>n \<psi>[M]\<^sub>\<Pi>\<^sub>1)) \<Longrightarrow> w \<Turnstile>\<^sub>n \<phi>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
w \<Turnstile>\<^sub>n \<phi>[N]\<^sub>\<Pi>\<^sub>2
M \<subseteq> \<G>\<F> \<phi> w
N \<subseteq> \<F>\<G> \<phi> w
[PROOF STEP]
have "w \<Turnstile>\<^sub>n \<phi>[\<F>\<G> \<phi> w]\<^sub>\<Pi>\<^sub>2"
[PROOF STATE]
proof (prove)
using this:
w \<Turnstile>\<^sub>n \<phi>[N]\<^sub>\<Pi>\<^sub>2
M \<subseteq> \<G>\<F> \<phi> w
N \<subseteq> \<F>\<G> \<phi> w

goal (1 subgoal):
 1. w \<Turnstile>\<^sub>n \<phi>[\<F>\<G> \<phi> w]\<^sub>\<Pi>\<^sub>2
[PROOF STEP]
using flatten_pi_2_monotone
[PROOF STATE]
proof (prove)
using this:
w \<Turnstile>\<^sub>n \<phi>[N]\<^sub>\<Pi>\<^sub>2
M \<subseteq> \<G>\<F> \<phi> w
N \<subseteq> \<F>\<G> \<phi> w
\<lbrakk>?w \<Turnstile>\<^sub>n ?\<phi>[?N]\<^sub>\<Pi>\<^sub>2; ?N \<subseteq> ?N'\<rbrakk> \<Longrightarrow> ?w \<Turnstile>\<^sub>n ?\<phi>[?N']\<^sub>\<Pi>\<^sub>2

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

goal (1 subgoal):
 1. \<exists>M\<subseteq>subformulas\<^sub>\<mu> \<phi>. \<exists>N\<subseteq>subformulas\<^sub>\<nu> \<phi>. w \<Turnstile>\<^sub>n \<phi>[N]\<^sub>\<Pi>\<^sub>2 \<and> (\<forall>\<psi>\<in>M. w \<Turnstile>\<^sub>n G\<^sub>n (F\<^sub>n \<psi>[N]\<^sub>\<Sigma>\<^sub>1)) \<and> (\<forall>\<psi>\<in>N. w \<Turnstile>\<^sub>n F\<^sub>n (G\<^sub>n \<psi>[M]\<^sub>\<Pi>\<^sub>1)) \<Longrightarrow> w \<Turnstile>\<^sub>n \<phi>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
w \<Turnstile>\<^sub>n \<phi>[\<F>\<G> \<phi> w]\<^sub>\<Pi>\<^sub>2
[PROOF STEP]
show ?lhs
[PROOF STATE]
proof (prove)
using this:
w \<Turnstile>\<^sub>n \<phi>[\<F>\<G> \<phi> w]\<^sub>\<Pi>\<^sub>2

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

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma m1_obs_id [simp]: "obs m1 = id"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. obs m1 = id
[PROOF STEP]
by (simp add: m1_def)


[STATEMENT]
lemma PO_m1_inv0_fin_init [iff]:
  "init m1 \<subseteq> m1_inv0_fin"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. init m1 \<subseteq> m1_inv0_fin
[PROOF STEP]
by (auto simp add: m1_defs intro!: m1_inv0_finI)


[STATEMENT]
lemma PO_m1_inv0_fin [iff]: "reach m1 \<subseteq> m1_inv0_fin"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. reach m1 \<subseteq> m1_inv0_fin
[PROOF STEP]
by (rule inv_rule_incr, auto del: subsetI)


[STATEMENT]
lemma PO_m1_step1_refines_m1a_step1:
  "{R1a1}
     (m1a_step1 Ra A B), (m1_step1 Ra A B)
   {> R1a1}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {R1a1} m1a_step1 Ra A B, m1_step1 Ra A B {> R1a1}
[PROOF STEP]
by (auto simp add: PO_rhoare_defs R1a1_defs m1_defs)


[STATEMENT]
lemma PO_m1_step2_refines_m1a_step2:
  "{R1a1}
     (m1a_step2 Rb A B), (m1_step2 Rb A B)
   {> R1a1}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {R1a1} m1a_step2 Rb A B, m1_step2 Rb A B {> R1a1}
[PROOF STEP]
by (auto simp add: PO_rhoare_defs R1a1_defs m1_defs)


[STATEMENT]
lemma PO_m1_step3_refines_m1a_step3:
  "{R1a1}
     (m1a_step3 Rs A B Kab [aNum Ts]), (m1_step3 Rs A B Kab Ts)
   {> R1a1}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {R1a1} m1a_step3 Rs A B Kab [aNum Ts], m1_step3 Rs A B Kab Ts {> R1a1}
[PROOF STEP]
by (auto simp add: PO_rhoare_defs R1a1_defs m1_defs)


[STATEMENT]
lemma PO_m1_step4_refines_m1a_step4:
  "{R1a1}
     (m1a_step4 Ra A B Kab [aNum Ts]), (m1_step4 Ra A B Kab Ts)
   {> R1a1}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {R1a1} m1a_step4 Ra A B Kab [aNum Ts], m1_step4 Ra A B Kab Ts {> R1a1}
[PROOF STEP]
by (auto simp add: PO_rhoare_defs R1a1_defs m1_defs)


[STATEMENT]
lemma PO_m1_step5_refines_m1a_step5:
  "{R1a1}
     (m1a_step5 Rb A B Kab [aNum Ts]), (m1_step5 Rb A B Kab Ts)
   {> R1a1}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {R1a1} m1a_step5 Rb A B Kab [aNum Ts], m1_step5 Rb A B Kab Ts {> R1a1}
[PROOF STEP]
by (auto simp add: PO_rhoare_defs R1a1_defs m1_defs)


[STATEMENT]
lemma PO_m1_leak_refines_m1a_leak:
  "{R1a1}
     (m1a_leak Rs), (m1_leak Rs)
   {> R1a1}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {R1a1} m1a_leak Rs, m1_leak Rs {> R1a1}
[PROOF STEP]
by (auto simp add: PO_rhoare_defs R1a1_defs m1_defs)


[STATEMENT]
lemma PO_m1_tick_refines_m1a_skip:
  "{R1a1}
     Id, (m1_tick T)
   {> R1a1}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {R1a1} Id, m1_tick T {> R1a1}
[PROOF STEP]
by (auto simp add: PO_rhoare_defs R1a1_defs m1_defs)


[STATEMENT]
lemma PO_m1_refines_init_m1a [iff]:
  "init m1 \<subseteq>  R1a1``(init m1a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. init m1 \<subseteq> R1a1 `` init m1a
[PROOF STEP]
by (auto simp add: R1a1_defs m1_defs intro!: s0g_secrecyI)


[STATEMENT]
lemma PO_m1_refines_trans_m1a [iff]:
  "{R1a1}
     (trans m1a), (trans m1)
   {> R1a1}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {R1a1} TS.trans m1a, TS.trans m1 {> R1a1}
[PROOF STEP]
apply (auto simp add: m1_def m1_trans_def m1a_def m1a_trans_def
         intro!: PO_m1_trans_refines_m1a_trans)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x xa xb. {R1a1} (\<Union>x xa xb xc xd. (\<Union>xe. m1a_step1 xb x xa \<union> m1a_step2 xc x xa \<union> \<Union> (range (m1a_step3 xd x xa xe)) \<union> \<Union> (range (m1a_step4 xb x xa xe)) \<union> \<Union> (range (m1a_step5 xc x xa xe))) \<union> m1a_leak xd)\<^sup>=, m1_step1 xb x xa {> R1a1}
 2. \<And>x xa xc. {R1a1} (\<Union>x xa xb xc xd. (\<Union>xe. m1a_step1 xb x xa \<union> m1a_step2 xc x xa \<union> \<Union> (range (m1a_step3 xd x xa xe)) \<union> \<Union> (range (m1a_step4 xb x xa xe)) \<union> \<Union> (range (m1a_step5 xc x xa xe))) \<union> m1a_leak xd)\<^sup>=, m1_step2 xc x xa {> R1a1}
 3. \<And>x xa xd xe xf. {R1a1} (\<Union>x xa xb xc xd. (\<Union>xe. m1a_step1 xb x xa \<union> m1a_step2 xc x xa \<union> \<Union> (range (m1a_step3 xd x xa xe)) \<union> \<Union> (range (m1a_step4 xb x xa xe)) \<union> \<Union> (range (m1a_step5 xc x xa xe))) \<union> m1a_leak xd)\<^sup>=, m1_step3 xd x xa xe xf {> R1a1}
[PROOF STEP]
apply (force intro!: PO_m1_trans_refines_m1a_trans)+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma obs_consistent_med1a1 [iff]:
  "obs_consistent R1a1 med1a1 m1a m1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. obs_consistent R1a1 med1a1 m1a m1
[PROOF STEP]
by (auto simp add: obs_consistent_def R1a1_def m1a_def m1_def)


[STATEMENT]
lemma PO_m1_refines_m1a [iff]:
  "refines R1a1 med1a1 m1a m1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. refines R1a1 med1a1 m1a m1
[PROOF STEP]
by (rule Refinement_basic) (auto del: subsetI)


[STATEMENT]
lemma  m1_implements_m1: "implements med1a1 m1a m1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. implements med1a1 m1a m1
[PROOF STEP]
by (rule refinement_soundness) (fast)


[STATEMENT]
lemma getIJProperties:
  assumes "card V \<ge> 2"
  assumes "(I, J) = getIJ Q_pos Q_neg V"
  shows "card I \<ge> 1" and "card J \<ge> 1" and "card I < card V" and "card J < card V"
    and "V = I \<union> J" and "I \<inter> J = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (1 \<le> card I &&& 1 \<le> card J &&& card I < card V) &&& card J < card V &&& V = I \<union> J &&& I \<inter> J = {}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (6 subgoals):
 1. 1 \<le> card I
 2. 1 \<le> card J
 3. card I < card V
 4. card J < card V
 5. V = I \<union> J
 6. I \<inter> J = {}
[PROOF STEP]
show "1 \<le> card I"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 \<le> card I
[PROOF STEP]
using coreProperties[of V Q_pos Q_neg I J] assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>2 \<le> card V; getIJ Q_pos Q_neg V = (I, J)\<rbrakk> \<Longrightarrow> 1 \<le> card I \<and> 1 \<le> card J \<and> V = I \<union> J \<and> I \<inter> J = {}
2 \<le> card V
(I, J) = getIJ Q_pos Q_neg V

goal (1 subgoal):
 1. 1 \<le> card I
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
1 \<le> card I

goal (5 subgoals):
 1. 1 \<le> card J
 2. card I < card V
 3. card J < card V
 4. V = I \<union> J
 5. I \<inter> J = {}
[PROOF STEP]
show "1 \<le> card J"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 \<le> card J
[PROOF STEP]
using coreProperties[of V Q_pos Q_neg I J] assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>2 \<le> card V; getIJ Q_pos Q_neg V = (I, J)\<rbrakk> \<Longrightarrow> 1 \<le> card I \<and> 1 \<le> card J \<and> V = I \<union> J \<and> I \<inter> J = {}
2 \<le> card V
(I, J) = getIJ Q_pos Q_neg V

goal (1 subgoal):
 1. 1 \<le> card J
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
1 \<le> card J

goal (4 subgoals):
 1. card I < card V
 2. card J < card V
 3. V = I \<union> J
 4. I \<inter> J = {}
[PROOF STEP]
show "card I < card V"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card I < card V
[PROOF STEP]
by (metis (no_types, lifting) Int_ac(3) One_nat_def Suc_le_lessD assms(1)
        assms(2) card_gt_0_iff card_seteq dual_order.trans getIJ.coreProperties getIJ_axioms leI
        le_iff_inf one_le_numeral sup_ge1 sup_ge2)
[PROOF STATE]
proof (state)
this:
card I < card V

goal (3 subgoals):
 1. card J < card V
 2. V = I \<union> J
 3. I \<inter> J = {}
[PROOF STEP]
show "card J < card V"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card J < card V
[PROOF STEP]
by (metis One_nat_def Suc_1 assms(1) assms(2) card_gt_0_iff card_seteq
        getIJ.coreProperties getIJ_axioms leI le_0_eq le_iff_inf nat.simps(3) sup_ge1 sup_ge2)
[PROOF STATE]
proof (state)
this:
card J < card V

goal (2 subgoals):
 1. V = I \<union> J
 2. I \<inter> J = {}
[PROOF STEP]
show "V = I \<union> J"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. V = I \<union> J
[PROOF STEP]
by (metis assms(1) assms(2) getIJ.coreProperties getIJ_axioms)
[PROOF STATE]
proof (state)
this:
V = I \<union> J

goal (1 subgoal):
 1. I \<inter> J = {}
[PROOF STEP]
show "I \<inter> J = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. I \<inter> J = {}
[PROOF STEP]
by (metis assms(1) assms(2) getIJ_axioms getIJ_def)
[PROOF STATE]
proof (state)
this:
I \<inter> J = {}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma arg_max_list_element:
  assumes "length l \<ge> 1" shows "arg_max_list f l \<in> set l"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. arg_max_list f l \<in> set l
[PROOF STEP]
by (metis One_nat_def arg_max_list.simps arg_min_list_in assms le_imp_less_Suc less_irrefl list.size(3))