[STATEMENT]
lemma C_eq_rd[rule_format]: 
  "p \<noteq> [] \<Longrightarrow> Cp (list2FWpolicy (remdups p)) = Cp (list2FWpolicy p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p \<noteq> [] \<Longrightarrow> Cp (list2FWpolicy (remdups p)) = Cp (list2FWpolicy p)
[PROOF STEP]
proof (rule ext, induct p)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. [] \<noteq> [] \<Longrightarrow> Cp (list2FWpolicy (remdups [])) x = Cp (list2FWpolicy []) x
 2. \<And>a p x. \<lbrakk>\<And>x. p \<noteq> [] \<Longrightarrow> Cp (list2FWpolicy (remdups p)) x = Cp (list2FWpolicy p) x; a # p \<noteq> []\<rbrakk> \<Longrightarrow> Cp (list2FWpolicy (remdups (a # p))) x = Cp (list2FWpolicy (a # p)) x
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
[] \<noteq> []

goal (2 subgoals):
 1. \<And>x. [] \<noteq> [] \<Longrightarrow> Cp (list2FWpolicy (remdups [])) x = Cp (list2FWpolicy []) x
 2. \<And>a p x. \<lbrakk>\<And>x. p \<noteq> [] \<Longrightarrow> Cp (list2FWpolicy (remdups p)) x = Cp (list2FWpolicy p) x; a # p \<noteq> []\<rbrakk> \<Longrightarrow> Cp (list2FWpolicy (remdups (a # p))) x = Cp (list2FWpolicy (a # p)) x
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
[] \<noteq> []

goal (1 subgoal):
 1. Cp (list2FWpolicy (remdups [])) x = Cp (list2FWpolicy []) x
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Cp (list2FWpolicy (remdups [])) x = Cp (list2FWpolicy []) x

goal (1 subgoal):
 1. \<And>a p x. \<lbrakk>\<And>x. p \<noteq> [] \<Longrightarrow> Cp (list2FWpolicy (remdups p)) x = Cp (list2FWpolicy p) x; a # p \<noteq> []\<rbrakk> \<Longrightarrow> Cp (list2FWpolicy (remdups (a # p))) x = Cp (list2FWpolicy (a # p)) x
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a p x. \<lbrakk>\<And>x. p \<noteq> [] \<Longrightarrow> Cp (list2FWpolicy (remdups p)) x = Cp (list2FWpolicy p) x; a # p \<noteq> []\<rbrakk> \<Longrightarrow> Cp (list2FWpolicy (remdups (a # p))) x = Cp (list2FWpolicy (a # p)) x
[PROOF STEP]
case (Cons y ys)
[PROOF STATE]
proof (state)
this:
ys \<noteq> [] \<Longrightarrow> Cp (list2FWpolicy (remdups ys)) ?x = Cp (list2FWpolicy ys) ?x
y # ys \<noteq> []

goal (1 subgoal):
 1. \<And>a p x. \<lbrakk>\<And>x. p \<noteq> [] \<Longrightarrow> Cp (list2FWpolicy (remdups p)) x = Cp (list2FWpolicy p) x; a # p \<noteq> []\<rbrakk> \<Longrightarrow> Cp (list2FWpolicy (remdups (a # p))) x = Cp (list2FWpolicy (a # p)) x
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
ys \<noteq> [] \<Longrightarrow> Cp (list2FWpolicy (remdups ys)) ?x = Cp (list2FWpolicy ys) ?x
y # ys \<noteq> []

