[STATEMENT]
lemma pltl_seq_sim: "\<sigma> \<simeq> atoms_pltl \<phi> \<simeq> \<tau> \<Longrightarrow> (\<sigma> \<Turnstile>\<^sub>p \<phi>) = (\<tau> \<Turnstile>\<^sub>p \<phi>)"
  (is "?sim \<sigma> \<phi> \<tau> \<Longrightarrow> ?P \<sigma> \<phi> \<tau>")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<sigma> \<simeq>atoms_pltl \<phi>\<simeq> \<tau> \<Longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<phi> = \<tau> \<Turnstile>\<^sub>p \<phi>
[PROOF STEP]
proof (induct \<phi> arbitrary: \<sigma> \<tau>)
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>\<sigma> \<tau>. \<sigma> \<simeq>atoms_pltl false\<^sub>p\<simeq> \<tau> \<Longrightarrow> \<sigma> \<Turnstile>\<^sub>p false\<^sub>p = \<tau> \<Turnstile>\<^sub>p false\<^sub>p
 2. \<And>x \<sigma> \<tau>. \<sigma> \<simeq>atoms_pltl atom\<^sub>p(x)\<simeq> \<tau> \<Longrightarrow> \<sigma> \<Turnstile>\<^sub>p atom\<^sub>p(x) = \<tau> \<Turnstile>\<^sub>p atom\<^sub>p(x)
 3. \<And>\<phi>1 \<phi>2 \<sigma> \<tau>. \<lbrakk>\<And>\<sigma> \<tau>. \<sigma> \<simeq>atoms_pltl \<phi>1\<simeq> \<tau> \<Longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<phi>1 = \<tau> \<Turnstile>\<^sub>p \<phi>1; \<And>\<sigma> \<tau>. \<sigma> \<simeq>atoms_pltl \<phi>2\<simeq> \<tau> \<Longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<phi>2 = \<tau> \<Turnstile>\<^sub>p \<phi>2; \<sigma> \<simeq>atoms_pltl (\<phi>1 implies\<^sub>p \<phi>2)\<simeq> \<tau>\<rbrakk> \<Longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<phi>1 implies\<^sub>p \<phi>2 = \<tau> \<Turnstile>\<^sub>p \<phi>1 implies\<^sub>p \<phi>2
 4. \<And>\<phi> \<sigma> \<tau>. \<lbrakk>\<And>\<sigma> \<tau>. \<sigma> \<simeq>atoms_pltl \<phi>\<simeq> \<tau> \<Longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<phi> = \<tau> \<Turnstile>\<^sub>p \<phi>; \<sigma> \<simeq>atoms_pltl (X\<^sub>p \<phi>)\<simeq> \<tau>\<rbrakk> \<Longrightarrow> \<sigma> \<Turnstile>\<^sub>p X\<^sub>p \<phi> = \<tau> \<Turnstile>\<^sub>p X\<^sub>p \<phi>
 5. \<And>\<phi>1 \<phi>2 \<sigma> \<tau>. \<lbrakk>\<And>\<sigma> \<tau>. \<sigma> \<simeq>atoms_pltl \<phi>1\<simeq> \<tau> \<Longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<phi>1 = \<tau> \<Turnstile>\<^sub>p \<phi>1; \<And>\<sigma> \<tau>. \<sigma> \<simeq>atoms_pltl \<phi>2\<simeq> \<tau> \<Longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<phi>2 = \<tau> \<Turnstile>\<^sub>p \<phi>2; \<sigma> \<simeq>atoms_pltl (\<phi>1 U\<^sub>p \<phi>2)\<simeq> \<tau>\<rbrakk> \<Longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<phi>1 U\<^sub>p \<phi>2 = \<tau> \<Turnstile>\<^sub>p \<phi>1 U\<^sub>p \<phi>2
[PROOF STEP]
fix \<sigma> \<tau>
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>\<sigma> \<tau>. \<sigma> \<simeq>atoms_pltl false\<^sub>p\<simeq> \<tau> \<Longrightarrow> \<sigma> \<Turnstile>\<^sub>p false\<^sub>p = \<tau> \<Turnstile>\<^sub>p false\<^sub>p
 2. \<And>x \<sigma> \<tau>. \<sigma> \<simeq>atoms_pltl atom\<^sub>p(x)\<simeq> \<tau> \<Longrightarrow> \<sigma> \<Turnstile>\<^sub>p atom\<^sub>p(x) = \<tau> \<Turnstile>\<^sub>p atom\<^sub>p(x)
 3. \<And>\<phi>1 \<phi>2 \<sigma> \<tau>. \<lbrakk>\<And>\<sigma> \<tau>. \<sigma> \<simeq>atoms_pltl \<phi>1\<simeq> \<tau> \<Longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<phi>1 = \<tau> \<Turnstile>\<^sub>p \<phi>1; \<And>\<sigma> \<tau>. \<sigma> \<simeq>atoms_pltl \<phi>2\<simeq> \<tau> \<Longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<phi>2 = \<tau> \<Turnstile>\<^sub>p \<phi>2; \<sigma> \<simeq>atoms_pltl (\<phi>1 implies\<^sub>p \<phi>2)\<simeq> \<tau>\<rbrakk> \<Longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<phi>1 implies\<^sub>p \<phi>2 = \<tau> \<Turnstile>\<^sub>p \<phi>1 implies\<^sub>p \<phi>2
 4. \<And>\<phi> \<sigma> \<tau>. \<lbrakk>\<And>\<sigma> \<tau>. \<sigma> \<simeq>atoms_pltl \<phi>\<simeq> \<tau> \<Longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<phi> = \<tau> \<Turnstile>\<^sub>p \<phi>; \<sigma> \<simeq>atoms_pltl (X\<^sub>p \<phi>)\<simeq> \<tau>\<rbrakk> \<Longrightarrow> \<sigma> \<Turnstile>\<^sub>p X\<^sub>p \<phi> = \<tau> \<Turnstile>\<^sub>p X\<^sub>p \<phi>
 5. \<And>\<phi>1 \<phi>2 \<sigma> \<tau>. \<lbrakk>\<And>\<sigma> \<tau>. \<sigma> \<simeq>atoms_pltl \<phi>1\<simeq> \<tau> \<Longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<phi>1 = \<tau> \<Turnstile>\<^sub>p \<phi>1; \<And>\<sigma> \<tau>. \<sigma> \<simeq>atoms_pltl \<phi>2\<simeq> \<tau> \<Longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<phi>2 = \<tau> \<Turnstile>\<^sub>p \<phi>2; \<sigma> \<simeq>atoms_pltl (\<phi>1 U\<^sub>p \<phi>2)\<simeq> \<tau>\<rbrakk> \<Longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<phi>1 U\<^sub>p \<phi>2 = \<tau> \<Turnstile>\<^sub>p \<phi>1 U\<^sub>p \<phi>2
[PROOF STEP]
show "?P \<sigma> false\<^sub>p \<tau>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<sigma> \<Turnstile>\<^sub>p false\<^sub>p = \<tau> \<Turnstile>\<^sub>p false\<^sub>p
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<sigma> \<Turnstile>\<^sub>p false\<^sub>p = \<tau> \<Turnstile>\<^sub>p false\<^sub>p

