[STATEMENT]
lemma nths_reencode_eq:
  assumes "B \<subseteq> A"
  shows "nths (nths xs A) (ind_in_set A ` B) = nths xs B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nths (nths xs A) (ind_in_set A ` B) = nths xs B
[PROOF STEP]
proof (induction xs rule: rev_induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. nths (nths [] A) (ind_in_set A ` B) = nths [] B
 2. \<And>x xs. nths (nths xs A) (ind_in_set A ` B) = nths xs B \<Longrightarrow> nths (nths (xs @ [x]) A) (ind_in_set A ` B) = nths (xs @ [x]) B
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. nths (nths [] A) (ind_in_set A ` B) = nths [] B
 2. \<And>x xs. nths (nths xs A) (ind_in_set A ` B) = nths xs B \<Longrightarrow> nths (nths (xs @ [x]) A) (ind_in_set A ` B) = nths (xs @ [x]) B
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nths (nths [] A) (ind_in_set A ` B) = nths [] B
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
nths (nths [] A) (ind_in_set A ` B) = nths [] B

goal (1 subgoal):
 1. \<And>x xs. nths (nths xs A) (ind_in_set A ` B) = nths xs B \<Longrightarrow> nths (nths (xs @ [x]) A) (ind_in_set A ` B) = nths (xs @ [x]) B
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x xs. nths (nths xs A) (ind_in_set A ` B) = nths xs B \<Longrightarrow> nths (nths (xs @ [x]) A) (ind_in_set A ` B) = nths (xs @ [x]) B
[PROOF STEP]
case (snoc x xs)
[PROOF STATE]
proof (state)
this:
nths (nths xs A) (ind_in_set A ` B) = nths xs B

goal (1 subgoal):
 1. \<And>x xs. nths (nths xs A) (ind_in_set A ` B) = nths xs B \<Longrightarrow> nths (nths (xs @ [x]) A) (ind_in_set A ` B) = nths (xs @ [x]) B
[PROOF STEP]
have seteq: "{i. i < length xs \<and> i \<in> A} = {i. i \<in> A \<and> i < length xs}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {i. i < length xs \<and> i \<in> A} = {i \<in> A. i < length xs}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{i. i < length xs \<and> i \<in> A} = {i \<in> A. i < length xs}

goal (1 subgoal):
 1. \<And>x xs. nths (nths xs A) (ind_in_set A ` B) = nths xs B \<Longrightarrow> nths (nths (xs @ [x]) A) (ind_in_set A ` B) = nths (xs @ [x]) B
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nths (nths (xs @ [x]) A) (ind_in_set A ` B) = nths (xs @ [x]) B
[PROOF STEP]
proof (cases "length xs \<in> B")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. length xs \<in> B \<Longrightarrow> nths (nths (xs @ [x]) A) (ind_in_set A ` B) = nths (xs @ [x]) B
 2. length xs \<notin> B \<Longrightarrow> nths (nths (xs @ [x]) A) (ind_in_set A ` B) = nths (xs @ [x]) B
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
length xs \<in> B

goal (2 subgoals):
 1. length xs \<in> B \<Longrightarrow> nths (nths (xs @ [x]) A) (ind_in_set A ` B) = nths (xs @ [x]) B
 2. length xs \<notin> B \<Longrightarrow> nths (nths (xs @ [x]) A) (ind_in_set A ` B) = nths (xs @ [x]) B
[PROOF STEP]
have "nths (xs @ [x]) B = nths xs B @ nths [x] {l. l + length xs \<in> B}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nths (xs @ [x]) B = nths xs B @ nths [x] {l. l + length xs \<in> B}
[PROOF STEP]
using nths_append[of xs]
[PROOF STATE]
proof (prove)
using this:
nths (xs @ ?l') ?A = nths xs ?A @ nths ?l' {j. j + length xs \<in> ?A}

goal (1 subgoal):
 1. nths (xs @ [x]) B = nths xs B @ nths [x] {l. l + length xs \<in> B}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
nths (xs @ [x]) B = nths xs B @ nths [x] {l. l + length xs \<in> B}

goal (2 subgoals):
 1. length xs \<in> B \<Longrightarrow> nths (nths (xs @ [x]) A) (ind_in_set A ` B) = nths (xs @ [x]) B
 2. length xs \<notin> B \<Longrightarrow> nths (nths (xs @ [x]) A) (ind_in_set A ` B) = nths (xs @ [x]) B
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
nths (xs @ [x]) B = nths xs B @ nths [x] {l. l + length xs \<in> B}

goal (2 subgoals):
 1. length xs \<in> B \<Longrightarrow> nths (nths (xs @ [x]) A) (ind_in_set A ` B) = nths (xs @ [x]) B
 2. length xs \<notin> B \<Longrightarrow> nths (nths (xs @ [x]) A) (ind_in_set A ` B) = nths (xs @ [x]) B
[PROOF STEP]
have "nths [x] {l. l + length xs \<in> B} = [x]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nths [x] {l. l + length xs \<in> B} = [x]
[PROOF STEP]
using nths_singleton True
[PROOF STATE]
proof (prove)
using this:
nths [?x] ?A = (if 0 \<in> ?A then [?x] else [])
length xs \<in> B

goal (1 subgoal):
 1. nths [x] {l. l + length xs \<in> B} = [x]
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
nths [x] {l. l + length xs \<in> B} = [x]

goal (2 subgoals):
 1. length xs \<in> B \<Longrightarrow> nths (nths (xs @ [x]) A) (ind_in_set A ` B) = nths (xs @ [x]) B
 2. length xs \<notin> B \<Longrightarrow> nths (nths (xs @ [x]) A) (ind_in_set A ` B) = nths (xs @ [x]) B
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
nths (xs @ [x]) B = nths xs B @ nths [x] {l. l + length xs \<in> B}
nths [x] {l. l + length xs \<in> B} = [x]
[PROOF STEP]
have eqT1: "nths (xs @ [x]) B = nths xs B @ [x]"
[PROOF STATE]
proof (prove)
using this:
nths (xs @ [x]) B = nths xs B @ nths [x] {l. l + length xs \<in> B}
nths [x] {l. l + length xs \<in> B} = [x]

goal (1 subgoal):
 1. nths (xs @ [x]) B = nths xs B @ [x]
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
nths (xs @ [x]) B = nths xs B @ [x]

goal (2 subgoals):
 1. length xs \<in> B \<Longrightarrow> nths (nths (xs @ [x]) A) (ind_in_set A ` B) = nths (xs @ [x]) B
 2. length xs \<notin> B \<Longrightarrow> nths (nths (xs @ [x]) A) (ind_in_set A ` B) = nths (xs @ [x]) B
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
nths (xs @ [x]) B = nths xs B @ [x]
[PROOF STEP]
have "length xs \<in> A"
[PROOF STATE]
proof (prove)
using this:
nths (xs @ [x]) B = nths xs B @ [x]

goal (1 subgoal):
 1. length xs \<in> A
[PROOF STEP]
using True assms
[PROOF STATE]
proof (prove)
using this:
nths (xs @ [x]) B = nths xs B @ [x]
length xs \<in> B
B \<subseteq> A

goal (1 subgoal):
 1. length xs \<in> A
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
length xs \<in> A

goal (2 subgoals):
 1. length xs \<in> B \<Longrightarrow> nths (nths (xs @ [x]) A) (ind_in_set A ` B) = nths (xs @ [x]) B
 2. length xs \<notin> B \<Longrightarrow> nths (nths (xs @ [x]) A) (ind_in_set A ` B) = nths (xs @ [x]) B
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
length xs \<in> A
[PROOF STEP]
have "nths [x] {l. l + length xs \<in> A} = [x]"
[PROOF STATE]
proof (prove)
using this:
length xs \<in> A

goal (1 subgoal):
 1. nths [x] {l. l + length xs \<in> A} = [x]
[PROOF STEP]
using nths_singleton
[PROOF STATE]
proof (prove)
using this:
length xs \<in> A
nths [?x] ?A = (if 0 \<in> ?A then [?x] else [])

goal (1 subgoal):
 1. nths [x] {l. l + length xs \<in> A} = [x]
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
nths [x] {l. l + length xs \<in> A} = [x]

goal (2 subgoals):
 1. length xs \<in> B \<Longrightarrow> nths (nths (xs @ [x]) A) (ind_in_set A ` B) = nths (xs @ [x]) B
 2. length xs \<notin> B \<Longrightarrow> nths (nths (xs @ [x]) A) (ind_in_set A ` B) = nths (xs @ [x]) B
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
nths [x] {l. l + length xs \<in> A} = [x]

goal (2 subgoals):
 1. length xs \<in> B \<Longrightarrow> nths (nths (xs @ [x]) A) (ind_in_set A ` B) = nths (xs @ [x]) B
 2. length xs \<notin> B \<Longrightarrow> nths (nths (xs @ [x]) A) (ind_in_set A ` B) = nths (xs @ [x]) B
[PROOF STEP]
have "nths (xs @ [x]) A = nths xs A @ nths [x] {l. l + length xs \<in> A}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nths (xs @ [x]) A = nths xs A @ nths [x] {l. l + length xs \<in> A}
[PROOF STEP]
using nths_append[of xs]
[PROOF STATE]
proof (prove)
using this:
nths (xs @ ?l') ?A = nths xs ?A @ nths ?l' {j. j + length xs \<in> ?A}

goal (1 subgoal):
 1. nths (xs @ [x]) A = nths xs A @ nths [x] {l. l + length xs \<in> A}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
nths (xs @ [x]) A = nths xs A @ nths [x] {l. l + length xs \<in> A}

goal (2 subgoals):
 1. length xs \<in> B \<Longrightarrow> nths (nths (xs @ [x]) A) (ind_in_set A ` B) = nths (xs @ [x]) B
 2. length xs \<notin> B \<Longrightarrow> nths (nths (xs @ [x]) A) (ind_in_set A ` B) = nths (xs @ [x]) B
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
nths [x] {l. l + length xs \<in> A} = [x]
nths (xs @ [x]) A = nths xs A @ nths [x] {l. l + length xs \<in> A}
[PROOF STEP]
have "nths (xs @ [x]) A = nths xs A @ [x]"
[PROOF STATE]
proof (prove)
using this:
nths [x] {l. l + length xs \<in> A} = [x]
nths (xs @ [x]) A = nths xs A @ nths [x] {l. l + length xs \<in> A}

goal (1 subgoal):
 1. nths (xs @ [x]) A = nths xs A @ [x]
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
nths (xs @ [x]) A = nths xs A @ [x]

goal (2 subgoals):
 1. length xs \<in> B \<Longrightarrow> nths (nths (xs @ [x]) A) (ind_in_set A ` B) = nths (xs @ [x]) B
 2. length xs \<notin> B \<Longrightarrow> nths (nths (xs @ [x]) A) (ind_in_set A ` B) = nths (xs @ [x]) B
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
nths (xs @ [x]) A = nths xs A @ [x]
[PROOF STEP]
have eqT2: "nths (nths (xs @ [x]) A) (ind_in_set A ` B) = nths (nths xs A @ [x]) (ind_in_set A ` B)"
[PROOF STATE]
proof (prove)
using this:
nths (xs @ [x]) A = nths xs A @ [x]

goal (1 subgoal):
 1. nths (nths (xs @ [x]) A) (ind_in_set A ` B) = nths (nths xs A @ [x]) (ind_in_set A ` B)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
nths (nths (xs @ [x]) A) (ind_in_set A ` B) = nths (nths xs A @ [x]) (ind_in_set A ` B)

goal (2 subgoals):
 1. length xs \<in> B \<Longrightarrow> nths (nths (xs @ [x]) A) (ind_in_set A ` B) = nths (xs @ [x]) B
 2. length xs \<notin> B \<Longrightarrow> nths (nths (xs @ [x]) A) (ind_in_set A ` B) = nths (xs @ [x]) B
[PROOF STEP]
have eqT3: "nths (nths xs A @ [x]) (ind_in_set A ` B)
      = nths xs B @ (nths [x] {l. l + length (nths xs A) \<in> (ind_in_set A ` B)})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nths (nths xs A @ [x]) (ind_in_set A ` B) = nths xs B @ nths [x] {l. l + length (nths xs A) \<in> ind_in_set A ` B}
[PROOF STEP]
using nths_append[of "nths xs A"] snoc
[PROOF STATE]
proof (prove)
using this:
nths (nths xs A @ ?l') ?A = nths (nths xs A) ?A @ nths ?l' {j. j + length (nths xs A) \<in> ?A}
nths (nths xs A) (ind_in_set A ` B) = nths xs B

goal (1 subgoal):
 1. nths (nths xs A @ [x]) (ind_in_set A ` B) = nths xs B @ nths [x] {l. l + length (nths xs A) \<in> ind_in_set A ` B}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
nths (nths xs A @ [x]) (ind_in_set A ` B) = nths xs B @ nths [x] {l. l + length (nths xs A) \<in> ind_in_set A ` B}

goal (2 subgoals):
 1. length xs \<in> B \<Longrightarrow> nths (nths (xs @ [x]) A) (ind_in_set A ` B) = nths (xs @ [x]) B
 2. length xs \<notin> B \<Longrightarrow> nths (nths (xs @ [x]) A) (ind_in_set A ` B) = nths (xs @ [x]) B
[PROOF STEP]
have "ind_in_set A (length xs) = card {i. i < length xs \<and> i \<in> A}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ind_in_set A (length xs) = card {i. i < length xs \<and> i \<in> A}
[PROOF STEP]
using ind_in_set_def seteq
[PROOF STATE]
proof (prove)
using this:
ind_in_set ?A ?x = card {i \<in> ?A. i < ?x}
{i. i < length xs \<and> i \<in> A} = {i \<in> A. i < length xs}

goal (1 subgoal):
 1. ind_in_set A (length xs) = card {i. i < length xs \<and> i \<in> A}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
ind_in_set A (length xs) = card {i. i < length xs \<and> i \<in> A}

goal (2 subgoals):
 1. length xs \<in> B \<Longrightarrow> nths (nths (xs @ [x]) A) (ind_in_set A ` B) = nths (xs @ [x]) B
 2. length xs \<notin> B \<Longrightarrow> nths (nths (xs @ [x]) A) (ind_in_set A ` B) = nths (xs @ [x]) B
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
ind_in_set A (length xs) = card {i. i < length xs \<and> i \<in> A}

goal (2 subgoals):
 1. length xs \<in> B \<Longrightarrow> nths (nths (xs @ [x]) A) (ind_in_set A ` B) = nths (xs @ [x]) B
 2. length xs \<notin> B \<Longrightarrow> nths (nths (xs @ [x]) A) (ind_in_set A ` B) = nths (xs @ [x]) B
[PROOF STEP]
have "length (nths xs A) = card {i. i < length xs \<and> i \<in> A}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (nths xs A) = card {i. i < length xs \<and> i \<in> A}
[PROOF STEP]
using length_nths
[PROOF STATE]
proof (prove)
using this:
length (nths ?xs ?I) = card {i. i < length ?xs \<and> i \<in> ?I}

goal (1 subgoal):
 1. length (nths xs A) = card {i. i < length xs \<and> i \<in> A}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
length (nths xs A) = card {i. i < length xs \<and> i \<in> A}

goal (2 subgoals):
 1. length xs \<in> B \<Longrightarrow> nths (nths (xs @ [x]) A) (ind_in_set A ` B) = nths (xs @ [x]) B
 2. length xs \<notin> B \<Longrightarrow> nths (nths (xs @ [x]) A) (ind_in_set A ` B) = nths (xs @ [x]) B
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
ind_in_set A (length xs) = card {i. i < length xs \<and> i \<in> A}
length (nths xs A) = card {i. i < length xs \<and> i \<in> A}
[PROOF STEP]
have "length (nths xs A) = ind_in_set A (length xs)"
[PROOF STATE]
proof (prove)
using this:
ind_in_set A (length xs) = card {i. i < length xs \<and> i \<in> A}
length (nths xs A) = card {i. i < length xs \<and> i \<in> A}

goal (1 subgoal):
 1. length (nths xs A) = ind_in_set A (length xs)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
length (nths xs A) = ind_in_set A (length xs)

goal (2 subgoals):
 1. length xs \<in> B \<Longrightarrow> nths (nths (xs @ [x]) A) (ind_in_set A ` B) = nths (xs @ [x]) B
 2. length xs \<notin> B \<Longrightarrow> nths (nths (xs @ [x]) A) (ind_in_set A ` B) = nths (xs @ [x]) B
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
length (nths xs A) = ind_in_set A (length xs)

goal (2 subgoals):
 1. length xs \<in> B \<Longrightarrow> nths (nths (xs @ [x]) A) (ind_in_set A ` B) = nths (xs @ [x]) B
 2. length xs \<notin> B \<Longrightarrow> nths (nths (xs @ [x]) A) (ind_in_set A ` B) = nths (xs @ [x]) B
[PROOF STEP]
have "ind_in_set A (length xs) \<in> ind_in_set A ` B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ind_in_set A (length xs) \<in> ind_in_set A ` B
[PROOF STEP]
using True
[PROOF STATE]
proof (prove)
using this:
length xs \<in> B

goal (1 subgoal):
 1. ind_in_set A (length xs) \<in> ind_in_set A ` B
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
ind_in_set A (length xs) \<in> ind_in_set A ` B

goal (2 subgoals):
 1. length xs \<in> B \<Longrightarrow> nths (nths (xs @ [x]) A) (ind_in_set A ` B) = nths (xs @ [x]) B
 2. length xs \<notin> B \<Longrightarrow> nths (nths (xs @ [x]) A) (ind_in_set A ` B) = nths (xs @ [x]) B
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
length (nths xs A) = ind_in_set A (length xs)
ind_in_set A (length xs) \<in> ind_in_set A ` B
[PROOF STEP]
have "length (nths xs A) \<in> ind_in_set A ` B"
[PROOF STATE]
proof (prove)
using this:
length (nths xs A) = ind_in_set A (length xs)
ind_in_set A (length xs) \<in> ind_in_set A ` B

goal (1 subgoal):
 1. length (nths xs A) \<in> ind_in_set A ` B
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
length (nths xs A) \<in> ind_in_set A ` B

goal (2 subgoals):
 1. length xs \<in> B \<Longrightarrow> nths (nths (xs @ [x]) A) (ind_in_set A ` B) = nths (xs @ [x]) B
 2. length xs \<notin> B \<Longrightarrow> nths (nths (xs @ [x]) A) (ind_in_set A ` B) = nths (xs @ [x]) B
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
length (nths xs A) \<in> ind_in_set A ` B
[PROOF STEP]
have "(nths [x] {l. l + length (nths xs A) \<in> (ind_in_set A ` B)}) = [x]"
[PROOF STATE]
proof (prove)
using this:
length (nths xs A) \<in> ind_in_set A ` B

goal (1 subgoal):
 1. nths [x] {l. l + length (nths xs A) \<in> ind_in_set A ` B} = [x]
[PROOF STEP]
using nths_singleton
[PROOF STATE]
proof (prove)
using this:
length (nths xs A) \<in> ind_in_set A ` B
nths [?x] ?A = (if 0 \<in> ?A then [?x] else [])

goal (1 subgoal):
 1. nths [x] {l. l + length (nths xs A) \<in> ind_in_set A ` B} = [x]
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
nths [x] {l. l + length (nths xs A) \<in> ind_in_set A ` B} = [x]

goal (2 subgoals):
 1. length xs \<in> B \<Longrightarrow> nths (nths (xs @ [x]) A) (ind_in_set A ` B) = nths (xs @ [x]) B
 2. length xs \<notin> B \<Longrightarrow> nths (nths (xs @ [x]) A) (ind_in_set A ` B) = nths (xs @ [x]) B
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
nths [x] {l. l + length (nths xs A) \<in> ind_in_set A ` B} = [x]
[PROOF STEP]
have "nths (nths xs A @ [x]) (ind_in_set A ` B) = nths xs B @ [x]"
[PROOF STATE]
proof (prove)
using this:
nths [x] {l. l + length (nths xs A) \<in> ind_in_set A ` B} = [x]

goal (1 subgoal):
 1. nths (nths xs A @ [x]) (ind_in_set A ` B) = nths xs B @ [x]
[PROOF STEP]
using eqT3
[PROOF STATE]
proof (prove)
using this:
nths [x] {l. l + length (nths xs A) \<in> ind_in_set A ` B} = [x]
nths (nths xs A @ [x]) (ind_in_set A ` B) = nths xs B @ nths [x] {l. l + length (nths xs A) \<in> ind_in_set A ` B}

goal (1 subgoal):
 1. nths (nths xs A @ [x]) (ind_in_set A ` B) = nths xs B @ [x]
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
nths (nths xs A @ [x]) (ind_in_set A ` B) = nths xs B @ [x]

goal (2 subgoals):
 1. length xs \<in> B \<Longrightarrow> nths (nths (xs @ [x]) A) (ind_in_set A ` B) = nths (xs @ [x]) B
 2. length xs \<notin> B \<Longrightarrow> nths (nths (xs @ [x]) A) (ind_in_set A ` B) = nths (xs @ [x]) B
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
nths (nths xs A @ [x]) (ind_in_set A ` B) = nths xs B @ [x]
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
nths (nths xs A @ [x]) (ind_in_set A ` B) = nths xs B @ [x]

goal (1 subgoal):
 1. nths (nths (xs @ [x]) A) (ind_in_set A ` B) = nths (xs @ [x]) B
[PROOF STEP]
using eqT1 eqT2
[PROOF STATE]
proof (prove)
using this:
nths (nths xs A @ [x]) (ind_in_set A ` B) = nths xs B @ [x]
nths (xs @ [x]) B = nths xs B @ [x]
nths (nths (xs @ [x]) A) (ind_in_set A ` B) = nths (nths xs A @ [x]) (ind_in_set A ` B)

goal (1 subgoal):
 1. nths (nths (xs @ [x]) A) (ind_in_set A ` B) = nths (xs @ [x]) B
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
nths (nths (xs @ [x]) A) (ind_in_set A ` B) = nths (xs @ [x]) B

goal (1 subgoal):
 1. length xs \<notin> B \<Longrightarrow> nths (nths (xs @ [x]) A) (ind_in_set A ` B) = nths (xs @ [x]) B
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. length xs \<notin> B \<Longrightarrow> nths (nths (xs @ [x]) A) (ind_in_set A ` B) = nths (xs @ [x]) B
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
length xs \<notin> B

goal (1 subgoal):
 1. length xs \<notin> B \<Longrightarrow> nths (nths (xs @ [x]) A) (ind_in_set A ` B) = nths (xs @ [x]) B
[PROOF STEP]
have "nths (xs @ [x]) B = nths xs B @ nths [x] {l. l + length xs \<in> B}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nths (xs @ [x]) B = nths xs B @ nths [x] {l. l + length xs \<in> B}
[PROOF STEP]
using nths_append[of xs]
[PROOF STATE]
proof (prove)
using this:
nths (xs @ ?l') ?A = nths xs ?A @ nths ?l' {j. j + length xs \<in> ?A}

goal (1 subgoal):
 1. nths (xs @ [x]) B = nths xs B @ nths [x] {l. l + length xs \<in> B}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
nths (xs @ [x]) B = nths xs B @ nths [x] {l. l + length xs \<in> B}

goal (1 subgoal):
 1. length xs \<notin> B \<Longrightarrow> nths (nths (xs @ [x]) A) (ind_in_set A ` B) = nths (xs @ [x]) B
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
nths (xs @ [x]) B = nths xs B @ nths [x] {l. l + length xs \<in> B}

goal (1 subgoal):
 1. length xs \<notin> B \<Longrightarrow> nths (nths (xs @ [x]) A) (ind_in_set A ` B) = nths (xs @ [x]) B
[PROOF STEP]
have "nths [x] {l. l + length xs \<in> B} = []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nths [x] {l. l + length xs \<in> B} = []
[PROOF STEP]
using nths_singleton False
[PROOF STATE]
proof (prove)
using this:
nths [?x] ?A = (if 0 \<in> ?A then [?x] else [])
length xs \<notin> B

goal (1 subgoal):
 1. nths [x] {l. l + length xs \<in> B} = []
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
nths [x] {l. l + length xs \<in> B} = []

goal (1 subgoal):
 1. length xs \<notin> B \<Longrightarrow> nths (nths (xs @ [x]) A) (ind_in_set A ` B) = nths (xs @ [x]) B
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
nths (xs @ [x]) B = nths xs B @ nths [x] {l. l + length xs \<in> B}
nths [x] {l. l + length xs \<in> B} = []
[PROOF STEP]
have eqT1: "nths (xs @ [x]) B = nths xs B"
[PROOF STATE]
proof (prove)
using this:
nths (xs @ [x]) B = nths xs B @ nths [x] {l. l + length xs \<in> B}
nths [x] {l. l + length xs \<in> B} = []

goal (1 subgoal):
 1. nths (xs @ [x]) B = nths xs B
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
nths (xs @ [x]) B = nths xs B

goal (1 subgoal):
 1. length xs \<notin> B \<Longrightarrow> nths (nths (xs @ [x]) A) (ind_in_set A ` B) = nths (xs @ [x]) B
[PROOF STEP]
have "nths (nths (xs @ [x]) A) (ind_in_set A ` B) = nths xs B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nths (nths (xs @ [x]) A) (ind_in_set A ` B) = nths xs B
[PROOF STEP]
proof (cases "length xs \<in> A")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. length xs \<in> A \<Longrightarrow> nths (nths (xs @ [x]) A) (ind_in_set A ` B) = nths xs B
 2. length xs \<notin> A \<Longrightarrow> nths (nths (xs @ [x]) A) (ind_in_set A ` B) = nths xs B
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
length xs \<in> A

goal (2 subgoals):
 1. length xs \<in> A \<Longrightarrow> nths (nths (xs @ [x]) A) (ind_in_set A ` B) = nths xs B
 2. length xs \<notin> A \<Longrightarrow> nths (nths (xs @ [x]) A) (ind_in_set A ` B) = nths xs B
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
length xs \<in> A
[PROOF STEP]
have "nths [x] {l. l + length xs \<in> A} = [x]"
[PROOF STATE]
proof (prove)
using this:
length xs \<in> A

goal (1 subgoal):
 1. nths [x] {l. l + length xs \<in> A} = [x]
[PROOF STEP]
using nths_singleton
[PROOF STATE]
proof (prove)
using this:
length xs \<in> A
nths [?x] ?A = (if 0 \<in> ?A then [?x] else [])

goal (1 subgoal):
 1. nths [x] {l. l + length xs \<in> A} = [x]
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
nths [x] {l. l + length xs \<in> A} = [x]

goal (2 subgoals):
 1. length xs \<in> A \<Longrightarrow> nths (nths (xs @ [x]) A) (ind_in_set A ` B) = nths xs B
 2. length xs \<notin> A \<Longrightarrow> nths (nths (xs @ [x]) A) (ind_in_set A ` B) = nths xs B
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
nths [x] {l. l + length xs \<in> A} = [x]

goal (2 subgoals):
 1. length xs \<in> A \<Longrightarrow> nths (nths (xs @ [x]) A) (ind_in_set A ` B) = nths xs B
 2. length xs \<notin> A \<Longrightarrow> nths (nths (xs @ [x]) A) (ind_in_set A ` B) = nths xs B
[PROOF STEP]
have "nths (xs @ [x]) A = nths xs A @ nths [x] {l. l + length xs \<in> A}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nths (xs @ [x]) A = nths xs A @ nths [x] {l. l + length xs \<in> A}
[PROOF STEP]
using nths_append[of xs]
[PROOF STATE]
proof (prove)
using this:
nths (xs @ ?l') ?A = nths xs ?A @ nths ?l' {j. j + length xs \<in> ?A}

goal (1 subgoal):
 1. nths (xs @ [x]) A = nths xs A @ nths [x] {l. l + length xs \<in> A}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
nths (xs @ [x]) A = nths xs A @ nths [x] {l. l + length xs \<in> A}

goal (2 subgoals):
 1. length xs \<in> A \<Longrightarrow> nths (nths (xs @ [x]) A) (ind_in_set A ` B) = nths xs B
 2. length xs \<notin> A \<Longrightarrow> nths (nths (xs @ [x]) A) (ind_in_set A ` B) = nths xs B
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
nths [x] {l. l + length xs \<in> A} = [x]
nths (xs @ [x]) A = nths xs A @ nths [x] {l. l + length xs \<in> A}
[PROOF STEP]
have "nths (xs @ [x]) A = nths xs A @ [x]"
[PROOF STATE]
proof (prove)
using this:
nths [x] {l. l + length xs \<in> A} = [x]
nths (xs @ [x]) A = nths xs A @ nths [x] {l. l + length xs \<in> A}

goal (1 subgoal):
 1. nths (xs @ [x]) A = nths xs A @ [x]
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
nths (xs @ [x]) A = nths xs A @ [x]

goal (2 subgoals):
 1. length xs \<in> A \<Longrightarrow> nths (nths (xs @ [x]) A) (ind_in_set A ` B) = nths xs B
 2. length xs \<notin> A \<Longrightarrow> nths (nths (xs @ [x]) A) (ind_in_set A ` B) = nths xs B
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
nths (xs @ [x]) A = nths xs A @ [x]
[PROOF STEP]
have "nths (nths (xs @ [x]) A) (ind_in_set A ` B) = nths (nths xs A @ [x]) (ind_in_set A ` B)"
[PROOF STATE]
proof (prove)
using this:
nths (xs @ [x]) A = nths xs A @ [x]

goal (1 subgoal):
 1. nths (nths (xs @ [x]) A) (ind_in_set A ` B) = nths (nths xs A @ [x]) (ind_in_set A ` B)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
nths (nths (xs @ [x]) A) (ind_in_set A ` B) = nths (nths xs A @ [x]) (ind_in_set A ` B)

goal (2 subgoals):
 1. length xs \<in> A \<Longrightarrow> nths (nths (xs @ [x]) A) (ind_in_set A ` B) = nths xs B
 2. length xs \<notin> A \<Longrightarrow> nths (nths (xs @ [x]) A) (ind_in_set A ` B) = nths xs B
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
nths (nths (xs @ [x]) A) (ind_in_set A ` B) = nths (nths xs A @ [x]) (ind_in_set A ` B)
[PROOF STEP]
have eqT2: "nths (nths (xs @ [x]) A) (ind_in_set A ` B)
        = nths xs B @ (nths [x] {l. l + length (nths xs A) \<in> (ind_in_set A ` B)})"
[PROOF STATE]
proof (prove)
using this:
nths (nths (xs @ [x]) A) (ind_in_set A ` B) = nths (nths xs A @ [x]) (ind_in_set A ` B)

goal (1 subgoal):
 1. nths (nths (xs @ [x]) A) (ind_in_set A ` B) = nths xs B @ nths [x] {l. l + length (nths xs A) \<in> ind_in_set A ` B}
[PROOF STEP]
using nths_append[of "nths xs A"] snoc
[PROOF STATE]
proof (prove)
using this:
nths (nths (xs @ [x]) A) (ind_in_set A ` B) = nths (nths xs A @ [x]) (ind_in_set A ` B)
nths (nths xs A @ ?l') ?A = nths (nths xs A) ?A @ nths ?l' {j. j + length (nths xs A) \<in> ?A}
nths (nths xs A) (ind_in_set A ` B) = nths xs B

goal (1 subgoal):
 1. nths (nths (xs @ [x]) A) (ind_in_set A ` B) = nths xs B @ nths [x] {l. l + length (nths xs A) \<in> ind_in_set A ` B}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
nths (nths (xs @ [x]) A) (ind_in_set A ` B) = nths xs B @ nths [x] {l. l + length (nths xs A) \<in> ind_in_set A ` B}

goal (2 subgoals):
 1. length xs \<in> A \<Longrightarrow> nths (nths (xs @ [x]) A) (ind_in_set A ` B) = nths xs B
 2. length xs \<notin> A \<Longrightarrow> nths (nths (xs @ [x]) A) (ind_in_set A ` B) = nths xs B
[PROOF STEP]
have "length (nths xs A) \<in> (ind_in_set A ` B) \<Longrightarrow> length xs \<in> B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (nths xs A) \<in> ind_in_set A ` B \<Longrightarrow> length xs \<in> B
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. length (nths xs A) \<in> ind_in_set A ` B \<Longrightarrow> length xs \<in> B
[PROOF STEP]
assume "length (nths xs A) \<in> (ind_in_set A ` B)"
[PROOF STATE]
proof (state)
this:
length (nths xs A) \<in> ind_in_set A ` B

goal (1 subgoal):
 1. length (nths xs A) \<in> ind_in_set A ` B \<Longrightarrow> length xs \<in> B
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
length (nths xs A) \<in> ind_in_set A ` B

goal (1 subgoal):
 1. length (nths xs A) \<in> ind_in_set A ` B \<Longrightarrow> length xs \<in> B
[PROOF STEP]
have "length (nths xs A) = card {i. i \<in> A \<and> i < length xs}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (nths xs A) = card {i \<in> A. i < length xs}
[PROOF STEP]
using length_nths[of xs] seteq
[PROOF STATE]
proof (prove)
using this:
length (nths xs ?I) = card {i. i < length xs \<and> i \<in> ?I}
{i. i < length xs \<and> i \<in> A} = {i \<in> A. i < length xs}

goal (1 subgoal):
 1. length (nths xs A) = card {i \<in> A. i < length xs}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
length (nths xs A) = card {i \<in> A. i < length xs}

goal (1 subgoal):
 1. length (nths xs A) \<in> ind_in_set A ` B \<Longrightarrow> length xs \<in> B
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
length (nths xs A) \<in> ind_in_set A ` B
length (nths xs A) = card {i \<in> A. i < length xs}
[PROOF STEP]
have "card {i. i \<in> A \<and> i < length xs} \<in> (ind_in_set A ` B)"
[PROOF STATE]
proof (prove)
using this:
length (nths xs A) \<in> ind_in_set A ` B
length (nths xs A) = card {i \<in> A. i < length xs}

goal (1 subgoal):
 1. card {i \<in> A. i < length xs} \<in> ind_in_set A ` B
[PROOF STEP]
unfolding ind_in_set_def
[PROOF STATE]
proof (prove)
using this:
length (nths xs A) \<in> (\<lambda>x. card {i \<in> A. i < x}) ` B
length (nths xs A) = card {i \<in> A. i < length xs}

goal (1 subgoal):
 1. card {i \<in> A. i < length xs} \<in> (\<lambda>x. card {i \<in> A. i < x}) ` B
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
card {i \<in> A. i < length xs} \<in> ind_in_set A ` B

goal (1 subgoal):
 1. length (nths xs A) \<in> ind_in_set A ` B \<Longrightarrow> length xs \<in> B
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
card {i \<in> A. i < length xs} \<in> ind_in_set A ` B
[PROOF STEP]
show "length xs \<in> B"
[PROOF STATE]
proof (prove)
using this:
card {i \<in> A. i < length xs} \<in> ind_in_set A ` B

goal (1 subgoal):
 1. length xs \<in> B
[PROOF STEP]
using ind_in_set_iff True assms
[PROOF STATE]
proof (prove)
using this:
card {i \<in> A. i < length xs} \<in> ind_in_set A ` B
\<lbrakk>?x \<in> ?A; ?B \<subseteq> ?A\<rbrakk> \<Longrightarrow> (ind_in_set ?A ?x \<in> ind_in_set ?A ` ?B) = (?x \<in> ?B)
length xs \<in> A
B \<subseteq> A

goal (1 subgoal):
 1. length xs \<in> B
[PROOF STEP]
unfolding ind_in_set_def
[PROOF STATE]
proof (prove)
using this:
card {i \<in> A. i < length xs} \<in> (\<lambda>x. card {i \<in> A. i < x}) ` B
\<lbrakk>?x \<in> ?A; ?B \<subseteq> ?A\<rbrakk> \<Longrightarrow> (card {i \<in> ?A. i < ?x} \<in> (\<lambda>x. card {i \<in> ?A. i < x}) ` ?B) = (?x \<in> ?B)
length xs \<in> A
B \<subseteq> A

goal (1 subgoal):
 1. length xs \<in> B
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
length xs \<in> B

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
length (nths xs A) \<in> ind_in_set A ` B \<Longrightarrow> length xs \<in> B

goal (2 subgoals):
 1. length xs \<in> A \<Longrightarrow> nths (nths (xs @ [x]) A) (ind_in_set A ` B) = nths xs B
 2. length xs \<notin> A \<Longrightarrow> nths (nths (xs @ [x]) A) (ind_in_set A ` B) = nths xs B
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
length (nths xs A) \<in> ind_in_set A ` B \<Longrightarrow> length xs \<in> B
[PROOF STEP]
have "length (nths xs A) \<notin> (ind_in_set A ` B)"
[PROOF STATE]
proof (prove)
using this:
length (nths xs A) \<in> ind_in_set A ` B \<Longrightarrow> length xs \<in> B

goal (1 subgoal):
 1. length (nths xs A) \<notin> ind_in_set A ` B
[PROOF STEP]
using False
[PROOF STATE]
proof (prove)
using this:
length (nths xs A) \<in> ind_in_set A ` B \<Longrightarrow> length xs \<in> B
length xs \<notin> B

goal (1 subgoal):
 1. length (nths xs A) \<notin> ind_in_set A ` B
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
length (nths xs A) \<notin> ind_in_set A ` B

goal (2 subgoals):
 1. length xs \<in> A \<Longrightarrow> nths (nths (xs @ [x]) A) (ind_in_set A ` B) = nths xs B
 2. length xs \<notin> A \<Longrightarrow> nths (nths (xs @ [x]) A) (ind_in_set A ` B) = nths xs B
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
length (nths xs A) \<notin> ind_in_set A ` B
[PROOF STEP]
have "nths [x] {l. l + length (nths xs A) \<in> (ind_in_set A ` B)} = []"
[PROOF STATE]
proof (prove)
using this:
length (nths xs A) \<notin> ind_in_set A ` B

goal (1 subgoal):
 1. nths [x] {l. l + length (nths xs A) \<in> ind_in_set A ` B} = []
[PROOF STEP]
using nths_singleton
[PROOF STATE]
proof (prove)
using this:
length (nths xs A) \<notin> ind_in_set A ` B
nths [?x] ?A = (if 0 \<in> ?A then [?x] else [])

goal (1 subgoal):
 1. nths [x] {l. l + length (nths xs A) \<in> ind_in_set A ` B} = []
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
nths [x] {l. l + length (nths xs A) \<in> ind_in_set A ` B} = []

goal (2 subgoals):
 1. length xs \<in> A \<Longrightarrow> nths (nths (xs @ [x]) A) (ind_in_set A ` B) = nths xs B
 2. length xs \<notin> A \<Longrightarrow> nths (nths (xs @ [x]) A) (ind_in_set A ` B) = nths xs B
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
nths [x] {l. l + length (nths xs A) \<in> ind_in_set A ` B} = []
[PROOF STEP]
show "nths (nths (xs @ [x]) A) (ind_in_set A ` B) = nths xs B"
[PROOF STATE]
proof (prove)
using this:
nths [x] {l. l + length (nths xs A) \<in> ind_in_set A ` B} = []

goal (1 subgoal):
 1. nths (nths (xs @ [x]) A) (ind_in_set A ` B) = nths xs B
[PROOF STEP]
using eqT2
[PROOF STATE]
proof (prove)
using this:
nths [x] {l. l + length (nths xs A) \<in> ind_in_set A ` B} = []
nths (nths (xs @ [x]) A) (ind_in_set A ` B) = nths xs B @ nths [x] {l. l + length (nths xs A) \<in> ind_in_set A ` B}

goal (1 subgoal):
 1. nths (nths (xs @ [x]) A) (ind_in_set A ` B) = nths xs B
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
nths (nths (xs @ [x]) A) (ind_in_set A ` B) = nths xs B

goal (1 subgoal):
 1. length xs \<notin> A \<Longrightarrow> nths (nths (xs @ [x]) A) (ind_in_set A ` B) = nths xs B
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. length xs \<notin> A \<Longrightarrow> nths (nths (xs @ [x]) A) (ind_in_set A ` B) = nths xs B
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
length xs \<notin> A

goal (1 subgoal):
 1. length xs \<notin> A \<Longrightarrow> nths (nths (xs @ [x]) A) (ind_in_set A ` B) = nths xs B
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
length xs \<notin> A
[PROOF STEP]
have "nths [x] {l. l + length xs \<in> A} = []"
[PROOF STATE]
proof (prove)
using this:
length xs \<notin> A

goal (1 subgoal):
 1. nths [x] {l. l + length xs \<in> A} = []
[PROOF STEP]
using nths_singleton
[PROOF STATE]
proof (prove)
using this:
length xs \<notin> A
nths [?x] ?A = (if 0 \<in> ?A then [?x] else [])

goal (1 subgoal):
 1. nths [x] {l. l + length xs \<in> A} = []
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
nths [x] {l. l + length xs \<in> A} = []

goal (1 subgoal):
 1. length xs \<notin> A \<Longrightarrow> nths (nths (xs @ [x]) A) (ind_in_set A ` B) = nths xs B
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
nths [x] {l. l + length xs \<in> A} = []

goal (1 subgoal):
 1. length xs \<notin> A \<Longrightarrow> nths (nths (xs @ [x]) A) (ind_in_set A ` B) = nths xs B
[PROOF STEP]
have "nths (xs @ [x]) A = nths xs A @ nths [x] {l. l + length xs \<in> A}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nths (xs @ [x]) A = nths xs A @ nths [x] {l. l + length xs \<in> A}
[PROOF STEP]
using nths_append[of xs]
[PROOF STATE]
proof (prove)
using this:
nths (xs @ ?l') ?A = nths xs ?A @ nths ?l' {j. j + length xs \<in> ?A}

goal (1 subgoal):
 1. nths (xs @ [x]) A = nths xs A @ nths [x] {l. l + length xs \<in> A}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
nths (xs @ [x]) A = nths xs A @ nths [x] {l. l + length xs \<in> A}

goal (1 subgoal):
 1. length xs \<notin> A \<Longrightarrow> nths (nths (xs @ [x]) A) (ind_in_set A ` B) = nths xs B
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
nths [x] {l. l + length xs \<in> A} = []
nths (xs @ [x]) A = nths xs A @ nths [x] {l. l + length xs \<in> A}
[PROOF STEP]
have "nths (xs @ [x]) A = nths xs A"
[PROOF STATE]
proof (prove)
using this:
nths [x] {l. l + length xs \<in> A} = []
nths (xs @ [x]) A = nths xs A @ nths [x] {l. l + length xs \<in> A}

goal (1 subgoal):
 1. nths (xs @ [x]) A = nths xs A
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
nths (xs @ [x]) A = nths xs A

goal (1 subgoal):
 1. length xs \<notin> A \<Longrightarrow> nths (nths (xs @ [x]) A) (ind_in_set A ` B) = nths xs B
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
nths (xs @ [x]) A = nths xs A
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
nths (xs @ [x]) A = nths xs A

goal (1 subgoal):
 1. nths (nths (xs @ [x]) A) (ind_in_set A ` B) = nths xs B
[PROOF STEP]
using snoc
[PROOF STATE]
proof (prove)
using this:
nths (xs @ [x]) A = nths xs A
nths (nths xs A) (ind_in_set A ` B) = nths xs B

goal (1 subgoal):
 1. nths (nths (xs @ [x]) A) (ind_in_set A ` B) = nths xs B
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
nths (nths (xs @ [x]) A) (ind_in_set A ` B) = nths xs B

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
nths (nths (xs @ [x]) A) (ind_in_set A ` B) = nths xs B

goal (1 subgoal):
 1. length xs \<notin> B \<Longrightarrow> nths (nths (xs @ [x]) A) (ind_in_set A ` B) = nths (xs @ [x]) B
[PROOF STEP]
with eqT1
[PROOF STATE]
proof (chain)
picking this:
nths (xs @ [x]) B = nths xs B
nths (nths (xs @ [x]) A) (ind_in_set A ` B) = nths xs B
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
nths (xs @ [x]) B = nths xs B
nths (nths (xs @ [x]) A) (ind_in_set A ` B) = nths xs B

goal (1 subgoal):
 1. nths (nths (xs @ [x]) A) (ind_in_set A ` B) = nths (xs @ [x]) B
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
nths (nths (xs @ [x]) A) (ind_in_set A ` B) = nths (xs @ [x]) B

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
nths (nths (xs @ [x]) A) (ind_in_set A ` B) = nths (xs @ [x]) B

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma nths_reencode_eq_comp:
  assumes "B \<subseteq> A"
  shows "nths (nths xs A) (- ind_in_set A ` B) = nths xs (A - B)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nths (nths xs A) (- ind_in_set A ` B) = nths xs (A - B)
[PROOF STEP]
proof (induction xs rule: rev_induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. nths (nths [] A) (- ind_in_set A ` B) = nths [] (A - B)
 2. \<And>x xs. nths (nths xs A) (- ind_in_set A ` B) = nths xs (A - B) \<Longrightarrow> nths (nths (xs @ [x]) A) (- ind_in_set A ` B) = nths (xs @ [x]) (A - B)
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. nths (nths [] A) (- ind_in_set A ` B) = nths [] (A - B)
 2. \<And>x xs. nths (nths xs A) (- ind_in_set A ` B) = nths xs (A - B) \<Longrightarrow> nths (nths (xs @ [x]) A) (- ind_in_set A ` B) = nths (xs @ [x]) (A - B)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nths (nths [] A) (- ind_in_set A ` B) = nths [] (A - B)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
nths (nths [] A) (- ind_in_set A ` B) = nths [] (A - B)

goal (1 subgoal):
 1. \<And>x xs. nths (nths xs A) (- ind_in_set A ` B) = nths xs (A - B) \<Longrightarrow> nths (nths (xs @ [x]) A) (- ind_in_set A ` B) = nths (xs @ [x]) (A - B)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x xs. nths (nths xs A) (- ind_in_set A ` B) = nths xs (A - B) \<Longrightarrow> nths (nths (xs @ [x]) A) (- ind_in_set A ` B) = nths (xs @ [x]) (A - B)
[PROOF STEP]
case (snoc x xs)
[PROOF STATE]
proof (state)
this:
nths (nths xs A) (- ind_in_set A ` B) = nths xs (A - B)

goal (1 subgoal):
 1. \<And>x xs. nths (nths xs A) (- ind_in_set A ` B) = nths xs (A - B) \<Longrightarrow> nths (nths (xs @ [x]) A) (- ind_in_set A ` B) = nths (xs @ [x]) (A - B)
[PROOF STEP]
have sub20: "A - B \<subseteq> A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A - B \<subseteq> A
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
B \<subseteq> A

goal (1 subgoal):
 1. A - B \<subseteq> A
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
A - B \<subseteq> A

goal (1 subgoal):
 1. \<And>x xs. nths (nths xs A) (- ind_in_set A ` B) = nths xs (A - B) \<Longrightarrow> nths (nths (xs @ [x]) A) (- ind_in_set A ` B) = nths (xs @ [x]) (A - B)
[PROOF STEP]
have seteq: "{i. i < length xs \<and> i \<in> A} = {i. i \<in> A \<and> i < length xs}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {i. i < length xs \<and> i \<in> A} = {i \<in> A. i < length xs}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{i. i < length xs \<and> i \<in> A} = {i \<in> A. i < length xs}

goal (1 subgoal):
 1. \<And>x xs. nths (nths xs A) (- ind_in_set A ` B) = nths xs (A - B) \<Longrightarrow> nths (nths (xs @ [x]) A) (- ind_in_set A ` B) = nths (xs @ [x]) (A - B)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nths (nths (xs @ [x]) A) (- ind_in_set A ` B) = nths (xs @ [x]) (A - B)
[PROOF STEP]
proof (cases "length xs \<in> (A - B)")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. length xs \<in> A - B \<Longrightarrow> nths (nths (xs @ [x]) A) (- ind_in_set A ` B) = nths (xs @ [x]) (A - B)
 2. length xs \<notin> A - B \<Longrightarrow> nths (nths (xs @ [x]) A) (- ind_in_set A ` B) = nths (xs @ [x]) (A - B)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
length xs \<in> A - B

goal (2 subgoals):
 1. length xs \<in> A - B \<Longrightarrow> nths (nths (xs @ [x]) A) (- ind_in_set A ` B) = nths (xs @ [x]) (A - B)
 2. length xs \<notin> A - B \<Longrightarrow> nths (nths (xs @ [x]) A) (- ind_in_set A ` B) = nths (xs @ [x]) (A - B)
[PROOF STEP]
have "nths (xs @ [x]) (A - B) = nths xs (A - B) @ nths [x] {l. l + length xs \<in> (A - B)}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nths (xs @ [x]) (A - B) = nths xs (A - B) @ nths [x] {l. l + length xs \<in> A - B}
[PROOF STEP]
using nths_append[of xs]
[PROOF STATE]
proof (prove)
using this:
nths (xs @ ?l') ?A = nths xs ?A @ nths ?l' {j. j + length xs \<in> ?A}

goal (1 subgoal):
 1. nths (xs @ [x]) (A - B) = nths xs (A - B) @ nths [x] {l. l + length xs \<in> A - B}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
nths (xs @ [x]) (A - B) = nths xs (A - B) @ nths [x] {l. l + length xs \<in> A - B}

goal (2 subgoals):
 1. length xs \<in> A - B \<Longrightarrow> nths (nths (xs @ [x]) A) (- ind_in_set A ` B) = nths (xs @ [x]) (A - B)
 2. length xs \<notin> A - B \<Longrightarrow> nths (nths (xs @ [x]) A) (- ind_in_set A ` B) = nths (xs @ [x]) (A - B)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
nths (xs @ [x]) (A - B) = nths xs (A - B) @ nths [x] {l. l + length xs \<in> A - B}

goal (2 subgoals):
 1. length xs \<in> A - B \<Longrightarrow> nths (nths (xs @ [x]) A) (- ind_in_set A ` B) = nths (xs @ [x]) (A - B)
 2. length xs \<notin> A - B \<Longrightarrow> nths (nths (xs @ [x]) A) (- ind_in_set A ` B) = nths (xs @ [x]) (A - B)
[PROOF STEP]
have "nths [x] {l. l + length xs \<in> (A - B)} = [x]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nths [x] {l. l + length xs \<in> A - B} = [x]
[PROOF STEP]
using nths_singleton True
[PROOF STATE]
proof (prove)
using this:
nths [?x] ?A = (if 0 \<in> ?A then [?x] else [])
length xs \<in> A - B

goal (1 subgoal):
 1. nths [x] {l. l + length xs \<in> A - B} = [x]
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
nths [x] {l. l + length xs \<in> A - B} = [x]

goal (2 subgoals):
 1. length xs \<in> A - B \<Longrightarrow> nths (nths (xs @ [x]) A) (- ind_in_set A ` B) = nths (xs @ [x]) (A - B)
 2. length xs \<notin> A - B \<Longrightarrow> nths (nths (xs @ [x]) A) (- ind_in_set A ` B) = nths (xs @ [x]) (A - B)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
nths (xs @ [x]) (A - B) = nths xs (A - B) @ nths [x] {l. l + length xs \<in> A - B}
nths [x] {l. l + length xs \<in> A - B} = [x]
[PROOF STEP]
have eqT1: "nths (xs @ [x]) (A - B) = nths xs (A - B) @ [x]"
[PROOF STATE]
proof (prove)
using this:
nths (xs @ [x]) (A - B) = nths xs (A - B) @ nths [x] {l. l + length xs \<in> A - B}
nths [x] {l. l + length xs \<in> A - B} = [x]

goal (1 subgoal):
 1. nths (xs @ [x]) (A - B) = nths xs (A - B) @ [x]
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
nths (xs @ [x]) (A - B) = nths xs (A - B) @ [x]

goal (2 subgoals):
 1. length xs \<in> A - B \<Longrightarrow> nths (nths (xs @ [x]) A) (- ind_in_set A ` B) = nths (xs @ [x]) (A - B)
 2. length xs \<notin> A - B \<Longrightarrow> nths (nths (xs @ [x]) A) (- ind_in_set A ` B) = nths (xs @ [x]) (A - B)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
nths (xs @ [x]) (A - B) = nths xs (A - B) @ [x]
[PROOF STEP]
have "length xs \<in> A"
[PROOF STATE]
proof (prove)
using this:
nths (xs @ [x]) (A - B) = nths xs (A - B) @ [x]

goal (1 subgoal):
 1. length xs \<in> A
[PROOF STEP]
using True sub20
[PROOF STATE]
proof (prove)
using this:
nths (xs @ [x]) (A - B) = nths xs (A - B) @ [x]
length xs \<in> A - B
A - B \<subseteq> A

goal (1 subgoal):
 1. length xs \<in> A
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
length xs \<in> A

goal (2 subgoals):
 1. length xs \<in> A - B \<Longrightarrow> nths (nths (xs @ [x]) A) (- ind_in_set A ` B) = nths (xs @ [x]) (A - B)
 2. length xs \<notin> A - B \<Longrightarrow> nths (nths (xs @ [x]) A) (- ind_in_set A ` B) = nths (xs @ [x]) (A - B)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
length xs \<in> A
[PROOF STEP]
have "nths [x] {l. l + length xs \<in> A} = [x]"
[PROOF STATE]
proof (prove)
using this:
length xs \<in> A

goal (1 subgoal):
 1. nths [x] {l. l + length xs \<in> A} = [x]
[PROOF STEP]
using nths_singleton
[PROOF STATE]
proof (prove)
using this:
length xs \<in> A
nths [?x] ?A = (if 0 \<in> ?A then [?x] else [])

goal (1 subgoal):
 1. nths [x] {l. l + length xs \<in> A} = [x]
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
nths [x] {l. l + length xs \<in> A} = [x]

goal (2 subgoals):
 1. length xs \<in> A - B \<Longrightarrow> nths (nths (xs @ [x]) A) (- ind_in_set A ` B) = nths (xs @ [x]) (A - B)
 2. length xs \<notin> A - B \<Longrightarrow> nths (nths (xs @ [x]) A) (- ind_in_set A ` B) = nths (xs @ [x]) (A - B)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
nths [x] {l. l + length xs \<in> A} = [x]

goal (2 subgoals):
 1. length xs \<in> A - B \<Longrightarrow> nths (nths (xs @ [x]) A) (- ind_in_set A ` B) = nths (xs @ [x]) (A - B)
 2. length xs \<notin> A - B \<Longrightarrow> nths (nths (xs @ [x]) A) (- ind_in_set A ` B) = nths (xs @ [x]) (A - B)
[PROOF STEP]
have "nths (xs @ [x]) A = nths xs A @ nths [x] {l. l + length xs \<in> A}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nths (xs @ [x]) A = nths xs A @ nths [x] {l. l + length xs \<in> A}
[PROOF STEP]
using nths_append[of xs]
[PROOF STATE]
proof (prove)
using this:
nths (xs @ ?l') ?A = nths xs ?A @ nths ?l' {j. j + length xs \<in> ?A}

goal (1 subgoal):
 1. nths (xs @ [x]) A = nths xs A @ nths [x] {l. l + length xs \<in> A}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
nths (xs @ [x]) A = nths xs A @ nths [x] {l. l + length xs \<in> A}

goal (2 subgoals):
 1. length xs \<in> A - B \<Longrightarrow> nths (nths (xs @ [x]) A) (- ind_in_set A ` B) = nths (xs @ [x]) (A - B)
 2. length xs \<notin> A - B \<Longrightarrow> nths (nths (xs @ [x]) A) (- ind_in_set A ` B) = nths (xs @ [x]) (A - B)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
nths [x] {l. l + length xs \<in> A} = [x]
nths (xs @ [x]) A = nths xs A @ nths [x] {l. l + length xs \<in> A}
[PROOF STEP]
have "nths (xs @ [x]) A = nths xs A @ [x]"
[PROOF STATE]
proof (prove)
using this:
nths [x] {l. l + length xs \<in> A} = [x]
nths (xs @ [x]) A = nths xs A @ nths [x] {l. l + length xs \<in> A}

goal (1 subgoal):
 1. nths (xs @ [x]) A = nths xs A @ [x]
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
nths (xs @ [x]) A = nths xs A @ [x]

goal (2 subgoals):
 1. length xs \<in> A - B \<Longrightarrow> nths (nths (xs @ [x]) A) (- ind_in_set A ` B) = nths (xs @ [x]) (A - B)
 2. length xs \<notin> A - B \<Longrightarrow> nths (nths (xs @ [x]) A) (- ind_in_set A ` B) = nths (xs @ [x]) (A - B)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
nths (xs @ [x]) A = nths xs A @ [x]
[PROOF STEP]
have "nths (nths (xs @ [x]) A) (- (ind_in_set A) ` B) = nths (nths xs A @ [x]) (- (ind_in_set A) ` B)"
[PROOF STATE]
proof (prove)
using this:
nths (xs @ [x]) A = nths xs A @ [x]

goal (1 subgoal):
 1. nths (nths (xs @ [x]) A) (- ind_in_set A ` B) = nths (nths xs A @ [x]) (- ind_in_set A ` B)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
nths (nths (xs @ [x]) A) (- ind_in_set A ` B) = nths (nths xs A @ [x]) (- ind_in_set A ` B)

goal (2 subgoals):
 1. length xs \<in> A - B \<Longrightarrow> nths (nths (xs @ [x]) A) (- ind_in_set A ` B) = nths (xs @ [x]) (A - B)
 2. length xs \<notin> A - B \<Longrightarrow> nths (nths (xs @ [x]) A) (- ind_in_set A ` B) = nths (xs @ [x]) (A - B)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
nths (nths (xs @ [x]) A) (- ind_in_set A ` B) = nths (nths xs A @ [x]) (- ind_in_set A ` B)
[PROOF STEP]
have eqT2: "nths (nths (xs @ [x]) A) (- (ind_in_set A) ` B)
      = nths xs (A - B) @ (nths [x] {l. l + length (nths xs A) \<in> (- (ind_in_set A) ` B)})"
[PROOF STATE]
proof (prove)
using this:
nths (nths (xs @ [x]) A) (- ind_in_set A ` B) = nths (nths xs A @ [x]) (- ind_in_set A ` B)

goal (1 subgoal):
 1. nths (nths (xs @ [x]) A) (- ind_in_set A ` B) = nths xs (A - B) @ nths [x] {l. l + length (nths xs A) \<in> - ind_in_set A ` B}
[PROOF STEP]
using nths_append[of "nths xs A"] snoc
[PROOF STATE]
proof (prove)
using this:
nths (nths (xs @ [x]) A) (- ind_in_set A ` B) = nths (nths xs A @ [x]) (- ind_in_set A ` B)
nths (nths xs A @ ?l') ?A = nths (nths xs A) ?A @ nths ?l' {j. j + length (nths xs A) \<in> ?A}
nths (nths xs A) (- ind_in_set A ` B) = nths xs (A - B)

goal (1 subgoal):
 1. nths (nths (xs @ [x]) A) (- ind_in_set A ` B) = nths xs (A - B) @ nths [x] {l. l + length (nths xs A) \<in> - ind_in_set A ` B}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
nths (nths (xs @ [x]) A) (- ind_in_set A ` B) = nths xs (A - B) @ nths [x] {l. l + length (nths xs A) \<in> - ind_in_set A ` B}

goal (2 subgoals):
 1. length xs \<in> A - B \<Longrightarrow> nths (nths (xs @ [x]) A) (- ind_in_set A ` B) = nths (xs @ [x]) (A - B)
 2. length xs \<notin> A - B \<Longrightarrow> nths (nths (xs @ [x]) A) (- ind_in_set A ` B) = nths (xs @ [x]) (A - B)
[PROOF STEP]
have "length (nths xs A) \<in> ((ind_in_set A) ` B) \<Longrightarrow> length xs \<in> B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (nths xs A) \<in> ind_in_set A ` B \<Longrightarrow> length xs \<in> B
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. length (nths xs A) \<in> ind_in_set A ` B \<Longrightarrow> length xs \<in> B
[PROOF STEP]
assume "length (nths xs A) \<in> ((ind_in_set A) ` B)"
[PROOF STATE]
proof (state)
this:
length (nths xs A) \<in> ind_in_set A ` B

goal (1 subgoal):
 1. length (nths xs A) \<in> ind_in_set A ` B \<Longrightarrow> length xs \<in> B
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
length (nths xs A) \<in> ind_in_set A ` B

goal (1 subgoal):
 1. length (nths xs A) \<in> ind_in_set A ` B \<Longrightarrow> length xs \<in> B
[PROOF STEP]
have "length (nths xs A) = card {i. i \<in> A \<and> i < length xs}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (nths xs A) = card {i \<in> A. i < length xs}
[PROOF STEP]
using length_nths[of xs] seteq
[PROOF STATE]
proof (prove)
using this:
length (nths xs ?I) = card {i. i < length xs \<and> i \<in> ?I}
{i. i < length xs \<and> i \<in> A} = {i \<in> A. i < length xs}

goal (1 subgoal):
 1. length (nths xs A) = card {i \<in> A. i < length xs}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
length (nths xs A) = card {i \<in> A. i < length xs}

goal (1 subgoal):
 1. length (nths xs A) \<in> ind_in_set A ` B \<Longrightarrow> length xs \<in> B
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
length (nths xs A) \<in> ind_in_set A ` B
length (nths xs A) = card {i \<in> A. i < length xs}
[PROOF STEP]
have "ind_in_set A (length xs) \<in> (ind_in_set A ` B)"
[PROOF STATE]
proof (prove)
using this:
length (nths xs A) \<in> ind_in_set A ` B
length (nths xs A) = card {i \<in> A. i < length xs}

goal (1 subgoal):
 1. ind_in_set A (length xs) \<in> ind_in_set A ` B
[PROOF STEP]
unfolding ind_in_set_def
[PROOF STATE]
proof (prove)
using this:
length (nths xs A) \<in> (\<lambda>x. card {i \<in> A. i < x}) ` B
length (nths xs A) = card {i \<in> A. i < length xs}

goal (1 subgoal):
 1. card {i \<in> A. i < length xs} \<in> (\<lambda>x. card {i \<in> A. i < x}) ` B
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
ind_in_set A (length xs) \<in> ind_in_set A ` B

goal (1 subgoal):
 1. length (nths xs A) \<in> ind_in_set A ` B \<Longrightarrow> length xs \<in> B
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ind_in_set A (length xs) \<in> ind_in_set A ` B
[PROOF STEP]
show "length xs \<in> B"
[PROOF STATE]
proof (prove)
using this:
ind_in_set A (length xs) \<in> ind_in_set A ` B

goal (1 subgoal):
 1. length xs \<in> B
[PROOF STEP]
using ind_in_set_iff True assms
[PROOF STATE]
proof (prove)
using this:
ind_in_set A (length xs) \<in> ind_in_set A ` B
\<lbrakk>?x \<in> ?A; ?B \<subseteq> ?A\<rbrakk> \<Longrightarrow> (ind_in_set ?A ?x \<in> ind_in_set ?A ` ?B) = (?x \<in> ?B)
length xs \<in> A - B
B \<subseteq> A

goal (1 subgoal):
 1. length xs \<in> B
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
length xs \<in> B

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
length (nths xs A) \<in> ind_in_set A ` B \<Longrightarrow> length xs \<in> B

goal (2 subgoals):
 1. length xs \<in> A - B \<Longrightarrow> nths (nths (xs @ [x]) A) (- ind_in_set A ` B) = nths (xs @ [x]) (A - B)
 2. length xs \<notin> A - B \<Longrightarrow> nths (nths (xs @ [x]) A) (- ind_in_set A ` B) = nths (xs @ [x]) (A - B)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
length (nths xs A) \<in> ind_in_set A ` B \<Longrightarrow> length xs \<in> B

goal (2 subgoals):
 1. length xs \<in> A - B \<Longrightarrow> nths (nths (xs @ [x]) A) (- ind_in_set A ` B) = nths (xs @ [x]) (A - B)
 2. length xs \<notin> A - B \<Longrightarrow> nths (nths (xs @ [x]) A) (- ind_in_set A ` B) = nths (xs @ [x]) (A - B)
[PROOF STEP]
have "length xs \<notin> B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length xs \<notin> B
[PROOF STEP]
using True
[PROOF STATE]
proof (prove)
using this:
length xs \<in> A - B

goal (1 subgoal):
 1. length xs \<notin> B
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
length xs \<notin> B

goal (2 subgoals):
 1. length xs \<in> A - B \<Longrightarrow> nths (nths (xs @ [x]) A) (- ind_in_set A ` B) = nths (xs @ [x]) (A - B)
 2. length xs \<notin> A - B \<Longrightarrow> nths (nths (xs @ [x]) A) (- ind_in_set A ` B) = nths (xs @ [x]) (A - B)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
length (nths xs A) \<in> ind_in_set A ` B \<Longrightarrow> length xs \<in> B
length xs \<notin> B
[PROOF STEP]
have "length (nths xs A) \<in> (- (ind_in_set A) ` B)"
[PROOF STATE]
proof (prove)
using this:
length (nths xs A) \<in> ind_in_set A ` B \<Longrightarrow> length xs \<in> B
length xs \<notin> B

goal (1 subgoal):
 1. length (nths xs A) \<in> - ind_in_set A ` B
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
length (nths xs A) \<in> - ind_in_set A ` B

goal (2 subgoals):
 1. length xs \<in> A - B \<Longrightarrow> nths (nths (xs @ [x]) A) (- ind_in_set A ` B) = nths (xs @ [x]) (A - B)
 2. length xs \<notin> A - B \<Longrightarrow> nths (nths (xs @ [x]) A) (- ind_in_set A ` B) = nths (xs @ [x]) (A - B)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
length (nths xs A) \<in> - ind_in_set A ` B
[PROOF STEP]
have "nths [x] {l. l + length (nths xs A) \<in> (- (ind_in_set A) ` B)} = [x]"
[PROOF STATE]
proof (prove)
using this:
length (nths xs A) \<in> - ind_in_set A ` B

goal (1 subgoal):
 1. nths [x] {l. l + length (nths xs A) \<in> - ind_in_set A ` B} = [x]
[PROOF STEP]
using nths_singleton
[PROOF STATE]
proof (prove)
using this:
length (nths xs A) \<in> - ind_in_set A ` B
nths [?x] ?A = (if 0 \<in> ?A then [?x] else [])

goal (1 subgoal):
 1. nths [x] {l. l + length (nths xs A) \<in> - ind_in_set A ` B} = [x]
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
nths [x] {l. l + length (nths xs A) \<in> - ind_in_set A ` B} = [x]

goal (2 subgoals):
 1. length xs \<in> A - B \<Longrightarrow> nths (nths (xs @ [x]) A) (- ind_in_set A ` B) = nths (xs @ [x]) (A - B)
 2. length xs \<notin> A - B \<Longrightarrow> nths (nths (xs @ [x]) A) (- ind_in_set A ` B) = nths (xs @ [x]) (A - B)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
nths [x] {l. l + length (nths xs A) \<in> - ind_in_set A ` B} = [x]
[PROOF STEP]
have "nths (nths (xs @ [x]) A) (- (ind_in_set A) ` B) = nths xs (A - B) @ [x]"
[PROOF STATE]
proof (prove)
using this:
nths [x] {l. l + length (nths xs A) \<in> - ind_in_set A ` B} = [x]

goal (1 subgoal):
 1. nths (nths (xs @ [x]) A) (- ind_in_set A ` B) = nths xs (A - B) @ [x]
