[STATEMENT]
lemma primerec_getpren[elim]: "\<lbrakk>i < n; n \<le> m\<rbrakk> \<Longrightarrow> primerec (get_fstn_args m n ! i) m"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>i < n; n \<le> m\<rbrakk> \<Longrightarrow> primerec (get_fstn_args m n ! i) m
[PROOF STEP]
apply(induct n, auto simp: get_fstn_args.simps)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>i < n \<Longrightarrow> primerec (get_fstn_args m n ! i) m; i < Suc n; Suc n \<le> m\<rbrakk> \<Longrightarrow> primerec ((get_fstn_args m n @ [recf.id m n]) ! i) m
[PROOF STEP]
apply(cases "i = n", auto simp: nth_append intro: prime_id)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done