[STATEMENT]
lemma stream_enc_welldef: "\<lbrakk>stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) \<phi>;
  wf_interp_for_formula (w, I) \<phi>; wf_interp_for_formula (w', I') \<phi>\<rbrakk> \<Longrightarrow>
  (w, I) \<Turnstile> \<phi> \<longleftrightarrow> (w', I') \<Turnstile> \<phi>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) \<phi>; wf_interp_for_formula (w, I) \<phi>; wf_interp_for_formula (w', I') \<phi>\<rbrakk> \<Longrightarrow> ((w, I) \<Turnstile> \<phi>) = ((w', I') \<Turnstile> \<phi>)
[PROOF STEP]
proof (induction \<phi> arbitrary: w w' I I')
[PROOF STATE]
proof (state)
goal (8 subgoals):
 1. \<And>x1 x2 w w' I I'. \<lbrakk>stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) (FQ x1 x2); wf_interp_for_formula (w, I) (FQ x1 x2); wf_interp_for_formula (w', I') (FQ x1 x2)\<rbrakk> \<Longrightarrow> ((w, I) \<Turnstile> FQ x1 x2) = ((w', I') \<Turnstile> FQ x1 x2)
 2. \<And>x1 x2 w w' I I'. \<lbrakk>stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) (FLess x1 x2); wf_interp_for_formula (w, I) (FLess x1 x2); wf_interp_for_formula (w', I') (FLess x1 x2)\<rbrakk> \<Longrightarrow> ((w, I) \<Turnstile> FLess x1 x2) = ((w', I') \<Turnstile> FLess x1 x2)
 3. \<And>x1 x2 w w' I I'. \<lbrakk>stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) (FIn x1 x2); wf_interp_for_formula (w, I) (FIn x1 x2); wf_interp_for_formula (w', I') (FIn x1 x2)\<rbrakk> \<Longrightarrow> ((w, I) \<Turnstile> FIn x1 x2) = ((w', I') \<Turnstile> FIn x1 x2)
 4. \<And>\<phi> w w' I I'. \<lbrakk>\<And>w w' I I'. \<lbrakk>stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) \<phi>; wf_interp_for_formula (w, I) \<phi>; wf_interp_for_formula (w', I') \<phi>\<rbrakk> \<Longrightarrow> ((w, I) \<Turnstile> \<phi>) = ((w', I') \<Turnstile> \<phi>); stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) (FNot \<phi>); wf_interp_for_formula (w, I) (FNot \<phi>); wf_interp_for_formula (w', I') (FNot \<phi>)\<rbrakk> \<Longrightarrow> ((w, I) \<Turnstile> FNot \<phi>) = ((w', I') \<Turnstile> FNot \<phi>)
 5. \<And>\<phi>1 \<phi>2 w w' I I'. \<lbrakk>\<And>w w' I I'. \<lbrakk>stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) \<phi>1; wf_interp_for_formula (w, I) \<phi>1; wf_interp_for_formula (w', I') \<phi>1\<rbrakk> \<Longrightarrow> ((w, I) \<Turnstile> \<phi>1) = ((w', I') \<Turnstile> \<phi>1); \<And>w w' I I'. \<lbrakk>stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) \<phi>2; wf_interp_for_formula (w, I) \<phi>2; wf_interp_for_formula (w', I') \<phi>2\<rbrakk> \<Longrightarrow> ((w, I) \<Turnstile> \<phi>2) = ((w', I') \<Turnstile> \<phi>2); stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) (FOr \<phi>1 \<phi>2); wf_interp_for_formula (w, I) (FOr \<phi>1 \<phi>2); wf_interp_for_formula (w', I') (FOr \<phi>1 \<phi>2)\<rbrakk> \<Longrightarrow> ((w, I) \<Turnstile> FOr \<phi>1 \<phi>2) = ((w', I') \<Turnstile> FOr \<phi>1 \<phi>2)
 6. \<And>\<phi>1 \<phi>2 w w' I I'. \<lbrakk>\<And>w w' I I'. \<lbrakk>stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) \<phi>1; wf_interp_for_formula (w, I) \<phi>1; wf_interp_for_formula (w', I') \<phi>1\<rbrakk> \<Longrightarrow> ((w, I) \<Turnstile> \<phi>1) = ((w', I') \<Turnstile> \<phi>1); \<And>w w' I I'. \<lbrakk>stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) \<phi>2; wf_interp_for_formula (w, I) \<phi>2; wf_interp_for_formula (w', I') \<phi>2\<rbrakk> \<Longrightarrow> ((w, I) \<Turnstile> \<phi>2) = ((w', I') \<Turnstile> \<phi>2); stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) (FAnd \<phi>1 \<phi>2); wf_interp_for_formula (w, I) (FAnd \<phi>1 \<phi>2); wf_interp_for_formula (w', I') (FAnd \<phi>1 \<phi>2)\<rbrakk> \<Longrightarrow> ((w, I) \<Turnstile> FAnd \<phi>1 \<phi>2) = ((w', I') \<Turnstile> FAnd \<phi>1 \<phi>2)
 7. \<And>\<phi> w w' I I'. \<lbrakk>\<And>w w' I I'. \<lbrakk>stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) \<phi>; wf_interp_for_formula (w, I) \<phi>; wf_interp_for_formula (w', I') \<phi>\<rbrakk> \<Longrightarrow> ((w, I) \<Turnstile> \<phi>) = ((w', I') \<Turnstile> \<phi>); stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) (FExists \<phi>); wf_interp_for_formula (w, I) (FExists \<phi>); wf_interp_for_formula (w', I') (FExists \<phi>)\<rbrakk> \<Longrightarrow> ((w, I) \<Turnstile> FExists \<phi>) = ((w', I') \<Turnstile> FExists \<phi>)
 8. \<And>\<phi> w w' I I'. \<lbrakk>\<And>w w' I I'. \<lbrakk>stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) \<phi>; wf_interp_for_formula (w, I) \<phi>; wf_interp_for_formula (w', I') \<phi>\<rbrakk> \<Longrightarrow> ((w, I) \<Turnstile> \<phi>) = ((w', I') \<Turnstile> \<phi>); stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) (FEXISTS \<phi>); wf_interp_for_formula (w, I) (FEXISTS \<phi>); wf_interp_for_formula (w', I') (FEXISTS \<phi>)\<rbrakk> \<Longrightarrow> ((w, I) \<Turnstile> FEXISTS \<phi>) = ((w', I') \<Turnstile> FEXISTS \<phi>)
[PROOF STEP]
case (FQ a m)
[PROOF STATE]
proof (state)
this:
stream_enc (w, I) = stream_enc (w', I')
wf_formula (length I) (FQ a m)
wf_interp_for_formula (w, I) (FQ a m)
wf_interp_for_formula (w', I') (FQ a m)

goal (8 subgoals):
 1. \<And>x1 x2 w w' I I'. \<lbrakk>stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) (FQ x1 x2); wf_interp_for_formula (w, I) (FQ x1 x2); wf_interp_for_formula (w', I') (FQ x1 x2)\<rbrakk> \<Longrightarrow> ((w, I) \<Turnstile> FQ x1 x2) = ((w', I') \<Turnstile> FQ x1 x2)
 2. \<And>x1 x2 w w' I I'. \<lbrakk>stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) (FLess x1 x2); wf_interp_for_formula (w, I) (FLess x1 x2); wf_interp_for_formula (w', I') (FLess x1 x2)\<rbrakk> \<Longrightarrow> ((w, I) \<Turnstile> FLess x1 x2) = ((w', I') \<Turnstile> FLess x1 x2)
 3. \<And>x1 x2 w w' I I'. \<lbrakk>stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) (FIn x1 x2); wf_interp_for_formula (w, I) (FIn x1 x2); wf_interp_for_formula (w', I') (FIn x1 x2)\<rbrakk> \<Longrightarrow> ((w, I) \<Turnstile> FIn x1 x2) = ((w', I') \<Turnstile> FIn x1 x2)
 4. \<And>\<phi> w w' I I'. \<lbrakk>\<And>w w' I I'. \<lbrakk>stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) \<phi>; wf_interp_for_formula (w, I) \<phi>; wf_interp_for_formula (w', I') \<phi>\<rbrakk> \<Longrightarrow> ((w, I) \<Turnstile> \<phi>) = ((w', I') \<Turnstile> \<phi>); stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) (FNot \<phi>); wf_interp_for_formula (w, I) (FNot \<phi>); wf_interp_for_formula (w', I') (FNot \<phi>)\<rbrakk> \<Longrightarrow> ((w, I) \<Turnstile> FNot \<phi>) = ((w', I') \<Turnstile> FNot \<phi>)
 5. \<And>\<phi>1 \<phi>2 w w' I I'. \<lbrakk>\<And>w w' I I'. \<lbrakk>stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) \<phi>1; wf_interp_for_formula (w, I) \<phi>1; wf_interp_for_formula (w', I') \<phi>1\<rbrakk> \<Longrightarrow> ((w, I) \<Turnstile> \<phi>1) = ((w', I') \<Turnstile> \<phi>1); \<And>w w' I I'. \<lbrakk>stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) \<phi>2; wf_interp_for_formula (w, I) \<phi>2; wf_interp_for_formula (w', I') \<phi>2\<rbrakk> \<Longrightarrow> ((w, I) \<Turnstile> \<phi>2) = ((w', I') \<Turnstile> \<phi>2); stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) (FOr \<phi>1 \<phi>2); wf_interp_for_formula (w, I) (FOr \<phi>1 \<phi>2); wf_interp_for_formula (w', I') (FOr \<phi>1 \<phi>2)\<rbrakk> \<Longrightarrow> ((w, I) \<Turnstile> FOr \<phi>1 \<phi>2) = ((w', I') \<Turnstile> FOr \<phi>1 \<phi>2)
 6. \<And>\<phi>1 \<phi>2 w w' I I'. \<lbrakk>\<And>w w' I I'. \<lbrakk>stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) \<phi>1; wf_interp_for_formula (w, I) \<phi>1; wf_interp_for_formula (w', I') \<phi>1\<rbrakk> \<Longrightarrow> ((w, I) \<Turnstile> \<phi>1) = ((w', I') \<Turnstile> \<phi>1); \<And>w w' I I'. \<lbrakk>stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) \<phi>2; wf_interp_for_formula (w, I) \<phi>2; wf_interp_for_formula (w', I') \<phi>2\<rbrakk> \<Longrightarrow> ((w, I) \<Turnstile> \<phi>2) = ((w', I') \<Turnstile> \<phi>2); stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) (FAnd \<phi>1 \<phi>2); wf_interp_for_formula (w, I) (FAnd \<phi>1 \<phi>2); wf_interp_for_formula (w', I') (FAnd \<phi>1 \<phi>2)\<rbrakk> \<Longrightarrow> ((w, I) \<Turnstile> FAnd \<phi>1 \<phi>2) = ((w', I') \<Turnstile> FAnd \<phi>1 \<phi>2)
 7. \<And>\<phi> w w' I I'. \<lbrakk>\<And>w w' I I'. \<lbrakk>stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) \<phi>; wf_interp_for_formula (w, I) \<phi>; wf_interp_for_formula (w', I') \<phi>\<rbrakk> \<Longrightarrow> ((w, I) \<Turnstile> \<phi>) = ((w', I') \<Turnstile> \<phi>); stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) (FExists \<phi>); wf_interp_for_formula (w, I) (FExists \<phi>); wf_interp_for_formula (w', I') (FExists \<phi>)\<rbrakk> \<Longrightarrow> ((w, I) \<Turnstile> FExists \<phi>) = ((w', I') \<Turnstile> FExists \<phi>)
 8. \<And>\<phi> w w' I I'. \<lbrakk>\<And>w w' I I'. \<lbrakk>stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) \<phi>; wf_interp_for_formula (w, I) \<phi>; wf_interp_for_formula (w', I') \<phi>\<rbrakk> \<Longrightarrow> ((w, I) \<Turnstile> \<phi>) = ((w', I') \<Turnstile> \<phi>); stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) (FEXISTS \<phi>); wf_interp_for_formula (w, I) (FEXISTS \<phi>); wf_interp_for_formula (w', I') (FEXISTS \<phi>)\<rbrakk> \<Longrightarrow> ((w, I) \<Turnstile> FEXISTS \<phi>) = ((w', I') \<Turnstile> FEXISTS \<phi>)
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
stream_enc (w, I) = stream_enc (w', I')
wf_formula (length I) (FQ a m)
wf_interp_for_formula (w, I) (FQ a m)
wf_interp_for_formula (w', I') (FQ a m)

goal (1 subgoal):
 1. ((w, I) \<Turnstile> FQ a m) = ((w', I') \<Turnstile> FQ a m)
[PROOF STEP]
using enc_atom_welldef[of I I' m]
[PROOF STATE]
proof (prove)
using this:
stream_enc (w, I) = stream_enc (w', I')
wf_formula (length I) (FQ a m)
wf_interp_for_formula (w, I) (FQ a m)
wf_interp_for_formula (w', I') (FQ a m)
\<lbrakk>\<forall>x a. enc_atom I x a = enc_atom I' x a; m < length I\<rbrakk> \<Longrightarrow> case (I ! m, I' ! m) of (Inl p, Inl q) \<Rightarrow> p = q | (Inl p, Inr ba) \<Rightarrow> True | (Inr P, Inl a) \<Rightarrow> True | (Inr P, Inr Q) \<Rightarrow> P = Q

goal (1 subgoal):
 1. ((w, I) \<Turnstile> FQ a m) = ((w', I') \<Turnstile> FQ a m)
[PROOF STEP]
by (simp split: sum.splits add: smap2_alt shift_snth)
      (metis snth_siterate[of id, simplified id_funpow id_apply])
[PROOF STATE]
proof (state)
this:
((w, I) \<Turnstile> FQ a m) = ((w', I') \<Turnstile> FQ a m)

