[STATEMENT]
lemma r_delay:
  "eval r_delay [i, x] \<down>=
    (if \<exists>j<e_length x. the (eval r_result1 [e_length x, i, e_take (Suc j) x]) > 0
     then Suc (GREATEST j.
        j < e_length x \<and> the (eval r_result1 [e_length x, i, e_take (Suc j) x]) > 0)
     else 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval r_delay [i, x] \<down>= (if \<exists>j<e_length x. 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x]) then Suc (GREATEST j. j < e_length x \<and> 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x])) else 0)
[PROOF STEP]
unfolding r_delay_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval (Cn 2 r_delay_aux [Cn 2 r_length [recf.Id 2 1], recf.Id 2 0, recf.Id 2 1]) [i, x] \<down>= (if \<exists>j<e_length x. 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x]) then Suc (GREATEST j. j < e_length x \<and> 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x])) else 0)
[PROOF STEP]
using r_delay_aux r_delay_aux_prim
[PROOF STATE]
proof (prove)
using this:
?n \<le> e_length ?x \<Longrightarrow> eval r_delay_aux [?n, ?i, ?x] \<down>= (if \<exists>j<?n. 0 < the (eval r_result1 [e_length ?x, ?i, e_take (Suc j) ?x]) then Suc (GREATEST j. j < ?n \<and> 0 < the (eval r_result1 [e_length ?x, ?i, e_take (Suc j) ?x])) else 0)
prim_recfn 3 r_delay_aux

goal (1 subgoal):
 1. eval (Cn 2 r_delay_aux [Cn 2 r_length [recf.Id 2 1], recf.Id 2 0, recf.Id 2 1]) [i, x] \<down>= (if \<exists>j<e_length x. 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x]) then Suc (GREATEST j. j < e_length x \<and> 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x])) else 0)
[PROOF STEP]
by simp