[STATEMENT]
lemma thetaWhileZOT_ZOretrT:
"thetaWhileZOT \<subseteq> ZOretrT (thetaWhileZOT Un ZObisT)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. thetaWhileZOT \<subseteq> ZOretrT (thetaWhileZOT \<union> ZObisT)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. thetaWhileZOT \<subseteq> ZOretrT (thetaWhileZOT \<union> ZObisT)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. thetaWhileZOT \<subseteq> ZOretrT (thetaWhileZOT \<union> ZObisT)
[PROOF STEP]
fix tst c d
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. thetaWhileZOT \<subseteq> ZOretrT (thetaWhileZOT \<union> ZObisT)
[PROOF STEP]
assume tst: "compatTst tst" and c_d: "c \<approx>01T d"
[PROOF STATE]
proof (state)
this:
compatTst tst
c \<approx>01T d

goal (1 subgoal):
 1. thetaWhileZOT \<subseteq> ZOretrT (thetaWhileZOT \<union> ZObisT)
[PROOF STEP]
hence matchC_ZOC: "matchC_ZOC ZObisT c d"
     and matchT_T: "matchT_T c d"
[PROOF STATE]
proof (prove)
using this:
compatTst tst
c \<approx>01T d

goal (1 subgoal):
 1. matchC_ZOC ZObisT c d &&& matchT_T c d
[PROOF STEP]
using ZObisT_matchC_ZOC ZObisT_matchT_T
[PROOF STATE]
proof (prove)
using this:
compatTst tst
c \<approx>01T d
?s \<approx>01T ?t \<Longrightarrow> matchC_ZOC ZObisT ?s ?t
?s \<approx>01T ?t \<Longrightarrow> matchT_T ?s ?t

goal (1 subgoal):
 1. matchC_ZOC ZObisT c d &&& matchT_T c d
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
matchC_ZOC ZObisT c d
matchT_T c d

goal (1 subgoal):
 1. thetaWhileZOT \<subseteq> ZOretrT (thetaWhileZOT \<union> ZObisT)
[PROOF STEP]
have "(While tst c, While tst d) \<in> ZOretrT (thetaWhileZOT Un ZObisT)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (while tst do c, while tst do d) \<in> ZOretrT (thetaWhileZOT \<union> ZObisT)
[PROOF STEP]
unfolding ZOretrT_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (while tst do c, while tst do d) \<in> {(c, d). matchC_ZOC (thetaWhileZOT \<union> ZObisT) c d \<and> matchT_T c d}
[PROOF STEP]
proof (clarify, intro conjI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. matchC_ZOC (thetaWhileZOT \<union> ZObisT) (while tst do c) (while tst do d)
 2. matchT_T (while tst do c) (while tst do d)
[PROOF STEP]
show "matchC_ZOC (thetaWhileZOT \<union> ZObisT) (While tst c) (While tst d)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. matchC_ZOC (thetaWhileZOT \<union> ZObisT) (while tst do c) (while tst do d)
[PROOF STEP]
unfolding matchC_ZOC_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>s t c' s'. s \<approx> t \<and> (while tst do c, s) \<rightarrow>c (c', s') \<longrightarrow> s' \<approx> t \<and> (c', while tst do d) \<in> thetaWhileZOT \<union> ZObisT \<or> (\<exists>d' t'. (while tst do d, t) \<rightarrow>c (d', t') \<and> s' \<approx> t' \<and> (c', d') \<in> thetaWhileZOT \<union> ZObisT)
[PROOF STEP]
proof (tactic \<open>mauto_no_simp_tac @{context}\<close>)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>s t c' s'. \<lbrakk>s \<approx> t; (while tst do c, s) \<rightarrow>c (c', s')\<rbrakk> \<Longrightarrow> s' \<approx> t \<and> (c', while tst do d) \<in> thetaWhileZOT \<union> ZObisT \<or> (\<exists>d' t'. (while tst do d, t) \<rightarrow>c (d', t') \<and> s' \<approx> t' \<and> (c', d') \<in> thetaWhileZOT \<union> ZObisT)
[PROOF STEP]
fix s t c' s'
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>s t c' s'. \<lbrakk>s \<approx> t; (while tst do c, s) \<rightarrow>c (c', s')\<rbrakk> \<Longrightarrow> s' \<approx> t \<and> (c', while tst do d) \<in> thetaWhileZOT \<union> ZObisT \<or> (\<exists>d' t'. (while tst do d, t) \<rightarrow>c (d', t') \<and> s' \<approx> t' \<and> (c', d') \<in> thetaWhileZOT \<union> ZObisT)
[PROOF STEP]
assume st: "s \<approx> t"
[PROOF STATE]
proof (state)
this:
s \<approx> t

goal (1 subgoal):
 1. \<And>s t c' s'. \<lbrakk>s \<approx> t; (while tst do c, s) \<rightarrow>c (c', s')\<rbrakk> \<Longrightarrow> s' \<approx> t \<and> (c', while tst do d) \<in> thetaWhileZOT \<union> ZObisT \<or> (\<exists>d' t'. (while tst do d, t) \<rightarrow>c (d', t') \<and> s' \<approx> t' \<and> (c', d') \<in> thetaWhileZOT \<union> ZObisT)
[PROOF STEP]
assume "(While tst c, s) \<rightarrow>c (c', s')"
[PROOF STATE]
proof (state)
this:
(while tst do c, s) \<rightarrow>c (c', s')

goal (1 subgoal):
 1. \<And>s t c' s'. \<lbrakk>s \<approx> t; (while tst do c, s) \<rightarrow>c (c', s')\<rbrakk> \<Longrightarrow> s' \<approx> t \<and> (c', while tst do d) \<in> thetaWhileZOT \<union> ZObisT \<or> (\<exists>d' t'. (while tst do d, t) \<rightarrow>c (d', t') \<and> s' \<approx> t' \<and> (c', d') \<in> thetaWhileZOT \<union> ZObisT)
[PROOF STEP]
thus
       "(s' \<approx> t \<and> (c', While tst d) \<in> thetaWhileZOT \<union> ZObisT) \<or>
        (\<exists>d' t'. (While tst d, t) \<rightarrow>c (d', t') \<and> s' \<approx> t' \<and> (c', d') \<in> thetaWhileZOT \<union> ZObisT)"
[PROOF STATE]
proof (prove)
using this:
(while tst do c, s) \<rightarrow>c (c', s')

goal (1 subgoal):
 1. s' \<approx> t \<and> (c', while tst do d) \<in> thetaWhileZOT \<union> ZObisT \<or> (\<exists>d' t'. (while tst do d, t) \<rightarrow>c (d', t') \<and> s' \<approx> t' \<and> (c', d') \<in> thetaWhileZOT \<union> ZObisT)
[PROOF STEP]
apply -
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (while tst do c, s) \<rightarrow>c (c', s') \<Longrightarrow> s' \<approx> t \<and> (c', while tst do d) \<in> thetaWhileZOT \<union> ZObisT \<or> (\<exists>d' t'. (while tst do d, t) \<rightarrow>c (d', t') \<and> s' \<approx> t' \<and> (c', d') \<in> thetaWhileZOT \<union> ZObisT)
[PROOF STEP]
apply(erule While_transC_invert)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>tval tst s; c' = c ;; while tst do c; s' = s\<rbrakk> \<Longrightarrow> s' \<approx> t \<and> (c', while tst do d) \<in> thetaWhileZOT \<union> ZObisT \<or> (\<exists>d' t'. (while tst do d, t) \<rightarrow>c (d', t') \<and> s' \<approx> t' \<and> (c', d') \<in> thetaWhileZOT \<union> ZObisT)
[PROOF STEP]
unfolding thetaWhileZOT_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>tval tst s; c' = c ;; while tst do c; s' = s\<rbrakk> \<Longrightarrow> s' \<approx> t \<and> (c', while tst do d) \<in> {(while tst do c, while tst do d) |tst c d. compatTst tst \<and> c \<approx>01T d} \<union> {(c1 ;; while tst do c, d1 ;; while tst do d) |tst c1 d1 c d. compatTst tst \<and> c1 \<approx>01T d1 \<and> c \<approx>01T d} \<union> ZObisT \<or> (\<exists>d' t'. (while tst do d, t) \<rightarrow>c (d', t') \<and> s' \<approx> t' \<and> (c', d') \<in> {(while tst do c, while tst do d) |tst c d. compatTst tst \<and> c \<approx>01T d} \<union> {(c1 ;; while tst do c, d1 ;; while tst do d) |tst c1 d1 c d. compatTst tst \<and> c1 \<approx>01T d1 \<and> c \<approx>01T d} \<union> ZObisT)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>tval tst s; c' = c ;; while tst do c; s' = s\<rbrakk> \<Longrightarrow> s \<approx> t \<and> c ;; while tst do c \<approx>01T while tst do d \<or> (\<exists>d' t'. (while tst do d, t) \<rightarrow>c (d', t') \<and> s \<approx> t' \<and> ((\<exists>d1 d. d' = d1 ;; while tst do d \<and> compatTst tst \<and> c \<approx>01T d1 \<and> c \<approx>01T d) \<or> c ;; while tst do c \<approx>01T d'))
[PROOF STEP]
by (metis WhileTrue c_d compatTst_def st tst)
[PROOF STATE]
proof (state)
this:
s' \<approx> t \<and> (c', while tst do d) \<in> thetaWhileZOT \<union> ZObisT \<or> (\<exists>d' t'. (while tst do d, t) \<rightarrow>c (d', t') \<and> s' \<approx> t' \<and> (c', d') \<in> thetaWhileZOT \<union> ZObisT)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
matchC_ZOC (thetaWhileZOT \<union> ZObisT) (while tst do c) (while tst do d)

goal (1 subgoal):
 1. matchT_T (while tst do c) (while tst do d)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. matchT_T (while tst do c) (while tst do d)
[PROOF STEP]
show "matchT_T (While tst c) (While tst d)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. matchT_T (while tst do c) (while tst do d)
[PROOF STEP]
unfolding matchT_T_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>s t s'. s \<approx> t \<and> (while tst do c, s) \<rightarrow>t s' \<longrightarrow> (\<exists>t'. (while tst do d, t) \<rightarrow>t t' \<and> s' \<approx> t')
[PROOF STEP]
proof (tactic \<open>mauto_no_simp_tac @{context}\<close>)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>s t s'. \<lbrakk>s \<approx> t; (while tst do c, s) \<rightarrow>t s'\<rbrakk> \<Longrightarrow> \<exists>t'. (while tst do d, t) \<rightarrow>t t' \<and> s' \<approx> t'
[PROOF STEP]
fix s t s'
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>s t s'. \<lbrakk>s \<approx> t; (while tst do c, s) \<rightarrow>t s'\<rbrakk> \<Longrightarrow> \<exists>t'. (while tst do d, t) \<rightarrow>t t' \<and> s' \<approx> t'
[PROOF STEP]
assume st: "s \<approx> t"
[PROOF STATE]
proof (state)
this:
s \<approx> t

goal (1 subgoal):
 1. \<And>s t s'. \<lbrakk>s \<approx> t; (while tst do c, s) \<rightarrow>t s'\<rbrakk> \<Longrightarrow> \<exists>t'. (while tst do d, t) \<rightarrow>t t' \<and> s' \<approx> t'
[PROOF STEP]
assume "(While tst c, s) \<rightarrow>t s'"
[PROOF STATE]
proof (state)
this:
(while tst do c, s) \<rightarrow>t s'

goal (1 subgoal):
 1. \<And>s t s'. \<lbrakk>s \<approx> t; (while tst do c, s) \<rightarrow>t s'\<rbrakk> \<Longrightarrow> \<exists>t'. (while tst do d, t) \<rightarrow>t t' \<and> s' \<approx> t'
[PROOF STEP]
thus "\<exists>t'. (While tst d, t) \<rightarrow>t t' \<and> s' \<approx> t' "
[PROOF STATE]
proof (prove)
using this:
(while tst do c, s) \<rightarrow>t s'

goal (1 subgoal):
 1. \<exists>t'. (while tst do d, t) \<rightarrow>t t' \<and> s' \<approx> t'
[PROOF STEP]
apply -
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (while tst do c, s) \<rightarrow>t s' \<Longrightarrow> \<exists>t'. (while tst do d, t) \<rightarrow>t t' \<and> s' \<approx> t'
[PROOF STEP]
apply(erule While_transT_invert)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> tval tst s; s' = s\<rbrakk> \<Longrightarrow> \<exists>t'. (while tst do d, t) \<rightarrow>t t' \<and> s' \<approx> t'
[PROOF STEP]
unfolding thetaWhileZOT_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> tval tst s; s' = s\<rbrakk> \<Longrightarrow> \<exists>t'. (while tst do d, t) \<rightarrow>t t' \<and> s' \<approx> t'
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> tval tst s; s' = s\<rbrakk> \<Longrightarrow> \<exists>t'. (while tst do d, t) \<rightarrow>t t' \<and> s \<approx> t'
[PROOF STEP]
by (metis PL.WhileFalse compatTst_def st tst)
[PROOF STATE]
proof (state)
this:
\<exists>t'. (while tst do d, t) \<rightarrow>t t' \<and> s' \<approx> t'

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
matchT_T (while tst do c) (while tst do d)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(while tst do c, while tst do d) \<in> ZOretrT (thetaWhileZOT \<union> ZObisT)

goal (1 subgoal):
 1. thetaWhileZOT \<subseteq> ZOretrT (thetaWhileZOT \<union> ZObisT)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>compatTst ?tst3; ?c3 \<approx>01T ?d3\<rbrakk> \<Longrightarrow> (while ?tst3 do ?c3, while ?tst3 do ?d3) \<in> ZOretrT (thetaWhileZOT \<union> ZObisT)

goal (1 subgoal):
 1. thetaWhileZOT \<subseteq> ZOretrT (thetaWhileZOT \<union> ZObisT)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<lbrakk>compatTst ?tst3; ?c3 \<approx>01T ?d3\<rbrakk> \<Longrightarrow> (while ?tst3 do ?c3, while ?tst3 do ?d3) \<in> ZOretrT (thetaWhileZOT \<union> ZObisT)

goal (1 subgoal):
 1. thetaWhileZOT \<subseteq> ZOretrT (thetaWhileZOT \<union> ZObisT)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
\<lbrakk>compatTst ?tst3; ?c3 \<approx>01T ?d3\<rbrakk> \<Longrightarrow> (while ?tst3 do ?c3, while ?tst3 do ?d3) \<in> ZOretrT (thetaWhileZOT \<union> ZObisT)

goal (1 subgoal):
 1. thetaWhileZOT \<subseteq> ZOretrT (thetaWhileZOT \<union> ZObisT)
[PROOF STEP]
fix tst c1 d1  c d
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. thetaWhileZOT \<subseteq> ZOretrT (thetaWhileZOT \<union> ZObisT)
[PROOF STEP]
assume tst: "compatTst tst" and c1d1: "c1 \<approx>01T d1" and c_d: "c \<approx>01T d"
[PROOF STATE]
proof (state)
this:
compatTst tst
c1 \<approx>01T d1
c \<approx>01T d

goal (1 subgoal):
 1. thetaWhileZOT \<subseteq> ZOretrT (thetaWhileZOT \<union> ZObisT)
[PROOF STEP]
hence matchC_ZOC1: "matchC_ZOC ZObisT c1 d1" and matchC_ZOC: "matchC_ZOC ZObisT c d"
     and matchT_T1: "matchT_T c1 d1" and matchT_T: "matchT_T c d"
[PROOF STATE]
proof (prove)
using this:
compatTst tst
c1 \<approx>01T d1
c \<approx>01T d

goal (1 subgoal):
 1. (matchC_ZOC ZObisT c1 d1 &&& matchC_ZOC ZObisT c d) &&& matchT_T c1 d1 &&& matchT_T c d
