[STATEMENT]
lemma step_eps_dest: "step_eps bs q q' \<Longrightarrow> q \<in> SQ"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. step_eps bs q q' \<Longrightarrow> q \<in> SQ
[PROOF STEP]
by (auto simp add: step_eps_def)


[STATEMENT]
lemma step_symb_closed: "step_symb q q' \<Longrightarrow> q' \<in> Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. step_symb q q' \<Longrightarrow> q' \<in> Q
[PROOF STEP]
using transs_q_in_set state_closed
[PROOF STATE]
proof (prove)
using this:
?q \<in> NFA.SQ ?q0.0 ?transs \<Longrightarrow> ?transs ! (?q - ?q0.0) \<in> set ?transs
?t \<in> set transs \<Longrightarrow> state_set ?t \<subseteq> Q

goal (1 subgoal):
 1. step_symb q q' \<Longrightarrow> q' \<in> Q
[PROOF STEP]
by (fastforce simp add: NFA.step_symb_def split: transition.splits)


[STATEMENT]
lemma recvupd_preserves_GlobVacantUpto:
  assumes "GlobVacantUpto c0 q t"
    and   "next_recvupd' c0 c1 p q"
    and   "InvInfoJustifiedWithGII c0"
    and   "InvGlobNonposEqVacant c1"
    and   "InvGlobVacantImpRecordsVacant c0"
    and   "InvRecordCount c0"
  shows   "GlobVacantUpto c1 q t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. GlobVacantUpto c1 q t
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> GlobVacantUpto c1 q t \<Longrightarrow> False
[PROOF STEP]
note npeq1 = assms(4)[unfolded InvGlobNonposEqVacant_def, rule_format]
[PROOF STATE]
proof (state)
this:
GlobVacantUpto c1 ?q ?t = GlobNonposUpto c1 ?q ?t

goal (1 subgoal):
 1. \<not> GlobVacantUpto c1 q t \<Longrightarrow> False
[PROOF STEP]
note gvu0 = assms(1)[unfolded vacant_upto_def, rule_format]
[PROOF STATE]
proof (state)
this:
?s \<le> t \<Longrightarrow> zcount (c_glob c0 q) ?s = 0

goal (1 subgoal):
 1. \<not> GlobVacantUpto c1 q t \<Longrightarrow> False
[PROOF STEP]
note nvu0 = assms(5)[unfolded InvGlobVacantImpRecordsVacant_def, rule_format, OF assms(1)]
[PROOF STATE]
proof (state)
this:
RecordsVacantUpto c0 t

goal (1 subgoal):
 1. \<not> GlobVacantUpto c1 q t \<Longrightarrow> False
[PROOF STEP]
note recordcount = assms(6)[unfolded InvRecordCount_def zmultiset_eq_iff zcount_union, rule_format]
[PROOF STATE]
proof (state)
this:
zcount (records c0) ?a = zcount (GlobalIncomingInfoAt c0 ?q) ?a + zcount (c_glob c0 ?q) ?a

goal (1 subgoal):
 1. \<not> GlobVacantUpto c1 q t \<Longrightarrow> False
[PROOF STEP]
note change = next_recvupdD[OF assms(2)]
[PROOF STATE]
proof (state)
this:
c_msg c0 p q \<noteq> []
c_temp c1 = c_temp c0
c_msg c1 = (\<lambda>p' q'. if p' = p \<and> q' = q then tl (c_msg c0 p q) else c_msg c0 p' q')
c_glob c1 = (c_glob c0)(q := c_glob c0 q + hd (c_msg c0 p q))
c_caps c1 = c_caps c0
c_data_msg c1 = c_data_msg c0

goal (1 subgoal):
 1. \<not> GlobVacantUpto c1 q t \<Longrightarrow> False
[PROOF STEP]
let ?\<kappa> = "hd (c_msg c0 p q)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> GlobVacantUpto c1 q t \<Longrightarrow> False
[PROOF STEP]
from change(1)
[PROOF STATE]
proof (chain)
picking this:
c_msg c0 p q \<noteq> []
[PROOF STEP]
have ia\<kappa>: "?\<kappa> = InfoAt c0 0 p q"
[PROOF STATE]
proof (prove)
using this:
c_msg c0 p q \<noteq> []

goal (1 subgoal):
 1. hd (c_msg c0 p q) = InfoAt c0 0 p q
[PROOF STEP]
unfolding InfoAt_def
[PROOF STATE]
proof (prove)
using this:
c_msg c0 p q \<noteq> []

goal (1 subgoal):
 1. hd (c_msg c0 p q) = (if 0 \<le> 0 \<and> 0 < length (c_msg c0 p q) then c_msg c0 p q ! 0 else {#}\<^sub>z)
[PROOF STEP]
by (simp add: hd_conv_nth)
[PROOF STATE]
proof (state)
this:
hd (c_msg c0 p q) = InfoAt c0 0 p q

goal (1 subgoal):
 1. \<not> GlobVacantUpto c1 q t \<Longrightarrow> False
[PROOF STEP]
assume gvu1: "\<not> GlobVacantUpto c1 q t"
[PROOF STATE]
proof (state)
this:
\<not> GlobVacantUpto c1 q t

goal (1 subgoal):
 1. \<not> GlobVacantUpto c1 q t \<Longrightarrow> False
[PROOF STEP]
obtain t' where t':
    "t' \<le> t"
    "0 < zcount (c_glob c1 q) t'"
    "zcount (c_glob c0 q) t' = 0"
    "\<forall>s<t'. zcount (c_glob c1 q) s \<le> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>t'. \<lbrakk>t' \<le> t; 0 < zcount (c_glob c1 q) t'; zcount (c_glob c0 q) t' = 0; \<forall>s<t'. zcount (c_glob c1 q) s \<le> 0\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
apply atomize_elim
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>t'\<le>t. 0 < zcount (c_glob c1 q) t' \<and> zcount (c_glob c0 q) t' = 0 \<and> (\<forall>s<t'. zcount (c_glob c1 q) s \<le> 0)
[PROOF STEP]
using gvu1
[PROOF STATE]
proof (prove)
using this:
\<not> GlobVacantUpto c1 q t

goal (1 subgoal):
 1. \<exists>t'\<le>t. 0 < zcount (c_glob c1 q) t' \<and> zcount (c_glob c0 q) t' = 0 \<and> (\<forall>s<t'. zcount (c_glob c1 q) s \<le> 0)
[PROOF STEP]
unfolding npeq1 nonpos_upto_def
[PROOF STATE]
proof (prove)
using this:
\<not> (\<forall>s\<le>t. zcount (c_glob c1 q) s \<le> 0)

goal (1 subgoal):
 1. \<exists>t'\<le>t. 0 < zcount (c_glob c1 q) t' \<and> zcount (c_glob c0 q) t' = 0 \<and> (\<forall>s<t'. zcount (c_glob c1 q) s \<le> 0)