[PROOF STEP]
using eqT2
[PROOF STATE]
proof (prove)
using this:
nths [x] {l. l + length (nths xs A) \<in> - ind_in_set A ` B} = [x]
nths (nths (xs @ [x]) A) (- ind_in_set A ` B) = nths xs (A - B) @ nths [x] {l. l + length (nths xs A) \<in> - ind_in_set A ` B}

goal (1 subgoal):
 1. nths (nths (xs @ [x]) A) (- ind_in_set A ` B) = nths xs (A - B) @ [x]
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
nths (nths (xs @ [x]) A) (- ind_in_set A ` B) = nths xs (A - B) @ [x]

goal (2 subgoals):
 1. length xs \<in> A - B \<Longrightarrow> nths (nths (xs @ [x]) A) (- ind_in_set A ` B) = nths (xs @ [x]) (A - B)
 2. length xs \<notin> A - B \<Longrightarrow> nths (nths (xs @ [x]) A) (- ind_in_set A ` B) = nths (xs @ [x]) (A - B)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
nths (nths (xs @ [x]) A) (- ind_in_set A ` B) = nths xs (A - B) @ [x]
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
nths (nths (xs @ [x]) A) (- ind_in_set A ` B) = nths xs (A - B) @ [x]

goal (1 subgoal):
 1. nths (nths (xs @ [x]) A) (- ind_in_set A ` B) = nths (xs @ [x]) (A - B)
[PROOF STEP]
using eqT1
[PROOF STATE]
proof (prove)
using this:
nths (nths (xs @ [x]) A) (- ind_in_set A ` B) = nths xs (A - B) @ [x]
nths (xs @ [x]) (A - B) = nths xs (A - B) @ [x]

goal (1 subgoal):
 1. nths (nths (xs @ [x]) A) (- ind_in_set A ` B) = nths (xs @ [x]) (A - B)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
nths (nths (xs @ [x]) A) (- ind_in_set A ` B) = nths (xs @ [x]) (A - B)

goal (1 subgoal):
 1. length xs \<notin> A - B \<Longrightarrow> nths (nths (xs @ [x]) A) (- ind_in_set A ` B) = nths (xs @ [x]) (A - B)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. length xs \<notin> A - B \<Longrightarrow> nths (nths (xs @ [x]) A) (- ind_in_set A ` B) = nths (xs @ [x]) (A - B)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
length xs \<notin> A - B

goal (1 subgoal):
 1. length xs \<notin> A - B \<Longrightarrow> nths (nths (xs @ [x]) A) (- ind_in_set A ` B) = nths (xs @ [x]) (A - B)
[PROOF STEP]
have "nths (xs @ [x]) (A - B) = nths xs (A - B) @ nths [x] {l. l + length xs \<in> (A - B)}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nths (xs @ [x]) (A - B) = nths xs (A - B) @ nths [x] {l. l + length xs \<in> A - B}
[PROOF STEP]
using nths_append[of xs]
[PROOF STATE]
proof (prove)
using this:
nths (xs @ ?l') ?A = nths xs ?A @ nths ?l' {j. j + length xs \<in> ?A}

goal (1 subgoal):
 1. nths (xs @ [x]) (A - B) = nths xs (A - B) @ nths [x] {l. l + length xs \<in> A - B}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
nths (xs @ [x]) (A - B) = nths xs (A - B) @ nths [x] {l. l + length xs \<in> A - B}

goal (1 subgoal):
 1. length xs \<notin> A - B \<Longrightarrow> nths (nths (xs @ [x]) A) (- ind_in_set A ` B) = nths (xs @ [x]) (A - B)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
nths (xs @ [x]) (A - B) = nths xs (A - B) @ nths [x] {l. l + length xs \<in> A - B}

goal (1 subgoal):
 1. length xs \<notin> A - B \<Longrightarrow> nths (nths (xs @ [x]) A) (- ind_in_set A ` B) = nths (xs @ [x]) (A - B)
[PROOF STEP]
have "nths [x] {l. l + length xs \<in> (A - B)} = []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nths [x] {l. l + length xs \<in> A - B} = []
[PROOF STEP]
using nths_singleton False
[PROOF STATE]
proof (prove)
using this:
nths [?x] ?A = (if 0 \<in> ?A then [?x] else [])
length xs \<notin> A - B

goal (1 subgoal):
 1. nths [x] {l. l + length xs \<in> A - B} = []
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
nths [x] {l. l + length xs \<in> A - B} = []

goal (1 subgoal):
 1. length xs \<notin> A - B \<Longrightarrow> nths (nths (xs @ [x]) A) (- ind_in_set A ` B) = nths (xs @ [x]) (A - B)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
nths (xs @ [x]) (A - B) = nths xs (A - B) @ nths [x] {l. l + length xs \<in> A - B}
nths [x] {l. l + length xs \<in> A - B} = []
[PROOF STEP]
have eqT1: "nths (xs @ [x]) (A - B) = nths xs (A - B)"
[PROOF STATE]
proof (prove)
using this:
nths (xs @ [x]) (A - B) = nths xs (A - B) @ nths [x] {l. l + length xs \<in> A - B}
nths [x] {l. l + length xs \<in> A - B} = []

goal (1 subgoal):
 1. nths (xs @ [x]) (A - B) = nths xs (A - B)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
nths (xs @ [x]) (A - B) = nths xs (A - B)

goal (1 subgoal):
 1. length xs \<notin> A - B \<Longrightarrow> nths (nths (xs @ [x]) A) (- ind_in_set A ` B) = nths (xs @ [x]) (A - B)
[PROOF STEP]
have "nths (nths (xs @ [x]) A) (- (ind_in_set A) ` B) = nths xs (A - B)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nths (nths (xs @ [x]) A) (- ind_in_set A ` B) = nths xs (A - B)
[PROOF STEP]
proof (cases "length xs \<in> A")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. length xs \<in> A \<Longrightarrow> nths (nths (xs @ [x]) A) (- ind_in_set A ` B) = nths xs (A - B)
 2. length xs \<notin> A \<Longrightarrow> nths (nths (xs @ [x]) A) (- ind_in_set A ` B) = nths xs (A - B)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
length xs \<in> A

goal (2 subgoals):
 1. length xs \<in> A \<Longrightarrow> nths (nths (xs @ [x]) A) (- ind_in_set A ` B) = nths xs (A - B)
 2. length xs \<notin> A \<Longrightarrow> nths (nths (xs @ [x]) A) (- ind_in_set A ` B) = nths xs (A - B)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
length xs \<in> A
[PROOF STEP]
have True1: "length xs \<in> B"
[PROOF STATE]
proof (prove)
using this:
length xs \<in> A

goal (1 subgoal):
 1. length xs \<in> B
[PROOF STEP]
using False
[PROOF STATE]
proof (prove)
using this:
length xs \<in> A
length xs \<notin> A - B

goal (1 subgoal):
 1. length xs \<in> B
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
length xs \<in> B

goal (2 subgoals):
 1. length xs \<in> A \<Longrightarrow> nths (nths (xs @ [x]) A) (- ind_in_set A ` B) = nths xs (A - B)
 2. length xs \<notin> A \<Longrightarrow> nths (nths (xs @ [x]) A) (- ind_in_set A ` B) = nths xs (A - B)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
length xs \<in> B
[PROOF STEP]
have "nths [x] {l. l + length xs \<in> A} = [x]"
[PROOF STATE]
proof (prove)
using this:
length xs \<in> B

goal (1 subgoal):
 1. nths [x] {l. l + length xs \<in> A} = [x]
[PROOF STEP]
using nths_singleton True
[PROOF STATE]
proof (prove)
using this:
length xs \<in> B
nths [?x] ?A = (if 0 \<in> ?A then [?x] else [])
length xs \<in> A

goal (1 subgoal):
 1. nths [x] {l. l + length xs \<in> A} = [x]
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
nths [x] {l. l + length xs \<in> A} = [x]

goal (2 subgoals):
 1. length xs \<in> A \<Longrightarrow> nths (nths (xs @ [x]) A) (- ind_in_set A ` B) = nths xs (A - B)
 2. length xs \<notin> A \<Longrightarrow> nths (nths (xs @ [x]) A) (- ind_in_set A ` B) = nths xs (A - B)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
nths [x] {l. l + length xs \<in> A} = [x]

goal (2 subgoals):
 1. length xs \<in> A \<Longrightarrow> nths (nths (xs @ [x]) A) (- ind_in_set A ` B) = nths xs (A - B)
 2. length xs \<notin> A \<Longrightarrow> nths (nths (xs @ [x]) A) (- ind_in_set A ` B) = nths xs (A - B)
[PROOF STEP]
have "nths (xs @ [x]) A = nths xs A @ nths [x] {l. l + length xs \<in> A}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nths (xs @ [x]) A = nths xs A @ nths [x] {l. l + length xs \<in> A}
[PROOF STEP]
using nths_append[of xs]
[PROOF STATE]
proof (prove)
using this:
nths (xs @ ?l') ?A = nths xs ?A @ nths ?l' {j. j + length xs \<in> ?A}

goal (1 subgoal):
 1. nths (xs @ [x]) A = nths xs A @ nths [x] {l. l + length xs \<in> A}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
nths (xs @ [x]) A = nths xs A @ nths [x] {l. l + length xs \<in> A}

goal (2 subgoals):
 1. length xs \<in> A \<Longrightarrow> nths (nths (xs @ [x]) A) (- ind_in_set A ` B) = nths xs (A - B)
 2. length xs \<notin> A \<Longrightarrow> nths (nths (xs @ [x]) A) (- ind_in_set A ` B) = nths xs (A - B)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
nths [x] {l. l + length xs \<in> A} = [x]
nths (xs @ [x]) A = nths xs A @ nths [x] {l. l + length xs \<in> A}
[PROOF STEP]
have "nths (xs @ [x]) A = nths xs A @ [x]"
[PROOF STATE]
proof (prove)
using this:
nths [x] {l. l + length xs \<in> A} = [x]
nths (xs @ [x]) A = nths xs A @ nths [x] {l. l + length xs \<in> A}

goal (1 subgoal):
 1. nths (xs @ [x]) A = nths xs A @ [x]
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
nths (xs @ [x]) A = nths xs A @ [x]

goal (2 subgoals):
 1. length xs \<in> A \<Longrightarrow> nths (nths (xs @ [x]) A) (- ind_in_set A ` B) = nths xs (A - B)
 2. length xs \<notin> A \<Longrightarrow> nths (nths (xs @ [x]) A) (- ind_in_set A ` B) = nths xs (A - B)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
nths (xs @ [x]) A = nths xs A @ [x]
[PROOF STEP]
have "nths (nths (xs @ [x]) A) (- (ind_in_set A) ` B) = nths (nths xs A @ [x]) (- (ind_in_set A) ` B)"
[PROOF STATE]
proof (prove)
using this:
nths (xs @ [x]) A = nths xs A @ [x]

goal (1 subgoal):
 1. nths (nths (xs @ [x]) A) (- ind_in_set A ` B) = nths (nths xs A @ [x]) (- ind_in_set A ` B)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
nths (nths (xs @ [x]) A) (- ind_in_set A ` B) = nths (nths xs A @ [x]) (- ind_in_set A ` B)

goal (2 subgoals):
 1. length xs \<in> A \<Longrightarrow> nths (nths (xs @ [x]) A) (- ind_in_set A ` B) = nths xs (A - B)
 2. length xs \<notin> A \<Longrightarrow> nths (nths (xs @ [x]) A) (- ind_in_set A ` B) = nths xs (A - B)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
nths (nths (xs @ [x]) A) (- ind_in_set A ` B) = nths (nths xs A @ [x]) (- ind_in_set A ` B)
[PROOF STEP]
have eqT2: "nths (nths (xs @ [x]) A) (- (ind_in_set A) ` B)
        = nths xs (A - B) @ (nths [x] {l. l + length (nths xs A) \<in> (- (ind_in_set A) ` B)})"
[PROOF STATE]
proof (prove)
using this:
nths (nths (xs @ [x]) A) (- ind_in_set A ` B) = nths (nths xs A @ [x]) (- ind_in_set A ` B)

goal (1 subgoal):
 1. nths (nths (xs @ [x]) A) (- ind_in_set A ` B) = nths xs (A - B) @ nths [x] {l. l + length (nths xs A) \<in> - ind_in_set A ` B}
[PROOF STEP]
using nths_append[of "nths xs A"] snoc
[PROOF STATE]
proof (prove)
using this:
nths (nths (xs @ [x]) A) (- ind_in_set A ` B) = nths (nths xs A @ [x]) (- ind_in_set A ` B)
nths (nths xs A @ ?l') ?A = nths (nths xs A) ?A @ nths ?l' {j. j + length (nths xs A) \<in> ?A}
nths (nths xs A) (- ind_in_set A ` B) = nths xs (A - B)

goal (1 subgoal):
 1. nths (nths (xs @ [x]) A) (- ind_in_set A ` B) = nths xs (A - B) @ nths [x] {l. l + length (nths xs A) \<in> - ind_in_set A ` B}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
nths (nths (xs @ [x]) A) (- ind_in_set A ` B) = nths xs (A - B) @ nths [x] {l. l + length (nths xs A) \<in> - ind_in_set A ` B}

goal (2 subgoals):
 1. length xs \<in> A \<Longrightarrow> nths (nths (xs @ [x]) A) (- ind_in_set A ` B) = nths xs (A - B)
 2. length xs \<notin> A \<Longrightarrow> nths (nths (xs @ [x]) A) (- ind_in_set A ` B) = nths xs (A - B)
[PROOF STEP]
have "length (nths xs A) \<in> ((ind_in_set A) ` B)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (nths xs A) \<in> ind_in_set A ` B
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. length (nths xs A) \<in> ind_in_set A ` B
[PROOF STEP]
have "length (nths xs A) = card {i. i \<in> A \<and> i < length xs}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (nths xs A) = card {i \<in> A. i < length xs}
[PROOF STEP]
using length_nths[of xs] seteq
[PROOF STATE]
proof (prove)
using this:
length (nths xs ?I) = card {i. i < length xs \<and> i \<in> ?I}
{i. i < length xs \<and> i \<in> A} = {i \<in> A. i < length xs}

goal (1 subgoal):
 1. length (nths xs A) = card {i \<in> A. i < length xs}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
length (nths xs A) = card {i \<in> A. i < length xs}

goal (1 subgoal):
 1. length (nths xs A) \<in> ind_in_set A ` B
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
length (nths xs A) = card {i \<in> A. i < length xs}

goal (1 subgoal):
 1. length (nths xs A) \<in> ind_in_set A ` B
[PROOF STEP]
have "card {i. i \<in> A \<and> i < length xs} \<in> (ind_in_set A ` B)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card {i \<in> A. i < length xs} \<in> ind_in_set A ` B
[PROOF STEP]
unfolding ind_in_set_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card {i \<in> A. i < length xs} \<in> (\<lambda>x. card {i \<in> A. i < x}) ` B
[PROOF STEP]
using True ind_in_set_iff[of "length xs"] True1
[PROOF STATE]
proof (prove)
using this:
length xs \<in> A
\<lbrakk>length xs \<in> ?A; ?B \<subseteq> ?A\<rbrakk> \<Longrightarrow> (ind_in_set ?A (length xs) \<in> ind_in_set ?A ` ?B) = (length xs \<in> ?B)
length xs \<in> B

goal (1 subgoal):
 1. card {i \<in> A. i < length xs} \<in> (\<lambda>x. card {i \<in> A. i < x}) ` B
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
card {i \<in> A. i < length xs} \<in> ind_in_set A ` B

goal (1 subgoal):
 1. length (nths xs A) \<in> ind_in_set A ` B
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
length (nths xs A) = card {i \<in> A. i < length xs}
card {i \<in> A. i < length xs} \<in> ind_in_set A ` B
[PROOF STEP]
show "length (nths xs A) \<in> (ind_in_set A) ` B"
[PROOF STATE]
proof (prove)
using this:
length (nths xs A) = card {i \<in> A. i < length xs}
card {i \<in> A. i < length xs} \<in> ind_in_set A ` B

goal (1 subgoal):
 1. length (nths xs A) \<in> ind_in_set A ` B
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
length (nths xs A) \<in> ind_in_set A ` B

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
length (nths xs A) \<in> ind_in_set A ` B

goal (2 subgoals):
 1. length xs \<in> A \<Longrightarrow> nths (nths (xs @ [x]) A) (- ind_in_set A ` B) = nths xs (A - B)
 2. length xs \<notin> A \<Longrightarrow> nths (nths (xs @ [x]) A) (- ind_in_set A ` B) = nths xs (A - B)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
length (nths xs A) \<in> ind_in_set A ` B
[PROOF STEP]
have "nths [x] {l. l + length (nths xs A) \<in> (- (ind_in_set A) ` B)} = []"
[PROOF STATE]
proof (prove)
using this:
length (nths xs A) \<in> ind_in_set A ` B

goal (1 subgoal):
 1. nths [x] {l. l + length (nths xs A) \<in> - ind_in_set A ` B} = []
[PROOF STEP]
using nths_singleton
[PROOF STATE]
proof (prove)
using this:
length (nths xs A) \<in> ind_in_set A ` B
nths [?x] ?A = (if 0 \<in> ?A then [?x] else [])

goal (1 subgoal):
 1. nths [x] {l. l + length (nths xs A) \<in> - ind_in_set A ` B} = []
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
nths [x] {l. l + length (nths xs A) \<in> - ind_in_set A ` B} = []

goal (2 subgoals):
 1. length xs \<in> A \<Longrightarrow> nths (nths (xs @ [x]) A) (- ind_in_set A ` B) = nths xs (A - B)
 2. length xs \<notin> A \<Longrightarrow> nths (nths (xs @ [x]) A) (- ind_in_set A ` B) = nths xs (A - B)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
nths [x] {l. l + length (nths xs A) \<in> - ind_in_set A ` B} = []
[PROOF STEP]
show "nths (nths (xs @ [x]) A) (- (ind_in_set A) ` B) = nths xs (A - B)"
[PROOF STATE]
proof (prove)
using this:
nths [x] {l. l + length (nths xs A) \<in> - ind_in_set A ` B} = []

goal (1 subgoal):
 1. nths (nths (xs @ [x]) A) (- ind_in_set A ` B) = nths xs (A - B)
