[STATEMENT]
lemma ex_next_free_stutter_free_canonical:
  assumes A: "atoms_pltl \<phi> \<subseteq> A" and fin: "finite A"
  shows "\<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and>
             (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> (\<sigma> \<Turnstile>\<^sub>p \<psi>) = (\<sigma> \<Turnstile>\<^sub>p \<phi>))"
    (is "\<exists>\<psi>. ?P \<phi> \<psi>")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>)
[PROOF STEP]
using A
[PROOF STATE]
proof (prove)
using this:
atoms_pltl \<phi> \<subseteq> A

goal (1 subgoal):
 1. \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>)
[PROOF STEP]
proof (induct \<phi>)
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. atoms_pltl false\<^sub>p \<subseteq> A \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p false\<^sub>p)
 2. \<And>x. atoms_pltl atom\<^sub>p(x) \<subseteq> A \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p atom\<^sub>p(x))
 3. \<And>\<phi>1 \<phi>2. \<lbrakk>atoms_pltl \<phi>1 \<subseteq> A \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>1); atoms_pltl \<phi>2 \<subseteq> A \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>2); atoms_pltl (\<phi>1 implies\<^sub>p \<phi>2) \<subseteq> A\<rbrakk> \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>1 implies\<^sub>p \<phi>2)
 4. \<And>\<phi>. \<lbrakk>atoms_pltl \<phi> \<subseteq> A \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>); atoms_pltl (X\<^sub>p \<phi>) \<subseteq> A\<rbrakk> \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p X\<^sub>p \<phi>)
 5. \<And>\<phi>1 \<phi>2. \<lbrakk>atoms_pltl \<phi>1 \<subseteq> A \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>1); atoms_pltl \<phi>2 \<subseteq> A \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>2); atoms_pltl (\<phi>1 U\<^sub>p \<phi>2) \<subseteq> A\<rbrakk> \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>1 U\<^sub>p \<phi>2)
[PROOF STEP]
txt \<open>The cases of \<open>false\<close> and atomic formulas are trivial.\<close>
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. atoms_pltl false\<^sub>p \<subseteq> A \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p false\<^sub>p)
 2. \<And>x. atoms_pltl atom\<^sub>p(x) \<subseteq> A \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p atom\<^sub>p(x))
 3. \<And>\<phi>1 \<phi>2. \<lbrakk>atoms_pltl \<phi>1 \<subseteq> A \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>1); atoms_pltl \<phi>2 \<subseteq> A \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>2); atoms_pltl (\<phi>1 implies\<^sub>p \<phi>2) \<subseteq> A\<rbrakk> \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>1 implies\<^sub>p \<phi>2)
 4. \<And>\<phi>. \<lbrakk>atoms_pltl \<phi> \<subseteq> A \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>); atoms_pltl (X\<^sub>p \<phi>) \<subseteq> A\<rbrakk> \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p X\<^sub>p \<phi>)
 5. \<And>\<phi>1 \<phi>2. \<lbrakk>atoms_pltl \<phi>1 \<subseteq> A \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>1); atoms_pltl \<phi>2 \<subseteq> A \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>2); atoms_pltl (\<phi>1 U\<^sub>p \<phi>2) \<subseteq> A\<rbrakk> \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>1 U\<^sub>p \<phi>2)
[PROOF STEP]
have "?P false\<^sub>p false\<^sub>p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. next_free false\<^sub>p \<and> atoms_pltl false\<^sub>p \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p false\<^sub>p = \<sigma> \<Turnstile>\<^sub>p false\<^sub>p)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
next_free false\<^sub>p \<and> atoms_pltl false\<^sub>p \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p false\<^sub>p = \<sigma> \<Turnstile>\<^sub>p false\<^sub>p)

goal (5 subgoals):
 1. atoms_pltl false\<^sub>p \<subseteq> A \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p false\<^sub>p)
 2. \<And>x. atoms_pltl atom\<^sub>p(x) \<subseteq> A \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p atom\<^sub>p(x))
 3. \<And>\<phi>1 \<phi>2. \<lbrakk>atoms_pltl \<phi>1 \<subseteq> A \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>1); atoms_pltl \<phi>2 \<subseteq> A \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>2); atoms_pltl (\<phi>1 implies\<^sub>p \<phi>2) \<subseteq> A\<rbrakk> \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>1 implies\<^sub>p \<phi>2)
 4. \<And>\<phi>. \<lbrakk>atoms_pltl \<phi> \<subseteq> A \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>); atoms_pltl (X\<^sub>p \<phi>) \<subseteq> A\<rbrakk> \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p X\<^sub>p \<phi>)
 5. \<And>\<phi>1 \<phi>2. \<lbrakk>atoms_pltl \<phi>1 \<subseteq> A \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>1); atoms_pltl \<phi>2 \<subseteq> A \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>2); atoms_pltl (\<phi>1 U\<^sub>p \<phi>2) \<subseteq> A\<rbrakk> \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>1 U\<^sub>p \<phi>2)
[PROOF STEP]
thus "\<exists>\<psi>. ?P false\<^sub>p \<psi>"
[PROOF STATE]
proof (prove)
using this:
next_free false\<^sub>p \<and> atoms_pltl false\<^sub>p \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p false\<^sub>p = \<sigma> \<Turnstile>\<^sub>p false\<^sub>p)

goal (1 subgoal):
 1. \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p false\<^sub>p)
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
\<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p false\<^sub>p)

goal (4 subgoals):
 1. \<And>x. atoms_pltl atom\<^sub>p(x) \<subseteq> A \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p atom\<^sub>p(x))
 2. \<And>\<phi>1 \<phi>2. \<lbrakk>atoms_pltl \<phi>1 \<subseteq> A \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>1); atoms_pltl \<phi>2 \<subseteq> A \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>2); atoms_pltl (\<phi>1 implies\<^sub>p \<phi>2) \<subseteq> A\<rbrakk> \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>1 implies\<^sub>p \<phi>2)
 3. \<And>\<phi>. \<lbrakk>atoms_pltl \<phi> \<subseteq> A \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>); atoms_pltl (X\<^sub>p \<phi>) \<subseteq> A\<rbrakk> \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p X\<^sub>p \<phi>)
 4. \<And>\<phi>1 \<phi>2. \<lbrakk>atoms_pltl \<phi>1 \<subseteq> A \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>1); atoms_pltl \<phi>2 \<subseteq> A \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>2); atoms_pltl (\<phi>1 U\<^sub>p \<phi>2) \<subseteq> A\<rbrakk> \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>1 U\<^sub>p \<phi>2)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>x. atoms_pltl atom\<^sub>p(x) \<subseteq> A \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p atom\<^sub>p(x))
 2. \<And>\<phi>1 \<phi>2. \<lbrakk>atoms_pltl \<phi>1 \<subseteq> A \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>1); atoms_pltl \<phi>2 \<subseteq> A \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>2); atoms_pltl (\<phi>1 implies\<^sub>p \<phi>2) \<subseteq> A\<rbrakk> \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>1 implies\<^sub>p \<phi>2)
 3. \<And>\<phi>. \<lbrakk>atoms_pltl \<phi> \<subseteq> A \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>); atoms_pltl (X\<^sub>p \<phi>) \<subseteq> A\<rbrakk> \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p X\<^sub>p \<phi>)
 4. \<And>\<phi>1 \<phi>2. \<lbrakk>atoms_pltl \<phi>1 \<subseteq> A \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>1); atoms_pltl \<phi>2 \<subseteq> A \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>2); atoms_pltl (\<phi>1 U\<^sub>p \<phi>2) \<subseteq> A\<rbrakk> \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>1 U\<^sub>p \<phi>2)
[PROOF STEP]
fix p
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>x. atoms_pltl atom\<^sub>p(x) \<subseteq> A \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p atom\<^sub>p(x))
 2. \<And>\<phi>1 \<phi>2. \<lbrakk>atoms_pltl \<phi>1 \<subseteq> A \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>1); atoms_pltl \<phi>2 \<subseteq> A \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>2); atoms_pltl (\<phi>1 implies\<^sub>p \<phi>2) \<subseteq> A\<rbrakk> \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>1 implies\<^sub>p \<phi>2)
 3. \<And>\<phi>. \<lbrakk>atoms_pltl \<phi> \<subseteq> A \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>); atoms_pltl (X\<^sub>p \<phi>) \<subseteq> A\<rbrakk> \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p X\<^sub>p \<phi>)
 4. \<And>\<phi>1 \<phi>2. \<lbrakk>atoms_pltl \<phi>1 \<subseteq> A \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>1); atoms_pltl \<phi>2 \<subseteq> A \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>2); atoms_pltl (\<phi>1 U\<^sub>p \<phi>2) \<subseteq> A\<rbrakk> \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>1 U\<^sub>p \<phi>2)
[PROOF STEP]
assume "atoms_pltl (atom\<^sub>p(p)) \<subseteq> A"
[PROOF STATE]
proof (state)
this:
atoms_pltl atom\<^sub>p(p) \<subseteq> A

goal (4 subgoals):
 1. \<And>x. atoms_pltl atom\<^sub>p(x) \<subseteq> A \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p atom\<^sub>p(x))
 2. \<And>\<phi>1 \<phi>2. \<lbrakk>atoms_pltl \<phi>1 \<subseteq> A \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>1); atoms_pltl \<phi>2 \<subseteq> A \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>2); atoms_pltl (\<phi>1 implies\<^sub>p \<phi>2) \<subseteq> A\<rbrakk> \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>1 implies\<^sub>p \<phi>2)
 3. \<And>\<phi>. \<lbrakk>atoms_pltl \<phi> \<subseteq> A \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>); atoms_pltl (X\<^sub>p \<phi>) \<subseteq> A\<rbrakk> \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p X\<^sub>p \<phi>)
 4. \<And>\<phi>1 \<phi>2. \<lbrakk>atoms_pltl \<phi>1 \<subseteq> A \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>1); atoms_pltl \<phi>2 \<subseteq> A \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>2); atoms_pltl (\<phi>1 U\<^sub>p \<phi>2) \<subseteq> A\<rbrakk> \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>1 U\<^sub>p \<phi>2)
[PROOF STEP]
hence "?P (atom\<^sub>p(p)) (atom\<^sub>p(p))"
[PROOF STATE]
proof (prove)
using this:
atoms_pltl atom\<^sub>p(p) \<subseteq> A

goal (1 subgoal):
 1. next_free atom\<^sub>p(p) \<and> atoms_pltl atom\<^sub>p(p) \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p atom\<^sub>p(p) = \<sigma> \<Turnstile>\<^sub>p atom\<^sub>p(p))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
next_free atom\<^sub>p(p) \<and> atoms_pltl atom\<^sub>p(p) \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p atom\<^sub>p(p) = \<sigma> \<Turnstile>\<^sub>p atom\<^sub>p(p))

goal (4 subgoals):
 1. \<And>x. atoms_pltl atom\<^sub>p(x) \<subseteq> A \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p atom\<^sub>p(x))
 2. \<And>\<phi>1 \<phi>2. \<lbrakk>atoms_pltl \<phi>1 \<subseteq> A \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>1); atoms_pltl \<phi>2 \<subseteq> A \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>2); atoms_pltl (\<phi>1 implies\<^sub>p \<phi>2) \<subseteq> A\<rbrakk> \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>1 implies\<^sub>p \<phi>2)
 3. \<And>\<phi>. \<lbrakk>atoms_pltl \<phi> \<subseteq> A \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>); atoms_pltl (X\<^sub>p \<phi>) \<subseteq> A\<rbrakk> \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p X\<^sub>p \<phi>)
 4. \<And>\<phi>1 \<phi>2. \<lbrakk>atoms_pltl \<phi>1 \<subseteq> A \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>1); atoms_pltl \<phi>2 \<subseteq> A \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>2); atoms_pltl (\<phi>1 U\<^sub>p \<phi>2) \<subseteq> A\<rbrakk> \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>1 U\<^sub>p \<phi>2)
[PROOF STEP]
thus "\<exists>\<psi>. ?P (atom\<^sub>p(p)) \<psi>"
[PROOF STATE]
proof (prove)
using this:
next_free atom\<^sub>p(p) \<and> atoms_pltl atom\<^sub>p(p) \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p atom\<^sub>p(p) = \<sigma> \<Turnstile>\<^sub>p atom\<^sub>p(p))

goal (1 subgoal):
 1. \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p atom\<^sub>p(p))
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
\<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p atom\<^sub>p(p))

goal (3 subgoals):
 1. \<And>\<phi>1 \<phi>2. \<lbrakk>atoms_pltl \<phi>1 \<subseteq> A \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>1); atoms_pltl \<phi>2 \<subseteq> A \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>2); atoms_pltl (\<phi>1 implies\<^sub>p \<phi>2) \<subseteq> A\<rbrakk> \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>1 implies\<^sub>p \<phi>2)
 2. \<And>\<phi>. \<lbrakk>atoms_pltl \<phi> \<subseteq> A \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>); atoms_pltl (X\<^sub>p \<phi>) \<subseteq> A\<rbrakk> \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p X\<^sub>p \<phi>)
 3. \<And>\<phi>1 \<phi>2. \<lbrakk>atoms_pltl \<phi>1 \<subseteq> A \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>1); atoms_pltl \<phi>2 \<subseteq> A \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>2); atoms_pltl (\<phi>1 U\<^sub>p \<phi>2) \<subseteq> A\<rbrakk> \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>1 U\<^sub>p \<phi>2)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>\<phi>1 \<phi>2. \<lbrakk>atoms_pltl \<phi>1 \<subseteq> A \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>1); atoms_pltl \<phi>2 \<subseteq> A \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>2); atoms_pltl (\<phi>1 implies\<^sub>p \<phi>2) \<subseteq> A\<rbrakk> \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>1 implies\<^sub>p \<phi>2)
 2. \<And>\<phi>. \<lbrakk>atoms_pltl \<phi> \<subseteq> A \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>); atoms_pltl (X\<^sub>p \<phi>) \<subseteq> A\<rbrakk> \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p X\<^sub>p \<phi>)
 3. \<And>\<phi>1 \<phi>2. \<lbrakk>atoms_pltl \<phi>1 \<subseteq> A \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>1); atoms_pltl \<phi>2 \<subseteq> A \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>2); atoms_pltl (\<phi>1 U\<^sub>p \<phi>2) \<subseteq> A\<rbrakk> \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>1 U\<^sub>p \<phi>2)
[PROOF STEP]
txt \<open>Implication is easy, using the induction hypothesis.\<close>
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>\<phi>1 \<phi>2. \<lbrakk>atoms_pltl \<phi>1 \<subseteq> A \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>1); atoms_pltl \<phi>2 \<subseteq> A \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>2); atoms_pltl (\<phi>1 implies\<^sub>p \<phi>2) \<subseteq> A\<rbrakk> \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>1 implies\<^sub>p \<phi>2)
 2. \<And>\<phi>. \<lbrakk>atoms_pltl \<phi> \<subseteq> A \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>); atoms_pltl (X\<^sub>p \<phi>) \<subseteq> A\<rbrakk> \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p X\<^sub>p \<phi>)
 3. \<And>\<phi>1 \<phi>2. \<lbrakk>atoms_pltl \<phi>1 \<subseteq> A \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>1); atoms_pltl \<phi>2 \<subseteq> A \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>2); atoms_pltl (\<phi>1 U\<^sub>p \<phi>2) \<subseteq> A\<rbrakk> \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>1 U\<^sub>p \<phi>2)
[PROOF STEP]
fix \<phi> \<psi>
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>\<phi>1 \<phi>2. \<lbrakk>atoms_pltl \<phi>1 \<subseteq> A \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>1); atoms_pltl \<phi>2 \<subseteq> A \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>2); atoms_pltl (\<phi>1 implies\<^sub>p \<phi>2) \<subseteq> A\<rbrakk> \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>1 implies\<^sub>p \<phi>2)
 2. \<And>\<phi>. \<lbrakk>atoms_pltl \<phi> \<subseteq> A \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>); atoms_pltl (X\<^sub>p \<phi>) \<subseteq> A\<rbrakk> \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p X\<^sub>p \<phi>)
 3. \<And>\<phi>1 \<phi>2. \<lbrakk>atoms_pltl \<phi>1 \<subseteq> A \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>1); atoms_pltl \<phi>2 \<subseteq> A \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>2); atoms_pltl (\<phi>1 U\<^sub>p \<phi>2) \<subseteq> A\<rbrakk> \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>1 U\<^sub>p \<phi>2)
[PROOF STEP]
assume "atoms_pltl \<phi> \<subseteq> A \<Longrightarrow> \<exists>\<phi>'. ?P \<phi> \<phi>'"
     and "atoms_pltl \<psi> \<subseteq> A \<Longrightarrow> \<exists>\<psi>'. ?P \<psi> \<psi>'"
     and "atoms_pltl (\<phi> implies\<^sub>p \<psi>) \<subseteq> A"
[PROOF STATE]
proof (state)
this:
atoms_pltl \<phi> \<subseteq> A \<Longrightarrow> \<exists>\<phi>''. next_free \<phi>'' \<and> atoms_pltl \<phi>'' \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<phi>'' = \<sigma> \<Turnstile>\<^sub>p \<phi>)
atoms_pltl \<psi> \<subseteq> A \<Longrightarrow> \<exists>\<psi>'. next_free \<psi>' \<and> atoms_pltl \<psi>' \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi>' = \<sigma> \<Turnstile>\<^sub>p \<psi>)
atoms_pltl (\<phi> implies\<^sub>p \<psi>) \<subseteq> A