goal (4 subgoals):
 1. \<And>x \<sigma> \<tau>. \<sigma> \<simeq>atoms_pltl atom\<^sub>p(x)\<simeq> \<tau> \<Longrightarrow> \<sigma> \<Turnstile>\<^sub>p atom\<^sub>p(x) = \<tau> \<Turnstile>\<^sub>p atom\<^sub>p(x)
 2. \<And>\<phi>1 \<phi>2 \<sigma> \<tau>. \<lbrakk>\<And>\<sigma> \<tau>. \<sigma> \<simeq>atoms_pltl \<phi>1\<simeq> \<tau> \<Longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<phi>1 = \<tau> \<Turnstile>\<^sub>p \<phi>1; \<And>\<sigma> \<tau>. \<sigma> \<simeq>atoms_pltl \<phi>2\<simeq> \<tau> \<Longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<phi>2 = \<tau> \<Turnstile>\<^sub>p \<phi>2; \<sigma> \<simeq>atoms_pltl (\<phi>1 implies\<^sub>p \<phi>2)\<simeq> \<tau>\<rbrakk> \<Longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<phi>1 implies\<^sub>p \<phi>2 = \<tau> \<Turnstile>\<^sub>p \<phi>1 implies\<^sub>p \<phi>2
 3. \<And>\<phi> \<sigma> \<tau>. \<lbrakk>\<And>\<sigma> \<tau>. \<sigma> \<simeq>atoms_pltl \<phi>\<simeq> \<tau> \<Longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<phi> = \<tau> \<Turnstile>\<^sub>p \<phi>; \<sigma> \<simeq>atoms_pltl (X\<^sub>p \<phi>)\<simeq> \<tau>\<rbrakk> \<Longrightarrow> \<sigma> \<Turnstile>\<^sub>p X\<^sub>p \<phi> = \<tau> \<Turnstile>\<^sub>p X\<^sub>p \<phi>
 4. \<And>\<phi>1 \<phi>2 \<sigma> \<tau>. \<lbrakk>\<And>\<sigma> \<tau>. \<sigma> \<simeq>atoms_pltl \<phi>1\<simeq> \<tau> \<Longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<phi>1 = \<tau> \<Turnstile>\<^sub>p \<phi>1; \<And>\<sigma> \<tau>. \<sigma> \<simeq>atoms_pltl \<phi>2\<simeq> \<tau> \<Longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<phi>2 = \<tau> \<Turnstile>\<^sub>p \<phi>2; \<sigma> \<simeq>atoms_pltl (\<phi>1 U\<^sub>p \<phi>2)\<simeq> \<tau>\<rbrakk> \<Longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<phi>1 U\<^sub>p \<phi>2 = \<tau> \<Turnstile>\<^sub>p \<phi>1 U\<^sub>p \<phi>2
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>x \<sigma> \<tau>. \<sigma> \<simeq>atoms_pltl atom\<^sub>p(x)\<simeq> \<tau> \<Longrightarrow> \<sigma> \<Turnstile>\<^sub>p atom\<^sub>p(x) = \<tau> \<Turnstile>\<^sub>p atom\<^sub>p(x)
 2. \<And>\<phi>1 \<phi>2 \<sigma> \<tau>. \<lbrakk>\<And>\<sigma> \<tau>. \<sigma> \<simeq>atoms_pltl \<phi>1\<simeq> \<tau> \<Longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<phi>1 = \<tau> \<Turnstile>\<^sub>p \<phi>1; \<And>\<sigma> \<tau>. \<sigma> \<simeq>atoms_pltl \<phi>2\<simeq> \<tau> \<Longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<phi>2 = \<tau> \<Turnstile>\<^sub>p \<phi>2; \<sigma> \<simeq>atoms_pltl (\<phi>1 implies\<^sub>p \<phi>2)\<simeq> \<tau>\<rbrakk> \<Longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<phi>1 implies\<^sub>p \<phi>2 = \<tau> \<Turnstile>\<^sub>p \<phi>1 implies\<^sub>p \<phi>2
 3. \<And>\<phi> \<sigma> \<tau>. \<lbrakk>\<And>\<sigma> \<tau>. \<sigma> \<simeq>atoms_pltl \<phi>\<simeq> \<tau> \<Longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<phi> = \<tau> \<Turnstile>\<^sub>p \<phi>; \<sigma> \<simeq>atoms_pltl (X\<^sub>p \<phi>)\<simeq> \<tau>\<rbrakk> \<Longrightarrow> \<sigma> \<Turnstile>\<^sub>p X\<^sub>p \<phi> = \<tau> \<Turnstile>\<^sub>p X\<^sub>p \<phi>
 4. \<And>\<phi>1 \<phi>2 \<sigma> \<tau>. \<lbrakk>\<And>\<sigma> \<tau>. \<sigma> \<simeq>atoms_pltl \<phi>1\<simeq> \<tau> \<Longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<phi>1 = \<tau> \<Turnstile>\<^sub>p \<phi>1; \<And>\<sigma> \<tau>. \<sigma> \<simeq>atoms_pltl \<phi>2\<simeq> \<tau> \<Longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<phi>2 = \<tau> \<Turnstile>\<^sub>p \<phi>2; \<sigma> \<simeq>atoms_pltl (\<phi>1 U\<^sub>p \<phi>2)\<simeq> \<tau>\<rbrakk> \<Longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<phi>1 U\<^sub>p \<phi>2 = \<tau> \<Turnstile>\<^sub>p \<phi>1 U\<^sub>p \<phi>2
[PROOF STEP]
fix p \<sigma> \<tau>
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>x \<sigma> \<tau>. \<sigma> \<simeq>atoms_pltl atom\<^sub>p(x)\<simeq> \<tau> \<Longrightarrow> \<sigma> \<Turnstile>\<^sub>p atom\<^sub>p(x) = \<tau> \<Turnstile>\<^sub>p atom\<^sub>p(x)
 2. \<And>\<phi>1 \<phi>2 \<sigma> \<tau>. \<lbrakk>\<And>\<sigma> \<tau>. \<sigma> \<simeq>atoms_pltl \<phi>1\<simeq> \<tau> \<Longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<phi>1 = \<tau> \<Turnstile>\<^sub>p \<phi>1; \<And>\<sigma> \<tau>. \<sigma> \<simeq>atoms_pltl \<phi>2\<simeq> \<tau> \<Longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<phi>2 = \<tau> \<Turnstile>\<^sub>p \<phi>2; \<sigma> \<simeq>atoms_pltl (\<phi>1 implies\<^sub>p \<phi>2)\<simeq> \<tau>\<rbrakk> \<Longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<phi>1 implies\<^sub>p \<phi>2 = \<tau> \<Turnstile>\<^sub>p \<phi>1 implies\<^sub>p \<phi>2
 3. \<And>\<phi> \<sigma> \<tau>. \<lbrakk>\<And>\<sigma> \<tau>. \<sigma> \<simeq>atoms_pltl \<phi>\<simeq> \<tau> \<Longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<phi> = \<tau> \<Turnstile>\<^sub>p \<phi>; \<sigma> \<simeq>atoms_pltl (X\<^sub>p \<phi>)\<simeq> \<tau>\<rbrakk> \<Longrightarrow> \<sigma> \<Turnstile>\<^sub>p X\<^sub>p \<phi> = \<tau> \<Turnstile>\<^sub>p X\<^sub>p \<phi>
 4. \<And>\<phi>1 \<phi>2 \<sigma> \<tau>. \<lbrakk>\<And>\<sigma> \<tau>. \<sigma> \<simeq>atoms_pltl \<phi>1\<simeq> \<tau> \<Longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<phi>1 = \<tau> \<Turnstile>\<^sub>p \<phi>1; \<And>\<sigma> \<tau>. \<sigma> \<simeq>atoms_pltl \<phi>2\<simeq> \<tau> \<Longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<phi>2 = \<tau> \<Turnstile>\<^sub>p \<phi>2; \<sigma> \<simeq>atoms_pltl (\<phi>1 U\<^sub>p \<phi>2)\<simeq> \<tau>\<rbrakk> \<Longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<phi>1 U\<^sub>p \<phi>2 = \<tau> \<Turnstile>\<^sub>p \<phi>1 U\<^sub>p \<phi>2
[PROOF STEP]
assume "?sim \<sigma> (atom\<^sub>p(p)) \<tau>"
[PROOF STATE]
proof (state)
this:
\<sigma> \<simeq>atoms_pltl atom\<^sub>p(p)\<simeq> \<tau>

goal (4 subgoals):
 1. \<And>x \<sigma> \<tau>. \<sigma> \<simeq>atoms_pltl atom\<^sub>p(x)\<simeq> \<tau> \<Longrightarrow> \<sigma> \<Turnstile>\<^sub>p atom\<^sub>p(x) = \<tau> \<Turnstile>\<^sub>p atom\<^sub>p(x)
 2. \<And>\<phi>1 \<phi>2 \<sigma> \<tau>. \<lbrakk>\<And>\<sigma> \<tau>. \<sigma> \<simeq>atoms_pltl \<phi>1\<simeq> \<tau> \<Longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<phi>1 = \<tau> \<Turnstile>\<^sub>p \<phi>1; \<And>\<sigma> \<tau>. \<sigma> \<simeq>atoms_pltl \<phi>2\<simeq> \<tau> \<Longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<phi>2 = \<tau> \<Turnstile>\<^sub>p \<phi>2; \<sigma> \<simeq>atoms_pltl (\<phi>1 implies\<^sub>p \<phi>2)\<simeq> \<tau>\<rbrakk> \<Longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<phi>1 implies\<^sub>p \<phi>2 = \<tau> \<Turnstile>\<^sub>p \<phi>1 implies\<^sub>p \<phi>2
 3. \<And>\<phi> \<sigma> \<tau>. \<lbrakk>\<And>\<sigma> \<tau>. \<sigma> \<simeq>atoms_pltl \<phi>\<simeq> \<tau> \<Longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<phi> = \<tau> \<Turnstile>\<^sub>p \<phi>; \<sigma> \<simeq>atoms_pltl (X\<^sub>p \<phi>)\<simeq> \<tau>\<rbrakk> \<Longrightarrow> \<sigma> \<Turnstile>\<^sub>p X\<^sub>p \<phi> = \<tau> \<Turnstile>\<^sub>p X\<^sub>p \<phi>
 4. \<And>\<phi>1 \<phi>2 \<sigma> \<tau>. \<lbrakk>\<And>\<sigma> \<tau>. \<sigma> \<simeq>atoms_pltl \<phi>1\<simeq> \<tau> \<Longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<phi>1 = \<tau> \<Turnstile>\<^sub>p \<phi>1; \<And>\<sigma> \<tau>. \<sigma> \<simeq>atoms_pltl \<phi>2\<simeq> \<tau> \<Longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<phi>2 = \<tau> \<Turnstile>\<^sub>p \<phi>2; \<sigma> \<simeq>atoms_pltl (\<phi>1 U\<^sub>p \<phi>2)\<simeq> \<tau>\<rbrakk> \<Longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<phi>1 U\<^sub>p \<phi>2 = \<tau> \<Turnstile>\<^sub>p \<phi>1 U\<^sub>p \<phi>2
