[STATEMENT]
lemma vdomain_vfsequence_of_vlist: "\<D>\<^sub>\<circ> (vfsequence_of_vlist xs) = length xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<D>\<^sub>\<circ> (vfsequence_of_vlist xs) = length xs\<^sub>\<nat>
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<D>\<^sub>\<circ> (vfsequence_of_vlist xs) = length xs\<^sub>\<nat>
[PROOF STEP]
define ys where "ys = vfsequence_of_vlist xs"
[PROOF STATE]
proof (state)
this:
ys = vfsequence_of_vlist xs

goal (1 subgoal):
 1. \<D>\<^sub>\<circ> (vfsequence_of_vlist xs) = length xs\<^sub>\<nat>
[PROOF STEP]
interpret vfsequence ys
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vfsequence ys
[PROOF STEP]
unfolding ys_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vfsequence (vfsequence_of_vlist xs)
[PROOF STEP]
by (rule vfsequence_vfsequence_of_vlist)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<D>\<^sub>\<circ> (vfsequence_of_vlist xs) = length xs\<^sub>\<nat>
[PROOF STEP]
have [transfer_rule]: "cr_vfsequence ys xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cr_vfsequence ys xs
[PROOF STEP]
unfolding ys_def cr_vfsequence_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vfsequence_of_vlist xs = vfsequence_of_vlist xs
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
cr_vfsequence ys xs

goal (1 subgoal):
 1. \<D>\<^sub>\<circ> (vfsequence_of_vlist xs) = length xs\<^sub>\<nat>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<D>\<^sub>\<circ> (vfsequence_of_vlist xs) = length xs\<^sub>\<nat>
[PROOF STEP]
by (fold ys_def, unfold vfsequence_vdomain, transfer) simp
[PROOF STATE]
proof (state)
this:
\<D>\<^sub>\<circ> (vfsequence_of_vlist xs) = length xs\<^sub>\<nat>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma vrange_vfsequence_of_vlist:
  "\<R>\<^sub>\<circ> (vfsequence_of_vlist xs) = set (list.set xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<R>\<^sub>\<circ> (vfsequence_of_vlist xs) = set (list.set xs)