[PROOF STEP]
using eqT2
[PROOF STATE]
proof (prove)
using this:
nths [x] {l. l + length (nths xs A) \<in> - ind_in_set A ` B} = []
nths (nths (xs @ [x]) A) (- ind_in_set A ` B) = nths xs (A - B) @ nths [x] {l. l + length (nths xs A) \<in> - ind_in_set A ` B}

goal (1 subgoal):
 1. nths (nths (xs @ [x]) A) (- ind_in_set A ` B) = nths xs (A - B)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
nths (nths (xs @ [x]) A) (- ind_in_set A ` B) = nths xs (A - B)

goal (1 subgoal):
 1. length xs \<notin> A \<Longrightarrow> nths (nths (xs @ [x]) A) (- ind_in_set A ` B) = nths xs (A - B)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. length xs \<notin> A \<Longrightarrow> nths (nths (xs @ [x]) A) (- ind_in_set A ` B) = nths xs (A - B)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
length xs \<notin> A

goal (1 subgoal):
 1. length xs \<notin> A \<Longrightarrow> nths (nths (xs @ [x]) A) (- ind_in_set A ` B) = nths xs (A - B)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
length xs \<notin> A
[PROOF STEP]
have "nths [x] {l. l + length xs \<in> A} = []"
[PROOF STATE]
proof (prove)
using this:
length xs \<notin> A

