equal
deleted
inserted
replaced
122 apply (unfold Blacken_Roots_def) |
122 apply (unfold Blacken_Roots_def) |
123 apply annhoare |
123 apply annhoare |
124 apply(simp_all add:collector_defs Graph_defs) |
124 apply(simp_all add:collector_defs Graph_defs) |
125 apply safe |
125 apply safe |
126 apply(simp_all add:nth_list_update) |
126 apply(simp_all add:nth_list_update) |
127 apply (erule less_SucE) |
|
128 apply simp+ |
|
129 apply (erule less_SucE) |
127 apply (erule less_SucE) |
130 apply simp+ |
128 apply simp+ |
131 apply(drule le_imp_less_or_eq) |
129 apply(drule le_imp_less_or_eq) |
132 apply force |
130 apply force |
133 apply force |
131 apply force |