[PROOF STEP]
apply (simp add: not_le)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>s\<le>t. 0 < zcount (c_glob c1 q) s \<Longrightarrow> \<exists>t'\<le>t. 0 < zcount (c_glob c1 q) t' \<and> zcount (c_glob c0 q) t' = 0 \<and> (\<forall>s<t'. zcount (c_glob c1 q) s \<le> 0)
[PROOF STEP]
apply (elim exE conjE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>s \<le> t; 0 < zcount (c_glob c1 q) s\<rbrakk> \<Longrightarrow> \<exists>t'\<le>t. 0 < zcount (c_glob c1 q) t' \<and> zcount (c_glob c0 q) t' = 0 \<and> (\<forall>s<t'. zcount (c_glob c1 q) s \<le> 0)
[PROOF STEP]
apply (drule order_zmset_exists_foundation')
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>s \<le> t; \<exists>sa\<le>s. 0 < zcount (c_glob c1 q) sa \<and> (\<forall>u<sa. zcount (c_glob c1 q) u \<le> 0)\<rbrakk> \<Longrightarrow> \<exists>t'\<le>t. 0 < zcount (c_glob c1 q) t' \<and> zcount (c_glob c0 q) t' = 0 \<and> (\<forall>s<t'. zcount (c_glob c1 q) s \<le> 0)
[PROOF STEP]
apply (elim exE conjE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s sa. \<lbrakk>s \<le> t; sa \<le> s; 0 < zcount (c_glob c1 q) sa; \<forall>u<sa. zcount (c_glob c1 q) u \<le> 0\<rbrakk> \<Longrightarrow> \<exists>t'\<le>t. 0 < zcount (c_glob c1 q) t' \<and> zcount (c_glob c0 q) t' = 0 \<and> (\<forall>s<t'. zcount (c_glob c1 q) s \<le> 0)
[PROOF STEP]
subgoal for s s'
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>s \<le> t; s' \<le> s; 0 < zcount (c_glob c1 q) s'; \<forall>u<s'. zcount (c_glob c1 q) u \<le> 0\<rbrakk> \<Longrightarrow> \<exists>t'\<le>t. 0 < zcount (c_glob c1 q) t' \<and> zcount (c_glob c0 q) t' = 0 \<and> (\<forall>s<t'. zcount (c_glob c1 q) s \<le> 0)
[PROOF STEP]
apply (rule exI[of _ s'])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>s \<le> t; s' \<le> s; 0 < zcount (c_glob c1 q) s'; \<forall>u<s'. zcount (c_glob c1 q) u \<le> 0\<rbrakk> \<Longrightarrow> s' \<le> t \<and> 0 < zcount (c_glob c1 q) s' \<and> zcount (c_glob c0 q) s' = 0 \<and> (\<forall>s<s'. zcount (c_glob c1 q) s \<le> 0)
[PROOF STEP]
using gvu0
[PROOF STATE]
proof (prove)
using this:
?s \<le> t \<Longrightarrow> zcount (c_glob c0 q) ?s = 0

goal (1 subgoal):
 1. \<lbrakk>s \<le> t; s' \<le> s; 0 < zcount (c_glob c1 q) s'; \<forall>u<s'. zcount (c_glob c1 q) u \<le> 0\<rbrakk> \<Longrightarrow> s' \<le> t \<and> 0 < zcount (c_glob c1 q) s' \<and> zcount (c_glob c0 q) s' = 0 \<and> (\<forall>s<s'. zcount (c_glob c1 q) s \<le> 0)
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
t' \<le> t
0 < zcount (c_glob c1 q) t'
zcount (c_glob c0 q) t' = 0
\<forall>s<t'. zcount (c_glob c1 q) s \<le> 0

goal (1 subgoal):
 1. \<not> GlobVacantUpto c1 q t \<Longrightarrow> False
[PROOF STEP]
from t'(2,3)
[PROOF STATE]
proof (chain)
picking this:
0 < zcount (c_glob c1 q) t'
zcount (c_glob c0 q) t' = 0
[PROOF STEP]
have count\<kappa>: "0 < zcount ?\<kappa> t'"
[PROOF STATE]
proof (prove)
using this:
0 < zcount (c_glob c1 q) t'
zcount (c_glob c0 q) t' = 0

goal (1 subgoal):
 1. 0 < zcount (hd (c_msg c0 p q)) t'
[PROOF STEP]
by (auto simp: change(4))
[PROOF STATE]
proof (state)
this:
0 < zcount (hd (c_msg c0 p q)) t'

goal (1 subgoal):
 1. \<not> GlobVacantUpto c1 q t \<Longrightarrow> False
[PROOF STEP]
note assms(3)[unfolded InvInfoJustifiedWithGII_def justified_with_alt, rule_format, OF count\<kappa>[unfolded ia\<kappa>]]
[PROOF STATE]
proof (state)
this:
(\<exists>s<t'. (zcount (InfoAt c0 0 p q) s < 0 \<or> zcount (GlobalIncomingInfo c0 (0 + 1) p q) s < 0) \<and> (\<forall>s'<s. zcount (InfoAt c0 0 p q) s' \<le> 0)) \<or> (\<exists>s<t'. 0 < zcount (records c0) s) \<or> zcount (InfoAt c0 0 p q + GlobalIncomingInfo c0 (0 + 1) p q) t' < zcount (records c0) t'

goal (1 subgoal):
 1. \<not> GlobVacantUpto c1 q t \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(\<exists>s<t'. (zcount (InfoAt c0 0 p q) s < 0 \<or> zcount (GlobalIncomingInfo c0 (0 + 1) p q) s < 0) \<and> (\<forall>s'<s. zcount (InfoAt c0 0 p q) s' \<le> 0)) \<or> (\<exists>s<t'. 0 < zcount (records c0) s) \<or> zcount (InfoAt c0 0 p q + GlobalIncomingInfo c0 (0 + 1) p q) t' < zcount (records c0) t'
[PROOF STEP]
consider
    "\<exists>s<t'. zcount (InfoAt c0 0 p q) s < 0 \<and> (\<forall>s'<s. zcount (InfoAt c0 0 p q) s' \<le> 0)" |
    "\<exists>s<t'. zcount (GlobalIncomingInfo c0 1 p q) s < 0 \<and> (\<forall>s'<s. zcount (InfoAt c0 0 p q) s' \<le> 0)"
    "\<nexists>s. s < t' \<and> zcount (InfoAt c0 0 p q) s < 0 \<and> (\<forall>s'<s. zcount (InfoAt c0 0 p q) s' \<le> 0)" |
    "\<exists>s<t'. 0 < zcount (records c0) s" |
    "zcount (InfoAt c0 0 p q + GlobalIncomingInfo c0 1 p q) t' < zcount (records c0) t'"
[PROOF STATE]
proof (prove)
using this:
(\<exists>s<t'. (zcount (InfoAt c0 0 p q) s < 0 \<or> zcount (GlobalIncomingInfo c0 (0 + 1) p q) s < 0) \<and> (\<forall>s'<s. zcount (InfoAt c0 0 p q) s' \<le> 0)) \<or> (\<exists>s<t'. 0 < zcount (records c0) s) \<or> zcount (InfoAt c0 0 p q + GlobalIncomingInfo c0 (0 + 1) p q) t' < zcount (records c0) t'

goal (1 subgoal):
 1. \<lbrakk>\<exists>s<t'. zcount (InfoAt c0 0 p q) s < 0 \<and> (\<forall>s'<s. zcount (InfoAt c0 0 p q) s' \<le> 0) \<Longrightarrow> thesis; \<lbrakk>\<exists>s<t'. zcount (GlobalIncomingInfo c0 1 p q) s < 0 \<and> (\<forall>s'<s. zcount (InfoAt c0 0 p q) s' \<le> 0); \<not> (\<exists>s<t'. zcount (InfoAt c0 0 p q) s < 0 \<and> (\<forall>s'<s. zcount (InfoAt c0 0 p q) s' \<le> 0))\<rbrakk> \<Longrightarrow> thesis; \<exists>s<t'. 0 < zcount (records c0) s \<Longrightarrow> thesis; zcount (InfoAt c0 0 p q + GlobalIncomingInfo c0 1 p q) t' < zcount (records c0) t' \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by atomize_elim auto
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<exists>s<t'. zcount (InfoAt c0 0 p q) s < 0 \<and> (\<forall>s'<s. zcount (InfoAt c0 0 p q) s' \<le> 0) \<Longrightarrow> ?thesis; \<lbrakk>\<exists>s<t'. zcount (GlobalIncomingInfo c0 1 p q) s < 0 \<and> (\<forall>s'<s. zcount (InfoAt c0 0 p q) s' \<le> 0); \<not> (\<exists>s<t'. zcount (InfoAt c0 0 p q) s < 0 \<and> (\<forall>s'<s. zcount (InfoAt c0 0 p q) s' \<le> 0))\<rbrakk> \<Longrightarrow> ?thesis; \<exists>s<t'. 0 < zcount (records c0) s \<Longrightarrow> ?thesis; zcount (InfoAt c0 0 p q + GlobalIncomingInfo c0 1 p q) t' < zcount (records c0) t' \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. \<not> GlobVacantUpto c1 q t \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>\<exists>s<t'. zcount (InfoAt c0 0 p q) s < 0 \<and> (\<forall>s'<s. zcount (InfoAt c0 0 p q) s' \<le> 0) \<Longrightarrow> ?thesis; \<lbrakk>\<exists>s<t'. zcount (GlobalIncomingInfo c0 1 p q) s < 0 \<and> (\<forall>s'<s. zcount (InfoAt c0 0 p q) s' \<le> 0); \<not> (\<exists>s<t'. zcount (InfoAt c0 0 p q) s < 0 \<and> (\<forall>s'<s. zcount (InfoAt c0 0 p q) s' \<le> 0))\<rbrakk> \<Longrightarrow> ?thesis; \<exists>s<t'. 0 < zcount (records c0) s \<Longrightarrow> ?thesis; zcount (InfoAt c0 0 p q + GlobalIncomingInfo c0 1 p q) t' < zcount (records c0) t' \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<exists>s<t'. zcount (InfoAt c0 0 p q) s < 0 \<and> (\<forall>s'<s. zcount (InfoAt c0 0 p q) s' \<le> 0) \<Longrightarrow> ?thesis; \<lbrakk>\<exists>s<t'. zcount (GlobalIncomingInfo c0 1 p q) s < 0 \<and> (\<forall>s'<s. zcount (InfoAt c0 0 p q) s' \<le> 0); \<not> (\<exists>s<t'. zcount (InfoAt c0 0 p q) s < 0 \<and> (\<forall>s'<s. zcount (InfoAt c0 0 p q) s' \<le> 0))\<rbrakk> \<Longrightarrow> ?thesis; \<exists>s<t'. 0 < zcount (records c0) s \<Longrightarrow> ?thesis; zcount (InfoAt c0 0 p q + GlobalIncomingInfo c0 1 p q) t' < zcount (records c0) t' \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. False
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<exists>s<t'. zcount (InfoAt c0 0 p q) s < 0 \<and> (\<forall>s'<s. zcount (InfoAt c0 0 p q) s' \<le> 0) \<Longrightarrow> False
 2. \<lbrakk>\<exists>s<t'. zcount (GlobalIncomingInfo c0 1 p q) s < 0 \<and> (\<forall>s'<s. zcount (InfoAt c0 0 p q) s' \<le> 0); \<not> (\<exists>s<t'. zcount (InfoAt c0 0 p q) s < 0 \<and> (\<forall>s'<s. zcount (InfoAt c0 0 p q) s' \<le> 0))\<rbrakk> \<Longrightarrow> False
 3. \<exists>s<t'. 0 < zcount (records c0) s \<Longrightarrow> False
 4. zcount (InfoAt c0 0 p q + GlobalIncomingInfo c0 1 p q) t' < zcount (records c0) t' \<Longrightarrow> False
[PROOF STEP]
case 1
[PROOF STATE]
proof (state)
this:
\<exists>s<t'. zcount (InfoAt c0 0 p q) s < 0 \<and> (\<forall>s'<s. zcount (InfoAt c0 0 p q) s' \<le> 0)

goal (4 subgoals):
 1. \<exists>s<t'. zcount (InfoAt c0 0 p q) s < 0 \<and> (\<forall>s'<s. zcount (InfoAt c0 0 p q) s' \<le> 0) \<Longrightarrow> False
 2. \<lbrakk>\<exists>s<t'. zcount (GlobalIncomingInfo c0 1 p q) s < 0 \<and> (\<forall>s'<s. zcount (InfoAt c0 0 p q) s' \<le> 0); \<not> (\<exists>s<t'. zcount (InfoAt c0 0 p q) s < 0 \<and> (\<forall>s'<s. zcount (InfoAt c0 0 p q) s' \<le> 0))\<rbrakk> \<Longrightarrow> False
 3. \<exists>s<t'. 0 < zcount (records c0) s \<Longrightarrow> False
 4. zcount (InfoAt c0 0 p q + GlobalIncomingInfo c0 1 p q) t' < zcount (records c0) t' \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>s<t'. zcount (InfoAt c0 0 p q) s < 0 \<and> (\<forall>s'<s. zcount (InfoAt c0 0 p q) s' \<le> 0)
[PROOF STEP]
obtain s where s: "s < t'" "zcount (InfoAt c0 0 p q) s < 0" "\<forall>s'<s. zcount (InfoAt c0 0 p q) s' \<le> 0"
[PROOF STATE]
proof (prove)
using this:
\<exists>s<t'. zcount (InfoAt c0 0 p q) s < 0 \<and> (\<forall>s'<s. zcount (InfoAt c0 0 p q) s' \<le> 0)

goal (1 subgoal):
 1. (\<And>s. \<lbrakk>s < t'; zcount (InfoAt c0 0 p q) s < 0; \<forall>s'<s. zcount (InfoAt c0 0 p q) s' \<le> 0\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
s < t'
zcount (InfoAt c0 0 p q) s < 0
\<forall>s'<s. zcount (InfoAt c0 0 p q) s' \<le> 0

goal (4 subgoals):
 1. \<exists>s<t'. zcount (InfoAt c0 0 p q) s < 0 \<and> (\<forall>s'<s. zcount (InfoAt c0 0 p q) s' \<le> 0) \<Longrightarrow> False
 2. \<lbrakk>\<exists>s<t'. zcount (GlobalIncomingInfo c0 1 p q) s < 0 \<and> (\<forall>s'<s. zcount (InfoAt c0 0 p q) s' \<le> 0); \<not> (\<exists>s<t'. zcount (InfoAt c0 0 p q) s < 0 \<and> (\<forall>s'<s. zcount (InfoAt c0 0 p q) s' \<le> 0))\<rbrakk> \<Longrightarrow> False
 3. \<exists>s<t'. 0 < zcount (records c0) s \<Longrightarrow> False
 4. zcount (InfoAt c0 0 p q + GlobalIncomingInfo c0 1 p q) t' < zcount (records c0) t' \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
s < t'
zcount (InfoAt c0 0 p q) s < 0
\<forall>s'<s. zcount (InfoAt c0 0 p q) s' \<le> 0
[PROOF STEP]
have globs: "zcount (c_glob c1 q) s < 0"
[PROOF STATE]
proof (prove)
using this:
s < t'
zcount (InfoAt c0 0 p q) s < 0
\<forall>s'<s. zcount (InfoAt c0 0 p q) s' \<le> 0

goal (1 subgoal):
 1. zcount (c_glob c1 q) s < 0
[PROOF STEP]
using gvu0 ia\<kappa> t'(1)
[PROOF STATE]
proof (prove)
using this:
s < t'
zcount (InfoAt c0 0 p q) s < 0
\<forall>s'<s. zcount (InfoAt c0 0 p q) s' \<le> 0
?s \<le> t \<Longrightarrow> zcount (c_glob c0 q) ?s = 0
hd (c_msg c0 p q) = InfoAt c0 0 p q
t' \<le> t

goal (1 subgoal):
 1. zcount (c_glob c1 q) s < 0
[PROOF STEP]
by (auto simp: change(4))
[PROOF STATE]
proof (state)
this:
zcount (c_glob c1 q) s < 0

goal (4 subgoals):
 1. \<exists>s<t'. zcount (InfoAt c0 0 p q) s < 0 \<and> (\<forall>s'<s. zcount (InfoAt c0 0 p q) s' \<le> 0) \<Longrightarrow> False
 2. \<lbrakk>\<exists>s<t'. zcount (GlobalIncomingInfo c0 1 p q) s < 0 \<and> (\<forall>s'<s. zcount (InfoAt c0 0 p q) s' \<le> 0); \<not> (\<exists>s<t'. zcount (InfoAt c0 0 p q) s < 0 \<and> (\<forall>s'<s. zcount (InfoAt c0 0 p q) s' \<le> 0))\<rbrakk> \<Longrightarrow> False
 3. \<exists>s<t'. 0 < zcount (records c0) s \<Longrightarrow> False
 4. zcount (InfoAt c0 0 p q + GlobalIncomingInfo c0 1 p q) t' < zcount (records c0) t' \<Longrightarrow> False
[PROOF STEP]
have "zcount (c_glob c1 q) s \<le> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. zcount (c_glob c1 q) s \<le> 0
[PROOF STEP]
using globs
[PROOF STATE]
proof (prove)
using this:
zcount (c_glob c1 q) s < 0

goal (1 subgoal):
 1. zcount (c_glob c1 q) s \<le> 0
[PROOF STEP]
by linarith
[PROOF STATE]
proof (state)
this:
zcount (c_glob c1 q) s \<le> 0

goal (4 subgoals):
 1. \<exists>s<t'. zcount (InfoAt c0 0 p q) s < 0 \<and> (\<forall>s'<s. zcount (InfoAt c0 0 p q) s' \<le> 0) \<Longrightarrow> False
 2. \<lbrakk>\<exists>s<t'. zcount (GlobalIncomingInfo c0 1 p q) s < 0 \<and> (\<forall>s'<s. zcount (InfoAt c0 0 p q) s' \<le> 0); \<not> (\<exists>s<t'. zcount (InfoAt c0 0 p q) s < 0 \<and> (\<forall>s'<s. zcount (InfoAt c0 0 p q) s' \<le> 0))\<rbrakk> \<Longrightarrow> False
 3. \<exists>s<t'. 0 < zcount (records c0) s \<Longrightarrow> False
 4. zcount (InfoAt c0 0 p q + GlobalIncomingInfo c0 1 p q) t' < zcount (records c0) t' \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
zcount (c_glob c1 q) s \<le> 0
[PROOF STEP]
have "\<forall>s'\<le>s. zcount (c_glob c1 q) s' \<le> 0"
[PROOF STATE]
proof (prove)
using this:
zcount (c_glob c1 q) s \<le> 0

goal (1 subgoal):
 1. \<forall>s'\<le>s. zcount (c_glob c1 q) s' \<le> 0
[PROOF STEP]
using s(1) t'(4)
[PROOF STATE]
proof (prove)
using this:
zcount (c_glob c1 q) s \<le> 0
s < t'
\<forall>s<t'. zcount (c_glob c1 q) s \<le> 0

goal (1 subgoal):
 1. \<forall>s'\<le>s. zcount (c_glob c1 q) s' \<le> 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>s'\<le>s. zcount (c_glob c1 q) s' \<le> 0

goal (4 subgoals):
 1. \<exists>s<t'. zcount (InfoAt c0 0 p q) s < 0 \<and> (\<forall>s'<s. zcount (InfoAt c0 0 p q) s' \<le> 0) \<Longrightarrow> False
 2. \<lbrakk>\<exists>s<t'. zcount (GlobalIncomingInfo c0 1 p q) s < 0 \<and> (\<forall>s'<s. zcount (InfoAt c0 0 p q) s' \<le> 0); \<not> (\<exists>s<t'. zcount (InfoAt c0 0 p q) s < 0 \<and> (\<forall>s'<s. zcount (InfoAt c0 0 p q) s' \<le> 0))\<rbrakk> \<Longrightarrow> False
 3. \<exists>s<t'. 0 < zcount (records c0) s \<Longrightarrow> False
 4. zcount (InfoAt c0 0 p q + GlobalIncomingInfo c0 1 p q) t' < zcount (records c0) t' \<Longrightarrow> False
[PROOF STEP]
with globs
[PROOF STATE]
proof (chain)
picking this:
zcount (c_glob c1 q) s < 0
\<forall>s'\<le>s. zcount (c_glob c1 q) s' \<le> 0
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
zcount (c_glob c1 q) s < 0
\<forall>s'\<le>s. zcount (c_glob c1 q) s' \<le> 0

goal (1 subgoal):
 1. False
[PROOF STEP]
by (auto simp: npeq1[unfolded nonpos_upto_def, symmetric] vacant_upto_def)
[PROOF STATE]
proof (state)
this:
False

goal (3 subgoals):
 1. \<lbrakk>\<exists>s<t'. zcount (GlobalIncomingInfo c0 1 p q) s < 0 \<and> (\<forall>s'<s. zcount (InfoAt c0 0 p q) s' \<le> 0); \<not> (\<exists>s<t'. zcount (InfoAt c0 0 p q) s < 0 \<and> (\<forall>s'<s. zcount (InfoAt c0 0 p q) s' \<le> 0))\<rbrakk> \<Longrightarrow> False
 2. \<exists>s<t'. 0 < zcount (records c0) s \<Longrightarrow> False
 3. zcount (InfoAt c0 0 p q + GlobalIncomingInfo c0 1 p q) t' < zcount (records c0) t' \<Longrightarrow> False
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<lbrakk>\<exists>s<t'. zcount (GlobalIncomingInfo c0 1 p q) s < 0 \<and> (\<forall>s'<s. zcount (InfoAt c0 0 p q) s' \<le> 0); \<not> (\<exists>s<t'. zcount (InfoAt c0 0 p q) s < 0 \<and> (\<forall>s'<s. zcount (InfoAt c0 0 p q) s' \<le> 0))\<rbrakk> \<Longrightarrow> False
 2. \<exists>s<t'. 0 < zcount (records c0) s \<Longrightarrow> False
 3. zcount (InfoAt c0 0 p q + GlobalIncomingInfo c0 1 p q) t' < zcount (records c0) t' \<Longrightarrow> False
[PROOF STEP]
case 2
[PROOF STATE]
proof (state)
this:
\<exists>s<t'. zcount (GlobalIncomingInfo c0 1 p q) s < 0 \<and> (\<forall>s'<s. zcount (InfoAt c0 0 p q) s' \<le> 0)
\<not> (\<exists>s<t'. zcount (InfoAt c0 0 p q) s < 0 \<and> (\<forall>s'<s. zcount (InfoAt c0 0 p q) s' \<le> 0))

goal (3 subgoals):
 1. \<lbrakk>\<exists>s<t'. zcount (GlobalIncomingInfo c0 1 p q) s < 0 \<and> (\<forall>s'<s. zcount (InfoAt c0 0 p q) s' \<le> 0); \<not> (\<exists>s<t'. zcount (InfoAt c0 0 p q) s < 0 \<and> (\<forall>s'<s. zcount (InfoAt c0 0 p q) s' \<le> 0))\<rbrakk> \<Longrightarrow> False
 2. \<exists>s<t'. 0 < zcount (records c0) s \<Longrightarrow> False
 3. zcount (InfoAt c0 0 p q + GlobalIncomingInfo c0 1 p q) t' < zcount (records c0) t' \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>s<t'. zcount (GlobalIncomingInfo c0 1 p q) s < 0 \<and> (\<forall>s'<s. zcount (InfoAt c0 0 p q) s' \<le> 0)
