[STATEMENT]
lemma sorted_sublist_wrt_le: \<open>hi \<le> lo \<Longrightarrow> hi < length xs \<Longrightarrow> sorted_sublist_wrt R xs lo hi\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>hi \<le> lo; hi < length xs\<rbrakk> \<Longrightarrow> sorted_sublist_wrt R xs lo hi
[PROOF STEP]
apply (auto simp add: nat_le_eq_or_lt)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>lo < length xs; hi = lo\<rbrakk> \<Longrightarrow> sorted_sublist_wrt R xs lo lo
 2. \<lbrakk>hi < length xs; hi < lo\<rbrakk> \<Longrightarrow> sorted_sublist_wrt R xs lo hi
[PROOF STEP]
unfolding sorted_sublist_wrt_def
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>lo < length xs; hi = lo\<rbrakk> \<Longrightarrow> sorted_wrt R (WB_Sort.sublist xs lo lo)
 2. \<lbrakk>hi < length xs; hi < lo\<rbrakk> \<Longrightarrow> sorted_wrt R (WB_Sort.sublist xs lo hi)
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>lo < length xs; hi = lo\<rbrakk> \<Longrightarrow> sorted_wrt R (WB_Sort.sublist xs lo lo)
[PROOF STEP]
apply (rewrite sublist_single)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>lo < length xs; hi = lo\<rbrakk> \<Longrightarrow> lo < length xs
 2. \<lbrakk>lo < length xs; hi = lo\<rbrakk> \<Longrightarrow> sorted_wrt R [xs ! lo]
[PROOF STEP]
by auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>hi < length xs; hi < lo\<rbrakk> \<Longrightarrow> sorted_wrt R (WB_Sort.sublist xs lo hi)
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>hi < length xs; hi < lo\<rbrakk> \<Longrightarrow> sorted_wrt R (WB_Sort.sublist xs lo hi)
[PROOF STEP]
by (auto simp add: sublist_lt)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done