equal
deleted
inserted
replaced
400 apply(clarsimp simp add: stables_def split_paired_all) |
400 apply(clarsimp simp add: stables_def split_paired_all) |
401 |
401 |
402 -- "Well-foundedness of the termination relation:" |
402 -- "Well-foundedness of the termination relation:" |
403 apply (rule wf_lex_prod) |
403 apply (rule wf_lex_prod) |
404 apply (insert orderI [THEN acc_le_listI]) |
404 apply (insert orderI [THEN acc_le_listI]) |
405 apply (simp only: acc_def lesssub_def) |
405 apply (simp add: acc_def lesssub_def wfP_wf_eq [symmetric]) |
406 apply (rule wf_finite_psubset) |
406 apply (rule wf_finite_psubset) |
407 |
407 |
408 -- "Loop decreases along termination relation:" |
408 -- "Loop decreases along termination relation:" |
409 apply(simp add: stables_def split_paired_all) |
409 apply(simp add: stables_def split_paired_all) |
410 apply(rename_tac ss w) |
410 apply(rename_tac ss w) |