[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