[STATEMENT]
lemma simple_fw_remdups_Rev: "simple_fw (remdups_rev rs) p = simple_fw rs p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. simple_fw (remdups_rev rs) p = simple_fw rs p
[PROOF STEP]
apply(induction rs p rule: simple_fw.induct)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>uu_. simple_fw (remdups_rev []) uu_ = simple_fw [] uu_
 2. \<And>m rs p. (\<not> simple_matches m p \<Longrightarrow> simple_fw (remdups_rev rs) p = simple_fw rs p) \<Longrightarrow> simple_fw (remdups_rev (SimpleRule m simple_action.Accept # rs)) p = simple_fw (SimpleRule m simple_action.Accept # rs) p
 3. \<And>m rs p. (\<not> simple_matches m p \<Longrightarrow> simple_fw (remdups_rev rs) p = simple_fw rs p) \<Longrightarrow> simple_fw (remdups_rev (SimpleRule m simple_action.Drop # rs)) p = simple_fw (SimpleRule m simple_action.Drop # rs) p
[PROOF STEP]
apply(simp add: remdups_rev_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>m rs p. (\<not> simple_matches m p \<Longrightarrow> simple_fw (remdups_rev rs) p = simple_fw rs p) \<Longrightarrow> simple_fw (remdups_rev (SimpleRule m simple_action.Accept # rs)) p = simple_fw (SimpleRule m simple_action.Accept # rs) p
 2. \<And>m rs p. (\<not> simple_matches m p \<Longrightarrow> simple_fw (remdups_rev rs) p = simple_fw rs p) \<Longrightarrow> simple_fw (remdups_rev (SimpleRule m simple_action.Drop # rs)) p = simple_fw (SimpleRule m simple_action.Drop # rs) p
[PROOF STEP]
apply(simp_all add: remdups_rev_fst remdups_rev_removeAll simple_fw_not_matches_removeAll)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done