[STATEMENT]
lemma r_prefixes_0: "eval r_prefixes [0, j] \<down>= list_encode [j]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval r_prefixes [0, j] \<down>= singleton_encode j
[PROOF STEP]
unfolding r_prefixes_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval (Pr 1 r_singleton_encode r_next) [0, j] \<down>= singleton_encode j
[PROOF STEP]
by simp