\<not> (\<exists>s<t'. zcount (InfoAt c0 0 p q) s < 0 \<and> (\<forall>s'<s. zcount (InfoAt c0 0 p q) s' \<le> 0))
[PROOF STEP]
obtain s where s: "s < t'" "zcount (GlobalIncomingInfo c0 1 p q) s < 0" "\<forall>s'<s. zcount (InfoAt c0 0 p q) s' \<le> 0"
[PROOF STATE]
proof (prove)
using this:
\<exists>s<t'. zcount (GlobalIncomingInfo c0 1 p q) s < 0 \<and> (\<forall>s'<s. zcount (InfoAt c0 0 p q) s' \<le> 0)
\<not> (\<exists>s<t'. zcount (InfoAt c0 0 p q) s < 0 \<and> (\<forall>s'<s. zcount (InfoAt c0 0 p q) s' \<le> 0))

goal (1 subgoal):
 1. (\<And>s. \<lbrakk>s < t'; zcount (GlobalIncomingInfo c0 1 p q) s < 0; \<forall>s'<s. zcount (InfoAt c0 0 p q) s' \<le> 0\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
s < t'
zcount (GlobalIncomingInfo c0 1 p q) s < 0
\<forall>s'<s. zcount (InfoAt c0 0 p q) s' \<le> 0

goal (3 subgoals):
 1. \<lbrakk>\<exists>s<t'. zcount (GlobalIncomingInfo c0 1 p q) s < 0 \<and> (\<forall>s'<s. zcount (InfoAt c0 0 p q) s' \<le> 0); \<not> (\<exists>s<t'. zcount (InfoAt c0 0 p q) s < 0 \<and> (\<forall>s'<s. zcount (InfoAt c0 0 p q) s' \<le> 0))\<rbrakk> \<Longrightarrow> False
 2. \<exists>s<t'. 0 < zcount (records c0) s \<Longrightarrow> False
 3. zcount (InfoAt c0 0 p q + GlobalIncomingInfo c0 1 p q) t' < zcount (records c0) t' \<Longrightarrow> False
[PROOF STEP]
from 2(2) s(1,3)
[PROOF STATE]
proof (chain)
picking this:
\<not> (\<exists>s<t'. zcount (InfoAt c0 0 p q) s < 0 \<and> (\<forall>s'<s. zcount (InfoAt c0 0 p q) s' \<le> 0))
s < t'
\<forall>s'<s. zcount (InfoAt c0 0 p q) s' \<le> 0
[PROOF STEP]
have "zcount (InfoAt c0 0 p q) s \<ge> 0"
[PROOF STATE]
proof (prove)
using this:
\<not> (\<exists>s<t'. zcount (InfoAt c0 0 p q) s < 0 \<and> (\<forall>s'<s. zcount (InfoAt c0 0 p q) s' \<le> 0))
s < t'
\<forall>s'<s. zcount (InfoAt c0 0 p q) s' \<le> 0

goal (1 subgoal):
 1. 0 \<le> zcount (InfoAt c0 0 p q) s
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
0 \<le> zcount (InfoAt c0 0 p q) s

goal (3 subgoals):
 1. \<lbrakk>\<exists>s<t'. zcount (GlobalIncomingInfo c0 1 p q) s < 0 \<and> (\<forall>s'<s. zcount (InfoAt c0 0 p q) s' \<le> 0); \<not> (\<exists>s<t'. zcount (InfoAt c0 0 p q) s < 0 \<and> (\<forall>s'<s. zcount (InfoAt c0 0 p q) s' \<le> 0))\<rbrakk> \<Longrightarrow> False
 2. \<exists>s<t'. 0 < zcount (records c0) s \<Longrightarrow> False
 3. zcount (InfoAt c0 0 p q + GlobalIncomingInfo c0 1 p q) t' < zcount (records c0) t' \<Longrightarrow> False
[PROOF STEP]
have rc: "zcount (records c0) s = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. zcount (records c0) s = 0
[PROOF STEP]
using order.strict_implies_order order.strict_trans2 nvu0 s(1) t'(1) vacant_upto_def
[PROOF STATE]
proof (prove)
using this:
?a < ?b \<Longrightarrow> ?a \<le> ?b
\<lbrakk>?a < ?b; ?b \<le> ?c\<rbrakk> \<Longrightarrow> ?a < ?c
RecordsVacantUpto c0 t
s < t'
t' \<le> t
vacant_upto ?a ?t \<equiv> \<forall>s\<le>?t. zcount ?a s = 0

goal (1 subgoal):
 1. zcount (records c0) s = 0
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
zcount (records c0) s = 0

goal (3 subgoals):
 1. \<lbrakk>\<exists>s<t'. zcount (GlobalIncomingInfo c0 1 p q) s < 0 \<and> (\<forall>s'<s. zcount (InfoAt c0 0 p q) s' \<le> 0); \<not> (\<exists>s<t'. zcount (InfoAt c0 0 p q) s < 0 \<and> (\<forall>s'<s. zcount (InfoAt c0 0 p q) s' \<le> 0))\<rbrakk> \<Longrightarrow> False
 2. \<exists>s<t'. 0 < zcount (records c0) s \<Longrightarrow> False
 3. zcount (InfoAt c0 0 p q + GlobalIncomingInfo c0 1 p q) t' < zcount (records c0) t' \<Longrightarrow> False
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. False
[PROOF STEP]
using assms(6) change(1,4) s(1,2) rc t'(4)
[PROOF STATE]
proof (prove)
using this:
InvRecordCount c0
c_msg c0 p q \<noteq> []
c_glob c1 = (c_glob c0)(q := c_glob c0 q + hd (c_msg c0 p q))
s < t'
zcount (GlobalIncomingInfo c0 1 p q) s < 0
zcount (records c0) s = 0
\<forall>s<t'. zcount (c_glob c1 q) s \<le> 0

goal (1 subgoal):
 1. False
[PROOF STEP]
unfolding GII_eq_GIA InvRecordCount_def fun_upd_same
[PROOF STATE]
proof (prove)
using this:
\<forall>q. records c0 = GlobalIncomingInfoAt c0 q + c_glob c0 q
c_msg c0 p q \<noteq> []
c_glob c1 = (c_glob c0)(q := c_glob c0 q + hd (c_msg c0 p q))
s < t'
zcount (if c_msg c0 p q = [] then GlobalIncomingInfoAt c0 q else GlobalIncomingInfoAt c0 q - hd (c_msg c0 p q)) s < 0
zcount (records c0) s = 0
\<forall>s<t'. zcount (c_glob c1 q) s \<le> 0

goal (1 subgoal):
 1. False
[PROOF STEP]
by clarsimp (metis add.commute add_mono_thms_linordered_field(1) not_le recordcount)
[PROOF STATE]
proof (state)
this:
False

goal (2 subgoals):
 1. \<exists>s<t'. 0 < zcount (records c0) s \<Longrightarrow> False
 2. zcount (InfoAt c0 0 p q + GlobalIncomingInfo c0 1 p q) t' < zcount (records c0) t' \<Longrightarrow> False
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<exists>s<t'. 0 < zcount (records c0) s \<Longrightarrow> False
 2. zcount (InfoAt c0 0 p q + GlobalIncomingInfo c0 1 p q) t' < zcount (records c0) t' \<Longrightarrow> False
[PROOF STEP]
case 3
[PROOF STATE]
proof (state)
this:
\<exists>s<t'. 0 < zcount (records c0) s

goal (2 subgoals):
 1. \<exists>s<t'. 0 < zcount (records c0) s \<Longrightarrow> False
 2. zcount (InfoAt c0 0 p q + GlobalIncomingInfo c0 1 p q) t' < zcount (records c0) t' \<Longrightarrow> False
[PROOF STEP]
with nvu0 t'(1)
[PROOF STATE]
proof (chain)
picking this:
RecordsVacantUpto c0 t
t' \<le> t
\<exists>s<t'. 0 < zcount (records c0) s
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
RecordsVacantUpto c0 t
t' \<le> t
\<exists>s<t'. 0 < zcount (records c0) s

goal (1 subgoal):
 1. False
[PROOF STEP]
unfolding vacant_upto_def
[PROOF STATE]
proof (prove)
using this:
\<forall>s\<le>t. zcount (records c0) s = 0
t' \<le> t
\<exists>s<t'. 0 < zcount (records c0) s

goal (1 subgoal):
 1. False
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
False

goal (1 subgoal):
 1. zcount (InfoAt c0 0 p q + GlobalIncomingInfo c0 1 p q) t' < zcount (records c0) t' \<Longrightarrow> False
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. zcount (InfoAt c0 0 p q + GlobalIncomingInfo c0 1 p q) t' < zcount (records c0) t' \<Longrightarrow> False
[PROOF STEP]
case 4
[PROOF STATE]
proof (state)
this:
zcount (InfoAt c0 0 p q + GlobalIncomingInfo c0 1 p q) t' < zcount (records c0) t'

goal (1 subgoal):
 1. zcount (InfoAt c0 0 p q + GlobalIncomingInfo c0 1 p q) t' < zcount (records c0) t' \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
zcount (InfoAt c0 0 p q + GlobalIncomingInfo c0 1 p q) t' < zcount (records c0) t'
[PROOF STEP]
have "0 < zcount (c_glob c0 q) t'"
[PROOF STATE]
proof (prove)
using this:
zcount (InfoAt c0 0 p q + GlobalIncomingInfo c0 1 p q) t' < zcount (records c0) t'

goal (1 subgoal):
 1. 0 < zcount (c_glob c0 q) t'
[PROOF STEP]
using change(1) ia\<kappa> t'(3)
[PROOF STATE]
proof (prove)
using this:
zcount (InfoAt c0 0 p q + GlobalIncomingInfo c0 1 p q) t' < zcount (records c0) t'
c_msg c0 p q \<noteq> []
hd (c_msg c0 p q) = InfoAt c0 0 p q
zcount (c_glob c0 q) t' = 0

goal (1 subgoal):
 1. 0 < zcount (c_glob c0 q) t'
[PROOF STEP]
unfolding GII_eq_GIA
[PROOF STATE]
proof (prove)
using this:
zcount (InfoAt c0 0 p q + (if c_msg c0 p q = [] then GlobalIncomingInfoAt c0 q else GlobalIncomingInfoAt c0 q - hd (c_msg c0 p q))) t' < zcount (records c0) t'
c_msg c0 p q \<noteq> []
hd (c_msg c0 p q) = InfoAt c0 0 p q
zcount (c_glob c0 q) t' = 0

goal (1 subgoal):
 1. 0 < zcount (c_glob c0 q) t'
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>zcount (GlobalIncomingInfoAt c0 q) t' < zcount (records c0) t'; c_msg c0 p q \<noteq> []; hd (c_msg c0 p q) = InfoAt c0 0 p q; zcount (c_glob c0 q) t' = 0\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (metis add.right_neutral preorder_class.less_irrefl recordcount)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
0 < zcount (c_glob c0 q) t'

goal (1 subgoal):
 1. zcount (InfoAt c0 0 p q + GlobalIncomingInfo c0 1 p q) t' < zcount (records c0) t' \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
0 < zcount (c_glob c0 q) t'
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
0 < zcount (c_glob c0 q) t'

goal (1 subgoal):
 1. False
[PROOF STEP]
by (simp add: t'(3))
[PROOF STATE]
proof (state)
this:
False

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma sup_state_opt_any_Some:
  "P \<turnstile> (Some s) \<le>' X = (\<exists>s'. X = Some s' \<and> P \<turnstile> s \<le>\<^sub>i s')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<turnstile> \<lfloor>s\<rfloor> \<le>' X = (\<exists>s'. X = \<lfloor>s'\<rfloor> \<and> P \<turnstile> s \<le>\<^sub>i s')
[PROOF STEP]
by (simp add: sup_state_opt_def Opt.le_def lesub_def)


[STATEMENT]
lemma weakTransitionClosed[eqvt]:
  fixes \<Psi>   :: 'b
  and   Q    :: "('a, 'b, 'c) psi"
  and   P    :: "('a, 'b, 'c) psi"
  and   \<alpha>    :: "'a action"
  and   P'   :: "('a, 'b, 'c) psi"
  and   p    :: "name prm"

  assumes "\<Psi> : Q \<rhd> P \<Longrightarrow>\<alpha> \<prec> P'"

  shows "(p \<bullet> \<Psi>) : (p \<bullet> Q) \<rhd> (p \<bullet> P) \<Longrightarrow>(p \<bullet> \<alpha>)\<prec> (p \<bullet> P')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p \<bullet> \<Psi> : p \<bullet> Q \<rhd> p \<bullet> P \<Longrightarrow>p \<bullet> \<alpha> \<prec> p \<bullet> P'
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. p \<bullet> \<Psi> : p \<bullet> Q \<rhd> p \<bullet> P \<Longrightarrow>p \<bullet> \<alpha> \<prec> p \<bullet> P'
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
\<Psi> : Q \<rhd> P \<Longrightarrow>\<alpha> \<prec> P'
[PROOF STEP]
obtain P'' where "\<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P''" and "insertAssertion (extractFrame Q) \<Psi> \<hookrightarrow>\<^sub>F insertAssertion (extractFrame P'') \<Psi>"
                           and "\<Psi> \<rhd> P'' \<longmapsto>\<alpha> \<prec> P'"
[PROOF STATE]
proof (prove)
using this:
\<Psi> : Q \<rhd> P \<Longrightarrow>\<alpha> \<prec> P'

goal (1 subgoal):
 1. (\<And>P''. \<lbrakk>\<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P''; insertAssertion (extractFrame Q) \<Psi> \<hookrightarrow>\<^sub>F insertAssertion (extractFrame P'') \<Psi>; \<Psi> \<rhd> P'' \<longmapsto> \<alpha> \<prec> P'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(rule weakTransitionE)
[PROOF STATE]
proof (state)
this:
\<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P''
insertAssertion (extractFrame Q) \<Psi> \<hookrightarrow>\<^sub>F insertAssertion (extractFrame P'') \<Psi>
\<Psi> \<rhd> P'' \<longmapsto> \<alpha> \<prec> P'

goal (1 subgoal):
 1. p \<bullet> \<Psi> : p \<bullet> Q \<rhd> p \<bullet> P \<Longrightarrow>p \<bullet> \<alpha> \<prec> p \<bullet> P'
[PROOF STEP]
from \<open>\<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P''\<close>
[PROOF STATE]
proof (chain)
picking this:
\<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P''
[PROOF STEP]
have "(p \<bullet> \<Psi>) \<rhd> (p \<bullet> P) \<Longrightarrow>\<^sup>^\<^sub>\<tau> (p \<bullet> P'')"
[PROOF STATE]
proof (prove)
using this:
\<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P''

goal (1 subgoal):
 1. p \<bullet> \<Psi> \<rhd> p \<bullet> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> p \<bullet> P''
[PROOF STEP]
by(rule tauChainEqvt)
[PROOF STATE]
proof (state)
this:
p \<bullet> \<Psi> \<rhd> p \<bullet> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> p \<bullet> P''

goal (1 subgoal):
 1. p \<bullet> \<Psi> : p \<bullet> Q \<rhd> p \<bullet> P \<Longrightarrow>p \<bullet> \<alpha> \<prec> p \<bullet> P'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
p \<bullet> \<Psi> \<rhd> p \<bullet> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> p \<bullet> P''

goal (1 subgoal):
 1. p \<bullet> \<Psi> : p \<bullet> Q \<rhd> p \<bullet> P \<Longrightarrow>p \<bullet> \<alpha> \<prec> p \<bullet> P'
[PROOF STEP]
from \<open>insertAssertion (extractFrame Q) \<Psi> \<hookrightarrow>\<^sub>F insertAssertion (extractFrame P'') \<Psi>\<close>
[PROOF STATE]
proof (chain)
picking this:
insertAssertion (extractFrame Q) \<Psi> \<hookrightarrow>\<^sub>F insertAssertion (extractFrame P'') \<Psi>
[PROOF STEP]
have "(p \<bullet> (insertAssertion (extractFrame Q) \<Psi>)) \<hookrightarrow>\<^sub>F (p \<bullet> (insertAssertion (extractFrame P'') \<Psi>))"
[PROOF STATE]
proof (prove)
using this:
insertAssertion (extractFrame Q) \<Psi> \<hookrightarrow>\<^sub>F insertAssertion (extractFrame P'') \<Psi>

goal (1 subgoal):
 1. p \<bullet> insertAssertion (extractFrame Q) \<Psi> \<hookrightarrow>\<^sub>F p \<bullet> insertAssertion (extractFrame P'') \<Psi>
[PROOF STEP]
by(rule FrameStatImpClosed)
[PROOF STATE]
proof (state)
this:
p \<bullet> insertAssertion (extractFrame Q) \<Psi> \<hookrightarrow>\<^sub>F p \<bullet> insertAssertion (extractFrame P'') \<Psi>

goal (1 subgoal):
 1. p \<bullet> \<Psi> : p \<bullet> Q \<rhd> p \<bullet> P \<Longrightarrow>p \<bullet> \<alpha> \<prec> p \<bullet> P'
[PROOF STEP]
hence "insertAssertion (extractFrame(p \<bullet> Q)) (p \<bullet> \<Psi>) \<hookrightarrow>\<^sub>F insertAssertion (extractFrame(p \<bullet> P'')) (p \<bullet> \<Psi>)"
[PROOF STATE]
proof (prove)
using this:
p \<bullet> insertAssertion (extractFrame Q) \<Psi> \<hookrightarrow>\<^sub>F p \<bullet> insertAssertion (extractFrame P'') \<Psi>

goal (1 subgoal):
 1. insertAssertion (extractFrame (p \<bullet> Q)) (p \<bullet> \<Psi>) \<hookrightarrow>\<^sub>F insertAssertion (extractFrame (p \<bullet> P'')) (p \<bullet> \<Psi>)
[PROOF STEP]
by(simp add: eqvts)
[PROOF STATE]
proof (state)
this:
insertAssertion (extractFrame (p \<bullet> Q)) (p \<bullet> \<Psi>) \<hookrightarrow>\<^sub>F insertAssertion (extractFrame (p \<bullet> P'')) (p \<bullet> \<Psi>)

goal (1 subgoal):
 1. p \<bullet> \<Psi> : p \<bullet> Q \<rhd> p \<bullet> P \<Longrightarrow>p \<bullet> \<alpha> \<prec> p \<bullet> P'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
insertAssertion (extractFrame (p \<bullet> Q)) (p \<bullet> \<Psi>) \<hookrightarrow>\<^sub>F insertAssertion (extractFrame (p \<bullet> P'')) (p \<bullet> \<Psi>)

goal (1 subgoal):
 1. p \<bullet> \<Psi> : p \<bullet> Q \<rhd> p \<bullet> P \<Longrightarrow>p \<bullet> \<alpha> \<prec> p \<bullet> P'
[PROOF STEP]
from \<open>\<Psi> \<rhd> P'' \<longmapsto>\<alpha> \<prec> P'\<close>
[PROOF STATE]
proof (chain)
picking this:
\<Psi> \<rhd> P'' \<longmapsto> \<alpha> \<prec> P'
[PROOF STEP]
have "(p \<bullet> \<Psi>) \<rhd> (p \<bullet> P'') \<longmapsto>(p \<bullet> (\<alpha> \<prec> P'))"
[PROOF STATE]
proof (prove)
using this:
\<Psi> \<rhd> P'' \<longmapsto> \<alpha> \<prec> P'

goal (1 subgoal):
 1. p \<bullet> \<Psi> \<rhd> p \<bullet> P'' \<longmapsto> p \<bullet> \<alpha> \<prec> P'
[PROOF STEP]
by(rule semantics.eqvt)
[PROOF STATE]
proof (state)
this:
p \<bullet> \<Psi> \<rhd> p \<bullet> P'' \<longmapsto> p \<bullet> \<alpha> \<prec> P'

goal (1 subgoal):
 1. p \<bullet> \<Psi> : p \<bullet> Q \<rhd> p \<bullet> P \<Longrightarrow>p \<bullet> \<alpha> \<prec> p \<bullet> P'
[PROOF STEP]
hence "(p \<bullet> \<Psi>) \<rhd> (p \<bullet> P'') \<longmapsto>(p \<bullet> \<alpha>) \<prec> (p \<bullet> P')"
[PROOF STATE]
proof (prove)
using this:
p \<bullet> \<Psi> \<rhd> p \<bullet> P'' \<longmapsto> p \<bullet> \<alpha> \<prec> P'

goal (1 subgoal):
 1. p \<bullet> \<Psi> \<rhd> p \<bullet> P'' \<longmapsto> p \<bullet> \<alpha> \<prec> p \<bullet> P'
[PROOF STEP]
by(simp add: eqvts)
[PROOF STATE]
proof (state)
this:
p \<bullet> \<Psi> \<rhd> p \<bullet> P'' \<longmapsto> p \<bullet> \<alpha> \<prec> p \<bullet> P'

goal (1 subgoal):
 1. p \<bullet> \<Psi> : p \<bullet> Q \<rhd> p \<bullet> P \<Longrightarrow>p \<bullet> \<alpha> \<prec> p \<bullet> P'
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
p \<bullet> \<Psi> \<rhd> p \<bullet> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> p \<bullet> P''
insertAssertion (extractFrame (p \<bullet> Q)) (p \<bullet> \<Psi>) \<hookrightarrow>\<^sub>F insertAssertion (extractFrame (p \<bullet> P'')) (p \<bullet> \<Psi>)
p \<bullet> \<Psi> \<rhd> p \<bullet> P'' \<longmapsto> p \<bullet> \<alpha> \<prec> p \<bullet> P'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
p \<bullet> \<Psi> \<rhd> p \<bullet> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> p \<bullet> P''
insertAssertion (extractFrame (p \<bullet> Q)) (p \<bullet> \<Psi>) \<hookrightarrow>\<^sub>F insertAssertion (extractFrame (p \<bullet> P'')) (p \<bullet> \<Psi>)
p \<bullet> \<Psi> \<rhd> p \<bullet> P'' \<longmapsto> p \<bullet> \<alpha> \<prec> p \<bullet> P'

goal (1 subgoal):
 1. p \<bullet> \<Psi> : p \<bullet> Q \<rhd> p \<bullet> P \<Longrightarrow>p \<bullet> \<alpha> \<prec> p \<bullet> P'
[PROOF STEP]
by(rule weakTransitionI)
[PROOF STATE]
proof (state)
this:
p \<bullet> \<Psi> : p \<bullet> Q \<rhd> p \<bullet> P \<Longrightarrow>p \<bullet> \<alpha> \<prec> p \<bullet> P'

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma foldl_Gauss_Jordan_column_k_det_P:
fixes A::"'a::{field}^'n::{mod_type}^'n::{mod_type}"
shows det_fst_Gauss_Jordan_upt_k_PA_eq_fst_Gauss_Jordan_upt_k_det_P: "fst (Gauss_Jordan_upt_k_det_P A k) = det (fst (Gauss_Jordan_upt_k_PA A k))"
and snd_Gauss_Jordan_upt_k_det_P_is_snd_Gauss_Jordan_upt_k_PA: "snd (Gauss_Jordan_upt_k_det_P A k) = snd (Gauss_Jordan_upt_k_PA A k)"
and fst_snd_foldl_Gauss_det_P_PA: "fst (snd (foldl Gauss_Jordan_column_k_det_P (1, 0, A) [0..<Suc k])) = fst (snd (foldl Gauss_Jordan_column_k_PA (mat 1, 0, A) [0..<Suc k]))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst (Gauss_Jordan_upt_k_det_P A k) = det (fst (Gauss_Jordan_upt_k_PA A k)) &&& snd (Gauss_Jordan_upt_k_det_P A k) = snd (Gauss_Jordan_upt_k_PA A k) &&& fst (snd (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc k])) = fst (snd (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc k]))
[PROOF STEP]
proof (induct k)
[PROOF STATE]
proof (state)
goal (6 subgoals):
 1. fst (Gauss_Jordan_upt_k_det_P A 0) = det (fst (Gauss_Jordan_upt_k_PA A 0))
 2. snd (Gauss_Jordan_upt_k_det_P A 0) = snd (Gauss_Jordan_upt_k_PA A 0)
 3. fst (snd (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc 0])) = fst (snd (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc 0]))
 4. \<And>k. \<lbrakk>fst (Gauss_Jordan_upt_k_det_P A k) = det (fst (Gauss_Jordan_upt_k_PA A k)); snd (Gauss_Jordan_upt_k_det_P A k) = snd (Gauss_Jordan_upt_k_PA A k); fst (snd (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc k])) = fst (snd (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc k]))\<rbrakk> \<Longrightarrow> fst (Gauss_Jordan_upt_k_det_P A (Suc k)) = det (fst (Gauss_Jordan_upt_k_PA A (Suc k)))
 5. \<And>k. \<lbrakk>fst (Gauss_Jordan_upt_k_det_P A k) = det (fst (Gauss_Jordan_upt_k_PA A k)); snd (Gauss_Jordan_upt_k_det_P A k) = snd (Gauss_Jordan_upt_k_PA A k); fst (snd (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc k])) = fst (snd (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc k]))\<rbrakk> \<Longrightarrow> snd (Gauss_Jordan_upt_k_det_P A (Suc k)) = snd (Gauss_Jordan_upt_k_PA A (Suc k))
 6. \<And>k. \<lbrakk>fst (Gauss_Jordan_upt_k_det_P A k) = det (fst (Gauss_Jordan_upt_k_PA A k)); snd (Gauss_Jordan_upt_k_det_P A k) = snd (Gauss_Jordan_upt_k_PA A k); fst (snd (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc k])) = fst (snd (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc k]))\<rbrakk> \<Longrightarrow> fst (snd (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc (Suc k)])) = fst (snd (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc (Suc k)]))
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:

goal (6 subgoals):
 1. fst (Gauss_Jordan_upt_k_det_P A 0) = det (fst (Gauss_Jordan_upt_k_PA A 0))
 2. snd (Gauss_Jordan_upt_k_det_P A 0) = snd (Gauss_Jordan_upt_k_PA A 0)
 3. fst (snd (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc 0])) = fst (snd (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc 0]))
 4. \<And>k. \<lbrakk>fst (Gauss_Jordan_upt_k_det_P A k) = det (fst (Gauss_Jordan_upt_k_PA A k)); snd (Gauss_Jordan_upt_k_det_P A k) = snd (Gauss_Jordan_upt_k_PA A k); fst (snd (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc k])) = fst (snd (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc k]))\<rbrakk> \<Longrightarrow> fst (Gauss_Jordan_upt_k_det_P A (Suc k)) = det (fst (Gauss_Jordan_upt_k_PA A (Suc k)))
 5. \<And>k. \<lbrakk>fst (Gauss_Jordan_upt_k_det_P A k) = det (fst (Gauss_Jordan_upt_k_PA A k)); snd (Gauss_Jordan_upt_k_det_P A k) = snd (Gauss_Jordan_upt_k_PA A k); fst (snd (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc k])) = fst (snd (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc k]))\<rbrakk> \<Longrightarrow> snd (Gauss_Jordan_upt_k_det_P A (Suc k)) = snd (Gauss_Jordan_upt_k_PA A (Suc k))
 6. \<And>k. \<lbrakk>fst (Gauss_Jordan_upt_k_det_P A k) = det (fst (Gauss_Jordan_upt_k_PA A k)); snd (Gauss_Jordan_upt_k_det_P A k) = snd (Gauss_Jordan_upt_k_PA A k); fst (snd (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc k])) = fst (snd (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc k]))\<rbrakk> \<Longrightarrow> fst (snd (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc (Suc k)])) = fst (snd (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc (Suc k)]))
[PROOF STEP]
show "fst (Gauss_Jordan_upt_k_det_P A 0) = det (fst (Gauss_Jordan_upt_k_PA A 0))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst (Gauss_Jordan_upt_k_det_P A 0) = det (fst (Gauss_Jordan_upt_k_PA A 0))
[PROOF STEP]
unfolding Gauss_Jordan_upt_k_det_P_def Gauss_Jordan_upt_k_PA_def Let_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst (fst (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc 0]), snd (snd (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc 0]))) = det (fst (fst (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc 0]), snd (snd (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc 0]))))
[PROOF STEP]
by (simp, metis det_fst_Gauss_Jordan_column_k_PA_eq_fst_Gauss_Jordan_column_k_det_P det_I)
[PROOF STATE]
proof (state)
this:
fst (Gauss_Jordan_upt_k_det_P A 0) = det (fst (Gauss_Jordan_upt_k_PA A 0))