[PROOF STEP]
using ZObisT_matchC_ZOC ZObisT_matchT_T
[PROOF STATE]
proof (prove)
using this:
compatTst tst
c1 \<approx>01T d1
c \<approx>01T d
?s \<approx>01T ?t \<Longrightarrow> matchC_ZOC ZObisT ?s ?t
?s \<approx>01T ?t \<Longrightarrow> matchT_T ?s ?t

goal (1 subgoal):
 1. (matchC_ZOC ZObisT c1 d1 &&& matchC_ZOC ZObisT c d) &&& matchT_T c1 d1 &&& matchT_T c d
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
matchC_ZOC ZObisT c1 d1
matchC_ZOC ZObisT c d
matchT_T c1 d1
matchT_T c d

goal (1 subgoal):
 1. thetaWhileZOT \<subseteq> ZOretrT (thetaWhileZOT \<union> ZObisT)
[PROOF STEP]
have "(c1 ;; (While tst c), d1 ;; (While tst d)) \<in> ZOretrT (thetaWhileZOT Un ZObisT)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (c1 ;; while tst do c, d1 ;; while tst do d) \<in> ZOretrT (thetaWhileZOT \<union> ZObisT)
[PROOF STEP]
unfolding ZOretrT_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (c1 ;; while tst do c, d1 ;; while tst do d) \<in> {(c, d). matchC_ZOC (thetaWhileZOT \<union> ZObisT) c d \<and> matchT_T c d}
[PROOF STEP]
proof (clarify, intro conjI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. matchC_ZOC (thetaWhileZOT \<union> ZObisT) (c1 ;; while tst do c) (d1 ;; while tst do d)
 2. matchT_T (c1 ;; while tst do c) (d1 ;; while tst do d)
[PROOF STEP]
show "matchC_ZOC (thetaWhileZOT \<union> ZObisT) (c1 ;; (While tst c)) (d1 ;; (While tst d))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. matchC_ZOC (thetaWhileZOT \<union> ZObisT) (c1 ;; while tst do c) (d1 ;; while tst do d)
[PROOF STEP]
unfolding matchC_ZOC_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>s t c' s'. s \<approx> t \<and> (c1 ;; while tst do c, s) \<rightarrow>c (c', s') \<longrightarrow> s' \<approx> t \<and> (c', d1 ;; while tst do d) \<in> thetaWhileZOT \<union> ZObisT \<or> (\<exists>d' t'. (d1 ;; while tst do d, t) \<rightarrow>c (d', t') \<and> s' \<approx> t' \<and> (c', d') \<in> thetaWhileZOT \<union> ZObisT)
[PROOF STEP]
proof (tactic \<open>mauto_no_simp_tac @{context}\<close>)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>s t c' s'. \<lbrakk>s \<approx> t; (c1 ;; while tst do c, s) \<rightarrow>c (c', s')\<rbrakk> \<Longrightarrow> s' \<approx> t \<and> (c', d1 ;; while tst do d) \<in> thetaWhileZOT \<union> ZObisT \<or> (\<exists>d' t'. (d1 ;; while tst do d, t) \<rightarrow>c (d', t') \<and> s' \<approx> t' \<and> (c', d') \<in> thetaWhileZOT \<union> ZObisT)
[PROOF STEP]
fix s t c' s'
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>s t c' s'. \<lbrakk>s \<approx> t; (c1 ;; while tst do c, s) \<rightarrow>c (c', s')\<rbrakk> \<Longrightarrow> s' \<approx> t \<and> (c', d1 ;; while tst do d) \<in> thetaWhileZOT \<union> ZObisT \<or> (\<exists>d' t'. (d1 ;; while tst do d, t) \<rightarrow>c (d', t') \<and> s' \<approx> t' \<and> (c', d') \<in> thetaWhileZOT \<union> ZObisT)
[PROOF STEP]
assume st: "s \<approx> t"
[PROOF STATE]
proof (state)
this:
s \<approx> t

goal (1 subgoal):
 1. \<And>s t c' s'. \<lbrakk>s \<approx> t; (c1 ;; while tst do c, s) \<rightarrow>c (c', s')\<rbrakk> \<Longrightarrow> s' \<approx> t \<and> (c', d1 ;; while tst do d) \<in> thetaWhileZOT \<union> ZObisT \<or> (\<exists>d' t'. (d1 ;; while tst do d, t) \<rightarrow>c (d', t') \<and> s' \<approx> t' \<and> (c', d') \<in> thetaWhileZOT \<union> ZObisT)
[PROOF STEP]
assume "(c1 ;; (While tst c), s) \<rightarrow>c (c', s')"
[PROOF STATE]
proof (state)
this:
(c1 ;; while tst do c, s) \<rightarrow>c (c', s')

goal (1 subgoal):
 1. \<And>s t c' s'. \<lbrakk>s \<approx> t; (c1 ;; while tst do c, s) \<rightarrow>c (c', s')\<rbrakk> \<Longrightarrow> s' \<approx> t \<and> (c', d1 ;; while tst do d) \<in> thetaWhileZOT \<union> ZObisT \<or> (\<exists>d' t'. (d1 ;; while tst do d, t) \<rightarrow>c (d', t') \<and> s' \<approx> t' \<and> (c', d') \<in> thetaWhileZOT \<union> ZObisT)
[PROOF STEP]
thus
       "(s' \<approx> t \<and> (c', d1 ;; (While tst d)) \<in> thetaWhileZOT \<union> ZObisT) \<or>
        (\<exists>d' t'. (d1 ;; (While tst d), t) \<rightarrow>c (d', t') \<and> s' \<approx> t' \<and> (c', d') \<in> thetaWhileZOT \<union> ZObisT)"
[PROOF STATE]
proof (prove)
using this:
(c1 ;; while tst do c, s) \<rightarrow>c (c', s')

goal (1 subgoal):
 1. s' \<approx> t \<and> (c', d1 ;; while tst do d) \<in> thetaWhileZOT \<union> ZObisT \<or> (\<exists>d' t'. (d1 ;; while tst do d, t) \<rightarrow>c (d', t') \<and> s' \<approx> t' \<and> (c', d') \<in> thetaWhileZOT \<union> ZObisT)
[PROOF STEP]
apply -
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (c1 ;; while tst do c, s) \<rightarrow>c (c', s') \<Longrightarrow> s' \<approx> t \<and> (c', d1 ;; while tst do d) \<in> thetaWhileZOT \<union> ZObisT \<or> (\<exists>d' t'. (d1 ;; while tst do d, t) \<rightarrow>c (d', t') \<and> s' \<approx> t' \<and> (c', d') \<in> thetaWhileZOT \<union> ZObisT)
[PROOF STEP]
proof(erule Seq_transC_invert)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>c1'. \<lbrakk>(c1, s) \<rightarrow>c (c1', s'); c' = c1' ;; while tst do c\<rbrakk> \<Longrightarrow> s' \<approx> t \<and> (c', d1 ;; while tst do d) \<in> thetaWhileZOT \<union> ZObisT \<or> (\<exists>d' t'. (d1 ;; while tst do d, t) \<rightarrow>c (d', t') \<and> s' \<approx> t' \<and> (c', d') \<in> thetaWhileZOT \<union> ZObisT)
 2. \<lbrakk>(c1, s) \<rightarrow>t s'; c' = while tst do c\<rbrakk> \<Longrightarrow> s' \<approx> t \<and> (c', d1 ;; while tst do d) \<in> thetaWhileZOT \<union> ZObisT \<or> (\<exists>d' t'. (d1 ;; while tst do d, t) \<rightarrow>c (d', t') \<and> s' \<approx> t' \<and> (c', d') \<in> thetaWhileZOT \<union> ZObisT)
[PROOF STEP]
fix c1'
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>c1'. \<lbrakk>(c1, s) \<rightarrow>c (c1', s'); c' = c1' ;; while tst do c\<rbrakk> \<Longrightarrow> s' \<approx> t \<and> (c', d1 ;; while tst do d) \<in> thetaWhileZOT \<union> ZObisT \<or> (\<exists>d' t'. (d1 ;; while tst do d, t) \<rightarrow>c (d', t') \<and> s' \<approx> t' \<and> (c', d') \<in> thetaWhileZOT \<union> ZObisT)
 2. \<lbrakk>(c1, s) \<rightarrow>t s'; c' = while tst do c\<rbrakk> \<Longrightarrow> s' \<approx> t \<and> (c', d1 ;; while tst do d) \<in> thetaWhileZOT \<union> ZObisT \<or> (\<exists>d' t'. (d1 ;; while tst do d, t) \<rightarrow>c (d', t') \<and> s' \<approx> t' \<and> (c', d') \<in> thetaWhileZOT \<union> ZObisT)
[PROOF STEP]
assume "(c1, s) \<rightarrow>c (c1', s')" and c': "c' = c1' ;; (While tst c)"
[PROOF STATE]
proof (state)
this:
(c1, s) \<rightarrow>c (c1', s')
c' = c1' ;; while tst do c

goal (2 subgoals):
 1. \<And>c1'. \<lbrakk>(c1, s) \<rightarrow>c (c1', s'); c' = c1' ;; while tst do c\<rbrakk> \<Longrightarrow> s' \<approx> t \<and> (c', d1 ;; while tst do d) \<in> thetaWhileZOT \<union> ZObisT \<or> (\<exists>d' t'. (d1 ;; while tst do d, t) \<rightarrow>c (d', t') \<and> s' \<approx> t' \<and> (c', d') \<in> thetaWhileZOT \<union> ZObisT)
 2. \<lbrakk>(c1, s) \<rightarrow>t s'; c' = while tst do c\<rbrakk> \<Longrightarrow> s' \<approx> t \<and> (c', d1 ;; while tst do d) \<in> thetaWhileZOT \<union> ZObisT \<or> (\<exists>d' t'. (d1 ;; while tst do d, t) \<rightarrow>c (d', t') \<and> s' \<approx> t' \<and> (c', d') \<in> thetaWhileZOT \<union> ZObisT)
[PROOF STEP]
hence
         "(s' \<approx> t \<and> c1' \<approx>01T d1) \<or>
          (\<exists>d' t'. (d1, t) \<rightarrow>c (d', t') \<and> s' \<approx> t' \<and> c1' \<approx>01T d')"
[PROOF STATE]
proof (prove)
using this:
(c1, s) \<rightarrow>c (c1', s')
c' = c1' ;; while tst do c

goal (1 subgoal):
 1. s' \<approx> t \<and> c1' \<approx>01T d1 \<or> (\<exists>d' t'. (d1, t) \<rightarrow>c (d', t') \<and> s' \<approx> t' \<and> c1' \<approx>01T d')
[PROOF STEP]
using st matchC_ZOC1
[PROOF STATE]
proof (prove)
using this:
(c1, s) \<rightarrow>c (c1', s')
c' = c1' ;; while tst do c
s \<approx> t
matchC_ZOC ZObisT c1 d1

goal (1 subgoal):
 1. s' \<approx> t \<and> c1' \<approx>01T d1 \<or> (\<exists>d' t'. (d1, t) \<rightarrow>c (d', t') \<and> s' \<approx> t' \<and> c1' \<approx>01T d')
[PROOF STEP]
unfolding matchC_ZOC_def
[PROOF STATE]
proof (prove)
using this:
(c1, s) \<rightarrow>c (c1', s')
c' = c1' ;; while tst do c
s \<approx> t
\<forall>s t c' s'. s \<approx> t \<and> (c1, s) \<rightarrow>c (c', s') \<longrightarrow> s' \<approx> t \<and> c' \<approx>01T d1 \<or> (\<exists>d' t'. (d1, t) \<rightarrow>c (d', t') \<and> s' \<approx> t' \<and> c' \<approx>01T d')

goal (1 subgoal):
 1. s' \<approx> t \<and> c1' \<approx>01T d1 \<or> (\<exists>d' t'. (d1, t) \<rightarrow>c (d', t') \<and> s' \<approx> t' \<and> c1' \<approx>01T d')
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
s' \<approx> t \<and> c1' \<approx>01T d1 \<or> (\<exists>d' t'. (d1, t) \<rightarrow>c (d', t') \<and> s' \<approx> t' \<and> c1' \<approx>01T d')

goal (2 subgoals):
 1. \<And>c1'. \<lbrakk>(c1, s) \<rightarrow>c (c1', s'); c' = c1' ;; while tst do c\<rbrakk> \<Longrightarrow> s' \<approx> t \<and> (c', d1 ;; while tst do d) \<in> thetaWhileZOT \<union> ZObisT \<or> (\<exists>d' t'. (d1 ;; while tst do d, t) \<rightarrow>c (d', t') \<and> s' \<approx> t' \<and> (c', d') \<in> thetaWhileZOT \<union> ZObisT)
 2. \<lbrakk>(c1, s) \<rightarrow>t s'; c' = while tst do c\<rbrakk> \<Longrightarrow> s' \<approx> t \<and> (c', d1 ;; while tst do d) \<in> thetaWhileZOT \<union> ZObisT \<or> (\<exists>d' t'. (d1 ;; while tst do d, t) \<rightarrow>c (d', t') \<and> s' \<approx> t' \<and> (c', d') \<in> thetaWhileZOT \<union> ZObisT)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
s' \<approx> t \<and> c1' \<approx>01T d1 \<or> (\<exists>d' t'. (d1, t) \<rightarrow>c (d', t') \<and> s' \<approx> t' \<and> c1' \<approx>01T d')

goal (1 subgoal):
 1. s' \<approx> t \<and> (c', d1 ;; while tst do d) \<in> thetaWhileZOT \<union> ZObisT \<or> (\<exists>d' t'. (d1 ;; while tst do d, t) \<rightarrow>c (d', t') \<and> s' \<approx> t' \<and> (c', d') \<in> thetaWhileZOT \<union> ZObisT)
[PROOF STEP]
unfolding c' thetaWhileZOT_def
[PROOF STATE]
proof (prove)
using this:
s' \<approx> t \<and> c1' \<approx>01T d1 \<or> (\<exists>d' t'. (d1, t) \<rightarrow>c (d', t') \<and> s' \<approx> t' \<and> c1' \<approx>01T d')

goal (1 subgoal):
 1. s' \<approx> t \<and> (c1' ;; while tst do c, d1 ;; while tst do d) \<in> {(while tst do c, while tst do d) |tst c d. compatTst tst \<and> c \<approx>01T d} \<union> {(c1 ;; while tst do c, d1 ;; while tst do d) |tst c1 d1 c d. compatTst tst \<and> c1 \<approx>01T d1 \<and> c \<approx>01T d} \<union> ZObisT \<or> (\<exists>d' t'. (d1 ;; while tst do d, t) \<rightarrow>c (d', t') \<and> s' \<approx> t' \<and> (c1' ;; while tst do c, d') \<in> {(while tst do c, while tst do d) |tst c d. compatTst tst \<and> c \<approx>01T d} \<union> {(c1 ;; while tst do c, d1 ;; while tst do d) |tst c1 d1 c d. compatTst tst \<and> c1 \<approx>01T d1 \<and> c \<approx>01T d} \<union> ZObisT)