[PROOF STEP]
thus "?P \<sigma> (atom\<^sub>p(p)) \<tau>"
[PROOF STATE]
proof (prove)
using this:
\<sigma> \<simeq>atoms_pltl atom\<^sub>p(p)\<simeq> \<tau>

goal (1 subgoal):
 1. \<sigma> \<Turnstile>\<^sub>p atom\<^sub>p(p) = \<tau> \<Turnstile>\<^sub>p atom\<^sub>p(p)
[PROOF STEP]
by (auto simp: seq_sim_def state_sim_def)
[PROOF STATE]
proof (state)
this:
\<sigma> \<Turnstile>\<^sub>p atom\<^sub>p(p) = \<tau> \<Turnstile>\<^sub>p atom\<^sub>p(p)

goal (3 subgoals):
 1. \<And>\<phi>1 \<phi>2 \<sigma> \<tau>. \<lbrakk>\<And>\<sigma> \<tau>. \<sigma> \<simeq>atoms_pltl \<phi>1\<simeq> \<tau> \<Longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<phi>1 = \<tau> \<Turnstile>\<^sub>p \<phi>1; \<And>\<sigma> \<tau>. \<sigma> \<simeq>atoms_pltl \<phi>2\<simeq> \<tau> \<Longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<phi>2 = \<tau> \<Turnstile>\<^sub>p \<phi>2; \<sigma> \<simeq>atoms_pltl (\<phi>1 implies\<^sub>p \<phi>2)\<simeq> \<tau>\<rbrakk> \<Longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<phi>1 implies\<^sub>p \<phi>2 = \<tau> \<Turnstile>\<^sub>p \<phi>1 implies\<^sub>p \<phi>2
 2. \<And>\<phi> \<sigma> \<tau>. \<lbrakk>\<And>\<sigma> \<tau>. \<sigma> \<simeq>atoms_pltl \<phi>\<simeq> \<tau> \<Longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<phi> = \<tau> \<Turnstile>\<^sub>p \<phi>; \<sigma> \<simeq>atoms_pltl (X\<^sub>p \<phi>)\<simeq> \<tau>\<rbrakk> \<Longrightarrow> \<sigma> \<Turnstile>\<^sub>p X\<^sub>p \<phi> = \<tau> \<Turnstile>\<^sub>p X\<^sub>p \<phi>
 3. \<And>\<phi>1 \<phi>2 \<sigma> \<tau>. \<lbrakk>\<And>\<sigma> \<tau>. \<sigma> \<simeq>atoms_pltl \<phi>1\<simeq> \<tau> \<Longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<phi>1 = \<tau> \<Turnstile>\<^sub>p \<phi>1; \<And>\<sigma> \<tau>. \<sigma> \<simeq>atoms_pltl \<phi>2\<simeq> \<tau> \<Longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<phi>2 = \<tau> \<Turnstile>\<^sub>p \<phi>2; \<sigma> \<simeq>atoms_pltl (\<phi>1 U\<^sub>p \<phi>2)\<simeq> \<tau>\<rbrakk> \<Longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<phi>1 U\<^sub>p \<phi>2 = \<tau> \<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 \<sigma> \<tau>. \<lbrakk>\<And>\<sigma> \<tau>. \<sigma> \<simeq>atoms_pltl \<phi>1\<simeq> \<tau> \<Longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<phi>1 = \<tau> \<Turnstile>\<^sub>p \<phi>1; \<And>\<sigma> \<tau>. \<sigma> \<simeq>atoms_pltl \<phi>2\<simeq> \<tau> \<Longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<phi>2 = \<tau> \<Turnstile>\<^sub>p \<phi>2; \<sigma> \<simeq>atoms_pltl (\<phi>1 implies\<^sub>p \<phi>2)\<simeq> \<tau>\<rbrakk> \<Longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<phi>1 implies\<^sub>p \<phi>2 = \<tau> \<Turnstile>\<^sub>p \<phi>1 implies\<^sub>p \<phi>2
 2. \<And>\<phi> \<sigma> \<tau>. \<lbrakk>\<And>\<sigma> \<tau>. \<sigma> \<simeq>atoms_pltl \<phi>\<simeq> \<tau> \<Longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<phi> = \<tau> \<Turnstile>\<^sub>p \<phi>; \<sigma> \<simeq>atoms_pltl (X\<^sub>p \<phi>)\<simeq> \<tau>\<rbrakk> \<Longrightarrow> \<sigma> \<Turnstile>\<^sub>p X\<^sub>p \<phi> = \<tau> \<Turnstile>\<^sub>p X\<^sub>p \<phi>
 3. \<And>\<phi>1 \<phi>2 \<sigma> \<tau>. \<lbrakk>\<And>\<sigma> \<tau>. \<sigma> \<simeq>atoms_pltl \<phi>1\<simeq> \<tau> \<Longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<phi>1 = \<tau> \<Turnstile>\<^sub>p \<phi>1; \<And>\<sigma> \<tau>. \<sigma> \<simeq>atoms_pltl \<phi>2\<simeq> \<tau> \<Longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<phi>2 = \<tau> \<Turnstile>\<^sub>p \<phi>2; \<sigma> \<simeq>atoms_pltl (\<phi>1 U\<^sub>p \<phi>2)\<simeq> \<tau>\<rbrakk> \<Longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<phi>1 U\<^sub>p \<phi>2 = \<tau> \<Turnstile>\<^sub>p \<phi>1 U\<^sub>p \<phi>2
[PROOF STEP]
fix \<phi> \<psi> \<sigma> \<tau>
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>\<phi>1 \<phi>2 \<sigma> \<tau>. \<lbrakk>\<And>\<sigma> \<tau>. \<sigma> \<simeq>atoms_pltl \<phi>1\<simeq> \<tau> \<Longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<phi>1 = \<tau> \<Turnstile>\<^sub>p \<phi>1; \<And>\<sigma> \<tau>. \<sigma> \<simeq>atoms_pltl \<phi>2\<simeq> \<tau> \<Longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<phi>2 = \<tau> \<Turnstile>\<^sub>p \<phi>2; \<sigma> \<simeq>atoms_pltl (\<phi>1 implies\<^sub>p \<phi>2)\<simeq> \<tau>\<rbrakk> \<Longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<phi>1 implies\<^sub>p \<phi>2 = \<tau> \<Turnstile>\<^sub>p \<phi>1 implies\<^sub>p \<phi>2
 2. \<And>\<phi> \<sigma> \<tau>. \<lbrakk>\<And>\<sigma> \<tau>. \<sigma> \<simeq>atoms_pltl \<phi>\<simeq> \<tau> \<Longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<phi> = \<tau> \<Turnstile>\<^sub>p \<phi>; \<sigma> \<simeq>atoms_pltl (X\<^sub>p \<phi>)\<simeq> \<tau>\<rbrakk> \<Longrightarrow> \<sigma> \<Turnstile>\<^sub>p X\<^sub>p \<phi> = \<tau> \<Turnstile>\<^sub>p X\<^sub>p \<phi>
 3. \<And>\<phi>1 \<phi>2 \<sigma> \<tau>. \<lbrakk>\<And>\<sigma> \<tau>. \<sigma> \<simeq>atoms_pltl \<phi>1\<simeq> \<tau> \<Longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<phi>1 = \<tau> \<Turnstile>\<^sub>p \<phi>1; \<And>\<sigma> \<tau>. \<sigma> \<simeq>atoms_pltl \<phi>2\<simeq> \<tau> \<Longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<phi>2 = \<tau> \<Turnstile>\<^sub>p \<phi>2; \<sigma> \<simeq>atoms_pltl (\<phi>1 U\<^sub>p \<phi>2)\<simeq> \<tau>\<rbrakk> \<Longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<phi>1 U\<^sub>p \<phi>2 = \<tau> \<Turnstile>\<^sub>p \<phi>1 U\<^sub>p \<phi>2
