[STATEMENT]
lemma and_neq_0_is_nth:
  \<open>x AND y \<noteq> 0 \<longleftrightarrow> bit x n\<close> if \<open>y = 2 ^ n\<close> for x y :: \<open>'a::len word\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x AND y \<noteq> 0) = bit x n
[PROOF STEP]
apply (simp add: bit_eq_iff bit_simps)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<exists>n<LENGTH('a). bit x n \<and> bit y n) = bit x n
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
y = 2 ^ n

goal (1 subgoal):
 1. (\<exists>n<LENGTH('a). bit x n \<and> bit y n) = bit x n
[PROOF STEP]
apply (simp add: bit_simps not_le)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. y = 2 ^ n \<Longrightarrow> (n < LENGTH('a) \<and> bit x n \<and> n < LENGTH('a)) = bit x n
[PROOF STEP]
apply transfer
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>y n x. take_bit LENGTH('a) y = take_bit LENGTH('a) (2 ^ n) \<Longrightarrow> (n < LENGTH('a) \<and> (n < LENGTH('a) \<and> bit x n) \<and> n < LENGTH('a)) = (n < LENGTH('a) \<and> bit x n)
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done