goal (5 subgoals):
 1. snd (Gauss_Jordan_upt_k_det_P A 0) = snd (Gauss_Jordan_upt_k_PA A 0)
 2. fst (snd (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc 0])) = fst (snd (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc 0]))
 3. \<And>k. \<lbrakk>fst (Gauss_Jordan_upt_k_det_P A k) = det (fst (Gauss_Jordan_upt_k_PA A k)); snd (Gauss_Jordan_upt_k_det_P A k) = snd (Gauss_Jordan_upt_k_PA A k); fst (snd (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc k])) = fst (snd (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc k]))\<rbrakk> \<Longrightarrow> fst (Gauss_Jordan_upt_k_det_P A (Suc k)) = det (fst (Gauss_Jordan_upt_k_PA A (Suc k)))
 4. \<And>k. \<lbrakk>fst (Gauss_Jordan_upt_k_det_P A k) = det (fst (Gauss_Jordan_upt_k_PA A k)); snd (Gauss_Jordan_upt_k_det_P A k) = snd (Gauss_Jordan_upt_k_PA A k); fst (snd (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc k])) = fst (snd (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc k]))\<rbrakk> \<Longrightarrow> snd (Gauss_Jordan_upt_k_det_P A (Suc k)) = snd (Gauss_Jordan_upt_k_PA A (Suc k))
 5. \<And>k. \<lbrakk>fst (Gauss_Jordan_upt_k_det_P A k) = det (fst (Gauss_Jordan_upt_k_PA A k)); snd (Gauss_Jordan_upt_k_det_P A k) = snd (Gauss_Jordan_upt_k_PA A k); fst (snd (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc k])) = fst (snd (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc k]))\<rbrakk> \<Longrightarrow> fst (snd (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc (Suc k)])) = fst (snd (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc (Suc k)]))
[PROOF STEP]
show "snd (Gauss_Jordan_upt_k_det_P A 0) = snd (Gauss_Jordan_upt_k_PA A 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. snd (Gauss_Jordan_upt_k_det_P A 0) = snd (Gauss_Jordan_upt_k_PA A 0)
[PROOF STEP]
unfolding Gauss_Jordan_upt_k_det_P_def Gauss_Jordan_upt_k_PA_def Let_def snd_conv
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. snd (snd (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc 0])) = snd (snd (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc 0]))
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. snd (snd (Gauss_Jordan_column_k_det_P (1::'a, 0, A) 0)) = snd (snd (Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) 0))
[PROOF STEP]
using snd_Gauss_Jordan_column_k_det_P_is_snd_Gauss_Jordan_column_k_PA
[PROOF STATE]
proof (prove)
using this:
snd (Gauss_Jordan_column_k_det_P (?n, ?i, ?A) ?k) = snd (Gauss_Jordan_column_k_PA (?P, ?i, ?A) ?k)

goal (1 subgoal):
 1. snd (snd (Gauss_Jordan_column_k_det_P (1::'a, 0, A) 0)) = snd (snd (Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) 0))
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
snd (Gauss_Jordan_upt_k_det_P A 0) = snd (Gauss_Jordan_upt_k_PA A 0)

goal (4 subgoals):
 1. fst (snd (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc 0])) = fst (snd (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc 0]))
 2. \<And>k. \<lbrakk>fst (Gauss_Jordan_upt_k_det_P A k) = det (fst (Gauss_Jordan_upt_k_PA A k)); snd (Gauss_Jordan_upt_k_det_P A k) = snd (Gauss_Jordan_upt_k_PA A k); fst (snd (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc k])) = fst (snd (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc k]))\<rbrakk> \<Longrightarrow> fst (Gauss_Jordan_upt_k_det_P A (Suc k)) = det (fst (Gauss_Jordan_upt_k_PA A (Suc k)))
 3. \<And>k. \<lbrakk>fst (Gauss_Jordan_upt_k_det_P A k) = det (fst (Gauss_Jordan_upt_k_PA A k)); snd (Gauss_Jordan_upt_k_det_P A k) = snd (Gauss_Jordan_upt_k_PA A k); fst (snd (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc k])) = fst (snd (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc k]))\<rbrakk> \<Longrightarrow> snd (Gauss_Jordan_upt_k_det_P A (Suc k)) = snd (Gauss_Jordan_upt_k_PA A (Suc k))
 4. \<And>k. \<lbrakk>fst (Gauss_Jordan_upt_k_det_P A k) = det (fst (Gauss_Jordan_upt_k_PA A k)); snd (Gauss_Jordan_upt_k_det_P A k) = snd (Gauss_Jordan_upt_k_PA A k); fst (snd (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc k])) = fst (snd (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc k]))\<rbrakk> \<Longrightarrow> fst (snd (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc (Suc k)])) = fst (snd (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc (Suc k)]))
[PROOF STEP]
show "fst (snd (foldl Gauss_Jordan_column_k_det_P (1, 0, A) [0..<Suc 0])) = fst (snd (foldl Gauss_Jordan_column_k_PA (mat 1, 0, A) [0..<Suc 0]))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst (snd (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc 0])) = fst (snd (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc 0]))
[PROOF STEP]
using [[unfold_abs_def = false]]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst (snd (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc 0])) = fst (snd (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc 0]))
[PROOF STEP]
unfolding Gauss_Jordan_column_k_det_P_def Gauss_Jordan_column_k_PA_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst (snd (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc 0])) = fst (snd (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc 0]))
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst (snd (Gauss_Jordan_column_k_det_P (1::'a, 0, A) 0)) = fst (snd (Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) 0))
[PROOF STEP]
using fst_snd_Gauss_Jordan_column_k_det_P_eq_fst_snd_Gauss_Jordan_column_k_PA
[PROOF STATE]
proof (prove)
using this:
fst (snd (Gauss_Jordan_column_k_det_P (?n, ?i, ?A) ?k)) = fst (snd (Gauss_Jordan_column_k_PA (?P, ?i, ?A) ?k))

goal (1 subgoal):
 1. fst (snd (Gauss_Jordan_column_k_det_P (1::'a, 0, A) 0)) = fst (snd (Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) 0))
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
fst (snd (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc 0])) = fst (snd (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc 0]))

goal (3 subgoals):
 1. \<And>k. \<lbrakk>fst (Gauss_Jordan_upt_k_det_P A k) = det (fst (Gauss_Jordan_upt_k_PA A k)); snd (Gauss_Jordan_upt_k_det_P A k) = snd (Gauss_Jordan_upt_k_PA A k); fst (snd (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc k])) = fst (snd (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc k]))\<rbrakk> \<Longrightarrow> fst (Gauss_Jordan_upt_k_det_P A (Suc k)) = det (fst (Gauss_Jordan_upt_k_PA A (Suc k)))
 2. \<And>k. \<lbrakk>fst (Gauss_Jordan_upt_k_det_P A k) = det (fst (Gauss_Jordan_upt_k_PA A k)); snd (Gauss_Jordan_upt_k_det_P A k) = snd (Gauss_Jordan_upt_k_PA A k); fst (snd (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc k])) = fst (snd (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc k]))\<rbrakk> \<Longrightarrow> snd (Gauss_Jordan_upt_k_det_P A (Suc k)) = snd (Gauss_Jordan_upt_k_PA A (Suc k))
 3. \<And>k. \<lbrakk>fst (Gauss_Jordan_upt_k_det_P A k) = det (fst (Gauss_Jordan_upt_k_PA A k)); snd (Gauss_Jordan_upt_k_det_P A k) = snd (Gauss_Jordan_upt_k_PA A k); fst (snd (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc k])) = fst (snd (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc k]))\<rbrakk> \<Longrightarrow> fst (snd (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc (Suc k)])) = fst (snd (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc (Suc k)]))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>k. \<lbrakk>fst (Gauss_Jordan_upt_k_det_P A k) = det (fst (Gauss_Jordan_upt_k_PA A k)); snd (Gauss_Jordan_upt_k_det_P A k) = snd (Gauss_Jordan_upt_k_PA A k); fst (snd (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc k])) = fst (snd (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc k]))\<rbrakk> \<Longrightarrow> fst (Gauss_Jordan_upt_k_det_P A (Suc k)) = det (fst (Gauss_Jordan_upt_k_PA A (Suc k)))
 2. \<And>k. \<lbrakk>fst (Gauss_Jordan_upt_k_det_P A k) = det (fst (Gauss_Jordan_upt_k_PA A k)); snd (Gauss_Jordan_upt_k_det_P A k) = snd (Gauss_Jordan_upt_k_PA A k); fst (snd (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc k])) = fst (snd (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc k]))\<rbrakk> \<Longrightarrow> snd (Gauss_Jordan_upt_k_det_P A (Suc k)) = snd (Gauss_Jordan_upt_k_PA A (Suc k))
 3. \<And>k. \<lbrakk>fst (Gauss_Jordan_upt_k_det_P A k) = det (fst (Gauss_Jordan_upt_k_PA A k)); snd (Gauss_Jordan_upt_k_det_P A k) = snd (Gauss_Jordan_upt_k_PA A k); fst (snd (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc k])) = fst (snd (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc k]))\<rbrakk> \<Longrightarrow> fst (snd (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc (Suc k)])) = fst (snd (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc (Suc k)]))
[PROOF STEP]
fix k
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>k. \<lbrakk>fst (Gauss_Jordan_upt_k_det_P A k) = det (fst (Gauss_Jordan_upt_k_PA A k)); snd (Gauss_Jordan_upt_k_det_P A k) = snd (Gauss_Jordan_upt_k_PA A k); fst (snd (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc k])) = fst (snd (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc k]))\<rbrakk> \<Longrightarrow> fst (Gauss_Jordan_upt_k_det_P A (Suc k)) = det (fst (Gauss_Jordan_upt_k_PA A (Suc k)))
 2. \<And>k. \<lbrakk>fst (Gauss_Jordan_upt_k_det_P A k) = det (fst (Gauss_Jordan_upt_k_PA A k)); snd (Gauss_Jordan_upt_k_det_P A k) = snd (Gauss_Jordan_upt_k_PA A k); fst (snd (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc k])) = fst (snd (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc k]))\<rbrakk> \<Longrightarrow> snd (Gauss_Jordan_upt_k_det_P A (Suc k)) = snd (Gauss_Jordan_upt_k_PA A (Suc k))
 3. \<And>k. \<lbrakk>fst (Gauss_Jordan_upt_k_det_P A k) = det (fst (Gauss_Jordan_upt_k_PA A k)); snd (Gauss_Jordan_upt_k_det_P A k) = snd (Gauss_Jordan_upt_k_PA A k); fst (snd (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc k])) = fst (snd (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc k]))\<rbrakk> \<Longrightarrow> fst (snd (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc (Suc k)])) = fst (snd (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc (Suc k)]))
[PROOF STEP]
assume hyp1: "fst (Gauss_Jordan_upt_k_det_P A k) = det (fst (Gauss_Jordan_upt_k_PA A k))"
and hyp2: "snd (Gauss_Jordan_upt_k_det_P A k) = snd (Gauss_Jordan_upt_k_PA A k)"
and hyp3: "fst (snd (foldl Gauss_Jordan_column_k_det_P (1, 0, A) [0..<Suc k])) = fst (snd (foldl Gauss_Jordan_column_k_PA (mat 1, 0, A) [0..<Suc k]))"
[PROOF STATE]
proof (state)
this:
fst (Gauss_Jordan_upt_k_det_P A k) = det (fst (Gauss_Jordan_upt_k_PA A k))
snd (Gauss_Jordan_upt_k_det_P A k) = snd (Gauss_Jordan_upt_k_PA A k)
fst (snd (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc k])) = fst (snd (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc k]))

goal (3 subgoals):
 1. \<And>k. \<lbrakk>fst (Gauss_Jordan_upt_k_det_P A k) = det (fst (Gauss_Jordan_upt_k_PA A k)); snd (Gauss_Jordan_upt_k_det_P A k) = snd (Gauss_Jordan_upt_k_PA A k); fst (snd (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc k])) = fst (snd (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc k]))\<rbrakk> \<Longrightarrow> fst (Gauss_Jordan_upt_k_det_P A (Suc k)) = det (fst (Gauss_Jordan_upt_k_PA A (Suc k)))
 2. \<And>k. \<lbrakk>fst (Gauss_Jordan_upt_k_det_P A k) = det (fst (Gauss_Jordan_upt_k_PA A k)); snd (Gauss_Jordan_upt_k_det_P A k) = snd (Gauss_Jordan_upt_k_PA A k); fst (snd (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc k])) = fst (snd (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc k]))\<rbrakk> \<Longrightarrow> snd (Gauss_Jordan_upt_k_det_P A (Suc k)) = snd (Gauss_Jordan_upt_k_PA A (Suc k))
 3. \<And>k. \<lbrakk>fst (Gauss_Jordan_upt_k_det_P A k) = det (fst (Gauss_Jordan_upt_k_PA A k)); snd (Gauss_Jordan_upt_k_det_P A k) = snd (Gauss_Jordan_upt_k_PA A k); fst (snd (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc k])) = fst (snd (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc k]))\<rbrakk> \<Longrightarrow> fst (snd (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc (Suc k)])) = fst (snd (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc (Suc k)]))
[PROOF STEP]
have list_rw: "[0..<Suc (Suc k)] = [0..<Suc k] @ [Suc k]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [0..<Suc (Suc k)] = [0..<Suc k] @ [Suc k]
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
[0..<Suc (Suc k)] = [0..<Suc k] @ [Suc k]

goal (3 subgoals):
 1. \<And>k. \<lbrakk>fst (Gauss_Jordan_upt_k_det_P A k) = det (fst (Gauss_Jordan_upt_k_PA A k)); snd (Gauss_Jordan_upt_k_det_P A k) = snd (Gauss_Jordan_upt_k_PA A k); fst (snd (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc k])) = fst (snd (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc k]))\<rbrakk> \<Longrightarrow> fst (Gauss_Jordan_upt_k_det_P A (Suc k)) = det (fst (Gauss_Jordan_upt_k_PA A (Suc k)))
 2. \<And>k. \<lbrakk>fst (Gauss_Jordan_upt_k_det_P A k) = det (fst (Gauss_Jordan_upt_k_PA A k)); snd (Gauss_Jordan_upt_k_det_P A k) = snd (Gauss_Jordan_upt_k_PA A k); fst (snd (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc k])) = fst (snd (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc k]))\<rbrakk> \<Longrightarrow> snd (Gauss_Jordan_upt_k_det_P A (Suc k)) = snd (Gauss_Jordan_upt_k_PA A (Suc k))
 3. \<And>k. \<lbrakk>fst (Gauss_Jordan_upt_k_det_P A k) = det (fst (Gauss_Jordan_upt_k_PA A k)); snd (Gauss_Jordan_upt_k_det_P A k) = snd (Gauss_Jordan_upt_k_PA A k); fst (snd (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc k])) = fst (snd (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc k]))\<rbrakk> \<Longrightarrow> fst (snd (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc (Suc k)])) = fst (snd (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc (Suc k)]))