[PROOF STEP]
proof(intro vsubset_antisym vsubsetI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. x \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> (vfsequence_of_vlist xs) \<Longrightarrow> x \<in>\<^sub>\<circ> set (list.set xs)
 2. \<And>x. x \<in>\<^sub>\<circ> set (list.set xs) \<Longrightarrow> x \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> (vfsequence_of_vlist xs)
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. x \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> (vfsequence_of_vlist xs) \<Longrightarrow> x \<in>\<^sub>\<circ> set (list.set xs)
 2. \<And>x. x \<in>\<^sub>\<circ> set (list.set xs) \<Longrightarrow> x \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> (vfsequence_of_vlist xs)
[PROOF STEP]
assume prems: "x \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> (vfsequence_of_vlist xs)"
[PROOF STATE]
proof (state)
this:
x \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> (vfsequence_of_vlist xs)

goal (2 subgoals):
 1. \<And>x. x \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> (vfsequence_of_vlist xs) \<Longrightarrow> x \<in>\<^sub>\<circ> set (list.set xs)
 2. \<And>x. x \<in>\<^sub>\<circ> set (list.set xs) \<Longrightarrow> x \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> (vfsequence_of_vlist xs)
[PROOF STEP]
define ys where "ys = vfsequence_of_vlist xs"
[PROOF STATE]
proof (state)
this:
ys = vfsequence_of_vlist xs

goal (2 subgoals):
 1. \<And>x. x \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> (vfsequence_of_vlist xs) \<Longrightarrow> x \<in>\<^sub>\<circ> set (list.set xs)
 2. \<And>x. x \<in>\<^sub>\<circ> set (list.set xs) \<Longrightarrow> x \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> (vfsequence_of_vlist xs)
[PROOF STEP]
have [transfer_rule]: "cr_vfsequence ys xs" "x = x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cr_vfsequence ys xs &&& x = x
[PROOF STEP]
unfolding ys_def cr_vfsequence_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vfsequence_of_vlist xs = vfsequence_of_vlist xs &&& x = x
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
cr_vfsequence ys xs
x = x

goal (2 subgoals):
 1. \<And>x. x \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> (vfsequence_of_vlist xs) \<Longrightarrow> x \<in>\<^sub>\<circ> set (list.set xs)
 2. \<And>x. x \<in>\<^sub>\<circ> set (list.set xs) \<Longrightarrow> x \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> (vfsequence_of_vlist xs)
[PROOF STEP]
show "x \<in>\<^sub>\<circ> set (list.set xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in>\<^sub>\<circ> set (list.set xs)
[PROOF STEP]
by transfer (simp add: prems[folded ys_def])
[PROOF STATE]
proof (state)
this:
x \<in>\<^sub>\<circ> set (list.set xs)

goal (1 subgoal):
 1. \<And>x. x \<in>\<^sub>\<circ> set (list.set xs) \<Longrightarrow> x \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> (vfsequence_of_vlist xs)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in>\<^sub>\<circ> set (list.set xs) \<Longrightarrow> x \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> (vfsequence_of_vlist xs)
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in>\<^sub>\<circ> set (list.set xs) \<Longrightarrow> x \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> (vfsequence_of_vlist xs)
[PROOF STEP]
assume prems: "x \<in>\<^sub>\<circ> set (list.set xs)"
[PROOF STATE]
proof (state)
this:
x \<in>\<^sub>\<circ> set (list.set xs)

goal (1 subgoal):
 1. \<And>x. x \<in>\<^sub>\<circ> set (list.set xs) \<Longrightarrow> x \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> (vfsequence_of_vlist xs)
[PROOF STEP]
define ys where "ys = vfsequence_of_vlist xs"
[PROOF STATE]
proof (state)
this:
ys = vfsequence_of_vlist xs

goal (1 subgoal):
 1. \<And>x. x \<in>\<^sub>\<circ> set (list.set xs) \<Longrightarrow> x \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> (vfsequence_of_vlist xs)
[PROOF STEP]
have [transfer_rule]: "cr_vfsequence ys xs" "x = x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cr_vfsequence ys xs &&& x = x
[PROOF STEP]
unfolding ys_def cr_vfsequence_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vfsequence_of_vlist xs = vfsequence_of_vlist xs &&& x = x
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
cr_vfsequence ys xs
x = x

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

goal (1 subgoal):
 1. x \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> (vfsequence_of_vlist xs)
[PROOF STEP]
unfolding ys_def
[PROOF STATE]
proof (prove)
using this:
x \<in>\<^sub>\<circ> set (elts (\<R>\<^sub>\<circ> (vfsequence_of_vlist xs)))

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma cr_cr_vfsequence_transfer_domain_rule[transfer_domain_rule]:
  "Domainp cr_cr_vfsequence =
    (\<lambda>xss. vfsequence xss \<and> (\<forall>xs\<in>\<^sub>\<circ>\<R>\<^sub>\<circ> xss. vfsequence xs))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Domainp cr_cr_vfsequence = (\<lambda>xss. vfsequence xss \<and> (\<forall>xs\<in>elts (\<R>\<^sub>\<circ> xss). vfsequence xs))
[PROOF STEP]
proof(intro HOL.ext, rule iffI; (elim conjE | intro conjI ballI))
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>xss. Domainp cr_cr_vfsequence xss \<Longrightarrow> vfsequence xss
 2. \<And>xss xs. \<lbrakk>Domainp cr_cr_vfsequence xss; xs \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> xss\<rbrakk> \<Longrightarrow> vfsequence xs
 3. \<And>xss. \<lbrakk>vfsequence xss; \<forall>xs\<in>elts (\<R>\<^sub>\<circ> xss). vfsequence xs\<rbrakk> \<Longrightarrow> Domainp cr_cr_vfsequence xss
[PROOF STEP]
fix xss
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>xss. Domainp cr_cr_vfsequence xss \<Longrightarrow> vfsequence xss
 2. \<And>xss xs. \<lbrakk>Domainp cr_cr_vfsequence xss; xs \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> xss\<rbrakk> \<Longrightarrow> vfsequence xs
 3. \<And>xss. \<lbrakk>vfsequence xss; \<forall>xs\<in>elts (\<R>\<^sub>\<circ> xss). vfsequence xs\<rbrakk> \<Longrightarrow> Domainp cr_cr_vfsequence xss
[PROOF STEP]
assume prems: "Domainp cr_cr_vfsequence xss"
[PROOF STATE]
proof (state)
this:
Domainp cr_cr_vfsequence xss

goal (3 subgoals):
 1. \<And>xss. Domainp cr_cr_vfsequence xss \<Longrightarrow> vfsequence xss
 2. \<And>xss xs. \<lbrakk>Domainp cr_cr_vfsequence xss; xs \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> xss\<rbrakk> \<Longrightarrow> vfsequence xs
 3. \<And>xss. \<lbrakk>vfsequence xss; \<forall>xs\<in>elts (\<R>\<^sub>\<circ> xss). vfsequence xs\<rbrakk> \<Longrightarrow> Domainp cr_cr_vfsequence xss
[PROOF STEP]
with vfsequence_vfsequence_of_vlist
[PROOF STATE]
proof (chain)
picking this:
vfsequence (vfsequence_of_vlist ?xs)
Domainp cr_cr_vfsequence xss
[PROOF STEP]
show xss: "vfsequence xss"
[PROOF STATE]
proof (prove)
using this:
vfsequence (vfsequence_of_vlist ?xs)
Domainp cr_cr_vfsequence xss

goal (1 subgoal):
 1. vfsequence xss
[PROOF STEP]
unfolding cr_cr_vfsequence_def
[PROOF STATE]
proof (prove)
using this:
vfsequence (vfsequence_of_vlist ?xs)
Domainp (\<lambda>a b. a = vfsequence_of_vlist (map vfsequence_of_vlist b)) xss

goal (1 subgoal):
 1. vfsequence xss
[PROOF STEP]
by clarsimp
[PROOF STATE]
proof (state)
this:
vfsequence xss

goal (2 subgoals):
 1. \<And>xss xs. \<lbrakk>Domainp cr_cr_vfsequence xss; xs \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> xss\<rbrakk> \<Longrightarrow> vfsequence xs
 2. \<And>xss. \<lbrakk>vfsequence xss; \<forall>xs\<in>elts (\<R>\<^sub>\<circ> xss). vfsequence xs\<rbrakk> \<Longrightarrow> Domainp cr_cr_vfsequence xss
[PROOF STEP]
interpret vfsequence xss
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vfsequence xss
[PROOF STEP]
by (rule xss)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>xss xs. \<lbrakk>Domainp cr_cr_vfsequence xss; xs \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> xss\<rbrakk> \<Longrightarrow> vfsequence xs
 2. \<And>xss. \<lbrakk>vfsequence xss; \<forall>xs\<in>elts (\<R>\<^sub>\<circ> xss). vfsequence xs\<rbrakk> \<Longrightarrow> Domainp cr_cr_vfsequence xss
[PROOF STEP]
fix xs
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>xss xs. \<lbrakk>Domainp cr_cr_vfsequence xss; xs \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> xss\<rbrakk> \<Longrightarrow> vfsequence xs
 2. \<And>xss. \<lbrakk>vfsequence xss; \<forall>xs\<in>elts (\<R>\<^sub>\<circ> xss). vfsequence xs\<rbrakk> \<Longrightarrow> Domainp cr_cr_vfsequence xss
[PROOF STEP]
assume prems': "xs \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> xss"
[PROOF STATE]
proof (state)
this:
xs \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> xss

goal (2 subgoals):
 1. \<And>xss xs. \<lbrakk>Domainp cr_cr_vfsequence xss; xs \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> xss\<rbrakk> \<Longrightarrow> vfsequence xs
 2. \<And>xss. \<lbrakk>vfsequence xss; \<forall>xs\<in>elts (\<R>\<^sub>\<circ> xss). vfsequence xs\<rbrakk> \<Longrightarrow> Domainp cr_cr_vfsequence xss
[PROOF STEP]
from prems
[PROOF STATE]
proof (chain)
picking this:
Domainp cr_cr_vfsequence xss
[PROOF STEP]
obtain yss where xss_def:
    "xss = vfsequence_of_vlist (map vfsequence_of_vlist yss)"
[PROOF STATE]
proof (prove)
using this:
Domainp cr_cr_vfsequence xss

goal (1 subgoal):
 1. (\<And>yss. xss = vfsequence_of_vlist (map vfsequence_of_vlist yss) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding cr_cr_vfsequence_def
[PROOF STATE]
proof (prove)
using this:
Domainp (\<lambda>a b. a = vfsequence_of_vlist (map vfsequence_of_vlist b)) xss

goal (1 subgoal):
 1. (\<And>yss. xss = vfsequence_of_vlist (map vfsequence_of_vlist yss) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by clarsimp
[PROOF STATE]
proof (state)
this:
xss = vfsequence_of_vlist (map vfsequence_of_vlist yss)

goal (2 subgoals):
 1. \<And>xss xs. \<lbrakk>Domainp cr_cr_vfsequence xss; xs \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> xss\<rbrakk> \<Longrightarrow> vfsequence xs
 2. \<And>xss. \<lbrakk>vfsequence xss; \<forall>xs\<in>elts (\<R>\<^sub>\<circ> xss). vfsequence xs\<rbrakk> \<Longrightarrow> Domainp cr_cr_vfsequence xss
[PROOF STEP]
from prems'
[PROOF STATE]
proof (chain)
picking this:
xs \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> xss
[PROOF STEP]
have "xs \<in>\<^sub>\<circ> set (list.set (map vfsequence_of_vlist yss))"
[PROOF STATE]
proof (prove)
using this:
xs \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> xss

goal (1 subgoal):
 1. xs \<in>\<^sub>\<circ> set (list.set (map vfsequence_of_vlist yss))
[PROOF STEP]
unfolding xss_def vrange_vfsequence_of_vlist
[PROOF STATE]
proof (prove)
using this:
xs \<in>\<^sub>\<circ> set (list.set (map vfsequence_of_vlist yss))

goal (1 subgoal):
 1. xs \<in>\<^sub>\<circ> set (list.set (map vfsequence_of_vlist yss))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
xs \<in>\<^sub>\<circ> set (list.set (map vfsequence_of_vlist yss))

goal (2 subgoals):
 1. \<And>xss xs. \<lbrakk>Domainp cr_cr_vfsequence xss; xs \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> xss\<rbrakk> \<Longrightarrow> vfsequence xs
 2. \<And>xss. \<lbrakk>vfsequence xss; \<forall>xs\<in>elts (\<R>\<^sub>\<circ> xss). vfsequence xs\<rbrakk> \<Longrightarrow> Domainp cr_cr_vfsequence xss
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
xs \<in>\<^sub>\<circ> set (list.set (map vfsequence_of_vlist yss))
[PROOF STEP]
obtain ys where xs_def: "xs = vfsequence_of_vlist ys"
[PROOF STATE]
proof (prove)
using this:
xs \<in>\<^sub>\<circ> set (list.set (map vfsequence_of_vlist yss))

goal (1 subgoal):
 1. (\<And>ys. xs = vfsequence_of_vlist ys \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by clarsimp
[PROOF STATE]
proof (state)
this:
xs = vfsequence_of_vlist ys

goal (2 subgoals):
 1. \<And>xss xs. \<lbrakk>Domainp cr_cr_vfsequence xss; xs \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> xss\<rbrakk> \<Longrightarrow> vfsequence xs
 2. \<And>xss. \<lbrakk>vfsequence xss; \<forall>xs\<in>elts (\<R>\<^sub>\<circ> xss). vfsequence xs\<rbrakk> \<Longrightarrow> Domainp cr_cr_vfsequence xss
[PROOF STEP]
show "vfsequence xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vfsequence xs
[PROOF STEP]
unfolding xs_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vfsequence (vfsequence_of_vlist ys)
[PROOF STEP]
by (simp add: vfsequence_vfsequence_of_vlist)
[PROOF STATE]
proof (state)
this:
vfsequence xs

goal (1 subgoal):
 1. \<And>xss. \<lbrakk>vfsequence xss; \<forall>xs\<in>elts (\<R>\<^sub>\<circ> xss). vfsequence xs\<rbrakk> \<Longrightarrow> Domainp cr_cr_vfsequence xss
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xss. \<lbrakk>vfsequence xss; \<forall>xs\<in>elts (\<R>\<^sub>\<circ> xss). vfsequence xs\<rbrakk> \<Longrightarrow> Domainp cr_cr_vfsequence xss
[PROOF STEP]
fix xss
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xss. \<lbrakk>vfsequence xss; \<forall>xs\<in>elts (\<R>\<^sub>\<circ> xss). vfsequence xs\<rbrakk> \<Longrightarrow> Domainp cr_cr_vfsequence xss
[PROOF STEP]
assume prems: "vfsequence xss" "\<forall>xs\<in>\<^sub>\<circ>\<R>\<^sub>\<circ> xss. vfsequence xs"
[PROOF STATE]
proof (state)
this:
vfsequence xss
\<forall>xs\<in>elts (\<R>\<^sub>\<circ> xss). vfsequence xs

goal (1 subgoal):
 1. \<And>xss. \<lbrakk>vfsequence xss; \<forall>xs\<in>elts (\<R>\<^sub>\<circ> xss). vfsequence xs\<rbrakk> \<Longrightarrow> Domainp cr_cr_vfsequence xss
[PROOF STEP]
have "\<exists>yss. xss = vfsequence_of_vlist (map vfsequence_of_vlist yss)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>yss. xss = vfsequence_of_vlist (map vfsequence_of_vlist yss)
[PROOF STEP]
using prems
[PROOF STATE]
proof (prove)
using this:
vfsequence xss
\<forall>xs\<in>elts (\<R>\<^sub>\<circ> xss). vfsequence xs

goal (1 subgoal):
 1. \<exists>yss. xss = vfsequence_of_vlist (map vfsequence_of_vlist yss)
[PROOF STEP]
proof(induction rule: vfsequence_induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. Ball (elts (\<R>\<^sub>\<circ> []\<^sub>\<circ>)) vfsequence \<Longrightarrow> \<exists>yss. []\<^sub>\<circ> = vfsequence_of_vlist (map vfsequence_of_vlist yss)
 2. \<And>xs x. \<lbrakk>vfsequence xs; Ball (elts (\<R>\<^sub>\<circ> xs)) vfsequence \<Longrightarrow> \<exists>yss. xs = vfsequence_of_vlist (map vfsequence_of_vlist yss); Ball (elts (\<R>\<^sub>\<circ> (xs #\<^sub>\<circ> x))) vfsequence\<rbrakk> \<Longrightarrow> \<exists>yss. xs #\<^sub>\<circ> x = vfsequence_of_vlist (map vfsequence_of_vlist yss)
[PROOF STEP]
case (vcons xss x)
[PROOF STATE]
proof (state)
this:
vfsequence xss
\<forall>a\<in>elts (\<R>\<^sub>\<circ> xss). vfsequence a \<Longrightarrow> \<exists>yss. xss = vfsequence_of_vlist (map vfsequence_of_vlist yss)
\<forall>a\<in>elts (\<R>\<^sub>\<circ> (xss #\<^sub>\<circ> x)). vfsequence a

goal (2 subgoals):
 1. Ball (elts (\<R>\<^sub>\<circ> []\<^sub>\<circ>)) vfsequence \<Longrightarrow> \<exists>yss. []\<^sub>\<circ> = vfsequence_of_vlist (map vfsequence_of_vlist yss)
 2. \<And>xs x. \<lbrakk>vfsequence xs; Ball (elts (\<R>\<^sub>\<circ> xs)) vfsequence \<Longrightarrow> \<exists>yss. xs = vfsequence_of_vlist (map vfsequence_of_vlist yss); Ball (elts (\<R>\<^sub>\<circ> (xs #\<^sub>\<circ> x))) vfsequence\<rbrakk> \<Longrightarrow> \<exists>yss. xs #\<^sub>\<circ> x = vfsequence_of_vlist (map vfsequence_of_vlist yss)
[PROOF STEP]
let ?y = \<open>vlist_of_vfsequence x\<close>
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. Ball (elts (\<R>\<^sub>\<circ> []\<^sub>\<circ>)) vfsequence \<Longrightarrow> \<exists>yss. []\<^sub>\<circ> = vfsequence_of_vlist (map vfsequence_of_vlist yss)
 2. \<And>xs x. \<lbrakk>vfsequence xs; Ball (elts (\<R>\<^sub>\<circ> xs)) vfsequence \<Longrightarrow> \<exists>yss. xs = vfsequence_of_vlist (map vfsequence_of_vlist yss); Ball (elts (\<R>\<^sub>\<circ> (xs #\<^sub>\<circ> x))) vfsequence\<rbrakk> \<Longrightarrow> \<exists>yss. xs #\<^sub>\<circ> x = vfsequence_of_vlist (map vfsequence_of_vlist yss)
[PROOF STEP]
from vcons(2,3)
[PROOF STATE]
proof (chain)
picking this:
\<forall>a\<in>elts (\<R>\<^sub>\<circ> xss). vfsequence a \<Longrightarrow> \<exists>yss. xss = vfsequence_of_vlist (map vfsequence_of_vlist yss)
\<forall>a\<in>elts (\<R>\<^sub>\<circ> (xss #\<^sub>\<circ> x)). vfsequence a
[PROOF STEP]
obtain yss where xss_def:
      "xss = vfsequence_of_vlist (map vfsequence_of_vlist yss)"
[PROOF STATE]
proof (prove)
using this:
\<forall>a\<in>elts (\<R>\<^sub>\<circ> xss). vfsequence a \<Longrightarrow> \<exists>yss. xss = vfsequence_of_vlist (map vfsequence_of_vlist yss)
\<forall>a\<in>elts (\<R>\<^sub>\<circ> (xss #\<^sub>\<circ> x)). vfsequence a

goal (1 subgoal):
 1. (\<And>yss. xss = vfsequence_of_vlist (map vfsequence_of_vlist yss) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
xss = vfsequence_of_vlist (map vfsequence_of_vlist yss)

goal (2 subgoals):
 1. Ball (elts (\<R>\<^sub>\<circ> []\<^sub>\<circ>)) vfsequence \<Longrightarrow> \<exists>yss. []\<^sub>\<circ> = vfsequence_of_vlist (map vfsequence_of_vlist yss)
 2. \<And>xs x. \<lbrakk>vfsequence xs; Ball (elts (\<R>\<^sub>\<circ> xs)) vfsequence \<Longrightarrow> \<exists>yss. xs = vfsequence_of_vlist (map vfsequence_of_vlist yss); Ball (elts (\<R>\<^sub>\<circ> (xs #\<^sub>\<circ> x))) vfsequence\<rbrakk> \<Longrightarrow> \<exists>yss. xs #\<^sub>\<circ> x = vfsequence_of_vlist (map vfsequence_of_vlist yss)
[PROOF STEP]
from vcons(3)
[PROOF STATE]
proof (chain)
picking this:
\<forall>a\<in>elts (\<R>\<^sub>\<circ> (xss #\<^sub>\<circ> x)). vfsequence a
[PROOF STEP]
have "vfsequence x"
[PROOF STATE]
proof (prove)
using this:
\<forall>a\<in>elts (\<R>\<^sub>\<circ> (xss #\<^sub>\<circ> x)). vfsequence a

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

goal (2 subgoals):
 1. Ball (elts (\<R>\<^sub>\<circ> []\<^sub>\<circ>)) vfsequence \<Longrightarrow> \<exists>yss. []\<^sub>\<circ> = vfsequence_of_vlist (map vfsequence_of_vlist yss)
 2. \<And>xs x. \<lbrakk>vfsequence xs; Ball (elts (\<R>\<^sub>\<circ> xs)) vfsequence \<Longrightarrow> \<exists>yss. xs = vfsequence_of_vlist (map vfsequence_of_vlist yss); Ball (elts (\<R>\<^sub>\<circ> (xs #\<^sub>\<circ> x))) vfsequence\<rbrakk> \<Longrightarrow> \<exists>yss. xs #\<^sub>\<circ> x = vfsequence_of_vlist (map vfsequence_of_vlist yss)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
vfsequence x
[PROOF STEP]
have x_def: "x = vfsequence_of_vlist (vlist_of_vfsequence x)"
[PROOF STATE]
proof (prove)
using this:
vfsequence x

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

goal (2 subgoals):
 1. Ball (elts (\<R>\<^sub>\<circ> []\<^sub>\<circ>)) vfsequence \<Longrightarrow> \<exists>yss. []\<^sub>\<circ> = vfsequence_of_vlist (map vfsequence_of_vlist yss)
 2. \<And>xs x. \<lbrakk>vfsequence xs; Ball (elts (\<R>\<^sub>\<circ> xs)) vfsequence \<Longrightarrow> \<exists>yss. xs = vfsequence_of_vlist (map vfsequence_of_vlist yss); Ball (elts (\<R>\<^sub>\<circ> (xs #\<^sub>\<circ> x))) vfsequence\<rbrakk> \<Longrightarrow> \<exists>yss. xs #\<^sub>\<circ> x = vfsequence_of_vlist (map vfsequence_of_vlist yss)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x = vfsequence_of_vlist (vlist_of_vfsequence x)
[PROOF STEP]
have
      "xss #\<^sub>\<circ> x = vfsequence_of_vlist (map vfsequence_of_vlist (?y # yss))"
[PROOF STATE]
proof (prove)
using this:
x = vfsequence_of_vlist (vlist_of_vfsequence x)

goal (1 subgoal):
 1. xss #\<^sub>\<circ> x = vfsequence_of_vlist (map vfsequence_of_vlist (vlist_of_vfsequence x # yss))
[PROOF STEP]
unfolding xss_def
[PROOF STATE]
proof (prove)
using this:
x = vfsequence_of_vlist (vlist_of_vfsequence x)

goal (1 subgoal):
 1. vfsequence_of_vlist (map vfsequence_of_vlist yss) #\<^sub>\<circ> x = vfsequence_of_vlist (map vfsequence_of_vlist (vlist_of_vfsequence x # yss))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
xss #\<^sub>\<circ> x = vfsequence_of_vlist (map vfsequence_of_vlist (vlist_of_vfsequence x # yss))

goal (2 subgoals):
 1. Ball (elts (\<R>\<^sub>\<circ> []\<^sub>\<circ>)) vfsequence \<Longrightarrow> \<exists>yss. []\<^sub>\<circ> = vfsequence_of_vlist (map vfsequence_of_vlist yss)
 2. \<And>xs x. \<lbrakk>vfsequence xs; Ball (elts (\<R>\<^sub>\<circ> xs)) vfsequence \<Longrightarrow> \<exists>yss. xs = vfsequence_of_vlist (map vfsequence_of_vlist yss); Ball (elts (\<R>\<^sub>\<circ> (xs #\<^sub>\<circ> x))) vfsequence\<rbrakk> \<Longrightarrow> \<exists>yss. xs #\<^sub>\<circ> x = vfsequence_of_vlist (map vfsequence_of_vlist yss)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
xss #\<^sub>\<circ> x = vfsequence_of_vlist (map vfsequence_of_vlist (vlist_of_vfsequence x # yss))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
xss #\<^sub>\<circ> x = vfsequence_of_vlist (map vfsequence_of_vlist (vlist_of_vfsequence x # yss))

goal (1 subgoal):
 1. \<exists>yss. xss #\<^sub>\<circ> x = vfsequence_of_vlist (map vfsequence_of_vlist yss)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>yss. xss #\<^sub>\<circ> x = vfsequence_of_vlist (map vfsequence_of_vlist yss)

goal (1 subgoal):
 1. Ball (elts (\<R>\<^sub>\<circ> []\<^sub>\<circ>)) vfsequence \<Longrightarrow> \<exists>yss. []\<^sub>\<circ> = vfsequence_of_vlist (map vfsequence_of_vlist yss)
[PROOF STEP]
qed (auto intro: exI[of _ \<open>[]\<close>])
[PROOF STATE]
proof (state)
this:
\<exists>yss. xss = vfsequence_of_vlist (map vfsequence_of_vlist yss)

goal (1 subgoal):
 1. \<And>xss. \<lbrakk>vfsequence xss; \<forall>xs\<in>elts (\<R>\<^sub>\<circ> xss). vfsequence xs\<rbrakk> \<Longrightarrow> Domainp cr_cr_vfsequence xss
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>yss. xss = vfsequence_of_vlist (map vfsequence_of_vlist yss)
[PROOF STEP]
show "Domainp cr_cr_vfsequence xss"
[PROOF STATE]
proof (prove)
using this:
\<exists>yss. xss = vfsequence_of_vlist (map vfsequence_of_vlist yss)

goal (1 subgoal):
 1. Domainp cr_cr_vfsequence xss
[PROOF STEP]
unfolding cr_cr_vfsequence_def
[PROOF STATE]
proof (prove)
using this:
\<exists>yss. xss = vfsequence_of_vlist (map vfsequence_of_vlist yss)

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma vappend_ll_transfer[transfer_rule]:
  includes lifting_syntax
  shows "(cr_cr_vfsequence ===> cr_cr_vfsequence ===> cr_cr_vfsequence)
    (\<lambda>xs ys. vappend ys xs) append"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (cr_cr_vfsequence ===> cr_cr_vfsequence ===> cr_cr_vfsequence) (\<lambda>xs ys. ys @\<^sub>\<circ> xs) (@)
[PROOF STEP]
by (intro rel_funI, unfold cr_cr_vfsequence_def) (simp add: vappend_def)


[STATEMENT]
lemma (in vfsequence) vfsequence_vappend_vempty_vfsequence[simp]:
  "[]\<^sub>\<circ> @\<^sub>\<circ> xs = xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. []\<^sub>\<circ> @\<^sub>\<circ> xs = xs
[PROOF STEP]
unfolding vappend_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vfsequence_of_vlist (vlist_of_vfsequence xs @ vlist_of_vfsequence []\<^sub>\<circ>) = xs
[PROOF STEP]
by auto


[STATEMENT]
lemma (in vfsequence) vfsequence_vappend_vfsequence_vempty[simp]:
  "xs @\<^sub>\<circ> []\<^sub>\<circ> = xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. xs @\<^sub>\<circ> []\<^sub>\<circ> = xs
[PROOF STEP]
unfolding vappend_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vfsequence_of_vlist (vlist_of_vfsequence []\<^sub>\<circ> @ vlist_of_vfsequence xs) = xs
[PROOF STEP]
by auto


[STATEMENT]
lemma vappend_vcons[simp]:
  assumes "vfsequence xs" and "vfsequence ys"
  shows "xs @\<^sub>\<circ> (ys #\<^sub>\<circ> y) = (xs @\<^sub>\<circ> ys) #\<^sub>\<circ> y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. xs @\<^sub>\<circ> ys #\<^sub>\<circ> y = (xs @\<^sub>\<circ> ys) #\<^sub>\<circ> y
[PROOF STEP]
using append_Cons[where 'a=V, untransferred, OF assms(2,1)]
[PROOF STATE]
proof (prove)
using this:
xs @\<^sub>\<circ> ys #\<^sub>\<circ> ?x = (xs @\<^sub>\<circ> ys) #\<^sub>\<circ> ?x

goal (1 subgoal):
 1. xs @\<^sub>\<circ> ys #\<^sub>\<circ> y = (xs @\<^sub>\<circ> ys) #\<^sub>\<circ> y
[PROOF STEP]
by simp


[STATEMENT]
lemma vdistinct_transfer[transfer_rule]:
  includes lifting_syntax
  shows "(cr_vfsequence ===> (=)) vdistinct distinct"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (cr_vfsequence ===> (=)) vdistinct distinct
[PROOF STEP]
by (intro rel_funI, unfold cr_vfsequence_def) (simp add: vdistinct_def)


[STATEMENT]
lemma vdistinct_ll_transfer[transfer_rule]:
  includes lifting_syntax
  shows "(cr_cr_vfsequence ===> (=)) vdistinct distinct"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (cr_cr_vfsequence ===> (=)) vdistinct distinct
[PROOF STEP]
by (intro rel_funI, unfold cr_cr_vfsequence_def)
    (
      metis
        vdistinct_def
        distinct_map
        inj_onI
        vlist_of_vfsequence_vfsequence_of_vlist
    )


[STATEMENT]
lemma (in vfsequence) vfsequence_vdistinct_if_vcard_vrange_eq_vcard:
  assumes "vcard (\<R>\<^sub>\<circ> xs) = vcard xs"
  shows "vdistinct xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vdistinct xs
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. vdistinct xs
[PROOF STEP]
have "finite (elts (\<R>\<^sub>\<circ> xs))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vfinite (\<R>\<^sub>\<circ> xs)
[PROOF STEP]
by (simp add: assms vcard_vfinite_omega)
[PROOF STATE]
proof (state)
this:
vfinite (\<R>\<^sub>\<circ> xs)

goal (1 subgoal):
 1. vdistinct xs
[PROOF STEP]
from vcard_finite_set[OF this] assms
[PROOF STATE]
proof (chain)
picking this:
vcard (set (elts (\<R>\<^sub>\<circ> xs))) = card (elts (\<R>\<^sub>\<circ> xs))\<^sub>\<nat>
vcard (\<R>\<^sub>\<circ> xs) = vcard xs
[PROOF STEP]
have "card (elts (\<R>\<^sub>\<circ> xs))\<^sub>\<nat> = vcard xs"
[PROOF STATE]
proof (prove)
using this:
vcard (set (elts (\<R>\<^sub>\<circ> xs))) = card (elts (\<R>\<^sub>\<circ> xs))\<^sub>\<nat>
vcard (\<R>\<^sub>\<circ> xs) = vcard xs

goal (1 subgoal):
 1. card (elts (\<R>\<^sub>\<circ> xs))\<^sub>\<nat> = vcard xs
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
card (elts (\<R>\<^sub>\<circ> xs))\<^sub>\<nat> = vcard xs

goal (1 subgoal):
 1. vdistinct xs
[PROOF STEP]
from card_distinct[where ?'a=V, untransferred, OF vfsequence_axioms this]
[PROOF STATE]
proof (chain)
picking this:
vdistinct xs
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
vdistinct xs

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma vdistinct_vempty[intro, simp]: "vdistinct []\<^sub>\<circ>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vdistinct []\<^sub>\<circ>
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. vdistinct []\<^sub>\<circ>
[PROOF STEP]
have t: "distinct ([]::V list)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distinct []
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
distinct []

goal (1 subgoal):
 1. vdistinct []\<^sub>\<circ>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vdistinct []\<^sub>\<circ>
[PROOF STEP]
by (rule t[untransferred])
[PROOF STATE]
proof (state)
this:
vdistinct []\<^sub>\<circ>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in vfsequence) vfsequence_vcons_vdistinct:
  assumes "vdistinct (xs #\<^sub>\<circ> x)"
  shows "vdistinct xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vdistinct xs
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. vdistinct xs
[PROOF STEP]
from distinct.simps(2)[where 'a=V, THEN iffD1, THEN conjunct2, untransferred]
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>vfsequence ?xs; vdistinct (?xs #\<^sub>\<circ> ?x)\<rbrakk> \<Longrightarrow> vdistinct ?xs
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>vfsequence ?xs; vdistinct (?xs #\<^sub>\<circ> ?x)\<rbrakk> \<Longrightarrow> vdistinct ?xs

goal (1 subgoal):
 1. vdistinct xs
[PROOF STEP]
using vfsequence_axioms assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>vfsequence ?xs; vdistinct (?xs #\<^sub>\<circ> ?x)\<rbrakk> \<Longrightarrow> vdistinct ?xs
vfsequence xs
vdistinct (xs #\<^sub>\<circ> x)

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in vfsequence) vfsequence_vcons_nin_vrange:
  assumes "vdistinct (xs #\<^sub>\<circ> x)"
  shows "x \<notin>\<^sub>\<circ> \<R>\<^sub>\<circ> xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<notin>\<^sub>\<circ> \<R>\<^sub>\<circ> xs
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x \<notin>\<^sub>\<circ> \<R>\<^sub>\<circ> xs
[PROOF STEP]
from distinct.simps(2)[where 'a=V, THEN iffD1, THEN conjunct1, untransferred]
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>vfsequence ?xs; vdistinct (?xs #\<^sub>\<circ> ?x)\<rbrakk> \<Longrightarrow> ?x \<notin>\<^sub>\<circ> \<R>\<^sub>\<circ> ?xs
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>vfsequence ?xs; vdistinct (?xs #\<^sub>\<circ> ?x)\<rbrakk> \<Longrightarrow> ?x \<notin>\<^sub>\<circ> \<R>\<^sub>\<circ> ?xs

goal (1 subgoal):
 1. x \<notin>\<^sub>\<circ> \<R>\<^sub>\<circ> xs
[PROOF STEP]
using vfsequence_axioms assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>vfsequence ?xs; vdistinct (?xs #\<^sub>\<circ> ?x)\<rbrakk> \<Longrightarrow> ?x \<notin>\<^sub>\<circ> \<R>\<^sub>\<circ> ?xs
vfsequence xs
vdistinct (xs #\<^sub>\<circ> x)

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in vfsequence) vfsequence_v11I[intro]:
  assumes "vdistinct xs"
  shows "v11 xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. v11 xs
[PROOF STEP]
using vfsequence_axioms assms
[PROOF STATE]
proof (prove)
using this:
vfsequence xs
vdistinct xs

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

goal (2 subgoals):
 1. vdistinct []\<^sub>\<circ> \<Longrightarrow> v11 []\<^sub>\<circ>
 2. \<And>xs x. \<lbrakk>vfsequence xs; vdistinct xs \<Longrightarrow> v11 xs; vdistinct (xs #\<^sub>\<circ> x)\<rbrakk> \<Longrightarrow> v11 (xs #\<^sub>\<circ> x)
[PROOF STEP]
interpret vfsequence xs
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vfsequence xs
[PROOF STEP]
by (rule vcons(1))
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. vdistinct []\<^sub>\<circ> \<Longrightarrow> v11 []\<^sub>\<circ>
 2. \<And>xs x. \<lbrakk>vfsequence xs; vdistinct xs \<Longrightarrow> v11 xs; vdistinct (xs #\<^sub>\<circ> x)\<rbrakk> \<Longrightarrow> v11 (xs #\<^sub>\<circ> x)
[PROOF STEP]
from vcons(3)
[PROOF STATE]
proof (chain)
picking this:
vdistinct (xs #\<^sub>\<circ> x)
[PROOF STEP]
have dxs: "vdistinct xs"
[PROOF STATE]
proof (prove)
using this:
vdistinct (xs #\<^sub>\<circ> x)

goal (1 subgoal):
 1. vdistinct xs
[PROOF STEP]
by (rule vfsequence_vcons_vdistinct)
[PROOF STATE]
proof (state)
this:
vdistinct xs

goal (2 subgoals):
 1. vdistinct []\<^sub>\<circ> \<Longrightarrow> v11 []\<^sub>\<circ>
 2. \<And>xs x. \<lbrakk>vfsequence xs; vdistinct xs \<Longrightarrow> v11 xs; vdistinct (xs #\<^sub>\<circ> x)\<rbrakk> \<Longrightarrow> v11 (xs #\<^sub>\<circ> x)
[PROOF STEP]
interpret v11 xs
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. v11 xs
[PROOF STEP]
using dxs
[PROOF STATE]
proof (prove)
using this:
vdistinct xs

goal (1 subgoal):
 1. v11 xs
[PROOF STEP]
by (rule vcons(2))
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. vdistinct []\<^sub>\<circ> \<Longrightarrow> v11 []\<^sub>\<circ>
 2. \<And>xs x. \<lbrakk>vfsequence xs; vdistinct xs \<Longrightarrow> v11 xs; vdistinct (xs #\<^sub>\<circ> x)\<rbrakk> \<Longrightarrow> v11 (xs #\<^sub>\<circ> x)
[PROOF STEP]
from vfsequence_vcons_nin_vrange[OF vcons(3)]
[PROOF STATE]
proof (chain)
picking this:
x \<notin>\<^sub>\<circ> \<R>\<^sub>\<circ> xs
[PROOF STEP]
have "x \<notin>\<^sub>\<circ> \<R>\<^sub>\<circ> xs"
[PROOF STATE]
proof (prove)
using this:
x \<notin>\<^sub>\<circ> \<R>\<^sub>\<circ> xs

goal (1 subgoal):
 1. x \<notin>\<^sub>\<circ> \<R>\<^sub>\<circ> xs
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
x \<notin>\<^sub>\<circ> \<R>\<^sub>\<circ> xs

goal (2 subgoals):
 1. vdistinct []\<^sub>\<circ> \<Longrightarrow> v11 []\<^sub>\<circ>
 2. \<And>xs x. \<lbrakk>vfsequence xs; vdistinct xs \<Longrightarrow> v11 xs; vdistinct (xs #\<^sub>\<circ> x)\<rbrakk> \<Longrightarrow> v11 (xs #\<^sub>\<circ> x)
[PROOF STEP]
show "v11 (xs #\<^sub>\<circ> x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. v11 (xs #\<^sub>\<circ> x)
[PROOF STEP]
by
      (
        simp_all add:
          vcons_def vfsequence_vdomain vfsequence_vcons_nin_vrange[OF vcons(3)]
      )
[PROOF STATE]
proof (state)
this:
v11 (xs #\<^sub>\<circ> x)

goal (1 subgoal):
 1. vdistinct []\<^sub>\<circ> \<Longrightarrow> v11 []\<^sub>\<circ>
[PROOF STEP]
qed simp


[STATEMENT]
lemma (in vfsequence) vfsequence_vcons_vdistinctI:
  assumes "vdistinct xs" and "x \<notin>\<^sub>\<circ> \<R>\<^sub>\<circ> xs"
  shows "vdistinct (xs #\<^sub>\<circ> x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vdistinct (xs #\<^sub>\<circ> x)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. vdistinct (xs #\<^sub>\<circ> x)
[PROOF STEP]
have t: "distinct xs \<Longrightarrow> x \<notin> list.set xs \<Longrightarrow> distinct (x # xs)"
    for x ::V and xs
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>distinct xs; x \<notin> list.set xs\<rbrakk> \<Longrightarrow> distinct (x # xs)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<lbrakk>distinct ?xs; ?x \<notin> list.set ?xs\<rbrakk> \<Longrightarrow> distinct (?x # ?xs)

goal (1 subgoal):
 1. vdistinct (xs #\<^sub>\<circ> x)
[PROOF STEP]
from vfsequence_axioms assms
[PROOF STATE]
proof (chain)
picking this:
vfsequence xs
vdistinct xs
x \<notin>\<^sub>\<circ> \<R>\<^sub>\<circ> xs
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
vfsequence xs
vdistinct xs
x \<notin>\<^sub>\<circ> \<R>\<^sub>\<circ> xs

goal (1 subgoal):
 1. vdistinct (xs #\<^sub>\<circ> x)
[PROOF STEP]
by (rule t[untransferred])
[PROOF STATE]
proof (state)
this:
vdistinct (xs #\<^sub>\<circ> x)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in vfsequence) vfsequence_nin_vrange_vcons:
  assumes "y \<notin>\<^sub>\<circ> \<R>\<^sub>\<circ> xs" and "y \<noteq> x"
  shows "y \<notin>\<^sub>\<circ> \<R>\<^sub>\<circ> (xs #\<^sub>\<circ> x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. y \<notin>\<^sub>\<circ> \<R>\<^sub>\<circ> (xs #\<^sub>\<circ> x)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. y \<notin>\<^sub>\<circ> \<R>\<^sub>\<circ> (xs #\<^sub>\<circ> x)
[PROOF STEP]
have t: "y \<notin> list.set xs \<Longrightarrow> y \<noteq> x \<Longrightarrow> y \<notin> list.set (x # xs)"
    for x y :: V and xs
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>y \<notin> list.set xs; y \<noteq> x\<rbrakk> \<Longrightarrow> y \<notin> list.set (x # xs)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<lbrakk>?y \<notin> list.set ?xs; ?y \<noteq> ?x\<rbrakk> \<Longrightarrow> ?y \<notin> list.set (?x # ?xs)

goal (1 subgoal):
 1. y \<notin>\<^sub>\<circ> \<R>\<^sub>\<circ> (xs #\<^sub>\<circ> x)
[PROOF STEP]
from vfsequence_axioms assms
[PROOF STATE]
proof (chain)
picking this:
vfsequence xs
y \<notin>\<^sub>\<circ> \<R>\<^sub>\<circ> xs
y \<noteq> x
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
vfsequence xs
y \<notin>\<^sub>\<circ> \<R>\<^sub>\<circ> xs
y \<noteq> x

goal (1 subgoal):
 1. y \<notin>\<^sub>\<circ> \<R>\<^sub>\<circ> (xs #\<^sub>\<circ> x)
[PROOF STEP]
by (rule t[untransferred])
[PROOF STATE]
proof (state)
this:
y \<notin>\<^sub>\<circ> \<R>\<^sub>\<circ> (xs #\<^sub>\<circ> x)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma vconcat_transfer[transfer_rule]:
  includes lifting_syntax
  shows "(cr_cr_vfsequence ===> cr_vfsequence) vconcat concat"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (cr_cr_vfsequence ===> cr_vfsequence) vconcat concat
[PROOF STEP]
proof(intro rel_funI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y. cr_cr_vfsequence x y \<Longrightarrow> cr_vfsequence (vconcat x) (concat y)
[PROOF STEP]
fix xs ys
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y. cr_cr_vfsequence x y \<Longrightarrow> cr_vfsequence (vconcat x) (concat y)
[PROOF STEP]
assume "cr_cr_vfsequence xs ys"
[PROOF STATE]
proof (state)
this:
cr_cr_vfsequence xs ys

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

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

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

goal (1 subgoal):
 1. \<And>x y. cr_cr_vfsequence x y \<Longrightarrow> cr_vfsequence (vconcat x) (concat y)
[PROOF STEP]
have main_eq: "map vlist_of_vfsequence (vlist_of_vfsequence xs) = ys"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map vlist_of_vfsequence (vlist_of_vfsequence xs) = ys
[PROOF STEP]
unfolding xs_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map vlist_of_vfsequence (vlist_of_vfsequence (vfsequence_of_vlist (map vfsequence_of_vlist ys))) = ys
[PROOF STEP]
by (simp add: map_idI)
[PROOF STATE]
proof (state)
this:
map vlist_of_vfsequence (vlist_of_vfsequence xs) = ys

goal (1 subgoal):
 1. \<And>x y. cr_cr_vfsequence x y \<Longrightarrow> cr_vfsequence (vconcat x) (concat y)
[PROOF STEP]
show "cr_vfsequence (vconcat xs) (concat ys)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cr_vfsequence (vconcat xs) (concat ys)
[PROOF STEP]
unfolding cr_vfsequence_def vconcat_def main_eq
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vfsequence_of_vlist (concat ys) = vfsequence_of_vlist (concat ys)
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
cr_vfsequence (vconcat xs) (concat ys)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma vconcat_vempty[simp]: "vconcat []\<^sub>\<circ> = []\<^sub>\<circ>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vconcat []\<^sub>\<circ> = []\<^sub>\<circ>
[PROOF STEP]
unfolding vconcat_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vfsequence_of_vlist (concat (map vlist_of_vfsequence (vlist_of_vfsequence []\<^sub>\<circ>))) = []\<^sub>\<circ>
[PROOF STEP]
by simp


[STATEMENT]
lemma vconcat_append[simp]:
  assumes "vfsequence xss"
    and "\<forall>xs\<in>\<^sub>\<circ>\<R>\<^sub>\<circ> xss. vfsequence xs"
    and "vfsequence yss"
    and "\<forall>xs\<in>\<^sub>\<circ>\<R>\<^sub>\<circ> yss. vfsequence xs"
  shows "vconcat (xss @\<^sub>\<circ> yss) = vconcat xss @\<^sub>\<circ> vconcat yss"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vconcat (xss @\<^sub>\<circ> yss) = vconcat xss @\<^sub>\<circ> vconcat yss
[PROOF STEP]
using assms concat_append[where 'a=V, untransferred]
[PROOF STATE]
proof (prove)
using this:
vfsequence xss
\<forall>xs\<in>elts (\<R>\<^sub>\<circ> xss). vfsequence xs
vfsequence yss
\<forall>xs\<in>elts (\<R>\<^sub>\<circ> yss). vfsequence xs
\<lbrakk>vfsequence ?xs \<and> Ball (elts (\<R>\<^sub>\<circ> ?xs)) vfsequence; vfsequence ?ys \<and> Ball (elts (\<R>\<^sub>\<circ> ?ys)) vfsequence\<rbrakk> \<Longrightarrow> vconcat (?ys @\<^sub>\<circ> ?xs) = vconcat ?ys @\<^sub>\<circ> vconcat ?xs

goal (1 subgoal):
 1. vconcat (xss @\<^sub>\<circ> yss) = vconcat xss @\<^sub>\<circ> vconcat yss
[PROOF STEP]
by simp


[STATEMENT]
lemma vconcat_vcons[simp]:
  assumes "vfsequence xs" and "vfsequence xss" and "\<forall>xs\<in>\<^sub>\<circ>\<R>\<^sub>\<circ> xss. vfsequence xs"
  shows "vconcat (xss #\<^sub>\<circ> xs) = vconcat xss @\<^sub>\<circ> xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vconcat (xss #\<^sub>\<circ> xs) = vconcat xss @\<^sub>\<circ> xs
[PROOF STEP]
using assms concat.simps(2)[where 'a=V, untransferred]
[PROOF STATE]
proof (prove)
using this:
vfsequence xs
vfsequence xss
\<forall>xs\<in>elts (\<R>\<^sub>\<circ> xss). vfsequence xs
\<lbrakk>vfsequence ?x; vfsequence ?xs \<and> Ball (elts (\<R>\<^sub>\<circ> ?xs)) vfsequence\<rbrakk> \<Longrightarrow> vconcat (?xs #\<^sub>\<circ> ?x) = vconcat ?xs @\<^sub>\<circ> ?x

goal (1 subgoal):
 1. vconcat (xss #\<^sub>\<circ> xs) = vconcat xss @\<^sub>\<circ> xs
[PROOF STEP]
by simp


[STATEMENT]
lemma (in vfsequence) vfsequence_vconcat_fsingleton[simp]: "vconcat [xs]\<^sub>\<circ> = xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vconcat [xs]\<^sub>\<circ> = xs
[PROOF STEP]
using vfsequence_axioms
[PROOF STATE]
proof (prove)
using this:
vfsequence xs

goal (1 subgoal):
 1. vconcat [xs]\<^sub>\<circ> = xs
[PROOF STEP]
by
    (
      metis
        vfsequence_vappend_vempty_vfsequence
        vconcat_vcons
        vconcat_vempty
        vempty_nin
        vfsequence_vempty
        vrange_vempty
    )


[STATEMENT]
lemma vfsequence_vcons_vproductI[intro!]:
  assumes "n \<in>\<^sub>\<circ> \<omega>"
    and "xs \<in>\<^sub>\<circ> (\<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>vcard xs. A i)"
    and "x \<in>\<^sub>\<circ> A (vcard xs)"
    and "n = vcard (xs #\<^sub>\<circ> x)"
  shows "xs #\<^sub>\<circ> x \<in>\<^sub>\<circ> (\<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>n. A i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. xs #\<^sub>\<circ> x \<in>\<^sub>\<circ> vproduct n A
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. vsv (xs #\<^sub>\<circ> x)
 2. \<D>\<^sub>\<circ> (xs #\<^sub>\<circ> x) = n
 3. \<forall>i\<in>elts n. (xs #\<^sub>\<circ> x)\<lparr>i\<rparr> \<in>\<^sub>\<circ> A i
[PROOF STEP]
interpret xs: vfsequence xs
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vfsequence xs
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
n \<in>\<^sub>\<circ> \<omega>
xs \<in>\<^sub>\<circ> vproduct (vcard xs) A
x \<in>\<^sub>\<circ> A (vcard xs)
n = vcard (xs #\<^sub>\<circ> x)

goal (1 subgoal):
 1. vfsequence xs
[PROOF STEP]
apply(intro vfsequenceI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>n \<in>\<^sub>\<circ> \<omega>; xs \<in>\<^sub>\<circ> vproduct (vcard xs) A; x \<in>\<^sub>\<circ> A (vcard xs); n = vcard (xs #\<^sub>\<circ> x)\<rbrakk> \<Longrightarrow> vsv xs
 2. \<lbrakk>n \<in>\<^sub>\<circ> \<omega>; xs \<in>\<^sub>\<circ> vproduct (vcard xs) A; x \<in>\<^sub>\<circ> A (vcard xs); n = vcard (xs #\<^sub>\<circ> x)\<rbrakk> \<Longrightarrow> \<D>\<^sub>\<circ> xs \<in>\<^sub>\<circ> \<omega>
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n \<in>\<^sub>\<circ> \<omega>; xs \<in>\<^sub>\<circ> vproduct (vcard xs) A; x \<in>\<^sub>\<circ> A (vcard xs); n = vcard (xs #\<^sub>\<circ> x)\<rbrakk> \<Longrightarrow> vsv xs
[PROOF STEP]
by auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n \<in>\<^sub>\<circ> \<omega>; xs \<in>\<^sub>\<circ> vproduct (vcard xs) A; x \<in>\<^sub>\<circ> A (vcard xs); n = vcard (xs #\<^sub>\<circ> x)\<rbrakk> \<Longrightarrow> \<D>\<^sub>\<circ> xs \<in>\<^sub>\<circ> \<omega>
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n \<in>\<^sub>\<circ> \<omega>; xs \<in>\<^sub>\<circ> vproduct (vcard xs) A; x \<in>\<^sub>\<circ> A (vcard xs); n = vcard (xs #\<^sub>\<circ> x)\<rbrakk> \<Longrightarrow> \<D>\<^sub>\<circ> xs \<in>\<^sub>\<circ> \<omega>
[PROOF STEP]
by
        (
          metis
            vcard_vfinite_omega
            vcons_vsubset
            vfinite_vcard_omega
            vfinite_vsubset vproductD(2)
        )
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. vsv (xs #\<^sub>\<circ> x)
 2. \<D>\<^sub>\<circ> (xs #\<^sub>\<circ> x) = n
 3. \<forall>i\<in>elts n. (xs #\<^sub>\<circ> x)\<lparr>i\<rparr> \<in>\<^sub>\<circ> A i
[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 auto
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. vsv (xs #\<^sub>\<circ> x)
 2. \<D>\<^sub>\<circ> (xs #\<^sub>\<circ> x) = n
 3. \<forall>i\<in>elts n. (xs #\<^sub>\<circ> x)\<lparr>i\<rparr> \<in>\<^sub>\<circ> A i
[PROOF STEP]
show "vsv (xs #\<^sub>\<circ> x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vsv (xs #\<^sub>\<circ> x)
[PROOF STEP]
by (simp add: xsx.vsv_axioms)
[PROOF STATE]
proof (state)
this:
vsv (xs #\<^sub>\<circ> x)

goal (2 subgoals):
 1. \<D>\<^sub>\<circ> (xs #\<^sub>\<circ> x) = n
 2. \<forall>i\<in>elts n. (xs #\<^sub>\<circ> x)\<lparr>i\<rparr> \<in>\<^sub>\<circ> A i
[PROOF STEP]
show D: "\<D>\<^sub>\<circ> (xs #\<^sub>\<circ> x) = n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<D>\<^sub>\<circ> (xs #\<^sub>\<circ> x) = n
[PROOF STEP]
unfolding assms(4) xsx.vfsequence_vdomain
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vcard (xs #\<^sub>\<circ> x) = vcard (xs #\<^sub>\<circ> x)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<D>\<^sub>\<circ> (xs #\<^sub>\<circ> x) = n

goal (1 subgoal):
 1. \<forall>i\<in>elts n. (xs #\<^sub>\<circ> x)\<lparr>i\<rparr> \<in>\<^sub>\<circ> A i
[PROOF STEP]
from vproductD[OF assms(2)]
[PROOF STATE]
proof (chain)
picking this:
vsv xs
\<D>\<^sub>\<circ> xs = vcard xs
\<forall>i\<in>elts (vcard xs). xs\<lparr>i\<rparr> \<in>\<^sub>\<circ> A i
[PROOF STEP]
have elem: "i \<in>\<^sub>\<circ> vcard xs \<Longrightarrow> xs\<lparr>i\<rparr> \<in>\<^sub>\<circ> A i" for i
[PROOF STATE]
proof (prove)
using this:
vsv xs
\<D>\<^sub>\<circ> xs = vcard xs
\<forall>i\<in>elts (vcard xs). xs\<lparr>i\<rparr> \<in>\<^sub>\<circ> A i

goal (1 subgoal):
 1. i \<in>\<^sub>\<circ> vcard xs \<Longrightarrow> xs\<lparr>i\<rparr> \<in>\<^sub>\<circ> A i
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
?i \<in>\<^sub>\<circ> vcard xs \<Longrightarrow> xs\<lparr>?i\<rparr> \<in>\<^sub>\<circ> A ?i

goal (1 subgoal):
 1. \<forall>i\<in>elts n. (xs #\<^sub>\<circ> x)\<lparr>i\<rparr> \<in>\<^sub>\<circ> A i
[PROOF STEP]
show "\<forall>i\<in>\<^sub>\<circ>n. (xs #\<^sub>\<circ> x)\<lparr>i\<rparr> \<in>\<^sub>\<circ> A i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>i\<in>elts n. (xs #\<^sub>\<circ> x)\<lparr>i\<rparr> \<in>\<^sub>\<circ> A i
[PROOF STEP]
by (auto simp: elem assms(3,4))
[PROOF STATE]
proof (state)
this:
\<forall>i\<in>elts n. (xs #\<^sub>\<circ> x)\<lparr>i\<rparr> \<in>\<^sub>\<circ> A i

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma vfsequence_vcons_vproductD[dest]:
  assumes "xs #\<^sub>\<circ> x \<in>\<^sub>\<circ> (\<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>n. A i)" and "n \<in>\<^sub>\<circ> \<omega>"
  shows "xs \<in>\<^sub>\<circ> (\<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>vcard xs. A i)"
    and "x \<in>\<^sub>\<circ> A (vcard xs)"
    and "n = vcard (xs #\<^sub>\<circ> x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. xs \<in>\<^sub>\<circ> vproduct (vcard xs) A &&& x \<in>\<^sub>\<circ> A (vcard xs) &&& n = vcard (xs #\<^sub>\<circ> x)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. xs \<in>\<^sub>\<circ> vproduct (vcard xs) A
 2. x \<in>\<^sub>\<circ> A (vcard xs)
 3. n = vcard (xs #\<^sub>\<circ> x)
[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 (meson assms succ_in_omega vfsequence_vproduct)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. xs \<in>\<^sub>\<circ> vproduct (vcard xs) A
 2. x \<in>\<^sub>\<circ> A (vcard xs)
 3. n = vcard (xs #\<^sub>\<circ> x)
[PROOF STEP]
interpret xs: vfsequence xs
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vfsequence xs
[PROOF STEP]
by (blast intro: xsx.vfsequence_vremove_vcons_vfsequence)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. xs \<in>\<^sub>\<circ> vproduct (vcard xs) A
 2. x \<in>\<^sub>\<circ> A (vcard xs)
 3. n = vcard (xs #\<^sub>\<circ> x)
[PROOF STEP]
show n_def: "n = vcard (xs #\<^sub>\<circ> x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n = vcard (xs #\<^sub>\<circ> x)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
xs #\<^sub>\<circ> x \<in>\<^sub>\<circ> vproduct n A
n \<in>\<^sub>\<circ> \<omega>

goal (1 subgoal):
 1. n = vcard (xs #\<^sub>\<circ> x)
[PROOF STEP]
using xsx.vfsequence_vdomain
[PROOF STATE]
proof (prove)
using this:
xs #\<^sub>\<circ> x \<in>\<^sub>\<circ> vproduct n A
n \<in>\<^sub>\<circ> \<omega>
\<D>\<^sub>\<circ> (xs #\<^sub>\<circ> x) = vcard (xs #\<^sub>\<circ> x)

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

goal (2 subgoals):
 1. xs \<in>\<^sub>\<circ> vproduct (vcard xs) A
 2. x \<in>\<^sub>\<circ> A (vcard xs)
[PROOF STEP]
from vproductD[OF assms(1), unfolded n_def]
[PROOF STATE]
proof (chain)
picking this:
vsv (xs #\<^sub>\<circ> x)
\<D>\<^sub>\<circ> (xs #\<^sub>\<circ> x) = vcard (xs #\<^sub>\<circ> x)
\<forall>i\<in>elts (vcard (xs #\<^sub>\<circ> x)). (xs #\<^sub>\<circ> x)\<lparr>i\<rparr> \<in>\<^sub>\<circ> A i
[PROOF STEP]
have elem_xs_x: "i \<in>\<^sub>\<circ> vcard (xs #\<^sub>\<circ> x) \<Longrightarrow> (xs #\<^sub>\<circ> x)\<lparr>i\<rparr> \<in>\<^sub>\<circ> A i"
    for i
[PROOF STATE]
proof (prove)
using this:
vsv (xs #\<^sub>\<circ> x)
\<D>\<^sub>\<circ> (xs #\<^sub>\<circ> x) = vcard (xs #\<^sub>\<circ> x)
\<forall>i\<in>elts (vcard (xs #\<^sub>\<circ> x)). (xs #\<^sub>\<circ> x)\<lparr>i\<rparr> \<in>\<^sub>\<circ> A i

goal (1 subgoal):
 1. i \<in>\<^sub>\<circ> vcard (xs #\<^sub>\<circ> x) \<Longrightarrow> (xs #\<^sub>\<circ> x)\<lparr>i\<rparr> \<in>\<^sub>\<circ> A i
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
?i \<in>\<^sub>\<circ> vcard (xs #\<^sub>\<circ> x) \<Longrightarrow> (xs #\<^sub>\<circ> x)\<lparr>?i\<rparr> \<in>\<^sub>\<circ> A ?i

goal (2 subgoals):
 1. xs \<in>\<^sub>\<circ> vproduct (vcard xs) A
 2. x \<in>\<^sub>\<circ> A (vcard xs)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
?i \<in>\<^sub>\<circ> vcard (xs #\<^sub>\<circ> x) \<Longrightarrow> (xs #\<^sub>\<circ> x)\<lparr>?i\<rparr> \<in>\<^sub>\<circ> A ?i
[PROOF STEP]
have elem_xs[simp]: "i \<in>\<^sub>\<circ> vcard xs \<Longrightarrow> xs\<lparr>i\<rparr> \<in>\<^sub>\<circ> A i" for i
[PROOF STATE]
proof (prove)
using this:
?i \<in>\<^sub>\<circ> vcard (xs #\<^sub>\<circ> x) \<Longrightarrow> (xs #\<^sub>\<circ> x)\<lparr>?i\<rparr> \<in>\<^sub>\<circ> A ?i

goal (1 subgoal):
 1. i \<in>\<^sub>\<circ> vcard xs \<Longrightarrow> xs\<lparr>i\<rparr> \<in>\<^sub>\<circ> A i
[PROOF STEP]
by (metis rev_vsubsetD vcard_mono vcons_vsubset xs.vfsequence_at_not_last)
[PROOF STATE]
proof (state)
this:
?i \<in>\<^sub>\<circ> vcard xs \<Longrightarrow> xs\<lparr>?i\<rparr> \<in>\<^sub>\<circ> A ?i

goal (2 subgoals):
 1. xs \<in>\<^sub>\<circ> vproduct (vcard xs) A
 2. x \<in>\<^sub>\<circ> A (vcard xs)
[PROOF STEP]
show "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]
by (auto simp: xs.vsv_axioms xs.vfsequence_vdomain)
[PROOF STATE]
proof (state)
this:
xs \<in>\<^sub>\<circ> vproduct (vcard xs) A

goal (1 subgoal):
 1. x \<in>\<^sub>\<circ> A (vcard xs)
[PROOF STEP]
from elem_xs_x
[PROOF STATE]
proof (chain)
picking this:
?i \<in>\<^sub>\<circ> vcard (xs #\<^sub>\<circ> x) \<Longrightarrow> (xs #\<^sub>\<circ> x)\<lparr>?i\<rparr> \<in>\<^sub>\<circ> A ?i
[PROOF STEP]
show "x \<in>\<^sub>\<circ> A (vcard xs)"
[PROOF STATE]
proof (prove)
using this:
?i \<in>\<^sub>\<circ> vcard (xs #\<^sub>\<circ> x) \<Longrightarrow> (xs #\<^sub>\<circ> x)\<lparr>?i\<rparr> \<in>\<^sub>\<circ> A ?i

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma vfsequence_vcons_vproductE[elim!]:
  assumes "xs #\<^sub>\<circ> x \<in>\<^sub>\<circ> (\<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>n. A i)" and "n \<in>\<^sub>\<circ> \<omega>"
  obtains "xs \<in>\<^sub>\<circ> (\<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>vcard xs. A i)"
    and "x \<in>\<^sub>\<circ> A (vcard xs)"
    and "n = vcard (xs #\<^sub>\<circ> x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lbrakk>xs \<in>\<^sub>\<circ> vproduct (vcard xs) A; x \<in>\<^sub>\<circ> A (vcard xs); n = vcard (xs #\<^sub>\<circ> x)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
xs #\<^sub>\<circ> x \<in>\<^sub>\<circ> vproduct n A
n \<in>\<^sub>\<circ> \<omega>

goal (1 subgoal):
 1. (\<lbrakk>xs \<in>\<^sub>\<circ> vproduct (vcard xs) A; x \<in>\<^sub>\<circ> A (vcard xs); n = vcard (xs #\<^sub>\<circ> x)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp: vfsequence_vcons_vproductD)


[STATEMENT]
lemma small_fpairs[simp]: "small {[a, b]\<^sub>\<circ> | a b. [a, b]\<^sub>\<circ> \<in>\<^sub>\<circ> r}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. small {[a, b]\<^sub>\<circ> |a b. [a, b]\<^sub>\<circ> \<in>\<^sub>\<circ> r}
[PROOF STEP]
by (rule down[of _ r]) clarsimp


[STATEMENT]
lemma ftimesI1[intro]:
  assumes "x = [a, b]\<^sub>\<circ>" and "a \<in>\<^sub>\<circ> A" and "b \<in>\<^sub>\<circ> B"
  shows "x \<in>\<^sub>\<circ> A \<times>\<^sub>\<bullet> B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in>\<^sub>\<circ> A \<times>\<^sub>\<bullet> B
[PROOF STEP]
unfolding ftimes_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in>\<^sub>\<circ> (\<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>2\<^sub>\<nat>. if i = []\<^sub>\<circ> \<Rightarrow> A | otherwise \<Rightarrow> B)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. vsv x
 2. \<D>\<^sub>\<circ> x = 2\<^sub>\<nat>
 3. \<forall>i\<in>elts (2\<^sub>\<nat>). x\<lparr>i\<rparr> \<in>\<^sub>\<circ> (if i = []\<^sub>\<circ> \<Rightarrow> A | otherwise \<Rightarrow> B)
[PROOF STEP]
show vsv: "vsv x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vsv x
[PROOF STEP]
by (simp add: assms(1) vfsequence.axioms(1))
[PROOF STATE]
proof (state)
this:
vsv x

goal (2 subgoals):
 1. \<D>\<^sub>\<circ> x = 2\<^sub>\<nat>
 2. \<forall>i\<in>elts (2\<^sub>\<nat>). x\<lparr>i\<rparr> \<in>\<^sub>\<circ> (if i = []\<^sub>\<circ> \<Rightarrow> A | otherwise \<Rightarrow> B)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
vsv x
[PROOF STEP]
interpret vsv x
[PROOF STATE]
proof (prove)
using this:
vsv x

goal (1 subgoal):
 1. vsv x
[PROOF STEP]
.
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<D>\<^sub>\<circ> x = 2\<^sub>\<nat>
 2. \<forall>i\<in>elts (2\<^sub>\<nat>). x\<lparr>i\<rparr> \<in>\<^sub>\<circ> (if i = []\<^sub>\<circ> \<Rightarrow> A | otherwise \<Rightarrow> B)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
x = [a, b]\<^sub>\<circ>
a \<in>\<^sub>\<circ> A
b \<in>\<^sub>\<circ> B
[PROOF STEP]
show D: "\<D>\<^sub>\<circ> x = 2\<^sub>\<nat>"
[PROOF STATE]
proof (prove)
using this:
x = [a, b]\<^sub>\<circ>
a \<in>\<^sub>\<circ> A
b \<in>\<^sub>\<circ> B

goal (1 subgoal):
 1. \<D>\<^sub>\<circ> x = 2\<^sub>\<nat>
[PROOF STEP]
unfolding nat_omega_simps two One_nat_def
[PROOF STATE]
proof (prove)
using this:
x = [a, b]\<^sub>\<circ>
a \<in>\<^sub>\<circ> A
b \<in>\<^sub>\<circ> B

goal (1 subgoal):
 1. \<D>\<^sub>\<circ> x = set {[]\<^sub>\<circ>, Suc 0\<^sub>\<nat>}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<D>\<^sub>\<circ> x = 2\<^sub>\<nat>

goal (1 subgoal):
 1. \<forall>i\<in>elts (2\<^sub>\<nat>). x\<lparr>i\<rparr> \<in>\<^sub>\<circ> (if i = []\<^sub>\<circ> \<Rightarrow> A | otherwise \<Rightarrow> B)
[PROOF STEP]
from assms(2,3)
[PROOF STATE]
proof (chain)
picking this:
a \<in>\<^sub>\<circ> A
b \<in>\<^sub>\<circ> B
[PROOF STEP]
have i: "i \<in>\<^sub>\<circ> 2\<^sub>\<nat> \<Longrightarrow> x\<lparr>i\<rparr> \<in>\<^sub>\<circ> (if i = 0\<^sub>\<nat> then A else B)"
    for i
[PROOF STATE]
proof (prove)
using this:
a \<in>\<^sub>\<circ> A
b \<in>\<^sub>\<circ> B

goal (1 subgoal):
 1. i \<in>\<^sub>\<circ> 2\<^sub>\<nat> \<Longrightarrow> x\<lparr>i\<rparr> \<in>\<^sub>\<circ> (if i = 0\<^sub>\<nat> \<Rightarrow> A | otherwise \<Rightarrow> B)
[PROOF STEP]
unfolding assms(1) two nat_omega_simps One_nat_def
[PROOF STATE]
proof (prove)
using this:
a \<in>\<^sub>\<circ> A
b \<in>\<^sub>\<circ> B

goal (1 subgoal):
 1. i \<in>\<^sub>\<circ> set {[]\<^sub>\<circ>, Suc 0\<^sub>\<nat>} \<Longrightarrow> [a, b]\<^sub>\<circ>\<lparr>i\<rparr> \<in>\<^sub>\<circ> (if i = 0\<^sub>\<nat> \<Rightarrow> A | otherwise \<Rightarrow> B)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
?i \<in>\<^sub>\<circ> 2\<^sub>\<nat> \<Longrightarrow> x\<lparr>?i\<rparr> \<in>\<^sub>\<circ> (if ?i = 0\<^sub>\<nat> \<Rightarrow> A | otherwise \<Rightarrow> B)

goal (1 subgoal):
 1. \<forall>i\<in>elts (2\<^sub>\<nat>). x\<lparr>i\<rparr> \<in>\<^sub>\<circ> (if i = []\<^sub>\<circ> \<Rightarrow> A | otherwise \<Rightarrow> B)
[PROOF STEP]
from i
[PROOF STATE]
proof (chain)
picking this:
?i \<in>\<^sub>\<circ> 2\<^sub>\<nat> \<Longrightarrow> x\<lparr>?i\<rparr> \<in>\<^sub>\<circ> (if ?i = 0\<^sub>\<nat> \<Rightarrow> A | otherwise \<Rightarrow> B)
[PROOF STEP]
show "\<forall>i\<in>\<^sub>\<circ>2\<^sub>\<nat>. x\<lparr>i\<rparr> \<in>\<^sub>\<circ> (if i = 0 then A else B)"
[PROOF STATE]
proof (prove)
using this:
?i \<in>\<^sub>\<circ> 2\<^sub>\<nat> \<Longrightarrow> x\<lparr>?i\<rparr> \<in>\<^sub>\<circ> (if ?i = 0\<^sub>\<nat> \<Rightarrow> A | otherwise \<Rightarrow> B)

goal (1 subgoal):
 1. \<forall>i\<in>elts (2\<^sub>\<nat>). x\<lparr>i\<rparr> \<in>\<^sub>\<circ> (if i = []\<^sub>\<circ> \<Rightarrow> A | otherwise \<Rightarrow> B)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>i\<in>elts (2\<^sub>\<nat>). x\<lparr>i\<rparr> \<in>\<^sub>\<circ> (if i = []\<^sub>\<circ> \<Rightarrow> A | otherwise \<Rightarrow> B)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ftimesI2[intro!]:
  assumes "a \<in>\<^sub>\<circ> A" and "b \<in>\<^sub>\<circ> B"
  shows "[a, b]\<^sub>\<circ> \<in>\<^sub>\<circ> A \<times>\<^sub>\<bullet> B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [a, b]\<^sub>\<circ> \<in>\<^sub>\<circ> A \<times>\<^sub>\<bullet> B
[PROOF STEP]
using assms ftimesI1
[PROOF STATE]
proof (prove)
using this:
a \<in>\<^sub>\<circ> A
b \<in>\<^sub>\<circ> B
\<lbrakk>?x = [?a, ?b]\<^sub>\<circ>; ?a \<in>\<^sub>\<circ> ?A; ?b \<in>\<^sub>\<circ> ?B\<rbrakk> \<Longrightarrow> ?x \<in>\<^sub>\<circ> ?A \<times>\<^sub>\<bullet> ?B

goal (1 subgoal):
 1. [a, b]\<^sub>\<circ> \<in>\<^sub>\<circ> A \<times>\<^sub>\<bullet> B
[PROOF STEP]
by auto


[STATEMENT]
lemma fproductE1[elim!]:
  assumes "x \<in>\<^sub>\<circ> A \<times>\<^sub>\<bullet> B"
  obtains a b where "x = [a, b]\<^sub>\<circ>" and "a \<in>\<^sub>\<circ> A" and "b \<in>\<^sub>\<circ> B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>a b. \<lbrakk>x = [a, b]\<^sub>\<circ>; a \<in>\<^sub>\<circ> A; b \<in>\<^sub>\<circ> B\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>a b. \<lbrakk>x = [a, b]\<^sub>\<circ>; a \<in>\<^sub>\<circ> A; b \<in>\<^sub>\<circ> B\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from vproduct_vdoubletonD[OF assms[unfolded two ftimes_def]]
[PROOF STATE]
proof (chain)
picking this:
vsv x
x\<lparr>[]\<^sub>\<circ>\<rparr> \<in>\<^sub>\<circ> (if []\<^sub>\<circ> = []\<^sub>\<circ> \<Rightarrow> A | otherwise \<Rightarrow> B)
x\<lparr>1\<^sub>\<nat>\<rparr> \<in>\<^sub>\<circ> (if 1\<^sub>\<nat> = []\<^sub>\<circ> \<Rightarrow> A | otherwise \<Rightarrow> B)
\<D>\<^sub>\<circ> x = set {[]\<^sub>\<circ>, 1\<^sub>\<nat>}
x = set {\<langle>[]\<^sub>\<circ>, x\<lparr>[]\<^sub>\<circ>\<rparr>\<rangle>, \<langle>1\<^sub>\<nat>, x\<lparr>1\<^sub>\<nat>\<rparr>\<rangle>}
[PROOF STEP]
have x_def: "x = set {\<langle>0\<^sub>\<nat>, x\<lparr>0\<^sub>\<nat>\<rparr>\<rangle>, \<langle>1\<^sub>\<nat>, x\<lparr>1\<^sub>\<nat>\<rparr>\<rangle>}"
    and "x\<lparr>0\<^sub>\<nat>\<rparr> \<in>\<^sub>\<circ> A"
    and "x\<lparr>1\<^sub>\<nat>\<rparr> \<in>\<^sub>\<circ> B"
[PROOF STATE]
proof (prove)
using this:
vsv x
x\<lparr>[]\<^sub>\<circ>\<rparr> \<in>\<^sub>\<circ> (if []\<^sub>\<circ> = []\<^sub>\<circ> \<Rightarrow> A | otherwise \<Rightarrow> B)
x\<lparr>1\<^sub>\<nat>\<rparr> \<in>\<^sub>\<circ> (if 1\<^sub>\<nat> = []\<^sub>\<circ> \<Rightarrow> A | otherwise \<Rightarrow> B)
\<D>\<^sub>\<circ> x = set {[]\<^sub>\<circ>, 1\<^sub>\<nat>}
x = set {\<langle>[]\<^sub>\<circ>, x\<lparr>[]\<^sub>\<circ>\<rparr>\<rangle>, \<langle>1\<^sub>\<nat>, x\<lparr>1\<^sub>\<nat>\<rparr>\<rangle>}

goal (1 subgoal):
 1. x = set {\<langle>0\<^sub>\<nat>, x\<lparr>0\<^sub>\<nat>\<rparr>\<rangle>, \<langle>1\<^sub>\<nat>, x\<lparr>1\<^sub>\<nat>\<rparr>\<rangle>} &&& x\<lparr>0\<^sub>\<nat>\<rparr> \<in>\<^sub>\<circ> A &&& x\<lparr>1\<^sub>\<nat>\<rparr> \<in>\<^sub>\<circ> B
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x = set {\<langle>0\<^sub>\<nat>, x\<lparr>0\<^sub>\<nat>\<rparr>\<rangle>, \<langle>1\<^sub>\<nat>, x\<lparr>1\<^sub>\<nat>\<rparr>\<rangle>}
x\<lparr>0\<^sub>\<nat>\<rparr> \<in>\<^sub>\<circ> A
x\<lparr>1\<^sub>\<nat>\<rparr> \<in>\<^sub>\<circ> B

goal (1 subgoal):
 1. (\<And>a b. \<lbrakk>x = [a, b]\<^sub>\<circ>; a \<in>\<^sub>\<circ> A; b \<in>\<^sub>\<circ> B\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x = set {\<langle>0\<^sub>\<nat>, x\<lparr>0\<^sub>\<nat>\<rparr>\<rangle>, \<langle>1\<^sub>\<nat>, x\<lparr>1\<^sub>\<nat>\<rparr>\<rangle>}
x\<lparr>0\<^sub>\<nat>\<rparr> \<in>\<^sub>\<circ> A
x\<lparr>1\<^sub>\<nat>\<rparr> \<in>\<^sub>\<circ> B
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
x = set {\<langle>0\<^sub>\<nat>, x\<lparr>0\<^sub>\<nat>\<rparr>\<rangle>, \<langle>1\<^sub>\<nat>, x\<lparr>1\<^sub>\<nat>\<rparr>\<rangle>}
x\<lparr>0\<^sub>\<nat>\<rparr> \<in>\<^sub>\<circ> A
x\<lparr>1\<^sub>\<nat>\<rparr> \<in>\<^sub>\<circ> B

goal (1 subgoal):
 1. thesis
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
x = set {\<langle>0\<^sub>\<nat>, x\<lparr>0\<^sub>\<nat>\<rparr>\<rangle>, \<langle>1\<^sub>\<nat>, x\<lparr>1\<^sub>\<nat>\<rparr>\<rangle>}
x\<lparr>0\<^sub>\<nat>\<rparr> \<in>\<^sub>\<circ> A
x\<lparr>1\<^sub>\<nat>\<rparr> \<in>\<^sub>\<circ> B
\<lbrakk>x = [?a, ?b]\<^sub>\<circ>; ?a \<in>\<^sub>\<circ> A; ?b \<in>\<^sub>\<circ> B\<rbrakk> \<Longrightarrow> thesis

goal (1 subgoal):
 1. thesis
[PROOF STEP]
using vcons_vdoubleton
[PROOF STATE]
proof (prove)
using this:
x = set {\<langle>0\<^sub>\<nat>, x\<lparr>0\<^sub>\<nat>\<rparr>\<rangle>, \<langle>1\<^sub>\<nat>, x\<lparr>1\<^sub>\<nat>\<rparr>\<rangle>}
x\<lparr>0\<^sub>\<nat>\<rparr> \<in>\<^sub>\<circ> A
x\<lparr>1\<^sub>\<nat>\<rparr> \<in>\<^sub>\<circ> B
\<lbrakk>x = [?a, ?b]\<^sub>\<circ>; ?a \<in>\<^sub>\<circ> A; ?b \<in>\<^sub>\<circ> B\<rbrakk> \<Longrightarrow> thesis
[?a, ?b]\<^sub>\<circ> = set {\<langle>0\<^sub>\<nat>, ?a\<rangle>, \<langle>1\<^sub>\<nat>, ?b\<rangle>}

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma fproductE2[elim!]:
  assumes "[a, b]\<^sub>\<circ> \<in>\<^sub>\<circ> A \<times>\<^sub>\<bullet> B" obtains "a \<in>\<^sub>\<circ> A" and "b \<in>\<^sub>\<circ> B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lbrakk>a \<in>\<^sub>\<circ> A; b \<in>\<^sub>\<circ> B\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
[a, b]\<^sub>\<circ> \<in>\<^sub>\<circ> A \<times>\<^sub>\<bullet> B

goal (1 subgoal):
 1. (\<lbrakk>a \<in>\<^sub>\<circ> A; b \<in>\<^sub>\<circ> B\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast


[STATEMENT]
lemma vfinite_0_left[simp]: "0 \<times>\<^sub>\<bullet> b = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. []\<^sub>\<circ> \<times>\<^sub>\<bullet> b = []\<^sub>\<circ>
[PROOF STEP]
by (meson eq0_iff fproductE1)


[STATEMENT]
lemma vfinite_0_right[simp]: "a \<times>\<^sub>\<bullet> 0 = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<times>\<^sub>\<bullet> []\<^sub>\<circ> = []\<^sub>\<circ>
[PROOF STEP]
by (meson eq0_iff fproductE1)


[STATEMENT]
lemma fproduct_vintersection: "(a \<inter>\<^sub>\<circ> b) \<times>\<^sub>\<bullet> (c \<inter>\<^sub>\<circ> d) = (a \<times>\<^sub>\<bullet> c) \<inter>\<^sub>\<circ> (b \<times>\<^sub>\<bullet> d)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (a \<inter>\<^sub>\<circ> b) \<times>\<^sub>\<bullet> (c \<inter>\<^sub>\<circ> d) = a \<times>\<^sub>\<bullet> c \<inter>\<^sub>\<circ> b \<times>\<^sub>\<bullet> d
[PROOF STEP]
by auto


[STATEMENT]
lemma fproduct_vdiff: "a \<times>\<^sub>\<bullet> (b -\<^sub>\<circ> c) = (a \<times>\<^sub>\<bullet> b) -\<^sub>\<circ> (a \<times>\<^sub>\<bullet> c)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<times>\<^sub>\<bullet> (b -\<^sub>\<circ> c) = a \<times>\<^sub>\<bullet> b -\<^sub>\<circ> a \<times>\<^sub>\<bullet> c
[PROOF STEP]
by auto


[STATEMENT]
lemma vfinite_ftimesI[intro!]:
  assumes "vfinite a" and "vfinite b"
  shows "vfinite (a \<times>\<^sub>\<bullet> b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vfinite (a \<times>\<^sub>\<bullet> b)
[PROOF STEP]
using assms(1,2)
[PROOF STATE]
proof (prove)
using this:
vfinite a
vfinite b

goal (1 subgoal):
 1. vfinite (a \<times>\<^sub>\<bullet> b)
[PROOF STEP]
proof(induction arbitrary: b rule: vfinite_induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>b. vfinite b \<Longrightarrow> vfinite ([]\<^sub>\<circ> \<times>\<^sub>\<bullet> b)
 2. \<And>x F b. \<lbrakk>vfinite F; x \<notin>\<^sub>\<circ> F; \<And>b. vfinite b \<Longrightarrow> vfinite (F \<times>\<^sub>\<bullet> b); vfinite b\<rbrakk> \<Longrightarrow> vfinite (vinsert x F \<times>\<^sub>\<bullet> b)
[PROOF STEP]
case (vinsert x a')
[PROOF STATE]
proof (state)
this:
vfinite a'
x \<notin>\<^sub>\<circ> a'
vfinite ?b \<Longrightarrow> vfinite (a' \<times>\<^sub>\<bullet> ?b)
vfinite b

goal (2 subgoals):
 1. \<And>b. vfinite b \<Longrightarrow> vfinite ([]\<^sub>\<circ> \<times>\<^sub>\<bullet> b)
 2. \<And>x F b. \<lbrakk>vfinite F; x \<notin>\<^sub>\<circ> F; \<And>b. vfinite b \<Longrightarrow> vfinite (F \<times>\<^sub>\<bullet> b); vfinite b\<rbrakk> \<Longrightarrow> vfinite (vinsert x F \<times>\<^sub>\<bullet> b)
[PROOF STEP]
from vinsert(4)
[PROOF STATE]
proof (chain)
picking this:
vfinite b
[PROOF STEP]
have "vfinite (set {x} \<times>\<^sub>\<bullet> b)"
[PROOF STATE]
proof (prove)
using this:
vfinite b

goal (1 subgoal):
 1. vfinite (set {x} \<times>\<^sub>\<bullet> b)
[PROOF STEP]
proof(induction rule: vfinite_induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. vfinite (set {x} \<times>\<^sub>\<bullet> []\<^sub>\<circ>)
 2. \<And>xa F. \<lbrakk>vfinite F; xa \<notin>\<^sub>\<circ> F; vfinite (set {x} \<times>\<^sub>\<bullet> F)\<rbrakk> \<Longrightarrow> vfinite (set {x} \<times>\<^sub>\<bullet> vinsert xa F)
[PROOF STEP]
case (vinsert y b')
[PROOF STATE]
proof (state)
this:
vfinite b'
y \<notin>\<^sub>\<circ> b'
vfinite (set {x} \<times>\<^sub>\<bullet> b')

goal (2 subgoals):
 1. vfinite (set {x} \<times>\<^sub>\<bullet> []\<^sub>\<circ>)
 2. \<And>xa F. \<lbrakk>vfinite F; xa \<notin>\<^sub>\<circ> F; vfinite (set {x} \<times>\<^sub>\<bullet> F)\<rbrakk> \<Longrightarrow> vfinite (set {x} \<times>\<^sub>\<bullet> vinsert xa F)
[PROOF STEP]
have "set {x} \<times>\<^sub>\<bullet> vinsert y b' = vinsert [x, y]\<^sub>\<circ> (set {x} \<times>\<^sub>\<bullet> b')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set {x} \<times>\<^sub>\<bullet> vinsert y b' = vinsert [x, y]\<^sub>\<circ> (set {x} \<times>\<^sub>\<bullet> b')
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
set {x} \<times>\<^sub>\<bullet> vinsert y b' = vinsert [x, y]\<^sub>\<circ> (set {x} \<times>\<^sub>\<bullet> b')

goal (2 subgoals):
 1. vfinite (set {x} \<times>\<^sub>\<bullet> []\<^sub>\<circ>)
 2. \<And>xa F. \<lbrakk>vfinite F; xa \<notin>\<^sub>\<circ> F; vfinite (set {x} \<times>\<^sub>\<bullet> F)\<rbrakk> \<Longrightarrow> vfinite (set {x} \<times>\<^sub>\<bullet> vinsert xa F)
[PROOF STEP]
with vinsert(3)
[PROOF STATE]
proof (chain)
picking this:
vfinite (set {x} \<times>\<^sub>\<bullet> b')
set {x} \<times>\<^sub>\<bullet> vinsert y b' = vinsert [x, y]\<^sub>\<circ> (set {x} \<times>\<^sub>\<bullet> b')
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
vfinite (set {x} \<times>\<^sub>\<bullet> b')
set {x} \<times>\<^sub>\<bullet> vinsert y b' = vinsert [x, y]\<^sub>\<circ> (set {x} \<times>\<^sub>\<bullet> b')

goal (1 subgoal):
 1. vfinite (set {x} \<times>\<^sub>\<bullet> vinsert y b')
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
vfinite (set {x} \<times>\<^sub>\<bullet> vinsert y b')

goal (1 subgoal):
 1. vfinite (set {x} \<times>\<^sub>\<bullet> []\<^sub>\<circ>)
[PROOF STEP]
qed simp
[PROOF STATE]
proof (state)
this:
vfinite (set {x} \<times>\<^sub>\<bullet> b)

goal (2 subgoals):
 1. \<And>b. vfinite b \<Longrightarrow> vfinite ([]\<^sub>\<circ> \<times>\<^sub>\<bullet> b)
 2. \<And>x F b. \<lbrakk>vfinite F; x \<notin>\<^sub>\<circ> F; \<And>b. vfinite b \<Longrightarrow> vfinite (F \<times>\<^sub>\<bullet> b); vfinite b\<rbrakk> \<Longrightarrow> vfinite (vinsert x F \<times>\<^sub>\<bullet> b)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
vfinite (set {x} \<times>\<^sub>\<bullet> b)

goal (2 subgoals):
 1. \<And>b. vfinite b \<Longrightarrow> vfinite ([]\<^sub>\<circ> \<times>\<^sub>\<bullet> b)
 2. \<And>x F b. \<lbrakk>vfinite F; x \<notin>\<^sub>\<circ> F; \<And>b. vfinite b \<Longrightarrow> vfinite (F \<times>\<^sub>\<bullet> b); vfinite b\<rbrakk> \<Longrightarrow> vfinite (vinsert x F \<times>\<^sub>\<bullet> b)
[PROOF STEP]
have "vinsert x a' \<times>\<^sub>\<bullet> b = (set {x} \<times>\<^sub>\<bullet> b) \<union>\<^sub>\<circ> (a' \<times>\<^sub>\<bullet> b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vinsert x a' \<times>\<^sub>\<bullet> b = set {x} \<times>\<^sub>\<bullet> b \<union>\<^sub>\<circ> a' \<times>\<^sub>\<bullet> b
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
vinsert x a' \<times>\<^sub>\<bullet> b = set {x} \<times>\<^sub>\<bullet> b \<union>\<^sub>\<circ> a' \<times>\<^sub>\<bullet> b

goal (2 subgoals):
 1. \<And>b. vfinite b \<Longrightarrow> vfinite ([]\<^sub>\<circ> \<times>\<^sub>\<bullet> b)
 2. \<And>x F b. \<lbrakk>vfinite F; x \<notin>\<^sub>\<circ> F; \<And>b. vfinite b \<Longrightarrow> vfinite (F \<times>\<^sub>\<bullet> b); vfinite b\<rbrakk> \<Longrightarrow> vfinite (vinsert x F \<times>\<^sub>\<bullet> b)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
vfinite (set {x} \<times>\<^sub>\<bullet> b)
vinsert x a' \<times>\<^sub>\<bullet> b = set {x} \<times>\<^sub>\<bullet> b \<union>\<^sub>\<circ> a' \<times>\<^sub>\<bullet> b
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
vfinite (set {x} \<times>\<^sub>\<bullet> b)
vinsert x a' \<times>\<^sub>\<bullet> b = set {x} \<times>\<^sub>\<bullet> b \<union>\<^sub>\<circ> a' \<times>\<^sub>\<bullet> b

goal (1 subgoal):
 1. vfinite (vinsert x a' \<times>\<^sub>\<bullet> b)
[PROOF STEP]
using vinsert
[PROOF STATE]
proof (prove)
using this:
vfinite (set {x} \<times>\<^sub>\<bullet> b)
vinsert x a' \<times>\<^sub>\<bullet> b = set {x} \<times>\<^sub>\<bullet> b \<union>\<^sub>\<circ> a' \<times>\<^sub>\<bullet> b
vfinite a'
x \<notin>\<^sub>\<circ> a'
vfinite ?b \<Longrightarrow> vfinite (a' \<times>\<^sub>\<bullet> ?b)
vfinite b

goal (1 subgoal):
 1. vfinite (vinsert x a' \<times>\<^sub>\<bullet> b)
[PROOF STEP]
by (auto simp: vfinite_vunionI)
[PROOF STATE]
proof (state)
this:
vfinite (vinsert x a' \<times>\<^sub>\<bullet> b)

goal (1 subgoal):
 1. \<And>b. vfinite b \<Longrightarrow> vfinite ([]\<^sub>\<circ> \<times>\<^sub>\<bullet> b)
[PROOF STEP]
qed simp


[STATEMENT]
lemma vproduct_vpair: "[a, b]\<^sub>\<circ> \<in>\<^sub>\<circ> (\<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>2\<^sub>\<nat>. f i) \<longleftrightarrow> \<langle>a, b\<rangle> \<in>\<^sub>\<circ> f (0\<^sub>\<nat>) \<times>\<^sub>\<circ> f (1\<^sub>\<nat>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ([a, b]\<^sub>\<circ> \<in>\<^sub>\<circ> vproduct (2\<^sub>\<nat>) f) = (\<langle>a, b\<rangle> \<in>\<^sub>\<circ> f (0\<^sub>\<nat>) \<times>\<^sub>\<circ> f (1\<^sub>\<nat>))
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. [a, b]\<^sub>\<circ> \<in>\<^sub>\<circ> vproduct (2\<^sub>\<nat>) f \<Longrightarrow> \<langle>a, b\<rangle> \<in>\<^sub>\<circ> f (0\<^sub>\<nat>) \<times>\<^sub>\<circ> f (1\<^sub>\<nat>)
 2. \<langle>a, b\<rangle> \<in>\<^sub>\<circ> f (0\<^sub>\<nat>) \<times>\<^sub>\<circ> f (1\<^sub>\<nat>) \<Longrightarrow> [a, b]\<^sub>\<circ> \<in>\<^sub>\<circ> vproduct (2\<^sub>\<nat>) f
[PROOF STEP]
interpret vfsequence \<open>[a, b]\<^sub>\<circ>\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vfsequence [a, b]\<^sub>\<circ>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. [a, b]\<^sub>\<circ> \<in>\<^sub>\<circ> vproduct (2\<^sub>\<nat>) f \<Longrightarrow> \<langle>a, b\<rangle> \<in>\<^sub>\<circ> f (0\<^sub>\<nat>) \<times>\<^sub>\<circ> f (1\<^sub>\<nat>)
 2. \<langle>a, b\<rangle> \<in>\<^sub>\<circ> f (0\<^sub>\<nat>) \<times>\<^sub>\<circ> f (1\<^sub>\<nat>) \<Longrightarrow> [a, b]\<^sub>\<circ> \<in>\<^sub>\<circ> vproduct (2\<^sub>\<nat>) f
[PROOF STEP]
show "[a, b]\<^sub>\<circ> \<in>\<^sub>\<circ> (\<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>2\<^sub>\<nat>. f i) \<Longrightarrow> \<langle>a, b\<rangle> \<in>\<^sub>\<circ> f (0\<^sub>\<nat>) \<times>\<^sub>\<circ> f (1\<^sub>\<nat>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [a, b]\<^sub>\<circ> \<in>\<^sub>\<circ> vproduct (2\<^sub>\<nat>) f \<Longrightarrow> \<langle>a, b\<rangle> \<in>\<^sub>\<circ> f (0\<^sub>\<nat>) \<times>\<^sub>\<circ> f (1\<^sub>\<nat>)
[PROOF STEP]
unfolding vcons_vdoubleton two
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set {\<langle>0\<^sub>\<nat>, a\<rangle>, \<langle>1\<^sub>\<nat>, b\<rangle>} \<in>\<^sub>\<circ> vproduct (set {[]\<^sub>\<circ>, 1\<^sub>\<nat>}) f \<Longrightarrow> \<langle>a, b\<rangle> \<in>\<^sub>\<circ> f (0\<^sub>\<nat>) \<times>\<^sub>\<circ> f (1\<^sub>\<nat>)
[PROOF STEP]
by (elim vproduct_vdoubletonE) auto
[PROOF STATE]
proof (state)
this:
[a, b]\<^sub>\<circ> \<in>\<^sub>\<circ> vproduct (2\<^sub>\<nat>) f \<Longrightarrow> \<langle>a, b\<rangle> \<in>\<^sub>\<circ> f (0\<^sub>\<nat>) \<times>\<^sub>\<circ> f (1\<^sub>\<nat>)

goal (1 subgoal):
 1. \<langle>a, b\<rangle> \<in>\<^sub>\<circ> f (0\<^sub>\<nat>) \<times>\<^sub>\<circ> f (1\<^sub>\<nat>) \<Longrightarrow> [a, b]\<^sub>\<circ> \<in>\<^sub>\<circ> vproduct (2\<^sub>\<nat>) f
[PROOF STEP]
assume hyp: "\<langle>a, b\<rangle> \<in>\<^sub>\<circ> f (0\<^sub>\<nat>) \<times>\<^sub>\<circ> f (1\<^sub>\<nat>)"
[PROOF STATE]
proof (state)
this:
\<langle>a, b\<rangle> \<in>\<^sub>\<circ> f (0\<^sub>\<nat>) \<times>\<^sub>\<circ> f (1\<^sub>\<nat>)

goal (1 subgoal):
 1. \<langle>a, b\<rangle> \<in>\<^sub>\<circ> f (0\<^sub>\<nat>) \<times>\<^sub>\<circ> f (1\<^sub>\<nat>) \<Longrightarrow> [a, b]\<^sub>\<circ> \<in>\<^sub>\<circ> vproduct (2\<^sub>\<nat>) f
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<langle>a, b\<rangle> \<in>\<^sub>\<circ> f (0\<^sub>\<nat>) \<times>\<^sub>\<circ> f (1\<^sub>\<nat>)
[PROOF STEP]
have af: "a \<in>\<^sub>\<circ> f (0\<^sub>\<nat>)" and bf: "b \<in>\<^sub>\<circ> f (1\<^sub>\<nat>)"
[PROOF STATE]
proof (prove)
using this:
\<langle>a, b\<rangle> \<in>\<^sub>\<circ> f (0\<^sub>\<nat>) \<times>\<^sub>\<circ> f (1\<^sub>\<nat>)

goal (1 subgoal):
 1. a \<in>\<^sub>\<circ> f (0\<^sub>\<nat>) &&& b \<in>\<^sub>\<circ> f (1\<^sub>\<nat>)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
a \<in>\<^sub>\<circ> f (0\<^sub>\<nat>)
b \<in>\<^sub>\<circ> f (1\<^sub>\<nat>)

goal (1 subgoal):
 1. \<langle>a, b\<rangle> \<in>\<^sub>\<circ> f (0\<^sub>\<nat>) \<times>\<^sub>\<circ> f (1\<^sub>\<nat>) \<Longrightarrow> [a, b]\<^sub>\<circ> \<in>\<^sub>\<circ> vproduct (2\<^sub>\<nat>) f
[PROOF STEP]
have dom: "\<D>\<^sub>\<circ> [a, b]\<^sub>\<circ> = set {0\<^sub>\<nat>, 1\<^sub>\<nat>}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<D>\<^sub>\<circ> [a, b]\<^sub>\<circ> = set {0\<^sub>\<nat>, 1\<^sub>\<nat>}
[PROOF STEP]
by (auto intro!: vsubset_antisym)
[PROOF STATE]
proof (state)
this:
\<D>\<^sub>\<circ> [a, b]\<^sub>\<circ> = set {0\<^sub>\<nat>, 1\<^sub>\<nat>}

goal (1 subgoal):
 1. \<langle>a, b\<rangle> \<in>\<^sub>\<circ> f (0\<^sub>\<nat>) \<times>\<^sub>\<circ> f (1\<^sub>\<nat>) \<Longrightarrow> [a, b]\<^sub>\<circ> \<in>\<^sub>\<circ> vproduct (2\<^sub>\<nat>) f
[PROOF STEP]
have ran: "\<R>\<^sub>\<circ> [a, b]\<^sub>\<circ> \<subseteq>\<^sub>\<circ> (\<Union>\<^sub>\<circ>i\<in>\<^sub>\<circ>2\<^sub>\<nat>. f i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<R>\<^sub>\<circ> [a, b]\<^sub>\<circ> \<subseteq>\<^sub>\<circ> \<Union>\<^sub>\<circ> (VLambda (2\<^sub>\<nat>) f `\<^sub>\<circ> 2\<^sub>\<nat>)
[PROOF STEP]
unfolding two
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<R>\<^sub>\<circ> [a, b]\<^sub>\<circ> \<subseteq>\<^sub>\<circ> \<Union>\<^sub>\<circ> (VLambda (set {[]\<^sub>\<circ>, 1\<^sub>\<nat>}) f `\<^sub>\<circ> set {[]\<^sub>\<circ>, 1\<^sub>\<nat>})
[PROOF STEP]
using af bf vifunion_vdoubleton
[PROOF STATE]
proof (prove)
using this:
a \<in>\<^sub>\<circ> f (0\<^sub>\<nat>)
b \<in>\<^sub>\<circ> f (1\<^sub>\<nat>)
\<Union>\<^sub>\<circ> (VLambda (set {?i, ?j}) ?f `\<^sub>\<circ> set {?i, ?j}) = ?f ?i \<union>\<^sub>\<circ> ?f ?j

goal (1 subgoal):
 1. \<R>\<^sub>\<circ> [a, b]\<^sub>\<circ> \<subseteq>\<^sub>\<circ> \<Union>\<^sub>\<circ> (VLambda (set {[]\<^sub>\<circ>, 1\<^sub>\<nat>}) f `\<^sub>\<circ> set {[]\<^sub>\<circ>, 1\<^sub>\<nat>})
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<R>\<^sub>\<circ> [a, b]\<^sub>\<circ> \<subseteq>\<^sub>\<circ> \<Union>\<^sub>\<circ> (VLambda (2\<^sub>\<nat>) f `\<^sub>\<circ> 2\<^sub>\<nat>)

goal (1 subgoal):
 1. \<langle>a, b\<rangle> \<in>\<^sub>\<circ> f (0\<^sub>\<nat>) \<times>\<^sub>\<circ> f (1\<^sub>\<nat>) \<Longrightarrow> [a, b]\<^sub>\<circ> \<in>\<^sub>\<circ> vproduct (2\<^sub>\<nat>) f
[PROOF STEP]
show "[a, b]\<^sub>\<circ> \<in>\<^sub>\<circ> (\<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>2\<^sub>\<nat>. f i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [a, b]\<^sub>\<circ> \<in>\<^sub>\<circ> vproduct (2\<^sub>\<nat>) f
[PROOF STEP]
apply(intro vproductI)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. vsv [a, b]\<^sub>\<circ>
 2. \<D>\<^sub>\<circ> [a, b]\<^sub>\<circ> = 2\<^sub>\<nat>
 3. \<forall>i\<in>elts (2\<^sub>\<nat>). [a, b]\<^sub>\<circ>\<lparr>i\<rparr> \<in>\<^sub>\<circ> f i
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vsv [a, b]\<^sub>\<circ>
[PROOF STEP]
using dom ran vsv_axioms
[PROOF STATE]
proof (prove)
using this:
\<D>\<^sub>\<circ> [a, b]\<^sub>\<circ> = set {0\<^sub>\<nat>, 1\<^sub>\<nat>}
\<R>\<^sub>\<circ> [a, b]\<^sub>\<circ> \<subseteq>\<^sub>\<circ> \<Union>\<^sub>\<circ> (VLambda (2\<^sub>\<nat>) f `\<^sub>\<circ> 2\<^sub>\<nat>)
vsv [a, b]\<^sub>\<circ>

goal (1 subgoal):
 1. vsv [a, b]\<^sub>\<circ>
[PROOF STEP]
unfolding two
[PROOF STATE]
proof (prove)
using this:
\<D>\<^sub>\<circ> [a, b]\<^sub>\<circ> = set {0\<^sub>\<nat>, 1\<^sub>\<nat>}
\<R>\<^sub>\<circ> [a, b]\<^sub>\<circ> \<subseteq>\<^sub>\<circ> \<Union>\<^sub>\<circ> (VLambda (set {[]\<^sub>\<circ>, 1\<^sub>\<nat>}) f `\<^sub>\<circ> set {[]\<^sub>\<circ>, 1\<^sub>\<nat>})
vsv [a, b]\<^sub>\<circ>

goal (1 subgoal):
 1. vsv [a, b]\<^sub>\<circ>
[PROOF STEP]
by auto
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<D>\<^sub>\<circ> [a, b]\<^sub>\<circ> = 2\<^sub>\<nat>
 2. \<forall>i\<in>elts (2\<^sub>\<nat>). [a, b]\<^sub>\<circ>\<lparr>i\<rparr> \<in>\<^sub>\<circ> f i
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<D>\<^sub>\<circ> [a, b]\<^sub>\<circ> = 2\<^sub>\<nat>
[PROOF STEP]
using af bf
[PROOF STATE]
proof (prove)
using this:
a \<in>\<^sub>\<circ> f (0\<^sub>\<nat>)
b \<in>\<^sub>\<circ> f (1\<^sub>\<nat>)

goal (1 subgoal):
 1. \<D>\<^sub>\<circ> [a, b]\<^sub>\<circ> = 2\<^sub>\<nat>
[PROOF STEP]
unfolding two
[PROOF STATE]
proof (prove)
using this:
a \<in>\<^sub>\<circ> f (0\<^sub>\<nat>)
b \<in>\<^sub>\<circ> f (1\<^sub>\<nat>)

goal (1 subgoal):
 1. \<D>\<^sub>\<circ> [a, b]\<^sub>\<circ> = set {[]\<^sub>\<circ>, 1\<^sub>\<nat>}
[PROOF STEP]
by (auto intro!: vsubset_antisym)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>i\<in>elts (2\<^sub>\<nat>). [a, b]\<^sub>\<circ>\<lparr>i\<rparr> \<in>\<^sub>\<circ> f i
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>i\<in>elts (2\<^sub>\<nat>). [a, b]\<^sub>\<circ>\<lparr>i\<rparr> \<in>\<^sub>\<circ> f i
[PROOF STEP]
unfolding two
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>i\<in>elts (set {[]\<^sub>\<circ>, 1\<^sub>\<nat>}). [a, b]\<^sub>\<circ>\<lparr>i\<rparr> \<in>\<^sub>\<circ> f i
[PROOF STEP]
using hyp VSigmaE2 small_empty vcons_vdoubleton
[PROOF STATE]
proof (prove)
using this:
\<langle>a, b\<rangle> \<in>\<^sub>\<circ> f (0\<^sub>\<nat>) \<times>\<^sub>\<circ> f (1\<^sub>\<nat>)
\<lbrakk>\<langle>?a, ?b\<rangle> \<in>\<^sub>\<circ> VSigma ?A ?B; \<lbrakk>?a \<in>\<^sub>\<circ> ?A; ?b \<in>\<^sub>\<circ> ?B ?a\<rbrakk> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis
small {}
[?a, ?b]\<^sub>\<circ> = set {\<langle>0\<^sub>\<nat>, ?a\<rangle>, \<langle>1\<^sub>\<nat>, ?b\<rangle>}

goal (1 subgoal):
 1. \<forall>i\<in>elts (set {[]\<^sub>\<circ>, 1\<^sub>\<nat>}). [a, b]\<^sub>\<circ>\<lparr>i\<rparr> \<in>\<^sub>\<circ> f i
[PROOF STEP]
by (auto simp: vinsert_set_insert_eq)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
[a, b]\<^sub>\<circ> \<in>\<^sub>\<circ> vproduct (2\<^sub>\<nat>) f

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma vcpower_two_ftimes: "A ^\<^sub>\<times> 2\<^sub>\<nat> = A \<times>\<^sub>\<bullet> A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A ^\<^sub>\<times> 2\<^sub>\<nat> = A \<times>\<^sub>\<bullet> A
[PROOF STEP]
unfolding vcpower_def ftimes_def two
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>set {[]\<^sub>\<circ>, 1\<^sub>\<nat>}. A) = (\<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>set {[]\<^sub>\<circ>, 1\<^sub>\<nat>}. if i = []\<^sub>\<circ> \<Rightarrow> A | otherwise \<Rightarrow> A)
[PROOF STEP]
by simp


[STATEMENT]
lemma vcpower_two_ftimesI[intro]:
  assumes "x \<in>\<^sub>\<circ> A \<times>\<^sub>\<bullet> A"
  shows "x \<in>\<^sub>\<circ> A ^\<^sub>\<times> 2\<^sub>\<nat>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in>\<^sub>\<circ> A ^\<^sub>\<times> 2\<^sub>\<nat>
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
x \<in>\<^sub>\<circ> A \<times>\<^sub>\<bullet> A

goal (1 subgoal):
 1. x \<in>\<^sub>\<circ> A ^\<^sub>\<times> 2\<^sub>\<nat>
[PROOF STEP]
unfolding ftimes_def two
[PROOF STATE]
proof (prove)
using this:
x \<in>\<^sub>\<circ> (\<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>set {[]\<^sub>\<circ>, 1\<^sub>\<nat>}. if i = []\<^sub>\<circ> \<Rightarrow> A | otherwise \<Rightarrow> A)

goal (1 subgoal):
 1. x \<in>\<^sub>\<circ> A ^\<^sub>\<times> set {[]\<^sub>\<circ>, 1\<^sub>\<nat>}
[PROOF STEP]
by auto


[STATEMENT]
lemma vcpower_two_ftimesD[dest]:
  assumes "x \<in>\<^sub>\<circ> A ^\<^sub>\<times> 2\<^sub>\<nat>"
  shows "x \<in>\<^sub>\<circ> A \<times>\<^sub>\<bullet> A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in>\<^sub>\<circ> A \<times>\<^sub>\<bullet> A
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
x \<in>\<^sub>\<circ> A ^\<^sub>\<times> 2\<^sub>\<nat>

goal (1 subgoal):
 1. x \<in>\<^sub>\<circ> A \<times>\<^sub>\<bullet> A
[PROOF STEP]
unfolding vcpower_def ftimes_def two
[PROOF STATE]
proof (prove)
using this:
x \<in>\<^sub>\<circ> (\<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>set {[]\<^sub>\<circ>, 1\<^sub>\<nat>}. A)

goal (1 subgoal):
 1. x \<in>\<^sub>\<circ> (\<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>set {[]\<^sub>\<circ>, 1\<^sub>\<nat>}. if i = []\<^sub>\<circ> \<Rightarrow> A | otherwise \<Rightarrow> A)
[PROOF STEP]
by simp


[STATEMENT]
lemma vcpower_two_ftimesE[elim]:
  assumes "x \<in>\<^sub>\<circ> A ^\<^sub>\<times> 2\<^sub>\<nat>" and "x \<in>\<^sub>\<circ> A \<times>\<^sub>\<bullet> A \<Longrightarrow> P"
  shows P
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
x \<in>\<^sub>\<circ> A ^\<^sub>\<times> 2\<^sub>\<nat>
x \<in>\<^sub>\<circ> A \<times>\<^sub>\<bullet> A \<Longrightarrow> P

goal (1 subgoal):
 1. P
[PROOF STEP]
unfolding vcpower_def ftimes_def two
[PROOF STATE]
proof (prove)
using this:
x \<in>\<^sub>\<circ> (\<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>set {[]\<^sub>\<circ>, 1\<^sub>\<nat>}. A)
x \<in>\<^sub>\<circ> (\<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>set {[]\<^sub>\<circ>, 1\<^sub>\<nat>}. if i = []\<^sub>\<circ> \<Rightarrow> A | otherwise \<Rightarrow> A) \<Longrightarrow> P

goal (1 subgoal):
 1. P
[PROOF STEP]
by simp


[STATEMENT]
lemma vfsequence_vcpower_two_vpair: "[a, b]\<^sub>\<circ> \<in>\<^sub>\<circ> A ^\<^sub>\<times> 2\<^sub>\<nat> \<longleftrightarrow> \<langle>a, b\<rangle> \<in>\<^sub>\<circ> A \<times>\<^sub>\<circ> A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ([a, b]\<^sub>\<circ> \<in>\<^sub>\<circ> A ^\<^sub>\<times> 2\<^sub>\<nat>) = (\<langle>a, b\<rangle> \<in>\<^sub>\<circ> A \<times>\<^sub>\<circ> A)
[PROOF STEP]
proof(rule iffI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. [a, b]\<^sub>\<circ> \<in>\<^sub>\<circ> A ^\<^sub>\<times> 2\<^sub>\<nat> \<Longrightarrow> \<langle>a, b\<rangle> \<in>\<^sub>\<circ> A \<times>\<^sub>\<circ> A
 2. \<langle>a, b\<rangle> \<in>\<^sub>\<circ> A \<times>\<^sub>\<circ> A \<Longrightarrow> [a, b]\<^sub>\<circ> \<in>\<^sub>\<circ> A ^\<^sub>\<times> 2\<^sub>\<nat>
[PROOF STEP]
show "[a, b]\<^sub>\<circ> \<in>\<^sub>\<circ> A ^\<^sub>\<times> 2\<^sub>\<nat> \<Longrightarrow> \<langle>a, b\<rangle> \<in>\<^sub>\<circ> A \<times>\<^sub>\<circ> A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [a, b]\<^sub>\<circ> \<in>\<^sub>\<circ> A ^\<^sub>\<times> 2\<^sub>\<nat> \<Longrightarrow> \<langle>a, b\<rangle> \<in>\<^sub>\<circ> A \<times>\<^sub>\<circ> A
[PROOF STEP]
by (elim vcpowerE, unfold vproduct_vpair)
[PROOF STATE]
proof (state)
this:
[a, b]\<^sub>\<circ> \<in>\<^sub>\<circ> A ^\<^sub>\<times> 2\<^sub>\<nat> \<Longrightarrow> \<langle>a, b\<rangle> \<in>\<^sub>\<circ> A \<times>\<^sub>\<circ> A

goal (1 subgoal):
 1. \<langle>a, b\<rangle> \<in>\<^sub>\<circ> A \<times>\<^sub>\<circ> A \<Longrightarrow> [a, b]\<^sub>\<circ> \<in>\<^sub>\<circ> A ^\<^sub>\<times> 2\<^sub>\<nat>
[PROOF STEP]
qed (intro vcpowerI, unfold vproduct_vpair)


[STATEMENT]
lemma vsv_vfsequence_two:
  assumes "vsv gf" and "\<D>\<^sub>\<circ> gf = 2\<^sub>\<nat>"
  shows "[vpfst gf, vpsnd gf]\<^sub>\<circ> = gf"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [gf\<lparr>[]\<^sub>\<circ>\<rparr>, gf\<lparr>1\<^sub>\<nat>\<rparr>]\<^sub>\<circ> = gf
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. [gf\<lparr>[]\<^sub>\<circ>\<rparr>, gf\<lparr>1\<^sub>\<nat>\<rparr>]\<^sub>\<circ> = gf
[PROOF STEP]
interpret gf: vsv gf
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vsv gf
[PROOF STEP]
by (auto intro: assms(1))
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. [gf\<lparr>[]\<^sub>\<circ>\<rparr>, gf\<lparr>1\<^sub>\<nat>\<rparr>]\<^sub>\<circ> = gf
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [gf\<lparr>[]\<^sub>\<circ>\<rparr>, gf\<lparr>1\<^sub>\<nat>\<rparr>]\<^sub>\<circ> = gf
[PROOF STEP]
by
      (
        rule sym,
        rule vsv_eqI,
        blast,
        blast,
        simp add: assms(2) nat_omega_simps,
        unfold assms(2),
        elim_in_numeral,
        all\<open>simp add: nat_omega_simps\<close>
      )
[PROOF STATE]
proof (state)
this:
[gf\<lparr>[]\<^sub>\<circ>\<rparr>, gf\<lparr>1\<^sub>\<nat>\<rparr>]\<^sub>\<circ> = gf

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma vsv_vfsequence_three:
  assumes "vsv hgf" and "\<D>\<^sub>\<circ> hgf = 3\<^sub>\<nat>"
  shows "[vpfst hgf, vpsnd hgf, vpthrd hgf]\<^sub>\<circ> = hgf"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [hgf\<lparr>[]\<^sub>\<circ>\<rparr>, hgf\<lparr>1\<^sub>\<nat>\<rparr>, hgf\<lparr>2\<^sub>\<nat>\<rparr>]\<^sub>\<circ> = hgf
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. [hgf\<lparr>[]\<^sub>\<circ>\<rparr>, hgf\<lparr>1\<^sub>\<nat>\<rparr>, hgf\<lparr>2\<^sub>\<nat>\<rparr>]\<^sub>\<circ> = hgf
[PROOF STEP]
interpret hgf: vsv hgf
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vsv hgf
[PROOF STEP]
by (auto intro: assms(1))
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. [hgf\<lparr>[]\<^sub>\<circ>\<rparr>, hgf\<lparr>1\<^sub>\<nat>\<rparr>, hgf\<lparr>2\<^sub>\<nat>\<rparr>]\<^sub>\<circ> = hgf
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [hgf\<lparr>[]\<^sub>\<circ>\<rparr>, hgf\<lparr>1\<^sub>\<nat>\<rparr>, hgf\<lparr>2\<^sub>\<nat>\<rparr>]\<^sub>\<circ> = hgf
[PROOF STEP]
by
      (
        rule sym,
        rule vsv_eqI,
        blast,
        blast,
        simp add: assms(2) nat_omega_simps,
        unfold assms(2),
        elim_in_numeral,
        all\<open>simp add: nat_omega_simps\<close>
      )
[PROOF STATE]
proof (state)
this:
[hgf\<lparr>[]\<^sub>\<circ>\<rparr>, hgf\<lparr>1\<^sub>\<nat>\<rparr>, hgf\<lparr>2\<^sub>\<nat>\<rparr>]\<^sub>\<circ> = hgf

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma vcons_in_vcpowerI[intro!]:
  assumes "n \<in>\<^sub>\<circ> \<omega>"
    and "xs \<in>\<^sub>\<circ> A ^\<^sub>\<times> vcard xs"
    and "x \<in>\<^sub>\<circ> A"
    and "n = vcard (xs #\<^sub>\<circ> x)"
  shows "xs #\<^sub>\<circ> x \<in>\<^sub>\<circ> A ^\<^sub>\<times> n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. xs #\<^sub>\<circ> x \<in>\<^sub>\<circ> A ^\<^sub>\<times> n
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. xs #\<^sub>\<circ> x \<in>\<^sub>\<circ> A ^\<^sub>\<times> n
[PROOF STEP]
interpret vfsequence xs
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vfsequence xs
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
n \<in>\<^sub>\<circ> \<omega>
xs \<in>\<^sub>\<circ> A ^\<^sub>\<times> vcard xs
x \<in>\<^sub>\<circ> A
n = vcard (xs #\<^sub>\<circ> x)

goal (1 subgoal):
 1. vfsequence xs
[PROOF STEP]
by
      (
        meson
          vcons_vsubset
          vfinite_vcard_omega_iff
          vfinite_vsubset
          vfsequence_vcpower
      )
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. xs #\<^sub>\<circ> x \<in>\<^sub>\<circ> A ^\<^sub>\<times> n
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. xs #\<^sub>\<circ> x \<in>\<^sub>\<circ> A ^\<^sub>\<times> n
[PROOF STEP]
by
      (
        metis
          assms(2,3,4)
          vcpower_vrange
          vfsequence_vcons
          vfsequence_vcons_vrange
          vfsequence.vfsequence_vrange_vcpower
          vsubset_vinsert_leftI
      )
[PROOF STATE]
proof (state)
this:
xs #\<^sub>\<circ> x \<in>\<^sub>\<circ> A ^\<^sub>\<times> n

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma vcons_in_vcpowerD[dest]:
  assumes "xs #\<^sub>\<circ> x \<in>\<^sub>\<circ> A ^\<^sub>\<times> n" and "n \<in>\<^sub>\<circ> \<omega>"
  shows "xs \<in>\<^sub>\<circ> A ^\<^sub>\<times> vcard xs"
    and "x \<in>\<^sub>\<circ> A"
    and "n = vcard (xs #\<^sub>\<circ> x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. xs \<in>\<^sub>\<circ> A ^\<^sub>\<times> vcard xs &&& x \<in>\<^sub>\<circ> A &&& n = vcard (xs #\<^sub>\<circ> x)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. xs \<in>\<^sub>\<circ> A ^\<^sub>\<times> vcard xs
 2. x \<in>\<^sub>\<circ> A
 3. n = vcard (xs #\<^sub>\<circ> x)
[PROOF STEP]
interpret vfsequence xs
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vfsequence xs
[PROOF STEP]
by
      (
        meson
          assms
          vfsequence.vfsequence_vremove_vcons_vfsequence
          vfsequence_vcpower
      )
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. xs \<in>\<^sub>\<circ> A ^\<^sub>\<times> vcard xs
 2. x \<in>\<^sub>\<circ> A
 3. n = vcard (xs #\<^sub>\<circ> x)
[PROOF STEP]
from assms vfsequence_vcard_vcons
[PROOF STATE]
proof (chain)
picking this:
xs #\<^sub>\<circ> x \<in>\<^sub>\<circ> A ^\<^sub>\<times> n
n \<in>\<^sub>\<circ> \<omega>
vcard (xs #\<^sub>\<circ> ?x) = ZFC_in_HOL.succ (vcard xs)
[PROOF STEP]
show "n = vcard (xs #\<^sub>\<circ> x)"
[PROOF STATE]
proof (prove)
using this:
xs #\<^sub>\<circ> x \<in>\<^sub>\<circ> A ^\<^sub>\<times> n
n \<in>\<^sub>\<circ> \<omega>
vcard (xs #\<^sub>\<circ> ?x) = ZFC_in_HOL.succ (vcard xs)

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

goal (2 subgoals):
 1. xs \<in>\<^sub>\<circ> A ^\<^sub>\<times> vcard xs
 2. x \<in>\<^sub>\<circ> A
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
n = vcard (xs #\<^sub>\<circ> x)
[PROOF STEP]
show "xs \<in>\<^sub>\<circ> A ^\<^sub>\<times> vcard xs"
[PROOF STATE]
proof (prove)
using this:
n = vcard (xs #\<^sub>\<circ> x)

goal (1 subgoal):
 1. xs \<in>\<^sub>\<circ> A ^\<^sub>\<times> vcard xs
[PROOF STEP]
by
      (
        metis
          assms(1)
          vcpower_vrange
          vfsequence_vcons_vrange
          vfsequence_vrange_vcpower
          vsubset_vinsert_leftD
      )
[PROOF STATE]
proof (state)
this:
xs \<in>\<^sub>\<circ> A ^\<^sub>\<times> vcard xs

goal (1 subgoal):
 1. x \<in>\<^sub>\<circ> A
[PROOF STEP]
show "x \<in>\<^sub>\<circ> A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in>\<^sub>\<circ> A
[PROOF STEP]
by
      (
        metis
          assms(1)
          vcpower_vrange
          vfsequence.vfsequence_vcons_vrange
          vfsequence_axioms
          vinsertI1
          vsubsetE
      )
[PROOF STATE]
proof (state)
this:
x \<in>\<^sub>\<circ> A

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma vcons_in_vcpowerE1[elim!]:
  assumes "xs #\<^sub>\<circ> x \<in>\<^sub>\<circ> A ^\<^sub>\<times> n" and "n \<in>\<^sub>\<circ> \<omega>"
  obtains "xs \<in>\<^sub>\<circ> A ^\<^sub>\<times> vcard xs" and "x \<in>\<^sub>\<circ> A" and "n = vcard (xs #\<^sub>\<circ> x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lbrakk>xs \<in>\<^sub>\<circ> A ^\<^sub>\<times> vcard xs; x \<in>\<^sub>\<circ> A; n = vcard (xs #\<^sub>\<circ> x)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
xs #\<^sub>\<circ> x \<in>\<^sub>\<circ> A ^\<^sub>\<times> n
n \<in>\<^sub>\<circ> \<omega>

goal (1 subgoal):
 1. (\<lbrakk>xs \<in>\<^sub>\<circ> A ^\<^sub>\<times> vcard xs; x \<in>\<^sub>\<circ> A; n = vcard (xs #\<^sub>\<circ> x)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast