[STATEMENT]
lemma (in vfsequence) vfsequence_vrange_vproduct:
  assumes "\<And>i. i \<in>\<^sub>\<circ> vcard xs \<Longrightarrow> xs\<lparr>i\<rparr> \<in>\<^sub>\<circ> A i"
  shows "xs \<in>\<^sub>\<circ> (\<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>vcard xs. A i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. xs \<in>\<^sub>\<circ> vproduct (vcard xs) A
[PROOF STEP]
using vfsequence_vdomain vsv_axioms assms
[PROOF STATE]
proof (prove)
using this:
\<D>\<^sub>\<circ> xs = vcard xs
vsv xs
?i \<in>\<^sub>\<circ> vcard xs \<Longrightarrow> xs\<lparr>?i\<rparr> \<in>\<^sub>\<circ> A ?i

goal (1 subgoal):
 1. xs \<in>\<^sub>\<circ> vproduct (vcard xs) A
[PROOF STEP]
by
    (
      intro vproductI;
      (intro vsv.vsv_vrange_vsubset_vifunion_app | tactic\<open>all_tac\<close>)
    ) auto


[STATEMENT]
lemma (in vfsequence) vfsequence_vrange_vcpower:
  assumes "\<R>\<^sub>\<circ> xs \<subseteq>\<^sub>\<circ> A"
  shows "xs \<in>\<^sub>\<circ> A ^\<^sub>\<times> (vcard xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. xs \<in>\<^sub>\<circ> A ^\<^sub>\<times> vcard xs
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<R>\<^sub>\<circ> xs \<subseteq>\<^sub>\<circ> A

goal (1 subgoal):
 1. xs \<in>\<^sub>\<circ> A ^\<^sub>\<times> vcard xs