goal (7 subgoals):
 1. \<And>x1 x2 w w' I I'. \<lbrakk>stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) (FLess x1 x2); wf_interp_for_formula (w, I) (FLess x1 x2); wf_interp_for_formula (w', I') (FLess x1 x2)\<rbrakk> \<Longrightarrow> ((w, I) \<Turnstile> FLess x1 x2) = ((w', I') \<Turnstile> FLess x1 x2)
 2. \<And>x1 x2 w w' I I'. \<lbrakk>stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) (FIn x1 x2); wf_interp_for_formula (w, I) (FIn x1 x2); wf_interp_for_formula (w', I') (FIn x1 x2)\<rbrakk> \<Longrightarrow> ((w, I) \<Turnstile> FIn x1 x2) = ((w', I') \<Turnstile> FIn x1 x2)
 3. \<And>\<phi> w w' I I'. \<lbrakk>\<And>w w' I I'. \<lbrakk>stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) \<phi>; wf_interp_for_formula (w, I) \<phi>; wf_interp_for_formula (w', I') \<phi>\<rbrakk> \<Longrightarrow> ((w, I) \<Turnstile> \<phi>) = ((w', I') \<Turnstile> \<phi>); stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) (FNot \<phi>); wf_interp_for_formula (w, I) (FNot \<phi>); wf_interp_for_formula (w', I') (FNot \<phi>)\<rbrakk> \<Longrightarrow> ((w, I) \<Turnstile> FNot \<phi>) = ((w', I') \<Turnstile> FNot \<phi>)
 4. \<And>\<phi>1 \<phi>2 w w' I I'. \<lbrakk>\<And>w w' I I'. \<lbrakk>stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) \<phi>1; wf_interp_for_formula (w, I) \<phi>1; wf_interp_for_formula (w', I') \<phi>1\<rbrakk> \<Longrightarrow> ((w, I) \<Turnstile> \<phi>1) = ((w', I') \<Turnstile> \<phi>1); \<And>w w' I I'. \<lbrakk>stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) \<phi>2; wf_interp_for_formula (w, I) \<phi>2; wf_interp_for_formula (w', I') \<phi>2\<rbrakk> \<Longrightarrow> ((w, I) \<Turnstile> \<phi>2) = ((w', I') \<Turnstile> \<phi>2); stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) (FOr \<phi>1 \<phi>2); wf_interp_for_formula (w, I) (FOr \<phi>1 \<phi>2); wf_interp_for_formula (w', I') (FOr \<phi>1 \<phi>2)\<rbrakk> \<Longrightarrow> ((w, I) \<Turnstile> FOr \<phi>1 \<phi>2) = ((w', I') \<Turnstile> FOr \<phi>1 \<phi>2)
 5. \<And>\<phi>1 \<phi>2 w w' I I'. \<lbrakk>\<And>w w' I I'. \<lbrakk>stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) \<phi>1; wf_interp_for_formula (w, I) \<phi>1; wf_interp_for_formula (w', I') \<phi>1\<rbrakk> \<Longrightarrow> ((w, I) \<Turnstile> \<phi>1) = ((w', I') \<Turnstile> \<phi>1); \<And>w w' I I'. \<lbrakk>stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) \<phi>2; wf_interp_for_formula (w, I) \<phi>2; wf_interp_for_formula (w', I') \<phi>2\<rbrakk> \<Longrightarrow> ((w, I) \<Turnstile> \<phi>2) = ((w', I') \<Turnstile> \<phi>2); stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) (FAnd \<phi>1 \<phi>2); wf_interp_for_formula (w, I) (FAnd \<phi>1 \<phi>2); wf_interp_for_formula (w', I') (FAnd \<phi>1 \<phi>2)\<rbrakk> \<Longrightarrow> ((w, I) \<Turnstile> FAnd \<phi>1 \<phi>2) = ((w', I') \<Turnstile> FAnd \<phi>1 \<phi>2)
 6. \<And>\<phi> w w' I I'. \<lbrakk>\<And>w w' I I'. \<lbrakk>stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) \<phi>; wf_interp_for_formula (w, I) \<phi>; wf_interp_for_formula (w', I') \<phi>\<rbrakk> \<Longrightarrow> ((w, I) \<Turnstile> \<phi>) = ((w', I') \<Turnstile> \<phi>); stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) (FExists \<phi>); wf_interp_for_formula (w, I) (FExists \<phi>); wf_interp_for_formula (w', I') (FExists \<phi>)\<rbrakk> \<Longrightarrow> ((w, I) \<Turnstile> FExists \<phi>) = ((w', I') \<Turnstile> FExists \<phi>)
 7. \<And>\<phi> w w' I I'. \<lbrakk>\<And>w w' I I'. \<lbrakk>stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) \<phi>; wf_interp_for_formula (w, I) \<phi>; wf_interp_for_formula (w', I') \<phi>\<rbrakk> \<Longrightarrow> ((w, I) \<Turnstile> \<phi>) = ((w', I') \<Turnstile> \<phi>); stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) (FEXISTS \<phi>); wf_interp_for_formula (w, I) (FEXISTS \<phi>); wf_interp_for_formula (w', I') (FEXISTS \<phi>)\<rbrakk> \<Longrightarrow> ((w, I) \<Turnstile> FEXISTS \<phi>) = ((w', I') \<Turnstile> FEXISTS \<phi>)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (7 subgoals):
 1. \<And>x1 x2 w w' I I'. \<lbrakk>stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) (FLess x1 x2); wf_interp_for_formula (w, I) (FLess x1 x2); wf_interp_for_formula (w', I') (FLess x1 x2)\<rbrakk> \<Longrightarrow> ((w, I) \<Turnstile> FLess x1 x2) = ((w', I') \<Turnstile> FLess x1 x2)
 2. \<And>x1 x2 w w' I I'. \<lbrakk>stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) (FIn x1 x2); wf_interp_for_formula (w, I) (FIn x1 x2); wf_interp_for_formula (w', I') (FIn x1 x2)\<rbrakk> \<Longrightarrow> ((w, I) \<Turnstile> FIn x1 x2) = ((w', I') \<Turnstile> FIn x1 x2)
 3. \<And>\<phi> w w' I I'. \<lbrakk>\<And>w w' I I'. \<lbrakk>stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) \<phi>; wf_interp_for_formula (w, I) \<phi>; wf_interp_for_formula (w', I') \<phi>\<rbrakk> \<Longrightarrow> ((w, I) \<Turnstile> \<phi>) = ((w', I') \<Turnstile> \<phi>); stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) (FNot \<phi>); wf_interp_for_formula (w, I) (FNot \<phi>); wf_interp_for_formula (w', I') (FNot \<phi>)\<rbrakk> \<Longrightarrow> ((w, I) \<Turnstile> FNot \<phi>) = ((w', I') \<Turnstile> FNot \<phi>)
 4. \<And>\<phi>1 \<phi>2 w w' I I'. \<lbrakk>\<And>w w' I I'. \<lbrakk>stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) \<phi>1; wf_interp_for_formula (w, I) \<phi>1; wf_interp_for_formula (w', I') \<phi>1\<rbrakk> \<Longrightarrow> ((w, I) \<Turnstile> \<phi>1) = ((w', I') \<Turnstile> \<phi>1); \<And>w w' I I'. \<lbrakk>stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) \<phi>2; wf_interp_for_formula (w, I) \<phi>2; wf_interp_for_formula (w', I') \<phi>2\<rbrakk> \<Longrightarrow> ((w, I) \<Turnstile> \<phi>2) = ((w', I') \<Turnstile> \<phi>2); stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) (FOr \<phi>1 \<phi>2); wf_interp_for_formula (w, I) (FOr \<phi>1 \<phi>2); wf_interp_for_formula (w', I') (FOr \<phi>1 \<phi>2)\<rbrakk> \<Longrightarrow> ((w, I) \<Turnstile> FOr \<phi>1 \<phi>2) = ((w', I') \<Turnstile> FOr \<phi>1 \<phi>2)
 5. \<And>\<phi>1 \<phi>2 w w' I I'. \<lbrakk>\<And>w w' I I'. \<lbrakk>stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) \<phi>1; wf_interp_for_formula (w, I) \<phi>1; wf_interp_for_formula (w', I') \<phi>1\<rbrakk> \<Longrightarrow> ((w, I) \<Turnstile> \<phi>1) = ((w', I') \<Turnstile> \<phi>1); \<And>w w' I I'. \<lbrakk>stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) \<phi>2; wf_interp_for_formula (w, I) \<phi>2; wf_interp_for_formula (w', I') \<phi>2\<rbrakk> \<Longrightarrow> ((w, I) \<Turnstile> \<phi>2) = ((w', I') \<Turnstile> \<phi>2); stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) (FAnd \<phi>1 \<phi>2); wf_interp_for_formula (w, I) (FAnd \<phi>1 \<phi>2); wf_interp_for_formula (w', I') (FAnd \<phi>1 \<phi>2)\<rbrakk> \<Longrightarrow> ((w, I) \<Turnstile> FAnd \<phi>1 \<phi>2) = ((w', I') \<Turnstile> FAnd \<phi>1 \<phi>2)
 6. \<And>\<phi> w w' I I'. \<lbrakk>\<And>w w' I I'. \<lbrakk>stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) \<phi>; wf_interp_for_formula (w, I) \<phi>; wf_interp_for_formula (w', I') \<phi>\<rbrakk> \<Longrightarrow> ((w, I) \<Turnstile> \<phi>) = ((w', I') \<Turnstile> \<phi>); stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) (FExists \<phi>); wf_interp_for_formula (w, I) (FExists \<phi>); wf_interp_for_formula (w', I') (FExists \<phi>)\<rbrakk> \<Longrightarrow> ((w, I) \<Turnstile> FExists \<phi>) = ((w', I') \<Turnstile> FExists \<phi>)
 7. \<And>\<phi> w w' I I'. \<lbrakk>\<And>w w' I I'. \<lbrakk>stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) \<phi>; wf_interp_for_formula (w, I) \<phi>; wf_interp_for_formula (w', I') \<phi>\<rbrakk> \<Longrightarrow> ((w, I) \<Turnstile> \<phi>) = ((w', I') \<Turnstile> \<phi>); stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) (FEXISTS \<phi>); wf_interp_for_formula (w, I) (FEXISTS \<phi>); wf_interp_for_formula (w', I') (FEXISTS \<phi>)\<rbrakk> \<Longrightarrow> ((w, I) \<Turnstile> FEXISTS \<phi>) = ((w', I') \<Turnstile> FEXISTS \<phi>)
[PROOF STEP]
case (FLess m1 m2)
[PROOF STATE]
proof (state)
this:
stream_enc (w, I) = stream_enc (w', I')
wf_formula (length I) (FLess m1 m2)
wf_interp_for_formula (w, I) (FLess m1 m2)
wf_interp_for_formula (w', I') (FLess m1 m2)

goal (7 subgoals):
 1. \<And>x1 x2 w w' I I'. \<lbrakk>stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) (FLess x1 x2); wf_interp_for_formula (w, I) (FLess x1 x2); wf_interp_for_formula (w', I') (FLess x1 x2)\<rbrakk> \<Longrightarrow> ((w, I) \<Turnstile> FLess x1 x2) = ((w', I') \<Turnstile> FLess x1 x2)
 2. \<And>x1 x2 w w' I I'. \<lbrakk>stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) (FIn x1 x2); wf_interp_for_formula (w, I) (FIn x1 x2); wf_interp_for_formula (w', I') (FIn x1 x2)\<rbrakk> \<Longrightarrow> ((w, I) \<Turnstile> FIn x1 x2) = ((w', I') \<Turnstile> FIn x1 x2)
 3. \<And>\<phi> w w' I I'. \<lbrakk>\<And>w w' I I'. \<lbrakk>stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) \<phi>; wf_interp_for_formula (w, I) \<phi>; wf_interp_for_formula (w', I') \<phi>\<rbrakk> \<Longrightarrow> ((w, I) \<Turnstile> \<phi>) = ((w', I') \<Turnstile> \<phi>); stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) (FNot \<phi>); wf_interp_for_formula (w, I) (FNot \<phi>); wf_interp_for_formula (w', I') (FNot \<phi>)\<rbrakk> \<Longrightarrow> ((w, I) \<Turnstile> FNot \<phi>) = ((w', I') \<Turnstile> FNot \<phi>)
 4. \<And>\<phi>1 \<phi>2 w w' I I'. \<lbrakk>\<And>w w' I I'. \<lbrakk>stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) \<phi>1; wf_interp_for_formula (w, I) \<phi>1; wf_interp_for_formula (w', I') \<phi>1\<rbrakk> \<Longrightarrow> ((w, I) \<Turnstile> \<phi>1) = ((w', I') \<Turnstile> \<phi>1); \<And>w w' I I'. \<lbrakk>stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) \<phi>2; wf_interp_for_formula (w, I) \<phi>2; wf_interp_for_formula (w', I') \<phi>2\<rbrakk> \<Longrightarrow> ((w, I) \<Turnstile> \<phi>2) = ((w', I') \<Turnstile> \<phi>2); stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) (FOr \<phi>1 \<phi>2); wf_interp_for_formula (w, I) (FOr \<phi>1 \<phi>2); wf_interp_for_formula (w', I') (FOr \<phi>1 \<phi>2)\<rbrakk> \<Longrightarrow> ((w, I) \<Turnstile> FOr \<phi>1 \<phi>2) = ((w', I') \<Turnstile> FOr \<phi>1 \<phi>2)
 5. \<And>\<phi>1 \<phi>2 w w' I I'. \<lbrakk>\<And>w w' I I'. \<lbrakk>stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) \<phi>1; wf_interp_for_formula (w, I) \<phi>1; wf_interp_for_formula (w', I') \<phi>1\<rbrakk> \<Longrightarrow> ((w, I) \<Turnstile> \<phi>1) = ((w', I') \<Turnstile> \<phi>1); \<And>w w' I I'. \<lbrakk>stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) \<phi>2; wf_interp_for_formula (w, I) \<phi>2; wf_interp_for_formula (w', I') \<phi>2\<rbrakk> \<Longrightarrow> ((w, I) \<Turnstile> \<phi>2) = ((w', I') \<Turnstile> \<phi>2); stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) (FAnd \<phi>1 \<phi>2); wf_interp_for_formula (w, I) (FAnd \<phi>1 \<phi>2); wf_interp_for_formula (w', I') (FAnd \<phi>1 \<phi>2)\<rbrakk> \<Longrightarrow> ((w, I) \<Turnstile> FAnd \<phi>1 \<phi>2) = ((w', I') \<Turnstile> FAnd \<phi>1 \<phi>2)
 6. \<And>\<phi> w w' I I'. \<lbrakk>\<And>w w' I I'. \<lbrakk>stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) \<phi>; wf_interp_for_formula (w, I) \<phi>; wf_interp_for_formula (w', I') \<phi>\<rbrakk> \<Longrightarrow> ((w, I) \<Turnstile> \<phi>) = ((w', I') \<Turnstile> \<phi>); stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) (FExists \<phi>); wf_interp_for_formula (w, I) (FExists \<phi>); wf_interp_for_formula (w', I') (FExists \<phi>)\<rbrakk> \<Longrightarrow> ((w, I) \<Turnstile> FExists \<phi>) = ((w', I') \<Turnstile> FExists \<phi>)
 7. \<And>\<phi> w w' I I'. \<lbrakk>\<And>w w' I I'. \<lbrakk>stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) \<phi>; wf_interp_for_formula (w, I) \<phi>; wf_interp_for_formula (w', I') \<phi>\<rbrakk> \<Longrightarrow> ((w, I) \<Turnstile> \<phi>) = ((w', I') \<Turnstile> \<phi>); stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) (FEXISTS \<phi>); wf_interp_for_formula (w, I) (FEXISTS \<phi>); wf_interp_for_formula (w', I') (FEXISTS \<phi>)\<rbrakk> \<Longrightarrow> ((w, I) \<Turnstile> FEXISTS \<phi>) = ((w', I') \<Turnstile> FEXISTS \<phi>)
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
stream_enc (w, I) = stream_enc (w', I')
wf_formula (length I) (FLess m1 m2)
wf_interp_for_formula (w, I) (FLess m1 m2)
wf_interp_for_formula (w', I') (FLess m1 m2)

goal (1 subgoal):
 1. ((w, I) \<Turnstile> FLess m1 m2) = ((w', I') \<Turnstile> FLess m1 m2)
[PROOF STEP]
using enc_atom_welldef[of I I' m1] enc_atom_welldef[of I I' m2]
[PROOF STATE]
proof (prove)
using this:
stream_enc (w, I) = stream_enc (w', I')
wf_formula (length I) (FLess m1 m2)
wf_interp_for_formula (w, I) (FLess m1 m2)
wf_interp_for_formula (w', I') (FLess m1 m2)
\<lbrakk>\<forall>x a. enc_atom I x a = enc_atom I' x a; m1 < length I\<rbrakk> \<Longrightarrow> case (I ! m1, I' ! m1) of (Inl p, Inl q) \<Rightarrow> p = q | (Inl p, Inr ba) \<Rightarrow> True | (Inr P, Inl a) \<Rightarrow> True | (Inr P, Inr Q) \<Rightarrow> P = Q
\<lbrakk>\<forall>x a. enc_atom I x a = enc_atom I' x a; m2 < length I\<rbrakk> \<Longrightarrow> case (I ! m2, I' ! m2) of (Inl p, Inl q) \<Rightarrow> p = q | (Inl p, Inr ba) \<Rightarrow> True | (Inr P, Inl a) \<Rightarrow> True | (Inr P, Inr Q) \<Rightarrow> P = Q

goal (1 subgoal):
 1. ((w, I) \<Turnstile> FLess m1 m2) = ((w', I') \<Turnstile> FLess m1 m2)
[PROOF STEP]
by (auto split: sum.splits simp add: smap2_alt)
[PROOF STATE]
proof (state)
this:
((w, I) \<Turnstile> FLess m1 m2) = ((w', I') \<Turnstile> FLess m1 m2)

