[STATEMENT]
lemma is_satis_g_i_upd2:
  assumes "eval_v i v s" and "is_satis ((i ( x \<mapsto> s))) c0" and "atom x \<sharp> G" and "wfG \<Theta> \<B> (G3@((x,b,c0)#\<^sub>\<Gamma>G))" and "wfV \<Theta> \<B> G v b" and "wfI \<Theta> (G3[x::=v]\<^sub>\<Gamma>\<^sub>v@G) i"
    and  "is_satis_g i (G3[x::=v]\<^sub>\<Gamma>\<^sub>v@G)"
  shows "is_satis_g (i ( x \<mapsto> s)) (G3@((x,b,c0)#\<^sub>\<Gamma>G))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1.  i(x \<mapsto> s) \<Turnstile> G3 @ (x, b, c0) #\<^sub>\<Gamma> G
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
i \<lbrakk> v \<rbrakk> ~ s
 i(x \<mapsto> s) \<Turnstile> c0
atom x \<sharp> G
 \<Theta> ; \<B>  \<turnstile>\<^sub>w\<^sub>f G3 @ (x, b, c0) #\<^sub>\<Gamma> G
 \<Theta> ; \<B> ; G \<turnstile>\<^sub>w\<^sub>f v : b
 \<Theta> ; G3[x::=v]\<^sub>\<Gamma>\<^sub>v @ G \<turnstile> i
 i \<Turnstile> G3[x::=v]\<^sub>\<Gamma>\<^sub>v @ G

goal (1 subgoal):
 1.  i(x \<mapsto> s) \<Turnstile> G3 @ (x, b, c0) #\<^sub>\<Gamma> G
