[STATEMENT]
lemma passes_test_suite_completeness :
  assumes "implies_completeness T M m"
  and     "observable M"
  and     "observable M'"
  and     "inputs M' = inputs M"
  and     "inputs M \<noteq> {}"
  and     "completely_specified M"
  and     "completely_specified M'"
  and     "size M' \<le> m"
shows     "(L M' \<subseteq> L M) \<longleftrightarrow> passes_test_suite M T M'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (L M' \<subseteq> L M) = passes_test_suite M T M'
[PROOF STEP]
using passes_test_suite_exhaustiveness[OF _ _ assms(2-8)]
        passes_test_suite_soundness[OF _ assms(2,3,4,6)]
        assms(1)
        test_suite.exhaust[of T]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>passes_test_suite M (Test_Suite ?prs ?tps ?rd_targets ?separators) M'; implies_completeness (Test_Suite ?prs ?tps ?rd_targets ?separators) M m\<rbrakk> \<Longrightarrow> L M' \<subseteq> L M
\<lbrakk>implies_completeness (Test_Suite ?prs ?tps ?rd_targets ?separators) M ?m; L M' \<subseteq> L M\<rbrakk> \<Longrightarrow> passes_test_suite M (Test_Suite ?prs ?tps ?rd_targets ?separators) M'
implies_completeness T M m
(\<And>x1 x2 x3 x4. T = Test_Suite x1 x2 x3 x4 \<Longrightarrow> ?P) \<Longrightarrow> ?P

