[STATEMENT]
lemma pts_symbolic_c_preserves_wf_is:
  assumes "(\<S>,\) \<Rightarrow>\<^sup>\<bullet>\<^sub>c\<^sup>* (\<S>',\')" "wf\<^sub>s\<^sub>t\<^sub>s' \<S> \" "wf\<^sub>s\<^sub>t V (to_st \)"
  shows "wf\<^sub>s\<^sub>t V (to_st \')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf\<^sub>e\<^sub>s\<^sub>t V \'
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
(\<S>, \) \<Rightarrow>\<^sup>\<bullet>\<^sub>c\<^sup>* (\<S>', \')
wf\<^sub>s\<^sub>t\<^sub>s' \<S> \
wf\<^sub>e\<^sub>s\<^sub>t V \

goal (1 subgoal):
 1. wf\<^sub>e\<^sub>s\<^sub>t V \'
[PROOF STEP]
proof (induction rule: rtranclp_induct2)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>wf\<^sub>s\<^sub>t\<^sub>s' \<S> \; wf\<^sub>e\<^sub>s\<^sub>t V \\<rbrakk> \<Longrightarrow> wf\<^sub>e\<^sub>s\<^sub>t V \
 2. \<And>a b aa ba. \<lbrakk>(\<S>, \) \<Rightarrow>\<^sup>\<bullet>\<^sub>c\<^sup>* (a, b); (a, b) \<Rightarrow>\<^sup>\<bullet>\<^sub>c (aa, ba); \<lbrakk>wf\<^sub>s\<^sub>t\<^sub>s' \<S> \; wf\<^sub>e\<^sub>s\<^sub>t V \\<rbrakk> \<Longrightarrow> wf\<^sub>e\<^sub>s\<^sub>t V b; wf\<^sub>s\<^sub>t\<^sub>s' \<S> \; wf\<^sub>e\<^sub>s\<^sub>t V \\<rbrakk> \<Longrightarrow> wf\<^sub>e\<^sub>s\<^sub>t V ba
[PROOF STEP]
case (step \<S>1 \1 \<S>2 \2)
[PROOF STATE]
proof (state)
this:
(\<S>, \) \<Rightarrow>\<^sup>\<bullet>\<^sub>c\<^sup>* (\<S>1, \1)
(\<S>1, \1) \<Rightarrow>\<^sup>\<bullet>\<^sub>c (\<S>2, \2)
\<lbrakk>wf\<^sub>s\<^sub>t\<^sub>s' \<S> \; wf\<^sub>e\<^sub>s\<^sub>t V \\<rbrakk> \<Longrightarrow> wf\<^sub>e\<^sub>s\<^sub>t V \1
wf\<^sub>s\<^sub>t\<^sub>s' \<S> \
wf\<^sub>e\<^sub>s\<^sub>t V \

goal (2 subgoals):
 1. \<lbrakk>wf\<^sub>s\<^sub>t\<^sub>s' \<S> \; wf\<^sub>e\<^sub>s\<^sub>t V \\<rbrakk> \<Longrightarrow> wf\<^sub>e\<^sub>s\<^sub>t V \
 2. \<And>a b aa ba. \<lbrakk>(\<S>, \) \<Rightarrow>\<^sup>\<bullet>\<^sub>c\<^sup>* (a, b); (a, b) \<Rightarrow>\<^sup>\<bullet>\<^sub>c (aa, ba); \<lbrakk>wf\<^sub>s\<^sub>t\<^sub>s' \<S> \; wf\<^sub>e\<^sub>s\<^sub>t V \\<rbrakk> \<Longrightarrow> wf\<^sub>e\<^sub>s\<^sub>t V b; wf\<^sub>s\<^sub>t\<^sub>s' \<S> \; wf\<^sub>e\<^sub>s\<^sub>t V \\<rbrakk> \<Longrightarrow> wf\<^sub>e\<^sub>s\<^sub>t V ba
[PROOF STEP]
hence "(\<S>, \) \<Rightarrow>\<^sup>\<bullet>\<^sub>c\<^sup>* (\<S>2, \2)"
[PROOF STATE]
proof (prove)
using this:
(\<S>, \) \<Rightarrow>\<^sup>\<bullet>\<^sub>c\<^sup>* (\<S>1, \1)
(\<S>1, \1) \<Rightarrow>\<^sup>\<bullet>\<^sub>c (\<S>2, \2)
\<lbrakk>wf\<^sub>s\<^sub>t\<^sub>s' \<S> \; wf\<^sub>e\<^sub>s\<^sub>t V \\<rbrakk> \<Longrightarrow> wf\<^sub>e\<^sub>s\<^sub>t V \1
wf\<^sub>s\<^sub>t\<^sub>s' \<S> \
wf\<^sub>e\<^sub>s\<^sub>t V \

goal (1 subgoal):
 1. (\<S>, \) \<Rightarrow>\<^sup>\<bullet>\<^sub>c\<^sup>* (\<S>2, \2)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<S>, \) \<Rightarrow>\<^sup>\<bullet>\<^sub>c\<^sup>* (\<S>2, \2)

goal (2 subgoals):
 1. \<lbrakk>wf\<^sub>s\<^sub>t\<^sub>s' \<S> \; wf\<^sub>e\<^sub>s\<^sub>t V \\<rbrakk> \<Longrightarrow> wf\<^sub>e\<^sub>s\<^sub>t V \
 2. \<And>a b aa ba. \<lbrakk>(\<S>, \) \<Rightarrow>\<^sup>\<bullet>\<^sub>c\<^sup>* (a, b); (a, b) \<Rightarrow>\<^sup>\<bullet>\<^sub>c (aa, ba); \<lbrakk>wf\<^sub>s\<^sub>t\<^sub>s' \<S> \; wf\<^sub>e\<^sub>s\<^sub>t V \\<rbrakk> \<Longrightarrow> wf\<^sub>e\<^sub>s\<^sub>t V b; wf\<^sub>s\<^sub>t\<^sub>s' \<S> \; wf\<^sub>e\<^sub>s\<^sub>t V \\<rbrakk> \<Longrightarrow> wf\<^sub>e\<^sub>s\<^sub>t V ba
[PROOF STEP]
hence *: "wf\<^sub>s\<^sub>t\<^sub>s' \<S>1 \1" "wf\<^sub>s\<^sub>t\<^sub>s' \<S>2 \2"
[PROOF STATE]
proof (prove)
using this:
(\<S>, \) \<Rightarrow>\<^sup>\<bullet>\<^sub>c\<^sup>* (\<S>2, \2)

goal (1 subgoal):
 1. wf\<^sub>s\<^sub>t\<^sub>s' \<S>1 \1 &&& wf\<^sub>s\<^sub>t\<^sub>s' \<S>2 \2
