[STATEMENT]
lemma interp_rga_reorder:
  assumes "rga_ops (pre @ suf @ [(oid, ref)])"
    and "\<And>i r. (i, Some r) \<in> set suf \<Longrightarrow> r \<noteq> oid"
    and "\<And>r. ref = Some r \<Longrightarrow> r \<notin> fst ` set suf"
  shows "interp_rga (pre @ (oid, ref) # suf) = interp_rga (pre @ suf @ [(oid, ref)])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. interp_rga (pre @ (oid, ref) # suf) = interp_rga (pre @ suf @ [(oid, ref)])
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
rga_ops (pre @ suf @ [(oid, ref)])
(?i, Some ?r) \<in> set suf \<Longrightarrow> ?r \<noteq> oid
ref = Some ?r \<Longrightarrow> ?r \<notin> fst ` set suf

goal (1 subgoal):
 1. interp_rga (pre @ (oid, ref) # suf) = interp_rga (pre @ suf @ [(oid, ref)])
[PROOF STEP]
proof(induction suf rule: List.rev_induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>rga_ops (pre @ [] @ [(oid, ref)]); \<And>i r. (i, Some r) \<in> set [] \<Longrightarrow> r \<noteq> oid; \<And>r. ref = Some r \<Longrightarrow> r \<notin> fst ` set []\<rbrakk> \<Longrightarrow> interp_rga (pre @ [(oid, ref)]) = interp_rga (pre @ [] @ [(oid, ref)])
 2. \<And>x xs. \<lbrakk>\<lbrakk>rga_ops (pre @ xs @ [(oid, ref)]); \<And>i r. (i, Some r) \<in> set xs \<Longrightarrow> r \<noteq> oid; \<And>r. ref = Some r \<Longrightarrow> r \<notin> fst ` set xs\<rbrakk> \<Longrightarrow> interp_rga (pre @ (oid, ref) # xs) = interp_rga (pre @ xs @ [(oid, ref)]); rga_ops (pre @ (xs @ [x]) @ [(oid, ref)]); \<And>i r. (i, Some r) \<in> set (xs @ [x]) \<Longrightarrow> r \<noteq> oid; \<And>r. ref = Some r \<Longrightarrow> r \<notin> fst ` set (xs @ [x])\<rbrakk> \<Longrightarrow> interp_rga (pre @ (oid, ref) # xs @ [x]) = interp_rga (pre @ (xs @ [x]) @ [(oid, ref)])
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
rga_ops (pre @ [] @ [(oid, ref)])
(?i, Some ?r) \<in> set [] \<Longrightarrow> ?r \<noteq> oid
ref = Some ?r \<Longrightarrow> ?r \<notin> fst ` set []

goal (2 subgoals):
 1. \<lbrakk>rga_ops (pre @ [] @ [(oid, ref)]); \<And>i r. (i, Some r) \<in> set [] \<Longrightarrow> r \<noteq> oid; \<And>r. ref = Some r \<Longrightarrow> r \<notin> fst ` set []\<rbrakk> \<Longrightarrow> interp_rga (pre @ [(oid, ref)]) = interp_rga (pre @ [] @ [(oid, ref)])
 2. \<And>x xs. \<lbrakk>\<lbrakk>rga_ops (pre @ xs @ [(oid, ref)]); \<And>i r. (i, Some r) \<in> set xs \<Longrightarrow> r \<noteq> oid; \<And>r. ref = Some r \<Longrightarrow> r \<notin> fst ` set xs\<rbrakk> \<Longrightarrow> interp_rga (pre @ (oid, ref) # xs) = interp_rga (pre @ xs @ [(oid, ref)]); rga_ops (pre @ (xs @ [x]) @ [(oid, ref)]); \<And>i r. (i, Some r) \<in> set (xs @ [x]) \<Longrightarrow> r \<noteq> oid; \<And>r. ref = Some r \<Longrightarrow> r \<notin> fst ` set (xs @ [x])\<rbrakk> \<Longrightarrow> interp_rga (pre @ (oid, ref) # xs @ [x]) = interp_rga (pre @ (xs @ [x]) @ [(oid, ref)])
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
rga_ops (pre @ [] @ [(oid, ref)])
(?i, Some ?r) \<in> set [] \<Longrightarrow> ?r \<noteq> oid
ref = Some ?r \<Longrightarrow> ?r \<notin> fst ` set []
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
rga_ops (pre @ [] @ [(oid, ref)])
(?i, Some ?r) \<in> set [] \<Longrightarrow> ?r \<noteq> oid
ref = Some ?r \<Longrightarrow> ?r \<notin> fst ` set []

goal (1 subgoal):
 1. interp_rga (pre @ [(oid, ref)]) = interp_rga (pre @ [] @ [(oid, ref)])
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
interp_rga (pre @ [(oid, ref)]) = interp_rga (pre @ [] @ [(oid, ref)])

goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>\<lbrakk>rga_ops (pre @ xs @ [(oid, ref)]); \<And>i r. (i, Some r) \<in> set xs \<Longrightarrow> r \<noteq> oid; \<And>r. ref = Some r \<Longrightarrow> r \<notin> fst ` set xs\<rbrakk> \<Longrightarrow> interp_rga (pre @ (oid, ref) # xs) = interp_rga (pre @ xs @ [(oid, ref)]); rga_ops (pre @ (xs @ [x]) @ [(oid, ref)]); \<And>i r. (i, Some r) \<in> set (xs @ [x]) \<Longrightarrow> r \<noteq> oid; \<And>r. ref = Some r \<Longrightarrow> r \<notin> fst ` set (xs @ [x])\<rbrakk> \<Longrightarrow> interp_rga (pre @ (oid, ref) # xs @ [x]) = interp_rga (pre @ (xs @ [x]) @ [(oid, ref)])
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>\<lbrakk>rga_ops (pre @ xs @ [(oid, ref)]); \<And>i r. (i, Some r) \<in> set xs \<Longrightarrow> r \<noteq> oid; \<And>r. ref = Some r \<Longrightarrow> r \<notin> fst ` set xs\<rbrakk> \<Longrightarrow> interp_rga (pre @ (oid, ref) # xs) = interp_rga (pre @ xs @ [(oid, ref)]); rga_ops (pre @ (xs @ [x]) @ [(oid, ref)]); \<And>i r. (i, Some r) \<in> set (xs @ [x]) \<Longrightarrow> r \<noteq> oid; \<And>r. ref = Some r \<Longrightarrow> r \<notin> fst ` set (xs @ [x])\<rbrakk> \<Longrightarrow> interp_rga (pre @ (oid, ref) # xs @ [x]) = interp_rga (pre @ (xs @ [x]) @ [(oid, ref)])
[PROOF STEP]
case (snoc x xs)
[PROOF STATE]
proof (state)
this:
\<lbrakk>rga_ops (pre @ xs @ [(oid, ref)]); \<And>i r. (i, Some r) \<in> set xs \<Longrightarrow> r \<noteq> oid; \<And>r. ref = Some r \<Longrightarrow> r \<notin> fst ` set xs\<rbrakk> \<Longrightarrow> interp_rga (pre @ (oid, ref) # xs) = interp_rga (pre @ xs @ [(oid, ref)])
rga_ops (pre @ (xs @ [x]) @ [(oid, ref)])
(?i, Some ?r) \<in> set (xs @ [x]) \<Longrightarrow> ?r \<noteq> oid
ref = Some ?r \<Longrightarrow> ?r \<notin> fst ` set (xs @ [x])

goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>\<lbrakk>rga_ops (pre @ xs @ [(oid, ref)]); \<And>i r. (i, Some r) \<in> set xs \<Longrightarrow> r \<noteq> oid; \<And>r. ref = Some r \<Longrightarrow> r \<notin> fst ` set xs\<rbrakk> \<Longrightarrow> interp_rga (pre @ (oid, ref) # xs) = interp_rga (pre @ xs @ [(oid, ref)]); rga_ops (pre @ (xs @ [x]) @ [(oid, ref)]); \<And>i r. (i, Some r) \<in> set (xs @ [x]) \<Longrightarrow> r \<noteq> oid; \<And>r. ref = Some r \<Longrightarrow> r \<notin> fst ` set (xs @ [x])\<rbrakk> \<Longrightarrow> interp_rga (pre @ (oid, ref) # xs @ [x]) = interp_rga (pre @ (xs @ [x]) @ [(oid, ref)])
[PROOF STEP]
have ref_not_x: "\<And>r. ref = Some r \<Longrightarrow> r \<noteq> fst x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>r. ref = Some r \<Longrightarrow> r \<noteq> fst x
[PROOF STEP]
using snoc.prems(3)
[PROOF STATE]
proof (prove)
using this:
ref = Some ?r \<Longrightarrow> ?r \<notin> fst ` set (xs @ [x])

goal (1 subgoal):
 1. \<And>r. ref = Some r \<Longrightarrow> r \<noteq> fst x
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
ref = Some ?r \<Longrightarrow> ?r \<noteq> fst x

goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>\<lbrakk>rga_ops (pre @ xs @ [(oid, ref)]); \<And>i r. (i, Some r) \<in> set xs \<Longrightarrow> r \<noteq> oid; \<And>r. ref = Some r \<Longrightarrow> r \<notin> fst ` set xs\<rbrakk> \<Longrightarrow> interp_rga (pre @ (oid, ref) # xs) = interp_rga (pre @ xs @ [(oid, ref)]); rga_ops (pre @ (xs @ [x]) @ [(oid, ref)]); \<And>i r. (i, Some r) \<in> set (xs @ [x]) \<Longrightarrow> r \<noteq> oid; \<And>r. ref = Some r \<Longrightarrow> r \<notin> fst ` set (xs @ [x])\<rbrakk> \<Longrightarrow> interp_rga (pre @ (oid, ref) # xs @ [x]) = interp_rga (pre @ (xs @ [x]) @ [(oid, ref)])
[PROOF STEP]
have IH: "interp_rga (pre @ (oid, ref) # xs) = interp_rga (pre @ xs @ [(oid, ref)])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. interp_rga (pre @ (oid, ref) # xs) = interp_rga (pre @ xs @ [(oid, ref)])
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. interp_rga (pre @ (oid, ref) # xs) = interp_rga (pre @ xs @ [(oid, ref)])
[PROOF STEP]
have "rga_ops ((pre @ xs) @ [x] @ [(oid, ref)])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rga_ops ((pre @ xs) @ [x] @ [(oid, ref)])
[PROOF STEP]
using snoc.prems(1)
[PROOF STATE]
proof (prove)
using this:
rga_ops (pre @ (xs @ [x]) @ [(oid, ref)])

goal (1 subgoal):
 1. rga_ops ((pre @ xs) @ [x] @ [(oid, ref)])
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
rga_ops ((pre @ xs) @ [x] @ [(oid, ref)])

goal (1 subgoal):
 1. interp_rga (pre @ (oid, ref) # xs) = interp_rga (pre @ xs @ [(oid, ref)])
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
rga_ops ((pre @ xs) @ [x] @ [(oid, ref)])

goal (1 subgoal):
 1. interp_rga (pre @ (oid, ref) # xs) = interp_rga (pre @ xs @ [(oid, ref)])
[PROOF STEP]
have "\<And>r. ref = Some r \<Longrightarrow> r \<noteq> fst x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>r. ref = Some r \<Longrightarrow> r \<noteq> fst x
[PROOF STEP]
by (simp add: ref_not_x)
[PROOF STATE]
proof (state)
this:
ref = Some ?r \<Longrightarrow> ?r \<noteq> fst x

goal (1 subgoal):
 1. interp_rga (pre @ (oid, ref) # xs) = interp_rga (pre @ xs @ [(oid, ref)])
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
rga_ops ((pre @ xs) @ [x] @ [(oid, ref)])
ref = Some ?r \<Longrightarrow> ?r \<noteq> fst x
[PROOF STEP]
have "rga_ops ((pre @ xs) @ [(oid, ref)])"
[PROOF STATE]
proof (prove)
using this:
rga_ops ((pre @ xs) @ [x] @ [(oid, ref)])
ref = Some ?r \<Longrightarrow> ?r \<noteq> fst x

goal (1 subgoal):
 1. rga_ops ((pre @ xs) @ [(oid, ref)])
[PROOF STEP]
using rga_ops_rem_penultimate
[PROOF STATE]
proof (prove)
using this:
rga_ops ((pre @ xs) @ [x] @ [(oid, ref)])
ref = Some ?r \<Longrightarrow> ?r \<noteq> fst x
\<lbrakk>rga_ops (?xs @ [(?i1.0, ?r1.0), (?i2.0, ?r2.0)]); \<And>r. ?r2.0 = Some r \<Longrightarrow> r \<noteq> ?i1.0\<rbrakk> \<Longrightarrow> rga_ops (?xs @ [(?i2.0, ?r2.0)])

goal (1 subgoal):
 1. rga_ops ((pre @ xs) @ [(oid, ref)])
[PROOF STEP]
by (metis (no_types, lifting) Cons_eq_append_conv prod.collapse)
[PROOF STATE]
proof (state)
this:
rga_ops ((pre @ xs) @ [(oid, ref)])

goal (1 subgoal):
 1. interp_rga (pre @ (oid, ref) # xs) = interp_rga (pre @ xs @ [(oid, ref)])
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
rga_ops ((pre @ xs) @ [(oid, ref)])

goal (1 subgoal):
 1. interp_rga (pre @ (oid, ref) # xs) = interp_rga (pre @ xs @ [(oid, ref)])
[PROOF STEP]
using snoc
[PROOF STATE]
proof (prove)
using this:
rga_ops ((pre @ xs) @ [(oid, ref)])
\<lbrakk>rga_ops (pre @ xs @ [(oid, ref)]); \<And>i r. (i, Some r) \<in> set xs \<Longrightarrow> r \<noteq> oid; \<And>r. ref = Some r \<Longrightarrow> r \<notin> fst ` set xs\<rbrakk> \<Longrightarrow> interp_rga (pre @ (oid, ref) # xs) = interp_rga (pre @ xs @ [(oid, ref)])
rga_ops (pre @ (xs @ [x]) @ [(oid, ref)])
(?i, Some ?r) \<in> set (xs @ [x]) \<Longrightarrow> ?r \<noteq> oid
ref = Some ?r \<Longrightarrow> ?r \<notin> fst ` set (xs @ [x])

goal (1 subgoal):
 1. interp_rga (pre @ (oid, ref) # xs) = interp_rga (pre @ xs @ [(oid, ref)])
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
interp_rga (pre @ (oid, ref) # xs) = interp_rga (pre @ xs @ [(oid, ref)])

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
interp_rga (pre @ (oid, ref) # xs) = interp_rga (pre @ xs @ [(oid, ref)])

goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>\<lbrakk>rga_ops (pre @ xs @ [(oid, ref)]); \<And>i r. (i, Some r) \<in> set xs \<Longrightarrow> r \<noteq> oid; \<And>r. ref = Some r \<Longrightarrow> r \<notin> fst ` set xs\<rbrakk> \<Longrightarrow> interp_rga (pre @ (oid, ref) # xs) = interp_rga (pre @ xs @ [(oid, ref)]); rga_ops (pre @ (xs @ [x]) @ [(oid, ref)]); \<And>i r. (i, Some r) \<in> set (xs @ [x]) \<Longrightarrow> r \<noteq> oid; \<And>r. ref = Some r \<Longrightarrow> r \<notin> fst ` set (xs @ [x])\<rbrakk> \<Longrightarrow> interp_rga (pre @ (oid, ref) # xs @ [x]) = interp_rga (pre @ (xs @ [x]) @ [(oid, ref)])
[PROOF STEP]
obtain xi xr where x_pair: "x = (xi, xr)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>xi xr. x = (xi, xr) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
x = (xi, xr)

goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>\<lbrakk>rga_ops (pre @ xs @ [(oid, ref)]); \<And>i r. (i, Some r) \<in> set xs \<Longrightarrow> r \<noteq> oid; \<And>r. ref = Some r \<Longrightarrow> r \<notin> fst ` set xs\<rbrakk> \<Longrightarrow> interp_rga (pre @ (oid, ref) # xs) = interp_rga (pre @ xs @ [(oid, ref)]); rga_ops (pre @ (xs @ [x]) @ [(oid, ref)]); \<And>i r. (i, Some r) \<in> set (xs @ [x]) \<Longrightarrow> r \<noteq> oid; \<And>r. ref = Some r \<Longrightarrow> r \<notin> fst ` set (xs @ [x])\<rbrakk> \<Longrightarrow> interp_rga (pre @ (oid, ref) # xs @ [x]) = interp_rga (pre @ (xs @ [x]) @ [(oid, ref)])
[PROOF STEP]
have "interp_rga (pre @ (oid, ref) # xs @ [(xi, xr)]) =
        insert_rga (interp_rga (pre @ xs @ [(oid, ref)])) (xi, xr)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. interp_rga (pre @ (oid, ref) # xs @ [(xi, xr)]) = insert_rga (interp_rga (pre @ xs @ [(oid, ref)])) (xi, xr)
[PROOF STEP]
using IH interp_rga_tail_unfold
[PROOF STATE]
proof (prove)
using this:
interp_rga (pre @ (oid, ref) # xs) = interp_rga (pre @ xs @ [(oid, ref)])
interp_rga (?xs @ [?x]) = insert_rga (interp_rga ?xs) ?x

goal (1 subgoal):
 1. interp_rga (pre @ (oid, ref) # xs @ [(xi, xr)]) = insert_rga (interp_rga (pre @ xs @ [(oid, ref)])) (xi, xr)
[PROOF STEP]
by (metis append.assoc append_Cons)
[PROOF STATE]
proof (state)
this:
interp_rga (pre @ (oid, ref) # xs @ [(xi, xr)]) = insert_rga (interp_rga (pre @ xs @ [(oid, ref)])) (xi, xr)

goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>\<lbrakk>rga_ops (pre @ xs @ [(oid, ref)]); \<And>i r. (i, Some r) \<in> set xs \<Longrightarrow> r \<noteq> oid; \<And>r. ref = Some r \<Longrightarrow> r \<notin> fst ` set xs\<rbrakk> \<Longrightarrow> interp_rga (pre @ (oid, ref) # xs) = interp_rga (pre @ xs @ [(oid, ref)]); rga_ops (pre @ (xs @ [x]) @ [(oid, ref)]); \<And>i r. (i, Some r) \<in> set (xs @ [x]) \<Longrightarrow> r \<noteq> oid; \<And>r. ref = Some r \<Longrightarrow> r \<notin> fst ` set (xs @ [x])\<rbrakk> \<Longrightarrow> interp_rga (pre @ (oid, ref) # xs @ [x]) = interp_rga (pre @ (xs @ [x]) @ [(oid, ref)])
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
interp_rga (pre @ (oid, ref) # xs @ [(xi, xr)]) = insert_rga (interp_rga (pre @ xs @ [(oid, ref)])) (xi, xr)

goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>\<lbrakk>rga_ops (pre @ xs @ [(oid, ref)]); \<And>i r. (i, Some r) \<in> set xs \<Longrightarrow> r \<noteq> oid; \<And>r. ref = Some r \<Longrightarrow> r \<notin> fst ` set xs\<rbrakk> \<Longrightarrow> interp_rga (pre @ (oid, ref) # xs) = interp_rga (pre @ xs @ [(oid, ref)]); rga_ops (pre @ (xs @ [x]) @ [(oid, ref)]); \<And>i r. (i, Some r) \<in> set (xs @ [x]) \<Longrightarrow> r \<noteq> oid; \<And>r. ref = Some r \<Longrightarrow> r \<notin> fst ` set (xs @ [x])\<rbrakk> \<Longrightarrow> interp_rga (pre @ (oid, ref) # xs @ [x]) = interp_rga (pre @ (xs @ [x]) @ [(oid, ref)])
[PROOF STEP]
have "... = insert_rga (insert_rga (interp_rga (pre @ xs)) (oid, ref)) (xi, xr)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insert_rga (interp_rga (pre @ xs @ [(oid, ref)])) (xi, xr) = insert_rga (insert_rga (interp_rga (pre @ xs)) (oid, ref)) (xi, xr)
[PROOF STEP]
using interp_rga_tail_unfold
[PROOF STATE]
proof (prove)
using this:
interp_rga (?xs @ [?x]) = insert_rga (interp_rga ?xs) ?x

goal (1 subgoal):
 1. insert_rga (interp_rga (pre @ xs @ [(oid, ref)])) (xi, xr) = insert_rga (insert_rga (interp_rga (pre @ xs)) (oid, ref)) (xi, xr)
[PROOF STEP]
by (metis append_assoc)
[PROOF STATE]
proof (state)
this:
insert_rga (interp_rga (pre @ xs @ [(oid, ref)])) (xi, xr) = insert_rga (insert_rga (interp_rga (pre @ xs)) (oid, ref)) (xi, xr)

goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>\<lbrakk>rga_ops (pre @ xs @ [(oid, ref)]); \<And>i r. (i, Some r) \<in> set xs \<Longrightarrow> r \<noteq> oid; \<And>r. ref = Some r \<Longrightarrow> r \<notin> fst ` set xs\<rbrakk> \<Longrightarrow> interp_rga (pre @ (oid, ref) # xs) = interp_rga (pre @ xs @ [(oid, ref)]); rga_ops (pre @ (xs @ [x]) @ [(oid, ref)]); \<And>i r. (i, Some r) \<in> set (xs @ [x]) \<Longrightarrow> r \<noteq> oid; \<And>r. ref = Some r \<Longrightarrow> r \<notin> fst ` set (xs @ [x])\<rbrakk> \<Longrightarrow> interp_rga (pre @ (oid, ref) # xs @ [x]) = interp_rga (pre @ (xs @ [x]) @ [(oid, ref)])
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
insert_rga (interp_rga (pre @ xs @ [(oid, ref)])) (xi, xr) = insert_rga (insert_rga (interp_rga (pre @ xs)) (oid, ref)) (xi, xr)

goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>\<lbrakk>rga_ops (pre @ xs @ [(oid, ref)]); \<And>i r. (i, Some r) \<in> set xs \<Longrightarrow> r \<noteq> oid; \<And>r. ref = Some r \<Longrightarrow> r \<notin> fst ` set xs\<rbrakk> \<Longrightarrow> interp_rga (pre @ (oid, ref) # xs) = interp_rga (pre @ xs @ [(oid, ref)]); rga_ops (pre @ (xs @ [x]) @ [(oid, ref)]); \<And>i r. (i, Some r) \<in> set (xs @ [x]) \<Longrightarrow> r \<noteq> oid; \<And>r. ref = Some r \<Longrightarrow> r \<notin> fst ` set (xs @ [x])\<rbrakk> \<Longrightarrow> interp_rga (pre @ (oid, ref) # xs @ [x]) = interp_rga (pre @ (xs @ [x]) @ [(oid, ref)])
[PROOF STEP]
have "... = insert_rga (insert_rga (interp_rga (pre @ xs)) (xi, xr)) (oid, ref)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insert_rga (insert_rga (interp_rga (pre @ xs)) (oid, ref)) (xi, xr) = insert_rga (insert_rga (interp_rga (pre @ xs)) (xi, xr)) (oid, ref)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. insert_rga (insert_rga (interp_rga (pre @ xs)) (oid, ref)) (xi, xr) = insert_rga (insert_rga (interp_rga (pre @ xs)) (xi, xr)) (oid, ref)
[PROOF STEP]
have "\<And>xrr. xr = Some xrr \<Longrightarrow> xrr \<noteq> oid"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>xrr. xr = Some xrr \<Longrightarrow> xrr \<noteq> oid
[PROOF STEP]
using x_pair snoc.prems(2)
[PROOF STATE]
proof (prove)
using this:
x = (xi, xr)
(?i, Some ?r) \<in> set (xs @ [x]) \<Longrightarrow> ?r \<noteq> oid

goal (1 subgoal):
 1. \<And>xrr. xr = Some xrr \<Longrightarrow> xrr \<noteq> oid
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
xr = Some ?xrr \<Longrightarrow> ?xrr \<noteq> oid

goal (1 subgoal):
 1. insert_rga (insert_rga (interp_rga (pre @ xs)) (oid, ref)) (xi, xr) = insert_rga (insert_rga (interp_rga (pre @ xs)) (xi, xr)) (oid, ref)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
xr = Some ?xrr \<Longrightarrow> ?xrr \<noteq> oid

goal (1 subgoal):
 1. insert_rga (insert_rga (interp_rga (pre @ xs)) (oid, ref)) (xi, xr) = insert_rga (insert_rga (interp_rga (pre @ xs)) (xi, xr)) (oid, ref)
[PROOF STEP]
using insert_rga_commutes ref_not_x
[PROOF STATE]
proof (prove)
using this:
xr = Some ?xrr \<Longrightarrow> ?xrr \<noteq> oid
\<lbrakk>?i2.0 \<noteq> Some ?e1.0; ?i1.0 \<noteq> Some ?e2.0\<rbrakk> \<Longrightarrow> insert_rga (insert_rga ?xs (?e1.0, ?i1.0)) (?e2.0, ?i2.0) = insert_rga (insert_rga ?xs (?e2.0, ?i2.0)) (?e1.0, ?i1.0)
ref = Some ?r \<Longrightarrow> ?r \<noteq> fst x

goal (1 subgoal):
 1. insert_rga (insert_rga (interp_rga (pre @ xs)) (oid, ref)) (xi, xr) = insert_rga (insert_rga (interp_rga (pre @ xs)) (xi, xr)) (oid, ref)
[PROOF STEP]
by (metis fst_conv x_pair)
[PROOF STATE]
proof (state)
this:
insert_rga (insert_rga (interp_rga (pre @ xs)) (oid, ref)) (xi, xr) = insert_rga (insert_rga (interp_rga (pre @ xs)) (xi, xr)) (oid, ref)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
insert_rga (insert_rga (interp_rga (pre @ xs)) (oid, ref)) (xi, xr) = insert_rga (insert_rga (interp_rga (pre @ xs)) (xi, xr)) (oid, ref)

goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>\<lbrakk>rga_ops (pre @ xs @ [(oid, ref)]); \<And>i r. (i, Some r) \<in> set xs \<Longrightarrow> r \<noteq> oid; \<And>r. ref = Some r \<Longrightarrow> r \<notin> fst ` set xs\<rbrakk> \<Longrightarrow> interp_rga (pre @ (oid, ref) # xs) = interp_rga (pre @ xs @ [(oid, ref)]); rga_ops (pre @ (xs @ [x]) @ [(oid, ref)]); \<And>i r. (i, Some r) \<in> set (xs @ [x]) \<Longrightarrow> r \<noteq> oid; \<And>r. ref = Some r \<Longrightarrow> r \<notin> fst ` set (xs @ [x])\<rbrakk> \<Longrightarrow> interp_rga (pre @ (oid, ref) # xs @ [x]) = interp_rga (pre @ (xs @ [x]) @ [(oid, ref)])
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
insert_rga (insert_rga (interp_rga (pre @ xs)) (oid, ref)) (xi, xr) = insert_rga (insert_rga (interp_rga (pre @ xs)) (xi, xr)) (oid, ref)

goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>\<lbrakk>rga_ops (pre @ xs @ [(oid, ref)]); \<And>i r. (i, Some r) \<in> set xs \<Longrightarrow> r \<noteq> oid; \<And>r. ref = Some r \<Longrightarrow> r \<notin> fst ` set xs\<rbrakk> \<Longrightarrow> interp_rga (pre @ (oid, ref) # xs) = interp_rga (pre @ xs @ [(oid, ref)]); rga_ops (pre @ (xs @ [x]) @ [(oid, ref)]); \<And>i r. (i, Some r) \<in> set (xs @ [x]) \<Longrightarrow> r \<noteq> oid; \<And>r. ref = Some r \<Longrightarrow> r \<notin> fst ` set (xs @ [x])\<rbrakk> \<Longrightarrow> interp_rga (pre @ (oid, ref) # xs @ [x]) = interp_rga (pre @ (xs @ [x]) @ [(oid, ref)])
[PROOF STEP]
have "... = interp_rga (pre @ xs @ [x] @ [(oid, ref)])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insert_rga (insert_rga (interp_rga (pre @ xs)) (xi, xr)) (oid, ref) = interp_rga (pre @ xs @ [x] @ [(oid, ref)])
[PROOF STEP]
by (metis append_assoc interp_rga_tail_unfold x_pair)
[PROOF STATE]
proof (state)
this:
insert_rga (insert_rga (interp_rga (pre @ xs)) (xi, xr)) (oid, ref) = interp_rga (pre @ xs @ [x] @ [(oid, ref)])

goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>\<lbrakk>rga_ops (pre @ xs @ [(oid, ref)]); \<And>i r. (i, Some r) \<in> set xs \<Longrightarrow> r \<noteq> oid; \<And>r. ref = Some r \<Longrightarrow> r \<notin> fst ` set xs\<rbrakk> \<Longrightarrow> interp_rga (pre @ (oid, ref) # xs) = interp_rga (pre @ xs @ [(oid, ref)]); rga_ops (pre @ (xs @ [x]) @ [(oid, ref)]); \<And>i r. (i, Some r) \<in> set (xs @ [x]) \<Longrightarrow> r \<noteq> oid; \<And>r. ref = Some r \<Longrightarrow> r \<notin> fst ` set (xs @ [x])\<rbrakk> \<Longrightarrow> interp_rga (pre @ (oid, ref) # xs @ [x]) = interp_rga (pre @ (xs @ [x]) @ [(oid, ref)])
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
interp_rga (pre @ (oid, ref) # xs @ [(xi, xr)]) = insert_rga (interp_rga (pre @ xs @ [(oid, ref)])) (xi, xr)
insert_rga (interp_rga (pre @ xs @ [(oid, ref)])) (xi, xr) = insert_rga (insert_rga (interp_rga (pre @ xs)) (oid, ref)) (xi, xr)
insert_rga (insert_rga (interp_rga (pre @ xs)) (oid, ref)) (xi, xr) = insert_rga (insert_rga (interp_rga (pre @ xs)) (xi, xr)) (oid, ref)
insert_rga (insert_rga (interp_rga (pre @ xs)) (xi, xr)) (oid, ref) = interp_rga (pre @ xs @ [x] @ [(oid, ref)])
[PROOF STEP]
show "interp_rga (pre @ (oid, ref) # xs @ [x]) =
                   interp_rga (pre @ (xs @ [x]) @ [(oid, ref)])"
[PROOF STATE]
proof (prove)
using this:
interp_rga (pre @ (oid, ref) # xs @ [(xi, xr)]) = insert_rga (interp_rga (pre @ xs @ [(oid, ref)])) (xi, xr)
insert_rga (interp_rga (pre @ xs @ [(oid, ref)])) (xi, xr) = insert_rga (insert_rga (interp_rga (pre @ xs)) (oid, ref)) (xi, xr)
insert_rga (insert_rga (interp_rga (pre @ xs)) (oid, ref)) (xi, xr) = insert_rga (insert_rga (interp_rga (pre @ xs)) (xi, xr)) (oid, ref)
insert_rga (insert_rga (interp_rga (pre @ xs)) (xi, xr)) (oid, ref) = interp_rga (pre @ xs @ [x] @ [(oid, ref)])

goal (1 subgoal):
 1. interp_rga (pre @ (oid, ref) # xs @ [x]) = interp_rga (pre @ (xs @ [x]) @ [(oid, ref)])
[PROOF STEP]
by (simp add: x_pair)
[PROOF STATE]
proof (state)
this:
interp_rga (pre @ (oid, ref) # xs @ [x]) = interp_rga (pre @ (xs @ [x]) @ [(oid, ref)])

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ss423conv:
  assumes "bijective x"
    shows "x ; y \<le> z \<longleftrightarrow> y \<le> x\<^sup>T ; z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x ; y \<le> z) = (y \<le> x\<^sup>T ; z)
[PROOF STEP]
by (metis assms conv_contrav conv_iso inj_p_fun is_map_def ss423 sur_total)


[STATEMENT]
lemma plus_top:
  "x\<^sup>+;1 = x;1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x\<^sup>+ ; 1 = x ; 1
[PROOF STEP]
by (metis comp_assoc conway.dagger_unfoldr_distr sup_top_left)


[STATEMENT]
lemma effect_ref[effect_elims]:
  assumes "effect (ref (x::('a::heap))) h h' r"
  obtains "r = fst (Ref.alloc x h)" and "h' = snd (Ref.alloc x h)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lbrakk>r = fst (Ref.alloc x h); h' = snd (Ref.alloc x h)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<lbrakk>r = fst (Ref.alloc x h); h' = snd (Ref.alloc x h)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
effect (ref x) h h' r
[PROOF STEP]
have "execute (ref x) h = Some (r, h')"
[PROOF STATE]
proof (prove)
using this:
effect (ref x) h h' r

goal (1 subgoal):
 1. execute (ref x) h = Some (r, h')
[PROOF STEP]
by (unfold effect_def)
[PROOF STATE]
proof (state)
this:
execute (ref x) h = Some (r, h')

goal (1 subgoal):
 1. (\<lbrakk>r = fst (Ref.alloc x h); h' = snd (Ref.alloc x h)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
execute (ref x) h = Some (r, h')
[PROOF STEP]
have "r = fst (Ref.alloc x h)" "h' = snd (Ref.alloc x h)"
[PROOF STATE]
proof (prove)
using this:
execute (ref x) h = Some (r, h')

goal (1 subgoal):
 1. r = fst (Ref.alloc x h) &&& h' = snd (Ref.alloc x h)
[PROOF STEP]
by (auto simp add: execute_simps)
[PROOF STATE]
proof (state)
this:
r = fst (Ref.alloc x h)
h' = snd (Ref.alloc x h)

goal (1 subgoal):
 1. (\<lbrakk>r = fst (Ref.alloc x h); h' = snd (Ref.alloc x h)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
r = fst (Ref.alloc x h)
h' = snd (Ref.alloc x h)
[PROOF STEP]
show thesis
[PROOF STATE]
proof (prove)
using this:
r = fst (Ref.alloc x h)
h' = snd (Ref.alloc x h)

goal (1 subgoal):
 1. thesis
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
thesis

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma prod_induct_gen:
  assumes "\<And> a r. f (h a * r :: 'a :: {comm_monoid_mult}) = f (g a * r)"
  shows "f (\<Prod>v\<leftarrow>lst. h v) = f (\<Prod>v\<leftarrow>lst. g v)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f (prod_list (map h lst)) = f (prod_list (map g lst))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. f (prod_list (map h lst)) = f (prod_list (map g lst))
[PROOF STEP]
let "?P x y" = "f x = f y"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. f (prod_list (map h lst)) = f (prod_list (map g lst))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f (prod_list (map h lst)) = f (prod_list (map g lst))
[PROOF STEP]
using comm_monoid_mult_class.prod_list.induct_gen_abs[of _ ?P,OF assms]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<And>x y z. \<lbrakk>f x = f y; f y = f z\<rbrakk> \<Longrightarrow> f x = f z; f (\<Prod>a\<leftarrow>?lst. g (?a3 a)) = f (\<Prod>a\<leftarrow>?lst. g (?a3 a))\<rbrakk> \<Longrightarrow> f (\<Prod>a\<leftarrow>?lst. h (?a3 a)) = f (\<Prod>a\<leftarrow>?lst. g (?a3 a))

goal (1 subgoal):
 1. f (prod_list (map h lst)) = f (prod_list (map g lst))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
f (prod_list (map h lst)) = f (prod_list (map g lst))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma mult_vm_vm [simp]:
  shows "(v *\<^sub>v\<^sub>m A) *\<^sub>v\<^sub>m B = v *\<^sub>v\<^sub>m (A *\<^sub>m\<^sub>m B)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. v *\<^sub>v\<^sub>m A *\<^sub>v\<^sub>m B = v *\<^sub>v\<^sub>m (A *\<^sub>m\<^sub>m B)
[PROOF STEP]
by (cases v, cases A, cases B) (auto simp add: field_simps)


[STATEMENT]
lemma height_gt_0_in_alphabet_imp_sibling_left[simp]:
"\<lbrakk>height t\<^sub>1 > 0; a \<in> alphabet t\<^sub>1\<rbrakk> \<Longrightarrow>
 sibling (Node w t\<^sub>1 t\<^sub>2) a = sibling t\<^sub>1 a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < height t\<^sub>1; a \<in> alphabet t\<^sub>1\<rbrakk> \<Longrightarrow> sibling (Node w t\<^sub>1 t\<^sub>2) a = sibling t\<^sub>1 a
[PROOF STEP]
by (case_tac t\<^sub>1) simp+


[STATEMENT]
lemma clock_simVal_def2[iff]: "clock_simVal (clock_sim t) = envVal (tLast t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. clock_simVal (clock_sim t) = envVal (tLast t)
[PROOF STEP]
unfolding clock_sim_def clock_simVal_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (envVal \<circ> snd) (clock_commonAbs t, tLast t) = envVal (tLast t)
[PROOF STEP]
by simp


[STATEMENT]
lemma hensel_hypothesis_weakened:
"val_Zp (f\<bullet>a) > val_Zp (f'\<bullet>a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. val_Zp (f' \<bullet> a) < val_Zp (f \<bullet> a)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. val_Zp (f' \<bullet> a) < val_Zp (f \<bullet> a)
[PROOF STEP]
have 0: "0 \<le> val_Zp (f'\<bullet>a) \<and> val_Zp (f'\<bullet>a) \<noteq> \<infinity>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> val_Zp (f' \<bullet> a) \<and> val_Zp (f' \<bullet> a) \<noteq> \<infinity>
[PROOF STEP]
using f'a_closed val_ord_Zp val_pos
[PROOF STATE]
proof (prove)
using this:
f' \<bullet> a \<in> carrier Zp
?a \<noteq> \<zero> \<Longrightarrow> val_Zp ?a = eint (ord_Zp ?a)
?x \<in> carrier Zp \<Longrightarrow> 0 \<le> val_Zp ?x

goal (1 subgoal):
 1. 0 \<le> val_Zp (f' \<bullet> a) \<and> val_Zp (f' \<bullet> a) \<noteq> \<infinity>
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
0 \<le> val_Zp (f' \<bullet> a) \<and> val_Zp (f' \<bullet> a) \<noteq> \<infinity>

goal (1 subgoal):
 1. val_Zp (f' \<bullet> a) < val_Zp (f \<bullet> a)
[PROOF STEP]
have 1: "1 < eint 2 "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 < eint 2
[PROOF STEP]
by (simp add: one_eint_def)
[PROOF STATE]
proof (state)
this:
1 < eint 2

goal (1 subgoal):
 1. val_Zp (f' \<bullet> a) < val_Zp (f \<bullet> a)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
1 < eint 2

goal (1 subgoal):
 1. val_Zp (f' \<bullet> a) < val_Zp (f \<bullet> a)
[PROOF STEP]
using 0 eint_mult_mono'[of "val_Zp (f'\<bullet>a)" 1 2] hensel_hypothesis
[PROOF STATE]
proof (prove)
using this:
1 < eint 2
0 \<le> val_Zp (f' \<bullet> a) \<and> val_Zp (f' \<bullet> a) \<noteq> \<infinity>
\<lbrakk>0 \<le> val_Zp (f' \<bullet> a) \<and> val_Zp (f' \<bullet> a) \<noteq> \<infinity>; 1 < eint 2\<rbrakk> \<Longrightarrow> 1 * val_Zp (f' \<bullet> a) \<le> eint 2 * val_Zp (f' \<bullet> a)
eint 2 * val_Zp (f' \<bullet> a) < val_Zp (f \<bullet> a)

goal (1 subgoal):
 1. val_Zp (f' \<bullet> a) < val_Zp (f \<bullet> a)
[PROOF STEP]
by (metis linorder_not_less mult_one_left order_trans)
[PROOF STATE]
proof (state)
this:
val_Zp (f' \<bullet> a) < val_Zp (f \<bullet> a)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma integrable_\<T>_bounded[intro]:
  fixes f :: "('s \<times> 'a) stream \<Rightarrow> 'd :: {second_countable_topology,banach}"
  assumes f[measurable]: "f \<in> borel_measurable S"
  assumes b: "bounded (range f)"
  shows "integrable (\<T> p s) f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. integrable (\<T> p s) f
[PROOF STEP]
using b
[PROOF STATE]
proof (prove)
using this:
bounded (range f)

goal (1 subgoal):
 1. integrable (\<T> p s) f
[PROOF STEP]
by (auto simp: prob_space.finite_measure \<T>_prob_space bounded_iff
      intro!: finite_measure.integrable_const_bound)


[STATEMENT]
lemma icard_not_empty_iff: "(0 < icard A) = (A \<noteq> {})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (0 < icard A) = (A \<noteq> {})
[PROOF STEP]
by (simp add: icard_empty_iff[symmetric])


[STATEMENT]
lemma wfp_on_ord_term_strict:
  assumes "dickson_grading d"
  shows "wfp_on (\<prec>\<^sub>t) (pp_of_term -` dgrad_set d m)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wfp_on (\<prec>\<^sub>t) (pp_of_term -` dgrad_set d m)
[PROOF STEP]
proof (rule wfp_onI_min)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x Q. \<lbrakk>x \<in> Q; Q \<subseteq> pp_of_term -` dgrad_set d m\<rbrakk> \<Longrightarrow> \<exists>z\<in>Q. \<forall>y\<in>pp_of_term -` dgrad_set d m. y \<prec>\<^sub>t z \<longrightarrow> y \<notin> Q
[PROOF STEP]
fix x Q
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x Q. \<lbrakk>x \<in> Q; Q \<subseteq> pp_of_term -` dgrad_set d m\<rbrakk> \<Longrightarrow> \<exists>z\<in>Q. \<forall>y\<in>pp_of_term -` dgrad_set d m. y \<prec>\<^sub>t z \<longrightarrow> y \<notin> Q
[PROOF STEP]
assume "x \<in> Q" and "Q \<subseteq> pp_of_term -` dgrad_set d m"
[PROOF STATE]
proof (state)
this:
x \<in> Q
Q \<subseteq> pp_of_term -` dgrad_set d m

goal (1 subgoal):
 1. \<And>x Q. \<lbrakk>x \<in> Q; Q \<subseteq> pp_of_term -` dgrad_set d m\<rbrakk> \<Longrightarrow> \<exists>z\<in>Q. \<forall>y\<in>pp_of_term -` dgrad_set d m. y \<prec>\<^sub>t z \<longrightarrow> y \<notin> Q
[PROOF STEP]
from wf_dickson_less_v[OF assms, of m] \<open>x \<in> Q\<close>
[PROOF STATE]
proof (chain)
picking this:
wfP (dickson_less_v d m)
x \<in> Q
[PROOF STEP]
obtain z
    where "z \<in> Q" and *: "\<And>y. dickson_less_v d m y z \<Longrightarrow> y \<notin> Q"
[PROOF STATE]
proof (prove)
using this:
wfP (dickson_less_v d m)
x \<in> Q

goal (1 subgoal):
 1. (\<And>z. \<lbrakk>z \<in> Q; \<And>y. dickson_less_v d m y z \<Longrightarrow> y \<notin> Q\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (rule wfE_min[to_pred], blast)
[PROOF STATE]
proof (state)
this:
z \<in> Q
dickson_less_v d m ?y94 z \<Longrightarrow> ?y94 \<notin> Q

goal (1 subgoal):
 1. \<And>x Q. \<lbrakk>x \<in> Q; Q \<subseteq> pp_of_term -` dgrad_set d m\<rbrakk> \<Longrightarrow> \<exists>z\<in>Q. \<forall>y\<in>pp_of_term -` dgrad_set d m. y \<prec>\<^sub>t z \<longrightarrow> y \<notin> Q
[PROOF STEP]
from this(1) \<open>Q \<subseteq> pp_of_term -` dgrad_set d m\<close>
[PROOF STATE]
proof (chain)
picking this:
z \<in> Q
Q \<subseteq> pp_of_term -` dgrad_set d m
[PROOF STEP]
have "z \<in> pp_of_term -` dgrad_set d m"
[PROOF STATE]
proof (prove)
using this:
z \<in> Q
Q \<subseteq> pp_of_term -` dgrad_set d m

goal (1 subgoal):
 1. z \<in> pp_of_term -` dgrad_set d m
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
z \<in> pp_of_term -` dgrad_set d m

goal (1 subgoal):
 1. \<And>x Q. \<lbrakk>x \<in> Q; Q \<subseteq> pp_of_term -` dgrad_set d m\<rbrakk> \<Longrightarrow> \<exists>z\<in>Q. \<forall>y\<in>pp_of_term -` dgrad_set d m. y \<prec>\<^sub>t z \<longrightarrow> y \<notin> Q
[PROOF STEP]
show "\<exists>z\<in>Q. \<forall>y \<in> pp_of_term -` dgrad_set d m. y \<prec>\<^sub>t z \<longrightarrow> y \<notin> Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>z\<in>Q. \<forall>y\<in>pp_of_term -` dgrad_set d m. y \<prec>\<^sub>t z \<longrightarrow> y \<notin> Q
[PROOF STEP]
proof (intro bexI ballI impI, rule *)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>y. \<lbrakk>y \<in> pp_of_term -` dgrad_set d m; y \<prec>\<^sub>t ?z\<rbrakk> \<Longrightarrow> dickson_less_v d m y z
 2. ?z \<in> Q
[PROOF STEP]
fix y
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>y. \<lbrakk>y \<in> pp_of_term -` dgrad_set d m; y \<prec>\<^sub>t ?z\<rbrakk> \<Longrightarrow> dickson_less_v d m y z
 2. ?z \<in> Q
[PROOF STEP]
assume "y \<in> pp_of_term -` dgrad_set d m" and "y \<prec>\<^sub>t z"
[PROOF STATE]
proof (state)
this:
y \<in> pp_of_term -` dgrad_set d m
y \<prec>\<^sub>t z

goal (2 subgoals):
 1. \<And>y. \<lbrakk>y \<in> pp_of_term -` dgrad_set d m; y \<prec>\<^sub>t ?z\<rbrakk> \<Longrightarrow> dickson_less_v d m y z
 2. ?z \<in> Q
[PROOF STEP]
from this(1) \<open>z \<in> pp_of_term -` dgrad_set d m\<close>
[PROOF STATE]
proof (chain)
picking this:
y \<in> pp_of_term -` dgrad_set d m
z \<in> pp_of_term -` dgrad_set d m
[PROOF STEP]
have "d (pp_of_term y) \<le> m" and "d (pp_of_term z) \<le> m"
[PROOF STATE]
proof (prove)
using this:
y \<in> pp_of_term -` dgrad_set d m
z \<in> pp_of_term -` dgrad_set d m

goal (1 subgoal):
 1. d (pp_of_term y) \<le> m &&& d (pp_of_term z) \<le> m
[PROOF STEP]
by (simp_all add: dgrad_set_def)
[PROOF STATE]
proof (state)
this:
d (pp_of_term y) \<le> m
d (pp_of_term z) \<le> m

goal (2 subgoals):
 1. \<And>y. \<lbrakk>y \<in> pp_of_term -` dgrad_set d m; y \<prec>\<^sub>t ?z\<rbrakk> \<Longrightarrow> dickson_less_v d m y z
 2. ?z \<in> Q
[PROOF STEP]
thus "dickson_less_v d m y z"
[PROOF STATE]
proof (prove)
using this:
d (pp_of_term y) \<le> m
d (pp_of_term z) \<le> m

goal (1 subgoal):
 1. dickson_less_v d m y z
[PROOF STEP]
using \<open>y \<prec>\<^sub>t z\<close>
[PROOF STATE]
proof (prove)
using this:
d (pp_of_term y) \<le> m
d (pp_of_term z) \<le> m
y \<prec>\<^sub>t z

goal (1 subgoal):
 1. dickson_less_v d m y z
[PROOF STEP]
by (rule dickson_less_vI)
[PROOF STATE]
proof (state)
this:
dickson_less_v d m y z

goal (1 subgoal):
 1. z \<in> Q
[PROOF STEP]
qed fact
[PROOF STATE]
proof (state)
this:
\<exists>z\<in>Q. \<forall>y\<in>pp_of_term -` dgrad_set d m. y \<prec>\<^sub>t z \<longrightarrow> y \<notin> Q

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma coeff_int_pCons_0[simp]: "coeff_int (pCons 0 b) i = coeff_int b (i - 1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. coeff_int (pCons (0::'a) b) i = coeff_int b (i - 1)
[PROOF STEP]
by (auto simp: Nitpick.case_nat_unfold coeff_int_def coeff_pCons nat_diff_distrib')


[STATEMENT]
lemma PO_m3_DY_fake_refines_m2_fake:
  "{R23 \<inter> UNIV \<times> (m3_inv1_lkeysec)}
     m2_fake, m3_DY_fake
   {> R23}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {R23 \<inter> UNIV \<times> m3_inv1_lkeysec} m2_fake, m3_DY_fake {> R23}
[PROOF STEP]
apply (auto simp add: PO_rhoare_defs R23_def m3_defs intro!: R23_intros
            del: abs_msg.cases)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>a y x. \<lbrakk>(a, y) \<in> R23_msgs; (a, y) \<in> R23_keys; (a, y) \<in> R23_pres; y \<in> m3_inv1_lkeysec; x \<in> abs_msg (parts (IK y))\<rbrakk> \<Longrightarrow> x \<in> fake ik0 (dom (runs a)) (chan a)
 2. \<And>a y x. \<lbrakk>(a, y) \<in> R23_msgs; (a, y) \<in> R23_keys; (a, y) \<in> R23_pres; y \<in> m3_inv1_lkeysec; x \<in> abs_msg (synth (analz (IK y)))\<rbrakk> \<Longrightarrow> x \<in> fake ik0 (dom (runs a)) (chan a)
 3. \<And>a y KK K. \<lbrakk>(a, y) \<in> R23_msgs; (a, y) \<in> R23_keys; (a, y) \<in> R23_pres; y \<in> m3_inv1_lkeysec; KK \<subseteq> range sesK; Key K \<in> analz (Key ` KK \<union> IK y)\<rbrakk> \<Longrightarrow> aKey K \<in> extr (aKey ` KK \<union> ik0) (chan a)
 4. \<And>a y KK K. \<lbrakk>(a, y) \<in> R23_msgs; (a, y) \<in> R23_keys; (a, y) \<in> R23_pres; y \<in> m3_inv1_lkeysec; KK \<subseteq> range sesK; Key K \<in> analz (IK y)\<rbrakk> \<Longrightarrow> aKey K \<in> extr (aKey ` KK \<union> ik0) (chan a)
[PROOF STEP]
apply (auto intro: abs_msg_DY_subset_fakeable [THEN subsetD]
            del: abs_msg.cases)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a y KK K. \<lbrakk>(a, y) \<in> R23_msgs; (a, y) \<in> R23_keys; (a, y) \<in> R23_pres; y \<in> m3_inv1_lkeysec; KK \<subseteq> range sesK; Key K \<in> analz (IK y)\<rbrakk> \<Longrightarrow> aKey K \<in> extr (aKey ` KK \<union> ik0) (chan a)
[PROOF STEP]
apply (auto simp add: R23_keys_simps)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma hypext_uminus:
  "(*h* uminus) x = - x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (*h* uminus) x = - x
[PROOF STEP]
using hypext_scaleH[of "-1" x]
[PROOF STATE]
proof (prove)
using this:
(*h* (*) (- (1::'a))) x = - (1::'a) *\<^sub>H x

goal (1 subgoal):
 1. (*h* uminus) x = - x
[PROOF STEP]
by simp


[STATEMENT]
lemma (in is_iso_dghm) iso_dghm_Obj_HomDom_if_Obj_HomCod[elim]:
  assumes "b \<in>\<^sub>\<circ> \<BB>\<lparr>Obj\<rparr>"
  obtains a where "a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>" and "b = \<FF>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>a. \<lbrakk>a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>; b = \<FF>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms ObjMap.vrange_atD iso_dghm_ObjMap_vrange
[PROOF STATE]
proof (prove)
using this:
b \<in>\<^sub>\<circ> \<BB>\<lparr>Obj\<rparr>
?b \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> (\<FF>\<lparr>ObjMap\<rparr>) \<Longrightarrow> \<exists>a\<in>elts (\<AA>\<lparr>Obj\<rparr>). \<FF>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr> = ?b
\<R>\<^sub>\<circ> (\<FF>\<lparr>ObjMap\<rparr>) = \<BB>\<lparr>Obj\<rparr>

goal (1 subgoal):
 1. (\<And>a. \<lbrakk>a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>; b = \<FF>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast


[STATEMENT]
lemma type_wf_put_ptr_in_heap_E:
  assumes "type_wf (put\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t ptr obj h)"
  assumes "ptr |\<in>| object_ptr_kinds h"
  assumes "ObjectClass.type_wf h"
  assumes "is_node_ptr_kind ptr \<Longrightarrow> is_node_kind (the (get ptr h))"
  shows "type_wf h"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. NodeClass.type_wf h
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
NodeClass.type_wf (put ptr obj h)
ptr |\<in>| object_ptr_kinds h
ObjectClass.type_wf h
is_node_ptr_kind ptr \<Longrightarrow> is_node_kind (the (get ptr h))

goal (1 subgoal):
 1. NodeClass.type_wf h
[PROOF STEP]
apply(auto simp add: type_wf_defs split: option.splits if_splits)[1]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>y node_ptr. \<lbrakk>ptr |\<in>| object_ptr_kinds h; ObjectClass.type_wf h; is_node_kind (the (get ptr h)); is_node_ptr_kind ptr; ObjectClass.type_wf (put ptr (cast y) h); \<forall>node_ptr\<in>fset (node_ptr_kinds h). ptr = cast node_ptr \<or> (\<exists>y. get node_ptr h = Some y); obj = cast y; node_ptr |\<in>| node_ptr_kinds h\<rbrakk> \<Longrightarrow> \<exists>y. get node_ptr h = Some y
[PROOF STEP]
by (metis ObjectClass.get\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t_type_wf bind.bind_lunit finite_set_in get\<^sub>N\<^sub>o\<^sub>d\<^sub>e_def is_node_kind_def option.exhaust_sel)


[STATEMENT]
lemma node_ptr_kinds_preserved:
  assumes "writes SW setter h h'"
  assumes "h \<turnstile> setter \<rightarrow>\<^sub>h h'"
  assumes "\<And>h h'. \<forall>w \<in> SW. h \<turnstile> w \<rightarrow>\<^sub>h h'
            \<longrightarrow> (\<forall>object_ptr. preserved (get_M\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t object_ptr RObject.nothing) h h')"
  shows "node_ptr_kinds h = node_ptr_kinds h'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. node_ptr_kinds h = node_ptr_kinds h'
[PROOF STEP]
using writes_small_big[OF assms]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>reflp (\<lambda>h h'. \<forall>w\<in>SW. ?h4 h h' \<turnstile> w \<rightarrow>\<^sub>h ?h'5 h h' \<longrightarrow> (\<forall>object_ptr. preserved (get_M object_ptr RObject.nothing) (?h4 h h') (?h'5 h h'))); transp (\<lambda>h h'. \<forall>w\<in>SW. ?h4 h h' \<turnstile> w \<rightarrow>\<^sub>h ?h'5 h h' \<longrightarrow> (\<forall>object_ptr. preserved (get_M object_ptr RObject.nothing) (?h4 h h') (?h'5 h h')))\<rbrakk> \<Longrightarrow> \<forall>w\<in>SW. ?h4 h h' \<turnstile> w \<rightarrow>\<^sub>h ?h'5 h h' \<longrightarrow> (\<forall>object_ptr. preserved (get_M object_ptr RObject.nothing) (?h4 h h') (?h'5 h h'))

goal (1 subgoal):
 1. node_ptr_kinds h = node_ptr_kinds h'
[PROOF STEP]
apply(simp add: reflp_def transp_def preserved_def node_ptr_kinds_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>ha h'a. \<lbrakk>\<forall>x. (\<exists>w\<in>SW. ha x x \<turnstile> w \<rightarrow>\<^sub>h h'a x x) \<longrightarrow> (\<forall>object_ptr. ha x x \<turnstile> get_M object_ptr RObject.nothing \<rightarrow>\<^sub>r () = h'a x x \<turnstile> get_M object_ptr RObject.nothing \<rightarrow>\<^sub>r ()); \<forall>x y. ((\<exists>w\<in>SW. ha x y \<turnstile> w \<rightarrow>\<^sub>h h'a x y) \<longrightarrow> (\<forall>object_ptr. ha x y \<turnstile> get_M object_ptr RObject.nothing \<rightarrow>\<^sub>r () = h'a x y \<turnstile> get_M object_ptr RObject.nothing \<rightarrow>\<^sub>r ())) \<longrightarrow> (\<forall>z. ((\<exists>w\<in>SW. ha y z \<turnstile> w \<rightarrow>\<^sub>h h'a y z) \<longrightarrow> (\<forall>object_ptr. ha y z \<turnstile> get_M object_ptr RObject.nothing \<rightarrow>\<^sub>r () = h'a y z \<turnstile> get_M object_ptr RObject.nothing \<rightarrow>\<^sub>r ())) \<longrightarrow> (\<exists>w\<in>SW. ha x z \<turnstile> w \<rightarrow>\<^sub>h h'a x z) \<longrightarrow> (\<forall>object_ptr. ha x z \<turnstile> get_M object_ptr RObject.nothing \<rightarrow>\<^sub>r () = h'a x z \<turnstile> get_M object_ptr RObject.nothing \<rightarrow>\<^sub>r ()))\<rbrakk> \<Longrightarrow> (\<exists>w\<in>SW. ha h h' \<turnstile> w \<rightarrow>\<^sub>h h'a h h') \<longrightarrow> (\<forall>object_ptr. ha h h' \<turnstile> get_M object_ptr RObject.nothing \<rightarrow>\<^sub>r () = h'a h h' \<turnstile> get_M object_ptr RObject.nothing \<rightarrow>\<^sub>r ())) \<Longrightarrow> (the \<circ> cast) |`| ffilter is_node_ptr_kind (object_ptr_kinds h) = (the \<circ> cast) |`| ffilter is_node_ptr_kind (object_ptr_kinds h')
[PROOF STEP]
by (metis assms object_ptr_kinds_preserved)


[STATEMENT]
lemma comp_cond_left_distr:
  "((P \<triangleleft> b \<triangleright>\<^sub>r Q) ;; R) = ((P ;; R) \<triangleleft> b \<triangleright>\<^sub>r (Q ;; R))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (P \<triangleleft> b \<triangleright>\<^sub>r Q) ;; R = P ;; R \<triangleleft> b \<triangleright>\<^sub>r Q ;; R
[PROOF STEP]
by (rel_auto)


[STATEMENT]
theorem while_infinite: "P ;; true\<^sub>h = true \<Longrightarrow> while\<^sub>\<bottom> true do P od = true"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P ;; true = true \<Longrightarrow> while\<^sub>\<bottom> true do P od = true
[PROOF STEP]
apply (simp add: while_bot_true)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P ;; true = true \<Longrightarrow> \<mu> ((;;) P) = true
[PROOF STEP]
apply (rule antisym)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. P ;; true = true \<Longrightarrow> true \<sqsubseteq> \<mu> ((;;) P)
 2. P ;; true = true \<Longrightarrow> \<mu> ((;;) P) \<sqsubseteq> true
[PROOF STEP]
apply (simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P ;; true = true \<Longrightarrow> \<mu> ((;;) P) \<sqsubseteq> true
[PROOF STEP]
apply (rule gfp_upperbound)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P ;; true = true \<Longrightarrow> P ;; true \<sqsubseteq> true
[PROOF STEP]
apply (simp)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma b_rel_subtyping_merge_eqA_tR[sepref_frame_merge_rules]:
  shows "hn_ctxt (b_assn A P) x y \<or>\<^sub>A hn_ctxt A x y \<Longrightarrow>\<^sub>t hn_ctxt A x y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hn_ctxt (b_assn A P) x y \<or>\<^sub>A hn_ctxt A x y \<Longrightarrow>\<^sub>t hn_ctxt A x y
[PROOF STEP]
using b_rel_subtyping_merge_eqA[of A P x y "\<lambda>_. True", simplified]
[PROOF STATE]
proof (prove)
using this:
hn_ctxt (b_assn A P) x y \<or>\<^sub>A hn_ctxt A x y \<Longrightarrow>\<^sub>t hn_ctxt A x y

goal (1 subgoal):
 1. hn_ctxt (b_assn A P) x y \<or>\<^sub>A hn_ctxt A x y \<Longrightarrow>\<^sub>t hn_ctxt A x y
[PROOF STEP]
.


[STATEMENT]
lemma \<Delta>\<^sub>\<epsilon>_def':
  "\<Delta>\<^sub>\<epsilon> \ \ = {|(\<alpha>, \<beta>). (\<exists>t. ground t \<and> \<alpha> |\<in>| ta_der \ t \<and> \<beta> |\<in>| ta_der \ t)|}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Delta>\<^sub>\<epsilon> \ \ = {|(\<alpha>, \<beta>). \<exists>t. ground t \<and> \<alpha> |\<in>| ta_der \ t \<and> \<beta> |\<in>| ta_der \ t|}
[PROOF STEP]
proof (intro fset_eqI iffI, goal_cases lr rl)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. x |\<in>| \<Delta>\<^sub>\<epsilon> \ \ \<Longrightarrow> x |\<in>| {|(\<alpha>, \<beta>). \<exists>t. ground t \<and> \<alpha> |\<in>| ta_der \ t \<and> \<beta> |\<in>| ta_der \ t|}
 2. \<And>x. x |\<in>| {|(\<alpha>, \<beta>). \<exists>t. ground t \<and> \<alpha> |\<in>| ta_der \ t \<and> \<beta> |\<in>| ta_der \ t|} \<Longrightarrow> x |\<in>| \<Delta>\<^sub>\<epsilon> \ \
[PROOF STEP]
case (lr x)
[PROOF STATE]
proof (state)
this:
x |\<in>| \<Delta>\<^sub>\<epsilon> \ \

goal (2 subgoals):
 1. \<And>x. x |\<in>| \<Delta>\<^sub>\<epsilon> \ \ \<Longrightarrow> x |\<in>| {|(\<alpha>, \<beta>). \<exists>t. ground t \<and> \<alpha> |\<in>| ta_der \ t \<and> \<beta> |\<in>| ta_der \ t|}
 2. \<And>x. x |\<in>| {|(\<alpha>, \<beta>). \<exists>t. ground t \<and> \<alpha> |\<in>| ta_der \ t \<and> \<beta> |\<in>| ta_der \ t|} \<Longrightarrow> x |\<in>| \<Delta>\<^sub>\<epsilon> \ \
[PROOF STEP]
obtain p q where x [simp]: "x = (p, q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>p q. x = (p, q) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (cases x)
[PROOF STATE]
proof (state)
this:
x = (p, q)

goal (2 subgoals):
 1. \<And>x. x |\<in>| \<Delta>\<^sub>\<epsilon> \ \ \<Longrightarrow> x |\<in>| {|(\<alpha>, \<beta>). \<exists>t. ground t \<and> \<alpha> |\<in>| ta_der \ t \<and> \<beta> |\<in>| ta_der \ t|}
 2. \<And>x. x |\<in>| {|(\<alpha>, \<beta>). \<exists>t. ground t \<and> \<alpha> |\<in>| ta_der \ t \<and> \<beta> |\<in>| ta_der \ t|} \<Longrightarrow> x |\<in>| \<Delta>\<^sub>\<epsilon> \ \
[PROOF STEP]
have "\<exists>t. ground t \<and> p |\<in>| ta_der \ t \<and> q |\<in>| ta_der \ t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>t. ground t \<and> p |\<in>| ta_der \ t \<and> q |\<in>| ta_der \ t
[PROOF STEP]
using lr
[PROOF STATE]
proof (prove)
using this:
x |\<in>| \<Delta>\<^sub>\<epsilon> \ \

goal (1 subgoal):
 1. \<exists>t. ground t \<and> p |\<in>| ta_der \ t \<and> q |\<in>| ta_der \ t
[PROOF STEP]
unfolding x
[PROOF STATE]
proof (prove)
using this:
(p, q) |\<in>| \<Delta>\<^sub>\<epsilon> \ \

goal (1 subgoal):
 1. \<exists>t. ground t \<and> p |\<in>| ta_der \ t \<and> q |\<in>| ta_der \ t
[PROOF STEP]
proof (induct rule: \<Delta>\<^sub>\<epsilon>_induct)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>f ps p qs q. \<lbrakk>f ps \<rightarrow> p |\<in>| rules \; f qs \<rightarrow> q |\<in>| rules \; length ps = length qs; \<And>i. i < length qs \<Longrightarrow> (ps ! i, qs ! i) |\<in>| \<Delta>\<^sub>\<epsilon> \ \; \<And>i. i < length qs \<Longrightarrow> \<exists>t. ground t \<and> ps ! i |\<in>| ta_der \ t \<and> qs ! i |\<in>| ta_der \ t\<rbrakk> \<Longrightarrow> \<exists>t. ground t \<and> p |\<in>| ta_der \ t \<and> q |\<in>| ta_der \ t
 2. \<And>p p' q. \<lbrakk>(p, p') |\<in>| eps \; (p, q) |\<in>| \<Delta>\<^sub>\<epsilon> \ \; \<exists>t. ground t \<and> p |\<in>| ta_der \ t \<and> q |\<in>| ta_der \ t\<rbrakk> \<Longrightarrow> \<exists>t. ground t \<and> p' |\<in>| ta_der \ t \<and> q |\<in>| ta_der \ t
 3. \<And>q q' p. \<lbrakk>(q, q') |\<in>| eps \; (p, q) |\<in>| \<Delta>\<^sub>\<epsilon> \ \; \<exists>t. ground t \<and> p |\<in>| ta_der \ t \<and> q |\<in>| ta_der \ t\<rbrakk> \<Longrightarrow> \<exists>t. ground t \<and> p |\<in>| ta_der \ t \<and> q' |\<in>| ta_der \ t
[PROOF STEP]
case (\<Delta>\<^sub>\<epsilon>_cong f ps p qs q)
[PROOF STATE]
proof (state)
this:
f ps \<rightarrow> p |\<in>| rules \
f qs \<rightarrow> q |\<in>| rules \
length ps = length qs
?i < length qs \<Longrightarrow> (ps ! ?i, qs ! ?i) |\<in>| \<Delta>\<^sub>\<epsilon> \ \
?i < length qs \<Longrightarrow> \<exists>t. ground t \<and> ps ! ?i |\<in>| ta_der \ t \<and> qs ! ?i |\<in>| ta_der \ t

goal (3 subgoals):
 1. \<And>f ps p qs q. \<lbrakk>f ps \<rightarrow> p |\<in>| rules \; f qs \<rightarrow> q |\<in>| rules \; length ps = length qs; \<And>i. i < length qs \<Longrightarrow> (ps ! i, qs ! i) |\<in>| \<Delta>\<^sub>\<epsilon> \ \; \<And>i. i < length qs \<Longrightarrow> \<exists>t. ground t \<and> ps ! i |\<in>| ta_der \ t \<and> qs ! i |\<in>| ta_der \ t\<rbrakk> \<Longrightarrow> \<exists>t. ground t \<and> p |\<in>| ta_der \ t \<and> q |\<in>| ta_der \ t
 2. \<And>p p' q. \<lbrakk>(p, p') |\<in>| eps \; (p, q) |\<in>| \<Delta>\<^sub>\<epsilon> \ \; \<exists>t. ground t \<and> p |\<in>| ta_der \ t \<and> q |\<in>| ta_der \ t\<rbrakk> \<Longrightarrow> \<exists>t. ground t \<and> p' |\<in>| ta_der \ t \<and> q |\<in>| ta_der \ t
 3. \<And>q q' p. \<lbrakk>(q, q') |\<in>| eps \; (p, q) |\<in>| \<Delta>\<^sub>\<epsilon> \ \; \<exists>t. ground t \<and> p |\<in>| ta_der \ t \<and> q |\<in>| ta_der \ t\<rbrakk> \<Longrightarrow> \<exists>t. ground t \<and> p |\<in>| ta_der \ t \<and> q' |\<in>| ta_der \ t
[PROOF STEP]
obtain ts where ts: "ground (ts i) \<and> ps ! i |\<in>| ta_der \ (ts i) \<and> qs ! i |\<in>| ta_der \ (ts i)"
      if "i < length qs" for i
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>ts. (\<And>i. i < length qs \<Longrightarrow> ground (ts i) \<and> ps ! i |\<in>| ta_der \ (ts i) \<and> qs ! i |\<in>| ta_der \ (ts i)) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using \<Delta>\<^sub>\<epsilon>_cong(5)
[PROOF STATE]
proof (prove)
using this:
?i < length qs \<Longrightarrow> \<exists>t. ground t \<and> ps ! ?i |\<in>| ta_der \ t \<and> qs ! ?i |\<in>| ta_der \ t

goal (1 subgoal):
 1. (\<And>ts. (\<And>i. i < length qs \<Longrightarrow> ground (ts i) \<and> ps ! i |\<in>| ta_der \ (ts i) \<and> qs ! i |\<in>| ta_der \ (ts i)) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
?i < length qs \<Longrightarrow> ground (ts ?i) \<and> ps ! ?i |\<in>| ta_der \ (ts ?i) \<and> qs ! ?i |\<in>| ta_der \ (ts ?i)

goal (3 subgoals):
 1. \<And>f ps p qs q. \<lbrakk>f ps \<rightarrow> p |\<in>| rules \; f qs \<rightarrow> q |\<in>| rules \; length ps = length qs; \<And>i. i < length qs \<Longrightarrow> (ps ! i, qs ! i) |\<in>| \<Delta>\<^sub>\<epsilon> \ \; \<And>i. i < length qs \<Longrightarrow> \<exists>t. ground t \<and> ps ! i |\<in>| ta_der \ t \<and> qs ! i |\<in>| ta_der \ t\<rbrakk> \<Longrightarrow> \<exists>t. ground t \<and> p |\<in>| ta_der \ t \<and> q |\<in>| ta_der \ t
 2. \<And>p p' q. \<lbrakk>(p, p') |\<in>| eps \; (p, q) |\<in>| \<Delta>\<^sub>\<epsilon> \ \; \<exists>t. ground t \<and> p |\<in>| ta_der \ t \<and> q |\<in>| ta_der \ t\<rbrakk> \<Longrightarrow> \<exists>t. ground t \<and> p' |\<in>| ta_der \ t \<and> q |\<in>| ta_der \ t
 3. \<And>q q' p. \<lbrakk>(q, q') |\<in>| eps \; (p, q) |\<in>| \<Delta>\<^sub>\<epsilon> \ \; \<exists>t. ground t \<and> p |\<in>| ta_der \ t \<and> q |\<in>| ta_der \ t\<rbrakk> \<Longrightarrow> \<exists>t. ground t \<and> p |\<in>| ta_der \ t \<and> q' |\<in>| ta_der \ t
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
?i < length qs \<Longrightarrow> ground (ts ?i) \<and> ps ! ?i |\<in>| ta_der \ (ts ?i) \<and> qs ! ?i |\<in>| ta_der \ (ts ?i)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
?i < length qs \<Longrightarrow> ground (ts ?i) \<and> ps ! ?i |\<in>| ta_der \ (ts ?i) \<and> qs ! ?i |\<in>| ta_der \ (ts ?i)

goal (1 subgoal):
 1. \<exists>t. ground t \<and> p |\<in>| ta_der \ t \<and> q |\<in>| ta_der \ t
[PROOF STEP]
using \<Delta>\<^sub>\<epsilon>_cong(1-3)
[PROOF STATE]
proof (prove)
using this:
?i < length qs \<Longrightarrow> ground (ts ?i) \<and> ps ! ?i |\<in>| ta_der \ (ts ?i) \<and> qs ! ?i |\<in>| ta_der \ (ts ?i)
f ps \<rightarrow> p |\<in>| rules \
f qs \<rightarrow> q |\<in>| rules \
length ps = length qs

goal (1 subgoal):
 1. \<exists>t. ground t \<and> p |\<in>| ta_der \ t \<and> q |\<in>| ta_der \ t
[PROOF STEP]
by (auto intro!: exI[of _ "Fun f (map ts [0..<length qs])"]) blast+
[PROOF STATE]
proof (state)
this:
\<exists>t. ground t \<and> p |\<in>| ta_der \ t \<and> q |\<in>| ta_der \ t

goal (2 subgoals):
 1. \<And>p p' q. \<lbrakk>(p, p') |\<in>| eps \; (p, q) |\<in>| \<Delta>\<^sub>\<epsilon> \ \; \<exists>t. ground t \<and> p |\<in>| ta_der \ t \<and> q |\<in>| ta_der \ t\<rbrakk> \<Longrightarrow> \<exists>t. ground t \<and> p' |\<in>| ta_der \ t \<and> q |\<in>| ta_der \ t
 2. \<And>q q' p. \<lbrakk>(q, q') |\<in>| eps \; (p, q) |\<in>| \<Delta>\<^sub>\<epsilon> \ \; \<exists>t. ground t \<and> p |\<in>| ta_der \ t \<and> q |\<in>| ta_der \ t\<rbrakk> \<Longrightarrow> \<exists>t. ground t \<and> p |\<in>| ta_der \ t \<and> q' |\<in>| ta_der \ t
[PROOF STEP]
qed (meson ta_der_eps)+
[PROOF STATE]
proof (state)
this:
\<exists>t. ground t \<and> p |\<in>| ta_der \ t \<and> q |\<in>| ta_der \ t

goal (2 subgoals):
 1. \<And>x. x |\<in>| \<Delta>\<^sub>\<epsilon> \ \ \<Longrightarrow> x |\<in>| {|(\<alpha>, \<beta>). \<exists>t. ground t \<and> \<alpha> |\<in>| ta_der \ t \<and> \<beta> |\<in>| ta_der \ t|}
 2. \<And>x. x |\<in>| {|(\<alpha>, \<beta>). \<exists>t. ground t \<and> \<alpha> |\<in>| ta_der \ t \<and> \<beta> |\<in>| ta_der \ t|} \<Longrightarrow> x |\<in>| \<Delta>\<^sub>\<epsilon> \ \
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>t. ground t \<and> p |\<in>| ta_der \ t \<and> q |\<in>| ta_der \ t
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<exists>t. ground t \<and> p |\<in>| ta_der \ t \<and> q |\<in>| ta_der \ t

goal (1 subgoal):
 1. x |\<in>| {|(\<alpha>, \<beta>). \<exists>t. ground t \<and> \<alpha> |\<in>| ta_der \ t \<and> \<beta> |\<in>| ta_der \ t|}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x |\<in>| {|(\<alpha>, \<beta>). \<exists>t. ground t \<and> \<alpha> |\<in>| ta_der \ t \<and> \<beta> |\<in>| ta_der \ t|}

goal (1 subgoal):
 1. \<And>x. x |\<in>| {|(\<alpha>, \<beta>). \<exists>t. ground t \<and> \<alpha> |\<in>| ta_der \ t \<and> \<beta> |\<in>| ta_der \ t|} \<Longrightarrow> x |\<in>| \<Delta>\<^sub>\<epsilon> \ \
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x |\<in>| {|(\<alpha>, \<beta>). \<exists>t. ground t \<and> \<alpha> |\<in>| ta_der \ t \<and> \<beta> |\<in>| ta_der \ t|} \<Longrightarrow> x |\<in>| \<Delta>\<^sub>\<epsilon> \ \
[PROOF STEP]
case (rl x)
[PROOF STATE]
proof (state)
this:
x |\<in>| {|(\<alpha>, \<beta>). \<exists>t. ground t \<and> \<alpha> |\<in>| ta_der \ t \<and> \<beta> |\<in>| ta_der \ t|}

goal (1 subgoal):
 1. \<And>x. x |\<in>| {|(\<alpha>, \<beta>). \<exists>t. ground t \<and> \<alpha> |\<in>| ta_der \ t \<and> \<beta> |\<in>| ta_der \ t|} \<Longrightarrow> x |\<in>| \<Delta>\<^sub>\<epsilon> \ \
[PROOF STEP]
obtain p q where x [simp]: "x = (p, q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>p q. x = (p, q) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (cases x)
[PROOF STATE]
proof (state)
this:
x = (p, q)

goal (1 subgoal):
 1. \<And>x. x |\<in>| {|(\<alpha>, \<beta>). \<exists>t. ground t \<and> \<alpha> |\<in>| ta_der \ t \<and> \<beta> |\<in>| ta_der \ t|} \<Longrightarrow> x |\<in>| \<Delta>\<^sub>\<epsilon> \ \
[PROOF STEP]
obtain t where "ground t" "p |\<in>| ta_der \ t" "q |\<in>| ta_der \ t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>t. \<lbrakk>ground t; p |\<in>| ta_der \ t; q |\<in>| ta_der \ t\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using rl
[PROOF STATE]
proof (prove)
using this:
x |\<in>| {|(\<alpha>, \<beta>). \<exists>t. ground t \<and> \<alpha> |\<in>| ta_der \ t \<and> \<beta> |\<in>| ta_der \ t|}

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

goal (1 subgoal):
 1. \<And>x. x |\<in>| {|(\<alpha>, \<beta>). \<exists>t. ground t \<and> \<alpha> |\<in>| ta_der \ t \<and> \<beta> |\<in>| ta_der \ t|} \<Longrightarrow> x |\<in>| \<Delta>\<^sub>\<epsilon> \ \
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ground t
p |\<in>| ta_der \ t
q |\<in>| ta_der \ t
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
ground t
p |\<in>| ta_der \ t
q |\<in>| ta_der \ t

goal (1 subgoal):
 1. x |\<in>| \<Delta>\<^sub>\<epsilon> \ \
[PROOF STEP]
unfolding x
[PROOF STATE]
proof (prove)
using this:
ground t
p |\<in>| ta_der \ t
q |\<in>| ta_der \ t

goal (1 subgoal):
 1. (p, q) |\<in>| \<Delta>\<^sub>\<epsilon> \ \
[PROOF STEP]
proof (induct t arbitrary: p q)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x p q. \<lbrakk>ground (Var x); p |\<in>| ta_der \ (Var x); q |\<in>| ta_der \ (Var x)\<rbrakk> \<Longrightarrow> (p, q) |\<in>| \<Delta>\<^sub>\<epsilon> \ \
 2. \<And>x1a x2 p q. \<lbrakk>\<And>x2a p q. \<lbrakk>x2a \<in> set x2; ground x2a; p |\<in>| ta_der \ x2a; q |\<in>| ta_der \ x2a\<rbrakk> \<Longrightarrow> (p, q) |\<in>| \<Delta>\<^sub>\<epsilon> \ \; ground (Fun x1a x2); p |\<in>| ta_der \ (Fun x1a x2); q |\<in>| ta_der \ (Fun x1a x2)\<rbrakk> \<Longrightarrow> (p, q) |\<in>| \<Delta>\<^sub>\<epsilon> \ \
[PROOF STEP]
case (Fun f ts)
[PROOF STATE]
proof (state)
this:
\<lbrakk>?x2a \<in> set ts; ground ?x2a; ?p |\<in>| ta_der \ ?x2a; ?q |\<in>| ta_der \ ?x2a\<rbrakk> \<Longrightarrow> (?p, ?q) |\<in>| \<Delta>\<^sub>\<epsilon> \ \
ground (Fun f ts)
p |\<in>| ta_der \ (Fun f ts)
q |\<in>| ta_der \ (Fun f ts)

goal (2 subgoals):
 1. \<And>x p q. \<lbrakk>ground (Var x); p |\<in>| ta_der \ (Var x); q |\<in>| ta_der \ (Var x)\<rbrakk> \<Longrightarrow> (p, q) |\<in>| \<Delta>\<^sub>\<epsilon> \ \
 2. \<And>x1a x2 p q. \<lbrakk>\<And>x2a p q. \<lbrakk>x2a \<in> set x2; ground x2a; p |\<in>| ta_der \ x2a; q |\<in>| ta_der \ x2a\<rbrakk> \<Longrightarrow> (p, q) |\<in>| \<Delta>\<^sub>\<epsilon> \ \; ground (Fun x1a x2); p |\<in>| ta_der \ (Fun x1a x2); q |\<in>| ta_der \ (Fun x1a x2)\<rbrakk> \<Longrightarrow> (p, q) |\<in>| \<Delta>\<^sub>\<epsilon> \ \
[PROOF STEP]
obtain p' ps where p': "TA_rule f ps p' |\<in>| rules \" "p' = p \<or> (p', p) |\<in>| (eps \)|\<^sup>+|" "length ps = length ts"
      "\<And>i. i < length ts \<Longrightarrow> ps ! i |\<in>| ta_der \ (ts ! i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>ps p'. \<lbrakk>f ps \<rightarrow> p' |\<in>| rules \; p' = p \<or> (p', p) |\<in>| (eps \)|\<^sup>+|; length ps = length ts; \<And>i. i < length ts \<Longrightarrow> ps ! i |\<in>| ta_der \ (ts ! i)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using Fun(3)
[PROOF STATE]
proof (prove)
using this:
p |\<in>| ta_der \ (Fun f ts)

goal (1 subgoal):
 1. (\<And>ps p'. \<lbrakk>f ps \<rightarrow> p' |\<in>| rules \; p' = p \<or> (p', p) |\<in>| (eps \)|\<^sup>+|; length ps = length ts; \<And>i. i < length ts \<Longrightarrow> ps ! i |\<in>| ta_der \ (ts ! i)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
f ps \<rightarrow> p' |\<in>| rules \
p' = p \<or> (p', p) |\<in>| (eps \)|\<^sup>+|
length ps = length ts
?i < length ts \<Longrightarrow> ps ! ?i |\<in>| ta_der \ (ts ! ?i)

goal (2 subgoals):
 1. \<And>x p q. \<lbrakk>ground (Var x); p |\<in>| ta_der \ (Var x); q |\<in>| ta_der \ (Var x)\<rbrakk> \<Longrightarrow> (p, q) |\<in>| \<Delta>\<^sub>\<epsilon> \ \
 2. \<And>x1a x2 p q. \<lbrakk>\<And>x2a p q. \<lbrakk>x2a \<in> set x2; ground x2a; p |\<in>| ta_der \ x2a; q |\<in>| ta_der \ x2a\<rbrakk> \<Longrightarrow> (p, q) |\<in>| \<Delta>\<^sub>\<epsilon> \ \; ground (Fun x1a x2); p |\<in>| ta_der \ (Fun x1a x2); q |\<in>| ta_der \ (Fun x1a x2)\<rbrakk> \<Longrightarrow> (p, q) |\<in>| \<Delta>\<^sub>\<epsilon> \ \
[PROOF STEP]
obtain q' qs where q': "f qs \<rightarrow> q' |\<in>| rules \" "q' = q \<or> (q', q) |\<in>| (eps \)|\<^sup>+|" "length qs = length ts"
      "\<And>i. i < length ts \<Longrightarrow> qs ! i |\<in>| ta_der \ (ts ! i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>qs q'. \<lbrakk>f qs \<rightarrow> q' |\<in>| rules \; q' = q \<or> (q', q) |\<in>| (eps \)|\<^sup>+|; length qs = length ts; \<And>i. i < length ts \<Longrightarrow> qs ! i |\<in>| ta_der \ (ts ! i)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using Fun(4)
[PROOF STATE]
proof (prove)
using this:
q |\<in>| ta_der \ (Fun f ts)

goal (1 subgoal):
 1. (\<And>qs q'. \<lbrakk>f qs \<rightarrow> q' |\<in>| rules \; q' = q \<or> (q', q) |\<in>| (eps \)|\<^sup>+|; length qs = length ts; \<And>i. i < length ts \<Longrightarrow> qs ! i |\<in>| ta_der \ (ts ! i)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
f qs \<rightarrow> q' |\<in>| rules \
q' = q \<or> (q', q) |\<in>| (eps \)|\<^sup>+|
length qs = length ts
?i < length ts \<Longrightarrow> qs ! ?i |\<in>| ta_der \ (ts ! ?i)

goal (2 subgoals):
 1. \<And>x p q. \<lbrakk>ground (Var x); p |\<in>| ta_der \ (Var x); q |\<in>| ta_der \ (Var x)\<rbrakk> \<Longrightarrow> (p, q) |\<in>| \<Delta>\<^sub>\<epsilon> \ \
 2. \<And>x1a x2 p q. \<lbrakk>\<And>x2a p q. \<lbrakk>x2a \<in> set x2; ground x2a; p |\<in>| ta_der \ x2a; q |\<in>| ta_der \ x2a\<rbrakk> \<Longrightarrow> (p, q) |\<in>| \<Delta>\<^sub>\<epsilon> \ \; ground (Fun x1a x2); p |\<in>| ta_der \ (Fun x1a x2); q |\<in>| ta_der \ (Fun x1a x2)\<rbrakk> \<Longrightarrow> (p, q) |\<in>| \<Delta>\<^sub>\<epsilon> \ \
[PROOF STEP]
have st: "(p', q') |\<in>| \<Delta>\<^sub>\<epsilon> \ \"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (p', q') |\<in>| \<Delta>\<^sub>\<epsilon> \ \
[PROOF STEP]
using Fun(1)[OF nth_mem _ p'(4) q'(4)] Fun(2) p'(3) q'(3)
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?i1 < length ts; ground (ts ! ?i1); ?i1 < length ts; ?i1 < length ts\<rbrakk> \<Longrightarrow> (ps ! ?i1, qs ! ?i1) |\<in>| \<Delta>\<^sub>\<epsilon> \ \
ground (Fun f ts)
length ps = length ts
length qs = length ts

goal (1 subgoal):
 1. (p', q') |\<in>| \<Delta>\<^sub>\<epsilon> \ \
[PROOF STEP]
by (intro \<Delta>\<^sub>\<epsilon>_cong[OF p'(1) q'(1)]) auto
[PROOF STATE]
proof (state)
this:
(p', q') |\<in>| \<Delta>\<^sub>\<epsilon> \ \

goal (2 subgoals):
 1. \<And>x p q. \<lbrakk>ground (Var x); p |\<in>| ta_der \ (Var x); q |\<in>| ta_der \ (Var x)\<rbrakk> \<Longrightarrow> (p, q) |\<in>| \<Delta>\<^sub>\<epsilon> \ \
 2. \<And>x1a x2 p q. \<lbrakk>\<And>x2a p q. \<lbrakk>x2a \<in> set x2; ground x2a; p |\<in>| ta_der \ x2a; q |\<in>| ta_der \ x2a\<rbrakk> \<Longrightarrow> (p, q) |\<in>| \<Delta>\<^sub>\<epsilon> \ \; ground (Fun x1a x2); p |\<in>| ta_der \ (Fun x1a x2); q |\<in>| ta_der \ (Fun x1a x2)\<rbrakk> \<Longrightarrow> (p, q) |\<in>| \<Delta>\<^sub>\<epsilon> \ \
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
(p', q') |\<in>| \<Delta>\<^sub>\<epsilon> \ \

goal (2 subgoals):
 1. \<And>x p q. \<lbrakk>ground (Var x); p |\<in>| ta_der \ (Var x); q |\<in>| ta_der \ (Var x)\<rbrakk> \<Longrightarrow> (p, q) |\<in>| \<Delta>\<^sub>\<epsilon> \ \
 2. \<And>x1a x2 p q. \<lbrakk>\<And>x2a p q. \<lbrakk>x2a \<in> set x2; ground x2a; p |\<in>| ta_der \ x2a; q |\<in>| ta_der \ x2a\<rbrakk> \<Longrightarrow> (p, q) |\<in>| \<Delta>\<^sub>\<epsilon> \ \; ground (Fun x1a x2); p |\<in>| ta_der \ (Fun x1a x2); q |\<in>| ta_der \ (Fun x1a x2)\<rbrakk> \<Longrightarrow> (p, q) |\<in>| \<Delta>\<^sub>\<epsilon> \ \
[PROOF STEP]
assume "(p', p) |\<in>| (eps \)|\<^sup>+|"
[PROOF STATE]
proof (state)
this:
(p', p) |\<in>| (eps \)|\<^sup>+|

goal (2 subgoals):
 1. \<And>x p q. \<lbrakk>ground (Var x); p |\<in>| ta_der \ (Var x); q |\<in>| ta_der \ (Var x)\<rbrakk> \<Longrightarrow> (p, q) |\<in>| \<Delta>\<^sub>\<epsilon> \ \
 2. \<And>x1a x2 p q. \<lbrakk>\<And>x2a p q. \<lbrakk>x2a \<in> set x2; ground x2a; p |\<in>| ta_der \ x2a; q |\<in>| ta_der \ x2a\<rbrakk> \<Longrightarrow> (p, q) |\<in>| \<Delta>\<^sub>\<epsilon> \ \; ground (Fun x1a x2); p |\<in>| ta_der \ (Fun x1a x2); q |\<in>| ta_der \ (Fun x1a x2)\<rbrakk> \<Longrightarrow> (p, q) |\<in>| \<Delta>\<^sub>\<epsilon> \ \
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(p', p) |\<in>| (eps \)|\<^sup>+|
[PROOF STEP]
have "(p, q') |\<in>| \<Delta>\<^sub>\<epsilon> \ \"
[PROOF STATE]
proof (prove)
using this:
(p', p) |\<in>| (eps \)|\<^sup>+|

goal (1 subgoal):
 1. (p, q') |\<in>| \<Delta>\<^sub>\<epsilon> \ \
[PROOF STEP]
using st
[PROOF STATE]
proof (prove)
using this:
(p', p) |\<in>| (eps \)|\<^sup>+|
(p', q') |\<in>| \<Delta>\<^sub>\<epsilon> \ \

goal (1 subgoal):
 1. (p, q') |\<in>| \<Delta>\<^sub>\<epsilon> \ \
[PROOF STEP]
by (induct rule: ftrancl_induct) (auto intro: \<Delta>\<^sub>\<epsilon>_eps1)
[PROOF STATE]
proof (state)
this:
(p, q') |\<in>| \<Delta>\<^sub>\<epsilon> \ \

goal (2 subgoals):
 1. \<And>x p q. \<lbrakk>ground (Var x); p |\<in>| ta_der \ (Var x); q |\<in>| ta_der \ (Var x)\<rbrakk> \<Longrightarrow> (p, q) |\<in>| \<Delta>\<^sub>\<epsilon> \ \
 2. \<And>x1a x2 p q. \<lbrakk>\<And>x2a p q. \<lbrakk>x2a \<in> set x2; ground x2a; p |\<in>| ta_der \ x2a; q |\<in>| ta_der \ x2a\<rbrakk> \<Longrightarrow> (p, q) |\<in>| \<Delta>\<^sub>\<epsilon> \ \; ground (Fun x1a x2); p |\<in>| ta_der \ (Fun x1a x2); q |\<in>| ta_der \ (Fun x1a x2)\<rbrakk> \<Longrightarrow> (p, q) |\<in>| \<Delta>\<^sub>\<epsilon> \ \
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
(p', p) |\<in>| (eps \)|\<^sup>+| \<Longrightarrow> (p, q') |\<in>| \<Delta>\<^sub>\<epsilon> \ \

goal (2 subgoals):
 1. \<And>x p q. \<lbrakk>ground (Var x); p |\<in>| ta_der \ (Var x); q |\<in>| ta_der \ (Var x)\<rbrakk> \<Longrightarrow> (p, q) |\<in>| \<Delta>\<^sub>\<epsilon> \ \
 2. \<And>x1a x2 p q. \<lbrakk>\<And>x2a p q. \<lbrakk>x2a \<in> set x2; ground x2a; p |\<in>| ta_der \ x2a; q |\<in>| ta_der \ x2a\<rbrakk> \<Longrightarrow> (p, q) |\<in>| \<Delta>\<^sub>\<epsilon> \ \; ground (Fun x1a x2); p |\<in>| ta_der \ (Fun x1a x2); q |\<in>| ta_der \ (Fun x1a x2)\<rbrakk> \<Longrightarrow> (p, q) |\<in>| \<Delta>\<^sub>\<epsilon> \ \
[PROOF STEP]
from st this p'(2)
[PROOF STATE]
proof (chain)
picking this:
(p', q') |\<in>| \<Delta>\<^sub>\<epsilon> \ \
(p', p) |\<in>| (eps \)|\<^sup>+| \<Longrightarrow> (p, q') |\<in>| \<Delta>\<^sub>\<epsilon> \ \
p' = p \<or> (p', p) |\<in>| (eps \)|\<^sup>+|
[PROOF STEP]
have st: "(p, q') |\<in>| \<Delta>\<^sub>\<epsilon> \ \"
[PROOF STATE]
proof (prove)
using this:
(p', q') |\<in>| \<Delta>\<^sub>\<epsilon> \ \
(p', p) |\<in>| (eps \)|\<^sup>+| \<Longrightarrow> (p, q') |\<in>| \<Delta>\<^sub>\<epsilon> \ \
p' = p \<or> (p', p) |\<in>| (eps \)|\<^sup>+|

goal (1 subgoal):
 1. (p, q') |\<in>| \<Delta>\<^sub>\<epsilon> \ \
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(p, q') |\<in>| \<Delta>\<^sub>\<epsilon> \ \

goal (2 subgoals):
 1. \<And>x p q. \<lbrakk>ground (Var x); p |\<in>| ta_der \ (Var x); q |\<in>| ta_der \ (Var x)\<rbrakk> \<Longrightarrow> (p, q) |\<in>| \<Delta>\<^sub>\<epsilon> \ \
 2. \<And>x1a x2 p q. \<lbrakk>\<And>x2a p q. \<lbrakk>x2a \<in> set x2; ground x2a; p |\<in>| ta_der \ x2a; q |\<in>| ta_der \ x2a\<rbrakk> \<Longrightarrow> (p, q) |\<in>| \<Delta>\<^sub>\<epsilon> \ \; ground (Fun x1a x2); p |\<in>| ta_der \ (Fun x1a x2); q |\<in>| ta_der \ (Fun x1a x2)\<rbrakk> \<Longrightarrow> (p, q) |\<in>| \<Delta>\<^sub>\<epsilon> \ \
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
(p, q') |\<in>| \<Delta>\<^sub>\<epsilon> \ \

goal (2 subgoals):
 1. \<And>x p q. \<lbrakk>ground (Var x); p |\<in>| ta_der \ (Var x); q |\<in>| ta_der \ (Var x)\<rbrakk> \<Longrightarrow> (p, q) |\<in>| \<Delta>\<^sub>\<epsilon> \ \
 2. \<And>x1a x2 p q. \<lbrakk>\<And>x2a p q. \<lbrakk>x2a \<in> set x2; ground x2a; p |\<in>| ta_der \ x2a; q |\<in>| ta_der \ x2a\<rbrakk> \<Longrightarrow> (p, q) |\<in>| \<Delta>\<^sub>\<epsilon> \ \; ground (Fun x1a x2); p |\<in>| ta_der \ (Fun x1a x2); q |\<in>| ta_der \ (Fun x1a x2)\<rbrakk> \<Longrightarrow> (p, q) |\<in>| \<Delta>\<^sub>\<epsilon> \ \
[PROOF STEP]
assume "(q', q) |\<in>| (eps \)|\<^sup>+|"
[PROOF STATE]
proof (state)
this:
(q', q) |\<in>| (eps \)|\<^sup>+|

goal (2 subgoals):
 1. \<And>x p q. \<lbrakk>ground (Var x); p |\<in>| ta_der \ (Var x); q |\<in>| ta_der \ (Var x)\<rbrakk> \<Longrightarrow> (p, q) |\<in>| \<Delta>\<^sub>\<epsilon> \ \
 2. \<And>x1a x2 p q. \<lbrakk>\<And>x2a p q. \<lbrakk>x2a \<in> set x2; ground x2a; p |\<in>| ta_der \ x2a; q |\<in>| ta_der \ x2a\<rbrakk> \<Longrightarrow> (p, q) |\<in>| \<Delta>\<^sub>\<epsilon> \ \; ground (Fun x1a x2); p |\<in>| ta_der \ (Fun x1a x2); q |\<in>| ta_der \ (Fun x1a x2)\<rbrakk> \<Longrightarrow> (p, q) |\<in>| \<Delta>\<^sub>\<epsilon> \ \
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(q', q) |\<in>| (eps \)|\<^sup>+|
[PROOF STEP]
have "(p, q) |\<in>| \<Delta>\<^sub>\<epsilon> \ \"
[PROOF STATE]
proof (prove)
using this:
(q', q) |\<in>| (eps \)|\<^sup>+|

goal (1 subgoal):
 1. (p, q) |\<in>| \<Delta>\<^sub>\<epsilon> \ \
[PROOF STEP]
using st
[PROOF STATE]
proof (prove)
using this:
(q', q) |\<in>| (eps \)|\<^sup>+|
(p, q') |\<in>| \<Delta>\<^sub>\<epsilon> \ \

goal (1 subgoal):
 1. (p, q) |\<in>| \<Delta>\<^sub>\<epsilon> \ \
[PROOF STEP]
by (induct rule: ftrancl_induct) (auto intro: \<Delta>\<^sub>\<epsilon>_eps2)
[PROOF STATE]
proof (state)
this:
(p, q) |\<in>| \<Delta>\<^sub>\<epsilon> \ \

goal (2 subgoals):
 1. \<And>x p q. \<lbrakk>ground (Var x); p |\<in>| ta_der \ (Var x); q |\<in>| ta_der \ (Var x)\<rbrakk> \<Longrightarrow> (p, q) |\<in>| \<Delta>\<^sub>\<epsilon> \ \
 2. \<And>x1a x2 p q. \<lbrakk>\<And>x2a p q. \<lbrakk>x2a \<in> set x2; ground x2a; p |\<in>| ta_der \ x2a; q |\<in>| ta_der \ x2a\<rbrakk> \<Longrightarrow> (p, q) |\<in>| \<Delta>\<^sub>\<epsilon> \ \; ground (Fun x1a x2); p |\<in>| ta_der \ (Fun x1a x2); q |\<in>| ta_der \ (Fun x1a x2)\<rbrakk> \<Longrightarrow> (p, q) |\<in>| \<Delta>\<^sub>\<epsilon> \ \
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
(q', q) |\<in>| (eps \)|\<^sup>+| \<Longrightarrow> (p, q) |\<in>| \<Delta>\<^sub>\<epsilon> \ \

goal (2 subgoals):
 1. \<And>x p q. \<lbrakk>ground (Var x); p |\<in>| ta_der \ (Var x); q |\<in>| ta_der \ (Var x)\<rbrakk> \<Longrightarrow> (p, q) |\<in>| \<Delta>\<^sub>\<epsilon> \ \
 2. \<And>x1a x2 p q. \<lbrakk>\<And>x2a p q. \<lbrakk>x2a \<in> set x2; ground x2a; p |\<in>| ta_der \ x2a; q |\<in>| ta_der \ x2a\<rbrakk> \<Longrightarrow> (p, q) |\<in>| \<Delta>\<^sub>\<epsilon> \ \; ground (Fun x1a x2); p |\<in>| ta_der \ (Fun x1a x2); q |\<in>| ta_der \ (Fun x1a x2)\<rbrakk> \<Longrightarrow> (p, q) |\<in>| \<Delta>\<^sub>\<epsilon> \ \
[PROOF STEP]
from st this q'(2)
[PROOF STATE]
proof (chain)
picking this:
(p, q') |\<in>| \<Delta>\<^sub>\<epsilon> \ \
(q', q) |\<in>| (eps \)|\<^sup>+| \<Longrightarrow> (p, q) |\<in>| \<Delta>\<^sub>\<epsilon> \ \
q' = q \<or> (q', q) |\<in>| (eps \)|\<^sup>+|
[PROOF STEP]
show "(p, q) |\<in>| \<Delta>\<^sub>\<epsilon> \ \"
[PROOF STATE]
proof (prove)
using this:
(p, q') |\<in>| \<Delta>\<^sub>\<epsilon> \ \
(q', q) |\<in>| (eps \)|\<^sup>+| \<Longrightarrow> (p, q) |\<in>| \<Delta>\<^sub>\<epsilon> \ \
q' = q \<or> (q', q) |\<in>| (eps \)|\<^sup>+|

goal (1 subgoal):
 1. (p, q) |\<in>| \<Delta>\<^sub>\<epsilon> \ \
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(p, q) |\<in>| \<Delta>\<^sub>\<epsilon> \ \

goal (1 subgoal):
 1. \<And>x p q. \<lbrakk>ground (Var x); p |\<in>| ta_der \ (Var x); q |\<in>| ta_der \ (Var x)\<rbrakk> \<Longrightarrow> (p, q) |\<in>| \<Delta>\<^sub>\<epsilon> \ \
[PROOF STEP]
qed auto
[PROOF STATE]
proof (state)
this:
x |\<in>| \<Delta>\<^sub>\<epsilon> \ \

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma bt_dfs_simp:
  "bt_dfs f t = f t # bts_dfs f (children t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bt_dfs f t = f t # bts_dfs f (children t)
[PROOF STEP]
by (cases t) simp_all


[STATEMENT]
lemma exist_dioph[dioph]:
  fixes D
  assumes "is_dioph_rel D"
  shows "is_dioph_rel ([\<exists>] D)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_dioph_rel ([\<exists>] D)
[PROOF STEP]
unfolding EXIST_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_dioph_rel ([\<exists>1] D)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
is_dioph_rel D

goal (1 subgoal):
 1. is_dioph_rel ([\<exists>1] D)
[PROOF STEP]
by (auto simp: exist_list_dioph)


[STATEMENT]
lemma lowner_le_refl:
  assumes "A \<in> carrier_mat n n"
  shows "A \<le>\<^sub>L A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A \<le>\<^sub>L A
[PROOF STEP]
unfolding lowner_le_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dim_row A = dim_row A \<and> dim_col A = dim_col A \<and> positive (A - A)
[PROOF STEP]
apply (simp add: minus_r_inv_mat[OF assms])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. positive (0\<^sub>m n n)
[PROOF STEP]
by (rule positive_zero)


[STATEMENT]
lemma wf_below_UNIV[simp]:
  shows "wf_below r UNIV \<longleftrightarrow> wf r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf_below r UNIV = wf r
[PROOF STEP]
by (auto simp: wf_below_def rtrancl_converse[symmetric] Image_closed_trancl[OF subset_UNIV])


[STATEMENT]
lemma Hermite_of_upt_row_preserves_zero_rows:
  fixes A::"'a::{bezout_ring_div,normalization_semidom,unique_euclidean_ring}^'cols::{mod_type}^'rows::{mod_type}"
  assumes i: "is_zero_row i A"
  and e: "echelon_form A" and a: "ass_function ass" and r: "res_function res" and k: "k \<le> nrows A"
  shows "is_zero_row i (Hermite_of_upt_row_i A k ass res)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_zero_row i (Hermite_of_upt_row_i A k ass res)
[PROOF STEP]
proof (cases "to_nat i\<ge>k")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. k \<le> mod_type_class.to_nat i \<Longrightarrow> is_zero_row i (Hermite_of_upt_row_i A k ass res)
 2. \<not> k \<le> mod_type_class.to_nat i \<Longrightarrow> is_zero_row i (Hermite_of_upt_row_i A k ass res)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
k \<le> mod_type_class.to_nat i

goal (2 subgoals):
 1. k \<le> mod_type_class.to_nat i \<Longrightarrow> is_zero_row i (Hermite_of_upt_row_i A k ass res)
 2. \<not> k \<le> mod_type_class.to_nat i \<Longrightarrow> is_zero_row i (Hermite_of_upt_row_i A k ass res)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_zero_row i (Hermite_of_upt_row_i A k ass res)
[PROOF STEP]
by (rule Hermite_of_upt_row_preserves_zero_rows_ge[OF i k True])
[PROOF STATE]
proof (state)
this:
is_zero_row i (Hermite_of_upt_row_i A k ass res)

goal (1 subgoal):
 1. \<not> k \<le> mod_type_class.to_nat i \<Longrightarrow> is_zero_row i (Hermite_of_upt_row_i A k ass res)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> k \<le> mod_type_class.to_nat i \<Longrightarrow> is_zero_row i (Hermite_of_upt_row_i A k ass res)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> k \<le> mod_type_class.to_nat i

goal (1 subgoal):
 1. \<not> k \<le> mod_type_class.to_nat i \<Longrightarrow> is_zero_row i (Hermite_of_upt_row_i A k ass res)
[PROOF STEP]
hence i_k: "to_nat i < k"
[PROOF STATE]
proof (prove)
using this:
\<not> k \<le> mod_type_class.to_nat i

goal (1 subgoal):
 1. mod_type_class.to_nat i < k
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
mod_type_class.to_nat i < k

goal (1 subgoal):
 1. \<not> k \<le> mod_type_class.to_nat i \<Longrightarrow> is_zero_row i (Hermite_of_upt_row_i A k ass res)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_zero_row i (Hermite_of_upt_row_i A k ass res)
[PROOF STEP]
using k i_k
[PROOF STATE]
proof (prove)
using this:
k \<le> nrows A
mod_type_class.to_nat i < k

goal (1 subgoal):
 1. is_zero_row i (Hermite_of_upt_row_i A k ass res)
[PROOF STEP]
proof (induct k)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>0 \<le> nrows A; mod_type_class.to_nat i < 0\<rbrakk> \<Longrightarrow> is_zero_row i (Hermite_of_upt_row_i A 0 ass res)
 2. \<And>k. \<lbrakk>\<lbrakk>k \<le> nrows A; mod_type_class.to_nat i < k\<rbrakk> \<Longrightarrow> is_zero_row i (Hermite_of_upt_row_i A k ass res); Suc k \<le> nrows A; mod_type_class.to_nat i < Suc k\<rbrakk> \<Longrightarrow> is_zero_row i (Hermite_of_upt_row_i A (Suc k) ass res)
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:
0 \<le> nrows A
mod_type_class.to_nat i < 0

goal (2 subgoals):
 1. \<lbrakk>0 \<le> nrows A; mod_type_class.to_nat i < 0\<rbrakk> \<Longrightarrow> is_zero_row i (Hermite_of_upt_row_i A 0 ass res)
 2. \<And>k. \<lbrakk>\<lbrakk>k \<le> nrows A; mod_type_class.to_nat i < k\<rbrakk> \<Longrightarrow> is_zero_row i (Hermite_of_upt_row_i A k ass res); Suc k \<le> nrows A; mod_type_class.to_nat i < Suc k\<rbrakk> \<Longrightarrow> is_zero_row i (Hermite_of_upt_row_i A (Suc k) ass res)
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
0 \<le> nrows A
mod_type_class.to_nat i < 0

goal (1 subgoal):
 1. is_zero_row i (Hermite_of_upt_row_i A 0 ass res)
[PROOF STEP]
unfolding Hermite_of_upt_row_i_def
[PROOF STATE]
proof (prove)
using this:
0 \<le> nrows A
mod_type_class.to_nat i < 0

goal (1 subgoal):
 1. is_zero_row i (foldl (Hermite_of_row_i ass res) A (map mod_type_class.from_nat [0..<0]))
[PROOF STEP]
by (simp add: i)
[PROOF STATE]
proof (state)
this:
is_zero_row i (Hermite_of_upt_row_i A 0 ass res)

goal (1 subgoal):
 1. \<And>k. \<lbrakk>\<lbrakk>k \<le> nrows A; mod_type_class.to_nat i < k\<rbrakk> \<Longrightarrow> is_zero_row i (Hermite_of_upt_row_i A k ass res); Suc k \<le> nrows A; mod_type_class.to_nat i < Suc k\<rbrakk> \<Longrightarrow> is_zero_row i (Hermite_of_upt_row_i A (Suc k) ass res)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>k. \<lbrakk>\<lbrakk>k \<le> nrows A; mod_type_class.to_nat i < k\<rbrakk> \<Longrightarrow> is_zero_row i (Hermite_of_upt_row_i A k ass res); Suc k \<le> nrows A; mod_type_class.to_nat i < Suc k\<rbrakk> \<Longrightarrow> is_zero_row i (Hermite_of_upt_row_i A (Suc k) ass res)
[PROOF STEP]
case (Suc k)
[PROOF STATE]
proof (state)
this:
\<lbrakk>k \<le> nrows A; mod_type_class.to_nat i < k\<rbrakk> \<Longrightarrow> is_zero_row i (Hermite_of_upt_row_i A k ass res)
Suc k \<le> nrows A
mod_type_class.to_nat i < Suc k

goal (1 subgoal):
 1. \<And>k. \<lbrakk>\<lbrakk>k \<le> nrows A; mod_type_class.to_nat i < k\<rbrakk> \<Longrightarrow> is_zero_row i (Hermite_of_upt_row_i A k ass res); Suc k \<le> nrows A; mod_type_class.to_nat i < Suc k\<rbrakk> \<Longrightarrow> is_zero_row i (Hermite_of_upt_row_i A (Suc k) ass res)
[PROOF STEP]
have k: "k\<le>nrows A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k \<le> nrows A
[PROOF STEP]
using Suc.prems
[PROOF STATE]
proof (prove)
using this:
Suc k \<le> nrows A
mod_type_class.to_nat i < Suc k

goal (1 subgoal):
 1. k \<le> nrows A
[PROOF STEP]
unfolding nrows_def
[PROOF STATE]
proof (prove)
using this:
Suc k \<le> CARD('rows)
mod_type_class.to_nat i < Suc k

goal (1 subgoal):
 1. k \<le> CARD('rows)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
k \<le> nrows A

goal (1 subgoal):
 1. \<And>k. \<lbrakk>\<lbrakk>k \<le> nrows A; mod_type_class.to_nat i < k\<rbrakk> \<Longrightarrow> is_zero_row i (Hermite_of_upt_row_i A k ass res); Suc k \<le> nrows A; mod_type_class.to_nat i < Suc k\<rbrakk> \<Longrightarrow> is_zero_row i (Hermite_of_upt_row_i A (Suc k) ass res)
[PROOF STEP]
have k2: "k<nrows A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k < nrows A
[PROOF STEP]
using Suc.prems
[PROOF STATE]
proof (prove)
using this:
Suc k \<le> nrows A
mod_type_class.to_nat i < Suc k

goal (1 subgoal):
 1. k < nrows A
[PROOF STEP]
unfolding nrows_def
[PROOF STATE]
proof (prove)
using this:
Suc k \<le> CARD('rows)
mod_type_class.to_nat i < Suc k

goal (1 subgoal):
 1. k < CARD('rows)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
k < nrows A

goal (1 subgoal):
 1. \<And>k. \<lbrakk>\<lbrakk>k \<le> nrows A; mod_type_class.to_nat i < k\<rbrakk> \<Longrightarrow> is_zero_row i (Hermite_of_upt_row_i A k ass res); Suc k \<le> nrows A; mod_type_class.to_nat i < Suc k\<rbrakk> \<Longrightarrow> is_zero_row i (Hermite_of_upt_row_i A (Suc k) ass res)
[PROOF STEP]
define A' where "A' = foldl (Hermite_of_row_i ass res) A (map from_nat [0..<k])"
[PROOF STATE]
proof (state)
this:
A' = foldl (Hermite_of_row_i ass res) A (map mod_type_class.from_nat [0..<k])

goal (1 subgoal):
 1. \<And>k. \<lbrakk>\<lbrakk>k \<le> nrows A; mod_type_class.to_nat i < k\<rbrakk> \<Longrightarrow> is_zero_row i (Hermite_of_upt_row_i A k ass res); Suc k \<le> nrows A; mod_type_class.to_nat i < Suc k\<rbrakk> \<Longrightarrow> is_zero_row i (Hermite_of_upt_row_i A (Suc k) ass res)
[PROOF STEP]
have A'_def2: "A' = Hermite_of_upt_row_i A k ass res"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A' = Hermite_of_upt_row_i A k ass res
[PROOF STEP]
unfolding Hermite_of_upt_row_i_def A'_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. foldl (Hermite_of_row_i ass res) A (map mod_type_class.from_nat [0..<k]) = foldl (Hermite_of_row_i ass res) A (map mod_type_class.from_nat [0..<k])
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
A' = Hermite_of_upt_row_i A k ass res

goal (1 subgoal):
 1. \<And>k. \<lbrakk>\<lbrakk>k \<le> nrows A; mod_type_class.to_nat i < k\<rbrakk> \<Longrightarrow> is_zero_row i (Hermite_of_upt_row_i A k ass res); Suc k \<le> nrows A; mod_type_class.to_nat i < Suc k\<rbrakk> \<Longrightarrow> is_zero_row i (Hermite_of_upt_row_i A (Suc k) ass res)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_zero_row i (Hermite_of_upt_row_i A (Suc k) ass res)
[PROOF STEP]
unfolding is_zero_row_def'
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>j. Hermite_of_upt_row_i A (Suc k) ass res $ i $ j = (0::'a)
[PROOF STEP]
proof (clarify, cases "to_nat i = k")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>j. mod_type_class.to_nat i = k \<Longrightarrow> Hermite_of_upt_row_i A (Suc k) ass res $ i $ j = (0::'a)
 2. \<And>j. mod_type_class.to_nat i \<noteq> k \<Longrightarrow> Hermite_of_upt_row_i A (Suc k) ass res $ i $ j = (0::'a)
[PROOF STEP]
fix j
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>j. mod_type_class.to_nat i = k \<Longrightarrow> Hermite_of_upt_row_i A (Suc k) ass res $ i $ j = (0::'a)
 2. \<And>j. mod_type_class.to_nat i \<noteq> k \<Longrightarrow> Hermite_of_upt_row_i A (Suc k) ass res $ i $ j = (0::'a)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
mod_type_class.to_nat i = k

goal (2 subgoals):
 1. \<And>j. mod_type_class.to_nat i = k \<Longrightarrow> Hermite_of_upt_row_i A (Suc k) ass res $ i $ j = (0::'a)
 2. \<And>j. mod_type_class.to_nat i \<noteq> k \<Longrightarrow> Hermite_of_upt_row_i A (Suc k) ass res $ i $ j = (0::'a)
[PROOF STEP]
have fn_k_i: "from_nat k = i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mod_type_class.from_nat k = i
[PROOF STEP]
by (metis True from_nat_to_nat_id)
[PROOF STATE]
proof (state)
this:
mod_type_class.from_nat k = i

goal (2 subgoals):
 1. \<And>j. mod_type_class.to_nat i = k \<Longrightarrow> Hermite_of_upt_row_i A (Suc k) ass res $ i $ j = (0::'a)
 2. \<And>j. mod_type_class.to_nat i \<noteq> k \<Longrightarrow> Hermite_of_upt_row_i A (Suc k) ass res $ i $ j = (0::'a)
[PROOF STEP]
have "(Hermite_of_upt_row_i A (Suc k) ass res) =
        (Hermite_of_row_i ass res A' i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Hermite_of_upt_row_i A (Suc k) ass res = Hermite_of_row_i ass res A' i
[PROOF STEP]
unfolding Hermite_of_upt_row_i_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. foldl (Hermite_of_row_i ass res) A (map mod_type_class.from_nat [0..<Suc k]) = Hermite_of_row_i ass res A' i
[PROOF STEP]
by (simp add: A'_def fn_k_i)
[PROOF STATE]
proof (state)
this:
Hermite_of_upt_row_i A (Suc k) ass res = Hermite_of_row_i ass res A' i

goal (2 subgoals):
 1. \<And>j. mod_type_class.to_nat i = k \<Longrightarrow> Hermite_of_upt_row_i A (Suc k) ass res $ i $ j = (0::'a)
 2. \<And>j. mod_type_class.to_nat i \<noteq> k \<Longrightarrow> Hermite_of_upt_row_i A (Suc k) ass res $ i $ j = (0::'a)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
Hermite_of_upt_row_i A (Suc k) ass res = Hermite_of_row_i ass res A' i

goal (2 subgoals):
 1. \<And>j. mod_type_class.to_nat i = k \<Longrightarrow> Hermite_of_upt_row_i A (Suc k) ass res $ i $ j = (0::'a)
 2. \<And>j. mod_type_class.to_nat i \<noteq> k \<Longrightarrow> Hermite_of_upt_row_i A (Suc k) ass res $ i $ j = (0::'a)
[PROOF STEP]
have "is_zero_row i (Hermite_of_upt_row_i A k ass res)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_zero_row i (Hermite_of_upt_row_i A k ass res)
[PROOF STEP]
by (rule Hermite_of_upt_row_preserves_zero_rows_ge[OF i k], simp add: True)
[PROOF STATE]
proof (state)
this:
is_zero_row i (Hermite_of_upt_row_i A k ass res)

goal (2 subgoals):
 1. \<And>j. mod_type_class.to_nat i = k \<Longrightarrow> Hermite_of_upt_row_i A (Suc k) ass res $ i $ j = (0::'a)
 2. \<And>j. mod_type_class.to_nat i \<noteq> k \<Longrightarrow> Hermite_of_upt_row_i A (Suc k) ass res $ i $ j = (0::'a)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
Hermite_of_upt_row_i A (Suc k) ass res = Hermite_of_row_i ass res A' i
is_zero_row i (Hermite_of_upt_row_i A k ass res)
[PROOF STEP]
show "(Hermite_of_upt_row_i A (Suc k) ass res) $ i $ j = 0"
[PROOF STATE]
proof (prove)
using this:
Hermite_of_upt_row_i A (Suc k) ass res = Hermite_of_row_i ass res A' i
is_zero_row i (Hermite_of_upt_row_i A k ass res)

goal (1 subgoal):
 1. Hermite_of_upt_row_i A (Suc k) ass res $ i $ j = (0::'a)
[PROOF STEP]
unfolding is_zero_row_def' A'_def2 Hermite_of_row_i_def
[PROOF STATE]
proof (prove)
using this:
Hermite_of_upt_row_i A (Suc k) ass res = (if \<forall>j. Hermite_of_upt_row_i A k ass res $ i $ j = (0::'a) then Hermite_of_upt_row_i A k ass res else let j = LEAST n. Hermite_of_upt_row_i A k ass res $ i $ n \<noteq> (0::'a); Aij = Hermite_of_upt_row_i A k ass res $ i $ j; A' = mult_row (Hermite_of_upt_row_i A k ass res) i (ass Aij div Aij) in Hermite_reduce_above A' (mod_type_class.to_nat i) i j res)
\<forall>j. Hermite_of_upt_row_i A k ass res $ i $ j = (0::'a)

goal (1 subgoal):
 1. Hermite_of_upt_row_i A (Suc k) ass res $ i $ j = (0::'a)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Hermite_of_upt_row_i A (Suc k) ass res $ i $ j = (0::'a)

goal (1 subgoal):
 1. \<And>j. mod_type_class.to_nat i \<noteq> k \<Longrightarrow> Hermite_of_upt_row_i A (Suc k) ass res $ i $ j = (0::'a)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>j. mod_type_class.to_nat i \<noteq> k \<Longrightarrow> Hermite_of_upt_row_i A (Suc k) ass res $ i $ j = (0::'a)
[PROOF STEP]
fix j
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>j. mod_type_class.to_nat i \<noteq> k \<Longrightarrow> Hermite_of_upt_row_i A (Suc k) ass res $ i $ j = (0::'a)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
mod_type_class.to_nat i \<noteq> k

goal (1 subgoal):
 1. \<And>j. mod_type_class.to_nat i \<noteq> k \<Longrightarrow> Hermite_of_upt_row_i A (Suc k) ass res $ i $ j = (0::'a)
[PROOF STEP]
hence i_less_k: "to_nat i < k"
[PROOF STATE]
proof (prove)
using this:
mod_type_class.to_nat i \<noteq> k

goal (1 subgoal):
 1. mod_type_class.to_nat i < k
[PROOF STEP]
using Suc.prems
[PROOF STATE]
proof (prove)
using this:
mod_type_class.to_nat i \<noteq> k
Suc k \<le> nrows A
mod_type_class.to_nat i < Suc k

goal (1 subgoal):
 1. mod_type_class.to_nat i < k
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
mod_type_class.to_nat i < k

goal (1 subgoal):
 1. \<And>j. mod_type_class.to_nat i \<noteq> k \<Longrightarrow> Hermite_of_upt_row_i A (Suc k) ass res $ i $ j = (0::'a)
[PROOF STEP]
hence i_less_k2: "i < from_nat k"
[PROOF STATE]
proof (prove)
using this:
mod_type_class.to_nat i < k

goal (1 subgoal):
 1. i < mod_type_class.from_nat k
[PROOF STEP]
using Suc.prems
[PROOF STATE]
proof (prove)
using this:
mod_type_class.to_nat i < k
Suc k \<le> nrows A
mod_type_class.to_nat i < Suc k

goal (1 subgoal):
 1. i < mod_type_class.from_nat k
[PROOF STEP]
by (metis from_nat_mono from_nat_to_nat_id k2 nrows_def)
[PROOF STATE]
proof (state)
this:
i < mod_type_class.from_nat k

goal (1 subgoal):
 1. \<And>j. mod_type_class.to_nat i \<noteq> k \<Longrightarrow> Hermite_of_upt_row_i A (Suc k) ass res $ i $ j = (0::'a)
[PROOF STEP]
show "(Hermite_of_upt_row_i A (Suc k) ass res) $ i $ j = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Hermite_of_upt_row_i A (Suc k) ass res $ i $ j = (0::'a)
[PROOF STEP]
proof (cases "is_zero_row (from_nat k) A'")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. is_zero_row (mod_type_class.from_nat k) A' \<Longrightarrow> Hermite_of_upt_row_i A (Suc k) ass res $ i $ j = (0::'a)
 2. \<not> is_zero_row (mod_type_class.from_nat k) A' \<Longrightarrow> Hermite_of_upt_row_i A (Suc k) ass res $ i $ j = (0::'a)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
is_zero_row (mod_type_class.from_nat k) A'

goal (2 subgoals):
 1. is_zero_row (mod_type_class.from_nat k) A' \<Longrightarrow> Hermite_of_upt_row_i A (Suc k) ass res $ i $ j = (0::'a)
 2. \<not> is_zero_row (mod_type_class.from_nat k) A' \<Longrightarrow> Hermite_of_upt_row_i A (Suc k) ass res $ i $ j = (0::'a)
[PROOF STEP]
have "is_zero_row i (Hermite_of_upt_row_i A k ass res)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_zero_row i (Hermite_of_upt_row_i A k ass res)
[PROOF STEP]
by (metis Suc.hyps i_less_k k)
[PROOF STATE]
proof (state)
this:
is_zero_row i (Hermite_of_upt_row_i A k ass res)

goal (2 subgoals):
 1. is_zero_row (mod_type_class.from_nat k) A' \<Longrightarrow> Hermite_of_upt_row_i A (Suc k) ass res $ i $ j = (0::'a)
 2. \<not> is_zero_row (mod_type_class.from_nat k) A' \<Longrightarrow> Hermite_of_upt_row_i A (Suc k) ass res $ i $ j = (0::'a)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
is_zero_row i (Hermite_of_upt_row_i A k ass res)

goal (2 subgoals):
 1. is_zero_row (mod_type_class.from_nat k) A' \<Longrightarrow> Hermite_of_upt_row_i A (Suc k) ass res $ i $ j = (0::'a)
 2. \<not> is_zero_row (mod_type_class.from_nat k) A' \<Longrightarrow> Hermite_of_upt_row_i A (Suc k) ass res $ i $ j = (0::'a)
[PROOF STEP]
have "Hermite_of_upt_row_i A (Suc k) ass res $ i $ j = Hermite_of_upt_row_i A k ass res $ i $ j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Hermite_of_upt_row_i A (Suc k) ass res $ i $ j = Hermite_of_upt_row_i A k ass res $ i $ j
[PROOF STEP]
using True
[PROOF STATE]
proof (prove)
using this:
is_zero_row (mod_type_class.from_nat k) A'

goal (1 subgoal):
 1. Hermite_of_upt_row_i A (Suc k) ass res $ i $ j = Hermite_of_upt_row_i A k ass res $ i $ j
[PROOF STEP]
by (simp add:  Hermite_of_upt_row_i_def Hermite_of_row_i_def A'_def Let_def)
[PROOF STATE]
proof (state)
this:
Hermite_of_upt_row_i A (Suc k) ass res $ i $ j = Hermite_of_upt_row_i A k ass res $ i $ j

goal (2 subgoals):
 1. is_zero_row (mod_type_class.from_nat k) A' \<Longrightarrow> Hermite_of_upt_row_i A (Suc k) ass res $ i $ j = (0::'a)
 2. \<not> is_zero_row (mod_type_class.from_nat k) A' \<Longrightarrow> Hermite_of_upt_row_i A (Suc k) ass res $ i $ j = (0::'a)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
is_zero_row i (Hermite_of_upt_row_i A k ass res)
Hermite_of_upt_row_i A (Suc k) ass res $ i $ j = Hermite_of_upt_row_i A k ass res $ i $ j
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
is_zero_row i (Hermite_of_upt_row_i A k ass res)
Hermite_of_upt_row_i A (Suc k) ass res $ i $ j = Hermite_of_upt_row_i A k ass res $ i $ j

goal (1 subgoal):
 1. Hermite_of_upt_row_i A (Suc k) ass res $ i $ j = (0::'a)
[PROOF STEP]
unfolding is_zero_row_def'
[PROOF STATE]
proof (prove)
using this:
\<forall>j. Hermite_of_upt_row_i A k ass res $ i $ j = (0::'a)
Hermite_of_upt_row_i A (Suc k) ass res $ i $ j = Hermite_of_upt_row_i A k ass res $ i $ j

goal (1 subgoal):
 1. Hermite_of_upt_row_i A (Suc k) ass res $ i $ j = (0::'a)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Hermite_of_upt_row_i A (Suc k) ass res $ i $ j = (0::'a)

goal (1 subgoal):
 1. \<not> is_zero_row (mod_type_class.from_nat k) A' \<Longrightarrow> Hermite_of_upt_row_i A (Suc k) ass res $ i $ j = (0::'a)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> is_zero_row (mod_type_class.from_nat k) A' \<Longrightarrow> Hermite_of_upt_row_i A (Suc k) ass res $ i $ j = (0::'a)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> is_zero_row (mod_type_class.from_nat k) A'

goal (1 subgoal):
 1. \<not> is_zero_row (mod_type_class.from_nat k) A' \<Longrightarrow> Hermite_of_upt_row_i A (Suc k) ass res $ i $ j = (0::'a)
[PROOF STEP]
have "is_zero_row i (Hermite_of_upt_row_i A k ass res)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_zero_row i (Hermite_of_upt_row_i A k ass res)
[PROOF STEP]
by (metis Suc.hyps i_less_k k)
[PROOF STATE]
proof (state)
this:
is_zero_row i (Hermite_of_upt_row_i A k ass res)

goal (1 subgoal):
 1. \<not> is_zero_row (mod_type_class.from_nat k) A' \<Longrightarrow> Hermite_of_upt_row_i A (Suc k) ass res $ i $ j = (0::'a)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
is_zero_row i (Hermite_of_upt_row_i A k ass res)

goal (1 subgoal):
 1. \<not> is_zero_row (mod_type_class.from_nat k) A' \<Longrightarrow> Hermite_of_upt_row_i A (Suc k) ass res $ i $ j = (0::'a)
[PROOF STEP]
have "\<not> is_zero_row i (Hermite_of_upt_row_i A k ass res)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> is_zero_row i (Hermite_of_upt_row_i A k ass res)
[PROOF STEP]
using echelon_form_condition1
[PROOF STATE]
proof (prove)
using this:
echelon_form ?A \<Longrightarrow> \<forall>i. is_zero_row i ?A \<longrightarrow> \<not> (\<exists>j>i. \<not> is_zero_row j ?A)

goal (1 subgoal):
 1. \<not> is_zero_row i (Hermite_of_upt_row_i A k ass res)
[PROOF STEP]
by (metis A'_def2 False e a r echelon_form_Hermite_of_upt_row_i i_less_k2)
[PROOF STATE]
proof (state)
this:
\<not> is_zero_row i (Hermite_of_upt_row_i A k ass res)

goal (1 subgoal):
 1. \<not> is_zero_row (mod_type_class.from_nat k) A' \<Longrightarrow> Hermite_of_upt_row_i A (Suc k) ass res $ i $ j = (0::'a)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
is_zero_row i (Hermite_of_upt_row_i A k ass res)
\<not> is_zero_row i (Hermite_of_upt_row_i A k ass res)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
is_zero_row i (Hermite_of_upt_row_i A k ass res)
\<not> is_zero_row i (Hermite_of_upt_row_i A k ass res)

goal (1 subgoal):
 1. Hermite_of_upt_row_i A (Suc k) ass res $ i $ j = (0::'a)
[PROOF STEP]
by contradiction
[PROOF STATE]
proof (state)
this:
Hermite_of_upt_row_i A (Suc k) ass res $ i $ j = (0::'a)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
Hermite_of_upt_row_i A (Suc k) ass res $ i $ j = (0::'a)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
is_zero_row i (Hermite_of_upt_row_i A (Suc k) ass res)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
is_zero_row i (Hermite_of_upt_row_i A k ass res)

goal:
No subgoals!
[PROOF STEP]
qed