[STATEMENT]
lemma len_alt: "len x = (LEAST i. x < 2 ^ i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. len x = (LEAST i. x < 2 ^ i)
[PROOF STEP]
proof (rule antisym)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. len x \<le> (LEAST i. x < 2 ^ i)
 2. (LEAST i. x < 2 ^ i) \<le> len x
[PROOF STEP]
show "len x \<le> (LEAST i. x < 2 ^ i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. len x \<le> (LEAST i. x < 2 ^ i)
[PROOF STEP]
unfolding len_le_iff
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x < 2 ^ (LEAST i. x < 2 ^ i)
[PROOF STEP]
by (rule LeastI) (rule less_pow2_len)
[PROOF STATE]
proof (state)
this:
len x \<le> (LEAST i. x < 2 ^ i)

goal (1 subgoal):
 1. (LEAST i. x < 2 ^ i) \<le> len x
[PROOF STEP]
qed (auto intro: Least_le)