[STATEMENT]
lemma e_append_zeros_length: "e_length (e_append_zeros b z) = e_length b + z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. e_length (e_append_zeros b z) = e_length b + z
[PROOF STEP]
using e_append_def e_append_zeros_def
[PROOF STATE]
proof (prove)
using this:
e_append ?xs ?ys \<equiv> Partial_Recursive.list_encode (Partial_Recursive.list_decode ?xs @ Partial_Recursive.list_decode ?ys)
e_append_zeros ?b ?z \<equiv> e_append ?b (Partial_Recursive.list_encode (replicate ?z 0))

goal (1 subgoal):
 1. e_length (e_append_zeros b z) = e_length b + z
[PROOF STEP]
by simp