equal
deleted
inserted
replaced
79 \<forall> t. t \<noteq> \<langle>l\<bullet> Skip\<rangle>; |
79 \<forall> t. t \<noteq> \<langle>l\<bullet> Skip\<rangle>; |
80 \<forall> C vn c. t \<noteq> \<langle>Try Skip Catch(C vn) c\<rangle>; |
80 \<forall> C vn c. t \<noteq> \<langle>Try Skip Catch(C vn) c\<rangle>; |
81 \<forall> x c. t \<noteq> \<langle>Skip Finally c\<rangle> \<and> xc \<noteq> Xcpt x; |
81 \<forall> x c. t \<noteq> \<langle>Skip Finally c\<rangle> \<and> xc \<noteq> Xcpt x; |
82 \<forall> a c. t \<noteq> \<langle>FinA a c\<rangle>\<rbrakk> |
82 \<forall> a c. t \<noteq> \<langle>FinA a c\<rangle>\<rbrakk> |
83 \<Longrightarrow> |
83 \<Longrightarrow> |
84 G\<turnstile>(t,Some xc,s) \<mapsto>1 (\<langle>Lit arbitrary\<rangle>,Some xc,s)" |
84 G\<turnstile>(t,Some xc,s) \<mapsto>1 (\<langle>Lit undefined\<rangle>,Some xc,s)" |
85 |
85 |
86 | InsInitE: "\<lbrakk>G\<turnstile>(\<langle>c\<rangle>,Norm s) \<mapsto>1 (\<langle>c'\<rangle>, s')\<rbrakk> |
86 | InsInitE: "\<lbrakk>G\<turnstile>(\<langle>c\<rangle>,Norm s) \<mapsto>1 (\<langle>c'\<rangle>, s')\<rbrakk> |
87 \<Longrightarrow> |
87 \<Longrightarrow> |
88 G\<turnstile>(\<langle>InsInitE c e\<rangle>,Norm s) \<mapsto>1 (\<langle>InsInitE c' e\<rangle>, s')" |
88 G\<turnstile>(\<langle>InsInitE c e\<rangle>,Norm s) \<mapsto>1 (\<langle>InsInitE c' e\<rangle>, s')" |
89 |
89 |