[STATEMENT]
lemma r_tl [simp]: "eval r_tl [e] \<down>= e_tl e"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval r_tl [e] \<down>= e_tl e
[PROOF STEP]
unfolding r_tl_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval (let r = Cn 1 r_pdec1 [r_dec] in Cn 1 r_ifz [recf.Id 1 0, Z, Cn 1 r_ifz [r, Z, Cn 1 S [Cn 1 r_prod_encode [Cn 1 r_dec [r], Cn 1 r_pdec22 [r_dec]]]]]) [e] \<down>= e_tl e
[PROOF STEP]
using e_tl_elementary
[PROOF STATE]
proof (prove)
using this:
e_tl ?e = (if ?e = 0 then 0 else if pdec1 (?e - 1) = 0 then 0 else Suc (prod_encode (pdec1 (?e - 1) - 1, pdec22 (?e - 1))))

goal (1 subgoal):
 1. eval (let r = Cn 1 r_pdec1 [r_dec] in Cn 1 r_ifz [recf.Id 1 0, Z, Cn 1 r_ifz [r, Z, Cn 1 S [Cn 1 r_prod_encode [Cn 1 r_dec [r], Cn 1 r_pdec22 [r_dec]]]]]) [e] \<down>= e_tl e
[PROOF STEP]
by (simp add: Let_def)