[PROOF STEP]
assume ih: "\<And>\<sigma> \<tau>. ?sim \<sigma> \<phi> \<tau> \<Longrightarrow> ?P \<sigma> \<phi> \<tau>"
             "\<And>\<sigma> \<tau>. ?sim \<sigma> \<psi> \<tau> \<Longrightarrow> ?P \<sigma> \<psi> \<tau>"
     and sim: "?sim \<sigma> (\<phi> implies\<^sub>p \<psi>) \<tau>"
[PROOF STATE]
proof (state)
this:
?\<sigma> \<simeq>atoms_pltl \<phi>\<simeq> ?\<tau> \<Longrightarrow> ?\<sigma> \<Turnstile>\<^sub>p \<phi> = ?\<tau> \<Turnstile>\<^sub>p \<phi>
?\<sigma> \<simeq>atoms_pltl \<psi>\<simeq> ?\<tau> \<Longrightarrow> ?\<sigma> \<Turnstile>\<^sub>p \<psi> = ?\<tau> \<Turnstile>\<^sub>p \<psi>
\<sigma> \<simeq>atoms_pltl (\<phi> implies\<^sub>p \<psi>)\<simeq> \<tau>

goal (3 subgoals):
 1. \<And>\<phi>1 \<phi>2 \<sigma> \<tau>. \<lbrakk>\<And>\<sigma> \<tau>. \<sigma> \<simeq>atoms_pltl \<phi>1\<simeq> \<tau> \<Longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<phi>1 = \<tau> \<Turnstile>\<^sub>p \<phi>1; \<And>\<sigma> \<tau>. \<sigma> \<simeq>atoms_pltl \<phi>2\<simeq> \<tau> \<Longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<phi>2 = \<tau> \<Turnstile>\<^sub>p \<phi>2; \<sigma> \<simeq>atoms_pltl (\<phi>1 implies\<^sub>p \<phi>2)\<simeq> \<tau>\<rbrakk> \<Longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<phi>1 implies\<^sub>p \<phi>2 = \<tau> \<Turnstile>\<^sub>p \<phi>1 implies\<^sub>p \<phi>2
 2. \<And>\<phi> \<sigma> \<tau>. \<lbrakk>\<And>\<sigma> \<tau>. \<sigma> \<simeq>atoms_pltl \<phi>\<simeq> \<tau> \<Longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<phi> = \<tau> \<Turnstile>\<^sub>p \<phi>; \<sigma> \<simeq>atoms_pltl (X\<^sub>p \<phi>)\<simeq> \<tau>\<rbrakk> \<Longrightarrow> \<sigma> \<Turnstile>\<^sub>p X\<^sub>p \<phi> = \<tau> \<Turnstile>\<^sub>p X\<^sub>p \<phi>
 3. \<And>\<phi>1 \<phi>2 \<sigma> \<tau>. \<lbrakk>\<And>\<sigma> \<tau>. \<sigma> \<simeq>atoms_pltl \<phi>1\<simeq> \<tau> \<Longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<phi>1 = \<tau> \<Turnstile>\<^sub>p \<phi>1; \<And>\<sigma> \<tau>. \<sigma> \<simeq>atoms_pltl \<phi>2\<simeq> \<tau> \<Longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<phi>2 = \<tau> \<Turnstile>\<^sub>p \<phi>2; \<sigma> \<simeq>atoms_pltl (\<phi>1 U\<^sub>p \<phi>2)\<simeq> \<tau>\<rbrakk> \<Longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<phi>1 U\<^sub>p \<phi>2 = \<tau> \<Turnstile>\<^sub>p \<phi>1 U\<^sub>p \<phi>2
[PROOF STEP]
from sim
[PROOF STATE]
proof (chain)
picking this:
\<sigma> \<simeq>atoms_pltl (\<phi> implies\<^sub>p \<psi>)\<simeq> \<tau>
[PROOF STEP]
have "?sim \<sigma> \<phi> \<tau>" "?sim \<sigma> \<psi> \<tau>"
[PROOF STATE]
proof (prove)
using this:
\<sigma> \<simeq>atoms_pltl (\<phi> implies\<^sub>p \<psi>)\<simeq> \<tau>

goal (1 subgoal):
 1. \<sigma> \<simeq>atoms_pltl \<phi>\<simeq> \<tau> &&& \<sigma> \<simeq>atoms_pltl \<psi>\<simeq> \<tau>
[PROOF STEP]
by (auto elim: seq_sim_mono)
[PROOF STATE]
proof (state)
this:
\<sigma> \<simeq>atoms_pltl \<phi>\<simeq> \<tau>
\<sigma> \<simeq>atoms_pltl \<psi>\<simeq> \<tau>

goal (3 subgoals):
 1. \<And>\<phi>1 \<phi>2 \<sigma> \<tau>. \<lbrakk>\<And>\<sigma> \<tau>. \<sigma> \<simeq>atoms_pltl \<phi>1\<simeq> \<tau> \<Longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<phi>1 = \<tau> \<Turnstile>\<^sub>p \<phi>1; \<And>\<sigma> \<tau>. \<sigma> \<simeq>atoms_pltl \<phi>2\<simeq> \<tau> \<Longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<phi>2 = \<tau> \<Turnstile>\<^sub>p \<phi>2; \<sigma> \<simeq>atoms_pltl (\<phi>1 implies\<^sub>p \<phi>2)\<simeq> \<tau>\<rbrakk> \<Longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<phi>1 implies\<^sub>p \<phi>2 = \<tau> \<Turnstile>\<^sub>p \<phi>1 implies\<^sub>p \<phi>2
 2. \<And>\<phi> \<sigma> \<tau>. \<lbrakk>\<And>\<sigma> \<tau>. \<sigma> \<simeq>atoms_pltl \<phi>\<simeq> \<tau> \<Longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<phi> = \<tau> \<Turnstile>\<^sub>p \<phi>; \<sigma> \<simeq>atoms_pltl (X\<^sub>p \<phi>)\<simeq> \<tau>\<rbrakk> \<Longrightarrow> \<sigma> \<Turnstile>\<^sub>p X\<^sub>p \<phi> = \<tau> \<Turnstile>\<^sub>p X\<^sub>p \<phi>
 3. \<And>\<phi>1 \<phi>2 \<sigma> \<tau>. \<lbrakk>\<And>\<sigma> \<tau>. \<sigma> \<simeq>atoms_pltl \<phi>1\<simeq> \<tau> \<Longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<phi>1 = \<tau> \<Turnstile>\<^sub>p \<phi>1; \<And>\<sigma> \<tau>. \<sigma> \<simeq>atoms_pltl \<phi>2\<simeq> \<tau> \<Longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<phi>2 = \<tau> \<Turnstile>\<^sub>p \<phi>2; \<sigma> \<simeq>atoms_pltl (\<phi>1 U\<^sub>p \<phi>2)\<simeq> \<tau>\<rbrakk> \<Longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<phi>1 U\<^sub>p \<phi>2 = \<tau> \<Turnstile>\<^sub>p \<phi>1 U\<^sub>p \<phi>2
[PROOF STEP]
with ih
[PROOF STATE]
proof (chain)
picking this:
?\<sigma> \<simeq>atoms_pltl \<phi>\<simeq> ?\<tau> \<Longrightarrow> ?\<sigma> \<Turnstile>\<^sub>p \<phi> = ?\<tau> \<Turnstile>\<^sub>p \<phi>
?\<sigma> \<simeq>atoms_pltl \<psi>\<simeq> ?\<tau> \<Longrightarrow> ?\<sigma> \<Turnstile>\<^sub>p \<psi> = ?\<tau> \<Turnstile>\<^sub>p \<psi>
\<sigma> \<simeq>atoms_pltl \<phi>\<simeq> \<tau>
\<sigma> \<simeq>atoms_pltl \<psi>\<simeq> \<tau>
[PROOF STEP]
show "?P \<sigma> (\<phi> implies\<^sub>p \<psi>) \<tau>"
[PROOF STATE]
proof (prove)
using this:
?\<sigma> \<simeq>atoms_pltl \<phi>\<simeq> ?\<tau> \<Longrightarrow> ?\<sigma> \<Turnstile>\<^sub>p \<phi> = ?\<tau> \<Turnstile>\<^sub>p \<phi>
?\<sigma> \<simeq>atoms_pltl \<psi>\<simeq> ?\<tau> \<Longrightarrow> ?\<sigma> \<Turnstile>\<^sub>p \<psi> = ?\<tau> \<Turnstile>\<^sub>p \<psi>
\<sigma> \<simeq>atoms_pltl \<phi>\<simeq> \<tau>
\<sigma> \<simeq>atoms_pltl \<psi>\<simeq> \<tau>

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

