[STATEMENT]
lemma freshChainPerm:
  fixes xvec :: "name list"
  and   yvec :: "name list"
  and   x    :: name
  and   C    :: "'a::pt_name"

  assumes "length xvec = length yvec"
  and     "yvec \<sharp>* C"
  and     "xvec \<sharp>* yvec"
  and     "x mem xvec"
  and     "distinct yvec"

  shows "x \<sharp> [xvec yvec] \<bullet>\<^sub>v C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<sharp> [xvec yvec] \<bullet>\<^sub>v C
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
length xvec = length yvec
yvec \<sharp>* C
xvec \<sharp>* yvec
x mem xvec
distinct yvec

goal (1 subgoal):
 1. x \<sharp> [xvec yvec] \<bullet>\<^sub>v C
[PROOF STEP]
proof(induct rule: composePermInduct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>[] \<sharp>* C; [] \<sharp>* []; x mem []; distinct []\<rbrakk> \<Longrightarrow> x \<sharp> [[] []] \<bullet>\<^sub>v C
 2. \<And>xa xvec y yvec. \<lbrakk>length xvec = length yvec; \<lbrakk>yvec \<sharp>* C; xvec \<sharp>* yvec; x mem xvec; distinct yvec\<rbrakk> \<Longrightarrow> x \<sharp> [xvec yvec] \<bullet>\<^sub>v C; (y # yvec) \<sharp>* C; (xa # xvec) \<sharp>* (y # yvec); x mem (xa # xvec); distinct (y # yvec)\<rbrakk> \<Longrightarrow> x \<sharp> [(xa # xvec) (y # yvec)] \<bullet>\<^sub>v C
[PROOF STEP]
case cBase
[PROOF STATE]
proof (state)
this:
[] \<sharp>* C
[] \<sharp>* []
x mem []
distinct []

goal (2 subgoals):
 1. \<lbrakk>[] \<sharp>* C; [] \<sharp>* []; x mem []; distinct []\<rbrakk> \<Longrightarrow> x \<sharp> [[] []] \<bullet>\<^sub>v C
 2. \<And>xa xvec y yvec. \<lbrakk>length xvec = length yvec; \<lbrakk>yvec \<sharp>* C; xvec \<sharp>* yvec; x mem xvec; distinct yvec\<rbrakk> \<Longrightarrow> x \<sharp> [xvec yvec] \<bullet>\<^sub>v C; (y # yvec) \<sharp>* C; (xa # xvec) \<sharp>* (y # yvec); x mem (xa # xvec); distinct (y # yvec)\<rbrakk> \<Longrightarrow> x \<sharp> [(xa # xvec) (y # yvec)] \<bullet>\<^sub>v C
[PROOF STEP]
have "x mem []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x mem []
[PROOF STEP]
by fact
[PROOF STATE]
proof (state)
this:
x mem []

goal (2 subgoals):
 1. \<lbrakk>[] \<sharp>* C; [] \<sharp>* []; x mem []; distinct []\<rbrakk> \<Longrightarrow> x \<sharp> [[] []] \<bullet>\<^sub>v C
 2. \<And>xa xvec y yvec. \<lbrakk>length xvec = length yvec; \<lbrakk>yvec \<sharp>* C; xvec \<sharp>* yvec; x mem xvec; distinct yvec\<rbrakk> \<Longrightarrow> x \<sharp> [xvec yvec] \<bullet>\<^sub>v C; (y # yvec) \<sharp>* C; (xa # xvec) \<sharp>* (y # yvec); x mem (xa # xvec); distinct (y # yvec)\<rbrakk> \<Longrightarrow> x \<sharp> [(xa # xvec) (y # yvec)] \<bullet>\<^sub>v C
[PROOF STEP]
hence False
[PROOF STATE]
proof (prove)
using this:
x mem []

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

goal (2 subgoals):
 1. \<lbrakk>[] \<sharp>* C; [] \<sharp>* []; x mem []; distinct []\<rbrakk> \<Longrightarrow> x \<sharp> [[] []] \<bullet>\<^sub>v C
 2. \<And>xa xvec y yvec. \<lbrakk>length xvec = length yvec; \<lbrakk>yvec \<sharp>* C; xvec \<sharp>* yvec; x mem xvec; distinct yvec\<rbrakk> \<Longrightarrow> x \<sharp> [xvec yvec] \<bullet>\<^sub>v C; (y # yvec) \<sharp>* C; (xa # xvec) \<sharp>* (y # yvec); x mem (xa # xvec); distinct (y # yvec)\<rbrakk> \<Longrightarrow> x \<sharp> [(xa # xvec) (y # yvec)] \<bullet>\<^sub>v C
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
False

goal (1 subgoal):
 1. x \<sharp> [[] []] \<bullet>\<^sub>v C
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
x \<sharp> [[] []] \<bullet>\<^sub>v C

goal (1 subgoal):
 1. \<And>xa xvec y yvec. \<lbrakk>length xvec = length yvec; \<lbrakk>yvec \<sharp>* C; xvec \<sharp>* yvec; x mem xvec; distinct yvec\<rbrakk> \<Longrightarrow> x \<sharp> [xvec yvec] \<bullet>\<^sub>v C; (y # yvec) \<sharp>* C; (xa # xvec) \<sharp>* (y # yvec); x mem (xa # xvec); distinct (y # yvec)\<rbrakk> \<Longrightarrow> x \<sharp> [(xa # xvec) (y # yvec)] \<bullet>\<^sub>v C
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xa xvec y yvec. \<lbrakk>length xvec = length yvec; \<lbrakk>yvec \<sharp>* C; xvec \<sharp>* yvec; x mem xvec; distinct yvec\<rbrakk> \<Longrightarrow> x \<sharp> [xvec yvec] \<bullet>\<^sub>v C; (y # yvec) \<sharp>* C; (xa # xvec) \<sharp>* (y # yvec); x mem (xa # xvec); distinct (y # yvec)\<rbrakk> \<Longrightarrow> x \<sharp> [(xa # xvec) (y # yvec)] \<bullet>\<^sub>v C
[PROOF STEP]
case(cStep x' xvec y yvec)
[PROOF STATE]
proof (state)
this:
length xvec = length yvec
\<lbrakk>yvec \<sharp>* C; xvec \<sharp>* yvec; x mem xvec; distinct yvec\<rbrakk> \<Longrightarrow> x \<sharp> [xvec yvec] \<bullet>\<^sub>v C
(y # yvec) \<sharp>* C
(x' # xvec) \<sharp>* (y # yvec)
x mem (x' # xvec)
distinct (y # yvec)

goal (1 subgoal):
 1. \<And>xa xvec y yvec. \<lbrakk>length xvec = length yvec; \<lbrakk>yvec \<sharp>* C; xvec \<sharp>* yvec; x mem xvec; distinct yvec\<rbrakk> \<Longrightarrow> x \<sharp> [xvec yvec] \<bullet>\<^sub>v C; (y # yvec) \<sharp>* C; (xa # xvec) \<sharp>* (y # yvec); x mem (xa # xvec); distinct (y # yvec)\<rbrakk> \<Longrightarrow> x \<sharp> [(xa # xvec) (y # yvec)] \<bullet>\<^sub>v C
[PROOF STEP]
have "(y # yvec) \<sharp>* C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (y # yvec) \<sharp>* C
[PROOF STEP]
by fact
[PROOF STATE]
proof (state)
this:
(y # yvec) \<sharp>* C

goal (1 subgoal):
 1. \<And>xa xvec y yvec. \<lbrakk>length xvec = length yvec; \<lbrakk>yvec \<sharp>* C; xvec \<sharp>* yvec; x mem xvec; distinct yvec\<rbrakk> \<Longrightarrow> x \<sharp> [xvec yvec] \<bullet>\<^sub>v C; (y # yvec) \<sharp>* C; (xa # xvec) \<sharp>* (y # yvec); x mem (xa # xvec); distinct (y # yvec)\<rbrakk> \<Longrightarrow> x \<sharp> [(xa # xvec) (y # yvec)] \<bullet>\<^sub>v C
[PROOF STEP]
hence yFreshC: "y \<sharp> C" and yvecFreshp: "yvec \<sharp>* C"
[PROOF STATE]
proof (prove)
using this:
(y # yvec) \<sharp>* C

goal (1 subgoal):
 1. y \<sharp> C &&& yvec \<sharp>* C
[PROOF STEP]
by simp+
[PROOF STATE]
proof (state)
this:
y \<sharp> C
yvec \<sharp>* C

goal (1 subgoal):
 1. \<And>xa xvec y yvec. \<lbrakk>length xvec = length yvec; \<lbrakk>yvec \<sharp>* C; xvec \<sharp>* yvec; x mem xvec; distinct yvec\<rbrakk> \<Longrightarrow> x \<sharp> [xvec yvec] \<bullet>\<^sub>v C; (y # yvec) \<sharp>* C; (xa # xvec) \<sharp>* (y # yvec); x mem (xa # xvec); distinct (y # yvec)\<rbrakk> \<Longrightarrow> x \<sharp> [(xa # xvec) (y # yvec)] \<bullet>\<^sub>v C
[PROOF STEP]
have "(x' # xvec) \<sharp>* (y # yvec)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x' # xvec) \<sharp>* (y # yvec)
[PROOF STEP]
by fact
[PROOF STATE]
proof (state)
this:
(x' # xvec) \<sharp>* (y # yvec)

goal (1 subgoal):
 1. \<And>xa xvec y yvec. \<lbrakk>length xvec = length yvec; \<lbrakk>yvec \<sharp>* C; xvec \<sharp>* yvec; x mem xvec; distinct yvec\<rbrakk> \<Longrightarrow> x \<sharp> [xvec yvec] \<bullet>\<^sub>v C; (y # yvec) \<sharp>* C; (xa # xvec) \<sharp>* (y # yvec); x mem (xa # xvec); distinct (y # yvec)\<rbrakk> \<Longrightarrow> x \<sharp> [(xa # xvec) (y # yvec)] \<bullet>\<^sub>v C
[PROOF STEP]
hence x'ineqy: "x' \<noteq> y" and xvecFreshyvec: "xvec \<sharp>* yvec"
    and x'Freshyvec: "x' \<sharp> yvec" and yFreshxvec: "y \<sharp> xvec"
[PROOF STATE]
proof (prove)
using this:
(x' # xvec) \<sharp>* (y # yvec)

goal (1 subgoal):
 1. (x' \<noteq> y &&& xvec \<sharp>* yvec) &&& x' \<sharp> yvec &&& y \<sharp> xvec
[PROOF STEP]
by(auto simp add: fresh_list_cons)
[PROOF STATE]
proof (state)
this:
x' \<noteq> y
xvec \<sharp>* yvec
x' \<sharp> yvec
y \<sharp> xvec

goal (1 subgoal):
 1. \<And>xa xvec y yvec. \<lbrakk>length xvec = length yvec; \<lbrakk>yvec \<sharp>* C; xvec \<sharp>* yvec; x mem xvec; distinct yvec\<rbrakk> \<Longrightarrow> x \<sharp> [xvec yvec] \<bullet>\<^sub>v C; (y # yvec) \<sharp>* C; (xa # xvec) \<sharp>* (y # yvec); x mem (xa # xvec); distinct (y # yvec)\<rbrakk> \<Longrightarrow> x \<sharp> [(xa # xvec) (y # yvec)] \<bullet>\<^sub>v C
[PROOF STEP]
have "distinct (y#yvec)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distinct (y # yvec)
[PROOF STEP]
by fact
[PROOF STATE]
proof (state)
this:
distinct (y # yvec)

goal (1 subgoal):
 1. \<And>xa xvec y yvec. \<lbrakk>length xvec = length yvec; \<lbrakk>yvec \<sharp>* C; xvec \<sharp>* yvec; x mem xvec; distinct yvec\<rbrakk> \<Longrightarrow> x \<sharp> [xvec yvec] \<bullet>\<^sub>v C; (y # yvec) \<sharp>* C; (xa # xvec) \<sharp>* (y # yvec); x mem (xa # xvec); distinct (y # yvec)\<rbrakk> \<Longrightarrow> x \<sharp> [(xa # xvec) (y # yvec)] \<bullet>\<^sub>v C
[PROOF STEP]
hence yFreshyvec: "y \<sharp> yvec" and yvecDist: "distinct yvec"
[PROOF STATE]
proof (prove)
using this:
distinct (y # yvec)

goal (1 subgoal):
 1. y \<sharp> yvec &&& distinct yvec
[PROOF STEP]
by simp+
[PROOF STATE]
proof (state)
this:
y \<sharp> yvec
distinct yvec

goal (1 subgoal):
 1. \<And>xa xvec y yvec. \<lbrakk>length xvec = length yvec; \<lbrakk>yvec \<sharp>* C; xvec \<sharp>* yvec; x mem xvec; distinct yvec\<rbrakk> \<Longrightarrow> x \<sharp> [xvec yvec] \<bullet>\<^sub>v C; (y # yvec) \<sharp>* C; (xa # xvec) \<sharp>* (y # yvec); x mem (xa # xvec); distinct (y # yvec)\<rbrakk> \<Longrightarrow> x \<sharp> [(xa # xvec) (y # yvec)] \<bullet>\<^sub>v C
[PROOF STEP]
have L: "length xvec = length yvec"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length xvec = length yvec
[PROOF STEP]
by fact
[PROOF STATE]
proof (state)
this:
length xvec = length yvec

goal (1 subgoal):
 1. \<And>xa xvec y yvec. \<lbrakk>length xvec = length yvec; \<lbrakk>yvec \<sharp>* C; xvec \<sharp>* yvec; x mem xvec; distinct yvec\<rbrakk> \<Longrightarrow> x \<sharp> [xvec yvec] \<bullet>\<^sub>v C; (y # yvec) \<sharp>* C; (xa # xvec) \<sharp>* (y # yvec); x mem (xa # xvec); distinct (y # yvec)\<rbrakk> \<Longrightarrow> x \<sharp> [(xa # xvec) (y # yvec)] \<bullet>\<^sub>v C
[PROOF STEP]
have "x \<sharp> [(x', y)] \<bullet> [xvec yvec] \<bullet>\<^sub>v C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<sharp> [(x', y)] \<bullet> [xvec yvec] \<bullet>\<^sub>v C
[PROOF STEP]
proof(case_tac "x = x'")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. x = x' \<Longrightarrow> x \<sharp> [(x', y)] \<bullet> [xvec yvec] \<bullet>\<^sub>v C
 2. x \<noteq> x' \<Longrightarrow> x \<sharp> [(x', y)] \<bullet> [xvec yvec] \<bullet>\<^sub>v C
[PROOF STEP]
assume xeqx': "x = x'"
[PROOF STATE]
proof (state)
this:
x = x'

goal (2 subgoals):
 1. x = x' \<Longrightarrow> x \<sharp> [(x', y)] \<bullet> [xvec yvec] \<bullet>\<^sub>v C
 2. x \<noteq> x' \<Longrightarrow> x \<sharp> [(x', y)] \<bullet> [xvec yvec] \<bullet>\<^sub>v C
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
x = x'

goal (2 subgoals):
 1. x = x' \<Longrightarrow> x \<sharp> [(x', y)] \<bullet> [xvec yvec] \<bullet>\<^sub>v C
 2. x \<noteq> x' \<Longrightarrow> x \<sharp> [(x', y)] \<bullet> [xvec yvec] \<bullet>\<^sub>v C
[PROOF STEP]
from yFreshxvec yFreshyvec yFreshC L
[PROOF STATE]
proof (chain)
picking this:
y \<sharp> xvec
y \<sharp> yvec
y \<sharp> C
length xvec = length yvec
[PROOF STEP]
have "y \<sharp> [xvec yvec] \<bullet>\<^sub>v C"
[PROOF STATE]
proof (prove)
using this:
y \<sharp> xvec
y \<sharp> yvec
y \<sharp> C
length xvec = length yvec

goal (1 subgoal):
 1. y \<sharp> [xvec yvec] \<bullet>\<^sub>v C
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
y \<sharp> [xvec yvec] \<bullet>\<^sub>v C

goal (2 subgoals):
 1. x = x' \<Longrightarrow> x \<sharp> [(x', y)] \<bullet> [xvec yvec] \<bullet>\<^sub>v C
 2. x \<noteq> x' \<Longrightarrow> x \<sharp> [(x', y)] \<bullet> [xvec yvec] \<bullet>\<^sub>v C
[PROOF STEP]
hence "([(x, y)] \<bullet> y) \<sharp> [(x, y)] \<bullet> [xvec yvec] \<bullet>\<^sub>v C"
[PROOF STATE]
proof (prove)
using this:
y \<sharp> [xvec yvec] \<bullet>\<^sub>v C

goal (1 subgoal):
 1. [(x, y)] \<bullet> y \<sharp> [(x, y)] \<bullet> [xvec yvec] \<bullet>\<^sub>v C
[PROOF STEP]
by(rule pt_fresh_bij1[OF pt_name_inst, OF at_name_inst])
[PROOF STATE]
proof (state)
this:
[(x, y)] \<bullet> y \<sharp> [(x, y)] \<bullet> [xvec yvec] \<bullet>\<^sub>v C

goal (2 subgoals):
 1. x = x' \<Longrightarrow> x \<sharp> [(x', y)] \<bullet> [xvec yvec] \<bullet>\<^sub>v C
 2. x \<noteq> x' \<Longrightarrow> x \<sharp> [(x', y)] \<bullet> [xvec yvec] \<bullet>\<^sub>v C
[PROOF STEP]
with x'ineqy xeqx'
[PROOF STATE]
proof (chain)
picking this:
x' \<noteq> y
x = x'
[(x, y)] \<bullet> y \<sharp> [(x, y)] \<bullet> [xvec yvec] \<bullet>\<^sub>v C
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
x' \<noteq> y
x = x'
[(x, y)] \<bullet> y \<sharp> [(x, y)] \<bullet> [xvec yvec] \<bullet>\<^sub>v C

goal (1 subgoal):
 1. x \<sharp> [(x', y)] \<bullet> [xvec yvec] \<bullet>\<^sub>v C
[PROOF STEP]
by(simp add: calc_atm)
[PROOF STATE]
proof (state)
this:
x \<sharp> [(x', y)] \<bullet> [xvec yvec] \<bullet>\<^sub>v C

goal (1 subgoal):
 1. x \<noteq> x' \<Longrightarrow> x \<sharp> [(x', y)] \<bullet> [xvec yvec] \<bullet>\<^sub>v C
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x \<noteq> x' \<Longrightarrow> x \<sharp> [(x', y)] \<bullet> [xvec yvec] \<bullet>\<^sub>v C
[PROOF STEP]
assume xineqx': "x \<noteq> x'"
[PROOF STATE]
proof (state)
this:
x \<noteq> x'

goal (1 subgoal):
 1. x \<noteq> x' \<Longrightarrow> x \<sharp> [(x', y)] \<bullet> [xvec yvec] \<bullet>\<^sub>v C
[PROOF STEP]
have "x mem (x' # xvec)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x mem (x' # xvec)
[PROOF STEP]
by fact
[PROOF STATE]
proof (state)
this:
x mem (x' # xvec)

goal (1 subgoal):
 1. x \<noteq> x' \<Longrightarrow> x \<sharp> [(x', y)] \<bullet> [xvec yvec] \<bullet>\<^sub>v C
[PROOF STEP]
with xineqx'
[PROOF STATE]
proof (chain)
picking this:
x \<noteq> x'
x mem (x' # xvec)
[PROOF STEP]
have xmemxvec: "x mem xvec"
[PROOF STATE]
proof (prove)
using this:
x \<noteq> x'
x mem (x' # xvec)

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

goal (1 subgoal):
 1. x \<noteq> x' \<Longrightarrow> x \<sharp> [(x', y)] \<bullet> [xvec yvec] \<bullet>\<^sub>v C
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
x mem xvec

goal (1 subgoal):
 1. x \<noteq> x' \<Longrightarrow> x \<sharp> [(x', y)] \<bullet> [xvec yvec] \<bullet>\<^sub>v C
[PROOF STEP]
have "\<lbrakk>yvec \<sharp>* C; xvec \<sharp>* yvec; x mem xvec; distinct yvec\<rbrakk> \<Longrightarrow> x \<sharp> [xvec yvec] \<bullet>\<^sub>v C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>yvec \<sharp>* C; xvec \<sharp>* yvec; x mem xvec; distinct yvec\<rbrakk> \<Longrightarrow> x \<sharp> [xvec yvec] \<bullet>\<^sub>v C
[PROOF STEP]
by fact
[PROOF STATE]
proof (state)
this:
\<lbrakk>yvec \<sharp>* C; xvec \<sharp>* yvec; x mem xvec; distinct yvec\<rbrakk> \<Longrightarrow> x \<sharp> [xvec yvec] \<bullet>\<^sub>v C

goal (1 subgoal):
 1. x \<noteq> x' \<Longrightarrow> x \<sharp> [(x', y)] \<bullet> [xvec yvec] \<bullet>\<^sub>v C
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
x mem xvec
\<lbrakk>yvec \<sharp>* C; xvec \<sharp>* yvec; x mem xvec; distinct yvec\<rbrakk> \<Longrightarrow> x \<sharp> [xvec yvec] \<bullet>\<^sub>v C
[PROOF STEP]
have "x \<sharp> [xvec yvec] \<bullet>\<^sub>v C"
[PROOF STATE]
proof (prove)
using this:
x mem xvec
\<lbrakk>yvec \<sharp>* C; xvec \<sharp>* yvec; x mem xvec; distinct yvec\<rbrakk> \<Longrightarrow> x \<sharp> [xvec yvec] \<bullet>\<^sub>v C

