[STATEMENT]
lemma psubst_LLq[simp]:
assumes 1: "t1 \<in> atrm" "t2 \<in> atrm" "fst ` set txs \<subseteq> atrm"
and 2: "snd ` set txs \<subseteq> var"
and 3: "distinct (map snd txs)"
shows "psubst (LLq t1 t2) txs = LLq (psubstT t1 txs) (psubstT t2 txs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. psubst (LLq t1 t2) txs = LLq (psubstT t1 txs) (psubstT t2 txs)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. psubst (LLq t1 t2) txs = LLq (psubstT t1 txs) (psubstT t2 txs)
[PROOF STEP]
have 0: "t1 \<in> trm" "t2 \<in> trm" "fst ` set txs \<subseteq> trm"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. t1 \<in> trm &&& t2 \<in> trm &&& fst ` set txs \<subseteq> trm
[PROOF STEP]
using 1
[PROOF STATE]
proof (prove)
using this:
t1 \<in> atrm
t2 \<in> atrm
fst ` set txs \<subseteq> atrm

goal (1 subgoal):
 1. t1 \<in> trm &&& t2 \<in> trm &&& fst ` set txs \<subseteq> trm
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
t1 \<in> trm
t2 \<in> trm
fst ` set txs \<subseteq> trm

goal (1 subgoal):
 1. psubst (LLq t1 t2) txs = LLq (psubstT t1 txs) (psubstT t2 txs)
[PROOF STEP]
define z where z: "z \<equiv> getFr ([xx,yy] @ map snd txs) ([t1,t2] @ map fst txs) []"
[PROOF STATE]
proof (state)
this:
z \<equiv> getFr ([xx, yy] @ map snd txs) ([t1, t2] @ map fst txs) []

goal (1 subgoal):
 1. psubst (LLq t1 t2) txs = LLq (psubstT t1 txs) (psubstT t2 txs)
[PROOF STEP]
have us_facts: "z \<in> var"  "z \<noteq> xx" "z \<noteq> yy"
  "z \<notin> FvarsT t1" "z \<notin> FvarsT t2"
  "z \<notin> \<Union> (FvarsT ` (fst ` (set txs)))"
  "z \<notin> snd ` (set txs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (z \<in> var &&& z \<noteq> xx &&& z \<noteq> yy) &&& (z \<notin> FvarsT t1 &&& z \<notin> FvarsT t2) &&& z \<notin> \<Union> (FvarsT ` fst ` set txs) &&& z \<notin> snd ` set txs
[PROOF STEP]
using 0 2
[PROOF STATE]
proof (prove)
using this:
t1 \<in> trm
t2 \<in> trm
fst ` set txs \<subseteq> trm
snd ` set txs \<subseteq> var

goal (1 subgoal):
 1. (z \<in> var &&& z \<noteq> xx &&& z \<noteq> yy) &&& (z \<notin> FvarsT t1 &&& z \<notin> FvarsT t2) &&& z \<notin> \<Union> (FvarsT ` fst ` set txs) &&& z \<notin> snd ` set txs
[PROOF STEP]
unfolding z
[PROOF STATE]
proof (prove)
using this:
t1 \<in> trm
t2 \<in> trm
fst ` set txs \<subseteq> trm
snd ` set txs \<subseteq> var

goal (1 subgoal):
 1. (getFr ([xx, yy] @ map snd txs) ([t1, t2] @ map fst txs) [] \<in> var &&& getFr ([xx, yy] @ map snd txs) ([t1, t2] @ map fst txs) [] \<noteq> xx &&& getFr ([xx, yy] @ map snd txs) ([t1, t2] @ map fst txs) [] \<noteq> yy) &&& (getFr ([xx, yy] @ map snd txs) ([t1, t2] @ map fst txs) [] \<notin> FvarsT t1 &&& getFr ([xx, yy] @ map snd txs) ([t1, t2] @ map fst txs) [] \<notin> FvarsT t2) &&& getFr ([xx, yy] @ map snd txs) ([t1, t2] @ map fst txs) [] \<notin> \<Union> (FvarsT ` fst ` set txs) &&& getFr ([xx, yy] @ map snd txs) ([t1, t2] @ map fst txs) [] \<notin> snd ` set txs
[PROOF STEP]
using getFr_FvarsT[of "[xx,yy] @  map snd txs" "[t1,t2] @ map fst txs" "[]" ]
        getFr_Fvars[of "[xx,yy] @  map snd txs" "[t1,t2] @ map fst txs" "[]" ]
        getFr_var[of "[xx,yy] @  map snd txs" "[t1,t2] @ map fst txs" "[]"]
[PROOF STATE]
proof (prove)
using this:
t1 \<in> trm
t2 \<in> trm
fst ` set txs \<subseteq> trm
snd ` set txs \<subseteq> var
\<lbrakk>set ([xx, yy] @ map snd txs) \<subseteq> var; set ([t1, t2] @ map fst txs) \<subseteq> trm; set [] \<subseteq> fmla; ?t \<in> set ([t1, t2] @ map fst txs)\<rbrakk> \<Longrightarrow> getFr ([xx, yy] @ map snd txs) ([t1, t2] @ map fst txs) [] \<notin> FvarsT ?t
\<lbrakk>set ([xx, yy] @ map snd txs) \<subseteq> var; set ([t1, t2] @ map fst txs) \<subseteq> trm; set [] \<subseteq> fmla; ?\<phi> \<in> set []\<rbrakk> \<Longrightarrow> getFr ([xx, yy] @ map snd txs) ([t1, t2] @ map fst txs) [] \<notin> Fvars ?\<phi>
\<lbrakk>set ([xx, yy] @ map snd txs) \<subseteq> var; set ([t1, t2] @ map fst txs) \<subseteq> trm; set [] \<subseteq> fmla; ?t \<in> set ([t1, t2] @ map fst txs)\<rbrakk> \<Longrightarrow> getFr ([xx, yy] @ map snd txs) ([t1, t2] @ map fst txs) [] \<notin> set ([xx, yy] @ map snd txs)