goal (1 subgoal):
 1. (L M' \<subseteq> L M) = passes_test_suite M T M'
[PROOF STEP]
by metis


[STATEMENT]
lemma ltln_strong_weak_2:
  "w \<Turnstile>\<^sub>n \<phi> U\<^sub>n \<psi> \<longleftrightarrow> w \<Turnstile>\<^sub>n (\<phi> and\<^sub>n F\<^sub>n \<psi>) W\<^sub>n \<psi>" (is "?thesis1")
  "w \<Turnstile>\<^sub>n \<phi> M\<^sub>n \<psi> \<longleftrightarrow> w \<Turnstile>\<^sub>n \<phi> R\<^sub>n (\<psi> and\<^sub>n F\<^sub>n \<phi>)" (is "?thesis2")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. w \<Turnstile>\<^sub>n \<phi> U\<^sub>n \<psi> = w \<Turnstile>\<^sub>n (\<phi> and\<^sub>n F\<^sub>n \<psi>) W\<^sub>n \<psi> &&& w \<Turnstile>\<^sub>n \<phi> M\<^sub>n \<psi> = w \<Turnstile>\<^sub>n \<phi> R\<^sub>n (\<psi> and\<^sub>n F\<^sub>n \<phi>)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. w \<Turnstile>\<^sub>n \<phi> U\<^sub>n \<psi> = w \<Turnstile>\<^sub>n (\<phi> and\<^sub>n F\<^sub>n \<psi>) W\<^sub>n \<psi>
 2. w \<Turnstile>\<^sub>n \<phi> M\<^sub>n \<psi> = w \<Turnstile>\<^sub>n \<phi> R\<^sub>n (\<psi> and\<^sub>n F\<^sub>n \<phi>)
[PROOF STEP]
have "\<exists>j. suffix (i + j) w \<Turnstile>\<^sub>n \<psi>"
    if "suffix j w \<Turnstile>\<^sub>n \<psi>" and "\<forall>j\<le>i. \<not> suffix j w \<Turnstile>\<^sub>n \<psi>" for i j
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>j. suffix (i + j) w \<Turnstile>\<^sub>n \<psi>
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. suffix (i + ?j) w \<Turnstile>\<^sub>n \<psi>
[PROOF STEP]
from that
[PROOF STATE]
proof (chain)
picking this:
suffix j w \<Turnstile>\<^sub>n \<psi>
\<forall>j\<le>i. \<not> suffix j w \<Turnstile>\<^sub>n \<psi>
[PROOF STEP]
have "j > i"
[PROOF STATE]
proof (prove)
using this:
suffix j w \<Turnstile>\<^sub>n \<psi>
\<forall>j\<le>i. \<not> suffix j w \<Turnstile>\<^sub>n \<psi>

goal (1 subgoal):
 1. i < j
[PROOF STEP]
by (cases "j > i") auto
[PROOF STATE]
proof (state)
this:
i < j

goal (1 subgoal):
 1. suffix (i + ?j) w \<Turnstile>\<^sub>n \<psi>
[PROOF STEP]
thus "suffix (i + (j - i)) w \<Turnstile>\<^sub>n \<psi>"
[PROOF STATE]
proof (prove)
using this:
i < j

goal (1 subgoal):
 1. suffix (i + (j - i)) w \<Turnstile>\<^sub>n \<psi>
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
i < j
suffix j w \<Turnstile>\<^sub>n \<psi>
\<forall>j\<le>i. \<not> suffix j w \<Turnstile>\<^sub>n \<psi>

goal (1 subgoal):
 1. suffix (i + (j - i)) w \<Turnstile>\<^sub>n \<psi>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
suffix (i + (j - i)) w \<Turnstile>\<^sub>n \<psi>

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<lbrakk>suffix ?j w \<Turnstile>\<^sub>n \<psi>; \<forall>j\<le>?i. \<not> suffix j w \<Turnstile>\<^sub>n \<psi>\<rbrakk> \<Longrightarrow> \<exists>j. suffix (?i + j) w \<Turnstile>\<^sub>n \<psi>

goal (2 subgoals):
 1. w \<Turnstile>\<^sub>n \<phi> U\<^sub>n \<psi> = w \<Turnstile>\<^sub>n (\<phi> and\<^sub>n F\<^sub>n \<psi>) W\<^sub>n \<psi>
 2. w \<Turnstile>\<^sub>n \<phi> M\<^sub>n \<psi> = w \<Turnstile>\<^sub>n \<phi> R\<^sub>n (\<psi> and\<^sub>n F\<^sub>n \<phi>)
[PROOF STEP]
thus ?thesis1
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>suffix ?j w \<Turnstile>\<^sub>n \<psi>; \<forall>j\<le>?i. \<not> suffix j w \<Turnstile>\<^sub>n \<psi>\<rbrakk> \<Longrightarrow> \<exists>j. suffix (?i + j) w \<Turnstile>\<^sub>n \<psi>

goal (1 subgoal):
 1. w \<Turnstile>\<^sub>n \<phi> U\<^sub>n \<psi> = w \<Turnstile>\<^sub>n (\<phi> and\<^sub>n F\<^sub>n \<psi>) W\<^sub>n \<psi>
[PROOF STEP]
unfolding ltln_strong_weak
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>suffix ?j w \<Turnstile>\<^sub>n \<psi>; \<forall>j\<le>?i. \<not> suffix j w \<Turnstile>\<^sub>n \<psi>\<rbrakk> \<Longrightarrow> \<exists>j. suffix (?i + j) w \<Turnstile>\<^sub>n \<psi>

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

goal (1 subgoal):
 1. w \<Turnstile>\<^sub>n \<phi> M\<^sub>n \<psi> = w \<Turnstile>\<^sub>n \<phi> R\<^sub>n (\<psi> and\<^sub>n F\<^sub>n \<phi>)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. w \<Turnstile>\<^sub>n \<phi> M\<^sub>n \<psi> = w \<Turnstile>\<^sub>n \<phi> R\<^sub>n (\<psi> and\<^sub>n F\<^sub>n \<phi>)
[PROOF STEP]
have "\<exists>j. suffix (i + j) w \<Turnstile>\<^sub>n \<phi>"
    if "suffix j w \<Turnstile>\<^sub>n \<phi>" and "\<forall>j<i. \<not> suffix j w \<Turnstile>\<^sub>n \<phi>" for i j
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>j. suffix (i + j) w \<Turnstile>\<^sub>n \<phi>
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. suffix (i + ?j) w \<Turnstile>\<^sub>n \<phi>
[PROOF STEP]
from that
[PROOF STATE]
proof (chain)
picking this:
suffix j w \<Turnstile>\<^sub>n \<phi>
\<forall>j<i. \<not> suffix j w \<Turnstile>\<^sub>n \<phi>
[PROOF STEP]
have "j \<ge> i"
[PROOF STATE]
proof (prove)
using this:
suffix j w \<Turnstile>\<^sub>n \<phi>
\<forall>j<i. \<not> suffix j w \<Turnstile>\<^sub>n \<phi>

goal (1 subgoal):
 1. i \<le> j
[PROOF STEP]
by (cases "j \<ge> i") auto
[PROOF STATE]
proof (state)
this:
i \<le> j

goal (1 subgoal):
 1. suffix (i + ?j) w \<Turnstile>\<^sub>n \<phi>
[PROOF STEP]
thus "suffix (i + (j - i)) w \<Turnstile>\<^sub>n \<phi>"
[PROOF STATE]
proof (prove)
using this:
i \<le> j

goal (1 subgoal):
 1. suffix (i + (j - i)) w \<Turnstile>\<^sub>n \<phi>
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
i \<le> j
suffix j w \<Turnstile>\<^sub>n \<phi>
\<forall>j<i. \<not> suffix j w \<Turnstile>\<^sub>n \<phi>

goal (1 subgoal):
 1. suffix (i + (j - i)) w \<Turnstile>\<^sub>n \<phi>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
suffix (i + (j - i)) w \<Turnstile>\<^sub>n \<phi>

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<lbrakk>suffix ?j w \<Turnstile>\<^sub>n \<phi>; \<forall>j<?i. \<not> suffix j w \<Turnstile>\<^sub>n \<phi>\<rbrakk> \<Longrightarrow> \<exists>j. suffix (?i + j) w \<Turnstile>\<^sub>n \<phi>

goal (1 subgoal):
 1. w \<Turnstile>\<^sub>n \<phi> M\<^sub>n \<psi> = w \<Turnstile>\<^sub>n \<phi> R\<^sub>n (\<psi> and\<^sub>n F\<^sub>n \<phi>)
[PROOF STEP]
thus ?thesis2
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>suffix ?j w \<Turnstile>\<^sub>n \<phi>; \<forall>j<?i. \<not> suffix j w \<Turnstile>\<^sub>n \<phi>\<rbrakk> \<Longrightarrow> \<exists>j. suffix (?i + j) w \<Turnstile>\<^sub>n \<phi>

goal (1 subgoal):
 1. w \<Turnstile>\<^sub>n \<phi> M\<^sub>n \<psi> = w \<Turnstile>\<^sub>n \<phi> R\<^sub>n (\<psi> and\<^sub>n F\<^sub>n \<phi>)
[PROOF STEP]
unfolding ltln_strong_weak
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>suffix ?j w \<Turnstile>\<^sub>n \<phi>; \<forall>j<?i. \<not> suffix j w \<Turnstile>\<^sub>n \<phi>\<rbrakk> \<Longrightarrow> \<exists>j. suffix (?i + j) w \<Turnstile>\<^sub>n \<phi>

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ltln_weak_strong_2:
  "w \<Turnstile>\<^sub>n \<phi> W\<^sub>n \<psi> \<longleftrightarrow> w \<Turnstile>\<^sub>n \<phi> U\<^sub>n (\<psi> or\<^sub>n G\<^sub>n \<phi>)" (is "?thesis1")
  "w \<Turnstile>\<^sub>n \<phi> R\<^sub>n \<psi> \<longleftrightarrow> w \<Turnstile>\<^sub>n (\<phi> or\<^sub>n G\<^sub>n \<psi>) M\<^sub>n \<psi>" (is "?thesis2")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. w \<Turnstile>\<^sub>n \<phi> W\<^sub>n \<psi> = w \<Turnstile>\<^sub>n \<phi> U\<^sub>n (\<psi> or\<^sub>n G\<^sub>n \<phi>) &&& w \<Turnstile>\<^sub>n \<phi> R\<^sub>n \<psi> = w \<Turnstile>\<^sub>n (\<phi> or\<^sub>n G\<^sub>n \<psi>) M\<^sub>n \<psi>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. w \<Turnstile>\<^sub>n \<phi> W\<^sub>n \<psi> = w \<Turnstile>\<^sub>n \<phi> U\<^sub>n (\<psi> or\<^sub>n G\<^sub>n \<phi>)
 2. w \<Turnstile>\<^sub>n \<phi> R\<^sub>n \<psi> = w \<Turnstile>\<^sub>n (\<phi> or\<^sub>n G\<^sub>n \<psi>) M\<^sub>n \<psi>
[PROOF STEP]
have "suffix j w \<Turnstile>\<^sub>n \<phi>"
    if "\<And>j. j < i \<Longrightarrow> suffix j w \<Turnstile>\<^sub>n \<phi>" and "\<And>j. suffix (i + j) w \<Turnstile>\<^sub>n \<phi>" for i j
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. suffix j w \<Turnstile>\<^sub>n \<phi>
[PROOF STEP]
using that(1)[of j] that(2)[of "j - i"]
[PROOF STATE]
proof (prove)
using this:
j < i \<Longrightarrow> suffix j w \<Turnstile>\<^sub>n \<phi>
suffix (i + (j - i)) w \<Turnstile>\<^sub>n \<phi>

goal (1 subgoal):
 1. suffix j w \<Turnstile>\<^sub>n \<phi>
[PROOF STEP]
by (cases "j < i") simp_all
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<And>j. j < ?i \<Longrightarrow> suffix j w \<Turnstile>\<^sub>n \<phi>; \<And>j. suffix (?i + j) w \<Turnstile>\<^sub>n \<phi>\<rbrakk> \<Longrightarrow> suffix ?j w \<Turnstile>\<^sub>n \<phi>

goal (2 subgoals):
 1. w \<Turnstile>\<^sub>n \<phi> W\<^sub>n \<psi> = w \<Turnstile>\<^sub>n \<phi> U\<^sub>n (\<psi> or\<^sub>n G\<^sub>n \<phi>)
 2. w \<Turnstile>\<^sub>n \<phi> R\<^sub>n \<psi> = w \<Turnstile>\<^sub>n (\<phi> or\<^sub>n G\<^sub>n \<psi>) M\<^sub>n \<psi>
[PROOF STEP]
thus ?thesis1
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<And>j. j < ?i \<Longrightarrow> suffix j w \<Turnstile>\<^sub>n \<phi>; \<And>j. suffix (?i + j) w \<Turnstile>\<^sub>n \<phi>\<rbrakk> \<Longrightarrow> suffix ?j w \<Turnstile>\<^sub>n \<phi>

goal (1 subgoal):
 1. w \<Turnstile>\<^sub>n \<phi> W\<^sub>n \<psi> = w \<Turnstile>\<^sub>n \<phi> U\<^sub>n (\<psi> or\<^sub>n G\<^sub>n \<phi>)
[PROOF STEP]
unfolding ltln_weak_strong
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<And>j. j < ?i \<Longrightarrow> suffix j w \<Turnstile>\<^sub>n \<phi>; \<And>j. suffix (?i + j) w \<Turnstile>\<^sub>n \<phi>\<rbrakk> \<Longrightarrow> suffix ?j w \<Turnstile>\<^sub>n \<phi>

goal (1 subgoal):
 1. w \<Turnstile>\<^sub>n G\<^sub>n \<phi> or\<^sub>n (\<phi> U\<^sub>n \<psi>) = w \<Turnstile>\<^sub>n \<phi> U\<^sub>n (\<psi> or\<^sub>n G\<^sub>n \<phi>)
[PROOF STEP]
unfolding semantics_ltln.simps suffix_suffix
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<And>j. j < ?i \<Longrightarrow> suffix j w \<Turnstile>\<^sub>n \<phi>; \<And>j. suffix (?i + j) w \<Turnstile>\<^sub>n \<phi>\<rbrakk> \<Longrightarrow> suffix ?j w \<Turnstile>\<^sub>n \<phi>

goal (1 subgoal):
 1. ((\<forall>i. suffix i w \<Turnstile>\<^sub>n \<phi> \<or> (\<exists>j<i. False)) \<or> (\<exists>i. suffix i w \<Turnstile>\<^sub>n \<psi> \<and> (\<forall>j<i. suffix j w \<Turnstile>\<^sub>n \<phi>))) = (\<exists>i. (suffix i w \<Turnstile>\<^sub>n \<psi> \<or> (\<forall>ia. suffix (i + ia) w \<Turnstile>\<^sub>n \<phi> \<or> (\<exists>j<ia. False))) \<and> (\<forall>j<i. suffix j w \<Turnstile>\<^sub>n \<phi>))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
w \<Turnstile>\<^sub>n \<phi> W\<^sub>n \<psi> = w \<Turnstile>\<^sub>n \<phi> U\<^sub>n (\<psi> or\<^sub>n G\<^sub>n \<phi>)

goal (1 subgoal):
 1. w \<Turnstile>\<^sub>n \<phi> R\<^sub>n \<psi> = w \<Turnstile>\<^sub>n (\<phi> or\<^sub>n G\<^sub>n \<psi>) M\<^sub>n \<psi>
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. w \<Turnstile>\<^sub>n \<phi> R\<^sub>n \<psi> = w \<Turnstile>\<^sub>n (\<phi> or\<^sub>n G\<^sub>n \<psi>) M\<^sub>n \<psi>
[PROOF STEP]
have "suffix j w \<Turnstile>\<^sub>n \<psi>"
    if "\<And>j. j \<le> i \<Longrightarrow> suffix j w \<Turnstile>\<^sub>n \<psi>" and "\<And>j. suffix (i + j) w \<Turnstile>\<^sub>n \<psi>" for i j
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. suffix j w \<Turnstile>\<^sub>n \<psi>
[PROOF STEP]
using that(1)[of j] that(2)[of "j - i"]
[PROOF STATE]
proof (prove)
using this:
j \<le> i \<Longrightarrow> suffix j w \<Turnstile>\<^sub>n \<psi>
suffix (i + (j - i)) w \<Turnstile>\<^sub>n \<psi>

goal (1 subgoal):
 1. suffix j w \<Turnstile>\<^sub>n \<psi>
[PROOF STEP]
by (cases "j \<le> i") simp_all
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<And>j. j \<le> ?i \<Longrightarrow> suffix j w \<Turnstile>\<^sub>n \<psi>; \<And>j. suffix (?i + j) w \<Turnstile>\<^sub>n \<psi>\<rbrakk> \<Longrightarrow> suffix ?j w \<Turnstile>\<^sub>n \<psi>

goal (1 subgoal):
 1. w \<Turnstile>\<^sub>n \<phi> R\<^sub>n \<psi> = w \<Turnstile>\<^sub>n (\<phi> or\<^sub>n G\<^sub>n \<psi>) M\<^sub>n \<psi>
[PROOF STEP]
thus ?thesis2
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<And>j. j \<le> ?i \<Longrightarrow> suffix j w \<Turnstile>\<^sub>n \<psi>; \<And>j. suffix (?i + j) w \<Turnstile>\<^sub>n \<psi>\<rbrakk> \<Longrightarrow> suffix ?j w \<Turnstile>\<^sub>n \<psi>

goal (1 subgoal):
 1. w \<Turnstile>\<^sub>n \<phi> R\<^sub>n \<psi> = w \<Turnstile>\<^sub>n (\<phi> or\<^sub>n G\<^sub>n \<psi>) M\<^sub>n \<psi>
[PROOF STEP]
unfolding ltln_weak_strong
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<And>j. j \<le> ?i \<Longrightarrow> suffix j w \<Turnstile>\<^sub>n \<psi>; \<And>j. suffix (?i + j) w \<Turnstile>\<^sub>n \<psi>\<rbrakk> \<Longrightarrow> suffix ?j w \<Turnstile>\<^sub>n \<psi>

goal (1 subgoal):
 1. w \<Turnstile>\<^sub>n G\<^sub>n \<psi> or\<^sub>n (\<phi> M\<^sub>n \<psi>) = w \<Turnstile>\<^sub>n (\<phi> or\<^sub>n G\<^sub>n \<psi>) M\<^sub>n \<psi>
[PROOF STEP]
unfolding semantics_ltln.simps suffix_suffix
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<And>j. j \<le> ?i \<Longrightarrow> suffix j w \<Turnstile>\<^sub>n \<psi>; \<And>j. suffix (?i + j) w \<Turnstile>\<^sub>n \<psi>\<rbrakk> \<Longrightarrow> suffix ?j w \<Turnstile>\<^sub>n \<psi>

goal (1 subgoal):
 1. ((\<forall>i. suffix i w \<Turnstile>\<^sub>n \<psi> \<or> (\<exists>j<i. False)) \<or> (\<exists>i. suffix i w \<Turnstile>\<^sub>n \<phi> \<and> (\<forall>j\<le>i. suffix j w \<Turnstile>\<^sub>n \<psi>))) = (\<exists>i. (suffix i w \<Turnstile>\<^sub>n \<phi> \<or> (\<forall>ia. suffix (i + ia) w \<Turnstile>\<^sub>n \<psi> \<or> (\<exists>j<ia. False))) \<and> (\<forall>j\<le>i. suffix j w \<Turnstile>\<^sub>n \<psi>))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
w \<Turnstile>\<^sub>n \<phi> R\<^sub>n \<psi> = w \<Turnstile>\<^sub>n (\<phi> or\<^sub>n G\<^sub>n \<psi>) M\<^sub>n \<psi>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma GF_advice_restriction:
  "\<phi>[\<G>\<F> (\<phi> W\<^sub>n \<psi>) w]\<^sub>\<Pi>\<^sub>1 = \<phi>[\<G>\<F> \<phi> w]\<^sub>\<Pi>\<^sub>1"
  "\<psi>[\<G>\<F> (\<phi> R\<^sub>n \<psi>) w]\<^sub>\<Pi>\<^sub>1 = \<psi>[\<G>\<F> \<psi> w]\<^sub>\<Pi>\<^sub>1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<phi>[\<G>\<F> (\<phi> W\<^sub>n \<psi>) w]\<^sub>\<Pi>\<^sub>1 = \<phi>[\<G>\<F> \<phi> w]\<^sub>\<Pi>\<^sub>1 &&& \<psi>[\<G>\<F> (\<phi> R\<^sub>n \<psi>) w]\<^sub>\<Pi>\<^sub>1 = \<psi>[\<G>\<F> \<psi> w]\<^sub>\<Pi>\<^sub>1
[PROOF STEP]
by (metis (no_types, lifting) \<G>\<F>_semantics' inf_commute inf_left_commute inf_sup_absorb subformulas\<^sub>\<mu>.simps(6) GF_advice_inter_subformulas)
     (metis (no_types, lifting) GF_advice_inter \<G>\<F>.simps(5) \<G>\<F>_semantics' \<G>\<F>_subformulas\<^sub>\<mu> inf.commute sup.boundedE)


[STATEMENT]
lemma FG_advice_restriction:
  "\<psi>[\<F>\<G> (\<phi> U\<^sub>n \<psi>) w]\<^sub>\<Sigma>\<^sub>1 = \<psi>[\<F>\<G> \<psi> w]\<^sub>\<Sigma>\<^sub>1"
  "\<phi>[\<F>\<G> (\<phi> M\<^sub>n \<psi>) w]\<^sub>\<Sigma>\<^sub>1 = \<phi>[\<F>\<G> \<phi> w]\<^sub>\<Sigma>\<^sub>1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<psi>[\<F>\<G> (\<phi> U\<^sub>n \<psi>) w]\<^sub>\<Sigma>\<^sub>1 = \<psi>[\<F>\<G> \<psi> w]\<^sub>\<Sigma>\<^sub>1 &&& \<phi>[\<F>\<G> (\<phi> M\<^sub>n \<psi>) w]\<^sub>\<Sigma>\<^sub>1 = \<phi>[\<F>\<G> \<phi> w]\<^sub>\<Sigma>\<^sub>1
[PROOF STEP]
by (metis (no_types, lifting) FG_advice_inter \<F>\<G>.simps(4) \<F>\<G>_semantics' \<F>\<G>_subformulas\<^sub>\<nu> inf.commute sup.boundedE)
     (metis (no_types, lifting) FG_advice_inter \<F>\<G>.simps(7) \<F>\<G>_semantics' \<F>\<G>_subformulas\<^sub>\<nu> inf.right_idem inf_commute sup.cobounded1)


[STATEMENT]
lemma flatten_sigma_2_intersection:
  "M \<inter> subformulas\<^sub>\<mu> \<phi> \<subseteq> S \<Longrightarrow> \<phi>[M \<inter> S]\<^sub>\<Sigma>\<^sub>2 = \<phi>[M]\<^sub>\<Sigma>\<^sub>2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. M \<inter> subformulas\<^sub>\<mu> \<phi> \<subseteq> S \<Longrightarrow> \<phi>[M \<inter> S]\<^sub>\<Sigma>\<^sub>2 = \<phi>[M]\<^sub>\<Sigma>\<^sub>2
[PROOF STEP]
by (induction \<phi>) (simp; blast intro: GF_advice_inter)+


[STATEMENT]
lemma flatten_sigma_2_intersection_eq:
  "M \<inter> subformulas\<^sub>\<mu> \<phi> = M' \<Longrightarrow> \<phi>[M']\<^sub>\<Sigma>\<^sub>2 = \<phi>[M]\<^sub>\<Sigma>\<^sub>2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. M \<inter> subformulas\<^sub>\<mu> \<phi> = M' \<Longrightarrow> \<phi>[M']\<^sub>\<Sigma>\<^sub>2 = \<phi>[M]\<^sub>\<Sigma>\<^sub>2
[PROOF STEP]
using flatten_sigma_2_intersection
[PROOF STATE]
proof (prove)
using this:
?M \<inter> subformulas\<^sub>\<mu> ?\<phi> \<subseteq> ?S \<Longrightarrow> ?\<phi>[?M \<inter> ?S]\<^sub>\<Sigma>\<^sub>2 = ?\<phi>[?M]\<^sub>\<Sigma>\<^sub>2

goal (1 subgoal):
 1. M \<inter> subformulas\<^sub>\<mu> \<phi> = M' \<Longrightarrow> \<phi>[M']\<^sub>\<Sigma>\<^sub>2 = \<phi>[M]\<^sub>\<Sigma>\<^sub>2
[PROOF STEP]
by auto


[STATEMENT]
lemma flatten_sigma_2_monotone:
  "w \<Turnstile>\<^sub>n \<phi>[M]\<^sub>\<Sigma>\<^sub>2 \<Longrightarrow> M \<subseteq> M' \<Longrightarrow> w \<Turnstile>\<^sub>n \<phi>[M']\<^sub>\<Sigma>\<^sub>2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<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
[PROOF STEP]
by (induction \<phi> arbitrary: w)
     (simp; blast dest: GF_advice_monotone)+


[STATEMENT]
lemma flatten_pi_2_intersection:
  "N \<inter> subformulas\<^sub>\<nu> \<phi> \<subseteq> S \<Longrightarrow> \<phi>[N \<inter> S]\<^sub>\<Pi>\<^sub>2 = \<phi>[N]\<^sub>\<Pi>\<^sub>2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. N \<inter> subformulas\<^sub>\<nu> \<phi> \<subseteq> S \<Longrightarrow> \<phi>[N \<inter> S]\<^sub>\<Pi>\<^sub>2 = \<phi>[N]\<^sub>\<Pi>\<^sub>2
[PROOF STEP]
by (induction \<phi>) (simp; blast intro: FG_advice_inter)+


[STATEMENT]
lemma flatten_pi_2_intersection_eq:
  "N \<inter> subformulas\<^sub>\<nu> \<phi> = N' \<Longrightarrow> \<phi>[N']\<^sub>\<Pi>\<^sub>2 = \<phi>[N]\<^sub>\<Pi>\<^sub>2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. N \<inter> subformulas\<^sub>\<nu> \<phi> = N' \<Longrightarrow> \<phi>[N']\<^sub>\<Pi>\<^sub>2 = \<phi>[N]\<^sub>\<Pi>\<^sub>2
[PROOF STEP]
using flatten_pi_2_intersection
[PROOF STATE]
proof (prove)
using this:
?N \<inter> subformulas\<^sub>\<nu> ?\<phi> \<subseteq> ?S \<Longrightarrow> ?\<phi>[?N \<inter> ?S]\<^sub>\<Pi>\<^sub>2 = ?\<phi>[?N]\<^sub>\<Pi>\<^sub>2

goal (1 subgoal):
 1. N \<inter> subformulas\<^sub>\<nu> \<phi> = N' \<Longrightarrow> \<phi>[N']\<^sub>\<Pi>\<^sub>2 = \<phi>[N]\<^sub>\<Pi>\<^sub>2
[PROOF STEP]
by auto


[STATEMENT]
lemma flatten_pi_2_monotone:
  "w \<Turnstile>\<^sub>n \<phi>[N]\<^sub>\<Pi>\<^sub>2 \<Longrightarrow> N \<subseteq> N' \<Longrightarrow> w \<Turnstile>\<^sub>n \<phi>[N']\<^sub>\<Pi>\<^sub>2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<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
[PROOF STEP]
by (induction \<phi> arbitrary: w)
     (simp; blast dest: FG_advice_monotone)+


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

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

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

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

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

goal (2 subgoals):
 1. w \<Turnstile>\<^sub>n \<phi> W\<^sub>n \<psi> \<Longrightarrow> w \<Turnstile>\<^sub>n \<phi> U\<^sub>n (\<psi> or\<^sub>n G\<^sub>n \<phi>[\<G>\<F> \<phi> w]\<^sub>\<Pi>\<^sub>1)
 2. w \<Turnstile>\<^sub>n \<phi> U\<^sub>n (\<psi> or\<^sub>n G\<^sub>n \<phi>[\<G>\<F> \<phi> w]\<^sub>\<Pi>\<^sub>1) \<Longrightarrow> w \<Turnstile>\<^sub>n \<phi> W\<^sub>n \<psi>
[PROOF STEP]
obtain i where "\<And>j. \<F> \<phi> (suffix i w) \<subseteq> \<G>\<F> \<phi> w"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>i. (\<And>j. \<F> \<phi> (suffix i w) \<subseteq> \<G>\<F> \<phi> w) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis MOST_nat_le \<G>\<F>_suffix \<mu>_stable_def order_refl suffix_\<mu>_stable)
[PROOF STATE]
proof (state)
this:
\<F> \<phi> (suffix i w) \<subseteq> \<G>\<F> \<phi> w

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

goal (1 subgoal):
 1. \<And>j. \<F> \<phi> (suffix i (suffix j w)) \<subseteq> \<G>\<F> \<phi> w
[PROOF STEP]
by (metis \<F>_suffix \<G>\<F>_\<F>_subset \<G>\<F>_suffix semiring_normalization_rules(24) subset_Un_eq suffix_suffix sup.orderE)
[PROOF STATE]
proof (state)
this:
\<F> \<phi> (suffix i (suffix ?j2 w)) \<subseteq> \<G>\<F> \<phi> w

goal (2 subgoals):
 1. w \<Turnstile>\<^sub>n \<phi> W\<^sub>n \<psi> \<Longrightarrow> w \<Turnstile>\<^sub>n \<phi> U\<^sub>n (\<psi> or\<^sub>n G\<^sub>n \<phi>[\<G>\<F> \<phi> w]\<^sub>\<Pi>\<^sub>1)
 2. w \<Turnstile>\<^sub>n \<phi> U\<^sub>n (\<psi> or\<^sub>n G\<^sub>n \<phi>[\<G>\<F> \<phi> w]\<^sub>\<Pi>\<^sub>1) \<Longrightarrow> w \<Turnstile>\<^sub>n \<phi> W\<^sub>n \<psi>
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
w \<Turnstile>\<^sub>n G\<^sub>n \<phi>
\<F> \<phi> (suffix i (suffix ?j2 w)) \<subseteq> \<G>\<F> \<phi> w
[PROOF STEP]
have "suffix i w \<Turnstile>\<^sub>n G\<^sub>n (\<phi>[\<G>\<F> \<phi> w]\<^sub>\<Pi>\<^sub>1)"
[PROOF STATE]
proof (prove)
using this:
w \<Turnstile>\<^sub>n G\<^sub>n \<phi>
\<F> \<phi> (suffix i (suffix ?j2 w)) \<subseteq> \<G>\<F> \<phi> w

goal (1 subgoal):
 1. suffix i w \<Turnstile>\<^sub>n G\<^sub>n \<phi>[\<G>\<F> \<phi> w]\<^sub>\<Pi>\<^sub>1
[PROOF STEP]
using GF_advice_a1[OF \<open>\<And>j. \<F> \<phi> (suffix i (suffix j w)) \<subseteq> \<G>\<F> \<phi> w\<close>]
[PROOF STATE]
proof (prove)
using this:
w \<Turnstile>\<^sub>n G\<^sub>n \<phi>
\<F> \<phi> (suffix i (suffix ?j2 w)) \<subseteq> \<G>\<F> \<phi> w
suffix i (suffix ?j1 w) \<Turnstile>\<^sub>n \<phi> \<Longrightarrow> suffix i (suffix ?j1 w) \<Turnstile>\<^sub>n \<phi>[\<G>\<F> \<phi> w]\<^sub>\<Pi>\<^sub>1

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

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

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

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

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

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

goal (2 subgoals):
 1. w \<Turnstile>\<^sub>n \<phi> W\<^sub>n \<psi> \<Longrightarrow> w \<Turnstile>\<^sub>n \<phi> U\<^sub>n (\<psi> or\<^sub>n G\<^sub>n \<phi>[\<G>\<F> \<phi> w]\<^sub>\<Pi>\<^sub>1)
 2. w \<Turnstile>\<^sub>n \<phi> U\<^sub>n (\<psi> or\<^sub>n G\<^sub>n \<phi>[\<G>\<F> \<phi> w]\<^sub>\<Pi>\<^sub>1) \<Longrightarrow> w \<Turnstile>\<^sub>n \<phi> W\<^sub>n \<psi>
[PROOF STEP]
have "w \<Turnstile>\<^sub>n \<phi> U\<^sub>n \<psi> \<Longrightarrow> ?rhs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. w \<Turnstile>\<^sub>n \<phi> U\<^sub>n \<psi> \<Longrightarrow> w \<Turnstile>\<^sub>n \<phi> U\<^sub>n (\<psi> or\<^sub>n G\<^sub>n \<phi>[\<G>\<F> \<phi> w]\<^sub>\<Pi>\<^sub>1)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
w \<Turnstile>\<^sub>n \<phi> U\<^sub>n \<psi> \<Longrightarrow> w \<Turnstile>\<^sub>n \<phi> U\<^sub>n (\<psi> or\<^sub>n G\<^sub>n \<phi>[\<G>\<F> \<phi> w]\<^sub>\<Pi>\<^sub>1)

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

goal (1 subgoal):
 1. w \<Turnstile>\<^sub>n \<phi> U\<^sub>n (\<psi> or\<^sub>n G\<^sub>n \<phi>[\<G>\<F> \<phi> w]\<^sub>\<Pi>\<^sub>1)
[PROOF STEP]
using ltln_weak_to_strong(1)
[PROOF STATE]
proof (prove)
using this:
w \<Turnstile>\<^sub>n \<phi> W\<^sub>n \<psi>
w \<Turnstile>\<^sub>n G\<^sub>n \<phi> \<Longrightarrow> w \<Turnstile>\<^sub>n \<phi> U\<^sub>n (\<psi> or\<^sub>n G\<^sub>n \<phi>[\<G>\<F> \<phi> w]\<^sub>\<Pi>\<^sub>1)
w \<Turnstile>\<^sub>n \<phi> U\<^sub>n \<psi> \<Longrightarrow> w \<Turnstile>\<^sub>n \<phi> U\<^sub>n (\<psi> or\<^sub>n G\<^sub>n \<phi>[\<G>\<F> \<phi> w]\<^sub>\<Pi>\<^sub>1)
\<lbrakk>?w \<Turnstile>\<^sub>n ?\<phi> W\<^sub>n ?\<psi>; \<not> ?w \<Turnstile>\<^sub>n G\<^sub>n ?\<phi>\<rbrakk> \<Longrightarrow> ?w \<Turnstile>\<^sub>n ?\<phi> U\<^sub>n ?\<psi>

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

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

goal (1 subgoal):
 1. w \<Turnstile>\<^sub>n \<phi> U\<^sub>n (\<psi> or\<^sub>n G\<^sub>n \<phi>[\<G>\<F> \<phi> w]\<^sub>\<Pi>\<^sub>1) \<Longrightarrow> w \<Turnstile>\<^sub>n \<phi> W\<^sub>n \<psi>
[PROOF STEP]
thus ?lhs
[PROOF STATE]
proof (prove)
using this:
w \<Turnstile>\<^sub>n \<phi> U\<^sub>n (\<psi> or\<^sub>n G\<^sub>n \<phi>[\<G>\<F> \<phi> w]\<^sub>\<Pi>\<^sub>1)

goal (1 subgoal):
 1. w \<Turnstile>\<^sub>n \<phi> W\<^sub>n \<psi>
[PROOF STEP]
unfolding ltln_weak_strong_2
[PROOF STATE]
proof (prove)
using this:
w \<Turnstile>\<^sub>n \<phi> U\<^sub>n (\<psi> or\<^sub>n G\<^sub>n \<phi>[\<G>\<F> \<phi> w]\<^sub>\<Pi>\<^sub>1)

goal (1 subgoal):
 1. w \<Turnstile>\<^sub>n \<phi> U\<^sub>n (\<psi> or\<^sub>n G\<^sub>n \<phi>)
[PROOF STEP]
unfolding semantics_ltln.simps
[PROOF STATE]
proof (prove)
using this:
\<exists>i. (suffix i w \<Turnstile>\<^sub>n \<psi> \<or> (\<forall>ia. suffix ia (suffix i w) \<Turnstile>\<^sub>n \<phi>[\<G>\<F> \<phi> w]\<^sub>\<Pi>\<^sub>1 \<or> (\<exists>j<ia. False))) \<and> (\<forall>j<i. suffix j w \<Turnstile>\<^sub>n \<phi>)

goal (1 subgoal):
 1. \<exists>i. (suffix i w \<Turnstile>\<^sub>n \<psi> \<or> (\<forall>ia. suffix ia (suffix i w) \<Turnstile>\<^sub>n \<phi> \<or> (\<exists>j<ia. False))) \<and> (\<forall>j<i. suffix j w \<Turnstile>\<^sub>n \<phi>)
[PROOF STEP]
by (metis \<G>\<F>_suffix order_refl GF_advice_a2)
[PROOF STATE]
proof (state)
this:
w \<Turnstile>\<^sub>n \<phi> W\<^sub>n \<psi>

goal:
No subgoals!
[PROOF STEP]
qed


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

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

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

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

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

goal (2 subgoals):
 1. w \<Turnstile>\<^sub>n \<phi> R\<^sub>n \<psi> \<Longrightarrow> w \<Turnstile>\<^sub>n (\<phi> or\<^sub>n G\<^sub>n \<psi>[\<G>\<F> \<psi> w]\<^sub>\<Pi>\<^sub>1) M\<^sub>n \<psi>
 2. w \<Turnstile>\<^sub>n (\<phi> or\<^sub>n G\<^sub>n \<psi>[\<G>\<F> \<psi> w]\<^sub>\<Pi>\<^sub>1) M\<^sub>n \<psi> \<Longrightarrow> w \<Turnstile>\<^sub>n \<phi> R\<^sub>n \<psi>
[PROOF STEP]
obtain i where "\<And>j. \<F> \<psi> (suffix i w) \<subseteq> \<G>\<F> \<psi> w"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>i. (\<And>j. \<F> \<psi> (suffix i w) \<subseteq> \<G>\<F> \<psi> w) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis MOST_nat_le \<G>\<F>_suffix \<mu>_stable_def order_refl suffix_\<mu>_stable)
[PROOF STATE]
proof (state)
this:
\<F> \<psi> (suffix i w) \<subseteq> \<G>\<F> \<psi> w

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

goal (1 subgoal):
 1. \<And>j. \<F> \<psi> (suffix i (suffix j w)) \<subseteq> \<G>\<F> \<psi> w
[PROOF STEP]
by (metis \<F>_suffix \<G>\<F>_\<F>_subset \<G>\<F>_suffix semiring_normalization_rules(24) subset_Un_eq suffix_suffix sup.orderE)
[PROOF STATE]
proof (state)
this:
\<F> \<psi> (suffix i (suffix ?j2 w)) \<subseteq> \<G>\<F> \<psi> w

goal (2 subgoals):
 1. w \<Turnstile>\<^sub>n \<phi> R\<^sub>n \<psi> \<Longrightarrow> w \<Turnstile>\<^sub>n (\<phi> or\<^sub>n G\<^sub>n \<psi>[\<G>\<F> \<psi> w]\<^sub>\<Pi>\<^sub>1) M\<^sub>n \<psi>
 2. w \<Turnstile>\<^sub>n (\<phi> or\<^sub>n G\<^sub>n \<psi>[\<G>\<F> \<psi> w]\<^sub>\<Pi>\<^sub>1) M\<^sub>n \<psi> \<Longrightarrow> w \<Turnstile>\<^sub>n \<phi> R\<^sub>n \<psi>
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
w \<Turnstile>\<^sub>n G\<^sub>n \<psi>
\<F> \<psi> (suffix i (suffix ?j2 w)) \<subseteq> \<G>\<F> \<psi> w
[PROOF STEP]
have "suffix i w \<Turnstile>\<^sub>n G\<^sub>n (\<psi>[\<G>\<F> \<psi> w]\<^sub>\<Pi>\<^sub>1)"
[PROOF STATE]
proof (prove)
using this:
w \<Turnstile>\<^sub>n G\<^sub>n \<psi>
\<F> \<psi> (suffix i (suffix ?j2 w)) \<subseteq> \<G>\<F> \<psi> w

goal (1 subgoal):
 1. suffix i w \<Turnstile>\<^sub>n G\<^sub>n \<psi>[\<G>\<F> \<psi> w]\<^sub>\<Pi>\<^sub>1
[PROOF STEP]
using GF_advice_a1[OF \<open>\<And>j. \<F> \<psi> (suffix i (suffix j w)) \<subseteq> \<G>\<F> \<psi> w\<close>]
[PROOF STATE]
proof (prove)
using this:
w \<Turnstile>\<^sub>n G\<^sub>n \<psi>
\<F> \<psi> (suffix i (suffix ?j2 w)) \<subseteq> \<G>\<F> \<psi> w
suffix i (suffix ?j1 w) \<Turnstile>\<^sub>n \<psi> \<Longrightarrow> suffix i (suffix ?j1 w) \<Turnstile>\<^sub>n \<psi>[\<G>\<F> \<psi> w]\<^sub>\<Pi>\<^sub>1

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

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

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

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

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

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

goal (2 subgoals):
 1. w \<Turnstile>\<^sub>n \<phi> R\<^sub>n \<psi> \<Longrightarrow> w \<Turnstile>\<^sub>n (\<phi> or\<^sub>n G\<^sub>n \<psi>[\<G>\<F> \<psi> w]\<^sub>\<Pi>\<^sub>1) M\<^sub>n \<psi>
 2. w \<Turnstile>\<^sub>n (\<phi> or\<^sub>n G\<^sub>n \<psi>[\<G>\<F> \<psi> w]\<^sub>\<Pi>\<^sub>1) M\<^sub>n \<psi> \<Longrightarrow> w \<Turnstile>\<^sub>n \<phi> R\<^sub>n \<psi>
[PROOF STEP]
have "w \<Turnstile>\<^sub>n \<phi> M\<^sub>n \<psi> \<Longrightarrow> ?rhs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. w \<Turnstile>\<^sub>n \<phi> M\<^sub>n \<psi> \<Longrightarrow> w \<Turnstile>\<^sub>n (\<phi> or\<^sub>n G\<^sub>n \<psi>[\<G>\<F> \<psi> w]\<^sub>\<Pi>\<^sub>1) M\<^sub>n \<psi>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
w \<Turnstile>\<^sub>n \<phi> M\<^sub>n \<psi> \<Longrightarrow> w \<Turnstile>\<^sub>n (\<phi> or\<^sub>n G\<^sub>n \<psi>[\<G>\<F> \<psi> w]\<^sub>\<Pi>\<^sub>1) M\<^sub>n \<psi>

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

goal (1 subgoal):
 1. w \<Turnstile>\<^sub>n (\<phi> or\<^sub>n G\<^sub>n \<psi>[\<G>\<F> \<psi> w]\<^sub>\<Pi>\<^sub>1) M\<^sub>n \<psi>
[PROOF STEP]
using ltln_weak_to_strong
[PROOF STATE]
proof (prove)
using this:
w \<Turnstile>\<^sub>n \<phi> R\<^sub>n \<psi>
w \<Turnstile>\<^sub>n G\<^sub>n \<psi> \<Longrightarrow> w \<Turnstile>\<^sub>n (\<phi> or\<^sub>n G\<^sub>n \<psi>[\<G>\<F> \<psi> w]\<^sub>\<Pi>\<^sub>1) M\<^sub>n \<psi>
w \<Turnstile>\<^sub>n \<phi> M\<^sub>n \<psi> \<Longrightarrow> w \<Turnstile>\<^sub>n (\<phi> or\<^sub>n G\<^sub>n \<psi>[\<G>\<F> \<psi> w]\<^sub>\<Pi>\<^sub>1) M\<^sub>n \<psi>
\<lbrakk>?w \<Turnstile>\<^sub>n ?\<phi> W\<^sub>n ?\<psi>; \<not> ?w \<Turnstile>\<^sub>n G\<^sub>n ?\<phi>\<rbrakk> \<Longrightarrow> ?w \<Turnstile>\<^sub>n ?\<phi> U\<^sub>n ?\<psi>
\<lbrakk>?w \<Turnstile>\<^sub>n ?\<phi> W\<^sub>n ?\<psi>; ?w \<Turnstile>\<^sub>n F\<^sub>n ?\<psi>\<rbrakk> \<Longrightarrow> ?w \<Turnstile>\<^sub>n ?\<phi> U\<^sub>n ?\<psi>
\<lbrakk>?w \<Turnstile>\<^sub>n ?\<phi> R\<^sub>n ?\<psi>; \<not> ?w \<Turnstile>\<^sub>n G\<^sub>n ?\<psi>\<rbrakk> \<Longrightarrow> ?w \<Turnstile>\<^sub>n ?\<phi> M\<^sub>n ?\<psi>
\<lbrakk>?w \<Turnstile>\<^sub>n ?\<phi> R\<^sub>n ?\<psi>; ?w \<Turnstile>\<^sub>n F\<^sub>n ?\<phi>\<rbrakk> \<Longrightarrow> ?w \<Turnstile>\<^sub>n ?\<phi> M\<^sub>n ?\<psi>

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

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

goal (1 subgoal):
 1. w \<Turnstile>\<^sub>n (\<phi> or\<^sub>n G\<^sub>n \<psi>[\<G>\<F> \<psi> w]\<^sub>\<Pi>\<^sub>1) M\<^sub>n \<psi> \<Longrightarrow> w \<Turnstile>\<^sub>n \<phi> R\<^sub>n \<psi>
[PROOF STEP]
thus ?lhs
[PROOF STATE]
proof (prove)
using this:
w \<Turnstile>\<^sub>n (\<phi> or\<^sub>n G\<^sub>n \<psi>[\<G>\<F> \<psi> w]\<^sub>\<Pi>\<^sub>1) M\<^sub>n \<psi>

goal (1 subgoal):
 1. w \<Turnstile>\<^sub>n \<phi> R\<^sub>n \<psi>
[PROOF STEP]
unfolding ltln_weak_strong_2
[PROOF STATE]
proof (prove)
using this:
w \<Turnstile>\<^sub>n (\<phi> or\<^sub>n G\<^sub>n \<psi>[\<G>\<F> \<psi> w]\<^sub>\<Pi>\<^sub>1) M\<^sub>n \<psi>

goal (1 subgoal):
 1. w \<Turnstile>\<^sub>n (\<phi> or\<^sub>n G\<^sub>n \<psi>) M\<^sub>n \<psi>
[PROOF STEP]
unfolding semantics_ltln.simps
[PROOF STATE]
proof (prove)
using this:
\<exists>i. (suffix i w \<Turnstile>\<^sub>n \<phi> \<or> (\<forall>ia. suffix ia (suffix i w) \<Turnstile>\<^sub>n \<psi>[\<G>\<F> \<psi> w]\<^sub>\<Pi>\<^sub>1 \<or> (\<exists>j<ia. False))) \<and> (\<forall>j\<le>i. suffix j w \<Turnstile>\<^sub>n \<psi>)

goal (1 subgoal):
 1. \<exists>i. (suffix i w \<Turnstile>\<^sub>n \<phi> \<or> (\<forall>ia. suffix ia (suffix i w) \<Turnstile>\<^sub>n \<psi> \<or> (\<exists>j<ia. False))) \<and> (\<forall>j\<le>i. suffix j w \<Turnstile>\<^sub>n \<psi>)
[PROOF STEP]
by (metis GF_advice_a2 \<G>\<F>_suffix order_refl)
[PROOF STATE]
proof (state)
this:
w \<Turnstile>\<^sub>n \<phi> R\<^sub>n \<psi>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ltln_weak_strong_stable_words:
  "w \<Turnstile>\<^sub>n (\<phi> W\<^sub>n \<psi>) \<longleftrightarrow> w \<Turnstile>\<^sub>n \<phi> U\<^sub>n (\<psi> or\<^sub>n (G\<^sub>n \<phi>[\<G>\<F> (\<phi> W\<^sub>n \<psi>) w]\<^sub>\<Pi>\<^sub>1))"
  "w \<Turnstile>\<^sub>n (\<phi> R\<^sub>n \<psi>) \<longleftrightarrow> w \<Turnstile>\<^sub>n (\<phi> or\<^sub>n (G\<^sub>n \<psi>[\<G>\<F> (\<phi> R\<^sub>n \<psi>) w]\<^sub>\<Pi>\<^sub>1)) M\<^sub>n \<psi>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. w \<Turnstile>\<^sub>n \<phi> W\<^sub>n \<psi> = w \<Turnstile>\<^sub>n \<phi> U\<^sub>n (\<psi> or\<^sub>n G\<^sub>n \<phi>[\<G>\<F> (\<phi> W\<^sub>n \<psi>) w]\<^sub>\<Pi>\<^sub>1) &&& w \<Turnstile>\<^sub>n \<phi> R\<^sub>n \<psi> = w \<Turnstile>\<^sub>n (\<phi> or\<^sub>n G\<^sub>n \<psi>[\<G>\<F> (\<phi> R\<^sub>n \<psi>) w]\<^sub>\<Pi>\<^sub>1) M\<^sub>n \<psi>
[PROOF STEP]
unfolding ltln_weak_strong_stable_words_1 ltln_weak_strong_stable_words_2 GF_advice_restriction
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. w \<Turnstile>\<^sub>n \<phi> U\<^sub>n (\<psi> or\<^sub>n G\<^sub>n \<phi>[\<G>\<F> \<phi> w]\<^sub>\<Pi>\<^sub>1) = w \<Turnstile>\<^sub>n \<phi> U\<^sub>n (\<psi> or\<^sub>n G\<^sub>n \<phi>[\<G>\<F> \<phi> w]\<^sub>\<Pi>\<^sub>1) &&& w \<Turnstile>\<^sub>n (\<phi> or\<^sub>n G\<^sub>n \<psi>[\<G>\<F> \<psi> w]\<^sub>\<Pi>\<^sub>1) M\<^sub>n \<psi> = w \<Turnstile>\<^sub>n (\<phi> or\<^sub>n G\<^sub>n \<psi>[\<G>\<F> \<psi> w]\<^sub>\<Pi>\<^sub>1) M\<^sub>n \<psi>
[PROOF STEP]
by simp+


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