goal (2 subgoals):
 1. \<And>\<phi> \<sigma> \<tau>. \<lbrakk>\<And>\<sigma> \<tau>. \<sigma> \<simeq>atoms_pltl \<phi>\<simeq> \<tau> \<Longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<phi> = \<tau> \<Turnstile>\<^sub>p \<phi>; \<sigma> \<simeq>atoms_pltl (X\<^sub>p \<phi>)\<simeq> \<tau>\<rbrakk> \<Longrightarrow> \<sigma> \<Turnstile>\<^sub>p X\<^sub>p \<phi> = \<tau> \<Turnstile>\<^sub>p X\<^sub>p \<phi>
 2. \<And>\<phi>1 \<phi>2 \<sigma> \<tau>. \<lbrakk>\<And>\<sigma> \<tau>. \<sigma> \<simeq>atoms_pltl \<phi>1\<simeq> \<tau> \<Longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<phi>1 = \<tau> \<Turnstile>\<^sub>p \<phi>1; \<And>\<sigma> \<tau>. \<sigma> \<simeq>atoms_pltl \<phi>2\<simeq> \<tau> \<Longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<phi>2 = \<tau> \<Turnstile>\<^sub>p \<phi>2; \<sigma> \<simeq>atoms_pltl (\<phi>1 U\<^sub>p \<phi>2)\<simeq> \<tau>\<rbrakk> \<Longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<phi>1 U\<^sub>p \<phi>2 = \<tau> \<Turnstile>\<^sub>p \<phi>1 U\<^sub>p \<phi>2
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>\<phi> \<sigma> \<tau>. \<lbrakk>\<And>\<sigma> \<tau>. \<sigma> \<simeq>atoms_pltl \<phi>\<simeq> \<tau> \<Longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<phi> = \<tau> \<Turnstile>\<^sub>p \<phi>; \<sigma> \<simeq>atoms_pltl (X\<^sub>p \<phi>)\<simeq> \<tau>\<rbrakk> \<Longrightarrow> \<sigma> \<Turnstile>\<^sub>p X\<^sub>p \<phi> = \<tau> \<Turnstile>\<^sub>p X\<^sub>p \<phi>
 2. \<And>\<phi>1 \<phi>2 \<sigma> \<tau>. \<lbrakk>\<And>\<sigma> \<tau>. \<sigma> \<simeq>atoms_pltl \<phi>1\<simeq> \<tau> \<Longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<phi>1 = \<tau> \<Turnstile>\<^sub>p \<phi>1; \<And>\<sigma> \<tau>. \<sigma> \<simeq>atoms_pltl \<phi>2\<simeq> \<tau> \<Longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<phi>2 = \<tau> \<Turnstile>\<^sub>p \<phi>2; \<sigma> \<simeq>atoms_pltl (\<phi>1 U\<^sub>p \<phi>2)\<simeq> \<tau>\<rbrakk> \<Longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<phi>1 U\<^sub>p \<phi>2 = \<tau> \<Turnstile>\<^sub>p \<phi>1 U\<^sub>p \<phi>2
[PROOF STEP]
fix \<phi> \<sigma> \<tau>
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>\<phi> \<sigma> \<tau>. \<lbrakk>\<And>\<sigma> \<tau>. \<sigma> \<simeq>atoms_pltl \<phi>\<simeq> \<tau> \<Longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<phi> = \<tau> \<Turnstile>\<^sub>p \<phi>; \<sigma> \<simeq>atoms_pltl (X\<^sub>p \<phi>)\<simeq> \<tau>\<rbrakk> \<Longrightarrow> \<sigma> \<Turnstile>\<^sub>p X\<^sub>p \<phi> = \<tau> \<Turnstile>\<^sub>p X\<^sub>p \<phi>
 2. \<And>\<phi>1 \<phi>2 \<sigma> \<tau>. \<lbrakk>\<And>\<sigma> \<tau>. \<sigma> \<simeq>atoms_pltl \<phi>1\<simeq> \<tau> \<Longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<phi>1 = \<tau> \<Turnstile>\<^sub>p \<phi>1; \<And>\<sigma> \<tau>. \<sigma> \<simeq>atoms_pltl \<phi>2\<simeq> \<tau> \<Longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<phi>2 = \<tau> \<Turnstile>\<^sub>p \<phi>2; \<sigma> \<simeq>atoms_pltl (\<phi>1 U\<^sub>p \<phi>2)\<simeq> \<tau>\<rbrakk> \<Longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<phi>1 U\<^sub>p \<phi>2 = \<tau> \<Turnstile>\<^sub>p \<phi>1 U\<^sub>p \<phi>2
[PROOF STEP]
assume ih: "\<And>\<sigma> \<tau>. ?sim \<sigma> \<phi> \<tau> \<Longrightarrow> ?P \<sigma> \<phi> \<tau>"
     and sim: "\<sigma> \<simeq> atoms_pltl (X\<^sub>p \<phi>) \<simeq> \<tau>"
[PROOF STATE]
proof (state)
this:
?\<sigma> \<simeq>atoms_pltl \<phi>\<simeq> ?\<tau> \<Longrightarrow> ?\<sigma> \<Turnstile>\<^sub>p \<phi> = ?\<tau> \<Turnstile>\<^sub>p \<phi>
\<sigma> \<simeq>atoms_pltl (X\<^sub>p \<phi>)\<simeq> \<tau>

goal (2 subgoals):
 1. \<And>\<phi> \<sigma> \<tau>. \<lbrakk>\<And>\<sigma> \<tau>. \<sigma> \<simeq>atoms_pltl \<phi>\<simeq> \<tau> \<Longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<phi> = \<tau> \<Turnstile>\<^sub>p \<phi>; \<sigma> \<simeq>atoms_pltl (X\<^sub>p \<phi>)\<simeq> \<tau>\<rbrakk> \<Longrightarrow> \<sigma> \<Turnstile>\<^sub>p X\<^sub>p \<phi> = \<tau> \<Turnstile>\<^sub>p X\<^sub>p \<phi>
 2. \<And>\<phi>1 \<phi>2 \<sigma> \<tau>. \<lbrakk>\<And>\<sigma> \<tau>. \<sigma> \<simeq>atoms_pltl \<phi>1\<simeq> \<tau> \<Longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<phi>1 = \<tau> \<Turnstile>\<^sub>p \<phi>1; \<And>\<sigma> \<tau>. \<sigma> \<simeq>atoms_pltl \<phi>2\<simeq> \<tau> \<Longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<phi>2 = \<tau> \<Turnstile>\<^sub>p \<phi>2; \<sigma> \<simeq>atoms_pltl (\<phi>1 U\<^sub>p \<phi>2)\<simeq> \<tau>\<rbrakk> \<Longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<phi>1 U\<^sub>p \<phi>2 = \<tau> \<Turnstile>\<^sub>p \<phi>1 U\<^sub>p \<phi>2
[PROOF STEP]
from sim
[PROOF STATE]
proof (chain)
picking this:
\<sigma> \<simeq>atoms_pltl (X\<^sub>p \<phi>)\<simeq> \<tau>
[PROOF STEP]
have "(\<sigma>[1..]) \<simeq> atoms_pltl \<phi> \<simeq> (\<tau>[1..])"
[PROOF STATE]
proof (prove)
using this:
\<sigma> \<simeq>atoms_pltl (X\<^sub>p \<phi>)\<simeq> \<tau>

goal (1 subgoal):
 1. \<sigma> [1..] \<simeq>atoms_pltl \<phi>\<simeq> \<tau> [1..]
[PROOF STEP]
by (auto simp: seq_sim_def)
[PROOF STATE]
proof (state)
this:
\<sigma> [1..] \<simeq>atoms_pltl \<phi>\<simeq> \<tau> [1..]