goal (1 subgoal):
 1. (getFr ([xx, yy] @ map snd txs) ([t1, t2] @ map fst txs) [] \<in> var &&& getFr ([xx, yy] @ map snd txs) ([t1, t2] @ map fst txs) [] \<noteq> xx &&& getFr ([xx, yy] @ map snd txs) ([t1, t2] @ map fst txs) [] \<noteq> yy) &&& (getFr ([xx, yy] @ map snd txs) ([t1, t2] @ map fst txs) [] \<notin> FvarsT t1 &&& getFr ([xx, yy] @ map snd txs) ([t1, t2] @ map fst txs) [] \<notin> FvarsT t2) &&& getFr ([xx, yy] @ map snd txs) ([t1, t2] @ map fst txs) [] \<notin> \<Union> (FvarsT ` fst ` set txs) &&& getFr ([xx, yy] @ map snd txs) ([t1, t2] @ map fst txs) [] \<notin> snd ` set txs
[PROOF STEP]
apply -
[PROOF STATE]
proof (prove)
goal (7 subgoals):
 1. \<lbrakk>t1 \<in> trm; t2 \<in> trm; fst ` set txs \<subseteq> trm; snd ` set txs \<subseteq> var; \<And>t. \<lbrakk>set ([xx, yy] @ map snd txs) \<subseteq> var; set ([t1, t2] @ map fst txs) \<subseteq> trm; set [] \<subseteq> fmla; t \<in> set ([t1, t2] @ map fst txs)\<rbrakk> \<Longrightarrow> getFr ([xx, yy] @ map snd txs) ([t1, t2] @ map fst txs) [] \<notin> FvarsT t; \<And>\<phi>. \<lbrakk>set ([xx, yy] @ map snd txs) \<subseteq> var; set ([t1, t2] @ map fst txs) \<subseteq> trm; set [] \<subseteq> fmla; \<phi> \<in> set []\<rbrakk> \<Longrightarrow> getFr ([xx, yy] @ map snd txs) ([t1, t2] @ map fst txs) [] \<notin> Fvars \<phi>; \<And>t. \<lbrakk>set ([xx, yy] @ map snd txs) \<subseteq> var; set ([t1, t2] @ map fst txs) \<subseteq> trm; set [] \<subseteq> fmla; t \<in> set ([t1, t2] @ map fst txs)\<rbrakk> \<Longrightarrow> getFr ([xx, yy] @ map snd txs) ([t1, t2] @ map fst txs) [] \<notin> set ([xx, yy] @ map snd txs)\<rbrakk> \<Longrightarrow> getFr ([xx, yy] @ map snd txs) ([t1, t2] @ map fst txs) [] \<in> var
 2. \<lbrakk>t1 \<in> trm; t2 \<in> trm; fst ` set txs \<subseteq> trm; snd ` set txs \<subseteq> var; \<And>t. \<lbrakk>set ([xx, yy] @ map snd txs) \<subseteq> var; set ([t1, t2] @ map fst txs) \<subseteq> trm; set [] \<subseteq> fmla; t \<in> set ([t1, t2] @ map fst txs)\<rbrakk> \<Longrightarrow> getFr ([xx, yy] @ map snd txs) ([t1, t2] @ map fst txs) [] \<notin> FvarsT t; \<And>\<phi>. \<lbrakk>set ([xx, yy] @ map snd txs) \<subseteq> var; set ([t1, t2] @ map fst txs) \<subseteq> trm; set [] \<subseteq> fmla; \<phi> \<in> set []\<rbrakk> \<Longrightarrow> getFr ([xx, yy] @ map snd txs) ([t1, t2] @ map fst txs) [] \<notin> Fvars \<phi>; \<And>t. \<lbrakk>set ([xx, yy] @ map snd txs) \<subseteq> var; set ([t1, t2] @ map fst txs) \<subseteq> trm; set [] \<subseteq> fmla; t \<in> set ([t1, t2] @ map fst txs)\<rbrakk> \<Longrightarrow> getFr ([xx, yy] @ map snd txs) ([t1, t2] @ map fst txs) [] \<notin> set ([xx, yy] @ map snd txs)\<rbrakk> \<Longrightarrow> getFr ([xx, yy] @ map snd txs) ([t1, t2] @ map fst txs) [] \<noteq> xx
 3. \<lbrakk>t1 \<in> trm; t2 \<in> trm; fst ` set txs \<subseteq> trm; snd ` set txs \<subseteq> var; \<And>t. \<lbrakk>set ([xx, yy] @ map snd txs) \<subseteq> var; set ([t1, t2] @ map fst txs) \<subseteq> trm; set [] \<subseteq> fmla; t \<in> set ([t1, t2] @ map fst txs)\<rbrakk> \<Longrightarrow> getFr ([xx, yy] @ map snd txs) ([t1, t2] @ map fst txs) [] \<notin> FvarsT t; \<And>\<phi>. \<lbrakk>set ([xx, yy] @ map snd txs) \<subseteq> var; set ([t1, t2] @ map fst txs) \<subseteq> trm; set [] \<subseteq> fmla; \<phi> \<in> set []\<rbrakk> \<Longrightarrow> getFr ([xx, yy] @ map snd txs) ([t1, t2] @ map fst txs) [] \<notin> Fvars \<phi>; \<And>t. \<lbrakk>set ([xx, yy] @ map snd txs) \<subseteq> var; set ([t1, t2] @ map fst txs) \<subseteq> trm; set [] \<subseteq> fmla; t \<in> set ([t1, t2] @ map fst txs)\<rbrakk> \<Longrightarrow> getFr ([xx, yy] @ map snd txs) ([t1, t2] @ map fst txs) [] \<notin> set ([xx, yy] @ map snd txs)\<rbrakk> \<Longrightarrow> getFr ([xx, yy] @ map snd txs) ([t1, t2] @ map fst txs) [] \<noteq> yy
 4. \<lbrakk>t1 \<in> trm; t2 \<in> trm; fst ` set txs \<subseteq> trm; snd ` set txs \<subseteq> var; \<And>t. \<lbrakk>set ([xx, yy] @ map snd txs) \<subseteq> var; set ([t1, t2] @ map fst txs) \<subseteq> trm; set [] \<subseteq> fmla; t \<in> set ([t1, t2] @ map fst txs)\<rbrakk> \<Longrightarrow> getFr ([xx, yy] @ map snd txs) ([t1, t2] @ map fst txs) [] \<notin> FvarsT t; \<And>\<phi>. \<lbrakk>set ([xx, yy] @ map snd txs) \<subseteq> var; set ([t1, t2] @ map fst txs) \<subseteq> trm; set [] \<subseteq> fmla; \<phi> \<in> set []\<rbrakk> \<Longrightarrow> getFr ([xx, yy] @ map snd txs) ([t1, t2] @ map fst txs) [] \<notin> Fvars \<phi>; \<And>t. \<lbrakk>set ([xx, yy] @ map snd txs) \<subseteq> var; set ([t1, t2] @ map fst txs) \<subseteq> trm; set [] \<subseteq> fmla; t \<in> set ([t1, t2] @ map fst txs)\<rbrakk> \<Longrightarrow> getFr ([xx, yy] @ map snd txs) ([t1, t2] @ map fst txs) [] \<notin> set ([xx, yy] @ map snd txs)\<rbrakk> \<Longrightarrow> getFr ([xx, yy] @ map snd txs) ([t1, t2] @ map fst txs) [] \<notin> FvarsT t1
 5. \<lbrakk>t1 \<in> trm; t2 \<in> trm; fst ` set txs \<subseteq> trm; snd ` set txs \<subseteq> var; \<And>t. \<lbrakk>set ([xx, yy] @ map snd txs) \<subseteq> var; set ([t1, t2] @ map fst txs) \<subseteq> trm; set [] \<subseteq> fmla; t \<in> set ([t1, t2] @ map fst txs)\<rbrakk> \<Longrightarrow> getFr ([xx, yy] @ map snd txs) ([t1, t2] @ map fst txs) [] \<notin> FvarsT t; \<And>\<phi>. \<lbrakk>set ([xx, yy] @ map snd txs) \<subseteq> var; set ([t1, t2] @ map fst txs) \<subseteq> trm; set [] \<subseteq> fmla; \<phi> \<in> set []\<rbrakk> \<Longrightarrow> getFr ([xx, yy] @ map snd txs) ([t1, t2] @ map fst txs) [] \<notin> Fvars \<phi>; \<And>t. \<lbrakk>set ([xx, yy] @ map snd txs) \<subseteq> var; set ([t1, t2] @ map fst txs) \<subseteq> trm; set [] \<subseteq> fmla; t \<in> set ([t1, t2] @ map fst txs)\<rbrakk> \<Longrightarrow> getFr ([xx, yy] @ map snd txs) ([t1, t2] @ map fst txs) [] \<notin> set ([xx, yy] @ map snd txs)\<rbrakk> \<Longrightarrow> getFr ([xx, yy] @ map snd txs) ([t1, t2] @ map fst txs) [] \<notin> FvarsT t2
 6. \<lbrakk>t1 \<in> trm; t2 \<in> trm; fst ` set txs \<subseteq> trm; snd ` set txs \<subseteq> var; \<And>t. \<lbrakk>set ([xx, yy] @ map snd txs) \<subseteq> var; set ([t1, t2] @ map fst txs) \<subseteq> trm; set [] \<subseteq> fmla; t \<in> set ([t1, t2] @ map fst txs)\<rbrakk> \<Longrightarrow> getFr ([xx, yy] @ map snd txs) ([t1, t2] @ map fst txs) [] \<notin> FvarsT t; \<And>\<phi>. \<lbrakk>set ([xx, yy] @ map snd txs) \<subseteq> var; set ([t1, t2] @ map fst txs) \<subseteq> trm; set [] \<subseteq> fmla; \<phi> \<in> set []\<rbrakk> \<Longrightarrow> getFr ([xx, yy] @ map snd txs) ([t1, t2] @ map fst txs) [] \<notin> Fvars \<phi>; \<And>t. \<lbrakk>set ([xx, yy] @ map snd txs) \<subseteq> var; set ([t1, t2] @ map fst txs) \<subseteq> trm; set [] \<subseteq> fmla; t \<in> set ([t1, t2] @ map fst txs)\<rbrakk> \<Longrightarrow> getFr ([xx, yy] @ map snd txs) ([t1, t2] @ map fst txs) [] \<notin> set ([xx, yy] @ map snd txs)\<rbrakk> \<Longrightarrow> getFr ([xx, yy] @ map snd txs) ([t1, t2] @ map fst txs) [] \<notin> \<Union> (FvarsT ` fst ` set txs)
 7. \<lbrakk>t1 \<in> trm; t2 \<in> trm; fst ` set txs \<subseteq> trm; snd ` set txs \<subseteq> var; \<And>t. \<lbrakk>set ([xx, yy] @ map snd txs) \<subseteq> var; set ([t1, t2] @ map fst txs) \<subseteq> trm; set [] \<subseteq> fmla; t \<in> set ([t1, t2] @ map fst txs)\<rbrakk> \<Longrightarrow> getFr ([xx, yy] @ map snd txs) ([t1, t2] @ map fst txs) [] \<notin> FvarsT t; \<And>\<phi>. \<lbrakk>set ([xx, yy] @ map snd txs) \<subseteq> var; set ([t1, t2] @ map fst txs) \<subseteq> trm; set [] \<subseteq> fmla; \<phi> \<in> set []\<rbrakk> \<Longrightarrow> getFr ([xx, yy] @ map snd txs) ([t1, t2] @ map fst txs) [] \<notin> Fvars \<phi>; \<And>t. \<lbrakk>set ([xx, yy] @ map snd txs) \<subseteq> var; set ([t1, t2] @ map fst txs) \<subseteq> trm; set [] \<subseteq> fmla; t \<in> set ([t1, t2] @ map fst txs)\<rbrakk> \<Longrightarrow> getFr ([xx, yy] @ map snd txs) ([t1, t2] @ map fst txs) [] \<notin> set ([xx, yy] @ map snd txs)\<rbrakk> \<Longrightarrow> getFr ([xx, yy] @ map snd txs) ([t1, t2] @ map fst txs) [] \<notin> snd ` set txs
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>t1 \<in> trm; t2 \<in> trm; fst ` set txs \<subseteq> trm; snd ` set txs \<subseteq> var; \<And>t. \<lbrakk>set ([xx, yy] @ map snd txs) \<subseteq> var; set ([t1, t2] @ map fst txs) \<subseteq> trm; set [] \<subseteq> fmla; t \<in> set ([t1, t2] @ map fst txs)\<rbrakk> \<Longrightarrow> getFr ([xx, yy] @ map snd txs) ([t1, t2] @ map fst txs) [] \<notin> FvarsT t; \<And>\<phi>. \<lbrakk>set ([xx, yy] @ map snd txs) \<subseteq> var; set ([t1, t2] @ map fst txs) \<subseteq> trm; set [] \<subseteq> fmla; \<phi> \<in> set []\<rbrakk> \<Longrightarrow> getFr ([xx, yy] @ map snd txs) ([t1, t2] @ map fst txs) [] \<notin> Fvars \<phi>; \<And>t. \<lbrakk>set ([xx, yy] @ map snd txs) \<subseteq> var; set ([t1, t2] @ map fst txs) \<subseteq> trm; set [] \<subseteq> fmla; t \<in> set ([t1, t2] @ map fst txs)\<rbrakk> \<Longrightarrow> getFr ([xx, yy] @ map snd txs) ([t1, t2] @ map fst txs) [] \<notin> set ([xx, yy] @ map snd txs)\<rbrakk> \<Longrightarrow> getFr ([xx, yy] @ map snd txs) ([t1, t2] @ map fst txs) [] \<in> var
[PROOF STEP]
by auto
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<lbrakk>t1 \<in> trm; t2 \<in> trm; fst ` set txs \<subseteq> trm; snd ` set txs \<subseteq> var; \<And>t. \<lbrakk>set ([xx, yy] @ map snd txs) \<subseteq> var; set ([t1, t2] @ map fst txs) \<subseteq> trm; set [] \<subseteq> fmla; t \<in> set ([t1, t2] @ map fst txs)\<rbrakk> \<Longrightarrow> getFr ([xx, yy] @ map snd txs) ([t1, t2] @ map fst txs) [] \<notin> FvarsT t; \<And>\<phi>. \<lbrakk>set ([xx, yy] @ map snd txs) \<subseteq> var; set ([t1, t2] @ map fst txs) \<subseteq> trm; set [] \<subseteq> fmla; \<phi> \<in> set []\<rbrakk> \<Longrightarrow> getFr ([xx, yy] @ map snd txs) ([t1, t2] @ map fst txs) [] \<notin> Fvars \<phi>; \<And>t. \<lbrakk>set ([xx, yy] @ map snd txs) \<subseteq> var; set ([t1, t2] @ map fst txs) \<subseteq> trm; set [] \<subseteq> fmla; t \<in> set ([t1, t2] @ map fst txs)\<rbrakk> \<Longrightarrow> getFr ([xx, yy] @ map snd txs) ([t1, t2] @ map fst txs) [] \<notin> set ([xx, yy] @ map snd txs)\<rbrakk> \<Longrightarrow> getFr ([xx, yy] @ map snd txs) ([t1, t2] @ map fst txs) [] \<noteq> xx
 2. \<lbrakk>t1 \<in> trm; t2 \<in> trm; fst ` set txs \<subseteq> trm; snd ` set txs \<subseteq> var; \<And>t. \<lbrakk>set ([xx, yy] @ map snd txs) \<subseteq> var; set ([t1, t2] @ map fst txs) \<subseteq> trm; set [] \<subseteq> fmla; t \<in> set ([t1, t2] @ map fst txs)\<rbrakk> \<Longrightarrow> getFr ([xx, yy] @ map snd txs) ([t1, t2] @ map fst txs) [] \<notin> FvarsT t; \<And>\<phi>. \<lbrakk>set ([xx, yy] @ map snd txs) \<subseteq> var; set ([t1, t2] @ map fst txs) \<subseteq> trm; set [] \<subseteq> fmla; \<phi> \<in> set []\<rbrakk> \<Longrightarrow> getFr ([xx, yy] @ map snd txs) ([t1, t2] @ map fst txs) [] \<notin> Fvars \<phi>; \<And>t. \<lbrakk>set ([xx, yy] @ map snd txs) \<subseteq> var; set ([t1, t2] @ map fst txs) \<subseteq> trm; set [] \<subseteq> fmla; t \<in> set ([t1, t2] @ map fst txs)\<rbrakk> \<Longrightarrow> getFr ([xx, yy] @ map snd txs) ([t1, t2] @ map fst txs) [] \<notin> set ([xx, yy] @ map snd txs)\<rbrakk> \<Longrightarrow> getFr ([xx, yy] @ map snd txs) ([t1, t2] @ map fst txs) [] \<noteq> yy
 3. \<lbrakk>t1 \<in> trm; t2 \<in> trm; fst ` set txs \<subseteq> trm; snd ` set txs \<subseteq> var; \<And>t. \<lbrakk>set ([xx, yy] @ map snd txs) \<subseteq> var; set ([t1, t2] @ map fst txs) \<subseteq> trm; set [] \<subseteq> fmla; t \<in> set ([t1, t2] @ map fst txs)\<rbrakk> \<Longrightarrow> getFr ([xx, yy] @ map snd txs) ([t1, t2] @ map fst txs) [] \<notin> FvarsT t; \<And>\<phi>. \<lbrakk>set ([xx, yy] @ map snd txs) \<subseteq> var; set ([t1, t2] @ map fst txs) \<subseteq> trm; set [] \<subseteq> fmla; \<phi> \<in> set []\<rbrakk> \<Longrightarrow> getFr ([xx, yy] @ map snd txs) ([t1, t2] @ map fst txs) [] \<notin> Fvars \<phi>; \<And>t. \<lbrakk>set ([xx, yy] @ map snd txs) \<subseteq> var; set ([t1, t2] @ map fst txs) \<subseteq> trm; set [] \<subseteq> fmla; t \<in> set ([t1, t2] @ map fst txs)\<rbrakk> \<Longrightarrow> getFr ([xx, yy] @ map snd txs) ([t1, t2] @ map fst txs) [] \<notin> set ([xx, yy] @ map snd txs)\<rbrakk> \<Longrightarrow> getFr ([xx, yy] @ map snd txs) ([t1, t2] @ map fst txs) [] \<notin> FvarsT t1
 4. \<lbrakk>t1 \<in> trm; t2 \<in> trm; fst ` set txs \<subseteq> trm; snd ` set txs \<subseteq> var; \<And>t. \<lbrakk>set ([xx, yy] @ map snd txs) \<subseteq> var; set ([t1, t2] @ map fst txs) \<subseteq> trm; set [] \<subseteq> fmla; t \<in> set ([t1, t2] @ map fst txs)\<rbrakk> \<Longrightarrow> getFr ([xx, yy] @ map snd txs) ([t1, t2] @ map fst txs) [] \<notin> FvarsT t; \<And>\<phi>. \<lbrakk>set ([xx, yy] @ map snd txs) \<subseteq> var; set ([t1, t2] @ map fst txs) \<subseteq> trm; set [] \<subseteq> fmla; \<phi> \<in> set []\<rbrakk> \<Longrightarrow> getFr ([xx, yy] @ map snd txs) ([t1, t2] @ map fst txs) [] \<notin> Fvars \<phi>; \<And>t. \<lbrakk>set ([xx, yy] @ map snd txs) \<subseteq> var; set ([t1, t2] @ map fst txs) \<subseteq> trm; set [] \<subseteq> fmla; t \<in> set ([t1, t2] @ map fst txs)\<rbrakk> \<Longrightarrow> getFr ([xx, yy] @ map snd txs) ([t1, t2] @ map fst txs) [] \<notin> set ([xx, yy] @ map snd txs)\<rbrakk> \<Longrightarrow> getFr ([xx, yy] @ map snd txs) ([t1, t2] @ map fst txs) [] \<notin> FvarsT t2
 5. \<lbrakk>t1 \<in> trm; t2 \<in> trm; fst ` set txs \<subseteq> trm; snd ` set txs \<subseteq> var; \<And>t. \<lbrakk>set ([xx, yy] @ map snd txs) \<subseteq> var; set ([t1, t2] @ map fst txs) \<subseteq> trm; set [] \<subseteq> fmla; t \<in> set ([t1, t2] @ map fst txs)\<rbrakk> \<Longrightarrow> getFr ([xx, yy] @ map snd txs) ([t1, t2] @ map fst txs) [] \<notin> FvarsT t; \<And>\<phi>. \<lbrakk>set ([xx, yy] @ map snd txs) \<subseteq> var; set ([t1, t2] @ map fst txs) \<subseteq> trm; set [] \<subseteq> fmla; \<phi> \<in> set []\<rbrakk> \<Longrightarrow> getFr ([xx, yy] @ map snd txs) ([t1, t2] @ map fst txs) [] \<notin> Fvars \<phi>; \<And>t. \<lbrakk>set ([xx, yy] @ map snd txs) \<subseteq> var; set ([t1, t2] @ map fst txs) \<subseteq> trm; set [] \<subseteq> fmla; t \<in> set ([t1, t2] @ map fst txs)\<rbrakk> \<Longrightarrow> getFr ([xx, yy] @ map snd txs) ([t1, t2] @ map fst txs) [] \<notin> set ([xx, yy] @ map snd txs)\<rbrakk> \<Longrightarrow> getFr ([xx, yy] @ map snd txs) ([t1, t2] @ map fst txs) [] \<notin> \<Union> (FvarsT ` fst ` set txs)
 6. \<lbrakk>t1 \<in> trm; t2 \<in> trm; fst ` set txs \<subseteq> trm; snd ` set txs \<subseteq> var; \<And>t. \<lbrakk>set ([xx, yy] @ map snd txs) \<subseteq> var; set ([t1, t2] @ map fst txs) \<subseteq> trm; set [] \<subseteq> fmla; t \<in> set ([t1, t2] @ map fst txs)\<rbrakk> \<Longrightarrow> getFr ([xx, yy] @ map snd txs) ([t1, t2] @ map fst txs) [] \<notin> FvarsT t; \<And>\<phi>. \<lbrakk>set ([xx, yy] @ map snd txs) \<subseteq> var; set ([t1, t2] @ map fst txs) \<subseteq> trm; set [] \<subseteq> fmla; \<phi> \<in> set []\<rbrakk> \<Longrightarrow> getFr ([xx, yy] @ map snd txs) ([t1, t2] @ map fst txs) [] \<notin> Fvars \<phi>; \<And>t. \<lbrakk>set ([xx, yy] @ map snd txs) \<subseteq> var; set ([t1, t2] @ map fst txs) \<subseteq> trm; set [] \<subseteq> fmla; t \<in> set ([t1, t2] @ map fst txs)\<rbrakk> \<Longrightarrow> getFr ([xx, yy] @ map snd txs) ([t1, t2] @ map fst txs) [] \<notin> set ([xx, yy] @ map snd txs)\<rbrakk> \<Longrightarrow> getFr ([xx, yy] @ map snd txs) ([t1, t2] @ map fst txs) [] \<notin> snd ` set txs
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>t1 \<in> trm; t2 \<in> trm; fst ` set txs \<subseteq> trm; snd ` set txs \<subseteq> var; \<And>t. \<lbrakk>set ([xx, yy] @ map snd txs) \<subseteq> var; set ([t1, t2] @ map fst txs) \<subseteq> trm; set [] \<subseteq> fmla; t \<in> set ([t1, t2] @ map fst txs)\<rbrakk> \<Longrightarrow> getFr ([xx, yy] @ map snd txs) ([t1, t2] @ map fst txs) [] \<notin> FvarsT t; \<And>\<phi>. \<lbrakk>set ([xx, yy] @ map snd txs) \<subseteq> var; set ([t1, t2] @ map fst txs) \<subseteq> trm; set [] \<subseteq> fmla; \<phi> \<in> set []\<rbrakk> \<Longrightarrow> getFr ([xx, yy] @ map snd txs) ([t1, t2] @ map fst txs) [] \<notin> Fvars \<phi>; \<And>t. \<lbrakk>set ([xx, yy] @ map snd txs) \<subseteq> var; set ([t1, t2] @ map fst txs) \<subseteq> trm; set [] \<subseteq> fmla; t \<in> set ([t1, t2] @ map fst txs)\<rbrakk> \<Longrightarrow> getFr ([xx, yy] @ map snd txs) ([t1, t2] @ map fst txs) [] \<notin> set ([xx, yy] @ map snd txs)\<rbrakk> \<Longrightarrow> getFr ([xx, yy] @ map snd txs) ([t1, t2] @ map fst txs) [] \<noteq> xx
[PROOF STEP]
by force
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<lbrakk>t1 \<in> trm; t2 \<in> trm; fst ` set txs \<subseteq> trm; snd ` set txs \<subseteq> var; \<And>t. \<lbrakk>set ([xx, yy] @ map snd txs) \<subseteq> var; set ([t1, t2] @ map fst txs) \<subseteq> trm; set [] \<subseteq> fmla; t \<in> set ([t1, t2] @ map fst txs)\<rbrakk> \<Longrightarrow> getFr ([xx, yy] @ map snd txs) ([t1, t2] @ map fst txs) [] \<notin> FvarsT t; \<And>\<phi>. \<lbrakk>set ([xx, yy] @ map snd txs) \<subseteq> var; set ([t1, t2] @ map fst txs) \<subseteq> trm; set [] \<subseteq> fmla; \<phi> \<in> set []\<rbrakk> \<Longrightarrow> getFr ([xx, yy] @ map snd txs) ([t1, t2] @ map fst txs) [] \<notin> Fvars \<phi>; \<And>t. \<lbrakk>set ([xx, yy] @ map snd txs) \<subseteq> var; set ([t1, t2] @ map fst txs) \<subseteq> trm; set [] \<subseteq> fmla; t \<in> set ([t1, t2] @ map fst txs)\<rbrakk> \<Longrightarrow> getFr ([xx, yy] @ map snd txs) ([t1, t2] @ map fst txs) [] \<notin> set ([xx, yy] @ map snd txs)\<rbrakk> \<Longrightarrow> getFr ([xx, yy] @ map snd txs) ([t1, t2] @ map fst txs) [] \<noteq> yy
 2. \<lbrakk>t1 \<in> trm; t2 \<in> trm; fst ` set txs \<subseteq> trm; snd ` set txs \<subseteq> var; \<And>t. \<lbrakk>set ([xx, yy] @ map snd txs) \<subseteq> var; set ([t1, t2] @ map fst txs) \<subseteq> trm; set [] \<subseteq> fmla; t \<in> set ([t1, t2] @ map fst txs)\<rbrakk> \<Longrightarrow> getFr ([xx, yy] @ map snd txs) ([t1, t2] @ map fst txs) [] \<notin> FvarsT t; \<And>\<phi>. \<lbrakk>set ([xx, yy] @ map snd txs) \<subseteq> var; set ([t1, t2] @ map fst txs) \<subseteq> trm; set [] \<subseteq> fmla; \<phi> \<in> set []\<rbrakk> \<Longrightarrow> getFr ([xx, yy] @ map snd txs) ([t1, t2] @ map fst txs) [] \<notin> Fvars \<phi>; \<And>t. \<lbrakk>set ([xx, yy] @ map snd txs) \<subseteq> var; set ([t1, t2] @ map fst txs) \<subseteq> trm; set [] \<subseteq> fmla; t \<in> set ([t1, t2] @ map fst txs)\<rbrakk> \<Longrightarrow> getFr ([xx, yy] @ map snd txs) ([t1, t2] @ map fst txs) [] \<notin> set ([xx, yy] @ map snd txs)\<rbrakk> \<Longrightarrow> getFr ([xx, yy] @ map snd txs) ([t1, t2] @ map fst txs) [] \<notin> FvarsT t1
 3. \<lbrakk>t1 \<in> trm; t2 \<in> trm; fst ` set txs \<subseteq> trm; snd ` set txs \<subseteq> var; \<And>t. \<lbrakk>set ([xx, yy] @ map snd txs) \<subseteq> var; set ([t1, t2] @ map fst txs) \<subseteq> trm; set [] \<subseteq> fmla; t \<in> set ([t1, t2] @ map fst txs)\<rbrakk> \<Longrightarrow> getFr ([xx, yy] @ map snd txs) ([t1, t2] @ map fst txs) [] \<notin> FvarsT t; \<And>\<phi>. \<lbrakk>set ([xx, yy] @ map snd txs) \<subseteq> var; set ([t1, t2] @ map fst txs) \<subseteq> trm; set [] \<subseteq> fmla; \<phi> \<in> set []\<rbrakk> \<Longrightarrow> getFr ([xx, yy] @ map snd txs) ([t1, t2] @ map fst txs) [] \<notin> Fvars \<phi>; \<And>t. \<lbrakk>set ([xx, yy] @ map snd txs) \<subseteq> var; set ([t1, t2] @ map fst txs) \<subseteq> trm; set [] \<subseteq> fmla; t \<in> set ([t1, t2] @ map fst txs)\<rbrakk> \<Longrightarrow> getFr ([xx, yy] @ map snd txs) ([t1, t2] @ map fst txs) [] \<notin> set ([xx, yy] @ map snd txs)\<rbrakk> \<Longrightarrow> getFr ([xx, yy] @ map snd txs) ([t1, t2] @ map fst txs) [] \<notin> FvarsT t2
 4. \<lbrakk>t1 \<in> trm; t2 \<in> trm; fst ` set txs \<subseteq> trm; snd ` set txs \<subseteq> var; \<And>t. \<lbrakk>set ([xx, yy] @ map snd txs) \<subseteq> var; set ([t1, t2] @ map fst txs) \<subseteq> trm; set [] \<subseteq> fmla; t \<in> set ([t1, t2] @ map fst txs)\<rbrakk> \<Longrightarrow> getFr ([xx, yy] @ map snd txs) ([t1, t2] @ map fst txs) [] \<notin> FvarsT t; \<And>\<phi>. \<lbrakk>set ([xx, yy] @ map snd txs) \<subseteq> var; set ([t1, t2] @ map fst txs) \<subseteq> trm; set [] \<subseteq> fmla; \<phi> \<in> set []\<rbrakk> \<Longrightarrow> getFr ([xx, yy] @ map snd txs) ([t1, t2] @ map fst txs) [] \<notin> Fvars \<phi>; \<And>t. \<lbrakk>set ([xx, yy] @ map snd txs) \<subseteq> var; set ([t1, t2] @ map fst txs) \<subseteq> trm; set [] \<subseteq> fmla; t \<in> set ([t1, t2] @ map fst txs)\<rbrakk> \<Longrightarrow> getFr ([xx, yy] @ map snd txs) ([t1, t2] @ map fst txs) [] \<notin> set ([xx, yy] @ map snd txs)\<rbrakk> \<Longrightarrow> getFr ([xx, yy] @ map snd txs) ([t1, t2] @ map fst txs) [] \<notin> \<Union> (FvarsT ` fst ` set txs)
 5. \<lbrakk>t1 \<in> trm; t2 \<in> trm; fst ` set txs \<subseteq> trm; snd ` set txs \<subseteq> var; \<And>t. \<lbrakk>set ([xx, yy] @ map snd txs) \<subseteq> var; set ([t1, t2] @ map fst txs) \<subseteq> trm; set [] \<subseteq> fmla; t \<in> set ([t1, t2] @ map fst txs)\<rbrakk> \<Longrightarrow> getFr ([xx, yy] @ map snd txs) ([t1, t2] @ map fst txs) [] \<notin> FvarsT t; \<And>\<phi>. \<lbrakk>set ([xx, yy] @ map snd txs) \<subseteq> var; set ([t1, t2] @ map fst txs) \<subseteq> trm; set [] \<subseteq> fmla; \<phi> \<in> set []\<rbrakk> \<Longrightarrow> getFr ([xx, yy] @ map snd txs) ([t1, t2] @ map fst txs) [] \<notin> Fvars \<phi>; \<And>t. \<lbrakk>set ([xx, yy] @ map snd txs) \<subseteq> var; set ([t1, t2] @ map fst txs) \<subseteq> trm; set [] \<subseteq> fmla; t \<in> set ([t1, t2] @ map fst txs)\<rbrakk> \<Longrightarrow> getFr ([xx, yy] @ map snd txs) ([t1, t2] @ map fst txs) [] \<notin> set ([xx, yy] @ map snd txs)\<rbrakk> \<Longrightarrow> getFr ([xx, yy] @ map snd txs) ([t1, t2] @ map fst txs) [] \<notin> snd ` set txs
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>t1 \<in> trm; t2 \<in> trm; fst ` set txs \<subseteq> trm; snd ` set txs \<subseteq> var; \<And>t. \<lbrakk>set ([xx, yy] @ map snd txs) \<subseteq> var; set ([t1, t2] @ map fst txs) \<subseteq> trm; set [] \<subseteq> fmla; t \<in> set ([t1, t2] @ map fst txs)\<rbrakk> \<Longrightarrow> getFr ([xx, yy] @ map snd txs) ([t1, t2] @ map fst txs) [] \<notin> FvarsT t; \<And>\<phi>. \<lbrakk>set ([xx, yy] @ map snd txs) \<subseteq> var; set ([t1, t2] @ map fst txs) \<subseteq> trm; set [] \<subseteq> fmla; \<phi> \<in> set []\<rbrakk> \<Longrightarrow> getFr ([xx, yy] @ map snd txs) ([t1, t2] @ map fst txs) [] \<notin> Fvars \<phi>; \<And>t. \<lbrakk>set ([xx, yy] @ map snd txs) \<subseteq> var; set ([t1, t2] @ map fst txs) \<subseteq> trm; set [] \<subseteq> fmla; t \<in> set ([t1, t2] @ map fst txs)\<rbrakk> \<Longrightarrow> getFr ([xx, yy] @ map snd txs) ([t1, t2] @ map fst txs) [] \<notin> set ([xx, yy] @ map snd txs)\<rbrakk> \<Longrightarrow> getFr ([xx, yy] @ map snd txs) ([t1, t2] @ map fst txs) [] \<noteq> yy
[PROOF STEP]
by force
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<lbrakk>t1 \<in> trm; t2 \<in> trm; fst ` set txs \<subseteq> trm; snd ` set txs \<subseteq> var; \<And>t. \<lbrakk>set ([xx, yy] @ map snd txs) \<subseteq> var; set ([t1, t2] @ map fst txs) \<subseteq> trm; set [] \<subseteq> fmla; t \<in> set ([t1, t2] @ map fst txs)\<rbrakk> \<Longrightarrow> getFr ([xx, yy] @ map snd txs) ([t1, t2] @ map fst txs) [] \<notin> FvarsT t; \<And>\<phi>. \<lbrakk>set ([xx, yy] @ map snd txs) \<subseteq> var; set ([t1, t2] @ map fst txs) \<subseteq> trm; set [] \<subseteq> fmla; \<phi> \<in> set []\<rbrakk> \<Longrightarrow> getFr ([xx, yy] @ map snd txs) ([t1, t2] @ map fst txs) [] \<notin> Fvars \<phi>; \<And>t. \<lbrakk>set ([xx, yy] @ map snd txs) \<subseteq> var; set ([t1, t2] @ map fst txs) \<subseteq> trm; set [] \<subseteq> fmla; t \<in> set ([t1, t2] @ map fst txs)\<rbrakk> \<Longrightarrow> getFr ([xx, yy] @ map snd txs) ([t1, t2] @ map fst txs) [] \<notin> set ([xx, yy] @ map snd txs)\<rbrakk> \<Longrightarrow> getFr ([xx, yy] @ map snd txs) ([t1, t2] @ map fst txs) [] \<notin> FvarsT t1
 2. \<lbrakk>t1 \<in> trm; t2 \<in> trm; fst ` set txs \<subseteq> trm; snd ` set txs \<subseteq> var; \<And>t. \<lbrakk>set ([xx, yy] @ map snd txs) \<subseteq> var; set ([t1, t2] @ map fst txs) \<subseteq> trm; set [] \<subseteq> fmla; t \<in> set ([t1, t2] @ map fst txs)\<rbrakk> \<Longrightarrow> getFr ([xx, yy] @ map snd txs) ([t1, t2] @ map fst txs) [] \<notin> FvarsT t; \<And>\<phi>. \<lbrakk>set ([xx, yy] @ map snd txs) \<subseteq> var; set ([t1, t2] @ map fst txs) \<subseteq> trm; set [] \<subseteq> fmla; \<phi> \<in> set []\<rbrakk> \<Longrightarrow> getFr ([xx, yy] @ map snd txs) ([t1, t2] @ map fst txs) [] \<notin> Fvars \<phi>; \<And>t. \<lbrakk>set ([xx, yy] @ map snd txs) \<subseteq> var; set ([t1, t2] @ map fst txs) \<subseteq> trm; set [] \<subseteq> fmla; t \<in> set ([t1, t2] @ map fst txs)\<rbrakk> \<Longrightarrow> getFr ([xx, yy] @ map snd txs) ([t1, t2] @ map fst txs) [] \<notin> set ([xx, yy] @ map snd txs)\<rbrakk> \<Longrightarrow> getFr ([xx, yy] @ map snd txs) ([t1, t2] @ map fst txs) [] \<notin> FvarsT t2
 3. \<lbrakk>t1 \<in> trm; t2 \<in> trm; fst ` set txs \<subseteq> trm; snd ` set txs \<subseteq> var; \<And>t. \<lbrakk>set ([xx, yy] @ map snd txs) \<subseteq> var; set ([t1, t2] @ map fst txs) \<subseteq> trm; set [] \<subseteq> fmla; t \<in> set ([t1, t2] @ map fst txs)\<rbrakk> \<Longrightarrow> getFr ([xx, yy] @ map snd txs) ([t1, t2] @ map fst txs) [] \<notin> FvarsT t; \<And>\<phi>. \<lbrakk>set ([xx, yy] @ map snd txs) \<subseteq> var; set ([t1, t2] @ map fst txs) \<subseteq> trm; set [] \<subseteq> fmla; \<phi> \<in> set []\<rbrakk> \<Longrightarrow> getFr ([xx, yy] @ map snd txs) ([t1, t2] @ map fst txs) [] \<notin> Fvars \<phi>; \<And>t. \<lbrakk>set ([xx, yy] @ map snd txs) \<subseteq> var; set ([t1, t2] @ map fst txs) \<subseteq> trm; set [] \<subseteq> fmla; t \<in> set ([t1, t2] @ map fst txs)\<rbrakk> \<Longrightarrow> getFr ([xx, yy] @ map snd txs) ([t1, t2] @ map fst txs) [] \<notin> set ([xx, yy] @ map snd txs)\<rbrakk> \<Longrightarrow> getFr ([xx, yy] @ map snd txs) ([t1, t2] @ map fst txs) [] \<notin> \<Union> (FvarsT ` fst ` set txs)
 4. \<lbrakk>t1 \<in> trm; t2 \<in> trm; fst ` set txs \<subseteq> trm; snd ` set txs \<subseteq> var; \<And>t. \<lbrakk>set ([xx, yy] @ map snd txs) \<subseteq> var; set ([t1, t2] @ map fst txs) \<subseteq> trm; set [] \<subseteq> fmla; t \<in> set ([t1, t2] @ map fst txs)\<rbrakk> \<Longrightarrow> getFr ([xx, yy] @ map snd txs) ([t1, t2] @ map fst txs) [] \<notin> FvarsT t; \<And>\<phi>. \<lbrakk>set ([xx, yy] @ map snd txs) \<subseteq> var; set ([t1, t2] @ map fst txs) \<subseteq> trm; set [] \<subseteq> fmla; \<phi> \<in> set []\<rbrakk> \<Longrightarrow> getFr ([xx, yy] @ map snd txs) ([t1, t2] @ map fst txs) [] \<notin> Fvars \<phi>; \<And>t. \<lbrakk>set ([xx, yy] @ map snd txs) \<subseteq> var; set ([t1, t2] @ map fst txs) \<subseteq> trm; set [] \<subseteq> fmla; t \<in> set ([t1, t2] @ map fst txs)\<rbrakk> \<Longrightarrow> getFr ([xx, yy] @ map snd txs) ([t1, t2] @ map fst txs) [] \<notin> set ([xx, yy] @ map snd txs)\<rbrakk> \<Longrightarrow> getFr ([xx, yy] @ map snd txs) ([t1, t2] @ map fst txs) [] \<notin> snd ` set txs
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>t1 \<in> trm; t2 \<in> trm; fst ` set txs \<subseteq> trm; snd ` set txs \<subseteq> var; \<And>t. \<lbrakk>set ([xx, yy] @ map snd txs) \<subseteq> var; set ([t1, t2] @ map fst txs) \<subseteq> trm; set [] \<subseteq> fmla; t \<in> set ([t1, t2] @ map fst txs)\<rbrakk> \<Longrightarrow> getFr ([xx, yy] @ map snd txs) ([t1, t2] @ map fst txs) [] \<notin> FvarsT t; \<And>\<phi>. \<lbrakk>set ([xx, yy] @ map snd txs) \<subseteq> var; set ([t1, t2] @ map fst txs) \<subseteq> trm; set [] \<subseteq> fmla; \<phi> \<in> set []\<rbrakk> \<Longrightarrow> getFr ([xx, yy] @ map snd txs) ([t1, t2] @ map fst txs) [] \<notin> Fvars \<phi>; \<And>t. \<lbrakk>set ([xx, yy] @ map snd txs) \<subseteq> var; set ([t1, t2] @ map fst txs) \<subseteq> trm; set [] \<subseteq> fmla; t \<in> set ([t1, t2] @ map fst txs)\<rbrakk> \<Longrightarrow> getFr ([xx, yy] @ map snd txs) ([t1, t2] @ map fst txs) [] \<notin> set ([xx, yy] @ map snd txs)\<rbrakk> \<Longrightarrow> getFr ([xx, yy] @ map snd txs) ([t1, t2] @ map fst txs) [] \<notin> FvarsT t1
[PROOF STEP]
by force
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>t1 \<in> trm; t2 \<in> trm; fst ` set txs \<subseteq> trm; snd ` set txs \<subseteq> var; \<And>t. \<lbrakk>set ([xx, yy] @ map snd txs) \<subseteq> var; set ([t1, t2] @ map fst txs) \<subseteq> trm; set [] \<subseteq> fmla; t \<in> set ([t1, t2] @ map fst txs)\<rbrakk> \<Longrightarrow> getFr ([xx, yy] @ map snd txs) ([t1, t2] @ map fst txs) [] \<notin> FvarsT t; \<And>\<phi>. \<lbrakk>set ([xx, yy] @ map snd txs) \<subseteq> var; set ([t1, t2] @ map fst txs) \<subseteq> trm; set [] \<subseteq> fmla; \<phi> \<in> set []\<rbrakk> \<Longrightarrow> getFr ([xx, yy] @ map snd txs) ([t1, t2] @ map fst txs) [] \<notin> Fvars \<phi>; \<And>t. \<lbrakk>set ([xx, yy] @ map snd txs) \<subseteq> var; set ([t1, t2] @ map fst txs) \<subseteq> trm; set [] \<subseteq> fmla; t \<in> set ([t1, t2] @ map fst txs)\<rbrakk> \<Longrightarrow> getFr ([xx, yy] @ map snd txs) ([t1, t2] @ map fst txs) [] \<notin> set ([xx, yy] @ map snd txs)\<rbrakk> \<Longrightarrow> getFr ([xx, yy] @ map snd txs) ([t1, t2] @ map fst txs) [] \<notin> FvarsT t2
 2. \<lbrakk>t1 \<in> trm; t2 \<in> trm; fst ` set txs \<subseteq> trm; snd ` set txs \<subseteq> var; \<And>t. \<lbrakk>set ([xx, yy] @ map snd txs) \<subseteq> var; set ([t1, t2] @ map fst txs) \<subseteq> trm; set [] \<subseteq> fmla; t \<in> set ([t1, t2] @ map fst txs)\<rbrakk> \<Longrightarrow> getFr ([xx, yy] @ map snd txs) ([t1, t2] @ map fst txs) [] \<notin> FvarsT t; \<And>\<phi>. \<lbrakk>set ([xx, yy] @ map snd txs) \<subseteq> var; set ([t1, t2] @ map fst txs) \<subseteq> trm; set [] \<subseteq> fmla; \<phi> \<in> set []\<rbrakk> \<Longrightarrow> getFr ([xx, yy] @ map snd txs) ([t1, t2] @ map fst txs) [] \<notin> Fvars \<phi>; \<And>t. \<lbrakk>set ([xx, yy] @ map snd txs) \<subseteq> var; set ([t1, t2] @ map fst txs) \<subseteq> trm; set [] \<subseteq> fmla; t \<in> set ([t1, t2] @ map fst txs)\<rbrakk> \<Longrightarrow> getFr ([xx, yy] @ map snd txs) ([t1, t2] @ map fst txs) [] \<notin> set ([xx, yy] @ map snd txs)\<rbrakk> \<Longrightarrow> getFr ([xx, yy] @ map snd txs) ([t1, t2] @ map fst txs) [] \<notin> \<Union> (FvarsT ` fst ` set txs)
 3. \<lbrakk>t1 \<in> trm; t2 \<in> trm; fst ` set txs \<subseteq> trm; snd ` set txs \<subseteq> var; \<And>t. \<lbrakk>set ([xx, yy] @ map snd txs) \<subseteq> var; set ([t1, t2] @ map fst txs) \<subseteq> trm; set [] \<subseteq> fmla; t \<in> set ([t1, t2] @ map fst txs)\<rbrakk> \<Longrightarrow> getFr ([xx, yy] @ map snd txs) ([t1, t2] @ map fst txs) [] \<notin> FvarsT t; \<And>\<phi>. \<lbrakk>set ([xx, yy] @ map snd txs) \<subseteq> var; set ([t1, t2] @ map fst txs) \<subseteq> trm; set [] \<subseteq> fmla; \<phi> \<in> set []\<rbrakk> \<Longrightarrow> getFr ([xx, yy] @ map snd txs) ([t1, t2] @ map fst txs) [] \<notin> Fvars \<phi>; \<And>t. \<lbrakk>set ([xx, yy] @ map snd txs) \<subseteq> var; set ([t1, t2] @ map fst txs) \<subseteq> trm; set [] \<subseteq> fmla; t \<in> set ([t1, t2] @ map fst txs)\<rbrakk> \<Longrightarrow> getFr ([xx, yy] @ map snd txs) ([t1, t2] @ map fst txs) [] \<notin> set ([xx, yy] @ map snd txs)\<rbrakk> \<Longrightarrow> getFr ([xx, yy] @ map snd txs) ([t1, t2] @ map fst txs) [] \<notin> snd ` set txs
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>t1 \<in> trm; t2 \<in> trm; fst ` set txs \<subseteq> trm; snd ` set txs \<subseteq> var; \<And>t. \<lbrakk>set ([xx, yy] @ map snd txs) \<subseteq> var; set ([t1, t2] @ map fst txs) \<subseteq> trm; set [] \<subseteq> fmla; t \<in> set ([t1, t2] @ map fst txs)\<rbrakk> \<Longrightarrow> getFr ([xx, yy] @ map snd txs) ([t1, t2] @ map fst txs) [] \<notin> FvarsT t; \<And>\<phi>. \<lbrakk>set ([xx, yy] @ map snd txs) \<subseteq> var; set ([t1, t2] @ map fst txs) \<subseteq> trm; set [] \<subseteq> fmla; \<phi> \<in> set []\<rbrakk> \<Longrightarrow> getFr ([xx, yy] @ map snd txs) ([t1, t2] @ map fst txs) [] \<notin> Fvars \<phi>; \<And>t. \<lbrakk>set ([xx, yy] @ map snd txs) \<subseteq> var; set ([t1, t2] @ map fst txs) \<subseteq> trm; set [] \<subseteq> fmla; t \<in> set ([t1, t2] @ map fst txs)\<rbrakk> \<Longrightarrow> getFr ([xx, yy] @ map snd txs) ([t1, t2] @ map fst txs) [] \<notin> set ([xx, yy] @ map snd txs)\<rbrakk> \<Longrightarrow> getFr ([xx, yy] @ map snd txs) ([t1, t2] @ map fst txs) [] \<notin> FvarsT t2
[PROOF STEP]
by force
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>t1 \<in> trm; t2 \<in> trm; fst ` set txs \<subseteq> trm; snd ` set txs \<subseteq> var; \<And>t. \<lbrakk>set ([xx, yy] @ map snd txs) \<subseteq> var; set ([t1, t2] @ map fst txs) \<subseteq> trm; set [] \<subseteq> fmla; t \<in> set ([t1, t2] @ map fst txs)\<rbrakk> \<Longrightarrow> getFr ([xx, yy] @ map snd txs) ([t1, t2] @ map fst txs) [] \<notin> FvarsT t; \<And>\<phi>. \<lbrakk>set ([xx, yy] @ map snd txs) \<subseteq> var; set ([t1, t2] @ map fst txs) \<subseteq> trm; set [] \<subseteq> fmla; \<phi> \<in> set []\<rbrakk> \<Longrightarrow> getFr ([xx, yy] @ map snd txs) ([t1, t2] @ map fst txs) [] \<notin> Fvars \<phi>; \<And>t. \<lbrakk>set ([xx, yy] @ map snd txs) \<subseteq> var; set ([t1, t2] @ map fst txs) \<subseteq> trm; set [] \<subseteq> fmla; t \<in> set ([t1, t2] @ map fst txs)\<rbrakk> \<Longrightarrow> getFr ([xx, yy] @ map snd txs) ([t1, t2] @ map fst txs) [] \<notin> set ([xx, yy] @ map snd txs)\<rbrakk> \<Longrightarrow> getFr ([xx, yy] @ map snd txs) ([t1, t2] @ map fst txs) [] \<notin> \<Union> (FvarsT ` fst ` set txs)
 2. \<lbrakk>t1 \<in> trm; t2 \<in> trm; fst ` set txs \<subseteq> trm; snd ` set txs \<subseteq> var; \<And>t. \<lbrakk>set ([xx, yy] @ map snd txs) \<subseteq> var; set ([t1, t2] @ map fst txs) \<subseteq> trm; set [] \<subseteq> fmla; t \<in> set ([t1, t2] @ map fst txs)\<rbrakk> \<Longrightarrow> getFr ([xx, yy] @ map snd txs) ([t1, t2] @ map fst txs) [] \<notin> FvarsT t; \<And>\<phi>. \<lbrakk>set ([xx, yy] @ map snd txs) \<subseteq> var; set ([t1, t2] @ map fst txs) \<subseteq> trm; set [] \<subseteq> fmla; \<phi> \<in> set []\<rbrakk> \<Longrightarrow> getFr ([xx, yy] @ map snd txs) ([t1, t2] @ map fst txs) [] \<notin> Fvars \<phi>; \<And>t. \<lbrakk>set ([xx, yy] @ map snd txs) \<subseteq> var; set ([t1, t2] @ map fst txs) \<subseteq> trm; set [] \<subseteq> fmla; t \<in> set ([t1, t2] @ map fst txs)\<rbrakk> \<Longrightarrow> getFr ([xx, yy] @ map snd txs) ([t1, t2] @ map fst txs) [] \<notin> set ([xx, yy] @ map snd txs)\<rbrakk> \<Longrightarrow> getFr ([xx, yy] @ map snd txs) ([t1, t2] @ map fst txs) [] \<notin> snd ` set txs
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>t1 \<in> trm; t2 \<in> trm; fst ` set txs \<subseteq> trm; snd ` set txs \<subseteq> var; \<And>t. \<lbrakk>set ([xx, yy] @ map snd txs) \<subseteq> var; set ([t1, t2] @ map fst txs) \<subseteq> trm; set [] \<subseteq> fmla; t \<in> set ([t1, t2] @ map fst txs)\<rbrakk> \<Longrightarrow> getFr ([xx, yy] @ map snd txs) ([t1, t2] @ map fst txs) [] \<notin> FvarsT t; \<And>\<phi>. \<lbrakk>set ([xx, yy] @ map snd txs) \<subseteq> var; set ([t1, t2] @ map fst txs) \<subseteq> trm; set [] \<subseteq> fmla; \<phi> \<in> set []\<rbrakk> \<Longrightarrow> getFr ([xx, yy] @ map snd txs) ([t1, t2] @ map fst txs) [] \<notin> Fvars \<phi>; \<And>t. \<lbrakk>set ([xx, yy] @ map snd txs) \<subseteq> var; set ([t1, t2] @ map fst txs) \<subseteq> trm; set [] \<subseteq> fmla; t \<in> set ([t1, t2] @ map fst txs)\<rbrakk> \<Longrightarrow> getFr ([xx, yy] @ map snd txs) ([t1, t2] @ map fst txs) [] \<notin> set ([xx, yy] @ map snd txs)\<rbrakk> \<Longrightarrow> getFr ([xx, yy] @ map snd txs) ([t1, t2] @ map fst txs) [] \<notin> \<Union> (FvarsT ` fst ` set txs)
[PROOF STEP]
by auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>t1 \<in> trm; t2 \<in> trm; fst ` set txs \<subseteq> trm; snd ` set txs \<subseteq> var; \<And>t. \<lbrakk>set ([xx, yy] @ map snd txs) \<subseteq> var; set ([t1, t2] @ map fst txs) \<subseteq> trm; set [] \<subseteq> fmla; t \<in> set ([t1, t2] @ map fst txs)\<rbrakk> \<Longrightarrow> getFr ([xx, yy] @ map snd txs) ([t1, t2] @ map fst txs) [] \<notin> FvarsT t; \<And>\<phi>. \<lbrakk>set ([xx, yy] @ map snd txs) \<subseteq> var; set ([t1, t2] @ map fst txs) \<subseteq> trm; set [] \<subseteq> fmla; \<phi> \<in> set []\<rbrakk> \<Longrightarrow> getFr ([xx, yy] @ map snd txs) ([t1, t2] @ map fst txs) [] \<notin> Fvars \<phi>; \<And>t. \<lbrakk>set ([xx, yy] @ map snd txs) \<subseteq> var; set ([t1, t2] @ map fst txs) \<subseteq> trm; set [] \<subseteq> fmla; t \<in> set ([t1, t2] @ map fst txs)\<rbrakk> \<Longrightarrow> getFr ([xx, yy] @ map snd txs) ([t1, t2] @ map fst txs) [] \<notin> set ([xx, yy] @ map snd txs)\<rbrakk> \<Longrightarrow> getFr ([xx, yy] @ map snd txs) ([t1, t2] @ map fst txs) [] \<notin> snd ` set txs
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>t1 \<in> trm; t2 \<in> trm; fst ` set txs \<subseteq> trm; snd ` set txs \<subseteq> var; \<And>t. \<lbrakk>set ([xx, yy] @ map snd txs) \<subseteq> var; set ([t1, t2] @ map fst txs) \<subseteq> trm; set [] \<subseteq> fmla; t \<in> set ([t1, t2] @ map fst txs)\<rbrakk> \<Longrightarrow> getFr ([xx, yy] @ map snd txs) ([t1, t2] @ map fst txs) [] \<notin> FvarsT t; \<And>\<phi>. \<lbrakk>set ([xx, yy] @ map snd txs) \<subseteq> var; set ([t1, t2] @ map fst txs) \<subseteq> trm; set [] \<subseteq> fmla; \<phi> \<in> set []\<rbrakk> \<Longrightarrow> getFr ([xx, yy] @ map snd txs) ([t1, t2] @ map fst txs) [] \<notin> Fvars \<phi>; \<And>t. \<lbrakk>set ([xx, yy] @ map snd txs) \<subseteq> var; set ([t1, t2] @ map fst txs) \<subseteq> trm; set [] \<subseteq> fmla; t \<in> set ([t1, t2] @ map fst txs)\<rbrakk> \<Longrightarrow> getFr ([xx, yy] @ map snd txs) ([t1, t2] @ map fst txs) [] \<notin> set ([xx, yy] @ map snd txs)\<rbrakk> \<Longrightarrow> getFr ([xx, yy] @ map snd txs) ([t1, t2] @ map fst txs) [] \<notin> snd ` set txs
[PROOF STEP]
by (force simp: image_iff)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
z \<in> var
z \<noteq> xx
z \<noteq> yy
z \<notin> FvarsT t1
z \<notin> FvarsT t2
z \<notin> \<Union> (FvarsT ` fst ` set txs)
z \<notin> snd ` set txs