goal (6 subgoals):
 1. \<And>x1 x2 w w' I I'. \<lbrakk>stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) (FIn x1 x2); wf_interp_for_formula (w, I) (FIn x1 x2); wf_interp_for_formula (w', I') (FIn x1 x2)\<rbrakk> \<Longrightarrow> ((w, I) \<Turnstile> FIn x1 x2) = ((w', I') \<Turnstile> FIn x1 x2)
 2. \<And>\<phi> w w' I I'. \<lbrakk>\<And>w w' I I'. \<lbrakk>stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) \<phi>; wf_interp_for_formula (w, I) \<phi>; wf_interp_for_formula (w', I') \<phi>\<rbrakk> \<Longrightarrow> ((w, I) \<Turnstile> \<phi>) = ((w', I') \<Turnstile> \<phi>); stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) (FNot \<phi>); wf_interp_for_formula (w, I) (FNot \<phi>); wf_interp_for_formula (w', I') (FNot \<phi>)\<rbrakk> \<Longrightarrow> ((w, I) \<Turnstile> FNot \<phi>) = ((w', I') \<Turnstile> FNot \<phi>)
 3. \<And>\<phi>1 \<phi>2 w w' I I'. \<lbrakk>\<And>w w' I I'. \<lbrakk>stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) \<phi>1; wf_interp_for_formula (w, I) \<phi>1; wf_interp_for_formula (w', I') \<phi>1\<rbrakk> \<Longrightarrow> ((w, I) \<Turnstile> \<phi>1) = ((w', I') \<Turnstile> \<phi>1); \<And>w w' I I'. \<lbrakk>stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) \<phi>2; wf_interp_for_formula (w, I) \<phi>2; wf_interp_for_formula (w', I') \<phi>2\<rbrakk> \<Longrightarrow> ((w, I) \<Turnstile> \<phi>2) = ((w', I') \<Turnstile> \<phi>2); stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) (FOr \<phi>1 \<phi>2); wf_interp_for_formula (w, I) (FOr \<phi>1 \<phi>2); wf_interp_for_formula (w', I') (FOr \<phi>1 \<phi>2)\<rbrakk> \<Longrightarrow> ((w, I) \<Turnstile> FOr \<phi>1 \<phi>2) = ((w', I') \<Turnstile> FOr \<phi>1 \<phi>2)
 4. \<And>\<phi>1 \<phi>2 w w' I I'. \<lbrakk>\<And>w w' I I'. \<lbrakk>stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) \<phi>1; wf_interp_for_formula (w, I) \<phi>1; wf_interp_for_formula (w', I') \<phi>1\<rbrakk> \<Longrightarrow> ((w, I) \<Turnstile> \<phi>1) = ((w', I') \<Turnstile> \<phi>1); \<And>w w' I I'. \<lbrakk>stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) \<phi>2; wf_interp_for_formula (w, I) \<phi>2; wf_interp_for_formula (w', I') \<phi>2\<rbrakk> \<Longrightarrow> ((w, I) \<Turnstile> \<phi>2) = ((w', I') \<Turnstile> \<phi>2); stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) (FAnd \<phi>1 \<phi>2); wf_interp_for_formula (w, I) (FAnd \<phi>1 \<phi>2); wf_interp_for_formula (w', I') (FAnd \<phi>1 \<phi>2)\<rbrakk> \<Longrightarrow> ((w, I) \<Turnstile> FAnd \<phi>1 \<phi>2) = ((w', I') \<Turnstile> FAnd \<phi>1 \<phi>2)
 5. \<And>\<phi> w w' I I'. \<lbrakk>\<And>w w' I I'. \<lbrakk>stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) \<phi>; wf_interp_for_formula (w, I) \<phi>; wf_interp_for_formula (w', I') \<phi>\<rbrakk> \<Longrightarrow> ((w, I) \<Turnstile> \<phi>) = ((w', I') \<Turnstile> \<phi>); stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) (FExists \<phi>); wf_interp_for_formula (w, I) (FExists \<phi>); wf_interp_for_formula (w', I') (FExists \<phi>)\<rbrakk> \<Longrightarrow> ((w, I) \<Turnstile> FExists \<phi>) = ((w', I') \<Turnstile> FExists \<phi>)
 6. \<And>\<phi> w w' I I'. \<lbrakk>\<And>w w' I I'. \<lbrakk>stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) \<phi>; wf_interp_for_formula (w, I) \<phi>; wf_interp_for_formula (w', I') \<phi>\<rbrakk> \<Longrightarrow> ((w, I) \<Turnstile> \<phi>) = ((w', I') \<Turnstile> \<phi>); stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) (FEXISTS \<phi>); wf_interp_for_formula (w, I) (FEXISTS \<phi>); wf_interp_for_formula (w', I') (FEXISTS \<phi>)\<rbrakk> \<Longrightarrow> ((w, I) \<Turnstile> FEXISTS \<phi>) = ((w', I') \<Turnstile> FEXISTS \<phi>)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (6 subgoals):
 1. \<And>x1 x2 w w' I I'. \<lbrakk>stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) (FIn x1 x2); wf_interp_for_formula (w, I) (FIn x1 x2); wf_interp_for_formula (w', I') (FIn x1 x2)\<rbrakk> \<Longrightarrow> ((w, I) \<Turnstile> FIn x1 x2) = ((w', I') \<Turnstile> FIn x1 x2)
 2. \<And>\<phi> w w' I I'. \<lbrakk>\<And>w w' I I'. \<lbrakk>stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) \<phi>; wf_interp_for_formula (w, I) \<phi>; wf_interp_for_formula (w', I') \<phi>\<rbrakk> \<Longrightarrow> ((w, I) \<Turnstile> \<phi>) = ((w', I') \<Turnstile> \<phi>); stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) (FNot \<phi>); wf_interp_for_formula (w, I) (FNot \<phi>); wf_interp_for_formula (w', I') (FNot \<phi>)\<rbrakk> \<Longrightarrow> ((w, I) \<Turnstile> FNot \<phi>) = ((w', I') \<Turnstile> FNot \<phi>)
 3. \<And>\<phi>1 \<phi>2 w w' I I'. \<lbrakk>\<And>w w' I I'. \<lbrakk>stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) \<phi>1; wf_interp_for_formula (w, I) \<phi>1; wf_interp_for_formula (w', I') \<phi>1\<rbrakk> \<Longrightarrow> ((w, I) \<Turnstile> \<phi>1) = ((w', I') \<Turnstile> \<phi>1); \<And>w w' I I'. \<lbrakk>stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) \<phi>2; wf_interp_for_formula (w, I) \<phi>2; wf_interp_for_formula (w', I') \<phi>2\<rbrakk> \<Longrightarrow> ((w, I) \<Turnstile> \<phi>2) = ((w', I') \<Turnstile> \<phi>2); stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) (FOr \<phi>1 \<phi>2); wf_interp_for_formula (w, I) (FOr \<phi>1 \<phi>2); wf_interp_for_formula (w', I') (FOr \<phi>1 \<phi>2)\<rbrakk> \<Longrightarrow> ((w, I) \<Turnstile> FOr \<phi>1 \<phi>2) = ((w', I') \<Turnstile> FOr \<phi>1 \<phi>2)
 4. \<And>\<phi>1 \<phi>2 w w' I I'. \<lbrakk>\<And>w w' I I'. \<lbrakk>stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) \<phi>1; wf_interp_for_formula (w, I) \<phi>1; wf_interp_for_formula (w', I') \<phi>1\<rbrakk> \<Longrightarrow> ((w, I) \<Turnstile> \<phi>1) = ((w', I') \<Turnstile> \<phi>1); \<And>w w' I I'. \<lbrakk>stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) \<phi>2; wf_interp_for_formula (w, I) \<phi>2; wf_interp_for_formula (w', I') \<phi>2\<rbrakk> \<Longrightarrow> ((w, I) \<Turnstile> \<phi>2) = ((w', I') \<Turnstile> \<phi>2); stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) (FAnd \<phi>1 \<phi>2); wf_interp_for_formula (w, I) (FAnd \<phi>1 \<phi>2); wf_interp_for_formula (w', I') (FAnd \<phi>1 \<phi>2)\<rbrakk> \<Longrightarrow> ((w, I) \<Turnstile> FAnd \<phi>1 \<phi>2) = ((w', I') \<Turnstile> FAnd \<phi>1 \<phi>2)
 5. \<And>\<phi> w w' I I'. \<lbrakk>\<And>w w' I I'. \<lbrakk>stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) \<phi>; wf_interp_for_formula (w, I) \<phi>; wf_interp_for_formula (w', I') \<phi>\<rbrakk> \<Longrightarrow> ((w, I) \<Turnstile> \<phi>) = ((w', I') \<Turnstile> \<phi>); stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) (FExists \<phi>); wf_interp_for_formula (w, I) (FExists \<phi>); wf_interp_for_formula (w', I') (FExists \<phi>)\<rbrakk> \<Longrightarrow> ((w, I) \<Turnstile> FExists \<phi>) = ((w', I') \<Turnstile> FExists \<phi>)
 6. \<And>\<phi> w w' I I'. \<lbrakk>\<And>w w' I I'. \<lbrakk>stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) \<phi>; wf_interp_for_formula (w, I) \<phi>; wf_interp_for_formula (w', I') \<phi>\<rbrakk> \<Longrightarrow> ((w, I) \<Turnstile> \<phi>) = ((w', I') \<Turnstile> \<phi>); stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) (FEXISTS \<phi>); wf_interp_for_formula (w, I) (FEXISTS \<phi>); wf_interp_for_formula (w', I') (FEXISTS \<phi>)\<rbrakk> \<Longrightarrow> ((w, I) \<Turnstile> FEXISTS \<phi>) = ((w', I') \<Turnstile> FEXISTS \<phi>)
[PROOF STEP]
case (FIn m M)
[PROOF STATE]
proof (state)
this:
stream_enc (w, I) = stream_enc (w', I')
wf_formula (length I) (FIn m M)
wf_interp_for_formula (w, I) (FIn m M)
wf_interp_for_formula (w', I') (FIn m M)

goal (6 subgoals):
 1. \<And>x1 x2 w w' I I'. \<lbrakk>stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) (FIn x1 x2); wf_interp_for_formula (w, I) (FIn x1 x2); wf_interp_for_formula (w', I') (FIn x1 x2)\<rbrakk> \<Longrightarrow> ((w, I) \<Turnstile> FIn x1 x2) = ((w', I') \<Turnstile> FIn x1 x2)
 2. \<And>\<phi> w w' I I'. \<lbrakk>\<And>w w' I I'. \<lbrakk>stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) \<phi>; wf_interp_for_formula (w, I) \<phi>; wf_interp_for_formula (w', I') \<phi>\<rbrakk> \<Longrightarrow> ((w, I) \<Turnstile> \<phi>) = ((w', I') \<Turnstile> \<phi>); stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) (FNot \<phi>); wf_interp_for_formula (w, I) (FNot \<phi>); wf_interp_for_formula (w', I') (FNot \<phi>)\<rbrakk> \<Longrightarrow> ((w, I) \<Turnstile> FNot \<phi>) = ((w', I') \<Turnstile> FNot \<phi>)
 3. \<And>\<phi>1 \<phi>2 w w' I I'. \<lbrakk>\<And>w w' I I'. \<lbrakk>stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) \<phi>1; wf_interp_for_formula (w, I) \<phi>1; wf_interp_for_formula (w', I') \<phi>1\<rbrakk> \<Longrightarrow> ((w, I) \<Turnstile> \<phi>1) = ((w', I') \<Turnstile> \<phi>1); \<And>w w' I I'. \<lbrakk>stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) \<phi>2; wf_interp_for_formula (w, I) \<phi>2; wf_interp_for_formula (w', I') \<phi>2\<rbrakk> \<Longrightarrow> ((w, I) \<Turnstile> \<phi>2) = ((w', I') \<Turnstile> \<phi>2); stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) (FOr \<phi>1 \<phi>2); wf_interp_for_formula (w, I) (FOr \<phi>1 \<phi>2); wf_interp_for_formula (w', I') (FOr \<phi>1 \<phi>2)\<rbrakk> \<Longrightarrow> ((w, I) \<Turnstile> FOr \<phi>1 \<phi>2) = ((w', I') \<Turnstile> FOr \<phi>1 \<phi>2)
 4. \<And>\<phi>1 \<phi>2 w w' I I'. \<lbrakk>\<And>w w' I I'. \<lbrakk>stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) \<phi>1; wf_interp_for_formula (w, I) \<phi>1; wf_interp_for_formula (w', I') \<phi>1\<rbrakk> \<Longrightarrow> ((w, I) \<Turnstile> \<phi>1) = ((w', I') \<Turnstile> \<phi>1); \<And>w w' I I'. \<lbrakk>stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) \<phi>2; wf_interp_for_formula (w, I) \<phi>2; wf_interp_for_formula (w', I') \<phi>2\<rbrakk> \<Longrightarrow> ((w, I) \<Turnstile> \<phi>2) = ((w', I') \<Turnstile> \<phi>2); stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) (FAnd \<phi>1 \<phi>2); wf_interp_for_formula (w, I) (FAnd \<phi>1 \<phi>2); wf_interp_for_formula (w', I') (FAnd \<phi>1 \<phi>2)\<rbrakk> \<Longrightarrow> ((w, I) \<Turnstile> FAnd \<phi>1 \<phi>2) = ((w', I') \<Turnstile> FAnd \<phi>1 \<phi>2)
 5. \<And>\<phi> w w' I I'. \<lbrakk>\<And>w w' I I'. \<lbrakk>stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) \<phi>; wf_interp_for_formula (w, I) \<phi>; wf_interp_for_formula (w', I') \<phi>\<rbrakk> \<Longrightarrow> ((w, I) \<Turnstile> \<phi>) = ((w', I') \<Turnstile> \<phi>); stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) (FExists \<phi>); wf_interp_for_formula (w, I) (FExists \<phi>); wf_interp_for_formula (w', I') (FExists \<phi>)\<rbrakk> \<Longrightarrow> ((w, I) \<Turnstile> FExists \<phi>) = ((w', I') \<Turnstile> FExists \<phi>)
 6. \<And>\<phi> w w' I I'. \<lbrakk>\<And>w w' I I'. \<lbrakk>stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) \<phi>; wf_interp_for_formula (w, I) \<phi>; wf_interp_for_formula (w', I') \<phi>\<rbrakk> \<Longrightarrow> ((w, I) \<Turnstile> \<phi>) = ((w', I') \<Turnstile> \<phi>); stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) (FEXISTS \<phi>); wf_interp_for_formula (w, I) (FEXISTS \<phi>); wf_interp_for_formula (w', I') (FEXISTS \<phi>)\<rbrakk> \<Longrightarrow> ((w, I) \<Turnstile> FEXISTS \<phi>) = ((w', I') \<Turnstile> FEXISTS \<phi>)
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
stream_enc (w, I) = stream_enc (w', I')
wf_formula (length I) (FIn m M)
wf_interp_for_formula (w, I) (FIn m M)
wf_interp_for_formula (w', I') (FIn m M)

goal (1 subgoal):
 1. ((w, I) \<Turnstile> FIn m M) = ((w', I') \<Turnstile> FIn m M)
[PROOF STEP]
using enc_atom_welldef[of I I' m] enc_atom_welldef[of I I' M]
[PROOF STATE]
proof (prove)
using this:
stream_enc (w, I) = stream_enc (w', I')
wf_formula (length I) (FIn m M)
wf_interp_for_formula (w, I) (FIn m M)
wf_interp_for_formula (w', I') (FIn m M)
\<lbrakk>\<forall>x a. enc_atom I x a = enc_atom I' x a; m < length I\<rbrakk> \<Longrightarrow> case (I ! m, I' ! m) of (Inl p, Inl q) \<Rightarrow> p = q | (Inl p, Inr ba) \<Rightarrow> True | (Inr P, Inl a) \<Rightarrow> True | (Inr P, Inr Q) \<Rightarrow> P = Q
\<lbrakk>\<forall>x a. enc_atom I x a = enc_atom I' x a; M < length I\<rbrakk> \<Longrightarrow> case (I ! M, I' ! M) of (Inl p, Inl q) \<Rightarrow> p = q | (Inl p, Inr ba) \<Rightarrow> True | (Inr P, Inl a) \<Rightarrow> True | (Inr P, Inr Q) \<Rightarrow> P = Q

goal (1 subgoal):
 1. ((w, I) \<Turnstile> FIn m M) = ((w', I') \<Turnstile> FIn m M)
[PROOF STEP]
by (auto split: sum.splits simp add: smap2_alt)
[PROOF STATE]
proof (state)
this:
((w, I) \<Turnstile> FIn m M) = ((w', I') \<Turnstile> FIn m M)