[PROOF STEP]
have det_mat_nn: "det (mat 1::'a^'n::{mod_type}^'n::{mod_type}) = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. det (mat (1::'a)) = (1::'a)
[PROOF STEP]
using det_I
[PROOF STATE]
proof (prove)
using this:
det (mat (1::?'a)) = (1::?'a)

goal (1 subgoal):
 1. det (mat (1::'a)) = (1::'a)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
det (mat (1::'a)) = (1::'a)

goal (3 subgoals):
 1. \<And>k. \<lbrakk>fst (Gauss_Jordan_upt_k_det_P A k) = det (fst (Gauss_Jordan_upt_k_PA A k)); snd (Gauss_Jordan_upt_k_det_P A k) = snd (Gauss_Jordan_upt_k_PA A k); fst (snd (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc k])) = fst (snd (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc k]))\<rbrakk> \<Longrightarrow> fst (Gauss_Jordan_upt_k_det_P A (Suc k)) = det (fst (Gauss_Jordan_upt_k_PA A (Suc k)))
 2. \<And>k. \<lbrakk>fst (Gauss_Jordan_upt_k_det_P A k) = det (fst (Gauss_Jordan_upt_k_PA A k)); snd (Gauss_Jordan_upt_k_det_P A k) = snd (Gauss_Jordan_upt_k_PA A k); fst (snd (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc k])) = fst (snd (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc k]))\<rbrakk> \<Longrightarrow> snd (Gauss_Jordan_upt_k_det_P A (Suc k)) = snd (Gauss_Jordan_upt_k_PA A (Suc k))
 3. \<And>k. \<lbrakk>fst (Gauss_Jordan_upt_k_det_P A k) = det (fst (Gauss_Jordan_upt_k_PA A k)); snd (Gauss_Jordan_upt_k_det_P A k) = snd (Gauss_Jordan_upt_k_PA A k); fst (snd (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc k])) = fst (snd (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc k]))\<rbrakk> \<Longrightarrow> fst (snd (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc (Suc k)])) = fst (snd (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc (Suc k)]))
[PROOF STEP]
define f where "f = foldl Gauss_Jordan_column_k_det_P (1, 0, A) [0..<Suc k]"
[PROOF STATE]
proof (state)
this:
f = foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc k]

goal (3 subgoals):
 1. \<And>k. \<lbrakk>fst (Gauss_Jordan_upt_k_det_P A k) = det (fst (Gauss_Jordan_upt_k_PA A k)); snd (Gauss_Jordan_upt_k_det_P A k) = snd (Gauss_Jordan_upt_k_PA A k); fst (snd (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc k])) = fst (snd (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc k]))\<rbrakk> \<Longrightarrow> fst (Gauss_Jordan_upt_k_det_P A (Suc k)) = det (fst (Gauss_Jordan_upt_k_PA A (Suc k)))
 2. \<And>k. \<lbrakk>fst (Gauss_Jordan_upt_k_det_P A k) = det (fst (Gauss_Jordan_upt_k_PA A k)); snd (Gauss_Jordan_upt_k_det_P A k) = snd (Gauss_Jordan_upt_k_PA A k); fst (snd (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc k])) = fst (snd (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc k]))\<rbrakk> \<Longrightarrow> snd (Gauss_Jordan_upt_k_det_P A (Suc k)) = snd (Gauss_Jordan_upt_k_PA A (Suc k))
 3. \<And>k. \<lbrakk>fst (Gauss_Jordan_upt_k_det_P A k) = det (fst (Gauss_Jordan_upt_k_PA A k)); snd (Gauss_Jordan_upt_k_det_P A k) = snd (Gauss_Jordan_upt_k_PA A k); fst (snd (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc k])) = fst (snd (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc k]))\<rbrakk> \<Longrightarrow> fst (snd (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc (Suc k)])) = fst (snd (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc (Suc k)]))
[PROOF STEP]
define g where "g = foldl Gauss_Jordan_column_k_PA (mat 1, 0, A) [0..<Suc k]"
[PROOF STATE]
proof (state)
this:
g = foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc k]

goal (3 subgoals):
 1. \<And>k. \<lbrakk>fst (Gauss_Jordan_upt_k_det_P A k) = det (fst (Gauss_Jordan_upt_k_PA A k)); snd (Gauss_Jordan_upt_k_det_P A k) = snd (Gauss_Jordan_upt_k_PA A k); fst (snd (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc k])) = fst (snd (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc k]))\<rbrakk> \<Longrightarrow> fst (Gauss_Jordan_upt_k_det_P A (Suc k)) = det (fst (Gauss_Jordan_upt_k_PA A (Suc k)))
 2. \<And>k. \<lbrakk>fst (Gauss_Jordan_upt_k_det_P A k) = det (fst (Gauss_Jordan_upt_k_PA A k)); snd (Gauss_Jordan_upt_k_det_P A k) = snd (Gauss_Jordan_upt_k_PA A k); fst (snd (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc k])) = fst (snd (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc k]))\<rbrakk> \<Longrightarrow> snd (Gauss_Jordan_upt_k_det_P A (Suc k)) = snd (Gauss_Jordan_upt_k_PA A (Suc k))
 3. \<And>k. \<lbrakk>fst (Gauss_Jordan_upt_k_det_P A k) = det (fst (Gauss_Jordan_upt_k_PA A k)); snd (Gauss_Jordan_upt_k_det_P A k) = snd (Gauss_Jordan_upt_k_PA A k); fst (snd (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc k])) = fst (snd (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc k]))\<rbrakk> \<Longrightarrow> fst (snd (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc (Suc k)])) = fst (snd (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc (Suc k)]))
[PROOF STEP]
have f_rw: "f = (fst f, fst (snd f), snd(snd f))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f = (fst f, fst (snd f), snd (snd f))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
f = (fst f, fst (snd f), snd (snd f))

goal (3 subgoals):
 1. \<And>k. \<lbrakk>fst (Gauss_Jordan_upt_k_det_P A k) = det (fst (Gauss_Jordan_upt_k_PA A k)); snd (Gauss_Jordan_upt_k_det_P A k) = snd (Gauss_Jordan_upt_k_PA A k); fst (snd (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc k])) = fst (snd (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc k]))\<rbrakk> \<Longrightarrow> fst (Gauss_Jordan_upt_k_det_P A (Suc k)) = det (fst (Gauss_Jordan_upt_k_PA A (Suc k)))
 2. \<And>k. \<lbrakk>fst (Gauss_Jordan_upt_k_det_P A k) = det (fst (Gauss_Jordan_upt_k_PA A k)); snd (Gauss_Jordan_upt_k_det_P A k) = snd (Gauss_Jordan_upt_k_PA A k); fst (snd (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc k])) = fst (snd (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc k]))\<rbrakk> \<Longrightarrow> snd (Gauss_Jordan_upt_k_det_P A (Suc k)) = snd (Gauss_Jordan_upt_k_PA A (Suc k))
 3. \<And>k. \<lbrakk>fst (Gauss_Jordan_upt_k_det_P A k) = det (fst (Gauss_Jordan_upt_k_PA A k)); snd (Gauss_Jordan_upt_k_det_P A k) = snd (Gauss_Jordan_upt_k_PA A k); fst (snd (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc k])) = fst (snd (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc k]))\<rbrakk> \<Longrightarrow> fst (snd (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc (Suc k)])) = fst (snd (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc (Suc k)]))
[PROOF STEP]
have g_rw: "g = (fst g, fst (snd g), snd(snd g))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. g = (fst g, fst (snd g), snd (snd g))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
g = (fst g, fst (snd g), snd (snd g))

goal (3 subgoals):
 1. \<And>k. \<lbrakk>fst (Gauss_Jordan_upt_k_det_P A k) = det (fst (Gauss_Jordan_upt_k_PA A k)); snd (Gauss_Jordan_upt_k_det_P A k) = snd (Gauss_Jordan_upt_k_PA A k); fst (snd (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc k])) = fst (snd (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc k]))\<rbrakk> \<Longrightarrow> fst (Gauss_Jordan_upt_k_det_P A (Suc k)) = det (fst (Gauss_Jordan_upt_k_PA A (Suc k)))
 2. \<And>k. \<lbrakk>fst (Gauss_Jordan_upt_k_det_P A k) = det (fst (Gauss_Jordan_upt_k_PA A k)); snd (Gauss_Jordan_upt_k_det_P A k) = snd (Gauss_Jordan_upt_k_PA A k); fst (snd (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc k])) = fst (snd (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc k]))\<rbrakk> \<Longrightarrow> snd (Gauss_Jordan_upt_k_det_P A (Suc k)) = snd (Gauss_Jordan_upt_k_PA A (Suc k))
 3. \<And>k. \<lbrakk>fst (Gauss_Jordan_upt_k_det_P A k) = det (fst (Gauss_Jordan_upt_k_PA A k)); snd (Gauss_Jordan_upt_k_det_P A k) = snd (Gauss_Jordan_upt_k_PA A k); fst (snd (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc k])) = fst (snd (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc k]))\<rbrakk> \<Longrightarrow> fst (snd (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc (Suc k)])) = fst (snd (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc (Suc k)]))
[PROOF STEP]
have fst_snd: "fst (snd f) = fst (snd g)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst (snd f) = fst (snd g)
[PROOF STEP]
unfolding f_def g_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst (snd (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc k])) = fst (snd (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc k]))
[PROOF STEP]
using hyp3
[PROOF STATE]
proof (prove)
using this:
fst (snd (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc k])) = fst (snd (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc k]))

goal (1 subgoal):
 1. fst (snd (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc k])) = fst (snd (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc k]))
[PROOF STEP]
unfolding Gauss_Jordan_upt_k_det_P_def Gauss_Jordan_upt_k_PA_def Let_def fst_conv snd_conv
[PROOF STATE]
proof (prove)
using this:
fst (snd (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc k])) = fst (snd (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc k]))

goal (1 subgoal):
 1. fst (snd (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc k])) = fst (snd (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc k]))
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
fst (snd f) = fst (snd g)

goal (3 subgoals):
 1. \<And>k. \<lbrakk>fst (Gauss_Jordan_upt_k_det_P A k) = det (fst (Gauss_Jordan_upt_k_PA A k)); snd (Gauss_Jordan_upt_k_det_P A k) = snd (Gauss_Jordan_upt_k_PA A k); fst (snd (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc k])) = fst (snd (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc k]))\<rbrakk> \<Longrightarrow> fst (Gauss_Jordan_upt_k_det_P A (Suc k)) = det (fst (Gauss_Jordan_upt_k_PA A (Suc k)))
 2. \<And>k. \<lbrakk>fst (Gauss_Jordan_upt_k_det_P A k) = det (fst (Gauss_Jordan_upt_k_PA A k)); snd (Gauss_Jordan_upt_k_det_P A k) = snd (Gauss_Jordan_upt_k_PA A k); fst (snd (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc k])) = fst (snd (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc k]))\<rbrakk> \<Longrightarrow> snd (Gauss_Jordan_upt_k_det_P A (Suc k)) = snd (Gauss_Jordan_upt_k_PA A (Suc k))
 3. \<And>k. \<lbrakk>fst (Gauss_Jordan_upt_k_det_P A k) = det (fst (Gauss_Jordan_upt_k_PA A k)); snd (Gauss_Jordan_upt_k_det_P A k) = snd (Gauss_Jordan_upt_k_PA A k); fst (snd (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc k])) = fst (snd (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc k]))\<rbrakk> \<Longrightarrow> fst (snd (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc (Suc k)])) = fst (snd (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc (Suc k)]))
[PROOF STEP]
have snd_snd: "snd (snd f) = snd (snd g)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. snd (snd f) = snd (snd g)
[PROOF STEP]
unfolding f_def g_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. snd (snd (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc k])) = snd (snd (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc k]))
[PROOF STEP]
using hyp2
[PROOF STATE]
proof (prove)
using this:
snd (Gauss_Jordan_upt_k_det_P A k) = snd (Gauss_Jordan_upt_k_PA A k)

goal (1 subgoal):
 1. snd (snd (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc k])) = snd (snd (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc k]))
[PROOF STEP]
unfolding Gauss_Jordan_upt_k_det_P_def Gauss_Jordan_upt_k_PA_def Let_def fst_conv snd_conv
[PROOF STATE]
proof (prove)
using this:
snd (snd (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc k])) = snd (snd (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc k]))

goal (1 subgoal):
 1. snd (snd (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc k])) = snd (snd (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc k]))
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
snd (snd f) = snd (snd g)

goal (3 subgoals):
 1. \<And>k. \<lbrakk>fst (Gauss_Jordan_upt_k_det_P A k) = det (fst (Gauss_Jordan_upt_k_PA A k)); snd (Gauss_Jordan_upt_k_det_P A k) = snd (Gauss_Jordan_upt_k_PA A k); fst (snd (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc k])) = fst (snd (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc k]))\<rbrakk> \<Longrightarrow> fst (Gauss_Jordan_upt_k_det_P A (Suc k)) = det (fst (Gauss_Jordan_upt_k_PA A (Suc k)))
 2. \<And>k. \<lbrakk>fst (Gauss_Jordan_upt_k_det_P A k) = det (fst (Gauss_Jordan_upt_k_PA A k)); snd (Gauss_Jordan_upt_k_det_P A k) = snd (Gauss_Jordan_upt_k_PA A k); fst (snd (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc k])) = fst (snd (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc k]))\<rbrakk> \<Longrightarrow> snd (Gauss_Jordan_upt_k_det_P A (Suc k)) = snd (Gauss_Jordan_upt_k_PA A (Suc k))
 3. \<And>k. \<lbrakk>fst (Gauss_Jordan_upt_k_det_P A k) = det (fst (Gauss_Jordan_upt_k_PA A k)); snd (Gauss_Jordan_upt_k_det_P A k) = snd (Gauss_Jordan_upt_k_PA A k); fst (snd (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc k])) = fst (snd (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc k]))\<rbrakk> \<Longrightarrow> fst (snd (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc (Suc k)])) = fst (snd (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc (Suc k)]))
[PROOF STEP]
have fst_det: "fst f = det (fst g)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst f = det (fst g)
[PROOF STEP]
unfolding f_def g_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc k]) = det (fst (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc k]))
[PROOF STEP]
using hyp1
[PROOF STATE]
proof (prove)
using this:
fst (Gauss_Jordan_upt_k_det_P A k) = det (fst (Gauss_Jordan_upt_k_PA A k))

goal (1 subgoal):
 1. fst (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc k]) = det (fst (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc k]))
[PROOF STEP]
unfolding Gauss_Jordan_upt_k_det_P_def Gauss_Jordan_upt_k_PA_def Let_def fst_conv
[PROOF STATE]
proof (prove)
using this:
fst (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc k]) = det (fst (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc k]))

goal (1 subgoal):
 1. fst (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc k]) = det (fst (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc k]))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
fst f = det (fst g)

