[STATEMENT]
lemma splitAtRec_notRam:
 "\<And> us. ram \<notin>  set vs \<Longrightarrow> splitAtRec ram us vs = (us @ vs, [])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>us. ram \<notin> set vs \<Longrightarrow> splitAtRec ram us vs = (us @ vs, [])
[PROOF STEP]
proof (induct vs)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>us. ram \<notin> set [] \<Longrightarrow> splitAtRec ram us [] = (us @ [], [])
 2. \<And>a vs us. \<lbrakk>\<And>us. ram \<notin> set vs \<Longrightarrow> splitAtRec ram us vs = (us @ vs, []); ram \<notin> set (a # vs)\<rbrakk> \<Longrightarrow> splitAtRec ram us (a # vs) = (us @ a # vs, [])
[PROOF STEP]
case  Nil
[PROOF STATE]
proof (state)
this:
ram \<notin> set []

goal (2 subgoals):
 1. \<And>us. ram \<notin> set [] \<Longrightarrow> splitAtRec ram us [] = (us @ [], [])
 2. \<And>a vs us. \<lbrakk>\<And>us. ram \<notin> set vs \<Longrightarrow> splitAtRec ram us vs = (us @ vs, []); ram \<notin> set (a # vs)\<rbrakk> \<Longrightarrow> splitAtRec ram us (a # vs) = (us @ a # vs, [])
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ram \<notin> set []
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
ram \<notin> set []

goal (1 subgoal):
 1. splitAtRec ram us [] = (us @ [], [])
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
splitAtRec ram us [] = (us @ [], [])

goal (1 subgoal):
 1. \<And>a vs us. \<lbrakk>\<And>us. ram \<notin> set vs \<Longrightarrow> splitAtRec ram us vs = (us @ vs, []); ram \<notin> set (a # vs)\<rbrakk> \<Longrightarrow> splitAtRec ram us (a # vs) = (us @ a # vs, [])
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a vs us. \<lbrakk>\<And>us. ram \<notin> set vs \<Longrightarrow> splitAtRec ram us vs = (us @ vs, []); ram \<notin> set (a # vs)\<rbrakk> \<Longrightarrow> splitAtRec ram us (a # vs) = (us @ a # vs, [])
[PROOF STEP]
case (Cons v vs)
[PROOF STATE]
proof (state)
this:
ram \<notin> set vs \<Longrightarrow> splitAtRec ram ?us vs = (?us @ vs, [])
ram \<notin> set (v # vs)

goal (1 subgoal):
 1. \<And>a vs us. \<lbrakk>\<And>us. ram \<notin> set vs \<Longrightarrow> splitAtRec ram us vs = (us @ vs, []); ram \<notin> set (a # vs)\<rbrakk> \<Longrightarrow> splitAtRec ram us (a # vs) = (us @ a # vs, [])
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ram \<notin> set vs \<Longrightarrow> splitAtRec ram ?us vs = (?us @ vs, [])
ram \<notin> set (v # vs)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
ram \<notin> set vs \<Longrightarrow> splitAtRec ram ?us vs = (?us @ vs, [])
ram \<notin> set (v # vs)

goal (1 subgoal):
 1. splitAtRec ram us (v # vs) = (us @ v # vs, [])
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
splitAtRec ram us (v # vs) = (us @ v # vs, [])

goal:
No subgoals!
[PROOF STEP]
qed