[STATEMENT]
lemma aux4[rule_format]: 
  "applied_rule_rev Cp x (a#p) = Some a \<longrightarrow> a \<notin> set (p) \<longrightarrow> applied_rule_rev Cp x p = None"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. applied_rule_rev Cp x (a # p) = \<lfloor>a\<rfloor> \<longrightarrow> a \<notin> set p \<longrightarrow> applied_rule_rev Cp x p = \<bottom>
[PROOF STEP]
by (rule rev_induct, simp_all) (intro impI,simp add: applied_rule_rev_def split: if_splits)