[STATEMENT]
lemma Q_inf_reach_state_rule:
  assumes "(p, q) \<in> Q_inf \" and "\<Q> \ |\<subseteq>| ta_reachable \"
  shows "\<exists> ss ts f C. q |\<in>| ta_der \ (More (None, Some f) ss C ts)\<langle>Var p\<rangle> \<and> ground_ctxt (More (None, Some f) ss C ts)"
    (is "\<exists> ss ts f C. ?P ss ts f C q p")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>ss ts f C. q |\<in>| ta_der \ (More (lift_None_Some f) ss C ts)\<langle>Var p\<rangle> \<and> ground_ctxt (More (lift_None_Some f) ss C ts)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
(p, q) \<in> Q_inf \
\<Q> \ |\<subseteq>| ta_reachable \

goal (1 subgoal):
 1. \<exists>ss ts f C. q |\<in>| ta_der \ (More (lift_None_Some f) ss C ts)\<langle>Var p\<rangle> \<and> ground_ctxt (More (lift_None_Some f) ss C ts)
[PROOF STEP]
proof (induct)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>p q r. \<lbrakk>(p, q) \<in> Q_inf \; \<Q> \ |\<subseteq>| ta_reachable \ \<Longrightarrow> \<exists>ss ts f C. q |\<in>| ta_der \ (More (lift_None_Some f) ss C ts)\<langle>Var p\<rangle> \<and> ground_ctxt (More (lift_None_Some f) ss C ts); (q, r) \<in> Q_inf \; \<Q> \ |\<subseteq>| ta_reachable \ \<Longrightarrow> \<exists>ss ts f C. r |\<in>| ta_der \ (More (lift_None_Some f) ss C ts)\<langle>Var q\<rangle> \<and> ground_ctxt (More (lift_None_Some f) ss C ts); \<Q> \ |\<subseteq>| ta_reachable \\<rbrakk> \<Longrightarrow> \<exists>ss ts f C. r |\<in>| ta_der \ (More (lift_None_Some f) ss C ts)\<langle>Var p\<rangle> \<and> ground_ctxt (More (lift_None_Some f) ss C ts)
 2. \<And>f qs q i. \<lbrakk>lift_None_Some f qs \<rightarrow> q |\<in>| rules \; i < length qs; \<Q> \ |\<subseteq>| ta_reachable \\<rbrakk> \<Longrightarrow> \<exists>ss ts f C. q |\<in>| ta_der \ (More (lift_None_Some f) ss C ts)\<langle>Var (qs ! i)\<rangle> \<and> ground_ctxt (More (lift_None_Some f) ss C ts)
 3. \<And>p q r. \<lbrakk>(p, q) \<in> Q_inf \; \<Q> \ |\<subseteq>| ta_reachable \ \<Longrightarrow> \<exists>ss ts f C. q |\<in>| ta_der \ (More (lift_None_Some f) ss C ts)\<langle>Var p\<rangle> \<and> ground_ctxt (More (lift_None_Some f) ss C ts); (q, r) |\<in>| eps \; \<Q> \ |\<subseteq>| ta_reachable \\<rbrakk> \<Longrightarrow> \<exists>ss ts f C. r |\<in>| ta_der \ (More (lift_None_Some f) ss C ts)\<langle>Var p\<rangle> \<and> ground_ctxt (More (lift_None_Some f) ss C ts)
[PROOF STEP]
case (trans p q r)
[PROOF STATE]
proof (state)
this:
(p, q) \<in> Q_inf \
\<Q> \ |\<subseteq>| ta_reachable \ \<Longrightarrow> \<exists>ss ts f C. q |\<in>| ta_der \ (More (lift_None_Some f) ss C ts)\<langle>Var p\<rangle> \<and> ground_ctxt (More (lift_None_Some f) ss C ts)
(q, r) \<in> Q_inf \
\<Q> \ |\<subseteq>| ta_reachable \ \<Longrightarrow> \<exists>ss ts f C. r |\<in>| ta_der \ (More (lift_None_Some f) ss C ts)\<langle>Var q\<rangle> \<and> ground_ctxt (More (lift_None_Some f) ss C ts)
\<Q> \ |\<subseteq>| ta_reachable \

goal (3 subgoals):
 1. \<And>p q r. \<lbrakk>(p, q) \<in> Q_inf \; \<Q> \ |\<subseteq>| ta_reachable \ \<Longrightarrow> \<exists>ss ts f C. q |\<in>| ta_der \ (More (lift_None_Some f) ss C ts)\<langle>Var p\<rangle> \<and> ground_ctxt (More (lift_None_Some f) ss C ts); (q, r) \<in> Q_inf \; \<Q> \ |\<subseteq>| ta_reachable \ \<Longrightarrow> \<exists>ss ts f C. r |\<in>| ta_der \ (More (lift_None_Some f) ss C ts)\<langle>Var q\<rangle> \<and> ground_ctxt (More (lift_None_Some f) ss C ts); \<Q> \ |\<subseteq>| ta_reachable \\<rbrakk> \<Longrightarrow> \<exists>ss ts f C. r |\<in>| ta_der \ (More (lift_None_Some f) ss C ts)\<langle>Var p\<rangle> \<and> ground_ctxt (More (lift_None_Some f) ss C ts)
 2. \<And>f qs q i. \<lbrakk>lift_None_Some f qs \<rightarrow> q |\<in>| rules \; i < length qs; \<Q> \ |\<subseteq>| ta_reachable \\<rbrakk> \<Longrightarrow> \<exists>ss ts f C. q |\<in>| ta_der \ (More (lift_None_Some f) ss C ts)\<langle>Var (qs ! i)\<rangle> \<and> ground_ctxt (More (lift_None_Some f) ss C ts)
 3. \<And>p q r. \<lbrakk>(p, q) \<in> Q_inf \; \<Q> \ |\<subseteq>| ta_reachable \ \<Longrightarrow> \<exists>ss ts f C. q |\<in>| ta_der \ (More (lift_None_Some f) ss C ts)\<langle>Var p\<rangle> \<and> ground_ctxt (More (lift_None_Some f) ss C ts); (q, r) |\<in>| eps \; \<Q> \ |\<subseteq>| ta_reachable \\<rbrakk> \<Longrightarrow> \<exists>ss ts f C. r |\<in>| ta_der \ (More (lift_None_Some f) ss C ts)\<langle>Var p\<rangle> \<and> ground_ctxt (More (lift_None_Some f) ss C ts)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(p, q) \<in> Q_inf \
\<Q> \ |\<subseteq>| ta_reachable \ \<Longrightarrow> \<exists>ss ts f C. q |\<in>| ta_der \ (More (lift_None_Some f) ss C ts)\<langle>Var p\<rangle> \<and> ground_ctxt (More (lift_None_Some f) ss C ts)
(q, r) \<in> Q_inf \
\<Q> \ |\<subseteq>| ta_reachable \ \<Longrightarrow> \<exists>ss ts f C. r |\<in>| ta_der \ (More (lift_None_Some f) ss C ts)\<langle>Var q\<rangle> \<and> ground_ctxt (More (lift_None_Some f) ss C ts)
\<Q> \ |\<subseteq>| ta_reachable \
[PROOF STEP]
obtain f1 f2 ss1 ts1 ss2 ts2 C1 C2 where
    C: "?P ss1 ts1 f1 C1 q p" "?P ss2 ts2 f2 C2 r q"
[PROOF STATE]
proof (prove)
using this:
(p, q) \<in> Q_inf \
\<Q> \ |\<subseteq>| ta_reachable \ \<Longrightarrow> \<exists>ss ts f C. q |\<in>| ta_der \ (More (lift_None_Some f) ss C ts)\<langle>Var p\<rangle> \<and> ground_ctxt (More (lift_None_Some f) ss C ts)
(q, r) \<in> Q_inf \
\<Q> \ |\<subseteq>| ta_reachable \ \<Longrightarrow> \<exists>ss ts f C. r |\<in>| ta_der \ (More (lift_None_Some f) ss C ts)\<langle>Var q\<rangle> \<and> ground_ctxt (More (lift_None_Some f) ss C ts)
\<Q> \ |\<subseteq>| ta_reachable \