goal (1 subgoal):
 1. psubst (LLq t1 t2) txs = LLq (psubstT t1 txs) (psubstT t2 txs)
[PROOF STEP]
note in_FvarsT_psubstTD[dest!]
[PROOF STATE]
proof (state)
this:
\<lbrakk>?y \<in> FvarsT (psubstT ?r ?txs); ?r \<in> atrm; snd ` set ?txs \<subseteq> var; fst ` set ?txs \<subseteq> atrm; distinct (map snd ?txs)\<rbrakk> \<Longrightarrow> ?y \<in> FvarsT ?r - snd ` set ?txs \<union> \<Union> {if x \<in> FvarsT ?r then FvarsT t else {} |t x. (t, x) \<in> set ?txs}

goal (1 subgoal):
 1. psubst (LLq t1 t2) txs = LLq (psubstT t1 txs) (psubstT t2 txs)
[PROOF STEP]
note if_splits[split]
[PROOF STATE]
proof (state)
this:
?P (if ?Q then ?x else ?y) = ((?Q \<longrightarrow> ?P ?x) \<and> (\<not> ?Q \<longrightarrow> ?P ?y))
?P (if ?Q then ?x else ?y) = (\<not> (?Q \<and> \<not> ?P ?x \<or> \<not> ?Q \<and> \<not> ?P ?y))

goal (1 subgoal):
 1. psubst (LLq t1 t2) txs = LLq (psubstT t1 txs) (psubstT t2 txs)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. psubst (LLq t1 t2) txs = LLq (psubstT t1 txs) (psubstT t2 txs)
[PROOF STEP]
using assms 0 us_facts
[PROOF STATE]
proof (prove)
using this:
t1 \<in> atrm
t2 \<in> atrm
fst ` set txs \<subseteq> atrm
snd ` set txs \<subseteq> var
distinct (map snd txs)
t1 \<in> trm
t2 \<in> trm
fst ` set txs \<subseteq> trm
z \<in> var
z \<noteq> xx
z \<noteq> yy
z \<notin> FvarsT t1
z \<notin> FvarsT t2
z \<notin> \<Union> (FvarsT ` fst ` set txs)
z \<notin> snd ` set txs

goal (1 subgoal):
 1. psubst (LLq t1 t2) txs = LLq (psubstT t1 txs) (psubstT t2 txs)
[PROOF STEP]
apply(subst LLq_pls[of _ _ z])
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<lbrakk>t1 \<in> atrm; t2 \<in> atrm; fst ` set txs \<subseteq> atrm; snd ` set txs \<subseteq> var; distinct (map snd txs); t1 \<in> trm; t2 \<in> trm; fst ` set txs \<subseteq> trm; z \<in> var; z \<noteq> xx; z \<noteq> yy; z \<notin> FvarsT t1; z \<notin> FvarsT t2; z \<notin> \<Union> (FvarsT ` fst ` set txs); z \<notin> snd ` set txs\<rbrakk> \<Longrightarrow> t1 \<in> atrm
 2. \<lbrakk>t1 \<in> atrm; t2 \<in> atrm; fst ` set txs \<subseteq> atrm; snd ` set txs \<subseteq> var; distinct (map snd txs); t1 \<in> trm; t2 \<in> trm; fst ` set txs \<subseteq> trm; z \<in> var; z \<noteq> xx; z \<noteq> yy; z \<notin> FvarsT t1; z \<notin> FvarsT t2; z \<notin> \<Union> (FvarsT ` fst ` set txs); z \<notin> snd ` set txs\<rbrakk> \<Longrightarrow> t2 \<in> atrm
 3. \<lbrakk>t1 \<in> atrm; t2 \<in> atrm; fst ` set txs \<subseteq> atrm; snd ` set txs \<subseteq> var; distinct (map snd txs); t1 \<in> trm; t2 \<in> trm; fst ` set txs \<subseteq> trm; z \<in> var; z \<noteq> xx; z \<noteq> yy; z \<notin> FvarsT t1; z \<notin> FvarsT t2; z \<notin> \<Union> (FvarsT ` fst ` set txs); z \<notin> snd ` set txs\<rbrakk> \<Longrightarrow> z \<in> var
 4. \<lbrakk>t1 \<in> atrm; t2 \<in> atrm; fst ` set txs \<subseteq> atrm; snd ` set txs \<subseteq> var; distinct (map snd txs); t1 \<in> trm; t2 \<in> trm; fst ` set txs \<subseteq> trm; z \<in> var; z \<noteq> xx; z \<noteq> yy; z \<notin> FvarsT t1; z \<notin> FvarsT t2; z \<notin> \<Union> (FvarsT ` fst ` set txs); z \<notin> snd ` set txs\<rbrakk> \<Longrightarrow> z \<notin> FvarsT t1
 5. \<lbrakk>t1 \<in> atrm; t2 \<in> atrm; fst ` set txs \<subseteq> atrm; snd ` set txs \<subseteq> var; distinct (map snd txs); t1 \<in> trm; t2 \<in> trm; fst ` set txs \<subseteq> trm; z \<in> var; z \<noteq> xx; z \<noteq> yy; z \<notin> FvarsT t1; z \<notin> FvarsT t2; z \<notin> \<Union> (FvarsT ` fst ` set txs); z \<notin> snd ` set txs\<rbrakk> \<Longrightarrow> z \<notin> FvarsT t2
 6. \<lbrakk>t1 \<in> atrm; t2 \<in> atrm; fst ` set txs \<subseteq> atrm; snd ` set txs \<subseteq> var; distinct (map snd txs); t1 \<in> trm; t2 \<in> trm; fst ` set txs \<subseteq> trm; z \<in> var; z \<noteq> xx; z \<noteq> yy; z \<notin> FvarsT t1; z \<notin> FvarsT t2; z \<notin> \<Union> (FvarsT ` fst ` set txs); z \<notin> snd ` set txs\<rbrakk> \<Longrightarrow> psubst (exi z (eql t2 (pls (Var z) t1))) txs = LLq (psubstT t1 txs) (psubstT t2 txs)
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>t1 \<in> atrm; t2 \<in> atrm; fst ` set txs \<subseteq> atrm; snd ` set txs \<subseteq> var; distinct (map snd txs); t1 \<in> trm; t2 \<in> trm; fst ` set txs \<subseteq> trm; z \<in> var; z \<noteq> xx; z \<noteq> yy; z \<notin> FvarsT t1; z \<notin> FvarsT t2; z \<notin> \<Union> (FvarsT ` fst ` set txs); z \<notin> snd ` set txs\<rbrakk> \<Longrightarrow> t1 \<in> atrm
[PROOF STEP]
by auto
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<lbrakk>t1 \<in> atrm; t2 \<in> atrm; fst ` set txs \<subseteq> atrm; snd ` set txs \<subseteq> var; distinct (map snd txs); t1 \<in> trm; t2 \<in> trm; fst ` set txs \<subseteq> trm; z \<in> var; z \<noteq> xx; z \<noteq> yy; z \<notin> FvarsT t1; z \<notin> FvarsT t2; z \<notin> \<Union> (FvarsT ` fst ` set txs); z \<notin> snd ` set txs\<rbrakk> \<Longrightarrow> t2 \<in> atrm
 2. \<lbrakk>t1 \<in> atrm; t2 \<in> atrm; fst ` set txs \<subseteq> atrm; snd ` set txs \<subseteq> var; distinct (map snd txs); t1 \<in> trm; t2 \<in> trm; fst ` set txs \<subseteq> trm; z \<in> var; z \<noteq> xx; z \<noteq> yy; z \<notin> FvarsT t1; z \<notin> FvarsT t2; z \<notin> \<Union> (FvarsT ` fst ` set txs); z \<notin> snd ` set txs\<rbrakk> \<Longrightarrow> z \<in> var
 3. \<lbrakk>t1 \<in> atrm; t2 \<in> atrm; fst ` set txs \<subseteq> atrm; snd ` set txs \<subseteq> var; distinct (map snd txs); t1 \<in> trm; t2 \<in> trm; fst ` set txs \<subseteq> trm; z \<in> var; z \<noteq> xx; z \<noteq> yy; z \<notin> FvarsT t1; z \<notin> FvarsT t2; z \<notin> \<Union> (FvarsT ` fst ` set txs); z \<notin> snd ` set txs\<rbrakk> \<Longrightarrow> z \<notin> FvarsT t1
 4. \<lbrakk>t1 \<in> atrm; t2 \<in> atrm; fst ` set txs \<subseteq> atrm; snd ` set txs \<subseteq> var; distinct (map snd txs); t1 \<in> trm; t2 \<in> trm; fst ` set txs \<subseteq> trm; z \<in> var; z \<noteq> xx; z \<noteq> yy; z \<notin> FvarsT t1; z \<notin> FvarsT t2; z \<notin> \<Union> (FvarsT ` fst ` set txs); z \<notin> snd ` set txs\<rbrakk> \<Longrightarrow> z \<notin> FvarsT t2
 5. \<lbrakk>t1 \<in> atrm; t2 \<in> atrm; fst ` set txs \<subseteq> atrm; snd ` set txs \<subseteq> var; distinct (map snd txs); t1 \<in> trm; t2 \<in> trm; fst ` set txs \<subseteq> trm; z \<in> var; z \<noteq> xx; z \<noteq> yy; z \<notin> FvarsT t1; z \<notin> FvarsT t2; z \<notin> \<Union> (FvarsT ` fst ` set txs); z \<notin> snd ` set txs\<rbrakk> \<Longrightarrow> psubst (exi z (eql t2 (pls (Var z) t1))) txs = LLq (psubstT t1 txs) (psubstT t2 txs)
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>t1 \<in> atrm; t2 \<in> atrm; fst ` set txs \<subseteq> atrm; snd ` set txs \<subseteq> var; distinct (map snd txs); t1 \<in> trm; t2 \<in> trm; fst ` set txs \<subseteq> trm; z \<in> var; z \<noteq> xx; z \<noteq> yy; z \<notin> FvarsT t1; z \<notin> FvarsT t2; z \<notin> \<Union> (FvarsT ` fst ` set txs); z \<notin> snd ` set txs\<rbrakk> \<Longrightarrow> t2 \<in> atrm
[PROOF STEP]
by auto
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<lbrakk>t1 \<in> atrm; t2 \<in> atrm; fst ` set txs \<subseteq> atrm; snd ` set txs \<subseteq> var; distinct (map snd txs); t1 \<in> trm; t2 \<in> trm; fst ` set txs \<subseteq> trm; z \<in> var; z \<noteq> xx; z \<noteq> yy; z \<notin> FvarsT t1; z \<notin> FvarsT t2; z \<notin> \<Union> (FvarsT ` fst ` set txs); z \<notin> snd ` set txs\<rbrakk> \<Longrightarrow> z \<in> var
 2. \<lbrakk>t1 \<in> atrm; t2 \<in> atrm; fst ` set txs \<subseteq> atrm; snd ` set txs \<subseteq> var; distinct (map snd txs); t1 \<in> trm; t2 \<in> trm; fst ` set txs \<subseteq> trm; z \<in> var; z \<noteq> xx; z \<noteq> yy; z \<notin> FvarsT t1; z \<notin> FvarsT t2; z \<notin> \<Union> (FvarsT ` fst ` set txs); z \<notin> snd ` set txs\<rbrakk> \<Longrightarrow> z \<notin> FvarsT t1
 3. \<lbrakk>t1 \<in> atrm; t2 \<in> atrm; fst ` set txs \<subseteq> atrm; snd ` set txs \<subseteq> var; distinct (map snd txs); t1 \<in> trm; t2 \<in> trm; fst ` set txs \<subseteq> trm; z \<in> var; z \<noteq> xx; z \<noteq> yy; z \<notin> FvarsT t1; z \<notin> FvarsT t2; z \<notin> \<Union> (FvarsT ` fst ` set txs); z \<notin> snd ` set txs\<rbrakk> \<Longrightarrow> z \<notin> FvarsT t2
 4. \<lbrakk>t1 \<in> atrm; t2 \<in> atrm; fst ` set txs \<subseteq> atrm; snd ` set txs \<subseteq> var; distinct (map snd txs); t1 \<in> trm; t2 \<in> trm; fst ` set txs \<subseteq> trm; z \<in> var; z \<noteq> xx; z \<noteq> yy; z \<notin> FvarsT t1; z \<notin> FvarsT t2; z \<notin> \<Union> (FvarsT ` fst ` set txs); z \<notin> snd ` set txs\<rbrakk> \<Longrightarrow> psubst (exi z (eql t2 (pls (Var z) t1))) txs = LLq (psubstT t1 txs) (psubstT t2 txs)
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>t1 \<in> atrm; t2 \<in> atrm; fst ` set txs \<subseteq> atrm; snd ` set txs \<subseteq> var; distinct (map snd txs); t1 \<in> trm; t2 \<in> trm; fst ` set txs \<subseteq> trm; z \<in> var; z \<noteq> xx; z \<noteq> yy; z \<notin> FvarsT t1; z \<notin> FvarsT t2; z \<notin> \<Union> (FvarsT ` fst ` set txs); z \<notin> snd ` set txs\<rbrakk> \<Longrightarrow> z \<in> var
[PROOF STEP]
by auto
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>t1 \<in> atrm; t2 \<in> atrm; fst ` set txs \<subseteq> atrm; snd ` set txs \<subseteq> var; distinct (map snd txs); t1 \<in> trm; t2 \<in> trm; fst ` set txs \<subseteq> trm; z \<in> var; z \<noteq> xx; z \<noteq> yy; z \<notin> FvarsT t1; z \<notin> FvarsT t2; z \<notin> \<Union> (FvarsT ` fst ` set txs); z \<notin> snd ` set txs\<rbrakk> \<Longrightarrow> z \<notin> FvarsT t1
 2. \<lbrakk>t1 \<in> atrm; t2 \<in> atrm; fst ` set txs \<subseteq> atrm; snd ` set txs \<subseteq> var; distinct (map snd txs); t1 \<in> trm; t2 \<in> trm; fst ` set txs \<subseteq> trm; z \<in> var; z \<noteq> xx; z \<noteq> yy; z \<notin> FvarsT t1; z \<notin> FvarsT t2; z \<notin> \<Union> (FvarsT ` fst ` set txs); z \<notin> snd ` set txs\<rbrakk> \<Longrightarrow> z \<notin> FvarsT t2
 3. \<lbrakk>t1 \<in> atrm; t2 \<in> atrm; fst ` set txs \<subseteq> atrm; snd ` set txs \<subseteq> var; distinct (map snd txs); t1 \<in> trm; t2 \<in> trm; fst ` set txs \<subseteq> trm; z \<in> var; z \<noteq> xx; z \<noteq> yy; z \<notin> FvarsT t1; z \<notin> FvarsT t2; z \<notin> \<Union> (FvarsT ` fst ` set txs); z \<notin> snd ` set txs\<rbrakk> \<Longrightarrow> psubst (exi z (eql t2 (pls (Var z) t1))) txs = LLq (psubstT t1 txs) (psubstT t2 txs)
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>t1 \<in> atrm; t2 \<in> atrm; fst ` set txs \<subseteq> atrm; snd ` set txs \<subseteq> var; distinct (map snd txs); t1 \<in> trm; t2 \<in> trm; fst ` set txs \<subseteq> trm; z \<in> var; z \<noteq> xx; z \<noteq> yy; z \<notin> FvarsT t1; z \<notin> FvarsT t2; z \<notin> \<Union> (FvarsT ` fst ` set txs); z \<notin> snd ` set txs\<rbrakk> \<Longrightarrow> z \<notin> FvarsT t1
[PROOF STEP]
by auto
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>t1 \<in> atrm; t2 \<in> atrm; fst ` set txs \<subseteq> atrm; snd ` set txs \<subseteq> var; distinct (map snd txs); t1 \<in> trm; t2 \<in> trm; fst ` set txs \<subseteq> trm; z \<in> var; z \<noteq> xx; z \<noteq> yy; z \<notin> FvarsT t1; z \<notin> FvarsT t2; z \<notin> \<Union> (FvarsT ` fst ` set txs); z \<notin> snd ` set txs\<rbrakk> \<Longrightarrow> z \<notin> FvarsT t2
 2. \<lbrakk>t1 \<in> atrm; t2 \<in> atrm; fst ` set txs \<subseteq> atrm; snd ` set txs \<subseteq> var; distinct (map snd txs); t1 \<in> trm; t2 \<in> trm; fst ` set txs \<subseteq> trm; z \<in> var; z \<noteq> xx; z \<noteq> yy; z \<notin> FvarsT t1; z \<notin> FvarsT t2; z \<notin> \<Union> (FvarsT ` fst ` set txs); z \<notin> snd ` set txs\<rbrakk> \<Longrightarrow> psubst (exi z (eql t2 (pls (Var z) t1))) txs = LLq (psubstT t1 txs) (psubstT t2 txs)
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>t1 \<in> atrm; t2 \<in> atrm; fst ` set txs \<subseteq> atrm; snd ` set txs \<subseteq> var; distinct (map snd txs); t1 \<in> trm; t2 \<in> trm; fst ` set txs \<subseteq> trm; z \<in> var; z \<noteq> xx; z \<noteq> yy; z \<notin> FvarsT t1; z \<notin> FvarsT t2; z \<notin> \<Union> (FvarsT ` fst ` set txs); z \<notin> snd ` set txs\<rbrakk> \<Longrightarrow> z \<notin> FvarsT t2
[PROOF STEP]
by auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>t1 \<in> atrm; t2 \<in> atrm; fst ` set txs \<subseteq> atrm; snd ` set txs \<subseteq> var; distinct (map snd txs); t1 \<in> trm; t2 \<in> trm; fst ` set txs \<subseteq> trm; z \<in> var; z \<noteq> xx; z \<noteq> yy; z \<notin> FvarsT t1; z \<notin> FvarsT t2; z \<notin> \<Union> (FvarsT ` fst ` set txs); z \<notin> snd ` set txs\<rbrakk> \<Longrightarrow> psubst (exi z (eql t2 (pls (Var z) t1))) txs = LLq (psubstT t1 txs) (psubstT t2 txs)
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>t1 \<in> atrm; t2 \<in> atrm; fst ` set txs \<subseteq> atrm; snd ` set txs \<subseteq> var; distinct (map snd txs); t1 \<in> trm; t2 \<in> trm; fst ` set txs \<subseteq> trm; z \<in> var; z \<noteq> xx; z \<noteq> yy; z \<notin> FvarsT t1; z \<notin> FvarsT t2; z \<notin> \<Union> (FvarsT ` fst ` set txs); z \<notin> snd ` set txs\<rbrakk> \<Longrightarrow> psubst (exi z (eql t2 (pls (Var z) t1))) txs = LLq (psubstT t1 txs) (psubstT t2 txs)
[PROOF STEP]
apply(subst LLq_pls[of _ _ z])
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<lbrakk>t1 \<in> atrm; t2 \<in> atrm; fst ` set txs \<subseteq> atrm; snd ` set txs \<subseteq> var; distinct (map snd txs); t1 \<in> trm; t2 \<in> trm; fst ` set txs \<subseteq> trm; z \<in> var; z \<noteq> xx; z \<noteq> yy; z \<notin> FvarsT t1; z \<notin> FvarsT t2; z \<notin> \<Union> (FvarsT ` fst ` set txs); z \<notin> snd ` set txs\<rbrakk> \<Longrightarrow> psubstT t1 txs \<in> atrm
 2. \<lbrakk>t1 \<in> atrm; t2 \<in> atrm; fst ` set txs \<subseteq> atrm; snd ` set txs \<subseteq> var; distinct (map snd txs); t1 \<in> trm; t2 \<in> trm; fst ` set txs \<subseteq> trm; z \<in> var; z \<noteq> xx; z \<noteq> yy; z \<notin> FvarsT t1; z \<notin> FvarsT t2; z \<notin> \<Union> (FvarsT ` fst ` set txs); z \<notin> snd ` set txs\<rbrakk> \<Longrightarrow> psubstT t2 txs \<in> atrm
 3. \<lbrakk>t1 \<in> atrm; t2 \<in> atrm; fst ` set txs \<subseteq> atrm; snd ` set txs \<subseteq> var; distinct (map snd txs); t1 \<in> trm; t2 \<in> trm; fst ` set txs \<subseteq> trm; z \<in> var; z \<noteq> xx; z \<noteq> yy; z \<notin> FvarsT t1; z \<notin> FvarsT t2; z \<notin> \<Union> (FvarsT ` fst ` set txs); z \<notin> snd ` set txs\<rbrakk> \<Longrightarrow> z \<in> var
 4. \<lbrakk>t1 \<in> atrm; t2 \<in> atrm; fst ` set txs \<subseteq> atrm; snd ` set txs \<subseteq> var; distinct (map snd txs); t1 \<in> trm; t2 \<in> trm; fst ` set txs \<subseteq> trm; z \<in> var; z \<noteq> xx; z \<noteq> yy; z \<notin> FvarsT t1; z \<notin> FvarsT t2; z \<notin> \<Union> (FvarsT ` fst ` set txs); z \<notin> snd ` set txs\<rbrakk> \<Longrightarrow> z \<notin> FvarsT (psubstT t1 txs)
 5. \<lbrakk>t1 \<in> atrm; t2 \<in> atrm; fst ` set txs \<subseteq> atrm; snd ` set txs \<subseteq> var; distinct (map snd txs); t1 \<in> trm; t2 \<in> trm; fst ` set txs \<subseteq> trm; z \<in> var; z \<noteq> xx; z \<noteq> yy; z \<notin> FvarsT t1; z \<notin> FvarsT t2; z \<notin> \<Union> (FvarsT ` fst ` set txs); z \<notin> snd ` set txs\<rbrakk> \<Longrightarrow> z \<notin> FvarsT (psubstT t2 txs)
 6. \<lbrakk>t1 \<in> atrm; t2 \<in> atrm; fst ` set txs \<subseteq> atrm; snd ` set txs \<subseteq> var; distinct (map snd txs); t1 \<in> trm; t2 \<in> trm; fst ` set txs \<subseteq> trm; z \<in> var; z \<noteq> xx; z \<noteq> yy; z \<notin> FvarsT t1; z \<notin> FvarsT t2; z \<notin> \<Union> (FvarsT ` fst ` set txs); z \<notin> snd ` set txs\<rbrakk> \<Longrightarrow> psubst (exi z (eql t2 (pls (Var z) t1))) txs = exi z (eql (psubstT t2 txs) (pls (Var z) (psubstT t1 txs)))
[PROOF STEP]
by auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
psubst (LLq t1 t2) txs = LLq (psubstT t1 txs) (psubstT t2 txs)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma iMOD_cut_le1: "
  t \<in> [r, mod m] \<Longrightarrow>
  [r, mod m] \<down>\<le> t = [r, mod m, (t - r) div m]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. t \<in> [ r, mod m ] \<Longrightarrow> [ r, mod m ] \<down>\<le> t = [ r, mod m, (t - r) div m ]
[PROOF STEP]
by (simp add: iMOD_cut_le iT_iff)


[STATEMENT]
lemma iIN_inext_nth_if : "
  [n\<dots>,d] \<rightarrow> a = (if a \<le> d then n + a else n + d)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [n\<dots>,d] \<rightarrow> a = (if a \<le> d then n + a else n + d)
[PROOF STEP]
by (simp add: iIN_inext_nth inext_nth_card_Max iT_finite iT_not_empty iT_Max iT_card)


[STATEMENT]
lemma invar_step: "invar (big :: 'a state) \<Longrightarrow> invar (step big)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. invar big \<Longrightarrow> invar (step big)
[PROOF STEP]
proof(induction big rule: step_state.induct)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>state. invar (Common state) \<Longrightarrow> invar (step (Common state))
 2. \<And>current uu_ aux. invar (Reverse current uu_ aux 0) \<Longrightarrow> invar (step (Reverse current uu_ aux 0))
 3. \<And>current big aux v. invar (Reverse current big aux (Suc v)) \<Longrightarrow> invar (step (Reverse current big aux (Suc v)))
[PROOF STEP]
case 1
[PROOF STATE]
proof (state)
this:
invar (Common state_)

goal (3 subgoals):
 1. \<And>state. invar (Common state) \<Longrightarrow> invar (step (Common state))
 2. \<And>current uu_ aux. invar (Reverse current uu_ aux 0) \<Longrightarrow> invar (step (Reverse current uu_ aux 0))
 3. \<And>current big aux v. invar (Reverse current big aux (Suc v)) \<Longrightarrow> invar (step (Reverse current big aux (Suc v)))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
invar (Common state_)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
invar (Common state_)

goal (1 subgoal):
 1. invar (step (Common state_))
[PROOF STEP]
by(auto simp: invar_step)
[PROOF STATE]
proof (state)
this:
invar (step (Common state_))

goal (2 subgoals):
 1. \<And>current uu_ aux. invar (Reverse current uu_ aux 0) \<Longrightarrow> invar (step (Reverse current uu_ aux 0))
 2. \<And>current big aux v. invar (Reverse current big aux (Suc v)) \<Longrightarrow> invar (step (Reverse current big aux (Suc v)))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>current uu_ aux. invar (Reverse current uu_ aux 0) \<Longrightarrow> invar (step (Reverse current uu_ aux 0))
 2. \<And>current big aux v. invar (Reverse current big aux (Suc v)) \<Longrightarrow> invar (step (Reverse current big aux (Suc v)))
[PROOF STEP]
case (2 current big aux)
[PROOF STATE]
proof (state)
this:
invar (Reverse current big aux 0)

goal (2 subgoals):
 1. \<And>current uu_ aux. invar (Reverse current uu_ aux 0) \<Longrightarrow> invar (step (Reverse current uu_ aux 0))
 2. \<And>current big aux v. invar (Reverse current big aux (Suc v)) \<Longrightarrow> invar (step (Reverse current big aux (Suc v)))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
invar (Reverse current big aux 0)
[PROOF STEP]
obtain extra old remained where current:
      "current = Current extra (length extra) old remained"
[PROOF STATE]
proof (prove)
using this:
invar (Reverse current big aux 0)

goal (1 subgoal):
 1. (\<And>extra old remained. current = Current extra (length extra) old remained \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(auto split: current.splits)
[PROOF STATE]
proof (state)
this:
current = Current extra (length extra) old remained

goal (2 subgoals):
 1. \<And>current uu_ aux. invar (Reverse current uu_ aux 0) \<Longrightarrow> invar (step (Reverse current uu_ aux 0))
 2. \<And>current big aux v. invar (Reverse current big aux (Suc v)) \<Longrightarrow> invar (step (Reverse current big aux (Suc v)))
[PROOF STEP]
(* TODO: *)
[PROOF STATE]
proof (state)
this:
current = Current extra (length extra) old remained

goal (2 subgoals):
 1. \<And>current uu_ aux. invar (Reverse current uu_ aux 0) \<Longrightarrow> invar (step (Reverse current uu_ aux 0))
 2. \<And>current big aux v. invar (Reverse current big aux (Suc v)) \<Longrightarrow> invar (step (Reverse current big aux (Suc v)))
[PROOF STEP]
with 2
[PROOF STATE]
proof (chain)
picking this:
invar (Reverse current big aux 0)
current = Current extra (length extra) old remained
[PROOF STEP]
have "\<lbrakk>current = Current extra (length extra) old remained; remained \<le> length aux;
     Stack.list old =
     rev (take (size old - size big) aux) @ rev (take (size old) (rev (Stack.list big)));
     take remained (rev (take (size old - size big) aux)) @
     take (remained - min (length aux) (size old - size big))
      (rev (take (size old) (rev (Stack.list big)))) =
     rev (take remained aux)\<rbrakk>
    \<Longrightarrow> remained \<le> size old"
[PROOF STATE]
proof (prove)
using this:
invar (Reverse current big aux 0)
current = Current extra (length extra) old remained

goal (1 subgoal):
 1. \<lbrakk>current = Current extra (length extra) old remained; remained \<le> length aux; Stack.list old = rev (take (size old - size big) aux) @ rev (take (size old) (rev (Stack.list big))); take remained (rev (take (size old - size big) aux)) @ take (remained - min (length aux) (size old - size big)) (rev (take (size old) (rev (Stack.list big)))) = rev (take remained aux)\<rbrakk> \<Longrightarrow> remained \<le> size old
[PROOF STEP]
by(metis length_rev length_take min.absorb_iff2 size_list_length take_append)
[PROOF STATE]
proof (state)
this:
\<lbrakk>current = Current extra (length extra) old remained; remained \<le> length aux; Stack.list old = rev (take (size old - size big) aux) @ rev (take (size old) (rev (Stack.list big))); take remained (rev (take (size old - size big) aux)) @ take (remained - min (length aux) (size old - size big)) (rev (take (size old) (rev (Stack.list big)))) = rev (take remained aux)\<rbrakk> \<Longrightarrow> remained \<le> size old

goal (2 subgoals):
 1. \<And>current uu_ aux. invar (Reverse current uu_ aux 0) \<Longrightarrow> invar (step (Reverse current uu_ aux 0))
 2. \<And>current big aux v. invar (Reverse current big aux (Suc v)) \<Longrightarrow> invar (step (Reverse current big aux (Suc v)))
[PROOF STEP]
with 2 current
[PROOF STATE]
proof (chain)
picking this:
invar (Reverse current big aux 0)
current = Current extra (length extra) old remained
\<lbrakk>current = Current extra (length extra) old remained; remained \<le> length aux; Stack.list old = rev (take (size old - size big) aux) @ rev (take (size old) (rev (Stack.list big))); take remained (rev (take (size old - size big) aux)) @ take (remained - min (length aux) (size old - size big)) (rev (take (size old) (rev (Stack.list big)))) = rev (take remained aux)\<rbrakk> \<Longrightarrow> remained \<le> size old
[PROOF STEP]
have "remained - size old = 0"
[PROOF STATE]
proof (prove)
using this:
invar (Reverse current big aux 0)
current = Current extra (length extra) old remained
\<lbrakk>current = Current extra (length extra) old remained; remained \<le> length aux; Stack.list old = rev (take (size old - size big) aux) @ rev (take (size old) (rev (Stack.list big))); take remained (rev (take (size old - size big) aux)) @ take (remained - min (length aux) (size old - size big)) (rev (take (size old) (rev (Stack.list big)))) = rev (take remained aux)\<rbrakk> \<Longrightarrow> remained \<le> size old

goal (1 subgoal):
 1. remained - size old = 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
remained - size old = 0

goal (2 subgoals):
 1. \<And>current uu_ aux. invar (Reverse current uu_ aux 0) \<Longrightarrow> invar (step (Reverse current uu_ aux 0))
 2. \<And>current big aux v. invar (Reverse current big aux (Suc v)) \<Longrightarrow> invar (step (Reverse current big aux (Suc v)))
[PROOF STEP]
with current 2
[PROOF STATE]
proof (chain)
picking this:
current = Current extra (length extra) old remained
invar (Reverse current big aux 0)
remained - size old = 0
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
current = Current extra (length extra) old remained
invar (Reverse current big aux 0)
remained - size old = 0

goal (1 subgoal):
 1. invar (step (Reverse current big aux 0))
[PROOF STEP]
by(auto simp: reverseN_drop drop_rev)
[PROOF STATE]
proof (state)
this:
invar (step (Reverse current big aux 0))

goal (1 subgoal):
 1. \<And>current big aux v. invar (Reverse current big aux (Suc v)) \<Longrightarrow> invar (step (Reverse current big aux (Suc v)))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>current big aux v. invar (Reverse current big aux (Suc v)) \<Longrightarrow> invar (step (Reverse current big aux (Suc v)))
[PROOF STEP]
case (3 current big aux count)
[PROOF STATE]
proof (state)
this:
invar (Reverse current big aux (Suc count))

goal (1 subgoal):
 1. \<And>current big aux v. invar (Reverse current big aux (Suc v)) \<Longrightarrow> invar (step (Reverse current big aux (Suc v)))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
invar (Reverse current big aux (Suc count))
[PROOF STEP]
have "0 < size big"
[PROOF STATE]
proof (prove)
using this:
invar (Reverse current big aux (Suc count))

goal (1 subgoal):
 1. 0 < size big
[PROOF STEP]
by(auto split: current.splits)
[PROOF STATE]
proof (state)
this:
0 < size big

goal (1 subgoal):
 1. \<And>current big aux v. invar (Reverse current big aux (Suc v)) \<Longrightarrow> invar (step (Reverse current big aux (Suc v)))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
0 < size big
[PROOF STEP]
have big_not_empty:  "Stack.list big \<noteq> []"
[PROOF STATE]
proof (prove)
using this:
0 < size big

goal (1 subgoal):
 1. Stack.list big \<noteq> []
[PROOF STEP]
by(auto simp: Stack_Proof.size_not_empty  Stack_Proof.list_not_empty)
[PROOF STATE]
proof (state)
this:
Stack.list big \<noteq> []

goal (1 subgoal):
 1. \<And>current big aux v. invar (Reverse current big aux (Suc v)) \<Longrightarrow> invar (step (Reverse current big aux (Suc v)))
[PROOF STEP]
with 3
[PROOF STATE]
proof (chain)
picking this:
invar (Reverse current big aux (Suc count))
Stack.list big \<noteq> []
[PROOF STEP]
have a: "
      rev (Stack.list big) @ aux =
      rev (Stack.list (Stack.pop big)) @ Stack.first big # aux"
[PROOF STATE]
proof (prove)
using this:
invar (Reverse current big aux (Suc count))
Stack.list big \<noteq> []

goal (1 subgoal):
 1. rev (Stack.list big) @ aux = rev (Stack.list (Stack.pop big)) @ Stack.first big # aux
[PROOF STEP]
by(auto simp: rev_tl_hd first_hd split: current.splits)
[PROOF STATE]
proof (state)
this:
rev (Stack.list big) @ aux = rev (Stack.list (Stack.pop big)) @ Stack.first big # aux

goal (1 subgoal):
 1. \<And>current big aux v. invar (Reverse current big aux (Suc v)) \<Longrightarrow> invar (step (Reverse current big aux (Suc v)))
[PROOF STEP]
from 3
[PROOF STATE]
proof (chain)
picking this:
invar (Reverse current big aux (Suc count))
[PROOF STEP]
have "0 < size big"
[PROOF STATE]
proof (prove)
using this:
invar (Reverse current big aux (Suc count))

goal (1 subgoal):
 1. 0 < size big
[PROOF STEP]
by(auto split: current.splits)
[PROOF STATE]
proof (state)
this:
0 < size big

goal (1 subgoal):
 1. \<And>current big aux v. invar (Reverse current big aux (Suc v)) \<Longrightarrow> invar (step (Reverse current big aux (Suc v)))
[PROOF STEP]
from 3 big_not_empty
[PROOF STATE]
proof (chain)
picking this:
invar (Reverse current big aux (Suc count))
Stack.list big \<noteq> []
[PROOF STEP]
have "
      reverseN (Suc count) (Stack.list big) aux =
      reverseN count (Stack.list (Stack.pop big)) (Stack.first big # aux)"
[PROOF STATE]
proof (prove)
using this:
invar (Reverse current big aux (Suc count))
Stack.list big \<noteq> []

goal (1 subgoal):
 1. reverseN (Suc count) (Stack.list big) aux = reverseN count (Stack.list (Stack.pop big)) (Stack.first big # aux)
[PROOF STEP]
using reverseN_tl_hd[of "Suc count" "Stack.list big" aux]
[PROOF STATE]
proof (prove)
using this:
invar (Reverse current big aux (Suc count))
Stack.list big \<noteq> []
\<lbrakk>0 < Suc count; Stack.list big \<noteq> []\<rbrakk> \<Longrightarrow> reverseN (Suc count) (Stack.list big) aux = reverseN (Suc count - Suc 0) (tl (Stack.list big)) (hd (Stack.list big) # aux)

goal (1 subgoal):
 1. reverseN (Suc count) (Stack.list big) aux = reverseN count (Stack.list (Stack.pop big)) (Stack.first big # aux)
[PROOF STEP]
by(auto simp: Stack_Proof.list_not_empty split: current.splits)
[PROOF STATE]
proof (state)
this:
reverseN (Suc count) (Stack.list big) aux = reverseN count (Stack.list (Stack.pop big)) (Stack.first big # aux)

goal (1 subgoal):
 1. \<And>current big aux v. invar (Reverse current big aux (Suc v)) \<Longrightarrow> invar (step (Reverse current big aux (Suc v)))
[PROOF STEP]
with 3 a
[PROOF STATE]
proof (chain)
picking this:
invar (Reverse current big aux (Suc count))
rev (Stack.list big) @ aux = rev (Stack.list (Stack.pop big)) @ Stack.first big # aux
reverseN (Suc count) (Stack.list big) aux = reverseN count (Stack.list (Stack.pop big)) (Stack.first big # aux)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
invar (Reverse current big aux (Suc count))
rev (Stack.list big) @ aux = rev (Stack.list (Stack.pop big)) @ Stack.first big # aux
reverseN (Suc count) (Stack.list big) aux = reverseN count (Stack.list (Stack.pop big)) (Stack.first big # aux)

goal (1 subgoal):
 1. invar (step (Reverse current big aux (Suc count)))
[PROOF STEP]
by(auto split: current.splits)
[PROOF STATE]
proof (state)
this:
invar (step (Reverse current big aux (Suc count)))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma subst_b_flip_eq_one:
  fixes z1::bv and z2::bv and x1::bv and x2::bv
  assumes "[[atom z1]]lst. c1 = [[atom z2]]lst. c2"
    and "atom x1 \<sharp> (z1,z2,c1,c2)"
  shows "(c1[z1::=B_var x1]\<^sub>b) = (c2[z2::=B_var x1]\<^sub>b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. c1[z1::=B_var x1]\<^sub>b = c2[z2::=B_var x1]\<^sub>b
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. c1[z1::=B_var x1]\<^sub>b = c2[z2::=B_var x1]\<^sub>b
[PROOF STEP]
have "(c1[z1::=B_var x1]\<^sub>b) = (x1 \<leftrightarrow> z1) \<bullet> c1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. c1[z1::=B_var x1]\<^sub>b = (x1 \<leftrightarrow> z1) \<bullet> c1
[PROOF STEP]
using assms flip_subst
[PROOF STATE]
proof (prove)
using this:
[[atom z1]]lst. c1 = [[atom z2]]lst. c2
atom x1 \<sharp> (z1, z2, c1, c2)
atom ?bv \<sharp> ?c \<Longrightarrow> (?bv \<leftrightarrow> ?z) \<bullet> ?c = ?c[?z::=B_var ?bv]\<^sub>b

goal (1 subgoal):
 1. c1[z1::=B_var x1]\<^sub>b = (x1 \<leftrightarrow> z1) \<bullet> c1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
c1[z1::=B_var x1]\<^sub>b = (x1 \<leftrightarrow> z1) \<bullet> c1

goal (1 subgoal):
 1. c1[z1::=B_var x1]\<^sub>b = c2[z2::=B_var x1]\<^sub>b
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
c1[z1::=B_var x1]\<^sub>b = (x1 \<leftrightarrow> z1) \<bullet> c1

goal (1 subgoal):
 1. c1[z1::=B_var x1]\<^sub>b = c2[z2::=B_var x1]\<^sub>b
[PROOF STEP]
have  "(c2[z2::=B_var x1]\<^sub>b) = (x1 \<leftrightarrow> z2) \<bullet> c2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. c2[z2::=B_var x1]\<^sub>b = (x1 \<leftrightarrow> z2) \<bullet> c2
[PROOF STEP]
using assms flip_subst
[PROOF STATE]
proof (prove)
using this:
[[atom z1]]lst. c1 = [[atom z2]]lst. c2
atom x1 \<sharp> (z1, z2, c1, c2)
atom ?bv \<sharp> ?c \<Longrightarrow> (?bv \<leftrightarrow> ?z) \<bullet> ?c = ?c[?z::=B_var ?bv]\<^sub>b

goal (1 subgoal):
 1. c2[z2::=B_var x1]\<^sub>b = (x1 \<leftrightarrow> z2) \<bullet> c2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
c2[z2::=B_var x1]\<^sub>b = (x1 \<leftrightarrow> z2) \<bullet> c2

goal (1 subgoal):
 1. c1[z1::=B_var x1]\<^sub>b = c2[z2::=B_var x1]\<^sub>b
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
c1[z1::=B_var x1]\<^sub>b = (x1 \<leftrightarrow> z1) \<bullet> c1
c2[z2::=B_var x1]\<^sub>b = (x1 \<leftrightarrow> z2) \<bullet> c2
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
c1[z1::=B_var x1]\<^sub>b = (x1 \<leftrightarrow> z1) \<bullet> c1
c2[z2::=B_var x1]\<^sub>b = (x1 \<leftrightarrow> z2) \<bullet> c2

goal (1 subgoal):
 1. c1[z1::=B_var x1]\<^sub>b = c2[z2::=B_var x1]\<^sub>b
[PROOF STEP]
using Abs1_eq_iff_all(3)[of z1 c1 z2 c2 z1]  assms
[PROOF STATE]
proof (prove)
using this:
c1[z1::=B_var x1]\<^sub>b = (x1 \<leftrightarrow> z1) \<bullet> c1
c2[z2::=B_var x1]\<^sub>b = (x1 \<leftrightarrow> z2) \<bullet> c2
([[atom z1]]lst. c1 = [[atom z2]]lst. c2) = (\<forall>c. atom c \<sharp> z1 \<longrightarrow> atom c \<sharp> (z1, z2, c1, c2) \<longrightarrow> (z1 \<leftrightarrow> c) \<bullet> c1 = (z2 \<leftrightarrow> c) \<bullet> c2)
[[atom z1]]lst. c1 = [[atom z2]]lst. c2
atom x1 \<sharp> (z1, z2, c1, c2)

goal (1 subgoal):
 1. c1[z1::=B_var x1]\<^sub>b = c2[z2::=B_var x1]\<^sub>b
[PROOF STEP]
by (metis Abs1_eq_iff_fresh(3) flip_commute)
[PROOF STATE]
proof (state)
this:
c1[z1::=B_var x1]\<^sub>b = c2[z2::=B_var x1]\<^sub>b

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma rrk_is_preserved:
fixes A::"'a::{field}^'cols^'rows::{finite, wellorder}"
  and P::"'a::{field}^'rows::{finite, wellorder}^'rows::{finite, wellorder}"
assumes inv_P: "invertible P"
shows "row_rank A = row_rank (P**A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. row_rank A = row_rank (P ** A)
[PROOF STEP]
by (metis row_space_is_preserved row_rank_def inv_P)


[STATEMENT]
lemma results'_gpv_induct [consumes 1, case_names Pure Cont, induct set: results'_gpv]:
  assumes x: "x \<in> results'_gpv gpv"
  and Pure: "\<And>generat gpv. \<lbrakk> generat \<in> set_spmf (the_gpv gpv); x \<in> generat_pures generat \<rbrakk> \<Longrightarrow> P gpv"
  and Cont: "\<And>generat gpv c input.
    \<lbrakk> generat \<in> set_spmf (the_gpv gpv); c \<in> generat_conts generat; x \<in> results'_gpv (c input); P (c input) \<rbrakk> \<Longrightarrow> P gpv"
  shows "P gpv"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P gpv
[PROOF STEP]
using x
[PROOF STATE]
proof (prove)
using this:
x \<in> results'_gpv gpv

goal (1 subgoal):
 1. P gpv
[PROOF STEP]
apply(induction y\<equiv>"x" gpv)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>z xa xb. \<lbrakk>xa \<in> set_pmf z; xb \<in> set_option xa; x \<in> generat_pures xb\<rbrakk> \<Longrightarrow> P (GPV z)
 2. \<And>z xa xb xe xf. \<lbrakk>xa \<in> set_pmf z; xb \<in> set_option xa; xe \<in> generat_conts xb; xf \<in> range xe; x \<in> results'_gpv xf; P xf\<rbrakk> \<Longrightarrow> P (GPV z)
[PROOF STEP]
apply(rule Pure; simp add: in_set_spmf)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>z xa xb xe xf. \<lbrakk>xa \<in> set_pmf z; xb \<in> set_option xa; xe \<in> generat_conts xb; xf \<in> range xe; x \<in> results'_gpv xf; P xf\<rbrakk> \<Longrightarrow> P (GPV z)
[PROOF STEP]
apply(erule imageE, rule Cont, simp add: in_set_spmf, simp, simp, simp)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
.


[STATEMENT]
lemma head_subst[simp]: "head (subst \<rho> s) = head (subst \<rho> (Hd (head s)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. head (subst \<rho> s) = head (subst \<rho> (Hd (head s)))
[PROOF STEP]
by (cases s rule: tm_exhaust_apps) (auto split: hd.split)


[STATEMENT]
lemma f2r_kcomp_pres: "\<R> (f \<circ>\<^sub>K g) = \<R> f ; \<R> g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<R> (f \<circ>\<^sub>K g) = \<R> f ; \<R> g
[PROOF STEP]
by (simp add: r2f_f2r_galois r2f_comp_pres pointfree_idE)


[STATEMENT]
lemma ProcBody:
 assumes WP: "P \<subseteq> P'"
 assumes deriv_body: "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P' body Q,A"
 assumes body: "\<Gamma> p = Some body"
 shows "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P Call p Q,A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma>,\<Theta>\<turnstile>\<^bsub>/F \<^esub>P Call p Q,A
[PROOF STEP]
apply (rule conseqPre [OF _ WP])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma>,\<Theta>\<turnstile>\<^bsub>/F \<^esub>P' Call p Q,A
[PROOF STEP]
apply (rule ProcNoRec1 [rule_format, where P="\<lambda>Z. P'" and Q="\<lambda>Z. Q" and A="\<lambda>Z. A"])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>Z. \<Gamma>,\<Theta>\<turnstile>\<^bsub>/F \<^esub>P' the (\<Gamma> p) Q,A
 2. p \<in> dom \<Gamma>
[PROOF STEP]
apply  (insert body)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>Z. \<Gamma> p = Some body \<Longrightarrow> \<Gamma>,\<Theta>\<turnstile>\<^bsub>/F \<^esub>P' the (\<Gamma> p) Q,A
 2. \<Gamma> p = Some body \<Longrightarrow> p \<in> dom \<Gamma>
[PROOF STEP]
apply  simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<Gamma> p = Some body \<Longrightarrow> \<Gamma>,\<Theta>\<turnstile>\<^bsub>/F \<^esub>P' body Q,A
 2. \<Gamma> p = Some body \<Longrightarrow> p \<in> dom \<Gamma>
[PROOF STEP]
apply  (rule hoare_augment_context [OF deriv_body])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<Gamma> p = Some body \<Longrightarrow> \<Theta> \<subseteq> \<Theta>
 2. \<Gamma> p = Some body \<Longrightarrow> p \<in> dom \<Gamma>
[PROOF STEP]
apply  blast
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma> p = Some body \<Longrightarrow> p \<in> dom \<Gamma>
[PROOF STEP]
apply fastforce
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma FOREACHi_refine_rcg'[refine]:
  fixes \<alpha> :: "'S \<Rightarrow> 'Sa"
  fixes S :: "'S set"
  fixes S' :: "'Sa set"
  assumes INJ: "inj_on \<alpha> S"
  assumes REFS: "S' = \<alpha>`S"
  assumes REF0: "(\<sigma>0,\<sigma>0')\<in>R"
  assumes REFSTEP: "\<And>x it \<sigma> x' it' \<sigma>'. \<lbrakk>
    x'=\<alpha> x; x\<in>it; x'\<in>it'; it'=\<alpha>`it; it\<subseteq>S; it'\<subseteq>S';
    \<Phi>' it' \<sigma>';
    (\<sigma>,\<sigma>')\<in>R
  \<rbrakk> \<Longrightarrow> f x \<sigma> \<le> \<Down>R (f' x' \<sigma>')"
  shows "FOREACH S f \<sigma>0 \<le> \<Down>R (FOREACHi \<Phi>' S' f' \<sigma>0')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. FOREACH S f \<sigma>0 \<le> \<Down> R (FOREACH\<^bsup>\<Phi>'\<^esup> S' f' \<sigma>0')
[PROOF STEP]
unfolding FOREACH_def FOREACHi_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. FOREACH\<^sub>C S (\<lambda>_. True) f \<sigma>0 \<le> \<Down> R (FOREACH\<^sub>C\<^bsup>\<Phi>'\<^esup> S' (\<lambda>_. True) f' \<sigma>0')
[PROOF STEP]
apply (rule FOREACHci_refine_rcg')
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. inj_on ?\<alpha> S
 2. S' = ?\<alpha> ` S
 3. (\<sigma>0, \<sigma>0') \<in> R
 4. \<And>it \<sigma> it' \<sigma>'. \<lbrakk>it' = ?\<alpha> ` it; it \<subseteq> S; it' \<subseteq> S'; \<Phi>' it' \<sigma>'; (\<sigma>, \<sigma>') \<in> R\<rbrakk> \<Longrightarrow> True = True
 5. \<And>x it \<sigma> x' it' \<sigma>'. \<lbrakk>x' = ?\<alpha> x; x \<in> it; x' \<in> it'; it' = ?\<alpha> ` it; it \<subseteq> S; it' \<subseteq> S'; \<Phi>' it' \<sigma>'; True; True; (\<sigma>, \<sigma>') \<in> R\<rbrakk> \<Longrightarrow> f x \<sigma> \<le> \<Down> R (f' x' \<sigma>')
[PROOF STEP]
apply (rule assms)+
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>it \<sigma> it' \<sigma>'. \<lbrakk>it' = \<alpha> ` it; it \<subseteq> S; it' \<subseteq> S'; \<Phi>' it' \<sigma>'; (\<sigma>, \<sigma>') \<in> R\<rbrakk> \<Longrightarrow> True = True
 2. \<And>x it \<sigma> x' it' \<sigma>'. \<lbrakk>x' = \<alpha> x; x \<in> it; x' \<in> it'; it' = \<alpha> ` it; it \<subseteq> S; it' \<subseteq> S'; \<Phi>' it' \<sigma>'; True; True; (\<sigma>, \<sigma>') \<in> R\<rbrakk> \<Longrightarrow> f x \<sigma> \<le> \<Down> R (f' x' \<sigma>')
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x it \<sigma> x' it' \<sigma>'. \<lbrakk>x' = \<alpha> x; x \<in> it; x' \<in> it'; it' = \<alpha> ` it; it \<subseteq> S; it' \<subseteq> S'; \<Phi>' it' \<sigma>'; True; True; (\<sigma>, \<sigma>') \<in> R\<rbrakk> \<Longrightarrow> f x \<sigma> \<le> \<Down> R (f' x' \<sigma>')
[PROOF STEP]
apply (rule REFSTEP, assumption+)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma LIST_FOREACH'_transfer_nres[refine_transfer]:
  assumes "nres_of tsl \<le> tsl'"
  assumes "\<And>x \<sigma>. nres_of (f x \<sigma>) \<le> f' x \<sigma>"
  shows "nres_of (
    do {
      xs\<leftarrow>tsl;
      foldli xs (case_dres False False c) (\<lambda>x s. s\<bind>f x) (dRETURN \<sigma>)
    }) \<le> LIST_FOREACH' tsl' c f' \<sigma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nres_of (tsl \<bind> (\<lambda>xs. foldli xs (case_dres False False c) (\<lambda>x s. s \<bind> f x) (dRETURN \<sigma>))) \<le> LIST_FOREACH' tsl' c f' \<sigma>
[PROOF STEP]
unfolding LIST_FOREACH'_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nres_of (tsl \<bind> (\<lambda>xs. foldli xs (case_dres False False c) (\<lambda>x s. s \<bind> f x) (dRETURN \<sigma>))) \<le> tsl' \<bind> (\<lambda>xs. nfoldli xs c f' \<sigma>)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
nres_of tsl \<le> tsl'
nres_of (f ?x ?\<sigma>) \<le> f' ?x ?\<sigma>

goal (1 subgoal):
 1. nres_of (tsl \<bind> (\<lambda>xs. foldli xs (case_dres False False c) (\<lambda>x s. s \<bind> f x) (dRETURN \<sigma>))) \<le> tsl' \<bind> (\<lambda>xs. nfoldli xs c f' \<sigma>)
[PROOF STEP]
by refine_transfer


[STATEMENT]
lemma sum_4_elems:
  shows "(\<Sum>i<(4::nat). f i) = f 0 + f 1 + f 2 + f 3"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum f {..<4} = f 0 + f 1 + f 2 + f 3
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. sum f {..<4} = f 0 + f 1 + f 2 + f 3
[PROOF STEP]
have "(\<Sum>i<(4::nat). f i) = (\<Sum>i<(3::nat). f i)  + f 3"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum f {..<4} = sum f {..<3} + f 3
[PROOF STEP]
by (metis Suc_numeral semiring_norm(2) semiring_norm(8) sum.lessThan_Suc)
[PROOF STATE]
proof (state)
this:
sum f {..<4} = sum f {..<3} + f 3

goal (1 subgoal):
 1. sum f {..<4} = f 0 + f 1 + f 2 + f 3
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
sum f {..<4} = sum f {..<3} + f 3

goal (1 subgoal):
 1. sum f {..<4} = f 0 + f 1 + f 2 + f 3
[PROOF STEP]
have "(\<Sum>i<(3::nat). f i) = (\<Sum>i<(2::nat). f i) + f 2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum f {..<3} = sum f {..<2} + f 2
[PROOF STEP]
by (metis Suc_1 add_2_eq_Suc' nat_1_add_1 numeral_code(3) numerals(1)
        one_plus_numeral_commute sum.lessThan_Suc)
[PROOF STATE]
proof (state)
this:
sum f {..<3} = sum f {..<2} + f 2

goal (1 subgoal):
 1. sum f {..<4} = f 0 + f 1 + f 2 + f 3
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
sum f {..<3} = sum f {..<2} + f 2

goal (1 subgoal):
 1. sum f {..<4} = f 0 + f 1 + f 2 + f 3
[PROOF STEP]
have "(\<Sum>i<(2::nat). f i) = (\<Sum>i<(1::nat). f i) + f 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum f {..<2} = sum f {..<1} + f 1
[PROOF STEP]
by (metis Suc_1 sum.lessThan_Suc)
[PROOF STATE]
proof (state)
this:
sum f {..<2} = sum f {..<1} + f 1

goal (1 subgoal):
 1. sum f {..<4} = f 0 + f 1 + f 2 + f 3
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
sum f {..<4} = sum f {..<3} + f 3
sum f {..<3} = sum f {..<2} + f 2
sum f {..<2} = sum f {..<1} + f 1
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
sum f {..<4} = sum f {..<3} + f 3
sum f {..<3} = sum f {..<2} + f 2
sum f {..<2} = sum f {..<1} + f 1

goal (1 subgoal):
 1. sum f {..<4} = f 0 + f 1 + f 2 + f 3
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
sum f {..<4} = f 0 + f 1 + f 2 + f 3

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma vreal_inverses_law_multiplication:
  assumes "x \<in>\<^sub>\<circ> \<real>\<^sub>\<circ>" and "x \<noteq> 0\<^sub>\<real>"
  shows "x *\<^sub>\<real> x\<inverse>\<^sub>\<real> = 1\<^sub>\<real>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x *\<^sub>\<real> x\<inverse>\<^sub>\<real> = 1\<^sub>\<real>
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x *\<^sub>\<real> x\<inverse>\<^sub>\<real> = 1\<^sub>\<real>
[PROOF STEP]
have "x' \<noteq> 0 \<Longrightarrow> x' * inverse x' = 1" for x' :: real
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x' \<noteq> 0 \<Longrightarrow> x' * inverse x' = 1
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
?x' \<noteq> 0 \<Longrightarrow> ?x' * inverse ?x' = 1

goal (1 subgoal):
 1. x *\<^sub>\<real> x\<inverse>\<^sub>\<real> = 1\<^sub>\<real>
[PROOF STEP]
from this[untransferred, OF assms]
[PROOF STATE]
proof (chain)
picking this:
x *\<^sub>\<real> x\<inverse>\<^sub>\<real> = 1\<^sub>\<real>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
x *\<^sub>\<real> x\<inverse>\<^sub>\<real> = 1\<^sub>\<real>

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

goal:
No subgoals!
[PROOF STEP]
qed