equal
deleted
inserted
replaced
125 apply clarsimp |
125 apply clarsimp |
126 apply (rename_tac p x ps xs) |
126 apply (rename_tac p x ps xs) |
127 apply (rule iffI) |
127 apply (rule iffI) |
128 apply (rule context_conjI) |
128 apply (rule context_conjI) |
129 apply (subgoal_tac "xs[p := x +_f xs!p] <=[r] xs") |
129 apply (subgoal_tac "xs[p := x +_f xs!p] <=[r] xs") |
130 apply (force dest!: le_listD simp add: nth_list_update) |
130 apply (drule_tac p = p in le_listD) |
|
131 apply simp |
|
132 apply simp |
131 apply (erule subst, rule merges_incr) |
133 apply (erule subst, rule merges_incr) |
132 apply (blast intro!: listE_set intro: closedD listE_length [THEN nth_in]) |
134 apply (blast intro!: listE_set intro: closedD listE_length [THEN nth_in]) |
133 apply clarify |
135 apply clarify |
134 apply (rule conjI) |
136 apply (rule conjI) |
135 apply simp |
137 apply simp |