[PROOF STEP]
apply -
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s' \<approx> t \<and> c1' \<approx>01T d1 \<or> (\<exists>d' t'. (d1, t) \<rightarrow>c (d', t') \<and> s' \<approx> t' \<and> c1' \<approx>01T d') \<Longrightarrow> s' \<approx> t \<and> (c1' ;; while tst do c, d1 ;; while tst do d) \<in> {(while tst do c, while tst do d) |tst c d. compatTst tst \<and> c \<approx>01T d} \<union> {(c1 ;; while tst do c, d1 ;; while tst do d) |tst c1 d1 c d. compatTst tst \<and> c1 \<approx>01T d1 \<and> c \<approx>01T d} \<union> ZObisT \<or> (\<exists>d' t'. (d1 ;; while tst do d, t) \<rightarrow>c (d', t') \<and> s' \<approx> t' \<and> (c1' ;; while tst do c, d') \<in> {(while tst do c, while tst do d) |tst c d. compatTst tst \<and> c \<approx>01T d} \<union> {(c1 ;; while tst do c, d1 ;; while tst do d) |tst c1 d1 c d. compatTst tst \<and> c1 \<approx>01T d1 \<and> c \<approx>01T d} \<union> ZObisT)
[PROOF STEP]
apply(tactic \<open>mauto_no_simp_tac @{context}\<close>)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>s' \<approx> t; c1' \<approx>01T d1\<rbrakk> \<Longrightarrow> s' \<approx> t \<and> (c1' ;; while tst do c, d1 ;; while tst do d) \<in> {(while tst do c, while tst do d) |tst c d. compatTst tst \<and> c \<approx>01T d} \<union> {(c1 ;; while tst do c, d1 ;; while tst do d) |tst c1 d1 c d. compatTst tst \<and> c1 \<approx>01T d1 \<and> c \<approx>01T d} \<union> ZObisT \<or> (\<exists>d' t'. (d1 ;; while tst do d, t) \<rightarrow>c (d', t') \<and> s' \<approx> t' \<and> (c1' ;; while tst do c, d') \<in> {(while tst do c, while tst do d) |tst c d. compatTst tst \<and> c \<approx>01T d} \<union> {(c1 ;; while tst do c, d1 ;; while tst do d) |tst c1 d1 c d. compatTst tst \<and> c1 \<approx>01T d1 \<and> c \<approx>01T d} \<union> ZObisT)
 2. \<And>d' t'. \<lbrakk>(d1, t) \<rightarrow>c (d', t'); s' \<approx> t'; c1' \<approx>01T d'\<rbrakk> \<Longrightarrow> s' \<approx> t \<and> (c1' ;; while tst do c, d1 ;; while tst do d) \<in> {(while tst do c, while tst do d) |tst c d. compatTst tst \<and> c \<approx>01T d} \<union> {(c1 ;; while tst do c, d1 ;; while tst do d) |tst c1 d1 c d. compatTst tst \<and> c1 \<approx>01T d1 \<and> c \<approx>01T d} \<union> ZObisT \<or> (\<exists>d' t'. (d1 ;; while tst do d, t) \<rightarrow>c (d', t') \<and> s' \<approx> t' \<and> (c1' ;; while tst do c, d') \<in> {(while tst do c, while tst do d) |tst c d. compatTst tst \<and> c \<approx>01T d} \<union> {(c1 ;; while tst do c, d1 ;; while tst do d) |tst c1 d1 c d. compatTst tst \<and> c1 \<approx>01T d1 \<and> c \<approx>01T d} \<union> ZObisT)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>s' \<approx> t; c1' \<approx>01T d1\<rbrakk> \<Longrightarrow> compatTst tst \<and> c \<approx>01T d \<or> c1' ;; while tst do c \<approx>01T d1 ;; while tst do d \<or> (\<exists>d' t'. (d1 ;; while tst do d, t) \<rightarrow>c (d', t') \<and> s' \<approx> t' \<and> ((\<exists>d1 d. d' = d1 ;; while tst do d \<and> compatTst tst \<and> c1' \<approx>01T d1 \<and> c \<approx>01T d) \<or> c1' ;; while tst do c \<approx>01T d'))
 2. \<And>d' t'. \<lbrakk>(d1, t) \<rightarrow>c (d', t'); s' \<approx> t'; c1' \<approx>01T d'\<rbrakk> \<Longrightarrow> s' \<approx> t \<and> (c1' ;; while tst do c, d1 ;; while tst do d) \<in> {(while tst do c, while tst do d) |tst c d. compatTst tst \<and> c \<approx>01T d} \<union> {(c1 ;; while tst do c, d1 ;; while tst do d) |tst c1 d1 c d. compatTst tst \<and> c1 \<approx>01T d1 \<and> c \<approx>01T d} \<union> ZObisT \<or> (\<exists>d' t'. (d1 ;; while tst do d, t) \<rightarrow>c (d', t') \<and> s' \<approx> t' \<and> (c1' ;; while tst do c, d') \<in> {(while tst do c, while tst do d) |tst c d. compatTst tst \<and> c \<approx>01T d} \<union> {(c1 ;; while tst do c, d1 ;; while tst do d) |tst c1 d1 c d. compatTst tst \<and> c1 \<approx>01T d1 \<and> c \<approx>01T d} \<union> ZObisT)
[PROOF STEP]
apply (metis c_d tst)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>d' t'. \<lbrakk>(d1, t) \<rightarrow>c (d', t'); s' \<approx> t'; c1' \<approx>01T d'\<rbrakk> \<Longrightarrow> s' \<approx> t \<and> (c1' ;; while tst do c, d1 ;; while tst do d) \<in> {(while tst do c, while tst do d) |tst c d. compatTst tst \<and> c \<approx>01T d} \<union> {(c1 ;; while tst do c, d1 ;; while tst do d) |tst c1 d1 c d. compatTst tst \<and> c1 \<approx>01T d1 \<and> c \<approx>01T d} \<union> ZObisT \<or> (\<exists>d' t'. (d1 ;; while tst do d, t) \<rightarrow>c (d', t') \<and> s' \<approx> t' \<and> (c1' ;; while tst do c, d') \<in> {(while tst do c, while tst do d) |tst c d. compatTst tst \<and> c \<approx>01T d} \<union> {(c1 ;; while tst do c, d1 ;; while tst do d) |tst c1 d1 c d. compatTst tst \<and> c1 \<approx>01T d1 \<and> c \<approx>01T d} \<union> ZObisT)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>d' t'. \<lbrakk>(d1, t) \<rightarrow>c (d', t'); s' \<approx> t'; c1' \<approx>01T d'\<rbrakk> \<Longrightarrow> s' \<approx> t \<and> (compatTst tst \<and> c1' \<approx>01T d1 \<and> c \<approx>01T d \<or> c1' ;; while tst do c \<approx>01T d1 ;; while tst do d) \<or> (\<exists>d' t'. (d1 ;; while tst do d, t) \<rightarrow>c (d', t') \<and> s' \<approx> t' \<and> ((\<exists>d1 d. d' = d1 ;; while tst do d \<and> compatTst tst \<and> c1' \<approx>01T d1 \<and> c \<approx>01T d) \<or> c1' ;; while tst do c \<approx>01T d'))
[PROOF STEP]
by (metis SeqC c_d tst)
[PROOF STATE]
proof (state)
this:
s' \<approx> t \<and> (c', d1 ;; while tst do d) \<in> thetaWhileZOT \<union> ZObisT \<or> (\<exists>d' t'. (d1 ;; while tst do d, t) \<rightarrow>c (d', t') \<and> s' \<approx> t' \<and> (c', d') \<in> thetaWhileZOT \<union> ZObisT)

goal (1 subgoal):
 1. \<lbrakk>(c1, s) \<rightarrow>t s'; c' = while tst do c\<rbrakk> \<Longrightarrow> s' \<approx> t \<and> (c', d1 ;; while tst do d) \<in> thetaWhileZOT \<union> ZObisT \<or> (\<exists>d' t'. (d1 ;; while tst do d, t) \<rightarrow>c (d', t') \<and> s' \<approx> t' \<and> (c', d') \<in> thetaWhileZOT \<union> ZObisT)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>(c1, s) \<rightarrow>t s'; c' = while tst do c\<rbrakk> \<Longrightarrow> s' \<approx> t \<and> (c', d1 ;; while tst do d) \<in> thetaWhileZOT \<union> ZObisT \<or> (\<exists>d' t'. (d1 ;; while tst do d, t) \<rightarrow>c (d', t') \<and> s' \<approx> t' \<and> (c', d') \<in> thetaWhileZOT \<union> ZObisT)
[PROOF STEP]
assume "(c1, s) \<rightarrow>t s'" and c': "c' = While tst c"
[PROOF STATE]
proof (state)
this:
(c1, s) \<rightarrow>t s'
c' = while tst do c

goal (1 subgoal):
 1. \<lbrakk>(c1, s) \<rightarrow>t s'; c' = while tst do c\<rbrakk> \<Longrightarrow> s' \<approx> t \<and> (c', d1 ;; while tst do d) \<in> thetaWhileZOT \<union> ZObisT \<or> (\<exists>d' t'. (d1 ;; while tst do d, t) \<rightarrow>c (d', t') \<and> s' \<approx> t' \<and> (c', d') \<in> thetaWhileZOT \<union> ZObisT)
[PROOF STEP]
hence "\<exists>t'. (d1, t) \<rightarrow>t t' \<and> s' \<approx> t'"
[PROOF STATE]
proof (prove)
using this:
(c1, s) \<rightarrow>t s'
c' = while tst do c

goal (1 subgoal):
 1. \<exists>t'. (d1, t) \<rightarrow>t t' \<and> s' \<approx> t'
[PROOF STEP]
using st matchT_T1
[PROOF STATE]
proof (prove)
using this:
(c1, s) \<rightarrow>t s'
c' = while tst do c
s \<approx> t
matchT_T c1 d1

goal (1 subgoal):
 1. \<exists>t'. (d1, t) \<rightarrow>t t' \<and> s' \<approx> t'
[PROOF STEP]
unfolding matchT_T_def
[PROOF STATE]
proof (prove)
using this:
(c1, s) \<rightarrow>t s'
c' = while tst do c
s \<approx> t
\<forall>s t s'. s \<approx> t \<and> (c1, s) \<rightarrow>t s' \<longrightarrow> (\<exists>t'. (d1, t) \<rightarrow>t t' \<and> s' \<approx> t')

goal (1 subgoal):
 1. \<exists>t'. (d1, t) \<rightarrow>t t' \<and> s' \<approx> t'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>t'. (d1, t) \<rightarrow>t t' \<and> s' \<approx> t'

goal (1 subgoal):
 1. \<lbrakk>(c1, s) \<rightarrow>t s'; c' = while tst do c\<rbrakk> \<Longrightarrow> s' \<approx> t \<and> (c', d1 ;; while tst do d) \<in> thetaWhileZOT \<union> ZObisT \<or> (\<exists>d' t'. (d1 ;; while tst do d, t) \<rightarrow>c (d', t') \<and> s' \<approx> t' \<and> (c', d') \<in> thetaWhileZOT \<union> ZObisT)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<exists>t'. (d1, t) \<rightarrow>t t' \<and> s' \<approx> t'

goal (1 subgoal):
 1. s' \<approx> t \<and> (c', d1 ;; while tst do d) \<in> thetaWhileZOT \<union> ZObisT \<or> (\<exists>d' t'. (d1 ;; while tst do d, t) \<rightarrow>c (d', t') \<and> s' \<approx> t' \<and> (c', d') \<in> thetaWhileZOT \<union> ZObisT)
[PROOF STEP]
unfolding c' thetaWhileZOT_def
[PROOF STATE]
proof (prove)
using this:
\<exists>t'. (d1, t) \<rightarrow>t t' \<and> s' \<approx> t'

goal (1 subgoal):
 1. s' \<approx> t \<and> (while tst do c, d1 ;; while tst do d) \<in> {(while tst do c, while tst do d) |tst c d. compatTst tst \<and> c \<approx>01T d} \<union> {(c1 ;; while tst do c, d1 ;; while tst do d) |tst c1 d1 c d. compatTst tst \<and> c1 \<approx>01T d1 \<and> c \<approx>01T d} \<union> ZObisT \<or> (\<exists>d' t'. (d1 ;; while tst do d, t) \<rightarrow>c (d', t') \<and> s' \<approx> t' \<and> (while tst do c, d') \<in> {(while tst do c, while tst do d) |tst c d. compatTst tst \<and> c \<approx>01T d} \<union> {(c1 ;; while tst do c, d1 ;; while tst do d) |tst c1 d1 c d. compatTst tst \<and> c1 \<approx>01T d1 \<and> c \<approx>01T d} \<union> ZObisT)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>t'. (d1, t) \<rightarrow>t t' \<and> s' \<approx> t' \<Longrightarrow> s' \<approx> t \<and> while tst do c \<approx>01T d1 ;; while tst do d \<or> (\<exists>d' t'. (d1 ;; while tst do d, t) \<rightarrow>c (d', t') \<and> s' \<approx> t' \<and> ((\<exists>d. d' = while tst do d \<and> compatTst tst \<and> c \<approx>01T d) \<or> while tst do c \<approx>01T d'))
[PROOF STEP]
by (metis PL.SeqT c_d tst)
[PROOF STATE]
proof (state)
this:
s' \<approx> t \<and> (c', d1 ;; while tst do d) \<in> thetaWhileZOT \<union> ZObisT \<or> (\<exists>d' t'. (d1 ;; while tst do d, t) \<rightarrow>c (d', t') \<and> s' \<approx> t' \<and> (c', d') \<in> thetaWhileZOT \<union> ZObisT)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
s' \<approx> t \<and> (c', d1 ;; while tst do d) \<in> thetaWhileZOT \<union> ZObisT \<or> (\<exists>d' t'. (d1 ;; while tst do d, t) \<rightarrow>c (d', t') \<and> s' \<approx> t' \<and> (c', d') \<in> thetaWhileZOT \<union> ZObisT)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
matchC_ZOC (thetaWhileZOT \<union> ZObisT) (c1 ;; while tst do c) (d1 ;; while tst do d)

goal (1 subgoal):
 1. matchT_T (c1 ;; while tst do c) (d1 ;; while tst do d)
[PROOF STEP]
qed (unfold matchT_T_def, auto)
[PROOF STATE]
proof (state)
this:
(c1 ;; while tst do c, d1 ;; while tst do d) \<in> ZOretrT (thetaWhileZOT \<union> ZObisT)

goal (1 subgoal):
 1. thetaWhileZOT \<subseteq> ZOretrT (thetaWhileZOT \<union> ZObisT)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>compatTst ?tst3; ?c1.3 \<approx>01T ?d1.3; ?c3 \<approx>01T ?d3\<rbrakk> \<Longrightarrow> (?c1.3 ;; while ?tst3 do ?c3, ?d1.3 ;; while ?tst3 do ?d3) \<in> ZOretrT (thetaWhileZOT \<union> ZObisT)

goal (1 subgoal):
 1. thetaWhileZOT \<subseteq> ZOretrT (thetaWhileZOT \<union> ZObisT)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>compatTst ?tst3; ?c3 \<approx>01T ?d3\<rbrakk> \<Longrightarrow> (while ?tst3 do ?c3, while ?tst3 do ?d3) \<in> ZOretrT (thetaWhileZOT \<union> ZObisT)
\<lbrakk>compatTst ?tst3; ?c1.3 \<approx>01T ?d1.3; ?c3 \<approx>01T ?d3\<rbrakk> \<Longrightarrow> (?c1.3 ;; while ?tst3 do ?c3, ?d1.3 ;; while ?tst3 do ?d3) \<in> ZOretrT (thetaWhileZOT \<union> ZObisT)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>compatTst ?tst3; ?c3 \<approx>01T ?d3\<rbrakk> \<Longrightarrow> (while ?tst3 do ?c3, while ?tst3 do ?d3) \<in> ZOretrT (thetaWhileZOT \<union> ZObisT)
\<lbrakk>compatTst ?tst3; ?c1.3 \<approx>01T ?d1.3; ?c3 \<approx>01T ?d3\<rbrakk> \<Longrightarrow> (?c1.3 ;; while ?tst3 do ?c3, ?d1.3 ;; while ?tst3 do ?d3) \<in> ZOretrT (thetaWhileZOT \<union> ZObisT)

goal (1 subgoal):
 1. thetaWhileZOT \<subseteq> ZOretrT (thetaWhileZOT \<union> ZObisT)