goal (2 subgoals):
 1. \<And>\<phi> \<sigma> \<tau>. \<lbrakk>\<And>\<sigma> \<tau>. \<sigma> \<simeq>atoms_pltl \<phi>\<simeq> \<tau> \<Longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<phi> = \<tau> \<Turnstile>\<^sub>p \<phi>; \<sigma> \<simeq>atoms_pltl (X\<^sub>p \<phi>)\<simeq> \<tau>\<rbrakk> \<Longrightarrow> \<sigma> \<Turnstile>\<^sub>p X\<^sub>p \<phi> = \<tau> \<Turnstile>\<^sub>p X\<^sub>p \<phi>
 2. \<And>\<phi>1 \<phi>2 \<sigma> \<tau>. \<lbrakk>\<And>\<sigma> \<tau>. \<sigma> \<simeq>atoms_pltl \<phi>1\<simeq> \<tau> \<Longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<phi>1 = \<tau> \<Turnstile>\<^sub>p \<phi>1; \<And>\<sigma> \<tau>. \<sigma> \<simeq>atoms_pltl \<phi>2\<simeq> \<tau> \<Longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<phi>2 = \<tau> \<Turnstile>\<^sub>p \<phi>2; \<sigma> \<simeq>atoms_pltl (\<phi>1 U\<^sub>p \<phi>2)\<simeq> \<tau>\<rbrakk> \<Longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<phi>1 U\<^sub>p \<phi>2 = \<tau> \<Turnstile>\<^sub>p \<phi>1 U\<^sub>p \<phi>2
[PROOF STEP]
with ih
[PROOF STATE]
proof (chain)
picking this:
?\<sigma> \<simeq>atoms_pltl \<phi>\<simeq> ?\<tau> \<Longrightarrow> ?\<sigma> \<Turnstile>\<^sub>p \<phi> = ?\<tau> \<Turnstile>\<^sub>p \<phi>
\<sigma> [1..] \<simeq>atoms_pltl \<phi>\<simeq> \<tau> [1..]
[PROOF STEP]
show "?P \<sigma> (X\<^sub>p \<phi>) \<tau>"
[PROOF STATE]
proof (prove)
using this:
?\<sigma> \<simeq>atoms_pltl \<phi>\<simeq> ?\<tau> \<Longrightarrow> ?\<sigma> \<Turnstile>\<^sub>p \<phi> = ?\<tau> \<Turnstile>\<^sub>p \<phi>
\<sigma> [1..] \<simeq>atoms_pltl \<phi>\<simeq> \<tau> [1..]

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

goal (1 subgoal):
 1. \<And>\<phi>1 \<phi>2 \<sigma> \<tau>. \<lbrakk>\<And>\<sigma> \<tau>. \<sigma> \<simeq>atoms_pltl \<phi>1\<simeq> \<tau> \<Longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<phi>1 = \<tau> \<Turnstile>\<^sub>p \<phi>1; \<And>\<sigma> \<tau>. \<sigma> \<simeq>atoms_pltl \<phi>2\<simeq> \<tau> \<Longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<phi>2 = \<tau> \<Turnstile>\<^sub>p \<phi>2; \<sigma> \<simeq>atoms_pltl (\<phi>1 U\<^sub>p \<phi>2)\<simeq> \<tau>\<rbrakk> \<Longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<phi>1 U\<^sub>p \<phi>2 = \<tau> \<Turnstile>\<^sub>p \<phi>1 U\<^sub>p \<phi>2
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>\<phi>1 \<phi>2 \<sigma> \<tau>. \<lbrakk>\<And>\<sigma> \<tau>. \<sigma> \<simeq>atoms_pltl \<phi>1\<simeq> \<tau> \<Longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<phi>1 = \<tau> \<Turnstile>\<^sub>p \<phi>1; \<And>\<sigma> \<tau>. \<sigma> \<simeq>atoms_pltl \<phi>2\<simeq> \<tau> \<Longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<phi>2 = \<tau> \<Turnstile>\<^sub>p \<phi>2; \<sigma> \<simeq>atoms_pltl (\<phi>1 U\<^sub>p \<phi>2)\<simeq> \<tau>\<rbrakk> \<Longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<phi>1 U\<^sub>p \<phi>2 = \<tau> \<Turnstile>\<^sub>p \<phi>1 U\<^sub>p \<phi>2
[PROOF STEP]
fix \<phi> \<psi> \<sigma> \<tau>
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>\<phi>1 \<phi>2 \<sigma> \<tau>. \<lbrakk>\<And>\<sigma> \<tau>. \<sigma> \<simeq>atoms_pltl \<phi>1\<simeq> \<tau> \<Longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<phi>1 = \<tau> \<Turnstile>\<^sub>p \<phi>1; \<And>\<sigma> \<tau>. \<sigma> \<simeq>atoms_pltl \<phi>2\<simeq> \<tau> \<Longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<phi>2 = \<tau> \<Turnstile>\<^sub>p \<phi>2; \<sigma> \<simeq>atoms_pltl (\<phi>1 U\<^sub>p \<phi>2)\<simeq> \<tau>\<rbrakk> \<Longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<phi>1 U\<^sub>p \<phi>2 = \<tau> \<Turnstile>\<^sub>p \<phi>1 U\<^sub>p \<phi>2
[PROOF STEP]
assume ih: "\<And>\<sigma> \<tau>. ?sim \<sigma> \<phi> \<tau> \<Longrightarrow> ?P \<sigma> \<phi> \<tau>"
             "\<And>\<sigma> \<tau>. ?sim \<sigma> \<psi> \<tau> \<Longrightarrow> ?P \<sigma> \<psi> \<tau>"
     and sim: "?sim \<sigma> (\<phi> U\<^sub>p \<psi>) \<tau>"
[PROOF STATE]
proof (state)
this:
?\<sigma> \<simeq>atoms_pltl \<phi>\<simeq> ?\<tau> \<Longrightarrow> ?\<sigma> \<Turnstile>\<^sub>p \<phi> = ?\<tau> \<Turnstile>\<^sub>p \<phi>
?\<sigma> \<simeq>atoms_pltl \<psi>\<simeq> ?\<tau> \<Longrightarrow> ?\<sigma> \<Turnstile>\<^sub>p \<psi> = ?\<tau> \<Turnstile>\<^sub>p \<psi>
\<sigma> \<simeq>atoms_pltl (\<phi> U\<^sub>p \<psi>)\<simeq> \<tau>

goal (1 subgoal):
 1. \<And>\<phi>1 \<phi>2 \<sigma> \<tau>. \<lbrakk>\<And>\<sigma> \<tau>. \<sigma> \<simeq>atoms_pltl \<phi>1\<simeq> \<tau> \<Longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<phi>1 = \<tau> \<Turnstile>\<^sub>p \<phi>1; \<And>\<sigma> \<tau>. \<sigma> \<simeq>atoms_pltl \<phi>2\<simeq> \<tau> \<Longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<phi>2 = \<tau> \<Turnstile>\<^sub>p \<phi>2; \<sigma> \<simeq>atoms_pltl (\<phi>1 U\<^sub>p \<phi>2)\<simeq> \<tau>\<rbrakk> \<Longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<phi>1 U\<^sub>p \<phi>2 = \<tau> \<Turnstile>\<^sub>p \<phi>1 U\<^sub>p \<phi>2
[PROOF STEP]
from sim
[PROOF STATE]
proof (chain)
picking this:
\<sigma> \<simeq>atoms_pltl (\<phi> U\<^sub>p \<psi>)\<simeq> \<tau>
[PROOF STEP]
have "\<forall>i. (\<sigma>[i..]) \<simeq> atoms_pltl \<phi> \<simeq> (\<tau>[i..])" "\<forall>j. (\<sigma>[j..]) \<simeq> atoms_pltl \<psi> \<simeq> (\<tau>[j..])"
[PROOF STATE]
proof (prove)
using this:
\<sigma> \<simeq>atoms_pltl (\<phi> U\<^sub>p \<psi>)\<simeq> \<tau>

goal (1 subgoal):
 1. \<forall>i. \<sigma> [i..] \<simeq>atoms_pltl \<phi>\<simeq> \<tau> [i..] &&& \<forall>j. \<sigma> [j..] \<simeq>atoms_pltl \<psi>\<simeq> \<tau> [j..]
[PROOF STEP]
by (auto simp: seq_sim_def state_sim_def)
[PROOF STATE]
proof (state)
this:
\<forall>i. \<sigma> [i..] \<simeq>atoms_pltl \<phi>\<simeq> \<tau> [i..]
\<forall>j. \<sigma> [j..] \<simeq>atoms_pltl \<psi>\<simeq> \<tau> [j..]