goal (5 subgoals):
 1. \<And>\<phi> w w' I I'. \<lbrakk>\<And>w w' I I'. \<lbrakk>stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) \<phi>; wf_interp_for_formula (w, I) \<phi>; wf_interp_for_formula (w', I') \<phi>\<rbrakk> \<Longrightarrow> ((w, I) \<Turnstile> \<phi>) = ((w', I') \<Turnstile> \<phi>); stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) (FNot \<phi>); wf_interp_for_formula (w, I) (FNot \<phi>); wf_interp_for_formula (w', I') (FNot \<phi>)\<rbrakk> \<Longrightarrow> ((w, I) \<Turnstile> FNot \<phi>) = ((w', I') \<Turnstile> FNot \<phi>)
 2. \<And>\<phi>1 \<phi>2 w w' I I'. \<lbrakk>\<And>w w' I I'. \<lbrakk>stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) \<phi>1; wf_interp_for_formula (w, I) \<phi>1; wf_interp_for_formula (w', I') \<phi>1\<rbrakk> \<Longrightarrow> ((w, I) \<Turnstile> \<phi>1) = ((w', I') \<Turnstile> \<phi>1); \<And>w w' I I'. \<lbrakk>stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) \<phi>2; wf_interp_for_formula (w, I) \<phi>2; wf_interp_for_formula (w', I') \<phi>2\<rbrakk> \<Longrightarrow> ((w, I) \<Turnstile> \<phi>2) = ((w', I') \<Turnstile> \<phi>2); stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) (FOr \<phi>1 \<phi>2); wf_interp_for_formula (w, I) (FOr \<phi>1 \<phi>2); wf_interp_for_formula (w', I') (FOr \<phi>1 \<phi>2)\<rbrakk> \<Longrightarrow> ((w, I) \<Turnstile> FOr \<phi>1 \<phi>2) = ((w', I') \<Turnstile> FOr \<phi>1 \<phi>2)
 3. \<And>\<phi>1 \<phi>2 w w' I I'. \<lbrakk>\<And>w w' I I'. \<lbrakk>stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) \<phi>1; wf_interp_for_formula (w, I) \<phi>1; wf_interp_for_formula (w', I') \<phi>1\<rbrakk> \<Longrightarrow> ((w, I) \<Turnstile> \<phi>1) = ((w', I') \<Turnstile> \<phi>1); \<And>w w' I I'. \<lbrakk>stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) \<phi>2; wf_interp_for_formula (w, I) \<phi>2; wf_interp_for_formula (w', I') \<phi>2\<rbrakk> \<Longrightarrow> ((w, I) \<Turnstile> \<phi>2) = ((w', I') \<Turnstile> \<phi>2); stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) (FAnd \<phi>1 \<phi>2); wf_interp_for_formula (w, I) (FAnd \<phi>1 \<phi>2); wf_interp_for_formula (w', I') (FAnd \<phi>1 \<phi>2)\<rbrakk> \<Longrightarrow> ((w, I) \<Turnstile> FAnd \<phi>1 \<phi>2) = ((w', I') \<Turnstile> FAnd \<phi>1 \<phi>2)
 4. \<And>\<phi> w w' I I'. \<lbrakk>\<And>w w' I I'. \<lbrakk>stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) \<phi>; wf_interp_for_formula (w, I) \<phi>; wf_interp_for_formula (w', I') \<phi>\<rbrakk> \<Longrightarrow> ((w, I) \<Turnstile> \<phi>) = ((w', I') \<Turnstile> \<phi>); stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) (FExists \<phi>); wf_interp_for_formula (w, I) (FExists \<phi>); wf_interp_for_formula (w', I') (FExists \<phi>)\<rbrakk> \<Longrightarrow> ((w, I) \<Turnstile> FExists \<phi>) = ((w', I') \<Turnstile> FExists \<phi>)
 5. \<And>\<phi> w w' I I'. \<lbrakk>\<And>w w' I I'. \<lbrakk>stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) \<phi>; wf_interp_for_formula (w, I) \<phi>; wf_interp_for_formula (w', I') \<phi>\<rbrakk> \<Longrightarrow> ((w, I) \<Turnstile> \<phi>) = ((w', I') \<Turnstile> \<phi>); stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) (FEXISTS \<phi>); wf_interp_for_formula (w, I) (FEXISTS \<phi>); wf_interp_for_formula (w', I') (FEXISTS \<phi>)\<rbrakk> \<Longrightarrow> ((w, I) \<Turnstile> FEXISTS \<phi>) = ((w', I') \<Turnstile> FEXISTS \<phi>)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>\<phi> w w' I I'. \<lbrakk>\<And>w w' I I'. \<lbrakk>stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) \<phi>; wf_interp_for_formula (w, I) \<phi>; wf_interp_for_formula (w', I') \<phi>\<rbrakk> \<Longrightarrow> ((w, I) \<Turnstile> \<phi>) = ((w', I') \<Turnstile> \<phi>); stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) (FNot \<phi>); wf_interp_for_formula (w, I) (FNot \<phi>); wf_interp_for_formula (w', I') (FNot \<phi>)\<rbrakk> \<Longrightarrow> ((w, I) \<Turnstile> FNot \<phi>) = ((w', I') \<Turnstile> FNot \<phi>)
 2. \<And>\<phi>1 \<phi>2 w w' I I'. \<lbrakk>\<And>w w' I I'. \<lbrakk>stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) \<phi>1; wf_interp_for_formula (w, I) \<phi>1; wf_interp_for_formula (w', I') \<phi>1\<rbrakk> \<Longrightarrow> ((w, I) \<Turnstile> \<phi>1) = ((w', I') \<Turnstile> \<phi>1); \<And>w w' I I'. \<lbrakk>stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) \<phi>2; wf_interp_for_formula (w, I) \<phi>2; wf_interp_for_formula (w', I') \<phi>2\<rbrakk> \<Longrightarrow> ((w, I) \<Turnstile> \<phi>2) = ((w', I') \<Turnstile> \<phi>2); stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) (FOr \<phi>1 \<phi>2); wf_interp_for_formula (w, I) (FOr \<phi>1 \<phi>2); wf_interp_for_formula (w', I') (FOr \<phi>1 \<phi>2)\<rbrakk> \<Longrightarrow> ((w, I) \<Turnstile> FOr \<phi>1 \<phi>2) = ((w', I') \<Turnstile> FOr \<phi>1 \<phi>2)
 3. \<And>\<phi>1 \<phi>2 w w' I I'. \<lbrakk>\<And>w w' I I'. \<lbrakk>stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) \<phi>1; wf_interp_for_formula (w, I) \<phi>1; wf_interp_for_formula (w', I') \<phi>1\<rbrakk> \<Longrightarrow> ((w, I) \<Turnstile> \<phi>1) = ((w', I') \<Turnstile> \<phi>1); \<And>w w' I I'. \<lbrakk>stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) \<phi>2; wf_interp_for_formula (w, I) \<phi>2; wf_interp_for_formula (w', I') \<phi>2\<rbrakk> \<Longrightarrow> ((w, I) \<Turnstile> \<phi>2) = ((w', I') \<Turnstile> \<phi>2); stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) (FAnd \<phi>1 \<phi>2); wf_interp_for_formula (w, I) (FAnd \<phi>1 \<phi>2); wf_interp_for_formula (w', I') (FAnd \<phi>1 \<phi>2)\<rbrakk> \<Longrightarrow> ((w, I) \<Turnstile> FAnd \<phi>1 \<phi>2) = ((w', I') \<Turnstile> FAnd \<phi>1 \<phi>2)
 4. \<And>\<phi> w w' I I'. \<lbrakk>\<And>w w' I I'. \<lbrakk>stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) \<phi>; wf_interp_for_formula (w, I) \<phi>; wf_interp_for_formula (w', I') \<phi>\<rbrakk> \<Longrightarrow> ((w, I) \<Turnstile> \<phi>) = ((w', I') \<Turnstile> \<phi>); stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) (FExists \<phi>); wf_interp_for_formula (w, I) (FExists \<phi>); wf_interp_for_formula (w', I') (FExists \<phi>)\<rbrakk> \<Longrightarrow> ((w, I) \<Turnstile> FExists \<phi>) = ((w', I') \<Turnstile> FExists \<phi>)
 5. \<And>\<phi> w w' I I'. \<lbrakk>\<And>w w' I I'. \<lbrakk>stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) \<phi>; wf_interp_for_formula (w, I) \<phi>; wf_interp_for_formula (w', I') \<phi>\<rbrakk> \<Longrightarrow> ((w, I) \<Turnstile> \<phi>) = ((w', I') \<Turnstile> \<phi>); stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) (FEXISTS \<phi>); wf_interp_for_formula (w, I) (FEXISTS \<phi>); wf_interp_for_formula (w', I') (FEXISTS \<phi>)\<rbrakk> \<Longrightarrow> ((w, I) \<Turnstile> FEXISTS \<phi>) = ((w', I') \<Turnstile> FEXISTS \<phi>)
[PROOF STEP]
case (FOr \<phi>1 \<phi>2)
[PROOF STATE]
proof (state)
this:
\<lbrakk>stream_enc (?w2, ?I2) = stream_enc (?w'2, ?I'2); wf_formula (length ?I2) \<phi>1; wf_interp_for_formula (?w2, ?I2) \<phi>1; wf_interp_for_formula (?w'2, ?I'2) \<phi>1\<rbrakk> \<Longrightarrow> ((?w2, ?I2) \<Turnstile> \<phi>1) = ((?w'2, ?I'2) \<Turnstile> \<phi>1)
\<lbrakk>stream_enc (?w2, ?I2) = stream_enc (?w'2, ?I'2); wf_formula (length ?I2) \<phi>2; wf_interp_for_formula (?w2, ?I2) \<phi>2; wf_interp_for_formula (?w'2, ?I'2) \<phi>2\<rbrakk> \<Longrightarrow> ((?w2, ?I2) \<Turnstile> \<phi>2) = ((?w'2, ?I'2) \<Turnstile> \<phi>2)
stream_enc (w, I) = stream_enc (w', I')
wf_formula (length I) (FOr \<phi>1 \<phi>2)
wf_interp_for_formula (w, I) (FOr \<phi>1 \<phi>2)
wf_interp_for_formula (w', I') (FOr \<phi>1 \<phi>2)

goal (5 subgoals):
 1. \<And>\<phi> w w' I I'. \<lbrakk>\<And>w w' I I'. \<lbrakk>stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) \<phi>; wf_interp_for_formula (w, I) \<phi>; wf_interp_for_formula (w', I') \<phi>\<rbrakk> \<Longrightarrow> ((w, I) \<Turnstile> \<phi>) = ((w', I') \<Turnstile> \<phi>); stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) (FNot \<phi>); wf_interp_for_formula (w, I) (FNot \<phi>); wf_interp_for_formula (w', I') (FNot \<phi>)\<rbrakk> \<Longrightarrow> ((w, I) \<Turnstile> FNot \<phi>) = ((w', I') \<Turnstile> FNot \<phi>)
 2. \<And>\<phi>1 \<phi>2 w w' I I'. \<lbrakk>\<And>w w' I I'. \<lbrakk>stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) \<phi>1; wf_interp_for_formula (w, I) \<phi>1; wf_interp_for_formula (w', I') \<phi>1\<rbrakk> \<Longrightarrow> ((w, I) \<Turnstile> \<phi>1) = ((w', I') \<Turnstile> \<phi>1); \<And>w w' I I'. \<lbrakk>stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) \<phi>2; wf_interp_for_formula (w, I) \<phi>2; wf_interp_for_formula (w', I') \<phi>2\<rbrakk> \<Longrightarrow> ((w, I) \<Turnstile> \<phi>2) = ((w', I') \<Turnstile> \<phi>2); stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) (FOr \<phi>1 \<phi>2); wf_interp_for_formula (w, I) (FOr \<phi>1 \<phi>2); wf_interp_for_formula (w', I') (FOr \<phi>1 \<phi>2)\<rbrakk> \<Longrightarrow> ((w, I) \<Turnstile> FOr \<phi>1 \<phi>2) = ((w', I') \<Turnstile> FOr \<phi>1 \<phi>2)
 3. \<And>\<phi>1 \<phi>2 w w' I I'. \<lbrakk>\<And>w w' I I'. \<lbrakk>stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) \<phi>1; wf_interp_for_formula (w, I) \<phi>1; wf_interp_for_formula (w', I') \<phi>1\<rbrakk> \<Longrightarrow> ((w, I) \<Turnstile> \<phi>1) = ((w', I') \<Turnstile> \<phi>1); \<And>w w' I I'. \<lbrakk>stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) \<phi>2; wf_interp_for_formula (w, I) \<phi>2; wf_interp_for_formula (w', I') \<phi>2\<rbrakk> \<Longrightarrow> ((w, I) \<Turnstile> \<phi>2) = ((w', I') \<Turnstile> \<phi>2); stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) (FAnd \<phi>1 \<phi>2); wf_interp_for_formula (w, I) (FAnd \<phi>1 \<phi>2); wf_interp_for_formula (w', I') (FAnd \<phi>1 \<phi>2)\<rbrakk> \<Longrightarrow> ((w, I) \<Turnstile> FAnd \<phi>1 \<phi>2) = ((w', I') \<Turnstile> FAnd \<phi>1 \<phi>2)
 4. \<And>\<phi> w w' I I'. \<lbrakk>\<And>w w' I I'. \<lbrakk>stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) \<phi>; wf_interp_for_formula (w, I) \<phi>; wf_interp_for_formula (w', I') \<phi>\<rbrakk> \<Longrightarrow> ((w, I) \<Turnstile> \<phi>) = ((w', I') \<Turnstile> \<phi>); stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) (FExists \<phi>); wf_interp_for_formula (w, I) (FExists \<phi>); wf_interp_for_formula (w', I') (FExists \<phi>)\<rbrakk> \<Longrightarrow> ((w, I) \<Turnstile> FExists \<phi>) = ((w', I') \<Turnstile> FExists \<phi>)
 5. \<And>\<phi> w w' I I'. \<lbrakk>\<And>w w' I I'. \<lbrakk>stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) \<phi>; wf_interp_for_formula (w, I) \<phi>; wf_interp_for_formula (w', I') \<phi>\<rbrakk> \<Longrightarrow> ((w, I) \<Turnstile> \<phi>) = ((w', I') \<Turnstile> \<phi>); stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) (FEXISTS \<phi>); wf_interp_for_formula (w, I) (FEXISTS \<phi>); wf_interp_for_formula (w', I') (FEXISTS \<phi>)\<rbrakk> \<Longrightarrow> ((w, I) \<Turnstile> FEXISTS \<phi>) = ((w', I') \<Turnstile> FEXISTS \<phi>)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((w, I) \<Turnstile> FOr \<phi>1 \<phi>2) = ((w', I') \<Turnstile> FOr \<phi>1 \<phi>2)
[PROOF STEP]
unfolding satisfies.simps(5)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((w, I) \<Turnstile> \<phi>1 \<or> (w, I) \<Turnstile> \<phi>2) = ((w', I') \<Turnstile> \<phi>1 \<or> (w', I') \<Turnstile> \<phi>2)
[PROOF STEP]
proof (intro disj_cong)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ((w, I) \<Turnstile> \<phi>1) = ((w', I') \<Turnstile> \<phi>1)
 2. \<not> (w', I') \<Turnstile> \<phi>1 \<Longrightarrow> ((w, I) \<Turnstile> \<phi>2) = ((w', I') \<Turnstile> \<phi>2)
[PROOF STEP]
from FOr(3-6)
[PROOF STATE]
proof (chain)
picking this:
stream_enc (w, I) = stream_enc (w', I')
wf_formula (length I) (FOr \<phi>1 \<phi>2)
wf_interp_for_formula (w, I) (FOr \<phi>1 \<phi>2)
wf_interp_for_formula (w', I') (FOr \<phi>1 \<phi>2)
[PROOF STEP]
show "(w, I) \<Turnstile> \<phi>1 \<longleftrightarrow> (w', I') \<Turnstile> \<phi>1"
[PROOF STATE]
proof (prove)
using this:
stream_enc (w, I) = stream_enc (w', I')
wf_formula (length I) (FOr \<phi>1 \<phi>2)
wf_interp_for_formula (w, I) (FOr \<phi>1 \<phi>2)
wf_interp_for_formula (w', I') (FOr \<phi>1 \<phi>2)

goal (1 subgoal):
 1. ((w, I) \<Turnstile> \<phi>1) = ((w', I') \<Turnstile> \<phi>1)
[PROOF STEP]
by (intro FOr(1)) auto
[PROOF STATE]
proof (state)
this:
((w, I) \<Turnstile> \<phi>1) = ((w', I') \<Turnstile> \<phi>1)

goal (1 subgoal):
 1. \<not> (w', I') \<Turnstile> \<phi>1 \<Longrightarrow> ((w, I) \<Turnstile> \<phi>2) = ((w', I') \<Turnstile> \<phi>2)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> (w', I') \<Turnstile> \<phi>1 \<Longrightarrow> ((w, I) \<Turnstile> \<phi>2) = ((w', I') \<Turnstile> \<phi>2)
[PROOF STEP]
from FOr(3-6)
[PROOF STATE]
proof (chain)
picking this:
stream_enc (w, I) = stream_enc (w', I')
wf_formula (length I) (FOr \<phi>1 \<phi>2)
wf_interp_for_formula (w, I) (FOr \<phi>1 \<phi>2)
wf_interp_for_formula (w', I') (FOr \<phi>1 \<phi>2)
[PROOF STEP]
show "(w, I) \<Turnstile> \<phi>2 \<longleftrightarrow> (w', I') \<Turnstile> \<phi>2"
[PROOF STATE]
proof (prove)
using this:
stream_enc (w, I) = stream_enc (w', I')
wf_formula (length I) (FOr \<phi>1 \<phi>2)
wf_interp_for_formula (w, I) (FOr \<phi>1 \<phi>2)
wf_interp_for_formula (w', I') (FOr \<phi>1 \<phi>2)

goal (1 subgoal):
 1. ((w, I) \<Turnstile> \<phi>2) = ((w', I') \<Turnstile> \<phi>2)
[PROOF STEP]
by (intro FOr(2)) auto
[PROOF STATE]
proof (state)
this:
((w, I) \<Turnstile> \<phi>2) = ((w', I') \<Turnstile> \<phi>2)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
((w, I) \<Turnstile> FOr \<phi>1 \<phi>2) = ((w', I') \<Turnstile> FOr \<phi>1 \<phi>2)

goal (4 subgoals):
 1. \<And>\<phi> w w' I I'. \<lbrakk>\<And>w w' I I'. \<lbrakk>stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) \<phi>; wf_interp_for_formula (w, I) \<phi>; wf_interp_for_formula (w', I') \<phi>\<rbrakk> \<Longrightarrow> ((w, I) \<Turnstile> \<phi>) = ((w', I') \<Turnstile> \<phi>); stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) (FNot \<phi>); wf_interp_for_formula (w, I) (FNot \<phi>); wf_interp_for_formula (w', I') (FNot \<phi>)\<rbrakk> \<Longrightarrow> ((w, I) \<Turnstile> FNot \<phi>) = ((w', I') \<Turnstile> FNot \<phi>)
 2. \<And>\<phi>1 \<phi>2 w w' I I'. \<lbrakk>\<And>w w' I I'. \<lbrakk>stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) \<phi>1; wf_interp_for_formula (w, I) \<phi>1; wf_interp_for_formula (w', I') \<phi>1\<rbrakk> \<Longrightarrow> ((w, I) \<Turnstile> \<phi>1) = ((w', I') \<Turnstile> \<phi>1); \<And>w w' I I'. \<lbrakk>stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) \<phi>2; wf_interp_for_formula (w, I) \<phi>2; wf_interp_for_formula (w', I') \<phi>2\<rbrakk> \<Longrightarrow> ((w, I) \<Turnstile> \<phi>2) = ((w', I') \<Turnstile> \<phi>2); stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) (FAnd \<phi>1 \<phi>2); wf_interp_for_formula (w, I) (FAnd \<phi>1 \<phi>2); wf_interp_for_formula (w', I') (FAnd \<phi>1 \<phi>2)\<rbrakk> \<Longrightarrow> ((w, I) \<Turnstile> FAnd \<phi>1 \<phi>2) = ((w', I') \<Turnstile> FAnd \<phi>1 \<phi>2)
 3. \<And>\<phi> w w' I I'. \<lbrakk>\<And>w w' I I'. \<lbrakk>stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) \<phi>; wf_interp_for_formula (w, I) \<phi>; wf_interp_for_formula (w', I') \<phi>\<rbrakk> \<Longrightarrow> ((w, I) \<Turnstile> \<phi>) = ((w', I') \<Turnstile> \<phi>); stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) (FExists \<phi>); wf_interp_for_formula (w, I) (FExists \<phi>); wf_interp_for_formula (w', I') (FExists \<phi>)\<rbrakk> \<Longrightarrow> ((w, I) \<Turnstile> FExists \<phi>) = ((w', I') \<Turnstile> FExists \<phi>)
 4. \<And>\<phi> w w' I I'. \<lbrakk>\<And>w w' I I'. \<lbrakk>stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) \<phi>; wf_interp_for_formula (w, I) \<phi>; wf_interp_for_formula (w', I') \<phi>\<rbrakk> \<Longrightarrow> ((w, I) \<Turnstile> \<phi>) = ((w', I') \<Turnstile> \<phi>); stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) (FEXISTS \<phi>); wf_interp_for_formula (w, I) (FEXISTS \<phi>); wf_interp_for_formula (w', I') (FEXISTS \<phi>)\<rbrakk> \<Longrightarrow> ((w, I) \<Turnstile> FEXISTS \<phi>) = ((w', I') \<Turnstile> FEXISTS \<phi>)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>\<phi> w w' I I'. \<lbrakk>\<And>w w' I I'. \<lbrakk>stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) \<phi>; wf_interp_for_formula (w, I) \<phi>; wf_interp_for_formula (w', I') \<phi>\<rbrakk> \<Longrightarrow> ((w, I) \<Turnstile> \<phi>) = ((w', I') \<Turnstile> \<phi>); stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) (FNot \<phi>); wf_interp_for_formula (w, I) (FNot \<phi>); wf_interp_for_formula (w', I') (FNot \<phi>)\<rbrakk> \<Longrightarrow> ((w, I) \<Turnstile> FNot \<phi>) = ((w', I') \<Turnstile> FNot \<phi>)
 2. \<And>\<phi>1 \<phi>2 w w' I I'. \<lbrakk>\<And>w w' I I'. \<lbrakk>stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) \<phi>1; wf_interp_for_formula (w, I) \<phi>1; wf_interp_for_formula (w', I') \<phi>1\<rbrakk> \<Longrightarrow> ((w, I) \<Turnstile> \<phi>1) = ((w', I') \<Turnstile> \<phi>1); \<And>w w' I I'. \<lbrakk>stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) \<phi>2; wf_interp_for_formula (w, I) \<phi>2; wf_interp_for_formula (w', I') \<phi>2\<rbrakk> \<Longrightarrow> ((w, I) \<Turnstile> \<phi>2) = ((w', I') \<Turnstile> \<phi>2); stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) (FAnd \<phi>1 \<phi>2); wf_interp_for_formula (w, I) (FAnd \<phi>1 \<phi>2); wf_interp_for_formula (w', I') (FAnd \<phi>1 \<phi>2)\<rbrakk> \<Longrightarrow> ((w, I) \<Turnstile> FAnd \<phi>1 \<phi>2) = ((w', I') \<Turnstile> FAnd \<phi>1 \<phi>2)
 3. \<And>\<phi> w w' I I'. \<lbrakk>\<And>w w' I I'. \<lbrakk>stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) \<phi>; wf_interp_for_formula (w, I) \<phi>; wf_interp_for_formula (w', I') \<phi>\<rbrakk> \<Longrightarrow> ((w, I) \<Turnstile> \<phi>) = ((w', I') \<Turnstile> \<phi>); stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) (FExists \<phi>); wf_interp_for_formula (w, I) (FExists \<phi>); wf_interp_for_formula (w', I') (FExists \<phi>)\<rbrakk> \<Longrightarrow> ((w, I) \<Turnstile> FExists \<phi>) = ((w', I') \<Turnstile> FExists \<phi>)
 4. \<And>\<phi> w w' I I'. \<lbrakk>\<And>w w' I I'. \<lbrakk>stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) \<phi>; wf_interp_for_formula (w, I) \<phi>; wf_interp_for_formula (w', I') \<phi>\<rbrakk> \<Longrightarrow> ((w, I) \<Turnstile> \<phi>) = ((w', I') \<Turnstile> \<phi>); stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) (FEXISTS \<phi>); wf_interp_for_formula (w, I) (FEXISTS \<phi>); wf_interp_for_formula (w', I') (FEXISTS \<phi>)\<rbrakk> \<Longrightarrow> ((w, I) \<Turnstile> FEXISTS \<phi>) = ((w', I') \<Turnstile> FEXISTS \<phi>)
