42 Proc: "((p,cp,ve)#pe,ve,f) \<turnstile> (c,s) \<Rightarrow> t |
42 Proc: "((p,cp,ve)#pe,ve,f) \<turnstile> (c,s) \<Rightarrow> t |
43 \<Longrightarrow> (pe,ve,f) \<turnstile> ({PROC p = cp;; c}, s) \<Rightarrow> t" |
43 \<Longrightarrow> (pe,ve,f) \<turnstile> ({PROC p = cp;; c}, s) \<Rightarrow> t" |
44 |
44 |
45 code_pred big_step . |
45 code_pred big_step . |
46 |
46 |
47 values "{map t [0,1] |t. ([], \<lambda>n. 0, 0) \<turnstile> (CALL ''p'', nth [42, 43]) \<Rightarrow> t}" |
|
48 |
47 |
49 (* FIXME: syntax *) |
48 values "{map t [0,1] |t. ([], <>, 0) \<turnstile> (CALL ''p'', nth [42, 43]) \<Rightarrow> t}" |
50 values "{map t [0, 1, 2] |t. ([], (\<lambda>_. 3)(''x'' := 0, ''y'' := 1,''z'' := 2), 0) \<turnstile> (test_com, (%_. 0)) \<Rightarrow> t}" |
|
51 |
49 |
|
50 values "{map t [0, 1, 2] |t. |
|
51 ([], <''x'' := 0, ''y'' := 1,''z'' := 2>, 0) |
|
52 \<turnstile> (test_com, <>) \<Rightarrow> t}" |
52 |
53 |
53 end |
54 end |