goal (1 subgoal):
 1. Cp (list2FWpolicy (remdups (y # ys))) x = Cp (list2FWpolicy (y # ys)) x
[PROOF STEP]
proof (cases "ys = []")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>\<And>x. ys \<noteq> [] \<Longrightarrow> Cp (list2FWpolicy (remdups ys)) x = Cp (list2FWpolicy ys) x; y # ys \<noteq> []; ys = []\<rbrakk> \<Longrightarrow> Cp (list2FWpolicy (remdups (y # ys))) x = Cp (list2FWpolicy (y # ys)) x
 2. \<lbrakk>\<And>x. ys \<noteq> [] \<Longrightarrow> Cp (list2FWpolicy (remdups ys)) x = Cp (list2FWpolicy ys) x; y # ys \<noteq> []; ys \<noteq> []\<rbrakk> \<Longrightarrow> Cp (list2FWpolicy (remdups (y # ys))) x = Cp (list2FWpolicy (y # ys)) x
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
ys = []

goal (2 subgoals):
 1. \<lbrakk>\<And>x. ys \<noteq> [] \<Longrightarrow> Cp (list2FWpolicy (remdups ys)) x = Cp (list2FWpolicy ys) x; y # ys \<noteq> []; ys = []\<rbrakk> \<Longrightarrow> Cp (list2FWpolicy (remdups (y # ys))) x = Cp (list2FWpolicy (y # ys)) x
 2. \<lbrakk>\<And>x. ys \<noteq> [] \<Longrightarrow> Cp (list2FWpolicy (remdups ys)) x = Cp (list2FWpolicy ys) x; y # ys \<noteq> []; ys \<noteq> []\<rbrakk> \<Longrightarrow> Cp (list2FWpolicy (remdups (y # ys))) x = Cp (list2FWpolicy (y # ys)) x
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
ys = []

goal (1 subgoal):
 1. Cp (list2FWpolicy (remdups (y # ys))) x = Cp (list2FWpolicy (y # ys)) x
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Cp (list2FWpolicy (remdups (y # ys))) x = Cp (list2FWpolicy (y # ys)) x

goal (1 subgoal):
 1. \<lbrakk>\<And>x. ys \<noteq> [] \<Longrightarrow> Cp (list2FWpolicy (remdups ys)) x = Cp (list2FWpolicy ys) x; y # ys \<noteq> []; ys \<noteq> []\<rbrakk> \<Longrightarrow> Cp (list2FWpolicy (remdups (y # ys))) x = Cp (list2FWpolicy (y # ys)) x
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>\<And>x. ys \<noteq> [] \<Longrightarrow> Cp (list2FWpolicy (remdups ys)) x = Cp (list2FWpolicy ys) x; y # ys \<noteq> []; ys \<noteq> []\<rbrakk> \<Longrightarrow> Cp (list2FWpolicy (remdups (y # ys))) x = Cp (list2FWpolicy (y # ys)) x
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
ys \<noteq> []

goal (1 subgoal):
 1. \<lbrakk>\<And>x. ys \<noteq> [] \<Longrightarrow> Cp (list2FWpolicy (remdups ys)) x = Cp (list2FWpolicy ys) x; y # ys \<noteq> []; ys \<noteq> []\<rbrakk> \<Longrightarrow> Cp (list2FWpolicy (remdups (y # ys))) x = Cp (list2FWpolicy (y # ys)) x
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
ys \<noteq> []

goal (1 subgoal):
 1. Cp (list2FWpolicy (remdups (y # ys))) x = Cp (list2FWpolicy (y # ys)) x
[PROOF STEP]
using Cons
[PROOF STATE]
proof (prove)
using this:
ys \<noteq> []
ys \<noteq> [] \<Longrightarrow> Cp (list2FWpolicy (remdups ys)) ?x = Cp (list2FWpolicy ys) ?x
y # ys \<noteq> []

goal (1 subgoal):
 1. Cp (list2FWpolicy (remdups (y # ys))) x = Cp (list2FWpolicy (y # ys)) x
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ys \<noteq> []; \<And>x. Cp (list2FWpolicy (remdups ys)) x = Cp (list2FWpolicy ys) x\<rbrakk> \<Longrightarrow> (y \<in> set ys \<longrightarrow> Cp (list2FWpolicy ys) x = Cp (list2FWpolicy (y # ys)) x) \<and> (y \<notin> set ys \<longrightarrow> Cp (list2FWpolicy (y # remdups ys)) x = Cp (list2FWpolicy (y # ys)) x)
[PROOF STEP]
apply (intro conjI impI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ys \<noteq> []; \<And>x. Cp (list2FWpolicy (remdups ys)) x = Cp (list2FWpolicy ys) x; y \<in> set ys\<rbrakk> \<Longrightarrow> Cp (list2FWpolicy ys) x = Cp (list2FWpolicy (y # ys)) x
 2. \<lbrakk>ys \<noteq> []; \<And>x. Cp (list2FWpolicy (remdups ys)) x = Cp (list2FWpolicy ys) x; y \<notin> set ys\<rbrakk> \<Longrightarrow> Cp (list2FWpolicy (y # remdups ys)) x = Cp (list2FWpolicy (y # ys)) x
[PROOF STEP]
apply (metis Cdom2 nlpaux notindom domIff l2p_aux)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ys \<noteq> []; \<And>x. Cp (list2FWpolicy (remdups ys)) x = Cp (list2FWpolicy ys) x; y \<notin> set ys\<rbrakk> \<Longrightarrow> Cp (list2FWpolicy (y # remdups ys)) x = Cp (list2FWpolicy (y # ys)) x
[PROOF STEP]
by (metis (no_types, lifting) Cdom2 nlpaux domIff l2p_aux remDupsNMT)
[PROOF STATE]
proof (state)
this:
Cp (list2FWpolicy (remdups (y # ys))) x = Cp (list2FWpolicy (y # ys)) x

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
Cp (list2FWpolicy (remdups (y # ys))) x = Cp (list2FWpolicy (y # ys)) x

goal:
No subgoals!
[PROOF STEP]
qed