[PROOF STEP]
case (FAnd \<phi>1 \<phi>2)
[PROOF STATE]
proof (state)
this:
\<lbrakk>stream_enc (?w2, ?I2) = stream_enc (?w'2, ?I'2); wf_formula (length ?I2) \<phi>1; wf_interp_for_formula (?w2, ?I2) \<phi>1; wf_interp_for_formula (?w'2, ?I'2) \<phi>1\<rbrakk> \<Longrightarrow> ((?w2, ?I2) \<Turnstile> \<phi>1) = ((?w'2, ?I'2) \<Turnstile> \<phi>1)
\<lbrakk>stream_enc (?w2, ?I2) = stream_enc (?w'2, ?I'2); wf_formula (length ?I2) \<phi>2; wf_interp_for_formula (?w2, ?I2) \<phi>2; wf_interp_for_formula (?w'2, ?I'2) \<phi>2\<rbrakk> \<Longrightarrow> ((?w2, ?I2) \<Turnstile> \<phi>2) = ((?w'2, ?I'2) \<Turnstile> \<phi>2)
stream_enc (w, I) = stream_enc (w', I')
wf_formula (length I) (FAnd \<phi>1 \<phi>2)
wf_interp_for_formula (w, I) (FAnd \<phi>1 \<phi>2)
wf_interp_for_formula (w', I') (FAnd \<phi>1 \<phi>2)

goal (4 subgoals):
 1. \<And>\<phi> w w' I I'. \<lbrakk>\<And>w w' I I'. \<lbrakk>stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) \<phi>; wf_interp_for_formula (w, I) \<phi>; wf_interp_for_formula (w', I') \<phi>\<rbrakk> \<Longrightarrow> ((w, I) \<Turnstile> \<phi>) = ((w', I') \<Turnstile> \<phi>); stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) (FNot \<phi>); wf_interp_for_formula (w, I) (FNot \<phi>); wf_interp_for_formula (w', I') (FNot \<phi>)\<rbrakk> \<Longrightarrow> ((w, I) \<Turnstile> FNot \<phi>) = ((w', I') \<Turnstile> FNot \<phi>)
 2. \<And>\<phi>1 \<phi>2 w w' I I'. \<lbrakk>\<And>w w' I I'. \<lbrakk>stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) \<phi>1; wf_interp_for_formula (w, I) \<phi>1; wf_interp_for_formula (w', I') \<phi>1\<rbrakk> \<Longrightarrow> ((w, I) \<Turnstile> \<phi>1) = ((w', I') \<Turnstile> \<phi>1); \<And>w w' I I'. \<lbrakk>stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) \<phi>2; wf_interp_for_formula (w, I) \<phi>2; wf_interp_for_formula (w', I') \<phi>2\<rbrakk> \<Longrightarrow> ((w, I) \<Turnstile> \<phi>2) = ((w', I') \<Turnstile> \<phi>2); stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) (FAnd \<phi>1 \<phi>2); wf_interp_for_formula (w, I) (FAnd \<phi>1 \<phi>2); wf_interp_for_formula (w', I') (FAnd \<phi>1 \<phi>2)\<rbrakk> \<Longrightarrow> ((w, I) \<Turnstile> FAnd \<phi>1 \<phi>2) = ((w', I') \<Turnstile> FAnd \<phi>1 \<phi>2)
 3. \<And>\<phi> w w' I I'. \<lbrakk>\<And>w w' I I'. \<lbrakk>stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) \<phi>; wf_interp_for_formula (w, I) \<phi>; wf_interp_for_formula (w', I') \<phi>\<rbrakk> \<Longrightarrow> ((w, I) \<Turnstile> \<phi>) = ((w', I') \<Turnstile> \<phi>); stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) (FExists \<phi>); wf_interp_for_formula (w, I) (FExists \<phi>); wf_interp_for_formula (w', I') (FExists \<phi>)\<rbrakk> \<Longrightarrow> ((w, I) \<Turnstile> FExists \<phi>) = ((w', I') \<Turnstile> FExists \<phi>)
 4. \<And>\<phi> w w' I I'. \<lbrakk>\<And>w w' I I'. \<lbrakk>stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) \<phi>; wf_interp_for_formula (w, I) \<phi>; wf_interp_for_formula (w', I') \<phi>\<rbrakk> \<Longrightarrow> ((w, I) \<Turnstile> \<phi>) = ((w', I') \<Turnstile> \<phi>); stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) (FEXISTS \<phi>); wf_interp_for_formula (w, I) (FEXISTS \<phi>); wf_interp_for_formula (w', I') (FEXISTS \<phi>)\<rbrakk> \<Longrightarrow> ((w, I) \<Turnstile> FEXISTS \<phi>) = ((w', I') \<Turnstile> FEXISTS \<phi>)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((w, I) \<Turnstile> FAnd \<phi>1 \<phi>2) = ((w', I') \<Turnstile> FAnd \<phi>1 \<phi>2)
[PROOF STEP]
unfolding satisfies.simps(6)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((w, I) \<Turnstile> \<phi>1 \<and> (w, I) \<Turnstile> \<phi>2) = ((w', I') \<Turnstile> \<phi>1 \<and> (w', I') \<Turnstile> \<phi>2)
[PROOF STEP]
proof (intro conj_cong)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ((w, I) \<Turnstile> \<phi>1) = ((w', I') \<Turnstile> \<phi>1)
 2. (w', I') \<Turnstile> \<phi>1 \<Longrightarrow> ((w, I) \<Turnstile> \<phi>2) = ((w', I') \<Turnstile> \<phi>2)
[PROOF STEP]
from FAnd(3-6)
[PROOF STATE]
proof (chain)
picking this:
stream_enc (w, I) = stream_enc (w', I')
wf_formula (length I) (FAnd \<phi>1 \<phi>2)
wf_interp_for_formula (w, I) (FAnd \<phi>1 \<phi>2)
wf_interp_for_formula (w', I') (FAnd \<phi>1 \<phi>2)
[PROOF STEP]
show "(w, I) \<Turnstile> \<phi>1 \<longleftrightarrow> (w', I') \<Turnstile> \<phi>1"
[PROOF STATE]
proof (prove)
using this:
stream_enc (w, I) = stream_enc (w', I')
wf_formula (length I) (FAnd \<phi>1 \<phi>2)
wf_interp_for_formula (w, I) (FAnd \<phi>1 \<phi>2)
wf_interp_for_formula (w', I') (FAnd \<phi>1 \<phi>2)

goal (1 subgoal):
 1. ((w, I) \<Turnstile> \<phi>1) = ((w', I') \<Turnstile> \<phi>1)
[PROOF STEP]
by (intro FAnd(1)) auto
[PROOF STATE]
proof (state)
this:
((w, I) \<Turnstile> \<phi>1) = ((w', I') \<Turnstile> \<phi>1)

goal (1 subgoal):
 1. (w', I') \<Turnstile> \<phi>1 \<Longrightarrow> ((w, I) \<Turnstile> \<phi>2) = ((w', I') \<Turnstile> \<phi>2)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (w', I') \<Turnstile> \<phi>1 \<Longrightarrow> ((w, I) \<Turnstile> \<phi>2) = ((w', I') \<Turnstile> \<phi>2)
[PROOF STEP]
from FAnd(3-6)
[PROOF STATE]
proof (chain)
picking this:
stream_enc (w, I) = stream_enc (w', I')
wf_formula (length I) (FAnd \<phi>1 \<phi>2)
wf_interp_for_formula (w, I) (FAnd \<phi>1 \<phi>2)
wf_interp_for_formula (w', I') (FAnd \<phi>1 \<phi>2)
[PROOF STEP]
show "(w, I) \<Turnstile> \<phi>2 \<longleftrightarrow> (w', I') \<Turnstile> \<phi>2"
[PROOF STATE]
proof (prove)
using this:
stream_enc (w, I) = stream_enc (w', I')
wf_formula (length I) (FAnd \<phi>1 \<phi>2)
wf_interp_for_formula (w, I) (FAnd \<phi>1 \<phi>2)
wf_interp_for_formula (w', I') (FAnd \<phi>1 \<phi>2)

goal (1 subgoal):
 1. ((w, I) \<Turnstile> \<phi>2) = ((w', I') \<Turnstile> \<phi>2)
[PROOF STEP]
by (intro FAnd(2)) auto
[PROOF STATE]
proof (state)
this:
((w, I) \<Turnstile> \<phi>2) = ((w', I') \<Turnstile> \<phi>2)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
((w, I) \<Turnstile> FAnd \<phi>1 \<phi>2) = ((w', I') \<Turnstile> FAnd \<phi>1 \<phi>2)

goal (3 subgoals):
 1. \<And>\<phi> w w' I I'. \<lbrakk>\<And>w w' I I'. \<lbrakk>stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) \<phi>; wf_interp_for_formula (w, I) \<phi>; wf_interp_for_formula (w', I') \<phi>\<rbrakk> \<Longrightarrow> ((w, I) \<Turnstile> \<phi>) = ((w', I') \<Turnstile> \<phi>); stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) (FNot \<phi>); wf_interp_for_formula (w, I) (FNot \<phi>); wf_interp_for_formula (w', I') (FNot \<phi>)\<rbrakk> \<Longrightarrow> ((w, I) \<Turnstile> FNot \<phi>) = ((w', I') \<Turnstile> FNot \<phi>)
 2. \<And>\<phi> w w' I I'. \<lbrakk>\<And>w w' I I'. \<lbrakk>stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) \<phi>; wf_interp_for_formula (w, I) \<phi>; wf_interp_for_formula (w', I') \<phi>\<rbrakk> \<Longrightarrow> ((w, I) \<Turnstile> \<phi>) = ((w', I') \<Turnstile> \<phi>); stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) (FExists \<phi>); wf_interp_for_formula (w, I) (FExists \<phi>); wf_interp_for_formula (w', I') (FExists \<phi>)\<rbrakk> \<Longrightarrow> ((w, I) \<Turnstile> FExists \<phi>) = ((w', I') \<Turnstile> FExists \<phi>)
 3. \<And>\<phi> w w' I I'. \<lbrakk>\<And>w w' I I'. \<lbrakk>stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) \<phi>; wf_interp_for_formula (w, I) \<phi>; wf_interp_for_formula (w', I') \<phi>\<rbrakk> \<Longrightarrow> ((w, I) \<Turnstile> \<phi>) = ((w', I') \<Turnstile> \<phi>); stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) (FEXISTS \<phi>); wf_interp_for_formula (w, I) (FEXISTS \<phi>); wf_interp_for_formula (w', I') (FEXISTS \<phi>)\<rbrakk> \<Longrightarrow> ((w, I) \<Turnstile> FEXISTS \<phi>) = ((w', I') \<Turnstile> FEXISTS \<phi>)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>\<phi> w w' I I'. \<lbrakk>\<And>w w' I I'. \<lbrakk>stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) \<phi>; wf_interp_for_formula (w, I) \<phi>; wf_interp_for_formula (w', I') \<phi>\<rbrakk> \<Longrightarrow> ((w, I) \<Turnstile> \<phi>) = ((w', I') \<Turnstile> \<phi>); stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) (FNot \<phi>); wf_interp_for_formula (w, I) (FNot \<phi>); wf_interp_for_formula (w', I') (FNot \<phi>)\<rbrakk> \<Longrightarrow> ((w, I) \<Turnstile> FNot \<phi>) = ((w', I') \<Turnstile> FNot \<phi>)
 2. \<And>\<phi> w w' I I'. \<lbrakk>\<And>w w' I I'. \<lbrakk>stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) \<phi>; wf_interp_for_formula (w, I) \<phi>; wf_interp_for_formula (w', I') \<phi>\<rbrakk> \<Longrightarrow> ((w, I) \<Turnstile> \<phi>) = ((w', I') \<Turnstile> \<phi>); stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) (FExists \<phi>); wf_interp_for_formula (w, I) (FExists \<phi>); wf_interp_for_formula (w', I') (FExists \<phi>)\<rbrakk> \<Longrightarrow> ((w, I) \<Turnstile> FExists \<phi>) = ((w', I') \<Turnstile> FExists \<phi>)
 3. \<And>\<phi> w w' I I'. \<lbrakk>\<And>w w' I I'. \<lbrakk>stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) \<phi>; wf_interp_for_formula (w, I) \<phi>; wf_interp_for_formula (w', I') \<phi>\<rbrakk> \<Longrightarrow> ((w, I) \<Turnstile> \<phi>) = ((w', I') \<Turnstile> \<phi>); stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) (FEXISTS \<phi>); wf_interp_for_formula (w, I) (FEXISTS \<phi>); wf_interp_for_formula (w', I') (FEXISTS \<phi>)\<rbrakk> \<Longrightarrow> ((w, I) \<Turnstile> FEXISTS \<phi>) = ((w', I') \<Turnstile> FEXISTS \<phi>)
[PROOF STEP]
case (FExists \<phi>)
[PROOF STATE]
proof (state)
this:
\<lbrakk>stream_enc (?w2, ?I2) = stream_enc (?w'2, ?I'2); wf_formula (length ?I2) \<phi>; wf_interp_for_formula (?w2, ?I2) \<phi>; wf_interp_for_formula (?w'2, ?I'2) \<phi>\<rbrakk> \<Longrightarrow> ((?w2, ?I2) \<Turnstile> \<phi>) = ((?w'2, ?I'2) \<Turnstile> \<phi>)
stream_enc (w, I) = stream_enc (w', I')
wf_formula (length I) (FExists \<phi>)
wf_interp_for_formula (w, I) (FExists \<phi>)
wf_interp_for_formula (w', I') (FExists \<phi>)

