[STATEMENT]
lemma oseq_broadcastTE [elim]:
  "\<lbrakk>((\<sigma>, {l}broadcast(s\<^sub>m\<^sub>s\<^sub>g). p), a, (\<sigma>', q)) \<in> oseqp_sos \<Gamma> i;
    \<lbrakk>a = broadcast (s\<^sub>m\<^sub>s\<^sub>g (\<sigma> i)); \<sigma>' i = \<sigma> i; q = p\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>((\<sigma>, {l}broadcast(s\<^sub>m\<^sub>s\<^sub>g) .
p), a, \<sigma>', q) \<in> oseqp_sos \<Gamma> i; \<lbrakk>a = broadcast (s\<^sub>m\<^sub>s\<^sub>g (\<sigma> i)); \<sigma>' i = \<sigma> i; q = p\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P
[PROOF STEP]
by (ind_cases "((\<sigma>, {l}broadcast(s\<^sub>m\<^sub>s\<^sub>g). p), a, (\<sigma>', q)) \<in> oseqp_sos \<Gamma> i") simp


[STATEMENT]
lemma oseq_groupcastTE [elim]:
  "\<lbrakk>((\<sigma>, {l}groupcast(s\<^sub>i\<^sub>p\<^sub>s, s\<^sub>m\<^sub>s\<^sub>g). p), a, (\<sigma>', q)) \<in> oseqp_sos \<Gamma> i;
    \<lbrakk>a = groupcast (s\<^sub>i\<^sub>p\<^sub>s (\<sigma> i)) (s\<^sub>m\<^sub>s\<^sub>g (\<sigma> i)); \<sigma>' i = \<sigma> i; q = p\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>((\<sigma>, {l}groupcast(s\<^sub>i\<^sub>p\<^sub>s, s\<^sub>m\<^sub>s\<^sub>g) .
p), a, \<sigma>', q) \<in> oseqp_sos \<Gamma> i; \<lbrakk>a = groupcast (s\<^sub>i\<^sub>p\<^sub>s (\<sigma> i)) (s\<^sub>m\<^sub>s\<^sub>g (\<sigma> i)); \<sigma>' i = \<sigma> i; q = p\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P
[PROOF STEP]
by (ind_cases "((\<sigma>, {l}groupcast(s\<^sub>i\<^sub>p\<^sub>s, s\<^sub>m\<^sub>s\<^sub>g). p), a, (\<sigma>', q)) \<in> oseqp_sos \<Gamma> i") simp


[STATEMENT]
lemma oseq_unicastTE [elim]:
  "\<lbrakk>((\<sigma>, {l}unicast(s\<^sub>i\<^sub>p, s\<^sub>m\<^sub>s\<^sub>g). p \<triangleright> q), a, (\<sigma>', r)) \<in> oseqp_sos \<Gamma> i;
    \<lbrakk>a = unicast (s\<^sub>i\<^sub>p (\<sigma> i)) (s\<^sub>m\<^sub>s\<^sub>g (\<sigma> i)); \<sigma>' i = \<sigma> i; r = p\<rbrakk> \<Longrightarrow> P;
    \<lbrakk>a = \<not>unicast (s\<^sub>i\<^sub>p (\<sigma> i)); \<sigma>' i = \<sigma> i; r = q\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>((\<sigma>, {l}unicast(s\<^sub>i\<^sub>p, s\<^sub>m\<^sub>s\<^sub>g) .
p \<triangleright> q), a, \<sigma>', r) \<in> oseqp_sos \<Gamma> i; \<lbrakk>a = unicast (s\<^sub>i\<^sub>p (\<sigma> i)) (s\<^sub>m\<^sub>s\<^sub>g (\<sigma> i)); \<sigma>' i = \<sigma> i; r = p\<rbrakk> \<Longrightarrow> P; \<lbrakk>a = \<not>unicast (s\<^sub>i\<^sub>p (\<sigma> i)); \<sigma>' i = \<sigma> i; r = q\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P
[PROOF STEP]
by (ind_cases "((\<sigma>, {l}unicast(s\<^sub>i\<^sub>p, s\<^sub>m\<^sub>s\<^sub>g). p \<triangleright> q), a, (\<sigma>', r)) \<in> oseqp_sos \<Gamma> i") simp_all


[STATEMENT]
lemma oseq_sendTE [elim]:
  "\<lbrakk>((\<sigma>, {l}send(s\<^sub>m\<^sub>s\<^sub>g). p), a, (\<sigma>', q)) \<in> oseqp_sos \<Gamma> i;
    \<lbrakk>a = send (s\<^sub>m\<^sub>s\<^sub>g (\<sigma> i)); \<sigma>' i = \<sigma> i; q = p\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>((\<sigma>, {l}send(s\<^sub>m\<^sub>s\<^sub>g) .
p), a, \<sigma>', q) \<in> oseqp_sos \<Gamma> i; \<lbrakk>a = send (s\<^sub>m\<^sub>s\<^sub>g (\<sigma> i)); \<sigma>' i = \<sigma> i; q = p\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P
[PROOF STEP]
by (ind_cases "((\<sigma>, {l}send(s\<^sub>m\<^sub>s\<^sub>g). p), a, (\<sigma>', q)) \<in> oseqp_sos \<Gamma> i") simp


[STATEMENT]
lemma oseq_deliverTE [elim]:
  "\<lbrakk>((\<sigma>, {l}deliver(s\<^sub>d\<^sub>a\<^sub>t\<^sub>a). p), a, (\<sigma>', q)) \<in> oseqp_sos \<Gamma> i;
    \<lbrakk>a = deliver (s\<^sub>d\<^sub>a\<^sub>t\<^sub>a (\<sigma> i)); \<sigma>' i = \<sigma> i; q = p\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>((\<sigma>, {l}deliver(s\<^sub>d\<^sub>a\<^sub>t\<^sub>a) .
p), a, \<sigma>', q) \<in> oseqp_sos \<Gamma> i; \<lbrakk>a = deliver (s\<^sub>d\<^sub>a\<^sub>t\<^sub>a (\<sigma> i)); \<sigma>' i = \<sigma> i; q = p\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P
[PROOF STEP]
by (ind_cases "((\<sigma>, {l}deliver(s\<^sub>d\<^sub>a\<^sub>t\<^sub>a). p), a, (\<sigma>', q)) \<in> oseqp_sos \<Gamma> i") simp


[STATEMENT]
lemma oseq_receiveTE [elim]:
  "\<lbrakk>((\<sigma>, {l}receive(u\<^sub>m\<^sub>s\<^sub>g). p), a, (\<sigma>', q)) \<in> oseqp_sos \<Gamma> i;
    \<And>msg. \<lbrakk>a = receive msg; \<sigma>' i = u\<^sub>m\<^sub>s\<^sub>g msg (\<sigma> i); q = p\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>((\<sigma>, {l}receive(u\<^sub>m\<^sub>s\<^sub>g) .
p), a, \<sigma>', q) \<in> oseqp_sos \<Gamma> i; \<And>msg. \<lbrakk>a = receive msg; \<sigma>' i = u\<^sub>m\<^sub>s\<^sub>g msg (\<sigma> i); q = p\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P
[PROOF STEP]
by (ind_cases "((\<sigma>, {l}receive(u\<^sub>m\<^sub>s\<^sub>g). p), a, (\<sigma>', q)) \<in> oseqp_sos \<Gamma> i") simp


[STATEMENT]
lemma oseq_assignTE [elim]:
  "\<lbrakk>((\<sigma>, {l}\<lbrakk>u\<rbrakk> p), a, (\<sigma>', q)) \<in> oseqp_sos \<Gamma> i; \<lbrakk>a = \<tau>; \<sigma>' i = u (\<sigma> i); q = p\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>((\<sigma>, {l}\<lbrakk>u\<rbrakk>
p), a, \<sigma>', q) \<in> oseqp_sos \<Gamma> i; \<lbrakk>a = \<tau>; \<sigma>' i = u (\<sigma> i); q = p\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P
[PROOF STEP]
by (ind_cases "((\<sigma>, {l}\<lbrakk>u\<rbrakk> p), a, (\<sigma>', q)) \<in> oseqp_sos \<Gamma> i") simp


[STATEMENT]
lemma oseq_guardTE [elim]:
  "\<lbrakk>((\<sigma>, {l}\<langle>g\<rangle> p), a, (\<sigma>', q)) \<in> oseqp_sos \<Gamma> i; \<lbrakk>a = \<tau>; \<sigma>' i \<in> g (\<sigma> i); q = p\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>((\<sigma>, {l}\<langle>g\<rangle>
p), a, \<sigma>', q) \<in> oseqp_sos \<Gamma> i; \<lbrakk>a = \<tau>; \<sigma>' i \<in> g (\<sigma> i); q = p\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P
[PROOF STEP]
by (ind_cases "((\<sigma>, {l}\<langle>g\<rangle> p), a, (\<sigma>', q)) \<in> oseqp_sos \<Gamma> i") simp


[STATEMENT]
lemma opar_broadcastTE [elim]:
  "\<lbrakk>((\<sigma>, (s, t)), broadcast m, (\<sigma>', (s', t'))) \<in> oparp_sos i S T;
    \<lbrakk>((\<sigma>, s), broadcast m, (\<sigma>', s')) \<in> S; t' = t\<rbrakk> \<Longrightarrow> P;
    \<lbrakk>(t, broadcast m, t') \<in> T; s' = s; \<sigma>' i = \<sigma> i\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>((\<sigma>, s, t), broadcast m, \<sigma>', s', t') \<in> oparp_sos i S T; \<lbrakk>((\<sigma>, s), broadcast m, \<sigma>', s') \<in> S; t' = t\<rbrakk> \<Longrightarrow> P; \<lbrakk>(t, broadcast m, t') \<in> T; s' = s; \<sigma>' i = \<sigma> i\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P
[PROOF STEP]
by (ind_cases "((\<sigma>, (s, t)), broadcast m, (\<sigma>', (s', t'))) \<in> oparp_sos i S T") simp_all


[STATEMENT]
lemma opar_groupcastTE [elim]:
  "\<lbrakk>((\<sigma>, (s, t)), groupcast ips m, (\<sigma>', (s', t'))) \<in> oparp_sos i S T;
    \<lbrakk>((\<sigma>, s), groupcast ips m, (\<sigma>', s')) \<in> S; t' = t\<rbrakk> \<Longrightarrow> P;
    \<lbrakk>(t, groupcast ips m, t') \<in> T; s' = s; \<sigma>' i = \<sigma> i\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>((\<sigma>, s, t), groupcast ips m, \<sigma>', s', t') \<in> oparp_sos i S T; \<lbrakk>((\<sigma>, s), groupcast ips m, \<sigma>', s') \<in> S; t' = t\<rbrakk> \<Longrightarrow> P; \<lbrakk>(t, groupcast ips m, t') \<in> T; s' = s; \<sigma>' i = \<sigma> i\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P
[PROOF STEP]
by (ind_cases "((\<sigma>, (s, t)), groupcast ips m, (\<sigma>', (s', t'))) \<in> oparp_sos i S T") simp_all


[STATEMENT]
lemma opar_unicastTE [elim]:
  "\<lbrakk>((\<sigma>, (s, t)), unicast i m, (\<sigma>', (s', t'))) \<in> oparp_sos i S T;
    \<lbrakk>((\<sigma>, s), unicast i m, (\<sigma>', s')) \<in> S; t' = t\<rbrakk> \<Longrightarrow> P;
    \<lbrakk>(t, unicast i m, t') \<in> T; s' = s; \<sigma>' i = \<sigma> i\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>((\<sigma>, s, t), unicast i m, \<sigma>', s', t') \<in> oparp_sos i S T; \<lbrakk>((\<sigma>, s), unicast i m, \<sigma>', s') \<in> S; t' = t\<rbrakk> \<Longrightarrow> P; \<lbrakk>(t, unicast i m, t') \<in> T; s' = s; \<sigma>' i = \<sigma> i\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P
[PROOF STEP]
by (ind_cases "((\<sigma>, (s, t)), unicast i m, (\<sigma>', (s', t'))) \<in> oparp_sos i S T") simp_all


[STATEMENT]
lemma opar_notunicastTE [elim]:
  "\<lbrakk>((\<sigma>, (s, t)), notunicast i, (\<sigma>', (s', t'))) \<in> oparp_sos i S T;
    \<lbrakk>((\<sigma>, s), notunicast i, (\<sigma>', s')) \<in> S; t' = t\<rbrakk> \<Longrightarrow> P;
    \<lbrakk>(t, notunicast i, t') \<in> T; s' = s; \<sigma>' i = \<sigma> i\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>((\<sigma>, s, t), \<not>unicast i, \<sigma>', s', t') \<in> oparp_sos i S T; \<lbrakk>((\<sigma>, s), \<not>unicast i, \<sigma>', s') \<in> S; t' = t\<rbrakk> \<Longrightarrow> P; \<lbrakk>(t, \<not>unicast i, t') \<in> T; s' = s; \<sigma>' i = \<sigma> i\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P
[PROOF STEP]
by (ind_cases "((\<sigma>, (s, t)), notunicast i, (\<sigma>', (s', t'))) \<in> oparp_sos i S T") simp_all


[STATEMENT]
lemma opar_sendTE [elim]:
  "\<lbrakk>((\<sigma>, (s, t)), send m, (\<sigma>', (s', t'))) \<in> oparp_sos i S T;
    \<lbrakk>((\<sigma>, s), send m, (\<sigma>', s')) \<in> S; t' = t\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>((\<sigma>, s, t), send m, \<sigma>', s', t') \<in> oparp_sos i S T; \<lbrakk>((\<sigma>, s), send m, \<sigma>', s') \<in> S; t' = t\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P
[PROOF STEP]
by (ind_cases "((\<sigma>, (s, t)), send m, (\<sigma>', (s', t'))) \<in> oparp_sos i S T") auto


[STATEMENT]
lemma opar_deliverTE [elim]:
  "\<lbrakk>((\<sigma>, (s, t)), deliver d, (\<sigma>', (s', t'))) \<in> oparp_sos i S T;
    \<lbrakk>((\<sigma>, s), deliver d, (\<sigma>', s')) \<in> S; t' = t\<rbrakk> \<Longrightarrow> P;
    \<lbrakk>(t, deliver d, t') \<in> T; s' = s; \<sigma>' i = \<sigma> i\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>((\<sigma>, s, t), deliver d, \<sigma>', s', t') \<in> oparp_sos i S T; \<lbrakk>((\<sigma>, s), deliver d, \<sigma>', s') \<in> S; t' = t\<rbrakk> \<Longrightarrow> P; \<lbrakk>(t, deliver d, t') \<in> T; s' = s; \<sigma>' i = \<sigma> i\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P
[PROOF STEP]
by (ind_cases "((\<sigma>, (s, t)), deliver d, (\<sigma>', (s', t'))) \<in> oparp_sos i S T") simp_all


