[STATEMENT]
lemma replacefacesAt2_5: "x \<in> set (replacefacesAt2 ns oldf newfs F ! k) \<Longrightarrow> x \<in> set (F!k) \<or> x \<in> set newfs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> set (replacefacesAt2 ns oldf newfs F ! k) \<Longrightarrow> x \<in> set (F ! k) \<or> x \<in> set newfs
[PROOF STEP]
proof (induct ns arbitrary: F)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>F. x \<in> set (replacefacesAt2 [] oldf newfs F ! k) \<Longrightarrow> x \<in> set (F ! k) \<or> x \<in> set newfs
 2. \<And>a ns F. \<lbrakk>\<And>F. x \<in> set (replacefacesAt2 ns oldf newfs F ! k) \<Longrightarrow> x \<in> set (F ! k) \<or> x \<in> set newfs; x \<in> set (replacefacesAt2 (a # ns) oldf newfs F ! k)\<rbrakk> \<Longrightarrow> x \<in> set (F ! k) \<or> x \<in> set newfs
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
x \<in> set (replacefacesAt2 [] oldf newfs F ! k)

goal (2 subgoals):
 1. \<And>F. x \<in> set (replacefacesAt2 [] oldf newfs F ! k) \<Longrightarrow> x \<in> set (F ! k) \<or> x \<in> set newfs
 2. \<And>a ns F. \<lbrakk>\<And>F. x \<in> set (replacefacesAt2 ns oldf newfs F ! k) \<Longrightarrow> x \<in> set (F ! k) \<or> x \<in> set newfs; x \<in> set (replacefacesAt2 (a # ns) oldf newfs F ! k)\<rbrakk> \<Longrightarrow> x \<in> set (F ! k) \<or> x \<in> set newfs
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<in> set (replacefacesAt2 [] oldf newfs F ! k)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
x \<in> set (replacefacesAt2 [] oldf newfs F ! k)

goal (1 subgoal):
 1. x \<in> set (F ! k) \<or> x \<in> set newfs
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
x \<in> set (F ! k) \<or> x \<in> set newfs

goal (1 subgoal):
 1. \<And>a ns F. \<lbrakk>\<And>F. x \<in> set (replacefacesAt2 ns oldf newfs F ! k) \<Longrightarrow> x \<in> set (F ! k) \<or> x \<in> set newfs; x \<in> set (replacefacesAt2 (a # ns) oldf newfs F ! k)\<rbrakk> \<Longrightarrow> x \<in> set (F ! k) \<or> x \<in> set newfs
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a ns F. \<lbrakk>\<And>F. x \<in> set (replacefacesAt2 ns oldf newfs F ! k) \<Longrightarrow> x \<in> set (F ! k) \<or> x \<in> set newfs; x \<in> set (replacefacesAt2 (a # ns) oldf newfs F ! k)\<rbrakk> \<Longrightarrow> x \<in> set (F ! k) \<or> x \<in> set newfs
[PROOF STEP]
case (Cons n ns)
[PROOF STATE]
proof (state)
this:
x \<in> set (replacefacesAt2 ns oldf newfs ?F ! k) \<Longrightarrow> x \<in> set (?F ! k) \<or> x \<in> set newfs
x \<in> set (replacefacesAt2 (n # ns) oldf newfs F ! k)

goal (1 subgoal):
 1. \<And>a ns F. \<lbrakk>\<And>F. x \<in> set (replacefacesAt2 ns oldf newfs F ! k) \<Longrightarrow> x \<in> set (F ! k) \<or> x \<in> set newfs; x \<in> set (replacefacesAt2 (a # ns) oldf newfs F ! k)\<rbrakk> \<Longrightarrow> x \<in> set (F ! k) \<or> x \<in> set newfs
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<in> set (replacefacesAt2 ns oldf newfs ?F ! k) \<Longrightarrow> x \<in> set (?F ! k) \<or> x \<in> set newfs
x \<in> set (replacefacesAt2 (n # ns) oldf newfs F ! k)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
x \<in> set (replacefacesAt2 ns oldf newfs ?F ! k) \<Longrightarrow> x \<in> set (?F ! k) \<or> x \<in> set newfs
x \<in> set (replacefacesAt2 (n # ns) oldf newfs F ! k)

goal (1 subgoal):
 1. x \<in> set (F ! k) \<or> x \<in> set newfs
[PROOF STEP]
apply(simp add: split: if_split_asm )
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>F. x \<in> set (replacefacesAt2 ns oldf newfs F ! k) \<Longrightarrow> x \<in> set (F ! k) \<or> x \<in> set newfs; n < |F|; x \<in> set (replacefacesAt2 ns oldf newfs (F[n := replace oldf newfs (F ! n)]) ! k)\<rbrakk> \<Longrightarrow> x \<in> set (F ! k) \<or> x \<in> set newfs
[PROOF STEP]
apply (frule Cons)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>F. x \<in> set (replacefacesAt2 ns oldf newfs F ! k) \<Longrightarrow> x \<in> set (F ! k) \<or> x \<in> set newfs; n < |F|; x \<in> set (replacefacesAt2 ns oldf newfs (F[n := replace oldf newfs (F ! n)]) ! k); x \<in> set (F[n := replace oldf newfs (F ! n)] ! k) \<or> x \<in> set newfs\<rbrakk> \<Longrightarrow> x \<in> set (F ! k) \<or> x \<in> set newfs
[PROOF STEP]
apply (thin_tac "\<And>F. x \<in> set (replacefacesAt2 ns oldf newfs F ! k) \<Longrightarrow> x \<in> set (F ! k) \<or> x \<in> set newfs")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n < |F|; x \<in> set (replacefacesAt2 ns oldf newfs (F[n := replace oldf newfs (F ! n)]) ! k); x \<in> set (F[n := replace oldf newfs (F ! n)] ! k) \<or> x \<in> set newfs\<rbrakk> \<Longrightarrow> x \<in> set (F ! k) \<or> x \<in> set newfs
[PROOF STEP]
apply (case_tac "x \<in> set newfs")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>n < |F|; x \<in> set (replacefacesAt2 ns oldf newfs (F[n := replace oldf newfs (F ! n)]) ! k); x \<in> set (F[n := replace oldf newfs (F ! n)] ! k) \<or> x \<in> set newfs; x \<in> set newfs\<rbrakk> \<Longrightarrow> x \<in> set (F ! k) \<or> x \<in> set newfs
 2. \<lbrakk>n < |F|; x \<in> set (replacefacesAt2 ns oldf newfs (F[n := replace oldf newfs (F ! n)]) ! k); x \<in> set (F[n := replace oldf newfs (F ! n)] ! k) \<or> x \<in> set newfs; x \<notin> set newfs\<rbrakk> \<Longrightarrow> x \<in> set (F ! k) \<or> x \<in> set newfs
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n < |F|; x \<in> set (replacefacesAt2 ns oldf newfs (F[n := replace oldf newfs (F ! n)]) ! k); x \<in> set (F[n := replace oldf newfs (F ! n)] ! k) \<or> x \<in> set newfs; x \<notin> set newfs\<rbrakk> \<Longrightarrow> x \<in> set (F ! k) \<or> x \<in> set newfs
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n < |F|; x \<in> set (replacefacesAt2 ns oldf newfs (F[n := replace oldf newfs (F ! n)]) ! k); x \<in> set (F[n := replace oldf newfs (F ! n)] ! k); x \<notin> set newfs\<rbrakk> \<Longrightarrow> x \<in> set (F ! k)
[PROOF STEP]
apply (case_tac "k = n")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>n < |F|; x \<in> set (replacefacesAt2 ns oldf newfs (F[n := replace oldf newfs (F ! n)]) ! k); x \<in> set (F[n := replace oldf newfs (F ! n)] ! k); x \<notin> set newfs; k = n\<rbrakk> \<Longrightarrow> x \<in> set (F ! k)
 2. \<lbrakk>n < |F|; x \<in> set (replacefacesAt2 ns oldf newfs (F[n := replace oldf newfs (F ! n)]) ! k); x \<in> set (F[n := replace oldf newfs (F ! n)] ! k); x \<notin> set newfs; k \<noteq> n\<rbrakk> \<Longrightarrow> x \<in> set (F ! k)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>n < |F|; x \<in> set (replacefacesAt2 ns oldf newfs (F[n := replace oldf newfs (F ! n)]) ! n); x \<in> set (replace oldf newfs (F ! n)); x \<notin> set newfs; k = n\<rbrakk> \<Longrightarrow> x \<in> set (F ! n)
 2. \<lbrakk>n < |F|; x \<in> set (replacefacesAt2 ns oldf newfs (F[n := replace oldf newfs (F ! n)]) ! k); x \<in> set (F[n := replace oldf newfs (F ! n)] ! k); x \<notin> set newfs; k \<noteq> n\<rbrakk> \<Longrightarrow> x \<in> set (F ! k)
[PROOF STEP]
apply (frule replace5)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>n < |F|; x \<in> set (replacefacesAt2 ns oldf newfs (F[n := replace oldf newfs (F ! n)]) ! n); x \<in> set (replace oldf newfs (F ! n)); x \<notin> set newfs; k = n; x \<in> set (F ! n) \<or> x \<in> set newfs\<rbrakk> \<Longrightarrow> x \<in> set (F ! n)
 2. \<lbrakk>n < |F|; x \<in> set (replacefacesAt2 ns oldf newfs (F[n := replace oldf newfs (F ! n)]) ! k); x \<in> set (F[n := replace oldf newfs (F ! n)] ! k); x \<notin> set newfs; k \<noteq> n\<rbrakk> \<Longrightarrow> x \<in> set (F ! k)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n < |F|; x \<in> set (replacefacesAt2 ns oldf newfs (F[n := replace oldf newfs (F ! n)]) ! k); x \<in> set (F[n := replace oldf newfs (F ! n)] ! k); x \<notin> set newfs; k \<noteq> n\<rbrakk> \<Longrightarrow> x \<in> set (F ! k)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
x \<in> set (F ! k) \<or> x \<in> set newfs

goal:
No subgoals!
[PROOF STEP]
qed