[STATEMENT]
theorem gt_trans: "u >\<^sub>t t \<Longrightarrow> t >\<^sub>t s \<Longrightarrow> u >\<^sub>t s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>u >\<^sub>t t; t >\<^sub>t s\<rbrakk> \<Longrightarrow> u >\<^sub>t s
[PROOF STEP]
proof (simp only: atomize_imp,
    rule measure_induct_rule[of "\<lambda>(u, t, s). {#size u, size t, size s#}"
        "\<lambda>(u, t, s). u >\<^sub>t t \<longrightarrow> t >\<^sub>t s \<longrightarrow> u >\<^sub>t s" "(u, t, s)",
      simplified prod.case],
    simp only: split_paired_all prod.case atomize_imp[symmetric])
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a aa b. \<lbrakk>\<And>ab ac ba. \<lbrakk>{#size ab, size ac, size ba#} < {#size a, size aa, size b#}; ab >\<^sub>t ac; ac >\<^sub>t ba\<rbrakk> \<Longrightarrow> ab >\<^sub>t ba; a >\<^sub>t aa; aa >\<^sub>t b\<rbrakk> \<Longrightarrow> a >\<^sub>t b
[PROOF STEP]
fix u t s
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a aa b. \<lbrakk>\<And>ab ac ba. \<lbrakk>{#size ab, size ac, size ba#} < {#size a, size aa, size b#}; ab >\<^sub>t ac; ac >\<^sub>t ba\<rbrakk> \<Longrightarrow> ab >\<^sub>t ba; a >\<^sub>t aa; aa >\<^sub>t b\<rbrakk> \<Longrightarrow> a >\<^sub>t b
[PROOF STEP]
assume
    ih: "\<And>ua ta sa. {#size ua, size ta, size sa#} < {#size u, size t, size s#} \<Longrightarrow>
      ua >\<^sub>t ta \<Longrightarrow> ta >\<^sub>t sa \<Longrightarrow> ua >\<^sub>t sa" and
    u_gt_t: "u >\<^sub>t t" and t_gt_s: "t >\<^sub>t s"
[PROOF STATE]
proof (state)
this:
\<lbrakk>{#size ?ua, size ?ta, size ?sa#} < {#size u, size t, size s#}; ?ua >\<^sub>t ?ta; ?ta >\<^sub>t ?sa\<rbrakk> \<Longrightarrow> ?ua >\<^sub>t ?sa
u >\<^sub>t t
t >\<^sub>t s

goal (1 subgoal):
 1. \<And>a aa b. \<lbrakk>\<And>ab ac ba. \<lbrakk>{#size ab, size ac, size ba#} < {#size a, size aa, size b#}; ab >\<^sub>t ac; ac >\<^sub>t ba\<rbrakk> \<Longrightarrow> ab >\<^sub>t ba; a >\<^sub>t aa; aa >\<^sub>t b\<rbrakk> \<Longrightarrow> a >\<^sub>t b
[PROOF STEP]
have chkvar: "chkvar u s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. chkvar u s
[PROOF STEP]
by clarsimp (meson u_gt_t t_gt_s gt_imp_vars hd.set_sel(2) vars_head_subseteq subsetCE)
[PROOF STATE]
proof (state)
this:
chkvar u s

goal (1 subgoal):
 1. \<And>a aa b. \<lbrakk>\<And>ab ac ba. \<lbrakk>{#size ab, size ac, size ba#} < {#size a, size aa, size b#}; ab >\<^sub>t ac; ac >\<^sub>t ba\<rbrakk> \<Longrightarrow> ab >\<^sub>t ba; a >\<^sub>t aa; aa >\<^sub>t b\<rbrakk> \<Longrightarrow> a >\<^sub>t b
[PROOF STEP]
have chk_u_s_if: "chksubs (>\<^sub>t) u s" if chk_t_s: "chksubs (>\<^sub>t) t s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. chksubs (>\<^sub>t) u s
[PROOF STEP]
proof (cases s)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x1. s = Hd x1 \<Longrightarrow> chksubs (>\<^sub>t) u s
 2. \<And>x21 x22. s = App x21 x22 \<Longrightarrow> chksubs (>\<^sub>t) u s
[PROOF STEP]
case (App s1 s2)
[PROOF STATE]
proof (state)
this:
s = App s1 s2

goal (2 subgoals):
 1. \<And>x1. s = Hd x1 \<Longrightarrow> chksubs (>\<^sub>t) u s
 2. \<And>x21 x22. s = App x21 x22 \<Longrightarrow> chksubs (>\<^sub>t) u s
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
s = App s1 s2

goal (1 subgoal):
 1. chksubs (>\<^sub>t) u s
[PROOF STEP]
using chk_t_s
[PROOF STATE]
proof (prove)
using this:
s = App s1 s2
chksubs (>\<^sub>t) t s

goal (1 subgoal):
 1. chksubs (>\<^sub>t) u s
[PROOF STEP]
by (auto intro: ih[of _ _ s1, OF _ u_gt_t] ih[of _ _ s2, OF _ u_gt_t])
[PROOF STATE]
proof (state)
this:
chksubs (>\<^sub>t) u s

goal (1 subgoal):
 1. \<And>x1. s = Hd x1 \<Longrightarrow> chksubs (>\<^sub>t) u s
[PROOF STEP]
qed auto
[PROOF STATE]
proof (state)
this:
chksubs (>\<^sub>t) t s \<Longrightarrow> chksubs (>\<^sub>t) u s

goal (1 subgoal):
 1. \<And>a aa b. \<lbrakk>\<And>ab ac ba. \<lbrakk>{#size ab, size ac, size ba#} < {#size a, size aa, size b#}; ab >\<^sub>t ac; ac >\<^sub>t ba\<rbrakk> \<Longrightarrow> ab >\<^sub>t ba; a >\<^sub>t aa; aa >\<^sub>t b\<rbrakk> \<Longrightarrow> a >\<^sub>t b
[PROOF STEP]
have
    fun_u_lt_etc: "is_App u \<Longrightarrow> {#size (fun u), size t, size s#} < {#size u, size t, size s#}" and
    arg_u_lt_etc: "is_App u \<Longrightarrow> {#size (arg u), size t, size s#} < {#size u, size t, size s#}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (is_App u \<Longrightarrow> {#size (fun u), size t, size s#} < {#size u, size t, size s#}) &&& (is_App u \<Longrightarrow> {#size (arg u), size t, size s#} < {#size u, size t, size s#})
[PROOF STEP]
by (simp_all add: size_fun_lt size_arg_lt)
[PROOF STATE]
proof (state)
this:
is_App u \<Longrightarrow> {#size (fun u), size t, size s#} < {#size u, size t, size s#}
is_App u \<Longrightarrow> {#size (arg u), size t, size s#} < {#size u, size t, size s#}

goal (1 subgoal):
 1. \<And>a aa b. \<lbrakk>\<And>ab ac ba. \<lbrakk>{#size ab, size ac, size ba#} < {#size a, size aa, size b#}; ab >\<^sub>t ac; ac >\<^sub>t ba\<rbrakk> \<Longrightarrow> ab >\<^sub>t ba; a >\<^sub>t aa; aa >\<^sub>t b\<rbrakk> \<Longrightarrow> a >\<^sub>t b
[PROOF STEP]
have u_gt_s_if_ui: "is_App u \<Longrightarrow> fun u \<ge>\<^sub>t t \<or> arg u \<ge>\<^sub>t t \<Longrightarrow> u >\<^sub>t s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_App u; fun u \<ge>\<^sub>t t \<or> arg u \<ge>\<^sub>t t\<rbrakk> \<Longrightarrow> u >\<^sub>t s
[PROOF STEP]
using ih[of "fun u" t s, OF fun_u_lt_etc] ih[of "arg u" t s, OF arg_u_lt_etc] gt_arg_imp
      gt_fun_imp t_gt_s
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>is_App u; fun u >\<^sub>t t; t >\<^sub>t s\<rbrakk> \<Longrightarrow> fun u >\<^sub>t s
\<lbrakk>is_App u; arg u >\<^sub>t t; t >\<^sub>t s\<rbrakk> \<Longrightarrow> arg u >\<^sub>t s
arg ?t >\<^sub>t ?s \<Longrightarrow> ?t >\<^sub>t ?s
fun ?t >\<^sub>t ?s \<Longrightarrow> ?t >\<^sub>t ?s
t >\<^sub>t s

goal (1 subgoal):
 1. \<lbrakk>is_App u; fun u \<ge>\<^sub>t t \<or> arg u \<ge>\<^sub>t t\<rbrakk> \<Longrightarrow> u >\<^sub>t s
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<lbrakk>is_App u; fun u \<ge>\<^sub>t t \<or> arg u \<ge>\<^sub>t t\<rbrakk> \<Longrightarrow> u >\<^sub>t s

goal (1 subgoal):
 1. \<And>a aa b. \<lbrakk>\<And>ab ac ba. \<lbrakk>{#size ab, size ac, size ba#} < {#size a, size aa, size b#}; ab >\<^sub>t ac; ac >\<^sub>t ba\<rbrakk> \<Longrightarrow> ab >\<^sub>t ba; a >\<^sub>t aa; aa >\<^sub>t b\<rbrakk> \<Longrightarrow> a >\<^sub>t b
[PROOF STEP]
show "u >\<^sub>t s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. u >\<^sub>t s
[PROOF STEP]
using t_gt_s
[PROOF STATE]
proof (prove)
using this:
t >\<^sub>t s

goal (1 subgoal):
 1. u >\<^sub>t s
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<lbrakk>is_App t; fun t \<ge>\<^sub>t s \<or> arg t \<ge>\<^sub>t s\<rbrakk> \<Longrightarrow> u >\<^sub>t s
 2. \<lbrakk>head t >\<^sub>h\<^sub>d head s; chkvar t s; chksubs (>\<^sub>t) t s\<rbrakk> \<Longrightarrow> u >\<^sub>t s
 3. \<lbrakk>head t = head s; chksubs (>\<^sub>t) t s; \<forall>f\<in>local.ground_heads (head t). extf f (>\<^sub>t) (args t) (args s)\<rbrakk> \<Longrightarrow> u >\<^sub>t s
[PROOF STEP]
case gt_sub_t_s: gt_sub
[PROOF STATE]
proof (state)
this:
is_App t
fun t \<ge>\<^sub>t s \<or> arg t \<ge>\<^sub>t s

goal (3 subgoals):
 1. \<lbrakk>is_App t; fun t \<ge>\<^sub>t s \<or> arg t \<ge>\<^sub>t s\<rbrakk> \<Longrightarrow> u >\<^sub>t s
 2. \<lbrakk>head t >\<^sub>h\<^sub>d head s; chkvar t s; chksubs (>\<^sub>t) t s\<rbrakk> \<Longrightarrow> u >\<^sub>t s
 3. \<lbrakk>head t = head s; chksubs (>\<^sub>t) t s; \<forall>f\<in>local.ground_heads (head t). extf f (>\<^sub>t) (args t) (args s)\<rbrakk> \<Longrightarrow> u >\<^sub>t s
[PROOF STEP]
have u_gt_s_if_chk_u_t: ?thesis if chk_u_t: "chksubs (>\<^sub>t) u t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. u >\<^sub>t s
[PROOF STEP]
using gt_sub_t_s(1)
[PROOF STATE]
proof (prove)
using this:
is_App t

goal (1 subgoal):
 1. u >\<^sub>t s
[PROOF STEP]
proof (cases t)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x1. \<lbrakk>is_App t; t = Hd x1\<rbrakk> \<Longrightarrow> u >\<^sub>t s
 2. \<And>x21 x22. \<lbrakk>is_App t; t = App x21 x22\<rbrakk> \<Longrightarrow> u >\<^sub>t s
[PROOF STEP]
case t: (App t1 t2)
[PROOF STATE]
proof (state)
this:
t = App t1 t2

goal (2 subgoals):
 1. \<And>x1. \<lbrakk>is_App t; t = Hd x1\<rbrakk> \<Longrightarrow> u >\<^sub>t s
 2. \<And>x21 x22. \<lbrakk>is_App t; t = App x21 x22\<rbrakk> \<Longrightarrow> u >\<^sub>t s
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. u >\<^sub>t s
[PROOF STEP]
using ih[of u t1 s] ih[of u t2 s] gt_sub_t_s(2) chk_u_t
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>{#size u, size t1, size s#} < {#size u, size t, size s#}; u >\<^sub>t t1; t1 >\<^sub>t s\<rbrakk> \<Longrightarrow> u >\<^sub>t s
\<lbrakk>{#size u, size t2, size s#} < {#size u, size t, size s#}; u >\<^sub>t t2; t2 >\<^sub>t s\<rbrakk> \<Longrightarrow> u >\<^sub>t s
fun t \<ge>\<^sub>t s \<or> arg t \<ge>\<^sub>t s
chksubs (>\<^sub>t) u t

goal (1 subgoal):
 1. u >\<^sub>t s
[PROOF STEP]
unfolding t
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>{#size u, size t1, size s#} < {#size u, size (App t1 t2), size s#}; u >\<^sub>t t1; t1 >\<^sub>t s\<rbrakk> \<Longrightarrow> u >\<^sub>t s
\<lbrakk>{#size u, size t2, size s#} < {#size u, size (App t1 t2), size s#}; u >\<^sub>t t2; t2 >\<^sub>t s\<rbrakk> \<Longrightarrow> u >\<^sub>t s
fun (App t1 t2) \<ge>\<^sub>t s \<or> arg (App t1 t2) \<ge>\<^sub>t s
chksubs (>\<^sub>t) u (App t1 t2)

goal (1 subgoal):
 1. u >\<^sub>t s
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
u >\<^sub>t s

goal (1 subgoal):
 1. \<And>x1. \<lbrakk>is_App t; t = Hd x1\<rbrakk> \<Longrightarrow> u >\<^sub>t s
[PROOF STEP]
qed auto
[PROOF STATE]
proof (state)
this:
chksubs (>\<^sub>t) u t \<Longrightarrow> u >\<^sub>t s

goal (3 subgoals):
 1. \<lbrakk>is_App t; fun t \<ge>\<^sub>t s \<or> arg t \<ge>\<^sub>t s\<rbrakk> \<Longrightarrow> u >\<^sub>t s
 2. \<lbrakk>head t >\<^sub>h\<^sub>d head s; chkvar t s; chksubs (>\<^sub>t) t s\<rbrakk> \<Longrightarrow> u >\<^sub>t s
 3. \<lbrakk>head t = head s; chksubs (>\<^sub>t) t s; \<forall>f\<in>local.ground_heads (head t). extf f (>\<^sub>t) (args t) (args s)\<rbrakk> \<Longrightarrow> u >\<^sub>t s
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. u >\<^sub>t s
[PROOF STEP]
using u_gt_t
[PROOF STATE]
proof (prove)
using this:
u >\<^sub>t t

goal (1 subgoal):
 1. u >\<^sub>t s
[PROOF STEP]
by cases (auto intro: u_gt_s_if_ui u_gt_s_if_chk_u_t)
[PROOF STATE]
proof (state)
this:
u >\<^sub>t s

goal (2 subgoals):
 1. \<lbrakk>head t >\<^sub>h\<^sub>d head s; chkvar t s; chksubs (>\<^sub>t) t s\<rbrakk> \<Longrightarrow> u >\<^sub>t s
 2. \<lbrakk>head t = head s; chksubs (>\<^sub>t) t s; \<forall>f\<in>local.ground_heads (head t). extf f (>\<^sub>t) (args t) (args s)\<rbrakk> \<Longrightarrow> u >\<^sub>t s
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>head t >\<^sub>h\<^sub>d head s; chkvar t s; chksubs (>\<^sub>t) t s\<rbrakk> \<Longrightarrow> u >\<^sub>t s
 2. \<lbrakk>head t = head s; chksubs (>\<^sub>t) t s; \<forall>f\<in>local.ground_heads (head t). extf f (>\<^sub>t) (args t) (args s)\<rbrakk> \<Longrightarrow> u >\<^sub>t s
[PROOF STEP]
case gt_diff_t_s: gt_diff
[PROOF STATE]
proof (state)
this:
head t >\<^sub>h\<^sub>d head s
chkvar t s
chksubs (>\<^sub>t) t s

goal (2 subgoals):
 1. \<lbrakk>head t >\<^sub>h\<^sub>d head s; chkvar t s; chksubs (>\<^sub>t) t s\<rbrakk> \<Longrightarrow> u >\<^sub>t s
 2. \<lbrakk>head t = head s; chksubs (>\<^sub>t) t s; \<forall>f\<in>local.ground_heads (head t). extf f (>\<^sub>t) (args t) (args s)\<rbrakk> \<Longrightarrow> u >\<^sub>t s
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. u >\<^sub>t s
[PROOF STEP]
using u_gt_t
[PROOF STATE]
proof (prove)
using this:
u >\<^sub>t t

goal (1 subgoal):
 1. u >\<^sub>t s
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<lbrakk>is_App u; fun u \<ge>\<^sub>t t \<or> arg u \<ge>\<^sub>t t\<rbrakk> \<Longrightarrow> u >\<^sub>t s
 2. \<lbrakk>head u >\<^sub>h\<^sub>d head t; chkvar u t; chksubs (>\<^sub>t) u t\<rbrakk> \<Longrightarrow> u >\<^sub>t s
 3. \<lbrakk>head u = head t; chksubs (>\<^sub>t) u t; \<forall>f\<in>local.ground_heads (head u). extf f (>\<^sub>t) (args u) (args t)\<rbrakk> \<Longrightarrow> u >\<^sub>t s
[PROOF STEP]
case gt_diff_u_t: gt_diff
[PROOF STATE]
proof (state)
this:
head u >\<^sub>h\<^sub>d head t
chkvar u t
chksubs (>\<^sub>t) u t

goal (3 subgoals):
 1. \<lbrakk>is_App u; fun u \<ge>\<^sub>t t \<or> arg u \<ge>\<^sub>t t\<rbrakk> \<Longrightarrow> u >\<^sub>t s
 2. \<lbrakk>head u >\<^sub>h\<^sub>d head t; chkvar u t; chksubs (>\<^sub>t) u t\<rbrakk> \<Longrightarrow> u >\<^sub>t s
 3. \<lbrakk>head u = head t; chksubs (>\<^sub>t) u t; \<forall>f\<in>local.ground_heads (head u). extf f (>\<^sub>t) (args u) (args t)\<rbrakk> \<Longrightarrow> u >\<^sub>t s
[PROOF STEP]
have "head u >\<^sub>h\<^sub>d head s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. head u >\<^sub>h\<^sub>d head s
[PROOF STEP]
using gt_diff_u_t(1) gt_diff_t_s(1)
[PROOF STATE]
proof (prove)
using this:
head u >\<^sub>h\<^sub>d head t
head t >\<^sub>h\<^sub>d head s

goal (1 subgoal):
 1. head u >\<^sub>h\<^sub>d head s
[PROOF STEP]
by (auto intro: gt_hd_trans)
[PROOF STATE]
proof (state)
this:
head u >\<^sub>h\<^sub>d head s

goal (3 subgoals):
 1. \<lbrakk>is_App u; fun u \<ge>\<^sub>t t \<or> arg u \<ge>\<^sub>t t\<rbrakk> \<Longrightarrow> u >\<^sub>t s
 2. \<lbrakk>head u >\<^sub>h\<^sub>d head t; chkvar u t; chksubs (>\<^sub>t) u t\<rbrakk> \<Longrightarrow> u >\<^sub>t s
 3. \<lbrakk>head u = head t; chksubs (>\<^sub>t) u t; \<forall>f\<in>local.ground_heads (head u). extf f (>\<^sub>t) (args u) (args t)\<rbrakk> \<Longrightarrow> u >\<^sub>t s
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
head u >\<^sub>h\<^sub>d head s

goal (1 subgoal):
 1. u >\<^sub>t s
[PROOF STEP]
by (rule gt_diff[OF _ chkvar chk_u_s_if[OF gt_diff_t_s(3)]])
[PROOF STATE]
proof (state)
this:
u >\<^sub>t s

goal (2 subgoals):
 1. \<lbrakk>is_App u; fun u \<ge>\<^sub>t t \<or> arg u \<ge>\<^sub>t t\<rbrakk> \<Longrightarrow> u >\<^sub>t s
 2. \<lbrakk>head u = head t; chksubs (>\<^sub>t) u t; \<forall>f\<in>local.ground_heads (head u). extf f (>\<^sub>t) (args u) (args t)\<rbrakk> \<Longrightarrow> u >\<^sub>t s
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>is_App u; fun u \<ge>\<^sub>t t \<or> arg u \<ge>\<^sub>t t\<rbrakk> \<Longrightarrow> u >\<^sub>t s
 2. \<lbrakk>head u = head t; chksubs (>\<^sub>t) u t; \<forall>f\<in>local.ground_heads (head u). extf f (>\<^sub>t) (args u) (args t)\<rbrakk> \<Longrightarrow> u >\<^sub>t s
[PROOF STEP]
case gt_same_u_t: gt_same
[PROOF STATE]
proof (state)
this:
head u = head t
chksubs (>\<^sub>t) u t
\<forall>f\<in>local.ground_heads (head u). extf f (>\<^sub>t) (args u) (args t)

goal (2 subgoals):
 1. \<lbrakk>is_App u; fun u \<ge>\<^sub>t t \<or> arg u \<ge>\<^sub>t t\<rbrakk> \<Longrightarrow> u >\<^sub>t s
 2. \<lbrakk>head u = head t; chksubs (>\<^sub>t) u t; \<forall>f\<in>local.ground_heads (head u). extf f (>\<^sub>t) (args u) (args t)\<rbrakk> \<Longrightarrow> u >\<^sub>t s
[PROOF STEP]
have "head u >\<^sub>h\<^sub>d head s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. head u >\<^sub>h\<^sub>d head s
[PROOF STEP]
using gt_diff_t_s(1) gt_same_u_t(1)
[PROOF STATE]
proof (prove)
using this:
head t >\<^sub>h\<^sub>d head s
head u = head t

goal (1 subgoal):
 1. head u >\<^sub>h\<^sub>d head s
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
head u >\<^sub>h\<^sub>d head s

goal (2 subgoals):
 1. \<lbrakk>is_App u; fun u \<ge>\<^sub>t t \<or> arg u \<ge>\<^sub>t t\<rbrakk> \<Longrightarrow> u >\<^sub>t s
 2. \<lbrakk>head u = head t; chksubs (>\<^sub>t) u t; \<forall>f\<in>local.ground_heads (head u). extf f (>\<^sub>t) (args u) (args t)\<rbrakk> \<Longrightarrow> u >\<^sub>t s
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
head u >\<^sub>h\<^sub>d head s

goal (1 subgoal):
 1. u >\<^sub>t s
[PROOF STEP]
by (rule gt_diff[OF _ chkvar chk_u_s_if[OF gt_diff_t_s(3)]])
[PROOF STATE]
proof (state)
this:
u >\<^sub>t s

goal (1 subgoal):
 1. \<lbrakk>is_App u; fun u \<ge>\<^sub>t t \<or> arg u \<ge>\<^sub>t t\<rbrakk> \<Longrightarrow> u >\<^sub>t s
[PROOF STEP]
qed (auto intro: u_gt_s_if_ui)
[PROOF STATE]
proof (state)
this:
u >\<^sub>t s

goal (1 subgoal):
 1. \<lbrakk>head t = head s; chksubs (>\<^sub>t) t s; \<forall>f\<in>local.ground_heads (head t). extf f (>\<^sub>t) (args t) (args s)\<rbrakk> \<Longrightarrow> u >\<^sub>t s
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>head t = head s; chksubs (>\<^sub>t) t s; \<forall>f\<in>local.ground_heads (head t). extf f (>\<^sub>t) (args t) (args s)\<rbrakk> \<Longrightarrow> u >\<^sub>t s
[PROOF STEP]
case gt_same_t_s: gt_same
[PROOF STATE]
proof (state)
this:
head t = head s
chksubs (>\<^sub>t) t s
\<forall>f\<in>local.ground_heads (head t). extf f (>\<^sub>t) (args t) (args s)

goal (1 subgoal):
 1. \<lbrakk>head t = head s; chksubs (>\<^sub>t) t s; \<forall>f\<in>local.ground_heads (head t). extf f (>\<^sub>t) (args t) (args s)\<rbrakk> \<Longrightarrow> u >\<^sub>t s
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. u >\<^sub>t s
[PROOF STEP]
using u_gt_t
[PROOF STATE]
proof (prove)
using this:
u >\<^sub>t t

goal (1 subgoal):
 1. u >\<^sub>t s
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<lbrakk>is_App u; fun u \<ge>\<^sub>t t \<or> arg u \<ge>\<^sub>t t\<rbrakk> \<Longrightarrow> u >\<^sub>t s
 2. \<lbrakk>head u >\<^sub>h\<^sub>d head t; chkvar u t; chksubs (>\<^sub>t) u t\<rbrakk> \<Longrightarrow> u >\<^sub>t s
 3. \<lbrakk>head u = head t; chksubs (>\<^sub>t) u t; \<forall>f\<in>local.ground_heads (head u). extf f (>\<^sub>t) (args u) (args t)\<rbrakk> \<Longrightarrow> u >\<^sub>t s
[PROOF STEP]
case gt_diff_u_t: gt_diff
[PROOF STATE]
proof (state)
this:
head u >\<^sub>h\<^sub>d head t
chkvar u t
chksubs (>\<^sub>t) u t

goal (3 subgoals):
 1. \<lbrakk>is_App u; fun u \<ge>\<^sub>t t \<or> arg u \<ge>\<^sub>t t\<rbrakk> \<Longrightarrow> u >\<^sub>t s
 2. \<lbrakk>head u >\<^sub>h\<^sub>d head t; chkvar u t; chksubs (>\<^sub>t) u t\<rbrakk> \<Longrightarrow> u >\<^sub>t s
 3. \<lbrakk>head u = head t; chksubs (>\<^sub>t) u t; \<forall>f\<in>local.ground_heads (head u). extf f (>\<^sub>t) (args u) (args t)\<rbrakk> \<Longrightarrow> u >\<^sub>t s
[PROOF STEP]
have "head u >\<^sub>h\<^sub>d head s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. head u >\<^sub>h\<^sub>d head s
[PROOF STEP]
using gt_diff_u_t(1) gt_same_t_s(1)
[PROOF STATE]
proof (prove)
using this:
head u >\<^sub>h\<^sub>d head t
head t = head s

goal (1 subgoal):
 1. head u >\<^sub>h\<^sub>d head s
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
head u >\<^sub>h\<^sub>d head s

goal (3 subgoals):
 1. \<lbrakk>is_App u; fun u \<ge>\<^sub>t t \<or> arg u \<ge>\<^sub>t t\<rbrakk> \<Longrightarrow> u >\<^sub>t s
 2. \<lbrakk>head u >\<^sub>h\<^sub>d head t; chkvar u t; chksubs (>\<^sub>t) u t\<rbrakk> \<Longrightarrow> u >\<^sub>t s
 3. \<lbrakk>head u = head t; chksubs (>\<^sub>t) u t; \<forall>f\<in>local.ground_heads (head u). extf f (>\<^sub>t) (args u) (args t)\<rbrakk> \<Longrightarrow> u >\<^sub>t s
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
head u >\<^sub>h\<^sub>d head s

goal (1 subgoal):
 1. u >\<^sub>t s
[PROOF STEP]
by (rule gt_diff[OF _ chkvar chk_u_s_if[OF gt_same_t_s(2)]])
[PROOF STATE]
proof (state)
this:
u >\<^sub>t s

goal (2 subgoals):
 1. \<lbrakk>is_App u; fun u \<ge>\<^sub>t t \<or> arg u \<ge>\<^sub>t t\<rbrakk> \<Longrightarrow> u >\<^sub>t s
 2. \<lbrakk>head u = head t; chksubs (>\<^sub>t) u t; \<forall>f\<in>local.ground_heads (head u). extf f (>\<^sub>t) (args u) (args t)\<rbrakk> \<Longrightarrow> u >\<^sub>t s
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>is_App u; fun u \<ge>\<^sub>t t \<or> arg u \<ge>\<^sub>t t\<rbrakk> \<Longrightarrow> u >\<^sub>t s
 2. \<lbrakk>head u = head t; chksubs (>\<^sub>t) u t; \<forall>f\<in>local.ground_heads (head u). extf f (>\<^sub>t) (args u) (args t)\<rbrakk> \<Longrightarrow> u >\<^sub>t s
[PROOF STEP]
case gt_same_u_t: gt_same
[PROOF STATE]
proof (state)
this:
head u = head t
chksubs (>\<^sub>t) u t
\<forall>f\<in>local.ground_heads (head u). extf f (>\<^sub>t) (args u) (args t)

goal (2 subgoals):
 1. \<lbrakk>is_App u; fun u \<ge>\<^sub>t t \<or> arg u \<ge>\<^sub>t t\<rbrakk> \<Longrightarrow> u >\<^sub>t s
 2. \<lbrakk>head u = head t; chksubs (>\<^sub>t) u t; \<forall>f\<in>local.ground_heads (head u). extf f (>\<^sub>t) (args u) (args t)\<rbrakk> \<Longrightarrow> u >\<^sub>t s
[PROOF STEP]
have hd_u_s: "head u = head s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. head u = head s
[PROOF STEP]
using gt_same_u_t(1) gt_same_t_s(1)
[PROOF STATE]
proof (prove)
using this:
head u = head t
head t = head s

goal (1 subgoal):
 1. head u = head s
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
head u = head s

goal (2 subgoals):
 1. \<lbrakk>is_App u; fun u \<ge>\<^sub>t t \<or> arg u \<ge>\<^sub>t t\<rbrakk> \<Longrightarrow> u >\<^sub>t s
 2. \<lbrakk>head u = head t; chksubs (>\<^sub>t) u t; \<forall>f\<in>local.ground_heads (head u). extf f (>\<^sub>t) (args u) (args t)\<rbrakk> \<Longrightarrow> u >\<^sub>t s
[PROOF STEP]
let ?S = "set (args u) \<union> set (args t) \<union> set (args s)"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>is_App u; fun u \<ge>\<^sub>t t \<or> arg u \<ge>\<^sub>t t\<rbrakk> \<Longrightarrow> u >\<^sub>t s
 2. \<lbrakk>head u = head t; chksubs (>\<^sub>t) u t; \<forall>f\<in>local.ground_heads (head u). extf f (>\<^sub>t) (args u) (args t)\<rbrakk> \<Longrightarrow> u >\<^sub>t s
[PROOF STEP]
have gt_trans_args: "\<forall>ua \<in> ?S. \<forall>ta \<in> ?S. \<forall>sa \<in> ?S. ua >\<^sub>t ta \<longrightarrow> ta >\<^sub>t sa \<longrightarrow> ua >\<^sub>t sa"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>uaa\<in>set (args u) \<union> set (args t) \<union> set (args s). \<forall>taa\<in>set (args u) \<union> set (args t) \<union> set (args s). \<forall>sa\<in>set (args u) \<union> set (args t) \<union> set (args s). uaa >\<^sub>t taa \<longrightarrow> taa >\<^sub>t sa \<longrightarrow> uaa >\<^sub>t sa
[PROOF STEP]
proof clarify
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>uaa taa saa. \<lbrakk>uaa \<in> set (args u) \<union> set (args t) \<union> set (args s); taa \<in> set (args u) \<union> set (args t) \<union> set (args s); saa \<in> set (args u) \<union> set (args t) \<union> set (args s); uaa >\<^sub>t taa; taa >\<^sub>t saa\<rbrakk> \<Longrightarrow> uaa >\<^sub>t saa
[PROOF STEP]
fix sa ta ua
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>uaa taa saa. \<lbrakk>uaa \<in> set (args u) \<union> set (args t) \<union> set (args s); taa \<in> set (args u) \<union> set (args t) \<union> set (args s); saa \<in> set (args u) \<union> set (args t) \<union> set (args s); uaa >\<^sub>t taa; taa >\<^sub>t saa\<rbrakk> \<Longrightarrow> uaa >\<^sub>t saa
[PROOF STEP]
assume
          ua_in: "ua \<in> ?S" and ta_in: "ta \<in> ?S" and sa_in: "sa \<in> ?S" and
          ua_gt_ta: "ua >\<^sub>t ta" and ta_gt_sa: "ta >\<^sub>t sa"
[PROOF STATE]
proof (state)
this:
ua \<in> set (args u) \<union> set (args t) \<union> set (args s)
ta \<in> set (args u) \<union> set (args t) \<union> set (args s)
sa \<in> set (args u) \<union> set (args t) \<union> set (args s)
ua >\<^sub>t ta
ta >\<^sub>t sa

goal (1 subgoal):
 1. \<And>uaa taa saa. \<lbrakk>uaa \<in> set (args u) \<union> set (args t) \<union> set (args s); taa \<in> set (args u) \<union> set (args t) \<union> set (args s); saa \<in> set (args u) \<union> set (args t) \<union> set (args s); uaa >\<^sub>t taa; taa >\<^sub>t saa\<rbrakk> \<Longrightarrow> uaa >\<^sub>t saa
[PROOF STEP]
show "ua >\<^sub>t sa"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ua >\<^sub>t sa
[PROOF STEP]
by (auto intro!: ih[OF Max_lt_imp_lt_mset ua_gt_ta ta_gt_sa])
            (meson ua_in ta_in sa_in Un_iff max.strict_coboundedI1 max.strict_coboundedI2
               size_in_args)+
[PROOF STATE]
proof (state)
this:
ua >\<^sub>t sa

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>uaa\<in>set (args u) \<union> set (args t) \<union> set (args s). \<forall>taa\<in>set (args u) \<union> set (args t) \<union> set (args s). \<forall>sa\<in>set (args u) \<union> set (args t) \<union> set (args s). uaa >\<^sub>t taa \<longrightarrow> taa >\<^sub>t sa \<longrightarrow> uaa >\<^sub>t sa

goal (2 subgoals):
 1. \<lbrakk>is_App u; fun u \<ge>\<^sub>t t \<or> arg u \<ge>\<^sub>t t\<rbrakk> \<Longrightarrow> u >\<^sub>t s
 2. \<lbrakk>head u = head t; chksubs (>\<^sub>t) u t; \<forall>f\<in>local.ground_heads (head u). extf f (>\<^sub>t) (args u) (args t)\<rbrakk> \<Longrightarrow> u >\<^sub>t s
[PROOF STEP]
have "\<forall>f \<in> ground_heads (head u). extf f (>\<^sub>t) (args u) (args s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>f\<in>local.ground_heads (head u). extf f (>\<^sub>t) (args u) (args s)
[PROOF STEP]
proof (clarify, rule extf_trans[OF _ _ _ gt_trans_args])
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>f. f \<in> local.ground_heads (head u) \<Longrightarrow> args u \<in> lists (set (args u) \<union> set (args t) \<union> set (args s))
 2. \<And>f. f \<in> local.ground_heads (head u) \<Longrightarrow> ?ys1 f \<in> lists (set (args u) \<union> set (args t) \<union> set (args s))
 3. \<And>f. f \<in> local.ground_heads (head u) \<Longrightarrow> args s \<in> lists (set (args u) \<union> set (args t) \<union> set (args s))
 4. \<And>f. f \<in> local.ground_heads (head u) \<Longrightarrow> extf f (>\<^sub>t) (args u) (?ys1 f)
 5. \<And>f. f \<in> local.ground_heads (head u) \<Longrightarrow> extf f (>\<^sub>t) (?ys1 f) (args s)
[PROOF STEP]
fix f
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>f. f \<in> local.ground_heads (head u) \<Longrightarrow> args u \<in> lists (set (args u) \<union> set (args t) \<union> set (args s))
 2. \<And>f. f \<in> local.ground_heads (head u) \<Longrightarrow> ?ys1 f \<in> lists (set (args u) \<union> set (args t) \<union> set (args s))
 3. \<And>f. f \<in> local.ground_heads (head u) \<Longrightarrow> args s \<in> lists (set (args u) \<union> set (args t) \<union> set (args s))
 4. \<And>f. f \<in> local.ground_heads (head u) \<Longrightarrow> extf f (>\<^sub>t) (args u) (?ys1 f)
 5. \<And>f. f \<in> local.ground_heads (head u) \<Longrightarrow> extf f (>\<^sub>t) (?ys1 f) (args s)
[PROOF STEP]
assume f_in_grounds: "f \<in> ground_heads (head u)"
[PROOF STATE]
proof (state)
this:
f \<in> local.ground_heads (head u)

goal (5 subgoals):
 1. \<And>f. f \<in> local.ground_heads (head u) \<Longrightarrow> args u \<in> lists (set (args u) \<union> set (args t) \<union> set (args s))
 2. \<And>f. f \<in> local.ground_heads (head u) \<Longrightarrow> ?ys1 f \<in> lists (set (args u) \<union> set (args t) \<union> set (args s))
 3. \<And>f. f \<in> local.ground_heads (head u) \<Longrightarrow> args s \<in> lists (set (args u) \<union> set (args t) \<union> set (args s))
 4. \<And>f. f \<in> local.ground_heads (head u) \<Longrightarrow> extf f (>\<^sub>t) (args u) (?ys1 f)
 5. \<And>f. f \<in> local.ground_heads (head u) \<Longrightarrow> extf f (>\<^sub>t) (?ys1 f) (args s)
[PROOF STEP]
show "extf f (>\<^sub>t) (args u) (args t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. extf f (>\<^sub>t) (args u) (args t)
[PROOF STEP]
using f_in_grounds gt_same_u_t(3)
[PROOF STATE]
proof (prove)
using this:
f \<in> local.ground_heads (head u)
\<forall>f\<in>local.ground_heads (head u). extf f (>\<^sub>t) (args u) (args t)

goal (1 subgoal):
 1. extf f (>\<^sub>t) (args u) (args t)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
extf f (>\<^sub>t) (args u) (args t)

goal (4 subgoals):
 1. \<And>f. f \<in> local.ground_heads (head u) \<Longrightarrow> args u \<in> lists (set (args u) \<union> set (args t) \<union> set (args s))
 2. \<And>f. f \<in> local.ground_heads (head u) \<Longrightarrow> args t \<in> lists (set (args u) \<union> set (args t) \<union> set (args s))
 3. \<And>f. f \<in> local.ground_heads (head u) \<Longrightarrow> args s \<in> lists (set (args u) \<union> set (args t) \<union> set (args s))
 4. \<And>f. f \<in> local.ground_heads (head u) \<Longrightarrow> extf f (>\<^sub>t) (args t) (args s)
[PROOF STEP]
show "extf f (>\<^sub>t) (args t) (args s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. extf f (>\<^sub>t) (args t) (args s)
[PROOF STEP]
using f_in_grounds gt_same_t_s(3)
[PROOF STATE]
proof (prove)
using this:
f \<in> local.ground_heads (head u)
\<forall>f\<in>local.ground_heads (head t). extf f (>\<^sub>t) (args t) (args s)

goal (1 subgoal):
 1. extf f (>\<^sub>t) (args t) (args s)
[PROOF STEP]
unfolding gt_same_u_t(1)
[PROOF STATE]
proof (prove)
using this:
f \<in> local.ground_heads (head t)
\<forall>f\<in>local.ground_heads (head t). extf f (>\<^sub>t) (args t) (args s)

goal (1 subgoal):
 1. extf f (>\<^sub>t) (args t) (args s)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
extf f (>\<^sub>t) (args t) (args s)

goal (3 subgoals):
 1. \<And>f. f \<in> local.ground_heads (head u) \<Longrightarrow> args u \<in> lists (set (args u) \<union> set (args t) \<union> set (args s))
 2. \<And>f. f \<in> local.ground_heads (head u) \<Longrightarrow> args t \<in> lists (set (args u) \<union> set (args t) \<union> set (args s))
 3. \<And>f. f \<in> local.ground_heads (head u) \<Longrightarrow> args s \<in> lists (set (args u) \<union> set (args t) \<union> set (args s))
[PROOF STEP]
qed auto
[PROOF STATE]
proof (state)
this:
\<forall>f\<in>local.ground_heads (head u). extf f (>\<^sub>t) (args u) (args s)

goal (2 subgoals):
 1. \<lbrakk>is_App u; fun u \<ge>\<^sub>t t \<or> arg u \<ge>\<^sub>t t\<rbrakk> \<Longrightarrow> u >\<^sub>t s
 2. \<lbrakk>head u = head t; chksubs (>\<^sub>t) u t; \<forall>f\<in>local.ground_heads (head u). extf f (>\<^sub>t) (args u) (args t)\<rbrakk> \<Longrightarrow> u >\<^sub>t s
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>f\<in>local.ground_heads (head u). extf f (>\<^sub>t) (args u) (args s)

goal (1 subgoal):
 1. u >\<^sub>t s
[PROOF STEP]
by (rule gt_same[OF hd_u_s chk_u_s_if[OF gt_same_t_s(2)]])
[PROOF STATE]
proof (state)
this:
u >\<^sub>t s

goal (1 subgoal):
 1. \<lbrakk>is_App u; fun u \<ge>\<^sub>t t \<or> arg u \<ge>\<^sub>t t\<rbrakk> \<Longrightarrow> u >\<^sub>t s
[PROOF STEP]
qed (auto intro: u_gt_s_if_ui)
[PROOF STATE]
proof (state)
this:
u >\<^sub>t s

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
u >\<^sub>t s

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma nth_least_list_card[simp]:
    assumes "enat n \<le> esize A"
    shows "card {k \<in> A. k < nth_least (lift A) n} = n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card {k \<in> A. k < nth_least (lift A) n} = n
[PROOF STEP]
using less_Suc_eq_le assms
[PROOF STATE]
proof (prove)
using this:
(?m < Suc ?n) = (?m \<le> ?n)
enat n \<le> esize A

goal (1 subgoal):
 1. card {k \<in> A. k < nth_least (lift A) n} = n
[PROOF STEP]
by (cases n, auto simp del: nth_least.simps)


[STATEMENT]
lemma induced_pow_fun_surj:
  "((`) f) ` (Pow A) = Pow (f`A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (`) f ` Pow A = Pow (f ` A)
[PROOF STEP]
proof (rule seteqI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. x \<in> (`) f ` Pow A \<Longrightarrow> x \<in> Pow (f ` A)
 2. \<And>x. x \<in> Pow (f ` A) \<Longrightarrow> x \<in> (`) f ` Pow A
[PROOF STEP]
fix X
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. x \<in> (`) f ` Pow A \<Longrightarrow> x \<in> Pow (f ` A)
 2. \<And>x. x \<in> Pow (f ` A) \<Longrightarrow> x \<in> (`) f ` Pow A
[PROOF STEP]
show "X \<in> ((`) f) ` (Pow A) \<Longrightarrow> X \<in> Pow (f`A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. X \<in> (`) f ` Pow A \<Longrightarrow> X \<in> Pow (f ` A)
[PROOF STEP]
by fast
[PROOF STATE]
proof (state)
this:
X \<in> (`) f ` Pow A \<Longrightarrow> X \<in> Pow (f ` A)

goal (1 subgoal):
 1. \<And>x. x \<in> Pow (f ` A) \<Longrightarrow> x \<in> (`) f ` Pow A
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> Pow (f ` A) \<Longrightarrow> x \<in> (`) f ` Pow A
[PROOF STEP]
fix Y
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> Pow (f ` A) \<Longrightarrow> x \<in> (`) f ` Pow A
[PROOF STEP]
assume Y: "Y \<in> Pow (f`A)"
[PROOF STATE]
proof (state)
this:
Y \<in> Pow (f ` A)

goal (1 subgoal):
 1. \<And>x. x \<in> Pow (f ` A) \<Longrightarrow> x \<in> (`) f ` Pow A
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
Y \<in> Pow (f ` A)

goal (1 subgoal):
 1. \<And>x. x \<in> Pow (f ` A) \<Longrightarrow> x \<in> (`) f ` Pow A
[PROOF STEP]
hence "Y = f`{a\<in>A. f a \<in> Y}"
[PROOF STATE]
proof (prove)
using this:
Y \<in> Pow (f ` A)

goal (1 subgoal):
 1. Y = f ` {a \<in> A. f a \<in> Y}
[PROOF STEP]
by fast
[PROOF STATE]
proof (state)
this:
Y = f ` {a \<in> A. f a \<in> Y}

goal (1 subgoal):
 1. \<And>x. x \<in> Pow (f ` A) \<Longrightarrow> x \<in> (`) f ` Pow A
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
Y \<in> Pow (f ` A)
Y = f ` {a \<in> A. f a \<in> Y}
[PROOF STEP]
show "Y\<in> ((`) f) ` (Pow A)"
[PROOF STATE]
proof (prove)
using this:
Y \<in> Pow (f ` A)
Y = f ` {a \<in> A. f a \<in> Y}

goal (1 subgoal):
 1. Y \<in> (`) f ` Pow A
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Y \<in> (`) f ` Pow A

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma setsetmapim_comp: "(f\<circ>g)\<turnstile>A = f\<turnstile>(g\<turnstile>A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (f \<circ> g) \<turnstile> A = f \<turnstile> (g \<turnstile> A)
[PROOF STEP]
by (auto simp add: image_comp)


[STATEMENT]
lemma list_cases_Cons_snoc [case_names Nil Single Cons_snoc]:
  assumes       Nil: "xs = [] \<Longrightarrow> P"
  and        Single: "\<And>x. xs = [x] \<Longrightarrow> P"
  and     Cons_snoc: "\<And>x ys y. xs = x # ys @ [y] \<Longrightarrow> P"
  shows "P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P
[PROOF STEP]
proof (cases xs, rule Nil)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. xs = [] \<Longrightarrow> xs = []
 2. \<And>a list. xs = a # list \<Longrightarrow> P
[PROOF STEP]
case (Cons x xs)
[PROOF STATE]
proof (state)
this:
xs = x # xs

goal (2 subgoals):
 1. xs = [] \<Longrightarrow> xs = []
 2. \<And>a list. xs = a # list \<Longrightarrow> P
[PROOF STEP]
with Single Cons_snoc
[PROOF STATE]
proof (chain)
picking this:
xs = [?x] \<Longrightarrow> P
xs = ?x # ?ys @ [?y] \<Longrightarrow> P
xs = x # xs
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
xs = [?x] \<Longrightarrow> P
xs = ?x # ?ys @ [?y] \<Longrightarrow> P
xs = x # xs

goal (1 subgoal):
 1. P
[PROOF STEP]
by (cases xs rule: rev_cases) auto
[PROOF STATE]
proof (state)
this:
P

goal (1 subgoal):
 1. xs = [] \<Longrightarrow> xs = []
[PROOF STEP]
qed


[STATEMENT]
lemma bottom_below_in:
  "has_bottom P \<Longrightarrow> x\<in>P \<Longrightarrow> bottom (P.\<^bold>\<le>x) = bottom P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>has_bottom P; x \<in> P\<rbrakk> \<Longrightarrow> bottom (P .\<^bold>\<le> x) = bottom P
[PROOF STEP]
using bottom_in_below_in
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>has_bottom ?P; ?x \<in> ?P\<rbrakk> \<Longrightarrow> bottom ?P \<in> ?P .\<^bold>\<le> ?x

goal (1 subgoal):
 1. \<lbrakk>has_bottom P; x \<in> P\<rbrakk> \<Longrightarrow> bottom (P .\<^bold>\<le> x) = bottom P
[PROOF STEP]
by (fast intro: bottomI[THEN sym])


[STATEMENT]
lemma [simp]: "\<eta>1 \<approx>>\<bullet> \<eta>2 \<Longrightarrow> NatTrans \<eta>1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<eta>1 \<approx>>\<bullet> \<eta>2 \<Longrightarrow> NatTrans \<eta>1
[PROOF STEP]
by auto


[STATEMENT]
lemma matrix_inv_Gauss_Jordan_iarrays_PA:
fixes A::"'a::{field}^'n::{mod_type}^'n::{mod_type}"
assumes inv_A: "invertible A"
shows "matrix_to_iarray (matrix_inv A) = fst (Gauss_Jordan_iarrays_PA (matrix_to_iarray A))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. matrix_to_iarray (matrix_inv A) = fst (Gauss_Jordan_iarrays_PA (matrix_to_iarray A))
[PROOF STEP]
by (metis inv_A matrix_inv_Gauss_Jordan_PA matrix_to_iarray_fst_Gauss_Jordan_PA)


[STATEMENT]
lemma take_from_mset_correct:
  assumes "s \<noteq> {#}"
  shows "take_from_mset s \<le> SPEC (\<lambda> (x, s'). x \<in># s \<and> s' = s - {#x#})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. take_from_mset s \<le> SPEC (\<lambda>(x, s'). x \<in># s \<and> s' = s - {#x#})
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
s \<noteq> {#}

goal (1 subgoal):
 1. take_from_mset s \<le> SPEC (\<lambda>(x, s'). x \<in># s \<and> s' = s - {#x#})
[PROOF STEP]
unfolding take_from_mset_def
[PROOF STATE]
proof (prove)
using this:
s \<noteq> {#}

goal (1 subgoal):
 1. ASSERT (s \<noteq> {#}) \<bind> (\<lambda>_. SPEC (\<lambda>(x, s'). x \<in># s \<and> s' = s - {#x#})) \<le> SPEC (\<lambda>(x, s'). x \<in># s \<and> s' = s - {#x#})
[PROOF STEP]
by simp


[STATEMENT]
lemma F2set3_JF2set_incl_JF2set:
  "a' \<in> F2set3 (dtor2 a) \<Longrightarrow> JF2set a' \<subseteq> JF2set a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a' \<in> F2set3 (dtor2 a) \<Longrightarrow> JF2set a' \<subseteq> JF2set a
[PROOF STEP]
apply (rule UN_least)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>a' \<in> F2set3 (dtor2 a); n \<in> UNIV\<rbrakk> \<Longrightarrow> JF2col n a' \<subseteq> JF2set a
[PROOF STEP]
apply (rule subsetI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n x. \<lbrakk>a' \<in> F2set3 (dtor2 a); n \<in> UNIV; x \<in> JF2col n a'\<rbrakk> \<Longrightarrow> x \<in> JF2set a
[PROOF STEP]
apply (rule UN_I)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>n x. \<lbrakk>a' \<in> F2set3 (dtor2 a); n \<in> UNIV; x \<in> JF2col n a'\<rbrakk> \<Longrightarrow> ?a4 n x \<in> UNIV
 2. \<And>n x. \<lbrakk>a' \<in> F2set3 (dtor2 a); n \<in> UNIV; x \<in> JF2col n a'\<rbrakk> \<Longrightarrow> x \<in> JF2col (?a4 n x) a
[PROOF STEP]
apply (rule UNIV_I)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n x. \<lbrakk>a' \<in> F2set3 (dtor2 a); n \<in> UNIV; x \<in> JF2col n a'\<rbrakk> \<Longrightarrow> x \<in> JF2col (?a4 n x) a
[PROOF STEP]
apply (rule subsetD)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>n x. \<lbrakk>a' \<in> F2set3 (dtor2 a); n \<in> UNIV; x \<in> JF2col n a'\<rbrakk> \<Longrightarrow> ?A8 n x \<subseteq> JF2col (?a4 n x) a
 2. \<And>n x. \<lbrakk>a' \<in> F2set3 (dtor2 a); n \<in> UNIV; x \<in> JF2col n a'\<rbrakk> \<Longrightarrow> x \<in> ?A8 n x
[PROOF STEP]
apply (rule equalityD2)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>n x. \<lbrakk>a' \<in> F2set3 (dtor2 a); n \<in> UNIV; x \<in> JF2col n a'\<rbrakk> \<Longrightarrow> JF2col (?a4 n x) a = ?A8 n x
 2. \<And>n x. \<lbrakk>a' \<in> F2set3 (dtor2 a); n \<in> UNIV; x \<in> JF2col n a'\<rbrakk> \<Longrightarrow> x \<in> ?A8 n x
[PROOF STEP]
apply (rule JF2col_Suc)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n x. \<lbrakk>a' \<in> F2set3 (dtor2 a); n \<in> UNIV; x \<in> JF2col n a'\<rbrakk> \<Longrightarrow> x \<in> F2set1 (dtor2 a) \<union> (\<Union> (JF1col (?n13 n x) ` F2set2 (dtor2 a)) \<union> \<Union> (JF2col (?n13 n x) ` F2set3 (dtor2 a)))
[PROOF STEP]
apply (rule UnI2)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n x. \<lbrakk>a' \<in> F2set3 (dtor2 a); n \<in> UNIV; x \<in> JF2col n a'\<rbrakk> \<Longrightarrow> x \<in> \<Union> (JF1col (?n13 n x) ` F2set2 (dtor2 a)) \<union> \<Union> (JF2col (?n13 n x) ` F2set3 (dtor2 a))
[PROOF STEP]
apply (tactic \<open>rtac @{context} (BNF_Util.mk_UnIN  2 2) 1\<close>)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n x. \<lbrakk>a' \<in> F2set3 (dtor2 a); n \<in> UNIV; x \<in> JF2col n a'\<rbrakk> \<Longrightarrow> x \<in> \<Union> (JF2col (?n13 n x) ` F2set3 (dtor2 a))
[PROOF STEP]
apply (erule UN_I)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n x. \<lbrakk>n \<in> UNIV; x \<in> JF2col n a'\<rbrakk> \<Longrightarrow> x \<in> JF2col (?n13 n x) a'
[PROOF STEP]
apply assumption
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in padic_integers) p_res_ring_one:
  assumes "k > 0"
  shows "\<one>\<^bsub>Zp_res_ring k\<^esub> = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<one>\<^bsub>residue_ring (p ^ k)\<^esub> = 1
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
0 < k

goal (1 subgoal):
 1. \<one>\<^bsub>residue_ring (p ^ k)\<^esub> = 1
[PROOF STEP]
by (simp add: residue_ring_def)


[STATEMENT]
lemma heap_wellformed_induct [consumes 1, case_names step]:
  assumes "heap_is_wellformed h"
    and step: "\<And>parent. (\<And>children child. h \<turnstile> get_child_nodes parent \<rightarrow>\<^sub>r children
               \<Longrightarrow> child \<in> set children \<Longrightarrow> P (cast child)) \<Longrightarrow> P parent"
  shows "P ptr"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P ptr
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. P ptr
[PROOF STEP]
fix ptr
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. P ptr
[PROOF STEP]
have "wf ((parent_child_rel h)\<inverse>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf ((parent_child_rel h)\<inverse>)
[PROOF STEP]
by (simp add: assms(1) finite_acyclic_wf_converse parent_child_rel_acyclic parent_child_rel_finite)
[PROOF STATE]
proof (state)
this:
wf ((parent_child_rel h)\<inverse>)

goal (1 subgoal):
 1. P ptr
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
wf ((parent_child_rel h)\<inverse>)
[PROOF STEP]
show "?thesis"
[PROOF STATE]
proof (prove)
using this:
wf ((parent_child_rel h)\<inverse>)

goal (1 subgoal):
 1. P ptr
[PROOF STEP]
proof (induct rule: wf_induct_rule)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. (\<And>y. (y, x) \<in> (parent_child_rel h)\<inverse> \<Longrightarrow> P y) \<Longrightarrow> P x
[PROOF STEP]
case (less parent)
[PROOF STATE]
proof (state)
this:
(?y, parent) \<in> (parent_child_rel h)\<inverse> \<Longrightarrow> P ?y

goal (1 subgoal):
 1. \<And>x. (\<And>y. (y, x) \<in> (parent_child_rel h)\<inverse> \<Longrightarrow> P y) \<Longrightarrow> P x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(?y, parent) \<in> (parent_child_rel h)\<inverse> \<Longrightarrow> P ?y
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
(?y, parent) \<in> (parent_child_rel h)\<inverse> \<Longrightarrow> P ?y

goal (1 subgoal):
 1. P parent
[PROOF STEP]
using assms parent_child_rel_child
[PROOF STATE]
proof (prove)
using this:
(?y, parent) \<in> (parent_child_rel h)\<inverse> \<Longrightarrow> P ?y
heap_is_wellformed h
(\<And>children child. \<lbrakk>h \<turnstile> get_child_nodes ?parent \<rightarrow>\<^sub>r children; child \<in> set children\<rbrakk> \<Longrightarrow> P (cast\<^sub>n\<^sub>o\<^sub>d\<^sub>e\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r child)) \<Longrightarrow> P ?parent
?h \<turnstile> get_child_nodes ?ptr \<rightarrow>\<^sub>r ?children \<Longrightarrow> (?child \<in> set ?children) = ((?ptr, cast\<^sub>n\<^sub>o\<^sub>d\<^sub>e\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r ?child) \<in> parent_child_rel ?h)

goal (1 subgoal):
 1. P parent
[PROOF STEP]
by (meson converse_iff)
[PROOF STATE]
proof (state)
this:
P parent

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma all_local_vars_Assumption[simp]:
  "all_local_vars (Assumption c) = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. all_local_vars (Assumption c) = {}
[PROOF STEP]
unfolding all_local_vars_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Union> (local_vars (Assumption c) ` fset (inPorts (Assumption c))) = {}
[PROOF STEP]
by simp


[STATEMENT]
lemma \<P>\<^sub>1_pow: "blinfun_apply (\<P>\<^sub>1 ^^ n) = blinfun_apply \<P>\<^sub>1 ^^ n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. blinfun_apply (\<P>\<^sub>1 ^^ n) = blinfun_apply \<P>\<^sub>1 ^^ n
[PROOF STEP]
by (induction n) auto


[STATEMENT]
lemma not_weak_iff:
  assumes x: "x \<in> A" and y: "y \<in> A" shows "\<not> y \<sqsubseteq> x \<longleftrightarrow> x \<sqsubseteq> y \<and> x \<noteq> y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<not> y \<sqsubseteq> x) = (x \<sqsubseteq> y \<and> x \<noteq> y)
[PROOF STEP]
using x y
[PROOF STATE]
proof (prove)
using this:
x \<in> A
y \<in> A

goal (1 subgoal):
 1. (\<not> y \<sqsubseteq> x) = (x \<sqsubseteq> y \<and> x \<noteq> y)
[PROOF STEP]
by (cases rule: comparable_cases, auto intro:antisym)


[STATEMENT]
lemma val_is_vD [elim]:
    fixes ip rt
  assumes "ip\<in>kD(rt)"
      and "the (flag rt ip) = val"
    shows "ip\<in>vD(rt)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ip \<in> vD rt
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
ip \<in> kD rt
the (flag rt ip) = val

goal (1 subgoal):
 1. ip \<in> vD rt
[PROOF STEP]
unfolding vD_def
[PROOF STATE]
proof (prove)
using this:
ip \<in> kD rt
the (flag rt ip) = val

goal (1 subgoal):
 1. ip \<in> {dip. flag rt dip = Some val}
[PROOF STEP]
by auto


[STATEMENT]
lemma Wbis_raw_coind2:
assumes "theta \<subseteq> Wretr theta" and
"theta ^-1 \<subseteq> Wretr (theta ^-1)"
shows "theta \<subseteq> Wbis"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. theta \<subseteq> Wbis
[PROOF STEP]
using assms mono_Retr bis_raw_coind2
[PROOF STATE]
proof (prove)
using this:
theta \<subseteq> Wretr theta
theta\<inverse> \<subseteq> Wretr (theta\<inverse>)
Bisim.mono Sretr
Bisim.mono ZOretr
Bisim.mono ZOretrT
Bisim.mono Wretr
Bisim.mono WretrT
Bisim.mono RetrT
\<lbrakk>Bisim.mono ?Retr; ?theta \<subseteq> ?Retr ?theta; ?theta\<inverse> \<subseteq> ?Retr (?theta\<inverse>)\<rbrakk> \<Longrightarrow> ?theta \<subseteq> bis ?Retr

goal (1 subgoal):
 1. theta \<subseteq> Wbis
[PROOF STEP]
unfolding Wbis_def
[PROOF STATE]
proof (prove)
using this:
theta \<subseteq> Wretr theta
theta\<inverse> \<subseteq> Wretr (theta\<inverse>)
Bisim.mono Sretr
Bisim.mono ZOretr
Bisim.mono ZOretrT
Bisim.mono Wretr
Bisim.mono WretrT
Bisim.mono RetrT
\<lbrakk>Bisim.mono ?Retr; ?theta \<subseteq> ?Retr ?theta; ?theta\<inverse> \<subseteq> ?Retr (?theta\<inverse>)\<rbrakk> \<Longrightarrow> ?theta \<subseteq> bis ?Retr

goal (1 subgoal):
 1. theta \<subseteq> bis Wretr
[PROOF STEP]
by blast


[STATEMENT]
lemma trace_callee_conv_trace_callee_aux:
  "trace_callee callee p xs a = bind_spmf (trace_callee_aux callee p xs) (\<lambda>s. map_spmf fst (callee s a))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. trace_callee callee p xs a = trace_callee_aux callee p xs \<bind> (\<lambda>s. map_spmf fst (callee s a))
[PROOF STEP]
by(induction xs arbitrary: p)(auto simp add: split_def)


[STATEMENT]
theorem sublistD_bounds_D_and_RD_bounds_sublistD:
  fixes PROB :: "'a problem"
  assumes "finite PROB"
  shows "
    problem_plan_bound_charles PROB \<le> problem_plan_bound PROB
    \<and> problem_plan_bound PROB \<le> RD PROB
  "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. problem_plan_bound_charles PROB \<le> problem_plan_bound PROB \<and> problem_plan_bound PROB \<le> RD PROB
[PROOF STEP]
using assms sublistD_bounds_D RD_bounds_sublistD
[PROOF STATE]
proof (prove)
using this:
finite PROB
finite ?PROB \<Longrightarrow> problem_plan_bound_charles ?PROB \<le> problem_plan_bound ?PROB
finite ?Pi \<Longrightarrow> problem_plan_bound ?Pi \<le> RD ?Pi

goal (1 subgoal):
 1. problem_plan_bound_charles PROB \<le> problem_plan_bound PROB \<and> problem_plan_bound PROB \<le> RD PROB
[PROOF STEP]
by auto

\<comment> \<open>NOTE type of `PROB` had to be fixed for MP of lemmas.\<close>


[STATEMENT]
theorem Theorem_3:
  assumes "\<forall>h. irc_on A (Ch h)"
  shows "(\<forall>h. substitutes_on A (Ch h)) \<longleftrightarrow> (\<forall>h. unilateral_substitutes_on A (Ch h) \<and> pareto_separable_on A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>h. substitutes_on A (Ch h)) = (\<forall>h. unilateral_substitutes_on A (Ch h) \<and> pareto_separable_on A)
[PROOF STEP]
using %invisible assms
      unilateral_substitutes_on_pareto_separable_on_substitutes_on substitutes_on_pareto_separable_on
      substitutes_on_unilateral_substitutes_on
[PROOF STATE]
proof (prove)
using this:
\<forall>h. irc_on A (Ch h)
\<lbrakk>\<forall>h. unilateral_substitutes_on ?A (Ch h); \<forall>h. irc_on ?A (Ch h); pareto_separable_on ?A\<rbrakk> \<Longrightarrow> substitutes_on ?A (Ch ?h)
\<forall>h. substitutes_on ?A (Ch h) \<Longrightarrow> pareto_separable_on ?A
substitutes_on ?A ?f \<Longrightarrow> unilateral_substitutes_on ?A ?f

goal (1 subgoal):
 1. (\<forall>h. substitutes_on A (Ch h)) = (\<forall>h. unilateral_substitutes_on A (Ch h) \<and> pareto_separable_on A)
[PROOF STEP]
by blast


[STATEMENT]
lemma expand_map_dom:
    assumes "g \<in> expand_map f"
    shows "dom g = dom f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dom g = dom f
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
g \<in> expand_map f

goal (1 subgoal):
 1. dom g = dom f
[PROOF STEP]
unfolding expand_map_def expand_def
[PROOF STATE]
proof (prove)
using this:
g \<in> {g. \<forall>x. g x \<in> (case_option {None} ((`) Some) \<circ> f) x}

goal (1 subgoal):
 1. dom g = dom f
[PROOF STEP]
by (auto split: option.splits)


[STATEMENT]
lemma subst_bvs_Abs[simp]: "\<forall>x \<in> set args . is_closed x \<Longrightarrow>
  subst_bvs args (Abs T t) = Abs T (subst_bvs1' t 1 args)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>set args. is_closed x \<Longrightarrow> subst_bvs args (Abs T t) = Abs T (subst_bvs1' t 1 args)
[PROOF STEP]
using subst_bvs1'_Abs subst_bvs_subst_bvs1'
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>set ?args. is_closed x \<Longrightarrow> subst_bvs1' (Abs ?T ?t) ?lev ?args = Abs ?T (subst_bvs1' ?t (Suc ?lev) ?args)
subst_bvs ?s ?t = subst_bvs1' ?t 0 ?s

goal (1 subgoal):
 1. \<forall>x\<in>set args. is_closed x \<Longrightarrow> subst_bvs args (Abs T t) = Abs T (subst_bvs1' t 1 args)
[PROOF STEP]
by auto


[STATEMENT]
lemma finite_SP: "finite (SP \<phi>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (SP \<phi>)
[PROOF STEP]
using SP_fv finite_fv_fo_fmla finite_subset
[PROOF STATE]
proof (prove)
using this:
SP ?\<phi> \<subseteq> fv_fo_fmla ?\<phi>
finite (fv_fo_fmla ?\<phi>)
\<lbrakk>?A \<subseteq> ?B; finite ?B\<rbrakk> \<Longrightarrow> finite ?A

goal (1 subgoal):
 1. finite (SP \<phi>)
[PROOF STEP]
by fastforce


[STATEMENT]
lemma is_syz_sigE:
  assumes "is_syz_sig d u"
  obtains r where "r \<noteq> 0" and "lt r = u" and "r \<in> dgrad_sig_set d" and "rep_list r = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>r. \<lbrakk>r \<noteq> 0; lt r = u; r \<in> dgrad_sig_set' (length fs) d; rep_list r = 0\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
is_syz_sig d u

goal (1 subgoal):
 1. (\<And>r. \<lbrakk>r \<noteq> 0; lt r = u; r \<in> dgrad_sig_set' (length fs) d; rep_list r = 0\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding is_syz_sig_def
[PROOF STATE]
proof (prove)
using this:
\<exists>s\<in>dgrad_sig_set' (length fs) d. s \<noteq> 0 \<and> lt s = u \<and> rep_list s = 0

goal (1 subgoal):
 1. (\<And>r. \<lbrakk>r \<noteq> 0; lt r = u; r \<in> dgrad_sig_set' (length fs) d; rep_list r = 0\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast


[STATEMENT]
lemma rb_aux_inv1_D5:
  "rb_aux_inv1 bs \<Longrightarrow> i < length bs \<Longrightarrow> is_RB_upt dgrad rword (set (drop (Suc i) bs)) (lt (bs ! i))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>rb_aux_inv1 bs; i < length bs\<rbrakk> \<Longrightarrow> is_RB_upt dgrad rword (set (drop (Suc i) bs)) (lt (bs ! i))
[PROOF STEP]
by (simp add: rb_aux_inv1_def)


[STATEMENT]
lemma integral_cos_Z' [simp]:
  assumes "n \<in> \<int>"
  shows "integral\<^sup>L (lebesgue_on {-pi..pi}) (\<lambda>x. cos(n * x)) = (if n = 0 then 2 * pi else 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. LINT x|lebesgue_on {- pi..pi}. cos (n * x) = (if n = 0 then 2 * pi else 0)
[PROOF STEP]
by (metis assms integral_cos_Z mult_commute_abs)


[STATEMENT]
lemma Fejer_kernel_continuous:
  "continuous_on {-pi..pi} (Fejer_kernel n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. continuous_on {- pi..pi} (Fejer_kernel n)
[PROOF STEP]
apply (rule continuous_on_subset [OF Fejer_kernel_continuous_strong])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {- pi..pi} \<subseteq> {- (2 * pi)<..<2 * pi}
[PROOF STEP]
apply (simp add: subset_iff)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>t. - pi \<le> t \<and> t \<le> pi \<longrightarrow> - (2 * pi) < t \<and> t < 2 * pi
[PROOF STEP]
using pi_gt_zero
[PROOF STATE]
proof (prove)
using this:
0 < pi

goal (1 subgoal):
 1. \<forall>t. - pi \<le> t \<and> t \<le> pi \<longrightarrow> - (2 * pi) < t \<and> t < 2 * pi
[PROOF STEP]
apply linarith
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma bigtheta_const [landau_simp]:
  "NO_MATCH 1 c \<Longrightarrow> c \<noteq> 0 \<Longrightarrow> (\<lambda>x. c) \<in> \<Theta>(\<lambda>x. 1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>NO_MATCH (1::'a) c; c \<noteq> (0::'b)\<rbrakk> \<Longrightarrow> (\<lambda>x. c) \<in> \<Theta>(\<lambda>x. 1::'b)
[PROOF STEP]
by simp


[STATEMENT]
lemma vcard_vlepoll: "vcard A \<le> vcard B \<longleftrightarrow> A \<lesssim>\<^sub>\<circ> B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (vcard A \<subseteq>\<^sub>\<circ> vcard B) = (A \<lesssim>\<^sub>\<circ> B)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. vcard A \<subseteq>\<^sub>\<circ> vcard B \<Longrightarrow> A \<lesssim>\<^sub>\<circ> B
 2. A \<lesssim>\<^sub>\<circ> B \<Longrightarrow> vcard A \<subseteq>\<^sub>\<circ> vcard B
[PROOF STEP]
assume "vcard A \<le> vcard B"
[PROOF STATE]
proof (state)
this:
vcard A \<subseteq>\<^sub>\<circ> vcard B

goal (2 subgoals):
 1. vcard A \<subseteq>\<^sub>\<circ> vcard B \<Longrightarrow> A \<lesssim>\<^sub>\<circ> B
 2. A \<lesssim>\<^sub>\<circ> B \<Longrightarrow> vcard A \<subseteq>\<^sub>\<circ> vcard B
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
vcard A \<subseteq>\<^sub>\<circ> vcard B

goal (2 subgoals):
 1. vcard A \<subseteq>\<^sub>\<circ> vcard B \<Longrightarrow> A \<lesssim>\<^sub>\<circ> B
 2. A \<lesssim>\<^sub>\<circ> B \<Longrightarrow> vcard A \<subseteq>\<^sub>\<circ> vcard B
[PROOF STEP]
have "vcard A \<approx>\<^sub>\<circ> A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vcard A \<approx>\<^sub>\<circ> A
[PROOF STEP]
by (rule cardinal_eqpoll)
[PROOF STATE]
proof (state)
this:
vcard A \<approx>\<^sub>\<circ> A

goal (2 subgoals):
 1. vcard A \<subseteq>\<^sub>\<circ> vcard B \<Longrightarrow> A \<lesssim>\<^sub>\<circ> B
 2. A \<lesssim>\<^sub>\<circ> B \<Longrightarrow> vcard A \<subseteq>\<^sub>\<circ> vcard B
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
vcard A \<approx>\<^sub>\<circ> A

goal (2 subgoals):
 1. vcard A \<subseteq>\<^sub>\<circ> vcard B \<Longrightarrow> A \<lesssim>\<^sub>\<circ> B
 2. A \<lesssim>\<^sub>\<circ> B \<Longrightarrow> vcard A \<subseteq>\<^sub>\<circ> vcard B
[PROOF STEP]
have "vcard B \<approx>\<^sub>\<circ> B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vcard B \<approx>\<^sub>\<circ> B
[PROOF STEP]
by (rule cardinal_eqpoll)
[PROOF STATE]
proof (state)
this:
vcard B \<approx>\<^sub>\<circ> B

goal (2 subgoals):
 1. vcard A \<subseteq>\<^sub>\<circ> vcard B \<Longrightarrow> A \<lesssim>\<^sub>\<circ> B
 2. A \<lesssim>\<^sub>\<circ> B \<Longrightarrow> vcard A \<subseteq>\<^sub>\<circ> vcard B
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
vcard A \<subseteq>\<^sub>\<circ> vcard B
vcard A \<approx>\<^sub>\<circ> A
vcard B \<approx>\<^sub>\<circ> B
[PROOF STEP]
show "A \<lesssim>\<^sub>\<circ> B"
[PROOF STATE]
proof (prove)
using this:
vcard A \<subseteq>\<^sub>\<circ> vcard B
vcard A \<approx>\<^sub>\<circ> A
vcard B \<approx>\<^sub>\<circ> B

goal (1 subgoal):
 1. A \<lesssim>\<^sub>\<circ> B
[PROOF STEP]
by (meson eqpoll_sym lepoll_trans1 lepoll_trans2 vlepoll_vsubset)
[PROOF STATE]
proof (state)
this:
A \<lesssim>\<^sub>\<circ> B

goal (1 subgoal):
 1. A \<lesssim>\<^sub>\<circ> B \<Longrightarrow> vcard A \<subseteq>\<^sub>\<circ> vcard B
[PROOF STEP]
qed (simp add: lepoll_imp_Card_le)


[STATEMENT]
lemma iterateoi_rule_P[case_names minv inv0 inv_pres i_complete i_inter]:
      assumes MINV: "invar m"
      assumes I0: "I (\<alpha> m) \<sigma>0"
      assumes IP: "!!k it \<sigma>. \<lbrakk>
        c \<sigma>;
        k \<in> it;
        \<forall>j\<in>it. k\<le>j;
        \<forall>j\<in>\<alpha> m - it. j\<le>k;
        it \<subseteq> \<alpha> m;
        I it \<sigma>
      \<rbrakk> \<Longrightarrow> I (it - {k}) (f k \<sigma>)"
      assumes IF: "!!\<sigma>. I {} \<sigma> \<Longrightarrow> P \<sigma>"
      assumes II: "!!\<sigma> it. \<lbrakk>
        it \<subseteq> \<alpha> m;
        it \<noteq> {};
        \<not> c \<sigma>;
        I it \<sigma>;
        \<forall>k\<in>it. \<forall>j\<in>\<alpha> m - it. j\<le>k
      \<rbrakk> \<Longrightarrow> P \<sigma>"
      shows "P (iterateoi m c f \<sigma>0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P (iterateoi m c f \<sigma>0)
[PROOF STEP]
using set_iterator_linord_rule_P [OF iterateoi_rule, OF MINV, of I \<sigma>0 c f P,
       OF I0 _ IF] IP II
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<And>S \<sigma> x. \<lbrakk>c \<sigma>; x \<in> S; I S \<sigma>; S \<subseteq> \<alpha> m; \<And>x'. x' \<in> \<alpha> m - S \<Longrightarrow> x' \<le> x; \<And>x'. x' \<in> S \<Longrightarrow> x \<le> x'\<rbrakk> \<Longrightarrow> I (S - {x}) (f x \<sigma>); \<And>\<sigma>. I {} \<sigma> \<Longrightarrow> I {} \<sigma>; \<And>\<sigma> S. \<lbrakk>S \<subseteq> \<alpha> m; S \<noteq> {}; \<And>x x'. \<lbrakk>x \<in> S; x' \<in> \<alpha> m - S\<rbrakk> \<Longrightarrow> x' \<le> x; \<not> c \<sigma>; I S \<sigma>\<rbrakk> \<Longrightarrow> P \<sigma>\<rbrakk> \<Longrightarrow> P (iterateoi m c f \<sigma>0)
\<lbrakk>c ?\<sigma>1; ?k1 \<in> ?it1; \<forall>j\<in>?it1. ?k1 \<le> j; \<forall>j\<in>\<alpha> m - ?it1. j \<le> ?k1; ?it1 \<subseteq> \<alpha> m; I ?it1 ?\<sigma>1\<rbrakk> \<Longrightarrow> I (?it1 - {?k1}) (f ?k1 ?\<sigma>1)
\<lbrakk>?it1 \<subseteq> \<alpha> m; ?it1 \<noteq> {}; \<not> c ?\<sigma>1; I ?it1 ?\<sigma>1; \<forall>k\<in>?it1. \<forall>j\<in>\<alpha> m - ?it1. j \<le> k\<rbrakk> \<Longrightarrow> P ?\<sigma>1

goal (1 subgoal):
 1. P (iterateoi m c f \<sigma>0)
[PROOF STEP]
by simp


[STATEMENT]
lemma "create_name_igba \<phi> \<le> SPEC (\<lambda>G. igba G \<and> (\<forall>\<xi>. igba.accept G \<xi> \<longleftrightarrow> \<xi> \<Turnstile>\<^sub>r \<phi>))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. create_name_igba \<phi> \<le> SPEC (\<lambda>G. igba G \<and> (\<forall>\<xi>. igba.accept G \<xi> = \<xi> \<Turnstile>\<^sub>r \<phi>))
[PROOF STEP]
unfolding create_name_igba_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. create_name_gba \<phi> \<bind> (\<lambda>A. gba_to_idx A \<bind> (\<lambda>A'. stat_set_data_nres (card (g_V A)) (card (g_V0 A')) (igbg_num_acc A') \<bind> (\<lambda>_. RETURN A'))) \<le> SPEC (\<lambda>G. igba G \<and> (\<forall>\<xi>. igba.accept G \<xi> = \<xi> \<Turnstile>\<^sub>r \<phi>))
[PROOF STEP]
proof (refine_rcg refine_vcg, clarsimp_all)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>gba x; finite (g_V x); \<forall>\<xi>. gba.accept x \<xi> = \<xi> \<Turnstile>\<^sub>r \<phi>\<rbrakk> \<Longrightarrow> gba_to_idx x \<le> SPEC (\<lambda>A'. igba A' \<and> (\<forall>\<xi>. igba.accept A' \<xi> = \<xi> \<Turnstile>\<^sub>r \<phi>))
[PROOF STEP]
fix G :: "(nat, 'a set) gba_rec"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>gba x; finite (g_V x); \<forall>\<xi>. gba.accept x \<xi> = \<xi> \<Turnstile>\<^sub>r \<phi>\<rbrakk> \<Longrightarrow> gba_to_idx x \<le> SPEC (\<lambda>A'. igba A' \<and> (\<forall>\<xi>. igba.accept A' \<xi> = \<xi> \<Turnstile>\<^sub>r \<phi>))
[PROOF STEP]
assume "gba G"
[PROOF STATE]
proof (state)
this:
gba G

goal (1 subgoal):
 1. \<And>x. \<lbrakk>gba x; finite (g_V x); \<forall>\<xi>. gba.accept x \<xi> = \<xi> \<Turnstile>\<^sub>r \<phi>\<rbrakk> \<Longrightarrow> gba_to_idx x \<le> SPEC (\<lambda>A'. igba A' \<and> (\<forall>\<xi>. igba.accept A' \<xi> = \<xi> \<Turnstile>\<^sub>r \<phi>))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
gba G
[PROOF STEP]
interpret gba G
[PROOF STATE]
proof (prove)
using this:
gba G

goal (1 subgoal):
 1. gba G
[PROOF STEP]
.
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>gba x; finite (g_V x); \<forall>\<xi>. gba.accept x \<xi> = \<xi> \<Turnstile>\<^sub>r \<phi>\<rbrakk> \<Longrightarrow> gba_to_idx x \<le> SPEC (\<lambda>A'. igba A' \<and> (\<forall>\<xi>. igba.accept A' \<xi> = \<xi> \<Turnstile>\<^sub>r \<phi>))
[PROOF STEP]
note [refine_vcg] = order_trans[OF gba_to_idx_ext_correct]
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<And>A. A \<in> F \<Longrightarrow> finite A; SPEC (\<lambda>G'. igba.accept G' = accept \<and> g_V G' = V \<and> g_E G' = E \<and> g_V0 G' = V0 \<and> igba_rec.more G' = ?ecnv1 G \<and> igba G') \<le> ?z\<rbrakk> \<Longrightarrow> gba_to_idx_ext ?ecnv1 G \<le> ?z

goal (1 subgoal):
 1. \<And>x. \<lbrakk>gba x; finite (g_V x); \<forall>\<xi>. gba.accept x \<xi> = \<xi> \<Turnstile>\<^sub>r \<phi>\<rbrakk> \<Longrightarrow> gba_to_idx x \<le> SPEC (\<lambda>A'. igba A' \<and> (\<forall>\<xi>. igba.accept A' \<xi> = \<xi> \<Turnstile>\<^sub>r \<phi>))
[PROOF STEP]
assume "\<forall>\<xi>. gba.accept G \<xi> = \<xi> \<Turnstile>\<^sub>r \<phi>" "finite (g_V G)"
[PROOF STATE]
proof (state)
this:
\<forall>\<xi>. accept \<xi> = \<xi> \<Turnstile>\<^sub>r \<phi>
finite V

goal (1 subgoal):
 1. \<And>x. \<lbrakk>gba x; finite (g_V x); \<forall>\<xi>. gba.accept x \<xi> = \<xi> \<Turnstile>\<^sub>r \<phi>\<rbrakk> \<Longrightarrow> gba_to_idx x \<le> SPEC (\<lambda>A'. igba A' \<and> (\<forall>\<xi>. igba.accept A' \<xi> = \<xi> \<Turnstile>\<^sub>r \<phi>))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>\<xi>. accept \<xi> = \<xi> \<Turnstile>\<^sub>r \<phi>
finite V
[PROOF STEP]
show "gba_to_idx G \<le> SPEC (\<lambda>G'. igba G' \<and> (\<forall>\<xi>. igba.accept G' \<xi> = \<xi> \<Turnstile>\<^sub>r \<phi>))"
[PROOF STATE]
proof (prove)
using this:
\<forall>\<xi>. accept \<xi> = \<xi> \<Turnstile>\<^sub>r \<phi>
finite V

goal (1 subgoal):
 1. gba_to_idx G \<le> SPEC (\<lambda>G'. igba G' \<and> (\<forall>\<xi>. igba.accept G' \<xi> = \<xi> \<Turnstile>\<^sub>r \<phi>))
[PROOF STEP]
by (refine_rcg refine_vcg) (auto intro: finite_V_Fe)
[PROOF STATE]
proof (state)
this:
gba_to_idx G \<le> SPEC (\<lambda>G'. igba G' \<and> (\<forall>\<xi>. igba.accept G' \<xi> = \<xi> \<Turnstile>\<^sub>r \<phi>))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma relabel_agtt_lang [simp]:
  "agtt_lang (relabel_gtt G) = agtt_lang G"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. agtt_lang (relabel_gtt G) = agtt_lang G
[PROOF STEP]
by (simp add: agtt_lang_fmap_states_gtt map_fset_to_nat_inj relabel_gtt_def)


[STATEMENT]
lemma coprod_qbs_canonical1':
  assumes "countable I"
      and "\<And>i. i \<in> I \<Longrightarrow> (\<lambda>x. f (i,x)) \<in> X i \<rightarrow>\<^sub>Q Y"
    shows  "f \<in> (\<amalg>\<^sub>Q i \<in>I. X i) \<rightarrow>\<^sub>Q Y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f \<in> coprod_qbs I X \<rightarrow>\<^sub>Q Y
[PROOF STEP]
using coprod_qbs_canonical1[where f="curry f"] assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>countable ?I; \<And>i. i \<in> ?I \<Longrightarrow> curry f i \<in> ?X i \<rightarrow>\<^sub>Q ?Y\<rbrakk> \<Longrightarrow> (\<lambda>(i, x). curry f i x) \<in> coprod_qbs ?I ?X \<rightarrow>\<^sub>Q ?Y
countable I
?i \<in> I \<Longrightarrow> (\<lambda>x. f (?i, x)) \<in> X ?i \<rightarrow>\<^sub>Q Y

goal (1 subgoal):
 1. f \<in> coprod_qbs I X \<rightarrow>\<^sub>Q Y
[PROOF STEP]
by(auto simp: curry_def)


[STATEMENT]
lemma less_\<tau>D: "\<tau> \<sigma> i < \<tau> \<sigma> j \<Longrightarrow> i < j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<tau> \<sigma> i < \<tau> \<sigma> j \<Longrightarrow> i < j
[PROOF STEP]
by (meson \<tau>_mono less_le_not_le not_le_imp_less)


[STATEMENT]
lemma irreflp_onI [Pure.intro]:
  "(\<And>a. a \<in> A \<Longrightarrow> \<not> P a a) \<Longrightarrow> irreflp_on P A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>a. a \<in> A \<Longrightarrow> \<not> P a a) \<Longrightarrow> irreflp_on P A
[PROOF STEP]
unfolding irreflp_on_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>a. a \<in> A \<Longrightarrow> \<not> P a a) \<Longrightarrow> \<forall>a\<in>A. \<not> P a a
[PROOF STEP]
by blast


[STATEMENT]
lemma accessible_on_restrict_to_downwards:
  assumes "(restrict_to P A)\<^sup>+\<^sup>+ a b" and "accessible_on P A b"
  shows "accessible_on P A a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. accessible_on P A a
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
(restrict_to P A)\<^sup>+\<^sup>+ a b
accessible_on P A b

goal (1 subgoal):
 1. accessible_on P A a
[PROOF STEP]
by (induct) (auto dest: accessible_on_imp_mem accessible_on_downward)


[STATEMENT]
theorem Spy_not_see_NB [dest]:
     "\<lbrakk>Says B A (Crypt (pubEK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) \<in> set evs;
       \<forall>C. Says A C (Crypt (pubEK C) (Nonce NB)) \<notin> set evs;
       A \<notin> bad;  B \<notin> bad;  evs \<in> ns_public\<rbrakk>
     \<Longrightarrow> Nonce NB \<notin> analz (knows Spy evs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Says B A (Crypt (pubK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) \<in> set evs; \<forall>C. Says A C (Crypt (pubK C) (Nonce NB)) \<notin> set evs; A \<notin> bad; B \<notin> bad; evs \<in> ns_public\<rbrakk> \<Longrightarrow> Nonce NB \<notin> analz (knows Spy evs)
[PROOF STEP]
apply (erule rev_mp, erule rev_mp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>A \<notin> bad; B \<notin> bad; evs \<in> ns_public\<rbrakk> \<Longrightarrow> (\<forall>C. Says A C (Crypt (pubK C) (Nonce NB)) \<notin> set evs) \<longrightarrow> Says B A (Crypt (pubK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) \<in> set evs \<longrightarrow> Nonce NB \<notin> analz (knows Spy evs)
[PROOF STEP]
apply (erule ns_public.induct, simp_all, spy_analz)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>evs1 NAa Ba. \<lbrakk>A \<notin> bad; B \<notin> bad; evs1 \<in> ns_public; (\<forall>C. Says A C (Crypt (pubK C) (Nonce NB)) \<notin> set evs1) \<longrightarrow> Says B A (Crypt (pubK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) \<in> set evs1 \<longrightarrow> Nonce NB \<notin> analz (knows Spy evs1); Nonce NAa \<notin> used evs1\<rbrakk> \<Longrightarrow> Ba \<in> bad \<longrightarrow> (\<forall>C. Says A C (Crypt (pubK C) (Nonce NB)) \<notin> set evs1) \<longrightarrow> Says B A (Crypt (pubK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) \<in> set evs1 \<longrightarrow> NB \<noteq> NAa
 2. \<And>evs2 NBa Ba NAa Aa. \<lbrakk>A \<notin> bad; B \<notin> bad; evs2 \<in> ns_public; (\<forall>C. Says A C (Crypt (pubK C) (Nonce NB)) \<notin> set evs2) \<longrightarrow> Says B A (Crypt (pubK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) \<in> set evs2 \<longrightarrow> Nonce NB \<notin> analz (knows Spy evs2); Nonce NBa \<notin> used evs2; Gets Ba (Crypt (pubK Ba) \<lbrace>Nonce NAa, Agent Aa\<rbrace>) \<in> set evs2\<rbrakk> \<Longrightarrow> (Aa \<in> bad \<longrightarrow> (\<forall>C. Says A C (Crypt (pubK C) (Nonce NB)) \<notin> set evs2) \<longrightarrow> (NA = NAa \<longrightarrow> A = Aa \<longrightarrow> B = Ba \<longrightarrow> NB \<noteq> NBa) \<and> (Says B A (Crypt (pubK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) \<in> set evs2 \<longrightarrow> NB \<noteq> NAa \<and> NB \<noteq> NBa)) \<and> (Aa \<notin> bad \<longrightarrow> (\<forall>C. Says A C (Crypt (pubK C) (Nonce NB)) \<notin> set evs2) \<longrightarrow> B = Ba \<and> A = Aa \<and> NA = NAa \<and> NB = NBa \<longrightarrow> Nonce NBa \<notin> analz (knows Spy evs2))
 3. \<And>evs3 Aa Ba NAa NBa. \<lbrakk>A \<notin> bad; B \<notin> bad; evs3 \<in> ns_public; (\<forall>C. Says A C (Crypt (pubK C) (Nonce NB)) \<notin> set evs3) \<longrightarrow> Says B A (Crypt (pubK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) \<in> set evs3 \<longrightarrow> Nonce NB \<notin> analz (knows Spy evs3); Says Aa Ba (Crypt (pubK Ba) \<lbrace>Nonce NAa, Agent Aa\<rbrace>) \<in> set evs3; Gets Aa (Crypt (pubK Aa) \<lbrace>Nonce NAa, Nonce NBa\<rbrace>) \<in> set evs3\<rbrakk> \<Longrightarrow> Ba \<in> bad \<longrightarrow> (\<forall>C. (C = Ba \<longrightarrow> A = Aa \<longrightarrow> NB \<noteq> NBa) \<and> Says A C (Crypt (pubK C) (Nonce NB)) \<notin> set evs3) \<longrightarrow> Says B A (Crypt (pubK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) \<in> set evs3 \<longrightarrow> NB \<noteq> NBa
[PROOF STEP]
apply (simp_all add: all_conj_distrib)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>evs1 NAa Ba. \<lbrakk>A \<notin> bad; B \<notin> bad; evs1 \<in> ns_public; (\<forall>C. Says A C (Crypt (pubK C) (Nonce NB)) \<notin> set evs1) \<longrightarrow> Says B A (Crypt (pubK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) \<in> set evs1 \<longrightarrow> Nonce NB \<notin> analz (knows Spy evs1); Nonce NAa \<notin> used evs1\<rbrakk> \<Longrightarrow> Ba \<in> bad \<longrightarrow> (\<forall>C. Says A C (Crypt (pubK C) (Nonce NB)) \<notin> set evs1) \<longrightarrow> Says B A (Crypt (pubK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) \<in> set evs1 \<longrightarrow> NB \<noteq> NAa
 2. \<And>evs2 NBa Ba NAa Aa. \<lbrakk>A \<notin> bad; B \<notin> bad; evs2 \<in> ns_public; (\<forall>C. Says A C (Crypt (pubK C) (Nonce NB)) \<notin> set evs2) \<longrightarrow> Says B A (Crypt (pubK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) \<in> set evs2 \<longrightarrow> Nonce NB \<notin> analz (knows Spy evs2); Nonce NBa \<notin> used evs2; Gets Ba (Crypt (pubK Ba) \<lbrace>Nonce NAa, Agent Aa\<rbrace>) \<in> set evs2\<rbrakk> \<Longrightarrow> (Aa \<in> bad \<longrightarrow> (\<forall>C. Says A C (Crypt (pubK C) (Nonce NB)) \<notin> set evs2) \<longrightarrow> (NA = NAa \<longrightarrow> A = Aa \<longrightarrow> B = Ba \<longrightarrow> NB \<noteq> NBa) \<and> (Says B A (Crypt (pubK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) \<in> set evs2 \<longrightarrow> NB \<noteq> NAa \<and> NB \<noteq> NBa)) \<and> (Aa \<notin> bad \<longrightarrow> (\<forall>C. Says A C (Crypt (pubK C) (Nonce NB)) \<notin> set evs2) \<longrightarrow> B = Ba \<and> A = Aa \<and> NA = NAa \<and> NB = NBa \<longrightarrow> Nonce NBa \<notin> analz (knows Spy evs2))
 3. \<And>evs3 Aa Ba NAa NBa. \<lbrakk>A \<notin> bad; B \<notin> bad; evs3 \<in> ns_public; (\<forall>C. Says A C (Crypt (pubK C) (Nonce NB)) \<notin> set evs3) \<longrightarrow> Says B A (Crypt (pubK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) \<in> set evs3 \<longrightarrow> Nonce NB \<notin> analz (knows Spy evs3); Says Aa Ba (Crypt (pubK Ba) \<lbrace>Nonce NAa, Agent Aa\<rbrace>) \<in> set evs3; Gets Aa (Crypt (pubK Aa) \<lbrace>Nonce NAa, Nonce NBa\<rbrace>) \<in> set evs3\<rbrakk> \<Longrightarrow> Ba \<in> bad \<longrightarrow> (A = Aa \<longrightarrow> NB \<noteq> NBa) \<and> (\<forall>C. Says A C (Crypt (pubK C) (Nonce NB)) \<notin> set evs3) \<longrightarrow> Says B A (Crypt (pubK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) \<in> set evs3 \<longrightarrow> NB \<noteq> NBa
[PROOF STEP]
(*speeds up the next step*)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>evs1 NAa Ba. \<lbrakk>A \<notin> bad; B \<notin> bad; evs1 \<in> ns_public; (\<forall>C. Says A C (Crypt (pubK C) (Nonce NB)) \<notin> set evs1) \<longrightarrow> Says B A (Crypt (pubK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) \<in> set evs1 \<longrightarrow> Nonce NB \<notin> analz (knows Spy evs1); Nonce NAa \<notin> used evs1\<rbrakk> \<Longrightarrow> Ba \<in> bad \<longrightarrow> (\<forall>C. Says A C (Crypt (pubK C) (Nonce NB)) \<notin> set evs1) \<longrightarrow> Says B A (Crypt (pubK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) \<in> set evs1 \<longrightarrow> NB \<noteq> NAa
 2. \<And>evs2 NBa Ba NAa Aa. \<lbrakk>A \<notin> bad; B \<notin> bad; evs2 \<in> ns_public; (\<forall>C. Says A C (Crypt (pubK C) (Nonce NB)) \<notin> set evs2) \<longrightarrow> Says B A (Crypt (pubK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) \<in> set evs2 \<longrightarrow> Nonce NB \<notin> analz (knows Spy evs2); Nonce NBa \<notin> used evs2; Gets Ba (Crypt (pubK Ba) \<lbrace>Nonce NAa, Agent Aa\<rbrace>) \<in> set evs2\<rbrakk> \<Longrightarrow> (Aa \<in> bad \<longrightarrow> (\<forall>C. Says A C (Crypt (pubK C) (Nonce NB)) \<notin> set evs2) \<longrightarrow> (NA = NAa \<longrightarrow> A = Aa \<longrightarrow> B = Ba \<longrightarrow> NB \<noteq> NBa) \<and> (Says B A (Crypt (pubK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) \<in> set evs2 \<longrightarrow> NB \<noteq> NAa \<and> NB \<noteq> NBa)) \<and> (Aa \<notin> bad \<longrightarrow> (\<forall>C. Says A C (Crypt (pubK C) (Nonce NB)) \<notin> set evs2) \<longrightarrow> B = Ba \<and> A = Aa \<and> NA = NAa \<and> NB = NBa \<longrightarrow> Nonce NBa \<notin> analz (knows Spy evs2))
 3. \<And>evs3 Aa Ba NAa NBa. \<lbrakk>A \<notin> bad; B \<notin> bad; evs3 \<in> ns_public; (\<forall>C. Says A C (Crypt (pubK C) (Nonce NB)) \<notin> set evs3) \<longrightarrow> Says B A (Crypt (pubK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) \<in> set evs3 \<longrightarrow> Nonce NB \<notin> analz (knows Spy evs3); Says Aa Ba (Crypt (pubK Ba) \<lbrace>Nonce NAa, Agent Aa\<rbrace>) \<in> set evs3; Gets Aa (Crypt (pubK Aa) \<lbrace>Nonce NAa, Nonce NBa\<rbrace>) \<in> set evs3\<rbrakk> \<Longrightarrow> Ba \<in> bad \<longrightarrow> (A = Aa \<longrightarrow> NB \<noteq> NBa) \<and> (\<forall>C. Says A C (Crypt (pubK C) (Nonce NB)) \<notin> set evs3) \<longrightarrow> Says B A (Crypt (pubK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) \<in> set evs3 \<longrightarrow> NB \<noteq> NBa
[PROOF STEP]
apply (blast intro: no_nonce_NS1_NS2)+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma Subset_E: "H \<turnstile> t SUBS u \<Longrightarrow> H \<turnstile> a IN t \<Longrightarrow> insert (a IN u) H \<turnstile> A \<Longrightarrow> H \<turnstile> A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>H \<turnstile> t SUBS u; H \<turnstile> a IN t; insert (a IN u) H \<turnstile> A\<rbrakk> \<Longrightarrow> H \<turnstile> A
[PROOF STEP]
by (metis Subset_D cut_same)


[STATEMENT]
lemma Disjoint_fresh_iff [simp]: "a \<sharp> Disjoint t u \<longleftrightarrow> a \<sharp> t \<and> a \<sharp> u"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<sharp> Disjoint t u = (a \<sharp> t \<and> a \<sharp> u)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. a \<sharp> Disjoint t u = (a \<sharp> t \<and> a \<sharp> u)
[PROOF STEP]
obtain j::name where j: "atom j \<sharp> (a,t,u)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>j. atom j \<sharp> (a, t, u) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (rule obtain_fresh)
[PROOF STATE]
proof (state)
this:
atom j \<sharp> (a, t, u)

goal (1 subgoal):
 1. a \<sharp> Disjoint t u = (a \<sharp> t \<and> a \<sharp> u)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
atom j \<sharp> (a, t, u)

goal (1 subgoal):
 1. a \<sharp> Disjoint t u = (a \<sharp> t \<and> a \<sharp> u)
[PROOF STEP]
by (auto simp: Disjoint.simps [of j])
[PROOF STATE]
proof (state)
this:
a \<sharp> Disjoint t u = (a \<sharp> t \<and> a \<sharp> u)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma Seq_iff: "Seq r d \<longleftrightarrow> d \<le> hdomain r \<and> hfun_sigma r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Seq r d = (d \<le> hdomain r \<and> hfun_sigma r)
[PROOF STEP]
by (auto simp: Seq_def hfun_sigma_iff)


[STATEMENT]
lemma degree_div_mod_smult:
  fixes g::"int poly"
  assumes g: "degree g < j"
  and r: "degree r < d"
  and u: "degree u = d"
  and g1: "g = q * u + smult m r"
  and q: "q \<noteq> 0" and m_not0: "m \<noteq> 0"
shows "degree q < j - d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. degree q < j - d
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. degree q < j - d
[PROOF STEP]
have u_not0: "u\<noteq>0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. u \<noteq> 0
[PROOF STEP]
using u r
[PROOF STATE]
proof (prove)
using this:
degree u = d
degree r < d

goal (1 subgoal):
 1. u \<noteq> 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
u \<noteq> 0

goal (1 subgoal):
 1. degree q < j - d
[PROOF STEP]
have d_uq: "d \<le> degree (u*q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d \<le> degree (u * q)
[PROOF STEP]
using u degree_mult_right_le[OF q]
[PROOF STATE]
proof (prove)
using this:
degree u = d
degree ?p \<le> degree (?p * q)

goal (1 subgoal):
 1. d \<le> degree (u * q)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
d \<le> degree (u * q)

goal (1 subgoal):
 1. degree q < j - d
[PROOF STEP]
have j: "j > degree (q* u + smult m r)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. degree (q * u + Polynomial.smult m r) < j
[PROOF STEP]
using g1 g
[PROOF STATE]
proof (prove)
using this:
g = q * u + Polynomial.smult m r
degree g < j

goal (1 subgoal):
 1. degree (q * u + Polynomial.smult m r) < j
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
degree (q * u + Polynomial.smult m r) < j

goal (1 subgoal):
 1. degree q < j - d
[PROOF STEP]
have "degree (smult m r) < d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. degree (Polynomial.smult m r) < d
[PROOF STEP]
using degree_smult_eq m_not0 r
[PROOF STATE]
proof (prove)
using this:
degree (Polynomial.smult ?a ?p) = (if ?a = (0::?'a) then 0 else degree ?p)
m \<noteq> 0
degree r < d

goal (1 subgoal):
 1. degree (Polynomial.smult m r) < d
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
degree (Polynomial.smult m r) < d

goal (1 subgoal):
 1. degree q < j - d
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
degree (Polynomial.smult m r) < d

goal (1 subgoal):
 1. degree q < j - d
[PROOF STEP]
have "... \<le> degree (u*q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d \<le> degree (u * q)
[PROOF STEP]
using d_uq
[PROOF STATE]
proof (prove)
using this:
d \<le> degree (u * q)

goal (1 subgoal):
 1. d \<le> degree (u * q)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
d \<le> degree (u * q)

goal (1 subgoal):
 1. degree q < j - d
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
degree (Polynomial.smult m r) < degree (u * q)
[PROOF STEP]
have deg_mr_uq: "degree (smult m r) < degree (q*u)"
[PROOF STATE]
proof (prove)
using this:
degree (Polynomial.smult m r) < degree (u * q)

goal (1 subgoal):
 1. degree (Polynomial.smult m r) < degree (q * u)
[PROOF STEP]
by (simp add: mult.commute)
[PROOF STATE]
proof (state)
this:
degree (Polynomial.smult m r) < degree (q * u)

goal (1 subgoal):
 1. degree q < j - d
[PROOF STEP]
have j2: "degree (q* u + smult m r) = degree (q*u)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. degree (q * u + Polynomial.smult m r) = degree (q * u)
[PROOF STEP]
by (rule degree_add_eq_left[OF deg_mr_uq])
[PROOF STATE]
proof (state)
this:
degree (q * u + Polynomial.smult m r) = degree (q * u)

goal (1 subgoal):
 1. degree q < j - d
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
degree (q * u + Polynomial.smult m r) = degree (q * u)

goal (1 subgoal):
 1. degree q < j - d
[PROOF STEP]
have "... = degree q + degree u"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. degree (q * u) = degree q + degree u
[PROOF STEP]
by (rule degree_mult_eq[OF q u_not0])
[PROOF STATE]
proof (state)
this:
degree (q * u) = degree q + degree u

goal (1 subgoal):
 1. degree q < j - d
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
degree (q * u + Polynomial.smult m r) = degree q + degree u
[PROOF STEP]
have "degree q = degree g - degree u"
[PROOF STATE]
proof (prove)
using this:
degree (q * u + Polynomial.smult m r) = degree q + degree u

goal (1 subgoal):
 1. degree q = degree g - degree u
[PROOF STEP]
using g1
[PROOF STATE]
proof (prove)
using this:
degree (q * u + Polynomial.smult m r) = degree q + degree u
g = q * u + Polynomial.smult m r

goal (1 subgoal):
 1. degree q = degree g - degree u
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
degree q = degree g - degree u

goal (1 subgoal):
 1. degree q < j - d
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
degree q = degree g - degree u

goal (1 subgoal):
 1. degree q < j - d
[PROOF STEP]
using j j2 \<open>degree (q * u) = degree q + degree u\<close> u
[PROOF STATE]
proof (prove)
using this:
degree q = degree g - degree u
degree (q * u + Polynomial.smult m r) < j
degree (q * u + Polynomial.smult m r) = degree (q * u)
degree (q * u) = degree q + degree u
degree u = d

goal (1 subgoal):
 1. degree q < j - d
[PROOF STEP]
by linarith
[PROOF STATE]
proof (state)
this:
degree q < j - d

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in LCD) foldD_insert:
  assumes "finite A" "x \<notin> A" "x \<in> B" "e \<in> D" "A \<subseteq> B"
  shows "foldD D f e (insert x A) = f x (foldD D f e A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. foldD D (\<cdot>) e (insert x A) = x \<cdot> foldD D (\<cdot>) e A
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. foldD D (\<cdot>) e (insert x A) = x \<cdot> foldD D (\<cdot>) e A
[PROOF STEP]
have "(THE v. \<exists>y. (A, y) \<in> foldSetD D (\<cdot>) e \<and> v = x \<cdot> y) = x \<cdot> (THE y. (A, y) \<in> foldSetD D (\<cdot>) e)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (THE v. \<exists>y. (A, y) \<in> foldSetD D (\<cdot>) e \<and> v = x \<cdot> y) = x \<cdot> (THE y. (A, y) \<in> foldSetD D (\<cdot>) e)
[PROOF STEP]
by (rule the_equality) (use assms foldD_def foldD_equality foldD_def finite_imp_foldSetD in \<open>metis+\<close>)
[PROOF STATE]
proof (state)
this:
(THE v. \<exists>y. (A, y) \<in> foldSetD D (\<cdot>) e \<and> v = x \<cdot> y) = x \<cdot> (THE y. (A, y) \<in> foldSetD D (\<cdot>) e)

goal (1 subgoal):
 1. foldD D (\<cdot>) e (insert x A) = x \<cdot> foldD D (\<cdot>) e A
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(THE v. \<exists>y. (A, y) \<in> foldSetD D (\<cdot>) e \<and> v = x \<cdot> y) = x \<cdot> (THE y. (A, y) \<in> foldSetD D (\<cdot>) e)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(THE v. \<exists>y. (A, y) \<in> foldSetD D (\<cdot>) e \<and> v = x \<cdot> y) = x \<cdot> (THE y. (A, y) \<in> foldSetD D (\<cdot>) e)

goal (1 subgoal):
 1. foldD D (\<cdot>) e (insert x A) = x \<cdot> foldD D (\<cdot>) e A
[PROOF STEP]
unfolding foldD_def
[PROOF STATE]
proof (prove)
using this:
(THE v. \<exists>y. (A, y) \<in> foldSetD D (\<cdot>) e \<and> v = x \<cdot> y) = x \<cdot> (THE y. (A, y) \<in> foldSetD D (\<cdot>) e)

goal (1 subgoal):
 1. (THE xa. (insert x A, xa) \<in> foldSetD D (\<cdot>) e) = x \<cdot> (THE x. (A, x) \<in> foldSetD D (\<cdot>) e)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
(THE v. \<exists>y. (A, y) \<in> foldSetD D (\<cdot>) e \<and> v = x \<cdot> y) = x \<cdot> (THE y. (A, y) \<in> foldSetD D (\<cdot>) e)
finite A
x \<notin> A
x \<in> B
e \<in> D
A \<subseteq> B

goal (1 subgoal):
 1. (THE xa. (insert x A, xa) \<in> foldSetD D (\<cdot>) e) = x \<cdot> (THE x. (A, x) \<in> foldSetD D (\<cdot>) e)
[PROOF STEP]
by (simp add: foldD_insert_aux)
[PROOF STATE]
proof (state)
this:
foldD D (\<cdot>) e (insert x A) = x \<cdot> foldD D (\<cdot>) e A

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma gmap_gappend[simp]: "gmap f (a @\<^sub>g b) = gmap f a @\<^sub>g gmap f b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gmap f (a @\<^sub>g b) = gmap f a @\<^sub>g gmap f b
[PROOF STEP]
by (unfold gappend_def, induct a, induct b, simp+)


[STATEMENT]
lemma HierAuto_EmptySet:
 "((@x. True),{Abs_seqauto ({@x. True}, (@x. True), {}, {})}, {},
  Map.empty ( @x. True \<mapsto> {})) \<in> {(D,F,E,G) | D F E G. HierAuto D F E G}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (SOME x. True, {Abs_seqauto ({SOME x. True}, SOME x. True, {}, {})}, {}, [SOME x. True \<mapsto> {}]) \<in> {(D, F, E, G) |D F E G. HierAuto D F E G}
[PROOF STEP]
apply (unfold HierAuto_def IsCompFun_def Root_def RootEx_def MutuallyDistinct_def
           OneAncestor_def NoCycles_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (SOME x. True, {Abs_seqauto ({SOME x. True}, SOME x. True, {}, {})}, {}, [SOME x. True \<mapsto> {}]) \<in> {(D, F, E, G) |D F E G. \<Union> (SAEvents ` F) \<subseteq> E \<and> (\<forall>a\<in>F. \<forall>b\<in>F. a \<noteq> b \<longrightarrow> States a \<inter> States b = {}) \<and> finite F \<and> dom G = \<Union> (States ` F) \<and> \<Union> (ran G) = F - {SOME A. A \<in> F \<and> A \<notin> \<Union> (ran G)} \<and> (\<exists>!A. A \<in> F \<and> A \<notin> \<Union> (ran G)) \<and> (\<forall>A\<in>F - {SOME A. A \<in> F \<and> A \<notin> \<Union> (ran G)}. \<exists>!s. s \<in> \<Union> (States ` (F - {A})) \<and> A \<in> the (G s)) \<and> (\<forall>S\<in>Pow (\<Union> (States ` F)). S \<noteq> {} \<longrightarrow> (\<exists>s\<in>S. S \<inter> \<Union> (States ` the (G s)) = {}))}
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma SAStates_notmem_Chi [simp]:
  "\<lbrakk> S \<in> States SA; T \<in> States SA;
     SA \<in> SAs A \<rbrakk> \<Longrightarrow> T \<notin> Chi A S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>S \<in> States SA; T \<in> States SA; SA \<in> SAs A\<rbrakk> \<Longrightarrow> T \<notin> Chi A S
[PROOF STEP]
apply (unfold Chi_def restrict_def, auto)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>SAa. \<lbrakk>S \<in> States SA; T \<in> States SA; SA \<in> SAs A; S \<in> HAStates A; SAa \<in> the (CompFun A S); T \<in> States SAa\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>S \<in> States SA; T \<in> States SA; SA \<in> SAs A; S \<notin> HAStates A; T \<in> (SOME y. True)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (rename_tac SAA)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>SAA. \<lbrakk>S \<in> States SA; T \<in> States SA; SA \<in> SAs A; S \<in> HAStates A; SAA \<in> the (CompFun A S); T \<in> States SAA\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>S \<in> States SA; T \<in> States SA; SA \<in> SAs A; S \<notin> HAStates A; T \<in> (SOME y. True)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (cut_tac HA="A" in MutuallyDistinct_HA)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>SAA. \<lbrakk>S \<in> States SA; T \<in> States SA; SA \<in> SAs A; S \<in> HAStates A; SAA \<in> the (CompFun A S); T \<in> States SAA; MutuallyDistinct (SAs A)\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>S \<in> States SA; T \<in> States SA; SA \<in> SAs A; S \<notin> HAStates A; T \<in> (SOME y. True)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (unfold MutuallyDistinct_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>SAA. \<lbrakk>S \<in> States SA; T \<in> States SA; SA \<in> SAs A; S \<in> HAStates A; SAA \<in> the (CompFun A S); T \<in> States SAA; \<forall>a\<in>SAs A. \<forall>b\<in>SAs A. a \<noteq> b \<longrightarrow> States a \<inter> States b = {}\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>S \<in> States SA; T \<in> States SA; SA \<in> SAs A; S \<notin> HAStates A; T \<in> (SOME y. True)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (erule_tac x="SAA" in ballE)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>SAA. \<lbrakk>S \<in> States SA; T \<in> States SA; SA \<in> SAs A; S \<in> HAStates A; SAA \<in> the (CompFun A S); T \<in> States SAA; \<forall>b\<in>SAs A. SAA \<noteq> b \<longrightarrow> States SAA \<inter> States b = {}\<rbrakk> \<Longrightarrow> False
 2. \<And>SAA. \<lbrakk>S \<in> States SA; T \<in> States SA; SA \<in> SAs A; S \<in> HAStates A; SAA \<in> the (CompFun A S); T \<in> States SAA; SAA \<notin> SAs A\<rbrakk> \<Longrightarrow> False
 3. \<lbrakk>S \<in> States SA; T \<in> States SA; SA \<in> SAs A; S \<notin> HAStates A; T \<in> (SOME y. True)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (erule_tac x="SA" in ballE)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>SAA. \<lbrakk>S \<in> States SA; T \<in> States SA; SA \<in> SAs A; S \<in> HAStates A; SAA \<in> the (CompFun A S); T \<in> States SAA; SAA \<noteq> SA \<longrightarrow> States SAA \<inter> States SA = {}\<rbrakk> \<Longrightarrow> False
 2. \<And>SAA. \<lbrakk>S \<in> States SA; T \<in> States SA; SA \<in> SAs A; S \<in> HAStates A; SAA \<in> the (CompFun A S); T \<in> States SAA; SA \<notin> SAs A\<rbrakk> \<Longrightarrow> False
 3. \<And>SAA. \<lbrakk>S \<in> States SA; T \<in> States SA; SA \<in> SAs A; S \<in> HAStates A; SAA \<in> the (CompFun A S); T \<in> States SAA; SAA \<notin> SAs A\<rbrakk> \<Longrightarrow> False
 4. \<lbrakk>S \<in> States SA; T \<in> States SA; SA \<in> SAs A; S \<notin> HAStates A; T \<in> (SOME y. True)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>S \<in> States SA; T \<in> States SA; SA \<in> SAs A; S \<notin> HAStates A; T \<in> (SOME y. True)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (unfold HAStates_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>S \<in> States SA; T \<in> States SA; SA \<in> SAs A; S \<notin> \<Union> (States ` SAs A); T \<in> (SOME y. True)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma smc_FUNCT_components:
  shows "smc_FUNCT \<alpha> \<AA> \<BB>\<lparr>Obj\<rparr> = cf_maps \<alpha> \<AA> \<BB>"
    and "smc_FUNCT \<alpha> \<AA> \<BB>\<lparr>Arr\<rparr> = ntcf_arrows \<alpha> \<AA> \<BB>"
    and "smc_FUNCT \<alpha> \<AA> \<BB>\<lparr>Dom\<rparr> = (\<lambda>\<NN>\<in>\<^sub>\<circ>ntcf_arrows \<alpha> \<AA> \<BB>. \<NN>\<lparr>NTDom\<rparr>)"
    and "smc_FUNCT \<alpha> \<AA> \<BB>\<lparr>Cod\<rparr> = (\<lambda>\<NN>\<in>\<^sub>\<circ>ntcf_arrows \<alpha> \<AA> \<BB>. \<NN>\<lparr>NTCod\<rparr>)"
    and "smc_FUNCT \<alpha> \<AA> \<BB>\<lparr>Comp\<rparr> =
      (\<lambda>\<MM>\<NN>\<in>\<^sub>\<circ>composable_arrs (dg_FUNCT \<alpha> \<AA> \<BB>). \<MM>\<NN>\<lparr>0\<rparr> \<bullet>\<^sub>N\<^sub>T\<^sub>C\<^sub>F\<^bsub>\<AA>,\<BB>\<^esub> \<MM>\<NN>\<lparr>1\<^sub>\<nat>\<rparr>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (smc_FUNCT \<alpha> \<AA> \<BB>\<lparr>Obj\<rparr> = cf_maps \<alpha> \<AA> \<BB> &&& smc_FUNCT \<alpha> \<AA> \<BB>\<lparr>Arr\<rparr> = ntcf_arrows \<alpha> \<AA> \<BB>) &&& smc_FUNCT \<alpha> \<AA> \<BB>\<lparr>Dom\<rparr> = (\<lambda>\<NN>\<in>\<^sub>\<circ>ntcf_arrows \<alpha> \<AA> \<BB>. \<NN>\<lparr>NTDom\<rparr>) &&& smc_FUNCT \<alpha> \<AA> \<BB>\<lparr>Cod\<rparr> = (\<lambda>\<NN>\<in>\<^sub>\<circ>ntcf_arrows \<alpha> \<AA> \<BB>. \<NN>\<lparr>NTCod\<rparr>) &&& smc_FUNCT \<alpha> \<AA> \<BB>\<lparr>Comp\<rparr> = (\<lambda>\<MM>\<NN>\<in>\<^sub>\<circ>composable_arrs (dg_FUNCT \<alpha> \<AA> \<BB>). \<MM>\<NN>\<lparr>[]\<^sub>\<circ>\<rparr> \<bullet>\<^sub>N\<^sub>T\<^sub>C\<^sub>F\<^bsub>\<AA>,\<BB>\<^esub> \<MM>\<NN>\<lparr>1\<^sub>\<nat>\<rparr>)
[PROOF STEP]
unfolding smc_FUNCT_def dg_field_simps
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ([cf_maps \<alpha> \<AA> \<BB>, ntcf_arrows \<alpha> \<AA> \<BB>, \<lambda>\<NN>\<in>\<^sub>\<circ>ntcf_arrows \<alpha> \<AA> \<BB>. \<NN>\<lparr>NTDom\<rparr>, \<lambda>\<NN>\<in>\<^sub>\<circ>ntcf_arrows \<alpha> \<AA> \<BB>. \<NN>\<lparr>NTCod\<rparr>, \<lambda>\<MM>\<NN>\<in>\<^sub>\<circ>composable_arrs (dg_FUNCT \<alpha> \<AA> \<BB>). \<MM>\<NN>\<lparr>[]\<^sub>\<circ>\<rparr> \<bullet>\<^sub>N\<^sub>T\<^sub>C\<^sub>F\<^bsub>\<AA>,\<BB>\<^esub> \<MM>\<NN>\<lparr>1\<^sub>\<nat>\<rparr>]\<^sub>\<circ>\<lparr>[]\<^sub>\<circ>\<rparr> = cf_maps \<alpha> \<AA> \<BB> &&& [cf_maps \<alpha> \<AA> \<BB>, ntcf_arrows \<alpha> \<AA> \<BB>, \<lambda>\<NN>\<in>\<^sub>\<circ>ntcf_arrows \<alpha> \<AA> \<BB>. \<NN>\<lparr>NTDom\<rparr>, \<lambda>\<NN>\<in>\<^sub>\<circ>ntcf_arrows \<alpha> \<AA> \<BB>. \<NN>\<lparr>NTCod\<rparr>, \<lambda>\<MM>\<NN>\<in>\<^sub>\<circ>composable_arrs (dg_FUNCT \<alpha> \<AA> \<BB>). \<MM>\<NN>\<lparr>[]\<^sub>\<circ>\<rparr> \<bullet>\<^sub>N\<^sub>T\<^sub>C\<^sub>F\<^bsub>\<AA>,\<BB>\<^esub> \<MM>\<NN>\<lparr>1\<^sub>\<nat>\<rparr>]\<^sub>\<circ>\<lparr>1\<^sub>\<nat>\<rparr> = ntcf_arrows \<alpha> \<AA> \<BB>) &&& [cf_maps \<alpha> \<AA> \<BB>, ntcf_arrows \<alpha> \<AA> \<BB>, \<lambda>\<NN>\<in>\<^sub>\<circ>ntcf_arrows \<alpha> \<AA> \<BB>. \<NN>\<lparr>NTDom\<rparr>, \<lambda>\<NN>\<in>\<^sub>\<circ>ntcf_arrows \<alpha> \<AA> \<BB>. \<NN>\<lparr>NTCod\<rparr>, \<lambda>\<MM>\<NN>\<in>\<^sub>\<circ>composable_arrs (dg_FUNCT \<alpha> \<AA> \<BB>). \<MM>\<NN>\<lparr>[]\<^sub>\<circ>\<rparr> \<bullet>\<^sub>N\<^sub>T\<^sub>C\<^sub>F\<^bsub>\<AA>,\<BB>\<^esub> \<MM>\<NN>\<lparr>1\<^sub>\<nat>\<rparr>]\<^sub>\<circ>\<lparr>2\<^sub>\<nat>\<rparr> = (\<lambda>\<NN>\<in>\<^sub>\<circ>ntcf_arrows \<alpha> \<AA> \<BB>. \<NN>\<lparr>NTDom\<rparr>) &&& [cf_maps \<alpha> \<AA> \<BB>, ntcf_arrows \<alpha> \<AA> \<BB>, \<lambda>\<NN>\<in>\<^sub>\<circ>ntcf_arrows \<alpha> \<AA> \<BB>. \<NN>\<lparr>NTDom\<rparr>, \<lambda>\<NN>\<in>\<^sub>\<circ>ntcf_arrows \<alpha> \<AA> \<BB>. \<NN>\<lparr>NTCod\<rparr>, \<lambda>\<MM>\<NN>\<in>\<^sub>\<circ>composable_arrs (dg_FUNCT \<alpha> \<AA> \<BB>). \<MM>\<NN>\<lparr>[]\<^sub>\<circ>\<rparr> \<bullet>\<^sub>N\<^sub>T\<^sub>C\<^sub>F\<^bsub>\<AA>,\<BB>\<^esub> \<MM>\<NN>\<lparr>1\<^sub>\<nat>\<rparr>]\<^sub>\<circ>\<lparr>3\<^sub>\<nat>\<rparr> = (\<lambda>\<NN>\<in>\<^sub>\<circ>ntcf_arrows \<alpha> \<AA> \<BB>. \<NN>\<lparr>NTCod\<rparr>) &&& [cf_maps \<alpha> \<AA> \<BB>, ntcf_arrows \<alpha> \<AA> \<BB>, \<lambda>\<NN>\<in>\<^sub>\<circ>ntcf_arrows \<alpha> \<AA> \<BB>. \<NN>\<lparr>NTDom\<rparr>, \<lambda>\<NN>\<in>\<^sub>\<circ>ntcf_arrows \<alpha> \<AA> \<BB>. \<NN>\<lparr>NTCod\<rparr>, \<lambda>\<MM>\<NN>\<in>\<^sub>\<circ>composable_arrs (dg_FUNCT \<alpha> \<AA> \<BB>). \<MM>\<NN>\<lparr>[]\<^sub>\<circ>\<rparr> \<bullet>\<^sub>N\<^sub>T\<^sub>C\<^sub>F\<^bsub>\<AA>,\<BB>\<^esub> \<MM>\<NN>\<lparr>1\<^sub>\<nat>\<rparr>]\<^sub>\<circ>\<lparr>4\<^sub>\<nat>\<rparr> = (\<lambda>\<MM>\<NN>\<in>\<^sub>\<circ>composable_arrs (dg_FUNCT \<alpha> \<AA> \<BB>). \<MM>\<NN>\<lparr>[]\<^sub>\<circ>\<rparr> \<bullet>\<^sub>N\<^sub>T\<^sub>C\<^sub>F\<^bsub>\<AA>,\<BB>\<^esub> \<MM>\<NN>\<lparr>1\<^sub>\<nat>\<rparr>)
[PROOF STEP]
by (simp_all add: nat_omega_simps)


[STATEMENT]
lemma memo_lookup:
  "bind (memo f x) (\<lambda>i. bind (lookup x) (g i)) = bind (memo f x) (\<lambda>i. g i i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bind (memo f x) (\<lambda>i. bind (lookup x) (g i)) = bind (memo f x) (\<lambda>i. g i i)
[PROOF STEP]
apply(simp cong del: option.case_cong_weak add: lookup_def memo_def bind_get option.case_distrib[where h="\<lambda>x. bind x _"] bind_assoc bind_update return_bind update_get o_def get_const)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. get (\<lambda>s. case s x of None \<Rightarrow> bind (f x) (\<lambda>y. update (\<lambda>m. m(x \<mapsto> y)) (g y y)) | Some xa \<Rightarrow> get (\<lambda>s. case s x of None \<Rightarrow> bind fail (g xa) | Some x \<Rightarrow> g xa x)) = get (\<lambda>s. case s x of None \<Rightarrow> bind (f x) (\<lambda>y. update (\<lambda>m. m(x \<mapsto> y)) (g y y)) | Some x \<Rightarrow> g x x)
[PROOF STEP]
apply(subst (3) get_const[symmetric])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. get (\<lambda>s. case s x of None \<Rightarrow> get (\<lambda>_. bind (f x) (\<lambda>y. update (\<lambda>m. m(x \<mapsto> y)) (g y y))) | Some xa \<Rightarrow> get (\<lambda>s. case s x of None \<Rightarrow> bind fail (g xa) | Some x \<Rightarrow> g xa x)) = get (\<lambda>s. case s x of None \<Rightarrow> bind (f x) (\<lambda>y. update (\<lambda>m. m(x \<mapsto> y)) (g y y)) | Some x \<Rightarrow> g x x)
[PROOF STEP]
apply(subst option.case_distrib[where h=get, symmetric])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. get (\<lambda>s. get (case s x of None \<Rightarrow> \<lambda>_. bind (f x) (\<lambda>y. update (\<lambda>m. m(x \<mapsto> y)) (g y y)) | Some xa \<Rightarrow> \<lambda>s. case s x of None \<Rightarrow> bind fail (g xa) | Some x \<Rightarrow> g xa x)) = get (\<lambda>s. case s x of None \<Rightarrow> bind (f x) (\<lambda>y. update (\<lambda>m. m(x \<mapsto> y)) (g y y)) | Some x \<Rightarrow> g x x)
[PROOF STEP]
apply(simp add: get_get case_option_apply cong: option.case_cong)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma eval_reverse:
  "eval E (Var x) = E x"
  "eval E (Const i) = return i"
  "eval E (Plus e1 e2) = bind (eval E e2) (\<lambda>j. bind (eval E e1) (\<lambda>i. return (i + j)))"
  "eval E (Div e1 e2) = bind (eval E e2) (\<lambda>j. bind (eval E e1) (\<lambda>i. if j = 0 then fail else return (i div j)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (eval E (Var x) = E x &&& eval E (Const i) = return i) &&& eval E (Plus e1 e2) = bind (eval E e2) (\<lambda>j. bind (eval E e1) (\<lambda>i. return (i + j))) &&& eval E (Div e1 e2) = bind (eval E e2) (\<lambda>j. bind (eval E e1) (\<lambda>i. if j = 0 then fail else return (i div j)))
[PROOF STEP]
by(simp; rule bind_commute)+


[STATEMENT]
lemma HPhase1or2ReadThen_HInv4a2:
  "\<lbrakk> HPhase1or2ReadThen s s' p d r; HInv4a2 s q \<rbrakk> \<Longrightarrow> HInv4a2 s' q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>HPhase1or2ReadThen s s' p d r; HInv4a2 s q\<rbrakk> \<Longrightarrow> HInv4a2 s' q
[PROOF STEP]
by(auto simp add: Phase1or2ReadThen_def HInv4a2_def)


[STATEMENT]
lemma HEndPhase1_HInv4a_p:
  assumes act: "HEndPhase1 s s' p"
  and inv: "HInv4a s p"
  and inv2a: "Inv2a s"
  shows "HInv4a s' p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. HInv4a s' p
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. HInv4a s' p
[PROOF STEP]
from act
[PROOF STATE]
proof (chain)
picking this:
HEndPhase1 s s' p
[PROOF STEP]
have phase: "0 < phase s p"
[PROOF STATE]
proof (prove)
using this:
HEndPhase1 s s' p

goal (1 subgoal):
 1. 0 < phase s p
[PROOF STEP]
by(auto simp add: EndPhase1_def)
[PROOF STATE]
proof (state)
this:
0 < phase s p

goal (1 subgoal):
 1. HInv4a s' p
[PROOF STEP]
with act inv inv2a
[PROOF STATE]
proof (chain)
picking this:
HEndPhase1 s s' p
HInv4a s p
Inv2a s
0 < phase s p
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
HEndPhase1 s s' p
HInv4a s p
Inv2a s
0 < phase s p

goal (1 subgoal):
 1. HInv4a s' p
[PROOF STEP]
by(auto simp del: HEndPhase1_def simp  add: HInv4a_def
               elim: HEndPhase1_HInv4a1 HEndPhase1_HInv4a2)
[PROOF STATE]
proof (state)
this:
HInv4a s' p

goal:
No subgoals!
[PROOF STEP]
qed