goal (1 subgoal):
 1. \<And>\<phi>1 \<phi>2 \<sigma> \<tau>. \<lbrakk>\<And>\<sigma> \<tau>. \<sigma> \<simeq>atoms_pltl \<phi>1\<simeq> \<tau> \<Longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<phi>1 = \<tau> \<Turnstile>\<^sub>p \<phi>1; \<And>\<sigma> \<tau>. \<sigma> \<simeq>atoms_pltl \<phi>2\<simeq> \<tau> \<Longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<phi>2 = \<tau> \<Turnstile>\<^sub>p \<phi>2; \<sigma> \<simeq>atoms_pltl (\<phi>1 U\<^sub>p \<phi>2)\<simeq> \<tau>\<rbrakk> \<Longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<phi>1 U\<^sub>p \<phi>2 = \<tau> \<Turnstile>\<^sub>p \<phi>1 U\<^sub>p \<phi>2
[PROOF STEP]
with ih
[PROOF STATE]
proof (chain)
picking this:
?\<sigma> \<simeq>atoms_pltl \<phi>\<simeq> ?\<tau> \<Longrightarrow> ?\<sigma> \<Turnstile>\<^sub>p \<phi> = ?\<tau> \<Turnstile>\<^sub>p \<phi>
?\<sigma> \<simeq>atoms_pltl \<psi>\<simeq> ?\<tau> \<Longrightarrow> ?\<sigma> \<Turnstile>\<^sub>p \<psi> = ?\<tau> \<Turnstile>\<^sub>p \<psi>
\<forall>i. \<sigma> [i..] \<simeq>atoms_pltl \<phi>\<simeq> \<tau> [i..]
\<forall>j. \<sigma> [j..] \<simeq>atoms_pltl \<psi>\<simeq> \<tau> [j..]
[PROOF STEP]
have "\<forall>i. ?P (\<sigma>[i..]) \<phi> (\<tau>[i..])" "\<forall>j. ?P (\<sigma>[j..]) \<psi> (\<tau>[j..])"
[PROOF STATE]
proof (prove)
using this:
?\<sigma> \<simeq>atoms_pltl \<phi>\<simeq> ?\<tau> \<Longrightarrow> ?\<sigma> \<Turnstile>\<^sub>p \<phi> = ?\<tau> \<Turnstile>\<^sub>p \<phi>
?\<sigma> \<simeq>atoms_pltl \<psi>\<simeq> ?\<tau> \<Longrightarrow> ?\<sigma> \<Turnstile>\<^sub>p \<psi> = ?\<tau> \<Turnstile>\<^sub>p \<psi>
\<forall>i. \<sigma> [i..] \<simeq>atoms_pltl \<phi>\<simeq> \<tau> [i..]
\<forall>j. \<sigma> [j..] \<simeq>atoms_pltl \<psi>\<simeq> \<tau> [j..]

goal (1 subgoal):
 1. \<forall>i. \<sigma> [i..] \<Turnstile>\<^sub>p \<phi> = \<tau> [i..] \<Turnstile>\<^sub>p \<phi> &&& \<forall>j. \<sigma> [j..] \<Turnstile>\<^sub>p \<psi> = \<tau> [j..] \<Turnstile>\<^sub>p \<psi>
[PROOF STEP]
by blast+
[PROOF STATE]
proof (state)
this:
\<forall>i. \<sigma> [i..] \<Turnstile>\<^sub>p \<phi> = \<tau> [i..] \<Turnstile>\<^sub>p \<phi>
\<forall>j. \<sigma> [j..] \<Turnstile>\<^sub>p \<psi> = \<tau> [j..] \<Turnstile>\<^sub>p \<psi>

goal (1 subgoal):
 1. \<And>\<phi>1 \<phi>2 \<sigma> \<tau>. \<lbrakk>\<And>\<sigma> \<tau>. \<sigma> \<simeq>atoms_pltl \<phi>1\<simeq> \<tau> \<Longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<phi>1 = \<tau> \<Turnstile>\<^sub>p \<phi>1; \<And>\<sigma> \<tau>. \<sigma> \<simeq>atoms_pltl \<phi>2\<simeq> \<tau> \<Longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<phi>2 = \<tau> \<Turnstile>\<^sub>p \<phi>2; \<sigma> \<simeq>atoms_pltl (\<phi>1 U\<^sub>p \<phi>2)\<simeq> \<tau>\<rbrakk> \<Longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<phi>1 U\<^sub>p \<phi>2 = \<tau> \<Turnstile>\<^sub>p \<phi>1 U\<^sub>p \<phi>2
[PROOF STEP]
thus "?P \<sigma> (\<phi> U\<^sub>p \<psi>) \<tau>"
[PROOF STATE]
proof (prove)
using this:
\<forall>i. \<sigma> [i..] \<Turnstile>\<^sub>p \<phi> = \<tau> [i..] \<Turnstile>\<^sub>p \<phi>
\<forall>j. \<sigma> [j..] \<Turnstile>\<^sub>p \<psi> = \<tau> [j..] \<Turnstile>\<^sub>p \<psi>

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma canonize_state_sim: "canonize A s ~A~ s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. canonize A s ~A~ s
[PROOF STEP]
unfolding canonize_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (SOME t. t ~A~ s) ~A~ s
[PROOF STEP]
by (rule someI, rule state_sim_refl)


[STATEMENT]
lemma canonize_canonical:
  assumes st: "s ~A~ t"
  shows "canonize A s = canonize A t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. canonize A s = canonize A t
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. canonize A s = canonize A t
[PROOF STEP]
from st
[PROOF STATE]
proof (chain)
picking this:
s ~A~ t
[PROOF STEP]
have "\<forall>u. (u ~A~s) = (u ~A~ t)"
[PROOF STATE]
proof (prove)
using this:
s ~A~ t

goal (1 subgoal):
 1. \<forall>u. (u ~A~ s) = (u ~A~ t)
[PROOF STEP]
by (auto elim: state_sim_sym state_sim_trans)
[PROOF STATE]
proof (state)
this:
\<forall>u. (u ~A~ s) = (u ~A~ t)

goal (1 subgoal):
 1. canonize A s = canonize A t
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>u. (u ~A~ s) = (u ~A~ t)

goal (1 subgoal):
 1. canonize A s = canonize A t
[PROOF STEP]
unfolding canonize_def
[PROOF STATE]
proof (prove)
using this:
\<forall>u. (u ~A~ s) = (u ~A~ t)

goal (1 subgoal):
 1. (SOME t. t ~A~ s) = (SOME ta. ta ~A~ t)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
canonize A s = canonize A t

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma canonize_idempotent:
  "canonize A (canonize A s) = canonize A s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. canonize A (canonize A s) = canonize A s
[PROOF STEP]
by (rule canonize_canonical[OF canonize_state_sim])


[STATEMENT]
lemma canonical_suffix:
  "canonical_sequence A \<sigma> \<Longrightarrow> canonical_sequence A (\<sigma>[k..])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. canonical_sequence A \<sigma> \<Longrightarrow> canonical_sequence A \<sigma> [k..]
[PROOF STEP]
by (auto simp: canonical_sequence_def)


[STATEMENT]
lemma canonical_sampled:
  "canonical_sequence A \<sigma> \<Longrightarrow> canonical_sequence A (\<sigma> \<circ> f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. canonical_sequence A \<sigma> \<Longrightarrow> canonical_sequence A (\<sigma> \<circ> f)
[PROOF STEP]
by (auto simp: canonical_sequence_def)


[STATEMENT]
lemma canonical_reduced:
  "canonical_sequence A \<sigma> \<Longrightarrow> canonical_sequence A (\<natural>\<sigma>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. canonical_sequence A \<sigma> \<Longrightarrow> canonical_sequence A (\<natural>\<sigma>)
[PROOF STEP]
unfolding stutter_reduced_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. canonical_sequence A \<sigma> \<Longrightarrow> canonical_sequence A (\<sigma> \<circ> max_stutter_sampler \<sigma>)
[PROOF STEP]
by (rule canonical_sampled)


[STATEMENT]
lemma canonical_exists:
  obtains \<tau> where "\<tau> \<simeq>A\<simeq> \<sigma>" "canonical_sequence A \<tau>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>\<tau>. \<lbrakk>\<tau> \<simeq>A\<simeq> \<sigma>; canonical_sequence A \<tau>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>\<tau>. \<lbrakk>\<tau> \<simeq>A\<simeq> \<sigma>; canonical_sequence A \<tau>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have "(canonize A \<circ> \<sigma>) \<simeq>A\<simeq> \<sigma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (canonize A \<circ> \<sigma>) \<simeq>A\<simeq> \<sigma>
