equal
deleted
inserted
replaced
11 |
11 |
12 subsection {*The Composition of Two Single-Assignment Programs*} |
12 subsection {*The Composition of Two Single-Assignment Programs*} |
13 text{*Thesis Section 4.4.2*} |
13 text{*Thesis Section 4.4.2*} |
14 |
14 |
15 definition FF :: "int program" where |
15 definition FF :: "int program" where |
16 "FF == mk_total_program (UNIV, {range (\<lambda>x. (x, x+1))}, UNIV)" |
16 "FF = mk_total_program (UNIV, {range (\<lambda>x. (x, x+1))}, UNIV)" |
17 |
17 |
18 definition GG :: "int program" where |
18 definition GG :: "int program" where |
19 "GG == mk_total_program (UNIV, {range (\<lambda>x. (x, 2*x))}, UNIV)" |
19 "GG = mk_total_program (UNIV, {range (\<lambda>x. (x, 2*x))}, UNIV)" |
20 |
20 |
21 subsubsection {*Calculating @{term "wens_set FF (atLeast k)"}*} |
21 subsubsection {*Calculating @{term "wens_set FF (atLeast k)"}*} |
22 |
22 |
23 lemma Domain_actFF: "Domain (range (\<lambda>x::int. (x, x + 1))) = UNIV" |
23 lemma Domain_actFF: "Domain (range (\<lambda>x::int. (x, x + 1))) = UNIV" |
24 by force |
24 by force |