goal (3 subgoals):
 1. \<And>\<phi>1 \<phi>2. \<lbrakk>atoms_pltl \<phi>1 \<subseteq> A \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>1); atoms_pltl \<phi>2 \<subseteq> A \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>2); atoms_pltl (\<phi>1 implies\<^sub>p \<phi>2) \<subseteq> A\<rbrakk> \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>1 implies\<^sub>p \<phi>2)
 2. \<And>\<phi>. \<lbrakk>atoms_pltl \<phi> \<subseteq> A \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>); atoms_pltl (X\<^sub>p \<phi>) \<subseteq> A\<rbrakk> \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p X\<^sub>p \<phi>)
 3. \<And>\<phi>1 \<phi>2. \<lbrakk>atoms_pltl \<phi>1 \<subseteq> A \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>1); atoms_pltl \<phi>2 \<subseteq> A \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>2); atoms_pltl (\<phi>1 U\<^sub>p \<phi>2) \<subseteq> A\<rbrakk> \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>1 U\<^sub>p \<phi>2)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
atoms_pltl \<phi> \<subseteq> A \<Longrightarrow> \<exists>\<phi>''. next_free \<phi>'' \<and> atoms_pltl \<phi>'' \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<phi>'' = \<sigma> \<Turnstile>\<^sub>p \<phi>)
atoms_pltl \<psi> \<subseteq> A \<Longrightarrow> \<exists>\<psi>'. next_free \<psi>' \<and> atoms_pltl \<psi>' \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi>' = \<sigma> \<Turnstile>\<^sub>p \<psi>)
atoms_pltl (\<phi> implies\<^sub>p \<psi>) \<subseteq> A
[PROOF STEP]
obtain \<phi>' \<psi>' where "?P \<phi> \<phi>'" "?P \<psi> \<psi>'"
[PROOF STATE]
proof (prove)
using this:
atoms_pltl \<phi> \<subseteq> A \<Longrightarrow> \<exists>\<phi>''. next_free \<phi>'' \<and> atoms_pltl \<phi>'' \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<phi>'' = \<sigma> \<Turnstile>\<^sub>p \<phi>)
atoms_pltl \<psi> \<subseteq> A \<Longrightarrow> \<exists>\<psi>'. next_free \<psi>' \<and> atoms_pltl \<psi>' \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi>' = \<sigma> \<Turnstile>\<^sub>p \<psi>)
atoms_pltl (\<phi> implies\<^sub>p \<psi>) \<subseteq> A

goal (1 subgoal):
 1. (\<And>\<phi>'' \<psi>'. \<lbrakk>next_free \<phi>'' \<and> atoms_pltl \<phi>'' \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<phi>'' = \<sigma> \<Turnstile>\<^sub>p \<phi>); next_free \<psi>' \<and> atoms_pltl \<psi>' \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi>' = \<sigma> \<Turnstile>\<^sub>p \<psi>)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
next_free \<phi>' \<and> atoms_pltl \<phi>' \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<phi>' = \<sigma> \<Turnstile>\<^sub>p \<phi>)
next_free \<psi>' \<and> atoms_pltl \<psi>' \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi>' = \<sigma> \<Turnstile>\<^sub>p \<psi>)

goal (3 subgoals):
 1. \<And>\<phi>1 \<phi>2. \<lbrakk>atoms_pltl \<phi>1 \<subseteq> A \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>1); atoms_pltl \<phi>2 \<subseteq> A \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>2); atoms_pltl (\<phi>1 implies\<^sub>p \<phi>2) \<subseteq> A\<rbrakk> \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>1 implies\<^sub>p \<phi>2)
 2. \<And>\<phi>. \<lbrakk>atoms_pltl \<phi> \<subseteq> A \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>); atoms_pltl (X\<^sub>p \<phi>) \<subseteq> A\<rbrakk> \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p X\<^sub>p \<phi>)
 3. \<And>\<phi>1 \<phi>2. \<lbrakk>atoms_pltl \<phi>1 \<subseteq> A \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>1); atoms_pltl \<phi>2 \<subseteq> A \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>2); atoms_pltl (\<phi>1 U\<^sub>p \<phi>2) \<subseteq> A\<rbrakk> \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>1 U\<^sub>p \<phi>2)
[PROOF STEP]
hence "?P (\<phi> implies\<^sub>p \<psi>) (\<phi>' implies\<^sub>p \<psi>')"
[PROOF STATE]
proof (prove)
using this:
next_free \<phi>' \<and> atoms_pltl \<phi>' \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<phi>' = \<sigma> \<Turnstile>\<^sub>p \<phi>)
next_free \<psi>' \<and> atoms_pltl \<psi>' \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi>' = \<sigma> \<Turnstile>\<^sub>p \<psi>)

goal (1 subgoal):
 1. next_free (\<phi>' implies\<^sub>p \<psi>') \<and> atoms_pltl (\<phi>' implies\<^sub>p \<psi>') \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<phi>' implies\<^sub>p \<psi>' = \<sigma> \<Turnstile>\<^sub>p \<phi> implies\<^sub>p \<psi>)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
next_free (\<phi>' implies\<^sub>p \<psi>') \<and> atoms_pltl (\<phi>' implies\<^sub>p \<psi>') \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<phi>' implies\<^sub>p \<psi>' = \<sigma> \<Turnstile>\<^sub>p \<phi> implies\<^sub>p \<psi>)

goal (3 subgoals):
 1. \<And>\<phi>1 \<phi>2. \<lbrakk>atoms_pltl \<phi>1 \<subseteq> A \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>1); atoms_pltl \<phi>2 \<subseteq> A \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>2); atoms_pltl (\<phi>1 implies\<^sub>p \<phi>2) \<subseteq> A\<rbrakk> \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>1 implies\<^sub>p \<phi>2)
 2. \<And>\<phi>. \<lbrakk>atoms_pltl \<phi> \<subseteq> A \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>); atoms_pltl (X\<^sub>p \<phi>) \<subseteq> A\<rbrakk> \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p X\<^sub>p \<phi>)
 3. \<And>\<phi>1 \<phi>2. \<lbrakk>atoms_pltl \<phi>1 \<subseteq> A \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>1); atoms_pltl \<phi>2 \<subseteq> A \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>2); atoms_pltl (\<phi>1 U\<^sub>p \<phi>2) \<subseteq> A\<rbrakk> \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>1 U\<^sub>p \<phi>2)
[PROOF STEP]
thus "\<exists>\<chi>. ?P (\<phi> implies\<^sub>p \<psi>) \<chi>"
[PROOF STATE]
proof (prove)
using this:
next_free (\<phi>' implies\<^sub>p \<psi>') \<and> atoms_pltl (\<phi>' implies\<^sub>p \<psi>') \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<phi>' implies\<^sub>p \<psi>' = \<sigma> \<Turnstile>\<^sub>p \<phi> implies\<^sub>p \<psi>)

goal (1 subgoal):
 1. \<exists>\<chi>. next_free \<chi> \<and> atoms_pltl \<chi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<chi> = \<sigma> \<Turnstile>\<^sub>p \<phi> implies\<^sub>p \<psi>)
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
\<exists>\<chi>. next_free \<chi> \<and> atoms_pltl \<chi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<chi> = \<sigma> \<Turnstile>\<^sub>p \<phi> implies\<^sub>p \<psi>)

goal (2 subgoals):
 1. \<And>\<phi>. \<lbrakk>atoms_pltl \<phi> \<subseteq> A \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>); atoms_pltl (X\<^sub>p \<phi>) \<subseteq> A\<rbrakk> \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p X\<^sub>p \<phi>)
 2. \<And>\<phi>1 \<phi>2. \<lbrakk>atoms_pltl \<phi>1 \<subseteq> A \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>1); atoms_pltl \<phi>2 \<subseteq> A \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>2); atoms_pltl (\<phi>1 U\<^sub>p \<phi>2) \<subseteq> A\<rbrakk> \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>1 U\<^sub>p \<phi>2)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>\<phi>. \<lbrakk>atoms_pltl \<phi> \<subseteq> A \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>); atoms_pltl (X\<^sub>p \<phi>) \<subseteq> A\<rbrakk> \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p X\<^sub>p \<phi>)
 2. \<And>\<phi>1 \<phi>2. \<lbrakk>atoms_pltl \<phi>1 \<subseteq> A \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>1); atoms_pltl \<phi>2 \<subseteq> A \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>2); atoms_pltl (\<phi>1 U\<^sub>p \<phi>2) \<subseteq> A\<rbrakk> \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>1 U\<^sub>p \<phi>2)
[PROOF STEP]
txt \<open>The case of \<open>until\<close> follows similarly.\<close>
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>\<phi>. \<lbrakk>atoms_pltl \<phi> \<subseteq> A \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>); atoms_pltl (X\<^sub>p \<phi>) \<subseteq> A\<rbrakk> \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p X\<^sub>p \<phi>)
 2. \<And>\<phi>1 \<phi>2. \<lbrakk>atoms_pltl \<phi>1 \<subseteq> A \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>1); atoms_pltl \<phi>2 \<subseteq> A \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>2); atoms_pltl (\<phi>1 U\<^sub>p \<phi>2) \<subseteq> A\<rbrakk> \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>1 U\<^sub>p \<phi>2)
[PROOF STEP]
fix \<phi> \<psi>
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>\<phi>. \<lbrakk>atoms_pltl \<phi> \<subseteq> A \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>); atoms_pltl (X\<^sub>p \<phi>) \<subseteq> A\<rbrakk> \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p X\<^sub>p \<phi>)
 2. \<And>\<phi>1 \<phi>2. \<lbrakk>atoms_pltl \<phi>1 \<subseteq> A \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>1); atoms_pltl \<phi>2 \<subseteq> A \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>2); atoms_pltl (\<phi>1 U\<^sub>p \<phi>2) \<subseteq> A\<rbrakk> \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>1 U\<^sub>p \<phi>2)
[PROOF STEP]
assume "atoms_pltl \<phi> \<subseteq> A \<Longrightarrow> \<exists>\<phi>'. ?P \<phi> \<phi>'"
     and "atoms_pltl \<psi> \<subseteq> A \<Longrightarrow> \<exists>\<psi>'. ?P \<psi> \<psi>'"
     and "atoms_pltl (\<phi> U\<^sub>p \<psi>) \<subseteq> A"
[PROOF STATE]
proof (state)
this:
atoms_pltl \<phi> \<subseteq> A \<Longrightarrow> \<exists>\<phi>''. next_free \<phi>'' \<and> atoms_pltl \<phi>'' \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<phi>'' = \<sigma> \<Turnstile>\<^sub>p \<phi>)
atoms_pltl \<psi> \<subseteq> A \<Longrightarrow> \<exists>\<psi>'. next_free \<psi>' \<and> atoms_pltl \<psi>' \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi>' = \<sigma> \<Turnstile>\<^sub>p \<psi>)
atoms_pltl (\<phi> U\<^sub>p \<psi>) \<subseteq> A

goal (2 subgoals):
 1. \<And>\<phi>. \<lbrakk>atoms_pltl \<phi> \<subseteq> A \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>); atoms_pltl (X\<^sub>p \<phi>) \<subseteq> A\<rbrakk> \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p X\<^sub>p \<phi>)
 2. \<And>\<phi>1 \<phi>2. \<lbrakk>atoms_pltl \<phi>1 \<subseteq> A \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>1); atoms_pltl \<phi>2 \<subseteq> A \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>2); atoms_pltl (\<phi>1 U\<^sub>p \<phi>2) \<subseteq> A\<rbrakk> \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>1 U\<^sub>p \<phi>2)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
atoms_pltl \<phi> \<subseteq> A \<Longrightarrow> \<exists>\<phi>''. next_free \<phi>'' \<and> atoms_pltl \<phi>'' \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<phi>'' = \<sigma> \<Turnstile>\<^sub>p \<phi>)
atoms_pltl \<psi> \<subseteq> A \<Longrightarrow> \<exists>\<psi>'. next_free \<psi>' \<and> atoms_pltl \<psi>' \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi>' = \<sigma> \<Turnstile>\<^sub>p \<psi>)
atoms_pltl (\<phi> U\<^sub>p \<psi>) \<subseteq> A
[PROOF STEP]
obtain \<phi>' \<psi>' where 1: "?P \<phi> \<phi>'" and 2: "?P \<psi> \<psi>'"
[PROOF STATE]
proof (prove)
using this:
atoms_pltl \<phi> \<subseteq> A \<Longrightarrow> \<exists>\<phi>''. next_free \<phi>'' \<and> atoms_pltl \<phi>'' \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<phi>'' = \<sigma> \<Turnstile>\<^sub>p \<phi>)
atoms_pltl \<psi> \<subseteq> A \<Longrightarrow> \<exists>\<psi>'. next_free \<psi>' \<and> atoms_pltl \<psi>' \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi>' = \<sigma> \<Turnstile>\<^sub>p \<psi>)
atoms_pltl (\<phi> U\<^sub>p \<psi>) \<subseteq> A

goal (1 subgoal):
 1. (\<And>\<phi>'' \<psi>'. \<lbrakk>next_free \<phi>'' \<and> atoms_pltl \<phi>'' \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<phi>'' = \<sigma> \<Turnstile>\<^sub>p \<phi>); next_free \<psi>' \<and> atoms_pltl \<psi>' \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi>' = \<sigma> \<Turnstile>\<^sub>p \<psi>)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
next_free \<phi>' \<and> atoms_pltl \<phi>' \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<phi>' = \<sigma> \<Turnstile>\<^sub>p \<phi>)
next_free \<psi>' \<and> atoms_pltl \<psi>' \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi>' = \<sigma> \<Turnstile>\<^sub>p \<psi>)

goal (2 subgoals):
 1. \<And>\<phi>. \<lbrakk>atoms_pltl \<phi> \<subseteq> A \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>); atoms_pltl (X\<^sub>p \<phi>) \<subseteq> A\<rbrakk> \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p X\<^sub>p \<phi>)
 2. \<And>\<phi>1 \<phi>2. \<lbrakk>atoms_pltl \<phi>1 \<subseteq> A \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>1); atoms_pltl \<phi>2 \<subseteq> A \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>2); atoms_pltl (\<phi>1 U\<^sub>p \<phi>2) \<subseteq> A\<rbrakk> \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>1 U\<^sub>p \<phi>2)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
next_free \<phi>' \<and> atoms_pltl \<phi>' \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<phi>' = \<sigma> \<Turnstile>\<^sub>p \<phi>)
next_free \<psi>' \<and> atoms_pltl \<psi>' \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi>' = \<sigma> \<Turnstile>\<^sub>p \<psi>)

goal (2 subgoals):
 1. \<And>\<phi>. \<lbrakk>atoms_pltl \<phi> \<subseteq> A \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>); atoms_pltl (X\<^sub>p \<phi>) \<subseteq> A\<rbrakk> \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p X\<^sub>p \<phi>)
 2. \<And>\<phi>1 \<phi>2. \<lbrakk>atoms_pltl \<phi>1 \<subseteq> A \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>1); atoms_pltl \<phi>2 \<subseteq> A \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>2); atoms_pltl (\<phi>1 U\<^sub>p \<phi>2) \<subseteq> A\<rbrakk> \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>1 U\<^sub>p \<phi>2)
[PROOF STEP]
fix \<sigma>
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>\<phi>. \<lbrakk>atoms_pltl \<phi> \<subseteq> A \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>); atoms_pltl (X\<^sub>p \<phi>) \<subseteq> A\<rbrakk> \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p X\<^sub>p \<phi>)
 2. \<And>\<phi>1 \<phi>2. \<lbrakk>atoms_pltl \<phi>1 \<subseteq> A \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>1); atoms_pltl \<phi>2 \<subseteq> A \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>2); atoms_pltl (\<phi>1 U\<^sub>p \<phi>2) \<subseteq> A\<rbrakk> \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>1 U\<^sub>p \<phi>2)
[PROOF STEP]
assume sigma: "stutter_free \<sigma>" "canonical_sequence A \<sigma>"
[PROOF STATE]
proof (state)
this:
stutter_free \<sigma>
canonical_sequence A \<sigma>

goal (2 subgoals):
 1. \<And>\<phi>. \<lbrakk>atoms_pltl \<phi> \<subseteq> A \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>); atoms_pltl (X\<^sub>p \<phi>) \<subseteq> A\<rbrakk> \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p X\<^sub>p \<phi>)
 2. \<And>\<phi>1 \<phi>2. \<lbrakk>atoms_pltl \<phi>1 \<subseteq> A \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>1); atoms_pltl \<phi>2 \<subseteq> A \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>2); atoms_pltl (\<phi>1 U\<^sub>p \<phi>2) \<subseteq> A\<rbrakk> \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>1 U\<^sub>p \<phi>2)
[PROOF STEP]
hence "\<And>k. stutter_free (\<sigma>[k..])" "\<And>k. canonical_sequence A (\<sigma>[k..])"
[PROOF STATE]
proof (prove)
using this:
stutter_free \<sigma>
canonical_sequence A \<sigma>