goal (1 subgoal):
 1. x \<sharp> [xvec yvec] \<bullet>\<^sub>v C
[PROOF STEP]
using yvecFreshp xvecFreshyvec yvecDist
[PROOF STATE]
proof (prove)
using this:
x mem xvec
\<lbrakk>yvec \<sharp>* C; xvec \<sharp>* yvec; x mem xvec; distinct yvec\<rbrakk> \<Longrightarrow> x \<sharp> [xvec yvec] \<bullet>\<^sub>v C
yvec \<sharp>* C
xvec \<sharp>* yvec
distinct yvec

goal (1 subgoal):
 1. x \<sharp> [xvec yvec] \<bullet>\<^sub>v C
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
x \<sharp> [xvec yvec] \<bullet>\<^sub>v C

goal (1 subgoal):
 1. x \<noteq> x' \<Longrightarrow> x \<sharp> [(x', y)] \<bullet> [xvec yvec] \<bullet>\<^sub>v C
[PROOF STEP]
hence "([(x', y)] \<bullet> x) \<sharp> [(x', y)] \<bullet> [xvec yvec] \<bullet>\<^sub>v C"
[PROOF STATE]
proof (prove)
using this:
x \<sharp> [xvec yvec] \<bullet>\<^sub>v C

goal (1 subgoal):
 1. [(x', y)] \<bullet> x \<sharp> [(x', y)] \<bullet> [xvec yvec] \<bullet>\<^sub>v C
[PROOF STEP]
by(rule pt_fresh_bij1[OF pt_name_inst, OF at_name_inst])
[PROOF STATE]
proof (state)
this:
[(x', y)] \<bullet> x \<sharp> [(x', y)] \<bullet> [xvec yvec] \<bullet>\<^sub>v C

goal (1 subgoal):
 1. x \<noteq> x' \<Longrightarrow> x \<sharp> [(x', y)] \<bullet> [xvec yvec] \<bullet>\<^sub>v C
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
[(x', y)] \<bullet> x \<sharp> [(x', y)] \<bullet> [xvec yvec] \<bullet>\<^sub>v C

goal (1 subgoal):
 1. x \<noteq> x' \<Longrightarrow> x \<sharp> [(x', y)] \<bullet> [xvec yvec] \<bullet>\<^sub>v C
[PROOF STEP]
from xmemxvec yFreshxvec
[PROOF STATE]
proof (chain)
picking this:
x mem xvec
y \<sharp> xvec
[PROOF STEP]
have "x \<noteq> y"
[PROOF STATE]
proof (prove)
using this:
x mem xvec
y \<sharp> xvec

goal (1 subgoal):
 1. x \<noteq> y
[PROOF STEP]
by(induct xvec) (auto simp add: fresh_list_cons)
[PROOF STATE]
proof (state)
this:
x \<noteq> y

goal (1 subgoal):
 1. x \<noteq> x' \<Longrightarrow> x \<sharp> [(x', y)] \<bullet> [xvec yvec] \<bullet>\<^sub>v C
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
[(x', y)] \<bullet> x \<sharp> [(x', y)] \<bullet> [xvec yvec] \<bullet>\<^sub>v C
x \<noteq> y
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
[(x', y)] \<bullet> x \<sharp> [(x', y)] \<bullet> [xvec yvec] \<bullet>\<^sub>v C
x \<noteq> y

goal (1 subgoal):
 1. x \<sharp> [(x', y)] \<bullet> [xvec yvec] \<bullet>\<^sub>v C
[PROOF STEP]
using xineqx' x'ineqy
[PROOF STATE]
proof (prove)
using this:
[(x', y)] \<bullet> x \<sharp> [(x', y)] \<bullet> [xvec yvec] \<bullet>\<^sub>v C
x \<noteq> y
x \<noteq> x'
x' \<noteq> y

goal (1 subgoal):
 1. x \<sharp> [(x', y)] \<bullet> [xvec yvec] \<bullet>\<^sub>v C
[PROOF STEP]
by(simp add: calc_atm)
[PROOF STATE]
proof (state)
this:
x \<sharp> [(x', y)] \<bullet> [xvec yvec] \<bullet>\<^sub>v C

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
x \<sharp> [(x', y)] \<bullet> [xvec yvec] \<bullet>\<^sub>v C

goal (1 subgoal):
 1. \<And>xa xvec y yvec. \<lbrakk>length xvec = length yvec; \<lbrakk>yvec \<sharp>* C; xvec \<sharp>* yvec; x mem xvec; distinct yvec\<rbrakk> \<Longrightarrow> x \<sharp> [xvec yvec] \<bullet>\<^sub>v C; (y # yvec) \<sharp>* C; (xa # xvec) \<sharp>* (y # yvec); x mem (xa # xvec); distinct (y # yvec)\<rbrakk> \<Longrightarrow> x \<sharp> [(xa # xvec) (y # yvec)] \<bullet>\<^sub>v C
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
x \<sharp> [(x', y)] \<bullet> [xvec yvec] \<bullet>\<^sub>v C

goal (1 subgoal):
 1. x \<sharp> [(x' # xvec) (y # yvec)] \<bullet>\<^sub>v C
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
x \<sharp> [(x' # xvec) (y # yvec)] \<bullet>\<^sub>v C

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma memFreshSimp[simp]:
  fixes y    :: name
  and   yvec :: "name list"

  shows "(\<not>(y mem yvec)) = y \<sharp> yvec"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (y \<notin> set yvec) = y \<sharp> yvec
[PROOF STEP]
by(induct yvec)
  (auto simp add: fresh_list_nil fresh_list_cons)


[STATEMENT]
lemma freshChainPerm':
  fixes xvec :: "name list"
  and   yvec :: "name list"
  and   p    :: "'a::pt_name"

  assumes "length xvec = length yvec"
  and     "yvec \<sharp>* p"
  and     "xvec \<sharp>* yvec"
  and     "distinct yvec"

  shows "xvec \<sharp>* ([xvec yvec] \<bullet>\<^sub>v p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. xvec \<sharp>* ([xvec yvec] \<bullet>\<^sub>v p)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
length xvec = length yvec
yvec \<sharp>* p
xvec \<sharp>* yvec
distinct yvec

goal (1 subgoal):
 1. xvec \<sharp>* ([xvec yvec] \<bullet>\<^sub>v p)
[PROOF STEP]
proof(induct rule: composePermInduct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>[] \<sharp>* p; [] \<sharp>* []; distinct []\<rbrakk> \<Longrightarrow> [] \<sharp>* ([[] []] \<bullet>\<^sub>v p)
 2. \<And>x xvec y yvec. \<lbrakk>length xvec = length yvec; \<lbrakk>yvec \<sharp>* p; xvec \<sharp>* yvec; distinct yvec\<rbrakk> \<Longrightarrow> xvec \<sharp>* ([xvec yvec] \<bullet>\<^sub>v p); (y # yvec) \<sharp>* p; (x # xvec) \<sharp>* (y # yvec); distinct (y # yvec)\<rbrakk> \<Longrightarrow> (x # xvec) \<sharp>* ([(x # xvec) (y # yvec)] \<bullet>\<^sub>v p)
[PROOF STEP]
case cBase
[PROOF STATE]
proof (state)
this:
[] \<sharp>* p
[] \<sharp>* []
distinct []

goal (2 subgoals):
 1. \<lbrakk>[] \<sharp>* p; [] \<sharp>* []; distinct []\<rbrakk> \<Longrightarrow> [] \<sharp>* ([[] []] \<bullet>\<^sub>v p)
 2. \<And>x xvec y yvec. \<lbrakk>length xvec = length yvec; \<lbrakk>yvec \<sharp>* p; xvec \<sharp>* yvec; distinct yvec\<rbrakk> \<Longrightarrow> xvec \<sharp>* ([xvec yvec] \<bullet>\<^sub>v p); (y # yvec) \<sharp>* p; (x # xvec) \<sharp>* (y # yvec); distinct (y # yvec)\<rbrakk> \<Longrightarrow> (x # xvec) \<sharp>* ([(x # xvec) (y # yvec)] \<bullet>\<^sub>v p)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [] \<sharp>* ([[] []] \<bullet>\<^sub>v p)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
[] \<sharp>* ([[] []] \<bullet>\<^sub>v p)

goal (1 subgoal):
 1. \<And>x xvec y yvec. \<lbrakk>length xvec = length yvec; \<lbrakk>yvec \<sharp>* p; xvec \<sharp>* yvec; distinct yvec\<rbrakk> \<Longrightarrow> xvec \<sharp>* ([xvec yvec] \<bullet>\<^sub>v p); (y # yvec) \<sharp>* p; (x # xvec) \<sharp>* (y # yvec); distinct (y # yvec)\<rbrakk> \<Longrightarrow> (x # xvec) \<sharp>* ([(x # xvec) (y # yvec)] \<bullet>\<^sub>v p)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x xvec y yvec. \<lbrakk>length xvec = length yvec; \<lbrakk>yvec \<sharp>* p; xvec \<sharp>* yvec; distinct yvec\<rbrakk> \<Longrightarrow> xvec \<sharp>* ([xvec yvec] \<bullet>\<^sub>v p); (y # yvec) \<sharp>* p; (x # xvec) \<sharp>* (y # yvec); distinct (y # yvec)\<rbrakk> \<Longrightarrow> (x # xvec) \<sharp>* ([(x # xvec) (y # yvec)] \<bullet>\<^sub>v p)
[PROOF STEP]
case(cStep x xvec y yvec)
[PROOF STATE]
proof (state)
this:
length xvec = length yvec
\<lbrakk>yvec \<sharp>* p; xvec \<sharp>* yvec; distinct yvec\<rbrakk> \<Longrightarrow> xvec \<sharp>* ([xvec yvec] \<bullet>\<^sub>v p)
(y # yvec) \<sharp>* p
(x # xvec) \<sharp>* (y # yvec)
distinct (y # yvec)

goal (1 subgoal):
 1. \<And>x xvec y yvec. \<lbrakk>length xvec = length yvec; \<lbrakk>yvec \<sharp>* p; xvec \<sharp>* yvec; distinct yvec\<rbrakk> \<Longrightarrow> xvec \<sharp>* ([xvec yvec] \<bullet>\<^sub>v p); (y # yvec) \<sharp>* p; (x # xvec) \<sharp>* (y # yvec); distinct (y # yvec)\<rbrakk> \<Longrightarrow> (x # xvec) \<sharp>* ([(x # xvec) (y # yvec)] \<bullet>\<^sub>v p)
[PROOF STEP]
have "(y # yvec) \<sharp>* p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (y # yvec) \<sharp>* p
[PROOF STEP]
by fact
[PROOF STATE]
proof (state)
this:
(y # yvec) \<sharp>* p

goal (1 subgoal):
 1. \<And>x xvec y yvec. \<lbrakk>length xvec = length yvec; \<lbrakk>yvec \<sharp>* p; xvec \<sharp>* yvec; distinct yvec\<rbrakk> \<Longrightarrow> xvec \<sharp>* ([xvec yvec] \<bullet>\<^sub>v p); (y # yvec) \<sharp>* p; (x # xvec) \<sharp>* (y # yvec); distinct (y # yvec)\<rbrakk> \<Longrightarrow> (x # xvec) \<sharp>* ([(x # xvec) (y # yvec)] \<bullet>\<^sub>v p)
[PROOF STEP]
hence yFreshp: "y \<sharp> p" and yvecFreshp: "yvec \<sharp>* p"
[PROOF STATE]
proof (prove)
using this:
(y # yvec) \<sharp>* p

goal (1 subgoal):
 1. y \<sharp> p &&& yvec \<sharp>* p
[PROOF STEP]
by simp+
[PROOF STATE]
proof (state)
this:
y \<sharp> p
yvec \<sharp>* p

goal (1 subgoal):
 1. \<And>x xvec y yvec. \<lbrakk>length xvec = length yvec; \<lbrakk>yvec \<sharp>* p; xvec \<sharp>* yvec; distinct yvec\<rbrakk> \<Longrightarrow> xvec \<sharp>* ([xvec yvec] \<bullet>\<^sub>v p); (y # yvec) \<sharp>* p; (x # xvec) \<sharp>* (y # yvec); distinct (y # yvec)\<rbrakk> \<Longrightarrow> (x # xvec) \<sharp>* ([(x # xvec) (y # yvec)] \<bullet>\<^sub>v p)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
y \<sharp> p
yvec \<sharp>* p

goal (1 subgoal):
 1. \<And>x xvec y yvec. \<lbrakk>length xvec = length yvec; \<lbrakk>yvec \<sharp>* p; xvec \<sharp>* yvec; distinct yvec\<rbrakk> \<Longrightarrow> xvec \<sharp>* ([xvec yvec] \<bullet>\<^sub>v p); (y # yvec) \<sharp>* p; (x # xvec) \<sharp>* (y # yvec); distinct (y # yvec)\<rbrakk> \<Longrightarrow> (x # xvec) \<sharp>* ([(x # xvec) (y # yvec)] \<bullet>\<^sub>v p)
[PROOF STEP]
have "(x # xvec) \<sharp>* (y # yvec)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x # xvec) \<sharp>* (y # yvec)
[PROOF STEP]
by fact
[PROOF STATE]
proof (state)
this:
(x # xvec) \<sharp>* (y # yvec)

goal (1 subgoal):
 1. \<And>x xvec y yvec. \<lbrakk>length xvec = length yvec; \<lbrakk>yvec \<sharp>* p; xvec \<sharp>* yvec; distinct yvec\<rbrakk> \<Longrightarrow> xvec \<sharp>* ([xvec yvec] \<bullet>\<^sub>v p); (y # yvec) \<sharp>* p; (x # xvec) \<sharp>* (y # yvec); distinct (y # yvec)\<rbrakk> \<Longrightarrow> (x # xvec) \<sharp>* ([(x # xvec) (y # yvec)] \<bullet>\<^sub>v p)
[PROOF STEP]
hence xineqy: "x \<noteq> y" and xvecFreshyvec: "xvec \<sharp>* yvec"
    and xFreshyvec: "x \<sharp> yvec" and yFreshxvec: "y \<sharp> xvec"
[PROOF STATE]
proof (prove)
using this:
(x # xvec) \<sharp>* (y # yvec)

goal (1 subgoal):
 1. (x \<noteq> y &&& xvec \<sharp>* yvec) &&& x \<sharp> yvec &&& y \<sharp> xvec
[PROOF STEP]
by(auto simp add: fresh_list_cons)
[PROOF STATE]
proof (state)
this:
x \<noteq> y
xvec \<sharp>* yvec
x \<sharp> yvec
y \<sharp> xvec

goal (1 subgoal):
 1. \<And>x xvec y yvec. \<lbrakk>length xvec = length yvec; \<lbrakk>yvec \<sharp>* p; xvec \<sharp>* yvec; distinct yvec\<rbrakk> \<Longrightarrow> xvec \<sharp>* ([xvec yvec] \<bullet>\<^sub>v p); (y # yvec) \<sharp>* p; (x # xvec) \<sharp>* (y # yvec); distinct (y # yvec)\<rbrakk> \<Longrightarrow> (x # xvec) \<sharp>* ([(x # xvec) (y # yvec)] \<bullet>\<^sub>v p)
[PROOF STEP]
have "distinct (y # yvec)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distinct (y # yvec)
[PROOF STEP]
by fact
[PROOF STATE]
proof (state)
this:
distinct (y # yvec)

goal (1 subgoal):
 1. \<And>x xvec y yvec. \<lbrakk>length xvec = length yvec; \<lbrakk>yvec \<sharp>* p; xvec \<sharp>* yvec; distinct yvec\<rbrakk> \<Longrightarrow> xvec \<sharp>* ([xvec yvec] \<bullet>\<^sub>v p); (y # yvec) \<sharp>* p; (x # xvec) \<sharp>* (y # yvec); distinct (y # yvec)\<rbrakk> \<Longrightarrow> (x # xvec) \<sharp>* ([(x # xvec) (y # yvec)] \<bullet>\<^sub>v p)
[PROOF STEP]
hence yFreshyvec: "y \<sharp> yvec" and yvecDist: "distinct yvec"
[PROOF STATE]
proof (prove)
using this:
distinct (y # yvec)

goal (1 subgoal):
 1. y \<sharp> yvec &&& distinct yvec
[PROOF STEP]
by simp+
[PROOF STATE]
proof (state)
this:
y \<sharp> yvec
distinct yvec

goal (1 subgoal):
 1. \<And>x xvec y yvec. \<lbrakk>length xvec = length yvec; \<lbrakk>yvec \<sharp>* p; xvec \<sharp>* yvec; distinct yvec\<rbrakk> \<Longrightarrow> xvec \<sharp>* ([xvec yvec] \<bullet>\<^sub>v p); (y # yvec) \<sharp>* p; (x # xvec) \<sharp>* (y # yvec); distinct (y # yvec)\<rbrakk> \<Longrightarrow> (x # xvec) \<sharp>* ([(x # xvec) (y # yvec)] \<bullet>\<^sub>v p)
[PROOF STEP]
have L: "length xvec = length yvec"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length xvec = length yvec
[PROOF STEP]
by fact
[PROOF STATE]
proof (state)
this:
length xvec = length yvec

goal (1 subgoal):
 1. \<And>x xvec y yvec. \<lbrakk>length xvec = length yvec; \<lbrakk>yvec \<sharp>* p; xvec \<sharp>* yvec; distinct yvec\<rbrakk> \<Longrightarrow> xvec \<sharp>* ([xvec yvec] \<bullet>\<^sub>v p); (y # yvec) \<sharp>* p; (x # xvec) \<sharp>* (y # yvec); distinct (y # yvec)\<rbrakk> \<Longrightarrow> (x # xvec) \<sharp>* ([(x # xvec) (y # yvec)] \<bullet>\<^sub>v p)
[PROOF STEP]
have "\<lbrakk>yvec \<sharp>* p; xvec \<sharp>* yvec; distinct yvec\<rbrakk> \<Longrightarrow> xvec \<sharp>* ([xvec yvec] \<bullet>\<^sub>v p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>yvec \<sharp>* p; xvec \<sharp>* yvec; distinct yvec\<rbrakk> \<Longrightarrow> xvec \<sharp>* ([xvec yvec] \<bullet>\<^sub>v p)
[PROOF STEP]
by fact
[PROOF STATE]
proof (state)
this:
\<lbrakk>yvec \<sharp>* p; xvec \<sharp>* yvec; distinct yvec\<rbrakk> \<Longrightarrow> xvec \<sharp>* ([xvec yvec] \<bullet>\<^sub>v p)

goal (1 subgoal):
 1. \<And>x xvec y yvec. \<lbrakk>length xvec = length yvec; \<lbrakk>yvec \<sharp>* p; xvec \<sharp>* yvec; distinct yvec\<rbrakk> \<Longrightarrow> xvec \<sharp>* ([xvec yvec] \<bullet>\<^sub>v p); (y # yvec) \<sharp>* p; (x # xvec) \<sharp>* (y # yvec); distinct (y # yvec)\<rbrakk> \<Longrightarrow> (x # xvec) \<sharp>* ([(x # xvec) (y # yvec)] \<bullet>\<^sub>v p)
[PROOF STEP]
with yvecFreshp xvecFreshyvec yvecDist
[PROOF STATE]
proof (chain)
picking this:
yvec \<sharp>* p
xvec \<sharp>* yvec
distinct yvec
\<lbrakk>yvec \<sharp>* p; xvec \<sharp>* yvec; distinct yvec\<rbrakk> \<Longrightarrow> xvec \<sharp>* ([xvec yvec] \<bullet>\<^sub>v p)
[PROOF STEP]
have IH: "xvec \<sharp>* ([xvec yvec] \<bullet>\<^sub>v p)"
[PROOF STATE]
proof (prove)
using this:
yvec \<sharp>* p
xvec \<sharp>* yvec
distinct yvec
\<lbrakk>yvec \<sharp>* p; xvec \<sharp>* yvec; distinct yvec\<rbrakk> \<Longrightarrow> xvec \<sharp>* ([xvec yvec] \<bullet>\<^sub>v p)

goal (1 subgoal):
 1. xvec \<sharp>* ([xvec yvec] \<bullet>\<^sub>v p)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
xvec \<sharp>* ([xvec yvec] \<bullet>\<^sub>v p)

goal (1 subgoal):
 1. \<And>x xvec y yvec. \<lbrakk>length xvec = length yvec; \<lbrakk>yvec \<sharp>* p; xvec \<sharp>* yvec; distinct yvec\<rbrakk> \<Longrightarrow> xvec \<sharp>* ([xvec yvec] \<bullet>\<^sub>v p); (y # yvec) \<sharp>* p; (x # xvec) \<sharp>* (y # yvec); distinct (y # yvec)\<rbrakk> \<Longrightarrow> (x # xvec) \<sharp>* ([(x # xvec) (y # yvec)] \<bullet>\<^sub>v p)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x # xvec) \<sharp>* ([(x # xvec) (y # yvec)] \<bullet>\<^sub>v p)
[PROOF STEP]
proof(auto)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. x \<sharp> [(x, y)] \<bullet> [xvec yvec] \<bullet>\<^sub>v p
 2. xvec \<sharp>* ([(x, y)] \<bullet> [xvec yvec] \<bullet>\<^sub>v p)
[PROOF STEP]
from L yFreshp yvecFreshp xineqy xvecFreshyvec yvecDist yFreshyvec yFreshxvec xFreshyvec
[PROOF STATE]
proof (chain)
picking this:
length xvec = length yvec
y \<sharp> p
yvec \<sharp>* p
x \<noteq> y
xvec \<sharp>* yvec
distinct yvec
y \<sharp> yvec
y \<sharp> xvec
x \<sharp> yvec
[PROOF STEP]
have "x \<sharp> [(x # xvec) (y # yvec)] \<bullet>\<^sub>v p"
[PROOF STATE]
proof (prove)
using this:
length xvec = length yvec
y \<sharp> p
yvec \<sharp>* p
x \<noteq> y
xvec \<sharp>* yvec
distinct yvec
y \<sharp> yvec
y \<sharp> xvec
x \<sharp> yvec

goal (1 subgoal):
 1. x \<sharp> [(x # xvec) (y # yvec)] \<bullet>\<^sub>v p
[PROOF STEP]
by(rule_tac freshChainPerm) (auto simp add: fresh_list_cons)
[PROOF STATE]
proof (state)
this:
x \<sharp> [(x # xvec) (y # yvec)] \<bullet>\<^sub>v p

goal (2 subgoals):
 1. x \<sharp> [(x, y)] \<bullet> [xvec yvec] \<bullet>\<^sub>v p
 2. xvec \<sharp>* ([(x, y)] \<bullet> [xvec yvec] \<bullet>\<^sub>v p)
[PROOF STEP]
thus "x \<sharp> [(x, y)] \<bullet> [xvec yvec] \<bullet>\<^sub>v p"
[PROOF STATE]
proof (prove)
using this:
x \<sharp> [(x # xvec) (y # yvec)] \<bullet>\<^sub>v p

goal (1 subgoal):
 1. x \<sharp> [(x, y)] \<bullet> [xvec yvec] \<bullet>\<^sub>v p
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
x \<sharp> [(x, y)] \<bullet> [xvec yvec] \<bullet>\<^sub>v p

goal (1 subgoal):
 1. xvec \<sharp>* ([(x, y)] \<bullet> [xvec yvec] \<bullet>\<^sub>v p)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. xvec \<sharp>* ([(x, y)] \<bullet> [xvec yvec] \<bullet>\<^sub>v p)
[PROOF STEP]
show "xvec \<sharp>* ([(x, y)] \<bullet> [xvec yvec] \<bullet>\<^sub>v p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. xvec \<sharp>* ([(x, y)] \<bullet> [xvec yvec] \<bullet>\<^sub>v p)
[PROOF STEP]
proof(case_tac "x mem xvec")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. x mem xvec \<Longrightarrow> xvec \<sharp>* ([(x, y)] \<bullet> [xvec yvec] \<bullet>\<^sub>v p)
 2. x \<notin> set xvec \<Longrightarrow> xvec \<sharp>* ([(x, y)] \<bullet> [xvec yvec] \<bullet>\<^sub>v p)
[PROOF STEP]
assume "x mem xvec"
[PROOF STATE]
proof (state)
this:
x mem xvec

goal (2 subgoals):
 1. x mem xvec \<Longrightarrow> xvec \<sharp>* ([(x, y)] \<bullet> [xvec yvec] \<bullet>\<^sub>v p)
 2. x \<notin> set xvec \<Longrightarrow> xvec \<sharp>* ([(x, y)] \<bullet> [xvec yvec] \<bullet>\<^sub>v p)
[PROOF STEP]
with L yvecFreshp xvecFreshyvec yvecDist xFreshyvec
[PROOF STATE]
proof (chain)
picking this:
length xvec = length yvec
yvec \<sharp>* p
xvec \<sharp>* yvec
distinct yvec
x \<sharp> yvec
x mem xvec
[PROOF STEP]
have"x \<sharp> [xvec yvec] \<bullet>\<^sub>v p"
[PROOF STATE]
proof (prove)
using this:
length xvec = length yvec
yvec \<sharp>* p
xvec \<sharp>* yvec
distinct yvec
x \<sharp> yvec
x mem xvec

goal (1 subgoal):
 1. x \<sharp> [xvec yvec] \<bullet>\<^sub>v p
[PROOF STEP]
by(rule_tac freshChainPerm) (auto simp add: fresh_list_cons)
[PROOF STATE]
proof (state)
this:
x \<sharp> [xvec yvec] \<bullet>\<^sub>v p

goal (2 subgoals):
 1. x mem xvec \<Longrightarrow> xvec \<sharp>* ([(x, y)] \<bullet> [xvec yvec] \<bullet>\<^sub>v p)
 2. x \<notin> set xvec \<Longrightarrow> xvec \<sharp>* ([(x, y)] \<bullet> [xvec yvec] \<bullet>\<^sub>v p)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
x \<sharp> [xvec yvec] \<bullet>\<^sub>v p

goal (2 subgoals):
 1. x mem xvec \<Longrightarrow> xvec \<sharp>* ([(x, y)] \<bullet> [xvec yvec] \<bullet>\<^sub>v p)
 2. x \<notin> set xvec \<Longrightarrow> xvec \<sharp>* ([(x, y)] \<bullet> [xvec yvec] \<bullet>\<^sub>v p)
[PROOF STEP]
from yFreshxvec yFreshyvec yFreshp L
[PROOF STATE]
proof (chain)
picking this:
y \<sharp> xvec
y \<sharp> yvec
y \<sharp> p
length xvec = length yvec
[PROOF STEP]
have "y \<sharp> [xvec yvec] \<bullet>\<^sub>v p"
[PROOF STATE]
proof (prove)
using this:
y \<sharp> xvec
y \<sharp> yvec
y \<sharp> p
length xvec = length yvec

goal (1 subgoal):
 1. y \<sharp> [xvec yvec] \<bullet>\<^sub>v p
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
y \<sharp> [xvec yvec] \<bullet>\<^sub>v p

goal (2 subgoals):
 1. x mem xvec \<Longrightarrow> xvec \<sharp>* ([(x, y)] \<bullet> [xvec yvec] \<bullet>\<^sub>v p)
 2. x \<notin> set xvec \<Longrightarrow> xvec \<sharp>* ([(x, y)] \<bullet> [xvec yvec] \<bullet>\<^sub>v p)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
x \<sharp> [xvec yvec] \<bullet>\<^sub>v p
y \<sharp> [xvec yvec] \<bullet>\<^sub>v p
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
x \<sharp> [xvec yvec] \<bullet>\<^sub>v p
y \<sharp> [xvec yvec] \<bullet>\<^sub>v p

goal (1 subgoal):
 1. xvec \<sharp>* ([(x, y)] \<bullet> [xvec yvec] \<bullet>\<^sub>v p)
[PROOF STEP]
using IH
[PROOF STATE]
proof (prove)
using this:
x \<sharp> [xvec yvec] \<bullet>\<^sub>v p
y \<sharp> [xvec yvec] \<bullet>\<^sub>v p
xvec \<sharp>* ([xvec yvec] \<bullet>\<^sub>v p)

goal (1 subgoal):
 1. xvec \<sharp>* ([(x, y)] \<bullet> [xvec yvec] \<bullet>\<^sub>v p)
[PROOF STEP]
by(subst consPerm) (simp add: perm_fresh_fresh)
[PROOF STATE]
proof (state)
this:
xvec \<sharp>* ([(x, y)] \<bullet> [xvec yvec] \<bullet>\<^sub>v p)

goal (1 subgoal):
 1. x \<notin> set xvec \<Longrightarrow> xvec \<sharp>* ([(x, y)] \<bullet> [xvec yvec] \<bullet>\<^sub>v p)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x \<notin> set xvec \<Longrightarrow> xvec \<sharp>* ([(x, y)] \<bullet> [xvec yvec] \<bullet>\<^sub>v p)
[PROOF STEP]
assume "\<not>(x mem xvec)"
[PROOF STATE]
proof (state)
this:
x \<notin> set xvec

goal (1 subgoal):
 1. x \<notin> set xvec \<Longrightarrow> xvec \<sharp>* ([(x, y)] \<bullet> [xvec yvec] \<bullet>\<^sub>v p)
[PROOF STEP]
hence xFreshxvec: "x \<sharp> xvec"
[PROOF STATE]
proof (prove)
using this:
x \<notin> set xvec

goal (1 subgoal):
 1. x \<sharp> xvec
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
x \<sharp> xvec

goal (1 subgoal):
 1. x \<notin> set xvec \<Longrightarrow> xvec \<sharp>* ([(x, y)] \<bullet> [xvec yvec] \<bullet>\<^sub>v p)
[PROOF STEP]
from IH
[PROOF STATE]
proof (chain)
picking this:
xvec \<sharp>* ([xvec yvec] \<bullet>\<^sub>v p)
[PROOF STEP]
have "([(x, y)] \<bullet> xvec) \<sharp>* ([(x, y)] \<bullet> [xvec yvec] \<bullet>\<^sub>v p)"
[PROOF STATE]
proof (prove)
using this:
xvec \<sharp>* ([xvec yvec] \<bullet>\<^sub>v p)

goal (1 subgoal):
 1. ([(x, y)] \<bullet> xvec) \<sharp>* ([(x, y)] \<bullet> [xvec yvec] \<bullet>\<^sub>v p)
[PROOF STEP]
by(simp add: pt_fresh_star_bij[OF pt_name_inst, OF at_name_inst])
[PROOF STATE]
proof (state)
this:
([(x, y)] \<bullet> xvec) \<sharp>* ([(x, y)] \<bullet> [xvec yvec] \<bullet>\<^sub>v p)

goal (1 subgoal):
 1. x \<notin> set xvec \<Longrightarrow> xvec \<sharp>* ([(x, y)] \<bullet> [xvec yvec] \<bullet>\<^sub>v p)
[PROOF STEP]
with xFreshxvec yFreshxvec
[PROOF STATE]
proof (chain)
picking this:
x \<sharp> xvec
y \<sharp> xvec
([(x, y)] \<bullet> xvec) \<sharp>* ([(x, y)] \<bullet> [xvec yvec] \<bullet>\<^sub>v p)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
x \<sharp> xvec
y \<sharp> xvec
([(x, y)] \<bullet> xvec) \<sharp>* ([(x, y)] \<bullet> [xvec yvec] \<bullet>\<^sub>v p)

goal (1 subgoal):
 1. xvec \<sharp>* ([(x, y)] \<bullet> [xvec yvec] \<bullet>\<^sub>v p)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
xvec \<sharp>* ([(x, y)] \<bullet> [xvec yvec] \<bullet>\<^sub>v p)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
xvec \<sharp>* ([(x, y)] \<bullet> [xvec yvec] \<bullet>\<^sub>v p)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(x # xvec) \<sharp>* ([(x # xvec) (y # yvec)] \<bullet>\<^sub>v p)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma permSym:
  fixes x    :: name
  and   y    :: name
  and   xvec :: "name list"
  and   yvec :: "name list"
  and   p    :: "'a::pt_name"

  assumes "x \<sharp> xvec"
  and     "x \<sharp> yvec"
  and     "y \<sharp> xvec"
  and     "y \<sharp> yvec"
  and     "length xvec = length yvec"

  shows "([(x, y)] \<bullet> [xvec yvec] \<bullet>\<^sub>v p) = [xvec yvec] \<bullet>\<^sub>v [(x, y)] \<bullet> p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [(x, y)] \<bullet> [xvec yvec] \<bullet>\<^sub>v p = [xvec yvec] \<bullet>\<^sub>v [(x, y)] \<bullet> p
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
x \<sharp> xvec
x \<sharp> yvec
y \<sharp> xvec
y \<sharp> yvec
length xvec = length yvec

goal (1 subgoal):
 1. [(x, y)] \<bullet> [xvec yvec] \<bullet>\<^sub>v p = [xvec yvec] \<bullet>\<^sub>v [(x, y)] \<bullet> p
[PROOF STEP]
apply(induct rule: composePerm.induct, auto)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>xa xs ya ys. \<lbrakk>[(x, y)] \<bullet> [xs ys] \<bullet>\<^sub>v p = [xs ys] \<bullet>\<^sub>v [(x, y)] \<bullet> p; length xs = length ys; x \<sharp> xvec; x \<sharp> yvec; y \<sharp> xvec; y \<sharp> yvec; length xvec = length yvec; x \<noteq> xa; x \<sharp> xs; x \<noteq> ya; x \<sharp> ys; y \<noteq> xa; y \<sharp> xs; y \<noteq> ya; y \<sharp> ys\<rbrakk> \<Longrightarrow> [(x, y)] \<bullet> [(xa, ya)] \<bullet> [xs ys] \<bullet>\<^sub>v p = [(xa, ya)] \<bullet> [xs ys] \<bullet>\<^sub>v [(x, y)] \<bullet> p
[PROOF STEP]
by(subst pt_perm_compose[OF pt_name_inst, OF at_name_inst]) simp


[STATEMENT]
lemma distinctPermClosed[simp]:
  fixes p :: "name prm"
  and   q :: "name prm"

  assumes "distinctPerm p"

  shows "distinctPerm(q \<bullet> p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distinctPerm (q \<bullet> p)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
distinctPerm p

goal (1 subgoal):
 1. distinctPerm (q \<bullet> p)
[PROOF STEP]
by(induct p) (auto simp add: pt_fresh_bij[OF pt_name_inst, OF at_name_inst] dest: pt_bij4[OF pt_name_inst, OF at_name_inst])


[STATEMENT]
lemma freshStarSimps:
  fixes x  :: name
  and   Xs :: "name set"
  and   Ys :: "name set"
  and   C  :: "'a::fs_name"
  and   p  :: "name prm"

  assumes "set p \<subseteq> Xs \<times> Ys"
  and     "Xs \<sharp>* x"
  and     "Ys \<sharp>* x"

  shows "x \<sharp> (p \<bullet> C) = x \<sharp> C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<sharp> p \<bullet> C = x \<sharp> C
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
set p \<subseteq> Xs \<times> Ys
Xs \<sharp>* x
Ys \<sharp>* x

goal (1 subgoal):
 1. x \<sharp> p \<bullet> C = x \<sharp> C
[PROOF STEP]
by(subst  pt_fresh_bij[OF pt_name_inst, OF at_name_inst, symmetric, of _ C p]) simp


[STATEMENT]
lemma freshStarChainSimps:
  fixes xvec :: "name list"
  and   Xs   :: "name set"
  and   Ys   :: "name set"
  and   C    :: "'a::fs_name"
  and   p    :: "name prm"

  assumes "set p \<subseteq> Xs \<times> Ys"
  and     "Xs \<sharp>* xvec"
  and     "Ys \<sharp>* xvec"

  shows   "xvec \<sharp>* (p \<bullet> C) = xvec \<sharp>* C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. xvec \<sharp>* (p \<bullet> C) = xvec \<sharp>* C
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
set p \<subseteq> Xs \<times> Ys
Xs \<sharp>* xvec
Ys \<sharp>* xvec

goal (1 subgoal):
 1. xvec \<sharp>* (p \<bullet> C) = xvec \<sharp>* C
[PROOF STEP]
by(induct xvec) (auto simp add: freshStarSimps)


[STATEMENT]
lemma permStarFresh:
  fixes xvec :: "name list"
  and   p    :: "name prm"
  and   T    :: "'a::pt_name"

  assumes "xvec \<sharp>* p"

  shows "xvec \<sharp>* (p \<bullet> T) = xvec \<sharp>* T"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. xvec \<sharp>* (p \<bullet> T) = xvec \<sharp>* T
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
xvec \<sharp>* p

goal (1 subgoal):
 1. xvec \<sharp>* (p \<bullet> T) = xvec \<sharp>* T
[PROOF STEP]
by(induct p) (auto simp add: chainFreshFresh)


[STATEMENT]
lemma swapStarFresh:
  fixes x :: name
  and   p :: "name prm"
  and   T :: "'a::pt_name"

  assumes "x \<sharp> p"

  shows "x \<sharp> (p \<bullet> T) = x \<sharp> T"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<sharp> p \<bullet> T = x \<sharp> T
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x \<sharp> p \<bullet> T = x \<sharp> T
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
x \<sharp> p
[PROOF STEP]
have "[x] \<sharp>* (p \<bullet> T) = [x] \<sharp>* T"
[PROOF STATE]
proof (prove)
using this:
x \<sharp> p

goal (1 subgoal):
 1. [x] \<sharp>* (p \<bullet> T) = [x] \<sharp>* T
[PROOF STEP]
by(rule_tac permStarFresh) auto
[PROOF STATE]
proof (state)
this:
[x] \<sharp>* (p \<bullet> T) = [x] \<sharp>* T

goal (1 subgoal):
 1. x \<sharp> p \<bullet> T = x \<sharp> T
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
[x] \<sharp>* (p \<bullet> T) = [x] \<sharp>* T

goal (1 subgoal):
 1. x \<sharp> p \<bullet> T = x \<sharp> T
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
x \<sharp> p \<bullet> T = x \<sharp> T

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma freshAlphaPerm:
  fixes xvec :: "name list"
  and   Xs   :: "name set"
  and   Ys   :: "name set"
  and   p    :: "name prm"

  assumes S: "set p \<subseteq> Xs \<times> Ys"
  and     "Xs \<sharp>* xvec"
  and     "Ys \<sharp>* xvec"

  shows "xvec \<sharp>* p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. xvec \<sharp>* p
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
set p \<subseteq> Xs \<times> Ys
Xs \<sharp>* xvec
Ys \<sharp>* xvec

goal (1 subgoal):
 1. xvec \<sharp>* p
[PROOF STEP]
apply(induct p)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>set [] \<subseteq> Xs \<times> Ys; Xs \<sharp>* xvec; Ys \<sharp>* xvec\<rbrakk> \<Longrightarrow> xvec \<sharp>* []
 2. \<And>a p. \<lbrakk>\<lbrakk>set p \<subseteq> Xs \<times> Ys; Xs \<sharp>* xvec; Ys \<sharp>* xvec\<rbrakk> \<Longrightarrow> xvec \<sharp>* p; set (a # p) \<subseteq> Xs \<times> Ys; Xs \<sharp>* xvec; Ys \<sharp>* xvec\<rbrakk> \<Longrightarrow> xvec \<sharp>* (a # p)
[PROOF STEP]
by auto (simp add: fresh_star_def fresh_def name_list_supp supp_list_nil)+


[STATEMENT]
lemma freshAlphaSwap:
  fixes x  :: name
  and   Xs :: "name set"
  and   Ys :: "name set"
  and   p  :: "name prm"

  assumes S: "set p \<subseteq> Xs \<times> Ys"
  and     "Xs \<sharp>* x"
  and     "Ys \<sharp>* x"

  shows "x \<sharp> p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<sharp> p
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x \<sharp> p
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
set p \<subseteq> Xs \<times> Ys
Xs \<sharp>* x
Ys \<sharp>* x
[PROOF STEP]
have "[x] \<sharp>* p"
[PROOF STATE]
proof (prove)
using this:
set p \<subseteq> Xs \<times> Ys
Xs \<sharp>* x
Ys \<sharp>* x

goal (1 subgoal):
 1. [x] \<sharp>* p
[PROOF STEP]
apply(rule_tac freshAlphaPerm)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>set p \<subseteq> Xs \<times> Ys; Xs \<sharp>* x; Ys \<sharp>* x\<rbrakk> \<Longrightarrow> set p \<subseteq> ?Xs3 \<times> ?Ys3
 2. \<lbrakk>set p \<subseteq> Xs \<times> Ys; Xs \<sharp>* x; Ys \<sharp>* x\<rbrakk> \<Longrightarrow> ?Xs3 \<sharp>* [x]
 3. \<lbrakk>set p \<subseteq> Xs \<times> Ys; Xs \<sharp>* x; Ys \<sharp>* x\<rbrakk> \<Longrightarrow> ?Ys3 \<sharp>* [x]
[PROOF STEP]
apply assumption
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>set p \<subseteq> Xs \<times> Ys; Xs \<sharp>* x; Ys \<sharp>* x\<rbrakk> \<Longrightarrow> Xs \<sharp>* [x]
 2. \<lbrakk>set p \<subseteq> Xs \<times> Ys; Xs \<sharp>* x; Ys \<sharp>* x\<rbrakk> \<Longrightarrow> Ys \<sharp>* [x]
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
[x] \<sharp>* p

goal (1 subgoal):
 1. x \<sharp> p
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
[x] \<sharp>* p

goal (1 subgoal):
 1. x \<sharp> p
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
x \<sharp> p

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma setToListFresh[simp]:
  fixes xvec :: "name list"
  and   C    :: "'a::fs_name"
  and   yvec :: "name list"
  and   Xs   :: "name set"
  and   x    :: name

  shows "xvec \<sharp>* (set yvec) = xvec \<sharp>* yvec"
  and   "Xs \<sharp>* (set yvec) = Xs \<sharp>* yvec"
  and   "x \<sharp> (set yvec) = x \<sharp> yvec"
  and   "set xvec \<sharp>* Xs = xvec \<sharp>* Xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (xvec \<sharp>* set yvec = xvec \<sharp>* yvec &&& Xs \<sharp>* set yvec = Xs \<sharp>* yvec) &&& x \<sharp> set yvec = x \<sharp> yvec &&& set xvec \<sharp>* Xs = xvec \<sharp>* Xs
[PROOF STEP]
by(auto simp add: fresh_star_def name_list_supp fresh_def fs_name1 at_fin_set_supp[OF at_name_inst])


[STATEMENT]
lemma get_initial_test_suite_H_set_and_finite :
shows  "{(V q)@io@[(x,y)] | q io x y . q \<in> reachable_states M \<and> io \<in> LS M q \<and> length io \<le> m - size_r M \<and> x \<in> inputs M \<and> y \<in> outputs M} \<subseteq> set (get_initial_test_suite_H V M m)"
and "finite_tree (get_initial_test_suite_H V M m)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {V q @ io @ [(x, y)] |q io x y. q \<in> reachable_states M \<and> io \<in> LS M q \<and> length io \<le> m - size_r M \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M} \<subseteq> Prefix_Tree.set (get_initial_test_suite_H V M m) &&& finite_tree (get_initial_test_suite_H V M m)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. {V q @ io @ [(x, y)] |q io x y. q \<in> reachable_states M \<and> io \<in> LS M q \<and> length io \<le> m - size_r M \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M} \<subseteq> Prefix_Tree.set (get_initial_test_suite_H V M m)
 2. finite_tree (get_initial_test_suite_H V M m)
[PROOF STEP]
define rstates where "rstates       = reachable_states_as_list M"
[PROOF STATE]
proof (state)
this:
rstates = reachable_states_as_list M

goal (2 subgoals):
 1. {V q @ io @ [(x, y)] |q io x y. q \<in> reachable_states M \<and> io \<in> LS M q \<and> length io \<le> m - size_r M \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M} \<subseteq> Prefix_Tree.set (get_initial_test_suite_H V M m)
 2. finite_tree (get_initial_test_suite_H V M m)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
rstates = reachable_states_as_list M

goal (2 subgoals):
 1. {V q @ io @ [(x, y)] |q io x y. q \<in> reachable_states M \<and> io \<in> LS M q \<and> length io \<le> m - size_r M \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M} \<subseteq> Prefix_Tree.set (get_initial_test_suite_H V M m)
 2. finite_tree (get_initial_test_suite_H V M m)
[PROOF STEP]
define n where "n             = size_r M"
[PROOF STATE]
proof (state)
this:
n = size_r M

goal (2 subgoals):
 1. {V q @ io @ [(x, y)] |q io x y. q \<in> reachable_states M \<and> io \<in> LS M q \<and> length io \<le> m - size_r M \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M} \<subseteq> Prefix_Tree.set (get_initial_test_suite_H V M m)
 2. finite_tree (get_initial_test_suite_H V M m)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
n = size_r M

goal (2 subgoals):
 1. {V q @ io @ [(x, y)] |q io x y. q \<in> reachable_states M \<and> io \<in> LS M q \<and> length io \<le> m - size_r M \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M} \<subseteq> Prefix_Tree.set (get_initial_test_suite_H V M m)
 2. finite_tree (get_initial_test_suite_H V M m)
[PROOF STEP]
define iM where "iM            = inputs_as_list M"
[PROOF STATE]
proof (state)
this:
iM = inputs_as_list M

goal (2 subgoals):
 1. {V q @ io @ [(x, y)] |q io x y. q \<in> reachable_states M \<and> io \<in> LS M q \<and> length io \<le> m - size_r M \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M} \<subseteq> Prefix_Tree.set (get_initial_test_suite_H V M m)
 2. finite_tree (get_initial_test_suite_H V M m)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
iM = inputs_as_list M

goal (2 subgoals):
 1. {V q @ io @ [(x, y)] |q io x y. q \<in> reachable_states M \<and> io \<in> LS M q \<and> length io \<le> m - size_r M \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M} \<subseteq> Prefix_Tree.set (get_initial_test_suite_H V M m)
 2. finite_tree (get_initial_test_suite_H V M m)
[PROOF STEP]
define T where "T             = from_list (concat (map (\<lambda>q . map (\<lambda>\<tau>. (V q)@\<tau>) (h_extensions M q (m-n))) rstates))"
[PROOF STATE]
proof (state)
this:
T = from_list (concat (map (\<lambda>q. map ((@) (V q)) (h_extensions M q (m - n))) rstates))

goal (2 subgoals):
 1. {V q @ io @ [(x, y)] |q io x y. q \<in> reachable_states M \<and> io \<in> LS M q \<and> length io \<le> m - size_r M \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M} \<subseteq> Prefix_Tree.set (get_initial_test_suite_H V M m)
 2. finite_tree (get_initial_test_suite_H V M m)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
rstates = reachable_states_as_list M
n = size_r M
iM = inputs_as_list M
T = from_list (concat (map (\<lambda>q. map ((@) (V q)) (h_extensions M q (m - n))) rstates))
[PROOF STEP]
have res: "get_initial_test_suite_H V M m = T"
[PROOF STATE]
proof (prove)
using this:
rstates = reachable_states_as_list M
n = size_r M
iM = inputs_as_list M
T = from_list (concat (map (\<lambda>q. map ((@) (V q)) (h_extensions M q (m - n))) rstates))

goal (1 subgoal):
 1. get_initial_test_suite_H V M m = T
[PROOF STEP]
unfolding get_initial_test_suite_H_def Let_def
[PROOF STATE]
proof (prove)
using this:
rstates = reachable_states_as_list M
n = size_r M
iM = inputs_as_list M
T = from_list (concat (map (\<lambda>q. map ((@) (V q)) (h_extensions M q (m - n))) rstates))

goal (1 subgoal):
 1. from_list (concat (map (\<lambda>q. map ((@) (V q)) (h_extensions M q (m - size_r M))) (reachable_states_as_list M))) = T
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
get_initial_test_suite_H V M m = T

goal (2 subgoals):
 1. {V q @ io @ [(x, y)] |q io x y. q \<in> reachable_states M \<and> io \<in> LS M q \<and> length io \<le> m - size_r M \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M} \<subseteq> Prefix_Tree.set (get_initial_test_suite_H V M m)
 2. finite_tree (get_initial_test_suite_H V M m)
[PROOF STEP]
define \<X> where \<X>: "\<X> = (\<lambda> q . {io@[(x,y)] | io x y . io \<in> LS M q \<and> length io \<le> m-n \<and> x \<in> inputs M \<and> y \<in> outputs M})"
[PROOF STATE]
proof (state)
this:
\<X> = (\<lambda>q. {io @ [(x, y)] |io x y. io \<in> LS M q \<and> length io \<le> m - n \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M})

goal (2 subgoals):
 1. {V q @ io @ [(x, y)] |q io x y. q \<in> reachable_states M \<and> io \<in> LS M q \<and> length io \<le> m - size_r M \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M} \<subseteq> Prefix_Tree.set (get_initial_test_suite_H V M m)
 2. finite_tree (get_initial_test_suite_H V M m)
[PROOF STEP]
have "list.set rstates = reachable_states M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. list.set rstates = reachable_states M
[PROOF STEP]
unfolding rstates_def reachable_states_as_list_set
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. reachable_states M = reachable_states M
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
list.set rstates = reachable_states M

goal (2 subgoals):
 1. {V q @ io @ [(x, y)] |q io x y. q \<in> reachable_states M \<and> io \<in> LS M q \<and> length io \<le> m - size_r M \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M} \<subseteq> Prefix_Tree.set (get_initial_test_suite_H V M m)
 2. finite_tree (get_initial_test_suite_H V M m)
[PROOF STEP]
have "{ (V q) @ \<tau> | q \<tau> . q \<in> reachable_states M \<and> \<tau> \<in> \<X> q} \<subseteq> set T"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {V q @ \<tau> |q \<tau>. q \<in> reachable_states M \<and> \<tau> \<in> \<X> q} \<subseteq> Prefix_Tree.set T
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> {V q @ \<tau> |q \<tau>. q \<in> reachable_states M \<and> \<tau> \<in> \<X> q} \<Longrightarrow> x \<in> Prefix_Tree.set T
[PROOF STEP]
fix io
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> {V q @ \<tau> |q \<tau>. q \<in> reachable_states M \<and> \<tau> \<in> \<X> q} \<Longrightarrow> x \<in> Prefix_Tree.set T
[PROOF STEP]
assume "io \<in> { (V q) @ \<tau> | q \<tau> . q \<in> reachable_states M \<and> \<tau> \<in> \<X> q}"
[PROOF STATE]
proof (state)
this:
io \<in> {V q @ \<tau> |q \<tau>. q \<in> reachable_states M \<and> \<tau> \<in> \<X> q}

goal (1 subgoal):
 1. \<And>x. x \<in> {V q @ \<tau> |q \<tau>. q \<in> reachable_states M \<and> \<tau> \<in> \<X> q} \<Longrightarrow> x \<in> Prefix_Tree.set T
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
io \<in> {V q @ \<tau> |q \<tau>. q \<in> reachable_states M \<and> \<tau> \<in> \<X> q}
[PROOF STEP]
obtain q \<tau> where "io = (V q) @ \<tau>"
                      and "q \<in> reachable_states M"
                      and "\<tau> \<in> \<X> q"
[PROOF STATE]
proof (prove)
using this:
io \<in> {V q @ \<tau> |q \<tau>. q \<in> reachable_states M \<and> \<tau> \<in> \<X> q}

goal (1 subgoal):
 1. (\<And>q \<tau>. \<lbrakk>io = V q @ \<tau>; q \<in> reachable_states M; \<tau> \<in> \<X> q\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
io = V q @ \<tau>
q \<in> reachable_states M
\<tau> \<in> \<X> q

goal (1 subgoal):
 1. \<And>x. x \<in> {V q @ \<tau> |q \<tau>. q \<in> reachable_states M \<and> \<tau> \<in> \<X> q} \<Longrightarrow> x \<in> Prefix_Tree.set T
[PROOF STEP]
have "\<tau> \<in> list.set (h_extensions M q (m - n))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<tau> \<in> list.set (h_extensions M q (m - n))
[PROOF STEP]
using \<open>\<tau> \<in> \<X> q\<close>
[PROOF STATE]
proof (prove)
using this:
\<tau> \<in> \<X> q

goal (1 subgoal):
 1. \<tau> \<in> list.set (h_extensions M q (m - n))
[PROOF STEP]
unfolding \<X>
[PROOF STATE]
proof (prove)
using this:
\<tau> \<in> {io @ [(x, y)] |io x y. io \<in> LS M q \<and> length io \<le> m - n \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M}

goal (1 subgoal):
 1. \<tau> \<in> list.set (h_extensions M q (m - n))
[PROOF STEP]
using h_extensions_set[OF reachable_state_is_state[OF \<open>q \<in> reachable_states M\<close>]]
[PROOF STATE]
proof (prove)
using this:
\<tau> \<in> {io @ [(x, y)] |io x y. io \<in> LS M q \<and> length io \<le> m - n \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M}
list.set (h_extensions M q ?k) = {io @ [(x, y)] |io x y. io \<in> LS M q \<and> length io \<le> ?k \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M}

goal (1 subgoal):
 1. \<tau> \<in> list.set (h_extensions M q (m - n))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<tau> \<in> list.set (h_extensions M q (m - n))

goal (1 subgoal):
 1. \<And>x. x \<in> {V q @ \<tau> |q \<tau>. q \<in> reachable_states M \<and> \<tau> \<in> \<X> q} \<Longrightarrow> x \<in> Prefix_Tree.set T
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<tau> \<in> list.set (h_extensions M q (m - n))
[PROOF STEP]
have "io \<in> list.set (map ((@) (V q)) (h_extensions M q (m - n)))"
[PROOF STATE]
proof (prove)
using this:
\<tau> \<in> list.set (h_extensions M q (m - n))

goal (1 subgoal):
 1. io \<in> list.set (map ((@) (V q)) (h_extensions M q (m - n)))
[PROOF STEP]
unfolding \<open>io = (V q) @ \<tau>\<close>
[PROOF STATE]
proof (prove)
using this:
\<tau> \<in> list.set (h_extensions M q (m - n))

goal (1 subgoal):
 1. V q @ \<tau> \<in> list.set (map ((@) (V q)) (h_extensions M q (m - n)))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
io \<in> list.set (map ((@) (V q)) (h_extensions M q (m - n)))

goal (1 subgoal):
 1. \<And>x. x \<in> {V q @ \<tau> |q \<tau>. q \<in> reachable_states M \<and> \<tau> \<in> \<X> q} \<Longrightarrow> x \<in> Prefix_Tree.set T
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
io \<in> list.set (map ((@) (V q)) (h_extensions M q (m - n)))

goal (1 subgoal):
 1. \<And>x. x \<in> {V q @ \<tau> |q \<tau>. q \<in> reachable_states M \<and> \<tau> \<in> \<X> q} \<Longrightarrow> x \<in> Prefix_Tree.set T
[PROOF STEP]
have "q \<in> list.set rstates"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. q \<in> list.set rstates
[PROOF STEP]
using \<open>list.set rstates = reachable_states M\<close> \<open>q \<in> reachable_states M\<close>
[PROOF STATE]
proof (prove)
using this:
list.set rstates = reachable_states M
q \<in> reachable_states M

goal (1 subgoal):
 1. q \<in> list.set rstates
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
q \<in> list.set rstates

goal (1 subgoal):
 1. \<And>x. x \<in> {V q @ \<tau> |q \<tau>. q \<in> reachable_states M \<and> \<tau> \<in> \<X> q} \<Longrightarrow> x \<in> Prefix_Tree.set T
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
io \<in> list.set (map ((@) (V q)) (h_extensions M q (m - n)))
q \<in> list.set rstates
[PROOF STEP]
have "io \<in> list.set (concat (map (\<lambda>q. map ((@) (V q)) (h_extensions M q (m - n))) rstates))"
[PROOF STATE]
proof (prove)
using this:
io \<in> list.set (map ((@) (V q)) (h_extensions M q (m - n)))
q \<in> list.set rstates

goal (1 subgoal):
 1. io \<in> list.set (concat (map (\<lambda>q. map ((@) (V q)) (h_extensions M q (m - n))) rstates))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
io \<in> list.set (concat (map (\<lambda>q. map ((@) (V q)) (h_extensions M q (m - n))) rstates))

goal (1 subgoal):
 1. \<And>x. x \<in> {V q @ \<tau> |q \<tau>. q \<in> reachable_states M \<and> \<tau> \<in> \<X> q} \<Longrightarrow> x \<in> Prefix_Tree.set T
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
io \<in> list.set (concat (map (\<lambda>q. map ((@) (V q)) (h_extensions M q (m - n))) rstates))
[PROOF STEP]
show "io \<in> set T"
[PROOF STATE]
proof (prove)
using this:
io \<in> list.set (concat (map (\<lambda>q. map ((@) (V q)) (h_extensions M q (m - n))) rstates))

goal (1 subgoal):
 1. io \<in> Prefix_Tree.set T
[PROOF STEP]
unfolding T_def from_list_set
[PROOF STATE]
proof (prove)
using this:
io \<in> list.set (concat (map (\<lambda>q. map ((@) (V q)) (h_extensions M q (m - n))) rstates))

goal (1 subgoal):
 1. io \<in> Set.insert [] {xs''. \<exists>xs' xs'''. xs' \<in> list.set (concat (map (\<lambda>q. map ((@) (V q)) (h_extensions M q (m - n))) rstates)) \<and> xs' = xs'' @ xs'''}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
io \<in> Prefix_Tree.set T

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
{V q @ \<tau> |q \<tau>. q \<in> reachable_states M \<and> \<tau> \<in> \<X> q} \<subseteq> Prefix_Tree.set T

goal (2 subgoals):
 1. {V q @ io @ [(x, y)] |q io x y. q \<in> reachable_states M \<and> io \<in> LS M q \<and> length io \<le> m - size_r M \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M} \<subseteq> Prefix_Tree.set (get_initial_test_suite_H V M m)
 2. finite_tree (get_initial_test_suite_H V M m)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
{V q @ \<tau> |q \<tau>. q \<in> reachable_states M \<and> \<tau> \<in> \<X> q} \<subseteq> Prefix_Tree.set T

goal (2 subgoals):
 1. {V q @ io @ [(x, y)] |q io x y. q \<in> reachable_states M \<and> io \<in> LS M q \<and> length io \<le> m - size_r M \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M} \<subseteq> Prefix_Tree.set (get_initial_test_suite_H V M m)
 2. finite_tree (get_initial_test_suite_H V M m)
[PROOF STEP]
have "{ (V q) @ \<tau> | q \<tau> . q \<in> reachable_states M \<and> \<tau> \<in> \<X> q} = {(V q)@io@[(x,y)] | q io x y . q \<in> reachable_states M \<and> io \<in> LS M q \<and> length io \<le> m - size_r M \<and> x \<in> inputs M \<and> y \<in> outputs M}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {V q @ \<tau> |q \<tau>. q \<in> reachable_states M \<and> \<tau> \<in> \<X> q} = {V q @ io @ [(x, y)] |q io x y. q \<in> reachable_states M \<and> io \<in> LS M q \<and> length io \<le> m - size_r M \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M}
[PROOF STEP]
unfolding \<X> n_def[symmetric]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {V q @ \<tau> |q \<tau>. q \<in> reachable_states M \<and> \<tau> \<in> {io @ [(x, y)] |io x y. io \<in> LS M q \<and> length io \<le> m - n \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M}} = {V q @ io @ [(x, y)] |q io x y. q \<in> reachable_states M \<and> io \<in> LS M q \<and> length io \<le> m - n \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M}
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
{V q @ \<tau> |q \<tau>. q \<in> reachable_states M \<and> \<tau> \<in> \<X> q} = {V q @ io @ [(x, y)] |q io x y. q \<in> reachable_states M \<and> io \<in> LS M q \<and> length io \<le> m - size_r M \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M}

goal (2 subgoals):
 1. {V q @ io @ [(x, y)] |q io x y. q \<in> reachable_states M \<and> io \<in> LS M q \<and> length io \<le> m - size_r M \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M} \<subseteq> Prefix_Tree.set (get_initial_test_suite_H V M m)
 2. finite_tree (get_initial_test_suite_H V M m)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
{V q @ \<tau> |q \<tau>. q \<in> reachable_states M \<and> \<tau> \<in> \<X> q} \<subseteq> Prefix_Tree.set T
{V q @ \<tau> |q \<tau>. q \<in> reachable_states M \<and> \<tau> \<in> \<X> q} = {V q @ io @ [(x, y)] |q io x y. q \<in> reachable_states M \<and> io \<in> LS M q \<and> length io \<le> m - size_r M \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M}
[PROOF STEP]
show "{(V q)@io@[(x,y)] | q io x y . q \<in> reachable_states M \<and> io \<in> LS M q \<and> length io \<le> m - size_r M \<and> x \<in> inputs M \<and> y \<in> outputs M} \<subseteq> set (get_initial_test_suite_H V M m)"
[PROOF STATE]
proof (prove)
using this:
{V q @ \<tau> |q \<tau>. q \<in> reachable_states M \<and> \<tau> \<in> \<X> q} \<subseteq> Prefix_Tree.set T
{V q @ \<tau> |q \<tau>. q \<in> reachable_states M \<and> \<tau> \<in> \<X> q} = {V q @ io @ [(x, y)] |q io x y. q \<in> reachable_states M \<and> io \<in> LS M q \<and> length io \<le> m - size_r M \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M}

goal (1 subgoal):
 1. {V q @ io @ [(x, y)] |q io x y. q \<in> reachable_states M \<and> io \<in> LS M q \<and> length io \<le> m - size_r M \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M} \<subseteq> Prefix_Tree.set (get_initial_test_suite_H V M m)
[PROOF STEP]
unfolding res
[PROOF STATE]
proof (prove)
using this:
{V q @ \<tau> |q \<tau>. q \<in> reachable_states M \<and> \<tau> \<in> \<X> q} \<subseteq> Prefix_Tree.set T
{V q @ \<tau> |q \<tau>. q \<in> reachable_states M \<and> \<tau> \<in> \<X> q} = {V q @ io @ [(x, y)] |q io x y. q \<in> reachable_states M \<and> io \<in> LS M q \<and> length io \<le> m - size_r M \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M}

goal (1 subgoal):
 1. {V q @ io @ [(x, y)] |q io x y. q \<in> reachable_states M \<and> io \<in> LS M q \<and> length io \<le> m - size_r M \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M} \<subseteq> Prefix_Tree.set T
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
{V q @ io @ [(x, y)] |q io x y. q \<in> reachable_states M \<and> io \<in> LS M q \<and> length io \<le> m - size_r M \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M} \<subseteq> Prefix_Tree.set (get_initial_test_suite_H V M m)

goal (1 subgoal):
 1. finite_tree (get_initial_test_suite_H V M m)
[PROOF STEP]
show "finite_tree (get_initial_test_suite_H V M m)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite_tree (get_initial_test_suite_H V M m)
[PROOF STEP]
unfolding res T_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite_tree (from_list (concat (map (\<lambda>q. map ((@) (V q)) (h_extensions M q (m - n))) rstates)))
[PROOF STEP]
using from_list_finite_tree
[PROOF STATE]
proof (prove)
using this:
finite_tree (from_list ?xs)

goal (1 subgoal):
 1. finite_tree (from_list (concat (map (\<lambda>q. map ((@) (V q)) (h_extensions M q (m - n))) rstates)))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
finite_tree (get_initial_test_suite_H V M m)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma complete_inputs_to_tree_finite_tree :
  "finite_tree (complete_inputs_to_tree M q ys xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite_tree (complete_inputs_to_tree M q ys xs)
[PROOF STEP]
proof (induction xs arbitrary: q ys)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>q ys. finite_tree (complete_inputs_to_tree M q ys [])
 2. \<And>a xs q ys. (\<And>q ys. finite_tree (complete_inputs_to_tree M q ys xs)) \<Longrightarrow> finite_tree (complete_inputs_to_tree M q ys (a # xs))
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. \<And>q ys. finite_tree (complete_inputs_to_tree M q ys [])
 2. \<And>a xs q ys. (\<And>q ys. finite_tree (complete_inputs_to_tree M q ys xs)) \<Longrightarrow> finite_tree (complete_inputs_to_tree M q ys (a # xs))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite_tree (complete_inputs_to_tree M q ys [])
[PROOF STEP]
using empty_finite_tree
[PROOF STATE]
proof (prove)
using this:
finite_tree Prefix_Tree.empty

goal (1 subgoal):
 1. finite_tree (complete_inputs_to_tree M q ys [])
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
finite_tree (complete_inputs_to_tree M q ys [])

goal (1 subgoal):
 1. \<And>a xs q ys. (\<And>q ys. finite_tree (complete_inputs_to_tree M q ys xs)) \<Longrightarrow> finite_tree (complete_inputs_to_tree M q ys (a # xs))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a xs q ys. (\<And>q ys. finite_tree (complete_inputs_to_tree M q ys xs)) \<Longrightarrow> finite_tree (complete_inputs_to_tree M q ys (a # xs))
[PROOF STEP]
case (Cons x xs)
[PROOF STATE]
proof (state)
this:
finite_tree (complete_inputs_to_tree M ?q ?ys xs)

goal (1 subgoal):
 1. \<And>a xs q ys. (\<And>q ys. finite_tree (complete_inputs_to_tree M q ys xs)) \<Longrightarrow> finite_tree (complete_inputs_to_tree M q ys (a # xs))
[PROOF STEP]
define ys' where "ys' = ys"
[PROOF STATE]
proof (state)
this:
ys' = ys

goal (1 subgoal):
 1. \<And>a xs q ys. (\<And>q ys. finite_tree (complete_inputs_to_tree M q ys xs)) \<Longrightarrow> finite_tree (complete_inputs_to_tree M q ys (a # xs))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
ys' = ys

goal (1 subgoal):
 1. \<And>a xs q ys. (\<And>q ys. finite_tree (complete_inputs_to_tree M q ys xs)) \<Longrightarrow> finite_tree (complete_inputs_to_tree M q ys (a # xs))
[PROOF STEP]
define f where "f = (\<lambda> t y . case h_obs M q x y of None \<Rightarrow> insert t [(x,y)] | Some q' \<Rightarrow> combine_after t [(x,y)] (complete_inputs_to_tree M q' ys' xs))"
[PROOF STATE]
proof (state)
this:
f = (\<lambda>t y. case FSM.h_obs M q x y of None \<Rightarrow> Prefix_Tree.insert t [(x, y)] | Some q' \<Rightarrow> combine_after t [(x, y)] (complete_inputs_to_tree M q' ys' xs))

goal (1 subgoal):
 1. \<And>a xs q ys. (\<And>q ys. finite_tree (complete_inputs_to_tree M q ys xs)) \<Longrightarrow> finite_tree (complete_inputs_to_tree M q ys (a # xs))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
ys' = ys
f = (\<lambda>t y. case FSM.h_obs M q x y of None \<Rightarrow> Prefix_Tree.insert t [(x, y)] | Some q' \<Rightarrow> combine_after t [(x, y)] (complete_inputs_to_tree M q' ys' xs))
[PROOF STEP]
have *:"complete_inputs_to_tree M q ys (x # xs)
              = foldl f Prefix_Tree.empty ys"
[PROOF STATE]
proof (prove)
using this:
ys' = ys
f = (\<lambda>t y. case FSM.h_obs M q x y of None \<Rightarrow> Prefix_Tree.insert t [(x, y)] | Some q' \<Rightarrow> combine_after t [(x, y)] (complete_inputs_to_tree M q' ys' xs))

goal (1 subgoal):
 1. complete_inputs_to_tree M q ys (x # xs) = foldl f Prefix_Tree.empty ys
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
complete_inputs_to_tree M q ys (x # xs) = foldl f Prefix_Tree.empty ys

goal (1 subgoal):
 1. \<And>a xs q ys. (\<And>q ys. finite_tree (complete_inputs_to_tree M q ys xs)) \<Longrightarrow> finite_tree (complete_inputs_to_tree M q ys (a # xs))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
complete_inputs_to_tree M q ys (x # xs) = foldl f Prefix_Tree.empty ys

goal (1 subgoal):
 1. \<And>a xs q ys. (\<And>q ys. finite_tree (complete_inputs_to_tree M q ys xs)) \<Longrightarrow> finite_tree (complete_inputs_to_tree M q ys (a # xs))
[PROOF STEP]
have "finite_tree (foldl f Prefix_Tree.empty ys)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite_tree (foldl f Prefix_Tree.empty ys)
[PROOF STEP]
proof (induction ys rule: rev_induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. finite_tree (foldl f Prefix_Tree.empty [])
 2. \<And>x xs. finite_tree (foldl f Prefix_Tree.empty xs) \<Longrightarrow> finite_tree (foldl f Prefix_Tree.empty (xs @ [x]))
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. finite_tree (foldl f Prefix_Tree.empty [])
 2. \<And>x xs. finite_tree (foldl f Prefix_Tree.empty xs) \<Longrightarrow> finite_tree (foldl f Prefix_Tree.empty (xs @ [x]))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite_tree (foldl f Prefix_Tree.empty [])
[PROOF STEP]
using empty_finite_tree
[PROOF STATE]
proof (prove)
using this:
finite_tree Prefix_Tree.empty

goal (1 subgoal):
 1. finite_tree (foldl f Prefix_Tree.empty [])
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
finite_tree (foldl f Prefix_Tree.empty [])

goal (1 subgoal):
 1. \<And>x xs. finite_tree (foldl f Prefix_Tree.empty xs) \<Longrightarrow> finite_tree (foldl f Prefix_Tree.empty (xs @ [x]))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x xs. finite_tree (foldl f Prefix_Tree.empty xs) \<Longrightarrow> finite_tree (foldl f Prefix_Tree.empty (xs @ [x]))
[PROOF STEP]
case (snoc y ys)
[PROOF STATE]
proof (state)
this:
finite_tree (foldl f Prefix_Tree.empty ys)

goal (1 subgoal):
 1. \<And>x xs. finite_tree (foldl f Prefix_Tree.empty xs) \<Longrightarrow> finite_tree (foldl f Prefix_Tree.empty (xs @ [x]))
[PROOF STEP]
define t where "t = foldl (\<lambda> t y . case h_obs M q x y of None \<Rightarrow> insert t [(x,y)] | Some q' \<Rightarrow> combine_after t [(x,y)] (complete_inputs_to_tree M q' ys' xs)) Prefix_Tree.empty ys"
[PROOF STATE]
proof (state)
this:
t = foldl (\<lambda>t y. case FSM.h_obs M q x y of None \<Rightarrow> Prefix_Tree.insert t [(x, y)] | Some q' \<Rightarrow> combine_after t [(x, y)] (complete_inputs_to_tree M q' ys' xs)) Prefix_Tree.empty ys

goal (1 subgoal):
 1. \<And>x xs. finite_tree (foldl f Prefix_Tree.empty xs) \<Longrightarrow> finite_tree (foldl f Prefix_Tree.empty (xs @ [x]))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
t = foldl (\<lambda>t y. case FSM.h_obs M q x y of None \<Rightarrow> Prefix_Tree.insert t [(x, y)] | Some q' \<Rightarrow> combine_after t [(x, y)] (complete_inputs_to_tree M q' ys' xs)) Prefix_Tree.empty ys
[PROOF STEP]
have *:"foldl f Prefix_Tree.empty (ys@[y])
                = (case h_obs M q x y of None \<Rightarrow> insert t [(x,y)] | Some q' \<Rightarrow> combine_after t [(x,y)] (complete_inputs_to_tree M q' ys' xs))"
[PROOF STATE]
proof (prove)
using this:
t = foldl (\<lambda>t y. case FSM.h_obs M q x y of None \<Rightarrow> Prefix_Tree.insert t [(x, y)] | Some q' \<Rightarrow> combine_after t [(x, y)] (complete_inputs_to_tree M q' ys' xs)) Prefix_Tree.empty ys

goal (1 subgoal):
 1. foldl f Prefix_Tree.empty (ys @ [y]) = (case FSM.h_obs M q x y of None \<Rightarrow> Prefix_Tree.insert t [(x, y)] | Some q' \<Rightarrow> combine_after t [(x, y)] (complete_inputs_to_tree M q' ys' xs))
[PROOF STEP]
unfolding f_def
[PROOF STATE]
proof (prove)
using this:
t = foldl (\<lambda>t y. case FSM.h_obs M q x y of None \<Rightarrow> Prefix_Tree.insert t [(x, y)] | Some q' \<Rightarrow> combine_after t [(x, y)] (complete_inputs_to_tree M q' ys' xs)) Prefix_Tree.empty ys

goal (1 subgoal):
 1. foldl (\<lambda>t y. case FSM.h_obs M q x y of None \<Rightarrow> Prefix_Tree.insert t [(x, y)] | Some q' \<Rightarrow> combine_after t [(x, y)] (complete_inputs_to_tree M q' ys' xs)) Prefix_Tree.empty (ys @ [y]) = (case FSM.h_obs M q x y of None \<Rightarrow> Prefix_Tree.insert t [(x, y)] | Some q' \<Rightarrow> combine_after t [(x, y)] (complete_inputs_to_tree M q' ys' xs))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
foldl f Prefix_Tree.empty (ys @ [y]) = (case FSM.h_obs M q x y of None \<Rightarrow> Prefix_Tree.insert t [(x, y)] | Some q' \<Rightarrow> combine_after t [(x, y)] (complete_inputs_to_tree M q' ys' xs))

goal (1 subgoal):
 1. \<And>x xs. finite_tree (foldl f Prefix_Tree.empty xs) \<Longrightarrow> finite_tree (foldl f Prefix_Tree.empty (xs @ [x]))
[PROOF STEP]
have "finite_tree t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite_tree t
[PROOF STEP]
using snoc
[PROOF STATE]
proof (prove)
using this:
finite_tree (foldl f Prefix_Tree.empty ys)

goal (1 subgoal):
 1. finite_tree t
[PROOF STEP]
unfolding t_def f_def
[PROOF STATE]
proof (prove)
using this:
finite_tree (foldl (\<lambda>a aa. case FSM.h_obs M q x aa of None \<Rightarrow> Prefix_Tree.insert a [(x, aa)] | Some q' \<Rightarrow> combine_after a [(x, aa)] (complete_inputs_to_tree M q' ys' xs)) Prefix_Tree.empty ys)

goal (1 subgoal):
 1. finite_tree (foldl (\<lambda>t y. case FSM.h_obs M q x y of None \<Rightarrow> Prefix_Tree.insert t [(x, y)] | Some q' \<Rightarrow> combine_after t [(x, y)] (complete_inputs_to_tree M q' ys' xs)) Prefix_Tree.empty ys)
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
finite_tree t

goal (1 subgoal):
 1. \<And>x xs. finite_tree (foldl f Prefix_Tree.empty xs) \<Longrightarrow> finite_tree (foldl f Prefix_Tree.empty (xs @ [x]))
[PROOF STEP]
have "finite_tree (insert t [(x,y)])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite_tree (Prefix_Tree.insert t [(x, y)])
[PROOF STEP]
using \<open>finite_tree t\<close> insert_finite_tree
[PROOF STATE]
proof (prove)
using this:
finite_tree t
finite_tree ?t \<Longrightarrow> finite_tree (Prefix_Tree.insert ?t ?xs)

goal (1 subgoal):
 1. finite_tree (Prefix_Tree.insert t [(x, y)])
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
finite_tree (Prefix_Tree.insert t [(x, y)])

goal (1 subgoal):
 1. \<And>x xs. finite_tree (foldl f Prefix_Tree.empty xs) \<Longrightarrow> finite_tree (foldl f Prefix_Tree.empty (xs @ [x]))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
finite_tree (Prefix_Tree.insert t [(x, y)])

goal (1 subgoal):
 1. \<And>x xs. finite_tree (foldl f Prefix_Tree.empty xs) \<Longrightarrow> finite_tree (foldl f Prefix_Tree.empty (xs @ [x]))
[PROOF STEP]
have "\<And> q' . finite_tree (combine_after t [(x,y)] (complete_inputs_to_tree M q' ys' xs))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>q'. finite_tree (combine_after t [(x, y)] (complete_inputs_to_tree M q' ys' xs))
[PROOF STEP]
using \<open>finite_tree t\<close> \<open>\<And> q ys . finite_tree (complete_inputs_to_tree M q ys xs)\<close> combine_after_finite_tree
[PROOF STATE]
proof (prove)
using this:
finite_tree t
finite_tree (complete_inputs_to_tree M ?q ?ys xs)
\<lbrakk>finite_tree ?t1.0; finite_tree ?t2.0\<rbrakk> \<Longrightarrow> finite_tree (combine_after ?t1.0 ?\<alpha> ?t2.0)

goal (1 subgoal):
 1. \<And>q'. finite_tree (combine_after t [(x, y)] (complete_inputs_to_tree M q' ys' xs))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
finite_tree (combine_after t [(x, y)] (complete_inputs_to_tree M ?q' ys' xs))

goal (1 subgoal):
 1. \<And>x xs. finite_tree (foldl f Prefix_Tree.empty xs) \<Longrightarrow> finite_tree (foldl f Prefix_Tree.empty (xs @ [x]))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
finite_tree (Prefix_Tree.insert t [(x, y)])
finite_tree (combine_after t [(x, y)] (complete_inputs_to_tree M ?q' ys' xs))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
finite_tree (Prefix_Tree.insert t [(x, y)])
finite_tree (combine_after t [(x, y)] (complete_inputs_to_tree M ?q' ys' xs))

goal (1 subgoal):
 1. finite_tree (foldl f Prefix_Tree.empty (ys @ [y]))
[PROOF STEP]
unfolding *
[PROOF STATE]
proof (prove)
using this:
finite_tree (Prefix_Tree.insert t [(x, y)])
finite_tree (combine_after t [(x, y)] (complete_inputs_to_tree M ?q' ys' xs))

goal (1 subgoal):
 1. finite_tree (case FSM.h_obs M q x y of None \<Rightarrow> Prefix_Tree.insert t [(x, y)] | Some q' \<Rightarrow> combine_after t [(x, y)] (complete_inputs_to_tree M q' ys' xs))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
finite_tree (foldl f Prefix_Tree.empty (ys @ [y]))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
finite_tree (foldl f Prefix_Tree.empty ys)

goal (1 subgoal):
 1. \<And>a xs q ys. (\<And>q ys. finite_tree (complete_inputs_to_tree M q ys xs)) \<Longrightarrow> finite_tree (complete_inputs_to_tree M q ys (a # xs))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
complete_inputs_to_tree M q ys (x # xs) = foldl f Prefix_Tree.empty ys
finite_tree (foldl f Prefix_Tree.empty ys)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
complete_inputs_to_tree M q ys (x # xs) = foldl f Prefix_Tree.empty ys
finite_tree (foldl f Prefix_Tree.empty ys)

goal (1 subgoal):
 1. finite_tree (complete_inputs_to_tree M q ys (x # xs))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
finite_tree (complete_inputs_to_tree M q ys (x # xs))

goal:
No subgoals!
[PROOF STEP]
qed