53 Mcall: |
53 Mcall: |
54 "\<lbrakk> me \<turnstile> (oe,c\<^sub>1) \<Rightarrow> (or,c\<^sub>2); me \<turnstile> (pe,c\<^sub>2) \<Rightarrow> (pr,ve\<^sub>3,sn\<^sub>3); |
54 "\<lbrakk> me \<turnstile> (oe,c\<^sub>1) \<Rightarrow> (or,c\<^sub>2); me \<turnstile> (pe,c\<^sub>2) \<Rightarrow> (pr,ve\<^sub>3,sn\<^sub>3); |
55 ve = (\<lambda>x. null)(''this'' := or, ''param'' := pr); |
55 ve = (\<lambda>x. null)(''this'' := or, ''param'' := pr); |
56 me \<turnstile> (me m,ve,sn\<^sub>3) \<Rightarrow> (r,ve',sn\<^sub>4) \<rbrakk> |
56 me \<turnstile> (me m,ve,sn\<^sub>3) \<Rightarrow> (r,ve',sn\<^sub>4) \<rbrakk> |
57 \<Longrightarrow> |
57 \<Longrightarrow> |
58 me \<turnstile> (oe\<bullet>m<pe>,c\<^sub>1) \<Rightarrow> (r,ve\<^sub>3,sn\<^sub>4)" | |
58 me \<turnstile> (oe\<bullet>m<pe>,c\<^sub>1) \<Rightarrow> (r,ve\<^sub>3,sn\<^sub>4)" for or | |
59 Seq: |
59 Seq: |
60 "\<lbrakk> me \<turnstile> (e\<^sub>1,c\<^sub>1) \<Rightarrow> (r,c\<^sub>2); me \<turnstile> (e\<^sub>2,c\<^sub>2) \<Rightarrow> c\<^sub>3 \<rbrakk> \<Longrightarrow> |
60 "\<lbrakk> me \<turnstile> (e\<^sub>1,c\<^sub>1) \<Rightarrow> (r,c\<^sub>2); me \<turnstile> (e\<^sub>2,c\<^sub>2) \<Rightarrow> c\<^sub>3 \<rbrakk> \<Longrightarrow> |
61 me \<turnstile> (e\<^sub>1; e\<^sub>2,c\<^sub>1) \<Rightarrow> c\<^sub>3" | |
61 me \<turnstile> (e\<^sub>1; e\<^sub>2,c\<^sub>1) \<Rightarrow> c\<^sub>3" | |
62 IfTrue: |
62 IfTrue: |
63 "\<lbrakk> me \<turnstile> (b,c\<^sub>1) \<rightarrow> (True,c\<^sub>2); me \<turnstile> (e\<^sub>1,c\<^sub>2) \<Rightarrow> c\<^sub>3 \<rbrakk> \<Longrightarrow> |
63 "\<lbrakk> me \<turnstile> (b,c\<^sub>1) \<rightarrow> (True,c\<^sub>2); me \<turnstile> (e\<^sub>1,c\<^sub>2) \<Rightarrow> c\<^sub>3 \<rbrakk> \<Longrightarrow> |