[PROOF STEP]
using pts_symbolic_c_preserves_wf_prot[OF _ step.prems(1)] step.hyps(1)
[PROOF STATE]
proof (prove)
using this:
(\<S>, \) \<Rightarrow>\<^sup>\<bullet>\<^sub>c\<^sup>* (\<S>2, \2)
(\<S>, \) \<Rightarrow>\<^sup>\<bullet>\<^sub>c\<^sup>* (?\<S>', ?\') \<Longrightarrow> wf\<^sub>s\<^sub>t\<^sub>s' ?\<S>' ?\'
(\<S>, \) \<Rightarrow>\<^sup>\<bullet>\<^sub>c\<^sup>* (\<S>1, \1)

goal (1 subgoal):
 1. wf\<^sub>s\<^sub>t\<^sub>s' \<S>1 \1 &&& wf\<^sub>s\<^sub>t\<^sub>s' \<S>2 \2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
wf\<^sub>s\<^sub>t\<^sub>s' \<S>1 \1
wf\<^sub>s\<^sub>t\<^sub>s' \<S>2 \2

goal (2 subgoals):
 1. \<lbrakk>wf\<^sub>s\<^sub>t\<^sub>s' \<S> \; wf\<^sub>e\<^sub>s\<^sub>t V \\<rbrakk> \<Longrightarrow> wf\<^sub>e\<^sub>s\<^sub>t V \
 2. \<And>a b aa ba. \<lbrakk>(\<S>, \) \<Rightarrow>\<^sup>\<bullet>\<^sub>c\<^sup>* (a, b); (a, b) \<Rightarrow>\<^sup>\<bullet>\<^sub>c (aa, ba); \<lbrakk>wf\<^sub>s\<^sub>t\<^sub>s' \<S> \; wf\<^sub>e\<^sub>s\<^sub>t V \\<rbrakk> \<Longrightarrow> wf\<^sub>e\<^sub>s\<^sub>t V b; wf\<^sub>s\<^sub>t\<^sub>s' \<S> \; wf\<^sub>e\<^sub>s\<^sub>t V \\<rbrakk> \<Longrightarrow> wf\<^sub>e\<^sub>s\<^sub>t V ba
[PROOF STEP]
from step.hyps(2) step.IH[OF step.prems]
[PROOF STATE]
proof (chain)
picking this:
(\<S>1, \1) \<Rightarrow>\<^sup>\<bullet>\<^sub>c (\<S>2, \2)
wf\<^sub>e\<^sub>s\<^sub>t V \1
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
(\<S>1, \1) \<Rightarrow>\<^sup>\<bullet>\<^sub>c (\<S>2, \2)
wf\<^sub>e\<^sub>s\<^sub>t V \1

goal (1 subgoal):
 1. wf\<^sub>e\<^sub>s\<^sub>t V \2
[PROOF STEP]
proof (induction rule: pts_symbolic_c_induct)
[PROOF STATE]
proof (state)
goal (6 subgoals):
 1. \<lbrakk>[] \<in> \<S>1; \<S>2 = update\<^sub>s\<^sub>t \<S>1 []; \2 = \1; wf\<^sub>e\<^sub>s\<^sub>t V \1\<rbrakk> \<Longrightarrow> wf\<^sub>e\<^sub>s\<^sub>t V \2
 2. \<And>t S. \<lbrakk>send\<langle>t\<rangle>\<^sub>s\<^sub>t # S \<in> \<S>1; \<S>2 = update\<^sub>s\<^sub>t \<S>1 (send\<langle>t\<rangle>\<^sub>s\<^sub>t # S); \2 = \1 @ [Step (receive\<langle>t\<rangle>\<^sub>s\<^sub>t)]; wf\<^sub>e\<^sub>s\<^sub>t V \1\<rbrakk> \<Longrightarrow> wf\<^sub>e\<^sub>s\<^sub>t V \2
 3. \<And>t S. \<lbrakk>receive\<langle>t\<rangle>\<^sub>s\<^sub>t # S \<in> \<S>1; \<S>2 = update\<^sub>s\<^sub>t \<S>1 (receive\<langle>t\<rangle>\<^sub>s\<^sub>t # S); \2 = \1 @ [Step (send\<langle>t\<rangle>\<^sub>s\<^sub>t)]; wf\<^sub>e\<^sub>s\<^sub>t V \1\<rbrakk> \<Longrightarrow> wf\<^sub>e\<^sub>s\<^sub>t V \2
 4. \<And>a t t' S. \<lbrakk>\<langle>a: t \<doteq> t'\<rangle>\<^sub>s\<^sub>t # S \<in> \<S>1; \<S>2 = update\<^sub>s\<^sub>t \<S>1 (\<langle>a: t \<doteq> t'\<rangle>\<^sub>s\<^sub>t # S); \2 = \1 @ [Step \<langle>a: t \<doteq> t'\<rangle>\<^sub>s\<^sub>t]; wf\<^sub>e\<^sub>s\<^sub>t V \1\<rbrakk> \<Longrightarrow> wf\<^sub>e\<^sub>s\<^sub>t V \2
 5. \<And>X F S. \<lbrakk>\<forall>X\<langle>\<or>\<noteq>: F\<rangle>\<^sub>s\<^sub>t # S \<in> \<S>1; \<S>2 = update\<^sub>s\<^sub>t \<S>1 (\<forall>X\<langle>\<or>\<noteq>: F\<rangle>\<^sub>s\<^sub>t # S); \2 = \1 @ [Step \<forall>X\<langle>\<or>\<noteq>: F\<rangle>\<^sub>s\<^sub>t]; wf\<^sub>e\<^sub>s\<^sub>t V \1\<rbrakk> \<Longrightarrow> wf\<^sub>e\<^sub>s\<^sub>t V \2
 6. \<And>f T. \<lbrakk>Fun f T \<sqsubseteq>\<^sub>s\<^sub>e\<^sub>t ik\<^sub>e\<^sub>s\<^sub>t \1 \<union> assignment_rhs\<^sub>e\<^sub>s\<^sub>t \1; \<S>2 = \<S>1; \2 = \1 @ [Decomp (Fun f T)]; wf\<^sub>e\<^sub>s\<^sub>t V \1\<rbrakk> \<Longrightarrow> wf\<^sub>e\<^sub>s\<^sub>t V \2
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
[] \<in> \<S>1
\<S>2 = update\<^sub>s\<^sub>t \<S>1 []
\2 = \1
wf\<^sub>e\<^sub>s\<^sub>t V \1

goal (6 subgoals):
 1. \<lbrakk>[] \<in> \<S>1; \<S>2 = update\<^sub>s\<^sub>t \<S>1 []; \2 = \1; wf\<^sub>e\<^sub>s\<^sub>t V \1\<rbrakk> \<Longrightarrow> wf\<^sub>e\<^sub>s\<^sub>t V \2
 2. \<And>t S. \<lbrakk>send\<langle>t\<rangle>\<^sub>s\<^sub>t # S \<in> \<S>1; \<S>2 = update\<^sub>s\<^sub>t \<S>1 (send\<langle>t\<rangle>\<^sub>s\<^sub>t # S); \2 = \1 @ [Step (receive\<langle>t\<rangle>\<^sub>s\<^sub>t)]; wf\<^sub>e\<^sub>s\<^sub>t V \1\<rbrakk> \<Longrightarrow> wf\<^sub>e\<^sub>s\<^sub>t V \2
 3. \<And>t S. \<lbrakk>receive\<langle>t\<rangle>\<^sub>s\<^sub>t # S \<in> \<S>1; \<S>2 = update\<^sub>s\<^sub>t \<S>1 (receive\<langle>t\<rangle>\<^sub>s\<^sub>t # S); \2 = \1 @ [Step (send\<langle>t\<rangle>\<^sub>s\<^sub>t)]; wf\<^sub>e\<^sub>s\<^sub>t V \1\<rbrakk> \<Longrightarrow> wf\<^sub>e\<^sub>s\<^sub>t V \2
 4. \<And>a t t' S. \<lbrakk>\<langle>a: t \<doteq> t'\<rangle>\<^sub>s\<^sub>t # S \<in> \<S>1; \<S>2 = update\<^sub>s\<^sub>t \<S>1 (\<langle>a: t \<doteq> t'\<rangle>\<^sub>s\<^sub>t # S); \2 = \1 @ [Step \<langle>a: t \<doteq> t'\<rangle>\<^sub>s\<^sub>t]; wf\<^sub>e\<^sub>s\<^sub>t V \1\<rbrakk> \<Longrightarrow> wf\<^sub>e\<^sub>s\<^sub>t V \2
 5. \<And>X F S. \<lbrakk>\<forall>X\<langle>\<or>\<noteq>: F\<rangle>\<^sub>s\<^sub>t # S \<in> \<S>1; \<S>2 = update\<^sub>s\<^sub>t \<S>1 (\<forall>X\<langle>\<or>\<noteq>: F\<rangle>\<^sub>s\<^sub>t # S); \2 = \1 @ [Step \<forall>X\<langle>\<or>\<noteq>: F\<rangle>\<^sub>s\<^sub>t]; wf\<^sub>e\<^sub>s\<^sub>t V \1\<rbrakk> \<Longrightarrow> wf\<^sub>e\<^sub>s\<^sub>t V \2
 6. \<And>f T. \<lbrakk>Fun f T \<sqsubseteq>\<^sub>s\<^sub>e\<^sub>t ik\<^sub>e\<^sub>s\<^sub>t \1 \<union> assignment_rhs\<^sub>e\<^sub>s\<^sub>t \1; \<S>2 = \<S>1; \2 = \1 @ [Decomp (Fun f T)]; wf\<^sub>e\<^sub>s\<^sub>t V \1\<rbrakk> \<Longrightarrow> wf\<^sub>e\<^sub>s\<^sub>t V \2
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
[] \<in> \<S>1
\<S>2 = update\<^sub>s\<^sub>t \<S>1 []
\2 = \1
wf\<^sub>e\<^sub>s\<^sub>t V \1

goal (1 subgoal):
 1. wf\<^sub>e\<^sub>s\<^sub>t V \2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
wf\<^sub>e\<^sub>s\<^sub>t V \2

goal (5 subgoals):
 1. \<And>t S. \<lbrakk>send\<langle>t\<rangle>\<^sub>s\<^sub>t # S \<in> \<S>1; \<S>2 = update\<^sub>s\<^sub>t \<S>1 (send\<langle>t\<rangle>\<^sub>s\<^sub>t # S); \2 = \1 @ [Step (receive\<langle>t\<rangle>\<^sub>s\<^sub>t)]; wf\<^sub>e\<^sub>s\<^sub>t V \1\<rbrakk> \<Longrightarrow> wf\<^sub>e\<^sub>s\<^sub>t V \2
 2. \<And>t S. \<lbrakk>receive\<langle>t\<rangle>\<^sub>s\<^sub>t # S \<in> \<S>1; \<S>2 = update\<^sub>s\<^sub>t \<S>1 (receive\<langle>t\<rangle>\<^sub>s\<^sub>t # S); \2 = \1 @ [Step (send\<langle>t\<rangle>\<^sub>s\<^sub>t)]; wf\<^sub>e\<^sub>s\<^sub>t V \1\<rbrakk> \<Longrightarrow> wf\<^sub>e\<^sub>s\<^sub>t V \2
 3. \<And>a t t' S. \<lbrakk>\<langle>a: t \<doteq> t'\<rangle>\<^sub>s\<^sub>t # S \<in> \<S>1; \<S>2 = update\<^sub>s\<^sub>t \<S>1 (\<langle>a: t \<doteq> t'\<rangle>\<^sub>s\<^sub>t # S); \2 = \1 @ [Step \<langle>a: t \<doteq> t'\<rangle>\<^sub>s\<^sub>t]; wf\<^sub>e\<^sub>s\<^sub>t V \1\<rbrakk> \<Longrightarrow> wf\<^sub>e\<^sub>s\<^sub>t V \2
 4. \<And>X F S. \<lbrakk>\<forall>X\<langle>\<or>\<noteq>: F\<rangle>\<^sub>s\<^sub>t # S \<in> \<S>1; \<S>2 = update\<^sub>s\<^sub>t \<S>1 (\<forall>X\<langle>\<or>\<noteq>: F\<rangle>\<^sub>s\<^sub>t # S); \2 = \1 @ [Step \<forall>X\<langle>\<or>\<noteq>: F\<rangle>\<^sub>s\<^sub>t]; wf\<^sub>e\<^sub>s\<^sub>t V \1\<rbrakk> \<Longrightarrow> wf\<^sub>e\<^sub>s\<^sub>t V \2
 5. \<And>f T. \<lbrakk>Fun f T \<sqsubseteq>\<^sub>s\<^sub>e\<^sub>t ik\<^sub>e\<^sub>s\<^sub>t \1 \<union> assignment_rhs\<^sub>e\<^sub>s\<^sub>t \1; \<S>2 = \<S>1; \2 = \1 @ [Decomp (Fun f T)]; wf\<^sub>e\<^sub>s\<^sub>t V \1\<rbrakk> \<Longrightarrow> wf\<^sub>e\<^sub>s\<^sub>t V \2
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>t S. \<lbrakk>send\<langle>t\<rangle>\<^sub>s\<^sub>t # S \<in> \<S>1; \<S>2 = update\<^sub>s\<^sub>t \<S>1 (send\<langle>t\<rangle>\<^sub>s\<^sub>t # S); \2 = \1 @ [Step (receive\<langle>t\<rangle>\<^sub>s\<^sub>t)]; wf\<^sub>e\<^sub>s\<^sub>t V \1\<rbrakk> \<Longrightarrow> wf\<^sub>e\<^sub>s\<^sub>t V \2
 2. \<And>t S. \<lbrakk>receive\<langle>t\<rangle>\<^sub>s\<^sub>t # S \<in> \<S>1; \<S>2 = update\<^sub>s\<^sub>t \<S>1 (receive\<langle>t\<rangle>\<^sub>s\<^sub>t # S); \2 = \1 @ [Step (send\<langle>t\<rangle>\<^sub>s\<^sub>t)]; wf\<^sub>e\<^sub>s\<^sub>t V \1\<rbrakk> \<Longrightarrow> wf\<^sub>e\<^sub>s\<^sub>t V \2
 3. \<And>a t t' S. \<lbrakk>\<langle>a: t \<doteq> t'\<rangle>\<^sub>s\<^sub>t # S \<in> \<S>1; \<S>2 = update\<^sub>s\<^sub>t \<S>1 (\<langle>a: t \<doteq> t'\<rangle>\<^sub>s\<^sub>t # S); \2 = \1 @ [Step \<langle>a: t \<doteq> t'\<rangle>\<^sub>s\<^sub>t]; wf\<^sub>e\<^sub>s\<^sub>t V \1\<rbrakk> \<Longrightarrow> wf\<^sub>e\<^sub>s\<^sub>t V \2
 4. \<And>X F S. \<lbrakk>\<forall>X\<langle>\<or>\<noteq>: F\<rangle>\<^sub>s\<^sub>t # S \<in> \<S>1; \<S>2 = update\<^sub>s\<^sub>t \<S>1 (\<forall>X\<langle>\<or>\<noteq>: F\<rangle>\<^sub>s\<^sub>t # S); \2 = \1 @ [Step \<forall>X\<langle>\<or>\<noteq>: F\<rangle>\<^sub>s\<^sub>t]; wf\<^sub>e\<^sub>s\<^sub>t V \1\<rbrakk> \<Longrightarrow> wf\<^sub>e\<^sub>s\<^sub>t V \2
 5. \<And>f T. \<lbrakk>Fun f T \<sqsubseteq>\<^sub>s\<^sub>e\<^sub>t ik\<^sub>e\<^sub>s\<^sub>t \1 \<union> assignment_rhs\<^sub>e\<^sub>s\<^sub>t \1; \<S>2 = \<S>1; \2 = \1 @ [Decomp (Fun f T)]; wf\<^sub>e\<^sub>s\<^sub>t V \1\<rbrakk> \<Longrightarrow> wf\<^sub>e\<^sub>s\<^sub>t V \2
[PROOF STEP]
case (Send ts S)
[PROOF STATE]
proof (state)
this:
send\<langle>ts\<rangle>\<^sub>s\<^sub>t # S \<in> \<S>1
\<S>2 = update\<^sub>s\<^sub>t \<S>1 (send\<langle>ts\<rangle>\<^sub>s\<^sub>t # S)
\2 = \1 @ [Step (receive\<langle>ts\<rangle>\<^sub>s\<^sub>t)]
wf\<^sub>e\<^sub>s\<^sub>t V \1

goal (5 subgoals):
 1. \<And>t S. \<lbrakk>send\<langle>t\<rangle>\<^sub>s\<^sub>t # S \<in> \<S>1; \<S>2 = update\<^sub>s\<^sub>t \<S>1 (send\<langle>t\<rangle>\<^sub>s\<^sub>t # S); \2 = \1 @ [Step (receive\<langle>t\<rangle>\<^sub>s\<^sub>t)]; wf\<^sub>e\<^sub>s\<^sub>t V \1\<rbrakk> \<Longrightarrow> wf\<^sub>e\<^sub>s\<^sub>t V \2
 2. \<And>t S. \<lbrakk>receive\<langle>t\<rangle>\<^sub>s\<^sub>t # S \<in> \<S>1; \<S>2 = update\<^sub>s\<^sub>t \<S>1 (receive\<langle>t\<rangle>\<^sub>s\<^sub>t # S); \2 = \1 @ [Step (send\<langle>t\<rangle>\<^sub>s\<^sub>t)]; wf\<^sub>e\<^sub>s\<^sub>t V \1\<rbrakk> \<Longrightarrow> wf\<^sub>e\<^sub>s\<^sub>t V \2
 3. \<And>a t t' S. \<lbrakk>\<langle>a: t \<doteq> t'\<rangle>\<^sub>s\<^sub>t # S \<in> \<S>1; \<S>2 = update\<^sub>s\<^sub>t \<S>1 (\<langle>a: t \<doteq> t'\<rangle>\<^sub>s\<^sub>t # S); \2 = \1 @ [Step \<langle>a: t \<doteq> t'\<rangle>\<^sub>s\<^sub>t]; wf\<^sub>e\<^sub>s\<^sub>t V \1\<rbrakk> \<Longrightarrow> wf\<^sub>e\<^sub>s\<^sub>t V \2
 4. \<And>X F S. \<lbrakk>\<forall>X\<langle>\<or>\<noteq>: F\<rangle>\<^sub>s\<^sub>t # S \<in> \<S>1; \<S>2 = update\<^sub>s\<^sub>t \<S>1 (\<forall>X\<langle>\<or>\<noteq>: F\<rangle>\<^sub>s\<^sub>t # S); \2 = \1 @ [Step \<forall>X\<langle>\<or>\<noteq>: F\<rangle>\<^sub>s\<^sub>t]; wf\<^sub>e\<^sub>s\<^sub>t V \1\<rbrakk> \<Longrightarrow> wf\<^sub>e\<^sub>s\<^sub>t V \2
 5. \<And>f T. \<lbrakk>Fun f T \<sqsubseteq>\<^sub>s\<^sub>e\<^sub>t ik\<^sub>e\<^sub>s\<^sub>t \1 \<union> assignment_rhs\<^sub>e\<^sub>s\<^sub>t \1; \<S>2 = \<S>1; \2 = \1 @ [Decomp (Fun f T)]; wf\<^sub>e\<^sub>s\<^sub>t V \1\<rbrakk> \<Longrightarrow> wf\<^sub>e\<^sub>s\<^sub>t V \2
[PROOF STEP]
hence "wf\<^sub>s\<^sub>t (wfrestrictedvars\<^sub>e\<^sub>s\<^sub>t \1) (receive\<langle>ts\<rangle>\<^sub>s\<^sub>t#(dual\<^sub>s\<^sub>t S))"
[PROOF STATE]
proof (prove)
using this:
send\<langle>ts\<rangle>\<^sub>s\<^sub>t # S \<in> \<S>1
\<S>2 = update\<^sub>s\<^sub>t \<S>1 (send\<langle>ts\<rangle>\<^sub>s\<^sub>t # S)
\2 = \1 @ [Step (receive\<langle>ts\<rangle>\<^sub>s\<^sub>t)]
wf\<^sub>e\<^sub>s\<^sub>t V \1

goal (1 subgoal):
 1. wf\<^sub>s\<^sub>t (wfrestrictedvars\<^sub>e\<^sub>s\<^sub>t \1) (receive\<langle>ts\<rangle>\<^sub>s\<^sub>t # dual\<^sub>s\<^sub>t S)
[PROOF STEP]
using *(1)
[PROOF STATE]
proof (prove)
using this:
send\<langle>ts\<rangle>\<^sub>s\<^sub>t # S \<in> \<S>1
\<S>2 = update\<^sub>s\<^sub>t \<S>1 (send\<langle>ts\<rangle>\<^sub>s\<^sub>t # S)
\2 = \1 @ [Step (receive\<langle>ts\<rangle>\<^sub>s\<^sub>t)]
wf\<^sub>e\<^sub>s\<^sub>t V \1
wf\<^sub>s\<^sub>t\<^sub>s' \<S>1 \1

goal (1 subgoal):
 1. wf\<^sub>s\<^sub>t (wfrestrictedvars\<^sub>e\<^sub>s\<^sub>t \1) (receive\<langle>ts\<rangle>\<^sub>s\<^sub>t # dual\<^sub>s\<^sub>t S)
[PROOF STEP]
unfolding wf\<^sub>s\<^sub>t\<^sub>s'_def
[PROOF STATE]
proof (prove)
using this:
send\<langle>ts\<rangle>\<^sub>s\<^sub>t # S \<in> \<S>1
\<S>2 = update\<^sub>s\<^sub>t \<S>1 (send\<langle>ts\<rangle>\<^sub>s\<^sub>t # S)
\2 = \1 @ [Step (receive\<langle>ts\<rangle>\<^sub>s\<^sub>t)]
wf\<^sub>e\<^sub>s\<^sub>t V \1
(\<forall>S\<in>\<S>1. wf\<^sub>s\<^sub>t (wfrestrictedvars\<^sub>e\<^sub>s\<^sub>t \1) (dual\<^sub>s\<^sub>t S)) \<and> (\<forall>S\<in>\<S>1. \<forall>S'\<in>\<S>1. fv\<^sub>s\<^sub>t S \<inter> bvars\<^sub>s\<^sub>t S' = {}) \<and> (\<forall>S\<in>\<S>1. fv\<^sub>s\<^sub>t S \<inter> bvars\<^sub>e\<^sub>s\<^sub>t \1 = {}) \<and> (\<forall>S\<in>\<S>1. fv\<^sub>e\<^sub>s\<^sub>t \1 \<inter> bvars\<^sub>s\<^sub>t S = {})

goal (1 subgoal):
 1. wf\<^sub>s\<^sub>t (wfrestrictedvars\<^sub>e\<^sub>s\<^sub>t \1) (receive\<langle>ts\<rangle>\<^sub>s\<^sub>t # dual\<^sub>s\<^sub>t S)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
wf\<^sub>s\<^sub>t (wfrestrictedvars\<^sub>e\<^sub>s\<^sub>t \1) (receive\<langle>ts\<rangle>\<^sub>s\<^sub>t # dual\<^sub>s\<^sub>t S)

goal (5 subgoals):
 1. \<And>t S. \<lbrakk>send\<langle>t\<rangle>\<^sub>s\<^sub>t # S \<in> \<S>1; \<S>2 = update\<^sub>s\<^sub>t \<S>1 (send\<langle>t\<rangle>\<^sub>s\<^sub>t # S); \2 = \1 @ [Step (receive\<langle>t\<rangle>\<^sub>s\<^sub>t)]; wf\<^sub>e\<^sub>s\<^sub>t V \1\<rbrakk> \<Longrightarrow> wf\<^sub>e\<^sub>s\<^sub>t V \2
 2. \<And>t S. \<lbrakk>receive\<langle>t\<rangle>\<^sub>s\<^sub>t # S \<in> \<S>1; \<S>2 = update\<^sub>s\<^sub>t \<S>1 (receive\<langle>t\<rangle>\<^sub>s\<^sub>t # S); \2 = \1 @ [Step (send\<langle>t\<rangle>\<^sub>s\<^sub>t)]; wf\<^sub>e\<^sub>s\<^sub>t V \1\<rbrakk> \<Longrightarrow> wf\<^sub>e\<^sub>s\<^sub>t V \2
 3. \<And>a t t' S. \<lbrakk>\<langle>a: t \<doteq> t'\<rangle>\<^sub>s\<^sub>t # S \<in> \<S>1; \<S>2 = update\<^sub>s\<^sub>t \<S>1 (\<langle>a: t \<doteq> t'\<rangle>\<^sub>s\<^sub>t # S); \2 = \1 @ [Step \<langle>a: t \<doteq> t'\<rangle>\<^sub>s\<^sub>t]; wf\<^sub>e\<^sub>s\<^sub>t V \1\<rbrakk> \<Longrightarrow> wf\<^sub>e\<^sub>s\<^sub>t V \2
 4. \<And>X F S. \<lbrakk>\<forall>X\<langle>\<or>\<noteq>: F\<rangle>\<^sub>s\<^sub>t # S \<in> \<S>1; \<S>2 = update\<^sub>s\<^sub>t \<S>1 (\<forall>X\<langle>\<or>\<noteq>: F\<rangle>\<^sub>s\<^sub>t # S); \2 = \1 @ [Step \<forall>X\<langle>\<or>\<noteq>: F\<rangle>\<^sub>s\<^sub>t]; wf\<^sub>e\<^sub>s\<^sub>t V \1\<rbrakk> \<Longrightarrow> wf\<^sub>e\<^sub>s\<^sub>t V \2
 5. \<And>f T. \<lbrakk>Fun f T \<sqsubseteq>\<^sub>s\<^sub>e\<^sub>t ik\<^sub>e\<^sub>s\<^sub>t \1 \<union> assignment_rhs\<^sub>e\<^sub>s\<^sub>t \1; \<S>2 = \<S>1; \2 = \1 @ [Decomp (Fun f T)]; wf\<^sub>e\<^sub>s\<^sub>t V \1\<rbrakk> \<Longrightarrow> wf\<^sub>e\<^sub>s\<^sub>t V \2
[PROOF STEP]
hence "fv\<^sub>s\<^sub>e\<^sub>t (set ts) \<subseteq> wfrestrictedvars\<^sub>s\<^sub>t (to_st \1) \<union> V"
[PROOF STATE]
proof (prove)
using this:
wf\<^sub>s\<^sub>t (wfrestrictedvars\<^sub>e\<^sub>s\<^sub>t \1) (receive\<langle>ts\<rangle>\<^sub>s\<^sub>t # dual\<^sub>s\<^sub>t S)

goal (1 subgoal):
 1. fv\<^sub>s\<^sub>e\<^sub>t (set ts) \<subseteq> wfrestrictedvars\<^sub>e\<^sub>s\<^sub>t \1 \<union> V
[PROOF STEP]
using wfrestrictedvars\<^sub>e\<^sub>s\<^sub>t_eq_wfrestrictedvars\<^sub>s\<^sub>t
[PROOF STATE]
proof (prove)
using this:
wf\<^sub>s\<^sub>t (wfrestrictedvars\<^sub>e\<^sub>s\<^sub>t \1) (receive\<langle>ts\<rangle>\<^sub>s\<^sub>t # dual\<^sub>s\<^sub>t S)
wfrestrictedvars\<^sub>e\<^sub>s\<^sub>t ?A = wfrestrictedvars\<^sub>e\<^sub>s\<^sub>t ?A

goal (1 subgoal):
 1. fv\<^sub>s\<^sub>e\<^sub>t (set ts) \<subseteq> wfrestrictedvars\<^sub>e\<^sub>s\<^sub>t \1 \<union> V
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
fv\<^sub>s\<^sub>e\<^sub>t (set ts) \<subseteq> wfrestrictedvars\<^sub>e\<^sub>s\<^sub>t \1 \<union> V

goal (5 subgoals):
 1. \<And>t S. \<lbrakk>send\<langle>t\<rangle>\<^sub>s\<^sub>t # S \<in> \<S>1; \<S>2 = update\<^sub>s\<^sub>t \<S>1 (send\<langle>t\<rangle>\<^sub>s\<^sub>t # S); \2 = \1 @ [Step (receive\<langle>t\<rangle>\<^sub>s\<^sub>t)]; wf\<^sub>e\<^sub>s\<^sub>t V \1\<rbrakk> \<Longrightarrow> wf\<^sub>e\<^sub>s\<^sub>t V \2
 2. \<And>t S. \<lbrakk>receive\<langle>t\<rangle>\<^sub>s\<^sub>t # S \<in> \<S>1; \<S>2 = update\<^sub>s\<^sub>t \<S>1 (receive\<langle>t\<rangle>\<^sub>s\<^sub>t # S); \2 = \1 @ [Step (send\<langle>t\<rangle>\<^sub>s\<^sub>t)]; wf\<^sub>e\<^sub>s\<^sub>t V \1\<rbrakk> \<Longrightarrow> wf\<^sub>e\<^sub>s\<^sub>t V \2
 3. \<And>a t t' S. \<lbrakk>\<langle>a: t \<doteq> t'\<rangle>\<^sub>s\<^sub>t # S \<in> \<S>1; \<S>2 = update\<^sub>s\<^sub>t \<S>1 (\<langle>a: t \<doteq> t'\<rangle>\<^sub>s\<^sub>t # S); \2 = \1 @ [Step \<langle>a: t \<doteq> t'\<rangle>\<^sub>s\<^sub>t]; wf\<^sub>e\<^sub>s\<^sub>t V \1\<rbrakk> \<Longrightarrow> wf\<^sub>e\<^sub>s\<^sub>t V \2
 4. \<And>X F S. \<lbrakk>\<forall>X\<langle>\<or>\<noteq>: F\<rangle>\<^sub>s\<^sub>t # S \<in> \<S>1; \<S>2 = update\<^sub>s\<^sub>t \<S>1 (\<forall>X\<langle>\<or>\<noteq>: F\<rangle>\<^sub>s\<^sub>t # S); \2 = \1 @ [Step \<forall>X\<langle>\<or>\<noteq>: F\<rangle>\<^sub>s\<^sub>t]; wf\<^sub>e\<^sub>s\<^sub>t V \1\<rbrakk> \<Longrightarrow> wf\<^sub>e\<^sub>s\<^sub>t V \2
 5. \<And>f T. \<lbrakk>Fun f T \<sqsubseteq>\<^sub>s\<^sub>e\<^sub>t ik\<^sub>e\<^sub>s\<^sub>t \1 \<union> assignment_rhs\<^sub>e\<^sub>s\<^sub>t \1; \<S>2 = \<S>1; \2 = \1 @ [Decomp (Fun f T)]; wf\<^sub>e\<^sub>s\<^sub>t V \1\<rbrakk> \<Longrightarrow> wf\<^sub>e\<^sub>s\<^sub>t V \2
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
fv\<^sub>s\<^sub>e\<^sub>t (set ts) \<subseteq> wfrestrictedvars\<^sub>e\<^sub>s\<^sub>t \1 \<union> V

goal (1 subgoal):
 1. wf\<^sub>e\<^sub>s\<^sub>t V \2
[PROOF STEP]
using Send wf_rcv_append''' to_st_append
[PROOF STATE]
proof (prove)
using this:
fv\<^sub>s\<^sub>e\<^sub>t (set ts) \<subseteq> wfrestrictedvars\<^sub>e\<^sub>s\<^sub>t \1 \<union> V
send\<langle>ts\<rangle>\<^sub>s\<^sub>t # S \<in> \<S>1
\<S>2 = update\<^sub>s\<^sub>t \<S>1 (send\<langle>ts\<rangle>\<^sub>s\<^sub>t # S)
\2 = \1 @ [Step (receive\<langle>ts\<rangle>\<^sub>s\<^sub>t)]
wf\<^sub>e\<^sub>s\<^sub>t V \1
\<lbrakk>wf\<^sub>s\<^sub>t ?V ?S; fv\<^sub>s\<^sub>e\<^sub>t (set ?ts) \<subseteq> wfrestrictedvars\<^sub>s\<^sub>t ?S \<union> ?V\<rbrakk> \<Longrightarrow> wf\<^sub>s\<^sub>t ?V (?S @ [receive\<langle>?ts\<rangle>\<^sub>s\<^sub>t])
to_st (?A @ ?B) = to_st ?A @ to_st ?B

goal (1 subgoal):
 1. wf\<^sub>e\<^sub>s\<^sub>t V \2
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
wf\<^sub>e\<^sub>s\<^sub>t V \2

goal (4 subgoals):
 1. \<And>t S. \<lbrakk>receive\<langle>t\<rangle>\<^sub>s\<^sub>t # S \<in> \<S>1; \<S>2 = update\<^sub>s\<^sub>t \<S>1 (receive\<langle>t\<rangle>\<^sub>s\<^sub>t # S); \2 = \1 @ [Step (send\<langle>t\<rangle>\<^sub>s\<^sub>t)]; wf\<^sub>e\<^sub>s\<^sub>t V \1\<rbrakk> \<Longrightarrow> wf\<^sub>e\<^sub>s\<^sub>t V \2
 2. \<And>a t t' S. \<lbrakk>\<langle>a: t \<doteq> t'\<rangle>\<^sub>s\<^sub>t # S \<in> \<S>1; \<S>2 = update\<^sub>s\<^sub>t \<S>1 (\<langle>a: t \<doteq> t'\<rangle>\<^sub>s\<^sub>t # S); \2 = \1 @ [Step \<langle>a: t \<doteq> t'\<rangle>\<^sub>s\<^sub>t]; wf\<^sub>e\<^sub>s\<^sub>t V \1\<rbrakk> \<Longrightarrow> wf\<^sub>e\<^sub>s\<^sub>t V \2
 3. \<And>X F S. \<lbrakk>\<forall>X\<langle>\<or>\<noteq>: F\<rangle>\<^sub>s\<^sub>t # S \<in> \<S>1; \<S>2 = update\<^sub>s\<^sub>t \<S>1 (\<forall>X\<langle>\<or>\<noteq>: F\<rangle>\<^sub>s\<^sub>t # S); \2 = \1 @ [Step \<forall>X\<langle>\<or>\<noteq>: F\<rangle>\<^sub>s\<^sub>t]; wf\<^sub>e\<^sub>s\<^sub>t V \1\<rbrakk> \<Longrightarrow> wf\<^sub>e\<^sub>s\<^sub>t V \2
 4. \<And>f T. \<lbrakk>Fun f T \<sqsubseteq>\<^sub>s\<^sub>e\<^sub>t ik\<^sub>e\<^sub>s\<^sub>t \1 \<union> assignment_rhs\<^sub>e\<^sub>s\<^sub>t \1; \<S>2 = \<S>1; \2 = \1 @ [Decomp (Fun f T)]; wf\<^sub>e\<^sub>s\<^sub>t V \1\<rbrakk> \<Longrightarrow> wf\<^sub>e\<^sub>s\<^sub>t V \2
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>t S. \<lbrakk>receive\<langle>t\<rangle>\<^sub>s\<^sub>t # S \<in> \<S>1; \<S>2 = update\<^sub>s\<^sub>t \<S>1 (receive\<langle>t\<rangle>\<^sub>s\<^sub>t # S); \2 = \1 @ [Step (send\<langle>t\<rangle>\<^sub>s\<^sub>t)]; wf\<^sub>e\<^sub>s\<^sub>t V \1\<rbrakk> \<Longrightarrow> wf\<^sub>e\<^sub>s\<^sub>t V \2
 2. \<And>a t t' S. \<lbrakk>\<langle>a: t \<doteq> t'\<rangle>\<^sub>s\<^sub>t # S \<in> \<S>1; \<S>2 = update\<^sub>s\<^sub>t \<S>1 (\<langle>a: t \<doteq> t'\<rangle>\<^sub>s\<^sub>t # S); \2 = \1 @ [Step \<langle>a: t \<doteq> t'\<rangle>\<^sub>s\<^sub>t]; wf\<^sub>e\<^sub>s\<^sub>t V \1\<rbrakk> \<Longrightarrow> wf\<^sub>e\<^sub>s\<^sub>t V \2
 3. \<And>X F S. \<lbrakk>\<forall>X\<langle>\<or>\<noteq>: F\<rangle>\<^sub>s\<^sub>t # S \<in> \<S>1; \<S>2 = update\<^sub>s\<^sub>t \<S>1 (\<forall>X\<langle>\<or>\<noteq>: F\<rangle>\<^sub>s\<^sub>t # S); \2 = \1 @ [Step \<forall>X\<langle>\<or>\<noteq>: F\<rangle>\<^sub>s\<^sub>t]; wf\<^sub>e\<^sub>s\<^sub>t V \1\<rbrakk> \<Longrightarrow> wf\<^sub>e\<^sub>s\<^sub>t V \2
 4. \<And>f T. \<lbrakk>Fun f T \<sqsubseteq>\<^sub>s\<^sub>e\<^sub>t ik\<^sub>e\<^sub>s\<^sub>t \1 \<union> assignment_rhs\<^sub>e\<^sub>s\<^sub>t \1; \<S>2 = \<S>1; \2 = \1 @ [Decomp (Fun f T)]; wf\<^sub>e\<^sub>s\<^sub>t V \1\<rbrakk> \<Longrightarrow> wf\<^sub>e\<^sub>s\<^sub>t V \2
[PROOF STEP]
case (Receive ts)
[PROOF STATE]
proof (state)
this:
receive\<langle>ts\<rangle>\<^sub>s\<^sub>t # S_ \<in> \<S>1
\<S>2 = update\<^sub>s\<^sub>t \<S>1 (receive\<langle>ts\<rangle>\<^sub>s\<^sub>t # S_)
\2 = \1 @ [Step (send\<langle>ts\<rangle>\<^sub>s\<^sub>t)]
wf\<^sub>e\<^sub>s\<^sub>t V \1

goal (4 subgoals):
 1. \<And>t S. \<lbrakk>receive\<langle>t\<rangle>\<^sub>s\<^sub>t # S \<in> \<S>1; \<S>2 = update\<^sub>s\<^sub>t \<S>1 (receive\<langle>t\<rangle>\<^sub>s\<^sub>t # S); \2 = \1 @ [Step (send\<langle>t\<rangle>\<^sub>s\<^sub>t)]; wf\<^sub>e\<^sub>s\<^sub>t V \1\<rbrakk> \<Longrightarrow> wf\<^sub>e\<^sub>s\<^sub>t V \2
 2. \<And>a t t' S. \<lbrakk>\<langle>a: t \<doteq> t'\<rangle>\<^sub>s\<^sub>t # S \<in> \<S>1; \<S>2 = update\<^sub>s\<^sub>t \<S>1 (\<langle>a: t \<doteq> t'\<rangle>\<^sub>s\<^sub>t # S); \2 = \1 @ [Step \<langle>a: t \<doteq> t'\<rangle>\<^sub>s\<^sub>t]; wf\<^sub>e\<^sub>s\<^sub>t V \1\<rbrakk> \<Longrightarrow> wf\<^sub>e\<^sub>s\<^sub>t V \2
 3. \<And>X F S. \<lbrakk>\<forall>X\<langle>\<or>\<noteq>: F\<rangle>\<^sub>s\<^sub>t # S \<in> \<S>1; \<S>2 = update\<^sub>s\<^sub>t \<S>1 (\<forall>X\<langle>\<or>\<noteq>: F\<rangle>\<^sub>s\<^sub>t # S); \2 = \1 @ [Step \<forall>X\<langle>\<or>\<noteq>: F\<rangle>\<^sub>s\<^sub>t]; wf\<^sub>e\<^sub>s\<^sub>t V \1\<rbrakk> \<Longrightarrow> wf\<^sub>e\<^sub>s\<^sub>t V \2
 4. \<And>f T. \<lbrakk>Fun f T \<sqsubseteq>\<^sub>s\<^sub>e\<^sub>t ik\<^sub>e\<^sub>s\<^sub>t \1 \<union> assignment_rhs\<^sub>e\<^sub>s\<^sub>t \1; \<S>2 = \<S>1; \2 = \1 @ [Decomp (Fun f T)]; wf\<^sub>e\<^sub>s\<^sub>t V \1\<rbrakk> \<Longrightarrow> wf\<^sub>e\<^sub>s\<^sub>t V \2
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
receive\<langle>ts\<rangle>\<^sub>s\<^sub>t # S_ \<in> \<S>1
\<S>2 = update\<^sub>s\<^sub>t \<S>1 (receive\<langle>ts\<rangle>\<^sub>s\<^sub>t # S_)
\2 = \1 @ [Step (send\<langle>ts\<rangle>\<^sub>s\<^sub>t)]
wf\<^sub>e\<^sub>s\<^sub>t V \1

goal (1 subgoal):
 1. wf\<^sub>e\<^sub>s\<^sub>t V \2
[PROOF STEP]
using wf_snd_append to_st_append
[PROOF STATE]
proof (prove)
using this:
receive\<langle>ts\<rangle>\<^sub>s\<^sub>t # S_ \<in> \<S>1
\<S>2 = update\<^sub>s\<^sub>t \<S>1 (receive\<langle>ts\<rangle>\<^sub>s\<^sub>t # S_)
\2 = \1 @ [Step (send\<langle>ts\<rangle>\<^sub>s\<^sub>t)]
wf\<^sub>e\<^sub>s\<^sub>t V \1
wf\<^sub>s\<^sub>t ?V (?S @ [send\<langle>?t\<rangle>\<^sub>s\<^sub>t]) = wf\<^sub>s\<^sub>t ?V ?S
to_st (?A @ ?B) = to_st ?A @ to_st ?B

goal (1 subgoal):
 1. wf\<^sub>e\<^sub>s\<^sub>t V \2
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
wf\<^sub>e\<^sub>s\<^sub>t V \2

goal (3 subgoals):
 1. \<And>a t t' S. \<lbrakk>\<langle>a: t \<doteq> t'\<rangle>\<^sub>s\<^sub>t # S \<in> \<S>1; \<S>2 = update\<^sub>s\<^sub>t \<S>1 (\<langle>a: t \<doteq> t'\<rangle>\<^sub>s\<^sub>t # S); \2 = \1 @ [Step \<langle>a: t \<doteq> t'\<rangle>\<^sub>s\<^sub>t]; wf\<^sub>e\<^sub>s\<^sub>t V \1\<rbrakk> \<Longrightarrow> wf\<^sub>e\<^sub>s\<^sub>t V \2
 2. \<And>X F S. \<lbrakk>\<forall>X\<langle>\<or>\<noteq>: F\<rangle>\<^sub>s\<^sub>t # S \<in> \<S>1; \<S>2 = update\<^sub>s\<^sub>t \<S>1 (\<forall>X\<langle>\<or>\<noteq>: F\<rangle>\<^sub>s\<^sub>t # S); \2 = \1 @ [Step \<forall>X\<langle>\<or>\<noteq>: F\<rangle>\<^sub>s\<^sub>t]; wf\<^sub>e\<^sub>s\<^sub>t V \1\<rbrakk> \<Longrightarrow> wf\<^sub>e\<^sub>s\<^sub>t V \2
 3. \<And>f T. \<lbrakk>Fun f T \<sqsubseteq>\<^sub>s\<^sub>e\<^sub>t ik\<^sub>e\<^sub>s\<^sub>t \1 \<union> assignment_rhs\<^sub>e\<^sub>s\<^sub>t \1; \<S>2 = \<S>1; \2 = \1 @ [Decomp (Fun f T)]; wf\<^sub>e\<^sub>s\<^sub>t V \1\<rbrakk> \<Longrightarrow> wf\<^sub>e\<^sub>s\<^sub>t V \2
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>a t t' S. \<lbrakk>\<langle>a: t \<doteq> t'\<rangle>\<^sub>s\<^sub>t # S \<in> \<S>1; \<S>2 = update\<^sub>s\<^sub>t \<S>1 (\<langle>a: t \<doteq> t'\<rangle>\<^sub>s\<^sub>t # S); \2 = \1 @ [Step \<langle>a: t \<doteq> t'\<rangle>\<^sub>s\<^sub>t]; wf\<^sub>e\<^sub>s\<^sub>t V \1\<rbrakk> \<Longrightarrow> wf\<^sub>e\<^sub>s\<^sub>t V \2
 2. \<And>X F S. \<lbrakk>\<forall>X\<langle>\<or>\<noteq>: F\<rangle>\<^sub>s\<^sub>t # S \<in> \<S>1; \<S>2 = update\<^sub>s\<^sub>t \<S>1 (\<forall>X\<langle>\<or>\<noteq>: F\<rangle>\<^sub>s\<^sub>t # S); \2 = \1 @ [Step \<forall>X\<langle>\<or>\<noteq>: F\<rangle>\<^sub>s\<^sub>t]; wf\<^sub>e\<^sub>s\<^sub>t V \1\<rbrakk> \<Longrightarrow> wf\<^sub>e\<^sub>s\<^sub>t V \2
 3. \<And>f T. \<lbrakk>Fun f T \<sqsubseteq>\<^sub>s\<^sub>e\<^sub>t ik\<^sub>e\<^sub>s\<^sub>t \1 \<union> assignment_rhs\<^sub>e\<^sub>s\<^sub>t \1; \<S>2 = \<S>1; \2 = \1 @ [Decomp (Fun f T)]; wf\<^sub>e\<^sub>s\<^sub>t V \1\<rbrakk> \<Longrightarrow> wf\<^sub>e\<^sub>s\<^sub>t V \2
[PROOF STEP]
case (Equality a t t' S)
[PROOF STATE]
proof (state)
this:
\<langle>a: t \<doteq> t'\<rangle>\<^sub>s\<^sub>t # S \<in> \<S>1
\<S>2 = update\<^sub>s\<^sub>t \<S>1 (\<langle>a: t \<doteq> t'\<rangle>\<^sub>s\<^sub>t # S)
\2 = \1 @ [Step \<langle>a: t \<doteq> t'\<rangle>\<^sub>s\<^sub>t]
wf\<^sub>e\<^sub>s\<^sub>t V \1

goal (3 subgoals):
 1. \<And>a t t' S. \<lbrakk>\<langle>a: t \<doteq> t'\<rangle>\<^sub>s\<^sub>t # S \<in> \<S>1; \<S>2 = update\<^sub>s\<^sub>t \<S>1 (\<langle>a: t \<doteq> t'\<rangle>\<^sub>s\<^sub>t # S); \2 = \1 @ [Step \<langle>a: t \<doteq> t'\<rangle>\<^sub>s\<^sub>t]; wf\<^sub>e\<^sub>s\<^sub>t V \1\<rbrakk> \<Longrightarrow> wf\<^sub>e\<^sub>s\<^sub>t V \2
 2. \<And>X F S. \<lbrakk>\<forall>X\<langle>\<or>\<noteq>: F\<rangle>\<^sub>s\<^sub>t # S \<in> \<S>1; \<S>2 = update\<^sub>s\<^sub>t \<S>1 (\<forall>X\<langle>\<or>\<noteq>: F\<rangle>\<^sub>s\<^sub>t # S); \2 = \1 @ [Step \<forall>X\<langle>\<or>\<noteq>: F\<rangle>\<^sub>s\<^sub>t]; wf\<^sub>e\<^sub>s\<^sub>t V \1\<rbrakk> \<Longrightarrow> wf\<^sub>e\<^sub>s\<^sub>t V \2
 3. \<And>f T. \<lbrakk>Fun f T \<sqsubseteq>\<^sub>s\<^sub>e\<^sub>t ik\<^sub>e\<^sub>s\<^sub>t \1 \<union> assignment_rhs\<^sub>e\<^sub>s\<^sub>t \1; \<S>2 = \<S>1; \2 = \1 @ [Decomp (Fun f T)]; wf\<^sub>e\<^sub>s\<^sub>t V \1\<rbrakk> \<Longrightarrow> wf\<^sub>e\<^sub>s\<^sub>t V \2
[PROOF STEP]
hence "wf\<^sub>s\<^sub>t (wfrestrictedvars\<^sub>e\<^sub>s\<^sub>t \1) (\<langle>a: t \<doteq> t'\<rangle>\<^sub>s\<^sub>t#(dual\<^sub>s\<^sub>t S))"
[PROOF STATE]
proof (prove)
using this:
\<langle>a: t \<doteq> t'\<rangle>\<^sub>s\<^sub>t # S \<in> \<S>1
\<S>2 = update\<^sub>s\<^sub>t \<S>1 (\<langle>a: t \<doteq> t'\<rangle>\<^sub>s\<^sub>t # S)
\2 = \1 @ [Step \<langle>a: t \<doteq> t'\<rangle>\<^sub>s\<^sub>t]
wf\<^sub>e\<^sub>s\<^sub>t V \1

goal (1 subgoal):
 1. wf\<^sub>s\<^sub>t (wfrestrictedvars\<^sub>e\<^sub>s\<^sub>t \1) (\<langle>a: t \<doteq> t'\<rangle>\<^sub>s\<^sub>t # dual\<^sub>s\<^sub>t S)
[PROOF STEP]
using *(1)
[PROOF STATE]
proof (prove)
using this:
\<langle>a: t \<doteq> t'\<rangle>\<^sub>s\<^sub>t # S \<in> \<S>1
\<S>2 = update\<^sub>s\<^sub>t \<S>1 (\<langle>a: t \<doteq> t'\<rangle>\<^sub>s\<^sub>t # S)
\2 = \1 @ [Step \<langle>a: t \<doteq> t'\<rangle>\<^sub>s\<^sub>t]
wf\<^sub>e\<^sub>s\<^sub>t V \1
wf\<^sub>s\<^sub>t\<^sub>s' \<S>1 \1

goal (1 subgoal):
 1. wf\<^sub>s\<^sub>t (wfrestrictedvars\<^sub>e\<^sub>s\<^sub>t \1) (\<langle>a: t \<doteq> t'\<rangle>\<^sub>s\<^sub>t # dual\<^sub>s\<^sub>t S)
[PROOF STEP]
unfolding wf\<^sub>s\<^sub>t\<^sub>s'_def
[PROOF STATE]
proof (prove)
using this:
\<langle>a: t \<doteq> t'\<rangle>\<^sub>s\<^sub>t # S \<in> \<S>1
\<S>2 = update\<^sub>s\<^sub>t \<S>1 (\<langle>a: t \<doteq> t'\<rangle>\<^sub>s\<^sub>t # S)
\2 = \1 @ [Step \<langle>a: t \<doteq> t'\<rangle>\<^sub>s\<^sub>t]
wf\<^sub>e\<^sub>s\<^sub>t V \1
(\<forall>S\<in>\<S>1. wf\<^sub>s\<^sub>t (wfrestrictedvars\<^sub>e\<^sub>s\<^sub>t \1) (dual\<^sub>s\<^sub>t S)) \<and> (\<forall>S\<in>\<S>1. \<forall>S'\<in>\<S>1. fv\<^sub>s\<^sub>t S \<inter> bvars\<^sub>s\<^sub>t S' = {}) \<and> (\<forall>S\<in>\<S>1. fv\<^sub>s\<^sub>t S \<inter> bvars\<^sub>e\<^sub>s\<^sub>t \1 = {}) \<and> (\<forall>S\<in>\<S>1. fv\<^sub>e\<^sub>s\<^sub>t \1 \<inter> bvars\<^sub>s\<^sub>t S = {})

goal (1 subgoal):
 1. wf\<^sub>s\<^sub>t (wfrestrictedvars\<^sub>e\<^sub>s\<^sub>t \1) (\<langle>a: t \<doteq> t'\<rangle>\<^sub>s\<^sub>t # dual\<^sub>s\<^sub>t S)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
wf\<^sub>s\<^sub>t (wfrestrictedvars\<^sub>e\<^sub>s\<^sub>t \1) (\<langle>a: t \<doteq> t'\<rangle>\<^sub>s\<^sub>t # dual\<^sub>s\<^sub>t S)

goal (3 subgoals):
 1. \<And>a t t' S. \<lbrakk>\<langle>a: t \<doteq> t'\<rangle>\<^sub>s\<^sub>t # S \<in> \<S>1; \<S>2 = update\<^sub>s\<^sub>t \<S>1 (\<langle>a: t \<doteq> t'\<rangle>\<^sub>s\<^sub>t # S); \2 = \1 @ [Step \<langle>a: t \<doteq> t'\<rangle>\<^sub>s\<^sub>t]; wf\<^sub>e\<^sub>s\<^sub>t V \1\<rbrakk> \<Longrightarrow> wf\<^sub>e\<^sub>s\<^sub>t V \2
 2. \<And>X F S. \<lbrakk>\<forall>X\<langle>\<or>\<noteq>: F\<rangle>\<^sub>s\<^sub>t # S \<in> \<S>1; \<S>2 = update\<^sub>s\<^sub>t \<S>1 (\<forall>X\<langle>\<or>\<noteq>: F\<rangle>\<^sub>s\<^sub>t # S); \2 = \1 @ [Step \<forall>X\<langle>\<or>\<noteq>: F\<rangle>\<^sub>s\<^sub>t]; wf\<^sub>e\<^sub>s\<^sub>t V \1\<rbrakk> \<Longrightarrow> wf\<^sub>e\<^sub>s\<^sub>t V \2
 3. \<And>f T. \<lbrakk>Fun f T \<sqsubseteq>\<^sub>s\<^sub>e\<^sub>t ik\<^sub>e\<^sub>s\<^sub>t \1 \<union> assignment_rhs\<^sub>e\<^sub>s\<^sub>t \1; \<S>2 = \<S>1; \2 = \1 @ [Decomp (Fun f T)]; wf\<^sub>e\<^sub>s\<^sub>t V \1\<rbrakk> \<Longrightarrow> wf\<^sub>e\<^sub>s\<^sub>t V \2
[PROOF STEP]
hence "fv t' \<subseteq> wfrestrictedvars\<^sub>s\<^sub>t (to_st \1) \<union> V" when "a = Assign"
[PROOF STATE]
proof (prove)
using this:
wf\<^sub>s\<^sub>t (wfrestrictedvars\<^sub>e\<^sub>s\<^sub>t \1) (\<langle>a: t \<doteq> t'\<rangle>\<^sub>s\<^sub>t # dual\<^sub>s\<^sub>t S)

goal (1 subgoal):
 1. fv t' \<subseteq> wfrestrictedvars\<^sub>e\<^sub>s\<^sub>t \1 \<union> V
[PROOF STEP]
using wfrestrictedvars\<^sub>e\<^sub>s\<^sub>t_eq_wfrestrictedvars\<^sub>s\<^sub>t that
[PROOF STATE]
proof (prove)
using this:
wf\<^sub>s\<^sub>t (wfrestrictedvars\<^sub>e\<^sub>s\<^sub>t \1) (\<langle>a: t \<doteq> t'\<rangle>\<^sub>s\<^sub>t # dual\<^sub>s\<^sub>t S)
wfrestrictedvars\<^sub>e\<^sub>s\<^sub>t ?A = wfrestrictedvars\<^sub>e\<^sub>s\<^sub>t ?A
a = assign

goal (1 subgoal):
 1. fv t' \<subseteq> wfrestrictedvars\<^sub>e\<^sub>s\<^sub>t \1 \<union> V
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
a = assign \<Longrightarrow> fv t' \<subseteq> wfrestrictedvars\<^sub>e\<^sub>s\<^sub>t \1 \<union> V

goal (3 subgoals):
 1. \<And>a t t' S. \<lbrakk>\<langle>a: t \<doteq> t'\<rangle>\<^sub>s\<^sub>t # S \<in> \<S>1; \<S>2 = update\<^sub>s\<^sub>t \<S>1 (\<langle>a: t \<doteq> t'\<rangle>\<^sub>s\<^sub>t # S); \2 = \1 @ [Step \<langle>a: t \<doteq> t'\<rangle>\<^sub>s\<^sub>t]; wf\<^sub>e\<^sub>s\<^sub>t V \1\<rbrakk> \<Longrightarrow> wf\<^sub>e\<^sub>s\<^sub>t V \2
 2. \<And>X F S. \<lbrakk>\<forall>X\<langle>\<or>\<noteq>: F\<rangle>\<^sub>s\<^sub>t # S \<in> \<S>1; \<S>2 = update\<^sub>s\<^sub>t \<S>1 (\<forall>X\<langle>\<or>\<noteq>: F\<rangle>\<^sub>s\<^sub>t # S); \2 = \1 @ [Step \<forall>X\<langle>\<or>\<noteq>: F\<rangle>\<^sub>s\<^sub>t]; wf\<^sub>e\<^sub>s\<^sub>t V \1\<rbrakk> \<Longrightarrow> wf\<^sub>e\<^sub>s\<^sub>t V \2
 3. \<And>f T. \<lbrakk>Fun f T \<sqsubseteq>\<^sub>s\<^sub>e\<^sub>t ik\<^sub>e\<^sub>s\<^sub>t \1 \<union> assignment_rhs\<^sub>e\<^sub>s\<^sub>t \1; \<S>2 = \<S>1; \2 = \1 @ [Decomp (Fun f T)]; wf\<^sub>e\<^sub>s\<^sub>t V \1\<rbrakk> \<Longrightarrow> wf\<^sub>e\<^sub>s\<^sub>t V \2
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
a = assign \<Longrightarrow> fv t' \<subseteq> wfrestrictedvars\<^sub>e\<^sub>s\<^sub>t \1 \<union> V

goal (1 subgoal):
 1. wf\<^sub>e\<^sub>s\<^sub>t V \2
[PROOF STEP]
using Equality wf_eq_append''' to_st_append
[PROOF STATE]
proof (prove)
using this:
a = assign \<Longrightarrow> fv t' \<subseteq> wfrestrictedvars\<^sub>e\<^sub>s\<^sub>t \1 \<union> V
\<langle>a: t \<doteq> t'\<rangle>\<^sub>s\<^sub>t # S \<in> \<S>1
\<S>2 = update\<^sub>s\<^sub>t \<S>1 (\<langle>a: t \<doteq> t'\<rangle>\<^sub>s\<^sub>t # S)
\2 = \1 @ [Step \<langle>a: t \<doteq> t'\<rangle>\<^sub>s\<^sub>t]
wf\<^sub>e\<^sub>s\<^sub>t V \1
\<lbrakk>wf\<^sub>s\<^sub>t ?V ?S; fv ?t' \<subseteq> wfrestrictedvars\<^sub>s\<^sub>t ?S \<union> ?V\<rbrakk> \<Longrightarrow> wf\<^sub>s\<^sub>t ?V (?S @ [\<langle>?a: ?t \<doteq> ?t'\<rangle>\<^sub>s\<^sub>t])
to_st (?A @ ?B) = to_st ?A @ to_st ?B

goal (1 subgoal):
 1. wf\<^sub>e\<^sub>s\<^sub>t V \2
[PROOF STEP]
by (cases a) auto
[PROOF STATE]
proof (state)
this:
wf\<^sub>e\<^sub>s\<^sub>t V \2

goal (2 subgoals):
 1. \<And>X F S. \<lbrakk>\<forall>X\<langle>\<or>\<noteq>: F\<rangle>\<^sub>s\<^sub>t # S \<in> \<S>1; \<S>2 = update\<^sub>s\<^sub>t \<S>1 (\<forall>X\<langle>\<or>\<noteq>: F\<rangle>\<^sub>s\<^sub>t # S); \2 = \1 @ [Step \<forall>X\<langle>\<or>\<noteq>: F\<rangle>\<^sub>s\<^sub>t]; wf\<^sub>e\<^sub>s\<^sub>t V \1\<rbrakk> \<Longrightarrow> wf\<^sub>e\<^sub>s\<^sub>t V \2
 2. \<And>f T. \<lbrakk>Fun f T \<sqsubseteq>\<^sub>s\<^sub>e\<^sub>t ik\<^sub>e\<^sub>s\<^sub>t \1 \<union> assignment_rhs\<^sub>e\<^sub>s\<^sub>t \1; \<S>2 = \<S>1; \2 = \1 @ [Decomp (Fun f T)]; wf\<^sub>e\<^sub>s\<^sub>t V \1\<rbrakk> \<Longrightarrow> wf\<^sub>e\<^sub>s\<^sub>t V \2
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>X F S. \<lbrakk>\<forall>X\<langle>\<or>\<noteq>: F\<rangle>\<^sub>s\<^sub>t # S \<in> \<S>1; \<S>2 = update\<^sub>s\<^sub>t \<S>1 (\<forall>X\<langle>\<or>\<noteq>: F\<rangle>\<^sub>s\<^sub>t # S); \2 = \1 @ [Step \<forall>X\<langle>\<or>\<noteq>: F\<rangle>\<^sub>s\<^sub>t]; wf\<^sub>e\<^sub>s\<^sub>t V \1\<rbrakk> \<Longrightarrow> wf\<^sub>e\<^sub>s\<^sub>t V \2
 2. \<And>f T. \<lbrakk>Fun f T \<sqsubseteq>\<^sub>s\<^sub>e\<^sub>t ik\<^sub>e\<^sub>s\<^sub>t \1 \<union> assignment_rhs\<^sub>e\<^sub>s\<^sub>t \1; \<S>2 = \<S>1; \2 = \1 @ [Decomp (Fun f T)]; wf\<^sub>e\<^sub>s\<^sub>t V \1\<rbrakk> \<Longrightarrow> wf\<^sub>e\<^sub>s\<^sub>t V \2
[PROOF STEP]
case (Inequality t t' S)
[PROOF STATE]
proof (state)
this:
\<forall>t\<langle>\<or>\<noteq>: t'\<rangle>\<^sub>s\<^sub>t # S \<in> \<S>1
\<S>2 = update\<^sub>s\<^sub>t \<S>1 (\<forall>t\<langle>\<or>\<noteq>: t'\<rangle>\<^sub>s\<^sub>t # S)
\2 = \1 @ [Step \<forall>t\<langle>\<or>\<noteq>: t'\<rangle>\<^sub>s\<^sub>t]
wf\<^sub>e\<^sub>s\<^sub>t V \1

goal (2 subgoals):
 1. \<And>X F S. \<lbrakk>\<forall>X\<langle>\<or>\<noteq>: F\<rangle>\<^sub>s\<^sub>t # S \<in> \<S>1; \<S>2 = update\<^sub>s\<^sub>t \<S>1 (\<forall>X\<langle>\<or>\<noteq>: F\<rangle>\<^sub>s\<^sub>t # S); \2 = \1 @ [Step \<forall>X\<langle>\<or>\<noteq>: F\<rangle>\<^sub>s\<^sub>t]; wf\<^sub>e\<^sub>s\<^sub>t V \1\<rbrakk> \<Longrightarrow> wf\<^sub>e\<^sub>s\<^sub>t V \2
 2. \<And>f T. \<lbrakk>Fun f T \<sqsubseteq>\<^sub>s\<^sub>e\<^sub>t ik\<^sub>e\<^sub>s\<^sub>t \1 \<union> assignment_rhs\<^sub>e\<^sub>s\<^sub>t \1; \<S>2 = \<S>1; \2 = \1 @ [Decomp (Fun f T)]; wf\<^sub>e\<^sub>s\<^sub>t V \1\<rbrakk> \<Longrightarrow> wf\<^sub>e\<^sub>s\<^sub>t V \2
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
\<forall>t\<langle>\<or>\<noteq>: t'\<rangle>\<^sub>s\<^sub>t # S \<in> \<S>1
\<S>2 = update\<^sub>s\<^sub>t \<S>1 (\<forall>t\<langle>\<or>\<noteq>: t'\<rangle>\<^sub>s\<^sub>t # S)
\2 = \1 @ [Step \<forall>t\<langle>\<or>\<noteq>: t'\<rangle>\<^sub>s\<^sub>t]
wf\<^sub>e\<^sub>s\<^sub>t V \1

goal (1 subgoal):
 1. wf\<^sub>e\<^sub>s\<^sub>t V \2
[PROOF STEP]
using wf_ineq_append'' to_st_append
[PROOF STATE]
proof (prove)
using this:
\<forall>t\<langle>\<or>\<noteq>: t'\<rangle>\<^sub>s\<^sub>t # S \<in> \<S>1
\<S>2 = update\<^sub>s\<^sub>t \<S>1 (\<forall>t\<langle>\<or>\<noteq>: t'\<rangle>\<^sub>s\<^sub>t # S)
\2 = \1 @ [Step \<forall>t\<langle>\<or>\<noteq>: t'\<rangle>\<^sub>s\<^sub>t]
wf\<^sub>e\<^sub>s\<^sub>t V \1
wf\<^sub>s\<^sub>t ?V ?S \<Longrightarrow> wf\<^sub>s\<^sub>t ?V (?S @ [\<forall>?X\<langle>\<or>\<noteq>: ?F\<rangle>\<^sub>s\<^sub>t])
to_st (?A @ ?B) = to_st ?A @ to_st ?B

goal (1 subgoal):
 1. wf\<^sub>e\<^sub>s\<^sub>t V \2
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
wf\<^sub>e\<^sub>s\<^sub>t V \2

goal (1 subgoal):
 1. \<And>f T. \<lbrakk>Fun f T \<sqsubseteq>\<^sub>s\<^sub>e\<^sub>t ik\<^sub>e\<^sub>s\<^sub>t \1 \<union> assignment_rhs\<^sub>e\<^sub>s\<^sub>t \1; \<S>2 = \<S>1; \2 = \1 @ [Decomp (Fun f T)]; wf\<^sub>e\<^sub>s\<^sub>t V \1\<rbrakk> \<Longrightarrow> wf\<^sub>e\<^sub>s\<^sub>t V \2
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>f T. \<lbrakk>Fun f T \<sqsubseteq>\<^sub>s\<^sub>e\<^sub>t ik\<^sub>e\<^sub>s\<^sub>t \1 \<union> assignment_rhs\<^sub>e\<^sub>s\<^sub>t \1; \<S>2 = \<S>1; \2 = \1 @ [Decomp (Fun f T)]; wf\<^sub>e\<^sub>s\<^sub>t V \1\<rbrakk> \<Longrightarrow> wf\<^sub>e\<^sub>s\<^sub>t V \2
[PROOF STEP]
case (Decompose f T)
[PROOF STATE]
proof (state)
this:
Fun f T \<sqsubseteq>\<^sub>s\<^sub>e\<^sub>t ik\<^sub>e\<^sub>s\<^sub>t \1 \<union> assignment_rhs\<^sub>e\<^sub>s\<^sub>t \1
\<S>2 = \<S>1
\2 = \1 @ [Decomp (Fun f T)]
wf\<^sub>e\<^sub>s\<^sub>t V \1

goal (1 subgoal):
 1. \<And>f T. \<lbrakk>Fun f T \<sqsubseteq>\<^sub>s\<^sub>e\<^sub>t ik\<^sub>e\<^sub>s\<^sub>t \1 \<union> assignment_rhs\<^sub>e\<^sub>s\<^sub>t \1; \<S>2 = \<S>1; \2 = \1 @ [Decomp (Fun f T)]; wf\<^sub>e\<^sub>s\<^sub>t V \1\<rbrakk> \<Longrightarrow> wf\<^sub>e\<^sub>s\<^sub>t V \2
[PROOF STEP]
hence "fv (Fun f T) \<subseteq> wfrestrictedvars\<^sub>e\<^sub>s\<^sub>t \1"
[PROOF STATE]
proof (prove)
using this:
Fun f T \<sqsubseteq>\<^sub>s\<^sub>e\<^sub>t ik\<^sub>e\<^sub>s\<^sub>t \1 \<union> assignment_rhs\<^sub>e\<^sub>s\<^sub>t \1
\<S>2 = \<S>1
\2 = \1 @ [Decomp (Fun f T)]
wf\<^sub>e\<^sub>s\<^sub>t V \1

goal (1 subgoal):
 1. fv (Fun f T) \<subseteq> wfrestrictedvars\<^sub>e\<^sub>s\<^sub>t \1
[PROOF STEP]
by (metis fv_subterms_set fv_subset subset_trans
                ik\<^sub>s\<^sub>t_assignment_rhs\<^sub>s\<^sub>t_wfrestrictedvars_subset)
[PROOF STATE]
proof (state)
this:
fv (Fun f T) \<subseteq> wfrestrictedvars\<^sub>e\<^sub>s\<^sub>t \1

goal (1 subgoal):
 1. \<And>f T. \<lbrakk>Fun f T \<sqsubseteq>\<^sub>s\<^sub>e\<^sub>t ik\<^sub>e\<^sub>s\<^sub>t \1 \<union> assignment_rhs\<^sub>e\<^sub>s\<^sub>t \1; \<S>2 = \<S>1; \2 = \1 @ [Decomp (Fun f T)]; wf\<^sub>e\<^sub>s\<^sub>t V \1\<rbrakk> \<Longrightarrow> wf\<^sub>e\<^sub>s\<^sub>t V \2
[PROOF STEP]
hence "vars\<^sub>s\<^sub>t (decomp (Fun f T)) \<subseteq> wfrestrictedvars\<^sub>s\<^sub>t (to_st \1) \<union> V"
[PROOF STATE]
proof (prove)
using this:
fv (Fun f T) \<subseteq> wfrestrictedvars\<^sub>e\<^sub>s\<^sub>t \1

goal (1 subgoal):
 1. vars\<^sub>s\<^sub>t (decomp (Fun f T)) \<subseteq> wfrestrictedvars\<^sub>e\<^sub>s\<^sub>t \1 \<union> V
[PROOF STEP]
using decomp_vars[of "Fun f T"] wfrestrictedvars\<^sub>e\<^sub>s\<^sub>t_eq_wfrestrictedvars\<^sub>s\<^sub>t[of \1]
[PROOF STATE]
proof (prove)
using this:
fv (Fun f T) \<subseteq> wfrestrictedvars\<^sub>e\<^sub>s\<^sub>t \1
wfrestrictedvars\<^sub>s\<^sub>t (decomp (Fun f T)) = fv (Fun f T)
vars\<^sub>s\<^sub>t (decomp (Fun f T)) = fv (Fun f T)
bvars\<^sub>s\<^sub>t (decomp (Fun f T)) = {}
fv\<^sub>s\<^sub>t (decomp (Fun f T)) = fv (Fun f T)
wfrestrictedvars\<^sub>e\<^sub>s\<^sub>t \1 = wfrestrictedvars\<^sub>e\<^sub>s\<^sub>t \1

goal (1 subgoal):
 1. vars\<^sub>s\<^sub>t (decomp (Fun f T)) \<subseteq> wfrestrictedvars\<^sub>e\<^sub>s\<^sub>t \1 \<union> V
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
vars\<^sub>s\<^sub>t (decomp (Fun f T)) \<subseteq> wfrestrictedvars\<^sub>e\<^sub>s\<^sub>t \1 \<union> V

goal (1 subgoal):
 1. \<And>f T. \<lbrakk>Fun f T \<sqsubseteq>\<^sub>s\<^sub>e\<^sub>t ik\<^sub>e\<^sub>s\<^sub>t \1 \<union> assignment_rhs\<^sub>e\<^sub>s\<^sub>t \1; \<S>2 = \<S>1; \2 = \1 @ [Decomp (Fun f T)]; wf\<^sub>e\<^sub>s\<^sub>t V \1\<rbrakk> \<Longrightarrow> wf\<^sub>e\<^sub>s\<^sub>t V \2
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
vars\<^sub>s\<^sub>t (decomp (Fun f T)) \<subseteq> wfrestrictedvars\<^sub>e\<^sub>s\<^sub>t \1 \<union> V

goal (1 subgoal):
 1. wf\<^sub>e\<^sub>s\<^sub>t V \2
[PROOF STEP]
using to_st_append[of \1 "[Decomp (Fun f T)]"]
            wf_append_suffix[OF Decompose.prems] Decompose.hyps(3)
[PROOF STATE]
proof (prove)
using this:
vars\<^sub>s\<^sub>t (decomp (Fun f T)) \<subseteq> wfrestrictedvars\<^sub>e\<^sub>s\<^sub>t \1 \<union> V
to_st (\1 @ [Decomp (Fun f T)]) = to_st \1 @ to_st [Decomp (Fun f T)]
wfrestrictedvars\<^sub>s\<^sub>t ?S' \<subseteq> wfrestrictedvars\<^sub>e\<^sub>s\<^sub>t \1 \<union> V \<Longrightarrow> wf\<^sub>s\<^sub>t V (to_st \1 @ ?S')
\2 = \1 @ [Decomp (Fun f T)]

goal (1 subgoal):
 1. wf\<^sub>e\<^sub>s\<^sub>t V \2
[PROOF STEP]
by (metis append_Nil2 decomp_vars(1,2) to_st.simps(1,3))
[PROOF STATE]
proof (state)
this:
wf\<^sub>e\<^sub>s\<^sub>t V \2

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
wf\<^sub>e\<^sub>s\<^sub>t V \2

goal (1 subgoal):
 1. \<lbrakk>wf\<^sub>s\<^sub>t\<^sub>s' \<S> \; wf\<^sub>e\<^sub>s\<^sub>t V \\<rbrakk> \<Longrightarrow> wf\<^sub>e\<^sub>s\<^sub>t V \
[PROOF STEP]
qed metis


[STATEMENT]
lemma coerce_bind [coerce_simp]:
  fixes m :: "'a\<cdot>'m::monad" and k :: "'a \<rightarrow> 'b\<cdot>'m"
  shows "COERCE('b\<cdot>'m,'c\<cdot>'m)\<cdot>(m \<bind> k) = m \<bind> (\<Lambda> x. COERCE('b\<cdot>'m,'c\<cdot>'m)\<cdot>(k\<cdot>x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. COERCE('b\<cdot>'m, 'c\<cdot>'m)\<cdot>(m \<bind> k) = m \<bind> (\<Lambda> x. COERCE('b\<cdot>'m, 'c\<cdot>'m)\<cdot>(k\<cdot>x))
[PROOF STEP]
by (simp add: coerce_functor fmap_bind)


[STATEMENT]
lemma list_to_assignment_set_None_simp [simp] :
  "list_to_assignment_set (None # l) =
   list_to_assignment_set (Some True # l) \<union> list_to_assignment_set (Some False # l)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. list_to_assignment_set (None # l) = list_to_assignment_set (Some True # l) \<union> list_to_assignment_set (Some False # l)
[PROOF STEP]
unfolding list_to_assignment_set_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {a. \<forall>v<length (None # l). \<forall>f. (None # l) ! v = Some f \<longrightarrow> a v = f} = {a. \<forall>v<length (Some True # l). \<forall>f. (Some True # l) ! v = Some f \<longrightarrow> a v = f} \<union> {a. \<forall>v<length (Some False # l). \<forall>f. (Some False # l) ! v = Some f \<longrightarrow> a v = f}
[PROOF STEP]
apply (simp add: set_eq_iff less_Suc_eq_0_disj
            del: all_simps add: all_simps[symmetric])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x. (\<forall>f j. j < length l \<longrightarrow> l ! j = Some f \<longrightarrow> x (Suc j) = f) = (\<forall>v f j va fa ja. (va = 0 \<longrightarrow> fa \<longrightarrow> x 0) \<and> (va = Suc ja \<and> ja < length l \<longrightarrow> l ! ja = Some fa \<longrightarrow> x (Suc ja) = fa) \<or> (v = 0 \<longrightarrow> \<not> f \<longrightarrow> \<not> x 0) \<and> (v = Suc j \<and> j < length l \<longrightarrow> l ! j = Some f \<longrightarrow> x (Suc j) = f))
[PROOF STEP]
apply (simp add: all_conj_distrib)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x. (\<forall>f j. j < length l \<longrightarrow> l ! j = Some f \<longrightarrow> x (Suc j) = f) = (((\<exists>f. f) \<longrightarrow> x 0) \<and> (\<forall>f j. j < length l \<longrightarrow> l ! j = Some f \<longrightarrow> x (Suc j) = f) \<or> (Ex Not \<longrightarrow> \<not> x 0) \<and> (\<forall>f j. j < length l \<longrightarrow> l ! j = Some f \<longrightarrow> x (Suc j) = f))
[PROOF STEP]
apply (intro allI iffI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<forall>f j. j < length l \<longrightarrow> l ! j = Some f \<longrightarrow> x (Suc j) = f \<Longrightarrow> ((\<exists>f. f) \<longrightarrow> x 0) \<and> (\<forall>f j. j < length l \<longrightarrow> l ! j = Some f \<longrightarrow> x (Suc j) = f) \<or> (Ex Not \<longrightarrow> \<not> x 0) \<and> (\<forall>f j. j < length l \<longrightarrow> l ! j = Some f \<longrightarrow> x (Suc j) = f)
 2. \<And>x f j. ((\<exists>f. f) \<longrightarrow> x 0) \<and> (\<forall>f j. j < length l \<longrightarrow> l ! j = Some f \<longrightarrow> x (Suc j) = f) \<or> (Ex Not \<longrightarrow> \<not> x 0) \<and> (\<forall>f j. j < length l \<longrightarrow> l ! j = Some f \<longrightarrow> x (Suc j) = f) \<Longrightarrow> j < length l \<longrightarrow> l ! j = Some f \<longrightarrow> x (Suc j) = f
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x f j. ((\<exists>f. f) \<longrightarrow> x 0) \<and> (\<forall>f j. j < length l \<longrightarrow> l ! j = Some f \<longrightarrow> x (Suc j) = f) \<or> (Ex Not \<longrightarrow> \<not> x 0) \<and> (\<forall>f j. j < length l \<longrightarrow> l ! j = Some f \<longrightarrow> x (Suc j) = f) \<Longrightarrow> j < length l \<longrightarrow> l ! j = Some f \<longrightarrow> x (Suc j) = f
[PROOF STEP]
apply (elim disjE conjE)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x f j. \<lbrakk>(\<exists>f. f) \<longrightarrow> x 0; \<forall>f j. j < length l \<longrightarrow> l ! j = Some f \<longrightarrow> x (Suc j) = f\<rbrakk> \<Longrightarrow> j < length l \<longrightarrow> l ! j = Some f \<longrightarrow> x (Suc j) = f
 2. \<And>x f j. \<lbrakk>Ex Not \<longrightarrow> \<not> x 0; \<forall>f j. j < length l \<longrightarrow> l ! j = Some f \<longrightarrow> x (Suc j) = f\<rbrakk> \<Longrightarrow> j < length l \<longrightarrow> l ! j = Some f \<longrightarrow> x (Suc j) = f
[PROOF STEP]
apply simp_all
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma And_propos:
  "propos (And xs) = \<Union>{propos x| x. x \<in> set xs}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. propos (And xs) = \<Union> {propos x |x. x \<in> set xs}
[PROOF STEP]
proof (cases xs)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. xs = [] \<Longrightarrow> propos (And xs) = \<Union> {propos x |x. x \<in> set xs}
 2. \<And>a list. xs = a # list \<Longrightarrow> propos (And xs) = \<Union> {propos x |x. x \<in> set xs}
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
xs = []

goal (2 subgoals):
 1. xs = [] \<Longrightarrow> propos (And xs) = \<Union> {propos x |x. x \<in> set xs}
 2. \<And>a list. xs = a # list \<Longrightarrow> propos (And xs) = \<Union> {propos x |x. x \<in> set xs}
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
xs = []

goal (1 subgoal):
 1. propos (And xs) = \<Union> {propos x |x. x \<in> set xs}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
propos (And xs) = \<Union> {propos x |x. x \<in> set xs}

goal (1 subgoal):
 1. \<And>a list. xs = a # list \<Longrightarrow> propos (And xs) = \<Union> {propos x |x. x \<in> set xs}
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a list. xs = a # list \<Longrightarrow> propos (And xs) = \<Union> {propos x |x. x \<in> set xs}
[PROOF STEP]
case (Cons x xs)
[PROOF STATE]
proof (state)
this:
xs = x # xs

goal (1 subgoal):
 1. \<And>a list. xs = a # list \<Longrightarrow> propos (And xs) = \<Union> {propos x |x. x \<in> set xs}
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
xs = x # xs

goal (1 subgoal):
 1. propos (And xs) = \<Union> {propos x |x. x \<in> set xs}
[PROOF STEP]
using propos_foldl[of LTLAnd x]
[PROOF STATE]
proof (prove)
using this:
xs = x # xs
(\<And>x y. propos (x and y) = propos x \<union> propos y) \<Longrightarrow> \<Union> {propos y |y. y = x \<or> y \<in> set ?xs} = propos (foldl LTLAnd x ?xs)

goal (1 subgoal):
 1. propos (And xs) = \<Union> {propos x |x. x \<in> set xs}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
propos (And xs) = \<Union> {propos x |x. x \<in> set xs}

goal:
No subgoals!
[PROOF STEP]
qed