[STATEMENT]
lemma uint8_shiftl_code [code]:
  "Rep_uint8 (uint8_shiftl w n) =
  (if n < 0 \<or> 8 \<le> n then Rep_uint8 (undefined (push_bit :: nat \<Rightarrow> uint8 \<Rightarrow> _) w n)
   else push_bit (nat_of_integer n) (Rep_uint8 w))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Rep_uint8 (uint8_shiftl w n) = (if n < 0 \<or> 8 \<le> n then Rep_uint8 (undefined push_bit w n) else push_bit (nat_of_integer n) (Rep_uint8 w))
[PROOF STEP]
including undefined_transfer
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Rep_uint8 (uint8_shiftl w n) = (if n < 0 \<or> 8 \<le> n then Rep_uint8 (undefined push_bit w n) else push_bit (nat_of_integer n) (Rep_uint8 w))
[PROOF STEP]
unfolding uint8_shiftl_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Rep_uint8 (if n < 0 \<or> 8 \<le> n then undefined push_bit w n else push_bit (nat_of_integer n) w) = (if n < 0 \<or> 8 \<le> n then Rep_uint8 (undefined push_bit w n) else push_bit (nat_of_integer n) (Rep_uint8 w))
[PROOF STEP]
by transfer simp