[PROOF STEP]
unfolding thetaWhileZOT_def
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>compatTst ?tst3; ?c3 \<approx>01T ?d3\<rbrakk> \<Longrightarrow> (while ?tst3 do ?c3, while ?tst3 do ?d3) \<in> ZOretrT ({(while tst do c, while tst do d) |tst c d. compatTst tst \<and> c \<approx>01T d} \<union> {(c1 ;; while tst do c, d1 ;; while tst do d) |tst c1 d1 c d. compatTst tst \<and> c1 \<approx>01T d1 \<and> c \<approx>01T d} \<union> ZObisT)
\<lbrakk>compatTst ?tst3; ?c1.3 \<approx>01T ?d1.3; ?c3 \<approx>01T ?d3\<rbrakk> \<Longrightarrow> (?c1.3 ;; while ?tst3 do ?c3, ?d1.3 ;; while ?tst3 do ?d3) \<in> ZOretrT ({(while tst do c, while tst do d) |tst c d. compatTst tst \<and> c \<approx>01T d} \<union> {(c1 ;; while tst do c, d1 ;; while tst do d) |tst c1 d1 c d. compatTst tst \<and> c1 \<approx>01T d1 \<and> c \<approx>01T d} \<union> ZObisT)

goal (1 subgoal):
 1. {(while tst do c, while tst do d) |tst c d. compatTst tst \<and> c \<approx>01T d} \<union> {(c1 ;; while tst do c, d1 ;; while tst do d) |tst c1 d1 c d. compatTst tst \<and> c1 \<approx>01T d1 \<and> c \<approx>01T d} \<subseteq> ZOretrT ({(while tst do c, while tst do d) |tst c d. compatTst tst \<and> c \<approx>01T d} \<union> {(c1 ;; while tst do c, d1 ;; while tst do d) |tst c1 d1 c d. compatTst tst \<and> c1 \<approx>01T d1 \<and> c \<approx>01T d} \<union> ZObisT)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
thetaWhileZOT \<subseteq> ZOretrT (thetaWhileZOT \<union> ZObisT)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma pbernpoly_over_power_tendsto_0:
  assumes "n > 0"
  shows   "(\<lambda>x. of_real (pbernpoly (Suc n) (real x)) / (of_nat (Suc n) * (s + of_nat x) ^ n)) \<longlonglongrightarrow> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. complex_of_real (pbernpoly (Suc n) (real x)) / (of_nat (Suc n) * (s + of_nat x) ^ n)) \<longlonglongrightarrow> 0
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<lambda>x. complex_of_real (pbernpoly (Suc n) (real x)) / (of_nat (Suc n) * (s + of_nat x) ^ n)) \<longlonglongrightarrow> 0
[PROOF STEP]
from s
[PROOF STATE]
proof (chain)
picking this:
s \<notin> \<real>\<^sub>\<le>\<^sub>0
[PROOF STEP]
have neq: "s + of_nat n \<noteq> 0" for n
[PROOF STATE]
proof (prove)
using this:
s \<notin> \<real>\<^sub>\<le>\<^sub>0

goal (1 subgoal):
 1. s + of_nat n \<noteq> 0
[PROOF STEP]
by (auto simp: complex_eq_iff complex_nonpos_Reals_iff)
[PROOF STATE]
proof (state)
this:
s + of_nat ?n \<noteq> 0

goal (1 subgoal):
 1. (\<lambda>x. complex_of_real (pbernpoly (Suc n) (real x)) / (of_nat (Suc n) * (s + of_nat x) ^ n)) \<longlonglongrightarrow> 0
[PROOF STEP]
obtain c where c: "\<And>x. norm (pbernpoly (Suc n) x) \<le> c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>c. (\<And>x. norm (pbernpoly (Suc n) x) \<le> c) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using bounded_pbernpoly
[PROOF STATE]
proof (prove)
using this:
(\<And>c. (\<And>x. norm (pbernpoly ?n x) \<le> c) \<Longrightarrow> ?thesis) \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. (\<And>c. (\<And>x. norm (pbernpoly (Suc n) x) \<le> c) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
norm (pbernpoly (Suc n) ?x) \<le> c

goal (1 subgoal):
 1. (\<lambda>x. complex_of_real (pbernpoly (Suc n) (real x)) / (of_nat (Suc n) * (s + of_nat x) ^ n)) \<longlonglongrightarrow> 0
[PROOF STEP]
have "eventually (\<lambda>x. real x + Re s > 0) at_top"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>\<^sub>F x in sequentially. 0 < real x + Re s
[PROOF STEP]
by real_asymp
[PROOF STATE]
proof (state)
this:
\<forall>\<^sub>F x in sequentially. 0 < real x + Re s

goal (1 subgoal):
 1. (\<lambda>x. complex_of_real (pbernpoly (Suc n) (real x)) / (of_nat (Suc n) * (s + of_nat x) ^ n)) \<longlonglongrightarrow> 0
[PROOF STEP]
hence "eventually (\<lambda>x. norm (of_real (pbernpoly (Suc n) (real x)) /
                                    (of_nat (Suc n) * (s + of_nat x) ^ n)) \<le>
                          (c / real (Suc n)) / (real x + Re s) ^ n) at_top"
[PROOF STATE]
proof (prove)
using this:
\<forall>\<^sub>F x in sequentially. 0 < real x + Re s

goal (1 subgoal):
 1. \<forall>\<^sub>F x in sequentially. cmod (complex_of_real (pbernpoly (Suc n) (real x)) / (of_nat (Suc n) * (s + of_nat x) ^ n)) \<le> c / real (Suc n) / (real x + Re s) ^ n
[PROOF STEP]
using eventually_gt_at_top[of "0::nat"]
[PROOF STATE]
proof (prove)
using this:
\<forall>\<^sub>F x in sequentially. 0 < real x + Re s
eventually ((<) 0) sequentially

goal (1 subgoal):
 1. \<forall>\<^sub>F x in sequentially. cmod (complex_of_real (pbernpoly (Suc n) (real x)) / (of_nat (Suc n) * (s + of_nat x) ^ n)) \<le> c / real (Suc n) / (real x + Re s) ^ n
[PROOF STEP]
proof eventually_elim
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>0 < real x + Re s; 0 < x\<rbrakk> \<Longrightarrow> cmod (complex_of_real (pbernpoly (Suc n) (real x)) / (of_nat (Suc n) * (s + of_nat x) ^ n)) \<le> c / real (Suc n) / (real x + Re s) ^ n
[PROOF STEP]
case (elim x)
[PROOF STATE]
proof (state)
this:
0 < real x + Re s
0 < x

goal (1 subgoal):
 1. \<And>x. \<lbrakk>0 < real x + Re s; 0 < x\<rbrakk> \<Longrightarrow> cmod (complex_of_real (pbernpoly (Suc n) (real x)) / (of_nat (Suc n) * (s + of_nat x) ^ n)) \<le> c / real (Suc n) / (real x + Re s) ^ n
[PROOF STEP]
have "norm (of_real (pbernpoly (Suc n) (real x)) /
                                    (of_nat (Suc n) * (s + of_nat x) ^ n)) \<le>
            (c / real (Suc n)) / norm (s + of_nat x) ^ n" (is "_ \<le> ?rhs")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cmod (complex_of_real (pbernpoly (Suc n) (real x)) / (of_nat (Suc n) * (s + of_nat x) ^ n)) \<le> c / real (Suc n) / cmod (s + of_nat x) ^ n
[PROOF STEP]
using c[of x]
[PROOF STATE]
proof (prove)
using this:
norm (pbernpoly (Suc n) (real x)) \<le> c

goal (1 subgoal):
 1. cmod (complex_of_real (pbernpoly (Suc n) (real x)) / (of_nat (Suc n) * (s + of_nat x) ^ n)) \<le> c / real (Suc n) / cmod (s + of_nat x) ^ n
[PROOF STEP]
by (auto simp: norm_divide norm_mult norm_power neq field_simps simp del: of_nat_Suc)
[PROOF STATE]
proof (state)
this:
cmod (complex_of_real (pbernpoly (Suc n) (real x)) / (of_nat (Suc n) * (s + of_nat x) ^ n)) \<le> c / real (Suc n) / cmod (s + of_nat x) ^ n

goal (1 subgoal):
 1. \<And>x. \<lbrakk>0 < real x + Re s; 0 < x\<rbrakk> \<Longrightarrow> cmod (complex_of_real (pbernpoly (Suc n) (real x)) / (of_nat (Suc n) * (s + of_nat x) ^ n)) \<le> c / real (Suc n) / (real x + Re s) ^ n
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
cmod (complex_of_real (pbernpoly (Suc n) (real x)) / (of_nat (Suc n) * (s + of_nat x) ^ n)) \<le> c / real (Suc n) / cmod (s + of_nat x) ^ n

goal (1 subgoal):
 1. \<And>x. \<lbrakk>0 < real x + Re s; 0 < x\<rbrakk> \<Longrightarrow> cmod (complex_of_real (pbernpoly (Suc n) (real x)) / (of_nat (Suc n) * (s + of_nat x) ^ n)) \<le> c / real (Suc n) / (real x + Re s) ^ n
[PROOF STEP]
have "(real x + Re s) \<le> cmod (s + of_nat x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real x + Re s \<le> cmod (s + of_nat x)
[PROOF STEP]
using complex_Re_le_cmod[of "s + of_nat x"] s
[PROOF STATE]
proof (prove)
using this:
Re (s + of_nat x) \<le> cmod (s + of_nat x)
s \<notin> \<real>\<^sub>\<le>\<^sub>0

goal (1 subgoal):
 1. real x + Re s \<le> cmod (s + of_nat x)
[PROOF STEP]
by (auto simp add: complex_nonpos_Reals_iff)
[PROOF STATE]
proof (state)
this:
real x + Re s \<le> cmod (s + of_nat x)

goal (1 subgoal):
 1. \<And>x. \<lbrakk>0 < real x + Re s; 0 < x\<rbrakk> \<Longrightarrow> cmod (complex_of_real (pbernpoly (Suc n) (real x)) / (of_nat (Suc n) * (s + of_nat x) ^ n)) \<le> c / real (Suc n) / (real x + Re s) ^ n
[PROOF STEP]
hence "?rhs \<le> (c / real (Suc n)) / (real x + Re s) ^ n"
[PROOF STATE]
proof (prove)
using this:
real x + Re s \<le> cmod (s + of_nat x)

goal (1 subgoal):
 1. c / real (Suc n) / cmod (s + of_nat x) ^ n \<le> c / real (Suc n) / (real x + Re s) ^ n
[PROOF STEP]
using s elim c[of 0] neq[of x]
[PROOF STATE]
proof (prove)
using this:
real x + Re s \<le> cmod (s + of_nat x)
s \<notin> \<real>\<^sub>\<le>\<^sub>0
0 < real x + Re s
0 < x
norm (pbernpoly (Suc n) 0) \<le> c
s + of_nat x \<noteq> 0

goal (1 subgoal):
 1. c / real (Suc n) / cmod (s + of_nat x) ^ n \<le> c / real (Suc n) / (real x + Re s) ^ n
[PROOF STEP]
by (intro divide_left_mono power_mono mult_pos_pos divide_nonneg_pos zero_less_power) auto
[PROOF STATE]
proof (state)
this:
c / real (Suc n) / cmod (s + of_nat x) ^ n \<le> c / real (Suc n) / (real x + Re s) ^ n

goal (1 subgoal):
 1. \<And>x. \<lbrakk>0 < real x + Re s; 0 < x\<rbrakk> \<Longrightarrow> cmod (complex_of_real (pbernpoly (Suc n) (real x)) / (of_nat (Suc n) * (s + of_nat x) ^ n)) \<le> c / real (Suc n) / (real x + Re s) ^ n
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
cmod (complex_of_real (pbernpoly (Suc n) (real x)) / (of_nat (Suc n) * (s + of_nat x) ^ n)) \<le> c / real (Suc n) / (real x + Re s) ^ n
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
cmod (complex_of_real (pbernpoly (Suc n) (real x)) / (of_nat (Suc n) * (s + of_nat x) ^ n)) \<le> c / real (Suc n) / (real x + Re s) ^ n

goal (1 subgoal):
 1. cmod (complex_of_real (pbernpoly (Suc n) (real x)) / (of_nat (Suc n) * (s + of_nat x) ^ n)) \<le> c / real (Suc n) / (real x + Re s) ^ n
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
cmod (complex_of_real (pbernpoly (Suc n) (real x)) / (of_nat (Suc n) * (s + of_nat x) ^ n)) \<le> c / real (Suc n) / (real x + Re s) ^ n

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>\<^sub>F x in sequentially. cmod (complex_of_real (pbernpoly (Suc n) (real x)) / (of_nat (Suc n) * (s + of_nat x) ^ n)) \<le> c / real (Suc n) / (real x + Re s) ^ n

goal (1 subgoal):
 1. (\<lambda>x. complex_of_real (pbernpoly (Suc n) (real x)) / (of_nat (Suc n) * (s + of_nat x) ^ n)) \<longlonglongrightarrow> 0
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<forall>\<^sub>F x in sequentially. cmod (complex_of_real (pbernpoly (Suc n) (real x)) / (of_nat (Suc n) * (s + of_nat x) ^ n)) \<le> c / real (Suc n) / (real x + Re s) ^ n

goal (1 subgoal):
 1. (\<lambda>x. complex_of_real (pbernpoly (Suc n) (real x)) / (of_nat (Suc n) * (s + of_nat x) ^ n)) \<longlonglongrightarrow> 0
[PROOF STEP]
have "(\<lambda>x. (c / real (Suc n)) / (real x + Re s) ^ n) \<longlonglongrightarrow> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. c / real (Suc n) / (real x + Re s) ^ n) \<longlonglongrightarrow> 0
[PROOF STEP]
using \<open>n > 0\<close>
[PROOF STATE]
proof (prove)
using this:
0 < n

goal (1 subgoal):
 1. (\<lambda>x. c / real (Suc n) / (real x + Re s) ^ n) \<longlonglongrightarrow> 0
[PROOF STEP]
by real_asymp
[PROOF STATE]
proof (state)
this:
(\<lambda>x. c / real (Suc n) / (real x + Re s) ^ n) \<longlonglongrightarrow> 0

goal (1 subgoal):
 1. (\<lambda>x. complex_of_real (pbernpoly (Suc n) (real x)) / (of_nat (Suc n) * (s + of_nat x) ^ n)) \<longlonglongrightarrow> 0
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<forall>\<^sub>F x in sequentially. cmod (complex_of_real (pbernpoly (Suc n) (real x)) / (of_nat (Suc n) * (s + of_nat x) ^ n)) \<le> c / real (Suc n) / (real x + Re s) ^ n
(\<lambda>x. c / real (Suc n) / (real x + Re s) ^ n) \<longlonglongrightarrow> 0
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>\<^sub>F x in sequentially. cmod (complex_of_real (pbernpoly (Suc n) (real x)) / (of_nat (Suc n) * (s + of_nat x) ^ n)) \<le> c / real (Suc n) / (real x + Re s) ^ n
(\<lambda>x. c / real (Suc n) / (real x + Re s) ^ n) \<longlonglongrightarrow> 0

goal (1 subgoal):
 1. (\<lambda>x. complex_of_real (pbernpoly (Suc n) (real x)) / (of_nat (Suc n) * (s + of_nat x) ^ n)) \<longlonglongrightarrow> 0