goal (1 subgoal):
 1. (\<And>k. stutter_free \<sigma> [k..]) &&& (\<And>k. canonical_sequence A \<sigma> [k..])
[PROOF STEP]
by (auto simp: stutter_free_suffix canonical_suffix)
[PROOF STATE]
proof (state)
this:
stutter_free \<sigma> [?k..]
canonical_sequence A \<sigma> [?k..]

goal (2 subgoals):
 1. \<And>\<phi>. \<lbrakk>atoms_pltl \<phi> \<subseteq> A \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>); atoms_pltl (X\<^sub>p \<phi>) \<subseteq> A\<rbrakk> \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p X\<^sub>p \<phi>)
 2. \<And>\<phi>1 \<phi>2. \<lbrakk>atoms_pltl \<phi>1 \<subseteq> A \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>1); atoms_pltl \<phi>2 \<subseteq> A \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>2); atoms_pltl (\<phi>1 U\<^sub>p \<phi>2) \<subseteq> A\<rbrakk> \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>1 U\<^sub>p \<phi>2)
[PROOF STEP]
with 1 2
[PROOF STATE]
proof (chain)
picking this:
next_free \<phi>' \<and> atoms_pltl \<phi>' \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<phi>' = \<sigma> \<Turnstile>\<^sub>p \<phi>)
next_free \<psi>' \<and> atoms_pltl \<psi>' \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi>' = \<sigma> \<Turnstile>\<^sub>p \<psi>)
stutter_free \<sigma> [?k..]
canonical_sequence A \<sigma> [?k..]
[PROOF STEP]
have "\<And>k. (\<sigma>[k..] \<Turnstile>\<^sub>p \<phi>') = (\<sigma>[k..] \<Turnstile>\<^sub>p \<phi>)"
     and "\<And>k. (\<sigma>[k..] \<Turnstile>\<^sub>p \<psi>') = (\<sigma>[k..] \<Turnstile>\<^sub>p \<psi>)"
[PROOF STATE]
proof (prove)
using this:
next_free \<phi>' \<and> atoms_pltl \<phi>' \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<phi>' = \<sigma> \<Turnstile>\<^sub>p \<phi>)
next_free \<psi>' \<and> atoms_pltl \<psi>' \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi>' = \<sigma> \<Turnstile>\<^sub>p \<psi>)
stutter_free \<sigma> [?k..]
canonical_sequence A \<sigma> [?k..]

goal (1 subgoal):
 1. (\<And>k. \<sigma> [k..] \<Turnstile>\<^sub>p \<phi>' = \<sigma> [k..] \<Turnstile>\<^sub>p \<phi>) &&& (\<And>k. \<sigma> [k..] \<Turnstile>\<^sub>p \<psi>' = \<sigma> [k..] \<Turnstile>\<^sub>p \<psi>)
[PROOF STEP]
by (blast+)
[PROOF STATE]
proof (state)
this:
\<sigma> [?k..] \<Turnstile>\<^sub>p \<phi>' = \<sigma> [?k..] \<Turnstile>\<^sub>p \<phi>
\<sigma> [?k..] \<Turnstile>\<^sub>p \<psi>' = \<sigma> [?k..] \<Turnstile>\<^sub>p \<psi>

goal (2 subgoals):
 1. \<And>\<phi>. \<lbrakk>atoms_pltl \<phi> \<subseteq> A \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>); atoms_pltl (X\<^sub>p \<phi>) \<subseteq> A\<rbrakk> \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p X\<^sub>p \<phi>)
 2. \<And>\<phi>1 \<phi>2. \<lbrakk>atoms_pltl \<phi>1 \<subseteq> A \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>1); atoms_pltl \<phi>2 \<subseteq> A \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>2); atoms_pltl (\<phi>1 U\<^sub>p \<phi>2) \<subseteq> A\<rbrakk> \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>1 U\<^sub>p \<phi>2)
[PROOF STEP]
hence "(\<sigma> \<Turnstile>\<^sub>p \<phi>' U\<^sub>p \<psi>') = (\<sigma> \<Turnstile>\<^sub>p \<phi> U\<^sub>p \<psi>)"
[PROOF STATE]
proof (prove)
using this:
\<sigma> [?k..] \<Turnstile>\<^sub>p \<phi>' = \<sigma> [?k..] \<Turnstile>\<^sub>p \<phi>
\<sigma> [?k..] \<Turnstile>\<^sub>p \<psi>' = \<sigma> [?k..] \<Turnstile>\<^sub>p \<psi>

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

goal (2 subgoals):
 1. \<And>\<phi>. \<lbrakk>atoms_pltl \<phi> \<subseteq> A \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>); atoms_pltl (X\<^sub>p \<phi>) \<subseteq> A\<rbrakk> \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p X\<^sub>p \<phi>)
 2. \<And>\<phi>1 \<phi>2. \<lbrakk>atoms_pltl \<phi>1 \<subseteq> A \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>1); atoms_pltl \<phi>2 \<subseteq> A \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>2); atoms_pltl (\<phi>1 U\<^sub>p \<phi>2) \<subseteq> A\<rbrakk> \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>1 U\<^sub>p \<phi>2)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>stutter_free ?\<sigma>2; canonical_sequence A ?\<sigma>2\<rbrakk> \<Longrightarrow> ?\<sigma>2 \<Turnstile>\<^sub>p \<phi>' U\<^sub>p \<psi>' = ?\<sigma>2 \<Turnstile>\<^sub>p \<phi> U\<^sub>p \<psi>

goal (2 subgoals):
 1. \<And>\<phi>. \<lbrakk>atoms_pltl \<phi> \<subseteq> A \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>); atoms_pltl (X\<^sub>p \<phi>) \<subseteq> A\<rbrakk> \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p X\<^sub>p \<phi>)
 2. \<And>\<phi>1 \<phi>2. \<lbrakk>atoms_pltl \<phi>1 \<subseteq> A \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>1); atoms_pltl \<phi>2 \<subseteq> A \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>2); atoms_pltl (\<phi>1 U\<^sub>p \<phi>2) \<subseteq> A\<rbrakk> \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>1 U\<^sub>p \<phi>2)
[PROOF STEP]
with 1 2
[PROOF STATE]
proof (chain)
picking this:
next_free \<phi>' \<and> atoms_pltl \<phi>' \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<phi>' = \<sigma> \<Turnstile>\<^sub>p \<phi>)
next_free \<psi>' \<and> atoms_pltl \<psi>' \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi>' = \<sigma> \<Turnstile>\<^sub>p \<psi>)
\<lbrakk>stutter_free ?\<sigma>2; canonical_sequence A ?\<sigma>2\<rbrakk> \<Longrightarrow> ?\<sigma>2 \<Turnstile>\<^sub>p \<phi>' U\<^sub>p \<psi>' = ?\<sigma>2 \<Turnstile>\<^sub>p \<phi> U\<^sub>p \<psi>
[PROOF STEP]
have "?P (\<phi> U\<^sub>p \<psi>) (\<phi>' U\<^sub>p \<psi>')"
[PROOF STATE]
proof (prove)
using this:
next_free \<phi>' \<and> atoms_pltl \<phi>' \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<phi>' = \<sigma> \<Turnstile>\<^sub>p \<phi>)
next_free \<psi>' \<and> atoms_pltl \<psi>' \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi>' = \<sigma> \<Turnstile>\<^sub>p \<psi>)
\<lbrakk>stutter_free ?\<sigma>2; canonical_sequence A ?\<sigma>2\<rbrakk> \<Longrightarrow> ?\<sigma>2 \<Turnstile>\<^sub>p \<phi>' U\<^sub>p \<psi>' = ?\<sigma>2 \<Turnstile>\<^sub>p \<phi> U\<^sub>p \<psi>

goal (1 subgoal):
 1. next_free (\<phi>' U\<^sub>p \<psi>') \<and> atoms_pltl (\<phi>' U\<^sub>p \<psi>') \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<phi>' U\<^sub>p \<psi>' = \<sigma> \<Turnstile>\<^sub>p \<phi> U\<^sub>p \<psi>)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
next_free (\<phi>' U\<^sub>p \<psi>') \<and> atoms_pltl (\<phi>' U\<^sub>p \<psi>') \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<phi>' U\<^sub>p \<psi>' = \<sigma> \<Turnstile>\<^sub>p \<phi> U\<^sub>p \<psi>)

goal (2 subgoals):
 1. \<And>\<phi>. \<lbrakk>atoms_pltl \<phi> \<subseteq> A \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>); atoms_pltl (X\<^sub>p \<phi>) \<subseteq> A\<rbrakk> \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p X\<^sub>p \<phi>)
 2. \<And>\<phi>1 \<phi>2. \<lbrakk>atoms_pltl \<phi>1 \<subseteq> A \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>1); atoms_pltl \<phi>2 \<subseteq> A \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>2); atoms_pltl (\<phi>1 U\<^sub>p \<phi>2) \<subseteq> A\<rbrakk> \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>1 U\<^sub>p \<phi>2)
[PROOF STEP]
thus "\<exists>\<chi>. ?P (\<phi> U\<^sub>p \<psi>) \<chi>"
[PROOF STATE]
proof (prove)
using this:
next_free (\<phi>' U\<^sub>p \<psi>') \<and> atoms_pltl (\<phi>' U\<^sub>p \<psi>') \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<phi>' U\<^sub>p \<psi>' = \<sigma> \<Turnstile>\<^sub>p \<phi> U\<^sub>p \<psi>)

goal (1 subgoal):
 1. \<exists>\<chi>. next_free \<chi> \<and> atoms_pltl \<chi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<chi> = \<sigma> \<Turnstile>\<^sub>p \<phi> U\<^sub>p \<psi>)
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
\<exists>\<chi>. next_free \<chi> \<and> atoms_pltl \<chi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<chi> = \<sigma> \<Turnstile>\<^sub>p \<phi> U\<^sub>p \<psi>)

goal (1 subgoal):
 1. \<And>\<phi>. \<lbrakk>atoms_pltl \<phi> \<subseteq> A \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>); atoms_pltl (X\<^sub>p \<phi>) \<subseteq> A\<rbrakk> \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p X\<^sub>p \<phi>)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>\<phi>. \<lbrakk>atoms_pltl \<phi> \<subseteq> A \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>); atoms_pltl (X\<^sub>p \<phi>) \<subseteq> A\<rbrakk> \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p X\<^sub>p \<phi>)
[PROOF STEP]
txt \<open>The interesting case is the one of the \<open>next\<close>-operator.\<close>
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>\<phi>. \<lbrakk>atoms_pltl \<phi> \<subseteq> A \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>); atoms_pltl (X\<^sub>p \<phi>) \<subseteq> A\<rbrakk> \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p X\<^sub>p \<phi>)
[PROOF STEP]
fix \<phi>
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>\<phi>. \<lbrakk>atoms_pltl \<phi> \<subseteq> A \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>); atoms_pltl (X\<^sub>p \<phi>) \<subseteq> A\<rbrakk> \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p X\<^sub>p \<phi>)
[PROOF STEP]
assume ih: "atoms_pltl \<phi> \<subseteq> A \<Longrightarrow> \<exists>\<psi>. ?P \<phi> \<psi>" and at: "atoms_pltl (X\<^sub>p \<phi>) \<subseteq> A"
[PROOF STATE]
proof (state)
this:
atoms_pltl \<phi> \<subseteq> A \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>)
atoms_pltl (X\<^sub>p \<phi>) \<subseteq> A

goal (1 subgoal):
 1. \<And>\<phi>. \<lbrakk>atoms_pltl \<phi> \<subseteq> A \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>); atoms_pltl (X\<^sub>p \<phi>) \<subseteq> A\<rbrakk> \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p X\<^sub>p \<phi>)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
atoms_pltl \<phi> \<subseteq> A \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>)
atoms_pltl (X\<^sub>p \<phi>) \<subseteq> A
[PROOF STEP]
obtain \<psi> where psi: "?P \<phi> \<psi>"
[PROOF STATE]
proof (prove)
using this:
atoms_pltl \<phi> \<subseteq> A \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>)
atoms_pltl (X\<^sub>p \<phi>) \<subseteq> A

goal (1 subgoal):
 1. (\<And>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>)

goal (1 subgoal):
 1. \<And>\<phi>. \<lbrakk>atoms_pltl \<phi> \<subseteq> A \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>); atoms_pltl (X\<^sub>p \<phi>) \<subseteq> A\<rbrakk> \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p X\<^sub>p \<phi>)
[PROOF STEP]
txt \<open>A valuation (over \<open>A\<close>) is a set \<open>val \<subseteq> A\<close> of atoms. We
    define some auxiliary notions: the valuation corresponding to a state and
    the characteristic formula for a valuation. Finally, we define the formula
    \<open>psi'\<close> that we will prove to be equivalent to \<open>X\<^sub>p \<phi>\<close> over
    the stutter-free and canonical sequence \<open>\<sigma>\<close>.\<close>
[PROOF STATE]
proof (state)
this:
next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>)

goal (1 subgoal):
 1. \<And>\<phi>. \<lbrakk>atoms_pltl \<phi> \<subseteq> A \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>); atoms_pltl (X\<^sub>p \<phi>) \<subseteq> A\<rbrakk> \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p X\<^sub>p \<phi>)
[PROOF STEP]
define stval where "stval = (\<lambda>s. { p \<in> A . p s })"
[PROOF STATE]
proof (state)
this:
stval = (\<lambda>s. {p \<in> A. p s})

goal (1 subgoal):
 1. \<And>\<phi>. \<lbrakk>atoms_pltl \<phi> \<subseteq> A \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>); atoms_pltl (X\<^sub>p \<phi>) \<subseteq> A\<rbrakk> \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p X\<^sub>p \<phi>)
[PROOF STEP]
define chi where "chi = (\<lambda>val. ((AND {atom\<^sub>p(p) | p . p \<in> val}) and\<^sub>p
                        (AND {not\<^sub>p (atom\<^sub>p(p)) | p . p \<in> A - val})))"
[PROOF STATE]
proof (state)
this:
chi = (\<lambda>val. AND {atom\<^sub>p(p) |p. p \<in> val} and\<^sub>p AND {not\<^sub>p atom\<^sub>p(p) |p. p \<in> A - val})

goal (1 subgoal):
 1. \<And>\<phi>. \<lbrakk>atoms_pltl \<phi> \<subseteq> A \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>); atoms_pltl (X\<^sub>p \<phi>) \<subseteq> A\<rbrakk> \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p X\<^sub>p \<phi>)
[PROOF STEP]
define psi' where "psi' = ((\<psi> and\<^sub>p (OR {G\<^sub>p (chi val) | val . val \<subseteq> A })) or\<^sub>p
                  (OR {(chi val) and\<^sub>p ((chi val) U\<^sub>p ( \<psi> and\<^sub>p (chi val'))) | val val'.
                        val \<subseteq> A \<and> val' \<subseteq> A \<and> val' \<noteq> val }))"
        (is "_ = (( _ and\<^sub>p (OR ?ALW)) or\<^sub>p (OR ?UNT))")
[PROOF STATE]
proof (state)
this:
psi' = \<psi> and\<^sub>p OR {G\<^sub>p chi val |val. val \<subseteq> A} or\<^sub>p OR {chi val and\<^sub>p chi val U\<^sub>p (\<psi> and\<^sub>p chi val') |val val'. val \<subseteq> A \<and> val' \<subseteq> A \<and> val' \<noteq> val}

goal (1 subgoal):
 1. \<And>\<phi>. \<lbrakk>atoms_pltl \<phi> \<subseteq> A \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>); atoms_pltl (X\<^sub>p \<phi>) \<subseteq> A\<rbrakk> \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p X\<^sub>p \<phi>)
[PROOF STEP]
have "\<And>s. {not\<^sub>p (atom\<^sub>p(p)) | p . p \<in> A - stval s}
           = {not\<^sub>p (atom\<^sub>p(p)) | p . p \<in> A \<and> \<not>(p s)}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s. {not\<^sub>p atom\<^sub>p(p) |p. p \<in> A - stval s} = {not\<^sub>p atom\<^sub>p(p) |p. p \<in> A \<and> \<not> p s}
[PROOF STEP]
by (auto simp: stval_def)
[PROOF STATE]
proof (state)
this:
{not\<^sub>p atom\<^sub>p(p) |p. p \<in> A - stval ?s} = {not\<^sub>p atom\<^sub>p(p) |p. p \<in> A \<and> \<not> p ?s}

goal (1 subgoal):
 1. \<And>\<phi>. \<lbrakk>atoms_pltl \<phi> \<subseteq> A \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>); atoms_pltl (X\<^sub>p \<phi>) \<subseteq> A\<rbrakk> \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p X\<^sub>p \<phi>)
[PROOF STEP]
hence chi1: "\<And>s. chi (stval s) = characteristic_formula A s"
[PROOF STATE]
proof (prove)
using this:
{not\<^sub>p atom\<^sub>p(p) |p. p \<in> A - stval ?s} = {not\<^sub>p atom\<^sub>p(p) |p. p \<in> A \<and> \<not> p ?s}

goal (1 subgoal):
 1. \<And>s. chi (stval s) = characteristic_formula A s
