equal
deleted
inserted
replaced
57 [where P = "\<lambda>s. s ''x'' = \<Sum> {1..s ''y''} \<and> 0 \<le> s ''y'' \<and> s ''y'' \<le> n"]) |
57 [where P = "\<lambda>s. s ''x'' = \<Sum> {1..s ''y''} \<and> 0 \<le> s ''y'' \<and> s ''y'' \<le> n"]) |
58 apply(rule Semi) |
58 apply(rule Semi) |
59 prefer 2 |
59 prefer 2 |
60 apply(rule Assign) |
60 apply(rule Assign) |
61 apply(rule Assign') |
61 apply(rule Assign') |
62 apply(fastsimp simp: atLeastAtMostPlus1_int_conv algebra_simps) |
62 apply(fastforce simp: atLeastAtMostPlus1_int_conv algebra_simps) |
63 apply(fastsimp) |
63 apply(fastforce) |
64 apply(rule Semi) |
64 apply(rule Semi) |
65 prefer 2 |
65 prefer 2 |
66 apply(rule Assign) |
66 apply(rule Assign) |
67 apply(rule Assign') |
67 apply(rule Assign') |
68 apply simp |
68 apply simp |