goal (3 subgoals):
 1. \<And>k. \<lbrakk>fst (Gauss_Jordan_upt_k_det_P A k) = det (fst (Gauss_Jordan_upt_k_PA A k)); snd (Gauss_Jordan_upt_k_det_P A k) = snd (Gauss_Jordan_upt_k_PA A k); fst (snd (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc k])) = fst (snd (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc k]))\<rbrakk> \<Longrightarrow> fst (Gauss_Jordan_upt_k_det_P A (Suc k)) = det (fst (Gauss_Jordan_upt_k_PA A (Suc k)))
 2. \<And>k. \<lbrakk>fst (Gauss_Jordan_upt_k_det_P A k) = det (fst (Gauss_Jordan_upt_k_PA A k)); snd (Gauss_Jordan_upt_k_det_P A k) = snd (Gauss_Jordan_upt_k_PA A k); fst (snd (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc k])) = fst (snd (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc k]))\<rbrakk> \<Longrightarrow> snd (Gauss_Jordan_upt_k_det_P A (Suc k)) = snd (Gauss_Jordan_upt_k_PA A (Suc k))
 3. \<And>k. \<lbrakk>fst (Gauss_Jordan_upt_k_det_P A k) = det (fst (Gauss_Jordan_upt_k_PA A k)); snd (Gauss_Jordan_upt_k_det_P A k) = snd (Gauss_Jordan_upt_k_PA A k); fst (snd (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc k])) = fst (snd (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc k]))\<rbrakk> \<Longrightarrow> fst (snd (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc (Suc k)])) = fst (snd (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc (Suc k)]))
[PROOF STEP]
show "fst (snd (foldl Gauss_Jordan_column_k_det_P (1, 0, A) [0..<Suc k])) = fst (snd (foldl Gauss_Jordan_column_k_PA (mat 1, 0, A) [0..<Suc k])) \<Longrightarrow>
        fst (Gauss_Jordan_upt_k_det_P A (Suc k)) = det (fst (Gauss_Jordan_upt_k_PA A (Suc k)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst (snd (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc k])) = fst (snd (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc k])) \<Longrightarrow> fst (Gauss_Jordan_upt_k_det_P A (Suc k)) = det (fst (Gauss_Jordan_upt_k_PA A (Suc k)))
[PROOF STEP]
unfolding Gauss_Jordan_upt_k_det_P_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst (snd (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc k])) = fst (snd (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc k])) \<Longrightarrow> fst (let foldl = foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc (Suc k)] in (fst foldl, snd (snd foldl))) = det (fst (Gauss_Jordan_upt_k_PA A (Suc k)))
[PROOF STEP]
unfolding Gauss_Jordan_upt_k_PA_def Let_def fst_conv
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst (snd (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc k])) = fst (snd (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc k])) \<Longrightarrow> fst (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc (Suc k)]) = det (fst (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc (Suc k)]))
[PROOF STEP]
unfolding list_rw foldl_append
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst (snd (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc k])) = fst (snd (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc k])) \<Longrightarrow> fst (foldl Gauss_Jordan_column_k_det_P (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc k]) [Suc k]) = det (fst (foldl Gauss_Jordan_column_k_PA (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc k]) [Suc k]))
[PROOF STEP]
unfolding List.foldl.simps
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst (snd (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc k])) = fst (snd (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc k])) \<Longrightarrow> fst (Gauss_Jordan_column_k_det_P (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc k]) (Suc k)) = det (fst (Gauss_Jordan_column_k_PA (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc k]) (Suc k)))
[PROOF STEP]
unfolding f_def[symmetric] g_def[symmetric]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst (snd f) = fst (snd g) \<Longrightarrow> fst (Gauss_Jordan_column_k_det_P f (Suc k)) = det (fst (Gauss_Jordan_column_k_PA g (Suc k)))
[PROOF STEP]
apply (subst f_rw)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst (snd f) = fst (snd g) \<Longrightarrow> fst (Gauss_Jordan_column_k_det_P (fst f, fst (snd f), snd (snd f)) (Suc k)) = det (fst (Gauss_Jordan_column_k_PA g (Suc k)))
[PROOF STEP]
apply (subst g_rw)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst (snd f) = fst (snd g) \<Longrightarrow> fst (Gauss_Jordan_column_k_det_P (fst f, fst (snd f), snd (snd f)) (Suc k)) = det (fst (Gauss_Jordan_column_k_PA (fst g, fst (snd g), snd (snd g)) (Suc k)))
[PROOF STEP]
unfolding fst_snd snd_snd fst_det
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst (snd g) = fst (snd g) \<Longrightarrow> fst (Gauss_Jordan_column_k_det_P (det (fst g), fst (snd g), snd (snd g)) (Suc k)) = det (fst (Gauss_Jordan_column_k_PA (fst g, fst (snd g), snd (snd g)) (Suc k)))
[PROOF STEP]
by (rule det_fst_Gauss_Jordan_column_k_PA_eq_fst_Gauss_Jordan_column_k_det_P)
[PROOF STATE]
proof (state)
this:
fst (snd (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc k])) = fst (snd (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc k])) \<Longrightarrow> fst (Gauss_Jordan_upt_k_det_P A (Suc k)) = det (fst (Gauss_Jordan_upt_k_PA A (Suc k)))

goal (2 subgoals):
 1. \<And>k. \<lbrakk>fst (Gauss_Jordan_upt_k_det_P A k) = det (fst (Gauss_Jordan_upt_k_PA A k)); snd (Gauss_Jordan_upt_k_det_P A k) = snd (Gauss_Jordan_upt_k_PA A k); fst (snd (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc k])) = fst (snd (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc k]))\<rbrakk> \<Longrightarrow> snd (Gauss_Jordan_upt_k_det_P A (Suc k)) = snd (Gauss_Jordan_upt_k_PA A (Suc k))
 2. \<And>k. \<lbrakk>fst (Gauss_Jordan_upt_k_det_P A k) = det (fst (Gauss_Jordan_upt_k_PA A k)); snd (Gauss_Jordan_upt_k_det_P A k) = snd (Gauss_Jordan_upt_k_PA A k); fst (snd (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc k])) = fst (snd (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc k]))\<rbrakk> \<Longrightarrow> fst (snd (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc (Suc k)])) = fst (snd (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc (Suc k)]))
[PROOF STEP]
show "snd (Gauss_Jordan_upt_k_det_P A (Suc k)) = snd (Gauss_Jordan_upt_k_PA A (Suc k))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. snd (Gauss_Jordan_upt_k_det_P A (Suc k)) = snd (Gauss_Jordan_upt_k_PA A (Suc k))
[PROOF STEP]
unfolding Gauss_Jordan_upt_k_det_P_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. snd (let foldl = foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc (Suc k)] in (fst foldl, snd (snd foldl))) = snd (Gauss_Jordan_upt_k_PA A (Suc k))
[PROOF STEP]
unfolding Gauss_Jordan_upt_k_PA_def Let_def fst_conv
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. snd (fst (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc (Suc k)]), snd (snd (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc (Suc k)]))) = snd (fst (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc (Suc k)]), snd (snd (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc (Suc k)])))
[PROOF STEP]
unfolding list_rw foldl_append
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. snd (fst (foldl Gauss_Jordan_column_k_det_P (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc k]) [Suc k]), snd (snd (foldl Gauss_Jordan_column_k_det_P (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc k]) [Suc k]))) = snd (fst (foldl Gauss_Jordan_column_k_PA (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc k]) [Suc k]), snd (snd (foldl Gauss_Jordan_column_k_PA (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc k]) [Suc k])))
[PROOF STEP]
unfolding List.foldl.simps
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. snd (fst (Gauss_Jordan_column_k_det_P (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc k]) (Suc k)), snd (snd (Gauss_Jordan_column_k_det_P (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc k]) (Suc k)))) = snd (fst (Gauss_Jordan_column_k_PA (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc k]) (Suc k)), snd (snd (Gauss_Jordan_column_k_PA (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc k]) (Suc k))))
[PROOF STEP]
unfolding f_def[symmetric] g_def[symmetric]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. snd (fst (Gauss_Jordan_column_k_det_P f (Suc k)), snd (snd (Gauss_Jordan_column_k_det_P f (Suc k)))) = snd (fst (Gauss_Jordan_column_k_PA g (Suc k)), snd (snd (Gauss_Jordan_column_k_PA g (Suc k))))
[PROOF STEP]
apply (subst f_rw)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. snd (fst (Gauss_Jordan_column_k_det_P (fst f, fst (snd f), snd (snd f)) (Suc k)), snd (snd (Gauss_Jordan_column_k_det_P f (Suc k)))) = snd (fst (Gauss_Jordan_column_k_PA g (Suc k)), snd (snd (Gauss_Jordan_column_k_PA g (Suc k))))
[PROOF STEP]
apply (subst g_rw)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. snd (fst (Gauss_Jordan_column_k_det_P (fst f, fst (snd f), snd (snd f)) (Suc k)), snd (snd (Gauss_Jordan_column_k_det_P f (Suc k)))) = snd (fst (Gauss_Jordan_column_k_PA (fst g, fst (snd g), snd (snd g)) (Suc k)), snd (snd (Gauss_Jordan_column_k_PA g (Suc k))))
[PROOF STEP]
unfolding fst_snd snd_snd fst_det
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. snd (fst (Gauss_Jordan_column_k_det_P (det (fst g), fst (snd g), snd (snd g)) (Suc k)), snd (snd (Gauss_Jordan_column_k_det_P f (Suc k)))) = snd (fst (Gauss_Jordan_column_k_PA (fst g, fst (snd g), snd (snd g)) (Suc k)), snd (snd (Gauss_Jordan_column_k_PA g (Suc k))))
[PROOF STEP]
by (metis fst_snd prod.collapse snd_Gauss_Jordan_column_k_det_P_is_snd_Gauss_Jordan_column_k_PA snd_eqD snd_snd)
[PROOF STATE]
proof (state)
this:
snd (Gauss_Jordan_upt_k_det_P A (Suc k)) = snd (Gauss_Jordan_upt_k_PA A (Suc k))

goal (1 subgoal):
 1. \<And>k. \<lbrakk>fst (Gauss_Jordan_upt_k_det_P A k) = det (fst (Gauss_Jordan_upt_k_PA A k)); snd (Gauss_Jordan_upt_k_det_P A k) = snd (Gauss_Jordan_upt_k_PA A k); fst (snd (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc k])) = fst (snd (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc k]))\<rbrakk> \<Longrightarrow> fst (snd (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc (Suc k)])) = fst (snd (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc (Suc k)]))
[PROOF STEP]
show "fst (snd (foldl Gauss_Jordan_column_k_det_P (1, 0, A) [0..<Suc (Suc k)])) = fst (snd (foldl Gauss_Jordan_column_k_PA (mat 1, 0, A) [0..<Suc (Suc k)]))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst (snd (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc (Suc k)])) = fst (snd (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc (Suc k)]))
[PROOF STEP]
unfolding Gauss_Jordan_upt_k_det_P_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst (snd (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc (Suc k)])) = fst (snd (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc (Suc k)]))
[PROOF STEP]
unfolding Gauss_Jordan_upt_k_PA_def Let_def fst_conv
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst (snd (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc (Suc k)])) = fst (snd (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc (Suc k)]))
[PROOF STEP]
unfolding list_rw foldl_append
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst (snd (foldl Gauss_Jordan_column_k_det_P (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc k]) [Suc k])) = fst (snd (foldl Gauss_Jordan_column_k_PA (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc k]) [Suc k]))
[PROOF STEP]
unfolding List.foldl.simps
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst (snd (Gauss_Jordan_column_k_det_P (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc k]) (Suc k))) = fst (snd (Gauss_Jordan_column_k_PA (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc k]) (Suc k)))
[PROOF STEP]
unfolding f_def[symmetric] g_def[symmetric]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst (snd (Gauss_Jordan_column_k_det_P f (Suc k))) = fst (snd (Gauss_Jordan_column_k_PA g (Suc k)))
[PROOF STEP]
apply (subst f_rw)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst (snd (Gauss_Jordan_column_k_det_P (fst f, fst (snd f), snd (snd f)) (Suc k))) = fst (snd (Gauss_Jordan_column_k_PA g (Suc k)))
[PROOF STEP]
apply (subst g_rw)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst (snd (Gauss_Jordan_column_k_det_P (fst f, fst (snd f), snd (snd f)) (Suc k))) = fst (snd (Gauss_Jordan_column_k_PA (fst g, fst (snd g), snd (snd g)) (Suc k)))
[PROOF STEP]
unfolding fst_snd snd_snd fst_det
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst (snd (Gauss_Jordan_column_k_det_P (det (fst g), fst (snd g), snd (snd g)) (Suc k))) = fst (snd (Gauss_Jordan_column_k_PA (fst g, fst (snd g), snd (snd g)) (Suc k)))
[PROOF STEP]
by (rule fst_snd_Gauss_Jordan_column_k_det_P_eq_fst_snd_Gauss_Jordan_column_k_PA)
[PROOF STATE]
proof (state)
this:
fst (snd (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc (Suc k)])) = fst (snd (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc (Suc k)]))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma r_delay:
  "eval r_delay [i, x] \<down>=
    (if \<exists>j<e_length x. the (eval r_result1 [e_length x, i, e_take (Suc j) x]) > 0
     then Suc (GREATEST j.
        j < e_length x \<and> the (eval r_result1 [e_length x, i, e_take (Suc j) x]) > 0)
     else 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval r_delay [i, x] \<down>= (if \<exists>j<e_length x. 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x]) then Suc (GREATEST j. j < e_length x \<and> 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x])) else 0)
[PROOF STEP]
unfolding r_delay_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval (Cn 2 r_delay_aux [Cn 2 r_length [recf.Id 2 1], recf.Id 2 0, recf.Id 2 1]) [i, x] \<down>= (if \<exists>j<e_length x. 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x]) then Suc (GREATEST j. j < e_length x \<and> 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x])) else 0)
[PROOF STEP]
using r_delay_aux r_delay_aux_prim
[PROOF STATE]
proof (prove)
using this:
?n \<le> e_length ?x \<Longrightarrow> eval r_delay_aux [?n, ?i, ?x] \<down>= (if \<exists>j<?n. 0 < the (eval r_result1 [e_length ?x, ?i, e_take (Suc j) ?x]) then Suc (GREATEST j. j < ?n \<and> 0 < the (eval r_result1 [e_length ?x, ?i, e_take (Suc j) ?x])) else 0)
prim_recfn 3 r_delay_aux

goal (1 subgoal):
 1. eval (Cn 2 r_delay_aux [Cn 2 r_length [recf.Id 2 1], recf.Id 2 0, recf.Id 2 1]) [i, x] \<down>= (if \<exists>j<e_length x. 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x]) then Suc (GREATEST j. j < e_length x \<and> 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x])) else 0)
[PROOF STEP]
by simp


[STATEMENT]
lemma r_limr_recfn: "recfn 1 r_limr"
  and r_limr_total: "total r_limr"
  and r_limr:
    "\<phi> (the (eval r_limr [i])) \<in> \<R>"
    "learn_lim \<psi> U (\<phi> i) \<Longrightarrow> learn_lim \<psi> U (\<phi> (the (eval r_limr [i])))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. recfn 1 r_limr &&& Partial_Recursive.total r_limr &&& \<phi> (the (eval r_limr [i])) \<in> \<R> &&& (learn_lim \<psi> U (\<phi> i) \<Longrightarrow> learn_lim \<psi> U (\<phi> (the (eval r_limr [i]))))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. recfn 1 r_limr
 2. Partial_Recursive.total r_limr
 3. \<phi> (the (eval r_limr [i])) \<in> \<R>
 4. learn_lim \<psi> U (\<phi> i) \<Longrightarrow> learn_lim \<psi> U (\<phi> (the (eval r_limr [i])))