[PROOF STEP]
by (auto simp: chi_def stval_def characteristic_formula_def)
[PROOF STATE]
proof (state)
this:
chi (stval ?s) = characteristic_formula A ?s

goal (1 subgoal):
 1. \<And>\<phi>. \<lbrakk>atoms_pltl \<phi> \<subseteq> A \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>); atoms_pltl (X\<^sub>p \<phi>) \<subseteq> A\<rbrakk> \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p X\<^sub>p \<phi>)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
chi (stval ?s) = characteristic_formula A ?s

goal (1 subgoal):
 1. \<And>\<phi>. \<lbrakk>atoms_pltl \<phi> \<subseteq> A \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>); atoms_pltl (X\<^sub>p \<phi>) \<subseteq> A\<rbrakk> \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p X\<^sub>p \<phi>)
[PROOF STEP]
fix val \<tau>
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>\<phi>. \<lbrakk>atoms_pltl \<phi> \<subseteq> A \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>); atoms_pltl (X\<^sub>p \<phi>) \<subseteq> A\<rbrakk> \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p X\<^sub>p \<phi>)
[PROOF STEP]
assume val: "val \<subseteq> A" and tau: "\<tau> \<Turnstile>\<^sub>p chi val"
[PROOF STATE]
proof (state)
this:
val \<subseteq> A
\<tau> \<Turnstile>\<^sub>p chi val

goal (1 subgoal):
 1. \<And>\<phi>. \<lbrakk>atoms_pltl \<phi> \<subseteq> A \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>); atoms_pltl (X\<^sub>p \<phi>) \<subseteq> A\<rbrakk> \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p X\<^sub>p \<phi>)
[PROOF STEP]
with fin
[PROOF STATE]
proof (chain)
picking this:
finite A
val \<subseteq> A
\<tau> \<Turnstile>\<^sub>p chi val
[PROOF STEP]
have "val = stval (\<tau> 0)"
[PROOF STATE]
proof (prove)
using this:
finite A
val \<subseteq> A
\<tau> \<Turnstile>\<^sub>p chi val

goal (1 subgoal):
 1. val = stval (\<tau> 0)
[PROOF STEP]
by (auto simp: stval_def chi_def finite_subset)
[PROOF STATE]
proof (state)
this:
val = stval (\<tau> 0)

goal (1 subgoal):
 1. \<And>\<phi>. \<lbrakk>atoms_pltl \<phi> \<subseteq> A \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>); atoms_pltl (X\<^sub>p \<phi>) \<subseteq> A\<rbrakk> \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p X\<^sub>p \<phi>)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>?val2 \<subseteq> A; ?\<tau>2 \<Turnstile>\<^sub>p chi ?val2\<rbrakk> \<Longrightarrow> ?val2 = stval (?\<tau>2 0)

goal (1 subgoal):
 1. \<And>\<phi>. \<lbrakk>atoms_pltl \<phi> \<subseteq> A \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>); atoms_pltl (X\<^sub>p \<phi>) \<subseteq> A\<rbrakk> \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p X\<^sub>p \<phi>)
[PROOF STEP]
note chi2 = this
[PROOF STATE]
proof (state)
this:
\<lbrakk>?val2 \<subseteq> A; ?\<tau>2 \<Turnstile>\<^sub>p chi ?val2\<rbrakk> \<Longrightarrow> ?val2 = stval (?\<tau>2 0)

goal (1 subgoal):
 1. \<And>\<phi>. \<lbrakk>atoms_pltl \<phi> \<subseteq> A \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>); atoms_pltl (X\<^sub>p \<phi>) \<subseteq> A\<rbrakk> \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p X\<^sub>p \<phi>)