[PROOF STEP]
by (rule Lim_null_comparison)
[PROOF STATE]
proof (state)
this:
(\<lambda>x. complex_of_real (pbernpoly (Suc n) (real x)) / (of_nat (Suc n) * (s + of_nat x) ^ n)) \<longlonglongrightarrow> 0

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma stirling_integral_bound':
  assumes "n > 0" and "\<alpha> \<in> {0<..<pi}"
  obtains c where
    "\<And>s::complex. s \<in> complex_cone' \<alpha> - {0} \<Longrightarrow> norm (stirling_integral n s) \<le> c / norm s ^ n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>c. (\<And>s. s \<in> complex_cone' \<alpha> - {0} \<Longrightarrow> cmod (stirling_integral n s) \<le> c / cmod s ^ n) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>c. (\<And>s. s \<in> complex_cone' \<alpha> - {0} \<Longrightarrow> cmod (stirling_integral n s) \<le> c / cmod s ^ n) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
let ?f = "\<lambda>s. of_nat n / of_nat (Suc n) * stirling_integral (Suc n) s -
                  of_real (bernoulli (Suc n)) / (of_nat (Suc n) * s ^ n)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>c. (\<And>s. s \<in> complex_cone' \<alpha> - {0} \<Longrightarrow> cmod (stirling_integral n s) \<le> c / cmod s ^ n) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from stirling_integral_bound_aux'[of "Suc n"] assms
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>1 < Suc n; ?\<alpha> \<in> {0<..<pi}; \<And>c. (\<And>s. s \<in> complex_cone' ?\<alpha> - {0} \<Longrightarrow> cmod (stirling_integral (Suc n) s) \<le> c / cmod s ^ (Suc n - 1)) \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis
0 < n
\<alpha> \<in> {0<..<pi}
[PROOF STEP]
obtain c where
    c: "\<And>s::complex. s \<in> complex_cone' \<alpha> - {0} \<Longrightarrow>
            norm (stirling_integral (Suc n) s) \<le> c / norm s ^ n"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>1 < Suc n; ?\<alpha> \<in> {0<..<pi}; \<And>c. (\<And>s. s \<in> complex_cone' ?\<alpha> - {0} \<Longrightarrow> cmod (stirling_integral (Suc n) s) \<le> c / cmod s ^ (Suc n - 1)) \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis
0 < n
\<alpha> \<in> {0<..<pi}

goal (1 subgoal):
 1. (\<And>c. (\<And>s. s \<in> complex_cone' \<alpha> - {0} \<Longrightarrow> cmod (stirling_integral (Suc n) s) \<le> c / cmod s ^ n) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
?s1 \<in> complex_cone' \<alpha> - {0} \<Longrightarrow> cmod (stirling_integral (Suc n) ?s1) \<le> c / cmod ?s1 ^ n

goal (1 subgoal):
 1. (\<And>c. (\<And>s. s \<in> complex_cone' \<alpha> - {0} \<Longrightarrow> cmod (stirling_integral n s) \<le> c / cmod s ^ n) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
define c1 where "c1 = real n / real (Suc n) * c"
[PROOF STATE]
proof (state)
this:
c1 = real n / real (Suc n) * c

goal (1 subgoal):
 1. (\<And>c. (\<And>s. s \<in> complex_cone' \<alpha> - {0} \<Longrightarrow> cmod (stirling_integral n s) \<le> c / cmod s ^ n) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
define c2 where "c2 = \<bar>bernoulli (Suc n)\<bar> / real (Suc n)"
[PROOF STATE]
proof (state)
this:
c2 = \<bar>bernoulli (Suc n)\<bar> / real (Suc n)

goal (1 subgoal):
 1. (\<And>c. (\<And>s. s \<in> complex_cone' \<alpha> - {0} \<Longrightarrow> cmod (stirling_integral n s) \<le> c / cmod s ^ n) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have c2_nonneg: "c2 \<ge> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> c2
[PROOF STEP]
by (simp add: c2_def)
[PROOF STATE]
proof (state)
this:
0 \<le> c2

goal (1 subgoal):
 1. (\<And>c. (\<And>s. s \<in> complex_cone' \<alpha> - {0} \<Longrightarrow> cmod (stirling_integral n s) \<le> c / cmod s ^ n) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. thesis
[PROOF STEP]
proof (rule that)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>s. s \<in> complex_cone' \<alpha> - {0} \<Longrightarrow> cmod (stirling_integral n s) \<le> ?c / cmod s ^ n
[PROOF STEP]
fix s :: complex
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>s. s \<in> complex_cone' \<alpha> - {0} \<Longrightarrow> cmod (stirling_integral n s) \<le> ?c / cmod s ^ n
[PROOF STEP]
assume s: "s \<in> complex_cone' \<alpha> - {0}"
[PROOF STATE]
proof (state)
this:
s \<in> complex_cone' \<alpha> - {0}

goal (1 subgoal):
 1. \<And>s. s \<in> complex_cone' \<alpha> - {0} \<Longrightarrow> cmod (stirling_integral n s) \<le> ?c / cmod s ^ n
[PROOF STEP]
have s': "s \<notin> \<real>\<^sub>\<le>\<^sub>0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s \<notin> \<real>\<^sub>\<le>\<^sub>0
[PROOF STEP]
using complex_cone_inter_nonpos_Reals[of "-\<alpha>" \<alpha>] assms s
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>- pi < - \<alpha>; - \<alpha> \<le> \<alpha>; \<alpha> < pi\<rbrakk> \<Longrightarrow> complex_cone' \<alpha> \<inter> \<real>\<^sub>\<le>\<^sub>0 = {0}
0 < n
\<alpha> \<in> {0<..<pi}
s \<in> complex_cone' \<alpha> - {0}

goal (1 subgoal):
 1. s \<notin> \<real>\<^sub>\<le>\<^sub>0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
s \<notin> \<real>\<^sub>\<le>\<^sub>0

goal (1 subgoal):
 1. \<And>s. s \<in> complex_cone' \<alpha> - {0} \<Longrightarrow> cmod (stirling_integral n s) \<le> ?c / cmod s ^ n
[PROOF STEP]
have "stirling_integral n s = ?f s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. stirling_integral n s = of_nat n / of_nat (Suc n) * stirling_integral (Suc n) s - complex_of_real (bernoulli (Suc n)) / (of_nat (Suc n) * s ^ n)
[PROOF STEP]
using s' assms
[PROOF STATE]
proof (prove)
using this:
s \<notin> \<real>\<^sub>\<le>\<^sub>0
0 < n
\<alpha> \<in> {0<..<pi}

goal (1 subgoal):
 1. stirling_integral n s = of_nat n / of_nat (Suc n) * stirling_integral (Suc n) s - complex_of_real (bernoulli (Suc n)) / (of_nat (Suc n) * s ^ n)
[PROOF STEP]
by (intro stirling_integral_conv_stirling_integral_Suc) auto
[PROOF STATE]
proof (state)
this:
stirling_integral n s = of_nat n / of_nat (Suc n) * stirling_integral (Suc n) s - complex_of_real (bernoulli (Suc n)) / (of_nat (Suc n) * s ^ n)

goal (1 subgoal):
 1. \<And>s. s \<in> complex_cone' \<alpha> - {0} \<Longrightarrow> cmod (stirling_integral n s) \<le> ?c / cmod s ^ n
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
stirling_integral n s = of_nat n / of_nat (Suc n) * stirling_integral (Suc n) s - complex_of_real (bernoulli (Suc n)) / (of_nat (Suc n) * s ^ n)

goal (1 subgoal):
 1. \<And>s. s \<in> complex_cone' \<alpha> - {0} \<Longrightarrow> cmod (stirling_integral n s) \<le> ?c / cmod s ^ n
[PROOF STEP]
have "norm \<dots> \<le> norm (of_nat n / of_nat (Suc n) * stirling_integral (Suc n) s) +
                           norm (of_real (bernoulli (Suc n)) / (of_nat (Suc n) * s ^ n))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cmod (of_nat n / of_nat (Suc n) * stirling_integral (Suc n) s - complex_of_real (bernoulli (Suc n)) / (of_nat (Suc n) * s ^ n)) \<le> cmod (of_nat n / of_nat (Suc n) * stirling_integral (Suc n) s) + cmod (complex_of_real (bernoulli (Suc n)) / (of_nat (Suc n) * s ^ n))
[PROOF STEP]
by (rule norm_triangle_ineq4)
[PROOF STATE]
proof (state)
this:
cmod (of_nat n / of_nat (Suc n) * stirling_integral (Suc n) s - complex_of_real (bernoulli (Suc n)) / (of_nat (Suc n) * s ^ n)) \<le> cmod (of_nat n / of_nat (Suc n) * stirling_integral (Suc n) s) + cmod (complex_of_real (bernoulli (Suc n)) / (of_nat (Suc n) * s ^ n))

goal (1 subgoal):
 1. \<And>s. s \<in> complex_cone' \<alpha> - {0} \<Longrightarrow> cmod (stirling_integral n s) \<le> ?c / cmod s ^ n
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
cmod (of_nat n / of_nat (Suc n) * stirling_integral (Suc n) s - complex_of_real (bernoulli (Suc n)) / (of_nat (Suc n) * s ^ n)) \<le> cmod (of_nat n / of_nat (Suc n) * stirling_integral (Suc n) s) + cmod (complex_of_real (bernoulli (Suc n)) / (of_nat (Suc n) * s ^ n))

goal (1 subgoal):
 1. \<And>s. s \<in> complex_cone' \<alpha> - {0} \<Longrightarrow> cmod (stirling_integral n s) \<le> ?c / cmod s ^ n
[PROOF STEP]
have "\<dots> = real n / real (Suc n) * norm (stirling_integral (Suc n) s) +
                      c2 / norm s ^ n" (is "_ = ?A + ?B")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cmod (of_nat n / of_nat (Suc n) * stirling_integral (Suc n) s) + cmod (complex_of_real (bernoulli (Suc n)) / (of_nat (Suc n) * s ^ n)) = real n / real (Suc n) * cmod (stirling_integral (Suc n) s) + c2 / cmod s ^ n
[PROOF STEP]
by (simp add: norm_divide norm_mult norm_power c2_def field_simps del: of_nat_Suc)
[PROOF STATE]
proof (state)
this:
cmod (of_nat n / of_nat (Suc n) * stirling_integral (Suc n) s) + cmod (complex_of_real (bernoulli (Suc n)) / (of_nat (Suc n) * s ^ n)) = real n / real (Suc n) * cmod (stirling_integral (Suc n) s) + c2 / cmod s ^ n

goal (1 subgoal):
 1. \<And>s. s \<in> complex_cone' \<alpha> - {0} \<Longrightarrow> cmod (stirling_integral n s) \<le> ?c / cmod s ^ n
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
cmod (of_nat n / of_nat (Suc n) * stirling_integral (Suc n) s) + cmod (complex_of_real (bernoulli (Suc n)) / (of_nat (Suc n) * s ^ n)) = real n / real (Suc n) * cmod (stirling_integral (Suc n) s) + c2 / cmod s ^ n

goal (1 subgoal):
 1. \<And>s. s \<in> complex_cone' \<alpha> - {0} \<Longrightarrow> cmod (stirling_integral n s) \<le> ?c / cmod s ^ n
[PROOF STEP]
have "?A \<le> real n / real (Suc n) * (c / norm s ^ n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real n / real (Suc n) * cmod (stirling_integral (Suc n) s) \<le> real n / real (Suc n) * (c / cmod s ^ n)
[PROOF STEP]
by (intro mult_left_mono c s) simp_all
[PROOF STATE]
proof (state)
this:
real n / real (Suc n) * cmod (stirling_integral (Suc n) s) \<le> real n / real (Suc n) * (c / cmod s ^ n)

goal (1 subgoal):
 1. \<And>s. s \<in> complex_cone' \<alpha> - {0} \<Longrightarrow> cmod (stirling_integral n s) \<le> ?c / cmod s ^ n
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
real n / real (Suc n) * cmod (stirling_integral (Suc n) s) \<le> real n / real (Suc n) * (c / cmod s ^ n)

goal (1 subgoal):
 1. \<And>s. s \<in> complex_cone' \<alpha> - {0} \<Longrightarrow> cmod (stirling_integral n s) \<le> ?c / cmod s ^ n
[PROOF STEP]
have "\<dots> = c1 / norm s ^ n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real n / real (Suc n) * (c / cmod s ^ n) = c1 / cmod s ^ n
[PROOF STEP]
by (simp add: c1_def)
[PROOF STATE]
proof (state)
this:
real n / real (Suc n) * (c / cmod s ^ n) = c1 / cmod s ^ n

goal (1 subgoal):
 1. \<And>s. s \<in> complex_cone' \<alpha> - {0} \<Longrightarrow> cmod (stirling_integral n s) \<le> ?c / cmod s ^ n
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
real n / real (Suc n) * (c / cmod s ^ n) = c1 / cmod s ^ n

goal (1 subgoal):
 1. \<And>s. s \<in> complex_cone' \<alpha> - {0} \<Longrightarrow> cmod (stirling_integral n s) \<le> ?c / cmod s ^ n
[PROOF STEP]
have "c1 / norm s ^ n + c2 / norm s ^ n = (c1 + c2) / norm s ^ n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. c1 / cmod s ^ n + c2 / cmod s ^ n = (c1 + c2) / cmod s ^ n
[PROOF STEP]
using s
[PROOF STATE]
proof (prove)
using this:
s \<in> complex_cone' \<alpha> - {0}

goal (1 subgoal):
 1. c1 / cmod s ^ n + c2 / cmod s ^ n = (c1 + c2) / cmod s ^ n
[PROOF STEP]
by (simp add: divide_simps)
[PROOF STATE]
proof (state)
this:
c1 / cmod s ^ n + c2 / cmod s ^ n = (c1 + c2) / cmod s ^ n

goal (1 subgoal):
 1. \<And>s. s \<in> complex_cone' \<alpha> - {0} \<Longrightarrow> cmod (stirling_integral n s) \<le> ?c / cmod s ^ n
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(\<And>x y. x \<le> y \<Longrightarrow> x + c2 / cmod s ^ n \<le> y + c2 / cmod s ^ n) \<Longrightarrow> cmod (stirling_integral n s) \<le> (c1 + c2) / cmod s ^ n
[PROOF STEP]
show "norm (stirling_integral n s) \<le> (c1 + c2) / norm s ^ n"
[PROOF STATE]
proof (prove)
using this:
(\<And>x y. x \<le> y \<Longrightarrow> x + c2 / cmod s ^ n \<le> y + c2 / cmod s ^ n) \<Longrightarrow> cmod (stirling_integral n s) \<le> (c1 + c2) / cmod s ^ n

goal (1 subgoal):
 1. cmod (stirling_integral n s) \<le> (c1 + c2) / cmod s ^ n
[PROOF STEP]
by - simp_all
[PROOF STATE]
proof (state)
this:
cmod (stirling_integral n s) \<le> (c1 + c2) / cmod s ^ n

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma maximal_acyclic_paths_code[code] :
  "maximal_acyclic_paths M = (let ps = acyclic_paths_up_to_length M (initial M) (size M - 1)
                               in Set.filter (\<lambda>p . \<not> (\<exists> p' \<in> ps . p' \<noteq> p \<and> is_prefix p p')) ps)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. maximal_acyclic_paths M = (let ps = acyclic_paths_up_to_length M (FSM.initial M) (FSM.size M - 1) in Set.filter (\<lambda>p. \<not> (\<exists>p'\<in>ps. p' \<noteq> p \<and> is_prefix p p')) ps)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. maximal_acyclic_paths M = (let ps = acyclic_paths_up_to_length M (FSM.initial M) (FSM.size M - 1) in Set.filter (\<lambda>p. \<not> (\<exists>p'\<in>ps. p' \<noteq> p \<and> is_prefix p p')) ps)
[PROOF STEP]
have scheme1: "\<And> P p . (\<exists> p' . p' \<noteq> [] \<and> P (p@p')) = (\<exists> p' \<in> {p . P p} . p' \<noteq> p \<and> is_prefix p p')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>P p. (\<exists>p'. p' \<noteq> [] \<and> P (p @ p')) = (\<exists>p'\<in>{p. P p}. p' \<noteq> p \<and> is_prefix p p')
[PROOF STEP]
unfolding is_prefix_prefix
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>P p. (\<exists>p'. p' \<noteq> [] \<and> P (p @ p')) = (\<exists>p'\<in>{p. P p}. p' \<noteq> p \<and> (\<exists>xs'. p' = p @ xs'))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(\<exists>p'. p' \<noteq> [] \<and> ?P (?p @ p')) = (\<exists>p'\<in>{p. ?P p}. p' \<noteq> ?p \<and> is_prefix ?p p')

goal (1 subgoal):
 1. maximal_acyclic_paths M = (let ps = acyclic_paths_up_to_length M (FSM.initial M) (FSM.size M - 1) in Set.filter (\<lambda>p. \<not> (\<exists>p'\<in>ps. p' \<noteq> p \<and> is_prefix p p')) ps)
[PROOF STEP]
have scheme2: "\<And> p . (path M (FSM.initial M) p
                          \<and> length p \<le> FSM.size M - 1
                          \<and> distinct (visited_states (FSM.initial M) p))
                      = (path M (FSM.initial M) p \<and> distinct (visited_states (FSM.initial M) p))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>p. (path M (FSM.initial M) p \<and> length p \<le> FSM.size M - 1 \<and> distinct (visited_states (FSM.initial M) p)) = (path M (FSM.initial M) p \<and> distinct (visited_states (FSM.initial M) p))
[PROOF STEP]
using acyclic_path_length_limit
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>path ?M ?q ?p; distinct (visited_states ?q ?p)\<rbrakk> \<Longrightarrow> length ?p < FSM.size ?M

goal (1 subgoal):
 1. \<And>p. (path M (FSM.initial M) p \<and> length p \<le> FSM.size M - 1 \<and> distinct (visited_states (FSM.initial M) p)) = (path M (FSM.initial M) p \<and> distinct (visited_states (FSM.initial M) p))
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
(path M (FSM.initial M) ?p1 \<and> length ?p1 \<le> FSM.size M - 1 \<and> distinct (visited_states (FSM.initial M) ?p1)) = (path M (FSM.initial M) ?p1 \<and> distinct (visited_states (FSM.initial M) ?p1))

goal (1 subgoal):
 1. maximal_acyclic_paths M = (let ps = acyclic_paths_up_to_length M (FSM.initial M) (FSM.size M - 1) in Set.filter (\<lambda>p. \<not> (\<exists>p'\<in>ps. p' \<noteq> p \<and> is_prefix p p')) ps)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. maximal_acyclic_paths M = (let ps = acyclic_paths_up_to_length M (FSM.initial M) (FSM.size M - 1) in Set.filter (\<lambda>p. \<not> (\<exists>p'\<in>ps. p' \<noteq> p \<and> is_prefix p p')) ps)
[PROOF STEP]
unfolding maximal_acyclic_paths_def acyclic_paths_up_to_length.simps Let_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {p. path M (FSM.initial M) p \<and> distinct (visited_states (FSM.initial M) p) \<and> (\<nexists>p'. p' \<noteq> [] \<and> path M (FSM.initial M) (p @ p') \<and> distinct (visited_states (FSM.initial M) (p @ p')))} = Set.filter (\<lambda>p. \<not> (\<exists>p'\<in>{p. path M (FSM.initial M) p \<and> length p \<le> FSM.size M - 1 \<and> distinct (visited_states (FSM.initial M) p)}. p' \<noteq> p \<and> is_prefix p p')) {p. path M (FSM.initial M) p \<and> length p \<le> FSM.size M - 1 \<and> distinct (visited_states (FSM.initial M) p)}
[PROOF STEP]
unfolding scheme1[of "\<lambda>p . path M (initial M) p \<and> distinct (visited_states (initial M) p)"]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {p. path M (FSM.initial M) p \<and> distinct (visited_states (FSM.initial M) p) \<and> \<not> (\<exists>p'\<in>{p. path M (FSM.initial M) p \<and> distinct (visited_states (FSM.initial M) p)}. p' \<noteq> p \<and> is_prefix p p')} = Set.filter (\<lambda>p. \<not> (\<exists>p'\<in>{p. path M (FSM.initial M) p \<and> length p \<le> FSM.size M - 1 \<and> distinct (visited_states (FSM.initial M) p)}. p' \<noteq> p \<and> is_prefix p p')) {p. path M (FSM.initial M) p \<and> length p \<le> FSM.size M - 1 \<and> distinct (visited_states (FSM.initial M) p)}
[PROOF STEP]
unfolding scheme2
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {p. path M (FSM.initial M) p \<and> distinct (visited_states (FSM.initial M) p) \<and> \<not> (\<exists>p'\<in>{p. path M (FSM.initial M) p \<and> distinct (visited_states (FSM.initial M) p)}. p' \<noteq> p \<and> is_prefix p p')} = Set.filter (\<lambda>p. \<not> (\<exists>p'\<in>{p. path M (FSM.initial M) p \<and> distinct (visited_states (FSM.initial M) p)}. p' \<noteq> p \<and> is_prefix p p')) {p. path M (FSM.initial M) p \<and> distinct (visited_states (FSM.initial M) p)}
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
maximal_acyclic_paths M = (let ps = acyclic_paths_up_to_length M (FSM.initial M) (FSM.size M - 1) in Set.filter (\<lambda>p. \<not> (\<exists>p'\<in>ps. p' \<noteq> p \<and> is_prefix p p')) ps)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma l2product_radd:
   "\<lbrakk>f square_integrable S; g square_integrable S; h square_integrable S\<rbrakk>
    \<Longrightarrow> l2product S f(\<lambda>x. g x + h x) = l2product S f g + l2product S f h"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>f square_integrable S; g square_integrable S; h square_integrable S\<rbrakk> \<Longrightarrow> l2product S f (\<lambda>x. g x + h x) = l2product S f g + l2product S f h
[PROOF STEP]
by (simp add: l2product_def algebra_simps square_integrable_imp_integrable_product)


[STATEMENT]
lemma alpha_equiv_refl[intro?]:
  assumes "fmpred (=) \<Gamma>"
  shows "alpha_equiv \<Gamma> t t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. alpha_equiv \<Gamma> t t
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
fmpred (=) \<Gamma>

goal (1 subgoal):
 1. alpha_equiv \<Gamma> t t
[PROOF STEP]
proof (induction t arbitrary: \<Gamma>)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>x \<Gamma>. fmpred (=) \<Gamma> \<Longrightarrow> alpha_equiv \<Gamma> (Nconst x) (Nconst x)
 2. \<And>x \<Gamma>. fmpred (=) \<Gamma> \<Longrightarrow> alpha_equiv \<Gamma> (Nvar x) (Nvar x)
 3. \<And>x1a t \<Gamma>. \<lbrakk>\<And>\<Gamma>. fmpred (=) \<Gamma> \<Longrightarrow> alpha_equiv \<Gamma> t t; fmpred (=) \<Gamma>\<rbrakk> \<Longrightarrow> alpha_equiv \<Gamma> (\<Lambda>\<^sub>n x1a. t) (\<Lambda>\<^sub>n x1a. t)
 4. \<And>t1 t2 \<Gamma>. \<lbrakk>\<And>\<Gamma>. fmpred (=) \<Gamma> \<Longrightarrow> alpha_equiv \<Gamma> t1 t1; \<And>\<Gamma>. fmpred (=) \<Gamma> \<Longrightarrow> alpha_equiv \<Gamma> t2 t2; fmpred (=) \<Gamma>\<rbrakk> \<Longrightarrow> alpha_equiv \<Gamma> (t1 $\<^sub>n t2) (t1 $\<^sub>n t2)
[PROOF STEP]
case Napp
[PROOF STATE]
proof (state)
this:
fmpred (=) ?\<Gamma> \<Longrightarrow> alpha_equiv ?\<Gamma> t1_ t1_
fmpred (=) ?\<Gamma> \<Longrightarrow> alpha_equiv ?\<Gamma> t2_ t2_
fmpred (=) \<Gamma>

goal (4 subgoals):
 1. \<And>x \<Gamma>. fmpred (=) \<Gamma> \<Longrightarrow> alpha_equiv \<Gamma> (Nconst x) (Nconst x)
 2. \<And>x \<Gamma>. fmpred (=) \<Gamma> \<Longrightarrow> alpha_equiv \<Gamma> (Nvar x) (Nvar x)
 3. \<And>x1a t \<Gamma>. \<lbrakk>\<And>\<Gamma>. fmpred (=) \<Gamma> \<Longrightarrow> alpha_equiv \<Gamma> t t; fmpred (=) \<Gamma>\<rbrakk> \<Longrightarrow> alpha_equiv \<Gamma> (\<Lambda>\<^sub>n x1a. t) (\<Lambda>\<^sub>n x1a. t)
 4. \<And>t1 t2 \<Gamma>. \<lbrakk>\<And>\<Gamma>. fmpred (=) \<Gamma> \<Longrightarrow> alpha_equiv \<Gamma> t1 t1; \<And>\<Gamma>. fmpred (=) \<Gamma> \<Longrightarrow> alpha_equiv \<Gamma> t2 t2; fmpred (=) \<Gamma>\<rbrakk> \<Longrightarrow> alpha_equiv \<Gamma> (t1 $\<^sub>n t2) (t1 $\<^sub>n t2)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. alpha_equiv \<Gamma> (t1_ $\<^sub>n t2_) (t1_ $\<^sub>n t2_)
[PROOF STEP]
apply (rule alpha_equiv.app; rule Napp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. fmpred (=) \<Gamma>
 2. fmpred (=) \<Gamma>
[PROOF STEP]
using Napp.prems
[PROOF STATE]
proof (prove)
using this:
fmpred (=) \<Gamma>

goal (2 subgoals):
 1. fmpred (=) \<Gamma>
 2. fmpred (=) \<Gamma>
[PROOF STEP]
unfolding fdisjnt_alt_def
[PROOF STATE]
proof (prove)
using this:
fmpred (=) \<Gamma>

goal (2 subgoals):
 1. fmpred (=) \<Gamma>
 2. fmpred (=) \<Gamma>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
alpha_equiv \<Gamma> (t1_ $\<^sub>n t2_) (t1_ $\<^sub>n t2_)

goal (3 subgoals):
 1. \<And>x \<Gamma>. fmpred (=) \<Gamma> \<Longrightarrow> alpha_equiv \<Gamma> (Nconst x) (Nconst x)
 2. \<And>x \<Gamma>. fmpred (=) \<Gamma> \<Longrightarrow> alpha_equiv \<Gamma> (Nvar x) (Nvar x)
 3. \<And>x1a t \<Gamma>. \<lbrakk>\<And>\<Gamma>. fmpred (=) \<Gamma> \<Longrightarrow> alpha_equiv \<Gamma> t t; fmpred (=) \<Gamma>\<rbrakk> \<Longrightarrow> alpha_equiv \<Gamma> (\<Lambda>\<^sub>n x1a. t) (\<Lambda>\<^sub>n x1a. t)
[PROOF STEP]
qed (auto simp: fdisjnt_alt_def intro: alpha_equiv.intros)


[STATEMENT]
lemma lemma2_3:
  assumes "\<Gamma> \<turnstile> e, eP, eV : \<tau>"
  shows   "erase_env \<Gamma> \<turnstile>\<^sub>W e : erase \<tau>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. erase_env \<Gamma> \<turnstile>\<^sub>W e : erase \<tau>
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<Gamma> \<turnstile> e, eP, eV : \<tau>

goal (1 subgoal):
 1. erase_env \<Gamma> \<turnstile>\<^sub>W e : erase \<tau>
[PROOF STEP]
unfolding erase_env_def
[PROOF STATE]
proof (prove)
using this:
\<Gamma> \<turnstile> e, eP, eV : \<tau>

goal (1 subgoal):
 1. fmmap erase \<Gamma> \<turnstile>\<^sub>W e : erase \<tau>
[PROOF STEP]
proof (nominal_induct \<Gamma> e eP eV \<tau> rule: agree.strong_induct)
[PROOF STATE]
proof (state)
goal (17 subgoals):
 1. \<And>\<Gamma>. fmmap erase \<Gamma> \<turnstile>\<^sub>W Unit : erase One
 2. \<And>\<Gamma> x \<tau>. \<Gamma> $$ x = Some \<tau> \<Longrightarrow> fmmap erase \<Gamma> \<turnstile>\<^sub>W Var x : erase \<tau>
 3. \<And>x \<Gamma> \<tau>\<^sub>1 e eP eV \<tau>\<^sub>2. \<lbrakk>atom x \<sharp> \<Gamma>; \<Gamma>(x $$:= \<tau>\<^sub>1) \<turnstile> e, eP, eV : \<tau>\<^sub>2; fmmap erase \<Gamma>(x $$:= \<tau>\<^sub>1) \<turnstile>\<^sub>W e : erase \<tau>\<^sub>2\<rbrakk> \<Longrightarrow> fmmap erase \<Gamma> \<turnstile>\<^sub>W Lam x e : erase (Fun \<tau>\<^sub>1 \<tau>\<^sub>2)
 4. \<And>\<Gamma> e\<^sub>1 eP\<^sub>1 eV\<^sub>1 \<tau>\<^sub>1 \<tau>\<^sub>2 e\<^sub>2 eP\<^sub>2 eV\<^sub>2. \<lbrakk>\<Gamma> \<turnstile> e\<^sub>1, eP\<^sub>1, eV\<^sub>1 : Fun \<tau>\<^sub>1 \<tau>\<^sub>2; fmmap erase \<Gamma> \<turnstile>\<^sub>W e\<^sub>1 : erase (Fun \<tau>\<^sub>1 \<tau>\<^sub>2); \<Gamma> \<turnstile> e\<^sub>2, eP\<^sub>2, eV\<^sub>2 : \<tau>\<^sub>1; fmmap erase \<Gamma> \<turnstile>\<^sub>W e\<^sub>2 : erase \<tau>\<^sub>1\<rbrakk> \<Longrightarrow> fmmap erase \<Gamma> \<turnstile>\<^sub>W App e\<^sub>1 e\<^sub>2 : erase \<tau>\<^sub>2
 5. \<And>x \<Gamma> e\<^sub>1 eP\<^sub>1 eV\<^sub>1 \<tau>\<^sub>1 e\<^sub>2 eP\<^sub>2 eV\<^sub>2 \<tau>\<^sub>2. \<lbrakk>atom x \<sharp> \<Gamma>; atom x \<sharp> e\<^sub>1; atom x \<sharp> eP\<^sub>1; atom x \<sharp> eV\<^sub>1; \<Gamma> \<turnstile> e\<^sub>1, eP\<^sub>1, eV\<^sub>1 : \<tau>\<^sub>1; fmmap erase \<Gamma> \<turnstile>\<^sub>W e\<^sub>1 : erase \<tau>\<^sub>1; \<Gamma>(x $$:= \<tau>\<^sub>1) \<turnstile> e\<^sub>2, eP\<^sub>2, eV\<^sub>2 : \<tau>\<^sub>2; fmmap erase \<Gamma>(x $$:= \<tau>\<^sub>1) \<turnstile>\<^sub>W e\<^sub>2 : erase \<tau>\<^sub>2\<rbrakk> \<Longrightarrow> fmmap erase \<Gamma> \<turnstile>\<^sub>W Syntax.Let e\<^sub>1 x e\<^sub>2 : erase \<tau>\<^sub>2
 6. \<And>x \<Gamma> y \<tau>\<^sub>1 \<tau>\<^sub>2 e eP eV. \<lbrakk>atom x \<sharp> \<Gamma>; atom y \<sharp> \<Gamma>; atom y \<sharp> x; \<Gamma>(x $$:= Fun \<tau>\<^sub>1 \<tau>\<^sub>2) \<turnstile> Lam y e, Lam y eP, Lam y eV : Fun \<tau>\<^sub>1 \<tau>\<^sub>2; fmmap erase \<Gamma>(x $$:= Fun \<tau>\<^sub>1 \<tau>\<^sub>2) \<turnstile>\<^sub>W Lam y e : erase (Fun \<tau>\<^sub>1 \<tau>\<^sub>2)\<rbrakk> \<Longrightarrow> fmmap erase \<Gamma> \<turnstile>\<^sub>W Rec x (Lam y e) : erase (Fun \<tau>\<^sub>1 \<tau>\<^sub>2)
 7. \<And>\<Gamma> e eP eV \<tau>\<^sub>1 \<tau>\<^sub>2. \<lbrakk>\<Gamma> \<turnstile> e, eP, eV : \<tau>\<^sub>1; fmmap erase \<Gamma> \<turnstile>\<^sub>W e : erase \<tau>\<^sub>1\<rbrakk> \<Longrightarrow> fmmap erase \<Gamma> \<turnstile>\<^sub>W Inj1 e : erase (Syntax.Sum \<tau>\<^sub>1 \<tau>\<^sub>2)
 8. \<And>\<Gamma> e eP eV \<tau>\<^sub>2 \<tau>\<^sub>1. \<lbrakk>\<Gamma> \<turnstile> e, eP, eV : \<tau>\<^sub>2; fmmap erase \<Gamma> \<turnstile>\<^sub>W e : erase \<tau>\<^sub>2\<rbrakk> \<Longrightarrow> fmmap erase \<Gamma> \<turnstile>\<^sub>W Inj2 e : erase (Syntax.Sum \<tau>\<^sub>1 \<tau>\<^sub>2)
 9. \<And>\<Gamma> e eP eV \<tau>\<^sub>1 \<tau>\<^sub>2 e\<^sub>1 eP\<^sub>1 eV\<^sub>1 \<tau> e\<^sub>2 eP\<^sub>2 eV\<^sub>2. \<lbrakk>\<Gamma> \<turnstile> e, eP, eV : Syntax.Sum \<tau>\<^sub>1 \<tau>\<^sub>2; fmmap erase \<Gamma> \<turnstile>\<^sub>W e : erase (Syntax.Sum \<tau>\<^sub>1 \<tau>\<^sub>2); \<Gamma> \<turnstile> e\<^sub>1, eP\<^sub>1, eV\<^sub>1 : Fun \<tau>\<^sub>1 \<tau>; fmmap erase \<Gamma> \<turnstile>\<^sub>W e\<^sub>1 : erase (Fun \<tau>\<^sub>1 \<tau>); \<Gamma> \<turnstile> e\<^sub>2, eP\<^sub>2, eV\<^sub>2 : Fun \<tau>\<^sub>2 \<tau>; fmmap erase \<Gamma> \<turnstile>\<^sub>W e\<^sub>2 : erase (Fun \<tau>\<^sub>2 \<tau>)\<rbrakk> \<Longrightarrow> fmmap erase \<Gamma> \<turnstile>\<^sub>W Case e e\<^sub>1 e\<^sub>2 : erase \<tau>
 10. \<And>\<Gamma> e\<^sub>1 eP\<^sub>1 eV\<^sub>1 \<tau>\<^sub>1 e\<^sub>2 eP\<^sub>2 eV\<^sub>2 \<tau>\<^sub>2. \<lbrakk>\<Gamma> \<turnstile> e\<^sub>1, eP\<^sub>1, eV\<^sub>1 : \<tau>\<^sub>1; fmmap erase \<Gamma> \<turnstile>\<^sub>W e\<^sub>1 : erase \<tau>\<^sub>1; \<Gamma> \<turnstile> e\<^sub>2, eP\<^sub>2, eV\<^sub>2 : \<tau>\<^sub>2; fmmap erase \<Gamma> \<turnstile>\<^sub>W e\<^sub>2 : erase \<tau>\<^sub>2\<rbrakk> \<Longrightarrow> fmmap erase \<Gamma> \<turnstile>\<^sub>W Syntax.Pair e\<^sub>1 e\<^sub>2 : erase (Syntax.Prod \<tau>\<^sub>1 \<tau>\<^sub>2)
A total of 17 subgoals...
[PROOF STEP]
case (a_HashI v vP \<tau> h \<Gamma>)
[PROOF STATE]
proof (state)
this:
{$$} \<turnstile> v, vP, \<lparr>vP\<rparr> : \<tau>
fmmap erase {$$} \<turnstile>\<^sub>W v : erase \<tau>
hash \<lparr>vP\<rparr> = h
value v
value vP

goal (17 subgoals):
 1. \<And>\<Gamma>. fmmap erase \<Gamma> \<turnstile>\<^sub>W Unit : erase One
 2. \<And>\<Gamma> x \<tau>. \<Gamma> $$ x = Some \<tau> \<Longrightarrow> fmmap erase \<Gamma> \<turnstile>\<^sub>W Var x : erase \<tau>
 3. \<And>x \<Gamma> \<tau>\<^sub>1 e eP eV \<tau>\<^sub>2. \<lbrakk>atom x \<sharp> \<Gamma>; \<Gamma>(x $$:= \<tau>\<^sub>1) \<turnstile> e, eP, eV : \<tau>\<^sub>2; fmmap erase \<Gamma>(x $$:= \<tau>\<^sub>1) \<turnstile>\<^sub>W e : erase \<tau>\<^sub>2\<rbrakk> \<Longrightarrow> fmmap erase \<Gamma> \<turnstile>\<^sub>W Lam x e : erase (Fun \<tau>\<^sub>1 \<tau>\<^sub>2)
 4. \<And>\<Gamma> e\<^sub>1 eP\<^sub>1 eV\<^sub>1 \<tau>\<^sub>1 \<tau>\<^sub>2 e\<^sub>2 eP\<^sub>2 eV\<^sub>2. \<lbrakk>\<Gamma> \<turnstile> e\<^sub>1, eP\<^sub>1, eV\<^sub>1 : Fun \<tau>\<^sub>1 \<tau>\<^sub>2; fmmap erase \<Gamma> \<turnstile>\<^sub>W e\<^sub>1 : erase (Fun \<tau>\<^sub>1 \<tau>\<^sub>2); \<Gamma> \<turnstile> e\<^sub>2, eP\<^sub>2, eV\<^sub>2 : \<tau>\<^sub>1; fmmap erase \<Gamma> \<turnstile>\<^sub>W e\<^sub>2 : erase \<tau>\<^sub>1\<rbrakk> \<Longrightarrow> fmmap erase \<Gamma> \<turnstile>\<^sub>W App e\<^sub>1 e\<^sub>2 : erase \<tau>\<^sub>2
 5. \<And>x \<Gamma> e\<^sub>1 eP\<^sub>1 eV\<^sub>1 \<tau>\<^sub>1 e\<^sub>2 eP\<^sub>2 eV\<^sub>2 \<tau>\<^sub>2. \<lbrakk>atom x \<sharp> \<Gamma>; atom x \<sharp> e\<^sub>1; atom x \<sharp> eP\<^sub>1; atom x \<sharp> eV\<^sub>1; \<Gamma> \<turnstile> e\<^sub>1, eP\<^sub>1, eV\<^sub>1 : \<tau>\<^sub>1; fmmap erase \<Gamma> \<turnstile>\<^sub>W e\<^sub>1 : erase \<tau>\<^sub>1; \<Gamma>(x $$:= \<tau>\<^sub>1) \<turnstile> e\<^sub>2, eP\<^sub>2, eV\<^sub>2 : \<tau>\<^sub>2; fmmap erase \<Gamma>(x $$:= \<tau>\<^sub>1) \<turnstile>\<^sub>W e\<^sub>2 : erase \<tau>\<^sub>2\<rbrakk> \<Longrightarrow> fmmap erase \<Gamma> \<turnstile>\<^sub>W Syntax.Let e\<^sub>1 x e\<^sub>2 : erase \<tau>\<^sub>2
 6. \<And>x \<Gamma> y \<tau>\<^sub>1 \<tau>\<^sub>2 e eP eV. \<lbrakk>atom x \<sharp> \<Gamma>; atom y \<sharp> \<Gamma>; atom y \<sharp> x; \<Gamma>(x $$:= Fun \<tau>\<^sub>1 \<tau>\<^sub>2) \<turnstile> Lam y e, Lam y eP, Lam y eV : Fun \<tau>\<^sub>1 \<tau>\<^sub>2; fmmap erase \<Gamma>(x $$:= Fun \<tau>\<^sub>1 \<tau>\<^sub>2) \<turnstile>\<^sub>W Lam y e : erase (Fun \<tau>\<^sub>1 \<tau>\<^sub>2)\<rbrakk> \<Longrightarrow> fmmap erase \<Gamma> \<turnstile>\<^sub>W Rec x (Lam y e) : erase (Fun \<tau>\<^sub>1 \<tau>\<^sub>2)
 7. \<And>\<Gamma> e eP eV \<tau>\<^sub>1 \<tau>\<^sub>2. \<lbrakk>\<Gamma> \<turnstile> e, eP, eV : \<tau>\<^sub>1; fmmap erase \<Gamma> \<turnstile>\<^sub>W e : erase \<tau>\<^sub>1\<rbrakk> \<Longrightarrow> fmmap erase \<Gamma> \<turnstile>\<^sub>W Inj1 e : erase (Syntax.Sum \<tau>\<^sub>1 \<tau>\<^sub>2)
 8. \<And>\<Gamma> e eP eV \<tau>\<^sub>2 \<tau>\<^sub>1. \<lbrakk>\<Gamma> \<turnstile> e, eP, eV : \<tau>\<^sub>2; fmmap erase \<Gamma> \<turnstile>\<^sub>W e : erase \<tau>\<^sub>2\<rbrakk> \<Longrightarrow> fmmap erase \<Gamma> \<turnstile>\<^sub>W Inj2 e : erase (Syntax.Sum \<tau>\<^sub>1 \<tau>\<^sub>2)
 9. \<And>\<Gamma> e eP eV \<tau>\<^sub>1 \<tau>\<^sub>2 e\<^sub>1 eP\<^sub>1 eV\<^sub>1 \<tau> e\<^sub>2 eP\<^sub>2 eV\<^sub>2. \<lbrakk>\<Gamma> \<turnstile> e, eP, eV : Syntax.Sum \<tau>\<^sub>1 \<tau>\<^sub>2; fmmap erase \<Gamma> \<turnstile>\<^sub>W e : erase (Syntax.Sum \<tau>\<^sub>1 \<tau>\<^sub>2); \<Gamma> \<turnstile> e\<^sub>1, eP\<^sub>1, eV\<^sub>1 : Fun \<tau>\<^sub>1 \<tau>; fmmap erase \<Gamma> \<turnstile>\<^sub>W e\<^sub>1 : erase (Fun \<tau>\<^sub>1 \<tau>); \<Gamma> \<turnstile> e\<^sub>2, eP\<^sub>2, eV\<^sub>2 : Fun \<tau>\<^sub>2 \<tau>; fmmap erase \<Gamma> \<turnstile>\<^sub>W e\<^sub>2 : erase (Fun \<tau>\<^sub>2 \<tau>)\<rbrakk> \<Longrightarrow> fmmap erase \<Gamma> \<turnstile>\<^sub>W Case e e\<^sub>1 e\<^sub>2 : erase \<tau>
 10. \<And>\<Gamma> e\<^sub>1 eP\<^sub>1 eV\<^sub>1 \<tau>\<^sub>1 e\<^sub>2 eP\<^sub>2 eV\<^sub>2 \<tau>\<^sub>2. \<lbrakk>\<Gamma> \<turnstile> e\<^sub>1, eP\<^sub>1, eV\<^sub>1 : \<tau>\<^sub>1; fmmap erase \<Gamma> \<turnstile>\<^sub>W e\<^sub>1 : erase \<tau>\<^sub>1; \<Gamma> \<turnstile> e\<^sub>2, eP\<^sub>2, eV\<^sub>2 : \<tau>\<^sub>2; fmmap erase \<Gamma> \<turnstile>\<^sub>W e\<^sub>2 : erase \<tau>\<^sub>2\<rbrakk> \<Longrightarrow> fmmap erase \<Gamma> \<turnstile>\<^sub>W Syntax.Pair e\<^sub>1 e\<^sub>2 : erase (Syntax.Prod \<tau>\<^sub>1 \<tau>\<^sub>2)
A total of 17 subgoals...
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
{$$} \<turnstile> v, vP, \<lparr>vP\<rparr> : \<tau>
fmmap erase {$$} \<turnstile>\<^sub>W v : erase \<tau>
hash \<lparr>vP\<rparr> = h
value v
value vP
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
{$$} \<turnstile> v, vP, \<lparr>vP\<rparr> : \<tau>
fmmap erase {$$} \<turnstile>\<^sub>W v : erase \<tau>
hash \<lparr>vP\<rparr> = h
value v
value vP

goal (1 subgoal):
 1. fmmap erase \<Gamma> \<turnstile>\<^sub>W v : erase (AuthT \<tau>)
[PROOF STEP]
by (induct \<Gamma>) (auto simp: judge_weak_weakening_2 fmmap_fmupd judge_weak_fresh_env_fresh_term fresh_tyenv_None)
[PROOF STATE]
proof (state)
this:
fmmap erase \<Gamma> \<turnstile>\<^sub>W v : erase (AuthT \<tau>)

goal (16 subgoals):
 1. \<And>\<Gamma>. fmmap erase \<Gamma> \<turnstile>\<^sub>W Unit : erase One
 2. \<And>\<Gamma> x \<tau>. \<Gamma> $$ x = Some \<tau> \<Longrightarrow> fmmap erase \<Gamma> \<turnstile>\<^sub>W Var x : erase \<tau>
 3. \<And>x \<Gamma> \<tau>\<^sub>1 e eP eV \<tau>\<^sub>2. \<lbrakk>atom x \<sharp> \<Gamma>; \<Gamma>(x $$:= \<tau>\<^sub>1) \<turnstile> e, eP, eV : \<tau>\<^sub>2; fmmap erase \<Gamma>(x $$:= \<tau>\<^sub>1) \<turnstile>\<^sub>W e : erase \<tau>\<^sub>2\<rbrakk> \<Longrightarrow> fmmap erase \<Gamma> \<turnstile>\<^sub>W Lam x e : erase (Fun \<tau>\<^sub>1 \<tau>\<^sub>2)
 4. \<And>\<Gamma> e\<^sub>1 eP\<^sub>1 eV\<^sub>1 \<tau>\<^sub>1 \<tau>\<^sub>2 e\<^sub>2 eP\<^sub>2 eV\<^sub>2. \<lbrakk>\<Gamma> \<turnstile> e\<^sub>1, eP\<^sub>1, eV\<^sub>1 : Fun \<tau>\<^sub>1 \<tau>\<^sub>2; fmmap erase \<Gamma> \<turnstile>\<^sub>W e\<^sub>1 : erase (Fun \<tau>\<^sub>1 \<tau>\<^sub>2); \<Gamma> \<turnstile> e\<^sub>2, eP\<^sub>2, eV\<^sub>2 : \<tau>\<^sub>1; fmmap erase \<Gamma> \<turnstile>\<^sub>W e\<^sub>2 : erase \<tau>\<^sub>1\<rbrakk> \<Longrightarrow> fmmap erase \<Gamma> \<turnstile>\<^sub>W App e\<^sub>1 e\<^sub>2 : erase \<tau>\<^sub>2
 5. \<And>x \<Gamma> e\<^sub>1 eP\<^sub>1 eV\<^sub>1 \<tau>\<^sub>1 e\<^sub>2 eP\<^sub>2 eV\<^sub>2 \<tau>\<^sub>2. \<lbrakk>atom x \<sharp> \<Gamma>; atom x \<sharp> e\<^sub>1; atom x \<sharp> eP\<^sub>1; atom x \<sharp> eV\<^sub>1; \<Gamma> \<turnstile> e\<^sub>1, eP\<^sub>1, eV\<^sub>1 : \<tau>\<^sub>1; fmmap erase \<Gamma> \<turnstile>\<^sub>W e\<^sub>1 : erase \<tau>\<^sub>1; \<Gamma>(x $$:= \<tau>\<^sub>1) \<turnstile> e\<^sub>2, eP\<^sub>2, eV\<^sub>2 : \<tau>\<^sub>2; fmmap erase \<Gamma>(x $$:= \<tau>\<^sub>1) \<turnstile>\<^sub>W e\<^sub>2 : erase \<tau>\<^sub>2\<rbrakk> \<Longrightarrow> fmmap erase \<Gamma> \<turnstile>\<^sub>W Syntax.Let e\<^sub>1 x e\<^sub>2 : erase \<tau>\<^sub>2
 6. \<And>x \<Gamma> y \<tau>\<^sub>1 \<tau>\<^sub>2 e eP eV. \<lbrakk>atom x \<sharp> \<Gamma>; atom y \<sharp> \<Gamma>; atom y \<sharp> x; \<Gamma>(x $$:= Fun \<tau>\<^sub>1 \<tau>\<^sub>2) \<turnstile> Lam y e, Lam y eP, Lam y eV : Fun \<tau>\<^sub>1 \<tau>\<^sub>2; fmmap erase \<Gamma>(x $$:= Fun \<tau>\<^sub>1 \<tau>\<^sub>2) \<turnstile>\<^sub>W Lam y e : erase (Fun \<tau>\<^sub>1 \<tau>\<^sub>2)\<rbrakk> \<Longrightarrow> fmmap erase \<Gamma> \<turnstile>\<^sub>W Rec x (Lam y e) : erase (Fun \<tau>\<^sub>1 \<tau>\<^sub>2)
 7. \<And>\<Gamma> e eP eV \<tau>\<^sub>1 \<tau>\<^sub>2. \<lbrakk>\<Gamma> \<turnstile> e, eP, eV : \<tau>\<^sub>1; fmmap erase \<Gamma> \<turnstile>\<^sub>W e : erase \<tau>\<^sub>1\<rbrakk> \<Longrightarrow> fmmap erase \<Gamma> \<turnstile>\<^sub>W Inj1 e : erase (Syntax.Sum \<tau>\<^sub>1 \<tau>\<^sub>2)
 8. \<And>\<Gamma> e eP eV \<tau>\<^sub>2 \<tau>\<^sub>1. \<lbrakk>\<Gamma> \<turnstile> e, eP, eV : \<tau>\<^sub>2; fmmap erase \<Gamma> \<turnstile>\<^sub>W e : erase \<tau>\<^sub>2\<rbrakk> \<Longrightarrow> fmmap erase \<Gamma> \<turnstile>\<^sub>W Inj2 e : erase (Syntax.Sum \<tau>\<^sub>1 \<tau>\<^sub>2)
 9. \<And>\<Gamma> e eP eV \<tau>\<^sub>1 \<tau>\<^sub>2 e\<^sub>1 eP\<^sub>1 eV\<^sub>1 \<tau> e\<^sub>2 eP\<^sub>2 eV\<^sub>2. \<lbrakk>\<Gamma> \<turnstile> e, eP, eV : Syntax.Sum \<tau>\<^sub>1 \<tau>\<^sub>2; fmmap erase \<Gamma> \<turnstile>\<^sub>W e : erase (Syntax.Sum \<tau>\<^sub>1 \<tau>\<^sub>2); \<Gamma> \<turnstile> e\<^sub>1, eP\<^sub>1, eV\<^sub>1 : Fun \<tau>\<^sub>1 \<tau>; fmmap erase \<Gamma> \<turnstile>\<^sub>W e\<^sub>1 : erase (Fun \<tau>\<^sub>1 \<tau>); \<Gamma> \<turnstile> e\<^sub>2, eP\<^sub>2, eV\<^sub>2 : Fun \<tau>\<^sub>2 \<tau>; fmmap erase \<Gamma> \<turnstile>\<^sub>W e\<^sub>2 : erase (Fun \<tau>\<^sub>2 \<tau>)\<rbrakk> \<Longrightarrow> fmmap erase \<Gamma> \<turnstile>\<^sub>W Case e e\<^sub>1 e\<^sub>2 : erase \<tau>
 10. \<And>\<Gamma> e\<^sub>1 eP\<^sub>1 eV\<^sub>1 \<tau>\<^sub>1 e\<^sub>2 eP\<^sub>2 eV\<^sub>2 \<tau>\<^sub>2. \<lbrakk>\<Gamma> \<turnstile> e\<^sub>1, eP\<^sub>1, eV\<^sub>1 : \<tau>\<^sub>1; fmmap erase \<Gamma> \<turnstile>\<^sub>W e\<^sub>1 : erase \<tau>\<^sub>1; \<Gamma> \<turnstile> e\<^sub>2, eP\<^sub>2, eV\<^sub>2 : \<tau>\<^sub>2; fmmap erase \<Gamma> \<turnstile>\<^sub>W e\<^sub>2 : erase \<tau>\<^sub>2\<rbrakk> \<Longrightarrow> fmmap erase \<Gamma> \<turnstile>\<^sub>W Syntax.Pair e\<^sub>1 e\<^sub>2 : erase (Syntax.Prod \<tau>\<^sub>1 \<tau>\<^sub>2)
A total of 16 subgoals...
[PROOF STEP]
qed (simp_all add: fresh_fmmap_erase_fresh fmmap_fmupd judge_weak_fresh_env_fresh_term)


[STATEMENT]
lemma rt_fresh_asI [intro!]:
  assumes "rt1 \<sqsubseteq>\<^bsub>dip\<^esub> rt2"
      and "rt2 \<sqsubseteq>\<^bsub>dip\<^esub> rt1"
    shows "rt1 \<approx>\<^bsub>dip\<^esub> rt2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rt1 \<approx>\<^bsub>dip\<^esub> rt2
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
rt1 \<sqsubseteq>\<^bsub>dip\<^esub> rt2
rt2 \<sqsubseteq>\<^bsub>dip\<^esub> rt1

goal (1 subgoal):
 1. rt1 \<approx>\<^bsub>dip\<^esub> rt2
[PROOF STEP]
unfolding rt_fresh_as_def
[PROOF STATE]
proof (prove)
using this:
rt1 \<sqsubseteq>\<^bsub>dip\<^esub> rt2
rt2 \<sqsubseteq>\<^bsub>dip\<^esub> rt1

goal (1 subgoal):
 1. rt1 \<sqsubseteq>\<^bsub>dip\<^esub> rt2 \<and> rt2 \<sqsubseteq>\<^bsub>dip\<^esub> rt1
[PROOF STEP]
by simp


[STATEMENT]
lemma succ_range: "\<forall>v \<in> succs n. v < length (g_V G)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>v\<in>succs n. v < length (g_V G)
[PROOF STEP]
by (insert succ_in_G verts_set) auto


[STATEMENT]
lemma pow_gen_mod_mult:
  shows"(\<^bold>g [^] (a::nat) \<otimes> \<^bold>g [^] (b::nat)) [^] ((c::int)* int (d::nat)) = (\<^bold>g [^] a \<otimes> \<^bold>g [^] b) [^] ((c*int d) mod (order G))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<^bold>g [^] a \<otimes> \<^bold>g [^] b) [^] (c * int d) = (\<^bold>g [^] a \<otimes> \<^bold>g [^] b) [^] (c * int d mod int (order G))
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<^bold>g [^] a \<otimes> \<^bold>g [^] b) [^] (c * int d) = (\<^bold>g [^] a \<otimes> \<^bold>g [^] b) [^] (c * int d mod int (order G))
[PROOF STEP]
have "(\<^bold>g [^] (a::nat) \<otimes> \<^bold>g [^] (b::nat)) \<in> carrier G"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<^bold>g [^] a \<otimes> \<^bold>g [^] b \<in> carrier G
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<^bold>g [^] a \<otimes> \<^bold>g [^] b \<in> carrier G

goal (1 subgoal):
 1. (\<^bold>g [^] a \<otimes> \<^bold>g [^] b) [^] (c * int d) = (\<^bold>g [^] a \<otimes> \<^bold>g [^] b) [^] (c * int d mod int (order G))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<^bold>g [^] a \<otimes> \<^bold>g [^] b \<in> carrier G
[PROOF STEP]
obtain n :: nat where n: "\<^bold>g [^] n = (\<^bold>g [^] (a::nat) \<otimes> \<^bold>g [^] (b::nat))"
[PROOF STATE]
proof (prove)
using this:
\<^bold>g [^] a \<otimes> \<^bold>g [^] b \<in> carrier G

goal (1 subgoal):
 1. (\<And>n. \<^bold>g [^] n = \<^bold>g [^] a \<otimes> \<^bold>g [^] b \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (simp add: monoid.nat_pow_mult)
[PROOF STATE]
proof (state)
this:
\<^bold>g [^] n = \<^bold>g [^] a \<otimes> \<^bold>g [^] b

goal (1 subgoal):
 1. (\<^bold>g [^] a \<otimes> \<^bold>g [^] b) [^] (c * int d) = (\<^bold>g [^] a \<otimes> \<^bold>g [^] b) [^] (c * int d mod int (order G))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<^bold>g [^] n = \<^bold>g [^] a \<otimes> \<^bold>g [^] b

goal (1 subgoal):
 1. (\<^bold>g [^] a \<otimes> \<^bold>g [^] b) [^] (c * int d) = (\<^bold>g [^] a \<otimes> \<^bold>g [^] b) [^] (c * int d mod int (order G))
[PROOF STEP]
obtain r where r: "r = c*int d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>r. r = c * int d \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
r = c * int d

goal (1 subgoal):
 1. (\<^bold>g [^] a \<otimes> \<^bold>g [^] b) [^] (c * int d) = (\<^bold>g [^] a \<otimes> \<^bold>g [^] b) [^] (c * int d mod int (order G))
[PROOF STEP]
have "(\<^bold>g [^] (a::nat) \<otimes> \<^bold>g [^] (b::nat)) [^] ((c::int)*int (d::nat)) = (\<^bold>g [^] n) [^] r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<^bold>g [^] a \<otimes> \<^bold>g [^] b) [^] (c * int d) = (\<^bold>g [^] n) [^] r
[PROOF STEP]
using n r
[PROOF STATE]
proof (prove)
using this:
\<^bold>g [^] n = \<^bold>g [^] a \<otimes> \<^bold>g [^] b
r = c * int d

goal (1 subgoal):
 1. (\<^bold>g [^] a \<otimes> \<^bold>g [^] b) [^] (c * int d) = (\<^bold>g [^] n) [^] r
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<^bold>g [^] a \<otimes> \<^bold>g [^] b) [^] (c * int d) = (\<^bold>g [^] n) [^] r

goal (1 subgoal):
 1. (\<^bold>g [^] a \<otimes> \<^bold>g [^] b) [^] (c * int d) = (\<^bold>g [^] a \<otimes> \<^bold>g [^] b) [^] (c * int d mod int (order G))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(\<^bold>g [^] a \<otimes> \<^bold>g [^] b) [^] (c * int d) = (\<^bold>g [^] n) [^] r

goal (1 subgoal):
 1. (\<^bold>g [^] a \<otimes> \<^bold>g [^] b) [^] (c * int d) = (\<^bold>g [^] a \<otimes> \<^bold>g [^] b) [^] (c * int d mod int (order G))
[PROOF STEP]
have"... = (\<^bold>g [^] n) [^] (r mod (order G))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<^bold>g [^] n) [^] r = (\<^bold>g [^] n) [^] (r mod int (order G))
[PROOF STEP]
using pow_generator_mod_int pow_generator_mod
[PROOF STATE]
proof (prove)
using this:
\<^bold>g [^] (?k mod int (order G)) = \<^bold>g [^] ?k
\<^bold>g [^] (?k mod order G) = \<^bold>g [^] ?k

goal (1 subgoal):
 1. (\<^bold>g [^] n) [^] r = (\<^bold>g [^] n) [^] (r mod int (order G))
[PROOF STEP]
by (metis int_nat_pow int_pow_int mod_mult_right_eq zero_le)
[PROOF STATE]
proof (state)
this:
(\<^bold>g [^] n) [^] r = (\<^bold>g [^] n) [^] (r mod int (order G))

goal (1 subgoal):
 1. (\<^bold>g [^] a \<otimes> \<^bold>g [^] b) [^] (c * int d) = (\<^bold>g [^] a \<otimes> \<^bold>g [^] b) [^] (c * int d mod int (order G))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(\<^bold>g [^] n) [^] r = (\<^bold>g [^] n) [^] (r mod int (order G))

goal (1 subgoal):
 1. (\<^bold>g [^] a \<otimes> \<^bold>g [^] b) [^] (c * int d) = (\<^bold>g [^] a \<otimes> \<^bold>g [^] b) [^] (c * int d mod int (order G))
[PROOF STEP]
have "... =  (\<^bold>g [^] a \<otimes> \<^bold>g [^] b) [^] ((c*int d) mod (order G))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<^bold>g [^] n) [^] (r mod int (order G)) = (\<^bold>g [^] a \<otimes> \<^bold>g [^] b) [^] (c * int d mod int (order G))
[PROOF STEP]
using r n
[PROOF STATE]
proof (prove)
using this:
r = c * int d
\<^bold>g [^] n = \<^bold>g [^] a \<otimes> \<^bold>g [^] b

goal (1 subgoal):
 1. (\<^bold>g [^] n) [^] (r mod int (order G)) = (\<^bold>g [^] a \<otimes> \<^bold>g [^] b) [^] (c * int d mod int (order G))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<^bold>g [^] n) [^] (r mod int (order G)) = (\<^bold>g [^] a \<otimes> \<^bold>g [^] b) [^] (c * int d mod int (order G))

goal (1 subgoal):
 1. (\<^bold>g [^] a \<otimes> \<^bold>g [^] b) [^] (c * int d) = (\<^bold>g [^] a \<otimes> \<^bold>g [^] b) [^] (c * int d mod int (order G))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<^bold>g [^] n = \<^bold>g [^] a \<otimes> \<^bold>g [^] b
(\<^bold>g [^] a \<otimes> \<^bold>g [^] b) [^] (c * int d) = (\<^bold>g [^] n) [^] r
(\<^bold>g [^] n) [^] r = (\<^bold>g [^] n) [^] (r mod int (order G))
(\<^bold>g [^] n) [^] (r mod int (order G)) = (\<^bold>g [^] a \<otimes> \<^bold>g [^] b) [^] (c * int d mod int (order G))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<^bold>g [^] n = \<^bold>g [^] a \<otimes> \<^bold>g [^] b
(\<^bold>g [^] a \<otimes> \<^bold>g [^] b) [^] (c * int d) = (\<^bold>g [^] n) [^] r
(\<^bold>g [^] n) [^] r = (\<^bold>g [^] n) [^] (r mod int (order G))
(\<^bold>g [^] n) [^] (r mod int (order G)) = (\<^bold>g [^] a \<otimes> \<^bold>g [^] b) [^] (c * int d mod int (order G))

goal (1 subgoal):
 1. (\<^bold>g [^] a \<otimes> \<^bold>g [^] b) [^] (c * int d) = (\<^bold>g [^] a \<otimes> \<^bold>g [^] b) [^] (c * int d mod int (order G))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<^bold>g [^] a \<otimes> \<^bold>g [^] b) [^] (c * int d) = (\<^bold>g [^] a \<otimes> \<^bold>g [^] b) [^] (c * int d mod int (order G))

goal:
No subgoals!
[PROOF STEP]
qed