[PROOF STEP]
let ?P = "\<lambda>g.
    g \<in> \<R> \<and>
    (\<forall>i. \<phi> (the (g i)) \<in> \<R> \<and> (\<forall>U \<psi>. learn_lim \<psi> U (\<phi> i) \<longrightarrow> learn_lim \<psi> U (\<phi> (the (g i)))))"
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. recfn 1 r_limr
 2. Partial_Recursive.total r_limr
 3. \<phi> (the (eval r_limr [i])) \<in> \<R>
 4. learn_lim \<psi> U (\<phi> i) \<Longrightarrow> learn_lim \<psi> U (\<phi> (the (eval r_limr [i])))
[PROOF STEP]
let ?Q = "\<lambda>g.
    recfn 1 g \<and>
    total g \<and>
    (\<forall>i. \<phi> (the (eval g [i])) \<in> \<R> \<and>
       (\<forall>U \<psi>. learn_lim \<psi> U (\<phi> i) \<longrightarrow> learn_lim \<psi> U (\<phi> (the (eval g [i])))))"
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. recfn 1 r_limr
 2. Partial_Recursive.total r_limr
 3. \<phi> (the (eval r_limr [i])) \<in> \<R>
 4. learn_lim \<psi> U (\<phi> i) \<Longrightarrow> learn_lim \<psi> U (\<phi> (the (eval r_limr [i])))
[PROOF STEP]
have "\<exists>g. ?P g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>g. g \<in> \<R> \<and> (\<forall>i. \<phi> (the (g i)) \<in> \<R> \<and> (\<forall>U \<psi>. learn_lim \<psi> U (\<phi> i) \<longrightarrow> learn_lim \<psi> U (\<phi> (the (g i)))))
[PROOF STEP]
using lemma_R_for_Lim_effective
[PROOF STATE]
proof (prove)
using this:
\<exists>g\<in>\<R>. \<forall>i. \<phi> (the (g i)) \<in> \<R> \<and> (\<forall>U \<psi>. learn_lim \<psi> U (\<phi> i) \<longrightarrow> learn_lim \<psi> U (\<phi> (the (g i))))

goal (1 subgoal):
 1. \<exists>g. g \<in> \<R> \<and> (\<forall>i. \<phi> (the (g i)) \<in> \<R> \<and> (\<forall>U \<psi>. learn_lim \<psi> U (\<phi> i) \<longrightarrow> learn_lim \<psi> U (\<phi> (the (g i)))))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>g. g \<in> \<R> \<and> (\<forall>i. \<phi> (the (g i)) \<in> \<R> \<and> (\<forall>U \<psi>. learn_lim \<psi> U (\<phi> i) \<longrightarrow> learn_lim \<psi> U (\<phi> (the (g i)))))

goal (4 subgoals):
 1. recfn 1 r_limr
 2. Partial_Recursive.total r_limr
 3. \<phi> (the (eval r_limr [i])) \<in> \<R>
 4. learn_lim \<psi> U (\<phi> i) \<Longrightarrow> learn_lim \<psi> U (\<phi> (the (eval r_limr [i])))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>g. g \<in> \<R> \<and> (\<forall>i. \<phi> (the (g i)) \<in> \<R> \<and> (\<forall>U \<psi>. learn_lim \<psi> U (\<phi> i) \<longrightarrow> learn_lim \<psi> U (\<phi> (the (g i)))))
[PROOF STEP]
obtain g where "?P g"
[PROOF STATE]
proof (prove)
using this:
\<exists>g. g \<in> \<R> \<and> (\<forall>i. \<phi> (the (g i)) \<in> \<R> \<and> (\<forall>U \<psi>. learn_lim \<psi> U (\<phi> i) \<longrightarrow> learn_lim \<psi> U (\<phi> (the (g i)))))

goal (1 subgoal):
 1. (\<And>g. g \<in> \<R> \<and> (\<forall>i. \<phi> (the (g i)) \<in> \<R> \<and> (\<forall>U \<psi>. learn_lim \<psi> U (\<phi> i) \<longrightarrow> learn_lim \<psi> U (\<phi> (the (g i))))) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
g \<in> \<R> \<and> (\<forall>i. \<phi> (the (g i)) \<in> \<R> \<and> (\<forall>U \<psi>. learn_lim \<psi> U (\<phi> i) \<longrightarrow> learn_lim \<psi> U (\<phi> (the (g i)))))

goal (4 subgoals):
 1. recfn 1 r_limr
 2. Partial_Recursive.total r_limr
 3. \<phi> (the (eval r_limr [i])) \<in> \<R>
 4. learn_lim \<psi> U (\<phi> i) \<Longrightarrow> learn_lim \<psi> U (\<phi> (the (eval r_limr [i])))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
g \<in> \<R> \<and> (\<forall>i. \<phi> (the (g i)) \<in> \<R> \<and> (\<forall>U \<psi>. learn_lim \<psi> U (\<phi> i) \<longrightarrow> learn_lim \<psi> U (\<phi> (the (g i)))))
[PROOF STEP]
obtain g' where g': "recfn 1 g'" "total g'" "\<forall>i. eval g' [i] = g i"
[PROOF STATE]
proof (prove)
using this:
g \<in> \<R> \<and> (\<forall>i. \<phi> (the (g i)) \<in> \<R> \<and> (\<forall>U \<psi>. learn_lim \<psi> U (\<phi> i) \<longrightarrow> learn_lim \<psi> U (\<phi> (the (g i)))))

goal (1 subgoal):
 1. (\<And>g'. \<lbrakk>recfn 1 g'; Partial_Recursive.total g'; \<forall>i. eval g' [i] = g i\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
recfn 1 g'
Partial_Recursive.total g'
\<forall>i. eval g' [i] = g i

goal (4 subgoals):
 1. recfn 1 r_limr
 2. Partial_Recursive.total r_limr
 3. \<phi> (the (eval r_limr [i])) \<in> \<R>
 4. learn_lim \<psi> U (\<phi> i) \<Longrightarrow> learn_lim \<psi> U (\<phi> (the (eval r_limr [i])))
[PROOF STEP]
with \<open>?P g\<close>
[PROOF STATE]
proof (chain)
picking this:
g \<in> \<R> \<and> (\<forall>i. \<phi> (the (g i)) \<in> \<R> \<and> (\<forall>U \<psi>. learn_lim \<psi> U (\<phi> i) \<longrightarrow> learn_lim \<psi> U (\<phi> (the (g i)))))
recfn 1 g'
Partial_Recursive.total g'
\<forall>i. eval g' [i] = g i
[PROOF STEP]
have "?Q g'"
[PROOF STATE]
proof (prove)
using this:
g \<in> \<R> \<and> (\<forall>i. \<phi> (the (g i)) \<in> \<R> \<and> (\<forall>U \<psi>. learn_lim \<psi> U (\<phi> i) \<longrightarrow> learn_lim \<psi> U (\<phi> (the (g i)))))
recfn 1 g'
Partial_Recursive.total g'
\<forall>i. eval g' [i] = g i

goal (1 subgoal):
 1. recfn 1 g' \<and> Partial_Recursive.total g' \<and> (\<forall>i. \<phi> (the (eval g' [i])) \<in> \<R> \<and> (\<forall>U \<psi>. learn_lim \<psi> U (\<phi> i) \<longrightarrow> learn_lim \<psi> U (\<phi> (the (eval g' [i])))))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
recfn 1 g' \<and> Partial_Recursive.total g' \<and> (\<forall>i. \<phi> (the (eval g' [i])) \<in> \<R> \<and> (\<forall>U \<psi>. learn_lim \<psi> U (\<phi> i) \<longrightarrow> learn_lim \<psi> U (\<phi> (the (eval g' [i])))))

goal (4 subgoals):
 1. recfn 1 r_limr
 2. Partial_Recursive.total r_limr
 3. \<phi> (the (eval r_limr [i])) \<in> \<R>
 4. learn_lim \<psi> U (\<phi> i) \<Longrightarrow> learn_lim \<psi> U (\<phi> (the (eval r_limr [i])))
[PROOF STEP]
with r_limr_def someI_ex[of ?Q]
[PROOF STATE]
proof (chain)
picking this:
r_limr \<equiv> SOME g. recfn 1 g \<and> Partial_Recursive.total g \<and> (\<forall>i. \<phi> (the (eval g [i])) \<in> \<R> \<and> (\<forall>U \<psi>. learn_lim \<psi> U (\<phi> i) \<longrightarrow> learn_lim \<psi> U (\<phi> (the (eval g [i])))))
\<exists>x. recfn 1 x \<and> Partial_Recursive.total x \<and> (\<forall>i. \<phi> (the (eval x [i])) \<in> \<R> \<and> (\<forall>U \<psi>. learn_lim \<psi> U (\<phi> i) \<longrightarrow> learn_lim \<psi> U (\<phi> (the (eval x [i]))))) \<Longrightarrow> recfn 1 (SOME x. recfn 1 x \<and> Partial_Recursive.total x \<and> (\<forall>i. \<phi> (the (eval x [i])) \<in> \<R> \<and> (\<forall>U \<psi>. learn_lim \<psi> U (\<phi> i) \<longrightarrow> learn_lim \<psi> U (\<phi> (the (eval x [i])))))) \<and> Partial_Recursive.total (SOME x. recfn 1 x \<and> Partial_Recursive.total x \<and> (\<forall>i. \<phi> (the (eval x [i])) \<in> \<R> \<and> (\<forall>U \<psi>. learn_lim \<psi> U (\<phi> i) \<longrightarrow> learn_lim \<psi> U (\<phi> (the (eval x [i])))))) \<and> (\<forall>i. \<phi> (the (eval (SOME x. recfn 1 x \<and> Partial_Recursive.total x \<and> (\<forall>i. \<phi> (the (eval x [i])) \<in> \<R> \<and> (\<forall>U \<psi>. learn_lim \<psi> U (\<phi> i) \<longrightarrow> learn_lim \<psi> U (\<phi> (the (eval x [i])))))) [i])) \<in> \<R> \<and> (\<forall>U \<psi>. learn_lim \<psi> U (\<phi> i) \<longrightarrow> learn_lim \<psi> U (\<phi> (the (eval (SOME x. recfn 1 x \<and> Partial_Recursive.total x \<and> (\<forall>i. \<phi> (the (eval x [i])) \<in> \<R> \<and> (\<forall>U \<psi>. learn_lim \<psi> U (\<phi> i) \<longrightarrow> learn_lim \<psi> U (\<phi> (the (eval x [i])))))) [i])))))
recfn 1 g' \<and> Partial_Recursive.total g' \<and> (\<forall>i. \<phi> (the (eval g' [i])) \<in> \<R> \<and> (\<forall>U \<psi>. learn_lim \<psi> U (\<phi> i) \<longrightarrow> learn_lim \<psi> U (\<phi> (the (eval g' [i])))))
[PROOF STEP]
show
    "recfn 1 r_limr"
    "total r_limr"
    "\<phi> (the (eval r_limr [i])) \<in> \<R>"
    "learn_lim \<psi> U (\<phi> i) \<Longrightarrow> learn_lim \<psi> U (\<phi> (the (eval r_limr [i])))"
[PROOF STATE]
proof (prove)
using this:
r_limr \<equiv> SOME g. recfn 1 g \<and> Partial_Recursive.total g \<and> (\<forall>i. \<phi> (the (eval g [i])) \<in> \<R> \<and> (\<forall>U \<psi>. learn_lim \<psi> U (\<phi> i) \<longrightarrow> learn_lim \<psi> U (\<phi> (the (eval g [i])))))
\<exists>x. recfn 1 x \<and> Partial_Recursive.total x \<and> (\<forall>i. \<phi> (the (eval x [i])) \<in> \<R> \<and> (\<forall>U \<psi>. learn_lim \<psi> U (\<phi> i) \<longrightarrow> learn_lim \<psi> U (\<phi> (the (eval x [i]))))) \<Longrightarrow> recfn 1 (SOME x. recfn 1 x \<and> Partial_Recursive.total x \<and> (\<forall>i. \<phi> (the (eval x [i])) \<in> \<R> \<and> (\<forall>U \<psi>. learn_lim \<psi> U (\<phi> i) \<longrightarrow> learn_lim \<psi> U (\<phi> (the (eval x [i])))))) \<and> Partial_Recursive.total (SOME x. recfn 1 x \<and> Partial_Recursive.total x \<and> (\<forall>i. \<phi> (the (eval x [i])) \<in> \<R> \<and> (\<forall>U \<psi>. learn_lim \<psi> U (\<phi> i) \<longrightarrow> learn_lim \<psi> U (\<phi> (the (eval x [i])))))) \<and> (\<forall>i. \<phi> (the (eval (SOME x. recfn 1 x \<and> Partial_Recursive.total x \<and> (\<forall>i. \<phi> (the (eval x [i])) \<in> \<R> \<and> (\<forall>U \<psi>. learn_lim \<psi> U (\<phi> i) \<longrightarrow> learn_lim \<psi> U (\<phi> (the (eval x [i])))))) [i])) \<in> \<R> \<and> (\<forall>U \<psi>. learn_lim \<psi> U (\<phi> i) \<longrightarrow> learn_lim \<psi> U (\<phi> (the (eval (SOME x. recfn 1 x \<and> Partial_Recursive.total x \<and> (\<forall>i. \<phi> (the (eval x [i])) \<in> \<R> \<and> (\<forall>U \<psi>. learn_lim \<psi> U (\<phi> i) \<longrightarrow> learn_lim \<psi> U (\<phi> (the (eval x [i])))))) [i])))))
recfn 1 g' \<and> Partial_Recursive.total g' \<and> (\<forall>i. \<phi> (the (eval g' [i])) \<in> \<R> \<and> (\<forall>U \<psi>. learn_lim \<psi> U (\<phi> i) \<longrightarrow> learn_lim \<psi> U (\<phi> (the (eval g' [i])))))

goal (1 subgoal):
 1. (recfn 1 r_limr &&& Partial_Recursive.total r_limr) &&& \<phi> (the (eval r_limr [i])) \<in> \<R> &&& (learn_lim \<psi> U (\<phi> i) \<Longrightarrow> learn_lim \<psi> U (\<phi> (the (eval r_limr [i]))))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
recfn 1 r_limr
Partial_Recursive.total r_limr
\<phi> (the (eval r_limr [i])) \<in> \<R>
learn_lim \<psi> U (\<phi> i) \<Longrightarrow> learn_lim \<psi> U (\<phi> (the (eval r_limr [i])))

goal:
No subgoals!
[PROOF STEP]
qed