[PROOF STEP]
proof(elim vsubsetE; intro vcpowerI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>\<And>x. x \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> xs \<Longrightarrow> x \<in>\<^sub>\<circ> A; \<R>\<^sub>\<circ> xs \<subseteq>\<^sub>\<circ> A\<rbrakk> \<Longrightarrow> xs \<in>\<^sub>\<circ> (\<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>vcard xs. A)
[PROOF STEP]
assume hyp: "x \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> xs \<Longrightarrow> x \<in>\<^sub>\<circ> A" for x
[PROOF STATE]
proof (state)
this:
?x \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> xs \<Longrightarrow> ?x \<in>\<^sub>\<circ> A

goal (1 subgoal):
 1. \<lbrakk>\<And>x. x \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> xs \<Longrightarrow> x \<in>\<^sub>\<circ> A; \<R>\<^sub>\<circ> xs \<subseteq>\<^sub>\<circ> A\<rbrakk> \<Longrightarrow> xs \<in>\<^sub>\<circ> (\<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>vcard xs. A)
[PROOF STEP]
from vfsequence_vdomain
[PROOF STATE]
proof (chain)
picking this:
\<D>\<^sub>\<circ> xs = vcard xs
[PROOF STEP]
show "xs \<in>\<^sub>\<circ> (\<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>vcard xs. A)"
[PROOF STATE]
proof (prove)
using this:
\<D>\<^sub>\<circ> xs = vcard xs

goal (1 subgoal):
 1. xs \<in>\<^sub>\<circ> (\<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>vcard xs. A)
[PROOF STEP]
by (intro vproductI) (blast intro: hyp elim: vdomain_atE)+
[PROOF STATE]
proof (state)
this:
xs \<in>\<^sub>\<circ> (\<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>vcard xs. A)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma vconsI[intro!]:
  assumes "a \<in>\<^sub>\<circ> vinsert \<langle>vcard xs, x\<rangle> xs"
  shows "a \<in>\<^sub>\<circ> xs #\<^sub>\<circ> x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<in>\<^sub>\<circ> xs #\<^sub>\<circ> x
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
a \<in>\<^sub>\<circ> vinsert \<langle>vcard xs, x\<rangle> xs

goal (1 subgoal):
 1. a \<in>\<^sub>\<circ> xs #\<^sub>\<circ> x
[PROOF STEP]
unfolding vcons_def
[PROOF STATE]
proof (prove)
using this:
a \<in>\<^sub>\<circ> vinsert \<langle>vcard xs, x\<rangle> xs

goal (1 subgoal):
 1. a \<in>\<^sub>\<circ> vinsert \<langle>vcard xs, x\<rangle> xs
[PROOF STEP]
by clarsimp


[STATEMENT]
lemma vconsD[dest!]:
  assumes "a \<in>\<^sub>\<circ> xs #\<^sub>\<circ> x"
  shows "a \<in>\<^sub>\<circ> vinsert \<langle>vcard xs, x\<rangle> xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<in>\<^sub>\<circ> vinsert \<langle>vcard xs, x\<rangle> xs
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
a \<in>\<^sub>\<circ> xs #\<^sub>\<circ> x

goal (1 subgoal):
 1. a \<in>\<^sub>\<circ> vinsert \<langle>vcard xs, x\<rangle> xs
[PROOF STEP]
unfolding vcons_def
[PROOF STATE]
proof (prove)
using this:
a \<in>\<^sub>\<circ> vinsert \<langle>vcard xs, x\<rangle> xs

goal (1 subgoal):
 1. a \<in>\<^sub>\<circ> vinsert \<langle>vcard xs, x\<rangle> xs
[PROOF STEP]
by clarsimp


[STATEMENT]
lemma vconsE[elim!]:
  assumes "a \<in>\<^sub>\<circ> xs #\<^sub>\<circ> x"
  obtains a where "a \<in>\<^sub>\<circ> vinsert \<langle>vcard xs, x\<rangle> xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>a. a \<in>\<^sub>\<circ> vinsert \<langle>vcard xs, x\<rangle> xs \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
a \<in>\<^sub>\<circ> xs #\<^sub>\<circ> x

goal (1 subgoal):
 1. (\<And>a. a \<in>\<^sub>\<circ> vinsert \<langle>vcard xs, x\<rangle> xs \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding vcons_def
[PROOF STATE]
proof (prove)
using this:
a \<in>\<^sub>\<circ> vinsert \<langle>vcard xs, x\<rangle> xs

goal (1 subgoal):
 1. (\<And>a. a \<in>\<^sub>\<circ> vinsert \<langle>vcard xs, x\<rangle> xs \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by clarsimp


[STATEMENT]
lemma vcons_neq_vempty[simp]: "ys #\<^sub>\<circ> y \<noteq> []\<^sub>\<circ>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ys #\<^sub>\<circ> y \<noteq> []\<^sub>\<circ>
[PROOF STEP]
by auto


[STATEMENT]
lemma vcons_vsingleton: "[a]\<^sub>\<circ> = set {\<langle>0\<^sub>\<nat>, a\<rangle>}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [a]\<^sub>\<circ> = set {\<langle>0\<^sub>\<nat>, a\<rangle>}
[PROOF STEP]
unfolding vcons_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vinsert \<langle>vcard []\<^sub>\<circ>, a\<rangle> []\<^sub>\<circ> = set {\<langle>0\<^sub>\<nat>, a\<rangle>}
[PROOF STEP]
by simp


[STATEMENT]
lemma vcons_vdoubleton: "[a, b]\<^sub>\<circ> = set {\<langle>0\<^sub>\<nat>, a\<rangle>, \<langle>1\<^sub>\<nat>, b\<rangle>}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [a, b]\<^sub>\<circ> = set {\<langle>0\<^sub>\<nat>, a\<rangle>, \<langle>1\<^sub>\<nat>, b\<rangle>}
[PROOF STEP]
unfolding vcons_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vinsert \<langle>vcard (vinsert \<langle>vcard []\<^sub>\<circ>, a\<rangle> []\<^sub>\<circ>), b\<rangle> (vinsert \<langle>vcard []\<^sub>\<circ>, a\<rangle> []\<^sub>\<circ>) = set {\<langle>0\<^sub>\<nat>, a\<rangle>, \<langle>1\<^sub>\<nat>, b\<rangle>}
[PROOF STEP]
using vinsert_vsingleton
[PROOF STATE]
proof (prove)
using this:
vinsert ?a (set {?b}) = set {?a, ?b}

goal (1 subgoal):
 1. vinsert \<langle>vcard (vinsert \<langle>vcard []\<^sub>\<circ>, a\<rangle> []\<^sub>\<circ>), b\<rangle> (vinsert \<langle>vcard []\<^sub>\<circ>, a\<rangle> []\<^sub>\<circ>) = set {\<langle>0\<^sub>\<nat>, a\<rangle>, \<langle>1\<^sub>\<nat>, b\<rangle>}
[PROOF STEP]
by (force simp: vinsert_set_insert_eq)


[STATEMENT]
lemma vcons_vsubset: "xs \<subseteq>\<^sub>\<circ> xs #\<^sub>\<circ> x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. xs \<subseteq>\<^sub>\<circ> xs #\<^sub>\<circ> x
[PROOF STEP]
by clarsimp


[STATEMENT]
lemma vcons_vsubset':
  assumes "vcons xs x \<subseteq>\<^sub>\<circ> ys"
  shows "vcons xs x \<subseteq>\<^sub>\<circ> vcons ys y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. xs #\<^sub>\<circ> x \<subseteq>\<^sub>\<circ> ys #\<^sub>\<circ> y
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
xs #\<^sub>\<circ> x \<subseteq>\<^sub>\<circ> ys

goal (1 subgoal):
 1. xs #\<^sub>\<circ> x \<subseteq>\<^sub>\<circ> ys #\<^sub>\<circ> y
[PROOF STEP]
unfolding vcons_def
[PROOF STATE]
proof (prove)
using this:
vinsert \<langle>vcard xs, x\<rangle> xs \<subseteq>\<^sub>\<circ> ys

goal (1 subgoal):
 1. vinsert \<langle>vcard xs, x\<rangle> xs \<subseteq>\<^sub>\<circ> vinsert \<langle>vcard ys, y\<rangle> ys
[PROOF STEP]
by auto


[STATEMENT]
lemma (in vfsequence) vfsequence_vcons[intro, simp]: "vfsequence (xs #\<^sub>\<circ> x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vfsequence (xs #\<^sub>\<circ> x)
[PROOF STEP]
proof(intro vfsequenceI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. vsv (xs #\<^sub>\<circ> x)
 2. \<D>\<^sub>\<circ> (xs #\<^sub>\<circ> x) \<in>\<^sub>\<circ> \<omega>
[PROOF STEP]
from vfsequence_vdomain_in_omega vsv_vcard_vdomain
[PROOF STATE]
proof (chain)
picking this:
\<D>\<^sub>\<circ> xs \<in>\<^sub>\<circ> \<omega>
vcard (\<D>\<^sub>\<circ> xs) = vcard xs
[PROOF STEP]
have "vcard xs = \<D>\<^sub>\<circ> xs"
[PROOF STATE]
proof (prove)
using this:
\<D>\<^sub>\<circ> xs \<in>\<^sub>\<circ> \<omega>
vcard (\<D>\<^sub>\<circ> xs) = vcard xs

goal (1 subgoal):
 1. vcard xs = \<D>\<^sub>\<circ> xs
[PROOF STEP]
by (simp add: vcard_veqpoll)
[PROOF STATE]
proof (state)
this:
vcard xs = \<D>\<^sub>\<circ> xs

goal (2 subgoals):
 1. vsv (xs #\<^sub>\<circ> x)
 2. \<D>\<^sub>\<circ> (xs #\<^sub>\<circ> x) \<in>\<^sub>\<circ> \<omega>
[PROOF STEP]
show "vsv (xs #\<^sub>\<circ> x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vsv (xs #\<^sub>\<circ> x)
[PROOF STEP]
proof(intro vsvI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. vbrelation (xs #\<^sub>\<circ> x)
 2. \<And>a b c. \<lbrakk>\<langle>a, b\<rangle> \<in>\<^sub>\<circ> xs #\<^sub>\<circ> x; \<langle>a, c\<rangle> \<in>\<^sub>\<circ> xs #\<^sub>\<circ> x\<rbrakk> \<Longrightarrow> b = c
[PROOF STEP]
fix a b c
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. vbrelation (xs #\<^sub>\<circ> x)
 2. \<And>a b c. \<lbrakk>\<langle>a, b\<rangle> \<in>\<^sub>\<circ> xs #\<^sub>\<circ> x; \<langle>a, c\<rangle> \<in>\<^sub>\<circ> xs #\<^sub>\<circ> x\<rbrakk> \<Longrightarrow> b = c
[PROOF STEP]
assume ab: "\<langle>a, b\<rangle> \<in>\<^sub>\<circ> xs #\<^sub>\<circ> x" and ac: "\<langle>a, c\<rangle> \<in>\<^sub>\<circ> xs #\<^sub>\<circ> x"
[PROOF STATE]
proof (state)
this:
\<langle>a, b\<rangle> \<in>\<^sub>\<circ> xs #\<^sub>\<circ> x
\<langle>a, c\<rangle> \<in>\<^sub>\<circ> xs #\<^sub>\<circ> x

goal (2 subgoals):
 1. vbrelation (xs #\<^sub>\<circ> x)
 2. \<And>a b c. \<lbrakk>\<langle>a, b\<rangle> \<in>\<^sub>\<circ> xs #\<^sub>\<circ> x; \<langle>a, c\<rangle> \<in>\<^sub>\<circ> xs #\<^sub>\<circ> x\<rbrakk> \<Longrightarrow> b = c
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<langle>a, b\<rangle> \<in>\<^sub>\<circ> xs #\<^sub>\<circ> x
\<langle>a, c\<rangle> \<in>\<^sub>\<circ> xs #\<^sub>\<circ> x
[PROOF STEP]
consider (dom) "a \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> xs" | (ndom) "a = vcard xs"
[PROOF STATE]
proof (prove)
using this:
\<langle>a, b\<rangle> \<in>\<^sub>\<circ> xs #\<^sub>\<circ> x
\<langle>a, c\<rangle> \<in>\<^sub>\<circ> xs #\<^sub>\<circ> x

goal (1 subgoal):
 1. \<lbrakk>a \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> xs \<Longrightarrow> thesis; a = vcard xs \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
unfolding vcons_def
[PROOF STATE]
proof (prove)
using this:
\<langle>a, b\<rangle> \<in>\<^sub>\<circ> vinsert \<langle>vcard xs, x\<rangle> xs
\<langle>a, c\<rangle> \<in>\<^sub>\<circ> vinsert \<langle>vcard xs, x\<rangle> xs

goal (1 subgoal):
 1. \<lbrakk>a \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> xs \<Longrightarrow> thesis; a = vcard xs \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<lbrakk>a \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> xs \<Longrightarrow> ?thesis; a = vcard xs \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (2 subgoals):
 1. vbrelation (xs #\<^sub>\<circ> x)
 2. \<And>a b c. \<lbrakk>\<langle>a, b\<rangle> \<in>\<^sub>\<circ> xs #\<^sub>\<circ> x; \<langle>a, c\<rangle> \<in>\<^sub>\<circ> xs #\<^sub>\<circ> x\<rbrakk> \<Longrightarrow> b = c
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>a \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> xs \<Longrightarrow> ?thesis; a = vcard xs \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis
[PROOF STEP]
show "b = c"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>a \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> xs \<Longrightarrow> ?thesis; a = vcard xs \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. b = c
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. a \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> xs \<Longrightarrow> b = c
 2. a = vcard xs \<Longrightarrow> b = c
[PROOF STEP]
case dom
[PROOF STATE]
proof (state)
this:
a \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> xs

goal (2 subgoals):
 1. a \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> xs \<Longrightarrow> b = c
 2. a = vcard xs \<Longrightarrow> b = c
[PROOF STEP]
with ab
[PROOF STATE]
proof (chain)
picking this:
\<langle>a, b\<rangle> \<in>\<^sub>\<circ> xs #\<^sub>\<circ> x
a \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> xs
[PROOF STEP]
have "\<langle>a, b\<rangle> \<in>\<^sub>\<circ> xs"
[PROOF STATE]
proof (prove)
using this:
\<langle>a, b\<rangle> \<in>\<^sub>\<circ> xs #\<^sub>\<circ> x
a \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> xs

goal (1 subgoal):
 1. \<langle>a, b\<rangle> \<in>\<^sub>\<circ> xs
[PROOF STEP]
unfolding vcons_def
[PROOF STATE]
proof (prove)
using this:
\<langle>a, b\<rangle> \<in>\<^sub>\<circ> vinsert \<langle>vcard xs, x\<rangle> xs
a \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> xs

goal (1 subgoal):
 1. \<langle>a, b\<rangle> \<in>\<^sub>\<circ> xs
[PROOF STEP]
by (auto simp: \<open>vcard xs = \<D>\<^sub>\<circ> xs\<close>)
[PROOF STATE]
proof (state)
this:
\<langle>a, b\<rangle> \<in>\<^sub>\<circ> xs

goal (2 subgoals):
 1. a \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> xs \<Longrightarrow> b = c
 2. a = vcard xs \<Longrightarrow> b = c
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<langle>a, b\<rangle> \<in>\<^sub>\<circ> xs

goal (2 subgoals):
 1. a \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> xs \<Longrightarrow> b = c
 2. a = vcard xs \<Longrightarrow> b = c
[PROOF STEP]
from dom ac
[PROOF STATE]
proof (chain)
picking this:
a \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> xs
\<langle>a, c\<rangle> \<in>\<^sub>\<circ> xs #\<^sub>\<circ> x
[PROOF STEP]
have "\<langle>a, c\<rangle> \<in>\<^sub>\<circ> xs"
[PROOF STATE]
proof (prove)
using this:
a \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> xs
\<langle>a, c\<rangle> \<in>\<^sub>\<circ> xs #\<^sub>\<circ> x

goal (1 subgoal):
 1. \<langle>a, c\<rangle> \<in>\<^sub>\<circ> xs
[PROOF STEP]
unfolding vcons_def
[PROOF STATE]
proof (prove)
using this:
a \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> xs
\<langle>a, c\<rangle> \<in>\<^sub>\<circ> vinsert \<langle>vcard xs, x\<rangle> xs

goal (1 subgoal):
 1. \<langle>a, c\<rangle> \<in>\<^sub>\<circ> xs
[PROOF STEP]
by (auto simp: \<open>vcard xs = \<D>\<^sub>\<circ> xs\<close>)
[PROOF STATE]
proof (state)
this:
\<langle>a, c\<rangle> \<in>\<^sub>\<circ> xs

goal (2 subgoals):
 1. a \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> xs \<Longrightarrow> b = c
 2. a = vcard xs \<Longrightarrow> b = c
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<langle>a, b\<rangle> \<in>\<^sub>\<circ> xs
\<langle>a, c\<rangle> \<in>\<^sub>\<circ> xs
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<langle>a, b\<rangle> \<in>\<^sub>\<circ> xs
\<langle>a, c\<rangle> \<in>\<^sub>\<circ> xs

goal (1 subgoal):
 1. b = c
[PROOF STEP]
using vsv
[PROOF STATE]
proof (prove)
using this:
\<langle>a, b\<rangle> \<in>\<^sub>\<circ> xs
\<langle>a, c\<rangle> \<in>\<^sub>\<circ> xs
\<lbrakk>\<langle>?a, ?b\<rangle> \<in>\<^sub>\<circ> xs; \<langle>?a, ?c\<rangle> \<in>\<^sub>\<circ> xs\<rbrakk> \<Longrightarrow> ?b = ?c

goal (1 subgoal):
 1. b = c
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
b = c

goal (1 subgoal):
 1. a = vcard xs \<Longrightarrow> b = c
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. a = vcard xs \<Longrightarrow> b = c
[PROOF STEP]
case ndom
[PROOF STATE]
proof (state)
this:
a = vcard xs

goal (1 subgoal):
 1. a = vcard xs \<Longrightarrow> b = c
[PROOF STEP]
from ab
[PROOF STATE]
proof (chain)
picking this:
\<langle>a, b\<rangle> \<in>\<^sub>\<circ> xs #\<^sub>\<circ> x
[PROOF STEP]
have "\<langle>a, b\<rangle> = \<langle>vcard xs, x\<rangle>"
[PROOF STATE]
proof (prove)
using this:
\<langle>a, b\<rangle> \<in>\<^sub>\<circ> xs #\<^sub>\<circ> x

goal (1 subgoal):
 1. \<langle>a, b\<rangle> = \<langle>vcard xs, x\<rangle>
[PROOF STEP]
unfolding ndom vcons_def
[PROOF STATE]
proof (prove)
using this:
\<langle>vcard xs, b\<rangle> \<in>\<^sub>\<circ> vinsert \<langle>vcard xs, x\<rangle> xs

goal (1 subgoal):
 1. \<langle>vcard xs, b\<rangle> = \<langle>vcard xs, x\<rangle>
[PROOF STEP]
using \<open>vcard xs = \<D>\<^sub>\<circ> xs\<close> mem_not_refl
[PROOF STATE]
proof (prove)
using this:
\<langle>vcard xs, b\<rangle> \<in>\<^sub>\<circ> vinsert \<langle>vcard xs, x\<rangle> xs
vcard xs = \<D>\<^sub>\<circ> xs
?i \<notin>\<^sub>\<circ> ?i

goal (1 subgoal):
 1. \<langle>vcard xs, b\<rangle> = \<langle>vcard xs, x\<rangle>
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<langle>a, b\<rangle> = \<langle>vcard xs, x\<rangle>

goal (1 subgoal):
 1. a = vcard xs \<Longrightarrow> b = c
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<langle>a, b\<rangle> = \<langle>vcard xs, x\<rangle>

goal (1 subgoal):
 1. a = vcard xs \<Longrightarrow> b = c
[PROOF STEP]
from ac
[PROOF STATE]
proof (chain)
picking this:
\<langle>a, c\<rangle> \<in>\<^sub>\<circ> xs #\<^sub>\<circ> x
[PROOF STEP]
have "\<langle>a, c\<rangle> = \<langle>vcard xs, x\<rangle>"
[PROOF STATE]
proof (prove)
using this:
\<langle>a, c\<rangle> \<in>\<^sub>\<circ> xs #\<^sub>\<circ> x

goal (1 subgoal):
 1. \<langle>a, c\<rangle> = \<langle>vcard xs, x\<rangle>
[PROOF STEP]
unfolding ndom vcons_def
[PROOF STATE]
proof (prove)
using this:
\<langle>vcard xs, c\<rangle> \<in>\<^sub>\<circ> vinsert \<langle>vcard xs, x\<rangle> xs

goal (1 subgoal):
 1. \<langle>vcard xs, c\<rangle> = \<langle>vcard xs, x\<rangle>
[PROOF STEP]
using \<open>vcard xs = \<D>\<^sub>\<circ> xs\<close> mem_not_refl
[PROOF STATE]
proof (prove)
using this:
\<langle>vcard xs, c\<rangle> \<in>\<^sub>\<circ> vinsert \<langle>vcard xs, x\<rangle> xs
vcard xs = \<D>\<^sub>\<circ> xs
?i \<notin>\<^sub>\<circ> ?i

goal (1 subgoal):
 1. \<langle>vcard xs, c\<rangle> = \<langle>vcard xs, x\<rangle>
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<langle>a, c\<rangle> = \<langle>vcard xs, x\<rangle>

goal (1 subgoal):
 1. a = vcard xs \<Longrightarrow> b = c
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<langle>a, b\<rangle> = \<langle>vcard xs, x\<rangle>
\<langle>a, c\<rangle> = \<langle>vcard xs, x\<rangle>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<langle>a, b\<rangle> = \<langle>vcard xs, x\<rangle>
\<langle>a, c\<rangle> = \<langle>vcard xs, x\<rangle>

goal (1 subgoal):
 1. b = c
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
b = c

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
b = c

goal (1 subgoal):
 1. vbrelation (xs #\<^sub>\<circ> x)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. vbrelation (xs #\<^sub>\<circ> x)
[PROOF STEP]
show "vbrelation (xs #\<^sub>\<circ> x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vbrelation (xs #\<^sub>\<circ> x)
[PROOF STEP]
unfolding vcons_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vbrelation (vinsert \<langle>vcard xs, x\<rangle> xs)
[PROOF STEP]
using vbrelation_vinsertI
[PROOF STATE]
proof (prove)
using this:
vbrelation (vinsert \<langle>?a, ?b\<rangle> xs)

goal (1 subgoal):
 1. vbrelation (vinsert \<langle>vcard xs, x\<rangle> xs)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
vbrelation (xs #\<^sub>\<circ> x)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
vsv (xs #\<^sub>\<circ> x)

goal (1 subgoal):
 1. \<D>\<^sub>\<circ> (xs #\<^sub>\<circ> x) \<in>\<^sub>\<circ> \<omega>
[PROOF STEP]
show "\<D>\<^sub>\<circ> (xs #\<^sub>\<circ> x) \<in>\<^sub>\<circ> \<omega>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<D>\<^sub>\<circ> (xs #\<^sub>\<circ> x) \<in>\<^sub>\<circ> \<omega>
[PROOF STEP]
unfolding vcons_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<D>\<^sub>\<circ> (vinsert \<langle>vcard xs, x\<rangle> xs) \<in>\<^sub>\<circ> \<omega>
[PROOF STEP]
using succ_in_omega
[PROOF STATE]
proof (prove)
using this:
?n \<in>\<^sub>\<circ> \<omega> \<Longrightarrow> ZFC_in_HOL.succ ?n \<in>\<^sub>\<circ> \<omega>

goal (1 subgoal):
 1. \<D>\<^sub>\<circ> (vinsert \<langle>vcard xs, x\<rangle> xs) \<in>\<^sub>\<circ> \<omega>
[PROOF STEP]
by (auto simp: vfsequence_vdomain_in_omega succ_def \<open>vcard xs = \<D>\<^sub>\<circ> xs\<close>)
[PROOF STATE]
proof (state)
this:
\<D>\<^sub>\<circ> (xs #\<^sub>\<circ> x) \<in>\<^sub>\<circ> \<omega>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in vfsequence) vfsequence_vcons_vdomain[simp]:
  "\<D>\<^sub>\<circ> (xs #\<^sub>\<circ> x) = succ (vcard xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<D>\<^sub>\<circ> (xs #\<^sub>\<circ> x) = ZFC_in_HOL.succ (vcard xs)
[PROOF STEP]
by (simp add: succ_def vcons_def vfsequence_vdomain)


[STATEMENT]
lemma (in vfsequence) vfsequence_vcons_vrange[simp]:
  "\<R>\<^sub>\<circ> (xs #\<^sub>\<circ> x) = vinsert x (\<R>\<^sub>\<circ> xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<R>\<^sub>\<circ> (xs #\<^sub>\<circ> x) = vinsert x (\<R>\<^sub>\<circ> xs)
[PROOF STEP]
by (simp add: vcons_def)


[STATEMENT]
lemma (in vfsequence) vfsequence_vrange_vconsI:
  assumes "\<R>\<^sub>\<circ> xs \<subseteq>\<^sub>\<circ> X" and "x \<in>\<^sub>\<circ> X"
  shows "\<R>\<^sub>\<circ> (xs #\<^sub>\<circ> x) \<subseteq>\<^sub>\<circ> X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<R>\<^sub>\<circ> (xs #\<^sub>\<circ> x) \<subseteq>\<^sub>\<circ> X
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<R>\<^sub>\<circ> xs \<subseteq>\<^sub>\<circ> X
x \<in>\<^sub>\<circ> X

goal (1 subgoal):
 1. \<R>\<^sub>\<circ> (xs #\<^sub>\<circ> x) \<subseteq>\<^sub>\<circ> X
[PROOF STEP]
unfolding vcons_def
[PROOF STATE]
proof (prove)
using this:
\<R>\<^sub>\<circ> xs \<subseteq>\<^sub>\<circ> X
x \<in>\<^sub>\<circ> X

goal (1 subgoal):
 1. \<R>\<^sub>\<circ> (vinsert \<langle>vcard xs, x\<rangle> xs) \<subseteq>\<^sub>\<circ> X
[PROOF STEP]
by auto


[STATEMENT]
lemma vcons_vrange_mono:
  assumes "xs \<subseteq>\<^sub>\<circ> ys"
  shows "\<R>\<^sub>\<circ> (xs #\<^sub>\<circ> x) \<subseteq>\<^sub>\<circ> \<R>\<^sub>\<circ> (ys #\<^sub>\<circ> x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<R>\<^sub>\<circ> (xs #\<^sub>\<circ> x) \<subseteq>\<^sub>\<circ> \<R>\<^sub>\<circ> (ys #\<^sub>\<circ> x)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
xs \<subseteq>\<^sub>\<circ> ys

goal (1 subgoal):
 1. \<R>\<^sub>\<circ> (xs #\<^sub>\<circ> x) \<subseteq>\<^sub>\<circ> \<R>\<^sub>\<circ> (ys #\<^sub>\<circ> x)
[PROOF STEP]
unfolding vcons_def
[PROOF STATE]
proof (prove)
using this:
xs \<subseteq>\<^sub>\<circ> ys

goal (1 subgoal):
 1. \<R>\<^sub>\<circ> (vinsert \<langle>vcard xs, x\<rangle> xs) \<subseteq>\<^sub>\<circ> \<R>\<^sub>\<circ> (vinsert \<langle>vcard ys, x\<rangle> ys)
[PROOF STEP]
by (simp add: vrange_mono vsubset_vinsert_leftI vsubset_vinsert_rightI)


[STATEMENT]
lemma (in vfsequence) vfsequence_vlrestriction_succ:
  assumes [simp]: "k \<in>\<^sub>\<circ> vcard xs"
  shows "xs \<restriction>\<^sup>l\<^sub>\<circ> succ k = xs \<restriction>\<^sup>l\<^sub>\<circ> k #\<^sub>\<circ> (xs\<lparr>k\<rparr>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. xs \<restriction>\<^sup>l\<^sub>\<circ> ZFC_in_HOL.succ k = xs \<restriction>\<^sup>l\<^sub>\<circ> k #\<^sub>\<circ> xs\<lparr>k\<rparr>
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. xs \<restriction>\<^sup>l\<^sub>\<circ> ZFC_in_HOL.succ k = xs \<restriction>\<^sup>l\<^sub>\<circ> k #\<^sub>\<circ> xs\<lparr>k\<rparr>
[PROOF STEP]
interpret vlr: vfsequence \<open>xs \<restriction>\<^sup>l\<^sub>\<circ> k\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vfsequence (xs \<restriction>\<^sup>l\<^sub>\<circ> k)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
k \<in>\<^sub>\<circ> vcard xs

goal (1 subgoal):
 1. vfsequence (xs \<restriction>\<^sup>l\<^sub>\<circ> k)
[PROOF STEP]
by (blast intro: vfsequence_vcard_in_omega Ord_trans)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. xs \<restriction>\<^sup>l\<^sub>\<circ> ZFC_in_HOL.succ k = xs \<restriction>\<^sup>l\<^sub>\<circ> k #\<^sub>\<circ> xs\<lparr>k\<rparr>
[PROOF STEP]
from vlr.vfsequence_vdomain[symmetric, simplified]
[PROOF STATE]
proof (chain)
picking this:
vcard (xs \<restriction>\<^sup>l\<^sub>\<circ> k) = k
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
vcard (xs \<restriction>\<^sup>l\<^sub>\<circ> k) = k

goal (1 subgoal):
 1. xs \<restriction>\<^sup>l\<^sub>\<circ> ZFC_in_HOL.succ k = xs \<restriction>\<^sup>l\<^sub>\<circ> k #\<^sub>\<circ> xs\<lparr>k\<rparr>
[PROOF STEP]
by
      (
        simp add:
          vcons_def succ_def vfsequence_vdomain vsv_vlrestriction_vinsert
      )
[PROOF STATE]
proof (state)
this:
xs \<restriction>\<^sup>l\<^sub>\<circ> ZFC_in_HOL.succ k = xs \<restriction>\<^sup>l\<^sub>\<circ> k #\<^sub>\<circ> xs\<lparr>k\<rparr>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in vfsequence) vfsequence_vremove_vcons_vfsequence:
  assumes "xs = xs' #\<^sub>\<circ> x"
  shows "vfsequence xs'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vfsequence xs'
[PROOF STEP]
proof(cases\<open>\<langle>vcard xs', x\<rangle> \<in>\<^sub>\<circ> xs'\<close>)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<langle>vcard xs', x\<rangle> \<in>\<^sub>\<circ> xs' \<Longrightarrow> vfsequence xs'
 2. \<langle>vcard xs', x\<rangle> \<notin>\<^sub>\<circ> xs' \<Longrightarrow> vfsequence xs'
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
\<langle>vcard xs', x\<rangle> \<in>\<^sub>\<circ> xs'

goal (2 subgoals):
 1. \<langle>vcard xs', x\<rangle> \<in>\<^sub>\<circ> xs' \<Longrightarrow> vfsequence xs'
 2. \<langle>vcard xs', x\<rangle> \<notin>\<^sub>\<circ> xs' \<Longrightarrow> vfsequence xs'
[PROOF STEP]
with assms[unfolded vcons_def]
[PROOF STATE]
proof (chain)
picking this:
xs = vinsert \<langle>vcard xs', x\<rangle> xs'
\<langle>vcard xs', x\<rangle> \<in>\<^sub>\<circ> xs'
[PROOF STEP]
have "xs = xs'"
[PROOF STATE]
proof (prove)
using this:
xs = vinsert \<langle>vcard xs', x\<rangle> xs'
\<langle>vcard xs', x\<rangle> \<in>\<^sub>\<circ> xs'

goal (1 subgoal):
 1. xs = xs'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
xs = xs'

goal (2 subgoals):
 1. \<langle>vcard xs', x\<rangle> \<in>\<^sub>\<circ> xs' \<Longrightarrow> vfsequence xs'
 2. \<langle>vcard xs', x\<rangle> \<notin>\<^sub>\<circ> xs' \<Longrightarrow> vfsequence xs'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
xs = xs'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
xs = xs'

goal (1 subgoal):
 1. vfsequence xs'
[PROOF STEP]
using vfsequence_axioms
[PROOF STATE]
proof (prove)
using this:
xs = xs'
vfsequence xs

goal (1 subgoal):
 1. vfsequence xs'
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
vfsequence xs'

goal (1 subgoal):
 1. \<langle>vcard xs', x\<rangle> \<notin>\<^sub>\<circ> xs' \<Longrightarrow> vfsequence xs'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<langle>vcard xs', x\<rangle> \<notin>\<^sub>\<circ> xs' \<Longrightarrow> vfsequence xs'
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<langle>vcard xs', x\<rangle> \<notin>\<^sub>\<circ> xs'

goal (1 subgoal):
 1. \<langle>vcard xs', x\<rangle> \<notin>\<^sub>\<circ> xs' \<Longrightarrow> vfsequence xs'
[PROOF STEP]
note x_def[simp] = assms[unfolded vcons_def]
[PROOF STATE]
proof (state)
this:
xs = vinsert \<langle>vcard xs', x\<rangle> xs'

goal (1 subgoal):
 1. \<langle>vcard xs', x\<rangle> \<notin>\<^sub>\<circ> xs' \<Longrightarrow> vfsequence xs'
[PROOF STEP]
interpret xs': vsv xs'
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vsv xs'
[PROOF STEP]
using vsv_axioms
[PROOF STATE]
proof (prove)
using this:
vsv xs

goal (1 subgoal):
 1. vsv xs'
[PROOF STEP]
by (auto intro: vsv_vinsertD)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<langle>vcard xs', x\<rangle> \<notin>\<^sub>\<circ> xs' \<Longrightarrow> vfsequence xs'
[PROOF STEP]
have fin: "vfinite xs'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vfinite xs'
[PROOF STEP]
using vfsequence_vfinite
[PROOF STATE]
proof (prove)
using this:
vfinite xs

goal (1 subgoal):
 1. vfinite xs'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
vfinite xs'

goal (1 subgoal):
 1. \<langle>vcard xs', x\<rangle> \<notin>\<^sub>\<circ> xs' \<Longrightarrow> vfsequence xs'
[PROOF STEP]
have vcard_xs: "vcard xs = succ (vcard xs')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vcard xs = ZFC_in_HOL.succ (vcard xs')
[PROOF STEP]
by (simp add: fin False)
[PROOF STATE]
proof (state)
this:
vcard xs = ZFC_in_HOL.succ (vcard xs')

goal (1 subgoal):
 1. \<langle>vcard xs', x\<rangle> \<notin>\<^sub>\<circ> xs' \<Longrightarrow> vfsequence xs'
[PROOF STEP]
have [simp]: "vcard xs' \<notin>\<^sub>\<circ> \<D>\<^sub>\<circ> xs'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vcard xs' \<notin>\<^sub>\<circ> \<D>\<^sub>\<circ> xs'
[PROOF STEP]
using False vsv_axioms
[PROOF STATE]
proof (prove)
using this:
\<langle>vcard xs', x\<rangle> \<notin>\<^sub>\<circ> xs'
vsv xs

goal (1 subgoal):
 1. vcard xs' \<notin>\<^sub>\<circ> \<D>\<^sub>\<circ> xs'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
vcard xs' \<notin>\<^sub>\<circ> \<D>\<^sub>\<circ> xs'

goal (1 subgoal):
 1. \<langle>vcard xs', x\<rangle> \<notin>\<^sub>\<circ> xs' \<Longrightarrow> vfsequence xs'
[PROOF STEP]
have "vcard xs' \<in>\<^sub>\<circ> \<omega>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vcard xs' \<in>\<^sub>\<circ> \<omega>
[PROOF STEP]
using fin vfinite_vcard_omega
[PROOF STATE]
proof (prove)
using this:
vfinite xs'
vfinite ?A \<Longrightarrow> vcard ?A \<in>\<^sub>\<circ> \<omega>

goal (1 subgoal):
 1. vcard xs' \<in>\<^sub>\<circ> \<omega>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
vcard xs' \<in>\<^sub>\<circ> \<omega>

goal (1 subgoal):
 1. \<langle>vcard xs', x\<rangle> \<notin>\<^sub>\<circ> xs' \<Longrightarrow> vfsequence xs'
[PROOF STEP]
have xs'_def: "xs' = xs \<restriction>\<^sup>l\<^sub>\<circ> (vcard xs')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. xs' = xs \<restriction>\<^sup>l\<^sub>\<circ> vcard xs'
[PROOF STEP]
using vcard_xs fin vfsequence_vdomain
[PROOF STATE]
proof (prove)
using this:
vcard xs = ZFC_in_HOL.succ (vcard xs')
vfinite xs'
\<D>\<^sub>\<circ> xs = vcard xs

goal (1 subgoal):
 1. xs' = xs \<restriction>\<^sup>l\<^sub>\<circ> vcard xs'
[PROOF STEP]
by (auto simp: vinsert_ident succ_def)
[PROOF STATE]
proof (state)
this:
xs' = xs \<restriction>\<^sup>l\<^sub>\<circ> vcard xs'

goal (1 subgoal):
 1. \<langle>vcard xs', x\<rangle> \<notin>\<^sub>\<circ> xs' \<Longrightarrow> vfsequence xs'
[PROOF STEP]
from vfsequence_vlrestriction[OF \<open>vcard xs' \<in>\<^sub>\<circ> \<omega>\<close>]
[PROOF STATE]
proof (chain)
picking this:
vfsequence (xs \<restriction>\<^sup>l\<^sub>\<circ> vcard xs')
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
vfsequence (xs \<restriction>\<^sup>l\<^sub>\<circ> vcard xs')

goal (1 subgoal):
 1. vfsequence xs'
[PROOF STEP]
unfolding xs'_def[symmetric]
[PROOF STATE]
proof (prove)
using this:
vfsequence xs'

goal (1 subgoal):
 1. vfsequence xs'
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
vfsequence xs'

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in vfsequence) vfsequence_vcons_ex:
  assumes "xs \<noteq> []\<^sub>\<circ>"
  obtains xs' x where "xs = xs' #\<^sub>\<circ> x" and "vfsequence xs'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>xs' x. \<lbrakk>xs = xs' #\<^sub>\<circ> x; vfsequence xs'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>xs' x. \<lbrakk>xs = xs' #\<^sub>\<circ> x; vfsequence xs'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from vcard_vempty
[PROOF STATE]
proof (chain)
picking this:
(vcard ?A = []\<^sub>\<circ>) = (?A = []\<^sub>\<circ>)
[PROOF STEP]
have "0 \<in>\<^sub>\<circ> vcard xs"
[PROOF STATE]
proof (prove)
using this:
(vcard ?A = []\<^sub>\<circ>) = (?A = []\<^sub>\<circ>)

goal (1 subgoal):
 1. []\<^sub>\<circ> \<in>\<^sub>\<circ> vcard xs
[PROOF STEP]
by (simp add: assms mem_0_Ord)
[PROOF STATE]
proof (state)
this:
[]\<^sub>\<circ> \<in>\<^sub>\<circ> vcard xs

goal (1 subgoal):
 1. (\<And>xs' x. \<lbrakk>xs = xs' #\<^sub>\<circ> x; vfsequence xs'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[]\<^sub>\<circ> \<in>\<^sub>\<circ> vcard xs
[PROOF STEP]
obtain k where succk: "succ k = vcard xs"
[PROOF STATE]
proof (prove)
using this:
[]\<^sub>\<circ> \<in>\<^sub>\<circ> vcard xs

goal (1 subgoal):
 1. (\<And>k. ZFC_in_HOL.succ k = vcard xs \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis omega_prev vfsequence_vcard_in_omega)
[PROOF STATE]
proof (state)
this:
ZFC_in_HOL.succ k = vcard xs

goal (1 subgoal):
 1. (\<And>xs' x. \<lbrakk>xs = xs' #\<^sub>\<circ> x; vfsequence xs'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ZFC_in_HOL.succ k = vcard xs
[PROOF STEP]
have "k \<in>\<^sub>\<circ> vcard xs"
[PROOF STATE]
proof (prove)
using this:
ZFC_in_HOL.succ k = vcard xs

goal (1 subgoal):
 1. k \<in>\<^sub>\<circ> vcard xs
[PROOF STEP]
using elts_succ
[PROOF STATE]
proof (prove)
using this:
ZFC_in_HOL.succ k = vcard xs
elts (ZFC_in_HOL.succ ?x) = insert ?x (elts ?x)

goal (1 subgoal):
 1. k \<in>\<^sub>\<circ> vcard xs
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
k \<in>\<^sub>\<circ> vcard xs

goal (1 subgoal):
 1. (\<And>xs' x. \<lbrakk>xs = xs' #\<^sub>\<circ> x; vfsequence xs'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from vfsequence_vlrestriction_succ[OF this, unfolded succk]
[PROOF STATE]
proof (chain)
picking this:
xs \<restriction>\<^sup>l\<^sub>\<circ> vcard xs = xs \<restriction>\<^sup>l\<^sub>\<circ> k #\<^sub>\<circ> xs\<lparr>k\<rparr>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
xs \<restriction>\<^sup>l\<^sub>\<circ> vcard xs = xs \<restriction>\<^sup>l\<^sub>\<circ> k #\<^sub>\<circ> xs\<lparr>k\<rparr>

goal (1 subgoal):
 1. thesis
[PROOF STEP]
by (simp add: vfsequence_vremove_vcons_vfsequence that)
[PROOF STATE]
proof (state)
this:
thesis

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma vfsequence_induct[consumes 1, case_names 0 vcons]:
  assumes "vfsequence xs"
    and "P []\<^sub>\<circ>"
    and "\<And>xs x. \<lbrakk>vfsequence xs; P xs\<rbrakk> \<Longrightarrow> P (xs #\<^sub>\<circ> x)"
  shows "P xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P xs
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. P xs
[PROOF STEP]
interpret vfsequence xs
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vfsequence xs
[PROOF STEP]
by (rule assms(1))
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. P xs
[PROOF STEP]
from assms(1)
[PROOF STATE]
proof (chain)
picking this:
vfsequence xs
[PROOF STEP]
obtain n where "n \<in>\<^sub>\<circ> \<omega>" and "\<D>\<^sub>\<circ> xs = n"
[PROOF STATE]
proof (prove)
using this:
vfsequence xs

goal (1 subgoal):
 1. (\<And>n. \<lbrakk>n \<in>\<^sub>\<circ> \<omega>; \<D>\<^sub>\<circ> xs = n\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
n \<in>\<^sub>\<circ> \<omega>
\<D>\<^sub>\<circ> xs = n

goal (1 subgoal):
 1. P xs
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
n \<in>\<^sub>\<circ> \<omega>
\<D>\<^sub>\<circ> xs = n
[PROOF STEP]
have "n \<le> \<D>\<^sub>\<circ> xs"
[PROOF STATE]
proof (prove)
using this:
n \<in>\<^sub>\<circ> \<omega>
\<D>\<^sub>\<circ> xs = n

goal (1 subgoal):
 1. n \<subseteq>\<^sub>\<circ> \<D>\<^sub>\<circ> xs
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
n \<subseteq>\<^sub>\<circ> \<D>\<^sub>\<circ> xs

goal (1 subgoal):
 1. P xs
[PROOF STEP]
define P' where "P' k = P (xs \<restriction>\<^sup>l\<^sub>\<circ> k)" for k
[PROOF STATE]
proof (state)
this:
P' ?k = P (xs \<restriction>\<^sup>l\<^sub>\<circ> ?k)

goal (1 subgoal):
 1. P xs
[PROOF STEP]
from \<open>n \<in>\<^sub>\<circ> \<omega>\<close> and \<open>n \<le> \<D>\<^sub>\<circ> xs\<close>
[PROOF STATE]
proof (chain)
picking this:
n \<in>\<^sub>\<circ> \<omega>
n \<subseteq>\<^sub>\<circ> \<D>\<^sub>\<circ> xs
[PROOF STEP]
have "P' n"
[PROOF STATE]
proof (prove)
using this:
n \<in>\<^sub>\<circ> \<omega>
n \<subseteq>\<^sub>\<circ> \<D>\<^sub>\<circ> xs

goal (1 subgoal):
 1. P' n
[PROOF STEP]
proof(induction rule: omega_induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. []\<^sub>\<circ> \<subseteq>\<^sub>\<circ> \<D>\<^sub>\<circ> xs \<Longrightarrow> P' []\<^sub>\<circ>
 2. \<And>n. \<lbrakk>n \<in>\<^sub>\<circ> \<omega>; n \<subseteq>\<^sub>\<circ> \<D>\<^sub>\<circ> xs \<Longrightarrow> P' n; ZFC_in_HOL.succ n \<subseteq>\<^sub>\<circ> \<D>\<^sub>\<circ> xs\<rbrakk> \<Longrightarrow> P' (ZFC_in_HOL.succ n)
[PROOF STEP]
case (succ n')
[PROOF STATE]
proof (state)
this:
n' \<in>\<^sub>\<circ> \<omega>
n' \<subseteq>\<^sub>\<circ> \<D>\<^sub>\<circ> xs \<Longrightarrow> P' n'
ZFC_in_HOL.succ n' \<subseteq>\<^sub>\<circ> \<D>\<^sub>\<circ> xs

goal (2 subgoals):
 1. []\<^sub>\<circ> \<subseteq>\<^sub>\<circ> \<D>\<^sub>\<circ> xs \<Longrightarrow> P' []\<^sub>\<circ>
 2. \<And>n. \<lbrakk>n \<in>\<^sub>\<circ> \<omega>; n \<subseteq>\<^sub>\<circ> \<D>\<^sub>\<circ> xs \<Longrightarrow> P' n; ZFC_in_HOL.succ n \<subseteq>\<^sub>\<circ> \<D>\<^sub>\<circ> xs\<rbrakk> \<Longrightarrow> P' (ZFC_in_HOL.succ n)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
n' \<in>\<^sub>\<circ> \<omega>
n' \<subseteq>\<^sub>\<circ> \<D>\<^sub>\<circ> xs \<Longrightarrow> P' n'
ZFC_in_HOL.succ n' \<subseteq>\<^sub>\<circ> \<D>\<^sub>\<circ> xs
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
n' \<in>\<^sub>\<circ> \<omega>
n' \<subseteq>\<^sub>\<circ> \<D>\<^sub>\<circ> xs \<Longrightarrow> P' n'
ZFC_in_HOL.succ n' \<subseteq>\<^sub>\<circ> \<D>\<^sub>\<circ> xs

goal (1 subgoal):
 1. P' (ZFC_in_HOL.succ n')
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>n' \<in>\<^sub>\<circ> \<omega>; n' \<subseteq>\<^sub>\<circ> \<D>\<^sub>\<circ> xs \<Longrightarrow> P' n'; ZFC_in_HOL.succ n' \<subseteq>\<^sub>\<circ> \<D>\<^sub>\<circ> xs\<rbrakk> \<Longrightarrow> P' (ZFC_in_HOL.succ n')
[PROOF STEP]
interpret vlr: vfsequence \<open>xs \<restriction>\<^sup>l\<^sub>\<circ> n'\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vfsequence (xs \<restriction>\<^sup>l\<^sub>\<circ> n')
[PROOF STEP]
by (simp add: succ.hyps)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>n' \<in>\<^sub>\<circ> \<omega>; n' \<subseteq>\<^sub>\<circ> \<D>\<^sub>\<circ> xs \<Longrightarrow> P' n'; ZFC_in_HOL.succ n' \<subseteq>\<^sub>\<circ> \<D>\<^sub>\<circ> xs\<rbrakk> \<Longrightarrow> P' (ZFC_in_HOL.succ n')
[PROOF STEP]
have "P' n'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P' n'
[PROOF STEP]
using succ.prems
[PROOF STATE]
proof (prove)
using this:
ZFC_in_HOL.succ n' \<subseteq>\<^sub>\<circ> \<D>\<^sub>\<circ> xs

goal (1 subgoal):
 1. P' n'
[PROOF STEP]
by (force intro: succ.IH)
[PROOF STATE]
proof (state)
this:
P' n'

goal (1 subgoal):
 1. \<lbrakk>n' \<in>\<^sub>\<circ> \<omega>; n' \<subseteq>\<^sub>\<circ> \<D>\<^sub>\<circ> xs \<Longrightarrow> P' n'; ZFC_in_HOL.succ n' \<subseteq>\<^sub>\<circ> \<D>\<^sub>\<circ> xs\<rbrakk> \<Longrightarrow> P' (ZFC_in_HOL.succ n')
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
P' n'
[PROOF STEP]
have "P (xs \<restriction>\<^sup>l\<^sub>\<circ> n')"
[PROOF STATE]
proof (prove)
using this:
P' n'

goal (1 subgoal):
 1. P (xs \<restriction>\<^sup>l\<^sub>\<circ> n')
[PROOF STEP]
unfolding P'_def
[PROOF STATE]
proof (prove)
using this:
P (xs \<restriction>\<^sup>l\<^sub>\<circ> n')

goal (1 subgoal):
 1. P (xs \<restriction>\<^sup>l\<^sub>\<circ> n')
[PROOF STEP]
by assumption
[PROOF STATE]
proof (state)
this:
P (xs \<restriction>\<^sup>l\<^sub>\<circ> n')

goal (1 subgoal):
 1. \<lbrakk>n' \<in>\<^sub>\<circ> \<omega>; n' \<subseteq>\<^sub>\<circ> \<D>\<^sub>\<circ> xs \<Longrightarrow> P' n'; ZFC_in_HOL.succ n' \<subseteq>\<^sub>\<circ> \<D>\<^sub>\<circ> xs\<rbrakk> \<Longrightarrow> P' (ZFC_in_HOL.succ n')
[PROOF STEP]
have "n' \<in>\<^sub>\<circ> vcard xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n' \<in>\<^sub>\<circ> vcard xs
[PROOF STEP]
using succ.prems
[PROOF STATE]
proof (prove)
using this:
ZFC_in_HOL.succ n' \<subseteq>\<^sub>\<circ> \<D>\<^sub>\<circ> xs

goal (1 subgoal):
 1. n' \<in>\<^sub>\<circ> vcard xs
[PROOF STEP]
by (auto simp: vsubset_iff vfsequence_vdomain)
[PROOF STATE]
proof (state)
this:
n' \<in>\<^sub>\<circ> vcard xs

goal (1 subgoal):
 1. \<lbrakk>n' \<in>\<^sub>\<circ> \<omega>; n' \<subseteq>\<^sub>\<circ> \<D>\<^sub>\<circ> xs \<Longrightarrow> P' n'; ZFC_in_HOL.succ n' \<subseteq>\<^sub>\<circ> \<D>\<^sub>\<circ> xs\<rbrakk> \<Longrightarrow> P' (ZFC_in_HOL.succ n')
[PROOF STEP]
from vfsequence_vlrestriction_succ[OF \<open>n' \<in>\<^sub>\<circ> vcard xs\<close>]
[PROOF STATE]
proof (chain)
picking this:
xs \<restriction>\<^sup>l\<^sub>\<circ> ZFC_in_HOL.succ n' = xs \<restriction>\<^sup>l\<^sub>\<circ> n' #\<^sub>\<circ> xs\<lparr>n'\<rparr>
[PROOF STEP]
show "P' (succ n')"
[PROOF STATE]
proof (prove)
using this:
xs \<restriction>\<^sup>l\<^sub>\<circ> ZFC_in_HOL.succ n' = xs \<restriction>\<^sup>l\<^sub>\<circ> n' #\<^sub>\<circ> xs\<lparr>n'\<rparr>

goal (1 subgoal):
 1. P' (ZFC_in_HOL.succ n')
[PROOF STEP]
by (simp add: P'_def \<open>P (xs \<restriction>\<^sup>l\<^sub>\<circ> n')\<close> assms(3) vlr.vfsequence_axioms)
[PROOF STATE]
proof (state)
this:
P' (ZFC_in_HOL.succ n')

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
P' (ZFC_in_HOL.succ n')

goal (1 subgoal):
 1. []\<^sub>\<circ> \<subseteq>\<^sub>\<circ> \<D>\<^sub>\<circ> xs \<Longrightarrow> P' []\<^sub>\<circ>
[PROOF STEP]
qed (simp add: P'_def assms(2))
[PROOF STATE]
proof (state)
this:
P' n

goal (1 subgoal):
 1. P xs
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
P' n
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
P' n

goal (1 subgoal):
 1. P xs
[PROOF STEP]
unfolding P'_def \<open>\<D>\<^sub>\<circ> xs = n\<close>[symmetric]
[PROOF STATE]
proof (prove)
using this:
P (xs \<restriction>\<^sup>l\<^sub>\<circ> \<D>\<^sub>\<circ> xs)

goal (1 subgoal):
 1. P xs
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
P xs

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma vfsequence_cases[consumes 1, case_names 0 vcons]:
  assumes "vfsequence xs"
    and "xs = []\<^sub>\<circ> \<Longrightarrow> P"
    and "\<And>xs' x. \<lbrakk>xs = xs' #\<^sub>\<circ> x; vfsequence xs'\<rbrakk> \<Longrightarrow> P"
  shows P
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. P
[PROOF STEP]
interpret vfsequence xs
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vfsequence xs
[PROOF STEP]
by (rule assms(1))
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. P
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P
[PROOF STEP]
proof(cases \<open>xs = 0\<close>)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. xs = []\<^sub>\<circ> \<Longrightarrow> P
 2. xs \<noteq> []\<^sub>\<circ> \<Longrightarrow> P
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
xs \<noteq> []\<^sub>\<circ>

goal (2 subgoals):
 1. xs = []\<^sub>\<circ> \<Longrightarrow> P
 2. xs \<noteq> []\<^sub>\<circ> \<Longrightarrow> P
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
xs \<noteq> []\<^sub>\<circ>
[PROOF STEP]
obtain xs' x where "xs = xs' #\<^sub>\<circ> x"
[PROOF STATE]
proof (prove)
using this:
xs \<noteq> []\<^sub>\<circ>

goal (1 subgoal):
 1. (\<And>xs' x. xs = xs' #\<^sub>\<circ> x \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (blast intro: vfsequence_vcons_ex)
[PROOF STATE]
proof (state)
this:
xs = xs' #\<^sub>\<circ> x

goal (2 subgoals):
 1. xs = []\<^sub>\<circ> \<Longrightarrow> P
 2. xs \<noteq> []\<^sub>\<circ> \<Longrightarrow> P
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
xs = xs' #\<^sub>\<circ> x
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
xs = xs' #\<^sub>\<circ> x

goal (1 subgoal):
 1. P
[PROOF STEP]
by (auto simp: assms(3) intro: vfsequence_vcons_ex)
[PROOF STATE]
proof (state)
this:
P

goal (1 subgoal):
 1. xs = []\<^sub>\<circ> \<Longrightarrow> P
[PROOF STEP]
qed (use assms(2) in auto)
[PROOF STATE]
proof (state)
this:
P

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in vfsequence) vfsequence_vcard_vcons[simp]:
  "vcard (xs #\<^sub>\<circ> x) = succ (vcard xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vcard (xs #\<^sub>\<circ> x) = ZFC_in_HOL.succ (vcard xs)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. vcard (xs #\<^sub>\<circ> x) = ZFC_in_HOL.succ (vcard xs)
[PROOF STEP]
interpret xsx: vfsequence \<open>xs #\<^sub>\<circ> x\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vfsequence (xs #\<^sub>\<circ> x)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. vcard (xs #\<^sub>\<circ> x) = ZFC_in_HOL.succ (vcard xs)
[PROOF STEP]
have "vcard (xs #\<^sub>\<circ> x) = \<D>\<^sub>\<circ> (xs #\<^sub>\<circ> x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vcard (xs #\<^sub>\<circ> x) = \<D>\<^sub>\<circ> (xs #\<^sub>\<circ> x)
[PROOF STEP]
by (rule xsx.vfsequence_vdomain[symmetric])
[PROOF STATE]
proof (state)
this:
vcard (xs #\<^sub>\<circ> x) = \<D>\<^sub>\<circ> (xs #\<^sub>\<circ> x)

goal (1 subgoal):
 1. vcard (xs #\<^sub>\<circ> x) = ZFC_in_HOL.succ (vcard xs)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
vcard (xs #\<^sub>\<circ> x) = \<D>\<^sub>\<circ> (xs #\<^sub>\<circ> x)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
vcard (xs #\<^sub>\<circ> x) = \<D>\<^sub>\<circ> (xs #\<^sub>\<circ> x)

goal (1 subgoal):
 1. vcard (xs #\<^sub>\<circ> x) = ZFC_in_HOL.succ (vcard xs)
[PROOF STEP]
by (subst vcons_def) (simp add: succ_def vcons_def vfsequence_vdomain)
[PROOF STATE]
proof (state)
this:
vcard (xs #\<^sub>\<circ> x) = ZFC_in_HOL.succ (vcard xs)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in vfsequence) vfsequence_at_last[intro, simp]:
  assumes "i = vcard xs"
  shows "(xs #\<^sub>\<circ> x)\<lparr>i\<rparr> = x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (xs #\<^sub>\<circ> x)\<lparr>i\<rparr> = x
[PROOF STEP]
by (simp add: vfsequence_vdomain vcons_def assms)


[STATEMENT]
lemma (in vfsequence) vfsequence_at_not_last[intro, simp]:
  assumes "i \<in>\<^sub>\<circ> vcard xs"
  shows "(xs #\<^sub>\<circ> x)\<lparr>i\<rparr> = xs\<lparr>i\<rparr>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (xs #\<^sub>\<circ> x)\<lparr>i\<rparr> = xs\<lparr>i\<rparr>
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (xs #\<^sub>\<circ> x)\<lparr>i\<rparr> = xs\<lparr>i\<rparr>
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
i \<in>\<^sub>\<circ> vcard xs
[PROOF STEP]
have [simp]: "\<D>\<^sub>\<circ> xs = vcard xs"
[PROOF STATE]
proof (prove)
using this:
i \<in>\<^sub>\<circ> vcard xs

goal (1 subgoal):
 1. \<D>\<^sub>\<circ> xs = vcard xs
[PROOF STEP]
by (auto simp: vfsequence_vdomain)
[PROOF STATE]
proof (state)
this:
\<D>\<^sub>\<circ> xs = vcard xs

goal (1 subgoal):
 1. (xs #\<^sub>\<circ> x)\<lparr>i\<rparr> = xs\<lparr>i\<rparr>
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
i \<in>\<^sub>\<circ> vcard xs
[PROOF STEP]
have "i \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> xs"
[PROOF STATE]
proof (prove)
using this:
i \<in>\<^sub>\<circ> vcard xs

goal (1 subgoal):
 1. i \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> xs
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
i \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> xs

goal (1 subgoal):
 1. (xs #\<^sub>\<circ> x)\<lparr>i\<rparr> = xs\<lparr>i\<rparr>
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
i \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> xs

goal (1 subgoal):
 1. (xs #\<^sub>\<circ> x)\<lparr>i\<rparr> = xs\<lparr>i\<rparr>
[PROOF STEP]
have "i \<noteq> vcard xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i \<noteq> vcard xs
[PROOF STEP]
using assms mem_not_refl
[PROOF STATE]
proof (prove)
using this:
i \<in>\<^sub>\<circ> vcard xs
?i \<notin>\<^sub>\<circ> ?i

goal (1 subgoal):
 1. i \<noteq> vcard xs
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
i \<noteq> vcard xs

goal (1 subgoal):
 1. (xs #\<^sub>\<circ> x)\<lparr>i\<rparr> = xs\<lparr>i\<rparr>
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
i \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> xs
i \<noteq> vcard xs
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
i \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> xs
i \<noteq> vcard xs

goal (1 subgoal):
 1. (xs #\<^sub>\<circ> x)\<lparr>i\<rparr> = xs\<lparr>i\<rparr>
[PROOF STEP]
unfolding vcons_def
[PROOF STATE]
proof (prove)
using this:
i \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> xs
i \<noteq> vcard xs

goal (1 subgoal):
 1. vinsert \<langle>vcard xs, x\<rangle> xs\<lparr>i\<rparr> = xs\<lparr>i\<rparr>
[PROOF STEP]
using vsv.vsv_vinsert vsvE vsv_axioms
[PROOF STATE]
proof (prove)
using this:
i \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> xs
i \<noteq> vcard xs
\<lbrakk>vsv ?r; ?a \<notin>\<^sub>\<circ> \<D>\<^sub>\<circ> ?r\<rbrakk> \<Longrightarrow> vsv (vinsert \<langle>?a, ?b\<rangle> ?r)
\<lbrakk>vsv ?r; \<lbrakk>vbrelation ?r; \<And>a b c. \<lbrakk>\<langle>a, b\<rangle> \<in>\<^sub>\<circ> ?r; \<langle>a, c\<rangle> \<in>\<^sub>\<circ> ?r\<rbrakk> \<Longrightarrow> b = c\<rbrakk> \<Longrightarrow> ?W\<rbrakk> \<Longrightarrow> ?W
vsv xs

goal (1 subgoal):
 1. vinsert \<langle>vcard xs, x\<rangle> xs\<lparr>i\<rparr> = xs\<lparr>i\<rparr>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(xs #\<^sub>\<circ> x)\<lparr>i\<rparr> = xs\<lparr>i\<rparr>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma vcons_eq_vcard_eq:
  assumes "xs\<^sub>1 #\<^sub>\<circ> x\<^sub>1 = xs\<^sub>2 #\<^sub>\<circ> x\<^sub>2"
  shows "vcard xs\<^sub>1 = vcard xs\<^sub>2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vcard xs\<^sub>1 = vcard xs\<^sub>2
[PROOF STEP]
by
    (
      metis
        assms
        succ_inject_iff
        vfsequence.vfsequence_vcons_vdomain
        r\<^sub>1.vfsequence_axioms
        r\<^sub>2.vfsequence_axioms
    )


[STATEMENT]
lemma vcons_eqD[dest]:
  assumes "xs\<^sub>1 #\<^sub>\<circ> x\<^sub>1 = xs\<^sub>2 #\<^sub>\<circ> x\<^sub>2"
  shows "xs\<^sub>1 = xs\<^sub>2" and "x\<^sub>1 = x\<^sub>2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. xs\<^sub>1 = xs\<^sub>2 &&& x\<^sub>1 = x\<^sub>2
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. xs\<^sub>1 = xs\<^sub>2
 2. x\<^sub>1 = x\<^sub>2
[PROOF STEP]
have xsx1_last: "(xs\<^sub>1 #\<^sub>\<circ> x\<^sub>1)\<lparr>vcard xs\<^sub>1\<rparr> = x\<^sub>1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (xs\<^sub>1 #\<^sub>\<circ> x\<^sub>1)\<lparr>vcard xs\<^sub>1\<rparr> = x\<^sub>1
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(xs\<^sub>1 #\<^sub>\<circ> x\<^sub>1)\<lparr>vcard xs\<^sub>1\<rparr> = x\<^sub>1

goal (2 subgoals):
 1. xs\<^sub>1 = xs\<^sub>2
 2. x\<^sub>1 = x\<^sub>2
[PROOF STEP]
have xsx2_last: "(xs\<^sub>2 #\<^sub>\<circ> x\<^sub>2)\<lparr>vcard xs\<^sub>2\<rparr> = x\<^sub>2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (xs\<^sub>2 #\<^sub>\<circ> x\<^sub>2)\<lparr>vcard xs\<^sub>2\<rparr> = x\<^sub>2
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(xs\<^sub>2 #\<^sub>\<circ> x\<^sub>2)\<lparr>vcard xs\<^sub>2\<rparr> = x\<^sub>2

goal (2 subgoals):
 1. xs\<^sub>1 = xs\<^sub>2
 2. x\<^sub>1 = x\<^sub>2
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
xs\<^sub>1 #\<^sub>\<circ> x\<^sub>1 = xs\<^sub>2 #\<^sub>\<circ> x\<^sub>2
[PROOF STEP]
have vcard: "vcard xs\<^sub>1 = vcard xs\<^sub>2"
[PROOF STATE]
proof (prove)
using this:
xs\<^sub>1 #\<^sub>\<circ> x\<^sub>1 = xs\<^sub>2 #\<^sub>\<circ> x\<^sub>2

goal (1 subgoal):
 1. vcard xs\<^sub>1 = vcard xs\<^sub>2
[PROOF STEP]
by (rule vcons_eq_vcard_eq)
[PROOF STATE]
proof (state)
this:
vcard xs\<^sub>1 = vcard xs\<^sub>2

goal (2 subgoals):
 1. xs\<^sub>1 = xs\<^sub>2
 2. x\<^sub>1 = x\<^sub>2
[PROOF STEP]
from trans[OF xsx1_last xsx1_last[unfolded vcard assms, symmetric]]
[PROOF STATE]
proof (chain)
picking this:
(xs\<^sub>1 #\<^sub>\<circ> x\<^sub>1)\<lparr>vcard xs\<^sub>1\<rparr> = (xs\<^sub>2 #\<^sub>\<circ> x\<^sub>2)\<lparr>vcard xs\<^sub>2\<rparr>
[PROOF STEP]
show "x\<^sub>1 = x\<^sub>2"
[PROOF STATE]
proof (prove)
using this:
(xs\<^sub>1 #\<^sub>\<circ> x\<^sub>1)\<lparr>vcard xs\<^sub>1\<rparr> = (xs\<^sub>2 #\<^sub>\<circ> x\<^sub>2)\<lparr>vcard xs\<^sub>2\<rparr>

goal (1 subgoal):
 1. x\<^sub>1 = x\<^sub>2
[PROOF STEP]
unfolding xsx1_last xsx2_last
[PROOF STATE]
proof (prove)
using this:
x\<^sub>1 = x\<^sub>2

goal (1 subgoal):
 1. x\<^sub>1 = x\<^sub>2
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
x\<^sub>1 = x\<^sub>2

goal (1 subgoal):
 1. xs\<^sub>1 = xs\<^sub>2
[PROOF STEP]
have nxs1: "\<langle>vcard xs\<^sub>1, x\<^sub>1\<rangle> \<notin>\<^sub>\<circ> xs\<^sub>1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<langle>vcard xs\<^sub>1, x\<^sub>1\<rangle> \<notin>\<^sub>\<circ> xs\<^sub>1
[PROOF STEP]
using mem_not_refl r\<^sub>1.vfsequence_vdomain
[PROOF STATE]
proof (prove)
using this:
?i \<notin>\<^sub>\<circ> ?i
\<D>\<^sub>\<circ> xs\<^sub>1 = vcard xs\<^sub>1

goal (1 subgoal):
 1. \<langle>vcard xs\<^sub>1, x\<^sub>1\<rangle> \<notin>\<^sub>\<circ> xs\<^sub>1
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<langle>vcard xs\<^sub>1, x\<^sub>1\<rangle> \<notin>\<^sub>\<circ> xs\<^sub>1

goal (1 subgoal):
 1. xs\<^sub>1 = xs\<^sub>2
[PROOF STEP]
have nxs2: "\<langle>vcard xs\<^sub>2, x\<^sub>2\<rangle> \<notin>\<^sub>\<circ> xs\<^sub>2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<langle>vcard xs\<^sub>2, x\<^sub>2\<rangle> \<notin>\<^sub>\<circ> xs\<^sub>2
[PROOF STEP]
using mem_not_refl r\<^sub>2.vfsequence_vdomain
[PROOF STATE]
proof (prove)
using this:
?i \<notin>\<^sub>\<circ> ?i
\<D>\<^sub>\<circ> xs\<^sub>2 = vcard xs\<^sub>2

goal (1 subgoal):
 1. \<langle>vcard xs\<^sub>2, x\<^sub>2\<rangle> \<notin>\<^sub>\<circ> xs\<^sub>2
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<langle>vcard xs\<^sub>2, x\<^sub>2\<rangle> \<notin>\<^sub>\<circ> xs\<^sub>2

goal (1 subgoal):
 1. xs\<^sub>1 = xs\<^sub>2
[PROOF STEP]
have xsx1_xsx2: "\<langle>vcard xs\<^sub>1, x\<^sub>1\<rangle> = \<langle>vcard xs\<^sub>2, x\<^sub>2\<rangle>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<langle>vcard xs\<^sub>1, x\<^sub>1\<rangle> = \<langle>vcard xs\<^sub>2, x\<^sub>2\<rangle>
[PROOF STEP]
unfolding vcons_eq_vcard_eq[OF assms(1)] \<open>x\<^sub>1 = x\<^sub>2\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<langle>vcard xs\<^sub>2, x\<^sub>2\<rangle> = \<langle>vcard xs\<^sub>2, x\<^sub>2\<rangle>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<langle>vcard xs\<^sub>1, x\<^sub>1\<rangle> = \<langle>vcard xs\<^sub>2, x\<^sub>2\<rangle>

goal (1 subgoal):
 1. xs\<^sub>1 = xs\<^sub>2
[PROOF STEP]
show "xs\<^sub>1 = xs\<^sub>2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. xs\<^sub>1 = xs\<^sub>2
[PROOF STEP]
proof(rule vinsert_identD[OF _ nxs1])
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. vinsert \<langle>vcard xs\<^sub>1, x\<^sub>1\<rangle> xs\<^sub>1 = vinsert \<langle>vcard xs\<^sub>1, x\<^sub>1\<rangle> xs\<^sub>2
 2. \<langle>vcard xs\<^sub>1, x\<^sub>1\<rangle> \<notin>\<^sub>\<circ> xs\<^sub>2
[PROOF STEP]
from assms(1)[unfolded vcons_def]
[PROOF STATE]
proof (chain)
picking this:
vinsert \<langle>vcard xs\<^sub>1, x\<^sub>1\<rangle> xs\<^sub>1 = vinsert \<langle>vcard xs\<^sub>2, x\<^sub>2\<rangle> xs\<^sub>2
[PROOF STEP]
show
      "vinsert \<langle>vcard xs\<^sub>1, x\<^sub>1\<rangle> xs\<^sub>1 = vinsert \<langle>vcard xs\<^sub>1, x\<^sub>1\<rangle> xs\<^sub>2"
[PROOF STATE]
proof (prove)
using this:
vinsert \<langle>vcard xs\<^sub>1, x\<^sub>1\<rangle> xs\<^sub>1 = vinsert \<langle>vcard xs\<^sub>2, x\<^sub>2\<rangle> xs\<^sub>2

goal (1 subgoal):
 1. vinsert \<langle>vcard xs\<^sub>1, x\<^sub>1\<rangle> xs\<^sub>1 = vinsert \<langle>vcard xs\<^sub>1, x\<^sub>1\<rangle> xs\<^sub>2
[PROOF STEP]
by (auto simp: xsx1_xsx2)
[PROOF STATE]
proof (state)
this:
vinsert \<langle>vcard xs\<^sub>1, x\<^sub>1\<rangle> xs\<^sub>1 = vinsert \<langle>vcard xs\<^sub>1, x\<^sub>1\<rangle> xs\<^sub>2

goal (1 subgoal):
 1. \<langle>vcard xs\<^sub>1, x\<^sub>1\<rangle> \<notin>\<^sub>\<circ> xs\<^sub>2
[PROOF STEP]
show "\<langle>vcard xs\<^sub>1, x\<^sub>1\<rangle> \<notin>\<^sub>\<circ> xs\<^sub>2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<langle>vcard xs\<^sub>1, x\<^sub>1\<rangle> \<notin>\<^sub>\<circ> xs\<^sub>2
[PROOF STEP]
by (rule nxs2[folded \<open>x\<^sub>1 = x\<^sub>2\<close> vcons_eq_vcard_eq[OF assms(1)]])
[PROOF STATE]
proof (state)
this:
\<langle>vcard xs\<^sub>1, x\<^sub>1\<rangle> \<notin>\<^sub>\<circ> xs\<^sub>2

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
xs\<^sub>1 = xs\<^sub>2

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma vcons_eqI:
  assumes "xs\<^sub>1 = xs\<^sub>2" and "x\<^sub>1 = x\<^sub>2"
  shows "xs\<^sub>1 #\<^sub>\<circ> x\<^sub>1 = xs\<^sub>2 #\<^sub>\<circ> x\<^sub>2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. xs\<^sub>1 #\<^sub>\<circ> x\<^sub>1 = xs\<^sub>2 #\<^sub>\<circ> x\<^sub>2
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
xs\<^sub>1 = xs\<^sub>2
x\<^sub>1 = x\<^sub>2

goal (1 subgoal):
 1. xs\<^sub>1 #\<^sub>\<circ> x\<^sub>1 = xs\<^sub>2 #\<^sub>\<circ> x\<^sub>2
[PROOF STEP]
by (rule arg_cong2)


[STATEMENT]
lemma vcons_eq_iff[simp]: "(xs\<^sub>1 #\<^sub>\<circ> x\<^sub>1 = xs\<^sub>2 #\<^sub>\<circ> x\<^sub>2) \<longleftrightarrow> (xs\<^sub>1 = xs\<^sub>2 \<and> x\<^sub>1 = x\<^sub>2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (xs\<^sub>1 #\<^sub>\<circ> x\<^sub>1 = xs\<^sub>2 #\<^sub>\<circ> x\<^sub>2) = (xs\<^sub>1 = xs\<^sub>2 \<and> x\<^sub>1 = x\<^sub>2)
[PROOF STEP]
by auto


[STATEMENT]
lemma vfsequence_vfsequence_of_vlist: "vfsequence (vfsequence_of_vlist xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vfsequence (vfsequence_of_vlist xs)
[PROOF STEP]
by (induction xs) auto


[STATEMENT]
lemma inj_vfsequence_of_vlist: "inj vfsequence_of_vlist"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inj vfsequence_of_vlist
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> UNIV; y \<in> UNIV; vfsequence_of_vlist x = vfsequence_of_vlist y\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
show "vfsequence_of_vlist x = vfsequence_of_vlist y \<Longrightarrow> x = y"
    for x y
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vfsequence_of_vlist x = vfsequence_of_vlist y \<Longrightarrow> x = y
[PROOF STEP]
proof(induction y arbitrary: x)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. vfsequence_of_vlist x = vfsequence_of_vlist [] \<Longrightarrow> x = []
 2. \<And>a y x. \<lbrakk>\<And>x. vfsequence_of_vlist x = vfsequence_of_vlist y \<Longrightarrow> x = y; vfsequence_of_vlist x = vfsequence_of_vlist (a # y)\<rbrakk> \<Longrightarrow> x = a # y
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
vfsequence_of_vlist x = vfsequence_of_vlist []

goal (2 subgoals):
 1. \<And>x. vfsequence_of_vlist x = vfsequence_of_vlist [] \<Longrightarrow> x = []
 2. \<And>a y x. \<lbrakk>\<And>x. vfsequence_of_vlist x = vfsequence_of_vlist y \<Longrightarrow> x = y; vfsequence_of_vlist x = vfsequence_of_vlist (a # y)\<rbrakk> \<Longrightarrow> x = a # y
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
vfsequence_of_vlist x = vfsequence_of_vlist []
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
vfsequence_of_vlist x = vfsequence_of_vlist []

goal (1 subgoal):
 1. x = []
[PROOF STEP]
by (cases x) auto
[PROOF STATE]
proof (state)
this:
x = []

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

goal (1 subgoal):
 1. \<And>a y x. \<lbrakk>\<And>x. vfsequence_of_vlist x = vfsequence_of_vlist y \<Longrightarrow> x = y; vfsequence_of_vlist x = vfsequence_of_vlist (a # y)\<rbrakk> \<Longrightarrow> x = a # y
[PROOF STEP]
note Cons' = Cons
[PROOF STATE]
proof (state)
this:
vfsequence_of_vlist ?x = vfsequence_of_vlist ys \<Longrightarrow> ?x = ys
vfsequence_of_vlist x = vfsequence_of_vlist (a # ys)

goal (1 subgoal):
 1. \<And>a y x. \<lbrakk>\<And>x. vfsequence_of_vlist x = vfsequence_of_vlist y \<Longrightarrow> x = y; vfsequence_of_vlist x = vfsequence_of_vlist (a # y)\<rbrakk> \<Longrightarrow> x = a # y
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x = a # ys
[PROOF STEP]
proof(cases x)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. x = [] \<Longrightarrow> x = a # ys
 2. \<And>aa list. x = aa # list \<Longrightarrow> x = a # ys
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
x = []

goal (2 subgoals):
 1. x = [] \<Longrightarrow> x = a # ys
 2. \<And>aa list. x = aa # list \<Longrightarrow> x = a # ys
[PROOF STEP]
with Cons
[PROOF STATE]
proof (chain)
picking this:
vfsequence_of_vlist ?x = vfsequence_of_vlist ys \<Longrightarrow> ?x = ys
vfsequence_of_vlist x = vfsequence_of_vlist (a # ys)
x = []
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
vfsequence_of_vlist ?x = vfsequence_of_vlist ys \<Longrightarrow> ?x = ys
vfsequence_of_vlist x = vfsequence_of_vlist (a # ys)
x = []

goal (1 subgoal):
 1. x = a # ys
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x = a # ys

goal (1 subgoal):
 1. \<And>aa list. x = aa # list \<Longrightarrow> x = a # ys
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>aa list. x = aa # list \<Longrightarrow> x = a # ys
[PROOF STEP]
case (Cons b zs)
[PROOF STATE]
proof (state)
this:
x = b # zs

goal (1 subgoal):
 1. \<And>aa list. x = aa # list \<Longrightarrow> x = a # ys
[PROOF STEP]
from Cons'[unfolded Cons vfsequence_of_vlist.simps]
[PROOF STATE]
proof (chain)
picking this:
vfsequence_of_vlist ?x = vfsequence_of_vlist ys \<Longrightarrow> ?x = ys
vfsequence_of_vlist zs #\<^sub>\<circ> b = vfsequence_of_vlist ys #\<^sub>\<circ> a
[PROOF STEP]
have
        "vfsequence_of_vlist zs #\<^sub>\<circ> b = vfsequence_of_vlist ys #\<^sub>\<circ> a"
[PROOF STATE]
proof (prove)
using this:
vfsequence_of_vlist ?x = vfsequence_of_vlist ys \<Longrightarrow> ?x = ys
vfsequence_of_vlist zs #\<^sub>\<circ> b = vfsequence_of_vlist ys #\<^sub>\<circ> a

goal (1 subgoal):
 1. vfsequence_of_vlist zs #\<^sub>\<circ> b = vfsequence_of_vlist ys #\<^sub>\<circ> a
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
vfsequence_of_vlist zs #\<^sub>\<circ> b = vfsequence_of_vlist ys #\<^sub>\<circ> a

goal (1 subgoal):
 1. \<And>aa list. x = aa # list \<Longrightarrow> x = a # ys
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
vfsequence_of_vlist zs #\<^sub>\<circ> b = vfsequence_of_vlist ys #\<^sub>\<circ> a
[PROOF STEP]
have "vfsequence_of_vlist zs = vfsequence_of_vlist ys" and "b = a"
[PROOF STATE]
proof (prove)
using this:
vfsequence_of_vlist zs #\<^sub>\<circ> b = vfsequence_of_vlist ys #\<^sub>\<circ> a

goal (1 subgoal):
 1. vfsequence_of_vlist zs = vfsequence_of_vlist ys &&& b = a
[PROOF STEP]
by (auto simp: vfsequence_vfsequence_of_vlist)
[PROOF STATE]
proof (state)
this:
vfsequence_of_vlist zs = vfsequence_of_vlist ys
b = a

goal (1 subgoal):
 1. \<And>aa list. x = aa # list \<Longrightarrow> x = a # ys
[PROOF STEP]
from Cons'(1)[OF this(1)] this(2)
[PROOF STATE]
proof (chain)
picking this:
zs = ys
b = a
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
zs = ys
b = a

goal (1 subgoal):
 1. x = a # ys
[PROOF STEP]
unfolding Cons
[PROOF STATE]
proof (prove)
using this:
zs = ys
b = a

goal (1 subgoal):
 1. b # zs = a # ys
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x = a # ys

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
vfsequence_of_vlist ?x = vfsequence_of_vlist ?y \<Longrightarrow> ?x = ?y

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma range_vfsequence_of_vlist:
  "range vfsequence_of_vlist = {xs. vfsequence xs}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. range vfsequence_of_vlist = {xs. vfsequence xs}
[PROOF STEP]
proof(intro subset_antisym subsetI; unfold mem_Collect_eq)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. x \<in> range vfsequence_of_vlist \<Longrightarrow> vfsequence x
 2. \<And>x. vfsequence x \<Longrightarrow> x \<in> range vfsequence_of_vlist
[PROOF STEP]
show "xs \<in> range vfsequence_of_vlist \<Longrightarrow> vfsequence xs" for xs
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. xs \<in> range vfsequence_of_vlist \<Longrightarrow> vfsequence xs
[PROOF STEP]
by (clarsimp simp: vfsequence_vfsequence_of_vlist)
[PROOF STATE]
proof (state)
this:
?xs \<in> range vfsequence_of_vlist \<Longrightarrow> vfsequence ?xs

goal (1 subgoal):
 1. \<And>x. vfsequence x \<Longrightarrow> x \<in> range vfsequence_of_vlist
[PROOF STEP]
fix xs
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. vfsequence x \<Longrightarrow> x \<in> range vfsequence_of_vlist
[PROOF STEP]
assume "vfsequence xs"
[PROOF STATE]
proof (state)
this:
vfsequence xs

goal (1 subgoal):
 1. \<And>x. vfsequence x \<Longrightarrow> x \<in> range vfsequence_of_vlist
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
vfsequence xs
[PROOF STEP]
show "xs \<in> range vfsequence_of_vlist"
[PROOF STATE]
proof (prove)
using this:
vfsequence xs

goal (1 subgoal):
 1. xs \<in> range vfsequence_of_vlist
[PROOF STEP]
proof(induction rule: vfsequence_induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. []\<^sub>\<circ> \<in> range vfsequence_of_vlist
 2. \<And>xs x. \<lbrakk>vfsequence xs; xs \<in> range vfsequence_of_vlist\<rbrakk> \<Longrightarrow> xs #\<^sub>\<circ> x \<in> range vfsequence_of_vlist
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. []\<^sub>\<circ> \<in> range vfsequence_of_vlist
 2. \<And>xs x. \<lbrakk>vfsequence xs; xs \<in> range vfsequence_of_vlist\<rbrakk> \<Longrightarrow> xs #\<^sub>\<circ> x \<in> range vfsequence_of_vlist
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. []\<^sub>\<circ> \<in> range vfsequence_of_vlist
[PROOF STEP]
by (metis image_iff iso_tuple_UNIV_I vfsequence_of_vlist.simps(1))
[PROOF STATE]
proof (state)
this:
[]\<^sub>\<circ> \<in> range vfsequence_of_vlist

goal (1 subgoal):
 1. \<And>xs x. \<lbrakk>vfsequence xs; xs \<in> range vfsequence_of_vlist\<rbrakk> \<Longrightarrow> xs #\<^sub>\<circ> x \<in> range vfsequence_of_vlist
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xs x. \<lbrakk>vfsequence xs; xs \<in> range vfsequence_of_vlist\<rbrakk> \<Longrightarrow> xs #\<^sub>\<circ> x \<in> range vfsequence_of_vlist
[PROOF STEP]
case (vcons xs x)
[PROOF STATE]
proof (state)
this:
vfsequence xs
xs \<in> range vfsequence_of_vlist

goal (1 subgoal):
 1. \<And>xs x. \<lbrakk>vfsequence xs; xs \<in> range vfsequence_of_vlist\<rbrakk> \<Longrightarrow> xs #\<^sub>\<circ> x \<in> range vfsequence_of_vlist
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
vfsequence xs
xs \<in> range vfsequence_of_vlist
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
vfsequence xs
xs \<in> range vfsequence_of_vlist

goal (1 subgoal):
 1. xs #\<^sub>\<circ> x \<in> range vfsequence_of_vlist
[PROOF STEP]
by (metis rangeE rangeI vfsequence_of_vlist.simps(2))
[PROOF STATE]
proof (state)
this:
xs #\<^sub>\<circ> x \<in> range vfsequence_of_vlist

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
xs \<in> range vfsequence_of_vlist

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma vlist_of_vfsequence_vfsequence_of_vlist[simp]:
  "vlist_of_vfsequence (vfsequence_of_vlist xs) = xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vlist_of_vfsequence (vfsequence_of_vlist xs) = xs
[PROOF STEP]
by (simp add: inj_vfsequence_of_vlist vlist_of_vfsequence_def)


[STATEMENT]
lemma (in vfsequence) vfsequence_of_vlist_vlist_of_vfsequence[simp]:
  "vfsequence_of_vlist (vlist_of_vfsequence xs) = xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vfsequence_of_vlist (vlist_of_vfsequence xs) = xs
[PROOF STEP]
using vfsequence_axioms range_vfsequence_of_vlist inj_vfsequence_of_vlist
[PROOF STATE]
proof (prove)
using this:
vfsequence xs
range vfsequence_of_vlist = {xs. vfsequence xs}
inj vfsequence_of_vlist

goal (1 subgoal):
 1. vfsequence_of_vlist (vlist_of_vfsequence xs) = xs
[PROOF STEP]
by (simp add: f_inv_into_f vlist_of_vfsequence_def)


[STATEMENT]
lemma vlist_of_vfsequence_vempty[simp]: "vlist_of_vfsequence []\<^sub>\<circ> = []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vlist_of_vfsequence []\<^sub>\<circ> = []
[PROOF STEP]
by
    (
      metis
        vfsequence_of_vlist.simps(1)
        vlist_of_vfsequence_vfsequence_of_vlist
    )


[STATEMENT]
lemma cr_vfsequence_right_total[transfer_rule]: "right_total cr_vfsequence"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. right_total cr_vfsequence
[PROOF STEP]
unfolding cr_vfsequence_def right_total_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>y. \<exists>x. x = vfsequence_of_vlist y
[PROOF STEP]
by simp


[STATEMENT]
lemma cr_vfsequence_bi_unqie[transfer_rule]: "bi_unique cr_vfsequence"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bi_unique cr_vfsequence
[PROOF STEP]
unfolding cr_vfsequence_def bi_unique_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>x y z. x = vfsequence_of_vlist y \<longrightarrow> x = vfsequence_of_vlist z \<longrightarrow> y = z) \<and> (\<forall>x y z. x = vfsequence_of_vlist z \<longrightarrow> y = vfsequence_of_vlist z \<longrightarrow> x = y)
[PROOF STEP]
by (simp add: inj_eq inj_vfsequence_of_vlist)


[STATEMENT]
lemma cr_vfsequence_transfer_domain_rule[transfer_domain_rule]:
  "Domainp cr_vfsequence = (\<lambda>xs. vfsequence xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Domainp cr_vfsequence = vfsequence
[PROOF STEP]
unfolding cr_vfsequence_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Domainp (\<lambda>a b. a = vfsequence_of_vlist b) = vfsequence
[PROOF STEP]
proof(intro HOL.ext, rule iffI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>xs. Domainp (\<lambda>a b. a = vfsequence_of_vlist b) xs \<Longrightarrow> vfsequence xs
 2. \<And>xs. vfsequence xs \<Longrightarrow> Domainp (\<lambda>a b. a = vfsequence_of_vlist b) xs
[PROOF STEP]
fix xs
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>xs. Domainp (\<lambda>a b. a = vfsequence_of_vlist b) xs \<Longrightarrow> vfsequence xs
 2. \<And>xs. vfsequence xs \<Longrightarrow> Domainp (\<lambda>a b. a = vfsequence_of_vlist b) xs
[PROOF STEP]
assume prems: "vfsequence xs"
[PROOF STATE]
proof (state)
this:
vfsequence xs

goal (2 subgoals):
 1. \<And>xs. Domainp (\<lambda>a b. a = vfsequence_of_vlist b) xs \<Longrightarrow> vfsequence xs
 2. \<And>xs. vfsequence xs \<Longrightarrow> Domainp (\<lambda>a b. a = vfsequence_of_vlist b) xs
[PROOF STEP]
interpret vfsequence xs
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vfsequence xs
[PROOF STEP]
by (rule prems)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>xs. Domainp (\<lambda>a b. a = vfsequence_of_vlist b) xs \<Longrightarrow> vfsequence xs
 2. \<And>xs. vfsequence xs \<Longrightarrow> Domainp (\<lambda>a b. a = vfsequence_of_vlist b) xs
[PROOF STEP]
have "\<exists>ys. xs = vfsequence_of_vlist ys"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>ys. xs = vfsequence_of_vlist ys
[PROOF STEP]
using prems
[PROOF STATE]
proof (prove)
using this:
vfsequence xs

goal (1 subgoal):
 1. \<exists>ys. xs = vfsequence_of_vlist ys
[PROOF STEP]
proof(induction rule: vfsequence_induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<exists>ys. []\<^sub>\<circ> = vfsequence_of_vlist ys
 2. \<And>xs x. \<lbrakk>vfsequence xs; \<exists>ys. xs = vfsequence_of_vlist ys\<rbrakk> \<Longrightarrow> \<exists>ys. xs #\<^sub>\<circ> x = vfsequence_of_vlist ys
[PROOF STEP]
show "\<lbrakk> vfsequence xs; \<exists>ys. xs = vfsequence_of_vlist ys \<rbrakk> \<Longrightarrow>
      \<exists>ys. xs #\<^sub>\<circ> x = vfsequence_of_vlist ys"
      for xs x
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>vfsequence xs; \<exists>ys. xs = vfsequence_of_vlist ys\<rbrakk> \<Longrightarrow> \<exists>ys. xs #\<^sub>\<circ> x = vfsequence_of_vlist ys
[PROOF STEP]
unfolding vfsequence_of_vlist_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>vfsequence xs; \<exists>ys. xs = rec_list []\<^sub>\<circ> (\<lambda>x xs xsa. xsa #\<^sub>\<circ> x) ys\<rbrakk> \<Longrightarrow> \<exists>ys. xs #\<^sub>\<circ> x = rec_list []\<^sub>\<circ> (\<lambda>x xs xsa. xsa #\<^sub>\<circ> x) ys
[PROOF STEP]
by (metis list.simps(7))
[PROOF STATE]
proof (state)
this:
\<lbrakk>vfsequence ?xs; \<exists>ys. ?xs = vfsequence_of_vlist ys\<rbrakk> \<Longrightarrow> \<exists>ys. ?xs #\<^sub>\<circ> ?x = vfsequence_of_vlist ys

goal (1 subgoal):
 1. \<exists>ys. []\<^sub>\<circ> = vfsequence_of_vlist ys
[PROOF STEP]
qed auto
[PROOF STATE]
proof (state)
this:
\<exists>ys. xs = vfsequence_of_vlist ys

goal (2 subgoals):
 1. \<And>xs. Domainp (\<lambda>a b. a = vfsequence_of_vlist b) xs \<Longrightarrow> vfsequence xs
 2. \<And>xs. vfsequence xs \<Longrightarrow> Domainp (\<lambda>a b. a = vfsequence_of_vlist b) xs
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>ys. xs = vfsequence_of_vlist ys
[PROOF STEP]
show "Domainp (\<lambda>a b. a = vfsequence_of_vlist b) xs"
[PROOF STATE]
proof (prove)
using this:
\<exists>ys. xs = vfsequence_of_vlist ys

goal (1 subgoal):
 1. Domainp (\<lambda>a b. a = vfsequence_of_vlist b) xs
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Domainp (\<lambda>a b. a = vfsequence_of_vlist b) xs

goal (1 subgoal):
 1. \<And>xs. Domainp (\<lambda>a b. a = vfsequence_of_vlist b) xs \<Longrightarrow> vfsequence xs
[PROOF STEP]
qed (clarsimp simp: vfsequence_vfsequence_of_vlist)


[STATEMENT]
lemma cr_vfsequence_vconsD:
  assumes "cr_vfsequence (xs #\<^sub>\<circ> x) (y # ys)"
  shows "cr_vfsequence xs ys" and "x = y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cr_vfsequence xs ys &&& x = y
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. cr_vfsequence xs ys
 2. x = y
[PROOF STEP]
from assms[unfolded cr_vfsequence_def]
[PROOF STATE]
proof (chain)
picking this:
xs #\<^sub>\<circ> x = vfsequence_of_vlist (y # ys)
[PROOF STEP]
have xs_x_def:
    "xs #\<^sub>\<circ> x = vfsequence_of_vlist (y # ys)"
[PROOF STATE]
proof (prove)
using this:
xs #\<^sub>\<circ> x = vfsequence_of_vlist (y # ys)

goal (1 subgoal):
 1. xs #\<^sub>\<circ> x = vfsequence_of_vlist (y # ys)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
xs #\<^sub>\<circ> x = vfsequence_of_vlist (y # ys)

goal (2 subgoals):
 1. cr_vfsequence xs ys
 2. x = y
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
xs #\<^sub>\<circ> x = vfsequence_of_vlist (y # ys)
[PROOF STEP]
have xs_x: "vfsequence (xs #\<^sub>\<circ> x)"
[PROOF STATE]
proof (prove)
using this:
xs #\<^sub>\<circ> x = vfsequence_of_vlist (y # ys)

goal (1 subgoal):
 1. vfsequence (xs #\<^sub>\<circ> x)
[PROOF STEP]
by (simp add: vfsequence_vfsequence_of_vlist)
[PROOF STATE]
proof (state)
this:
vfsequence (xs #\<^sub>\<circ> x)

goal (2 subgoals):
 1. cr_vfsequence xs ys
 2. x = y
[PROOF STEP]
interpret vfsequence xs
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vfsequence xs
[PROOF STEP]
by (blast intro: vfsequence.vfsequence_vremove_vcons_vfsequence xs_x)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. cr_vfsequence xs ys
 2. x = y
[PROOF STEP]
from
    assms[unfolded cr_vfsequence_def vfsequence_of_vlist.simps(2)]
    vfsequence_axioms
[PROOF STATE]
proof (chain)
picking this:
xs #\<^sub>\<circ> x = vfsequence_of_vlist ys #\<^sub>\<circ> y
vfsequence xs
[PROOF STEP]
show "cr_vfsequence xs ys" and "x = y"
[PROOF STATE]
proof (prove)
using this:
xs #\<^sub>\<circ> x = vfsequence_of_vlist ys #\<^sub>\<circ> y
vfsequence xs

goal (1 subgoal):
 1. cr_vfsequence xs ys &&& x = y
[PROOF STEP]
unfolding cr_vfsequence_def
[PROOF STATE]
proof (prove)
using this:
xs #\<^sub>\<circ> x = vfsequence_of_vlist ys #\<^sub>\<circ> y
vfsequence xs

goal (1 subgoal):
 1. xs = vfsequence_of_vlist ys &&& x = y
[PROOF STEP]
by (auto simp: vfsequence_vfsequence_of_vlist)
[PROOF STATE]
proof (state)
this:
cr_vfsequence xs ys
x = y

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma cr_cr_vfsequence_right_total[transfer_rule]:
  "right_total cr_cr_vfsequence"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. right_total cr_cr_vfsequence
[PROOF STEP]
unfolding cr_cr_vfsequence_def right_total_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>y. \<exists>x. x = vfsequence_of_vlist (map vfsequence_of_vlist y)
[PROOF STEP]
by simp


[STATEMENT]
lemma cr_cr_vfsequence_bi_unqie[transfer_rule]: "bi_unique cr_cr_vfsequence"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bi_unique cr_cr_vfsequence
[PROOF STEP]
unfolding cr_cr_vfsequence_def bi_unique_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>x y z. x = vfsequence_of_vlist (map vfsequence_of_vlist y) \<longrightarrow> x = vfsequence_of_vlist (map vfsequence_of_vlist z) \<longrightarrow> y = z) \<and> (\<forall>x y z. x = vfsequence_of_vlist (map vfsequence_of_vlist z) \<longrightarrow> y = vfsequence_of_vlist (map vfsequence_of_vlist z) \<longrightarrow> x = y)
[PROOF STEP]
by (simp add: inj_eq inj_vfsequence_of_vlist)


[STATEMENT]
lemma cr_scalar_bi_unique[transfer_rule]:
  assumes "bi_unique R"
  shows "bi_unique (cr_scalar R)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bi_unique (cr_scalar R)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
bi_unique R

goal (1 subgoal):
 1. bi_unique (cr_scalar R)
[PROOF STEP]
unfolding cr_scalar_def bi_unique_def
[PROOF STATE]
proof (prove)
using this:
(\<forall>x y z. R x y \<longrightarrow> R x z \<longrightarrow> y = z) \<and> (\<forall>x y z. R x z \<longrightarrow> R y z \<longrightarrow> x = y)

goal (1 subgoal):
 1. (\<forall>x y z. (\<exists>a. x = [a]\<^sub>\<circ> \<and> R a y) \<longrightarrow> (\<exists>a. x = [a]\<^sub>\<circ> \<and> R a z) \<longrightarrow> y = z) \<and> (\<forall>x y z. (\<exists>a. x = [a]\<^sub>\<circ> \<and> R a z) \<longrightarrow> (\<exists>a. y = [a]\<^sub>\<circ> \<and> R a z) \<longrightarrow> x = y)
[PROOF STEP]
by auto


[STATEMENT]
lemma cr_scalar_right_total[transfer_rule]:
  assumes "right_total R"
  shows "right_total (cr_scalar R)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. right_total (cr_scalar R)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
right_total R

goal (1 subgoal):
 1. right_total (cr_scalar R)
[PROOF STEP]
unfolding cr_scalar_def right_total_def
[PROOF STATE]
proof (prove)
using this:
\<forall>y. \<exists>x. R x y

goal (1 subgoal):
 1. \<forall>y. \<exists>x a. x = [a]\<^sub>\<circ> \<and> R a y
[PROOF STEP]
by simp


[STATEMENT]
lemma vfsequence_vempty_transfer[transfer_rule]: "cr_vfsequence []\<^sub>\<circ> []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cr_vfsequence []\<^sub>\<circ> []
[PROOF STEP]
unfolding cr_vfsequence_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. []\<^sub>\<circ> = vfsequence_of_vlist []
[PROOF STEP]
by simp


[STATEMENT]
lemma vfsequence_vempty_ll_transfer[transfer_rule]:
  "cr_cr_vfsequence [[]\<^sub>\<circ>]\<^sub>\<circ> [[]]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cr_cr_vfsequence [[]\<^sub>\<circ>]\<^sub>\<circ> [[]]
[PROOF STEP]
unfolding cr_cr_vfsequence_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [[]\<^sub>\<circ>]\<^sub>\<circ> = vfsequence_of_vlist (map vfsequence_of_vlist [[]])
[PROOF STEP]
by simp


[STATEMENT]
lemma vcons_transfer[transfer_rule]:
  "((=) ===> cr_vfsequence ===> cr_vfsequence) (\<lambda>x xs. xs #\<^sub>\<circ> x) (\<lambda>x xs. x # xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((=) ===> cr_vfsequence ===> cr_vfsequence) (\<lambda>x xs. xs #\<^sub>\<circ> x) (#)
[PROOF STEP]
by (intro rel_funI) (simp add: cr_vfsequence_def)


[STATEMENT]
lemma vcons_ll_transfer[transfer_rule]:
  "(cr_vfsequence ===> cr_cr_vfsequence ===> cr_cr_vfsequence)
    (\<lambda>x xs. xs #\<^sub>\<circ> x) (\<lambda>x xs. x # xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (cr_vfsequence ===> cr_cr_vfsequence ===> cr_cr_vfsequence) (\<lambda>x xs. xs #\<^sub>\<circ> x) (#)
[PROOF STEP]
by (intro rel_funI) (simp add: cr_vfsequence_def cr_cr_vfsequence_def)


[STATEMENT]
lemma vfsequence_vrange_transfer[transfer_rule]:
  "(cr_vfsequence ===> (=)) (\<lambda>xs. elts (\<R>\<^sub>\<circ> xs)) list.set"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (cr_vfsequence ===> (=)) (\<lambda>xs. elts (\<R>\<^sub>\<circ> xs)) list.set
[PROOF STEP]
proof(intro rel_funI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y. cr_vfsequence x y \<Longrightarrow> elts (\<R>\<^sub>\<circ> x) = list.set y
[PROOF STEP]
fix xs ys
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y. cr_vfsequence x y \<Longrightarrow> elts (\<R>\<^sub>\<circ> x) = list.set y
[PROOF STEP]
assume prems: "cr_vfsequence xs ys"
[PROOF STATE]
proof (state)
this:
cr_vfsequence xs ys

goal (1 subgoal):
 1. \<And>x y. cr_vfsequence x y \<Longrightarrow> elts (\<R>\<^sub>\<circ> x) = list.set y
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
cr_vfsequence xs ys
[PROOF STEP]
have "xs = vfsequence_of_vlist ys"
[PROOF STATE]
proof (prove)
using this:
cr_vfsequence xs ys

goal (1 subgoal):
 1. xs = vfsequence_of_vlist ys
[PROOF STEP]
unfolding cr_vfsequence_def
[PROOF STATE]
proof (prove)
using this:
xs = vfsequence_of_vlist ys

goal (1 subgoal):
 1. xs = vfsequence_of_vlist ys
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
xs = vfsequence_of_vlist ys

goal (1 subgoal):
 1. \<And>x y. cr_vfsequence x y \<Longrightarrow> elts (\<R>\<^sub>\<circ> x) = list.set y
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
xs = vfsequence_of_vlist ys
[PROOF STEP]
have "vfsequence xs"
[PROOF STATE]
proof (prove)
using this:
xs = vfsequence_of_vlist ys

goal (1 subgoal):
 1. vfsequence xs
[PROOF STEP]
by (simp add: vfsequence_vfsequence_of_vlist)
[PROOF STATE]
proof (state)
this:
vfsequence xs

goal (1 subgoal):
 1. \<And>x y. cr_vfsequence x y \<Longrightarrow> elts (\<R>\<^sub>\<circ> x) = list.set y
[PROOF STEP]
from this prems
[PROOF STATE]
proof (chain)
picking this:
vfsequence xs
cr_vfsequence xs ys
[PROOF STEP]
show "elts (\<R>\<^sub>\<circ> xs) = list.set ys"
[PROOF STATE]
proof (prove)
using this:
vfsequence xs
cr_vfsequence xs ys

goal (1 subgoal):
 1. elts (\<R>\<^sub>\<circ> xs) = list.set ys
[PROOF STEP]
proof(induction ys arbitrary: xs)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>xs. \<lbrakk>vfsequence xs; cr_vfsequence xs []\<rbrakk> \<Longrightarrow> elts (\<R>\<^sub>\<circ> xs) = list.set []
 2. \<And>a ys xs. \<lbrakk>\<And>xs. \<lbrakk>vfsequence xs; cr_vfsequence xs ys\<rbrakk> \<Longrightarrow> elts (\<R>\<^sub>\<circ> xs) = list.set ys; vfsequence xs; cr_vfsequence xs (a # ys)\<rbrakk> \<Longrightarrow> elts (\<R>\<^sub>\<circ> xs) = list.set (a # ys)
[PROOF STEP]
case (Cons a ys)
[PROOF STATE]
proof (state)
this:
\<lbrakk>vfsequence ?xs; cr_vfsequence ?xs ys\<rbrakk> \<Longrightarrow> elts (\<R>\<^sub>\<circ> ?xs) = list.set ys
vfsequence xs
cr_vfsequence xs (a # ys)

goal (2 subgoals):
 1. \<And>xs. \<lbrakk>vfsequence xs; cr_vfsequence xs []\<rbrakk> \<Longrightarrow> elts (\<R>\<^sub>\<circ> xs) = list.set []
 2. \<And>a ys xs. \<lbrakk>\<And>xs. \<lbrakk>vfsequence xs; cr_vfsequence xs ys\<rbrakk> \<Longrightarrow> elts (\<R>\<^sub>\<circ> xs) = list.set ys; vfsequence xs; cr_vfsequence xs (a # ys)\<rbrakk> \<Longrightarrow> elts (\<R>\<^sub>\<circ> xs) = list.set (a # ys)
[PROOF STEP]
from Cons(2)
[PROOF STATE]
proof (chain)
picking this:
vfsequence xs
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
vfsequence xs

goal (1 subgoal):
 1. elts (\<R>\<^sub>\<circ> xs) = list.set (a # ys)
[PROOF STEP]
proof(cases xs rule: vfsequence_cases)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. xs = []\<^sub>\<circ> \<Longrightarrow> elts (\<R>\<^sub>\<circ> xs) = list.set (a # ys)
 2. \<And>xs' x. \<lbrakk>xs = xs' #\<^sub>\<circ> x; vfsequence xs'\<rbrakk> \<Longrightarrow> elts (\<R>\<^sub>\<circ> xs) = list.set (a # ys)
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:
xs = []\<^sub>\<circ>

goal (2 subgoals):
 1. xs = []\<^sub>\<circ> \<Longrightarrow> elts (\<R>\<^sub>\<circ> xs) = list.set (a # ys)
 2. \<And>xs' x. \<lbrakk>xs = xs' #\<^sub>\<circ> x; vfsequence xs'\<rbrakk> \<Longrightarrow> elts (\<R>\<^sub>\<circ> xs) = list.set (a # ys)
[PROOF STEP]
with Cons
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>vfsequence ?xs; cr_vfsequence ?xs ys\<rbrakk> \<Longrightarrow> elts (\<R>\<^sub>\<circ> ?xs) = list.set ys
vfsequence xs
cr_vfsequence xs (a # ys)
xs = []\<^sub>\<circ>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>vfsequence ?xs; cr_vfsequence ?xs ys\<rbrakk> \<Longrightarrow> elts (\<R>\<^sub>\<circ> ?xs) = list.set ys
vfsequence xs
cr_vfsequence xs (a # ys)
xs = []\<^sub>\<circ>

goal (1 subgoal):
 1. elts (\<R>\<^sub>\<circ> xs) = list.set (a # ys)
[PROOF STEP]
by (simp add: Cons.IH cr_vfsequence_def)
[PROOF STATE]
proof (state)
this:
elts (\<R>\<^sub>\<circ> xs) = list.set (a # ys)

goal (1 subgoal):
 1. \<And>xs' x. \<lbrakk>xs = xs' #\<^sub>\<circ> x; vfsequence xs'\<rbrakk> \<Longrightarrow> elts (\<R>\<^sub>\<circ> xs) = list.set (a # ys)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xs' x. \<lbrakk>xs = xs' #\<^sub>\<circ> x; vfsequence xs'\<rbrakk> \<Longrightarrow> elts (\<R>\<^sub>\<circ> xs) = list.set (a # ys)
[PROOF STEP]
case (vcons xs' x)
[PROOF STATE]
proof (state)
this:
xs = xs' #\<^sub>\<circ> x
vfsequence xs'

goal (1 subgoal):
 1. \<And>xs' x. \<lbrakk>xs = xs' #\<^sub>\<circ> x; vfsequence xs'\<rbrakk> \<Longrightarrow> elts (\<R>\<^sub>\<circ> xs) = list.set (a # ys)
[PROOF STEP]
interpret vfsequence xs'
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vfsequence xs'
[PROOF STEP]
by (rule vcons(2))
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xs' x. \<lbrakk>xs = xs' #\<^sub>\<circ> x; vfsequence xs'\<rbrakk> \<Longrightarrow> elts (\<R>\<^sub>\<circ> xs) = list.set (a # ys)
[PROOF STEP]
note vcons_transfer = cr_vfsequence_vconsD[OF Cons(3)[unfolded vcons(1)]]
[PROOF STATE]
proof (state)
this:
cr_vfsequence xs' ys
x = a

goal (1 subgoal):
 1. \<And>xs' x. \<lbrakk>xs = xs' #\<^sub>\<circ> x; vfsequence xs'\<rbrakk> \<Longrightarrow> elts (\<R>\<^sub>\<circ> xs) = list.set (a # ys)
[PROOF STEP]
have a_ys: "list.set (a # ys) = insert a (list.set ys)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. list.set (a # ys) = insert a (list.set ys)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
list.set (a # ys) = insert a (list.set ys)

goal (1 subgoal):
 1. \<And>xs' x. \<lbrakk>xs = xs' #\<^sub>\<circ> x; vfsequence xs'\<rbrakk> \<Longrightarrow> elts (\<R>\<^sub>\<circ> xs) = list.set (a # ys)
[PROOF STEP]
from vcons(2)
[PROOF STATE]
proof (chain)
picking this:
vfsequence xs'
[PROOF STEP]
have R_xs'x: "\<R>\<^sub>\<circ> (xs' #\<^sub>\<circ> x) = vinsert x (\<R>\<^sub>\<circ> xs')"
[PROOF STATE]
proof (prove)
using this:
vfsequence xs'

goal (1 subgoal):
 1. \<R>\<^sub>\<circ> (xs' #\<^sub>\<circ> x) = vinsert x (\<R>\<^sub>\<circ> xs')
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<R>\<^sub>\<circ> (xs' #\<^sub>\<circ> x) = vinsert x (\<R>\<^sub>\<circ> xs')

goal (1 subgoal):
 1. \<And>xs' x. \<lbrakk>xs = xs' #\<^sub>\<circ> x; vfsequence xs'\<rbrakk> \<Longrightarrow> elts (\<R>\<^sub>\<circ> xs) = list.set (a # ys)
[PROOF STEP]
show "elts (\<R>\<^sub>\<circ> xs) = (list.set (a # ys))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. elts (\<R>\<^sub>\<circ> xs) = list.set (a # ys)
[PROOF STEP]
unfolding vcons(1) R_xs'x a_ys
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. elts (vinsert x (\<R>\<^sub>\<circ> xs')) = insert a (list.set ys)
[PROOF STEP]
by
          (
            auto simp:
              vcons_transfer(2) Cons(1)[OF vfsequence_axioms vcons_transfer(1)]
          )
[PROOF STATE]
proof (state)
this:
elts (\<R>\<^sub>\<circ> xs) = list.set (a # ys)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
elts (\<R>\<^sub>\<circ> xs) = list.set (a # ys)

goal (1 subgoal):
 1. \<And>xs. \<lbrakk>vfsequence xs; cr_vfsequence xs []\<rbrakk> \<Longrightarrow> elts (\<R>\<^sub>\<circ> xs) = list.set []
[PROOF STEP]
qed (auto simp: cr_vfsequence_def)
[PROOF STATE]
proof (state)
this:
elts (\<R>\<^sub>\<circ> xs) = list.set ys

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma vcard_transfer[transfer_rule]:
  "(cr_vfsequence ===> cr_omega) vcard length"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (cr_vfsequence ===> cr_omega) vcard length
[PROOF STEP]
proof(intro rel_funI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y. cr_vfsequence x y \<Longrightarrow> cr_omega (vcard x) (length y)
[PROOF STEP]
fix xs ys
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y. cr_vfsequence x y \<Longrightarrow> cr_omega (vcard x) (length y)
[PROOF STEP]
assume prems: "cr_vfsequence xs ys"
[PROOF STATE]
proof (state)
this:
cr_vfsequence xs ys

goal (1 subgoal):
 1. \<And>x y. cr_vfsequence x y \<Longrightarrow> cr_omega (vcard x) (length y)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
cr_vfsequence xs ys
[PROOF STEP]
have "xs = vfsequence_of_vlist ys"
[PROOF STATE]
proof (prove)
using this:
cr_vfsequence xs ys

goal (1 subgoal):
 1. xs = vfsequence_of_vlist ys
[PROOF STEP]
unfolding cr_vfsequence_def
[PROOF STATE]
proof (prove)
using this:
xs = vfsequence_of_vlist ys

goal (1 subgoal):
 1. xs = vfsequence_of_vlist ys
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
xs = vfsequence_of_vlist ys

goal (1 subgoal):
 1. \<And>x y. cr_vfsequence x y \<Longrightarrow> cr_omega (vcard x) (length y)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
xs = vfsequence_of_vlist ys
[PROOF STEP]
have "vfsequence xs"
[PROOF STATE]
proof (prove)
using this:
xs = vfsequence_of_vlist ys

goal (1 subgoal):
 1. vfsequence xs
[PROOF STEP]
by (simp add: vfsequence_vfsequence_of_vlist)
[PROOF STATE]
proof (state)
this:
vfsequence xs

goal (1 subgoal):
 1. \<And>x y. cr_vfsequence x y \<Longrightarrow> cr_omega (vcard x) (length y)
[PROOF STEP]
from this prems
[PROOF STATE]
proof (chain)
picking this:
vfsequence xs
cr_vfsequence xs ys
[PROOF STEP]
show "cr_omega (vcard xs) (length ys)"
[PROOF STATE]
proof (prove)
using this:
vfsequence xs
cr_vfsequence xs ys

goal (1 subgoal):
 1. cr_omega (vcard xs) (length ys)
[PROOF STEP]
proof(induction ys arbitrary: xs)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>xs. \<lbrakk>vfsequence xs; cr_vfsequence xs []\<rbrakk> \<Longrightarrow> cr_omega (vcard xs) (length [])
 2. \<And>a ys xs. \<lbrakk>\<And>xs. \<lbrakk>vfsequence xs; cr_vfsequence xs ys\<rbrakk> \<Longrightarrow> cr_omega (vcard xs) (length ys); vfsequence xs; cr_vfsequence xs (a # ys)\<rbrakk> \<Longrightarrow> cr_omega (vcard xs) (length (a # ys))
[PROOF STEP]
case (Cons y ys)
[PROOF STATE]
proof (state)
this:
\<lbrakk>vfsequence ?xs; cr_vfsequence ?xs ys\<rbrakk> \<Longrightarrow> cr_omega (vcard ?xs) (length ys)
vfsequence xs
cr_vfsequence xs (y # ys)

goal (2 subgoals):
 1. \<And>xs. \<lbrakk>vfsequence xs; cr_vfsequence xs []\<rbrakk> \<Longrightarrow> cr_omega (vcard xs) (length [])
 2. \<And>a ys xs. \<lbrakk>\<And>xs. \<lbrakk>vfsequence xs; cr_vfsequence xs ys\<rbrakk> \<Longrightarrow> cr_omega (vcard xs) (length ys); vfsequence xs; cr_vfsequence xs (a # ys)\<rbrakk> \<Longrightarrow> cr_omega (vcard xs) (length (a # ys))
[PROOF STEP]
from Cons(2)
[PROOF STATE]
proof (chain)
picking this:
vfsequence xs
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
vfsequence xs

goal (1 subgoal):
 1. cr_omega (vcard xs) (length (y # ys))
[PROOF STEP]
proof(cases xs rule: vfsequence_cases)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. xs = []\<^sub>\<circ> \<Longrightarrow> cr_omega (vcard xs) (length (y # ys))
 2. \<And>xs' x. \<lbrakk>xs = xs' #\<^sub>\<circ> x; vfsequence xs'\<rbrakk> \<Longrightarrow> cr_omega (vcard xs) (length (y # ys))
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:
xs = []\<^sub>\<circ>

goal (2 subgoals):
 1. xs = []\<^sub>\<circ> \<Longrightarrow> cr_omega (vcard xs) (length (y # ys))
 2. \<And>xs' x. \<lbrakk>xs = xs' #\<^sub>\<circ> x; vfsequence xs'\<rbrakk> \<Longrightarrow> cr_omega (vcard xs) (length (y # ys))
[PROOF STEP]
with Cons
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>vfsequence ?xs; cr_vfsequence ?xs ys\<rbrakk> \<Longrightarrow> cr_omega (vcard ?xs) (length ys)
vfsequence xs
cr_vfsequence xs (y # ys)
xs = []\<^sub>\<circ>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>vfsequence ?xs; cr_vfsequence ?xs ys\<rbrakk> \<Longrightarrow> cr_omega (vcard ?xs) (length ys)
vfsequence xs
cr_vfsequence xs (y # ys)
xs = []\<^sub>\<circ>

goal (1 subgoal):
 1. cr_omega (vcard xs) (length (y # ys))
[PROOF STEP]
by (simp add: Cons.IH cr_vfsequence_def)
[PROOF STATE]
proof (state)
this:
cr_omega (vcard xs) (length (y # ys))

goal (1 subgoal):
 1. \<And>xs' x. \<lbrakk>xs = xs' #\<^sub>\<circ> x; vfsequence xs'\<rbrakk> \<Longrightarrow> cr_omega (vcard xs) (length (y # ys))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xs' x. \<lbrakk>xs = xs' #\<^sub>\<circ> x; vfsequence xs'\<rbrakk> \<Longrightarrow> cr_omega (vcard xs) (length (y # ys))
[PROOF STEP]
case (vcons xs' x)
[PROOF STATE]
proof (state)
this:
xs = xs' #\<^sub>\<circ> x
vfsequence xs'

goal (1 subgoal):
 1. \<And>xs' x. \<lbrakk>xs = xs' #\<^sub>\<circ> x; vfsequence xs'\<rbrakk> \<Longrightarrow> cr_omega (vcard xs) (length (y # ys))
[PROOF STEP]
interpret vfsequence xs'
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vfsequence xs'
[PROOF STEP]
by (rule vcons(2))
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xs' x. \<lbrakk>xs = xs' #\<^sub>\<circ> x; vfsequence xs'\<rbrakk> \<Longrightarrow> cr_omega (vcard xs) (length (y # ys))
[PROOF STEP]
note vcons_transfer = cr_vfsequence_vconsD[OF Cons(3)[unfolded vcons(1)]]
[PROOF STATE]
proof (state)
this:
cr_vfsequence xs' ys
x = y

goal (1 subgoal):
 1. \<And>xs' x. \<lbrakk>xs = xs' #\<^sub>\<circ> x; vfsequence xs'\<rbrakk> \<Longrightarrow> cr_omega (vcard xs) (length (y # ys))
[PROOF STEP]
have vcard_xs_x: "vcard (xs' #\<^sub>\<circ> x) = succ (vcard xs')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vcard (xs' #\<^sub>\<circ> x) = ZFC_in_HOL.succ (vcard xs')
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
vcard (xs' #\<^sub>\<circ> x) = ZFC_in_HOL.succ (vcard xs')

goal (1 subgoal):
 1. \<And>xs' x. \<lbrakk>xs = xs' #\<^sub>\<circ> x; vfsequence xs'\<rbrakk> \<Longrightarrow> cr_omega (vcard xs) (length (y # ys))
[PROOF STEP]
have vcard_y_ys: "length (y # ys) = Suc (length ys)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (y # ys) = Suc (length ys)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
length (y # ys) = Suc (length ys)

goal (1 subgoal):
 1. \<And>xs' x. \<lbrakk>xs = xs' #\<^sub>\<circ> x; vfsequence xs'\<rbrakk> \<Longrightarrow> cr_omega (vcard xs) (length (y # ys))
[PROOF STEP]
from vfsequence_axioms
[PROOF STATE]
proof (chain)
picking this:
vfsequence xs'
[PROOF STEP]
have [transfer_rule]:
        "cr_omega (vcard xs') (length ys)"
[PROOF STATE]
proof (prove)
using this:
vfsequence xs'

goal (1 subgoal):
 1. cr_omega (vcard xs') (length ys)
[PROOF STEP]
by (simp add: vcons_transfer(1) Cons.IH)
[PROOF STATE]
proof (state)
this:
cr_omega (vcard xs') (length ys)

goal (1 subgoal):
 1. \<And>xs' x. \<lbrakk>xs = xs' #\<^sub>\<circ> x; vfsequence xs'\<rbrakk> \<Longrightarrow> cr_omega (vcard xs) (length (y # ys))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cr_omega (vcard xs) (length (y # ys))
[PROOF STEP]
unfolding vcons(1) vcard_xs_x vcard_y_ys
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cr_omega (ZFC_in_HOL.succ (vcard xs')) (Suc (length ys))
[PROOF STEP]
by transfer_prover
[PROOF STATE]
proof (state)
this:
cr_omega (vcard xs) (length (y # ys))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
cr_omega (vcard xs) (length (y # ys))

goal (1 subgoal):
 1. \<And>xs. \<lbrakk>vfsequence xs; cr_vfsequence xs []\<rbrakk> \<Longrightarrow> cr_omega (vcard xs) (length [])
[PROOF STEP]
qed (auto simp: cr_omega_def cr_vfsequence_def)
[PROOF STATE]
proof (state)
this:
cr_omega (vcard xs) (length ys)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma vcard_ll_transfer[transfer_rule]:
  "(cr_cr_vfsequence ===> cr_omega) vcard length"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (cr_cr_vfsequence ===> cr_omega) vcard length
[PROOF STEP]
unfolding cr_cr_vfsequence_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<lambda>a b. a = vfsequence_of_vlist (map vfsequence_of_vlist b)) ===> cr_omega) vcard length
[PROOF STEP]
by (intro rel_funI)
    (metis cr_vfsequence_def length_map rel_funD vcard_transfer)