[PROOF STEP]
proof(induct G3 rule: \<Gamma>_induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ;  i(x \<mapsto> s) \<Turnstile> c0 ; atom x \<sharp> G;  \<Theta> ; \<B>  \<turnstile>\<^sub>w\<^sub>f GNil @ (x, b, c0) #\<^sub>\<Gamma> G ;  \<Theta> ; \<B> ; G \<turnstile>\<^sub>w\<^sub>f v : b ;  \<Theta> ; GNil[x::=v]\<^sub>\<Gamma>\<^sub>v @ G \<turnstile> i;  i \<Turnstile> GNil[x::=v]\<^sub>\<Gamma>\<^sub>v @ G \<rbrakk> \<Longrightarrow>  i(x \<mapsto> s) \<Turnstile> GNil @ (x, b, c0) #\<^sub>\<Gamma> G
 2. \<And>xa ba c \<Gamma>'. \<lbrakk>\<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ;  i(x \<mapsto> s) \<Turnstile> c0 ; atom x \<sharp> G;  \<Theta> ; \<B>  \<turnstile>\<^sub>w\<^sub>f \<Gamma>' @ (x, b, c0) #\<^sub>\<Gamma> G ;  \<Theta> ; \<B> ; G \<turnstile>\<^sub>w\<^sub>f v : b ;  \<Theta> ; \<Gamma>'[x::=v]\<^sub>\<Gamma>\<^sub>v @ G \<turnstile> i;  i \<Turnstile> \<Gamma>'[x::=v]\<^sub>\<Gamma>\<^sub>v @ G \<rbrakk> \<Longrightarrow>  i(x \<mapsto> s) \<Turnstile> \<Gamma>' @ (x, b, c0) #\<^sub>\<Gamma> G ; i \<lbrakk> v \<rbrakk> ~ s ;  i(x \<mapsto> s) \<Turnstile> c0 ; atom x \<sharp> G;  \<Theta> ; \<B>  \<turnstile>\<^sub>w\<^sub>f ((xa, ba, c) #\<^sub>\<Gamma> \<Gamma>') @ (x, b, c0) #\<^sub>\<Gamma> G ;  \<Theta> ; \<B> ; G \<turnstile>\<^sub>w\<^sub>f v : b ;  \<Theta> ; ((xa, ba, c) #\<^sub>\<Gamma> \<Gamma>')[x::=v]\<^sub>\<Gamma>\<^sub>v @ G \<turnstile> i;  i \<Turnstile> ((xa, ba, c) #\<^sub>\<Gamma> \<Gamma>')[x::=v]\<^sub>\<Gamma>\<^sub>v @ G \<rbrakk> \<Longrightarrow>  i(x \<mapsto> s) \<Turnstile> ((xa, ba, c) #\<^sub>\<Gamma> \<Gamma>') @ (x, b, c0) #\<^sub>\<Gamma> G
[PROOF STEP]
case GNil
[PROOF STATE]
proof (state)
this:
i \<lbrakk> v \<rbrakk> ~ s
 i(x \<mapsto> s) \<Turnstile> c0
atom x \<sharp> G
 \<Theta> ; \<B>  \<turnstile>\<^sub>w\<^sub>f GNil @ (x, b, c0) #\<^sub>\<Gamma> G
 \<Theta> ; \<B> ; G \<turnstile>\<^sub>w\<^sub>f v : b
 \<Theta> ; GNil[x::=v]\<^sub>\<Gamma>\<^sub>v @ G \<turnstile> i
 i \<Turnstile> GNil[x::=v]\<^sub>\<Gamma>\<^sub>v @ G

goal (2 subgoals):
 1. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ;  i(x \<mapsto> s) \<Turnstile> c0 ; atom x \<sharp> G;  \<Theta> ; \<B>  \<turnstile>\<^sub>w\<^sub>f GNil @ (x, b, c0) #\<^sub>\<Gamma> G ;  \<Theta> ; \<B> ; G \<turnstile>\<^sub>w\<^sub>f v : b ;  \<Theta> ; GNil[x::=v]\<^sub>\<Gamma>\<^sub>v @ G \<turnstile> i;  i \<Turnstile> GNil[x::=v]\<^sub>\<Gamma>\<^sub>v @ G \<rbrakk> \<Longrightarrow>  i(x \<mapsto> s) \<Turnstile> GNil @ (x, b, c0) #\<^sub>\<Gamma> G
 2. \<And>xa ba c \<Gamma>'. \<lbrakk>\<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ;  i(x \<mapsto> s) \<Turnstile> c0 ; atom x \<sharp> G;  \<Theta> ; \<B>  \<turnstile>\<^sub>w\<^sub>f \<Gamma>' @ (x, b, c0) #\<^sub>\<Gamma> G ;  \<Theta> ; \<B> ; G \<turnstile>\<^sub>w\<^sub>f v : b ;  \<Theta> ; \<Gamma>'[x::=v]\<^sub>\<Gamma>\<^sub>v @ G \<turnstile> i;  i \<Turnstile> \<Gamma>'[x::=v]\<^sub>\<Gamma>\<^sub>v @ G \<rbrakk> \<Longrightarrow>  i(x \<mapsto> s) \<Turnstile> \<Gamma>' @ (x, b, c0) #\<^sub>\<Gamma> G ; i \<lbrakk> v \<rbrakk> ~ s ;  i(x \<mapsto> s) \<Turnstile> c0 ; atom x \<sharp> G;  \<Theta> ; \<B>  \<turnstile>\<^sub>w\<^sub>f ((xa, ba, c) #\<^sub>\<Gamma> \<Gamma>') @ (x, b, c0) #\<^sub>\<Gamma> G ;  \<Theta> ; \<B> ; G \<turnstile>\<^sub>w\<^sub>f v : b ;  \<Theta> ; ((xa, ba, c) #\<^sub>\<Gamma> \<Gamma>')[x::=v]\<^sub>\<Gamma>\<^sub>v @ G \<turnstile> i;  i \<Turnstile> ((xa, ba, c) #\<^sub>\<Gamma> \<Gamma>')[x::=v]\<^sub>\<Gamma>\<^sub>v @ G \<rbrakk> \<Longrightarrow>  i(x \<mapsto> s) \<Turnstile> ((xa, ba, c) #\<^sub>\<Gamma> \<Gamma>') @ (x, b, c0) #\<^sub>\<Gamma> G
[PROOF STEP]
hence "is_satis_g (i(x \<mapsto> s)) G"
[PROOF STATE]
proof (prove)
using this:
i \<lbrakk> v \<rbrakk> ~ s
 i(x \<mapsto> s) \<Turnstile> c0
atom x \<sharp> G
 \<Theta> ; \<B>  \<turnstile>\<^sub>w\<^sub>f GNil @ (x, b, c0) #\<^sub>\<Gamma> G
 \<Theta> ; \<B> ; G \<turnstile>\<^sub>w\<^sub>f v : b
 \<Theta> ; GNil[x::=v]\<^sub>\<Gamma>\<^sub>v @ G \<turnstile> i
 i \<Turnstile> GNil[x::=v]\<^sub>\<Gamma>\<^sub>v @ G

goal (1 subgoal):
 1.  i(x \<mapsto> s) \<Turnstile> G
[PROOF STEP]
using is_satis_g_i_upd
[PROOF STATE]
proof (prove)
using this:
i \<lbrakk> v \<rbrakk> ~ s
 i(x \<mapsto> s) \<Turnstile> c0
atom x \<sharp> G
 \<Theta> ; \<B>  \<turnstile>\<^sub>w\<^sub>f GNil @ (x, b, c0) #\<^sub>\<Gamma> G
 \<Theta> ; \<B> ; G \<turnstile>\<^sub>w\<^sub>f v : b
 \<Theta> ; GNil[x::=v]\<^sub>\<Gamma>\<^sub>v @ G \<turnstile> i
 i \<Turnstile> GNil[x::=v]\<^sub>\<Gamma>\<^sub>v @ G
\<lbrakk>atom ?x \<sharp> ?G;  ?i \<Turnstile> ?G \<rbrakk> \<Longrightarrow>  ?i(?x \<mapsto> ?s) \<Turnstile> ?G

goal (1 subgoal):
 1.  i(x \<mapsto> s) \<Turnstile> G
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
 i(x \<mapsto> s) \<Turnstile> G

goal (2 subgoals):
 1. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ;  i(x \<mapsto> s) \<Turnstile> c0 ; atom x \<sharp> G;  \<Theta> ; \<B>  \<turnstile>\<^sub>w\<^sub>f GNil @ (x, b, c0) #\<^sub>\<Gamma> G ;  \<Theta> ; \<B> ; G \<turnstile>\<^sub>w\<^sub>f v : b ;  \<Theta> ; GNil[x::=v]\<^sub>\<Gamma>\<^sub>v @ G \<turnstile> i;  i \<Turnstile> GNil[x::=v]\<^sub>\<Gamma>\<^sub>v @ G \<rbrakk> \<Longrightarrow>  i(x \<mapsto> s) \<Turnstile> GNil @ (x, b, c0) #\<^sub>\<Gamma> G
 2. \<And>xa ba c \<Gamma>'. \<lbrakk>\<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ;  i(x \<mapsto> s) \<Turnstile> c0 ; atom x \<sharp> G;  \<Theta> ; \<B>  \<turnstile>\<^sub>w\<^sub>f \<Gamma>' @ (x, b, c0) #\<^sub>\<Gamma> G ;  \<Theta> ; \<B> ; G \<turnstile>\<^sub>w\<^sub>f v : b ;  \<Theta> ; \<Gamma>'[x::=v]\<^sub>\<Gamma>\<^sub>v @ G \<turnstile> i;  i \<Turnstile> \<Gamma>'[x::=v]\<^sub>\<Gamma>\<^sub>v @ G \<rbrakk> \<Longrightarrow>  i(x \<mapsto> s) \<Turnstile> \<Gamma>' @ (x, b, c0) #\<^sub>\<Gamma> G ; i \<lbrakk> v \<rbrakk> ~ s ;  i(x \<mapsto> s) \<Turnstile> c0 ; atom x \<sharp> G;  \<Theta> ; \<B>  \<turnstile>\<^sub>w\<^sub>f ((xa, ba, c) #\<^sub>\<Gamma> \<Gamma>') @ (x, b, c0) #\<^sub>\<Gamma> G ;  \<Theta> ; \<B> ; G \<turnstile>\<^sub>w\<^sub>f v : b ;  \<Theta> ; ((xa, ba, c) #\<^sub>\<Gamma> \<Gamma>')[x::=v]\<^sub>\<Gamma>\<^sub>v @ G \<turnstile> i;  i \<Turnstile> ((xa, ba, c) #\<^sub>\<Gamma> \<Gamma>')[x::=v]\<^sub>\<Gamma>\<^sub>v @ G \<rbrakk> \<Longrightarrow>  i(x \<mapsto> s) \<Turnstile> ((xa, ba, c) #\<^sub>\<Gamma> \<Gamma>') @ (x, b, c0) #\<^sub>\<Gamma> G
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
 i(x \<mapsto> s) \<Turnstile> G
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
 i(x \<mapsto> s) \<Turnstile> G

goal (1 subgoal):
 1.  i(x \<mapsto> s) \<Turnstile> GNil @ (x, b, c0) #\<^sub>\<Gamma> G
[PROOF STEP]
using GNil
[PROOF STATE]
proof (prove)
using this:
 i(x \<mapsto> s) \<Turnstile> G
i \<lbrakk> v \<rbrakk> ~ s
 i(x \<mapsto> s) \<Turnstile> c0
atom x \<sharp> G
 \<Theta> ; \<B>  \<turnstile>\<^sub>w\<^sub>f GNil @ (x, b, c0) #\<^sub>\<Gamma> G
 \<Theta> ; \<B> ; G \<turnstile>\<^sub>w\<^sub>f v : b
 \<Theta> ; GNil[x::=v]\<^sub>\<Gamma>\<^sub>v @ G \<turnstile> i
 i \<Turnstile> GNil[x::=v]\<^sub>\<Gamma>\<^sub>v @ G

goal (1 subgoal):
 1.  i(x \<mapsto> s) \<Turnstile> GNil @ (x, b, c0) #\<^sub>\<Gamma> G
[PROOF STEP]
using is_satis_g.simps append_g.simps
[PROOF STATE]
proof (prove)
using this:
 i(x \<mapsto> s) \<Turnstile> G
i \<lbrakk> v \<rbrakk> ~ s
 i(x \<mapsto> s) \<Turnstile> c0
atom x \<sharp> G
 \<Theta> ; \<B>  \<turnstile>\<^sub>w\<^sub>f GNil @ (x, b, c0) #\<^sub>\<Gamma> G
 \<Theta> ; \<B> ; G \<turnstile>\<^sub>w\<^sub>f v : b
 \<Theta> ; GNil[x::=v]\<^sub>\<Gamma>\<^sub>v @ G \<turnstile> i
 i \<Turnstile> GNil[x::=v]\<^sub>\<Gamma>\<^sub>v @ G
 ?i \<Turnstile> GNil  = True
 ?i \<Turnstile> (?x, ?b, ?c) #\<^sub>\<Gamma> ?G  = ( ?i \<Turnstile> ?c  \<and>  ?i \<Turnstile> ?G )
GNil @ ?g = ?g
(?xbc #\<^sub>\<Gamma> ?g1.0) @ ?g2.0 = ?xbc #\<^sub>\<Gamma> ?g1.0 @ ?g2.0

goal (1 subgoal):
 1.  i(x \<mapsto> s) \<Turnstile> GNil @ (x, b, c0) #\<^sub>\<Gamma> G
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
 i(x \<mapsto> s) \<Turnstile> GNil @ (x, b, c0) #\<^sub>\<Gamma> G

goal (1 subgoal):
 1. \<And>xa ba c \<Gamma>'. \<lbrakk>\<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ;  i(x \<mapsto> s) \<Turnstile> c0 ; atom x \<sharp> G;  \<Theta> ; \<B>  \<turnstile>\<^sub>w\<^sub>f \<Gamma>' @ (x, b, c0) #\<^sub>\<Gamma> G ;  \<Theta> ; \<B> ; G \<turnstile>\<^sub>w\<^sub>f v : b ;  \<Theta> ; \<Gamma>'[x::=v]\<^sub>\<Gamma>\<^sub>v @ G \<turnstile> i;  i \<Turnstile> \<Gamma>'[x::=v]\<^sub>\<Gamma>\<^sub>v @ G \<rbrakk> \<Longrightarrow>  i(x \<mapsto> s) \<Turnstile> \<Gamma>' @ (x, b, c0) #\<^sub>\<Gamma> G ; i \<lbrakk> v \<rbrakk> ~ s ;  i(x \<mapsto> s) \<Turnstile> c0 ; atom x \<sharp> G;  \<Theta> ; \<B>  \<turnstile>\<^sub>w\<^sub>f ((xa, ba, c) #\<^sub>\<Gamma> \<Gamma>') @ (x, b, c0) #\<^sub>\<Gamma> G ;  \<Theta> ; \<B> ; G \<turnstile>\<^sub>w\<^sub>f v : b ;  \<Theta> ; ((xa, ba, c) #\<^sub>\<Gamma> \<Gamma>')[x::=v]\<^sub>\<Gamma>\<^sub>v @ G \<turnstile> i;  i \<Turnstile> ((xa, ba, c) #\<^sub>\<Gamma> \<Gamma>')[x::=v]\<^sub>\<Gamma>\<^sub>v @ G \<rbrakk> \<Longrightarrow>  i(x \<mapsto> s) \<Turnstile> ((xa, ba, c) #\<^sub>\<Gamma> \<Gamma>') @ (x, b, c0) #\<^sub>\<Gamma> G
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xa ba c \<Gamma>'. \<lbrakk>\<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ;  i(x \<mapsto> s) \<Turnstile> c0 ; atom x \<sharp> G;  \<Theta> ; \<B>  \<turnstile>\<^sub>w\<^sub>f \<Gamma>' @ (x, b, c0) #\<^sub>\<Gamma> G ;  \<Theta> ; \<B> ; G \<turnstile>\<^sub>w\<^sub>f v : b ;  \<Theta> ; \<Gamma>'[x::=v]\<^sub>\<Gamma>\<^sub>v @ G \<turnstile> i;  i \<Turnstile> \<Gamma>'[x::=v]\<^sub>\<Gamma>\<^sub>v @ G \<rbrakk> \<Longrightarrow>  i(x \<mapsto> s) \<Turnstile> \<Gamma>' @ (x, b, c0) #\<^sub>\<Gamma> G ; i \<lbrakk> v \<rbrakk> ~ s ;  i(x \<mapsto> s) \<Turnstile> c0 ; atom x \<sharp> G;  \<Theta> ; \<B>  \<turnstile>\<^sub>w\<^sub>f ((xa, ba, c) #\<^sub>\<Gamma> \<Gamma>') @ (x, b, c0) #\<^sub>\<Gamma> G ;  \<Theta> ; \<B> ; G \<turnstile>\<^sub>w\<^sub>f v : b ;  \<Theta> ; ((xa, ba, c) #\<^sub>\<Gamma> \<Gamma>')[x::=v]\<^sub>\<Gamma>\<^sub>v @ G \<turnstile> i;  i \<Turnstile> ((xa, ba, c) #\<^sub>\<Gamma> \<Gamma>')[x::=v]\<^sub>\<Gamma>\<^sub>v @ G \<rbrakk> \<Longrightarrow>  i(x \<mapsto> s) \<Turnstile> ((xa, ba, c) #\<^sub>\<Gamma> \<Gamma>') @ (x, b, c0) #\<^sub>\<Gamma> G
[PROOF STEP]
case (GCons x' b' c' \<Gamma>')
[PROOF STATE]
proof (state)
this:
\<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ;  i(x \<mapsto> s) \<Turnstile> c0 ; atom x \<sharp> G;  \<Theta> ; \<B>  \<turnstile>\<^sub>w\<^sub>f \<Gamma>' @ (x, b, c0) #\<^sub>\<Gamma> G ;  \<Theta> ; \<B> ; G \<turnstile>\<^sub>w\<^sub>f v : b ;  \<Theta> ; \<Gamma>'[x::=v]\<^sub>\<Gamma>\<^sub>v @ G \<turnstile> i;  i \<Turnstile> \<Gamma>'[x::=v]\<^sub>\<Gamma>\<^sub>v @ G \<rbrakk> \<Longrightarrow>  i(x \<mapsto> s) \<Turnstile> \<Gamma>' @ (x, b, c0) #\<^sub>\<Gamma> G
i \<lbrakk> v \<rbrakk> ~ s
 i(x \<mapsto> s) \<Turnstile> c0
atom x \<sharp> G
 \<Theta> ; \<B>  \<turnstile>\<^sub>w\<^sub>f ((x', b', c') #\<^sub>\<Gamma> \<Gamma>') @ (x, b, c0) #\<^sub>\<Gamma> G
 \<Theta> ; \<B> ; G \<turnstile>\<^sub>w\<^sub>f v : b
 \<Theta> ; ((x', b', c') #\<^sub>\<Gamma> \<Gamma>')[x::=v]\<^sub>\<Gamma>\<^sub>v @ G \<turnstile> i
 i \<Turnstile> ((x', b', c') #\<^sub>\<Gamma> \<Gamma>')[x::=v]\<^sub>\<Gamma>\<^sub>v @ G

goal (1 subgoal):
 1. \<And>xa ba c \<Gamma>'. \<lbrakk>\<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ;  i(x \<mapsto> s) \<Turnstile> c0 ; atom x \<sharp> G;  \<Theta> ; \<B>  \<turnstile>\<^sub>w\<^sub>f \<Gamma>' @ (x, b, c0) #\<^sub>\<Gamma> G ;  \<Theta> ; \<B> ; G \<turnstile>\<^sub>w\<^sub>f v : b ;  \<Theta> ; \<Gamma>'[x::=v]\<^sub>\<Gamma>\<^sub>v @ G \<turnstile> i;  i \<Turnstile> \<Gamma>'[x::=v]\<^sub>\<Gamma>\<^sub>v @ G \<rbrakk> \<Longrightarrow>  i(x \<mapsto> s) \<Turnstile> \<Gamma>' @ (x, b, c0) #\<^sub>\<Gamma> G ; i \<lbrakk> v \<rbrakk> ~ s ;  i(x \<mapsto> s) \<Turnstile> c0 ; atom x \<sharp> G;  \<Theta> ; \<B>  \<turnstile>\<^sub>w\<^sub>f ((xa, ba, c) #\<^sub>\<Gamma> \<Gamma>') @ (x, b, c0) #\<^sub>\<Gamma> G ;  \<Theta> ; \<B> ; G \<turnstile>\<^sub>w\<^sub>f v : b ;  \<Theta> ; ((xa, ba, c) #\<^sub>\<Gamma> \<Gamma>')[x::=v]\<^sub>\<Gamma>\<^sub>v @ G \<turnstile> i;  i \<Turnstile> ((xa, ba, c) #\<^sub>\<Gamma> \<Gamma>')[x::=v]\<^sub>\<Gamma>\<^sub>v @ G \<rbrakk> \<Longrightarrow>  i(x \<mapsto> s) \<Turnstile> ((xa, ba, c) #\<^sub>\<Gamma> \<Gamma>') @ (x, b, c0) #\<^sub>\<Gamma> G
[PROOF STEP]
hence "x\<noteq>x'"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ;  i(x \<mapsto> s) \<Turnstile> c0 ; atom x \<sharp> G;  \<Theta> ; \<B>  \<turnstile>\<^sub>w\<^sub>f \<Gamma>' @ (x, b, c0) #\<^sub>\<Gamma> G ;  \<Theta> ; \<B> ; G \<turnstile>\<^sub>w\<^sub>f v : b ;  \<Theta> ; \<Gamma>'[x::=v]\<^sub>\<Gamma>\<^sub>v @ G \<turnstile> i;  i \<Turnstile> \<Gamma>'[x::=v]\<^sub>\<Gamma>\<^sub>v @ G \<rbrakk> \<Longrightarrow>  i(x \<mapsto> s) \<Turnstile> \<Gamma>' @ (x, b, c0) #\<^sub>\<Gamma> G
i \<lbrakk> v \<rbrakk> ~ s
 i(x \<mapsto> s) \<Turnstile> c0
atom x \<sharp> G
 \<Theta> ; \<B>  \<turnstile>\<^sub>w\<^sub>f ((x', b', c') #\<^sub>\<Gamma> \<Gamma>') @ (x, b, c0) #\<^sub>\<Gamma> G
 \<Theta> ; \<B> ; G \<turnstile>\<^sub>w\<^sub>f v : b
 \<Theta> ; ((x', b', c') #\<^sub>\<Gamma> \<Gamma>')[x::=v]\<^sub>\<Gamma>\<^sub>v @ G \<turnstile> i
 i \<Turnstile> ((x', b', c') #\<^sub>\<Gamma> \<Gamma>')[x::=v]\<^sub>\<Gamma>\<^sub>v @ G

goal (1 subgoal):
 1. x \<noteq> x'
[PROOF STEP]
using wfG_cons_append
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ;  i(x \<mapsto> s) \<Turnstile> c0 ; atom x \<sharp> G;  \<Theta> ; \<B>  \<turnstile>\<^sub>w\<^sub>f \<Gamma>' @ (x, b, c0) #\<^sub>\<Gamma> G ;  \<Theta> ; \<B> ; G \<turnstile>\<^sub>w\<^sub>f v : b ;  \<Theta> ; \<Gamma>'[x::=v]\<^sub>\<Gamma>\<^sub>v @ G \<turnstile> i;  i \<Turnstile> \<Gamma>'[x::=v]\<^sub>\<Gamma>\<^sub>v @ G \<rbrakk> \<Longrightarrow>  i(x \<mapsto> s) \<Turnstile> \<Gamma>' @ (x, b, c0) #\<^sub>\<Gamma> G
i \<lbrakk> v \<rbrakk> ~ s
 i(x \<mapsto> s) \<Turnstile> c0
atom x \<sharp> G
 \<Theta> ; \<B>  \<turnstile>\<^sub>w\<^sub>f ((x', b', c') #\<^sub>\<Gamma> \<Gamma>') @ (x, b, c0) #\<^sub>\<Gamma> G
 \<Theta> ; \<B> ; G \<turnstile>\<^sub>w\<^sub>f v : b
 \<Theta> ; ((x', b', c') #\<^sub>\<Gamma> \<Gamma>')[x::=v]\<^sub>\<Gamma>\<^sub>v @ G \<turnstile> i
 i \<Turnstile> ((x', b', c') #\<^sub>\<Gamma> \<Gamma>')[x::=v]\<^sub>\<Gamma>\<^sub>v @ G
 ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f ((?x', ?b', ?c') #\<^sub>\<Gamma> ?\<Gamma>') @ (?x, ?b, ?c) #\<^sub>\<Gamma> ?\<Gamma>  \<Longrightarrow>  ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f ?\<Gamma>' @ (?x, ?b, ?c) #\<^sub>\<Gamma> ?\<Gamma>  \<and> atom ?x' \<sharp> ?\<Gamma>' @ (?x, ?b, ?c) #\<^sub>\<Gamma> ?\<Gamma> \<and>  ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f ?b'  \<and> ?x' \<noteq> ?x

goal (1 subgoal):
 1. x \<noteq> x'
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
x \<noteq> x'

goal (1 subgoal):
 1. \<And>xa ba c \<Gamma>'. \<lbrakk>\<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ;  i(x \<mapsto> s) \<Turnstile> c0 ; atom x \<sharp> G;  \<Theta> ; \<B>  \<turnstile>\<^sub>w\<^sub>f \<Gamma>' @ (x, b, c0) #\<^sub>\<Gamma> G ;  \<Theta> ; \<B> ; G \<turnstile>\<^sub>w\<^sub>f v : b ;  \<Theta> ; \<Gamma>'[x::=v]\<^sub>\<Gamma>\<^sub>v @ G \<turnstile> i;  i \<Turnstile> \<Gamma>'[x::=v]\<^sub>\<Gamma>\<^sub>v @ G \<rbrakk> \<Longrightarrow>  i(x \<mapsto> s) \<Turnstile> \<Gamma>' @ (x, b, c0) #\<^sub>\<Gamma> G ; i \<lbrakk> v \<rbrakk> ~ s ;  i(x \<mapsto> s) \<Turnstile> c0 ; atom x \<sharp> G;  \<Theta> ; \<B>  \<turnstile>\<^sub>w\<^sub>f ((xa, ba, c) #\<^sub>\<Gamma> \<Gamma>') @ (x, b, c0) #\<^sub>\<Gamma> G ;  \<Theta> ; \<B> ; G \<turnstile>\<^sub>w\<^sub>f v : b ;  \<Theta> ; ((xa, ba, c) #\<^sub>\<Gamma> \<Gamma>')[x::=v]\<^sub>\<Gamma>\<^sub>v @ G \<turnstile> i;  i \<Turnstile> ((xa, ba, c) #\<^sub>\<Gamma> \<Gamma>')[x::=v]\<^sub>\<Gamma>\<^sub>v @ G \<rbrakk> \<Longrightarrow>  i(x \<mapsto> s) \<Turnstile> ((xa, ba, c) #\<^sub>\<Gamma> \<Gamma>') @ (x, b, c0) #\<^sub>\<Gamma> G
[PROOF STEP]
hence "is_satis_g i (((x', b', c'[x::=v]\<^sub>c\<^sub>v) #\<^sub>\<Gamma> (\<Gamma>'[x::=v]\<^sub>\<Gamma>\<^sub>v) @ G))"
[PROOF STATE]
proof (prove)
using this:
x \<noteq> x'

goal (1 subgoal):
 1.  i \<Turnstile> (x', b', c'[x::=v]\<^sub>c\<^sub>v) #\<^sub>\<Gamma> \<Gamma>'[x::=v]\<^sub>\<Gamma>\<^sub>v @ G
[PROOF STEP]
using subst_gv.simps GCons
[PROOF STATE]
proof (prove)
using this:
x \<noteq> x'
GNil[?x::=?v]\<^sub>\<Gamma>\<^sub>v = GNil
((?y, ?b, ?c) #\<^sub>\<Gamma> ?\<Gamma>)[?x::=?v]\<^sub>\<Gamma>\<^sub>v = (if ?x = ?y then ?\<Gamma> else (?y, ?b, ?c[?x::=?v]\<^sub>c\<^sub>v) #\<^sub>\<Gamma> ?\<Gamma>[?x::=?v]\<^sub>\<Gamma>\<^sub>v)
\<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ;  i(x \<mapsto> s) \<Turnstile> c0 ; atom x \<sharp> G;  \<Theta> ; \<B>  \<turnstile>\<^sub>w\<^sub>f \<Gamma>' @ (x, b, c0) #\<^sub>\<Gamma> G ;  \<Theta> ; \<B> ; G \<turnstile>\<^sub>w\<^sub>f v : b ;  \<Theta> ; \<Gamma>'[x::=v]\<^sub>\<Gamma>\<^sub>v @ G \<turnstile> i;  i \<Turnstile> \<Gamma>'[x::=v]\<^sub>\<Gamma>\<^sub>v @ G \<rbrakk> \<Longrightarrow>  i(x \<mapsto> s) \<Turnstile> \<Gamma>' @ (x, b, c0) #\<^sub>\<Gamma> G
i \<lbrakk> v \<rbrakk> ~ s
 i(x \<mapsto> s) \<Turnstile> c0
atom x \<sharp> G
 \<Theta> ; \<B>  \<turnstile>\<^sub>w\<^sub>f ((x', b', c') #\<^sub>\<Gamma> \<Gamma>') @ (x, b, c0) #\<^sub>\<Gamma> G
 \<Theta> ; \<B> ; G \<turnstile>\<^sub>w\<^sub>f v : b
 \<Theta> ; ((x', b', c') #\<^sub>\<Gamma> \<Gamma>')[x::=v]\<^sub>\<Gamma>\<^sub>v @ G \<turnstile> i
 i \<Turnstile> ((x', b', c') #\<^sub>\<Gamma> \<Gamma>')[x::=v]\<^sub>\<Gamma>\<^sub>v @ G

goal (1 subgoal):
 1.  i \<Turnstile> (x', b', c'[x::=v]\<^sub>c\<^sub>v) #\<^sub>\<Gamma> \<Gamma>'[x::=v]\<^sub>\<Gamma>\<^sub>v @ G
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
 i \<Turnstile> (x', b', c'[x::=v]\<^sub>c\<^sub>v) #\<^sub>\<Gamma> \<Gamma>'[x::=v]\<^sub>\<Gamma>\<^sub>v @ G

goal (1 subgoal):
 1. \<And>xa ba c \<Gamma>'. \<lbrakk>\<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ;  i(x \<mapsto> s) \<Turnstile> c0 ; atom x \<sharp> G;  \<Theta> ; \<B>  \<turnstile>\<^sub>w\<^sub>f \<Gamma>' @ (x, b, c0) #\<^sub>\<Gamma> G ;  \<Theta> ; \<B> ; G \<turnstile>\<^sub>w\<^sub>f v : b ;  \<Theta> ; \<Gamma>'[x::=v]\<^sub>\<Gamma>\<^sub>v @ G \<turnstile> i;  i \<Turnstile> \<Gamma>'[x::=v]\<^sub>\<Gamma>\<^sub>v @ G \<rbrakk> \<Longrightarrow>  i(x \<mapsto> s) \<Turnstile> \<Gamma>' @ (x, b, c0) #\<^sub>\<Gamma> G ; i \<lbrakk> v \<rbrakk> ~ s ;  i(x \<mapsto> s) \<Turnstile> c0 ; atom x \<sharp> G;  \<Theta> ; \<B>  \<turnstile>\<^sub>w\<^sub>f ((xa, ba, c) #\<^sub>\<Gamma> \<Gamma>') @ (x, b, c0) #\<^sub>\<Gamma> G ;  \<Theta> ; \<B> ; G \<turnstile>\<^sub>w\<^sub>f v : b ;  \<Theta> ; ((xa, ba, c) #\<^sub>\<Gamma> \<Gamma>')[x::=v]\<^sub>\<Gamma>\<^sub>v @ G \<turnstile> i;  i \<Turnstile> ((xa, ba, c) #\<^sub>\<Gamma> \<Gamma>')[x::=v]\<^sub>\<Gamma>\<^sub>v @ G \<rbrakk> \<Longrightarrow>  i(x \<mapsto> s) \<Turnstile> ((xa, ba, c) #\<^sub>\<Gamma> \<Gamma>') @ (x, b, c0) #\<^sub>\<Gamma> G
[PROOF STEP]
hence *:"is_satis i c'[x::=v]\<^sub>c\<^sub>v \<and> is_satis_g i ((\<Gamma>'[x::=v]\<^sub>\<Gamma>\<^sub>v) @ G)"
[PROOF STATE]
proof (prove)
using this:
 i \<Turnstile> (x', b', c'[x::=v]\<^sub>c\<^sub>v) #\<^sub>\<Gamma> \<Gamma>'[x::=v]\<^sub>\<Gamma>\<^sub>v @ G

goal (1 subgoal):
 1.  i \<Turnstile> c'[x::=v]\<^sub>c\<^sub>v  \<and>  i \<Turnstile> \<Gamma>'[x::=v]\<^sub>\<Gamma>\<^sub>v @ G
[PROOF STEP]
using subst_gv.simps
[PROOF STATE]
proof (prove)
using this:
 i \<Turnstile> (x', b', c'[x::=v]\<^sub>c\<^sub>v) #\<^sub>\<Gamma> \<Gamma>'[x::=v]\<^sub>\<Gamma>\<^sub>v @ G
GNil[?x::=?v]\<^sub>\<Gamma>\<^sub>v = GNil
((?y, ?b, ?c) #\<^sub>\<Gamma> ?\<Gamma>)[?x::=?v]\<^sub>\<Gamma>\<^sub>v = (if ?x = ?y then ?\<Gamma> else (?y, ?b, ?c[?x::=?v]\<^sub>c\<^sub>v) #\<^sub>\<Gamma> ?\<Gamma>[?x::=?v]\<^sub>\<Gamma>\<^sub>v)

goal (1 subgoal):
 1.  i \<Turnstile> c'[x::=v]\<^sub>c\<^sub>v  \<and>  i \<Turnstile> \<Gamma>'[x::=v]\<^sub>\<Gamma>\<^sub>v @ G
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
 i \<Turnstile> c'[x::=v]\<^sub>c\<^sub>v  \<and>  i \<Turnstile> \<Gamma>'[x::=v]\<^sub>\<Gamma>\<^sub>v @ G

goal (1 subgoal):
 1. \<And>xa ba c \<Gamma>'. \<lbrakk>\<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ;  i(x \<mapsto> s) \<Turnstile> c0 ; atom x \<sharp> G;  \<Theta> ; \<B>  \<turnstile>\<^sub>w\<^sub>f \<Gamma>' @ (x, b, c0) #\<^sub>\<Gamma> G ;  \<Theta> ; \<B> ; G \<turnstile>\<^sub>w\<^sub>f v : b ;  \<Theta> ; \<Gamma>'[x::=v]\<^sub>\<Gamma>\<^sub>v @ G \<turnstile> i;  i \<Turnstile> \<Gamma>'[x::=v]\<^sub>\<Gamma>\<^sub>v @ G \<rbrakk> \<Longrightarrow>  i(x \<mapsto> s) \<Turnstile> \<Gamma>' @ (x, b, c0) #\<^sub>\<Gamma> G ; i \<lbrakk> v \<rbrakk> ~ s ;  i(x \<mapsto> s) \<Turnstile> c0 ; atom x \<sharp> G;  \<Theta> ; \<B>  \<turnstile>\<^sub>w\<^sub>f ((xa, ba, c) #\<^sub>\<Gamma> \<Gamma>') @ (x, b, c0) #\<^sub>\<Gamma> G ;  \<Theta> ; \<B> ; G \<turnstile>\<^sub>w\<^sub>f v : b ;  \<Theta> ; ((xa, ba, c) #\<^sub>\<Gamma> \<Gamma>')[x::=v]\<^sub>\<Gamma>\<^sub>v @ G \<turnstile> i;  i \<Turnstile> ((xa, ba, c) #\<^sub>\<Gamma> \<Gamma>')[x::=v]\<^sub>\<Gamma>\<^sub>v @ G \<rbrakk> \<Longrightarrow>  i(x \<mapsto> s) \<Turnstile> ((xa, ba, c) #\<^sub>\<Gamma> \<Gamma>') @ (x, b, c0) #\<^sub>\<Gamma> G
[PROOF STEP]
have "is_satis_g (i(x \<mapsto> s)) ((x', b', c') #\<^sub>\<Gamma> (\<Gamma>'@  (x, b, c0) #\<^sub>\<Gamma> G))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1.  i(x \<mapsto> s) \<Turnstile> (x', b', c') #\<^sub>\<Gamma> \<Gamma>' @ (x, b, c0) #\<^sub>\<Gamma> G
[PROOF STEP]
proof(subst is_satis_g.simps,rule)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1.  i(x \<mapsto> s) \<Turnstile> c'
 2.  i(x \<mapsto> s) \<Turnstile> \<Gamma>' @ (x, b, c0) #\<^sub>\<Gamma> G
[PROOF STEP]
show "is_satis (i(x \<mapsto> s)) c'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1.  i(x \<mapsto> s) \<Turnstile> c'
[PROOF STEP]
proof(subst subst_c_satis_full[symmetric])
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. i \<lbrakk> ?v \<rbrakk> ~ s
 2.  ?\<Theta> ; ?B ; ?\<Gamma>' @ (x, ?b, ?c') #\<^sub>\<Gamma> ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f c'
 3.  ?\<Theta> ; ?\<Gamma>'[x::=?v]\<^sub>\<Gamma>\<^sub>v @ ?\<Gamma> \<turnstile> i
 4.  ?\<Theta> ; ?B ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?v : ?b
 5.  i \<Turnstile> c'[x::=?v]\<^sub>c\<^sub>v
[PROOF STEP]
show \<open>eval_v i v s\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i \<lbrakk> v \<rbrakk> ~ s
[PROOF STEP]
using GCons
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ;  i(x \<mapsto> s) \<Turnstile> c0 ; atom x \<sharp> G;  \<Theta> ; \<B>  \<turnstile>\<^sub>w\<^sub>f \<Gamma>' @ (x, b, c0) #\<^sub>\<Gamma> G ;  \<Theta> ; \<B> ; G \<turnstile>\<^sub>w\<^sub>f v : b ;  \<Theta> ; \<Gamma>'[x::=v]\<^sub>\<Gamma>\<^sub>v @ G \<turnstile> i;  i \<Turnstile> \<Gamma>'[x::=v]\<^sub>\<Gamma>\<^sub>v @ G \<rbrakk> \<Longrightarrow>  i(x \<mapsto> s) \<Turnstile> \<Gamma>' @ (x, b, c0) #\<^sub>\<Gamma> G
i \<lbrakk> v \<rbrakk> ~ s
 i(x \<mapsto> s) \<Turnstile> c0
atom x \<sharp> G
 \<Theta> ; \<B>  \<turnstile>\<^sub>w\<^sub>f ((x', b', c') #\<^sub>\<Gamma> \<Gamma>') @ (x, b, c0) #\<^sub>\<Gamma> G
 \<Theta> ; \<B> ; G \<turnstile>\<^sub>w\<^sub>f v : b
 \<Theta> ; ((x', b', c') #\<^sub>\<Gamma> \<Gamma>')[x::=v]\<^sub>\<Gamma>\<^sub>v @ G \<turnstile> i
 i \<Turnstile> ((x', b', c') #\<^sub>\<Gamma> \<Gamma>')[x::=v]\<^sub>\<Gamma>\<^sub>v @ G

goal (1 subgoal):
 1. i \<lbrakk> v \<rbrakk> ~ s
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
i \<lbrakk> v \<rbrakk> ~ s

goal (4 subgoals):
 1.  ?\<Theta> ; ?B ; ?\<Gamma>' @ (x, ?b, ?c') #\<^sub>\<Gamma> ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f c'
 2.  ?\<Theta> ; ?\<Gamma>'[x::=v]\<^sub>\<Gamma>\<^sub>v @ ?\<Gamma> \<turnstile> i
 3.  ?\<Theta> ; ?B ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f v : ?b
 4.  i \<Turnstile> c'[x::=v]\<^sub>c\<^sub>v
[PROOF STEP]
show \<open> \<Theta> ; \<B> ; ((x', b', c') #\<^sub>\<Gamma>\<Gamma>')@(x, b, c0) #\<^sub>\<Gamma> G \<turnstile>\<^sub>w\<^sub>f c' \<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1.  \<Theta> ; \<B> ; ((x', b', c') #\<^sub>\<Gamma> \<Gamma>') @ (x, b, c0) #\<^sub>\<Gamma> G   \<turnstile>\<^sub>w\<^sub>f c'
[PROOF STEP]
using GCons wfC_refl
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ;  i(x \<mapsto> s) \<Turnstile> c0 ; atom x \<sharp> G;  \<Theta> ; \<B>  \<turnstile>\<^sub>w\<^sub>f \<Gamma>' @ (x, b, c0) #\<^sub>\<Gamma> G ;  \<Theta> ; \<B> ; G \<turnstile>\<^sub>w\<^sub>f v : b ;  \<Theta> ; \<Gamma>'[x::=v]\<^sub>\<Gamma>\<^sub>v @ G \<turnstile> i;  i \<Turnstile> \<Gamma>'[x::=v]\<^sub>\<Gamma>\<^sub>v @ G \<rbrakk> \<Longrightarrow>  i(x \<mapsto> s) \<Turnstile> \<Gamma>' @ (x, b, c0) #\<^sub>\<Gamma> G
i \<lbrakk> v \<rbrakk> ~ s
 i(x \<mapsto> s) \<Turnstile> c0
atom x \<sharp> G
 \<Theta> ; \<B>  \<turnstile>\<^sub>w\<^sub>f ((x', b', c') #\<^sub>\<Gamma> \<Gamma>') @ (x, b, c0) #\<^sub>\<Gamma> G
 \<Theta> ; \<B> ; G \<turnstile>\<^sub>w\<^sub>f v : b
 \<Theta> ; ((x', b', c') #\<^sub>\<Gamma> \<Gamma>')[x::=v]\<^sub>\<Gamma>\<^sub>v @ G \<turnstile> i
 i \<Turnstile> ((x', b', c') #\<^sub>\<Gamma> \<Gamma>')[x::=v]\<^sub>\<Gamma>\<^sub>v @ G
 ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f (?x, ?b', ?c') #\<^sub>\<Gamma> ?\<Gamma>  \<Longrightarrow>  ?\<Theta> ; ?\<B> ; (?x, ?b', ?c') #\<^sub>\<Gamma> ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f ?c'

goal (1 subgoal):
 1.  \<Theta> ; \<B> ; ((x', b', c') #\<^sub>\<Gamma> \<Gamma>') @ (x, b, c0) #\<^sub>\<Gamma> G   \<turnstile>\<^sub>w\<^sub>f c'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
 \<Theta> ; \<B> ; ((x', b', c') #\<^sub>\<Gamma> \<Gamma>') @ (x, b, c0) #\<^sub>\<Gamma> G   \<turnstile>\<^sub>w\<^sub>f c'

goal (3 subgoals):
 1.  \<Theta> ; ((x', b', c') #\<^sub>\<Gamma> \<Gamma>')[x::=v]\<^sub>\<Gamma>\<^sub>v @ G \<turnstile> i
 2.  \<Theta> ; \<B> ; G \<turnstile>\<^sub>w\<^sub>f v : b
 3.  i \<Turnstile> c'[x::=v]\<^sub>c\<^sub>v
[PROOF STEP]
show \<open>wfI \<Theta> ((((x', b', c') #\<^sub>\<Gamma> \<Gamma>')[x::=v]\<^sub>\<Gamma>\<^sub>v) @ G) i\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1.  \<Theta> ; ((x', b', c') #\<^sub>\<Gamma> \<Gamma>')[x::=v]\<^sub>\<Gamma>\<^sub>v @ G \<turnstile> i
[PROOF STEP]
using GCons
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ;  i(x \<mapsto> s) \<Turnstile> c0 ; atom x \<sharp> G;  \<Theta> ; \<B>  \<turnstile>\<^sub>w\<^sub>f \<Gamma>' @ (x, b, c0) #\<^sub>\<Gamma> G ;  \<Theta> ; \<B> ; G \<turnstile>\<^sub>w\<^sub>f v : b ;  \<Theta> ; \<Gamma>'[x::=v]\<^sub>\<Gamma>\<^sub>v @ G \<turnstile> i;  i \<Turnstile> \<Gamma>'[x::=v]\<^sub>\<Gamma>\<^sub>v @ G \<rbrakk> \<Longrightarrow>  i(x \<mapsto> s) \<Turnstile> \<Gamma>' @ (x, b, c0) #\<^sub>\<Gamma> G
i \<lbrakk> v \<rbrakk> ~ s
 i(x \<mapsto> s) \<Turnstile> c0
atom x \<sharp> G
 \<Theta> ; \<B>  \<turnstile>\<^sub>w\<^sub>f ((x', b', c') #\<^sub>\<Gamma> \<Gamma>') @ (x, b, c0) #\<^sub>\<Gamma> G
 \<Theta> ; \<B> ; G \<turnstile>\<^sub>w\<^sub>f v : b
 \<Theta> ; ((x', b', c') #\<^sub>\<Gamma> \<Gamma>')[x::=v]\<^sub>\<Gamma>\<^sub>v @ G \<turnstile> i
 i \<Turnstile> ((x', b', c') #\<^sub>\<Gamma> \<Gamma>')[x::=v]\<^sub>\<Gamma>\<^sub>v @ G

goal (1 subgoal):
 1.  \<Theta> ; ((x', b', c') #\<^sub>\<Gamma> \<Gamma>')[x::=v]\<^sub>\<Gamma>\<^sub>v @ G \<turnstile> i
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
 \<Theta> ; ((x', b', c') #\<^sub>\<Gamma> \<Gamma>')[x::=v]\<^sub>\<Gamma>\<^sub>v @ G \<turnstile> i

goal (2 subgoals):
 1.  \<Theta> ; \<B> ; G \<turnstile>\<^sub>w\<^sub>f v : b
 2.  i \<Turnstile> c'[x::=v]\<^sub>c\<^sub>v
[PROOF STEP]
show \<open> \<Theta> ; \<B> ; G \<turnstile>\<^sub>w\<^sub>f v : b \<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1.  \<Theta> ; \<B> ; G \<turnstile>\<^sub>w\<^sub>f v : b
[PROOF STEP]
using GCons
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ;  i(x \<mapsto> s) \<Turnstile> c0 ; atom x \<sharp> G;  \<Theta> ; \<B>  \<turnstile>\<^sub>w\<^sub>f \<Gamma>' @ (x, b, c0) #\<^sub>\<Gamma> G ;  \<Theta> ; \<B> ; G \<turnstile>\<^sub>w\<^sub>f v : b ;  \<Theta> ; \<Gamma>'[x::=v]\<^sub>\<Gamma>\<^sub>v @ G \<turnstile> i;  i \<Turnstile> \<Gamma>'[x::=v]\<^sub>\<Gamma>\<^sub>v @ G \<rbrakk> \<Longrightarrow>  i(x \<mapsto> s) \<Turnstile> \<Gamma>' @ (x, b, c0) #\<^sub>\<Gamma> G
i \<lbrakk> v \<rbrakk> ~ s
 i(x \<mapsto> s) \<Turnstile> c0
atom x \<sharp> G
 \<Theta> ; \<B>  \<turnstile>\<^sub>w\<^sub>f ((x', b', c') #\<^sub>\<Gamma> \<Gamma>') @ (x, b, c0) #\<^sub>\<Gamma> G
 \<Theta> ; \<B> ; G \<turnstile>\<^sub>w\<^sub>f v : b
 \<Theta> ; ((x', b', c') #\<^sub>\<Gamma> \<Gamma>')[x::=v]\<^sub>\<Gamma>\<^sub>v @ G \<turnstile> i
 i \<Turnstile> ((x', b', c') #\<^sub>\<Gamma> \<Gamma>')[x::=v]\<^sub>\<Gamma>\<^sub>v @ G

goal (1 subgoal):
 1.  \<Theta> ; \<B> ; G \<turnstile>\<^sub>w\<^sub>f v : b
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
 \<Theta> ; \<B> ; G \<turnstile>\<^sub>w\<^sub>f v : b

goal (1 subgoal):
 1.  i \<Turnstile> c'[x::=v]\<^sub>c\<^sub>v
[PROOF STEP]
show \<open>is_satis i c'[x::=v]\<^sub>c\<^sub>v\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1.  i \<Turnstile> c'[x::=v]\<^sub>c\<^sub>v
[PROOF STEP]
using *
[PROOF STATE]
proof (prove)
using this:
 i \<Turnstile> c'[x::=v]\<^sub>c\<^sub>v  \<and>  i \<Turnstile> \<Gamma>'[x::=v]\<^sub>\<Gamma>\<^sub>v @ G

goal (1 subgoal):
 1.  i \<Turnstile> c'[x::=v]\<^sub>c\<^sub>v
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
 i \<Turnstile> c'[x::=v]\<^sub>c\<^sub>v

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
 i(x \<mapsto> s) \<Turnstile> c'

goal (1 subgoal):
 1.  i(x \<mapsto> s) \<Turnstile> \<Gamma>' @ (x, b, c0) #\<^sub>\<Gamma> G
[PROOF STEP]
show "is_satis_g (i(x \<mapsto> s)) (\<Gamma>' @ (x, b, c0) #\<^sub>\<Gamma> G)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1.  i(x \<mapsto> s) \<Turnstile> \<Gamma>' @ (x, b, c0) #\<^sub>\<Gamma> G
[PROOF STEP]
proof(rule  GCons(1))
[PROOF STATE]
proof (state)
goal (7 subgoals):
 1. i \<lbrakk> v \<rbrakk> ~ s
 2.  i(x \<mapsto> s) \<Turnstile> c0
 3. atom x \<sharp> G
 4.  \<Theta> ; \<B>  \<turnstile>\<^sub>w\<^sub>f \<Gamma>' @ (x, b, c0) #\<^sub>\<Gamma> G
 5.  \<Theta> ; \<B> ; G \<turnstile>\<^sub>w\<^sub>f v : b
 6.  \<Theta> ; \<Gamma>'[x::=v]\<^sub>\<Gamma>\<^sub>v @ G \<turnstile> i
 7.  i \<Turnstile> \<Gamma>'[x::=v]\<^sub>\<Gamma>\<^sub>v @ G
[PROOF STEP]
show \<open>eval_v i v s\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i \<lbrakk> v \<rbrakk> ~ s
[PROOF STEP]
using GCons
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ;  i(x \<mapsto> s) \<Turnstile> c0 ; atom x \<sharp> G;  \<Theta> ; \<B>  \<turnstile>\<^sub>w\<^sub>f \<Gamma>' @ (x, b, c0) #\<^sub>\<Gamma> G ;  \<Theta> ; \<B> ; G \<turnstile>\<^sub>w\<^sub>f v : b ;  \<Theta> ; \<Gamma>'[x::=v]\<^sub>\<Gamma>\<^sub>v @ G \<turnstile> i;  i \<Turnstile> \<Gamma>'[x::=v]\<^sub>\<Gamma>\<^sub>v @ G \<rbrakk> \<Longrightarrow>  i(x \<mapsto> s) \<Turnstile> \<Gamma>' @ (x, b, c0) #\<^sub>\<Gamma> G
i \<lbrakk> v \<rbrakk> ~ s
 i(x \<mapsto> s) \<Turnstile> c0
atom x \<sharp> G
 \<Theta> ; \<B>  \<turnstile>\<^sub>w\<^sub>f ((x', b', c') #\<^sub>\<Gamma> \<Gamma>') @ (x, b, c0) #\<^sub>\<Gamma> G
 \<Theta> ; \<B> ; G \<turnstile>\<^sub>w\<^sub>f v : b
 \<Theta> ; ((x', b', c') #\<^sub>\<Gamma> \<Gamma>')[x::=v]\<^sub>\<Gamma>\<^sub>v @ G \<turnstile> i
 i \<Turnstile> ((x', b', c') #\<^sub>\<Gamma> \<Gamma>')[x::=v]\<^sub>\<Gamma>\<^sub>v @ G

goal (1 subgoal):
 1. i \<lbrakk> v \<rbrakk> ~ s
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
i \<lbrakk> v \<rbrakk> ~ s

goal (6 subgoals):
 1.  i(x \<mapsto> s) \<Turnstile> c0
 2. atom x \<sharp> G
 3.  \<Theta> ; \<B>  \<turnstile>\<^sub>w\<^sub>f \<Gamma>' @ (x, b, c0) #\<^sub>\<Gamma> G
 4.  \<Theta> ; \<B> ; G \<turnstile>\<^sub>w\<^sub>f v : b
 5.  \<Theta> ; \<Gamma>'[x::=v]\<^sub>\<Gamma>\<^sub>v @ G \<turnstile> i
 6.  i \<Turnstile> \<Gamma>'[x::=v]\<^sub>\<Gamma>\<^sub>v @ G
[PROOF STEP]
show \<open>is_satis (i(x \<mapsto> s)) c0\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1.  i(x \<mapsto> s) \<Turnstile> c0
[PROOF STEP]
using GCons
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ;  i(x \<mapsto> s) \<Turnstile> c0 ; atom x \<sharp> G;  \<Theta> ; \<B>  \<turnstile>\<^sub>w\<^sub>f \<Gamma>' @ (x, b, c0) #\<^sub>\<Gamma> G ;  \<Theta> ; \<B> ; G \<turnstile>\<^sub>w\<^sub>f v : b ;  \<Theta> ; \<Gamma>'[x::=v]\<^sub>\<Gamma>\<^sub>v @ G \<turnstile> i;  i \<Turnstile> \<Gamma>'[x::=v]\<^sub>\<Gamma>\<^sub>v @ G \<rbrakk> \<Longrightarrow>  i(x \<mapsto> s) \<Turnstile> \<Gamma>' @ (x, b, c0) #\<^sub>\<Gamma> G
i \<lbrakk> v \<rbrakk> ~ s
 i(x \<mapsto> s) \<Turnstile> c0
atom x \<sharp> G
 \<Theta> ; \<B>  \<turnstile>\<^sub>w\<^sub>f ((x', b', c') #\<^sub>\<Gamma> \<Gamma>') @ (x, b, c0) #\<^sub>\<Gamma> G
 \<Theta> ; \<B> ; G \<turnstile>\<^sub>w\<^sub>f v : b
 \<Theta> ; ((x', b', c') #\<^sub>\<Gamma> \<Gamma>')[x::=v]\<^sub>\<Gamma>\<^sub>v @ G \<turnstile> i
 i \<Turnstile> ((x', b', c') #\<^sub>\<Gamma> \<Gamma>')[x::=v]\<^sub>\<Gamma>\<^sub>v @ G

goal (1 subgoal):
 1.  i(x \<mapsto> s) \<Turnstile> c0
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
 i(x \<mapsto> s) \<Turnstile> c0

goal (5 subgoals):
 1. atom x \<sharp> G
 2.  \<Theta> ; \<B>  \<turnstile>\<^sub>w\<^sub>f \<Gamma>' @ (x, b, c0) #\<^sub>\<Gamma> G
 3.  \<Theta> ; \<B> ; G \<turnstile>\<^sub>w\<^sub>f v : b
 4.  \<Theta> ; \<Gamma>'[x::=v]\<^sub>\<Gamma>\<^sub>v @ G \<turnstile> i
 5.  i \<Turnstile> \<Gamma>'[x::=v]\<^sub>\<Gamma>\<^sub>v @ G
[PROOF STEP]
show \<open>atom x \<sharp> G\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. atom x \<sharp> G
[PROOF STEP]
using GCons
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ;  i(x \<mapsto> s) \<Turnstile> c0 ; atom x \<sharp> G;  \<Theta> ; \<B>  \<turnstile>\<^sub>w\<^sub>f \<Gamma>' @ (x, b, c0) #\<^sub>\<Gamma> G ;  \<Theta> ; \<B> ; G \<turnstile>\<^sub>w\<^sub>f v : b ;  \<Theta> ; \<Gamma>'[x::=v]\<^sub>\<Gamma>\<^sub>v @ G \<turnstile> i;  i \<Turnstile> \<Gamma>'[x::=v]\<^sub>\<Gamma>\<^sub>v @ G \<rbrakk> \<Longrightarrow>  i(x \<mapsto> s) \<Turnstile> \<Gamma>' @ (x, b, c0) #\<^sub>\<Gamma> G
i \<lbrakk> v \<rbrakk> ~ s
 i(x \<mapsto> s) \<Turnstile> c0
atom x \<sharp> G
 \<Theta> ; \<B>  \<turnstile>\<^sub>w\<^sub>f ((x', b', c') #\<^sub>\<Gamma> \<Gamma>') @ (x, b, c0) #\<^sub>\<Gamma> G
 \<Theta> ; \<B> ; G \<turnstile>\<^sub>w\<^sub>f v : b
 \<Theta> ; ((x', b', c') #\<^sub>\<Gamma> \<Gamma>')[x::=v]\<^sub>\<Gamma>\<^sub>v @ G \<turnstile> i
 i \<Turnstile> ((x', b', c') #\<^sub>\<Gamma> \<Gamma>')[x::=v]\<^sub>\<Gamma>\<^sub>v @ G

goal (1 subgoal):
 1. atom x \<sharp> G
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
atom x \<sharp> G

goal (4 subgoals):
 1.  \<Theta> ; \<B>  \<turnstile>\<^sub>w\<^sub>f \<Gamma>' @ (x, b, c0) #\<^sub>\<Gamma> G
 2.  \<Theta> ; \<B> ; G \<turnstile>\<^sub>w\<^sub>f v : b
 3.  \<Theta> ; \<Gamma>'[x::=v]\<^sub>\<Gamma>\<^sub>v @ G \<turnstile> i
 4.  i \<Turnstile> \<Gamma>'[x::=v]\<^sub>\<Gamma>\<^sub>v @ G
[PROOF STEP]
show \<open> \<Theta> ; \<B>\<turnstile>\<^sub>w\<^sub>f \<Gamma>' @ (x, b, c0) #\<^sub>\<Gamma> G \<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1.  \<Theta> ; \<B>  \<turnstile>\<^sub>w\<^sub>f \<Gamma>' @ (x, b, c0) #\<^sub>\<Gamma> G
[PROOF STEP]
using GCons wfG_elims append_g.simps
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ;  i(x \<mapsto> s) \<Turnstile> c0 ; atom x \<sharp> G;  \<Theta> ; \<B>  \<turnstile>\<^sub>w\<^sub>f \<Gamma>' @ (x, b, c0) #\<^sub>\<Gamma> G ;  \<Theta> ; \<B> ; G \<turnstile>\<^sub>w\<^sub>f v : b ;  \<Theta> ; \<Gamma>'[x::=v]\<^sub>\<Gamma>\<^sub>v @ G \<turnstile> i;  i \<Turnstile> \<Gamma>'[x::=v]\<^sub>\<Gamma>\<^sub>v @ G \<rbrakk> \<Longrightarrow>  i(x \<mapsto> s) \<Turnstile> \<Gamma>' @ (x, b, c0) #\<^sub>\<Gamma> G
i \<lbrakk> v \<rbrakk> ~ s
 i(x \<mapsto> s) \<Turnstile> c0
atom x \<sharp> G
 \<Theta> ; \<B>  \<turnstile>\<^sub>w\<^sub>f ((x', b', c') #\<^sub>\<Gamma> \<Gamma>') @ (x, b, c0) #\<^sub>\<Gamma> G
 \<Theta> ; \<B> ; G \<turnstile>\<^sub>w\<^sub>f v : b
 \<Theta> ; ((x', b', c') #\<^sub>\<Gamma> \<Gamma>')[x::=v]\<^sub>\<Gamma>\<^sub>v @ G \<turnstile> i
 i \<Turnstile> ((x', b', c') #\<^sub>\<Gamma> \<Gamma>')[x::=v]\<^sub>\<Gamma>\<^sub>v @ G
\<lbrakk> ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f GNil ;    \<turnstile>\<^sub>w\<^sub>f ?\<Theta>  \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk> ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f (?x, ?b, ?c) #\<^sub>\<Gamma> ?\<Gamma> ; \<lbrakk> ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f ?\<Gamma> ; atom ?x \<sharp> ?\<Gamma>;  ?\<Theta> ; ?\<B> ; (?x, ?b, TRUE) #\<^sub>\<Gamma> ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f ?c ;  ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f ?b ; ?c \<noteq> (TRUE); ?c \<noteq> (FALSE)\<rbrakk> \<Longrightarrow> ?P; \<lbrakk>?c = (TRUE) \<or> ?c = (FALSE);  ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f ?\<Gamma> ; atom ?x \<sharp> ?\<Gamma>;  ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f ?b \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk> ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f (?x, ?b, TRUE) #\<^sub>\<Gamma> ?\<Gamma> ; \<lbrakk> ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f ?\<Gamma> ; atom ?x \<sharp> ?\<Gamma>;  ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f ?b \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk> ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f (?x, ?b, FALSE) #\<^sub>\<Gamma> ?\<Gamma> ; \<lbrakk> ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f ?\<Gamma> ; atom ?x \<sharp> ?\<Gamma>;  ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f ?b \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
GNil @ ?g = ?g
(?xbc #\<^sub>\<Gamma> ?g1.0) @ ?g2.0 = ?xbc #\<^sub>\<Gamma> ?g1.0 @ ?g2.0

goal (1 subgoal):
 1.  \<Theta> ; \<B>  \<turnstile>\<^sub>w\<^sub>f \<Gamma>' @ (x, b, c0) #\<^sub>\<Gamma> G
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
 \<Theta> ; \<B>  \<turnstile>\<^sub>w\<^sub>f \<Gamma>' @ (x, b, c0) #\<^sub>\<Gamma> G

goal (3 subgoals):
 1.  \<Theta> ; \<B> ; G \<turnstile>\<^sub>w\<^sub>f v : b
 2.  \<Theta> ; \<Gamma>'[x::=v]\<^sub>\<Gamma>\<^sub>v @ G \<turnstile> i
 3.  i \<Turnstile> \<Gamma>'[x::=v]\<^sub>\<Gamma>\<^sub>v @ G
[PROOF STEP]
show \<open>is_satis_g i (\<Gamma>'[x::=v]\<^sub>\<Gamma>\<^sub>v @ G)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1.  i \<Turnstile> \<Gamma>'[x::=v]\<^sub>\<Gamma>\<^sub>v @ G
[PROOF STEP]
using *
[PROOF STATE]
proof (prove)
using this:
 i \<Turnstile> c'[x::=v]\<^sub>c\<^sub>v  \<and>  i \<Turnstile> \<Gamma>'[x::=v]\<^sub>\<Gamma>\<^sub>v @ G

goal (1 subgoal):
 1.  i \<Turnstile> \<Gamma>'[x::=v]\<^sub>\<Gamma>\<^sub>v @ G
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
 i \<Turnstile> \<Gamma>'[x::=v]\<^sub>\<Gamma>\<^sub>v @ G

goal (2 subgoals):
 1.  \<Theta> ; \<B> ; G \<turnstile>\<^sub>w\<^sub>f v : b
 2.  \<Theta> ; \<Gamma>'[x::=v]\<^sub>\<Gamma>\<^sub>v @ G \<turnstile> i
[PROOF STEP]
show "wfI \<Theta> (\<Gamma>'[x::=v]\<^sub>\<Gamma>\<^sub>v @ G) i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1.  \<Theta> ; \<Gamma>'[x::=v]\<^sub>\<Gamma>\<^sub>v @ G \<turnstile> i
[PROOF STEP]
using GCons wfI_def subst_g_assoc_cons \<open>x\<noteq>x'\<close>
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ;  i(x \<mapsto> s) \<Turnstile> c0 ; atom x \<sharp> G;  \<Theta> ; \<B>  \<turnstile>\<^sub>w\<^sub>f \<Gamma>' @ (x, b, c0) #\<^sub>\<Gamma> G ;  \<Theta> ; \<B> ; G \<turnstile>\<^sub>w\<^sub>f v : b ;  \<Theta> ; \<Gamma>'[x::=v]\<^sub>\<Gamma>\<^sub>v @ G \<turnstile> i;  i \<Turnstile> \<Gamma>'[x::=v]\<^sub>\<Gamma>\<^sub>v @ G \<rbrakk> \<Longrightarrow>  i(x \<mapsto> s) \<Turnstile> \<Gamma>' @ (x, b, c0) #\<^sub>\<Gamma> G
i \<lbrakk> v \<rbrakk> ~ s
 i(x \<mapsto> s) \<Turnstile> c0
atom x \<sharp> G
 \<Theta> ; \<B>  \<turnstile>\<^sub>w\<^sub>f ((x', b', c') #\<^sub>\<Gamma> \<Gamma>') @ (x, b, c0) #\<^sub>\<Gamma> G
 \<Theta> ; \<B> ; G \<turnstile>\<^sub>w\<^sub>f v : b
 \<Theta> ; ((x', b', c') #\<^sub>\<Gamma> \<Gamma>')[x::=v]\<^sub>\<Gamma>\<^sub>v @ G \<turnstile> i
 i \<Turnstile> ((x', b', c') #\<^sub>\<Gamma> \<Gamma>')[x::=v]\<^sub>\<Gamma>\<^sub>v @ G
 ?\<Theta> ; ?\<Gamma> \<turnstile> ?i = (\<forall>(x, b, c)\<in>toSet ?\<Gamma>. \<exists>s. Some s = ?i x \<and>  ?\<Theta>  \<turnstile> s : b)
?x \<noteq> ?x' \<Longrightarrow> ((?x', ?b', ?c') #\<^sub>\<Gamma> ?\<Gamma>')[?x::=?v]\<^sub>\<Gamma>\<^sub>v @ ?G = (?x', ?b', ?c'[?x::=?v]\<^sub>c\<^sub>v) #\<^sub>\<Gamma> ?\<Gamma>'[?x::=?v]\<^sub>\<Gamma>\<^sub>v @ ?G
x \<noteq> x'

goal (1 subgoal):
 1.  \<Theta> ; \<Gamma>'[x::=v]\<^sub>\<Gamma>\<^sub>v @ G \<turnstile> i
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
 \<Theta> ; \<Gamma>'[x::=v]\<^sub>\<Gamma>\<^sub>v @ G \<turnstile> i

goal (1 subgoal):
 1.  \<Theta> ; \<B> ; G \<turnstile>\<^sub>w\<^sub>f v : b
[PROOF STEP]
show "\<Theta> ; \<B> ; G \<turnstile>\<^sub>w\<^sub>f v : b "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1.  \<Theta> ; \<B> ; G \<turnstile>\<^sub>w\<^sub>f v : b
[PROOF STEP]
using GCons
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ;  i(x \<mapsto> s) \<Turnstile> c0 ; atom x \<sharp> G;  \<Theta> ; \<B>  \<turnstile>\<^sub>w\<^sub>f \<Gamma>' @ (x, b, c0) #\<^sub>\<Gamma> G ;  \<Theta> ; \<B> ; G \<turnstile>\<^sub>w\<^sub>f v : b ;  \<Theta> ; \<Gamma>'[x::=v]\<^sub>\<Gamma>\<^sub>v @ G \<turnstile> i;  i \<Turnstile> \<Gamma>'[x::=v]\<^sub>\<Gamma>\<^sub>v @ G \<rbrakk> \<Longrightarrow>  i(x \<mapsto> s) \<Turnstile> \<Gamma>' @ (x, b, c0) #\<^sub>\<Gamma> G
i \<lbrakk> v \<rbrakk> ~ s
 i(x \<mapsto> s) \<Turnstile> c0
atom x \<sharp> G
 \<Theta> ; \<B>  \<turnstile>\<^sub>w\<^sub>f ((x', b', c') #\<^sub>\<Gamma> \<Gamma>') @ (x, b, c0) #\<^sub>\<Gamma> G
 \<Theta> ; \<B> ; G \<turnstile>\<^sub>w\<^sub>f v : b
 \<Theta> ; ((x', b', c') #\<^sub>\<Gamma> \<Gamma>')[x::=v]\<^sub>\<Gamma>\<^sub>v @ G \<turnstile> i
 i \<Turnstile> ((x', b', c') #\<^sub>\<Gamma> \<Gamma>')[x::=v]\<^sub>\<Gamma>\<^sub>v @ G

goal (1 subgoal):
 1.  \<Theta> ; \<B> ; G \<turnstile>\<^sub>w\<^sub>f v : b
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
 \<Theta> ; \<B> ; G \<turnstile>\<^sub>w\<^sub>f v : b

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
 i(x \<mapsto> s) \<Turnstile> \<Gamma>' @ (x, b, c0) #\<^sub>\<Gamma> G

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
 i(x \<mapsto> s) \<Turnstile> (x', b', c') #\<^sub>\<Gamma> \<Gamma>' @ (x, b, c0) #\<^sub>\<Gamma> G

goal (1 subgoal):
 1. \<And>xa ba c \<Gamma>'. \<lbrakk>\<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ;  i(x \<mapsto> s) \<Turnstile> c0 ; atom x \<sharp> G;  \<Theta> ; \<B>  \<turnstile>\<^sub>w\<^sub>f \<Gamma>' @ (x, b, c0) #\<^sub>\<Gamma> G ;  \<Theta> ; \<B> ; G \<turnstile>\<^sub>w\<^sub>f v : b ;  \<Theta> ; \<Gamma>'[x::=v]\<^sub>\<Gamma>\<^sub>v @ G \<turnstile> i;  i \<Turnstile> \<Gamma>'[x::=v]\<^sub>\<Gamma>\<^sub>v @ G \<rbrakk> \<Longrightarrow>  i(x \<mapsto> s) \<Turnstile> \<Gamma>' @ (x, b, c0) #\<^sub>\<Gamma> G ; i \<lbrakk> v \<rbrakk> ~ s ;  i(x \<mapsto> s) \<Turnstile> c0 ; atom x \<sharp> G;  \<Theta> ; \<B>  \<turnstile>\<^sub>w\<^sub>f ((xa, ba, c) #\<^sub>\<Gamma> \<Gamma>') @ (x, b, c0) #\<^sub>\<Gamma> G ;  \<Theta> ; \<B> ; G \<turnstile>\<^sub>w\<^sub>f v : b ;  \<Theta> ; ((xa, ba, c) #\<^sub>\<Gamma> \<Gamma>')[x::=v]\<^sub>\<Gamma>\<^sub>v @ G \<turnstile> i;  i \<Turnstile> ((xa, ba, c) #\<^sub>\<Gamma> \<Gamma>')[x::=v]\<^sub>\<Gamma>\<^sub>v @ G \<rbrakk> \<Longrightarrow>  i(x \<mapsto> s) \<Turnstile> ((xa, ba, c) #\<^sub>\<Gamma> \<Gamma>') @ (x, b, c0) #\<^sub>\<Gamma> G
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
 i(x \<mapsto> s) \<Turnstile> (x', b', c') #\<^sub>\<Gamma> \<Gamma>' @ (x, b, c0) #\<^sub>\<Gamma> G

goal (1 subgoal):
 1. \<And>xa ba c \<Gamma>'. \<lbrakk>\<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ;  i(x \<mapsto> s) \<Turnstile> c0 ; atom x \<sharp> G;  \<Theta> ; \<B>  \<turnstile>\<^sub>w\<^sub>f \<Gamma>' @ (x, b, c0) #\<^sub>\<Gamma> G ;  \<Theta> ; \<B> ; G \<turnstile>\<^sub>w\<^sub>f v : b ;  \<Theta> ; \<Gamma>'[x::=v]\<^sub>\<Gamma>\<^sub>v @ G \<turnstile> i;  i \<Turnstile> \<Gamma>'[x::=v]\<^sub>\<Gamma>\<^sub>v @ G \<rbrakk> \<Longrightarrow>  i(x \<mapsto> s) \<Turnstile> \<Gamma>' @ (x, b, c0) #\<^sub>\<Gamma> G ; i \<lbrakk> v \<rbrakk> ~ s ;  i(x \<mapsto> s) \<Turnstile> c0 ; atom x \<sharp> G;  \<Theta> ; \<B>  \<turnstile>\<^sub>w\<^sub>f ((xa, ba, c) #\<^sub>\<Gamma> \<Gamma>') @ (x, b, c0) #\<^sub>\<Gamma> G ;  \<Theta> ; \<B> ; G \<turnstile>\<^sub>w\<^sub>f v : b ;  \<Theta> ; ((xa, ba, c) #\<^sub>\<Gamma> \<Gamma>')[x::=v]\<^sub>\<Gamma>\<^sub>v @ G \<turnstile> i;  i \<Turnstile> ((xa, ba, c) #\<^sub>\<Gamma> \<Gamma>')[x::=v]\<^sub>\<Gamma>\<^sub>v @ G \<rbrakk> \<Longrightarrow>  i(x \<mapsto> s) \<Turnstile> ((xa, ba, c) #\<^sub>\<Gamma> \<Gamma>') @ (x, b, c0) #\<^sub>\<Gamma> G
[PROOF STEP]
have "((x', b', c') #\<^sub>\<Gamma> \<Gamma>' @ (x, b, c0) #\<^sub>\<Gamma> G) = (((x', b', c') #\<^sub>\<Gamma> \<Gamma>') @ (x, b, c0) #\<^sub>\<Gamma> G)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x', b', c') #\<^sub>\<Gamma> \<Gamma>' @ (x, b, c0) #\<^sub>\<Gamma> G = ((x', b', c') #\<^sub>\<Gamma> \<Gamma>') @ (x, b, c0) #\<^sub>\<Gamma> G
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(x', b', c') #\<^sub>\<Gamma> \<Gamma>' @ (x, b, c0) #\<^sub>\<Gamma> G = ((x', b', c') #\<^sub>\<Gamma> \<Gamma>') @ (x, b, c0) #\<^sub>\<Gamma> G

goal (1 subgoal):
 1. \<And>xa ba c \<Gamma>'. \<lbrakk>\<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ;  i(x \<mapsto> s) \<Turnstile> c0 ; atom x \<sharp> G;  \<Theta> ; \<B>  \<turnstile>\<^sub>w\<^sub>f \<Gamma>' @ (x, b, c0) #\<^sub>\<Gamma> G ;  \<Theta> ; \<B> ; G \<turnstile>\<^sub>w\<^sub>f v : b ;  \<Theta> ; \<Gamma>'[x::=v]\<^sub>\<Gamma>\<^sub>v @ G \<turnstile> i;  i \<Turnstile> \<Gamma>'[x::=v]\<^sub>\<Gamma>\<^sub>v @ G \<rbrakk> \<Longrightarrow>  i(x \<mapsto> s) \<Turnstile> \<Gamma>' @ (x, b, c0) #\<^sub>\<Gamma> G ; i \<lbrakk> v \<rbrakk> ~ s ;  i(x \<mapsto> s) \<Turnstile> c0 ; atom x \<sharp> G;  \<Theta> ; \<B>  \<turnstile>\<^sub>w\<^sub>f ((xa, ba, c) #\<^sub>\<Gamma> \<Gamma>') @ (x, b, c0) #\<^sub>\<Gamma> G ;  \<Theta> ; \<B> ; G \<turnstile>\<^sub>w\<^sub>f v : b ;  \<Theta> ; ((xa, ba, c) #\<^sub>\<Gamma> \<Gamma>')[x::=v]\<^sub>\<Gamma>\<^sub>v @ G \<turnstile> i;  i \<Turnstile> ((xa, ba, c) #\<^sub>\<Gamma> \<Gamma>')[x::=v]\<^sub>\<Gamma>\<^sub>v @ G \<rbrakk> \<Longrightarrow>  i(x \<mapsto> s) \<Turnstile> ((xa, ba, c) #\<^sub>\<Gamma> \<Gamma>') @ (x, b, c0) #\<^sub>\<Gamma> G
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
 i(x \<mapsto> s) \<Turnstile> (x', b', c') #\<^sub>\<Gamma> \<Gamma>' @ (x, b, c0) #\<^sub>\<Gamma> G
(x', b', c') #\<^sub>\<Gamma> \<Gamma>' @ (x, b, c0) #\<^sub>\<Gamma> G = ((x', b', c') #\<^sub>\<Gamma> \<Gamma>') @ (x, b, c0) #\<^sub>\<Gamma> G
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
 i(x \<mapsto> s) \<Turnstile> (x', b', c') #\<^sub>\<Gamma> \<Gamma>' @ (x, b, c0) #\<^sub>\<Gamma> G
(x', b', c') #\<^sub>\<Gamma> \<Gamma>' @ (x, b, c0) #\<^sub>\<Gamma> G = ((x', b', c') #\<^sub>\<Gamma> \<Gamma>') @ (x, b, c0) #\<^sub>\<Gamma> G

goal (1 subgoal):
 1.  i(x \<mapsto> s) \<Turnstile> ((x', b', c') #\<^sub>\<Gamma> \<Gamma>') @ (x, b, c0) #\<^sub>\<Gamma> G
[PROOF STEP]
using GCons
[PROOF STATE]
proof (prove)
using this:
 i(x \<mapsto> s) \<Turnstile> (x', b', c') #\<^sub>\<Gamma> \<Gamma>' @ (x, b, c0) #\<^sub>\<Gamma> G
(x', b', c') #\<^sub>\<Gamma> \<Gamma>' @ (x, b, c0) #\<^sub>\<Gamma> G = ((x', b', c') #\<^sub>\<Gamma> \<Gamma>') @ (x, b, c0) #\<^sub>\<Gamma> G
\<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ;  i(x \<mapsto> s) \<Turnstile> c0 ; atom x \<sharp> G;  \<Theta> ; \<B>  \<turnstile>\<^sub>w\<^sub>f \<Gamma>' @ (x, b, c0) #\<^sub>\<Gamma> G ;  \<Theta> ; \<B> ; G \<turnstile>\<^sub>w\<^sub>f v : b ;  \<Theta> ; \<Gamma>'[x::=v]\<^sub>\<Gamma>\<^sub>v @ G \<turnstile> i;  i \<Turnstile> \<Gamma>'[x::=v]\<^sub>\<Gamma>\<^sub>v @ G \<rbrakk> \<Longrightarrow>  i(x \<mapsto> s) \<Turnstile> \<Gamma>' @ (x, b, c0) #\<^sub>\<Gamma> G
i \<lbrakk> v \<rbrakk> ~ s
 i(x \<mapsto> s) \<Turnstile> c0
atom x \<sharp> G
 \<Theta> ; \<B>  \<turnstile>\<^sub>w\<^sub>f ((x', b', c') #\<^sub>\<Gamma> \<Gamma>') @ (x, b, c0) #\<^sub>\<Gamma> G
 \<Theta> ; \<B> ; G \<turnstile>\<^sub>w\<^sub>f v : b
 \<Theta> ; ((x', b', c') #\<^sub>\<Gamma> \<Gamma>')[x::=v]\<^sub>\<Gamma>\<^sub>v @ G \<turnstile> i
 i \<Turnstile> ((x', b', c') #\<^sub>\<Gamma> \<Gamma>')[x::=v]\<^sub>\<Gamma>\<^sub>v @ G

goal (1 subgoal):
 1.  i(x \<mapsto> s) \<Turnstile> ((x', b', c') #\<^sub>\<Gamma> \<Gamma>') @ (x, b, c0) #\<^sub>\<Gamma> G
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
 i(x \<mapsto> s) \<Turnstile> ((x', b', c') #\<^sub>\<Gamma> \<Gamma>') @ (x, b, c0) #\<^sub>\<Gamma> G

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma monotonic:
  fixes A  :: "(pi \<times> pi) set"
  and   B  :: "(pi \<times> pi) set"
  and   P  :: pi
  and   P' :: pi

  assumes "P \<leadsto>[A] P'"
  and     "A \<subseteq> B"

  shows "P \<leadsto>[B] P'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<leadsto>[B] P'
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
P \<leadsto>[A] P'
A \<subseteq> B

goal (1 subgoal):
 1. P \<leadsto>[B] P'
[PROOF STEP]
by(fastforce simp add: strongSimEarly_def)


[STATEMENT]
lemma freshUnit[simp]:
  fixes y :: name

  shows "y \<sharp> ()"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. y \<sharp> ()
[PROOF STEP]
by(auto simp add: fresh_def supp_unit)


[STATEMENT]
lemma simCasesCont[consumes 1, case_names Bound Free]:
  fixes P   :: pi
  and   Q   :: pi
  and   Rel :: "(pi \<times> pi) set"
  and   C   :: "'a::fs_name"

  assumes Eqvt:  "eqvt Rel"
  and     Bound: "\<And>a y Q'. \<lbrakk>Q \<longmapsto> a<\<nu>y> \<prec> Q'; y \<sharp> P; y \<sharp> Q; y \<sharp> C\<rbrakk> \<Longrightarrow> \<exists>P'. P \<longmapsto> a<\<nu>y> \<prec> P' \<and> (P', Q') \<in> Rel"
  and     Free:  "\<And>\<alpha> Q'. Q \<longmapsto> \<alpha> \<prec> Q' \<Longrightarrow> \<exists>P'. P \<longmapsto> \<alpha> \<prec> P' \<and> (P', Q') \<in> Rel"

  shows "P \<leadsto>[Rel] Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<leadsto>[Rel] Q
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. P \<leadsto>[Rel] Q
[PROOF STEP]
from Free
[PROOF STATE]
proof (chain)
picking this:
Q \<longmapsto> ?\<alpha> \<prec> ?Q' \<Longrightarrow> \<exists>P'. P \<longmapsto> ?\<alpha> \<prec> P' \<and> (P', ?Q') \<in> Rel
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
Q \<longmapsto> ?\<alpha> \<prec> ?Q' \<Longrightarrow> \<exists>P'. P \<longmapsto> ?\<alpha> \<prec> P' \<and> (P', ?Q') \<in> Rel

goal (1 subgoal):
 1. P \<leadsto>[Rel] Q
[PROOF STEP]
proof(auto simp add: strongSimEarly_def)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a y Q'. \<lbrakk>\<And>\<alpha> Q'. Q \<longmapsto> \<alpha> \<prec> Q' \<Longrightarrow> \<exists>P'. P \<longmapsto> \<alpha> \<prec> P' \<and> (P', Q') \<in> Rel; Q \<longmapsto> a<\<nu>y> \<prec> Q'; y \<sharp> P\<rbrakk> \<Longrightarrow> \<exists>P'. P \<longmapsto> a<\<nu>y> \<prec> P' \<and> (P', Q') \<in> Rel
[PROOF STEP]
fix Q' a y
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a y Q'. \<lbrakk>\<And>\<alpha> Q'. Q \<longmapsto> \<alpha> \<prec> Q' \<Longrightarrow> \<exists>P'. P \<longmapsto> \<alpha> \<prec> P' \<and> (P', Q') \<in> Rel; Q \<longmapsto> a<\<nu>y> \<prec> Q'; y \<sharp> P\<rbrakk> \<Longrightarrow> \<exists>P'. P \<longmapsto> a<\<nu>y> \<prec> P' \<and> (P', Q') \<in> Rel
[PROOF STEP]
assume yFreshP: "(y::name) \<sharp> P"
[PROOF STATE]
proof (state)
this:
y \<sharp> P

goal (1 subgoal):
 1. \<And>a y Q'. \<lbrakk>\<And>\<alpha> Q'. Q \<longmapsto> \<alpha> \<prec> Q' \<Longrightarrow> \<exists>P'. P \<longmapsto> \<alpha> \<prec> P' \<and> (P', Q') \<in> Rel; Q \<longmapsto> a<\<nu>y> \<prec> Q'; y \<sharp> P\<rbrakk> \<Longrightarrow> \<exists>P'. P \<longmapsto> a<\<nu>y> \<prec> P' \<and> (P', Q') \<in> Rel
[PROOF STEP]
assume Trans: "Q \<longmapsto> a<\<nu>y> \<prec> Q'"
[PROOF STATE]
proof (state)
this:
Q \<longmapsto> a<\<nu>y> \<prec> Q'

goal (1 subgoal):
 1. \<And>a y Q'. \<lbrakk>\<And>\<alpha> Q'. Q \<longmapsto> \<alpha> \<prec> Q' \<Longrightarrow> \<exists>P'. P \<longmapsto> \<alpha> \<prec> P' \<and> (P', Q') \<in> Rel; Q \<longmapsto> a<\<nu>y> \<prec> Q'; y \<sharp> P\<rbrakk> \<Longrightarrow> \<exists>P'. P \<longmapsto> a<\<nu>y> \<prec> P' \<and> (P', Q') \<in> Rel
[PROOF STEP]
have "\<exists>c::name. c \<sharp> (P, Q', y, Q, C)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>c. c \<sharp> (P, Q', y, Q, C)
[PROOF STEP]
by(blast intro: name_exists_fresh)
[PROOF STATE]
proof (state)
this:
\<exists>c. c \<sharp> (P, Q', y, Q, C)

goal (1 subgoal):
 1. \<And>a y Q'. \<lbrakk>\<And>\<alpha> Q'. Q \<longmapsto> \<alpha> \<prec> Q' \<Longrightarrow> \<exists>P'. P \<longmapsto> \<alpha> \<prec> P' \<and> (P', Q') \<in> Rel; Q \<longmapsto> a<\<nu>y> \<prec> Q'; y \<sharp> P\<rbrakk> \<Longrightarrow> \<exists>P'. P \<longmapsto> a<\<nu>y> \<prec> P' \<and> (P', Q') \<in> Rel
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>c. c \<sharp> (P, Q', y, Q, C)
[PROOF STEP]
obtain c::name where cFreshP: "c \<sharp> P" and cFreshQ': "c \<sharp> Q'" and cFreshC: "c \<sharp> C"
                          and cineqy: "c \<noteq> y" and "c \<sharp> Q"
[PROOF STATE]
proof (prove)
using this:
\<exists>c. c \<sharp> (P, Q', y, Q, C)

goal (1 subgoal):
 1. (\<And>c. \<lbrakk>c \<sharp> P; c \<sharp> Q'; c \<sharp> C; c \<noteq> y; c \<sharp> Q\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(force simp add: fresh_prod name_fresh)
[PROOF STATE]
proof (state)
this:
c \<sharp> P
c \<sharp> Q'
c \<sharp> C
c \<noteq> y
c \<sharp> Q

goal (1 subgoal):
 1. \<And>a y Q'. \<lbrakk>\<And>\<alpha> Q'. Q \<longmapsto> \<alpha> \<prec> Q' \<Longrightarrow> \<exists>P'. P \<longmapsto> \<alpha> \<prec> P' \<and> (P', Q') \<in> Rel; Q \<longmapsto> a<\<nu>y> \<prec> Q'; y \<sharp> P\<rbrakk> \<Longrightarrow> \<exists>P'. P \<longmapsto> a<\<nu>y> \<prec> P' \<and> (P', Q') \<in> Rel
[PROOF STEP]
from Trans cFreshQ'
[PROOF STATE]
proof (chain)
picking this:
Q \<longmapsto> a<\<nu>y> \<prec> Q'
c \<sharp> Q'
[PROOF STEP]
have "Q \<longmapsto> a<\<nu>c> \<prec> ([(y, c)] \<bullet> Q')"
[PROOF STATE]
proof (prove)
using this:
Q \<longmapsto> a<\<nu>y> \<prec> Q'
c \<sharp> Q'

goal (1 subgoal):
 1. Q \<longmapsto> a<\<nu>c> \<prec> ([(y, c)] \<bullet> Q')
[PROOF STEP]
by(simp add: alphaBoundOutput)
[PROOF STATE]
proof (state)
this:
Q \<longmapsto> a<\<nu>c> \<prec> ([(y, c)] \<bullet> Q')

goal (1 subgoal):
 1. \<And>a y Q'. \<lbrakk>\<And>\<alpha> Q'. Q \<longmapsto> \<alpha> \<prec> Q' \<Longrightarrow> \<exists>P'. P \<longmapsto> \<alpha> \<prec> P' \<and> (P', Q') \<in> Rel; Q \<longmapsto> a<\<nu>y> \<prec> Q'; y \<sharp> P\<rbrakk> \<Longrightarrow> \<exists>P'. P \<longmapsto> a<\<nu>y> \<prec> P' \<and> (P', Q') \<in> Rel
[PROOF STEP]
hence "\<exists>P'. P \<longmapsto> a<\<nu>c> \<prec> P' \<and> (P', [(y, c)] \<bullet> Q') \<in> Rel"
[PROOF STATE]
proof (prove)
using this:
Q \<longmapsto> a<\<nu>c> \<prec> ([(y, c)] \<bullet> Q')

goal (1 subgoal):
 1. \<exists>P'. P \<longmapsto> a<\<nu>c> \<prec> P' \<and> (P', [(y, c)] \<bullet> Q') \<in> Rel
[PROOF STEP]
using \<open>c \<sharp> P\<close> \<open>c \<sharp> Q\<close> \<open>c \<sharp> C\<close>
[PROOF STATE]
proof (prove)
using this:
Q \<longmapsto> a<\<nu>c> \<prec> ([(y, c)] \<bullet> Q')
c \<sharp> P
c \<sharp> Q
c \<sharp> C

goal (1 subgoal):
 1. \<exists>P'. P \<longmapsto> a<\<nu>c> \<prec> P' \<and> (P', [(y, c)] \<bullet> Q') \<in> Rel
[PROOF STEP]
by(rule Bound)
[PROOF STATE]
proof (state)
this:
\<exists>P'. P \<longmapsto> a<\<nu>c> \<prec> P' \<and> (P', [(y, c)] \<bullet> Q') \<in> Rel

goal (1 subgoal):
 1. \<And>a y Q'. \<lbrakk>\<And>\<alpha> Q'. Q \<longmapsto> \<alpha> \<prec> Q' \<Longrightarrow> \<exists>P'. P \<longmapsto> \<alpha> \<prec> P' \<and> (P', Q') \<in> Rel; Q \<longmapsto> a<\<nu>y> \<prec> Q'; y \<sharp> P\<rbrakk> \<Longrightarrow> \<exists>P'. P \<longmapsto> a<\<nu>y> \<prec> P' \<and> (P', Q') \<in> Rel
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>P'. P \<longmapsto> a<\<nu>c> \<prec> P' \<and> (P', [(y, c)] \<bullet> Q') \<in> Rel
[PROOF STEP]
obtain P' where PTrans: "P \<longmapsto> a<\<nu>c> \<prec> P'" and P'RelQ': "(P', [(y, c)] \<bullet> Q') \<in> Rel"
[PROOF STATE]
proof (prove)
using this:
\<exists>P'. P \<longmapsto> a<\<nu>c> \<prec> P' \<and> (P', [(y, c)] \<bullet> Q') \<in> Rel

goal (1 subgoal):
 1. (\<And>P'. \<lbrakk>P \<longmapsto> a<\<nu>c> \<prec> P'; (P', [(y, c)] \<bullet> Q') \<in> Rel\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
P \<longmapsto> a<\<nu>c> \<prec> P'
(P', [(y, c)] \<bullet> Q') \<in> Rel

goal (1 subgoal):
 1. \<And>a y Q'. \<lbrakk>\<And>\<alpha> Q'. Q \<longmapsto> \<alpha> \<prec> Q' \<Longrightarrow> \<exists>P'. P \<longmapsto> \<alpha> \<prec> P' \<and> (P', Q') \<in> Rel; Q \<longmapsto> a<\<nu>y> \<prec> Q'; y \<sharp> P\<rbrakk> \<Longrightarrow> \<exists>P'. P \<longmapsto> a<\<nu>y> \<prec> P' \<and> (P', Q') \<in> Rel
[PROOF STEP]
from PTrans yFreshP cineqy
[PROOF STATE]
proof (chain)
picking this:
P \<longmapsto> a<\<nu>c> \<prec> P'
y \<sharp> P
c \<noteq> y
[PROOF STEP]
have yFreshP': "y \<sharp> P'"
[PROOF STATE]
proof (prove)
using this:
P \<longmapsto> a<\<nu>c> \<prec> P'
y \<sharp> P
c \<noteq> y

goal (1 subgoal):
 1. y \<sharp> P'
[PROOF STEP]
by(force intro: freshTransition)
[PROOF STATE]
proof (state)
this:
y \<sharp> P'

goal (1 subgoal):
 1. \<And>a y Q'. \<lbrakk>\<And>\<alpha> Q'. Q \<longmapsto> \<alpha> \<prec> Q' \<Longrightarrow> \<exists>P'. P \<longmapsto> \<alpha> \<prec> P' \<and> (P', Q') \<in> Rel; Q \<longmapsto> a<\<nu>y> \<prec> Q'; y \<sharp> P\<rbrakk> \<Longrightarrow> \<exists>P'. P \<longmapsto> a<\<nu>y> \<prec> P' \<and> (P', Q') \<in> Rel
[PROOF STEP]
with PTrans
[PROOF STATE]
proof (chain)
picking this:
P \<longmapsto> a<\<nu>c> \<prec> P'
y \<sharp> P'
[PROOF STEP]
have "P \<longmapsto> a<\<nu>y> \<prec> ([(y, c)] \<bullet> P')"
[PROOF STATE]
proof (prove)
using this:
P \<longmapsto> a<\<nu>c> \<prec> P'
y \<sharp> P'

goal (1 subgoal):
 1. P \<longmapsto> a<\<nu>y> \<prec> ([(y, c)] \<bullet> P')
[PROOF STEP]
by(simp add: alphaBoundOutput name_swap)
[PROOF STATE]
proof (state)
this:
P \<longmapsto> a<\<nu>y> \<prec> ([(y, c)] \<bullet> P')

goal (1 subgoal):
 1. \<And>a y Q'. \<lbrakk>\<And>\<alpha> Q'. Q \<longmapsto> \<alpha> \<prec> Q' \<Longrightarrow> \<exists>P'. P \<longmapsto> \<alpha> \<prec> P' \<and> (P', Q') \<in> Rel; Q \<longmapsto> a<\<nu>y> \<prec> Q'; y \<sharp> P\<rbrakk> \<Longrightarrow> \<exists>P'. P \<longmapsto> a<\<nu>y> \<prec> P' \<and> (P', Q') \<in> Rel
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
P \<longmapsto> a<\<nu>y> \<prec> ([(y, c)] \<bullet> P')

goal (1 subgoal):
 1. \<And>a y Q'. \<lbrakk>\<And>\<alpha> Q'. Q \<longmapsto> \<alpha> \<prec> Q' \<Longrightarrow> \<exists>P'. P \<longmapsto> \<alpha> \<prec> P' \<and> (P', Q') \<in> Rel; Q \<longmapsto> a<\<nu>y> \<prec> Q'; y \<sharp> P\<rbrakk> \<Longrightarrow> \<exists>P'. P \<longmapsto> a<\<nu>y> \<prec> P' \<and> (P', Q') \<in> Rel
[PROOF STEP]
have "([(y, c)] \<bullet> P', Q') \<in> Rel" (is "?goal")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ([(y, c)] \<bullet> P', Q') \<in> Rel
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ([(y, c)] \<bullet> P', Q') \<in> Rel
[PROOF STEP]
from Eqvt P'RelQ'
[PROOF STATE]
proof (chain)
picking this:
eqvt Rel
(P', [(y, c)] \<bullet> Q') \<in> Rel
[PROOF STEP]
have "([(y, c)] \<bullet> P', [(y, c)] \<bullet> [(y, c)] \<bullet> Q') \<in> Rel"
[PROOF STATE]
proof (prove)
using this:
eqvt Rel
(P', [(y, c)] \<bullet> Q') \<in> Rel

goal (1 subgoal):
 1. ([(y, c)] \<bullet> P', [(y, c)] \<bullet> [(y, c)] \<bullet> Q') \<in> Rel
[PROOF STEP]
by(rule eqvtRelI)
[PROOF STATE]
proof (state)
this:
([(y, c)] \<bullet> P', [(y, c)] \<bullet> [(y, c)] \<bullet> Q') \<in> Rel

goal (1 subgoal):
 1. ([(y, c)] \<bullet> P', Q') \<in> Rel
[PROOF STEP]
with cineqy
[PROOF STATE]
proof (chain)
picking this:
c \<noteq> y
([(y, c)] \<bullet> P', [(y, c)] \<bullet> [(y, c)] \<bullet> Q') \<in> Rel
[PROOF STEP]
show ?goal
[PROOF STATE]
proof (prove)
using this:
c \<noteq> y
([(y, c)] \<bullet> P', [(y, c)] \<bullet> [(y, c)] \<bullet> Q') \<in> Rel

goal (1 subgoal):
 1. ([(y, c)] \<bullet> P', Q') \<in> Rel
[PROOF STEP]
by(simp add: name_calc)
[PROOF STATE]
proof (state)
this:
([(y, c)] \<bullet> P', Q') \<in> Rel

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
([(y, c)] \<bullet> P', Q') \<in> Rel

goal (1 subgoal):
 1. \<And>a y Q'. \<lbrakk>\<And>\<alpha> Q'. Q \<longmapsto> \<alpha> \<prec> Q' \<Longrightarrow> \<exists>P'. P \<longmapsto> \<alpha> \<prec> P' \<and> (P', Q') \<in> Rel; Q \<longmapsto> a<\<nu>y> \<prec> Q'; y \<sharp> P\<rbrakk> \<Longrightarrow> \<exists>P'. P \<longmapsto> a<\<nu>y> \<prec> P' \<and> (P', Q') \<in> Rel
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
P \<longmapsto> a<\<nu>y> \<prec> ([(y, c)] \<bullet> P')
([(y, c)] \<bullet> P', Q') \<in> Rel
[PROOF STEP]
show "\<exists>P'. P \<longmapsto>a<\<nu>y> \<prec> P' \<and> (P', Q') \<in> Rel"
[PROOF STATE]
proof (prove)
using this:
P \<longmapsto> a<\<nu>y> \<prec> ([(y, c)] \<bullet> P')
([(y, c)] \<bullet> P', Q') \<in> Rel

goal (1 subgoal):
 1. \<exists>P'. P \<longmapsto> a<\<nu>y> \<prec> P' \<and> (P', Q') \<in> Rel
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>P'. P \<longmapsto> a<\<nu>y> \<prec> P' \<and> (P', Q') \<in> Rel

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
P \<leadsto>[Rel] Q

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma simCases[consumes 0, case_names Bound Free]:
  fixes P   :: pi
  and   Q   :: pi
  and   Rel :: "(pi \<times> pi) set"
  and   C   :: "'a::fs_name"

  assumes Bound: "\<And>a y Q'. \<lbrakk>Q \<longmapsto> a<\<nu>y> \<prec> Q'; y \<sharp> P\<rbrakk> \<Longrightarrow> \<exists>P'. P \<longmapsto> a<\<nu>y> \<prec> P' \<and> (P', Q') \<in> Rel"
  and     Free:  "\<And>\<alpha> Q'. Q \<longmapsto> \<alpha> \<prec> Q' \<Longrightarrow> \<exists>P'. P \<longmapsto> \<alpha> \<prec> P' \<and> (P', Q') \<in> Rel"

  shows "P \<leadsto>[Rel] Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<leadsto>[Rel] Q
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>Q \<longmapsto> ?a<\<nu>?y> \<prec> ?Q'; ?y \<sharp> P\<rbrakk> \<Longrightarrow> \<exists>P'. P \<longmapsto> ?a<\<nu>?y> \<prec> P' \<and> (P', ?Q') \<in> Rel
Q \<longmapsto> ?\<alpha> \<prec> ?Q' \<Longrightarrow> \<exists>P'. P \<longmapsto> ?\<alpha> \<prec> P' \<and> (P', ?Q') \<in> Rel

goal (1 subgoal):
 1. P \<leadsto>[Rel] Q
[PROOF STEP]
by(auto simp add: strongSimEarly_def)


[STATEMENT]
lemma elim:
  fixes P   :: pi
  and   Rel :: "(pi \<times> pi) set"
  and   Q   :: pi
  and   a   :: name
  and   x   :: name
  and   Q'  :: pi

  assumes "P \<leadsto>[Rel] Q"

  shows "Q \<longmapsto> a<\<nu>x> \<prec> Q' \<Longrightarrow> x \<sharp> P \<Longrightarrow> \<exists>P'. P \<longmapsto> a<\<nu>x> \<prec> P' \<and> (P', Q') \<in> Rel"
  and   "Q \<longmapsto> \<alpha> \<prec> Q' \<Longrightarrow> \<exists>P'. P \<longmapsto> \<alpha> \<prec> P' \<and> (P', Q') \<in> Rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lbrakk>Q \<longmapsto> a<\<nu>x> \<prec> Q'; x \<sharp> P\<rbrakk> \<Longrightarrow> \<exists>P'. P \<longmapsto> a<\<nu>x> \<prec> P' \<and> (P', Q') \<in> Rel) &&& (Q \<longmapsto> \<alpha> \<prec> Q' \<Longrightarrow> \<exists>P'. P \<longmapsto> \<alpha> \<prec> P' \<and> (P', Q') \<in> Rel)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
P \<leadsto>[Rel] Q

goal (1 subgoal):
 1. (\<lbrakk>Q \<longmapsto> a<\<nu>x> \<prec> Q'; x \<sharp> P\<rbrakk> \<Longrightarrow> \<exists>P'. P \<longmapsto> a<\<nu>x> \<prec> P' \<and> (P', Q') \<in> Rel) &&& (Q \<longmapsto> \<alpha> \<prec> Q' \<Longrightarrow> \<exists>P'. P \<longmapsto> \<alpha> \<prec> P' \<and> (P', Q') \<in> Rel)
[PROOF STEP]
by(simp add: strongSimEarly_def)+


[STATEMENT]
lemma eqvtI:
  fixes P    :: pi
  and   Q    :: pi
  and   Rel  :: "(pi \<times> pi) set"
  and   perm :: "name prm"

  assumes Sim: "P \<leadsto>[Rel] Q"
  and     RelRel': "Rel \<subseteq> Rel'"
  and     EqvtRel': "eqvt Rel'"

  shows "(perm \<bullet> P) \<leadsto>[Rel'] (perm \<bullet> Q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. perm \<bullet> P \<leadsto>[Rel'] perm \<bullet> Q
[PROOF STEP]
proof(induct rule: simCases)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>a y Q'. \<lbrakk>perm \<bullet> Q \<longmapsto> a<\<nu>y> \<prec> Q'; y \<sharp> perm \<bullet> P\<rbrakk> \<Longrightarrow> \<exists>P'. perm \<bullet> P \<longmapsto> a<\<nu>y> \<prec> P' \<and> (P', Q') \<in> Rel'
 2. \<And>\<alpha> Q'. perm \<bullet> Q \<longmapsto> \<alpha> \<prec> Q' \<Longrightarrow> \<exists>P'. perm \<bullet> P \<longmapsto> \<alpha> \<prec> P' \<and> (P', Q') \<in> Rel'
[PROOF STEP]
case(Bound a y Q')
[PROOF STATE]
proof (state)
this:
perm \<bullet> Q \<longmapsto> a<\<nu>y> \<prec> Q'
y \<sharp> perm \<bullet> P

goal (2 subgoals):
 1. \<And>a y Q'. \<lbrakk>perm \<bullet> Q \<longmapsto> a<\<nu>y> \<prec> Q'; y \<sharp> perm \<bullet> P\<rbrakk> \<Longrightarrow> \<exists>P'. perm \<bullet> P \<longmapsto> a<\<nu>y> \<prec> P' \<and> (P', Q') \<in> Rel'
 2. \<And>\<alpha> Q'. perm \<bullet> Q \<longmapsto> \<alpha> \<prec> Q' \<Longrightarrow> \<exists>P'. perm \<bullet> P \<longmapsto> \<alpha> \<prec> P' \<and> (P', Q') \<in> Rel'
[PROOF STEP]
have Trans: "(perm \<bullet> Q) \<longmapsto> a<\<nu>y> \<prec> Q'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. perm \<bullet> Q \<longmapsto> a<\<nu>y> \<prec> Q'
[PROOF STEP]
by fact
[PROOF STATE]
proof (state)
this:
perm \<bullet> Q \<longmapsto> a<\<nu>y> \<prec> Q'

goal (2 subgoals):
 1. \<And>a y Q'. \<lbrakk>perm \<bullet> Q \<longmapsto> a<\<nu>y> \<prec> Q'; y \<sharp> perm \<bullet> P\<rbrakk> \<Longrightarrow> \<exists>P'. perm \<bullet> P \<longmapsto> a<\<nu>y> \<prec> P' \<and> (P', Q') \<in> Rel'
 2. \<And>\<alpha> Q'. perm \<bullet> Q \<longmapsto> \<alpha> \<prec> Q' \<Longrightarrow> \<exists>P'. perm \<bullet> P \<longmapsto> \<alpha> \<prec> P' \<and> (P', Q') \<in> Rel'
[PROOF STEP]
have yFreshP: "y \<sharp> perm \<bullet> P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. y \<sharp> perm \<bullet> P
[PROOF STEP]
by fact
[PROOF STATE]
proof (state)
this:
y \<sharp> perm \<bullet> P

goal (2 subgoals):
 1. \<And>a y Q'. \<lbrakk>perm \<bullet> Q \<longmapsto> a<\<nu>y> \<prec> Q'; y \<sharp> perm \<bullet> P\<rbrakk> \<Longrightarrow> \<exists>P'. perm \<bullet> P \<longmapsto> a<\<nu>y> \<prec> P' \<and> (P', Q') \<in> Rel'
 2. \<And>\<alpha> Q'. perm \<bullet> Q \<longmapsto> \<alpha> \<prec> Q' \<Longrightarrow> \<exists>P'. perm \<bullet> P \<longmapsto> \<alpha> \<prec> P' \<and> (P', Q') \<in> Rel'
[PROOF STEP]
from Trans
[PROOF STATE]
proof (chain)
picking this:
perm \<bullet> Q \<longmapsto> a<\<nu>y> \<prec> Q'
[PROOF STEP]
have "(rev perm \<bullet> (perm \<bullet> Q)) \<longmapsto> rev perm \<bullet> (a<\<nu>y> \<prec> Q')"
[PROOF STATE]
proof (prove)
using this:
perm \<bullet> Q \<longmapsto> a<\<nu>y> \<prec> Q'

goal (1 subgoal):
 1. rev perm \<bullet> perm \<bullet> Q \<longmapsto> rev perm \<bullet> a<\<nu>y> \<prec> Q'
[PROOF STEP]
by(rule TransitionsEarly.eqvt)
[PROOF STATE]
proof (state)
this:
rev perm \<bullet> perm \<bullet> Q \<longmapsto> rev perm \<bullet> a<\<nu>y> \<prec> Q'

goal (2 subgoals):
 1. \<And>a y Q'. \<lbrakk>perm \<bullet> Q \<longmapsto> a<\<nu>y> \<prec> Q'; y \<sharp> perm \<bullet> P\<rbrakk> \<Longrightarrow> \<exists>P'. perm \<bullet> P \<longmapsto> a<\<nu>y> \<prec> P' \<and> (P', Q') \<in> Rel'
 2. \<And>\<alpha> Q'. perm \<bullet> Q \<longmapsto> \<alpha> \<prec> Q' \<Longrightarrow> \<exists>P'. perm \<bullet> P \<longmapsto> \<alpha> \<prec> P' \<and> (P', Q') \<in> Rel'
[PROOF STEP]
hence "Q \<longmapsto> (rev perm \<bullet> a)<\<nu>(rev perm \<bullet> y)> \<prec> (rev perm \<bullet> Q')"
[PROOF STATE]
proof (prove)
using this:
rev perm \<bullet> perm \<bullet> Q \<longmapsto> rev perm \<bullet> a<\<nu>y> \<prec> Q'

goal (1 subgoal):
 1. Q \<longmapsto> (rev perm \<bullet> a)<\<nu>(rev perm \<bullet> y)> \<prec> (rev perm \<bullet> Q')
[PROOF STEP]
by(simp add: name_rev_per)
[PROOF STATE]
proof (state)
this:
Q \<longmapsto> (rev perm \<bullet> a)<\<nu>(rev perm \<bullet> y)> \<prec> (rev perm \<bullet> Q')

goal (2 subgoals):
 1. \<And>a y Q'. \<lbrakk>perm \<bullet> Q \<longmapsto> a<\<nu>y> \<prec> Q'; y \<sharp> perm \<bullet> P\<rbrakk> \<Longrightarrow> \<exists>P'. perm \<bullet> P \<longmapsto> a<\<nu>y> \<prec> P' \<and> (P', Q') \<in> Rel'
 2. \<And>\<alpha> Q'. perm \<bullet> Q \<longmapsto> \<alpha> \<prec> Q' \<Longrightarrow> \<exists>P'. perm \<bullet> P \<longmapsto> \<alpha> \<prec> P' \<and> (P', Q') \<in> Rel'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
Q \<longmapsto> (rev perm \<bullet> a)<\<nu>(rev perm \<bullet> y)> \<prec> (rev perm \<bullet> Q')

goal (2 subgoals):
 1. \<And>a y Q'. \<lbrakk>perm \<bullet> Q \<longmapsto> a<\<nu>y> \<prec> Q'; y \<sharp> perm \<bullet> P\<rbrakk> \<Longrightarrow> \<exists>P'. perm \<bullet> P \<longmapsto> a<\<nu>y> \<prec> P' \<and> (P', Q') \<in> Rel'
 2. \<And>\<alpha> Q'. perm \<bullet> Q \<longmapsto> \<alpha> \<prec> Q' \<Longrightarrow> \<exists>P'. perm \<bullet> P \<longmapsto> \<alpha> \<prec> P' \<and> (P', Q') \<in> Rel'
[PROOF STEP]
from yFreshP
[PROOF STATE]
proof (chain)
picking this:
y \<sharp> perm \<bullet> P
[PROOF STEP]
have "(rev perm \<bullet> y) \<sharp> P"
[PROOF STATE]
proof (prove)
using this:
y \<sharp> perm \<bullet> P

goal (1 subgoal):
 1. rev perm \<bullet> y \<sharp> P
[PROOF STEP]
by(simp add: name_fresh_left)
[PROOF STATE]
proof (state)
this:
rev perm \<bullet> y \<sharp> P

goal (2 subgoals):
 1. \<And>a y Q'. \<lbrakk>perm \<bullet> Q \<longmapsto> a<\<nu>y> \<prec> Q'; y \<sharp> perm \<bullet> P\<rbrakk> \<Longrightarrow> \<exists>P'. perm \<bullet> P \<longmapsto> a<\<nu>y> \<prec> P' \<and> (P', Q') \<in> Rel'
 2. \<And>\<alpha> Q'. perm \<bullet> Q \<longmapsto> \<alpha> \<prec> Q' \<Longrightarrow> \<exists>P'. perm \<bullet> P \<longmapsto> \<alpha> \<prec> P' \<and> (P', Q') \<in> Rel'
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
Q \<longmapsto> (rev perm \<bullet> a)<\<nu>(rev perm \<bullet> y)> \<prec> (rev perm \<bullet> Q')
rev perm \<bullet> y \<sharp> P
[PROOF STEP]
have "\<exists>P'. P \<longmapsto> (rev perm \<bullet> a)<\<nu>(rev perm \<bullet> y)> \<prec> P' \<and> (P', rev perm \<bullet> Q') \<in> Rel"
[PROOF STATE]
proof (prove)
using this:
Q \<longmapsto> (rev perm \<bullet> a)<\<nu>(rev perm \<bullet> y)> \<prec> (rev perm \<bullet> Q')
rev perm \<bullet> y \<sharp> P

goal (1 subgoal):
 1. \<exists>P'. P \<longmapsto> (rev perm \<bullet> a)<\<nu>(rev perm \<bullet> y)> \<prec> P' \<and> (P', rev perm \<bullet> Q') \<in> Rel
[PROOF STEP]
using Sim
[PROOF STATE]
proof (prove)
using this:
Q \<longmapsto> (rev perm \<bullet> a)<\<nu>(rev perm \<bullet> y)> \<prec> (rev perm \<bullet> Q')
rev perm \<bullet> y \<sharp> P
P \<leadsto>[Rel] Q

goal (1 subgoal):
 1. \<exists>P'. P \<longmapsto> (rev perm \<bullet> a)<\<nu>(rev perm \<bullet> y)> \<prec> P' \<and> (P', rev perm \<bullet> Q') \<in> Rel
[PROOF STEP]
by(force intro: elim)
[PROOF STATE]
proof (state)
this:
\<exists>P'. P \<longmapsto> (rev perm \<bullet> a)<\<nu>(rev perm \<bullet> y)> \<prec> P' \<and> (P', rev perm \<bullet> Q') \<in> Rel

goal (2 subgoals):
 1. \<And>a y Q'. \<lbrakk>perm \<bullet> Q \<longmapsto> a<\<nu>y> \<prec> Q'; y \<sharp> perm \<bullet> P\<rbrakk> \<Longrightarrow> \<exists>P'. perm \<bullet> P \<longmapsto> a<\<nu>y> \<prec> P' \<and> (P', Q') \<in> Rel'
 2. \<And>\<alpha> Q'. perm \<bullet> Q \<longmapsto> \<alpha> \<prec> Q' \<Longrightarrow> \<exists>P'. perm \<bullet> P \<longmapsto> \<alpha> \<prec> P' \<and> (P', Q') \<in> Rel'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>P'. P \<longmapsto> (rev perm \<bullet> a)<\<nu>(rev perm \<bullet> y)> \<prec> P' \<and> (P', rev perm \<bullet> Q') \<in> Rel
[PROOF STEP]
obtain P' where PTrans: "P \<longmapsto> (rev perm \<bullet> a)<\<nu>(rev perm \<bullet> y)> \<prec> P'" and P'RelQ': "(P', rev perm \<bullet> Q') \<in> Rel"
[PROOF STATE]
proof (prove)
using this:
\<exists>P'. P \<longmapsto> (rev perm \<bullet> a)<\<nu>(rev perm \<bullet> y)> \<prec> P' \<and> (P', rev perm \<bullet> Q') \<in> Rel

goal (1 subgoal):
 1. (\<And>P'. \<lbrakk>P \<longmapsto> (rev perm \<bullet> a)<\<nu>(rev perm \<bullet> y)> \<prec> P'; (P', rev perm \<bullet> Q') \<in> Rel\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
P \<longmapsto> (rev perm \<bullet> a)<\<nu>(rev perm \<bullet> y)> \<prec> P'
(P', rev perm \<bullet> Q') \<in> Rel

goal (2 subgoals):
 1. \<And>a y Q'. \<lbrakk>perm \<bullet> Q \<longmapsto> a<\<nu>y> \<prec> Q'; y \<sharp> perm \<bullet> P\<rbrakk> \<Longrightarrow> \<exists>P'. perm \<bullet> P \<longmapsto> a<\<nu>y> \<prec> P' \<and> (P', Q') \<in> Rel'
 2. \<And>\<alpha> Q'. perm \<bullet> Q \<longmapsto> \<alpha> \<prec> Q' \<Longrightarrow> \<exists>P'. perm \<bullet> P \<longmapsto> \<alpha> \<prec> P' \<and> (P', Q') \<in> Rel'
[PROOF STEP]
from PTrans
[PROOF STATE]
proof (chain)
picking this:
P \<longmapsto> (rev perm \<bullet> a)<\<nu>(rev perm \<bullet> y)> \<prec> P'
[PROOF STEP]
have "(perm \<bullet> P) \<longmapsto> perm \<bullet> ((rev perm \<bullet> a)<\<nu>(rev perm \<bullet> y)> \<prec> P')"
[PROOF STATE]
proof (prove)
using this:
P \<longmapsto> (rev perm \<bullet> a)<\<nu>(rev perm \<bullet> y)> \<prec> P'

goal (1 subgoal):
 1. perm \<bullet> P \<longmapsto> perm \<bullet> (rev perm \<bullet> a)<\<nu>(rev perm \<bullet> y)> \<prec> P'
[PROOF STEP]
by(rule TransitionsEarly.eqvt)
[PROOF STATE]
proof (state)
this:
perm \<bullet> P \<longmapsto> perm \<bullet> (rev perm \<bullet> a)<\<nu>(rev perm \<bullet> y)> \<prec> P'

goal (2 subgoals):
 1. \<And>a y Q'. \<lbrakk>perm \<bullet> Q \<longmapsto> a<\<nu>y> \<prec> Q'; y \<sharp> perm \<bullet> P\<rbrakk> \<Longrightarrow> \<exists>P'. perm \<bullet> P \<longmapsto> a<\<nu>y> \<prec> P' \<and> (P', Q') \<in> Rel'
 2. \<And>\<alpha> Q'. perm \<bullet> Q \<longmapsto> \<alpha> \<prec> Q' \<Longrightarrow> \<exists>P'. perm \<bullet> P \<longmapsto> \<alpha> \<prec> P' \<and> (P', Q') \<in> Rel'
[PROOF STEP]
hence L1: "(perm \<bullet> P) \<longmapsto> a<\<nu>y> \<prec> (perm \<bullet> P')"
[PROOF STATE]
proof (prove)
using this:
perm \<bullet> P \<longmapsto> perm \<bullet> (rev perm \<bullet> a)<\<nu>(rev perm \<bullet> y)> \<prec> P'

goal (1 subgoal):
 1. perm \<bullet> P \<longmapsto> a<\<nu>y> \<prec> (perm \<bullet> P')
[PROOF STEP]
by(simp add: name_per_rev)
[PROOF STATE]
proof (state)
this:
perm \<bullet> P \<longmapsto> a<\<nu>y> \<prec> (perm \<bullet> P')

goal (2 subgoals):
 1. \<And>a y Q'. \<lbrakk>perm \<bullet> Q \<longmapsto> a<\<nu>y> \<prec> Q'; y \<sharp> perm \<bullet> P\<rbrakk> \<Longrightarrow> \<exists>P'. perm \<bullet> P \<longmapsto> a<\<nu>y> \<prec> P' \<and> (P', Q') \<in> Rel'
 2. \<And>\<alpha> Q'. perm \<bullet> Q \<longmapsto> \<alpha> \<prec> Q' \<Longrightarrow> \<exists>P'. perm \<bullet> P \<longmapsto> \<alpha> \<prec> P' \<and> (P', Q') \<in> Rel'
[PROOF STEP]
from P'RelQ' RelRel'
[PROOF STATE]
proof (chain)
picking this:
(P', rev perm \<bullet> Q') \<in> Rel
Rel \<subseteq> Rel'
[PROOF STEP]
have "(P', rev perm \<bullet> Q') \<in> Rel'"
[PROOF STATE]
proof (prove)
using this:
(P', rev perm \<bullet> Q') \<in> Rel
Rel \<subseteq> Rel'

goal (1 subgoal):
 1. (P', rev perm \<bullet> Q') \<in> Rel'
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(P', rev perm \<bullet> Q') \<in> Rel'

goal (2 subgoals):
 1. \<And>a y Q'. \<lbrakk>perm \<bullet> Q \<longmapsto> a<\<nu>y> \<prec> Q'; y \<sharp> perm \<bullet> P\<rbrakk> \<Longrightarrow> \<exists>P'. perm \<bullet> P \<longmapsto> a<\<nu>y> \<prec> P' \<and> (P', Q') \<in> Rel'
 2. \<And>\<alpha> Q'. perm \<bullet> Q \<longmapsto> \<alpha> \<prec> Q' \<Longrightarrow> \<exists>P'. perm \<bullet> P \<longmapsto> \<alpha> \<prec> P' \<and> (P', Q') \<in> Rel'
[PROOF STEP]
with EqvtRel'
[PROOF STATE]
proof (chain)
picking this:
eqvt Rel'
(P', rev perm \<bullet> Q') \<in> Rel'
[PROOF STEP]
have "(perm \<bullet> P', perm \<bullet> (rev perm \<bullet> Q')) \<in> Rel'"
[PROOF STATE]
proof (prove)
using this:
eqvt Rel'
(P', rev perm \<bullet> Q') \<in> Rel'

goal (1 subgoal):
 1. (perm \<bullet> P', perm \<bullet> rev perm \<bullet> Q') \<in> Rel'
[PROOF STEP]
by(rule eqvtRelI)
[PROOF STATE]
proof (state)
this:
(perm \<bullet> P', perm \<bullet> rev perm \<bullet> Q') \<in> Rel'

goal (2 subgoals):
 1. \<And>a y Q'. \<lbrakk>perm \<bullet> Q \<longmapsto> a<\<nu>y> \<prec> Q'; y \<sharp> perm \<bullet> P\<rbrakk> \<Longrightarrow> \<exists>P'. perm \<bullet> P \<longmapsto> a<\<nu>y> \<prec> P' \<and> (P', Q') \<in> Rel'
 2. \<And>\<alpha> Q'. perm \<bullet> Q \<longmapsto> \<alpha> \<prec> Q' \<Longrightarrow> \<exists>P'. perm \<bullet> P \<longmapsto> \<alpha> \<prec> P' \<and> (P', Q') \<in> Rel'
[PROOF STEP]
hence "(perm \<bullet> P', Q') \<in> Rel'"
[PROOF STATE]
proof (prove)
using this:
(perm \<bullet> P', perm \<bullet> rev perm \<bullet> Q') \<in> Rel'

goal (1 subgoal):
 1. (perm \<bullet> P', Q') \<in> Rel'
[PROOF STEP]
by(simp add: name_per_rev)
[PROOF STATE]
proof (state)
this:
(perm \<bullet> P', Q') \<in> Rel'

goal (2 subgoals):
 1. \<And>a y Q'. \<lbrakk>perm \<bullet> Q \<longmapsto> a<\<nu>y> \<prec> Q'; y \<sharp> perm \<bullet> P\<rbrakk> \<Longrightarrow> \<exists>P'. perm \<bullet> P \<longmapsto> a<\<nu>y> \<prec> P' \<and> (P', Q') \<in> Rel'
 2. \<And>\<alpha> Q'. perm \<bullet> Q \<longmapsto> \<alpha> \<prec> Q' \<Longrightarrow> \<exists>P'. perm \<bullet> P \<longmapsto> \<alpha> \<prec> P' \<and> (P', Q') \<in> Rel'
[PROOF STEP]
with L1
[PROOF STATE]
proof (chain)
picking this:
perm \<bullet> P \<longmapsto> a<\<nu>y> \<prec> (perm \<bullet> P')
(perm \<bullet> P', Q') \<in> Rel'
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
perm \<bullet> P \<longmapsto> a<\<nu>y> \<prec> (perm \<bullet> P')
(perm \<bullet> P', Q') \<in> Rel'

goal (1 subgoal):
 1. \<exists>P'. perm \<bullet> P \<longmapsto> a<\<nu>y> \<prec> P' \<and> (P', Q') \<in> Rel'
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>P'. perm \<bullet> P \<longmapsto> a<\<nu>y> \<prec> P' \<and> (P', Q') \<in> Rel'

goal (1 subgoal):
 1. \<And>\<alpha> Q'. perm \<bullet> Q \<longmapsto> \<alpha> \<prec> Q' \<Longrightarrow> \<exists>P'. perm \<bullet> P \<longmapsto> \<alpha> \<prec> P' \<and> (P', Q') \<in> Rel'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>\<alpha> Q'. perm \<bullet> Q \<longmapsto> \<alpha> \<prec> Q' \<Longrightarrow> \<exists>P'. perm \<bullet> P \<longmapsto> \<alpha> \<prec> P' \<and> (P', Q') \<in> Rel'
[PROOF STEP]
case(Free \<alpha> Q')
[PROOF STATE]
proof (state)
this:
perm \<bullet> Q \<longmapsto> \<alpha> \<prec> Q'

goal (1 subgoal):
 1. \<And>\<alpha> Q'. perm \<bullet> Q \<longmapsto> \<alpha> \<prec> Q' \<Longrightarrow> \<exists>P'. perm \<bullet> P \<longmapsto> \<alpha> \<prec> P' \<and> (P', Q') \<in> Rel'
[PROOF STEP]
have Trans: "(perm \<bullet> Q) \<longmapsto> \<alpha> \<prec> Q'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. perm \<bullet> Q \<longmapsto> \<alpha> \<prec> Q'
[PROOF STEP]
by fact
[PROOF STATE]
proof (state)
this:
perm \<bullet> Q \<longmapsto> \<alpha> \<prec> Q'

goal (1 subgoal):
 1. \<And>\<alpha> Q'. perm \<bullet> Q \<longmapsto> \<alpha> \<prec> Q' \<Longrightarrow> \<exists>P'. perm \<bullet> P \<longmapsto> \<alpha> \<prec> P' \<and> (P', Q') \<in> Rel'
[PROOF STEP]
from Trans
[PROOF STATE]
proof (chain)
picking this:
perm \<bullet> Q \<longmapsto> \<alpha> \<prec> Q'
[PROOF STEP]
have "(rev perm \<bullet> (perm \<bullet> Q)) \<longmapsto> rev perm \<bullet> (\<alpha> \<prec> Q')"
[PROOF STATE]
proof (prove)
using this:
perm \<bullet> Q \<longmapsto> \<alpha> \<prec> Q'

goal (1 subgoal):
 1. rev perm \<bullet> perm \<bullet> Q \<longmapsto> rev perm \<bullet> \<alpha> \<prec> Q'
[PROOF STEP]
by(rule TransitionsEarly.eqvt)
[PROOF STATE]
proof (state)
this:
rev perm \<bullet> perm \<bullet> Q \<longmapsto> rev perm \<bullet> \<alpha> \<prec> Q'

goal (1 subgoal):
 1. \<And>\<alpha> Q'. perm \<bullet> Q \<longmapsto> \<alpha> \<prec> Q' \<Longrightarrow> \<exists>P'. perm \<bullet> P \<longmapsto> \<alpha> \<prec> P' \<and> (P', Q') \<in> Rel'
[PROOF STEP]
hence "Q \<longmapsto> (rev perm \<bullet> \<alpha>) \<prec> (rev perm \<bullet> Q')"
[PROOF STATE]
proof (prove)
using this:
rev perm \<bullet> perm \<bullet> Q \<longmapsto> rev perm \<bullet> \<alpha> \<prec> Q'

goal (1 subgoal):
 1. Q \<longmapsto> rev perm \<bullet> \<alpha> \<prec> rev perm \<bullet> Q'
[PROOF STEP]
by(simp add: name_rev_per)
[PROOF STATE]
proof (state)
this:
Q \<longmapsto> rev perm \<bullet> \<alpha> \<prec> rev perm \<bullet> Q'

goal (1 subgoal):
 1. \<And>\<alpha> Q'. perm \<bullet> Q \<longmapsto> \<alpha> \<prec> Q' \<Longrightarrow> \<exists>P'. perm \<bullet> P \<longmapsto> \<alpha> \<prec> P' \<and> (P', Q') \<in> Rel'
[PROOF STEP]
with Sim
[PROOF STATE]
proof (chain)
picking this:
P \<leadsto>[Rel] Q
Q \<longmapsto> rev perm \<bullet> \<alpha> \<prec> rev perm \<bullet> Q'
[PROOF STEP]
have "\<exists>P'. P \<longmapsto> (rev perm \<bullet> \<alpha>) \<prec> P' \<and> (P', (rev perm \<bullet> Q')) \<in> Rel"
[PROOF STATE]
proof (prove)
using this:
P \<leadsto>[Rel] Q
Q \<longmapsto> rev perm \<bullet> \<alpha> \<prec> rev perm \<bullet> Q'

goal (1 subgoal):
 1. \<exists>P'. P \<longmapsto> rev perm \<bullet> \<alpha> \<prec> P' \<and> (P', rev perm \<bullet> Q') \<in> Rel
[PROOF STEP]
by(force intro: elim)
[PROOF STATE]
proof (state)
this:
\<exists>P'. P \<longmapsto> rev perm \<bullet> \<alpha> \<prec> P' \<and> (P', rev perm \<bullet> Q') \<in> Rel

goal (1 subgoal):
 1. \<And>\<alpha> Q'. perm \<bullet> Q \<longmapsto> \<alpha> \<prec> Q' \<Longrightarrow> \<exists>P'. perm \<bullet> P \<longmapsto> \<alpha> \<prec> P' \<and> (P', Q') \<in> Rel'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>P'. P \<longmapsto> rev perm \<bullet> \<alpha> \<prec> P' \<and> (P', rev perm \<bullet> Q') \<in> Rel
[PROOF STEP]
obtain P' where PTrans: "P \<longmapsto> (rev perm \<bullet> \<alpha>) \<prec> P'" and PRel: "(P', (rev perm \<bullet> Q')) \<in> Rel"
[PROOF STATE]
proof (prove)
using this:
\<exists>P'. P \<longmapsto> rev perm \<bullet> \<alpha> \<prec> P' \<and> (P', rev perm \<bullet> Q') \<in> Rel

goal (1 subgoal):
 1. (\<And>P'. \<lbrakk>P \<longmapsto> rev perm \<bullet> \<alpha> \<prec> P'; (P', rev perm \<bullet> Q') \<in> Rel\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
P \<longmapsto> rev perm \<bullet> \<alpha> \<prec> P'
(P', rev perm \<bullet> Q') \<in> Rel

goal (1 subgoal):
 1. \<And>\<alpha> Q'. perm \<bullet> Q \<longmapsto> \<alpha> \<prec> Q' \<Longrightarrow> \<exists>P'. perm \<bullet> P \<longmapsto> \<alpha> \<prec> P' \<and> (P', Q') \<in> Rel'
[PROOF STEP]
from PTrans
[PROOF STATE]
proof (chain)
picking this:
P \<longmapsto> rev perm \<bullet> \<alpha> \<prec> P'
[PROOF STEP]
have "(perm \<bullet> P) \<longmapsto> perm \<bullet> ((rev perm \<bullet> \<alpha>)\<prec> P')"
[PROOF STATE]
proof (prove)
using this:
P \<longmapsto> rev perm \<bullet> \<alpha> \<prec> P'

goal (1 subgoal):
 1. perm \<bullet> P \<longmapsto> perm \<bullet> rev perm \<bullet> \<alpha> \<prec> P'
[PROOF STEP]
by(rule TransitionsEarly.eqvt)
[PROOF STATE]
proof (state)
this:
perm \<bullet> P \<longmapsto> perm \<bullet> rev perm \<bullet> \<alpha> \<prec> P'

goal (1 subgoal):
 1. \<And>\<alpha> Q'. perm \<bullet> Q \<longmapsto> \<alpha> \<prec> Q' \<Longrightarrow> \<exists>P'. perm \<bullet> P \<longmapsto> \<alpha> \<prec> P' \<and> (P', Q') \<in> Rel'
[PROOF STEP]
hence L1: "(perm \<bullet> P) \<longmapsto> \<alpha> \<prec> (perm \<bullet> P')"
[PROOF STATE]
proof (prove)
using this:
perm \<bullet> P \<longmapsto> perm \<bullet> rev perm \<bullet> \<alpha> \<prec> P'

goal (1 subgoal):
 1. perm \<bullet> P \<longmapsto> \<alpha> \<prec> perm \<bullet> P'
[PROOF STEP]
by(simp add: name_per_rev)
[PROOF STATE]
proof (state)
this:
perm \<bullet> P \<longmapsto> \<alpha> \<prec> perm \<bullet> P'

goal (1 subgoal):
 1. \<And>\<alpha> Q'. perm \<bullet> Q \<longmapsto> \<alpha> \<prec> Q' \<Longrightarrow> \<exists>P'. perm \<bullet> P \<longmapsto> \<alpha> \<prec> P' \<and> (P', Q') \<in> Rel'
[PROOF STEP]
from PRel EqvtRel' RelRel'
[PROOF STATE]
proof (chain)
picking this:
(P', rev perm \<bullet> Q') \<in> Rel
eqvt Rel'
Rel \<subseteq> Rel'
[PROOF STEP]
have "((perm \<bullet> P'), (perm \<bullet> (rev perm \<bullet> Q'))) \<in> Rel'"
[PROOF STATE]
proof (prove)
using this:
(P', rev perm \<bullet> Q') \<in> Rel
eqvt Rel'
Rel \<subseteq> Rel'

goal (1 subgoal):
 1. (perm \<bullet> P', perm \<bullet> rev perm \<bullet> Q') \<in> Rel'
[PROOF STEP]
by(force intro: eqvtRelI)
[PROOF STATE]
proof (state)
this:
(perm \<bullet> P', perm \<bullet> rev perm \<bullet> Q') \<in> Rel'

goal (1 subgoal):
 1. \<And>\<alpha> Q'. perm \<bullet> Q \<longmapsto> \<alpha> \<prec> Q' \<Longrightarrow> \<exists>P'. perm \<bullet> P \<longmapsto> \<alpha> \<prec> P' \<and> (P', Q') \<in> Rel'
[PROOF STEP]
hence "((perm \<bullet> P'), Q') \<in> Rel'"
[PROOF STATE]
proof (prove)
using this:
(perm \<bullet> P', perm \<bullet> rev perm \<bullet> Q') \<in> Rel'

goal (1 subgoal):
 1. (perm \<bullet> P', Q') \<in> Rel'
[PROOF STEP]
by(simp add: name_per_rev)
[PROOF STATE]
proof (state)
this:
(perm \<bullet> P', Q') \<in> Rel'

goal (1 subgoal):
 1. \<And>\<alpha> Q'. perm \<bullet> Q \<longmapsto> \<alpha> \<prec> Q' \<Longrightarrow> \<exists>P'. perm \<bullet> P \<longmapsto> \<alpha> \<prec> P' \<and> (P', Q') \<in> Rel'
[PROOF STEP]
with L1
[PROOF STATE]
proof (chain)
picking this:
perm \<bullet> P \<longmapsto> \<alpha> \<prec> perm \<bullet> P'
(perm \<bullet> P', Q') \<in> Rel'
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
perm \<bullet> P \<longmapsto> \<alpha> \<prec> perm \<bullet> P'
(perm \<bullet> P', Q') \<in> Rel'

goal (1 subgoal):
 1. \<exists>P'. perm \<bullet> P \<longmapsto> \<alpha> \<prec> P' \<and> (P', Q') \<in> Rel'
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>P'. perm \<bullet> P \<longmapsto> \<alpha> \<prec> P' \<and> (P', Q') \<in> Rel'

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma reflexive:
  fixes P   :: pi
  and   Rel :: "(pi \<times> pi) set"

  assumes "Id \<subseteq> Rel"

  shows "P \<leadsto>[Rel] P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<leadsto>[Rel] P
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
Id \<subseteq> Rel

goal (1 subgoal):
 1. P \<leadsto>[Rel] P
[PROOF STEP]
by(auto simp add: strongSimEarly_def)