goal (1 subgoal):
 1. nths [x] {l. l + length xs \<in> A} = []
[PROOF STEP]
using nths_singleton
[PROOF STATE]
proof (prove)
using this:
length xs \<notin> A
nths [?x] ?A = (if 0 \<in> ?A then [?x] else [])

goal (1 subgoal):
 1. nths [x] {l. l + length xs \<in> A} = []
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
nths [x] {l. l + length xs \<in> A} = []

goal (1 subgoal):
 1. length xs \<notin> A \<Longrightarrow> nths (nths (xs @ [x]) A) (- ind_in_set A ` B) = nths xs (A - B)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
nths [x] {l. l + length xs \<in> A} = []

goal (1 subgoal):
 1. length xs \<notin> A \<Longrightarrow> nths (nths (xs @ [x]) A) (- ind_in_set A ` B) = nths xs (A - B)
[PROOF STEP]
have "nths (xs @ [x]) A = nths xs A @ nths [x] {l. l + length xs \<in> A}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nths (xs @ [x]) A = nths xs A @ nths [x] {l. l + length xs \<in> A}
[PROOF STEP]
using nths_append[of xs]
[PROOF STATE]
proof (prove)
using this:
nths (xs @ ?l') ?A = nths xs ?A @ nths ?l' {j. j + length xs \<in> ?A}

goal (1 subgoal):
 1. nths (xs @ [x]) A = nths xs A @ nths [x] {l. l + length xs \<in> A}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
nths (xs @ [x]) A = nths xs A @ nths [x] {l. l + length xs \<in> A}

goal (1 subgoal):
 1. length xs \<notin> A \<Longrightarrow> nths (nths (xs @ [x]) A) (- ind_in_set A ` B) = nths xs (A - B)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
nths [x] {l. l + length xs \<in> A} = []
nths (xs @ [x]) A = nths xs A @ nths [x] {l. l + length xs \<in> A}
[PROOF STEP]
have "nths (xs @ [x]) A = nths xs A"
[PROOF STATE]
proof (prove)
using this:
nths [x] {l. l + length xs \<in> A} = []
nths (xs @ [x]) A = nths xs A @ nths [x] {l. l + length xs \<in> A}

goal (1 subgoal):
 1. nths (xs @ [x]) A = nths xs A
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
nths (xs @ [x]) A = nths xs A

goal (1 subgoal):
 1. length xs \<notin> A \<Longrightarrow> nths (nths (xs @ [x]) A) (- ind_in_set A ` B) = nths xs (A - B)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
nths (xs @ [x]) A = nths xs A
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
nths (xs @ [x]) A = nths xs A

goal (1 subgoal):
 1. nths (nths (xs @ [x]) A) (- ind_in_set A ` B) = nths xs (A - B)
[PROOF STEP]
using snoc
[PROOF STATE]
proof (prove)
using this:
nths (xs @ [x]) A = nths xs A
nths (nths xs A) (- ind_in_set A ` B) = nths xs (A - B)

goal (1 subgoal):
 1. nths (nths (xs @ [x]) A) (- ind_in_set A ` B) = nths xs (A - B)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
nths (nths (xs @ [x]) A) (- ind_in_set A ` B) = nths xs (A - B)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
nths (nths (xs @ [x]) A) (- ind_in_set A ` B) = nths xs (A - B)

goal (1 subgoal):
 1. length xs \<notin> A - B \<Longrightarrow> nths (nths (xs @ [x]) A) (- ind_in_set A ` B) = nths (xs @ [x]) (A - B)
[PROOF STEP]
with eqT1
[PROOF STATE]
proof (chain)
picking this:
nths (xs @ [x]) (A - B) = nths xs (A - B)
nths (nths (xs @ [x]) A) (- ind_in_set A ` B) = nths xs (A - B)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
nths (xs @ [x]) (A - B) = nths xs (A - B)
nths (nths (xs @ [x]) A) (- ind_in_set A ` B) = nths xs (A - B)

goal (1 subgoal):
 1. nths (nths (xs @ [x]) A) (- ind_in_set A ` B) = nths (xs @ [x]) (A - B)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
nths (nths (xs @ [x]) A) (- ind_in_set A ` B) = nths (xs @ [x]) (A - B)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
nths (nths (xs @ [x]) A) (- ind_in_set A ` B) = nths (xs @ [x]) (A - B)

goal:
No subgoals!
[PROOF STEP]
qed