[PROOF STEP]
have "?UNT \<subseteq> (\<lambda>(val,val'). (chi val) and\<^sub>p ((chi val) U\<^sub>p (\<psi> and\<^sub>p (chi val'))))
               ` (Pow A \<times> Pow A)"
    (is "_ \<subseteq> ?S")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {chi val and\<^sub>p chi val U\<^sub>p (\<psi> and\<^sub>p chi val') |val val'. val \<subseteq> A \<and> val' \<subseteq> A \<and> val' \<noteq> val} \<subseteq> (\<lambda>(val, val'). chi val and\<^sub>p chi val U\<^sub>p (\<psi> and\<^sub>p chi val')) ` (Pow A \<times> Pow A)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{chi val and\<^sub>p chi val U\<^sub>p (\<psi> and\<^sub>p chi val') |val val'. val \<subseteq> A \<and> val' \<subseteq> A \<and> val' \<noteq> val} \<subseteq> (\<lambda>(val, val'). chi val and\<^sub>p chi val U\<^sub>p (\<psi> and\<^sub>p chi val')) ` (Pow A \<times> Pow A)

goal (1 subgoal):
 1. \<And>\<phi>. \<lbrakk>atoms_pltl \<phi> \<subseteq> A \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>); atoms_pltl (X\<^sub>p \<phi>) \<subseteq> A\<rbrakk> \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p X\<^sub>p \<phi>)
[PROOF STEP]
with fin
[PROOF STATE]
proof (chain)
picking this:
finite A
{chi val and\<^sub>p chi val U\<^sub>p (\<psi> and\<^sub>p chi val') |val val'. val \<subseteq> A \<and> val' \<subseteq> A \<and> val' \<noteq> val} \<subseteq> (\<lambda>(val, val'). chi val and\<^sub>p chi val U\<^sub>p (\<psi> and\<^sub>p chi val')) ` (Pow A \<times> Pow A)
[PROOF STEP]
have fin_UNT: "finite ?UNT"
[PROOF STATE]
proof (prove)
using this:
finite A
{chi val and\<^sub>p chi val U\<^sub>p (\<psi> and\<^sub>p chi val') |val val'. val \<subseteq> A \<and> val' \<subseteq> A \<and> val' \<noteq> val} \<subseteq> (\<lambda>(val, val'). chi val and\<^sub>p chi val U\<^sub>p (\<psi> and\<^sub>p chi val')) ` (Pow A \<times> Pow A)

goal (1 subgoal):
 1. finite {chi val and\<^sub>p chi val U\<^sub>p (\<psi> and\<^sub>p chi val') |val val'. val \<subseteq> A \<and> val' \<subseteq> A \<and> val' \<noteq> val}
[PROOF STEP]
by (auto simp: finite_subset)
[PROOF STATE]
proof (state)
this:
finite {chi val and\<^sub>p chi val U\<^sub>p (\<psi> and\<^sub>p chi val') |val val'. val \<subseteq> A \<and> val' \<subseteq> A \<and> val' \<noteq> val}

goal (1 subgoal):
 1. \<And>\<phi>. \<lbrakk>atoms_pltl \<phi> \<subseteq> A \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>); atoms_pltl (X\<^sub>p \<phi>) \<subseteq> A\<rbrakk> \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p X\<^sub>p \<phi>)
[PROOF STEP]
have nf: "next_free psi'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. next_free psi'
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. next_free psi'
[PROOF STEP]
from fin
[PROOF STATE]
proof (chain)
picking this:
finite A
[PROOF STEP]
have "\<And>val. val \<subseteq> A \<Longrightarrow> next_free (chi val)"
[PROOF STATE]
proof (prove)
using this:
finite A

goal (1 subgoal):
 1. \<And>val. val \<subseteq> A \<Longrightarrow> next_free (chi val)
[PROOF STEP]
by (auto simp: chi_def finite_subset)
[PROOF STATE]
proof (state)
this:
?val \<subseteq> A \<Longrightarrow> next_free (chi ?val)

goal (1 subgoal):
 1. next_free psi'
[PROOF STEP]
with fin fin_UNT psi
[PROOF STATE]
proof (chain)
picking this:
finite A
finite {chi val and\<^sub>p chi val U\<^sub>p (\<psi> and\<^sub>p chi val') |val val'. val \<subseteq> A \<and> val' \<subseteq> A \<and> val' \<noteq> val}
next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>)
?val \<subseteq> A \<Longrightarrow> next_free (chi ?val)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
finite A
finite {chi val and\<^sub>p chi val U\<^sub>p (\<psi> and\<^sub>p chi val') |val val'. val \<subseteq> A \<and> val' \<subseteq> A \<and> val' \<noteq> val}
next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>)
?val \<subseteq> A \<Longrightarrow> next_free (chi ?val)

goal (1 subgoal):
 1. next_free psi'
[PROOF STEP]
by (force simp: psi'_def finite_subset)
[PROOF STATE]
proof (state)
this:
next_free psi'

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
next_free psi'

goal (1 subgoal):
 1. \<And>\<phi>. \<lbrakk>atoms_pltl \<phi> \<subseteq> A \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>); atoms_pltl (X\<^sub>p \<phi>) \<subseteq> A\<rbrakk> \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p X\<^sub>p \<phi>)
[PROOF STEP]
have atoms_pltl: "atoms_pltl psi' \<subseteq> A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. atoms_pltl psi' \<subseteq> A
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. atoms_pltl psi' \<subseteq> A
[PROOF STEP]
from fin
[PROOF STATE]
proof (chain)
picking this:
finite A
[PROOF STEP]
have at_chi: "\<And>val. val \<subseteq> A \<Longrightarrow> atoms_pltl (chi val) \<subseteq> A"
[PROOF STATE]
proof (prove)
using this:
finite A

goal (1 subgoal):
 1. \<And>val. val \<subseteq> A \<Longrightarrow> atoms_pltl (chi val) \<subseteq> A
[PROOF STEP]
by (auto simp: chi_def finite_subset)
[PROOF STATE]
proof (state)
this:
?val \<subseteq> A \<Longrightarrow> atoms_pltl (chi ?val) \<subseteq> A

goal (1 subgoal):
 1. atoms_pltl psi' \<subseteq> A
[PROOF STEP]
with fin psi
[PROOF STATE]
proof (chain)
picking this:
finite A
next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>)
?val \<subseteq> A \<Longrightarrow> atoms_pltl (chi ?val) \<subseteq> A
[PROOF STEP]
have at_alw: "atoms_pltl (\<psi> and\<^sub>p (OR ?ALW)) \<subseteq> A"
[PROOF STATE]
proof (prove)
using this:
finite A
next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>)
?val \<subseteq> A \<Longrightarrow> atoms_pltl (chi ?val) \<subseteq> A

goal (1 subgoal):
 1. atoms_pltl (\<psi> and\<^sub>p OR {G\<^sub>p chi val |val. val \<subseteq> A}) \<subseteq> A
[PROOF STEP]
by auto blast?
[PROOF STATE]
proof (state)
this:
atoms_pltl (\<psi> and\<^sub>p OR {G\<^sub>p chi val |val. val \<subseteq> A}) \<subseteq> A

goal (1 subgoal):
 1. atoms_pltl psi' \<subseteq> A
[PROOF STEP]
(** FRAGILE: auto leaves trivial goal about subset **)
[PROOF STATE]
proof (state)
this:
atoms_pltl (\<psi> and\<^sub>p OR {G\<^sub>p chi val |val. val \<subseteq> A}) \<subseteq> A

goal (1 subgoal):
 1. atoms_pltl psi' \<subseteq> A
[PROOF STEP]
from fin fin_UNT psi at_chi
[PROOF STATE]
proof (chain)
picking this:
finite A
finite {chi val and\<^sub>p chi val U\<^sub>p (\<psi> and\<^sub>p chi val') |val val'. val \<subseteq> A \<and> val' \<subseteq> A \<and> val' \<noteq> val}
next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>)
?val \<subseteq> A \<Longrightarrow> atoms_pltl (chi ?val) \<subseteq> A
[PROOF STEP]
have "atoms_pltl (OR ?UNT) \<subseteq> A"
[PROOF STATE]
proof (prove)
using this:
finite A
finite {chi val and\<^sub>p chi val U\<^sub>p (\<psi> and\<^sub>p chi val') |val val'. val \<subseteq> A \<and> val' \<subseteq> A \<and> val' \<noteq> val}
next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>)
?val \<subseteq> A \<Longrightarrow> atoms_pltl (chi ?val) \<subseteq> A

goal (1 subgoal):
 1. atoms_pltl (OR {chi val and\<^sub>p chi val U\<^sub>p (\<psi> and\<^sub>p chi val') |val val'. val \<subseteq> A \<and> val' \<subseteq> A \<and> val' \<noteq> val}) \<subseteq> A
[PROOF STEP]
by auto (blast+)?
[PROOF STATE]
proof (state)
this:
atoms_pltl (OR {chi val and\<^sub>p chi val U\<^sub>p (\<psi> and\<^sub>p chi val') |val val'. val \<subseteq> A \<and> val' \<subseteq> A \<and> val' \<noteq> val}) \<subseteq> A

goal (1 subgoal):
 1. atoms_pltl psi' \<subseteq> A
[PROOF STEP]
(** FRAGILE: even more left-over goals here **)
[PROOF STATE]
proof (state)
this:
atoms_pltl (OR {chi val and\<^sub>p chi val U\<^sub>p (\<psi> and\<^sub>p chi val') |val val'. val \<subseteq> A \<and> val' \<subseteq> A \<and> val' \<noteq> val}) \<subseteq> A

goal (1 subgoal):
 1. atoms_pltl psi' \<subseteq> A
[PROOF STEP]
with at_alw
[PROOF STATE]
proof (chain)
picking this:
atoms_pltl (\<psi> and\<^sub>p OR {G\<^sub>p chi val |val. val \<subseteq> A}) \<subseteq> A
atoms_pltl (OR {chi val and\<^sub>p chi val U\<^sub>p (\<psi> and\<^sub>p chi val') |val val'. val \<subseteq> A \<and> val' \<subseteq> A \<and> val' \<noteq> val}) \<subseteq> A
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
atoms_pltl (\<psi> and\<^sub>p OR {G\<^sub>p chi val |val. val \<subseteq> A}) \<subseteq> A
atoms_pltl (OR {chi val and\<^sub>p chi val U\<^sub>p (\<psi> and\<^sub>p chi val') |val val'. val \<subseteq> A \<and> val' \<subseteq> A \<and> val' \<noteq> val}) \<subseteq> A

goal (1 subgoal):
 1. atoms_pltl psi' \<subseteq> A
[PROOF STEP]
by (auto simp: psi'_def)
[PROOF STATE]
proof (state)
this:
atoms_pltl psi' \<subseteq> A

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
atoms_pltl psi' \<subseteq> A

goal (1 subgoal):
 1. \<And>\<phi>. \<lbrakk>atoms_pltl \<phi> \<subseteq> A \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>); atoms_pltl (X\<^sub>p \<phi>) \<subseteq> A\<rbrakk> \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p X\<^sub>p \<phi>)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
atoms_pltl psi' \<subseteq> A

goal (1 subgoal):
 1. \<And>\<phi>. \<lbrakk>atoms_pltl \<phi> \<subseteq> A \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>); atoms_pltl (X\<^sub>p \<phi>) \<subseteq> A\<rbrakk> \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p X\<^sub>p \<phi>)
[PROOF STEP]
fix \<sigma>
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>\<phi>. \<lbrakk>atoms_pltl \<phi> \<subseteq> A \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>); atoms_pltl (X\<^sub>p \<phi>) \<subseteq> A\<rbrakk> \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p X\<^sub>p \<phi>)
[PROOF STEP]
assume st: "stutter_free \<sigma>" and can: "canonical_sequence A \<sigma>"
[PROOF STATE]
proof (state)
this:
stutter_free \<sigma>
canonical_sequence A \<sigma>

goal (1 subgoal):
 1. \<And>\<phi>. \<lbrakk>atoms_pltl \<phi> \<subseteq> A \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>); atoms_pltl (X\<^sub>p \<phi>) \<subseteq> A\<rbrakk> \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p X\<^sub>p \<phi>)
[PROOF STEP]
have "(\<sigma> \<Turnstile>\<^sub>p X\<^sub>p \<phi>) = (\<sigma> \<Turnstile>\<^sub>p psi')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<sigma> \<Turnstile>\<^sub>p X\<^sub>p \<phi> = \<sigma> \<Turnstile>\<^sub>p psi'
[PROOF STEP]
proof (cases "\<sigma> (Suc 0) = \<sigma> 0")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<sigma> (Suc 0) = \<sigma> 0 \<Longrightarrow> \<sigma> \<Turnstile>\<^sub>p X\<^sub>p \<phi> = \<sigma> \<Turnstile>\<^sub>p psi'
 2. \<sigma> (Suc 0) \<noteq> \<sigma> 0 \<Longrightarrow> \<sigma> \<Turnstile>\<^sub>p X\<^sub>p \<phi> = \<sigma> \<Turnstile>\<^sub>p psi'
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
\<sigma> (Suc 0) = \<sigma> 0

goal (2 subgoals):
 1. \<sigma> (Suc 0) = \<sigma> 0 \<Longrightarrow> \<sigma> \<Turnstile>\<^sub>p X\<^sub>p \<phi> = \<sigma> \<Turnstile>\<^sub>p psi'
 2. \<sigma> (Suc 0) \<noteq> \<sigma> 0 \<Longrightarrow> \<sigma> \<Turnstile>\<^sub>p X\<^sub>p \<phi> = \<sigma> \<Turnstile>\<^sub>p psi'
[PROOF STEP]
txt \<open>In the case of a stuttering transition at the beginning, we must have
        infinite stuttering, and the first disjunct of \<open>psi'\<close> holds,
        whereas the second does not.\<close>
[PROOF STATE]
proof (state)
this:
\<sigma> (Suc 0) = \<sigma> 0

goal (2 subgoals):
 1. \<sigma> (Suc 0) = \<sigma> 0 \<Longrightarrow> \<sigma> \<Turnstile>\<^sub>p X\<^sub>p \<phi> = \<sigma> \<Turnstile>\<^sub>p psi'
 2. \<sigma> (Suc 0) \<noteq> \<sigma> 0 \<Longrightarrow> \<sigma> \<Turnstile>\<^sub>p X\<^sub>p \<phi> = \<sigma> \<Turnstile>\<^sub>p psi'
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
\<sigma> (Suc 0) = \<sigma> 0

goal (2 subgoals):
 1. \<sigma> (Suc 0) = \<sigma> 0 \<Longrightarrow> \<sigma> \<Turnstile>\<^sub>p X\<^sub>p \<phi> = \<sigma> \<Turnstile>\<^sub>p psi'
 2. \<sigma> (Suc 0) \<noteq> \<sigma> 0 \<Longrightarrow> \<sigma> \<Turnstile>\<^sub>p X\<^sub>p \<phi> = \<sigma> \<Turnstile>\<^sub>p psi'
[PROOF STEP]
fix n
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<sigma> (Suc 0) = \<sigma> 0 \<Longrightarrow> \<sigma> \<Turnstile>\<^sub>p X\<^sub>p \<phi> = \<sigma> \<Turnstile>\<^sub>p psi'
 2. \<sigma> (Suc 0) \<noteq> \<sigma> 0 \<Longrightarrow> \<sigma> \<Turnstile>\<^sub>p X\<^sub>p \<phi> = \<sigma> \<Turnstile>\<^sub>p psi'
[PROOF STEP]
have "\<sigma> n = \<sigma> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<sigma> n = \<sigma> 0
[PROOF STEP]
proof (cases n)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. n = 0 \<Longrightarrow> \<sigma> n = \<sigma> 0
 2. \<And>nat. n = Suc nat \<Longrightarrow> \<sigma> n = \<sigma> 0
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:
n = 0

goal (2 subgoals):
 1. n = 0 \<Longrightarrow> \<sigma> n = \<sigma> 0
 2. \<And>nat. n = Suc nat \<Longrightarrow> \<sigma> n = \<sigma> 0
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
n = 0

goal (1 subgoal):
 1. \<sigma> n = \<sigma> 0
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<sigma> n = \<sigma> 0

goal (1 subgoal):
 1. \<And>nat. n = Suc nat \<Longrightarrow> \<sigma> n = \<sigma> 0
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>nat. n = Suc nat \<Longrightarrow> \<sigma> n = \<sigma> 0
[PROOF STEP]
case Suc
[PROOF STATE]
proof (state)
this:
n = Suc nat_

goal (1 subgoal):
 1. \<And>nat. n = Suc nat \<Longrightarrow> \<sigma> n = \<sigma> 0
[PROOF STEP]
hence "n > 0"
[PROOF STATE]
proof (prove)
using this:
n = Suc nat_

goal (1 subgoal):
 1. 0 < n
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
0 < n

goal (1 subgoal):
 1. \<And>nat. n = Suc nat \<Longrightarrow> \<sigma> n = \<sigma> 0
[PROOF STEP]
with True st
[PROOF STATE]
proof (chain)
picking this:
\<sigma> (Suc 0) = \<sigma> 0
stutter_free \<sigma>
0 < n
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<sigma> (Suc 0) = \<sigma> 0
stutter_free \<sigma>
0 < n

goal (1 subgoal):
 1. \<sigma> n = \<sigma> 0
[PROOF STEP]
unfolding stutter_free_def
[PROOF STATE]
proof (prove)
using this:
\<sigma> (Suc 0) = \<sigma> 0
\<forall>k. \<sigma> (Suc k) = \<sigma> k \<longrightarrow> (\<forall>n>k. \<sigma> n = \<sigma> k)
0 < n

goal (1 subgoal):
 1. \<sigma> n = \<sigma> 0
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<sigma> n = \<sigma> 0

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<sigma> n = \<sigma> 0

goal (2 subgoals):
 1. \<sigma> (Suc 0) = \<sigma> 0 \<Longrightarrow> \<sigma> \<Turnstile>\<^sub>p X\<^sub>p \<phi> = \<sigma> \<Turnstile>\<^sub>p psi'
 2. \<sigma> (Suc 0) \<noteq> \<sigma> 0 \<Longrightarrow> \<sigma> \<Turnstile>\<^sub>p X\<^sub>p \<phi> = \<sigma> \<Turnstile>\<^sub>p psi'
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<sigma> ?n2 = \<sigma> 0

goal (2 subgoals):
 1. \<sigma> (Suc 0) = \<sigma> 0 \<Longrightarrow> \<sigma> \<Turnstile>\<^sub>p X\<^sub>p \<phi> = \<sigma> \<Turnstile>\<^sub>p psi'
 2. \<sigma> (Suc 0) \<noteq> \<sigma> 0 \<Longrightarrow> \<sigma> \<Turnstile>\<^sub>p X\<^sub>p \<phi> = \<sigma> \<Turnstile>\<^sub>p psi'
[PROOF STEP]
note alleq = this
[PROOF STATE]
proof (state)
this:
\<sigma> ?n2 = \<sigma> 0

goal (2 subgoals):
 1. \<sigma> (Suc 0) = \<sigma> 0 \<Longrightarrow> \<sigma> \<Turnstile>\<^sub>p X\<^sub>p \<phi> = \<sigma> \<Turnstile>\<^sub>p psi'
 2. \<sigma> (Suc 0) \<noteq> \<sigma> 0 \<Longrightarrow> \<sigma> \<Turnstile>\<^sub>p X\<^sub>p \<phi> = \<sigma> \<Turnstile>\<^sub>p psi'
[PROOF STEP]
have suffix: "\<And>n. \<sigma>[n..] = \<sigma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<sigma> [n..] = \<sigma>
[PROOF STEP]
proof (rule ext)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n x. \<sigma> [n..] x = \<sigma> x
[PROOF STEP]
fix n i
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n x. \<sigma> [n..] x = \<sigma> x
[PROOF STEP]
have "(\<sigma>[n..]) i = \<sigma> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<sigma> [n..] i = \<sigma> 0
[PROOF STEP]
by (auto intro: alleq)
[PROOF STATE]
proof (state)
this:
\<sigma> [n..] i = \<sigma> 0

goal (1 subgoal):
 1. \<And>n x. \<sigma> [n..] x = \<sigma> x
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<sigma> [n..] i = \<sigma> 0

goal (1 subgoal):
 1. \<And>n x. \<sigma> [n..] x = \<sigma> x
[PROOF STEP]
have "\<sigma> i = \<sigma> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<sigma> i = \<sigma> 0
[PROOF STEP]
by (rule alleq)
[PROOF STATE]
proof (state)
this:
\<sigma> i = \<sigma> 0

goal (1 subgoal):
 1. \<And>n x. \<sigma> [n..] x = \<sigma> x
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<sigma> [n..] i = \<sigma> 0
\<sigma> i = \<sigma> 0
[PROOF STEP]
show "(\<sigma>[n..]) i = \<sigma> i"
[PROOF STATE]
proof (prove)
using this:
\<sigma> [n..] i = \<sigma> 0
\<sigma> i = \<sigma> 0

goal (1 subgoal):
 1. \<sigma> [n..] i = \<sigma> i
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<sigma> [n..] i = \<sigma> i

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<sigma> [?n..] = \<sigma>

goal (2 subgoals):
 1. \<sigma> (Suc 0) = \<sigma> 0 \<Longrightarrow> \<sigma> \<Turnstile>\<^sub>p X\<^sub>p \<phi> = \<sigma> \<Turnstile>\<^sub>p psi'
 2. \<sigma> (Suc 0) \<noteq> \<sigma> 0 \<Longrightarrow> \<sigma> \<Turnstile>\<^sub>p X\<^sub>p \<phi> = \<sigma> \<Turnstile>\<^sub>p psi'
[PROOF STEP]
with st can psi
[PROOF STATE]
proof (chain)
picking this:
stutter_free \<sigma>
canonical_sequence A \<sigma>
next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>)
\<sigma> [?n..] = \<sigma>
[PROOF STEP]
have 1: "(\<sigma> \<Turnstile>\<^sub>p X\<^sub>p \<phi>) = (\<sigma> \<Turnstile>\<^sub>p \<psi>)"
[PROOF STATE]
proof (prove)
using this:
stutter_free \<sigma>
canonical_sequence A \<sigma>
next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>)
\<sigma> [?n..] = \<sigma>

goal (1 subgoal):
 1. \<sigma> \<Turnstile>\<^sub>p X\<^sub>p \<phi> = \<sigma> \<Turnstile>\<^sub>p \<psi>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<sigma> \<Turnstile>\<^sub>p X\<^sub>p \<phi> = \<sigma> \<Turnstile>\<^sub>p \<psi>

goal (2 subgoals):
 1. \<sigma> (Suc 0) = \<sigma> 0 \<Longrightarrow> \<sigma> \<Turnstile>\<^sub>p X\<^sub>p \<phi> = \<sigma> \<Turnstile>\<^sub>p psi'
 2. \<sigma> (Suc 0) \<noteq> \<sigma> 0 \<Longrightarrow> \<sigma> \<Turnstile>\<^sub>p X\<^sub>p \<phi> = \<sigma> \<Turnstile>\<^sub>p psi'
[PROOF STEP]
from fin
[PROOF STATE]
proof (chain)
picking this:
finite A
[PROOF STEP]
have "\<sigma> \<Turnstile>\<^sub>p chi (stval (\<sigma> 0))"
[PROOF STATE]
proof (prove)
using this:
finite A

goal (1 subgoal):
 1. \<sigma> \<Turnstile>\<^sub>p chi (stval (\<sigma> 0))
[PROOF STEP]
by (simp add: chi1 characteristic_holds)
[PROOF STATE]
proof (state)
this:
\<sigma> \<Turnstile>\<^sub>p chi (stval (\<sigma> 0))

goal (2 subgoals):
 1. \<sigma> (Suc 0) = \<sigma> 0 \<Longrightarrow> \<sigma> \<Turnstile>\<^sub>p X\<^sub>p \<phi> = \<sigma> \<Turnstile>\<^sub>p psi'
 2. \<sigma> (Suc 0) \<noteq> \<sigma> 0 \<Longrightarrow> \<sigma> \<Turnstile>\<^sub>p X\<^sub>p \<phi> = \<sigma> \<Turnstile>\<^sub>p psi'
[PROOF STEP]
with suffix
[PROOF STATE]
proof (chain)
picking this:
\<sigma> [?n..] = \<sigma>
\<sigma> \<Turnstile>\<^sub>p chi (stval (\<sigma> 0))
[PROOF STEP]
have "\<sigma> \<Turnstile>\<^sub>p G\<^sub>p (chi (stval (\<sigma> 0)))" (is "_ \<Turnstile>\<^sub>p ?alw")
[PROOF STATE]
proof (prove)
using this:
\<sigma> [?n..] = \<sigma>
\<sigma> \<Turnstile>\<^sub>p chi (stval (\<sigma> 0))

goal (1 subgoal):
 1. \<sigma> \<Turnstile>\<^sub>p G\<^sub>p chi (stval (\<sigma> 0))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<sigma> \<Turnstile>\<^sub>p G\<^sub>p chi (stval (\<sigma> 0))

goal (2 subgoals):
 1. \<sigma> (Suc 0) = \<sigma> 0 \<Longrightarrow> \<sigma> \<Turnstile>\<^sub>p X\<^sub>p \<phi> = \<sigma> \<Turnstile>\<^sub>p psi'
 2. \<sigma> (Suc 0) \<noteq> \<sigma> 0 \<Longrightarrow> \<sigma> \<Turnstile>\<^sub>p X\<^sub>p \<phi> = \<sigma> \<Turnstile>\<^sub>p psi'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<sigma> \<Turnstile>\<^sub>p G\<^sub>p chi (stval (\<sigma> 0))

goal (2 subgoals):
 1. \<sigma> (Suc 0) = \<sigma> 0 \<Longrightarrow> \<sigma> \<Turnstile>\<^sub>p X\<^sub>p \<phi> = \<sigma> \<Turnstile>\<^sub>p psi'
 2. \<sigma> (Suc 0) \<noteq> \<sigma> 0 \<Longrightarrow> \<sigma> \<Turnstile>\<^sub>p X\<^sub>p \<phi> = \<sigma> \<Turnstile>\<^sub>p psi'
[PROOF STEP]
have "?alw \<in> ?ALW"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. G\<^sub>p chi (stval (\<sigma> 0)) \<in> {G\<^sub>p chi val |val. val \<subseteq> A}
[PROOF STEP]
by (auto simp: stval_def)
[PROOF STATE]
proof (state)
this:
G\<^sub>p chi (stval (\<sigma> 0)) \<in> {G\<^sub>p chi val |val. val \<subseteq> A}

goal (2 subgoals):
 1. \<sigma> (Suc 0) = \<sigma> 0 \<Longrightarrow> \<sigma> \<Turnstile>\<^sub>p X\<^sub>p \<phi> = \<sigma> \<Turnstile>\<^sub>p psi'
 2. \<sigma> (Suc 0) \<noteq> \<sigma> 0 \<Longrightarrow> \<sigma> \<Turnstile>\<^sub>p X\<^sub>p \<phi> = \<sigma> \<Turnstile>\<^sub>p psi'
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<sigma> \<Turnstile>\<^sub>p G\<^sub>p chi (stval (\<sigma> 0))
G\<^sub>p chi (stval (\<sigma> 0)) \<in> {G\<^sub>p chi val |val. val \<subseteq> A}
[PROOF STEP]
have 2: "\<sigma> \<Turnstile>\<^sub>p OR ?ALW"
[PROOF STATE]
proof (prove)
using this:
\<sigma> \<Turnstile>\<^sub>p G\<^sub>p chi (stval (\<sigma> 0))
G\<^sub>p chi (stval (\<sigma> 0)) \<in> {G\<^sub>p chi val |val. val \<subseteq> A}

goal (1 subgoal):
 1. \<sigma> \<Turnstile>\<^sub>p OR {G\<^sub>p chi val |val. val \<subseteq> A}
[PROOF STEP]
using fin
[PROOF STATE]
proof (prove)
using this:
\<sigma> \<Turnstile>\<^sub>p G\<^sub>p chi (stval (\<sigma> 0))
G\<^sub>p chi (stval (\<sigma> 0)) \<in> {G\<^sub>p chi val |val. val \<subseteq> A}
finite A

goal (1 subgoal):
 1. \<sigma> \<Turnstile>\<^sub>p OR {G\<^sub>p chi val |val. val \<subseteq> A}
[PROOF STEP]
by (auto simp: finite_subset simp del: semantics_pltl_sugar)
[PROOF STATE]
proof (state)
this:
\<sigma> \<Turnstile>\<^sub>p OR {G\<^sub>p chi val |val. val \<subseteq> A}

goal (2 subgoals):
 1. \<sigma> (Suc 0) = \<sigma> 0 \<Longrightarrow> \<sigma> \<Turnstile>\<^sub>p X\<^sub>p \<phi> = \<sigma> \<Turnstile>\<^sub>p psi'
 2. \<sigma> (Suc 0) \<noteq> \<sigma> 0 \<Longrightarrow> \<sigma> \<Turnstile>\<^sub>p X\<^sub>p \<phi> = \<sigma> \<Turnstile>\<^sub>p psi'
[PROOF STEP]
have 3: "\<not>(\<sigma> \<Turnstile>\<^sub>p OR ?UNT)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> \<sigma> \<Turnstile>\<^sub>p OR {chi val and\<^sub>p chi val U\<^sub>p (\<psi> and\<^sub>p chi val') |val val'. val \<subseteq> A \<and> val' \<subseteq> A \<and> val' \<noteq> val}
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<sigma> \<Turnstile>\<^sub>p OR {chi val and\<^sub>p chi val U\<^sub>p (\<psi> and\<^sub>p chi val') |val val'. val \<subseteq> A \<and> val' \<subseteq> A \<and> val' \<noteq> val} \<Longrightarrow> False
[PROOF STEP]
assume unt: "\<sigma> \<Turnstile>\<^sub>p OR ?UNT"
[PROOF STATE]
proof (state)
this:
\<sigma> \<Turnstile>\<^sub>p OR {chi val and\<^sub>p chi val U\<^sub>p (\<psi> and\<^sub>p chi val') |val val'. val \<subseteq> A \<and> val' \<subseteq> A \<and> val' \<noteq> val}

goal (1 subgoal):
 1. \<sigma> \<Turnstile>\<^sub>p OR {chi val and\<^sub>p chi val U\<^sub>p (\<psi> and\<^sub>p chi val') |val val'. val \<subseteq> A \<and> val' \<subseteq> A \<and> val' \<noteq> val} \<Longrightarrow> False
[PROOF STEP]
with fin_UNT
[PROOF STATE]
proof (chain)
picking this:
finite {chi val and\<^sub>p chi val U\<^sub>p (\<psi> and\<^sub>p chi val') |val val'. val \<subseteq> A \<and> val' \<subseteq> A \<and> val' \<noteq> val}
\<sigma> \<Turnstile>\<^sub>p OR {chi val and\<^sub>p chi val U\<^sub>p (\<psi> and\<^sub>p chi val') |val val'. val \<subseteq> A \<and> val' \<subseteq> A \<and> val' \<noteq> val}
[PROOF STEP]
obtain val val' k where
          val: "val \<subseteq> A" "val' \<subseteq> A" "val' \<noteq> val" and
          now: "\<sigma> \<Turnstile>\<^sub>p chi val" and k: "\<sigma>[k..] \<Turnstile>\<^sub>p chi val'"
[PROOF STATE]
proof (prove)
using this:
finite {chi val and\<^sub>p chi val U\<^sub>p (\<psi> and\<^sub>p chi val') |val val'. val \<subseteq> A \<and> val' \<subseteq> A \<and> val' \<noteq> val}
\<sigma> \<Turnstile>\<^sub>p OR {chi val and\<^sub>p chi val U\<^sub>p (\<psi> and\<^sub>p chi val') |val val'. val \<subseteq> A \<and> val' \<subseteq> A \<and> val' \<noteq> val}

goal (1 subgoal):
 1. (\<And>val val' k. \<lbrakk>val \<subseteq> A; val' \<subseteq> A; val' \<noteq> val; \<sigma> \<Turnstile>\<^sub>p chi val; \<sigma> [k..] \<Turnstile>\<^sub>p chi val'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto (blast+)?
[PROOF STATE]
proof (state)
this:
val \<subseteq> A
val' \<subseteq> A
val' \<noteq> val
\<sigma> \<Turnstile>\<^sub>p chi val
\<sigma> [k..] \<Turnstile>\<^sub>p chi val'

goal (1 subgoal):
 1. \<sigma> \<Turnstile>\<^sub>p OR {chi val and\<^sub>p chi val U\<^sub>p (\<psi> and\<^sub>p chi val') |val val'. val \<subseteq> A \<and> val' \<subseteq> A \<and> val' \<noteq> val} \<Longrightarrow> False
[PROOF STEP]
(* FRAGILE: similar as above *)
[PROOF STATE]
proof (state)
this:
val \<subseteq> A
val' \<subseteq> A
val' \<noteq> val
\<sigma> \<Turnstile>\<^sub>p chi val
\<sigma> [k..] \<Turnstile>\<^sub>p chi val'

goal (1 subgoal):
 1. \<sigma> \<Turnstile>\<^sub>p OR {chi val and\<^sub>p chi val U\<^sub>p (\<psi> and\<^sub>p chi val') |val val'. val \<subseteq> A \<and> val' \<subseteq> A \<and> val' \<noteq> val} \<Longrightarrow> False
[PROOF STEP]
from \<open>val \<subseteq> A\<close> now
[PROOF STATE]
proof (chain)
picking this:
val \<subseteq> A
\<sigma> \<Turnstile>\<^sub>p chi val
[PROOF STEP]
have "val = stval (\<sigma> 0)"
[PROOF STATE]
proof (prove)
using this:
val \<subseteq> A
\<sigma> \<Turnstile>\<^sub>p chi val

goal (1 subgoal):
 1. val = stval (\<sigma> 0)
[PROOF STEP]
by (rule chi2)
[PROOF STATE]
proof (state)
this:
val = stval (\<sigma> 0)

goal (1 subgoal):
 1. \<sigma> \<Turnstile>\<^sub>p OR {chi val and\<^sub>p chi val U\<^sub>p (\<psi> and\<^sub>p chi val') |val val'. val \<subseteq> A \<and> val' \<subseteq> A \<and> val' \<noteq> val} \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
val = stval (\<sigma> 0)

goal (1 subgoal):
 1. \<sigma> \<Turnstile>\<^sub>p OR {chi val and\<^sub>p chi val U\<^sub>p (\<psi> and\<^sub>p chi val') |val val'. val \<subseteq> A \<and> val' \<subseteq> A \<and> val' \<noteq> val} \<Longrightarrow> False
[PROOF STEP]
from \<open>val' \<subseteq> A\<close> k suffix
[PROOF STATE]
proof (chain)
picking this:
val' \<subseteq> A
\<sigma> [k..] \<Turnstile>\<^sub>p chi val'
\<sigma> [?n..] = \<sigma>
[PROOF STEP]
have "val' = stval (\<sigma> 0)"
[PROOF STATE]
proof (prove)
using this:
val' \<subseteq> A
\<sigma> [k..] \<Turnstile>\<^sub>p chi val'
\<sigma> [?n..] = \<sigma>

goal (1 subgoal):
 1. val' = stval (\<sigma> 0)
[PROOF STEP]
by (simp add: chi2)
[PROOF STATE]
proof (state)
this:
val' = stval (\<sigma> 0)

goal (1 subgoal):
 1. \<sigma> \<Turnstile>\<^sub>p OR {chi val and\<^sub>p chi val U\<^sub>p (\<psi> and\<^sub>p chi val') |val val'. val \<subseteq> A \<and> val' \<subseteq> A \<and> val' \<noteq> val} \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
val' = stval (\<sigma> 0)

goal (1 subgoal):
 1. \<sigma> \<Turnstile>\<^sub>p OR {chi val and\<^sub>p chi val U\<^sub>p (\<psi> and\<^sub>p chi val') |val val'. val \<subseteq> A \<and> val' \<subseteq> A \<and> val' \<noteq> val} \<Longrightarrow> False
[PROOF STEP]
note \<open>val' \<noteq> val\<close>
[PROOF STATE]
proof (state)
this:
val' \<noteq> val

goal (1 subgoal):
 1. \<sigma> \<Turnstile>\<^sub>p OR {chi val and\<^sub>p chi val U\<^sub>p (\<psi> and\<^sub>p chi val') |val val'. val \<subseteq> A \<and> val' \<subseteq> A \<and> val' \<noteq> val} \<Longrightarrow> False
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
val = stval (\<sigma> 0)
val' = stval (\<sigma> 0)
val' \<noteq> val
[PROOF STEP]
show "False"
[PROOF STATE]
proof (prove)
using this:
val = stval (\<sigma> 0)
val' = stval (\<sigma> 0)
val' \<noteq> val

goal (1 subgoal):
 1. False
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
False

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<not> \<sigma> \<Turnstile>\<^sub>p OR {chi val and\<^sub>p chi val U\<^sub>p (\<psi> and\<^sub>p chi val') |val val'. val \<subseteq> A \<and> val' \<subseteq> A \<and> val' \<noteq> val}

goal (2 subgoals):
 1. \<sigma> (Suc 0) = \<sigma> 0 \<Longrightarrow> \<sigma> \<Turnstile>\<^sub>p X\<^sub>p \<phi> = \<sigma> \<Turnstile>\<^sub>p psi'
 2. \<sigma> (Suc 0) \<noteq> \<sigma> 0 \<Longrightarrow> \<sigma> \<Turnstile>\<^sub>p X\<^sub>p \<phi> = \<sigma> \<Turnstile>\<^sub>p psi'
[PROOF STEP]
from 1 2 3
[PROOF STATE]
proof (chain)
picking this:
\<sigma> \<Turnstile>\<^sub>p X\<^sub>p \<phi> = \<sigma> \<Turnstile>\<^sub>p \<psi>
\<sigma> \<Turnstile>\<^sub>p OR {G\<^sub>p chi val |val. val \<subseteq> A}
\<not> \<sigma> \<Turnstile>\<^sub>p OR {chi val and\<^sub>p chi val U\<^sub>p (\<psi> and\<^sub>p chi val') |val val'. val \<subseteq> A \<and> val' \<subseteq> A \<and> val' \<noteq> val}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<sigma> \<Turnstile>\<^sub>p X\<^sub>p \<phi> = \<sigma> \<Turnstile>\<^sub>p \<psi>
\<sigma> \<Turnstile>\<^sub>p OR {G\<^sub>p chi val |val. val \<subseteq> A}
\<not> \<sigma> \<Turnstile>\<^sub>p OR {chi val and\<^sub>p chi val U\<^sub>p (\<psi> and\<^sub>p chi val') |val val'. val \<subseteq> A \<and> val' \<subseteq> A \<and> val' \<noteq> val}

goal (1 subgoal):
 1. \<sigma> \<Turnstile>\<^sub>p X\<^sub>p \<phi> = \<sigma> \<Turnstile>\<^sub>p psi'
[PROOF STEP]
by (simp add: psi'_def)
[PROOF STATE]
proof (state)
this:
\<sigma> \<Turnstile>\<^sub>p X\<^sub>p \<phi> = \<sigma> \<Turnstile>\<^sub>p psi'

goal (1 subgoal):
 1. \<sigma> (Suc 0) \<noteq> \<sigma> 0 \<Longrightarrow> \<sigma> \<Turnstile>\<^sub>p X\<^sub>p \<phi> = \<sigma> \<Turnstile>\<^sub>p psi'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<sigma> (Suc 0) \<noteq> \<sigma> 0 \<Longrightarrow> \<sigma> \<Turnstile>\<^sub>p X\<^sub>p \<phi> = \<sigma> \<Turnstile>\<^sub>p psi'
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<sigma> (Suc 0) \<noteq> \<sigma> 0

goal (1 subgoal):
 1. \<sigma> (Suc 0) \<noteq> \<sigma> 0 \<Longrightarrow> \<sigma> \<Turnstile>\<^sub>p X\<^sub>p \<phi> = \<sigma> \<Turnstile>\<^sub>p psi'
[PROOF STEP]
txt \<open>Otherwise, \<open>\<sigma> \<Turnstile>\<^sub>p X\<^sub>p \<phi>\<close> is equivalent to \<open>\<sigma>\<close> satisfying
        the second disjunct of \<open>psi'\<close>. We show both implications separately.\<close>
[PROOF STATE]
proof (state)
this:
\<sigma> (Suc 0) \<noteq> \<sigma> 0

goal (1 subgoal):
 1. \<sigma> (Suc 0) \<noteq> \<sigma> 0 \<Longrightarrow> \<sigma> \<Turnstile>\<^sub>p X\<^sub>p \<phi> = \<sigma> \<Turnstile>\<^sub>p psi'
[PROOF STEP]
let ?val = "stval (\<sigma> 0)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<sigma> (Suc 0) \<noteq> \<sigma> 0 \<Longrightarrow> \<sigma> \<Turnstile>\<^sub>p X\<^sub>p \<phi> = \<sigma> \<Turnstile>\<^sub>p psi'
[PROOF STEP]
let ?val' = "stval (\<sigma> 1)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<sigma> (Suc 0) \<noteq> \<sigma> 0 \<Longrightarrow> \<sigma> \<Turnstile>\<^sub>p X\<^sub>p \<phi> = \<sigma> \<Turnstile>\<^sub>p psi'
[PROOF STEP]
from False can
[PROOF STATE]
proof (chain)
picking this:
\<sigma> (Suc 0) \<noteq> \<sigma> 0
canonical_sequence A \<sigma>
[PROOF STEP]
have vals: "?val' \<noteq> ?val"
[PROOF STATE]
proof (prove)
using this:
\<sigma> (Suc 0) \<noteq> \<sigma> 0
canonical_sequence A \<sigma>

goal (1 subgoal):
 1. stval (\<sigma> 1) \<noteq> stval (\<sigma> 0)
[PROOF STEP]
by (auto simp: canonical_sequence_def state_sim_def stval_def)
[PROOF STATE]
proof (state)
this:
stval (\<sigma> 1) \<noteq> stval (\<sigma> 0)

goal (1 subgoal):
 1. \<sigma> (Suc 0) \<noteq> \<sigma> 0 \<Longrightarrow> \<sigma> \<Turnstile>\<^sub>p X\<^sub>p \<phi> = \<sigma> \<Turnstile>\<^sub>p psi'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<sigma> \<Turnstile>\<^sub>p X\<^sub>p \<phi> = \<sigma> \<Turnstile>\<^sub>p psi'
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<sigma> \<Turnstile>\<^sub>p X\<^sub>p \<phi> \<Longrightarrow> \<sigma> \<Turnstile>\<^sub>p psi'
 2. \<sigma> \<Turnstile>\<^sub>p psi' \<Longrightarrow> \<sigma> \<Turnstile>\<^sub>p X\<^sub>p \<phi>
[PROOF STEP]
assume phi: "\<sigma> \<Turnstile>\<^sub>p X\<^sub>p \<phi>"
[PROOF STATE]
proof (state)
this:
\<sigma> \<Turnstile>\<^sub>p X\<^sub>p \<phi>

goal (2 subgoals):
 1. \<sigma> \<Turnstile>\<^sub>p X\<^sub>p \<phi> \<Longrightarrow> \<sigma> \<Turnstile>\<^sub>p psi'
 2. \<sigma> \<Turnstile>\<^sub>p psi' \<Longrightarrow> \<sigma> \<Turnstile>\<^sub>p X\<^sub>p \<phi>
[PROOF STEP]
from fin
[PROOF STATE]
proof (chain)
picking this:
finite A
[PROOF STEP]
have 1: "\<sigma> \<Turnstile>\<^sub>p chi ?val"
[PROOF STATE]
proof (prove)
using this:
finite A

goal (1 subgoal):
 1. \<sigma> \<Turnstile>\<^sub>p chi (stval (\<sigma> 0))
[PROOF STEP]
by (simp add: chi1 characteristic_holds)
[PROOF STATE]
proof (state)
this:
\<sigma> \<Turnstile>\<^sub>p chi (stval (\<sigma> 0))

goal (2 subgoals):
 1. \<sigma> \<Turnstile>\<^sub>p X\<^sub>p \<phi> \<Longrightarrow> \<sigma> \<Turnstile>\<^sub>p psi'
 2. \<sigma> \<Turnstile>\<^sub>p psi' \<Longrightarrow> \<sigma> \<Turnstile>\<^sub>p X\<^sub>p \<phi>
[PROOF STEP]
from st can
[PROOF STATE]
proof (chain)
picking this:
stutter_free \<sigma>
canonical_sequence A \<sigma>
[PROOF STEP]
have "stutter_free (\<sigma>[1..])" "canonical_sequence A (\<sigma>[1..])"
[PROOF STATE]
proof (prove)
using this:
stutter_free \<sigma>
canonical_sequence A \<sigma>

goal (1 subgoal):
 1. stutter_free \<sigma> [1..] &&& canonical_sequence A \<sigma> [1..]
[PROOF STEP]
by (auto simp: stutter_free_suffix canonical_suffix)
[PROOF STATE]
proof (state)
this:
stutter_free \<sigma> [1..]
canonical_sequence A \<sigma> [1..]

goal (2 subgoals):
 1. \<sigma> \<Turnstile>\<^sub>p X\<^sub>p \<phi> \<Longrightarrow> \<sigma> \<Turnstile>\<^sub>p psi'
 2. \<sigma> \<Turnstile>\<^sub>p psi' \<Longrightarrow> \<sigma> \<Turnstile>\<^sub>p X\<^sub>p \<phi>
[PROOF STEP]
with phi psi
[PROOF STATE]
proof (chain)
picking this:
\<sigma> \<Turnstile>\<^sub>p X\<^sub>p \<phi>
next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>)
stutter_free \<sigma> [1..]
canonical_sequence A \<sigma> [1..]
[PROOF STEP]
have 2: "\<sigma>[1..] \<Turnstile>\<^sub>p \<psi>"
[PROOF STATE]
proof (prove)
using this:
\<sigma> \<Turnstile>\<^sub>p X\<^sub>p \<phi>
next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>)
stutter_free \<sigma> [1..]
canonical_sequence A \<sigma> [1..]

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

goal (2 subgoals):
 1. \<sigma> \<Turnstile>\<^sub>p X\<^sub>p \<phi> \<Longrightarrow> \<sigma> \<Turnstile>\<^sub>p psi'
 2. \<sigma> \<Turnstile>\<^sub>p psi' \<Longrightarrow> \<sigma> \<Turnstile>\<^sub>p X\<^sub>p \<phi>
[PROOF STEP]
from fin
[PROOF STATE]
proof (chain)
picking this:
finite A
[PROOF STEP]
have "\<sigma>[1..] \<Turnstile>\<^sub>p characteristic_formula A ((\<sigma>[1..]) 0)"
[PROOF STATE]
proof (prove)
using this:
finite A

goal (1 subgoal):
 1. \<sigma> [1..] \<Turnstile>\<^sub>p characteristic_formula A (\<sigma> [1..] 0)
[PROOF STEP]
by (rule characteristic_holds)
[PROOF STATE]
proof (state)
this:
\<sigma> [1..] \<Turnstile>\<^sub>p characteristic_formula A (\<sigma> [1..] 0)

goal (2 subgoals):
 1. \<sigma> \<Turnstile>\<^sub>p X\<^sub>p \<phi> \<Longrightarrow> \<sigma> \<Turnstile>\<^sub>p psi'
 2. \<sigma> \<Turnstile>\<^sub>p psi' \<Longrightarrow> \<sigma> \<Turnstile>\<^sub>p X\<^sub>p \<phi>
[PROOF STEP]
hence 3: "\<sigma>[1..] \<Turnstile>\<^sub>p chi ?val'"
[PROOF STATE]
proof (prove)
using this:
\<sigma> [1..] \<Turnstile>\<^sub>p characteristic_formula A (\<sigma> [1..] 0)

goal (1 subgoal):
 1. \<sigma> [1..] \<Turnstile>\<^sub>p chi (stval (\<sigma> 1))
[PROOF STEP]
by (simp add: chi1)
[PROOF STATE]
proof (state)
this:
\<sigma> [1..] \<Turnstile>\<^sub>p chi (stval (\<sigma> 1))

goal (2 subgoals):
 1. \<sigma> \<Turnstile>\<^sub>p X\<^sub>p \<phi> \<Longrightarrow> \<sigma> \<Turnstile>\<^sub>p psi'
 2. \<sigma> \<Turnstile>\<^sub>p psi' \<Longrightarrow> \<sigma> \<Turnstile>\<^sub>p X\<^sub>p \<phi>
[PROOF STEP]
from 1 2 3
[PROOF STATE]
proof (chain)
picking this:
\<sigma> \<Turnstile>\<^sub>p chi (stval (\<sigma> 0))
\<sigma> [1..] \<Turnstile>\<^sub>p \<psi>
\<sigma> [1..] \<Turnstile>\<^sub>p chi (stval (\<sigma> 1))
[PROOF STEP]
have "\<sigma> \<Turnstile>\<^sub>p And_ltlp (chi ?val) ((chi ?val) U\<^sub>p (And_ltlp \<psi> (chi ?val')))"
          (is "_ \<Turnstile>\<^sub>p ?unt")
[PROOF STATE]
proof (prove)
using this:
\<sigma> \<Turnstile>\<^sub>p chi (stval (\<sigma> 0))
\<sigma> [1..] \<Turnstile>\<^sub>p \<psi>
\<sigma> [1..] \<Turnstile>\<^sub>p chi (stval (\<sigma> 1))

goal (1 subgoal):
 1. \<sigma> \<Turnstile>\<^sub>p chi (stval (\<sigma> 0)) and\<^sub>p chi (stval (\<sigma> 0)) U\<^sub>p (\<psi> and\<^sub>p chi (stval (\<sigma> 1)))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<sigma> \<Turnstile>\<^sub>p chi (stval (\<sigma> 0)) and\<^sub>p chi (stval (\<sigma> 0)) U\<^sub>p (\<psi> and\<^sub>p chi (stval (\<sigma> 1)))

goal (2 subgoals):
 1. \<sigma> \<Turnstile>\<^sub>p X\<^sub>p \<phi> \<Longrightarrow> \<sigma> \<Turnstile>\<^sub>p psi'
 2. \<sigma> \<Turnstile>\<^sub>p psi' \<Longrightarrow> \<sigma> \<Turnstile>\<^sub>p X\<^sub>p \<phi>
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<sigma> \<Turnstile>\<^sub>p chi (stval (\<sigma> 0)) and\<^sub>p chi (stval (\<sigma> 0)) U\<^sub>p (\<psi> and\<^sub>p chi (stval (\<sigma> 1)))

goal (2 subgoals):
 1. \<sigma> \<Turnstile>\<^sub>p X\<^sub>p \<phi> \<Longrightarrow> \<sigma> \<Turnstile>\<^sub>p psi'
 2. \<sigma> \<Turnstile>\<^sub>p psi' \<Longrightarrow> \<sigma> \<Turnstile>\<^sub>p X\<^sub>p \<phi>
[PROOF STEP]
from vals
[PROOF STATE]
proof (chain)
picking this:
stval (\<sigma> 1) \<noteq> stval (\<sigma> 0)
[PROOF STEP]
have "?unt \<in> ?UNT"
[PROOF STATE]
proof (prove)
using this:
stval (\<sigma> 1) \<noteq> stval (\<sigma> 0)

goal (1 subgoal):
 1. chi (stval (\<sigma> 0)) and\<^sub>p chi (stval (\<sigma> 0)) U\<^sub>p (\<psi> and\<^sub>p chi (stval (\<sigma> 1))) \<in> {chi val and\<^sub>p chi val U\<^sub>p (\<psi> and\<^sub>p chi val') |val val'. val \<subseteq> A \<and> val' \<subseteq> A \<and> val' \<noteq> val}
[PROOF STEP]
by (auto simp: stval_def)
[PROOF STATE]
proof (state)
this:
chi (stval (\<sigma> 0)) and\<^sub>p chi (stval (\<sigma> 0)) U\<^sub>p (\<psi> and\<^sub>p chi (stval (\<sigma> 1))) \<in> {chi val and\<^sub>p chi val U\<^sub>p (\<psi> and\<^sub>p chi val') |val val'. val \<subseteq> A \<and> val' \<subseteq> A \<and> val' \<noteq> val}

goal (2 subgoals):
 1. \<sigma> \<Turnstile>\<^sub>p X\<^sub>p \<phi> \<Longrightarrow> \<sigma> \<Turnstile>\<^sub>p psi'
 2. \<sigma> \<Turnstile>\<^sub>p psi' \<Longrightarrow> \<sigma> \<Turnstile>\<^sub>p X\<^sub>p \<phi>
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<sigma> \<Turnstile>\<^sub>p chi (stval (\<sigma> 0)) and\<^sub>p chi (stval (\<sigma> 0)) U\<^sub>p (\<psi> and\<^sub>p chi (stval (\<sigma> 1)))
chi (stval (\<sigma> 0)) and\<^sub>p chi (stval (\<sigma> 0)) U\<^sub>p (\<psi> and\<^sub>p chi (stval (\<sigma> 1))) \<in> {chi val and\<^sub>p chi val U\<^sub>p (\<psi> and\<^sub>p chi val') |val val'. val \<subseteq> A \<and> val' \<subseteq> A \<and> val' \<noteq> val}
[PROOF STEP]
have "\<sigma> \<Turnstile>\<^sub>p OR ?UNT"
[PROOF STATE]
proof (prove)
using this:
\<sigma> \<Turnstile>\<^sub>p chi (stval (\<sigma> 0)) and\<^sub>p chi (stval (\<sigma> 0)) U\<^sub>p (\<psi> and\<^sub>p chi (stval (\<sigma> 1)))
chi (stval (\<sigma> 0)) and\<^sub>p chi (stval (\<sigma> 0)) U\<^sub>p (\<psi> and\<^sub>p chi (stval (\<sigma> 1))) \<in> {chi val and\<^sub>p chi val U\<^sub>p (\<psi> and\<^sub>p chi val') |val val'. val \<subseteq> A \<and> val' \<subseteq> A \<and> val' \<noteq> val}

goal (1 subgoal):
 1. \<sigma> \<Turnstile>\<^sub>p OR {chi val and\<^sub>p chi val U\<^sub>p (\<psi> and\<^sub>p chi val') |val val'. val \<subseteq> A \<and> val' \<subseteq> A \<and> val' \<noteq> val}
[PROOF STEP]
using fin_UNT[THEN holds_of_OR]
[PROOF STATE]
proof (prove)
using this:
\<sigma> \<Turnstile>\<^sub>p chi (stval (\<sigma> 0)) and\<^sub>p chi (stval (\<sigma> 0)) U\<^sub>p (\<psi> and\<^sub>p chi (stval (\<sigma> 1)))
chi (stval (\<sigma> 0)) and\<^sub>p chi (stval (\<sigma> 0)) U\<^sub>p (\<psi> and\<^sub>p chi (stval (\<sigma> 1))) \<in> {chi val and\<^sub>p chi val U\<^sub>p (\<psi> and\<^sub>p chi val') |val val'. val \<subseteq> A \<and> val' \<subseteq> A \<and> val' \<noteq> val}
?\<sigma> \<Turnstile>\<^sub>p OR {chi val and\<^sub>p chi val U\<^sub>p (\<psi> and\<^sub>p chi val') |val val'. val \<subseteq> A \<and> val' \<subseteq> A \<and> val' \<noteq> val} = (\<exists>\<phi>\<in>{chi val and\<^sub>p chi val U\<^sub>p (\<psi> and\<^sub>p chi val') |val val'. val \<subseteq> A \<and> val' \<subseteq> A \<and> val' \<noteq> val}. ?\<sigma> \<Turnstile>\<^sub>p \<phi>)

goal (1 subgoal):
 1. \<sigma> \<Turnstile>\<^sub>p OR {chi val and\<^sub>p chi val U\<^sub>p (\<psi> and\<^sub>p chi val') |val val'. val \<subseteq> A \<and> val' \<subseteq> A \<and> val' \<noteq> val}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<sigma> \<Turnstile>\<^sub>p OR {chi val and\<^sub>p chi val U\<^sub>p (\<psi> and\<^sub>p chi val') |val val'. val \<subseteq> A \<and> val' \<subseteq> A \<and> val' \<noteq> val}

goal (2 subgoals):
 1. \<sigma> \<Turnstile>\<^sub>p X\<^sub>p \<phi> \<Longrightarrow> \<sigma> \<Turnstile>\<^sub>p psi'
 2. \<sigma> \<Turnstile>\<^sub>p psi' \<Longrightarrow> \<sigma> \<Turnstile>\<^sub>p X\<^sub>p \<phi>
[PROOF STEP]
thus "\<sigma> \<Turnstile>\<^sub>p psi'"
[PROOF STATE]
proof (prove)
using this:
\<sigma> \<Turnstile>\<^sub>p OR {chi val and\<^sub>p chi val U\<^sub>p (\<psi> and\<^sub>p chi val') |val val'. val \<subseteq> A \<and> val' \<subseteq> A \<and> val' \<noteq> val}

goal (1 subgoal):
 1. \<sigma> \<Turnstile>\<^sub>p psi'
[PROOF STEP]
by (simp add: psi'_def)
[PROOF STATE]
proof (state)
this:
\<sigma> \<Turnstile>\<^sub>p psi'

goal (1 subgoal):
 1. \<sigma> \<Turnstile>\<^sub>p psi' \<Longrightarrow> \<sigma> \<Turnstile>\<^sub>p X\<^sub>p \<phi>
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<sigma> \<Turnstile>\<^sub>p psi' \<Longrightarrow> \<sigma> \<Turnstile>\<^sub>p X\<^sub>p \<phi>
[PROOF STEP]
assume psi': "\<sigma> \<Turnstile>\<^sub>p psi'"
[PROOF STATE]
proof (state)
this:
\<sigma> \<Turnstile>\<^sub>p psi'

goal (1 subgoal):
 1. \<sigma> \<Turnstile>\<^sub>p psi' \<Longrightarrow> \<sigma> \<Turnstile>\<^sub>p X\<^sub>p \<phi>
[PROOF STEP]
have "\<not>(\<sigma> \<Turnstile>\<^sub>p OR ?ALW)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> \<sigma> \<Turnstile>\<^sub>p OR {G\<^sub>p chi val |val. val \<subseteq> A}
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<sigma> \<Turnstile>\<^sub>p OR {G\<^sub>p chi val |val. val \<subseteq> A} \<Longrightarrow> False
[PROOF STEP]
assume "\<sigma> \<Turnstile>\<^sub>p OR ?ALW"
[PROOF STATE]
proof (state)
this:
\<sigma> \<Turnstile>\<^sub>p OR {G\<^sub>p chi val |val. val \<subseteq> A}

goal (1 subgoal):
 1. \<sigma> \<Turnstile>\<^sub>p OR {G\<^sub>p chi val |val. val \<subseteq> A} \<Longrightarrow> False
[PROOF STEP]
with fin
[PROOF STATE]
proof (chain)
picking this:
finite A
\<sigma> \<Turnstile>\<^sub>p OR {G\<^sub>p chi val |val. val \<subseteq> A}
[PROOF STEP]
obtain val where 1: "val \<subseteq> A" and 2: "\<forall>n. (\<sigma>[n..] \<Turnstile>\<^sub>p chi val)"
[PROOF STATE]
proof (prove)
using this:
finite A
\<sigma> \<Turnstile>\<^sub>p OR {G\<^sub>p chi val |val. val \<subseteq> A}

goal (1 subgoal):
 1. (\<And>val. \<lbrakk>val \<subseteq> A; \<forall>n. \<sigma> [n..] \<Turnstile>\<^sub>p chi val\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (force simp: finite_subset)
[PROOF STATE]
proof (state)
this:
val \<subseteq> A
\<forall>n. \<sigma> [n..] \<Turnstile>\<^sub>p chi val

goal (1 subgoal):
 1. \<sigma> \<Turnstile>\<^sub>p OR {G\<^sub>p chi val |val. val \<subseteq> A} \<Longrightarrow> False
[PROOF STEP]
from 2
[PROOF STATE]
proof (chain)
picking this:
\<forall>n. \<sigma> [n..] \<Turnstile>\<^sub>p chi val
[PROOF STEP]
have "\<sigma>[0..] \<Turnstile>\<^sub>p chi val"
[PROOF STATE]
proof (prove)
using this:
\<forall>n. \<sigma> [n..] \<Turnstile>\<^sub>p chi val

goal (1 subgoal):
 1. \<sigma> [0..] \<Turnstile>\<^sub>p chi val
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
\<sigma> [0..] \<Turnstile>\<^sub>p chi val

goal (1 subgoal):
 1. \<sigma> \<Turnstile>\<^sub>p OR {G\<^sub>p chi val |val. val \<subseteq> A} \<Longrightarrow> False
[PROOF STEP]
with 1
[PROOF STATE]
proof (chain)
picking this:
val \<subseteq> A
\<sigma> [0..] \<Turnstile>\<^sub>p chi val
[PROOF STEP]
have "val = ?val"
[PROOF STATE]
proof (prove)
using this:
val \<subseteq> A
\<sigma> [0..] \<Turnstile>\<^sub>p chi val

goal (1 subgoal):
 1. val = stval (\<sigma> 0)
[PROOF STEP]
by (simp add: chi2)
[PROOF STATE]
proof (state)
this:
val = stval (\<sigma> 0)

goal (1 subgoal):
 1. \<sigma> \<Turnstile>\<^sub>p OR {G\<^sub>p chi val |val. val \<subseteq> A} \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
val = stval (\<sigma> 0)

goal (1 subgoal):
 1. \<sigma> \<Turnstile>\<^sub>p OR {G\<^sub>p chi val |val. val \<subseteq> A} \<Longrightarrow> False
[PROOF STEP]
from 2
[PROOF STATE]
proof (chain)
picking this:
\<forall>n. \<sigma> [n..] \<Turnstile>\<^sub>p chi val
[PROOF STEP]
have "\<sigma>[1..] \<Turnstile>\<^sub>p chi val"
[PROOF STATE]
proof (prove)
using this:
\<forall>n. \<sigma> [n..] \<Turnstile>\<^sub>p chi val

goal (1 subgoal):
 1. \<sigma> [1..] \<Turnstile>\<^sub>p chi val
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
\<sigma> [1..] \<Turnstile>\<^sub>p chi val

goal (1 subgoal):
 1. \<sigma> \<Turnstile>\<^sub>p OR {G\<^sub>p chi val |val. val \<subseteq> A} \<Longrightarrow> False
[PROOF STEP]
with 1
[PROOF STATE]
proof (chain)
picking this:
val \<subseteq> A
\<sigma> [1..] \<Turnstile>\<^sub>p chi val
[PROOF STEP]
have "val = ?val'"
[PROOF STATE]
proof (prove)
using this:
val \<subseteq> A
\<sigma> [1..] \<Turnstile>\<^sub>p chi val

goal (1 subgoal):
 1. val = stval (\<sigma> 1)
[PROOF STEP]
by (force dest: chi2)
[PROOF STATE]
proof (state)
this:
val = stval (\<sigma> 1)

goal (1 subgoal):
 1. \<sigma> \<Turnstile>\<^sub>p OR {G\<^sub>p chi val |val. val \<subseteq> A} \<Longrightarrow> False
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
val = stval (\<sigma> 0)
val = stval (\<sigma> 1)
[PROOF STEP]
show "False"
[PROOF STATE]
proof (prove)
using this:
val = stval (\<sigma> 0)
val = stval (\<sigma> 1)

goal (1 subgoal):
 1. False
[PROOF STEP]
using vals
[PROOF STATE]
proof (prove)
using this:
val = stval (\<sigma> 0)
val = stval (\<sigma> 1)
stval (\<sigma> 1) \<noteq> stval (\<sigma> 0)

goal (1 subgoal):
 1. False
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
False

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<not> \<sigma> \<Turnstile>\<^sub>p OR {G\<^sub>p chi val |val. val \<subseteq> A}

goal (1 subgoal):
 1. \<sigma> \<Turnstile>\<^sub>p psi' \<Longrightarrow> \<sigma> \<Turnstile>\<^sub>p X\<^sub>p \<phi>
[PROOF STEP]
with psi'
[PROOF STATE]
proof (chain)
picking this:
\<sigma> \<Turnstile>\<^sub>p psi'
\<not> \<sigma> \<Turnstile>\<^sub>p OR {G\<^sub>p chi val |val. val \<subseteq> A}
[PROOF STEP]
have "\<sigma> \<Turnstile>\<^sub>p OR ?UNT"
[PROOF STATE]
proof (prove)
using this:
\<sigma> \<Turnstile>\<^sub>p psi'
\<not> \<sigma> \<Turnstile>\<^sub>p OR {G\<^sub>p chi val |val. val \<subseteq> A}

goal (1 subgoal):
 1. \<sigma> \<Turnstile>\<^sub>p OR {chi val and\<^sub>p chi val U\<^sub>p (\<psi> and\<^sub>p chi val') |val val'. val \<subseteq> A \<and> val' \<subseteq> A \<and> val' \<noteq> val}
[PROOF STEP]
by (simp add: psi'_def)
[PROOF STATE]
proof (state)
this:
\<sigma> \<Turnstile>\<^sub>p OR {chi val and\<^sub>p chi val U\<^sub>p (\<psi> and\<^sub>p chi val') |val val'. val \<subseteq> A \<and> val' \<subseteq> A \<and> val' \<noteq> val}

goal (1 subgoal):
 1. \<sigma> \<Turnstile>\<^sub>p psi' \<Longrightarrow> \<sigma> \<Turnstile>\<^sub>p X\<^sub>p \<phi>
[PROOF STEP]
with fin_UNT
[PROOF STATE]
proof (chain)
picking this:
finite {chi val and\<^sub>p chi val U\<^sub>p (\<psi> and\<^sub>p chi val') |val val'. val \<subseteq> A \<and> val' \<subseteq> A \<and> val' \<noteq> val}
\<sigma> \<Turnstile>\<^sub>p OR {chi val and\<^sub>p chi val U\<^sub>p (\<psi> and\<^sub>p chi val') |val val'. val \<subseteq> A \<and> val' \<subseteq> A \<and> val' \<noteq> val}
[PROOF STEP]
obtain val val' k where
          val: "val \<subseteq> A" "val' \<subseteq> A" "val' \<noteq> val" and
          now: "\<sigma> \<Turnstile>\<^sub>p chi val" and
          k: "\<sigma>[k..] \<Turnstile>\<^sub>p \<psi>" "\<sigma>[k..] \<Turnstile>\<^sub>p chi val'" and
          i: "\<forall>i<k. (\<sigma>[i..] \<Turnstile>\<^sub>p chi val)"
[PROOF STATE]
proof (prove)
using this:
finite {chi val and\<^sub>p chi val U\<^sub>p (\<psi> and\<^sub>p chi val') |val val'. val \<subseteq> A \<and> val' \<subseteq> A \<and> val' \<noteq> val}
\<sigma> \<Turnstile>\<^sub>p OR {chi val and\<^sub>p chi val U\<^sub>p (\<psi> and\<^sub>p chi val') |val val'. val \<subseteq> A \<and> val' \<subseteq> A \<and> val' \<noteq> val}

goal (1 subgoal):
 1. (\<And>val val' k. \<lbrakk>val \<subseteq> A; val' \<subseteq> A; val' \<noteq> val; \<sigma> \<Turnstile>\<^sub>p chi val; \<sigma> [k..] \<Turnstile>\<^sub>p \<psi>; \<sigma> [k..] \<Turnstile>\<^sub>p chi val'; \<forall>i<k. \<sigma> [i..] \<Turnstile>\<^sub>p chi val\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto (blast+)?
[PROOF STATE]
proof (state)
this:
val \<subseteq> A
val' \<subseteq> A
val' \<noteq> val
\<sigma> \<Turnstile>\<^sub>p chi val
\<sigma> [k..] \<Turnstile>\<^sub>p \<psi>
\<sigma> [k..] \<Turnstile>\<^sub>p chi val'
\<forall>i<k. \<sigma> [i..] \<Turnstile>\<^sub>p chi val

goal (1 subgoal):
 1. \<sigma> \<Turnstile>\<^sub>p psi' \<Longrightarrow> \<sigma> \<Turnstile>\<^sub>p X\<^sub>p \<phi>
[PROOF STEP]
(* FRAGILE: similar as above *)
[PROOF STATE]
proof (state)
this:
val \<subseteq> A
val' \<subseteq> A
val' \<noteq> val
\<sigma> \<Turnstile>\<^sub>p chi val
\<sigma> [k..] \<Turnstile>\<^sub>p \<psi>
\<sigma> [k..] \<Turnstile>\<^sub>p chi val'
\<forall>i<k. \<sigma> [i..] \<Turnstile>\<^sub>p chi val

goal (1 subgoal):
 1. \<sigma> \<Turnstile>\<^sub>p psi' \<Longrightarrow> \<sigma> \<Turnstile>\<^sub>p X\<^sub>p \<phi>
[PROOF STEP]
from val now
[PROOF STATE]
proof (chain)
picking this:
val \<subseteq> A
val' \<subseteq> A
val' \<noteq> val
\<sigma> \<Turnstile>\<^sub>p chi val
[PROOF STEP]
have 1: "val = ?val"
[PROOF STATE]
proof (prove)
using this:
val \<subseteq> A
val' \<subseteq> A
val' \<noteq> val
\<sigma> \<Turnstile>\<^sub>p chi val

goal (1 subgoal):
 1. val = stval (\<sigma> 0)
[PROOF STEP]
by (simp add: chi2)
[PROOF STATE]
proof (state)
this:
val = stval (\<sigma> 0)

goal (1 subgoal):
 1. \<sigma> \<Turnstile>\<^sub>p psi' \<Longrightarrow> \<sigma> \<Turnstile>\<^sub>p X\<^sub>p \<phi>
[PROOF STEP]
have 2: "k \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k \<noteq> 0
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. k = 0 \<Longrightarrow> False
[PROOF STEP]
assume "k=0"
[PROOF STATE]
proof (state)
this:
k = 0

goal (1 subgoal):
 1. k = 0 \<Longrightarrow> False
[PROOF STEP]
with val k
[PROOF STATE]
proof (chain)
picking this:
val \<subseteq> A
val' \<subseteq> A
val' \<noteq> val
\<sigma> [k..] \<Turnstile>\<^sub>p \<psi>
\<sigma> [k..] \<Turnstile>\<^sub>p chi val'
k = 0
[PROOF STEP]
have "val' = ?val"
[PROOF STATE]
proof (prove)
using this:
val \<subseteq> A
val' \<subseteq> A
val' \<noteq> val
\<sigma> [k..] \<Turnstile>\<^sub>p \<psi>
\<sigma> [k..] \<Turnstile>\<^sub>p chi val'
k = 0

goal (1 subgoal):
 1. val' = stval (\<sigma> 0)
[PROOF STEP]
by (simp add: chi2)
[PROOF STATE]
proof (state)
this:
val' = stval (\<sigma> 0)

goal (1 subgoal):
 1. k = 0 \<Longrightarrow> False
[PROOF STEP]
with 1 \<open>val' \<noteq> val\<close>
[PROOF STATE]
proof (chain)
picking this:
val = stval (\<sigma> 0)
val' \<noteq> val
val' = stval (\<sigma> 0)
[PROOF STEP]
show "False"
[PROOF STATE]
proof (prove)
using this:
val = stval (\<sigma> 0)
val' \<noteq> val
val' = stval (\<sigma> 0)

goal (1 subgoal):
 1. False
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
False

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
k \<noteq> 0

goal (1 subgoal):
 1. \<sigma> \<Turnstile>\<^sub>p psi' \<Longrightarrow> \<sigma> \<Turnstile>\<^sub>p X\<^sub>p \<phi>
[PROOF STEP]
have 3: "k \<le> 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k \<le> 1
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> k \<le> 1 \<Longrightarrow> False
[PROOF STEP]
assume "\<not>(k \<le> 1)"
[PROOF STATE]
proof (state)
this:
\<not> k \<le> 1

goal (1 subgoal):
 1. \<not> k \<le> 1 \<Longrightarrow> False
[PROOF STEP]
with i
[PROOF STATE]
proof (chain)
picking this:
\<forall>i<k. \<sigma> [i..] \<Turnstile>\<^sub>p chi val
\<not> k \<le> 1
[PROOF STEP]
have "\<sigma>[1..] \<Turnstile>\<^sub>p chi val"
[PROOF STATE]
proof (prove)
using this:
\<forall>i<k. \<sigma> [i..] \<Turnstile>\<^sub>p chi val
\<not> k \<le> 1

goal (1 subgoal):
 1. \<sigma> [1..] \<Turnstile>\<^sub>p chi val
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<sigma> [1..] \<Turnstile>\<^sub>p chi val

goal (1 subgoal):
 1. \<not> k \<le> 1 \<Longrightarrow> False
[PROOF STEP]
with 1
[PROOF STATE]
proof (chain)
picking this:
val = stval (\<sigma> 0)
\<sigma> [1..] \<Turnstile>\<^sub>p chi val
[PROOF STEP]
have "\<sigma>[1..] \<Turnstile>\<^sub>p characteristic_formula A (\<sigma> 0)"
[PROOF STATE]
proof (prove)
using this:
val = stval (\<sigma> 0)
\<sigma> [1..] \<Turnstile>\<^sub>p chi val

goal (1 subgoal):
 1. \<sigma> [1..] \<Turnstile>\<^sub>p characteristic_formula A (\<sigma> 0)
[PROOF STEP]
by (simp add: chi1)
[PROOF STATE]
proof (state)
this:
\<sigma> [1..] \<Turnstile>\<^sub>p characteristic_formula A (\<sigma> 0)

goal (1 subgoal):
 1. \<not> k \<le> 1 \<Longrightarrow> False
[PROOF STEP]
hence "(\<sigma> 0) ~A~ ((\<sigma>[1..]) 0)"
[PROOF STATE]
proof (prove)
using this:
\<sigma> [1..] \<Turnstile>\<^sub>p characteristic_formula A (\<sigma> 0)

goal (1 subgoal):
 1. \<sigma> 0 ~A~ \<sigma> [1..] 0
[PROOF STEP]
using characteristic_state_sim[OF fin]
[PROOF STATE]
proof (prove)
using this:
\<sigma> [1..] \<Turnstile>\<^sub>p characteristic_formula A (\<sigma> 0)
(?\<sigma> 0 ~A~ ?\<tau> 0) = ?\<tau> \<Turnstile>\<^sub>p characteristic_formula A (?\<sigma> 0)

goal (1 subgoal):
 1. \<sigma> 0 ~A~ \<sigma> [1..] 0
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<sigma> 0 ~A~ \<sigma> [1..] 0

goal (1 subgoal):
 1. \<not> k \<le> 1 \<Longrightarrow> False
[PROOF STEP]
with can
[PROOF STATE]
proof (chain)
picking this:
canonical_sequence A \<sigma>
\<sigma> 0 ~A~ \<sigma> [1..] 0
[PROOF STEP]
have "\<sigma> 0 = \<sigma> 1"
[PROOF STATE]
proof (prove)
using this:
canonical_sequence A \<sigma>
\<sigma> 0 ~A~ \<sigma> [1..] 0

goal (1 subgoal):
 1. \<sigma> 0 = \<sigma> 1
[PROOF STEP]
by (simp add: canonical_sequence_def)
[PROOF STATE]
proof (state)
this:
\<sigma> 0 = \<sigma> 1

goal (1 subgoal):
 1. \<not> k \<le> 1 \<Longrightarrow> False
[PROOF STEP]
with \<open>\<sigma> (Suc 0) \<noteq> \<sigma> 0\<close>
[PROOF STATE]
proof (chain)
picking this:
\<sigma> (Suc 0) \<noteq> \<sigma> 0
\<sigma> 0 = \<sigma> 1
[PROOF STEP]
show "False"
[PROOF STATE]
proof (prove)
using this:
\<sigma> (Suc 0) \<noteq> \<sigma> 0
\<sigma> 0 = \<sigma> 1

goal (1 subgoal):
 1. False
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
False

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
k \<le> 1

goal (1 subgoal):
 1. \<sigma> \<Turnstile>\<^sub>p psi' \<Longrightarrow> \<sigma> \<Turnstile>\<^sub>p X\<^sub>p \<phi>
[PROOF STEP]
from 2 3
[PROOF STATE]
proof (chain)
picking this:
k \<noteq> 0
k \<le> 1
[PROOF STEP]
have "k=1"
[PROOF STATE]
proof (prove)
using this:
k \<noteq> 0
k \<le> 1

goal (1 subgoal):
 1. k = 1
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
k = 1

goal (1 subgoal):
 1. \<sigma> \<Turnstile>\<^sub>p psi' \<Longrightarrow> \<sigma> \<Turnstile>\<^sub>p X\<^sub>p \<phi>
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
k = 1

goal (1 subgoal):
 1. \<sigma> \<Turnstile>\<^sub>p psi' \<Longrightarrow> \<sigma> \<Turnstile>\<^sub>p X\<^sub>p \<phi>
[PROOF STEP]
from st can
[PROOF STATE]
proof (chain)
picking this:
stutter_free \<sigma>
canonical_sequence A \<sigma>
[PROOF STEP]
have "stutter_free (\<sigma>[1..])" "canonical_sequence A (\<sigma>[1..])"
[PROOF STATE]
proof (prove)
using this:
stutter_free \<sigma>
canonical_sequence A \<sigma>

goal (1 subgoal):
 1. stutter_free \<sigma> [1..] &&& canonical_sequence A \<sigma> [1..]
[PROOF STEP]
by (auto simp: stutter_free_suffix canonical_suffix)
[PROOF STATE]
proof (state)
this:
stutter_free \<sigma> [1..]
canonical_sequence A \<sigma> [1..]

goal (1 subgoal):
 1. \<sigma> \<Turnstile>\<^sub>p psi' \<Longrightarrow> \<sigma> \<Turnstile>\<^sub>p X\<^sub>p \<phi>
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
k = 1
stutter_free \<sigma> [1..]
canonical_sequence A \<sigma> [1..]
[PROOF STEP]
show "\<sigma> \<Turnstile>\<^sub>p X\<^sub>p \<phi>"
[PROOF STATE]
proof (prove)
using this:
k = 1
stutter_free \<sigma> [1..]
canonical_sequence A \<sigma> [1..]

goal (1 subgoal):
 1. \<sigma> \<Turnstile>\<^sub>p X\<^sub>p \<phi>
[PROOF STEP]
using \<open>\<sigma>[k..] \<Turnstile>\<^sub>p \<psi>\<close> psi
[PROOF STATE]
proof (prove)
using this:
k = 1
stutter_free \<sigma> [1..]
canonical_sequence A \<sigma> [1..]
\<sigma> [k..] \<Turnstile>\<^sub>p \<psi>
next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>)

goal (1 subgoal):
 1. \<sigma> \<Turnstile>\<^sub>p X\<^sub>p \<phi>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<sigma> \<Turnstile>\<^sub>p X\<^sub>p \<phi>

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<sigma> \<Turnstile>\<^sub>p X\<^sub>p \<phi> = \<sigma> \<Turnstile>\<^sub>p psi'

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<sigma> \<Turnstile>\<^sub>p X\<^sub>p \<phi> = \<sigma> \<Turnstile>\<^sub>p psi'

goal (1 subgoal):
 1. \<And>\<phi>. \<lbrakk>atoms_pltl \<phi> \<subseteq> A \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>); atoms_pltl (X\<^sub>p \<phi>) \<subseteq> A\<rbrakk> \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p X\<^sub>p \<phi>)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>stutter_free ?\<sigma>2; canonical_sequence A ?\<sigma>2\<rbrakk> \<Longrightarrow> ?\<sigma>2 \<Turnstile>\<^sub>p X\<^sub>p \<phi> = ?\<sigma>2 \<Turnstile>\<^sub>p psi'

goal (1 subgoal):
 1. \<And>\<phi>. \<lbrakk>atoms_pltl \<phi> \<subseteq> A \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>); atoms_pltl (X\<^sub>p \<phi>) \<subseteq> A\<rbrakk> \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p X\<^sub>p \<phi>)
[PROOF STEP]
with nf atoms_pltl
[PROOF STATE]
proof (chain)
picking this:
next_free psi'
atoms_pltl psi' \<subseteq> A
\<lbrakk>stutter_free ?\<sigma>2; canonical_sequence A ?\<sigma>2\<rbrakk> \<Longrightarrow> ?\<sigma>2 \<Turnstile>\<^sub>p X\<^sub>p \<phi> = ?\<sigma>2 \<Turnstile>\<^sub>p psi'
[PROOF STEP]
show "\<exists>\<psi>'. ?P (X\<^sub>p \<phi>) \<psi>'"
[PROOF STATE]
proof (prove)
using this:
next_free psi'
atoms_pltl psi' \<subseteq> A
\<lbrakk>stutter_free ?\<sigma>2; canonical_sequence A ?\<sigma>2\<rbrakk> \<Longrightarrow> ?\<sigma>2 \<Turnstile>\<^sub>p X\<^sub>p \<phi> = ?\<sigma>2 \<Turnstile>\<^sub>p psi'

goal (1 subgoal):
 1. \<exists>\<psi>'. next_free \<psi>' \<and> atoms_pltl \<psi>' \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi>' = \<sigma> \<Turnstile>\<^sub>p X\<^sub>p \<phi>)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>\<psi>'. next_free \<psi>' \<and> atoms_pltl \<psi>' \<subseteq> A \<and> (\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence A \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi>' = \<sigma> \<Turnstile>\<^sub>p X\<^sub>p \<phi>)

goal:
No subgoals!
[PROOF STEP]
qed