goal (1 subgoal):
 1. (\<And>f1 ss1 C1 ts1 f2 ss2 C2 ts2. \<lbrakk>q |\<in>| ta_der \ (More (lift_None_Some f1) ss1 C1 ts1)\<langle>Var p\<rangle> \<and> ground_ctxt (More (lift_None_Some f1) ss1 C1 ts1); r |\<in>| ta_der \ (More (lift_None_Some f2) ss2 C2 ts2)\<langle>Var q\<rangle> \<and> ground_ctxt (More (lift_None_Some f2) ss2 C2 ts2)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
q |\<in>| ta_der \ (More (lift_None_Some f1) ss1 C1 ts1)\<langle>Var p\<rangle> \<and> ground_ctxt (More (lift_None_Some f1) ss1 C1 ts1)
r |\<in>| ta_der \ (More (lift_None_Some f2) ss2 C2 ts2)\<langle>Var q\<rangle> \<and> ground_ctxt (More (lift_None_Some f2) ss2 C2 ts2)

goal (3 subgoals):
 1. \<And>p q r. \<lbrakk>(p, q) \<in> Q_inf \; \<Q> \ |\<subseteq>| ta_reachable \ \<Longrightarrow> \<exists>ss ts f C. q |\<in>| ta_der \ (More (lift_None_Some f) ss C ts)\<langle>Var p\<rangle> \<and> ground_ctxt (More (lift_None_Some f) ss C ts); (q, r) \<in> Q_inf \; \<Q> \ |\<subseteq>| ta_reachable \ \<Longrightarrow> \<exists>ss ts f C. r |\<in>| ta_der \ (More (lift_None_Some f) ss C ts)\<langle>Var q\<rangle> \<and> ground_ctxt (More (lift_None_Some f) ss C ts); \<Q> \ |\<subseteq>| ta_reachable \\<rbrakk> \<Longrightarrow> \<exists>ss ts f C. r |\<in>| ta_der \ (More (lift_None_Some f) ss C ts)\<langle>Var p\<rangle> \<and> ground_ctxt (More (lift_None_Some f) ss C ts)
 2. \<And>f qs q i. \<lbrakk>lift_None_Some f qs \<rightarrow> q |\<in>| rules \; i < length qs; \<Q> \ |\<subseteq>| ta_reachable \\<rbrakk> \<Longrightarrow> \<exists>ss ts f C. q |\<in>| ta_der \ (More (lift_None_Some f) ss C ts)\<langle>Var (qs ! i)\<rangle> \<and> ground_ctxt (More (lift_None_Some f) ss C ts)
 3. \<And>p q r. \<lbrakk>(p, q) \<in> Q_inf \; \<Q> \ |\<subseteq>| ta_reachable \ \<Longrightarrow> \<exists>ss ts f C. q |\<in>| ta_der \ (More (lift_None_Some f) ss C ts)\<langle>Var p\<rangle> \<and> ground_ctxt (More (lift_None_Some f) ss C ts); (q, r) |\<in>| eps \; \<Q> \ |\<subseteq>| ta_reachable \\<rbrakk> \<Longrightarrow> \<exists>ss ts f C. r |\<in>| ta_der \ (More (lift_None_Some f) ss C ts)\<langle>Var p\<rangle> \<and> ground_ctxt (More (lift_None_Some f) ss C ts)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
q |\<in>| ta_der \ (More (lift_None_Some f1) ss1 C1 ts1)\<langle>Var p\<rangle> \<and> ground_ctxt (More (lift_None_Some f1) ss1 C1 ts1)
r |\<in>| ta_der \ (More (lift_None_Some f2) ss2 C2 ts2)\<langle>Var q\<rangle> \<and> ground_ctxt (More (lift_None_Some f2) ss2 C2 ts2)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
q |\<in>| ta_der \ (More (lift_None_Some f1) ss1 C1 ts1)\<langle>Var p\<rangle> \<and> ground_ctxt (More (lift_None_Some f1) ss1 C1 ts1)
r |\<in>| ta_der \ (More (lift_None_Some f2) ss2 C2 ts2)\<langle>Var q\<rangle> \<and> ground_ctxt (More (lift_None_Some f2) ss2 C2 ts2)

goal (1 subgoal):
 1. \<exists>ss ts f C. r |\<in>| ta_der \ (More (lift_None_Some f) ss C ts)\<langle>Var p\<rangle> \<and> ground_ctxt (More (lift_None_Some f) ss C ts)
[PROOF STEP]
apply (rule_tac x = "ss2" in exI, rule_tac x = "ts2" in exI, rule_tac x = "f2" in exI,
        rule_tac x = "C2 \<circ>\<^sub>c (More (None, Some f1) ss1 C1 ts1)" in exI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>q |\<in>| ta_der \ (More (lift_None_Some f1) ss1 C1 ts1)\<langle>Var p\<rangle> \<and> ground_ctxt (More (lift_None_Some f1) ss1 C1 ts1); r |\<in>| ta_der \ (More (lift_None_Some f2) ss2 C2 ts2)\<langle>Var q\<rangle> \<and> ground_ctxt (More (lift_None_Some f2) ss2 C2 ts2); q |\<in>| ta_der \ (More (lift_None_Some f1) ss1 C1 ts1)\<langle>Var p\<rangle> \<and> ground_ctxt (More (lift_None_Some f1) ss1 C1 ts1); r |\<in>| ta_der \ (More (lift_None_Some f2) ss2 C2 ts2)\<langle>Var q\<rangle> \<and> ground_ctxt (More (lift_None_Some f2) ss2 C2 ts2); q |\<in>| ta_der \ (More (lift_None_Some f1) ss1 C1 ts1)\<langle>Var p\<rangle> \<and> ground_ctxt (More (lift_None_Some f1) ss1 C1 ts1); r |\<in>| ta_der \ (More (lift_None_Some f2) ss2 C2 ts2)\<langle>Var q\<rangle> \<and> ground_ctxt (More (lift_None_Some f2) ss2 C2 ts2); q |\<in>| ta_der \ (More (lift_None_Some f1) ss1 C1 ts1)\<langle>Var p\<rangle> \<and> ground_ctxt (More (lift_None_Some f1) ss1 C1 ts1); r |\<in>| ta_der \ (More (lift_None_Some f2) ss2 C2 ts2)\<langle>Var q\<rangle> \<and> ground_ctxt (More (lift_None_Some f2) ss2 C2 ts2)\<rbrakk> \<Longrightarrow> r |\<in>| ta_der \ (More (lift_None_Some f2) ss2 (C2 \<circ>\<^sub>c More (lift_None_Some f1) ss1 C1 ts1) ts2)\<langle>Var p\<rangle> \<and> ground_ctxt (More (lift_None_Some f2) ss2 (C2 \<circ>\<^sub>c More (lift_None_Some f1) ss1 C1 ts1) ts2)
[PROOF STEP]
apply (auto simp del: ctxt_apply_term.simps)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>q |\<in>| ta_der \ (More (lift_None_Some f1) ss1 C1 ts1)\<langle>Var p\<rangle>; r |\<in>| ta_der \ (More (lift_None_Some f2) ss2 C2 ts2)\<langle>Var q\<rangle>; \<forall>x\<in>set ss1. ground x; \<forall>x\<in>set ss2. ground x; ground_ctxt C1; \<forall>x\<in>set ts1. ground x; ground_ctxt C2; \<forall>x\<in>set ts2. ground x\<rbrakk> \<Longrightarrow> r |\<in>| ta_der \ (More (lift_None_Some f2) ss2 (C2 \<circ>\<^sub>c More (lift_None_Some f1) ss1 C1 ts1) ts2)\<langle>Var p\<rangle>
[PROOF STEP]
apply (metis Subterm_and_Context.ctxt_ctxt_compose ctxt_compose.simps(2) ta_der_ctxt)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
\<exists>ss ts f C. r |\<in>| ta_der \ (More (lift_None_Some f) ss C ts)\<langle>Var p\<rangle> \<and> ground_ctxt (More (lift_None_Some f) ss C ts)

goal (2 subgoals):
 1. \<And>f qs q i. \<lbrakk>lift_None_Some f qs \<rightarrow> q |\<in>| rules \; i < length qs; \<Q> \ |\<subseteq>| ta_reachable \\<rbrakk> \<Longrightarrow> \<exists>ss ts f C. q |\<in>| ta_der \ (More (lift_None_Some f) ss C ts)\<langle>Var (qs ! i)\<rangle> \<and> ground_ctxt (More (lift_None_Some f) ss C ts)
 2. \<And>p q r. \<lbrakk>(p, q) \<in> Q_inf \; \<Q> \ |\<subseteq>| ta_reachable \ \<Longrightarrow> \<exists>ss ts f C. q |\<in>| ta_der \ (More (lift_None_Some f) ss C ts)\<langle>Var p\<rangle> \<and> ground_ctxt (More (lift_None_Some f) ss C ts); (q, r) |\<in>| eps \; \<Q> \ |\<subseteq>| ta_reachable \\<rbrakk> \<Longrightarrow> \<exists>ss ts f C. r |\<in>| ta_der \ (More (lift_None_Some f) ss C ts)\<langle>Var p\<rangle> \<and> ground_ctxt (More (lift_None_Some f) ss C ts)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>f qs q i. \<lbrakk>lift_None_Some f qs \<rightarrow> q |\<in>| rules \; i < length qs; \<Q> \ |\<subseteq>| ta_reachable \\<rbrakk> \<Longrightarrow> \<exists>ss ts f C. q |\<in>| ta_der \ (More (lift_None_Some f) ss C ts)\<langle>Var (qs ! i)\<rangle> \<and> ground_ctxt (More (lift_None_Some f) ss C ts)
 2. \<And>p q r. \<lbrakk>(p, q) \<in> Q_inf \; \<Q> \ |\<subseteq>| ta_reachable \ \<Longrightarrow> \<exists>ss ts f C. q |\<in>| ta_der \ (More (lift_None_Some f) ss C ts)\<langle>Var p\<rangle> \<and> ground_ctxt (More (lift_None_Some f) ss C ts); (q, r) |\<in>| eps \; \<Q> \ |\<subseteq>| ta_reachable \\<rbrakk> \<Longrightarrow> \<exists>ss ts f C. r |\<in>| ta_der \ (More (lift_None_Some f) ss C ts)\<langle>Var p\<rangle> \<and> ground_ctxt (More (lift_None_Some f) ss C ts)
[PROOF STEP]
case (rule f qs q i)
[PROOF STATE]
proof (state)
this:
lift_None_Some f qs \<rightarrow> q |\<in>| rules \
i < length qs
\<Q> \ |\<subseteq>| ta_reachable \

goal (2 subgoals):
 1. \<And>f qs q i. \<lbrakk>lift_None_Some f qs \<rightarrow> q |\<in>| rules \; i < length qs; \<Q> \ |\<subseteq>| ta_reachable \\<rbrakk> \<Longrightarrow> \<exists>ss ts f C. q |\<in>| ta_der \ (More (lift_None_Some f) ss C ts)\<langle>Var (qs ! i)\<rangle> \<and> ground_ctxt (More (lift_None_Some f) ss C ts)
 2. \<And>p q r. \<lbrakk>(p, q) \<in> Q_inf \; \<Q> \ |\<subseteq>| ta_reachable \ \<Longrightarrow> \<exists>ss ts f C. q |\<in>| ta_der \ (More (lift_None_Some f) ss C ts)\<langle>Var p\<rangle> \<and> ground_ctxt (More (lift_None_Some f) ss C ts); (q, r) |\<in>| eps \; \<Q> \ |\<subseteq>| ta_reachable \\<rbrakk> \<Longrightarrow> \<exists>ss ts f C. r |\<in>| ta_der \ (More (lift_None_Some f) ss C ts)\<langle>Var p\<rangle> \<and> ground_ctxt (More (lift_None_Some f) ss C ts)
[PROOF STEP]
have "\<forall> i < length qs. \<exists> t. qs ! i |\<in>| ta_der \ t \<and> ground t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>i<length qs. \<exists>t. qs ! i |\<in>| ta_der \ t \<and> ground t
[PROOF STEP]
using rule(1, 2) fset_mp[OF rule(3), of "qs ! i" for i]
[PROOF STATE]
proof (prove)
using this:
lift_None_Some f qs \<rightarrow> q |\<in>| rules \
i < length qs
qs ! ?ia2 |\<in>| \<Q> \ \<Longrightarrow> qs ! ?ia2 |\<in>| ta_reachable \

goal (1 subgoal):
 1. \<forall>i<length qs. \<exists>t. qs ! i |\<in>| ta_der \ t \<and> ground t
[PROOF STEP]
by auto (meson fnth_mem rule_statesD(4) ta_reachableE)
[PROOF STATE]
proof (state)
this:
\<forall>i<length qs. \<exists>t. qs ! i |\<in>| ta_der \ t \<and> ground t

goal (2 subgoals):
 1. \<And>f qs q i. \<lbrakk>lift_None_Some f qs \<rightarrow> q |\<in>| rules \; i < length qs; \<Q> \ |\<subseteq>| ta_reachable \\<rbrakk> \<Longrightarrow> \<exists>ss ts f C. q |\<in>| ta_der \ (More (lift_None_Some f) ss C ts)\<langle>Var (qs ! i)\<rangle> \<and> ground_ctxt (More (lift_None_Some f) ss C ts)
 2. \<And>p q r. \<lbrakk>(p, q) \<in> Q_inf \; \<Q> \ |\<subseteq>| ta_reachable \ \<Longrightarrow> \<exists>ss ts f C. q |\<in>| ta_der \ (More (lift_None_Some f) ss C ts)\<langle>Var p\<rangle> \<and> ground_ctxt (More (lift_None_Some f) ss C ts); (q, r) |\<in>| eps \; \<Q> \ |\<subseteq>| ta_reachable \\<rbrakk> \<Longrightarrow> \<exists>ss ts f C. r |\<in>| ta_der \ (More (lift_None_Some f) ss C ts)\<langle>Var p\<rangle> \<and> ground_ctxt (More (lift_None_Some f) ss C ts)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>i<length qs. \<exists>t. qs ! i |\<in>| ta_der \ t \<and> ground t
[PROOF STEP]
obtain ts where wit: "length ts = length qs"
    "\<forall> i < length qs. qs ! i |\<in>| ta_der \ (ts ! i) \<and> ground (ts ! i)"
[PROOF STATE]
proof (prove)
using this:
\<forall>i<length qs. \<exists>t. qs ! i |\<in>| ta_der \ t \<and> ground t

goal (1 subgoal):
 1. (\<And>ts. \<lbrakk>length ts = length qs; \<forall>i<length qs. qs ! i |\<in>| ta_der \ (ts ! i) \<and> ground (ts ! i)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using Ex_list_of_length_P[of "length qs" "\<lambda> x i. qs ! i |\<in>| ta_der \ x \<and> ground x"]
[PROOF STATE]
proof (prove)
using this:
\<forall>i<length qs. \<exists>t. qs ! i |\<in>| ta_der \ t \<and> ground t
\<forall>i<length qs. \<exists>x. qs ! i |\<in>| ta_der \ x \<and> ground x \<Longrightarrow> \<exists>xs. length xs = length qs \<and> (\<forall>i<length qs. qs ! i |\<in>| ta_der \ (xs ! i) \<and> ground (xs ! i))

goal (1 subgoal):
 1. (\<And>ts. \<lbrakk>length ts = length qs; \<forall>i<length qs. qs ! i |\<in>| ta_der \ (ts ! i) \<and> ground (ts ! i)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
length ts = length qs
\<forall>i<length qs. qs ! i |\<in>| ta_der \ (ts ! i) \<and> ground (ts ! i)

goal (2 subgoals):
 1. \<And>f qs q i. \<lbrakk>lift_None_Some f qs \<rightarrow> q |\<in>| rules \; i < length qs; \<Q> \ |\<subseteq>| ta_reachable \\<rbrakk> \<Longrightarrow> \<exists>ss ts f C. q |\<in>| ta_der \ (More (lift_None_Some f) ss C ts)\<langle>Var (qs ! i)\<rangle> \<and> ground_ctxt (More (lift_None_Some f) ss C ts)
 2. \<And>p q r. \<lbrakk>(p, q) \<in> Q_inf \; \<Q> \ |\<subseteq>| ta_reachable \ \<Longrightarrow> \<exists>ss ts f C. q |\<in>| ta_der \ (More (lift_None_Some f) ss C ts)\<langle>Var p\<rangle> \<and> ground_ctxt (More (lift_None_Some f) ss C ts); (q, r) |\<in>| eps \; \<Q> \ |\<subseteq>| ta_reachable \\<rbrakk> \<Longrightarrow> \<exists>ss ts f C. r |\<in>| ta_der \ (More (lift_None_Some f) ss C ts)\<langle>Var p\<rangle> \<and> ground_ctxt (More (lift_None_Some f) ss C ts)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
length ts = length qs
\<forall>i<length qs. qs ! i |\<in>| ta_der \ (ts ! i) \<and> ground (ts ! i)

goal (2 subgoals):
 1. \<And>f qs q i. \<lbrakk>lift_None_Some f qs \<rightarrow> q |\<in>| rules \; i < length qs; \<Q> \ |\<subseteq>| ta_reachable \\<rbrakk> \<Longrightarrow> \<exists>ss ts f C. q |\<in>| ta_der \ (More (lift_None_Some f) ss C ts)\<langle>Var (qs ! i)\<rangle> \<and> ground_ctxt (More (lift_None_Some f) ss C ts)
 2. \<And>p q r. \<lbrakk>(p, q) \<in> Q_inf \; \<Q> \ |\<subseteq>| ta_reachable \ \<Longrightarrow> \<exists>ss ts f C. q |\<in>| ta_der \ (More (lift_None_Some f) ss C ts)\<langle>Var p\<rangle> \<and> ground_ctxt (More (lift_None_Some f) ss C ts); (q, r) |\<in>| eps \; \<Q> \ |\<subseteq>| ta_reachable \\<rbrakk> \<Longrightarrow> \<exists>ss ts f C. r |\<in>| ta_der \ (More (lift_None_Some f) ss C ts)\<langle>Var p\<rangle> \<and> ground_ctxt (More (lift_None_Some f) ss C ts)
[PROOF STEP]
fix j
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>f qs q i. \<lbrakk>lift_None_Some f qs \<rightarrow> q |\<in>| rules \; i < length qs; \<Q> \ |\<subseteq>| ta_reachable \\<rbrakk> \<Longrightarrow> \<exists>ss ts f C. q |\<in>| ta_der \ (More (lift_None_Some f) ss C ts)\<langle>Var (qs ! i)\<rangle> \<and> ground_ctxt (More (lift_None_Some f) ss C ts)
 2. \<And>p q r. \<lbrakk>(p, q) \<in> Q_inf \; \<Q> \ |\<subseteq>| ta_reachable \ \<Longrightarrow> \<exists>ss ts f C. q |\<in>| ta_der \ (More (lift_None_Some f) ss C ts)\<langle>Var p\<rangle> \<and> ground_ctxt (More (lift_None_Some f) ss C ts); (q, r) |\<in>| eps \; \<Q> \ |\<subseteq>| ta_reachable \\<rbrakk> \<Longrightarrow> \<exists>ss ts f C. r |\<in>| ta_der \ (More (lift_None_Some f) ss C ts)\<langle>Var p\<rangle> \<and> ground_ctxt (More (lift_None_Some f) ss C ts)
[PROOF STEP]
assume "j < length qs"
[PROOF STATE]
proof (state)
this:
j < length qs

goal (2 subgoals):
 1. \<And>f qs q i. \<lbrakk>lift_None_Some f qs \<rightarrow> q |\<in>| rules \; i < length qs; \<Q> \ |\<subseteq>| ta_reachable \\<rbrakk> \<Longrightarrow> \<exists>ss ts f C. q |\<in>| ta_der \ (More (lift_None_Some f) ss C ts)\<langle>Var (qs ! i)\<rangle> \<and> ground_ctxt (More (lift_None_Some f) ss C ts)
 2. \<And>p q r. \<lbrakk>(p, q) \<in> Q_inf \; \<Q> \ |\<subseteq>| ta_reachable \ \<Longrightarrow> \<exists>ss ts f C. q |\<in>| ta_der \ (More (lift_None_Some f) ss C ts)\<langle>Var p\<rangle> \<and> ground_ctxt (More (lift_None_Some f) ss C ts); (q, r) |\<in>| eps \; \<Q> \ |\<subseteq>| ta_reachable \\<rbrakk> \<Longrightarrow> \<exists>ss ts f C. r |\<in>| ta_der \ (More (lift_None_Some f) ss C ts)\<langle>Var p\<rangle> \<and> ground_ctxt (More (lift_None_Some f) ss C ts)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
j < length qs
[PROOF STEP]
have "qs ! j |\<in>| ta_der \ ((take i ts @ Var (qs ! i) # drop (Suc i) ts) ! j)"
[PROOF STATE]
proof (prove)
using this:
j < length qs

goal (1 subgoal):
 1. qs ! j |\<in>| ta_der \ ((take i ts @ Var (qs ! i) # drop (Suc i) ts) ! j)
[PROOF STEP]
using wit
[PROOF STATE]
proof (prove)
using this:
j < length qs
length ts = length qs
\<forall>i<length qs. qs ! i |\<in>| ta_der \ (ts ! i) \<and> ground (ts ! i)

goal (1 subgoal):
 1. qs ! j |\<in>| ta_der \ ((take i ts @ Var (qs ! i) # drop (Suc i) ts) ! j)
[PROOF STEP]
by (cases "j < i") (auto simp: min_def nth_append_Cons)
[PROOF STATE]
proof (state)
this:
qs ! j |\<in>| ta_der \ ((take i ts @ Var (qs ! i) # drop (Suc i) ts) ! j)

goal (2 subgoals):
 1. \<And>f qs q i. \<lbrakk>lift_None_Some f qs \<rightarrow> q |\<in>| rules \; i < length qs; \<Q> \ |\<subseteq>| ta_reachable \\<rbrakk> \<Longrightarrow> \<exists>ss ts f C. q |\<in>| ta_der \ (More (lift_None_Some f) ss C ts)\<langle>Var (qs ! i)\<rangle> \<and> ground_ctxt (More (lift_None_Some f) ss C ts)
 2. \<And>p q r. \<lbrakk>(p, q) \<in> Q_inf \; \<Q> \ |\<subseteq>| ta_reachable \ \<Longrightarrow> \<exists>ss ts f C. q |\<in>| ta_der \ (More (lift_None_Some f) ss C ts)\<langle>Var p\<rangle> \<and> ground_ctxt (More (lift_None_Some f) ss C ts); (q, r) |\<in>| eps \; \<Q> \ |\<subseteq>| ta_reachable \\<rbrakk> \<Longrightarrow> \<exists>ss ts f C. r |\<in>| ta_der \ (More (lift_None_Some f) ss C ts)\<langle>Var p\<rangle> \<and> ground_ctxt (More (lift_None_Some f) ss C ts)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?j2 < length qs \<Longrightarrow> qs ! ?j2 |\<in>| ta_der \ ((take i ts @ Var (qs ! i) # drop (Suc i) ts) ! ?j2)

goal (2 subgoals):
 1. \<And>f qs q i. \<lbrakk>lift_None_Some f qs \<rightarrow> q |\<in>| rules \; i < length qs; \<Q> \ |\<subseteq>| ta_reachable \\<rbrakk> \<Longrightarrow> \<exists>ss ts f C. q |\<in>| ta_der \ (More (lift_None_Some f) ss C ts)\<langle>Var (qs ! i)\<rangle> \<and> ground_ctxt (More (lift_None_Some f) ss C ts)
 2. \<And>p q r. \<lbrakk>(p, q) \<in> Q_inf \; \<Q> \ |\<subseteq>| ta_reachable \ \<Longrightarrow> \<exists>ss ts f C. q |\<in>| ta_der \ (More (lift_None_Some f) ss C ts)\<langle>Var p\<rangle> \<and> ground_ctxt (More (lift_None_Some f) ss C ts); (q, r) |\<in>| eps \; \<Q> \ |\<subseteq>| ta_reachable \\<rbrakk> \<Longrightarrow> \<exists>ss ts f C. r |\<in>| ta_der \ (More (lift_None_Some f) ss C ts)\<langle>Var p\<rangle> \<and> ground_ctxt (More (lift_None_Some f) ss C ts)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
?j2 < length qs \<Longrightarrow> qs ! ?j2 |\<in>| ta_der \ ((take i ts @ Var (qs ! i) # drop (Suc i) ts) ! ?j2)
[PROOF STEP]
have "\<forall> i < length qs. qs ! i |\<in>| (map (ta_der \) (take i ts @ Var (qs ! i) # drop (Suc i) ts)) ! i"
[PROOF STATE]
proof (prove)
using this:
?j2 < length qs \<Longrightarrow> qs ! ?j2 |\<in>| ta_der \ ((take i ts @ Var (qs ! i) # drop (Suc i) ts) ! ?j2)

goal (1 subgoal):
 1. \<forall>i<length qs. qs ! i |\<in>| map (ta_der \) (take i ts @ Var (qs ! i) # drop (Suc i) ts) ! i
[PROOF STEP]
using wit rule(2)
[PROOF STATE]
proof (prove)
using this:
?j2 < length qs \<Longrightarrow> qs ! ?j2 |\<in>| ta_der \ ((take i ts @ Var (qs ! i) # drop (Suc i) ts) ! ?j2)
length ts = length qs
\<forall>i<length qs. qs ! i |\<in>| ta_der \ (ts ! i) \<and> ground (ts ! i)
i < length qs

goal (1 subgoal):
 1. \<forall>i<length qs. qs ! i |\<in>| map (ta_der \) (take i ts @ Var (qs ! i) # drop (Suc i) ts) ! i
[PROOF STEP]
by (auto simp: nth_append_Cons)
[PROOF STATE]
proof (state)
this:
\<forall>i<length qs. qs ! i |\<in>| map (ta_der \) (take i ts @ Var (qs ! i) # drop (Suc i) ts) ! i

goal (2 subgoals):
 1. \<And>f qs q i. \<lbrakk>lift_None_Some f qs \<rightarrow> q |\<in>| rules \; i < length qs; \<Q> \ |\<subseteq>| ta_reachable \\<rbrakk> \<Longrightarrow> \<exists>ss ts f C. q |\<in>| ta_der \ (More (lift_None_Some f) ss C ts)\<langle>Var (qs ! i)\<rangle> \<and> ground_ctxt (More (lift_None_Some f) ss C ts)
 2. \<And>p q r. \<lbrakk>(p, q) \<in> Q_inf \; \<Q> \ |\<subseteq>| ta_reachable \ \<Longrightarrow> \<exists>ss ts f C. q |\<in>| ta_der \ (More (lift_None_Some f) ss C ts)\<langle>Var p\<rangle> \<and> ground_ctxt (More (lift_None_Some f) ss C ts); (q, r) |\<in>| eps \; \<Q> \ |\<subseteq>| ta_reachable \\<rbrakk> \<Longrightarrow> \<exists>ss ts f C. r |\<in>| ta_der \ (More (lift_None_Some f) ss C ts)\<langle>Var p\<rangle> \<and> ground_ctxt (More (lift_None_Some f) ss C ts)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>i<length qs. qs ! i |\<in>| map (ta_der \) (take i ts @ Var (qs ! i) # drop (Suc i) ts) ! i
[PROOF STEP]
have res: "q |\<in>| ta_der \ (Fun (None, Some f) (take i ts @ Var (qs ! i) # drop (Suc i) ts))"
[PROOF STATE]
proof (prove)
using this:
\<forall>i<length qs. qs ! i |\<in>| map (ta_der \) (take i ts @ Var (qs ! i) # drop (Suc i) ts) ! i

goal (1 subgoal):
 1. q |\<in>| ta_der \ (Fun (lift_None_Some f) (take i ts @ Var (qs ! i) # drop (Suc i) ts))
[PROOF STEP]
using rule(1, 2) wit
[PROOF STATE]
proof (prove)
using this:
\<forall>i<length qs. qs ! i |\<in>| map (ta_der \) (take i ts @ Var (qs ! i) # drop (Suc i) ts) ! i
lift_None_Some f qs \<rightarrow> q |\<in>| rules \
i < length qs
length ts = length qs
\<forall>i<length qs. qs ! i |\<in>| ta_der \ (ts ! i) \<and> ground (ts ! i)

goal (1 subgoal):
 1. q |\<in>| ta_der \ (Fun (lift_None_Some f) (take i ts @ Var (qs ! i) # drop (Suc i) ts))
[PROOF STEP]
by (auto simp: min_def nth_append_Cons intro!: exI[of _ q] exI[of _ qs])
[PROOF STATE]
proof (state)
this:
q |\<in>| ta_der \ (Fun (lift_None_Some f) (take i ts @ Var (qs ! i) # drop (Suc i) ts))

goal (2 subgoals):
 1. \<And>f qs q i. \<lbrakk>lift_None_Some f qs \<rightarrow> q |\<in>| rules \; i < length qs; \<Q> \ |\<subseteq>| ta_reachable \\<rbrakk> \<Longrightarrow> \<exists>ss ts f C. q |\<in>| ta_der \ (More (lift_None_Some f) ss C ts)\<langle>Var (qs ! i)\<rangle> \<and> ground_ctxt (More (lift_None_Some f) ss C ts)
 2. \<And>p q r. \<lbrakk>(p, q) \<in> Q_inf \; \<Q> \ |\<subseteq>| ta_reachable \ \<Longrightarrow> \<exists>ss ts f C. q |\<in>| ta_der \ (More (lift_None_Some f) ss C ts)\<langle>Var p\<rangle> \<and> ground_ctxt (More (lift_None_Some f) ss C ts); (q, r) |\<in>| eps \; \<Q> \ |\<subseteq>| ta_reachable \\<rbrakk> \<Longrightarrow> \<exists>ss ts f C. r |\<in>| ta_der \ (More (lift_None_Some f) ss C ts)\<langle>Var p\<rangle> \<and> ground_ctxt (More (lift_None_Some f) ss C ts)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
q |\<in>| ta_der \ (Fun (lift_None_Some f) (take i ts @ Var (qs ! i) # drop (Suc i) ts))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
q |\<in>| ta_der \ (Fun (lift_None_Some f) (take i ts @ Var (qs ! i) # drop (Suc i) ts))

goal (1 subgoal):
 1. \<exists>ss ts f C. q |\<in>| ta_der \ (More (lift_None_Some f) ss C ts)\<langle>Var (qs ! i)\<rangle> \<and> ground_ctxt (More (lift_None_Some f) ss C ts)
[PROOF STEP]
using rule(1, 2) wit
[PROOF STATE]
proof (prove)
using this:
q |\<in>| ta_der \ (Fun (lift_None_Some f) (take i ts @ Var (qs ! i) # drop (Suc i) ts))
lift_None_Some f qs \<rightarrow> q |\<in>| rules \
i < length qs
length ts = length qs
\<forall>i<length qs. qs ! i |\<in>| ta_der \ (ts ! i) \<and> ground (ts ! i)

goal (1 subgoal):
 1. \<exists>ss ts f C. q |\<in>| ta_der \ (More (lift_None_Some f) ss C ts)\<langle>Var (qs ! i)\<rangle> \<and> ground_ctxt (More (lift_None_Some f) ss C ts)
[PROOF STEP]
apply (rule_tac x = "take i ts" in exI, rule_tac x = "drop (Suc i) ts" in exI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>q |\<in>| ta_der \ (Fun (lift_None_Some f) (take i ts @ Var (qs ! i) # drop (Suc i) ts)); lift_None_Some f qs \<rightarrow> q |\<in>| rules \; i < length qs; length ts = length qs; \<forall>i<length qs. qs ! i |\<in>| ta_der \ (ts ! i) \<and> ground (ts ! i); q |\<in>| ta_der \ (Fun (lift_None_Some f) (take i ts @ Var (qs ! i) # drop (Suc i) ts)); lift_None_Some f qs \<rightarrow> q |\<in>| rules \; i < length qs; length ts = length qs; \<forall>i<length qs. qs ! i |\<in>| ta_der \ (ts ! i) \<and> ground (ts ! i)\<rbrakk> \<Longrightarrow> \<exists>f C. q |\<in>| ta_der \ (More (lift_None_Some f) (take i ts) C (drop (Suc i) ts))\<langle>Var (qs ! i)\<rangle> \<and> ground_ctxt (More (lift_None_Some f) (take i ts) C (drop (Suc i) ts))
[PROOF STEP]
apply (auto simp: take_map drop_map  dest!: in_set_takeD in_set_dropD simp del: ta_der_simps intro!: exI[of _ f] exI[of _ Hole])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>q |\<in>| ta_der \ (Fun (lift_None_Some f) (take i ts @ Var (qs ! i) # drop (Suc i) ts)); lift_None_Some f qs \<rightarrow> q |\<in>| rules \; i < length qs; length ts = length qs; \<forall>i<length qs. qs ! i |\<in>| ta_der \ (ts ! i) \<and> ground (ts ! i); x \<in> set ts\<rbrakk> \<Longrightarrow> ground x
 2. \<And>x. \<lbrakk>q |\<in>| ta_der \ (Fun (lift_None_Some f) (take i ts @ Var (qs ! i) # drop (Suc i) ts)); lift_None_Some f qs \<rightarrow> q |\<in>| rules \; i < length qs; length ts = length qs; \<forall>i<length qs. qs ! i |\<in>| ta_der \ (ts ! i) \<and> ground (ts ! i); x \<in> set ts\<rbrakk> \<Longrightarrow> ground x
[PROOF STEP]
apply (metis all_nth_imp_all_set)+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
\<exists>ss ts f C. q |\<in>| ta_der \ (More (lift_None_Some f) ss C ts)\<langle>Var (qs ! i)\<rangle> \<and> ground_ctxt (More (lift_None_Some f) ss C ts)

goal (1 subgoal):
 1. \<And>p q r. \<lbrakk>(p, q) \<in> Q_inf \; \<Q> \ |\<subseteq>| ta_reachable \ \<Longrightarrow> \<exists>ss ts f C. q |\<in>| ta_der \ (More (lift_None_Some f) ss C ts)\<langle>Var p\<rangle> \<and> ground_ctxt (More (lift_None_Some f) ss C ts); (q, r) |\<in>| eps \; \<Q> \ |\<subseteq>| ta_reachable \\<rbrakk> \<Longrightarrow> \<exists>ss ts f C. r |\<in>| ta_der \ (More (lift_None_Some f) ss C ts)\<langle>Var p\<rangle> \<and> ground_ctxt (More (lift_None_Some f) ss C ts)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>p q r. \<lbrakk>(p, q) \<in> Q_inf \; \<Q> \ |\<subseteq>| ta_reachable \ \<Longrightarrow> \<exists>ss ts f C. q |\<in>| ta_der \ (More (lift_None_Some f) ss C ts)\<langle>Var p\<rangle> \<and> ground_ctxt (More (lift_None_Some f) ss C ts); (q, r) |\<in>| eps \; \<Q> \ |\<subseteq>| ta_reachable \\<rbrakk> \<Longrightarrow> \<exists>ss ts f C. r |\<in>| ta_der \ (More (lift_None_Some f) ss C ts)\<langle>Var p\<rangle> \<and> ground_ctxt (More (lift_None_Some f) ss C ts)
[PROOF STEP]
case (eps p q r)
[PROOF STATE]
proof (state)
this:
(p, q) \<in> Q_inf \
\<Q> \ |\<subseteq>| ta_reachable \ \<Longrightarrow> \<exists>ss ts f C. q |\<in>| ta_der \ (More (lift_None_Some f) ss C ts)\<langle>Var p\<rangle> \<and> ground_ctxt (More (lift_None_Some f) ss C ts)
(q, r) |\<in>| eps \
\<Q> \ |\<subseteq>| ta_reachable \

goal (1 subgoal):
 1. \<And>p q r. \<lbrakk>(p, q) \<in> Q_inf \; \<Q> \ |\<subseteq>| ta_reachable \ \<Longrightarrow> \<exists>ss ts f C. q |\<in>| ta_der \ (More (lift_None_Some f) ss C ts)\<langle>Var p\<rangle> \<and> ground_ctxt (More (lift_None_Some f) ss C ts); (q, r) |\<in>| eps \; \<Q> \ |\<subseteq>| ta_reachable \\<rbrakk> \<Longrightarrow> \<exists>ss ts f C. r |\<in>| ta_der \ (More (lift_None_Some f) ss C ts)\<langle>Var p\<rangle> \<and> ground_ctxt (More (lift_None_Some f) ss C ts)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(p, q) \<in> Q_inf \
\<Q> \ |\<subseteq>| ta_reachable \ \<Longrightarrow> \<exists>ss ts f C. q |\<in>| ta_der \ (More (lift_None_Some f) ss C ts)\<langle>Var p\<rangle> \<and> ground_ctxt (More (lift_None_Some f) ss C ts)
(q, r) |\<in>| eps \
\<Q> \ |\<subseteq>| ta_reachable \
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
(p, q) \<in> Q_inf \
\<Q> \ |\<subseteq>| ta_reachable \ \<Longrightarrow> \<exists>ss ts f C. q |\<in>| ta_der \ (More (lift_None_Some f) ss C ts)\<langle>Var p\<rangle> \<and> ground_ctxt (More (lift_None_Some f) ss C ts)
(q, r) |\<in>| eps \
\<Q> \ |\<subseteq>| ta_reachable \

goal (1 subgoal):
 1. \<exists>ss ts f C. r |\<in>| ta_der \ (More (lift_None_Some f) ss C ts)\<langle>Var p\<rangle> \<and> ground_ctxt (More (lift_None_Some f) ss C ts)
[PROOF STEP]
by (meson r_into_rtrancl ta_der_eps)
[PROOF STATE]
proof (state)
this:
\<exists>ss ts f C. r |\<in>| ta_der \ (More (lift_None_Some f) ss C ts)\<langle>Var p\<rangle> \<and> ground_ctxt (More (lift_None_Some f) ss C ts)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma rule_target_Q_inf:
  assumes "(None, Some f) qs \<rightarrow> q' |\<in>| rules \" and "i < length qs"
   shows "(qs ! i, q') \<in> Q_inf \"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (qs ! i, q') \<in> Q_inf \
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
lift_None_Some f qs \<rightarrow> q' |\<in>| rules \
i < length qs

goal (1 subgoal):
 1. (qs ! i, q') \<in> Q_inf \
[PROOF STEP]
by (intro rule) auto


[STATEMENT]
lemma rule_target_eps_Q_inf:
  assumes "(None, Some f) qs \<rightarrow> q' |\<in>| rules \" "(q', q) |\<in>| (eps \)|\<^sup>+|"
     and "i < length qs"
   shows "(qs ! i, q) \<in> Q_inf \"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (qs ! i, q) \<in> Q_inf \
[PROOF STEP]
using assms(2, 1, 3)
[PROOF STATE]
proof (prove)
using this:
(q', q) |\<in>| (eps \)|\<^sup>+|
lift_None_Some f qs \<rightarrow> q' |\<in>| rules \
i < length qs

goal (1 subgoal):
 1. (qs ! i, q) \<in> Q_inf \
[PROOF STEP]
by (induct rule: ftrancl_induct) (auto intro: rule eps)


[STATEMENT]
lemma step_in_Q_inf:
  assumes "q |\<in>| ta_der_strict \ (map_funs_term (\<lambda>f. (None, Some f)) (Fun f (ss @ Var p # ts)))"
    shows "(p, q) \<in> Q_inf \"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (p, q) \<in> Q_inf \
[PROOF STEP]
using assms rule_target_eps_Q_inf[of f _ _ \ q] rule_target_Q_inf[of f _ q \]
[PROOF STATE]
proof (prove)
using this:
q |\<in>| ta_der_strict \ (map_funs_term lift_None_Some (Fun f (ss @ Var p # ts)))
\<lbrakk>lift_None_Some f ?qs \<rightarrow> ?q' |\<in>| rules \; (?q', q) |\<in>| (eps \)|\<^sup>+|; ?i < length ?qs\<rbrakk> \<Longrightarrow> (?qs ! ?i, q) \<in> Q_inf \
\<lbrakk>lift_None_Some f ?qs \<rightarrow> q |\<in>| rules \; ?i < length ?qs\<rbrakk> \<Longrightarrow> (?qs ! ?i, q) \<in> Q_inf \

goal (1 subgoal):
 1. (p, q) \<in> Q_inf \
[PROOF STEP]
by (auto simp: comp_def nth_append_Cons split!: if_splits)


[STATEMENT]
lemma ta_der_Q_inf:
  assumes "q |\<in>| ta_der_strict \ (map_funs_term (\<lambda>f. (None, Some f)) (C\<langle>Var p\<rangle>))" and "C \<noteq> Hole"
  shows "(p, q) \<in> Q_inf \"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (p, q) \<in> Q_inf \
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
q |\<in>| ta_der_strict \ (map_funs_term lift_None_Some C\<langle>Var p\<rangle>)
C \<noteq> \<box>

goal (1 subgoal):
 1. (p, q) \<in> Q_inf \
[PROOF STEP]
proof (induct C arbitrary: q)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>q. \<lbrakk>q |\<in>| ta_der_strict \ (map_funs_term lift_None_Some \<box>\<langle>Var p\<rangle>); \<box> \<noteq> \<box>\<rbrakk> \<Longrightarrow> (p, q) \<in> Q_inf \
 2. \<And>x1 x2 C x4 q. \<lbrakk>\<And>q. \<lbrakk>q |\<in>| ta_der_strict \ (map_funs_term lift_None_Some C\<langle>Var p\<rangle>); C \<noteq> \<box>\<rbrakk> \<Longrightarrow> (p, q) \<in> Q_inf \; q |\<in>| ta_der_strict \ (map_funs_term lift_None_Some (More x1 x2 C x4)\<langle>Var p\<rangle>); More x1 x2 C x4 \<noteq> \<box>\<rbrakk> \<Longrightarrow> (p, q) \<in> Q_inf \
[PROOF STEP]
case (More f ss C ts)
[PROOF STATE]
proof (state)
this:
\<lbrakk>?q |\<in>| ta_der_strict \ (map_funs_term lift_None_Some C\<langle>Var p\<rangle>); C \<noteq> \<box>\<rbrakk> \<Longrightarrow> (p, ?q) \<in> Q_inf \
q |\<in>| ta_der_strict \ (map_funs_term lift_None_Some (More f ss C ts)\<langle>Var p\<rangle>)
More f ss C ts \<noteq> \<box>

goal (2 subgoals):
 1. \<And>q. \<lbrakk>q |\<in>| ta_der_strict \ (map_funs_term lift_None_Some \<box>\<langle>Var p\<rangle>); \<box> \<noteq> \<box>\<rbrakk> \<Longrightarrow> (p, q) \<in> Q_inf \
 2. \<And>x1 x2 C x4 q. \<lbrakk>\<And>q. \<lbrakk>q |\<in>| ta_der_strict \ (map_funs_term lift_None_Some C\<langle>Var p\<rangle>); C \<noteq> \<box>\<rbrakk> \<Longrightarrow> (p, q) \<in> Q_inf \; q |\<in>| ta_der_strict \ (map_funs_term lift_None_Some (More x1 x2 C x4)\<langle>Var p\<rangle>); More x1 x2 C x4 \<noteq> \<box>\<rbrakk> \<Longrightarrow> (p, q) \<in> Q_inf \
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>?q |\<in>| ta_der_strict \ (map_funs_term lift_None_Some C\<langle>Var p\<rangle>); C \<noteq> \<box>\<rbrakk> \<Longrightarrow> (p, ?q) \<in> Q_inf \
q |\<in>| ta_der_strict \ (map_funs_term lift_None_Some (More f ss C ts)\<langle>Var p\<rangle>)
More f ss C ts \<noteq> \<box>
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?q |\<in>| ta_der_strict \ (map_funs_term lift_None_Some C\<langle>Var p\<rangle>); C \<noteq> \<box>\<rbrakk> \<Longrightarrow> (p, ?q) \<in> Q_inf \
q |\<in>| ta_der_strict \ (map_funs_term lift_None_Some (More f ss C ts)\<langle>Var p\<rangle>)
More f ss C ts \<noteq> \<box>

goal (1 subgoal):
 1. (p, q) \<in> Q_inf \
[PROOF STEP]
proof (cases "C = Hole")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>\<And>q. \<lbrakk>q |\<in>| ta_der_strict \ (map_funs_term lift_None_Some C\<langle>Var p\<rangle>); C \<noteq> \<box>\<rbrakk> \<Longrightarrow> (p, q) \<in> Q_inf \; q |\<in>| ta_der_strict \ (map_funs_term lift_None_Some (More f ss C ts)\<langle>Var p\<rangle>); More f ss C ts \<noteq> \<box>; C = \<box>\<rbrakk> \<Longrightarrow> (p, q) \<in> Q_inf \
 2. \<lbrakk>\<And>q. \<lbrakk>q |\<in>| ta_der_strict \ (map_funs_term lift_None_Some C\<langle>Var p\<rangle>); C \<noteq> \<box>\<rbrakk> \<Longrightarrow> (p, q) \<in> Q_inf \; q |\<in>| ta_der_strict \ (map_funs_term lift_None_Some (More f ss C ts)\<langle>Var p\<rangle>); More f ss C ts \<noteq> \<box>; C \<noteq> \<box>\<rbrakk> \<Longrightarrow> (p, q) \<in> Q_inf \
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
C = \<box>

goal (2 subgoals):
 1. \<lbrakk>\<And>q. \<lbrakk>q |\<in>| ta_der_strict \ (map_funs_term lift_None_Some C\<langle>Var p\<rangle>); C \<noteq> \<box>\<rbrakk> \<Longrightarrow> (p, q) \<in> Q_inf \; q |\<in>| ta_der_strict \ (map_funs_term lift_None_Some (More f ss C ts)\<langle>Var p\<rangle>); More f ss C ts \<noteq> \<box>; C = \<box>\<rbrakk> \<Longrightarrow> (p, q) \<in> Q_inf \
 2. \<lbrakk>\<And>q. \<lbrakk>q |\<in>| ta_der_strict \ (map_funs_term lift_None_Some C\<langle>Var p\<rangle>); C \<noteq> \<box>\<rbrakk> \<Longrightarrow> (p, q) \<in> Q_inf \; q |\<in>| ta_der_strict \ (map_funs_term lift_None_Some (More f ss C ts)\<langle>Var p\<rangle>); More f ss C ts \<noteq> \<box>; C \<noteq> \<box>\<rbrakk> \<Longrightarrow> (p, q) \<in> Q_inf \
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
C = \<box>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
C = \<box>

goal (1 subgoal):
 1. (p, q) \<in> Q_inf \
[PROOF STEP]
using More(2)
[PROOF STATE]
proof (prove)
using this:
C = \<box>
q |\<in>| ta_der_strict \ (map_funs_term lift_None_Some (More f ss C ts)\<langle>Var p\<rangle>)

goal (1 subgoal):
 1. (p, q) \<in> Q_inf \
[PROOF STEP]
by (auto simp: step_in_Q_inf)
[PROOF STATE]
proof (state)
this:
(p, q) \<in> Q_inf \

goal (1 subgoal):
 1. \<lbrakk>\<And>q. \<lbrakk>q |\<in>| ta_der_strict \ (map_funs_term lift_None_Some C\<langle>Var p\<rangle>); C \<noteq> \<box>\<rbrakk> \<Longrightarrow> (p, q) \<in> Q_inf \; q |\<in>| ta_der_strict \ (map_funs_term lift_None_Some (More f ss C ts)\<langle>Var p\<rangle>); More f ss C ts \<noteq> \<box>; C \<noteq> \<box>\<rbrakk> \<Longrightarrow> (p, q) \<in> Q_inf \
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>\<And>q. \<lbrakk>q |\<in>| ta_der_strict \ (map_funs_term lift_None_Some C\<langle>Var p\<rangle>); C \<noteq> \<box>\<rbrakk> \<Longrightarrow> (p, q) \<in> Q_inf \; q |\<in>| ta_der_strict \ (map_funs_term lift_None_Some (More f ss C ts)\<langle>Var p\<rangle>); More f ss C ts \<noteq> \<box>; C \<noteq> \<box>\<rbrakk> \<Longrightarrow> (p, q) \<in> Q_inf \
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
C \<noteq> \<box>

goal (1 subgoal):
 1. \<lbrakk>\<And>q. \<lbrakk>q |\<in>| ta_der_strict \ (map_funs_term lift_None_Some C\<langle>Var p\<rangle>); C \<noteq> \<box>\<rbrakk> \<Longrightarrow> (p, q) \<in> Q_inf \; q |\<in>| ta_der_strict \ (map_funs_term lift_None_Some (More f ss C ts)\<langle>Var p\<rangle>); More f ss C ts \<noteq> \<box>; C \<noteq> \<box>\<rbrakk> \<Longrightarrow> (p, q) \<in> Q_inf \
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
C \<noteq> \<box>
[PROOF STEP]
obtain q' where q: "q' |\<in>| ta_der_strict \ (map_funs_term (\<lambda>f. (None, Some f)) C\<langle>Var p\<rangle>)"
     "q |\<in>| ta_der_strict \ (map_funs_term (\<lambda>f. (None, Some f)) (Fun f (ss @ Var q' # ts)))"
[PROOF STATE]
proof (prove)
using this:
C \<noteq> \<box>

goal (1 subgoal):
 1. (\<And>q'. \<lbrakk>q' |\<in>| ta_der_strict \ (map_funs_term lift_None_Some C\<langle>Var p\<rangle>); q |\<in>| ta_der_strict \ (map_funs_term lift_None_Some (Fun f (ss @ Var q' # ts)))\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using More(2) length_map
[PROOF STATE]
proof (prove)
using this:
C \<noteq> \<box>
q |\<in>| ta_der_strict \ (map_funs_term lift_None_Some (More f ss C ts)\<langle>Var p\<rangle>)
length (map ?f ?xs) = length ?xs

goal (1 subgoal):
 1. (\<And>q'. \<lbrakk>q' |\<in>| ta_der_strict \ (map_funs_term lift_None_Some C\<langle>Var p\<rangle>); q |\<in>| ta_der_strict \ (map_funs_term lift_None_Some (Fun f (ss @ Var q' # ts)))\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
(* SLOW *)
[PROOF STATE]
proof (prove)
using this:
C \<noteq> \<box>
q |\<in>| ta_der_strict \ (map_funs_term lift_None_Some (More f ss C ts)\<langle>Var p\<rangle>)
length (map ?f ?xs) = length ?xs

goal (1 subgoal):
 1. (\<And>q'. \<lbrakk>q' |\<in>| ta_der_strict \ (map_funs_term lift_None_Some C\<langle>Var p\<rangle>); q |\<in>| ta_der_strict \ (map_funs_term lift_None_Some (Fun f (ss @ Var q' # ts)))\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp: comp_def nth_append_Cons split: if_splits cong: if_cong')
         (smt nat_neq_iff nth_map ta_der_strict_simps)+
[PROOF STATE]
proof (state)
this:
q' |\<in>| ta_der_strict \ (map_funs_term lift_None_Some C\<langle>Var p\<rangle>)
q |\<in>| ta_der_strict \ (map_funs_term lift_None_Some (Fun f (ss @ Var q' # ts)))

goal (1 subgoal):
 1. \<lbrakk>\<And>q. \<lbrakk>q |\<in>| ta_der_strict \ (map_funs_term lift_None_Some C\<langle>Var p\<rangle>); C \<noteq> \<box>\<rbrakk> \<Longrightarrow> (p, q) \<in> Q_inf \; q |\<in>| ta_der_strict \ (map_funs_term lift_None_Some (More f ss C ts)\<langle>Var p\<rangle>); More f ss C ts \<noteq> \<box>; C \<noteq> \<box>\<rbrakk> \<Longrightarrow> (p, q) \<in> Q_inf \
[PROOF STEP]
have "(p, q') \<in> Q_inf \"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (p, q') \<in> Q_inf \
[PROOF STEP]
using More(1)[OF q(1) False]
[PROOF STATE]
proof (prove)
using this:
(p, q') \<in> Q_inf \

goal (1 subgoal):
 1. (p, q') \<in> Q_inf \
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
(p, q') \<in> Q_inf \

goal (1 subgoal):
 1. \<lbrakk>\<And>q. \<lbrakk>q |\<in>| ta_der_strict \ (map_funs_term lift_None_Some C\<langle>Var p\<rangle>); C \<noteq> \<box>\<rbrakk> \<Longrightarrow> (p, q) \<in> Q_inf \; q |\<in>| ta_der_strict \ (map_funs_term lift_None_Some (More f ss C ts)\<langle>Var p\<rangle>); More f ss C ts \<noteq> \<box>; C \<noteq> \<box>\<rbrakk> \<Longrightarrow> (p, q) \<in> Q_inf \
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(p, q') \<in> Q_inf \
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(p, q') \<in> Q_inf \

goal (1 subgoal):
 1. (p, q) \<in> Q_inf \
[PROOF STEP]
using step_in_Q_inf[OF q(2)]
[PROOF STATE]
proof (prove)
using this:
(p, q') \<in> Q_inf \
(q', q) \<in> Q_inf \

goal (1 subgoal):
 1. (p, q) \<in> Q_inf \
[PROOF STEP]
by (auto intro: trans)
[PROOF STATE]
proof (state)
this:
(p, q) \<in> Q_inf \

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(p, q) \<in> Q_inf \

goal (1 subgoal):
 1. \<And>q. \<lbrakk>q |\<in>| ta_der_strict \ (map_funs_term lift_None_Some \<box>\<langle>Var p\<rangle>); \<box> \<noteq> \<box>\<rbrakk> \<Longrightarrow> (p, q) \<in> Q_inf \
[PROOF STEP]
qed auto


[STATEMENT]
lemma Q_inf_e_infinite_terms_res:
  assumes "q \<in> Q_inf_e \" and "\<Q> \ |\<subseteq>| ta_reachable \"
  shows "infinite {t. q |\<in>| ta_der \ (term_of_gterm t) \<and> fst (groot_sym t) = None}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. infinite {t. q |\<in>| ta_der \ (term_of_gterm t) \<and> fst (groot_sym t) = None}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. infinite {t. q |\<in>| ta_der \ (term_of_gterm t) \<and> fst (groot_sym t) = None}
[PROOF STEP]
let ?P ="\<lambda> u. ground u \<and> q |\<in>| ta_der \ u \<and> fst (fst (the (root u))) = None"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. infinite {t. q |\<in>| ta_der \ (term_of_gterm t) \<and> fst (groot_sym t) = None}
[PROOF STEP]
have groot[simp]: "fst (fst (the (root (term_of_gterm t)))) = fst (groot_sym t)" for t
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst (fst (the (root (term_of_gterm t)))) = fst (groot_sym t)
[PROOF STEP]
by (cases t) auto
[PROOF STATE]
proof (state)
this:
fst (fst (the (root (term_of_gterm ?t1)))) = fst (groot_sym ?t1)

goal (1 subgoal):
 1. infinite {t. q |\<in>| ta_der \ (term_of_gterm t) \<and> fst (groot_sym t) = None}
[PROOF STEP]
have [simp]: "C \<noteq> \<box> \<Longrightarrow> fst (fst (the (root C\<langle>t\<rangle>))) = fst (root_ctxt C)" for C t
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. C \<noteq> \<box> \<Longrightarrow> fst (fst (the (root C\<langle>t\<rangle>))) = fst (root_ctxt C)
[PROOF STEP]
by (cases C) auto
[PROOF STATE]
proof (state)
this:
?C2 \<noteq> \<box> \<Longrightarrow> fst (fst (the (root ?C2\<langle>?t2\<rangle>))) = fst (root_ctxt ?C2)

goal (1 subgoal):
 1. infinite {t. q |\<in>| ta_der \ (term_of_gterm t) \<and> fst (groot_sym t) = None}
[PROOF STEP]
from assms(1)
[PROOF STATE]
proof (chain)
picking this:
q \<in> Q_inf_e \
[PROOF STEP]
obtain p where cycle: "(p, p) \<in> Q_inf \" "(p, q) \<in> Q_inf \"
[PROOF STATE]
proof (prove)
using this:
q \<in> Q_inf_e \

goal (1 subgoal):
 1. (\<And>p. \<lbrakk>(p, p) \<in> Q_inf \; (p, q) \<in> Q_inf \\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(p, p) \<in> Q_inf \
(p, q) \<in> Q_inf \

goal (1 subgoal):
 1. infinite {t. q |\<in>| ta_der \ (term_of_gterm t) \<and> fst (groot_sym t) = None}
[PROOF STEP]
from Q_inf_reach_state_rule[OF cycle(1) assms(2)]
[PROOF STATE]
proof (chain)
picking this:
\<exists>ss ts f C. p |\<in>| ta_der \ (More (lift_None_Some f) ss C ts)\<langle>Var p\<rangle> \<and> ground_ctxt (More (lift_None_Some f) ss C ts)
[PROOF STEP]
obtain C where
    ctxt: "C \<noteq> \<box>" "ground_ctxt C" and reach: "p |\<in>| ta_der \ C\<langle>Var p\<rangle>"
[PROOF STATE]
proof (prove)
using this:
\<exists>ss ts f C. p |\<in>| ta_der \ (More (lift_None_Some f) ss C ts)\<langle>Var p\<rangle> \<and> ground_ctxt (More (lift_None_Some f) ss C ts)

goal (1 subgoal):
 1. (\<And>C. \<lbrakk>C \<noteq> \<box>; ground_ctxt C; p |\<in>| ta_der \ C\<langle>Var p\<rangle>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
C \<noteq> \<box>
ground_ctxt C
p |\<in>| ta_der \ C\<langle>Var p\<rangle>

goal (1 subgoal):
 1. infinite {t. q |\<in>| ta_der \ (term_of_gterm t) \<and> fst (groot_sym t) = None}
[PROOF STEP]
obtain C2 where
    closing_ctxt: "C2 \<noteq> \<box>" "ground_ctxt C2" "fst (root_ctxt C2) = None" and cl_reach: "q |\<in>| ta_der \ C2\<langle>Var p\<rangle>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>C2. \<lbrakk>C2 \<noteq> \<box>; ground_ctxt C2; fst (root_ctxt C2) = None; q |\<in>| ta_der \ C2\<langle>Var p\<rangle>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis (full_types) Q_inf_reach_state_rule[OF cycle(2) assms(2)] ctxt.distinct(1) fst_conv root_ctxt.simps(1))
[PROOF STATE]
proof (state)
this:
C2 \<noteq> \<box>
ground_ctxt C2
fst (root_ctxt C2) = None
q |\<in>| ta_der \ C2\<langle>Var p\<rangle>

goal (1 subgoal):
 1. infinite {t. q |\<in>| ta_der \ (term_of_gterm t) \<and> fst (groot_sym t) = None}
[PROOF STEP]
from assms(2)
[PROOF STATE]
proof (chain)
picking this:
\<Q> \ |\<subseteq>| ta_reachable \
[PROOF STEP]
obtain t where t: "p |\<in>| ta_der \ t" and gr_t: "ground t"
[PROOF STATE]
proof (prove)
using this:
\<Q> \ |\<subseteq>| ta_reachable \

goal (1 subgoal):
 1. (\<And>t. \<lbrakk>p |\<in>| ta_der \ t; ground t\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (meson Q_inf_states_ta_states(1) cycle(1) fsubsetD ta_reachableE)
[PROOF STATE]
proof (state)
this:
p |\<in>| ta_der \ t
ground t

goal (1 subgoal):
 1. infinite {t. q |\<in>| ta_der \ (term_of_gterm t) \<and> fst (groot_sym t) = None}
[PROOF STEP]
let ?terms = "\<lambda> n. (C ^ Suc n)\<langle>t\<rangle>"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. infinite {t. q |\<in>| ta_der \ (term_of_gterm t) \<and> fst (groot_sym t) = None}
[PROOF STEP]
let ?S = "{?terms n | n. p |\<in>| ta_der \ (?terms n) \<and> ground (?terms n)}"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. infinite {t. q |\<in>| ta_der \ (term_of_gterm t) \<and> fst (groot_sym t) = None}
[PROOF STEP]
have "ground (?terms n)" for n
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ground (C ^ Suc n)\<langle>t\<rangle>
[PROOF STEP]
using ctxt(2) gr_t
[PROOF STATE]
proof (prove)
using this:
ground_ctxt C
ground t

goal (1 subgoal):
 1. ground (C ^ Suc n)\<langle>t\<rangle>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
ground (C ^ Suc ?n2)\<langle>t\<rangle>

goal (1 subgoal):
 1. infinite {t. q |\<in>| ta_der \ (term_of_gterm t) \<and> fst (groot_sym t) = None}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
ground (C ^ Suc ?n2)\<langle>t\<rangle>

goal (1 subgoal):
 1. infinite {t. q |\<in>| ta_der \ (term_of_gterm t) \<and> fst (groot_sym t) = None}
[PROOF STEP]
have "p |\<in>| ta_der \ (?terms n)" for n
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p |\<in>| ta_der \ (C ^ Suc n)\<langle>t\<rangle>
[PROOF STEP]
using reach t(1)
[PROOF STATE]
proof (prove)
using this:
p |\<in>| ta_der \ C\<langle>Var p\<rangle>
p |\<in>| ta_der \ t

goal (1 subgoal):
 1. p |\<in>| ta_der \ (C ^ Suc n)\<langle>t\<rangle>
[PROOF STEP]
by (auto simp: ta_der_ctxt) (meson ta_der_ctxt ta_der_ctxt_n_loop)
[PROOF STATE]
proof (state)
this:
p |\<in>| ta_der \ (C ^ Suc ?n2)\<langle>t\<rangle>

goal (1 subgoal):
 1. infinite {t. q |\<in>| ta_der \ (term_of_gterm t) \<and> fst (groot_sym t) = None}
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
ground (C ^ Suc ?n2)\<langle>t\<rangle>
p |\<in>| ta_der \ (C ^ Suc ?n2)\<langle>t\<rangle>
[PROOF STEP]
have inf: "infinite ?S"
[PROOF STATE]
proof (prove)
using this:
ground (C ^ Suc ?n2)\<langle>t\<rangle>
p |\<in>| ta_der \ (C ^ Suc ?n2)\<langle>t\<rangle>

goal (1 subgoal):
 1. infinite {(C ^ Suc n)\<langle>t\<rangle> |n. p |\<in>| ta_der \ (C ^ Suc n)\<langle>t\<rangle> \<and> ground (C ^ Suc n)\<langle>t\<rangle>}
[PROOF STEP]
using ctxt_comp_n_lower_bound[OF ctxt(1)]
[PROOF STATE]
proof (prove)
using this:
ground (C ^ Suc ?n2)\<langle>t\<rangle>
p |\<in>| ta_der \ (C ^ Suc ?n2)\<langle>t\<rangle>
?n < depth (C ^ Suc ?n)\<langle>?t\<rangle>

goal (1 subgoal):
 1. infinite {(C ^ Suc n)\<langle>t\<rangle> |n. p |\<in>| ta_der \ (C ^ Suc n)\<langle>t\<rangle> \<and> ground (C ^ Suc n)\<langle>t\<rangle>}
[PROOF STEP]
using no_upper_bound_infinite[of _ depth, of ?S]
[PROOF STATE]
proof (prove)
using this:
ground (C ^ Suc ?n2)\<langle>t\<rangle>
p |\<in>| ta_der \ (C ^ Suc ?n2)\<langle>t\<rangle>
?n < depth (C ^ Suc ?n)\<langle>?t\<rangle>
\<forall>n. \<exists>t\<in>{(C ^ Suc n)\<langle>t\<rangle> |n. p |\<in>| ta_der \ (C ^ Suc n)\<langle>t\<rangle> \<and> ground (C ^ Suc n)\<langle>t\<rangle>}. n < depth t \<Longrightarrow> infinite {(C ^ Suc n)\<langle>t\<rangle> |n. p |\<in>| ta_der \ (C ^ Suc n)\<langle>t\<rangle> \<and> ground (C ^ Suc n)\<langle>t\<rangle>}

goal (1 subgoal):
 1. infinite {(C ^ Suc n)\<langle>t\<rangle> |n. p |\<in>| ta_der \ (C ^ Suc n)\<langle>t\<rangle> \<and> ground (C ^ Suc n)\<langle>t\<rangle>}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
infinite {(C ^ Suc n)\<langle>t\<rangle> |n. p |\<in>| ta_der \ (C ^ Suc n)\<langle>t\<rangle> \<and> ground (C ^ Suc n)\<langle>t\<rangle>}

goal (1 subgoal):
 1. infinite {t. q |\<in>| ta_der \ (term_of_gterm t) \<and> fst (groot_sym t) = None}
[PROOF STEP]
from infinite_inj_image_infinite[OF this]
[PROOF STATE]
proof (chain)
picking this:
inj_on ?f {(C ^ Suc n)\<langle>t\<rangle> |n. p |\<in>| ta_der \ (C ^ Suc n)\<langle>t\<rangle> \<and> ground (C ^ Suc n)\<langle>t\<rangle>} \<Longrightarrow> infinite (?f ` {(C ^ Suc n)\<langle>t\<rangle> |n. p |\<in>| ta_der \ (C ^ Suc n)\<langle>t\<rangle> \<and> ground (C ^ Suc n)\<langle>t\<rangle>})
[PROOF STEP]
have inf:"infinite (ctxt_apply_term C2 ` ?S)"
[PROOF STATE]
proof (prove)
using this:
inj_on ?f {(C ^ Suc n)\<langle>t\<rangle> |n. p |\<in>| ta_der \ (C ^ Suc n)\<langle>t\<rangle> \<and> ground (C ^ Suc n)\<langle>t\<rangle>} \<Longrightarrow> infinite (?f ` {(C ^ Suc n)\<langle>t\<rangle> |n. p |\<in>| ta_der \ (C ^ Suc n)\<langle>t\<rangle> \<and> ground (C ^ Suc n)\<langle>t\<rangle>})

goal (1 subgoal):
 1. infinite (ctxt_apply_term C2 ` {(C ^ Suc n)\<langle>t\<rangle> |n. p |\<in>| ta_der \ (C ^ Suc n)\<langle>t\<rangle> \<and> ground (C ^ Suc n)\<langle>t\<rangle>})
[PROOF STEP]
by (smt ctxt_eq inj_on_def)
[PROOF STATE]
proof (state)
this:
infinite (ctxt_apply_term C2 ` {(C ^ Suc n)\<langle>t\<rangle> |n. p |\<in>| ta_der \ (C ^ Suc n)\<langle>t\<rangle> \<and> ground (C ^ Suc n)\<langle>t\<rangle>})

goal (1 subgoal):
 1. infinite {t. q |\<in>| ta_der \ (term_of_gterm t) \<and> fst (groot_sym t) = None}
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
infinite (ctxt_apply_term C2 ` {(C ^ Suc n)\<langle>t\<rangle> |n. p |\<in>| ta_der \ (C ^ Suc n)\<langle>t\<rangle> \<and> ground (C ^ Suc n)\<langle>t\<rangle>})

goal (1 subgoal):
 1. infinite {t. q |\<in>| ta_der \ (term_of_gterm t) \<and> fst (groot_sym t) = None}
[PROOF STEP]
fix u
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. infinite {t. q |\<in>| ta_der \ (term_of_gterm t) \<and> fst (groot_sym t) = None}
[PROOF STEP]
assume "u \<in> (ctxt_apply_term C2 ` ?S)"
[PROOF STATE]
proof (state)
this:
u \<in> ctxt_apply_term C2 ` {(C ^ Suc n)\<langle>t\<rangle> |n. p |\<in>| ta_der \ (C ^ Suc n)\<langle>t\<rangle> \<and> ground (C ^ Suc n)\<langle>t\<rangle>}

goal (1 subgoal):
 1. infinite {t. q |\<in>| ta_der \ (term_of_gterm t) \<and> fst (groot_sym t) = None}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
u \<in> ctxt_apply_term C2 ` {(C ^ Suc n)\<langle>t\<rangle> |n. p |\<in>| ta_der \ (C ^ Suc n)\<langle>t\<rangle> \<and> ground (C ^ Suc n)\<langle>t\<rangle>}
[PROOF STEP]
have "?P u"
[PROOF STATE]
proof (prove)
using this:
u \<in> ctxt_apply_term C2 ` {(C ^ Suc n)\<langle>t\<rangle> |n. p |\<in>| ta_der \ (C ^ Suc n)\<langle>t\<rangle> \<and> ground (C ^ Suc n)\<langle>t\<rangle>}

goal (1 subgoal):
 1. ground u \<and> q |\<in>| ta_der \ u \<and> fst (fst (the (root u))) = None
[PROOF STEP]
unfolding image_Collect
[PROOF STATE]
proof (prove)
using this:
u \<in> {C2\<langle>x\<rangle> |x. \<exists>n. x = (C ^ Suc n)\<langle>t\<rangle> \<and> p |\<in>| ta_der \ (C ^ Suc n)\<langle>t\<rangle> \<and> ground (C ^ Suc n)\<langle>t\<rangle>}

goal (1 subgoal):
 1. ground u \<and> q |\<in>| ta_der \ u \<and> fst (fst (the (root u))) = None
[PROOF STEP]
using closing_ctxt cl_reach
[PROOF STATE]
proof (prove)
using this:
u \<in> {C2\<langle>x\<rangle> |x. \<exists>n. x = (C ^ Suc n)\<langle>t\<rangle> \<and> p |\<in>| ta_der \ (C ^ Suc n)\<langle>t\<rangle> \<and> ground (C ^ Suc n)\<langle>t\<rangle>}
C2 \<noteq> \<box>
ground_ctxt C2
fst (root_ctxt C2) = None
q |\<in>| ta_der \ C2\<langle>Var p\<rangle>

goal (1 subgoal):
 1. ground u \<and> q |\<in>| ta_der \ u \<and> fst (fst (the (root u))) = None
[PROOF STEP]
by (auto simp: ta_der_ctxt)
[PROOF STATE]
proof (state)
this:
ground u \<and> q |\<in>| ta_der \ u \<and> fst (fst (the (root u))) = None

goal (1 subgoal):
 1. infinite {t. q |\<in>| ta_der \ (term_of_gterm t) \<and> fst (groot_sym t) = None}
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?u4 \<in> ctxt_apply_term C2 ` {(C ^ Suc n)\<langle>t\<rangle> |n. p |\<in>| ta_der \ (C ^ Suc n)\<langle>t\<rangle> \<and> ground (C ^ Suc n)\<langle>t\<rangle>} \<Longrightarrow> ground ?u4 \<and> q |\<in>| ta_der \ ?u4 \<and> fst (fst (the (root ?u4))) = None

goal (1 subgoal):
 1. infinite {t. q |\<in>| ta_der \ (term_of_gterm t) \<and> fst (groot_sym t) = None}
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
?u4 \<in> ctxt_apply_term C2 ` {(C ^ Suc n)\<langle>t\<rangle> |n. p |\<in>| ta_der \ (C ^ Suc n)\<langle>t\<rangle> \<and> ground (C ^ Suc n)\<langle>t\<rangle>} \<Longrightarrow> ground ?u4 \<and> q |\<in>| ta_der \ ?u4 \<and> fst (fst (the (root ?u4))) = None
[PROOF STEP]
have inf: "infinite {u. ground u \<and> q |\<in>| ta_der \ u \<and> fst (fst (the (root u))) = None}"
[PROOF STATE]
proof (prove)
using this:
?u4 \<in> ctxt_apply_term C2 ` {(C ^ Suc n)\<langle>t\<rangle> |n. p |\<in>| ta_der \ (C ^ Suc n)\<langle>t\<rangle> \<and> ground (C ^ Suc n)\<langle>t\<rangle>} \<Longrightarrow> ground ?u4 \<and> q |\<in>| ta_der \ ?u4 \<and> fst (fst (the (root ?u4))) = None

goal (1 subgoal):
 1. infinite {u. ground u \<and> q |\<in>| ta_der \ u \<and> fst (fst (the (root u))) = None}
[PROOF STEP]
by (intro infinite_super[OF _ inf] subsetI) fast
[PROOF STATE]
proof (state)
this:
infinite {u. ground u \<and> q |\<in>| ta_der \ u \<and> fst (fst (the (root u))) = None}

goal (1 subgoal):
 1. infinite {t. q |\<in>| ta_der \ (term_of_gterm t) \<and> fst (groot_sym t) = None}
[PROOF STEP]
have inf: "infinite (gterm_of_term ` {u. ground u \<and> q |\<in>| ta_der \ u \<and> fst (fst (the (root u))) = None})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. infinite (gterm_of_term ` {u. ground u \<and> q |\<in>| ta_der \ u \<and> fst (fst (the (root u))) = None})
[PROOF STEP]
by (intro infinite_inj_image_infinite[OF inf] gterm_of_term_inj) auto
[PROOF STATE]
proof (state)
this:
infinite (gterm_of_term ` {u. ground u \<and> q |\<in>| ta_der \ u \<and> fst (fst (the (root u))) = None})

goal (1 subgoal):
 1. infinite {t. q |\<in>| ta_der \ (term_of_gterm t) \<and> fst (groot_sym t) = None}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. infinite {t. q |\<in>| ta_der \ (term_of_gterm t) \<and> fst (groot_sym t) = None}
[PROOF STEP]
by (intro infinite_super[OF _ inf]) (auto dest: groot_sym_gterm_of_term)
[PROOF STATE]
proof (state)
this:
infinite {t. q |\<in>| ta_der \ (term_of_gterm t) \<and> fst (groot_sym t) = None}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma gfun_at_after_hole_pos:
  assumes "ghole_pos C \<le>\<^sub>p p"
  shows "gfun_at C\<langle>t\<rangle>\<^sub>G p = gfun_at t (p -\<^sub>p ghole_pos C)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gfun_at C\<langle>t\<rangle>\<^sub>G p = gfun_at t (p -\<^sub>p ghole_pos C)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
ghole_pos C \<le>\<^sub>p p

goal (1 subgoal):
 1. gfun_at C\<langle>t\<rangle>\<^sub>G p = gfun_at t (p -\<^sub>p ghole_pos C)
[PROOF STEP]
proof (induct C arbitrary: p)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>p. ghole_pos \<box>\<^sub>G \<le>\<^sub>p p \<Longrightarrow> gfun_at \<box>\<^sub>G\<langle>t\<rangle>\<^sub>G p = gfun_at t (p -\<^sub>p ghole_pos \<box>\<^sub>G)
 2. \<And>x1 x2 C x4 p. \<lbrakk>\<And>p. ghole_pos C \<le>\<^sub>p p \<Longrightarrow> gfun_at C\<langle>t\<rangle>\<^sub>G p = gfun_at t (p -\<^sub>p ghole_pos C); ghole_pos (GMore x1 x2 C x4) \<le>\<^sub>p p\<rbrakk> \<Longrightarrow> gfun_at (GMore x1 x2 C x4)\<langle>t\<rangle>\<^sub>G p = gfun_at t (p -\<^sub>p ghole_pos (GMore x1 x2 C x4))
[PROOF STEP]
case (GMore f ss C ts)
[PROOF STATE]
proof (state)
this:
ghole_pos C \<le>\<^sub>p ?p \<Longrightarrow> gfun_at C\<langle>t\<rangle>\<^sub>G ?p = gfun_at t (?p -\<^sub>p ghole_pos C)
ghole_pos (GMore f ss C ts) \<le>\<^sub>p p

goal (2 subgoals):
 1. \<And>p. ghole_pos \<box>\<^sub>G \<le>\<^sub>p p \<Longrightarrow> gfun_at \<box>\<^sub>G\<langle>t\<rangle>\<^sub>G p = gfun_at t (p -\<^sub>p ghole_pos \<box>\<^sub>G)
 2. \<And>x1 x2 C x4 p. \<lbrakk>\<And>p. ghole_pos C \<le>\<^sub>p p \<Longrightarrow> gfun_at C\<langle>t\<rangle>\<^sub>G p = gfun_at t (p -\<^sub>p ghole_pos C); ghole_pos (GMore x1 x2 C x4) \<le>\<^sub>p p\<rbrakk> \<Longrightarrow> gfun_at (GMore x1 x2 C x4)\<langle>t\<rangle>\<^sub>G p = gfun_at t (p -\<^sub>p ghole_pos (GMore x1 x2 C x4))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ghole_pos C \<le>\<^sub>p ?p \<Longrightarrow> gfun_at C\<langle>t\<rangle>\<^sub>G ?p = gfun_at t (?p -\<^sub>p ghole_pos C)
ghole_pos (GMore f ss C ts) \<le>\<^sub>p p
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
ghole_pos C \<le>\<^sub>p ?p \<Longrightarrow> gfun_at C\<langle>t\<rangle>\<^sub>G ?p = gfun_at t (?p -\<^sub>p ghole_pos C)
ghole_pos (GMore f ss C ts) \<le>\<^sub>p p

goal (1 subgoal):
 1. gfun_at (GMore f ss C ts)\<langle>t\<rangle>\<^sub>G p = gfun_at t (p -\<^sub>p ghole_pos (GMore f ss C ts))
[PROOF STEP]
by (cases p) auto
[PROOF STATE]
proof (state)
this:
gfun_at (GMore f ss C ts)\<langle>t\<rangle>\<^sub>G p = gfun_at t (p -\<^sub>p ghole_pos (GMore f ss C ts))

goal (1 subgoal):
 1. \<And>p. ghole_pos \<box>\<^sub>G \<le>\<^sub>p p \<Longrightarrow> gfun_at \<box>\<^sub>G\<langle>t\<rangle>\<^sub>G p = gfun_at t (p -\<^sub>p ghole_pos \<box>\<^sub>G)
[PROOF STEP]
qed auto


[STATEMENT]
lemma pos_diff_0 [simp]: "p -\<^sub>p p = []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p -\<^sub>p p = []
[PROOF STEP]
by (auto simp: pos_diff_def)


[STATEMENT]
lemma Max_suffI: "finite A \<Longrightarrow> A = B \<Longrightarrow> Max A = Max B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>finite A; A = B\<rbrakk> \<Longrightarrow> Max A = Max B
[PROOF STEP]
by (intro Max_eq_if) auto


[STATEMENT]
lemma nth_args_depth_eqI:
  assumes "length ss = length ts"
    and "\<And> i. i < length ts \<Longrightarrow> depth (ss ! i) = depth (ts ! i)"
  shows "depth (Fun f ss) = depth (Fun g ts)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. depth (Fun f ss) = depth (Fun g ts)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. depth (Fun f ss) = depth (Fun g ts)
[PROOF STEP]
from assms(1, 2)
[PROOF STATE]
proof (chain)
picking this:
length ss = length ts
?i < length ts \<Longrightarrow> depth (ss ! ?i) = depth (ts ! ?i)
[PROOF STEP]
have "depth ` set ss = depth ` set ts"
[PROOF STATE]
proof (prove)
using this:
length ss = length ts
?i < length ts \<Longrightarrow> depth (ss ! ?i) = depth (ts ! ?i)

goal (1 subgoal):
 1. depth ` set ss = depth ` set ts
[PROOF STEP]
using nth_map_conv[OF assms(1), of depth depth]
[PROOF STATE]
proof (prove)
using this:
length ss = length ts
?i < length ts \<Longrightarrow> depth (ss ! ?i) = depth (ts ! ?i)
\<forall>i<length ss. depth (ss ! i) = depth (ts ! i) \<Longrightarrow> map depth ss = map depth ts

goal (1 subgoal):
 1. depth ` set ss = depth ` set ts
[PROOF STEP]
by (simp flip: set_map)
[PROOF STATE]
proof (state)
this:
depth ` set ss = depth ` set ts

goal (1 subgoal):
 1. depth (Fun f ss) = depth (Fun g ts)
[PROOF STEP]
from Max_suffI[OF _ this]
[PROOF STATE]
proof (chain)
picking this:
finite (depth ` set ss) \<Longrightarrow> Max (depth ` set ss) = Max (depth ` set ts)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
finite (depth ` set ss) \<Longrightarrow> Max (depth ` set ss) = Max (depth ` set ts)

goal (1 subgoal):
 1. depth (Fun f ss) = depth (Fun g ts)
[PROOF STEP]
using assms(1)
[PROOF STATE]
proof (prove)
using this:
finite (depth ` set ss) \<Longrightarrow> Max (depth ` set ss) = Max (depth ` set ts)
length ss = length ts

goal (1 subgoal):
 1. depth (Fun f ss) = depth (Fun g ts)
[PROOF STEP]
by (cases ss; cases ts) auto
[PROOF STATE]
proof (state)
this:
depth (Fun f ss) = depth (Fun g ts)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma subt_at_ctxt_apply_hole_pos [simp]: "C\<langle>s\<rangle> |_ hole_pos C = s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. C\<langle>s\<rangle> |_ hole_pos C = s
[PROOF STEP]
by (induct C) auto


[STATEMENT]
lemma ctxt_at_pos_ctxt_apply_hole_poss [simp]: "ctxt_at_pos C\<langle>s\<rangle> (hole_pos C) = C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ctxt_at_pos C\<langle>s\<rangle> (hole_pos C) = C
[PROOF STEP]
by (induct C) auto


[STATEMENT]
lemma map_funs_term_ctxt_apply [simp]:
  "map_funs_term f C\<langle>s\<rangle> = (map_funs_ctxt f C)\<langle>map_funs_term f s\<rangle>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_funs_term f C\<langle>s\<rangle> = (map_funs_ctxt f C)\<langle>map_funs_term f s\<rangle>
[PROOF STEP]
by (induct C) auto


[STATEMENT]
lemma map_funs_term_ctxt_decomp:
  assumes "map_funs_term fg t = C\<langle>s\<rangle>"
  shows "\<exists> D u. C = map_funs_ctxt fg D \<and> s = map_funs_term fg u \<and> t = D\<langle>u\<rangle>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>D u. C = map_funs_ctxt fg D \<and> s = map_funs_term fg u \<and> t = D\<langle>u\<rangle>
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
map_funs_term fg t = C\<langle>s\<rangle>

goal (1 subgoal):
 1. \<exists>D u. C = map_funs_ctxt fg D \<and> s = map_funs_term fg u \<and> t = D\<langle>u\<rangle>
[PROOF STEP]
proof (induct C arbitrary: t)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>t. map_funs_term fg t = \<box>\<langle>s\<rangle> \<Longrightarrow> \<exists>D u. \<box> = map_funs_ctxt fg D \<and> s = map_funs_term fg u \<and> t = D\<langle>u\<rangle>
 2. \<And>x1 x2 C x4 t. \<lbrakk>\<And>t. map_funs_term fg t = C\<langle>s\<rangle> \<Longrightarrow> \<exists>D u. C = map_funs_ctxt fg D \<and> s = map_funs_term fg u \<and> t = D\<langle>u\<rangle>; map_funs_term fg t = (More x1 x2 C x4)\<langle>s\<rangle>\<rbrakk> \<Longrightarrow> \<exists>D u. More x1 x2 C x4 = map_funs_ctxt fg D \<and> s = map_funs_term fg u \<and> t = D\<langle>u\<rangle>
[PROOF STEP]
case Hole
[PROOF STATE]
proof (state)
this:
map_funs_term fg t = \<box>\<langle>s\<rangle>

goal (2 subgoals):
 1. \<And>t. map_funs_term fg t = \<box>\<langle>s\<rangle> \<Longrightarrow> \<exists>D u. \<box> = map_funs_ctxt fg D \<and> s = map_funs_term fg u \<and> t = D\<langle>u\<rangle>
 2. \<And>x1 x2 C x4 t. \<lbrakk>\<And>t. map_funs_term fg t = C\<langle>s\<rangle> \<Longrightarrow> \<exists>D u. C = map_funs_ctxt fg D \<and> s = map_funs_term fg u \<and> t = D\<langle>u\<rangle>; map_funs_term fg t = (More x1 x2 C x4)\<langle>s\<rangle>\<rbrakk> \<Longrightarrow> \<exists>D u. More x1 x2 C x4 = map_funs_ctxt fg D \<and> s = map_funs_term fg u \<and> t = D\<langle>u\<rangle>
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>D u. \<box> = map_funs_ctxt fg D \<and> s = map_funs_term fg u \<and> t = D\<langle>u\<rangle>
[PROOF STEP]
by (rule exI[of _ Hole], rule exI[of _ t], insert Hole, auto)
[PROOF STATE]
proof (state)
this:
\<exists>D u. \<box> = map_funs_ctxt fg D \<and> s = map_funs_term fg u \<and> t = D\<langle>u\<rangle>

goal (1 subgoal):
 1. \<And>x1 x2 C x4 t. \<lbrakk>\<And>t. map_funs_term fg t = C\<langle>s\<rangle> \<Longrightarrow> \<exists>D u. C = map_funs_ctxt fg D \<and> s = map_funs_term fg u \<and> t = D\<langle>u\<rangle>; map_funs_term fg t = (More x1 x2 C x4)\<langle>s\<rangle>\<rbrakk> \<Longrightarrow> \<exists>D u. More x1 x2 C x4 = map_funs_ctxt fg D \<and> s = map_funs_term fg u \<and> t = D\<langle>u\<rangle>
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x1 x2 C x4 t. \<lbrakk>\<And>t. map_funs_term fg t = C\<langle>s\<rangle> \<Longrightarrow> \<exists>D u. C = map_funs_ctxt fg D \<and> s = map_funs_term fg u \<and> t = D\<langle>u\<rangle>; map_funs_term fg t = (More x1 x2 C x4)\<langle>s\<rangle>\<rbrakk> \<Longrightarrow> \<exists>D u. More x1 x2 C x4 = map_funs_ctxt fg D \<and> s = map_funs_term fg u \<and> t = D\<langle>u\<rangle>
[PROOF STEP]
case (More g bef C aft)
[PROOF STATE]
proof (state)
this:
map_funs_term fg ?t = C\<langle>s\<rangle> \<Longrightarrow> \<exists>D u. C = map_funs_ctxt fg D \<and> s = map_funs_term fg u \<and> ?t = D\<langle>u\<rangle>
map_funs_term fg t = (More g bef C aft)\<langle>s\<rangle>

goal (1 subgoal):
 1. \<And>x1 x2 C x4 t. \<lbrakk>\<And>t. map_funs_term fg t = C\<langle>s\<rangle> \<Longrightarrow> \<exists>D u. C = map_funs_ctxt fg D \<and> s = map_funs_term fg u \<and> t = D\<langle>u\<rangle>; map_funs_term fg t = (More x1 x2 C x4)\<langle>s\<rangle>\<rbrakk> \<Longrightarrow> \<exists>D u. More x1 x2 C x4 = map_funs_ctxt fg D \<and> s = map_funs_term fg u \<and> t = D\<langle>u\<rangle>
[PROOF STEP]
from More(2)
[PROOF STATE]
proof (chain)
picking this:
map_funs_term fg t = (More g bef C aft)\<langle>s\<rangle>
[PROOF STEP]
obtain f ts where t: "t = Fun f ts"
[PROOF STATE]
proof (prove)
using this:
map_funs_term fg t = (More g bef C aft)\<langle>s\<rangle>

goal (1 subgoal):
 1. (\<And>f ts. t = Fun f ts \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (cases t, auto)
[PROOF STATE]
proof (state)
this:
t = Fun f ts

goal (1 subgoal):
 1. \<And>x1 x2 C x4 t. \<lbrakk>\<And>t. map_funs_term fg t = C\<langle>s\<rangle> \<Longrightarrow> \<exists>D u. C = map_funs_ctxt fg D \<and> s = map_funs_term fg u \<and> t = D\<langle>u\<rangle>; map_funs_term fg t = (More x1 x2 C x4)\<langle>s\<rangle>\<rbrakk> \<Longrightarrow> \<exists>D u. More x1 x2 C x4 = map_funs_ctxt fg D \<and> s = map_funs_term fg u \<and> t = D\<langle>u\<rangle>
[PROOF STEP]
from More(2)[unfolded t]
[PROOF STATE]
proof (chain)
picking this:
map_funs_term fg (Fun f ts) = (More g bef C aft)\<langle>s\<rangle>
[PROOF STEP]
have f: "fg f = g" and ts: "map (map_funs_term fg) ts = bef @ C\<langle>s\<rangle> # aft" (is "?ts = ?bca")
[PROOF STATE]
proof (prove)
using this:
map_funs_term fg (Fun f ts) = (More g bef C aft)\<langle>s\<rangle>

goal (1 subgoal):
 1. fg f = g &&& map (map_funs_term fg) ts = bef @ C\<langle>s\<rangle> # aft
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
fg f = g
map (map_funs_term fg) ts = bef @ C\<langle>s\<rangle> # aft

goal (1 subgoal):
 1. \<And>x1 x2 C x4 t. \<lbrakk>\<And>t. map_funs_term fg t = C\<langle>s\<rangle> \<Longrightarrow> \<exists>D u. C = map_funs_ctxt fg D \<and> s = map_funs_term fg u \<and> t = D\<langle>u\<rangle>; map_funs_term fg t = (More x1 x2 C x4)\<langle>s\<rangle>\<rbrakk> \<Longrightarrow> \<exists>D u. More x1 x2 C x4 = map_funs_ctxt fg D \<and> s = map_funs_term fg u \<and> t = D\<langle>u\<rangle>
[PROOF STEP]
from ts
[PROOF STATE]
proof (chain)
picking this:
map (map_funs_term fg) ts = bef @ C\<langle>s\<rangle> # aft
[PROOF STEP]
have "length ?ts = length ?bca"
[PROOF STATE]
proof (prove)
using this:
map (map_funs_term fg) ts = bef @ C\<langle>s\<rangle> # aft

goal (1 subgoal):
 1. length (map (map_funs_term fg) ts) = length (bef @ C\<langle>s\<rangle> # aft)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
length (map (map_funs_term fg) ts) = length (bef @ C\<langle>s\<rangle> # aft)

goal (1 subgoal):
 1. \<And>x1 x2 C x4 t. \<lbrakk>\<And>t. map_funs_term fg t = C\<langle>s\<rangle> \<Longrightarrow> \<exists>D u. C = map_funs_ctxt fg D \<and> s = map_funs_term fg u \<and> t = D\<langle>u\<rangle>; map_funs_term fg t = (More x1 x2 C x4)\<langle>s\<rangle>\<rbrakk> \<Longrightarrow> \<exists>D u. More x1 x2 C x4 = map_funs_ctxt fg D \<and> s = map_funs_term fg u \<and> t = D\<langle>u\<rangle>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
length (map (map_funs_term fg) ts) = length (bef @ C\<langle>s\<rangle> # aft)
[PROOF STEP]
have len: "length ts = length ?bca"
[PROOF STATE]
proof (prove)
using this:
length (map (map_funs_term fg) ts) = length (bef @ C\<langle>s\<rangle> # aft)

goal (1 subgoal):
 1. length ts = length (bef @ C\<langle>s\<rangle> # aft)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
length ts = length (bef @ C\<langle>s\<rangle> # aft)

goal (1 subgoal):
 1. \<And>x1 x2 C x4 t. \<lbrakk>\<And>t. map_funs_term fg t = C\<langle>s\<rangle> \<Longrightarrow> \<exists>D u. C = map_funs_ctxt fg D \<and> s = map_funs_term fg u \<and> t = D\<langle>u\<rangle>; map_funs_term fg t = (More x1 x2 C x4)\<langle>s\<rangle>\<rbrakk> \<Longrightarrow> \<exists>D u. More x1 x2 C x4 = map_funs_ctxt fg D \<and> s = map_funs_term fg u \<and> t = D\<langle>u\<rangle>
[PROOF STEP]
note id = ts[unfolded map_nth_eq_conv[OF len], THEN spec, THEN mp]
[PROOF STATE]
proof (state)
this:
?x1 < length (bef @ C\<langle>s\<rangle> # aft) \<Longrightarrow> map_funs_term fg (ts ! ?x1) = (bef @ C\<langle>s\<rangle> # aft) ! ?x1

goal (1 subgoal):
 1. \<And>x1 x2 C x4 t. \<lbrakk>\<And>t. map_funs_term fg t = C\<langle>s\<rangle> \<Longrightarrow> \<exists>D u. C = map_funs_ctxt fg D \<and> s = map_funs_term fg u \<and> t = D\<langle>u\<rangle>; map_funs_term fg t = (More x1 x2 C x4)\<langle>s\<rangle>\<rbrakk> \<Longrightarrow> \<exists>D u. More x1 x2 C x4 = map_funs_ctxt fg D \<and> s = map_funs_term fg u \<and> t = D\<langle>u\<rangle>
[PROOF STEP]
let ?i = "length bef"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x1 x2 C x4 t. \<lbrakk>\<And>t. map_funs_term fg t = C\<langle>s\<rangle> \<Longrightarrow> \<exists>D u. C = map_funs_ctxt fg D \<and> s = map_funs_term fg u \<and> t = D\<langle>u\<rangle>; map_funs_term fg t = (More x1 x2 C x4)\<langle>s\<rangle>\<rbrakk> \<Longrightarrow> \<exists>D u. More x1 x2 C x4 = map_funs_ctxt fg D \<and> s = map_funs_term fg u \<and> t = D\<langle>u\<rangle>
[PROOF STEP]
from len
[PROOF STATE]
proof (chain)
picking this:
length ts = length (bef @ C\<langle>s\<rangle> # aft)
[PROOF STEP]
have i: "?i < length ts"
[PROOF STATE]
proof (prove)
using this:
length ts = length (bef @ C\<langle>s\<rangle> # aft)

goal (1 subgoal):
 1. length bef < length ts
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
length bef < length ts

goal (1 subgoal):
 1. \<And>x1 x2 C x4 t. \<lbrakk>\<And>t. map_funs_term fg t = C\<langle>s\<rangle> \<Longrightarrow> \<exists>D u. C = map_funs_ctxt fg D \<and> s = map_funs_term fg u \<and> t = D\<langle>u\<rangle>; map_funs_term fg t = (More x1 x2 C x4)\<langle>s\<rangle>\<rbrakk> \<Longrightarrow> \<exists>D u. More x1 x2 C x4 = map_funs_ctxt fg D \<and> s = map_funs_term fg u \<and> t = D\<langle>u\<rangle>
[PROOF STEP]
from id[of ?i]
[PROOF STATE]
proof (chain)
picking this:
length bef < length (bef @ C\<langle>s\<rangle> # aft) \<Longrightarrow> map_funs_term fg (ts ! length bef) = (bef @ C\<langle>s\<rangle> # aft) ! length bef
[PROOF STEP]
have "map_funs_term fg (ts ! ?i) = C\<langle>s\<rangle>"
[PROOF STATE]
proof (prove)
using this:
length bef < length (bef @ C\<langle>s\<rangle> # aft) \<Longrightarrow> map_funs_term fg (ts ! length bef) = (bef @ C\<langle>s\<rangle> # aft) ! length bef

goal (1 subgoal):
 1. map_funs_term fg (ts ! length bef) = C\<langle>s\<rangle>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
map_funs_term fg (ts ! length bef) = C\<langle>s\<rangle>

goal (1 subgoal):
 1. \<And>x1 x2 C x4 t. \<lbrakk>\<And>t. map_funs_term fg t = C\<langle>s\<rangle> \<Longrightarrow> \<exists>D u. C = map_funs_ctxt fg D \<and> s = map_funs_term fg u \<and> t = D\<langle>u\<rangle>; map_funs_term fg t = (More x1 x2 C x4)\<langle>s\<rangle>\<rbrakk> \<Longrightarrow> \<exists>D u. More x1 x2 C x4 = map_funs_ctxt fg D \<and> s = map_funs_term fg u \<and> t = D\<langle>u\<rangle>
[PROOF STEP]
from More(1)[OF this]
[PROOF STATE]
proof (chain)
picking this:
\<exists>D u. C = map_funs_ctxt fg D \<and> s = map_funs_term fg u \<and> ts ! length bef = D\<langle>u\<rangle>
[PROOF STEP]
obtain D u where D: "C = map_funs_ctxt fg D" and
    u: "s = map_funs_term fg u" and id: "ts ! ?i = D\<langle>u\<rangle>"
[PROOF STATE]
proof (prove)
using this:
\<exists>D u. C = map_funs_ctxt fg D \<and> s = map_funs_term fg u \<and> ts ! length bef = D\<langle>u\<rangle>

goal (1 subgoal):
 1. (\<And>D u. \<lbrakk>C = map_funs_ctxt fg D; s = map_funs_term fg u; ts ! length bef = D\<langle>u\<rangle>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
C = map_funs_ctxt fg D
s = map_funs_term fg u
ts ! length bef = D\<langle>u\<rangle>

goal (1 subgoal):
 1. \<And>x1 x2 C x4 t. \<lbrakk>\<And>t. map_funs_term fg t = C\<langle>s\<rangle> \<Longrightarrow> \<exists>D u. C = map_funs_ctxt fg D \<and> s = map_funs_term fg u \<and> t = D\<langle>u\<rangle>; map_funs_term fg t = (More x1 x2 C x4)\<langle>s\<rangle>\<rbrakk> \<Longrightarrow> \<exists>D u. More x1 x2 C x4 = map_funs_ctxt fg D \<and> s = map_funs_term fg u \<and> t = D\<langle>u\<rangle>
[PROOF STEP]
from ts
[PROOF STATE]
proof (chain)
picking this:
map (map_funs_term fg) ts = bef @ C\<langle>s\<rangle> # aft
[PROOF STEP]
have "take ?i ?ts = take ?i ?bca"
[PROOF STATE]
proof (prove)
using this:
map (map_funs_term fg) ts = bef @ C\<langle>s\<rangle> # aft

goal (1 subgoal):
 1. take (length bef) (map (map_funs_term fg) ts) = take (length bef) (bef @ C\<langle>s\<rangle> # aft)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
take (length bef) (map (map_funs_term fg) ts) = take (length bef) (bef @ C\<langle>s\<rangle> # aft)

goal (1 subgoal):
 1. \<And>x1 x2 C x4 t. \<lbrakk>\<And>t. map_funs_term fg t = C\<langle>s\<rangle> \<Longrightarrow> \<exists>D u. C = map_funs_ctxt fg D \<and> s = map_funs_term fg u \<and> t = D\<langle>u\<rangle>; map_funs_term fg t = (More x1 x2 C x4)\<langle>s\<rangle>\<rbrakk> \<Longrightarrow> \<exists>D u. More x1 x2 C x4 = map_funs_ctxt fg D \<and> s = map_funs_term fg u \<and> t = D\<langle>u\<rangle>
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
take (length bef) (map (map_funs_term fg) ts) = take (length bef) (bef @ C\<langle>s\<rangle> # aft)

goal (1 subgoal):
 1. \<And>x1 x2 C x4 t. \<lbrakk>\<And>t. map_funs_term fg t = C\<langle>s\<rangle> \<Longrightarrow> \<exists>D u. C = map_funs_ctxt fg D \<and> s = map_funs_term fg u \<and> t = D\<langle>u\<rangle>; map_funs_term fg t = (More x1 x2 C x4)\<langle>s\<rangle>\<rbrakk> \<Longrightarrow> \<exists>D u. More x1 x2 C x4 = map_funs_ctxt fg D \<and> s = map_funs_term fg u \<and> t = D\<langle>u\<rangle>
[PROOF STEP]
have "... = bef"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. take (length bef) (bef @ C\<langle>s\<rangle> # aft) = bef
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
take (length bef) (bef @ C\<langle>s\<rangle> # aft) = bef

goal (1 subgoal):
 1. \<And>x1 x2 C x4 t. \<lbrakk>\<And>t. map_funs_term fg t = C\<langle>s\<rangle> \<Longrightarrow> \<exists>D u. C = map_funs_ctxt fg D \<and> s = map_funs_term fg u \<and> t = D\<langle>u\<rangle>; map_funs_term fg t = (More x1 x2 C x4)\<langle>s\<rangle>\<rbrakk> \<Longrightarrow> \<exists>D u. More x1 x2 C x4 = map_funs_ctxt fg D \<and> s = map_funs_term fg u \<and> t = D\<langle>u\<rangle>
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
take (length bef) (map (map_funs_term fg) ts) = bef
[PROOF STEP]
have bef: "map (map_funs_term fg) (take ?i ts) = bef"
[PROOF STATE]
proof (prove)
using this:
take (length bef) (map (map_funs_term fg) ts) = bef

goal (1 subgoal):
 1. map (map_funs_term fg) (take (length bef) ts) = bef
[PROOF STEP]
by (simp add: take_map)
[PROOF STATE]
proof (state)
this:
map (map_funs_term fg) (take (length bef) ts) = bef

goal (1 subgoal):
 1. \<And>x1 x2 C x4 t. \<lbrakk>\<And>t. map_funs_term fg t = C\<langle>s\<rangle> \<Longrightarrow> \<exists>D u. C = map_funs_ctxt fg D \<and> s = map_funs_term fg u \<and> t = D\<langle>u\<rangle>; map_funs_term fg t = (More x1 x2 C x4)\<langle>s\<rangle>\<rbrakk> \<Longrightarrow> \<exists>D u. More x1 x2 C x4 = map_funs_ctxt fg D \<and> s = map_funs_term fg u \<and> t = D\<langle>u\<rangle>
[PROOF STEP]
from ts
[PROOF STATE]
proof (chain)
picking this:
map (map_funs_term fg) ts = bef @ C\<langle>s\<rangle> # aft
[PROOF STEP]
have "drop (Suc ?i) ?ts = drop (Suc ?i) ?bca"
[PROOF STATE]
proof (prove)
using this:
map (map_funs_term fg) ts = bef @ C\<langle>s\<rangle> # aft

goal (1 subgoal):
 1. drop (Suc (length bef)) (map (map_funs_term fg) ts) = drop (Suc (length bef)) (bef @ C\<langle>s\<rangle> # aft)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
drop (Suc (length bef)) (map (map_funs_term fg) ts) = drop (Suc (length bef)) (bef @ C\<langle>s\<rangle> # aft)

goal (1 subgoal):
 1. \<And>x1 x2 C x4 t. \<lbrakk>\<And>t. map_funs_term fg t = C\<langle>s\<rangle> \<Longrightarrow> \<exists>D u. C = map_funs_ctxt fg D \<and> s = map_funs_term fg u \<and> t = D\<langle>u\<rangle>; map_funs_term fg t = (More x1 x2 C x4)\<langle>s\<rangle>\<rbrakk> \<Longrightarrow> \<exists>D u. More x1 x2 C x4 = map_funs_ctxt fg D \<and> s = map_funs_term fg u \<and> t = D\<langle>u\<rangle>
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
drop (Suc (length bef)) (map (map_funs_term fg) ts) = drop (Suc (length bef)) (bef @ C\<langle>s\<rangle> # aft)

goal (1 subgoal):
 1. \<And>x1 x2 C x4 t. \<lbrakk>\<And>t. map_funs_term fg t = C\<langle>s\<rangle> \<Longrightarrow> \<exists>D u. C = map_funs_ctxt fg D \<and> s = map_funs_term fg u \<and> t = D\<langle>u\<rangle>; map_funs_term fg t = (More x1 x2 C x4)\<langle>s\<rangle>\<rbrakk> \<Longrightarrow> \<exists>D u. More x1 x2 C x4 = map_funs_ctxt fg D \<and> s = map_funs_term fg u \<and> t = D\<langle>u\<rangle>
[PROOF STEP]
have "... = aft"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. drop (Suc (length bef)) (bef @ C\<langle>s\<rangle> # aft) = aft
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
drop (Suc (length bef)) (bef @ C\<langle>s\<rangle> # aft) = aft

goal (1 subgoal):
 1. \<And>x1 x2 C x4 t. \<lbrakk>\<And>t. map_funs_term fg t = C\<langle>s\<rangle> \<Longrightarrow> \<exists>D u. C = map_funs_ctxt fg D \<and> s = map_funs_term fg u \<and> t = D\<langle>u\<rangle>; map_funs_term fg t = (More x1 x2 C x4)\<langle>s\<rangle>\<rbrakk> \<Longrightarrow> \<exists>D u. More x1 x2 C x4 = map_funs_ctxt fg D \<and> s = map_funs_term fg u \<and> t = D\<langle>u\<rangle>
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
drop (Suc (length bef)) (map (map_funs_term fg) ts) = aft
[PROOF STEP]
have aft: "map (map_funs_term fg) (drop (Suc ?i) ts) = aft"
[PROOF STATE]
proof (prove)
using this:
drop (Suc (length bef)) (map (map_funs_term fg) ts) = aft

goal (1 subgoal):
 1. map (map_funs_term fg) (drop (Suc (length bef)) ts) = aft
[PROOF STEP]
by (simp add:drop_map)
[PROOF STATE]
proof (state)
this:
map (map_funs_term fg) (drop (Suc (length bef)) ts) = aft

goal (1 subgoal):
 1. \<And>x1 x2 C x4 t. \<lbrakk>\<And>t. map_funs_term fg t = C\<langle>s\<rangle> \<Longrightarrow> \<exists>D u. C = map_funs_ctxt fg D \<and> s = map_funs_term fg u \<and> t = D\<langle>u\<rangle>; map_funs_term fg t = (More x1 x2 C x4)\<langle>s\<rangle>\<rbrakk> \<Longrightarrow> \<exists>D u. More x1 x2 C x4 = map_funs_ctxt fg D \<and> s = map_funs_term fg u \<and> t = D\<langle>u\<rangle>
[PROOF STEP]
let ?bda = "take ?i ts @ D\<langle>u\<rangle> # drop (Suc ?i) ts"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x1 x2 C x4 t. \<lbrakk>\<And>t. map_funs_term fg t = C\<langle>s\<rangle> \<Longrightarrow> \<exists>D u. C = map_funs_ctxt fg D \<and> s = map_funs_term fg u \<and> t = D\<langle>u\<rangle>; map_funs_term fg t = (More x1 x2 C x4)\<langle>s\<rangle>\<rbrakk> \<Longrightarrow> \<exists>D u. More x1 x2 C x4 = map_funs_ctxt fg D \<and> s = map_funs_term fg u \<and> t = D\<langle>u\<rangle>
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>D u. More g bef C aft = map_funs_ctxt fg D \<and> s = map_funs_term fg u \<and> t = D\<langle>u\<rangle>
[PROOF STEP]
proof (rule exI[of _ "More f (take ?i ts) D (drop (Suc ?i) ts)"],
      rule exI[of _ u], simp add: u f D bef aft t)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ts = take (length bef) ts @ D\<langle>u\<rangle> # drop (Suc (length bef)) ts
[PROOF STEP]
have "ts = take ?i ts @ ts ! ?i # drop (Suc ?i) ts"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ts = take (length bef) ts @ ts ! length bef # drop (Suc (length bef)) ts
[PROOF STEP]
by (rule id_take_nth_drop[OF i])
[PROOF STATE]
proof (state)
this:
ts = take (length bef) ts @ ts ! length bef # drop (Suc (length bef)) ts

goal (1 subgoal):
 1. ts = take (length bef) ts @ D\<langle>u\<rangle> # drop (Suc (length bef)) ts
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
ts = take (length bef) ts @ ts ! length bef # drop (Suc (length bef)) ts

goal (1 subgoal):
 1. ts = take (length bef) ts @ D\<langle>u\<rangle> # drop (Suc (length bef)) ts
[PROOF STEP]
have "... = ?bda"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. take (length bef) ts @ ts ! length bef # drop (Suc (length bef)) ts = take (length bef) ts @ D\<langle>u\<rangle> # drop (Suc (length bef)) ts
[PROOF STEP]
by (simp add: id)
[PROOF STATE]
proof (state)
this:
take (length bef) ts @ ts ! length bef # drop (Suc (length bef)) ts = take (length bef) ts @ D\<langle>u\<rangle> # drop (Suc (length bef)) ts

goal (1 subgoal):
 1. ts = take (length bef) ts @ D\<langle>u\<rangle> # drop (Suc (length bef)) ts
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
ts = take (length bef) ts @ D\<langle>u\<rangle> # drop (Suc (length bef)) ts
[PROOF STEP]
show "ts = ?bda"
[PROOF STATE]
proof (prove)
using this:
ts = take (length bef) ts @ D\<langle>u\<rangle> # drop (Suc (length bef)) ts

goal (1 subgoal):
 1. ts = take (length bef) ts @ D\<langle>u\<rangle> # drop (Suc (length bef)) ts
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
ts = take (length bef) ts @ D\<langle>u\<rangle> # drop (Suc (length bef)) ts

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>D u. More g bef C aft = map_funs_ctxt fg D \<and> s = map_funs_term fg u \<and> t = D\<langle>u\<rangle>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma prod_automata_from_none_root_dec:
  assumes "gta_lang Q \ \<subseteq> {gpair s t| s t. funas_gterm s \<subseteq> \<F> \<and> funas_gterm t \<subseteq> \<F>}"
    and "q |\<in>| ta_der \ (term_of_gterm t)" and "fst (groot_sym t) = None"
    and "\<Q> \ |\<subseteq>| ta_reachable \" and "q |\<in>| ta_productive Q \"
  shows "\<exists> u. t = gterm_to_None_Some u \<and> funas_gterm u \<subseteq> \<F>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>u. t = gterm_to_None_Some u \<and> funas_gterm u \<subseteq> \<F>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>u. t = gterm_to_None_Some u \<and> funas_gterm u \<subseteq> \<F>
[PROOF STEP]
have *: "gfun_at t [] = Some (groot_sym t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gfun_at t [] = Some (groot_sym t)
[PROOF STEP]
by (cases t) auto
[PROOF STATE]
proof (state)
this:
gfun_at t [] = Some (groot_sym t)

goal (1 subgoal):
 1. \<exists>u. t = gterm_to_None_Some u \<and> funas_gterm u \<subseteq> \<F>
[PROOF STEP]
from assms(4, 5)
[PROOF STATE]
proof (chain)
picking this:
\<Q> \ |\<subseteq>| ta_reachable \
q |\<in>| ta_productive Q \
[PROOF STEP]
obtain C q\<^sub>f where ctxt: "ground_ctxt C" and
    fin: "q\<^sub>f |\<in>| ta_der \ C\<langle>Var q\<rangle>" "q\<^sub>f |\<in>| Q"
[PROOF STATE]
proof (prove)
using this:
\<Q> \ |\<subseteq>| ta_reachable \
q |\<in>| ta_productive Q \

goal (1 subgoal):
 1. (\<And>C q\<^sub>f. \<lbrakk>ground_ctxt C; q\<^sub>f |\<in>| ta_der \ C\<langle>Var q\<rangle>; q\<^sub>f |\<in>| Q\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp: ta_productive_def'[OF assms(4)])
[PROOF STATE]
proof (state)
this:
ground_ctxt C
q\<^sub>f |\<in>| ta_der \ C\<langle>Var q\<rangle>
q\<^sub>f |\<in>| Q

goal (1 subgoal):
 1. \<exists>u. t = gterm_to_None_Some u \<and> funas_gterm u \<subseteq> \<F>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ground_ctxt C
q\<^sub>f |\<in>| ta_der \ C\<langle>Var q\<rangle>
q\<^sub>f |\<in>| Q
[PROOF STEP]
obtain s v where gp: "gpair s v = (gctxt_of_ctxt C)\<langle>t\<rangle>\<^sub>G" and
   funas: "funas_gterm v \<subseteq> \<F>"
[PROOF STATE]
proof (prove)
using this:
ground_ctxt C
q\<^sub>f |\<in>| ta_der \ C\<langle>Var q\<rangle>
q\<^sub>f |\<in>| Q

goal (1 subgoal):
 1. (\<And>s v. \<lbrakk>gpair s v = (gctxt_of_ctxt C)\<langle>t\<rangle>\<^sub>G; funas_gterm v \<subseteq> \<F>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms(1, 2) gta_langI[OF fin(2), of \ "(gctxt_of_ctxt C)\<langle>t\<rangle>\<^sub>G"]
[PROOF STATE]
proof (prove)
using this:
ground_ctxt C
q\<^sub>f |\<in>| ta_der \ C\<langle>Var q\<rangle>
q\<^sub>f |\<in>| Q
gta_lang Q \ \<subseteq> {gpair s t |s t. funas_gterm s \<subseteq> \<F> \<and> funas_gterm t \<subseteq> \<F>}
q |\<in>| ta_der \ (term_of_gterm t)
q\<^sub>f |\<in>| ta_der \ (term_of_gterm (gctxt_of_ctxt C)\<langle>t\<rangle>\<^sub>G) \<Longrightarrow> (gctxt_of_ctxt C)\<langle>t\<rangle>\<^sub>G \<in> gta_lang Q \

goal (1 subgoal):
 1. (\<And>s v. \<lbrakk>gpair s v = (gctxt_of_ctxt C)\<langle>t\<rangle>\<^sub>G; funas_gterm v \<subseteq> \<F>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp: ta_der_ctxt ground_gctxt_of_ctxt_apply_gterm)
[PROOF STATE]
proof (state)
this:
gpair s v = (gctxt_of_ctxt C)\<langle>t\<rangle>\<^sub>G
funas_gterm v \<subseteq> \<F>

goal (1 subgoal):
 1. \<exists>u. t = gterm_to_None_Some u \<and> funas_gterm u \<subseteq> \<F>
[PROOF STEP]
from gp
[PROOF STATE]
proof (chain)
picking this:
gpair s v = (gctxt_of_ctxt C)\<langle>t\<rangle>\<^sub>G
[PROOF STEP]
have mem: "hole_pos C \<in> gposs s \<union> gposs v"
[PROOF STATE]
proof (prove)
using this:
gpair s v = (gctxt_of_ctxt C)\<langle>t\<rangle>\<^sub>G

goal (1 subgoal):
 1. hole_pos C \<in> gposs s \<union> gposs v
[PROOF STEP]
by auto (metis Un_iff ctxt ghole_pos_in_apply gposs_of_gpair ground_hole_pos_to_ghole)
[PROOF STATE]
proof (state)
this:
hole_pos C \<in> gposs s \<union> gposs v

goal (1 subgoal):
 1. \<exists>u. t = gterm_to_None_Some u \<and> funas_gterm u \<subseteq> \<F>
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
hole_pos C \<in> gposs s \<union> gposs v
[PROOF STEP]
have "hole_pos C \<notin> gposs s"
[PROOF STATE]
proof (prove)
using this:
hole_pos C \<in> gposs s \<union> gposs v

goal (1 subgoal):
 1. hole_pos C \<notin> gposs s
[PROOF STEP]
using assms(3)
[PROOF STATE]
proof (prove)
using this:
hole_pos C \<in> gposs s \<union> gposs v
fst (groot_sym t) = None

goal (1 subgoal):
 1. hole_pos C \<notin> gposs s
[PROOF STEP]
using arg_cong[OF gp, of "\<lambda> t. gfun_at t (hole_pos C)"]
[PROOF STATE]
proof (prove)
using this:
hole_pos C \<in> gposs s \<union> gposs v
fst (groot_sym t) = None
gfun_at (gpair s v) (hole_pos C) = gfun_at (gctxt_of_ctxt C)\<langle>t\<rangle>\<^sub>G (hole_pos C)

goal (1 subgoal):
 1. hole_pos C \<notin> gposs s
[PROOF STEP]
using ground_hole_pos_to_ghole[OF ctxt]
[PROOF STATE]
proof (prove)
using this:
hole_pos C \<in> gposs s \<union> gposs v
fst (groot_sym t) = None
gfun_at (gpair s v) (hole_pos C) = gfun_at (gctxt_of_ctxt C)\<langle>t\<rangle>\<^sub>G (hole_pos C)
ghole_pos (gctxt_of_ctxt C) = hole_pos C

goal (1 subgoal):
 1. hole_pos C \<notin> gposs s
[PROOF STEP]
using gfun_at_after_hole_pos[OF position_less_refl, of "gctxt_of_ctxt C"]
[PROOF STATE]
proof (prove)
using this:
hole_pos C \<in> gposs s \<union> gposs v
fst (groot_sym t) = None
gfun_at (gpair s v) (hole_pos C) = gfun_at (gctxt_of_ctxt C)\<langle>t\<rangle>\<^sub>G (hole_pos C)
ghole_pos (gctxt_of_ctxt C) = hole_pos C
gfun_at (gctxt_of_ctxt C)\<langle>?t\<rangle>\<^sub>G (ghole_pos (gctxt_of_ctxt C)) = gfun_at ?t (ghole_pos (gctxt_of_ctxt C) -\<^sub>p ghole_pos (gctxt_of_ctxt C))

goal (1 subgoal):
 1. hole_pos C \<notin> gposs s
[PROOF STEP]
by (auto simp: gfun_at_gpair * split: if_splits)
       (metis fstI gfun_at_None_ngposs_iff)+
[PROOF STATE]
proof (state)
this:
hole_pos C \<notin> gposs s

goal (1 subgoal):
 1. \<exists>u. t = gterm_to_None_Some u \<and> funas_gterm u \<subseteq> \<F>
[PROOF STEP]
from subst_at_gpair_nt_poss_None_Some[OF _ this, of v] this
[PROOF STATE]
proof (chain)
picking this:
hole_pos C \<in> gposs v \<Longrightarrow> gsubt_at (gpair s v) (hole_pos C) = gterm_to_None_Some (gsubt_at v (hole_pos C))
hole_pos C \<notin> gposs s
[PROOF STEP]
have "t = gterm_to_None_Some (gsubt_at v (hole_pos C)) \<and> funas_gterm (gsubt_at v (hole_pos C)) \<subseteq> \<F>"
[PROOF STATE]
proof (prove)
using this:
hole_pos C \<in> gposs v \<Longrightarrow> gsubt_at (gpair s v) (hole_pos C) = gterm_to_None_Some (gsubt_at v (hole_pos C))
hole_pos C \<notin> gposs s

goal (1 subgoal):
 1. t = gterm_to_None_Some (gsubt_at v (hole_pos C)) \<and> funas_gterm (gsubt_at v (hole_pos C)) \<subseteq> \<F>
[PROOF STEP]
using funas mem funas_gterm_gsubt_at_subseteq
[PROOF STATE]
proof (prove)
using this:
hole_pos C \<in> gposs v \<Longrightarrow> gsubt_at (gpair s v) (hole_pos C) = gterm_to_None_Some (gsubt_at v (hole_pos C))
hole_pos C \<notin> gposs s
funas_gterm v \<subseteq> \<F>
hole_pos C \<in> gposs s \<union> gposs v
?p \<in> gposs ?s \<Longrightarrow> funas_gterm (gsubt_at ?s ?p) \<subseteq> funas_gterm ?s

goal (1 subgoal):
 1. t = gterm_to_None_Some (gsubt_at v (hole_pos C)) \<and> funas_gterm (gsubt_at v (hole_pos C)) \<subseteq> \<F>
[PROOF STEP]
by (auto simp: gp intro!: exI[of _ "gsubt_at v (hole_pos C)"])
       (metis ctxt ground_hole_pos_to_ghole gsubt_at_gctxt_apply_ghole)
[PROOF STATE]
proof (state)
this:
t = gterm_to_None_Some (gsubt_at v (hole_pos C)) \<and> funas_gterm (gsubt_at v (hole_pos C)) \<subseteq> \<F>

goal (1 subgoal):
 1. \<exists>u. t = gterm_to_None_Some u \<and> funas_gterm u \<subseteq> \<F>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
t = gterm_to_None_Some (gsubt_at v (hole_pos C)) \<and> funas_gterm (gsubt_at v (hole_pos C)) \<subseteq> \<F>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
t = gterm_to_None_Some (gsubt_at v (hole_pos C)) \<and> funas_gterm (gsubt_at v (hole_pos C)) \<subseteq> \<F>

goal (1 subgoal):
 1. \<exists>u. t = gterm_to_None_Some u \<and> funas_gterm u \<subseteq> \<F>
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>u. t = gterm_to_None_Some u \<and> funas_gterm u \<subseteq> \<F>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma infinite_set_dec_infinite:
  assumes "infinite S" and "\<And> s. s \<in> S \<Longrightarrow> \<exists> t. f t = s \<and> P t"
  shows "infinite {t | t s. s \<in> S \<and> f t = s \<and> P t}" (is "infinite ?T")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. infinite {uu_. \<exists>t s. uu_ = t \<and> s \<in> S \<and> f t = s \<and> P t}
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> infinite {uu_. \<exists>t s. uu_ = t \<and> s \<in> S \<and> f t = s \<and> P t} \<Longrightarrow> False
[PROOF STEP]
assume ass: "\<not> infinite ?T"
[PROOF STATE]
proof (state)
this:
\<not> infinite {uu_. \<exists>t s. uu_ = t \<and> s \<in> S \<and> f t = s \<and> P t}

goal (1 subgoal):
 1. \<not> infinite {uu_. \<exists>t s. uu_ = t \<and> s \<in> S \<and> f t = s \<and> P t} \<Longrightarrow> False
[PROOF STEP]
have "S \<subseteq> f ` {x . P x}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. S \<subseteq> f ` {x. P x}
[PROOF STEP]
using assms(2)
[PROOF STATE]
proof (prove)
using this:
?s \<in> S \<Longrightarrow> \<exists>t. f t = ?s \<and> P t

goal (1 subgoal):
 1. S \<subseteq> f ` {x. P x}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
S \<subseteq> f ` {x. P x}

goal (1 subgoal):
 1. \<not> infinite {uu_. \<exists>t s. uu_ = t \<and> s \<in> S \<and> f t = s \<and> P t} \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
S \<subseteq> f ` {x. P x}
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
S \<subseteq> f ` {x. P x}

goal (1 subgoal):
 1. False
[PROOF STEP]
using ass assms(1)
[PROOF STATE]
proof (prove)
using this:
S \<subseteq> f ` {x. P x}
\<not> infinite {uu_. \<exists>t s. uu_ = t \<and> s \<in> S \<and> f t = s \<and> P t}
infinite S

goal (1 subgoal):
 1. False
[PROOF STEP]
by (auto simp: subset_image_iff)
      (smt Ball_Collect finite_imageI image_subset_iff infinite_iff_countable_subset subset_eq)
[PROOF STATE]
proof (state)
this:
False

goal:
No subgoals!
[PROOF STEP]
qed