goal (3 subgoals):
 1. \<And>\<phi> w w' I I'. \<lbrakk>\<And>w w' I I'. \<lbrakk>stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) \<phi>; wf_interp_for_formula (w, I) \<phi>; wf_interp_for_formula (w', I') \<phi>\<rbrakk> \<Longrightarrow> ((w, I) \<Turnstile> \<phi>) = ((w', I') \<Turnstile> \<phi>); stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) (FNot \<phi>); wf_interp_for_formula (w, I) (FNot \<phi>); wf_interp_for_formula (w', I') (FNot \<phi>)\<rbrakk> \<Longrightarrow> ((w, I) \<Turnstile> FNot \<phi>) = ((w', I') \<Turnstile> FNot \<phi>)
 2. \<And>\<phi> w w' I I'. \<lbrakk>\<And>w w' I I'. \<lbrakk>stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) \<phi>; wf_interp_for_formula (w, I) \<phi>; wf_interp_for_formula (w', I') \<phi>\<rbrakk> \<Longrightarrow> ((w, I) \<Turnstile> \<phi>) = ((w', I') \<Turnstile> \<phi>); stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) (FExists \<phi>); wf_interp_for_formula (w, I) (FExists \<phi>); wf_interp_for_formula (w', I') (FExists \<phi>)\<rbrakk> \<Longrightarrow> ((w, I) \<Turnstile> FExists \<phi>) = ((w', I') \<Turnstile> FExists \<phi>)
 3. \<And>\<phi> w w' I I'. \<lbrakk>\<And>w w' I I'. \<lbrakk>stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) \<phi>; wf_interp_for_formula (w, I) \<phi>; wf_interp_for_formula (w', I') \<phi>\<rbrakk> \<Longrightarrow> ((w, I) \<Turnstile> \<phi>) = ((w', I') \<Turnstile> \<phi>); stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) (FEXISTS \<phi>); wf_interp_for_formula (w, I) (FEXISTS \<phi>); wf_interp_for_formula (w', I') (FEXISTS \<phi>)\<rbrakk> \<Longrightarrow> ((w, I) \<Turnstile> FEXISTS \<phi>) = ((w', I') \<Turnstile> FEXISTS \<phi>)
[PROOF STEP]
hence length: "length I' = length I"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>stream_enc (?w2, ?I2) = stream_enc (?w'2, ?I'2); wf_formula (length ?I2) \<phi>; wf_interp_for_formula (?w2, ?I2) \<phi>; wf_interp_for_formula (?w'2, ?I'2) \<phi>\<rbrakk> \<Longrightarrow> ((?w2, ?I2) \<Turnstile> \<phi>) = ((?w'2, ?I'2) \<Turnstile> \<phi>)
stream_enc (w, I) = stream_enc (w', I')
wf_formula (length I) (FExists \<phi>)
wf_interp_for_formula (w, I) (FExists \<phi>)
wf_interp_for_formula (w', I') (FExists \<phi>)

goal (1 subgoal):
 1. length I' = length I
[PROOF STEP]
by (metis length_snth_enc)
[PROOF STATE]
proof (state)
this:
length I' = length I

goal (3 subgoals):
 1. \<And>\<phi> w w' I I'. \<lbrakk>\<And>w w' I I'. \<lbrakk>stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) \<phi>; wf_interp_for_formula (w, I) \<phi>; wf_interp_for_formula (w', I') \<phi>\<rbrakk> \<Longrightarrow> ((w, I) \<Turnstile> \<phi>) = ((w', I') \<Turnstile> \<phi>); stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) (FNot \<phi>); wf_interp_for_formula (w, I) (FNot \<phi>); wf_interp_for_formula (w', I') (FNot \<phi>)\<rbrakk> \<Longrightarrow> ((w, I) \<Turnstile> FNot \<phi>) = ((w', I') \<Turnstile> FNot \<phi>)
 2. \<And>\<phi> w w' I I'. \<lbrakk>\<And>w w' I I'. \<lbrakk>stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) \<phi>; wf_interp_for_formula (w, I) \<phi>; wf_interp_for_formula (w', I') \<phi>\<rbrakk> \<Longrightarrow> ((w, I) \<Turnstile> \<phi>) = ((w', I') \<Turnstile> \<phi>); stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) (FExists \<phi>); wf_interp_for_formula (w, I) (FExists \<phi>); wf_interp_for_formula (w', I') (FExists \<phi>)\<rbrakk> \<Longrightarrow> ((w, I) \<Turnstile> FExists \<phi>) = ((w', I') \<Turnstile> FExists \<phi>)
 3. \<And>\<phi> w w' I I'. \<lbrakk>\<And>w w' I I'. \<lbrakk>stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) \<phi>; wf_interp_for_formula (w, I) \<phi>; wf_interp_for_formula (w', I') \<phi>\<rbrakk> \<Longrightarrow> ((w, I) \<Turnstile> \<phi>) = ((w', I') \<Turnstile> \<phi>); stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) (FEXISTS \<phi>); wf_interp_for_formula (w, I) (FEXISTS \<phi>); wf_interp_for_formula (w', I') (FEXISTS \<phi>)\<rbrakk> \<Longrightarrow> ((w, I) \<Turnstile> FEXISTS \<phi>) = ((w', I') \<Turnstile> FEXISTS \<phi>)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((w, I) \<Turnstile> FExists \<phi>) = ((w', I') \<Turnstile> FExists \<phi>)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. (w, I) \<Turnstile> FExists \<phi> \<Longrightarrow> (w', I') \<Turnstile> FExists \<phi>
 2. (w', I') \<Turnstile> FExists \<phi> \<Longrightarrow> (w, I) \<Turnstile> FExists \<phi>
[PROOF STEP]
assume "(w, I) \<Turnstile> FExists \<phi>"
[PROOF STATE]
proof (state)
this:
(w, I) \<Turnstile> FExists \<phi>

goal (2 subgoals):
 1. (w, I) \<Turnstile> FExists \<phi> \<Longrightarrow> (w', I') \<Turnstile> FExists \<phi>
 2. (w', I') \<Turnstile> FExists \<phi> \<Longrightarrow> (w, I) \<Turnstile> FExists \<phi>
[PROOF STEP]
with FExists.prems(3)
[PROOF STATE]
proof (chain)
picking this:
wf_interp_for_formula (w, I) (FExists \<phi>)
(w, I) \<Turnstile> FExists \<phi>
[PROOF STEP]
obtain p where "(w, Inl p # I) \<Turnstile> \<phi>"
[PROOF STATE]
proof (prove)
using this:
wf_interp_for_formula (w, I) (FExists \<phi>)
(w, I) \<Turnstile> FExists \<phi>