[STATEMENT]
lemma opar_receiveTE [elim]:
  "\<lbrakk>((\<sigma>, (s, t)), receive m, (\<sigma>', (s', t'))) \<in> oparp_sos i S T;
    \<lbrakk>(t, receive m, t') \<in> T; s' = s; \<sigma>' i = \<sigma> i\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>((\<sigma>, s, t), receive m, \<sigma>', s', t') \<in> oparp_sos i S T; \<lbrakk>(t, receive m, t') \<in> T; s' = s; \<sigma>' i = \<sigma> i\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P
[PROOF STEP]
by (ind_cases "((\<sigma>, (s, t)), receive m, (\<sigma>', (s', t'))) \<in> oparp_sos i S T") auto


[STATEMENT]
lemma oparp_sos_cases [elim]:
  assumes "((\<sigma>, (s, t)), a, (\<sigma>', (s', t'))) \<in> oparp_sos i S T"
      and "\<lbrakk> ((\<sigma>, s), a, (\<sigma>', s')) \<in> S; \<And>m. a \<noteq> receive m; t' = t \<rbrakk> \<Longrightarrow> P"
      and "\<lbrakk> (t, a, t') \<in> T; \<And>m. a \<noteq> send m; s' = s; \<sigma>' i = \<sigma> i \<rbrakk> \<Longrightarrow> P"
      and "\<And>m. \<lbrakk> a = \<tau>; ((\<sigma>, s), receive m, (\<sigma>', s')) \<in> S; (t, send m, t') \<in> T \<rbrakk> \<Longrightarrow> P"
    shows "P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
((\<sigma>, s, t), a, \<sigma>', s', t') \<in> oparp_sos i S T
\<lbrakk>((\<sigma>, s), a, \<sigma>', s') \<in> S; \<And>m. a \<noteq> receive m; t' = t\<rbrakk> \<Longrightarrow> P
\<lbrakk>(t, a, t') \<in> T; \<And>m. a \<noteq> send m; s' = s; \<sigma>' i = \<sigma> i\<rbrakk> \<Longrightarrow> P
\<lbrakk>a = \<tau>; ((\<sigma>, s), receive ?m, \<sigma>', s') \<in> S; (t, send ?m, t') \<in> T\<rbrakk> \<Longrightarrow> P

goal (1 subgoal):
 1. P
[PROOF STEP]
by cases auto


[STATEMENT]
lemma extgsimp [simp]:
  "extg ((\<sigma>, l1), l2) = (\<sigma>, (l1, l2))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. extg ((\<sigma>, l1), l2) = (\<sigma>, l1, l2)
[PROOF STEP]
unfolding extg_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (case ((\<sigma>, l1), l2) of (x, xa) \<Rightarrow> (case x of (\<sigma>, l1) \<Rightarrow> \<lambda>l2. (\<sigma>, l1, l2)) xa) = (\<sigma>, l1, l2)
[PROOF STEP]
by simp


[STATEMENT]
lemma extg_range_prod: "extg ` (i1 \<times> i2) = {(\<sigma>, (s1, s2))|\<sigma> s1 s2. (\<sigma>, s1) \<in> i1 \<and> s2 \<in> i2}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. extg ` (i1 \<times> i2) = {(\<sigma>, s1, s2) |\<sigma> s1 s2. (\<sigma>, s1) \<in> i1 \<and> s2 \<in> i2}
[PROOF STEP]
unfolding image_def extg_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {y. \<exists>x\<in>i1 \<times> i2. y = (case x of (x, xa) \<Rightarrow> (case x of (\<sigma>, l1) \<Rightarrow> \<lambda>l2. (\<sigma>, l1, l2)) xa)} = {(\<sigma>, s1, s2) |\<sigma> s1 s2. (\<sigma>, s1) \<in> i1 \<and> s2 \<in> i2}
[PROOF STEP]
by (rule Collect_cong) (auto split: prod.split)


[STATEMENT]
lemma opar_comp_def':
  "s \<langle>\<langle>\<^bsub>i\<^esub> t = \<lparr> init = {(\<sigma>, (s\<^sub>l, t\<^sub>l))|\<sigma> s\<^sub>l t\<^sub>l. (\<sigma>, s\<^sub>l) \<in> init s \<and> t\<^sub>l \<in> init t},
                trans = oparp_sos i (trans s) (trans t) \<rparr>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s \<langle>\<langle>\<^bsub>i\<^esub> t = \<lparr>init = {(\<sigma>, s\<^sub>l, t\<^sub>l) |\<sigma> s\<^sub>l t\<^sub>l. (\<sigma>, s\<^sub>l) \<in> init s \<and> t\<^sub>l \<in> init t}, trans = oparp_sos i (automaton.trans s) (automaton.trans t)\<rparr>
[PROOF STEP]
unfolding opar_comp_def extg_def image_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lparr>init = {y. \<exists>x\<in>init s \<times> init t. y = (case x of (x, xa) \<Rightarrow> (case x of (\<sigma>, l1) \<Rightarrow> \<lambda>l2. (\<sigma>, l1, l2)) xa)}, trans = oparp_sos i (automaton.trans s) (automaton.trans t)\<rparr> = \<lparr>init = {(\<sigma>, s\<^sub>l, t\<^sub>l) |\<sigma> s\<^sub>l t\<^sub>l. (\<sigma>, s\<^sub>l) \<in> init s \<and> t\<^sub>l \<in> init t}, trans = oparp_sos i (automaton.trans s) (automaton.trans t)\<rparr>
[PROOF STEP]
by (auto split: prod.split)


[STATEMENT]
lemma trans_opar_comp [simp]:
  "trans (s \<langle>\<langle>\<^bsub>i\<^esub> t) = oparp_sos i (trans s) (trans t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. automaton.trans (s \<langle>\<langle>\<^bsub>i\<^esub> t) = oparp_sos i (automaton.trans s) (automaton.trans t)
[PROOF STEP]
unfolding opar_comp_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. automaton.trans \<lparr>init = extg ` (init s \<times> init t), trans = oparp_sos i (automaton.trans s) (automaton.trans t)\<rparr> = oparp_sos i (automaton.trans s) (automaton.trans t)
[PROOF STEP]
by simp


[STATEMENT]
lemma init_opar_comp [simp]:
  "init (s \<langle>\<langle>\<^bsub>i\<^esub> t) = extg ` (init s \<times> init t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. init (s \<langle>\<langle>\<^bsub>i\<^esub> t) = extg ` (init s \<times> init t)
[PROOF STEP]
unfolding opar_comp_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. init \<lparr>init = extg ` (init s \<times> init t), trans = oparp_sos i (automaton.trans s) (automaton.trans t)\<rparr> = extg ` (init s \<times> init t)
[PROOF STEP]
by simp


[STATEMENT]
lemma oarrives_or_not:
  assumes "((\<sigma>, NodeS i s R), ii\<not>ni:arrive(m), (\<sigma>', NodeS i' s' R')) \<in> onode_sos S"
    shows "(ii = {i} \<and> ni = {}) \<or> (ii = {} \<and> ni = {i})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ii = {i} \<and> ni = {} \<or> ii = {} \<and> ni = {i}
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
((\<sigma>, NodeS i s R), ii\<not>ni:arrive(m), \<sigma>', NodeS i' s' R') \<in> onode_sos S

goal (1 subgoal):
 1. ii = {i} \<and> ni = {} \<or> ii = {} \<and> ni = {i}
[PROOF STEP]
by rule simp_all


[STATEMENT]
lemma trans_onode_comp:
  "trans (\<langle>i : S : R\<rangle>\<^sub>o) = onode_sos (trans S)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. automaton.trans (\<langle>i : S : R\<rangle>\<^sub>o) = onode_sos (automaton.trans S)
[PROOF STEP]
unfolding onode_comp_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. automaton.trans \<lparr>init = {(\<sigma>, NodeS i s R) |\<sigma> s. (\<sigma>, s) \<in> init S}, trans = onode_sos (automaton.trans S)\<rparr> = onode_sos (automaton.trans S)
[PROOF STEP]
by simp


[STATEMENT]
lemma init_onode_comp:
  "init (\<langle>i : S : R\<rangle>\<^sub>o) = {(\<sigma>, NodeS i s R)|\<sigma> s. (\<sigma>, s) \<in> init S}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. init (\<langle>i : S : R\<rangle>\<^sub>o) = {(\<sigma>, NodeS i s R) |\<sigma> s. (\<sigma>, s) \<in> init S}
[PROOF STEP]
unfolding onode_comp_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. init \<lparr>init = {(\<sigma>, NodeS i s R) |\<sigma> s. (\<sigma>, s) \<in> init S}, trans = onode_sos (automaton.trans S)\<rparr> = {(\<sigma>, NodeS i s R) |\<sigma> s. (\<sigma>, s) \<in> init S}
[PROOF STEP]
by simp


[STATEMENT]
lemma fst_par_onode_comp [simp]:
  "trans (\<langle>i : s \<langle>\<langle>\<^bsub>I\<^esub> t : R\<rangle>\<^sub>o) = onode_sos (oparp_sos I (trans s) (trans t))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. automaton.trans (\<langle>i : s \<langle>\<langle>\<^bsub>I\<^esub> t : R\<rangle>\<^sub>o) = onode_sos (oparp_sos I (automaton.trans s) (automaton.trans t))
[PROOF STEP]
unfolding onode_comp_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. automaton.trans \<lparr>init = {(\<sigma>, NodeS i sa R) |\<sigma> sa. (\<sigma>, sa) \<in> init (s \<langle>\<langle>\<^bsub>I\<^esub> t)}, trans = onode_sos (automaton.trans (s \<langle>\<langle>\<^bsub>I\<^esub> t))\<rparr> = onode_sos (oparp_sos I (automaton.trans s) (automaton.trans t))
[PROOF STEP]
by simp


[STATEMENT]
lemma init_par_onode_comp [simp]:
  "init (\<langle>i : s \<langle>\<langle>\<^bsub>I\<^esub> t : R\<rangle>\<^sub>o) = {(\<sigma>, NodeS i (s1, s2) R)|\<sigma> s1 s2. ((\<sigma>, s1), s2) \<in> init s \<times> init t}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. init (\<langle>i : s \<langle>\<langle>\<^bsub>I\<^esub> t : R\<rangle>\<^sub>o) = {(\<sigma>, NodeS i (s1, s2) R) |\<sigma> s1 s2. ((\<sigma>, s1), s2) \<in> init s \<times> init t}
[PROOF STEP]
unfolding onode_comp_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. init \<lparr>init = {(\<sigma>, NodeS i sa R) |\<sigma> sa. (\<sigma>, sa) \<in> init (s \<langle>\<langle>\<^bsub>I\<^esub> t)}, trans = onode_sos (automaton.trans (s \<langle>\<langle>\<^bsub>I\<^esub> t))\<rparr> = {(\<sigma>, NodeS i (s1, s2) R) |\<sigma> s1 s2. ((\<sigma>, s1), s2) \<in> init s \<times> init t}
[PROOF STEP]
by (simp add: extg_range_prod)


[STATEMENT]
lemma onode_sos_dest_is_net_state:
  assumes "((\<sigma>, p), a, s') \<in> onode_sos S"
    shows "\<exists>\<sigma>' i' \<zeta>' R'. s' = (\<sigma>', NodeS i' \<zeta>' R')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>\<sigma>' i' \<zeta>' R'. s' = (\<sigma>', NodeS i' \<zeta>' R')
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
((\<sigma>, p), a, s') \<in> onode_sos S

goal (1 subgoal):
 1. \<exists>\<sigma>' i' \<zeta>' R'. s' = (\<sigma>', NodeS i' \<zeta>' R')
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ((\<sigma>, p), a, s') \<in> onode_sos S \<Longrightarrow> \<exists>\<sigma>' i' \<zeta>' R'. s' = (\<sigma>', NodeS i' \<zeta>' R')
[PROOF STEP]
assume "((\<sigma>, p), a, s') \<in> onode_sos S"
[PROOF STATE]
proof (state)
this:
((\<sigma>, p), a, s') \<in> onode_sos S

goal (1 subgoal):
 1. ((\<sigma>, p), a, s') \<in> onode_sos S \<Longrightarrow> \<exists>\<sigma>' i' \<zeta>' R'. s' = (\<sigma>', NodeS i' \<zeta>' R')
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
((\<sigma>, p), a, s') \<in> onode_sos S
[PROOF STEP]
obtain \<sigma>' i' \<zeta>' R' where "s' = (\<sigma>', NodeS i' \<zeta>' R')"
[PROOF STATE]
proof (prove)
using this:
((\<sigma>, p), a, s') \<in> onode_sos S

goal (1 subgoal):
 1. (\<And>\<sigma>' i' \<zeta>' R'. s' = (\<sigma>', NodeS i' \<zeta>' R') \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (cases s') (auto elim!: onode_sos.cases)
[PROOF STATE]
proof (state)
this:
s' = (\<sigma>', NodeS i' \<zeta>' R')

goal (1 subgoal):
 1. ((\<sigma>, p), a, s') \<in> onode_sos S \<Longrightarrow> \<exists>\<sigma>' i' \<zeta>' R'. s' = (\<sigma>', NodeS i' \<zeta>' R')
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
s' = (\<sigma>', NodeS i' \<zeta>' R')

goal (1 subgoal):
 1. \<exists>\<sigma>' i' \<zeta>' R'. s' = (\<sigma>', NodeS i' \<zeta>' R')
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<exists>\<sigma>' i' \<zeta>' R'. s' = (\<sigma>', NodeS i' \<zeta>' R')

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma onode_sos_dest_is_net_state':
  assumes "((\<sigma>, NodeS i p R), a, s') \<in> onode_sos S"
    shows "\<exists>\<sigma>' \<zeta>' R'. s' = (\<sigma>', NodeS i \<zeta>' R')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>\<sigma>' \<zeta>' R'. s' = (\<sigma>', NodeS i \<zeta>' R')
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
((\<sigma>, NodeS i p R), a, s') \<in> onode_sos S

goal (1 subgoal):
 1. \<exists>\<sigma>' \<zeta>' R'. s' = (\<sigma>', NodeS i \<zeta>' R')
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ((\<sigma>, NodeS i p R), a, s') \<in> onode_sos S \<Longrightarrow> \<exists>\<sigma>' \<zeta>' R'. s' = (\<sigma>', NodeS i \<zeta>' R')
[PROOF STEP]
assume "((\<sigma>, NodeS i p R), a, s') \<in> onode_sos S"
[PROOF STATE]
proof (state)
this:
((\<sigma>, NodeS i p R), a, s') \<in> onode_sos S

goal (1 subgoal):
 1. ((\<sigma>, NodeS i p R), a, s') \<in> onode_sos S \<Longrightarrow> \<exists>\<sigma>' \<zeta>' R'. s' = (\<sigma>', NodeS i \<zeta>' R')
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
((\<sigma>, NodeS i p R), a, s') \<in> onode_sos S
[PROOF STEP]
obtain \<sigma>' \<zeta>' R' where "s' = (\<sigma>', NodeS i \<zeta>' R')"
[PROOF STATE]
proof (prove)
using this:
((\<sigma>, NodeS i p R), a, s') \<in> onode_sos S

goal (1 subgoal):
 1. (\<And>\<sigma>' \<zeta>' R'. s' = (\<sigma>', NodeS i \<zeta>' R') \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (cases s') (auto elim!: onode_sos.cases)
[PROOF STATE]
proof (state)
this:
s' = (\<sigma>', NodeS i \<zeta>' R')

goal (1 subgoal):
 1. ((\<sigma>, NodeS i p R), a, s') \<in> onode_sos S \<Longrightarrow> \<exists>\<sigma>' \<zeta>' R'. s' = (\<sigma>', NodeS i \<zeta>' R')
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
s' = (\<sigma>', NodeS i \<zeta>' R')

goal (1 subgoal):
 1. \<exists>\<sigma>' \<zeta>' R'. s' = (\<sigma>', NodeS i \<zeta>' R')
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<exists>\<sigma>' \<zeta>' R'. s' = (\<sigma>', NodeS i \<zeta>' R')

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma onode_sos_dest_is_net_state'':
  assumes "((\<sigma>, NodeS i p R), a, (\<sigma>', s')) \<in> onode_sos S"
    shows "\<exists>\<zeta>' R'. s' = NodeS i \<zeta>' R'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>\<zeta>' R'. s' = NodeS i \<zeta>' R'
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>\<zeta>' R'. s' = NodeS i \<zeta>' R'
[PROOF STEP]
define ns' where "ns' = (\<sigma>', s')"
[PROOF STATE]
proof (state)
this:
ns' = (\<sigma>', s')

goal (1 subgoal):
 1. \<exists>\<zeta>' R'. s' = NodeS i \<zeta>' R'
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
((\<sigma>, NodeS i p R), a, \<sigma>', s') \<in> onode_sos S
ns' = (\<sigma>', s')
[PROOF STEP]
have "((\<sigma>, NodeS i p R), a, ns') \<in> onode_sos S"
[PROOF STATE]
proof (prove)
using this:
((\<sigma>, NodeS i p R), a, \<sigma>', s') \<in> onode_sos S
ns' = (\<sigma>', s')

goal (1 subgoal):
 1. ((\<sigma>, NodeS i p R), a, ns') \<in> onode_sos S
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
((\<sigma>, NodeS i p R), a, ns') \<in> onode_sos S

goal (1 subgoal):
 1. \<exists>\<zeta>' R'. s' = NodeS i \<zeta>' R'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
((\<sigma>, NodeS i p R), a, ns') \<in> onode_sos S
[PROOF STEP]
obtain \<sigma>'' \<zeta>' R' where "ns' = (\<sigma>'', NodeS i \<zeta>' R')"
[PROOF STATE]
proof (prove)
using this:
((\<sigma>, NodeS i p R), a, ns') \<in> onode_sos S

goal (1 subgoal):
 1. (\<And>\<sigma>'' \<zeta>' R'. ns' = (\<sigma>'', NodeS i \<zeta>' R') \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis onode_sos_dest_is_net_state')
[PROOF STATE]
proof (state)
this:
ns' = (\<sigma>'', NodeS i \<zeta>' R')

goal (1 subgoal):
 1. \<exists>\<zeta>' R'. s' = NodeS i \<zeta>' R'
[PROOF STEP]
hence "s' = NodeS i \<zeta>' R'"
[PROOF STATE]
proof (prove)
using this:
ns' = (\<sigma>'', NodeS i \<zeta>' R')

goal (1 subgoal):
 1. s' = NodeS i \<zeta>' R'
[PROOF STEP]
by (simp add: ns'_def)
[PROOF STATE]
proof (state)
this:
s' = NodeS i \<zeta>' R'

goal (1 subgoal):
 1. \<exists>\<zeta>' R'. s' = NodeS i \<zeta>' R'
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
s' = NodeS i \<zeta>' R'

goal (1 subgoal):
 1. \<exists>\<zeta>' R'. s' = NodeS i \<zeta>' R'
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<exists>\<zeta>' R'. s' = NodeS i \<zeta>' R'

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma onode_sos_src_is_net_state:
  assumes "((\<sigma>, p), a, s') \<in> onode_sos S"
    shows "\<exists>i \<zeta> R. p = NodeS i \<zeta> R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>i \<zeta> R. p = NodeS i \<zeta> R
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
((\<sigma>, p), a, s') \<in> onode_sos S

goal (1 subgoal):
 1. \<exists>i \<zeta> R. p = NodeS i \<zeta> R
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ((\<sigma>, p), a, s') \<in> onode_sos S \<Longrightarrow> \<exists>i \<zeta> R. p = NodeS i \<zeta> R
[PROOF STEP]
assume "((\<sigma>, p), a, s') \<in> onode_sos S"
[PROOF STATE]
proof (state)
this:
((\<sigma>, p), a, s') \<in> onode_sos S

goal (1 subgoal):
 1. ((\<sigma>, p), a, s') \<in> onode_sos S \<Longrightarrow> \<exists>i \<zeta> R. p = NodeS i \<zeta> R
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
((\<sigma>, p), a, s') \<in> onode_sos S
[PROOF STEP]
obtain i \<zeta> R where "p = NodeS i \<zeta> R"
[PROOF STATE]
proof (prove)
using this:
((\<sigma>, p), a, s') \<in> onode_sos S

goal (1 subgoal):
 1. (\<And>i \<zeta> R. p = NodeS i \<zeta> R \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (cases s') (auto elim!: onode_sos.cases)
[PROOF STATE]
proof (state)
this:
p = NodeS i \<zeta> R

goal (1 subgoal):
 1. ((\<sigma>, p), a, s') \<in> onode_sos S \<Longrightarrow> \<exists>i \<zeta> R. p = NodeS i \<zeta> R
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
p = NodeS i \<zeta> R

goal (1 subgoal):
 1. \<exists>i \<zeta> R. p = NodeS i \<zeta> R
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<exists>i \<zeta> R. p = NodeS i \<zeta> R

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma onode_sos_net_states:
  assumes "((\<sigma>, s), a, (\<sigma>', s')) \<in> onode_sos S"
    shows "\<exists>i \<zeta> R \<zeta>' R'. s = NodeS i \<zeta> R \<and> s' = NodeS i \<zeta>' R'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>i \<zeta> R \<zeta>' R'. s = NodeS i \<zeta> R \<and> s' = NodeS i \<zeta>' R'
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>i \<zeta> R \<zeta>' R'. s = NodeS i \<zeta> R \<and> s' = NodeS i \<zeta>' R'
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
((\<sigma>, s), a, \<sigma>', s') \<in> onode_sos S
[PROOF STEP]
obtain i \<zeta> R where "s = NodeS i \<zeta> R"
[PROOF STATE]
proof (prove)
using this:
((\<sigma>, s), a, \<sigma>', s') \<in> onode_sos S

goal (1 subgoal):
 1. (\<And>i \<zeta> R. s = NodeS i \<zeta> R \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis onode_sos_src_is_net_state)
[PROOF STATE]
proof (state)
this:
s = NodeS i \<zeta> R

goal (1 subgoal):
 1. \<exists>i \<zeta> R \<zeta>' R'. s = NodeS i \<zeta> R \<and> s' = NodeS i \<zeta>' R'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
s = NodeS i \<zeta> R

goal (1 subgoal):
 1. \<exists>i \<zeta> R \<zeta>' R'. s = NodeS i \<zeta> R \<and> s' = NodeS i \<zeta>' R'
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
((\<sigma>, s), a, \<sigma>', s') \<in> onode_sos S
s = NodeS i \<zeta> R
[PROOF STEP]
obtain \<zeta>' R' where "s' = NodeS i \<zeta>' R'"
[PROOF STATE]
proof (prove)
using this:
((\<sigma>, s), a, \<sigma>', s') \<in> onode_sos S
s = NodeS i \<zeta> R

goal (1 subgoal):
 1. (\<And>\<zeta>' R'. s' = NodeS i \<zeta>' R' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto dest!: onode_sos_dest_is_net_state')
[PROOF STATE]
proof (state)
this:
s' = NodeS i \<zeta>' R'

goal (1 subgoal):
 1. \<exists>i \<zeta> R \<zeta>' R'. s = NodeS i \<zeta> R \<and> s' = NodeS i \<zeta>' R'
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
s = NodeS i \<zeta> R
s' = NodeS i \<zeta>' R'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
s = NodeS i \<zeta> R
s' = NodeS i \<zeta>' R'

goal (1 subgoal):
 1. \<exists>i \<zeta> R \<zeta>' R'. s = NodeS i \<zeta> R \<and> s' = NodeS i \<zeta>' R'
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<exists>i \<zeta> R \<zeta>' R'. s = NodeS i \<zeta> R \<and> s' = NodeS i \<zeta>' R'

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma node_sos_cases [elim]:
  "((\<sigma>, NodeS i p R), a, (\<sigma>', NodeS i p' R')) \<in> onode_sos S \<Longrightarrow>
  (\<And>m .       \<lbrakk> a = R:*cast(m);          R' = R; ((\<sigma>, p), broadcast m,   (\<sigma>', p')) \<in> S \<rbrakk> \<Longrightarrow> P) \<Longrightarrow>
  (\<And>m D.      \<lbrakk> a = (R \<inter> D):*cast(m);    R' = R; ((\<sigma>, p), groupcast D m, (\<sigma>', p')) \<in> S \<rbrakk> \<Longrightarrow> P) \<Longrightarrow>
  (\<And>d m.      \<lbrakk> a = {d}:*cast(m);        R' = R; ((\<sigma>, p), unicast d m,   (\<sigma>', p')) \<in> S; d \<in> R \<rbrakk> \<Longrightarrow> P) \<Longrightarrow>
  (\<And>d.        \<lbrakk> a = \<tau>;                   R' = R; ((\<sigma>, p), \<not>unicast d,    (\<sigma>', p')) \<in> S; d \<notin> R \<rbrakk> \<Longrightarrow> P) \<Longrightarrow>
  (\<And>d.        \<lbrakk> a = i:deliver(d);        R' = R; ((\<sigma>, p), deliver d,     (\<sigma>', p')) \<in> S \<rbrakk> \<Longrightarrow> P) \<Longrightarrow>
  (\<And>m.        \<lbrakk> a = {i}\<not>{}:arrive(m);    R' = R; ((\<sigma>, p), receive m,     (\<sigma>', p')) \<in> S \<rbrakk> \<Longrightarrow> P) \<Longrightarrow>
  (            \<lbrakk> a = \<tau>;                   R' = R; ((\<sigma>, p), \<tau>,             (\<sigma>', p')) \<in> S \<rbrakk> \<Longrightarrow> P) \<Longrightarrow>
  (\<And>m.        \<lbrakk> a = {}\<not>{i}:arrive(m);    R' = R; p = p'; \<sigma>' i = \<sigma> i \<rbrakk> \<Longrightarrow> P) \<Longrightarrow>
  (\<And>i i'.     \<lbrakk> a = connect(i, i');      R' = R \<union> {i'}; p = p'; \<sigma>' i = \<sigma> i \<rbrakk> \<Longrightarrow> P) \<Longrightarrow>
  (\<And>i i'.     \<lbrakk> a = connect(i', i);      R' = R \<union> {i'}; p = p'; \<sigma>' i = \<sigma> i \<rbrakk> \<Longrightarrow> P) \<Longrightarrow>
  (\<And>i i'.     \<lbrakk> a = disconnect(i, i');   R' = R - {i'}; p = p'; \<sigma>' i = \<sigma> i \<rbrakk> \<Longrightarrow> P) \<Longrightarrow>
  (\<And>i i'.     \<lbrakk> a = disconnect(i', i);   R' = R - {i'}; p = p'; \<sigma>' i = \<sigma> i \<rbrakk> \<Longrightarrow> P) \<Longrightarrow>
  (\<And>i i' i''. \<lbrakk> a = connect(i', i'');    R' = R; p = p'; i \<noteq> i'; i \<noteq> i''; \<sigma>' i = \<sigma> i \<rbrakk> \<Longrightarrow> P) \<Longrightarrow>
  (\<And>i i' i''. \<lbrakk> a = disconnect(i', i''); R' = R; p = p'; i \<noteq> i'; i \<noteq> i''; \<sigma>' i = \<sigma> i \<rbrakk> \<Longrightarrow> P) \<Longrightarrow>
  P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>((\<sigma>, NodeS i p R), a, \<sigma>', NodeS i p' R') \<in> onode_sos S; \<And>m. \<lbrakk>a = R:*cast(m); R' = R; ((\<sigma>, p), broadcast m, \<sigma>', p') \<in> S\<rbrakk> \<Longrightarrow> P; \<And>m D. \<lbrakk>a = (R \<inter> D):*cast(m); R' = R; ((\<sigma>, p), groupcast D m, \<sigma>', p') \<in> S\<rbrakk> \<Longrightarrow> P; \<And>d m. \<lbrakk>a = {d}:*cast(m); R' = R; ((\<sigma>, p), unicast d m, \<sigma>', p') \<in> S; d \<in> R\<rbrakk> \<Longrightarrow> P; \<And>d. \<lbrakk>a = \<tau>; R' = R; ((\<sigma>, p), \<not>unicast d, \<sigma>', p') \<in> S; d \<notin> R\<rbrakk> \<Longrightarrow> P; \<And>d. \<lbrakk>a = i:deliver(d); R' = R; ((\<sigma>, p), deliver d, \<sigma>', p') \<in> S\<rbrakk> \<Longrightarrow> P; \<And>m. \<lbrakk>a = {i}\<not>{}:arrive(m); R' = R; ((\<sigma>, p), receive m, \<sigma>', p') \<in> S\<rbrakk> \<Longrightarrow> P; \<lbrakk>a = \<tau>; R' = R; ((\<sigma>, p), \<tau>, \<sigma>', p') \<in> S\<rbrakk> \<Longrightarrow> P; \<And>m. \<lbrakk>a = {}\<not>{i}:arrive(m); R' = R; p = p'; \<sigma>' i = \<sigma> i\<rbrakk> \<Longrightarrow> P; \<And>i i'. \<lbrakk>a = connect(i, i'); R' = R \<union> {i'}; p = p'; \<sigma>' i = \<sigma> i\<rbrakk> \<Longrightarrow> P; \<And>i i'. \<lbrakk>a = connect(i', i); R' = R \<union> {i'}; p = p'; \<sigma>' i = \<sigma> i\<rbrakk> \<Longrightarrow> P; \<And>i i'. \<lbrakk>a = disconnect(i, i'); R' = R - {i'}; p = p'; \<sigma>' i = \<sigma> i\<rbrakk> \<Longrightarrow> P; \<And>i i'. \<lbrakk>a = disconnect(i', i); R' = R - {i'}; p = p'; \<sigma>' i = \<sigma> i\<rbrakk> \<Longrightarrow> P; \<And>i i' i''. \<lbrakk>a = connect(i', i''); R' = R; p = p'; i \<noteq> i'; i \<noteq> i''; \<sigma>' i = \<sigma> i\<rbrakk> \<Longrightarrow> P; \<And>i i' i''. \<lbrakk>a = disconnect(i', i''); R' = R; p = p'; i \<noteq> i'; i \<noteq> i''; \<sigma>' i = \<sigma> i\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P
[PROOF STEP]
by (erule onode_sos.cases) (simp | metis)+


[STATEMENT]
lemma opnet_node_init [elim, simp]:
  assumes "(\<sigma>, s) \<in> init (opnet onp \<langle>i; R\<rangle>)"
    shows "(\<sigma>, s) \<in> { (\<sigma>, NodeS i ns R) |\<sigma> ns. (\<sigma>, ns) \<in> init (onp i)}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<sigma>, s) \<in> {(\<sigma>, NodeS i ns R) |\<sigma> ns. (\<sigma>, ns) \<in> init (onp i)}
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
(\<sigma>, s) \<in> init (opnet onp \<langle>i; R\<rangle>)

goal (1 subgoal):
 1. (\<sigma>, s) \<in> {(\<sigma>, NodeS i ns R) |\<sigma> ns. (\<sigma>, ns) \<in> init (onp i)}
[PROOF STEP]
by (simp add: onode_comp_def)


[STATEMENT]
lemma opnet_node_init' [elim]:
 assumes "(\<sigma>, s) \<in> init (opnet onp \<langle>i; R\<rangle>)"
 obtains ns where "s = NodeS i ns R"
             and "(\<sigma>, ns) \<in> init (onp i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>ns. \<lbrakk>s = NodeS i ns R; (\<sigma>, ns) \<in> init (onp i)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
(\<sigma>, s) \<in> init (opnet onp \<langle>i; R\<rangle>)

goal (1 subgoal):
 1. (\<And>ns. \<lbrakk>s = NodeS i ns R; (\<sigma>, ns) \<in> init (onp i)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp add: onode_comp_def)


[STATEMENT]
lemma opnet_node_trans [elim, simp]:
  assumes "(s, a, s') \<in> trans (opnet onp \<langle>i; R\<rangle>)"
    shows "(s, a, s') \<in> onode_sos (trans (onp i))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (s, a, s') \<in> onode_sos (automaton.trans (onp i))
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
(s, a, s') \<in> automaton.trans (opnet onp \<langle>i; R\<rangle>)

goal (1 subgoal):
 1. (s, a, s') \<in> onode_sos (automaton.trans (onp i))
[PROOF STEP]
by (simp add: trans_onode_comp)


[STATEMENT]
lemma ocomplete_no_cast [simp]:
  "((\<sigma>, s), R:*cast(m), (\<sigma>', s')) \<notin> ocnet_sos T"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<sigma>, s), R:*cast(m), \<sigma>', s') \<notin> ocnet_sos T
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ((\<sigma>, s), R:*cast(m), \<sigma>', s') \<in> ocnet_sos T \<Longrightarrow> False
[PROOF STEP]
assume "((\<sigma>, s), R:*cast(m), (\<sigma>', s')) \<in> ocnet_sos T"
[PROOF STATE]
proof (state)
this:
((\<sigma>, s), R:*cast(m), \<sigma>', s') \<in> ocnet_sos T

goal (1 subgoal):
 1. ((\<sigma>, s), R:*cast(m), \<sigma>', s') \<in> ocnet_sos T \<Longrightarrow> False
[PROOF STEP]
hence "R:*cast(m) \<noteq> R:*cast(m)"
[PROOF STATE]
proof (prove)
using this:
((\<sigma>, s), R:*cast(m), \<sigma>', s') \<in> ocnet_sos T

goal (1 subgoal):
 1. R:*cast(m) \<noteq> R:*cast(m)
[PROOF STEP]
by (rule ocnet_sos.cases) auto
[PROOF STATE]
proof (state)
this:
R:*cast(m) \<noteq> R:*cast(m)

goal (1 subgoal):
 1. ((\<sigma>, s), R:*cast(m), \<sigma>', s') \<in> ocnet_sos T \<Longrightarrow> False
[PROOF STEP]
thus False
[PROOF STATE]
proof (prove)
using this:
R:*cast(m) \<noteq> R:*cast(m)

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ocomplete_no_arrive [simp]:
  "((\<sigma>, s), ii\<not>ni:arrive(m), (\<sigma>', s')) \<notin> ocnet_sos T"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<sigma>, s), ii\<not>ni:arrive(m), \<sigma>', s') \<notin> ocnet_sos T
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ((\<sigma>, s), ii\<not>ni:arrive(m), \<sigma>', s') \<in> ocnet_sos T \<Longrightarrow> False
[PROOF STEP]
assume "((\<sigma>, s), ii\<not>ni:arrive(m), (\<sigma>', s')) \<in> ocnet_sos T"
[PROOF STATE]
proof (state)
this:
((\<sigma>, s), ii\<not>ni:arrive(m), \<sigma>', s') \<in> ocnet_sos T

goal (1 subgoal):
 1. ((\<sigma>, s), ii\<not>ni:arrive(m), \<sigma>', s') \<in> ocnet_sos T \<Longrightarrow> False
[PROOF STEP]
hence "ii\<not>ni:arrive(m) \<noteq> ii\<not>ni:arrive(m)"
[PROOF STATE]
proof (prove)
using this:
((\<sigma>, s), ii\<not>ni:arrive(m), \<sigma>', s') \<in> ocnet_sos T

goal (1 subgoal):
 1. ii\<not>ni:arrive(m) \<noteq> ii\<not>ni:arrive(m)
[PROOF STEP]
by (rule ocnet_sos.cases) auto
[PROOF STATE]
proof (state)
this:
ii\<not>ni:arrive(m) \<noteq> ii\<not>ni:arrive(m)

goal (1 subgoal):
 1. ((\<sigma>, s), ii\<not>ni:arrive(m), \<sigma>', s') \<in> ocnet_sos T \<Longrightarrow> False
[PROOF STEP]
thus False
[PROOF STATE]
proof (prove)
using this:
ii\<not>ni:arrive(m) \<noteq> ii\<not>ni:arrive(m)

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ocomplete_no_change [elim]:
  assumes "((\<sigma>, s), a, (\<sigma>', s')) \<in> ocnet_sos T"
      and "j \<notin> net_ips s"
    shows "\<sigma>' j = \<sigma> j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<sigma>' j = \<sigma> j
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
((\<sigma>, s), a, \<sigma>', s') \<in> ocnet_sos T
j \<notin> net_ips s

goal (1 subgoal):
 1. \<sigma>' j = \<sigma> j
[PROOF STEP]
by cases simp_all


[STATEMENT]
lemma ocomplete_transE [elim]:
  assumes "((\<sigma>, \<zeta>), a, (\<sigma>', \<zeta>')) \<in> ocnet_sos (trans (opnet onp n))"
  obtains a' where "((\<sigma>, \<zeta>), a', (\<sigma>', \<zeta>')) \<in> trans (opnet onp n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>a'. ((\<sigma>, \<zeta>), a', \<sigma>', \<zeta>') \<in> automaton.trans (opnet onp n) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
((\<sigma>, \<zeta>), a, \<sigma>', \<zeta>') \<in> ocnet_sos (automaton.trans (opnet onp n))

goal (1 subgoal):
 1. (\<And>a'. ((\<sigma>, \<zeta>), a', \<sigma>', \<zeta>') \<in> automaton.trans (opnet onp n) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (cases a) (auto elim!: ocompleteTEs [simplified])


[STATEMENT]
lemma semilattice_transfer[transfer_rule]:
  assumes [transfer_rule]: "bi_unique A" "right_total A"
  shows
    "((A ===> A ===> A) ===> (=))
      (\<lambda>f. semilattice_ow (Collect (Domainp A)) f) semilattice"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((A ===> A ===> A) ===> (=)) (semilattice_ow (Collect (Domainp A))) semilattice
[PROOF STEP]
unfolding
    semilattice_ow_def semilattice_def
    semilattice_ow_axioms_def semilattice_axioms_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((A ===> A ===> A) ===> (=)) (\<lambda>f. abel_semigroup_ow (Collect (Domainp A)) f \<and> (\<forall>x. x \<in> Collect (Domainp A) \<longrightarrow> f x x = x)) (\<lambda>f. abel_semigroup f \<and> (\<forall>a. f a a = a))
[PROOF STEP]
apply transfer_prover_start
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. Transfer.Rel (A ===> A ===> ?Rh11) ?ac11 (=)
 2. Transfer.Rel ((A ===> ?Rh11) ===> ?Rf11) ?ab11 All
 3. Transfer.Rel ((A ===> A ===> A) ===> ?Re11) ?aa11 abel_semigroup
 4. Transfer.Rel (?Re11 ===> ?Rf11 ===> (=)) ?a11 (\<and>)
 5. (\<lambda>f. abel_semigroup_ow (Collect (Domainp A)) f \<and> (\<forall>x. x \<in> Collect (Domainp A) \<longrightarrow> f x x = x)) = (\<lambda>f. ?a11 (?aa11 f) (?ab11 (\<lambda>a. ?ac11 (f a a) a)))
[PROOF STEP]
apply transfer_step+
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>f. abel_semigroup_ow (Collect (Domainp A)) f \<and> (\<forall>x. x \<in> Collect (Domainp A) \<longrightarrow> f x x = x)) = (\<lambda>f. abel_semigroup_ow (Collect (Domainp A)) f \<and> (\<forall>a\<in>Collect (Domainp A). f a a = a))
[PROOF STEP]
by simp


[STATEMENT]
lemma semilattice_set_transfer[transfer_rule]:
  assumes [transfer_rule]: "bi_unique A" "right_total A"
  shows
    "((A ===> A ===> A) ===> (=))
      (\<lambda>f. semilattice_set_ow (Collect (Domainp A)) f) semilattice_set"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((A ===> A ===> A) ===> (=)) (semilattice_set_ow (Collect (Domainp A))) semilattice_set
[PROOF STEP]
unfolding semilattice_set_ow_def semilattice_set_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((A ===> A ===> A) ===> (=)) (semilattice_ow (Collect (Domainp A))) semilattice
[PROOF STEP]
by transfer_prover


[STATEMENT]
lemma inf_closed'[simp]: "\<forall>x\<in>U. \<forall>y\<in>U. x \<sqinter>\<^sub>o\<^sub>w y \<in> U"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>U. \<forall>y\<in>U. x \<sqinter>\<^sub>o\<^sub>w y \<in> U
[PROOF STEP]
by simp


[STATEMENT]
lemma sup_closed'[simp]: "\<forall>x\<in>U. \<forall>y\<in>U. x \<squnion>\<^sub>o\<^sub>w y \<in> U"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>U. \<forall>y\<in>U. x \<squnion>\<^sub>o\<^sub>w y \<in> U
[PROOF STEP]
by simp


[STATEMENT]
lemma semilattice_order_transfer[transfer_rule]:
  assumes [transfer_rule]: "bi_unique A" "right_total A"
  shows
    "(
      (A ===> A ===> A) ===>
      (A ===> A ===> (=)) ===>
      (A ===> A ===> (=)) ===>
      (=)
    ) (semilattice_order_ow (Collect (Domainp A))) semilattice_order"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((A ===> A ===> A) ===> (A ===> A ===> (=)) ===> (A ===> A ===> (=)) ===> (=)) (semilattice_order_ow (Collect (Domainp A))) semilattice_order
[PROOF STEP]
unfolding
    semilattice_order_ow_def semilattice_order_def
    semilattice_order_ow_axioms_def semilattice_order_axioms_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((A ===> A ===> A) ===> (A ===> A ===> (=)) ===> (A ===> A ===> (=)) ===> (=)) (\<lambda>f le ls. semilattice_ow (Collect (Domainp A)) f \<and> (\<forall>a b. a \<in> Collect (Domainp A) \<longrightarrow> b \<in> Collect (Domainp A) \<longrightarrow> le a b = (a = f a b)) \<and> (\<forall>a b. a \<in> Collect (Domainp A) \<longrightarrow> b \<in> Collect (Domainp A) \<longrightarrow> ls a b = (a = f a b \<and> a \<noteq> b))) (\<lambda>f less_eq less. semilattice f \<and> (\<forall>a b. less_eq a b = (a = f a b)) \<and> (\<forall>a b. less a b = (a = f a b \<and> a \<noteq> b)))
[PROOF STEP]
apply transfer_prover_start
[PROOF STATE]
proof (prove)
goal (15 subgoals):
 1. Transfer.Rel (A ===> A ===> ?Ru33) ?am33 (=)
 2. Transfer.Rel (?Ru33 ===> ?Rt33) ?al33 Not
 3. Transfer.Rel (A ===> A ===> ?Rs33) ?ak33 (=)
 4. Transfer.Rel (?Rs33 ===> ?Rt33 ===> ?Rr33) ?aj33 (\<and>)
 5. Transfer.Rel ((=) ===> ?Rr33 ===> ?Rq33) ?ai33 (=)
 6. Transfer.Rel ((A ===> ?Rq33) ===> ?Rp33) ?ah33 All
 7. Transfer.Rel ((A ===> ?Rp33) ===> ?Rl33) ?ag33 All
 8. Transfer.Rel (A ===> A ===> ?Ro33) ?af33 (=)
 9. Transfer.Rel ((=) ===> ?Ro33 ===> ?Rn33) ?ae33 (=)
 10. Transfer.Rel ((A ===> ?Rn33) ===> ?Rm33) ?ad33 All
A total of 15 subgoals...
[PROOF STEP]
apply transfer_step+
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>f le ls. semilattice_ow (Collect (Domainp A)) f \<and> (\<forall>a b. a \<in> Collect (Domainp A) \<longrightarrow> b \<in> Collect (Domainp A) \<longrightarrow> le a b = (a = f a b)) \<and> (\<forall>a b. a \<in> Collect (Domainp A) \<longrightarrow> b \<in> Collect (Domainp A) \<longrightarrow> ls a b = (a = f a b \<and> a \<noteq> b))) = (\<lambda>f less_eq less. semilattice_ow (Collect (Domainp A)) f \<and> (\<forall>a\<in>Collect (Domainp A). \<forall>b\<in>Collect (Domainp A). less_eq a b = (a = f a b)) \<and> (\<forall>a\<in>Collect (Domainp A). \<forall>b\<in>Collect (Domainp A). less a b = (a = f a b \<and> a \<noteq> b)))
[PROOF STEP]
by simp


[STATEMENT]
lemma semilattice_order_set_transfer[transfer_rule]:
  assumes [transfer_rule]: "bi_unique A" "right_total A"
  shows
    "(
      (A ===> A ===> A) ===>
      (A ===> A ===> (=)) ===>
      (A ===> A ===> (=)) ===>
      (=)
    ) (semilattice_order_set_ow (Collect (Domainp A))) semilattice_order_set"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((A ===> A ===> A) ===> (A ===> A ===> (=)) ===> (A ===> A ===> (=)) ===> (=)) (semilattice_order_set_ow (Collect (Domainp A))) semilattice_order_set
[PROOF STEP]
unfolding semilattice_order_set_ow_def semilattice_order_set_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((A ===> A ===> A) ===> (A ===> A ===> (=)) ===> (A ===> A ===> (=)) ===> (=)) (\<lambda>f le ls. semilattice_order_ow (Collect (Domainp A)) f le ls \<and> semilattice_set_ow (Collect (Domainp A)) f) (\<lambda>f less_eq less. semilattice_order f less_eq less \<and> semilattice_set f)
[PROOF STEP]
apply transfer_prover_start
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. Transfer.Rel ((A ===> A ===> A) ===> ?Rg9) ?ab9 semilattice_set
 2. Transfer.Rel ((A ===> A ===> A) ===> (A ===> A ===> (=)) ===> (A ===> A ===> (=)) ===> ?Rf9) ?aa9 semilattice_order
 3. Transfer.Rel (?Rf9 ===> ?Rg9 ===> (=)) ?a9 (\<and>)
 4. (\<lambda>f le ls. semilattice_order_ow (Collect (Domainp A)) f le ls \<and> semilattice_set_ow (Collect (Domainp A)) f) = (\<lambda>f less_eq less. ?a9 (?aa9 f less_eq less) (?ab9 f))
[PROOF STEP]
apply transfer_step+
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>f le ls. semilattice_order_ow (Collect (Domainp A)) f le ls \<and> semilattice_set_ow (Collect (Domainp A)) f) = (\<lambda>f less_eq less. semilattice_order_ow (Collect (Domainp A)) f less_eq less \<and> semilattice_set_ow (Collect (Domainp A)) f)
[PROOF STEP]
by simp


[STATEMENT]
lemma semilattice_inf_transfer[transfer_rule]:
  assumes [transfer_rule]: "bi_unique A" "right_total A"
  shows
    "(
      (A ===> A ===> A) ===>
      (A ===> A ===> (=)) ===>
      (A ===> A ===> (=)) ===>
      (=)
    ) (semilattice_inf_ow (Collect (Domainp A))) class.semilattice_inf"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((A ===> A ===> A) ===> (A ===> A ===> (=)) ===> (A ===> A ===> (=)) ===> (=)) (semilattice_inf_ow (Collect (Domainp A))) class.semilattice_inf
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ((A ===> A ===> A) ===> (A ===> A ===> (=)) ===> (A ===> A ===> (=)) ===> (=)) (semilattice_inf_ow (Collect (Domainp A))) class.semilattice_inf
[PROOF STEP]
let ?P =
    "(
      (A ===> A ===> A) ===>
      (A ===> A ===> (=)) ===>
      (A ===> A ===> (=)) ===>
      (=)
    )"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ((A ===> A ===> A) ===> (A ===> A ===> (=)) ===> (A ===> A ===> (=)) ===> (=)) (semilattice_inf_ow (Collect (Domainp A))) class.semilattice_inf
[PROOF STEP]
let ?semilattice_ow = "semilattice_inf_ow (Collect (Domainp A))"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ((A ===> A ===> A) ===> (A ===> A ===> (=)) ===> (A ===> A ===> (=)) ===> (=)) (semilattice_inf_ow (Collect (Domainp A))) class.semilattice_inf
[PROOF STEP]
let ?rf_UNIV =
    "(\<lambda>inf::['b, 'b] \<Rightarrow> 'b. (\<forall>x y. x \<in> UNIV \<longrightarrow> y \<in> UNIV \<longrightarrow> inf x y \<in> UNIV))"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ((A ===> A ===> A) ===> (A ===> A ===> (=)) ===> (A ===> A ===> (=)) ===> (=)) (semilattice_inf_ow (Collect (Domainp A))) class.semilattice_inf
[PROOF STEP]
have
    "?P
    ?semilattice_ow
    (\<lambda>inf le ls. ?rf_UNIV inf \<and> class.semilattice_inf inf le ls)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((A ===> A ===> A) ===> (A ===> A ===> (=)) ===> (A ===> A ===> (=)) ===> (=)) (semilattice_inf_ow (Collect (Domainp A))) (\<lambda>inf le ls. (\<forall>x y. x \<in> UNIV \<longrightarrow> y \<in> UNIV \<longrightarrow> inf x y \<in> UNIV) \<and> class.semilattice_inf inf le ls)
[PROOF STEP]
unfolding
      class.semilattice_inf_def semilattice_inf_ow_def
      class.semilattice_inf_axioms_def semilattice_inf_ow_axioms_def
      inf_ow_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((A ===> A ===> A) ===> (A ===> A ===> (=)) ===> (A ===> A ===> (=)) ===> (=)) (\<lambda>inf le ls. (\<forall>x y. x \<in> Collect (Domainp A) \<longrightarrow> y \<in> Collect (Domainp A) \<longrightarrow> inf x y \<in> Collect (Domainp A)) \<and> order_ow (Collect (Domainp A)) le ls \<and> (\<forall>x y. x \<in> Collect (Domainp A) \<longrightarrow> y \<in> Collect (Domainp A) \<longrightarrow> le (inf x y) x) \<and> (\<forall>x y. x \<in> Collect (Domainp A) \<longrightarrow> y \<in> Collect (Domainp A) \<longrightarrow> le (inf x y) y) \<and> (\<forall>x y z. x \<in> Collect (Domainp A) \<longrightarrow> y \<in> Collect (Domainp A) \<longrightarrow> z \<in> Collect (Domainp A) \<longrightarrow> le x y \<longrightarrow> le x z \<longrightarrow> le x (inf y z))) (\<lambda>inf le ls. (\<forall>x y. x \<in> UNIV \<longrightarrow> y \<in> UNIV \<longrightarrow> inf x y \<in> UNIV) \<and> class.order le ls \<and> (\<forall>x y. le (inf x y) x) \<and> (\<forall>x y. le (inf x y) y) \<and> (\<forall>x y z. le x y \<longrightarrow> le x z \<longrightarrow> le x (inf y z)))
[PROOF STEP]
apply transfer_prover_start
[PROOF STATE]
proof (prove)
goal (25 subgoals):
 1. Transfer.Rel ((=) ===> (=) ===> ?Rac54) ?aw54 (\<longrightarrow>)
 2. Transfer.Rel ((=) ===> ?Rac54 ===> ?Rab54) ?av54 (\<longrightarrow>)
 3. Transfer.Rel ((A ===> ?Rab54) ===> ?Raa54) ?au54 All
 4. Transfer.Rel ((A ===> ?Raa54) ===> ?Rz54) ?at54 All
 5. Transfer.Rel ((A ===> ?Rz54) ===> ?Rx54) ?as54 All
 6. Transfer.Rel ((A ===> (=)) ===> ?Ry54) ?ar54 All
 7. Transfer.Rel ((A ===> ?Ry54) ===> ?Rw54) ?aq54 All
 8. Transfer.Rel (?Rw54 ===> ?Rx54 ===> ?Ru54) ?ap54 (\<and>)
 9. Transfer.Rel ((A ===> (=)) ===> ?Rv54) ?ao54 All
 10. Transfer.Rel ((A ===> ?Rv54) ===> ?Rt54) ?an54 All
A total of 25 subgoals...
[PROOF STEP]
apply transfer_step+
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>inf le ls. (\<forall>x y. x \<in> Collect (Domainp A) \<longrightarrow> y \<in> Collect (Domainp A) \<longrightarrow> inf x y \<in> Collect (Domainp A)) \<and> order_ow (Collect (Domainp A)) le ls \<and> (\<forall>x y. x \<in> Collect (Domainp A) \<longrightarrow> y \<in> Collect (Domainp A) \<longrightarrow> le (inf x y) x) \<and> (\<forall>x y. x \<in> Collect (Domainp A) \<longrightarrow> y \<in> Collect (Domainp A) \<longrightarrow> le (inf x y) y) \<and> (\<forall>x y z. x \<in> Collect (Domainp A) \<longrightarrow> y \<in> Collect (Domainp A) \<longrightarrow> z \<in> Collect (Domainp A) \<longrightarrow> le x y \<longrightarrow> le x z \<longrightarrow> le x (inf y z))) = (\<lambda>inf le ls. (\<forall>x\<in>Collect (Domainp A). \<forall>y\<in>Collect (Domainp A). x \<in> Collect (Domainp A) \<longrightarrow> y \<in> Collect (Domainp A) \<longrightarrow> inf x y \<in> Collect (Domainp A)) \<and> order_ow (Collect (Domainp A)) le ls \<and> (\<forall>x\<in>Collect (Domainp A). \<forall>y\<in>Collect (Domainp A). le (inf x y) x) \<and> (\<forall>x\<in>Collect (Domainp A). \<forall>y\<in>Collect (Domainp A). le (inf x y) y) \<and> (\<forall>x\<in>Collect (Domainp A). \<forall>y\<in>Collect (Domainp A). \<forall>z\<in>Collect (Domainp A). le x y \<longrightarrow> le x z \<longrightarrow> le x (inf y z)))
[PROOF STEP]
unfolding Ball_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>inf le ls. (\<forall>x y. x \<in> Collect (Domainp A) \<longrightarrow> y \<in> Collect (Domainp A) \<longrightarrow> inf x y \<in> Collect (Domainp A)) \<and> order_ow (Collect (Domainp A)) le ls \<and> (\<forall>x y. x \<in> Collect (Domainp A) \<longrightarrow> y \<in> Collect (Domainp A) \<longrightarrow> le (inf x y) x) \<and> (\<forall>x y. x \<in> Collect (Domainp A) \<longrightarrow> y \<in> Collect (Domainp A) \<longrightarrow> le (inf x y) y) \<and> (\<forall>x y z. x \<in> Collect (Domainp A) \<longrightarrow> y \<in> Collect (Domainp A) \<longrightarrow> z \<in> Collect (Domainp A) \<longrightarrow> le x y \<longrightarrow> le x z \<longrightarrow> le x (inf y z))) = (\<lambda>inf le ls. (\<forall>x. x \<in> Collect (Domainp A) \<longrightarrow> (\<forall>xa. xa \<in> Collect (Domainp A) \<longrightarrow> x \<in> Collect (Domainp A) \<longrightarrow> xa \<in> Collect (Domainp A) \<longrightarrow> inf x xa \<in> Collect (Domainp A))) \<and> order_ow (Collect (Domainp A)) le ls \<and> (\<forall>x. x \<in> Collect (Domainp A) \<longrightarrow> (\<forall>xa. xa \<in> Collect (Domainp A) \<longrightarrow> le (inf x xa) x)) \<and> (\<forall>x. x \<in> Collect (Domainp A) \<longrightarrow> (\<forall>xa. xa \<in> Collect (Domainp A) \<longrightarrow> le (inf x xa) xa)) \<and> (\<forall>x. x \<in> Collect (Domainp A) \<longrightarrow> (\<forall>xa. xa \<in> Collect (Domainp A) \<longrightarrow> (\<forall>xb. xb \<in> Collect (Domainp A) \<longrightarrow> le x xa \<longrightarrow> le x xb \<longrightarrow> le x (inf xa xb)))))
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
((A ===> A ===> A) ===> (A ===> A ===> (=)) ===> (A ===> A ===> (=)) ===> (=)) (semilattice_inf_ow (Collect (Domainp A))) (\<lambda>inf le ls. (\<forall>x y. x \<in> UNIV \<longrightarrow> y \<in> UNIV \<longrightarrow> inf x y \<in> UNIV) \<and> class.semilattice_inf inf le ls)

goal (1 subgoal):
 1. ((A ===> A ===> A) ===> (A ===> A ===> (=)) ===> (A ===> A ===> (=)) ===> (=)) (semilattice_inf_ow (Collect (Domainp A))) class.semilattice_inf
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
((A ===> A ===> A) ===> (A ===> A ===> (=)) ===> (A ===> A ===> (=)) ===> (=)) (semilattice_inf_ow (Collect (Domainp A))) (\<lambda>inf le ls. (\<forall>x y. x \<in> UNIV \<longrightarrow> y \<in> UNIV \<longrightarrow> inf x y \<in> UNIV) \<and> class.semilattice_inf inf le ls)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
((A ===> A ===> A) ===> (A ===> A ===> (=)) ===> (A ===> A ===> (=)) ===> (=)) (semilattice_inf_ow (Collect (Domainp A))) (\<lambda>inf le ls. (\<forall>x y. x \<in> UNIV \<longrightarrow> y \<in> UNIV \<longrightarrow> inf x y \<in> UNIV) \<and> class.semilattice_inf inf le ls)

goal (1 subgoal):
 1. ((A ===> A ===> A) ===> (A ===> A ===> (=)) ===> (A ===> A ===> (=)) ===> (=)) (semilattice_inf_ow (Collect (Domainp A))) class.semilattice_inf
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
((A ===> A ===> A) ===> (A ===> A ===> (=)) ===> (A ===> A ===> (=)) ===> (=)) (semilattice_inf_ow (Collect (Domainp A))) class.semilattice_inf

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma semilattice_sup_transfer[transfer_rule]:
  assumes [transfer_rule]: "bi_unique A" "right_total A"
  shows
    "(
      (A ===> A ===> A) ===>
      (A ===> A ===> (=)) ===>
      (A ===> A ===> (=)) ===>
      (=)
    ) (semilattice_sup_ow (Collect (Domainp A))) class.semilattice_sup"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((A ===> A ===> A) ===> (A ===> A ===> (=)) ===> (A ===> A ===> (=)) ===> (=)) (semilattice_sup_ow (Collect (Domainp A))) class.semilattice_sup
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ((A ===> A ===> A) ===> (A ===> A ===> (=)) ===> (A ===> A ===> (=)) ===> (=)) (semilattice_sup_ow (Collect (Domainp A))) class.semilattice_sup
[PROOF STEP]
let ?P =
    "(
      (A ===> A ===> A) ===>
      (A ===> A ===> (=)) ===>
      (A ===> A ===> (=)) ===>
      (=)
    )"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ((A ===> A ===> A) ===> (A ===> A ===> (=)) ===> (A ===> A ===> (=)) ===> (=)) (semilattice_sup_ow (Collect (Domainp A))) class.semilattice_sup
[PROOF STEP]
let ?semilattice_ow = "semilattice_sup_ow (Collect (Domainp A))"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ((A ===> A ===> A) ===> (A ===> A ===> (=)) ===> (A ===> A ===> (=)) ===> (=)) (semilattice_sup_ow (Collect (Domainp A))) class.semilattice_sup
[PROOF STEP]
let ?rf_UNIV =
    "(\<lambda>sup::['b, 'b] \<Rightarrow> 'b. (\<forall>x y. x \<in> UNIV \<longrightarrow> y \<in> UNIV \<longrightarrow> sup x y \<in> UNIV))"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ((A ===> A ===> A) ===> (A ===> A ===> (=)) ===> (A ===> A ===> (=)) ===> (=)) (semilattice_sup_ow (Collect (Domainp A))) class.semilattice_sup
[PROOF STEP]
have
    "?P
    ?semilattice_ow
    (\<lambda>sup le ls. ?rf_UNIV sup \<and> class.semilattice_sup sup le ls)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((A ===> A ===> A) ===> (A ===> A ===> (=)) ===> (A ===> A ===> (=)) ===> (=)) (semilattice_sup_ow (Collect (Domainp A))) (\<lambda>sup le ls. (\<forall>x y. x \<in> UNIV \<longrightarrow> y \<in> UNIV \<longrightarrow> sup x y \<in> UNIV) \<and> class.semilattice_sup sup le ls)
[PROOF STEP]
unfolding
    class.semilattice_sup_def semilattice_sup_ow_def
    class.semilattice_sup_axioms_def semilattice_sup_ow_axioms_def
    sup_ow_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((A ===> A ===> A) ===> (A ===> A ===> (=)) ===> (A ===> A ===> (=)) ===> (=)) (\<lambda>sup le ls. (\<forall>x y. x \<in> Collect (Domainp A) \<longrightarrow> y \<in> Collect (Domainp A) \<longrightarrow> sup x y \<in> Collect (Domainp A)) \<and> order_ow (Collect (Domainp A)) le ls \<and> (\<forall>x y. x \<in> Collect (Domainp A) \<longrightarrow> y \<in> Collect (Domainp A) \<longrightarrow> le x (sup x y)) \<and> (\<forall>y x. y \<in> Collect (Domainp A) \<longrightarrow> x \<in> Collect (Domainp A) \<longrightarrow> le y (sup x y)) \<and> (\<forall>y x z. y \<in> Collect (Domainp A) \<longrightarrow> x \<in> Collect (Domainp A) \<longrightarrow> z \<in> Collect (Domainp A) \<longrightarrow> le y x \<longrightarrow> le z x \<longrightarrow> le (sup y z) x)) (\<lambda>sup le ls. (\<forall>x y. x \<in> UNIV \<longrightarrow> y \<in> UNIV \<longrightarrow> sup x y \<in> UNIV) \<and> class.order le ls \<and> (\<forall>x y. le x (sup x y)) \<and> (\<forall>y x. le y (sup x y)) \<and> (\<forall>y x z. le y x \<longrightarrow> le z x \<longrightarrow> le (sup y z) x))
[PROOF STEP]
apply transfer_prover_start
[PROOF STATE]
proof (prove)
goal (25 subgoals):
 1. Transfer.Rel ((=) ===> (=) ===> ?Rac54) ?aw54 (\<longrightarrow>)
 2. Transfer.Rel ((=) ===> ?Rac54 ===> ?Rab54) ?av54 (\<longrightarrow>)
 3. Transfer.Rel ((A ===> ?Rab54) ===> ?Raa54) ?au54 All
 4. Transfer.Rel ((A ===> ?Raa54) ===> ?Rz54) ?at54 All
 5. Transfer.Rel ((A ===> ?Rz54) ===> ?Rx54) ?as54 All
 6. Transfer.Rel ((A ===> (=)) ===> ?Ry54) ?ar54 All
 7. Transfer.Rel ((A ===> ?Ry54) ===> ?Rw54) ?aq54 All
 8. Transfer.Rel (?Rw54 ===> ?Rx54 ===> ?Ru54) ?ap54 (\<and>)
 9. Transfer.Rel ((A ===> (=)) ===> ?Rv54) ?ao54 All
 10. Transfer.Rel ((A ===> ?Rv54) ===> ?Rt54) ?an54 All
A total of 25 subgoals...
[PROOF STEP]
apply transfer_step+
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>sup le ls. (\<forall>x y. x \<in> Collect (Domainp A) \<longrightarrow> y \<in> Collect (Domainp A) \<longrightarrow> sup x y \<in> Collect (Domainp A)) \<and> order_ow (Collect (Domainp A)) le ls \<and> (\<forall>x y. x \<in> Collect (Domainp A) \<longrightarrow> y \<in> Collect (Domainp A) \<longrightarrow> le x (sup x y)) \<and> (\<forall>y x. y \<in> Collect (Domainp A) \<longrightarrow> x \<in> Collect (Domainp A) \<longrightarrow> le y (sup x y)) \<and> (\<forall>y x z. y \<in> Collect (Domainp A) \<longrightarrow> x \<in> Collect (Domainp A) \<longrightarrow> z \<in> Collect (Domainp A) \<longrightarrow> le y x \<longrightarrow> le z x \<longrightarrow> le (sup y z) x)) = (\<lambda>sup le ls. (\<forall>x\<in>Collect (Domainp A). \<forall>y\<in>Collect (Domainp A). x \<in> Collect (Domainp A) \<longrightarrow> y \<in> Collect (Domainp A) \<longrightarrow> sup x y \<in> Collect (Domainp A)) \<and> order_ow (Collect (Domainp A)) le ls \<and> (\<forall>x\<in>Collect (Domainp A). \<forall>y\<in>Collect (Domainp A). le x (sup x y)) \<and> (\<forall>y\<in>Collect (Domainp A). \<forall>x\<in>Collect (Domainp A). le y (sup x y)) \<and> (\<forall>y\<in>Collect (Domainp A). \<forall>x\<in>Collect (Domainp A). \<forall>z\<in>Collect (Domainp A). le y x \<longrightarrow> le z x \<longrightarrow> le (sup y z) x))
[PROOF STEP]
unfolding Ball_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>sup le ls. (\<forall>x y. x \<in> Collect (Domainp A) \<longrightarrow> y \<in> Collect (Domainp A) \<longrightarrow> sup x y \<in> Collect (Domainp A)) \<and> order_ow (Collect (Domainp A)) le ls \<and> (\<forall>x y. x \<in> Collect (Domainp A) \<longrightarrow> y \<in> Collect (Domainp A) \<longrightarrow> le x (sup x y)) \<and> (\<forall>y x. y \<in> Collect (Domainp A) \<longrightarrow> x \<in> Collect (Domainp A) \<longrightarrow> le y (sup x y)) \<and> (\<forall>y x z. y \<in> Collect (Domainp A) \<longrightarrow> x \<in> Collect (Domainp A) \<longrightarrow> z \<in> Collect (Domainp A) \<longrightarrow> le y x \<longrightarrow> le z x \<longrightarrow> le (sup y z) x)) = (\<lambda>sup le ls. (\<forall>x. x \<in> Collect (Domainp A) \<longrightarrow> (\<forall>xa. xa \<in> Collect (Domainp A) \<longrightarrow> x \<in> Collect (Domainp A) \<longrightarrow> xa \<in> Collect (Domainp A) \<longrightarrow> sup x xa \<in> Collect (Domainp A))) \<and> order_ow (Collect (Domainp A)) le ls \<and> (\<forall>x. x \<in> Collect (Domainp A) \<longrightarrow> (\<forall>xa. xa \<in> Collect (Domainp A) \<longrightarrow> le x (sup x xa))) \<and> (\<forall>x. x \<in> Collect (Domainp A) \<longrightarrow> (\<forall>xa. xa \<in> Collect (Domainp A) \<longrightarrow> le x (sup xa x))) \<and> (\<forall>x. x \<in> Collect (Domainp A) \<longrightarrow> (\<forall>xa. xa \<in> Collect (Domainp A) \<longrightarrow> (\<forall>xb. xb \<in> Collect (Domainp A) \<longrightarrow> le x xa \<longrightarrow> le xb xa \<longrightarrow> le (sup x xb) xa))))
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
((A ===> A ===> A) ===> (A ===> A ===> (=)) ===> (A ===> A ===> (=)) ===> (=)) (semilattice_sup_ow (Collect (Domainp A))) (\<lambda>sup le ls. (\<forall>x y. x \<in> UNIV \<longrightarrow> y \<in> UNIV \<longrightarrow> sup x y \<in> UNIV) \<and> class.semilattice_sup sup le ls)

goal (1 subgoal):
 1. ((A ===> A ===> A) ===> (A ===> A ===> (=)) ===> (A ===> A ===> (=)) ===> (=)) (semilattice_sup_ow (Collect (Domainp A))) class.semilattice_sup
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
((A ===> A ===> A) ===> (A ===> A ===> (=)) ===> (A ===> A ===> (=)) ===> (=)) (semilattice_sup_ow (Collect (Domainp A))) (\<lambda>sup le ls. (\<forall>x y. x \<in> UNIV \<longrightarrow> y \<in> UNIV \<longrightarrow> sup x y \<in> UNIV) \<and> class.semilattice_sup sup le ls)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
((A ===> A ===> A) ===> (A ===> A ===> (=)) ===> (A ===> A ===> (=)) ===> (=)) (semilattice_sup_ow (Collect (Domainp A))) (\<lambda>sup le ls. (\<forall>x y. x \<in> UNIV \<longrightarrow> y \<in> UNIV \<longrightarrow> sup x y \<in> UNIV) \<and> class.semilattice_sup sup le ls)

goal (1 subgoal):
 1. ((A ===> A ===> A) ===> (A ===> A ===> (=)) ===> (A ===> A ===> (=)) ===> (=)) (semilattice_sup_ow (Collect (Domainp A))) class.semilattice_sup
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
((A ===> A ===> A) ===> (A ===> A ===> (=)) ===> (A ===> A ===> (=)) ===> (=)) (semilattice_sup_ow (Collect (Domainp A))) class.semilattice_sup

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma semilattice_neutral_transfer[transfer_rule]:
  assumes [transfer_rule]: "bi_unique A" "right_total A"
  shows
    "((A ===> A ===> A) ===> A ===> (=))
      (semilattice_neutral_ow (Collect (Domainp A))) semilattice_neutr"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((A ===> A ===> A) ===> A ===> (=)) (semilattice_neutral_ow (Collect (Domainp A))) semilattice_neutr
[PROOF STEP]
unfolding semilattice_neutral_ow_def semilattice_neutr_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((A ===> A ===> A) ===> A ===> (=)) (\<lambda>f z. semilattice_ow (Collect (Domainp A)) f \<and> comm_monoid_ow (Collect (Domainp A)) f z) (\<lambda>f z. semilattice f \<and> comm_monoid f z)
[PROOF STEP]
by transfer_prover


[STATEMENT]
lemma semilattice_neutr_order_transfer[transfer_rule]:
  assumes [transfer_rule]: "bi_unique A" "right_total A"
  shows
    "(
      (A ===> A ===> A) ===>
      A ===>
      (A ===> A ===> (=)) ===>
      (A ===> A ===> (=)) ===>
      (=)
    )
    (semilattice_neutral_order_ow (Collect (Domainp A)))
    semilattice_neutr_order"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((A ===> A ===> A) ===> A ===> (A ===> A ===> (=)) ===> (A ===> A ===> (=)) ===> (=)) (semilattice_neutral_order_ow (Collect (Domainp A))) semilattice_neutr_order
[PROOF STEP]
unfolding semilattice_neutral_order_ow_def semilattice_neutr_order_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((A ===> A ===> A) ===> A ===> (A ===> A ===> (=)) ===> (A ===> A ===> (=)) ===> (=)) (\<lambda>f z le ls. semilattice_neutral_ow (Collect (Domainp A)) f z \<and> semilattice_order_ow (Collect (Domainp A)) f le ls) (\<lambda>f z less_eq less. semilattice_neutr f z \<and> semilattice_order f less_eq less)
[PROOF STEP]
by transfer_prover


[STATEMENT]
lemma bounded_semilattice_inf_top_transfer[transfer_rule]:
  assumes [transfer_rule]: "bi_unique A" "right_total A"
  shows
    "(
      (A ===> A ===> A) ===>
      (A ===> A ===> (=)) ===>
      (A ===> A ===> (=)) ===>
      A ===>
      (=)
    )
    (bounded_semilattice_inf_top_ow (Collect (Domainp A)))
    class.bounded_semilattice_inf_top"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((A ===> A ===> A) ===> (A ===> A ===> (=)) ===> (A ===> A ===> (=)) ===> A ===> (=)) (bounded_semilattice_inf_top_ow (Collect (Domainp A))) class.bounded_semilattice_inf_top
[PROOF STEP]
unfolding
    bounded_semilattice_inf_top_ow_def class.bounded_semilattice_inf_top_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((A ===> A ===> A) ===> (A ===> A ===> (=)) ===> (A ===> A ===> (=)) ===> A ===> (=)) (\<lambda>inf le ls top. semilattice_inf_ow (Collect (Domainp A)) inf le ls \<and> order_top_ow (Collect (Domainp A)) le ls top) (\<lambda>inf less_eq less top. class.semilattice_inf inf less_eq less \<and> class.order_top less_eq less top)
[PROOF STEP]
by transfer_prover


[STATEMENT]
lemma bounded_semilattice_sup_bot_transfer[transfer_rule]:
  assumes [transfer_rule]: "bi_unique A" "right_total A"
  shows
    "(
      (A ===> A ===> A) ===>
      (A ===> A ===> (=)) ===>
      (A ===> A ===> (=)) ===>
      A ===>
      (=)
    )
    (bounded_semilattice_sup_bot_ow (Collect (Domainp A)))
    class.bounded_semilattice_sup_bot"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((A ===> A ===> A) ===> (A ===> A ===> (=)) ===> (A ===> A ===> (=)) ===> A ===> (=)) (bounded_semilattice_sup_bot_ow (Collect (Domainp A))) class.bounded_semilattice_sup_bot
[PROOF STEP]
unfolding
    bounded_semilattice_sup_bot_ow_def class.bounded_semilattice_sup_bot_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((A ===> A ===> A) ===> (A ===> A ===> (=)) ===> (A ===> A ===> (=)) ===> A ===> (=)) (\<lambda>sup le ls bot. semilattice_sup_ow (Collect (Domainp A)) sup le ls \<and> order_bot_ow (Collect (Domainp A)) bot le ls) (\<lambda>sup less_eq less bot. class.semilattice_sup sup less_eq less \<and> class.order_bot bot less_eq less)
[PROOF STEP]
by transfer_prover


[STATEMENT]
lemma false_not_true: "is_false d \<Longrightarrow> \<not> is_true d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_false d \<Longrightarrow> \<not> is_true d
[PROOF STEP]
using not_true_and_false
[PROOF STATE]
proof (prove)
using this:
\<not> (is_true ?d \<and> is_false ?d)

goal (1 subgoal):
 1. is_false d \<Longrightarrow> \<not> is_true d
[PROOF STEP]
by blast


[STATEMENT]
lemma true_not_false: "is_true d \<Longrightarrow> \<not> is_false d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_true d \<Longrightarrow> \<not> is_false d
[PROOF STEP]
using not_true_and_false
[PROOF STATE]
proof (prove)
using this:
\<not> (is_true ?d \<and> is_false ?d)

goal (1 subgoal):
 1. is_true d \<Longrightarrow> \<not> is_false d
[PROOF STEP]
by blast


[STATEMENT]
lemma is_true_and_is_false_implies_False: "is_true d \<Longrightarrow> is_false d \<Longrightarrow> False"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_true d; is_false d\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
using true_not_false false_not_true
[PROOF STATE]
proof (prove)
using this:
is_true ?d \<Longrightarrow> \<not> is_false ?d
is_false ?d \<Longrightarrow> \<not> is_true ?d

goal (1 subgoal):
 1. \<lbrakk>is_true d; is_false d\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
by simp


[STATEMENT]
lemma ground_mctxt_map_vars_mctxt [simp]:
  "ground_mctxt (map_vars_mctxt f C) = ground_mctxt C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ground_mctxt (map_vars_mctxt f C) = ground_mctxt C
[PROOF STEP]
by (induct C) auto


[STATEMENT]
lemma root_single_automaton:
  assumes "RR2_spec \<A> R"
  shows "RR2_spec \<A> (lift_root_step \<F> PRoot ESingle R)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. RR2_spec \<A> (lift_root_step \<F> PRoot ESingle R)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
RR2_spec \<A> R

goal (1 subgoal):
 1. RR2_spec \<A> (lift_root_step \<F> PRoot ESingle R)
[PROOF STEP]
unfolding RR2_spec_def
[PROOF STATE]
proof (prove)
using this:
\<L> \<A> = {gpair t u |t u. (t, u) \<in> R}

goal (1 subgoal):
 1. \<L> \<A> = {gpair t u |t u. (t, u) \<in> lift_root_step \<F> PRoot ESingle R}
[PROOF STEP]
by (auto simp: lift_root_step.simps)


[STATEMENT]
lemma root_strictparallel_automaton:
  assumes "RR2_spec \<A> R"
  shows "RR2_spec \<A> (lift_root_step \<F> PRoot EStrictParallel R)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. RR2_spec \<A> (lift_root_step \<F> PRoot EStrictParallel R)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
RR2_spec \<A> R

goal (1 subgoal):
 1. RR2_spec \<A> (lift_root_step \<F> PRoot EStrictParallel R)
[PROOF STEP]
unfolding RR2_spec_def
[PROOF STATE]
proof (prove)
using this:
\<L> \<A> = {gpair t u |t u. (t, u) \<in> R}

goal (1 subgoal):
 1. \<L> \<A> = {gpair t u |t u. (t, u) \<in> lift_root_step \<F> PRoot EStrictParallel R}
[PROOF STEP]
by (auto simp: lift_root_step.simps)


[STATEMENT]
lemma reflcl_automaton:
  assumes "RR2_spec \<A> R"
  shows "RR2_spec (reflcl_reg (lift_sig_RR2 |`| \<F>) \<A>) (lift_root_step (fset \<F>) PRoot EParallel R)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. RR2_spec (reflcl_reg (lift_sig_RR2 |`| \<F>) \<A>) (lift_root_step (fset \<F>) PRoot EParallel R)
[PROOF STEP]
unfolding RR2_spec_def \<L>_reflcl_reg
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<L> \<A> \<union> \<T>\<^sub>G (fset (lift_sig_RR2 |`| \<F>)) = {gpair t u |t u. (t, u) \<in> lift_root_step (fset \<F>) PRoot EParallel R}
[PROOF STEP]
unfolding lift_root_step.simps \<T>\<^sub>G_equivalent_def assms[unfolded RR2_spec_def]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {gpair t u |t u. (t, u) \<in> R} \<union> gterms (fset (lift_sig_RR2 |`| \<F>)) = {gpair t u |t u. (t, u) \<in> R \<union> Restr Id (gterms (fset \<F>))}
[PROOF STEP]
by (auto simp flip: \<T>\<^sub>G_equivalent_def)


[STATEMENT]
lemma parallel_closure_automaton:
  assumes "RR2_spec \<A> R"
  shows "RR2_spec (parallel_closure_reg (lift_sig_RR2 |`| \<F>) \<A>) (lift_root_step (fset \<F>) PAny EParallel R)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. RR2_spec (parallel_closure_reg (lift_sig_RR2 |`| \<F>) \<A>) (lift_root_step (fset \<F>) PAny EParallel R)
[PROOF STEP]
unfolding RR2_spec_def parallelcl_gmctxt_lang lift_root_step.simps
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {fill_gholes C ss |C ss. num_gholes C = length ss \<and> funas_gmctxt C \<subseteq> fset (lift_sig_RR2 |`| \<F>) \<and> (\<forall>i<length ss. ss ! i \<in> \<L> \<A>)} = {gpair t u |t u. (t, u) \<in> gmctxtcl_funas (fset \<F>) R}
[PROOF STEP]
unfolding gmctxtex_onp_gpair_set_conv assms[unfolded RR2_spec_def]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {fill_gholes C ss |C ss. num_gholes C = length ss \<and> funas_gmctxt C \<subseteq> fset (lift_sig_RR2 |`| \<F>) \<and> (\<forall>i<length ss. ss ! i \<in> {gpair t u |t u. (t, u) \<in> R})} = {fill_gholes (map_gmctxt lift_fun C) ss |C ss. num_gholes C = length ss \<and> funas_gmctxt C \<subseteq> fset \<F> \<and> (\<forall>i<length ss. ss ! i \<in> {gpair t u |t u. (t, u) \<in> R})}
[PROOF STEP]
by (intro RR2_gmctxt_cl_to_gmctxt) auto


[STATEMENT]
lemma ctxt_closure_automaton:
  assumes "RR2_spec \<A> R"
  shows "RR2_spec (ctxt_closure_reg (lift_sig_RR2 |`| \<F>) \<A>) (lift_root_step (fset \<F>) PAny ESingle R)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. RR2_spec (ctxt_closure_reg (lift_sig_RR2 |`| \<F>) \<A>) (lift_root_step (fset \<F>) PAny ESingle R)
[PROOF STEP]
unfolding RR2_spec_def gctxt_closure_lang lift_root_step.simps
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {C\<langle>s\<rangle>\<^sub>G |C s. funas_gctxt C \<subseteq> fset (lift_sig_RR2 |`| \<F>) \<and> s \<in> \<L> \<A>} = {gpair t u |t u. (t, u) \<in> gctxtcl_funas (fset \<F>) R}
[PROOF STEP]
unfolding gctxtex_onp_gpair_set_conv assms[unfolded RR2_spec_def]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {C\<langle>s\<rangle>\<^sub>G |C s. funas_gctxt C \<subseteq> fset (lift_sig_RR2 |`| \<F>) \<and> s \<in> {gpair t u |t u. (t, u) \<in> R}} = {(map_gctxt lift_fun C)\<langle>s\<rangle>\<^sub>G |C s. funas_gctxt C \<subseteq> fset \<F> \<and> s \<in> {gpair t u |t u. (t, u) \<in> R}}
[PROOF STEP]
by (intro RR2_gctxt_cl_to_gctxt) auto


[STATEMENT]
lemma mctxt_closure_automaton:
  assumes "RR2_spec \<A> R"
  shows "RR2_spec (mctxt_closure_reg (lift_sig_RR2 |`| \<F>) \<A>) (lift_root_step (fset \<F>) PAny EStrictParallel R)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. RR2_spec (mctxt_closure_reg (lift_sig_RR2 |`| \<F>) \<A>) (lift_root_step (fset \<F>) PAny EStrictParallel R)
[PROOF STEP]
unfolding RR2_spec_def gmctxt_closure_lang lift_root_step.simps
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {fill_gholes C ss |C ss. num_gholes C = length ss \<and> 0 < num_gholes C \<and> funas_gmctxt C \<subseteq> fset (lift_sig_RR2 |`| \<F>) \<and> (\<forall>i<length ss. ss ! i \<in> \<L> \<A>)} = {gpair t u |t u. (t, u) \<in> gmctxtcl_funas_strict (fset \<F>) R}
[PROOF STEP]
unfolding gmctxtex_onp_gpair_set_conv assms[unfolded RR2_spec_def] conj_assoc
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {fill_gholes C ss |C ss. num_gholes C = length ss \<and> 0 < num_gholes C \<and> funas_gmctxt C \<subseteq> fset (lift_sig_RR2 |`| \<F>) \<and> (\<forall>i<length ss. ss ! i \<in> {gpair t u |t u. (t, u) \<in> R})} = {fill_gholes (map_gmctxt lift_fun C) ss |C ss. num_gholes C = length ss \<and> 0 < num_gholes C \<and> funas_gmctxt C \<subseteq> fset \<F> \<and> (\<forall>i<length ss. ss ! i \<in> {gpair t u |t u. (t, u) \<in> R})}
[PROOF STEP]
by (intro RR2_gmctxt_cl_to_gmctxt[where ?P = "\<lambda> C. 0 < num_gholes C \<and> funas_gmctxt C \<subseteq> fset (lift_sig_RR2 |`| \<F>)" and
       ?R = "\<lambda> C. 0 < num_gholes C \<and> funas_gmctxt C \<subseteq> fset \<F>", unfolded conj_assoc]) auto


[STATEMENT]
lemma nhole_ctxt_closure_automaton:
  assumes "RR2_spec \<A> R"
  shows "RR2_spec (nhole_ctxt_closure_reg (lift_sig_RR2 |`| \<F>) \<A>) (lift_root_step (fset \<F>) PNonRoot ESingle R)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. RR2_spec (nhole_ctxt_closure_reg (lift_sig_RR2 |`| \<F>) \<A>) (lift_root_step (fset \<F>) PNonRoot ESingle R)
[PROOF STEP]
unfolding RR2_spec_def nhole_ctxtcl_lang lift_root_step.simps
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {C\<langle>s\<rangle>\<^sub>G |C s. C \<noteq> \<box>\<^sub>G \<and> funas_gctxt C \<subseteq> fset (lift_sig_RR2 |`| \<F>) \<and> s \<in> \<L> \<A>} = {gpair t u |t u. (t, u) \<in> gctxtex_funas_nroot (fset \<F>) R}
[PROOF STEP]
unfolding gctxtex_onp_gpair_set_conv assms[unfolded RR2_spec_def]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {C\<langle>s\<rangle>\<^sub>G |C s. C \<noteq> \<box>\<^sub>G \<and> funas_gctxt C \<subseteq> fset (lift_sig_RR2 |`| \<F>) \<and> s \<in> {gpair t u |t u. (t, u) \<in> R}} = {(map_gctxt lift_fun C)\<langle>s\<rangle>\<^sub>G |C s. (funas_gctxt C \<subseteq> fset \<F> \<and> C \<noteq> \<box>\<^sub>G) \<and> s \<in> {gpair t u |t u. (t, u) \<in> R}}
[PROOF STEP]
by (intro RR2_gctxt_cl_to_gctxt[where
    ?P = "\<lambda> C. C \<noteq> \<box>\<^sub>G \<and> funas_gctxt C \<subseteq> fset (lift_sig_RR2 |`| \<F>)", unfolded conj_assoc]) auto


[STATEMENT]
lemma nhole_mctxt_closure_automaton:
  assumes "RR2_spec \<A> R"
  shows "RR2_spec (nhole_mctxt_closure_reg (lift_sig_RR2 |`| \<F>) \<A>) (lift_root_step (fset \<F>) PNonRoot EStrictParallel R)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. RR2_spec (nhole_mctxt_closure_reg (lift_sig_RR2 |`| \<F>) \<A>) (lift_root_step (fset \<F>) PNonRoot EStrictParallel R)
[PROOF STEP]
unfolding RR2_spec_def nhole_gmctxt_closure_lang lift_root_step.simps
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {fill_gholes C ss |C ss. num_gholes C = length ss \<and> 0 < num_gholes C \<and> C \<noteq> GMHole \<and> funas_gmctxt C \<subseteq> fset (lift_sig_RR2 |`| \<F>) \<and> (\<forall>i<length ss. ss ! i \<in> \<L> \<A>)} = {gpair t u |t u. (t, u) \<in> gmctxtex_funas_nroot_strict (fset \<F>) R}
[PROOF STEP]
unfolding gmctxtex_onp_gpair_set_conv assms[unfolded RR2_spec_def]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {fill_gholes C ss |C ss. num_gholes C = length ss \<and> 0 < num_gholes C \<and> C \<noteq> GMHole \<and> funas_gmctxt C \<subseteq> fset (lift_sig_RR2 |`| \<F>) \<and> (\<forall>i<length ss. ss ! i \<in> {gpair t u |t u. (t, u) \<in> R})} = {fill_gholes (map_gmctxt lift_fun C) ss |C ss. num_gholes C = length ss \<and> (0 < num_gholes C \<and> funas_gmctxt C \<subseteq> fset \<F> \<and> C \<noteq> GMHole) \<and> (\<forall>i<length ss. ss ! i \<in> {gpair t u |t u. (t, u) \<in> R})}
[PROOF STEP]
by (intro RR2_gmctxt_cl_to_gmctxt[where
    ?P = "\<lambda> C. 0 < num_gholes C \<and> C \<noteq> GMHole \<and> funas_gmctxt C \<subseteq> fset (lift_sig_RR2 |`| \<F>)", unfolded conj_assoc])
    auto


[STATEMENT]
lemma nhole_mctxt_reflcl_automaton:
  assumes "RR2_spec \<A> R"
  shows "RR2_spec (nhole_mctxt_reflcl_reg (lift_sig_RR2 |`| \<F>) \<A>) (lift_root_step (fset \<F>) PNonRoot EParallel R)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. RR2_spec (nhole_mctxt_reflcl_reg (lift_sig_RR2 |`| \<F>) \<A>) (lift_root_step (fset \<F>) PNonRoot EParallel R)
[PROOF STEP]
using nhole_mctxt_closure_automaton[OF assms, of \<F>]
[PROOF STATE]
proof (prove)
using this:
RR2_spec (nhole_mctxt_closure_reg (lift_sig_RR2 |`| \<F>) \<A>) (lift_root_step (fset \<F>) PNonRoot EStrictParallel R)

goal (1 subgoal):
 1. RR2_spec (nhole_mctxt_reflcl_reg (lift_sig_RR2 |`| \<F>) \<A>) (lift_root_step (fset \<F>) PNonRoot EParallel R)
[PROOF STEP]
unfolding RR2_spec_def lift_root_step_Parallel_conv nhole_mctxt_reflcl_lang
[PROOF STATE]
proof (prove)
using this:
\<L> (nhole_mctxt_closure_reg (lift_sig_RR2 |`| \<F>) \<A>) = {gpair t u |t u. (t, u) \<in> lift_root_step (fset \<F>) PNonRoot EStrictParallel R}

goal (1 subgoal):
 1. \<L> (nhole_mctxt_closure_reg (lift_sig_RR2 |`| \<F>) \<A>) \<union> \<T>\<^sub>G (fset (lift_sig_RR2 |`| \<F>)) = {gpair t u |t u. (t, u) \<in> lift_root_step (fset \<F>) PNonRoot EStrictParallel R \<union> Restr Id (\<T>\<^sub>G (fset \<F>))}
[PROOF STEP]
by (auto simp flip: \<T>\<^sub>G_equivalent_def)


[STATEMENT]
lemma GTT_to_RR2_root:
  "RR2_spec (GTT_to_RR2_root_reg \<G>) (agtt_lang \<G>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. RR2_spec (GTT_to_RR2_root_reg \<G>) (agtt_lang \<G>)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. RR2_spec (GTT_to_RR2_root_reg \<G>) (agtt_lang \<G>)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. RR2_spec (GTT_to_RR2_root_reg \<G>) (agtt_lang \<G>)
[PROOF STEP]
fix s
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. RR2_spec (GTT_to_RR2_root_reg \<G>) (agtt_lang \<G>)
[PROOF STEP]
assume "s \<in> \<L> (GTT_to_RR2_root_reg \<G>)"
[PROOF STATE]
proof (state)
this:
s \<in> \<L> (GTT_to_RR2_root_reg \<G>)

goal (1 subgoal):
 1. RR2_spec (GTT_to_RR2_root_reg \<G>) (agtt_lang \<G>)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
s \<in> \<L> (GTT_to_RR2_root_reg \<G>)
[PROOF STEP]
obtain q where q: "q |\<in>| fin (GTT_to_RR2_root_reg \<G>)" "q |\<in>| ta_der (GTT_to_RR2_root \<G>) (term_of_gterm s)"
[PROOF STATE]
proof (prove)
using this:
s \<in> \<L> (GTT_to_RR2_root_reg \<G>)

goal (1 subgoal):
 1. (\<And>q. \<lbrakk>q |\<in>| fin (GTT_to_RR2_root_reg \<G>); q |\<in>| ta_der (GTT_to_RR2_root \<G>) (term_of_gterm s)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp: \<L>_def gta_lang_def GTT_to_RR2_root_reg_def gta_der_def)
[PROOF STATE]
proof (state)
this:
q |\<in>| fin (GTT_to_RR2_root_reg \<G>)
q |\<in>| ta_der (GTT_to_RR2_root \<G>) (term_of_gterm s)

goal (1 subgoal):
 1. RR2_spec (GTT_to_RR2_root_reg \<G>) (agtt_lang \<G>)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
q |\<in>| fin (GTT_to_RR2_root_reg \<G>)
q |\<in>| ta_der (GTT_to_RR2_root \<G>) (term_of_gterm s)
[PROOF STEP]
obtain q' where [simp]: "q = (Some q', Some q')"
[PROOF STATE]
proof (prove)
using this:
q |\<in>| fin (GTT_to_RR2_root_reg \<G>)
q |\<in>| ta_der (GTT_to_RR2_root \<G>) (term_of_gterm s)

goal (1 subgoal):
 1. (\<And>q'. q = lift_fun q' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using q(1)
[PROOF STATE]
proof (prove)
using this:
q |\<in>| fin (GTT_to_RR2_root_reg \<G>)
q |\<in>| ta_der (GTT_to_RR2_root \<G>) (term_of_gterm s)
q |\<in>| fin (GTT_to_RR2_root_reg \<G>)

goal (1 subgoal):
 1. (\<And>q'. q = lift_fun q' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp: GTT_to_RR2_root_reg_def)
[PROOF STATE]
proof (state)
this:
q = lift_fun q'

goal (1 subgoal):
 1. RR2_spec (GTT_to_RR2_root_reg \<G>) (agtt_lang \<G>)
[PROOF STEP]
have "\<exists>t u q. s = gpair t u \<and> q |\<in>| ta_der (fst \<G>) (term_of_gterm t) \<and> q |\<in>| ta_der (snd \<G>) (term_of_gterm u)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>t u q. s = gpair t u \<and> q |\<in>| ta_der (fst \<G>) (term_of_gterm t) \<and> q |\<in>| ta_der (snd \<G>) (term_of_gterm u)
[PROOF STEP]
using fsubsetD[OF ta_der_mono' q(2), of "pair_automaton (fst \<G>) (snd \<G>)"]
[PROOF STATE]
proof (prove)
using this:
ta_subset (GTT_to_RR2_root \<G>) (pair_automaton (fst \<G>) (snd \<G>)) \<Longrightarrow> q |\<in>| ta_der (pair_automaton (fst \<G>) (snd \<G>)) (term_of_gterm s)

goal (1 subgoal):
 1. \<exists>t u q. s = gpair t u \<and> q |\<in>| ta_der (fst \<G>) (term_of_gterm t) \<and> q |\<in>| ta_der (snd \<G>) (term_of_gterm u)
[PROOF STEP]
by (auto simp: GTT_to_RR2_root_def dest!: from_ta_der_pair_automaton(4))
[PROOF STATE]
proof (state)
this:
\<exists>t u q. s = gpair t u \<and> q |\<in>| ta_der (fst \<G>) (term_of_gterm t) \<and> q |\<in>| ta_der (snd \<G>) (term_of_gterm u)

goal (1 subgoal):
 1. RR2_spec (GTT_to_RR2_root_reg \<G>) (agtt_lang \<G>)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?s2 \<in> \<L> (GTT_to_RR2_root_reg \<G>) \<Longrightarrow> \<exists>t u q. ?s2 = gpair t u \<and> q |\<in>| ta_der (fst \<G>) (term_of_gterm t) \<and> q |\<in>| ta_der (snd \<G>) (term_of_gterm u)

goal (1 subgoal):
 1. RR2_spec (GTT_to_RR2_root_reg \<G>) (agtt_lang \<G>)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
?s2 \<in> \<L> (GTT_to_RR2_root_reg \<G>) \<Longrightarrow> \<exists>t u q. ?s2 = gpair t u \<and> q |\<in>| ta_der (fst \<G>) (term_of_gterm t) \<and> q |\<in>| ta_der (snd \<G>) (term_of_gterm u)

goal (1 subgoal):
 1. RR2_spec (GTT_to_RR2_root_reg \<G>) (agtt_lang \<G>)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
?s2 \<in> \<L> (GTT_to_RR2_root_reg \<G>) \<Longrightarrow> \<exists>t u q. ?s2 = gpair t u \<and> q |\<in>| ta_der (fst \<G>) (term_of_gterm t) \<and> q |\<in>| ta_der (snd \<G>) (term_of_gterm u)

goal (1 subgoal):
 1. RR2_spec (GTT_to_RR2_root_reg \<G>) (agtt_lang \<G>)
[PROOF STEP]
fix t u q
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. RR2_spec (GTT_to_RR2_root_reg \<G>) (agtt_lang \<G>)
[PROOF STEP]
assume q: "q |\<in>| ta_der (fst \<G>) (term_of_gterm t)" "q |\<in>| ta_der (snd \<G>) (term_of_gterm u)"
[PROOF STATE]
proof (state)
this:
q |\<in>| ta_der (fst \<G>) (term_of_gterm t)
q |\<in>| ta_der (snd \<G>) (term_of_gterm u)

goal (1 subgoal):
 1. RR2_spec (GTT_to_RR2_root_reg \<G>) (agtt_lang \<G>)
[PROOF STEP]
have "lift_fun q |\<in>| map_both Some |`| fId_on (\<Q> (fst \<G>) |\<union>| \<Q> (snd \<G>))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lift_fun q |\<in>| map_both Some |`| fId_on (\<Q> (fst \<G>) |\<union>| \<Q> (snd \<G>))
[PROOF STEP]
using q[THEN fsubsetD[OF ground_ta_der_states[OF  ground_term_of_gterm]]]
[PROOF STATE]
proof (prove)
using this:
q |\<in>| \<Q> (fst \<G>)
q |\<in>| \<Q> (snd \<G>)

goal (1 subgoal):
 1. lift_fun q |\<in>| map_both Some |`| fId_on (\<Q> (fst \<G>) |\<union>| \<Q> (snd \<G>))
[PROOF STEP]
by (auto simp: fimage_iff fBex_def)
[PROOF STATE]
proof (state)
this:
lift_fun q |\<in>| map_both Some |`| fId_on (\<Q> (fst \<G>) |\<union>| \<Q> (snd \<G>))

goal (1 subgoal):
 1. RR2_spec (GTT_to_RR2_root_reg \<G>) (agtt_lang \<G>)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
lift_fun q |\<in>| map_both Some |`| fId_on (\<Q> (fst \<G>) |\<union>| \<Q> (snd \<G>))
[PROOF STEP]
have "gpair t u \<in> \<L> (GTT_to_RR2_root_reg \<G>)"
[PROOF STATE]
proof (prove)
using this:
lift_fun q |\<in>| map_both Some |`| fId_on (\<Q> (fst \<G>) |\<union>| \<Q> (snd \<G>))

goal (1 subgoal):
 1. gpair t u \<in> \<L> (GTT_to_RR2_root_reg \<G>)
[PROOF STEP]
using q
[PROOF STATE]
proof (prove)
using this:
lift_fun q |\<in>| map_both Some |`| fId_on (\<Q> (fst \<G>) |\<union>| \<Q> (snd \<G>))
q |\<in>| ta_der (fst \<G>) (term_of_gterm t)
q |\<in>| ta_der (snd \<G>) (term_of_gterm u)

goal (1 subgoal):
 1. gpair t u \<in> \<L> (GTT_to_RR2_root_reg \<G>)
[PROOF STEP]
using fsubsetD[OF ta_der_mono to_ta_der_pair_automaton(3)[OF q], of "GTT_to_RR2_root \<G>"]
[PROOF STATE]
proof (prove)
using this:
lift_fun q |\<in>| map_both Some |`| fId_on (\<Q> (fst \<G>) |\<union>| \<Q> (snd \<G>))
q |\<in>| ta_der (fst \<G>) (term_of_gterm t)
q |\<in>| ta_der (snd \<G>) (term_of_gterm u)
\<lbrakk>rules (pair_automaton (fst \<G>) (snd \<G>)) |\<subseteq>| rules (GTT_to_RR2_root \<G>); eps (pair_automaton (fst \<G>) (snd \<G>)) |\<subseteq>| eps (GTT_to_RR2_root \<G>)\<rbrakk> \<Longrightarrow> lift_fun q |\<in>| ta_der (GTT_to_RR2_root \<G>) (term_of_gterm (gpair t u))

goal (1 subgoal):
 1. gpair t u \<in> \<L> (GTT_to_RR2_root_reg \<G>)
[PROOF STEP]
by (auto simp: \<L>_def GTT_to_RR2_root_def gta_lang_def image_def gtt_states_def
        gta_der_def GTT_to_RR2_root_reg_def)
[PROOF STATE]
proof (state)
this:
gpair t u \<in> \<L> (GTT_to_RR2_root_reg \<G>)

goal (1 subgoal):
 1. RR2_spec (GTT_to_RR2_root_reg \<G>) (agtt_lang \<G>)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>?q2 |\<in>| ta_der (fst \<G>) (term_of_gterm ?t2); ?q2 |\<in>| ta_der (snd \<G>) (term_of_gterm ?u2)\<rbrakk> \<Longrightarrow> gpair ?t2 ?u2 \<in> \<L> (GTT_to_RR2_root_reg \<G>)

goal (1 subgoal):
 1. RR2_spec (GTT_to_RR2_root_reg \<G>) (agtt_lang \<G>)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
?s2 \<in> \<L> (GTT_to_RR2_root_reg \<G>) \<Longrightarrow> \<exists>t u q. ?s2 = gpair t u \<and> q |\<in>| ta_der (fst \<G>) (term_of_gterm t) \<and> q |\<in>| ta_der (snd \<G>) (term_of_gterm u)
\<lbrakk>?q2 |\<in>| ta_der (fst \<G>) (term_of_gterm ?t2); ?q2 |\<in>| ta_der (snd \<G>) (term_of_gterm ?u2)\<rbrakk> \<Longrightarrow> gpair ?t2 ?u2 \<in> \<L> (GTT_to_RR2_root_reg \<G>)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
?s2 \<in> \<L> (GTT_to_RR2_root_reg \<G>) \<Longrightarrow> \<exists>t u q. ?s2 = gpair t u \<and> q |\<in>| ta_der (fst \<G>) (term_of_gterm t) \<and> q |\<in>| ta_der (snd \<G>) (term_of_gterm u)
\<lbrakk>?q2 |\<in>| ta_der (fst \<G>) (term_of_gterm ?t2); ?q2 |\<in>| ta_der (snd \<G>) (term_of_gterm ?u2)\<rbrakk> \<Longrightarrow> gpair ?t2 ?u2 \<in> \<L> (GTT_to_RR2_root_reg \<G>)

goal (1 subgoal):
 1. RR2_spec (GTT_to_RR2_root_reg \<G>) (agtt_lang \<G>)
[PROOF STEP]
by (auto simp: RR2_spec_def agtt_lang_def \<L>_def gta_der_def)
[PROOF STATE]
proof (state)
this:
RR2_spec (GTT_to_RR2_root_reg \<G>) (agtt_lang \<G>)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma swap_GTT_to_RR2_root:
  "gpair s t \<in> \<L> (GTT_to_RR2_root_reg (prod.swap \<G>)) \<longleftrightarrow>
   gpair t s \<in> \<L> (GTT_to_RR2_root_reg \<G>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (gpair s t \<in> \<L> (GTT_to_RR2_root_reg (prod.swap \<G>))) = (gpair t s \<in> \<L> (GTT_to_RR2_root_reg \<G>))
[PROOF STEP]
by (auto simp: GTT_to_RR2_root[unfolded RR2_spec_def] agtt_lang_def)


[STATEMENT]
lemma funas_mctxt_map_vars_mctxt [simp]:
  "funas_mctxt (map_vars_mctxt f C) = funas_mctxt C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. funas_mctxt (map_vars_mctxt f C) = funas_mctxt C
[PROOF STEP]
by (induct C) auto


[STATEMENT]
lemma agtt_lang_syms:
  "gtt_syms \<G> |\<subseteq>| \<F> \<Longrightarrow> agtt_lang \<G> \<subseteq> {t. funas_gterm t \<subseteq> fset \<F>} \<times> {t. funas_gterm t \<subseteq> fset \<F>}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gtt_syms \<G> |\<subseteq>| \<F> \<Longrightarrow> agtt_lang \<G> \<subseteq> gterms (fset \<F>) \<times> gterms (fset \<F>)
[PROOF STEP]
by (auto simp: agtt_lang_def gta_der_def funas_term_of_gterm_conv)
     (metis ffunas_gterm.rep_eq fin_mono notin_fset ta_der_gterm_sig)+


[STATEMENT]
lemma gtt_lang_from_agtt_lang:
  "gtt_lang \<G> = lift_root_step UNIV PAny EParallel (agtt_lang \<G>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gtt_lang \<G> = lift_root_step UNIV PAny EParallel (agtt_lang \<G>)
[PROOF STEP]
unfolding lift_root_step.simps agtt_lang_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gmctxt_cl UNIV {uu_. \<exists>t u q. uu_ = (t, u) \<and> q |\<in>| gta_der (fst \<G>) t \<and> q |\<in>| gta_der (snd \<G>) u} = gmctxtcl_funas UNIV {uu_. \<exists>t u q. uu_ = (t, u) \<and> q |\<in>| gta_der (fst \<G>) t \<and> q |\<in>| gta_der (snd \<G>) u}
[PROOF STEP]
by (auto simp: lift_root_step.simps agtt_lang_def gmctxt_cl_gmctxtex_onp_conv)