[STATEMENT]
lemma bin_lists_len_count: assumes "x \<noteq> y" and "ws \<in> lists {x,y}" shows
  "count_list ws x + count_list ws y = \<^bold>|ws\<^bold>|"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. count_list ws x + count_list ws y = \<^bold>|ws\<^bold>|
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. count_list ws x + count_list ws y = \<^bold>|ws\<^bold>|
[PROOF STEP]
have "finite {x,y}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite {x, y}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
finite {x, y}

goal (1 subgoal):
 1. count_list ws x + count_list ws y = \<^bold>|ws\<^bold>|
[PROOF STEP]
have "set ws \<subseteq> {x,y}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set ws \<subseteq> {x, y}
[PROOF STEP]
using \<open>ws \<in> lists{x,y}\<close>
[PROOF STATE]
proof (prove)
using this:
ws \<in> lists {x, y}

goal (1 subgoal):
 1. set ws \<subseteq> {x, y}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
set ws \<subseteq> {x, y}

goal (1 subgoal):
 1. count_list ws x + count_list ws y = \<^bold>|ws\<^bold>|
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. count_list ws x + count_list ws y = \<^bold>|ws\<^bold>|
[PROOF STEP]
using sum_count_set[OF \<open>set ws \<subseteq> {x,y}\<close> \<open>finite {x,y}\<close>] \<open>x \<noteq> y\<close>
[PROOF STATE]
proof (prove)
using this:
sum (count_list ws) {x, y} = \<^bold>|ws\<^bold>|
x \<noteq> y

goal (1 subgoal):
 1. count_list ws x + count_list ws y = \<^bold>|ws\<^bold>|
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
count_list ws x + count_list ws y = \<^bold>|ws\<^bold>|

goal:
No subgoals!
[PROOF STEP]
qed