goal (1 subgoal):
 1. (\<And>p. (w, Inl p # I) \<Turnstile> \<phi> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(w, Inl p # I) \<Turnstile> \<phi>

goal (2 subgoals):
 1. (w, I) \<Turnstile> FExists \<phi> \<Longrightarrow> (w', I') \<Turnstile> FExists \<phi>
 2. (w', I') \<Turnstile> FExists \<phi> \<Longrightarrow> (w, I) \<Turnstile> FExists \<phi>
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(w, Inl p # I) \<Turnstile> \<phi>

goal (2 subgoals):
 1. (w, I) \<Turnstile> FExists \<phi> \<Longrightarrow> (w', I') \<Turnstile> FExists \<phi>
 2. (w', I') \<Turnstile> FExists \<phi> \<Longrightarrow> (w, I) \<Turnstile> FExists \<phi>
[PROOF STEP]
with FExists.prems(1,2)
[PROOF STATE]
proof (chain)
picking this:
stream_enc (w, I) = stream_enc (w', I')
wf_formula (length I) (FExists \<phi>)
(w, Inl p # I) \<Turnstile> \<phi>
[PROOF STEP]
have "(w', Inl p # I') \<Turnstile> \<phi>"
[PROOF STATE]
proof (prove)
using this:
stream_enc (w, I) = stream_enc (w', I')
wf_formula (length I) (FExists \<phi>)
(w, Inl p # I) \<Turnstile> \<phi>

goal (1 subgoal):
 1. (w', Inl p # I') \<Turnstile> \<phi>
[PROOF STEP]
proof (intro iffD1[OF FExists.IH[of w "Inl p # I" w' "Inl p # I'"]])
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<lbrakk>stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) (FExists \<phi>); (w, Inl p # I) \<Turnstile> \<phi>\<rbrakk> \<Longrightarrow> stream_enc (w, Inl p # I) = stream_enc (w', Inl p # I')
 2. \<lbrakk>stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) (FExists \<phi>); (w, Inl p # I) \<Turnstile> \<phi>\<rbrakk> \<Longrightarrow> wf_formula (length (Inl p # I)) \<phi>
 3. \<lbrakk>stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) (FExists \<phi>); (w, Inl p # I) \<Turnstile> \<phi>\<rbrakk> \<Longrightarrow> wf_interp_for_formula (w, Inl p # I) \<phi>
 4. \<lbrakk>stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) (FExists \<phi>); (w, Inl p # I) \<Turnstile> \<phi>\<rbrakk> \<Longrightarrow> wf_interp_for_formula (w', Inl p # I') \<phi>
 5. \<lbrakk>stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) (FExists \<phi>); (w, Inl p # I) \<Turnstile> \<phi>\<rbrakk> \<Longrightarrow> (w, Inl p # I) \<Turnstile> \<phi>
[PROOF STEP]
from FExists.prems(2,3)
[PROOF STATE]
proof (chain)
picking this:
wf_formula (length I) (FExists \<phi>)
wf_interp_for_formula (w, I) (FExists \<phi>)
[PROOF STEP]
show "wf_interp_for_formula (w, Inl p # I) \<phi>"
[PROOF STATE]
proof (prove)
using this:
wf_formula (length I) (FExists \<phi>)
wf_interp_for_formula (w, I) (FExists \<phi>)

goal (1 subgoal):
 1. wf_interp_for_formula (w, Inl p # I) \<phi>
[PROOF STEP]
by (blast dest: wf_interp_for_formula_FExists[of I])
[PROOF STATE]
proof (state)
this:
wf_interp_for_formula (w, Inl p # I) \<phi>

goal (4 subgoals):
 1. \<lbrakk>stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) (FExists \<phi>); (w, Inl p # I) \<Turnstile> \<phi>\<rbrakk> \<Longrightarrow> stream_enc (w, Inl p # I) = stream_enc (w', Inl p # I')
 2. \<lbrakk>stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) (FExists \<phi>); (w, Inl p # I) \<Turnstile> \<phi>\<rbrakk> \<Longrightarrow> wf_formula (length (Inl p # I)) \<phi>
 3. \<lbrakk>stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) (FExists \<phi>); (w, Inl p # I) \<Turnstile> \<phi>\<rbrakk> \<Longrightarrow> wf_interp_for_formula (w', Inl p # I') \<phi>
 4. \<lbrakk>stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) (FExists \<phi>); (w, Inl p # I) \<Turnstile> \<phi>\<rbrakk> \<Longrightarrow> (w, Inl p # I) \<Turnstile> \<phi>
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<lbrakk>stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) (FExists \<phi>); (w, Inl p # I) \<Turnstile> \<phi>\<rbrakk> \<Longrightarrow> stream_enc (w, Inl p # I) = stream_enc (w', Inl p # I')
 2. \<lbrakk>stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) (FExists \<phi>); (w, Inl p # I) \<Turnstile> \<phi>\<rbrakk> \<Longrightarrow> wf_formula (length (Inl p # I)) \<phi>
 3. \<lbrakk>stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) (FExists \<phi>); (w, Inl p # I) \<Turnstile> \<phi>\<rbrakk> \<Longrightarrow> wf_interp_for_formula (w', Inl p # I') \<phi>
 4. \<lbrakk>stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) (FExists \<phi>); (w, Inl p # I) \<Turnstile> \<phi>\<rbrakk> \<Longrightarrow> (w, Inl p # I) \<Turnstile> \<phi>
[PROOF STEP]
from FExists.prems(2,4)
[PROOF STATE]
proof (chain)
picking this:
wf_formula (length I) (FExists \<phi>)
wf_interp_for_formula (w', I') (FExists \<phi>)
[PROOF STEP]
show "wf_interp_for_formula (w', Inl p # I') \<phi>"
[PROOF STATE]
proof (prove)
using this:
wf_formula (length I) (FExists \<phi>)
wf_interp_for_formula (w', I') (FExists \<phi>)

goal (1 subgoal):
 1. wf_interp_for_formula (w', Inl p # I') \<phi>
[PROOF STEP]
by (blast dest: wf_interp_for_formula_FExists[of I', unfolded length])
[PROOF STATE]
proof (state)
this:
wf_interp_for_formula (w', Inl p # I') \<phi>

goal (3 subgoals):
 1. \<lbrakk>stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) (FExists \<phi>); (w, Inl p # I) \<Turnstile> \<phi>\<rbrakk> \<Longrightarrow> stream_enc (w, Inl p # I) = stream_enc (w', Inl p # I')
 2. \<lbrakk>stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) (FExists \<phi>); (w, Inl p # I) \<Turnstile> \<phi>\<rbrakk> \<Longrightarrow> wf_formula (length (Inl p # I)) \<phi>
 3. \<lbrakk>stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) (FExists \<phi>); (w, Inl p # I) \<Turnstile> \<phi>\<rbrakk> \<Longrightarrow> (w, Inl p # I) \<Turnstile> \<phi>
[PROOF STEP]
qed (auto simp: smap2_alt split: sum.splits if_split_asm)
[PROOF STATE]
proof (state)
this:
(w', Inl p # I') \<Turnstile> \<phi>

goal (2 subgoals):
 1. (w, I) \<Turnstile> FExists \<phi> \<Longrightarrow> (w', I') \<Turnstile> FExists \<phi>
 2. (w', I') \<Turnstile> FExists \<phi> \<Longrightarrow> (w, I) \<Turnstile> FExists \<phi>
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(w, Inl p # I) \<Turnstile> \<phi>
(w', Inl p # I') \<Turnstile> \<phi>
[PROOF STEP]
show "(w', I') \<Turnstile> FExists \<phi>"
[PROOF STATE]
proof (prove)
using this:
(w, Inl p # I) \<Turnstile> \<phi>
(w', Inl p # I') \<Turnstile> \<phi>

goal (1 subgoal):
 1. (w', I') \<Turnstile> FExists \<phi>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(w', I') \<Turnstile> FExists \<phi>

goal (1 subgoal):
 1. (w', I') \<Turnstile> FExists \<phi> \<Longrightarrow> (w, I) \<Turnstile> FExists \<phi>
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (w', I') \<Turnstile> FExists \<phi> \<Longrightarrow> (w, I) \<Turnstile> FExists \<phi>
[PROOF STEP]
assume "(w', I') \<Turnstile> FExists \<phi>"
[PROOF STATE]
proof (state)
this:
(w', I') \<Turnstile> FExists \<phi>

goal (1 subgoal):
 1. (w', I') \<Turnstile> FExists \<phi> \<Longrightarrow> (w, I) \<Turnstile> FExists \<phi>
[PROOF STEP]
with FExists.prems(1,2,4)
[PROOF STATE]
proof (chain)
picking this:
stream_enc (w, I) = stream_enc (w', I')
wf_formula (length I) (FExists \<phi>)
wf_interp_for_formula (w', I') (FExists \<phi>)
(w', I') \<Turnstile> FExists \<phi>
[PROOF STEP]
obtain p where "(w', Inl p # I') \<Turnstile> \<phi>"
[PROOF STATE]
proof (prove)
using this:
stream_enc (w, I) = stream_enc (w', I')
wf_formula (length I) (FExists \<phi>)
wf_interp_for_formula (w', I') (FExists \<phi>)
(w', I') \<Turnstile> FExists \<phi>

goal (1 subgoal):
 1. (\<And>p. (w', Inl p # I') \<Turnstile> \<phi> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(w', Inl p # I') \<Turnstile> \<phi>

goal (1 subgoal):
 1. (w', I') \<Turnstile> FExists \<phi> \<Longrightarrow> (w, I) \<Turnstile> FExists \<phi>
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(w', Inl p # I') \<Turnstile> \<phi>

goal (1 subgoal):
 1. (w', I') \<Turnstile> FExists \<phi> \<Longrightarrow> (w, I) \<Turnstile> FExists \<phi>
[PROOF STEP]
with FExists.prems(1,2)
[PROOF STATE]
proof (chain)
picking this:
stream_enc (w, I) = stream_enc (w', I')
wf_formula (length I) (FExists \<phi>)
(w', Inl p # I') \<Turnstile> \<phi>
[PROOF STEP]
have "(w, Inl p # I) \<Turnstile> \<phi>"
[PROOF STATE]
proof (prove)
using this:
stream_enc (w, I) = stream_enc (w', I')
wf_formula (length I) (FExists \<phi>)
(w', Inl p # I') \<Turnstile> \<phi>

goal (1 subgoal):
 1. (w, Inl p # I) \<Turnstile> \<phi>
[PROOF STEP]
proof (intro iffD2[OF FExists.IH[of w "Inl p # I" w' "Inl p # I'"]])
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<lbrakk>stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) (FExists \<phi>); (w', Inl p # I') \<Turnstile> \<phi>\<rbrakk> \<Longrightarrow> stream_enc (w, Inl p # I) = stream_enc (w', Inl p # I')
 2. \<lbrakk>stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) (FExists \<phi>); (w', Inl p # I') \<Turnstile> \<phi>\<rbrakk> \<Longrightarrow> wf_formula (length (Inl p # I)) \<phi>
 3. \<lbrakk>stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) (FExists \<phi>); (w', Inl p # I') \<Turnstile> \<phi>\<rbrakk> \<Longrightarrow> wf_interp_for_formula (w, Inl p # I) \<phi>
 4. \<lbrakk>stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) (FExists \<phi>); (w', Inl p # I') \<Turnstile> \<phi>\<rbrakk> \<Longrightarrow> wf_interp_for_formula (w', Inl p # I') \<phi>
 5. \<lbrakk>stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) (FExists \<phi>); (w', Inl p # I') \<Turnstile> \<phi>\<rbrakk> \<Longrightarrow> (w', Inl p # I') \<Turnstile> \<phi>
[PROOF STEP]
from FExists.prems(2,3)
[PROOF STATE]
proof (chain)
picking this:
wf_formula (length I) (FExists \<phi>)
wf_interp_for_formula (w, I) (FExists \<phi>)
[PROOF STEP]
show "wf_interp_for_formula (w, Inl p # I) \<phi>"
[PROOF STATE]
proof (prove)
using this:
wf_formula (length I) (FExists \<phi>)
wf_interp_for_formula (w, I) (FExists \<phi>)

goal (1 subgoal):
 1. wf_interp_for_formula (w, Inl p # I) \<phi>
[PROOF STEP]
by (blast dest: wf_interp_for_formula_FExists[of I])
[PROOF STATE]
proof (state)
this:
wf_interp_for_formula (w, Inl p # I) \<phi>

goal (4 subgoals):
 1. \<lbrakk>stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) (FExists \<phi>); (w', Inl p # I') \<Turnstile> \<phi>\<rbrakk> \<Longrightarrow> stream_enc (w, Inl p # I) = stream_enc (w', Inl p # I')
 2. \<lbrakk>stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) (FExists \<phi>); (w', Inl p # I') \<Turnstile> \<phi>\<rbrakk> \<Longrightarrow> wf_formula (length (Inl p # I)) \<phi>
 3. \<lbrakk>stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) (FExists \<phi>); (w', Inl p # I') \<Turnstile> \<phi>\<rbrakk> \<Longrightarrow> wf_interp_for_formula (w', Inl p # I') \<phi>
 4. \<lbrakk>stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) (FExists \<phi>); (w', Inl p # I') \<Turnstile> \<phi>\<rbrakk> \<Longrightarrow> (w', Inl p # I') \<Turnstile> \<phi>
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<lbrakk>stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) (FExists \<phi>); (w', Inl p # I') \<Turnstile> \<phi>\<rbrakk> \<Longrightarrow> stream_enc (w, Inl p # I) = stream_enc (w', Inl p # I')
 2. \<lbrakk>stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) (FExists \<phi>); (w', Inl p # I') \<Turnstile> \<phi>\<rbrakk> \<Longrightarrow> wf_formula (length (Inl p # I)) \<phi>
 3. \<lbrakk>stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) (FExists \<phi>); (w', Inl p # I') \<Turnstile> \<phi>\<rbrakk> \<Longrightarrow> wf_interp_for_formula (w', Inl p # I') \<phi>
 4. \<lbrakk>stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) (FExists \<phi>); (w', Inl p # I') \<Turnstile> \<phi>\<rbrakk> \<Longrightarrow> (w', Inl p # I') \<Turnstile> \<phi>
[PROOF STEP]
from FExists.prems(2,4)
[PROOF STATE]
proof (chain)
picking this:
wf_formula (length I) (FExists \<phi>)
wf_interp_for_formula (w', I') (FExists \<phi>)
[PROOF STEP]
show "wf_interp_for_formula (w', Inl p # I') \<phi>"
[PROOF STATE]
proof (prove)
using this:
wf_formula (length I) (FExists \<phi>)
wf_interp_for_formula (w', I') (FExists \<phi>)

goal (1 subgoal):
 1. wf_interp_for_formula (w', Inl p # I') \<phi>
[PROOF STEP]
by (blast dest: wf_interp_for_formula_FExists[of I', unfolded length])
[PROOF STATE]
proof (state)
this:
wf_interp_for_formula (w', Inl p # I') \<phi>

goal (3 subgoals):
 1. \<lbrakk>stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) (FExists \<phi>); (w', Inl p # I') \<Turnstile> \<phi>\<rbrakk> \<Longrightarrow> stream_enc (w, Inl p # I) = stream_enc (w', Inl p # I')
 2. \<lbrakk>stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) (FExists \<phi>); (w', Inl p # I') \<Turnstile> \<phi>\<rbrakk> \<Longrightarrow> wf_formula (length (Inl p # I)) \<phi>
 3. \<lbrakk>stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) (FExists \<phi>); (w', Inl p # I') \<Turnstile> \<phi>\<rbrakk> \<Longrightarrow> (w', Inl p # I') \<Turnstile> \<phi>
[PROOF STEP]
qed (auto simp: smap2_alt split: sum.splits if_split_asm)
[PROOF STATE]
proof (state)
this:
(w, Inl p # I) \<Turnstile> \<phi>

goal (1 subgoal):
 1. (w', I') \<Turnstile> FExists \<phi> \<Longrightarrow> (w, I) \<Turnstile> FExists \<phi>
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(w', Inl p # I') \<Turnstile> \<phi>
(w, Inl p # I) \<Turnstile> \<phi>
[PROOF STEP]
show "(w, I) \<Turnstile> FExists \<phi>"
[PROOF STATE]
proof (prove)
using this:
(w', Inl p # I') \<Turnstile> \<phi>
(w, Inl p # I) \<Turnstile> \<phi>

goal (1 subgoal):
 1. (w, I) \<Turnstile> FExists \<phi>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(w, I) \<Turnstile> FExists \<phi>

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
((w, I) \<Turnstile> FExists \<phi>) = ((w', I') \<Turnstile> FExists \<phi>)

goal (2 subgoals):
 1. \<And>\<phi> w w' I I'. \<lbrakk>\<And>w w' I I'. \<lbrakk>stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) \<phi>; wf_interp_for_formula (w, I) \<phi>; wf_interp_for_formula (w', I') \<phi>\<rbrakk> \<Longrightarrow> ((w, I) \<Turnstile> \<phi>) = ((w', I') \<Turnstile> \<phi>); stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) (FNot \<phi>); wf_interp_for_formula (w, I) (FNot \<phi>); wf_interp_for_formula (w', I') (FNot \<phi>)\<rbrakk> \<Longrightarrow> ((w, I) \<Turnstile> FNot \<phi>) = ((w', I') \<Turnstile> FNot \<phi>)
 2. \<And>\<phi> w w' I I'. \<lbrakk>\<And>w w' I I'. \<lbrakk>stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) \<phi>; wf_interp_for_formula (w, I) \<phi>; wf_interp_for_formula (w', I') \<phi>\<rbrakk> \<Longrightarrow> ((w, I) \<Turnstile> \<phi>) = ((w', I') \<Turnstile> \<phi>); stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) (FEXISTS \<phi>); wf_interp_for_formula (w, I) (FEXISTS \<phi>); wf_interp_for_formula (w', I') (FEXISTS \<phi>)\<rbrakk> \<Longrightarrow> ((w, I) \<Turnstile> FEXISTS \<phi>) = ((w', I') \<Turnstile> FEXISTS \<phi>)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>\<phi> w w' I I'. \<lbrakk>\<And>w w' I I'. \<lbrakk>stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) \<phi>; wf_interp_for_formula (w, I) \<phi>; wf_interp_for_formula (w', I') \<phi>\<rbrakk> \<Longrightarrow> ((w, I) \<Turnstile> \<phi>) = ((w', I') \<Turnstile> \<phi>); stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) (FNot \<phi>); wf_interp_for_formula (w, I) (FNot \<phi>); wf_interp_for_formula (w', I') (FNot \<phi>)\<rbrakk> \<Longrightarrow> ((w, I) \<Turnstile> FNot \<phi>) = ((w', I') \<Turnstile> FNot \<phi>)
 2. \<And>\<phi> w w' I I'. \<lbrakk>\<And>w w' I I'. \<lbrakk>stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) \<phi>; wf_interp_for_formula (w, I) \<phi>; wf_interp_for_formula (w', I') \<phi>\<rbrakk> \<Longrightarrow> ((w, I) \<Turnstile> \<phi>) = ((w', I') \<Turnstile> \<phi>); stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) (FEXISTS \<phi>); wf_interp_for_formula (w, I) (FEXISTS \<phi>); wf_interp_for_formula (w', I') (FEXISTS \<phi>)\<rbrakk> \<Longrightarrow> ((w, I) \<Turnstile> FEXISTS \<phi>) = ((w', I') \<Turnstile> FEXISTS \<phi>)
[PROOF STEP]
case (FEXISTS \<phi>)
[PROOF STATE]
proof (state)
this:
\<lbrakk>stream_enc (?w2, ?I2) = stream_enc (?w'2, ?I'2); wf_formula (length ?I2) \<phi>; wf_interp_for_formula (?w2, ?I2) \<phi>; wf_interp_for_formula (?w'2, ?I'2) \<phi>\<rbrakk> \<Longrightarrow> ((?w2, ?I2) \<Turnstile> \<phi>) = ((?w'2, ?I'2) \<Turnstile> \<phi>)
stream_enc (w, I) = stream_enc (w', I')
wf_formula (length I) (FEXISTS \<phi>)
wf_interp_for_formula (w, I) (FEXISTS \<phi>)
wf_interp_for_formula (w', I') (FEXISTS \<phi>)

goal (2 subgoals):
 1. \<And>\<phi> w w' I I'. \<lbrakk>\<And>w w' I I'. \<lbrakk>stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) \<phi>; wf_interp_for_formula (w, I) \<phi>; wf_interp_for_formula (w', I') \<phi>\<rbrakk> \<Longrightarrow> ((w, I) \<Turnstile> \<phi>) = ((w', I') \<Turnstile> \<phi>); stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) (FNot \<phi>); wf_interp_for_formula (w, I) (FNot \<phi>); wf_interp_for_formula (w', I') (FNot \<phi>)\<rbrakk> \<Longrightarrow> ((w, I) \<Turnstile> FNot \<phi>) = ((w', I') \<Turnstile> FNot \<phi>)
 2. \<And>\<phi> w w' I I'. \<lbrakk>\<And>w w' I I'. \<lbrakk>stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) \<phi>; wf_interp_for_formula (w, I) \<phi>; wf_interp_for_formula (w', I') \<phi>\<rbrakk> \<Longrightarrow> ((w, I) \<Turnstile> \<phi>) = ((w', I') \<Turnstile> \<phi>); stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) (FEXISTS \<phi>); wf_interp_for_formula (w, I) (FEXISTS \<phi>); wf_interp_for_formula (w', I') (FEXISTS \<phi>)\<rbrakk> \<Longrightarrow> ((w, I) \<Turnstile> FEXISTS \<phi>) = ((w', I') \<Turnstile> FEXISTS \<phi>)
[PROOF STEP]
hence length: "length I' = length I"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>stream_enc (?w2, ?I2) = stream_enc (?w'2, ?I'2); wf_formula (length ?I2) \<phi>; wf_interp_for_formula (?w2, ?I2) \<phi>; wf_interp_for_formula (?w'2, ?I'2) \<phi>\<rbrakk> \<Longrightarrow> ((?w2, ?I2) \<Turnstile> \<phi>) = ((?w'2, ?I'2) \<Turnstile> \<phi>)
stream_enc (w, I) = stream_enc (w', I')
wf_formula (length I) (FEXISTS \<phi>)
wf_interp_for_formula (w, I) (FEXISTS \<phi>)
wf_interp_for_formula (w', I') (FEXISTS \<phi>)

goal (1 subgoal):
 1. length I' = length I
[PROOF STEP]
by (metis length_snth_enc)
[PROOF STATE]
proof (state)
this:
length I' = length I

goal (2 subgoals):
 1. \<And>\<phi> w w' I I'. \<lbrakk>\<And>w w' I I'. \<lbrakk>stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) \<phi>; wf_interp_for_formula (w, I) \<phi>; wf_interp_for_formula (w', I') \<phi>\<rbrakk> \<Longrightarrow> ((w, I) \<Turnstile> \<phi>) = ((w', I') \<Turnstile> \<phi>); stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) (FNot \<phi>); wf_interp_for_formula (w, I) (FNot \<phi>); wf_interp_for_formula (w', I') (FNot \<phi>)\<rbrakk> \<Longrightarrow> ((w, I) \<Turnstile> FNot \<phi>) = ((w', I') \<Turnstile> FNot \<phi>)
 2. \<And>\<phi> w w' I I'. \<lbrakk>\<And>w w' I I'. \<lbrakk>stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) \<phi>; wf_interp_for_formula (w, I) \<phi>; wf_interp_for_formula (w', I') \<phi>\<rbrakk> \<Longrightarrow> ((w, I) \<Turnstile> \<phi>) = ((w', I') \<Turnstile> \<phi>); stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) (FEXISTS \<phi>); wf_interp_for_formula (w, I) (FEXISTS \<phi>); wf_interp_for_formula (w', I') (FEXISTS \<phi>)\<rbrakk> \<Longrightarrow> ((w, I) \<Turnstile> FEXISTS \<phi>) = ((w', I') \<Turnstile> FEXISTS \<phi>)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((w, I) \<Turnstile> FEXISTS \<phi>) = ((w', I') \<Turnstile> FEXISTS \<phi>)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. (w, I) \<Turnstile> FEXISTS \<phi> \<Longrightarrow> (w', I') \<Turnstile> FEXISTS \<phi>
 2. (w', I') \<Turnstile> FEXISTS \<phi> \<Longrightarrow> (w, I) \<Turnstile> FEXISTS \<phi>
[PROOF STEP]
assume "(w, I) \<Turnstile> FEXISTS \<phi>"
[PROOF STATE]
proof (state)
this:
(w, I) \<Turnstile> FEXISTS \<phi>

goal (2 subgoals):
 1. (w, I) \<Turnstile> FEXISTS \<phi> \<Longrightarrow> (w', I') \<Turnstile> FEXISTS \<phi>
 2. (w', I') \<Turnstile> FEXISTS \<phi> \<Longrightarrow> (w, I) \<Turnstile> FEXISTS \<phi>
[PROOF STEP]
with FEXISTS.prems(3)
[PROOF STATE]
proof (chain)
picking this:
wf_interp_for_formula (w, I) (FEXISTS \<phi>)
(w, I) \<Turnstile> FEXISTS \<phi>
[PROOF STEP]
obtain P where "finite P" "(w, Inr P # I) \<Turnstile> \<phi>"
[PROOF STATE]
proof (prove)
using this:
wf_interp_for_formula (w, I) (FEXISTS \<phi>)
(w, I) \<Turnstile> FEXISTS \<phi>

goal (1 subgoal):
 1. (\<And>P. \<lbrakk>finite P; (w, Inr P # I) \<Turnstile> \<phi>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
finite P
(w, Inr P # I) \<Turnstile> \<phi>

goal (2 subgoals):
 1. (w, I) \<Turnstile> FEXISTS \<phi> \<Longrightarrow> (w', I') \<Turnstile> FEXISTS \<phi>
 2. (w', I') \<Turnstile> FEXISTS \<phi> \<Longrightarrow> (w, I) \<Turnstile> FEXISTS \<phi>
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
finite P
(w, Inr P # I) \<Turnstile> \<phi>

goal (2 subgoals):
 1. (w, I) \<Turnstile> FEXISTS \<phi> \<Longrightarrow> (w', I') \<Turnstile> FEXISTS \<phi>
 2. (w', I') \<Turnstile> FEXISTS \<phi> \<Longrightarrow> (w, I) \<Turnstile> FEXISTS \<phi>
[PROOF STEP]
with FEXISTS.prems(1,2)
[PROOF STATE]
proof (chain)
picking this:
stream_enc (w, I) = stream_enc (w', I')
wf_formula (length I) (FEXISTS \<phi>)
finite P
(w, Inr P # I) \<Turnstile> \<phi>
[PROOF STEP]
have "(w', Inr P # I') \<Turnstile> \<phi>"
[PROOF STATE]
proof (prove)
using this:
stream_enc (w, I) = stream_enc (w', I')
wf_formula (length I) (FEXISTS \<phi>)
finite P
(w, Inr P # I) \<Turnstile> \<phi>

goal (1 subgoal):
 1. (w', Inr P # I') \<Turnstile> \<phi>
[PROOF STEP]
proof (intro iffD1[OF FEXISTS.IH[of w "Inr P # I" w' "Inr P # I'"]])
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<lbrakk>stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) (FEXISTS \<phi>); finite P; (w, Inr P # I) \<Turnstile> \<phi>\<rbrakk> \<Longrightarrow> stream_enc (w, Inr P # I) = stream_enc (w', Inr P # I')
 2. \<lbrakk>stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) (FEXISTS \<phi>); finite P; (w, Inr P # I) \<Turnstile> \<phi>\<rbrakk> \<Longrightarrow> wf_formula (length (Inr P # I)) \<phi>
 3. \<lbrakk>stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) (FEXISTS \<phi>); finite P; (w, Inr P # I) \<Turnstile> \<phi>\<rbrakk> \<Longrightarrow> wf_interp_for_formula (w, Inr P # I) \<phi>
 4. \<lbrakk>stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) (FEXISTS \<phi>); finite P; (w, Inr P # I) \<Turnstile> \<phi>\<rbrakk> \<Longrightarrow> wf_interp_for_formula (w', Inr P # I') \<phi>
 5. \<lbrakk>stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) (FEXISTS \<phi>); finite P; (w, Inr P # I) \<Turnstile> \<phi>\<rbrakk> \<Longrightarrow> (w, Inr P # I) \<Turnstile> \<phi>
[PROOF STEP]
from FEXISTS.prems(2,3) \<open>finite P\<close>
[PROOF STATE]
proof (chain)
picking this:
wf_formula (length I) (FEXISTS \<phi>)
wf_interp_for_formula (w, I) (FEXISTS \<phi>)
finite P
[PROOF STEP]
show "wf_interp_for_formula (w, Inr P # I) \<phi>"
[PROOF STATE]
proof (prove)
using this:
wf_formula (length I) (FEXISTS \<phi>)
wf_interp_for_formula (w, I) (FEXISTS \<phi>)
finite P

goal (1 subgoal):
 1. wf_interp_for_formula (w, Inr P # I) \<phi>
[PROOF STEP]
by (blast dest: wf_interp_for_formula_FEXISTS[of I])
[PROOF STATE]
proof (state)
this:
wf_interp_for_formula (w, Inr P # I) \<phi>

goal (4 subgoals):
 1. \<lbrakk>stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) (FEXISTS \<phi>); finite P; (w, Inr P # I) \<Turnstile> \<phi>\<rbrakk> \<Longrightarrow> stream_enc (w, Inr P # I) = stream_enc (w', Inr P # I')
 2. \<lbrakk>stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) (FEXISTS \<phi>); finite P; (w, Inr P # I) \<Turnstile> \<phi>\<rbrakk> \<Longrightarrow> wf_formula (length (Inr P # I)) \<phi>
 3. \<lbrakk>stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) (FEXISTS \<phi>); finite P; (w, Inr P # I) \<Turnstile> \<phi>\<rbrakk> \<Longrightarrow> wf_interp_for_formula (w', Inr P # I') \<phi>
 4. \<lbrakk>stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) (FEXISTS \<phi>); finite P; (w, Inr P # I) \<Turnstile> \<phi>\<rbrakk> \<Longrightarrow> (w, Inr P # I) \<Turnstile> \<phi>
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<lbrakk>stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) (FEXISTS \<phi>); finite P; (w, Inr P # I) \<Turnstile> \<phi>\<rbrakk> \<Longrightarrow> stream_enc (w, Inr P # I) = stream_enc (w', Inr P # I')
 2. \<lbrakk>stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) (FEXISTS \<phi>); finite P; (w, Inr P # I) \<Turnstile> \<phi>\<rbrakk> \<Longrightarrow> wf_formula (length (Inr P # I)) \<phi>
 3. \<lbrakk>stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) (FEXISTS \<phi>); finite P; (w, Inr P # I) \<Turnstile> \<phi>\<rbrakk> \<Longrightarrow> wf_interp_for_formula (w', Inr P # I') \<phi>
 4. \<lbrakk>stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) (FEXISTS \<phi>); finite P; (w, Inr P # I) \<Turnstile> \<phi>\<rbrakk> \<Longrightarrow> (w, Inr P # I) \<Turnstile> \<phi>
[PROOF STEP]
from FEXISTS.prems(2,4) \<open>finite P\<close>
[PROOF STATE]
proof (chain)
picking this:
wf_formula (length I) (FEXISTS \<phi>)
wf_interp_for_formula (w', I') (FEXISTS \<phi>)
finite P
[PROOF STEP]
show "wf_interp_for_formula (w', Inr P # I') \<phi>"
[PROOF STATE]
proof (prove)
using this:
wf_formula (length I) (FEXISTS \<phi>)
wf_interp_for_formula (w', I') (FEXISTS \<phi>)
finite P

goal (1 subgoal):
 1. wf_interp_for_formula (w', Inr P # I') \<phi>
[PROOF STEP]
by (blast dest: wf_interp_for_formula_FEXISTS[of I', unfolded length])
[PROOF STATE]
proof (state)
this:
wf_interp_for_formula (w', Inr P # I') \<phi>

goal (3 subgoals):
 1. \<lbrakk>stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) (FEXISTS \<phi>); finite P; (w, Inr P # I) \<Turnstile> \<phi>\<rbrakk> \<Longrightarrow> stream_enc (w, Inr P # I) = stream_enc (w', Inr P # I')
 2. \<lbrakk>stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) (FEXISTS \<phi>); finite P; (w, Inr P # I) \<Turnstile> \<phi>\<rbrakk> \<Longrightarrow> wf_formula (length (Inr P # I)) \<phi>
 3. \<lbrakk>stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) (FEXISTS \<phi>); finite P; (w, Inr P # I) \<Turnstile> \<phi>\<rbrakk> \<Longrightarrow> (w, Inr P # I) \<Turnstile> \<phi>
[PROOF STEP]
qed (auto simp: smap2_alt split: sum.splits if_split_asm)
[PROOF STATE]
proof (state)
this:
(w', Inr P # I') \<Turnstile> \<phi>

goal (2 subgoals):
 1. (w, I) \<Turnstile> FEXISTS \<phi> \<Longrightarrow> (w', I') \<Turnstile> FEXISTS \<phi>
 2. (w', I') \<Turnstile> FEXISTS \<phi> \<Longrightarrow> (w, I) \<Turnstile> FEXISTS \<phi>
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
finite P
(w, Inr P # I) \<Turnstile> \<phi>
(w', Inr P # I') \<Turnstile> \<phi>
[PROOF STEP]
show "(w', I') \<Turnstile> FEXISTS \<phi>"
[PROOF STATE]
proof (prove)
using this:
finite P
(w, Inr P # I) \<Turnstile> \<phi>
(w', Inr P # I') \<Turnstile> \<phi>

goal (1 subgoal):
 1. (w', I') \<Turnstile> FEXISTS \<phi>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(w', I') \<Turnstile> FEXISTS \<phi>

goal (1 subgoal):
 1. (w', I') \<Turnstile> FEXISTS \<phi> \<Longrightarrow> (w, I) \<Turnstile> FEXISTS \<phi>
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (w', I') \<Turnstile> FEXISTS \<phi> \<Longrightarrow> (w, I) \<Turnstile> FEXISTS \<phi>
[PROOF STEP]
assume "(w', I') \<Turnstile> FEXISTS \<phi>"
[PROOF STATE]
proof (state)
this:
(w', I') \<Turnstile> FEXISTS \<phi>

goal (1 subgoal):
 1. (w', I') \<Turnstile> FEXISTS \<phi> \<Longrightarrow> (w, I) \<Turnstile> FEXISTS \<phi>
[PROOF STEP]
with FEXISTS.prems(1,2,4)
[PROOF STATE]
proof (chain)
picking this:
stream_enc (w, I) = stream_enc (w', I')
wf_formula (length I) (FEXISTS \<phi>)
wf_interp_for_formula (w', I') (FEXISTS \<phi>)
(w', I') \<Turnstile> FEXISTS \<phi>
[PROOF STEP]
obtain P where "finite P" "(w', Inr P # I') \<Turnstile> \<phi>"
[PROOF STATE]
proof (prove)
using this:
stream_enc (w, I) = stream_enc (w', I')
wf_formula (length I) (FEXISTS \<phi>)
wf_interp_for_formula (w', I') (FEXISTS \<phi>)
(w', I') \<Turnstile> FEXISTS \<phi>

goal (1 subgoal):
 1. (\<And>P. \<lbrakk>finite P; (w', Inr P # I') \<Turnstile> \<phi>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
finite P
(w', Inr P # I') \<Turnstile> \<phi>

goal (1 subgoal):
 1. (w', I') \<Turnstile> FEXISTS \<phi> \<Longrightarrow> (w, I) \<Turnstile> FEXISTS \<phi>
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
finite P
(w', Inr P # I') \<Turnstile> \<phi>

goal (1 subgoal):
 1. (w', I') \<Turnstile> FEXISTS \<phi> \<Longrightarrow> (w, I) \<Turnstile> FEXISTS \<phi>
[PROOF STEP]
with FEXISTS.prems
[PROOF STATE]
proof (chain)
picking this:
stream_enc (w, I) = stream_enc (w', I')
wf_formula (length I) (FEXISTS \<phi>)
wf_interp_for_formula (w, I) (FEXISTS \<phi>)
wf_interp_for_formula (w', I') (FEXISTS \<phi>)
finite P
(w', Inr P # I') \<Turnstile> \<phi>
[PROOF STEP]
have "(w, Inr P # I) \<Turnstile> \<phi>"
[PROOF STATE]
proof (prove)
using this:
stream_enc (w, I) = stream_enc (w', I')
wf_formula (length I) (FEXISTS \<phi>)
wf_interp_for_formula (w, I) (FEXISTS \<phi>)
wf_interp_for_formula (w', I') (FEXISTS \<phi>)
finite P
(w', Inr P # I') \<Turnstile> \<phi>

goal (1 subgoal):
 1. (w, Inr P # I) \<Turnstile> \<phi>
[PROOF STEP]
proof (intro iffD2[OF FEXISTS.IH[of w "Inr P # I" w' "Inr P # I'"]])
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<lbrakk>stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) (FEXISTS \<phi>); wf_interp_for_formula (w, I) (FEXISTS \<phi>); wf_interp_for_formula (w', I') (FEXISTS \<phi>); finite P; (w', Inr P # I') \<Turnstile> \<phi>\<rbrakk> \<Longrightarrow> stream_enc (w, Inr P # I) = stream_enc (w', Inr P # I')
 2. \<lbrakk>stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) (FEXISTS \<phi>); wf_interp_for_formula (w, I) (FEXISTS \<phi>); wf_interp_for_formula (w', I') (FEXISTS \<phi>); finite P; (w', Inr P # I') \<Turnstile> \<phi>\<rbrakk> \<Longrightarrow> wf_formula (length (Inr P # I)) \<phi>
 3. \<lbrakk>stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) (FEXISTS \<phi>); wf_interp_for_formula (w, I) (FEXISTS \<phi>); wf_interp_for_formula (w', I') (FEXISTS \<phi>); finite P; (w', Inr P # I') \<Turnstile> \<phi>\<rbrakk> \<Longrightarrow> wf_interp_for_formula (w, Inr P # I) \<phi>
 4. \<lbrakk>stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) (FEXISTS \<phi>); wf_interp_for_formula (w, I) (FEXISTS \<phi>); wf_interp_for_formula (w', I') (FEXISTS \<phi>); finite P; (w', Inr P # I') \<Turnstile> \<phi>\<rbrakk> \<Longrightarrow> wf_interp_for_formula (w', Inr P # I') \<phi>
 5. \<lbrakk>stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) (FEXISTS \<phi>); wf_interp_for_formula (w, I) (FEXISTS \<phi>); wf_interp_for_formula (w', I') (FEXISTS \<phi>); finite P; (w', Inr P # I') \<Turnstile> \<phi>\<rbrakk> \<Longrightarrow> (w', Inr P # I') \<Turnstile> \<phi>
[PROOF STEP]
from FEXISTS.prems(2,3) \<open>finite P\<close>
[PROOF STATE]
proof (chain)
picking this:
wf_formula (length I) (FEXISTS \<phi>)
wf_interp_for_formula (w, I) (FEXISTS \<phi>)
finite P
[PROOF STEP]
show "wf_interp_for_formula (w, Inr P # I) \<phi>"
[PROOF STATE]
proof (prove)
using this:
wf_formula (length I) (FEXISTS \<phi>)
wf_interp_for_formula (w, I) (FEXISTS \<phi>)
finite P

goal (1 subgoal):
 1. wf_interp_for_formula (w, Inr P # I) \<phi>
[PROOF STEP]
by (blast dest: wf_interp_for_formula_FEXISTS[of I])
[PROOF STATE]
proof (state)
this:
wf_interp_for_formula (w, Inr P # I) \<phi>

goal (4 subgoals):
 1. \<lbrakk>stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) (FEXISTS \<phi>); wf_interp_for_formula (w, I) (FEXISTS \<phi>); wf_interp_for_formula (w', I') (FEXISTS \<phi>); finite P; (w', Inr P # I') \<Turnstile> \<phi>\<rbrakk> \<Longrightarrow> stream_enc (w, Inr P # I) = stream_enc (w', Inr P # I')
 2. \<lbrakk>stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) (FEXISTS \<phi>); wf_interp_for_formula (w, I) (FEXISTS \<phi>); wf_interp_for_formula (w', I') (FEXISTS \<phi>); finite P; (w', Inr P # I') \<Turnstile> \<phi>\<rbrakk> \<Longrightarrow> wf_formula (length (Inr P # I)) \<phi>
 3. \<lbrakk>stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) (FEXISTS \<phi>); wf_interp_for_formula (w, I) (FEXISTS \<phi>); wf_interp_for_formula (w', I') (FEXISTS \<phi>); finite P; (w', Inr P # I') \<Turnstile> \<phi>\<rbrakk> \<Longrightarrow> wf_interp_for_formula (w', Inr P # I') \<phi>
 4. \<lbrakk>stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) (FEXISTS \<phi>); wf_interp_for_formula (w, I) (FEXISTS \<phi>); wf_interp_for_formula (w', I') (FEXISTS \<phi>); finite P; (w', Inr P # I') \<Turnstile> \<phi>\<rbrakk> \<Longrightarrow> (w', Inr P # I') \<Turnstile> \<phi>
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<lbrakk>stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) (FEXISTS \<phi>); wf_interp_for_formula (w, I) (FEXISTS \<phi>); wf_interp_for_formula (w', I') (FEXISTS \<phi>); finite P; (w', Inr P # I') \<Turnstile> \<phi>\<rbrakk> \<Longrightarrow> stream_enc (w, Inr P # I) = stream_enc (w', Inr P # I')
 2. \<lbrakk>stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) (FEXISTS \<phi>); wf_interp_for_formula (w, I) (FEXISTS \<phi>); wf_interp_for_formula (w', I') (FEXISTS \<phi>); finite P; (w', Inr P # I') \<Turnstile> \<phi>\<rbrakk> \<Longrightarrow> wf_formula (length (Inr P # I)) \<phi>
 3. \<lbrakk>stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) (FEXISTS \<phi>); wf_interp_for_formula (w, I) (FEXISTS \<phi>); wf_interp_for_formula (w', I') (FEXISTS \<phi>); finite P; (w', Inr P # I') \<Turnstile> \<phi>\<rbrakk> \<Longrightarrow> wf_interp_for_formula (w', Inr P # I') \<phi>
 4. \<lbrakk>stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) (FEXISTS \<phi>); wf_interp_for_formula (w, I) (FEXISTS \<phi>); wf_interp_for_formula (w', I') (FEXISTS \<phi>); finite P; (w', Inr P # I') \<Turnstile> \<phi>\<rbrakk> \<Longrightarrow> (w', Inr P # I') \<Turnstile> \<phi>
[PROOF STEP]
from FEXISTS.prems(2,4) \<open>finite P\<close>
[PROOF STATE]
proof (chain)
picking this:
wf_formula (length I) (FEXISTS \<phi>)
wf_interp_for_formula (w', I') (FEXISTS \<phi>)
finite P
[PROOF STEP]
show "wf_interp_for_formula (w', Inr P # I') \<phi>"
[PROOF STATE]
proof (prove)
using this:
wf_formula (length I) (FEXISTS \<phi>)
wf_interp_for_formula (w', I') (FEXISTS \<phi>)
finite P

goal (1 subgoal):
 1. wf_interp_for_formula (w', Inr P # I') \<phi>
[PROOF STEP]
by (blast dest: wf_interp_for_formula_FEXISTS[of I', unfolded length])
[PROOF STATE]
proof (state)
this:
wf_interp_for_formula (w', Inr P # I') \<phi>

goal (3 subgoals):
 1. \<lbrakk>stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) (FEXISTS \<phi>); wf_interp_for_formula (w, I) (FEXISTS \<phi>); wf_interp_for_formula (w', I') (FEXISTS \<phi>); finite P; (w', Inr P # I') \<Turnstile> \<phi>\<rbrakk> \<Longrightarrow> stream_enc (w, Inr P # I) = stream_enc (w', Inr P # I')
 2. \<lbrakk>stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) (FEXISTS \<phi>); wf_interp_for_formula (w, I) (FEXISTS \<phi>); wf_interp_for_formula (w', I') (FEXISTS \<phi>); finite P; (w', Inr P # I') \<Turnstile> \<phi>\<rbrakk> \<Longrightarrow> wf_formula (length (Inr P # I)) \<phi>
 3. \<lbrakk>stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) (FEXISTS \<phi>); wf_interp_for_formula (w, I) (FEXISTS \<phi>); wf_interp_for_formula (w', I') (FEXISTS \<phi>); finite P; (w', Inr P # I') \<Turnstile> \<phi>\<rbrakk> \<Longrightarrow> (w', Inr P # I') \<Turnstile> \<phi>
[PROOF STEP]
qed (auto simp: smap2_alt split: sum.splits if_split_asm)
[PROOF STATE]
proof (state)
this:
(w, Inr P # I) \<Turnstile> \<phi>

goal (1 subgoal):
 1. (w', I') \<Turnstile> FEXISTS \<phi> \<Longrightarrow> (w, I) \<Turnstile> FEXISTS \<phi>
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
finite P
(w', Inr P # I') \<Turnstile> \<phi>
(w, Inr P # I) \<Turnstile> \<phi>
[PROOF STEP]
show "(w, I) \<Turnstile> FEXISTS \<phi>"
[PROOF STATE]
proof (prove)
using this:
finite P
(w', Inr P # I') \<Turnstile> \<phi>
(w, Inr P # I) \<Turnstile> \<phi>

goal (1 subgoal):
 1. (w, I) \<Turnstile> FEXISTS \<phi>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(w, I) \<Turnstile> FEXISTS \<phi>

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
((w, I) \<Turnstile> FEXISTS \<phi>) = ((w', I') \<Turnstile> FEXISTS \<phi>)

goal (1 subgoal):
 1. \<And>\<phi> w w' I I'. \<lbrakk>\<And>w w' I I'. \<lbrakk>stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) \<phi>; wf_interp_for_formula (w, I) \<phi>; wf_interp_for_formula (w', I') \<phi>\<rbrakk> \<Longrightarrow> ((w, I) \<Turnstile> \<phi>) = ((w', I') \<Turnstile> \<phi>); stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) (FNot \<phi>); wf_interp_for_formula (w, I) (FNot \<phi>); wf_interp_for_formula (w', I') (FNot \<phi>)\<rbrakk> \<Longrightarrow> ((w, I) \<Turnstile> FNot \<phi>) = ((w', I') \<Turnstile> FNot \<phi>)
[PROOF STEP]
qed auto