[PROOF STEP]
by (simp add: seq_sim_def canonize_state_sim)
[PROOF STATE]
proof (state)
this:
(canonize A \<circ> \<sigma>) \<simeq>A\<simeq> \<sigma>

goal (1 subgoal):
 1. (\<And>\<tau>. \<lbrakk>\<tau> \<simeq>A\<simeq> \<sigma>; canonical_sequence A \<tau>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(canonize A \<circ> \<sigma>) \<simeq>A\<simeq> \<sigma>

goal (1 subgoal):
 1. (\<And>\<tau>. \<lbrakk>\<tau> \<simeq>A\<simeq> \<sigma>; canonical_sequence A \<tau>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have "canonical_sequence A (canonize A \<circ> \<sigma>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. canonical_sequence A (canonize A \<circ> \<sigma>)
[PROOF STEP]
by (auto simp: canonical_sequence_def canonize_idempotent
             dest: canonize_canonical)
[PROOF STATE]
proof (state)
this:
canonical_sequence A (canonize A \<circ> \<sigma>)

goal (1 subgoal):
 1. (\<And>\<tau>. \<lbrakk>\<tau> \<simeq>A\<simeq> \<sigma>; canonical_sequence A \<tau>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(canonize A \<circ> \<sigma>) \<simeq>A\<simeq> \<sigma>
canonical_sequence A (canonize A \<circ> \<sigma>)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(canonize A \<circ> \<sigma>) \<simeq>A\<simeq> \<sigma>
canonical_sequence A (canonize A \<circ> \<sigma>)

goal (1 subgoal):
 1. thesis
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
(canonize A \<circ> \<sigma>) \<simeq>A\<simeq> \<sigma>
canonical_sequence A (canonize A \<circ> \<sigma>)
\<lbrakk>?\<tau> \<simeq>A\<simeq> \<sigma>; canonical_sequence A ?\<tau>\<rbrakk> \<Longrightarrow> thesis

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma characteristic_holds:
  "finite A \<Longrightarrow> \<sigma> \<Turnstile>\<^sub>p characteristic_formula A (\<sigma> 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite A \<Longrightarrow> \<sigma> \<Turnstile>\<^sub>p characteristic_formula A (\<sigma> 0)
[PROOF STEP]
by (auto simp: characteristic_formula_def)


[STATEMENT]
lemma characteristic_state_sim:
  assumes fin: "finite A"
  shows "(\<sigma> 0 ~A~ \<tau> 0) = (\<tau> \<Turnstile>\<^sub>p characteristic_formula A (\<sigma> (0::nat)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<sigma> 0 ~A~ \<tau> 0) = \<tau> \<Turnstile>\<^sub>p characteristic_formula A (\<sigma> 0)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<sigma> 0 ~A~ \<tau> 0 \<Longrightarrow> \<tau> \<Turnstile>\<^sub>p characteristic_formula A (\<sigma> 0)
 2. \<tau> \<Turnstile>\<^sub>p characteristic_formula A (\<sigma> 0) \<Longrightarrow> \<sigma> 0 ~A~ \<tau> 0
[PROOF STEP]
assume sim: "\<sigma> 0 ~A~ \<tau> 0"
[PROOF STATE]
proof (state)
this:
\<sigma> 0 ~A~ \<tau> 0

goal (2 subgoals):
 1. \<sigma> 0 ~A~ \<tau> 0 \<Longrightarrow> \<tau> \<Turnstile>\<^sub>p characteristic_formula A (\<sigma> 0)
 2. \<tau> \<Turnstile>\<^sub>p characteristic_formula A (\<sigma> 0) \<Longrightarrow> \<sigma> 0 ~A~ \<tau> 0
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
\<sigma> 0 ~A~ \<tau> 0

goal (2 subgoals):
 1. \<sigma> 0 ~A~ \<tau> 0 \<Longrightarrow> \<tau> \<Turnstile>\<^sub>p characteristic_formula A (\<sigma> 0)
 2. \<tau> \<Turnstile>\<^sub>p characteristic_formula A (\<sigma> 0) \<Longrightarrow> \<sigma> 0 ~A~ \<tau> 0
[PROOF STEP]
fix p
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<sigma> 0 ~A~ \<tau> 0 \<Longrightarrow> \<tau> \<Turnstile>\<^sub>p characteristic_formula A (\<sigma> 0)
 2. \<tau> \<Turnstile>\<^sub>p characteristic_formula A (\<sigma> 0) \<Longrightarrow> \<sigma> 0 ~A~ \<tau> 0
[PROOF STEP]
assume "p \<in> A"
[PROOF STATE]
proof (state)
this:
p \<in> A

goal (2 subgoals):
 1. \<sigma> 0 ~A~ \<tau> 0 \<Longrightarrow> \<tau> \<Turnstile>\<^sub>p characteristic_formula A (\<sigma> 0)
 2. \<tau> \<Turnstile>\<^sub>p characteristic_formula A (\<sigma> 0) \<Longrightarrow> \<sigma> 0 ~A~ \<tau> 0
[PROOF STEP]
with sim
[PROOF STATE]
proof (chain)
picking this:
\<sigma> 0 ~A~ \<tau> 0
p \<in> A
[PROOF STEP]
have "p (\<tau> 0) = p (\<sigma> 0)"
[PROOF STATE]
proof (prove)
using this:
\<sigma> 0 ~A~ \<tau> 0
p \<in> A

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

goal (2 subgoals):
 1. \<sigma> 0 ~A~ \<tau> 0 \<Longrightarrow> \<tau> \<Turnstile>\<^sub>p characteristic_formula A (\<sigma> 0)
 2. \<tau> \<Turnstile>\<^sub>p characteristic_formula A (\<sigma> 0) \<Longrightarrow> \<sigma> 0 ~A~ \<tau> 0
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?p2 \<in> A \<Longrightarrow> ?p2 (\<tau> 0) = ?p2 (\<sigma> 0)

goal (2 subgoals):
 1. \<sigma> 0 ~A~ \<tau> 0 \<Longrightarrow> \<tau> \<Turnstile>\<^sub>p characteristic_formula A (\<sigma> 0)
 2. \<tau> \<Turnstile>\<^sub>p characteristic_formula A (\<sigma> 0) \<Longrightarrow> \<sigma> 0 ~A~ \<tau> 0
[PROOF STEP]
with fin
[PROOF STATE]
proof (chain)
picking this:
finite A
?p2 \<in> A \<Longrightarrow> ?p2 (\<tau> 0) = ?p2 (\<sigma> 0)
[PROOF STEP]
show "\<tau> \<Turnstile>\<^sub>p characteristic_formula A (\<sigma> 0)"
[PROOF STATE]
proof (prove)
using this:
finite A
?p2 \<in> A \<Longrightarrow> ?p2 (\<tau> 0) = ?p2 (\<sigma> 0)

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

goal (1 subgoal):
 1. \<tau> \<Turnstile>\<^sub>p characteristic_formula A (\<sigma> 0) \<Longrightarrow> \<sigma> 0 ~A~ \<tau> 0
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<tau> \<Turnstile>\<^sub>p characteristic_formula A (\<sigma> 0) \<Longrightarrow> \<sigma> 0 ~A~ \<tau> 0
[PROOF STEP]
assume "\<tau> \<Turnstile>\<^sub>p characteristic_formula A (\<sigma> 0)"
[PROOF STATE]
proof (state)
this:
\<tau> \<Turnstile>\<^sub>p characteristic_formula A (\<sigma> 0)

goal (1 subgoal):
 1. \<tau> \<Turnstile>\<^sub>p characteristic_formula A (\<sigma> 0) \<Longrightarrow> \<sigma> 0 ~A~ \<tau> 0
[PROOF STEP]
with fin
[PROOF STATE]
proof (chain)
picking this:
finite A
\<tau> \<Turnstile>\<^sub>p characteristic_formula A (\<sigma> 0)
[PROOF STEP]
show "\<sigma> 0 ~A~ \<tau> 0"
[PROOF STATE]
proof (prove)
using this:
finite A
\<tau> \<Turnstile>\<^sub>p characteristic_formula A (\<sigma> 0)

goal (1 subgoal):
 1. \<sigma> 0 ~A~ \<tau> 0
[PROOF STEP]
by (auto simp: characteristic_formula_def state_sim_def)
[PROOF STATE]
proof (state)
this:
\<sigma> 0 ~A~ \<tau> 0

goal:
No subgoals!
[PROOF STEP]
qed