220 apply(erule_tac x = "i" in allE) |
220 apply(erule_tac x = "i" in allE) |
221 apply simp |
221 apply simp |
222 apply clarify |
222 apply clarify |
223 apply(rule_tac x = "j" in exI) |
223 apply(rule_tac x = "j" in exI) |
224 apply(case_tac "Suc i<m") |
224 apply(case_tac "Suc i<m") |
225 apply(simp add: nth_append min_def) |
225 apply(simp add: nth_append) |
226 apply(case_tac "R=j") |
226 apply(case_tac "R=j") |
227 apply(simp add: nth_list_update) |
227 apply(simp add: nth_list_update) |
228 apply(case_tac "i=m") |
228 apply(case_tac "i=m") |
229 apply force |
229 apply force |
230 apply(erule_tac x = "i" in allE) |
230 apply(erule_tac x = "i" in allE) |
231 apply force |
231 apply force |
232 apply(force simp add: nth_list_update) |
232 apply(force simp add: nth_list_update) |
233 apply(simp add: nth_append min_def) |
233 apply(simp add: nth_append) |
234 apply(subgoal_tac "i=m - 1") |
234 apply(subgoal_tac "i=m - 1") |
235 prefer 2 apply arith |
235 prefer 2 apply arith |
236 apply(case_tac "R=j") |
236 apply(case_tac "R=j") |
237 apply(erule_tac x = "m - 1" in allE) |
237 apply(erule_tac x = "m - 1" in allE) |
238 apply(simp add: nth_list_update) |
238 apply(simp add: nth_list_update) |