[STATEMENT]
lemma \<R>\<^sub>3_sym: "sym (\<R>\<^sub>3 \<Gamma> \<S> P)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sym (\<R>\<^sub>3 \<Gamma> \<S> P)
[PROOF STEP]
unfolding sym_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x y. (x, y) \<in> \<R>\<^sub>3 \<Gamma> \<S> P \<longrightarrow> (y, x) \<in> \<R>\<^sub>3 \<Gamma> \<S> P
[PROOF STEP]
proof (clarify)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a b ba aa bb bc. \<langle>a, b, ba\<rangle> \<R>\<^sup>3\<^bsub>\<Gamma>,\<S>,P\<^esub> \<langle>aa, bb, bc\<rangle> \<Longrightarrow> \<langle>aa, bb, bc\<rangle> \<R>\<^sup>3\<^bsub>\<Gamma>,\<S>,P\<^esub> \<langle>a, b, ba\<rangle>
[PROOF STEP]
fix c\<^sub>1 mds mem\<^sub>1 c\<^sub>2 mds' mem\<^sub>2
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a b ba aa bb bc. \<langle>a, b, ba\<rangle> \<R>\<^sup>3\<^bsub>\<Gamma>,\<S>,P\<^esub> \<langle>aa, bb, bc\<rangle> \<Longrightarrow> \<langle>aa, bb, bc\<rangle> \<R>\<^sup>3\<^bsub>\<Gamma>,\<S>,P\<^esub> \<langle>a, b, ba\<rangle>
[PROOF STEP]
assume asm: "\<langle>c\<^sub>1, mds, mem\<^sub>1\<rangle> \<R>\<^sup>3\<^bsub>\<Gamma>,\<S>,P\<^esub> \<langle>c\<^sub>2, mds', mem\<^sub>2\<rangle>"
[PROOF STATE]
proof (state)
this:
\<langle>c\<^sub>1, mds, mem\<^sub>1\<rangle> \<R>\<^sup>3\<^bsub>\<Gamma>,\<S>,P\<^esub> \<langle>c\<^sub>2, mds', mem\<^sub>2\<rangle>

goal (1 subgoal):
 1. \<And>a b ba aa bb bc. \<langle>a, b, ba\<rangle> \<R>\<^sup>3\<^bsub>\<Gamma>,\<S>,P\<^esub> \<langle>aa, bb, bc\<rangle> \<Longrightarrow> \<langle>aa, bb, bc\<rangle> \<R>\<^sup>3\<^bsub>\<Gamma>,\<S>,P\<^esub> \<langle>a, b, ba\<rangle>
[PROOF STEP]
hence [simp]: "mds' = mds"
[PROOF STATE]
proof (prove)
using this:
\<langle>c\<^sub>1, mds, mem\<^sub>1\<rangle> \<R>\<^sup>3\<^bsub>\<Gamma>,\<S>,P\<^esub> \<langle>c\<^sub>2, mds', mem\<^sub>2\<rangle>

goal (1 subgoal):
 1. mds' = mds
[PROOF STEP]
using \<R>\<^sub>3_elim'
[PROOF STATE]
proof (prove)
using this:
\<langle>c\<^sub>1, mds, mem\<^sub>1\<rangle> \<R>\<^sup>3\<^bsub>\<Gamma>,\<S>,P\<^esub> \<langle>c\<^sub>2, mds', mem\<^sub>2\<rangle>
\<lbrakk>\<langle>?c\<^sub>1, ?mds, ?mem\<^sub>1\<rangle> \<R>\<^sup>3\<^bsub>?\<Gamma>,?\<S>,?P\<^esub> \<langle>?c\<^sub>2, ?mds\<^sub>2, ?mem\<^sub>2\<rangle>; \<And>c\<^sub>1 \<Gamma> \<S> P c\<^sub>2 c. \<lbrakk>?c\<^sub>1 = c\<^sub>1 ;; c; \<langle>c\<^sub>1, ?mds, ?mem\<^sub>1\<rangle> \<R>\<^sup>1\<^bsub>\<Gamma>,\<S>,P\<^esub> \<langle>c\<^sub>2, ?mds, ?mem\<^sub>2\<rangle>; \<turnstile> \<Gamma>,\<S>,P {c} ?\<Gamma>,?\<S>,?P; ?c\<^sub>2 = c\<^sub>2 ;; c; ?mds\<^sub>2 = ?mds\<rbrakk> \<Longrightarrow> ?Pa; \<And>c\<^sub>1 \<Gamma> \<S> P c\<^sub>2 c. \<lbrakk>?c\<^sub>1 = c\<^sub>1 ;; c; \<langle>c\<^sub>1, ?mds, ?mem\<^sub>1\<rangle> \<R>\<^sup>3\<^bsub>\<Gamma>,\<S>,P\<^esub> \<langle>c\<^sub>2, ?mds, ?mem\<^sub>2\<rangle>; \<turnstile> \<Gamma>,\<S>,P {c} ?\<Gamma>,?\<S>,?P; ?c\<^sub>2 = c\<^sub>2 ;; c; ?mds\<^sub>2 = ?mds\<rbrakk> \<Longrightarrow> ?Pa\<rbrakk> \<Longrightarrow> ?Pa

goal (1 subgoal):
 1. mds' = mds
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
mds' = mds

goal (1 subgoal):
 1. \<And>a b ba aa bb bc. \<langle>a, b, ba\<rangle> \<R>\<^sup>3\<^bsub>\<Gamma>,\<S>,P\<^esub> \<langle>aa, bb, bc\<rangle> \<Longrightarrow> \<langle>aa, bb, bc\<rangle> \<R>\<^sup>3\<^bsub>\<Gamma>,\<S>,P\<^esub> \<langle>a, b, ba\<rangle>
[PROOF STEP]
from asm
[PROOF STATE]
proof (chain)
picking this:
\<langle>c\<^sub>1, mds, mem\<^sub>1\<rangle> \<R>\<^sup>3\<^bsub>\<Gamma>,\<S>,P\<^esub> \<langle>c\<^sub>2, mds', mem\<^sub>2\<rangle>
[PROOF STEP]
show "\<langle>c\<^sub>2, mds', mem\<^sub>2\<rangle> \<R>\<^sup>3\<^bsub>\<Gamma>,\<S>,P\<^esub> \<langle>c\<^sub>1, mds, mem\<^sub>1\<rangle>"
[PROOF STATE]
proof (prove)
using this:
\<langle>c\<^sub>1, mds, mem\<^sub>1\<rangle> \<R>\<^sup>3\<^bsub>\<Gamma>,\<S>,P\<^esub> \<langle>c\<^sub>2, mds', mem\<^sub>2\<rangle>

goal (1 subgoal):
 1. \<langle>c\<^sub>2, mds', mem\<^sub>2\<rangle> \<R>\<^sup>3\<^bsub>\<Gamma>,\<S>,P\<^esub> \<langle>c\<^sub>1, mds, mem\<^sub>1\<rangle>
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<langle>c\<^sub>1, mds, mem\<^sub>1\<rangle> \<R>\<^sup>3\<^bsub>\<Gamma>,\<S>,P\<^esub> \<langle>c\<^sub>2, mds, mem\<^sub>2\<rangle> \<Longrightarrow> \<langle>c\<^sub>2, mds, mem\<^sub>2\<rangle> \<R>\<^sup>3\<^bsub>\<Gamma>,\<S>,P\<^esub> \<langle>c\<^sub>1, mds, mem\<^sub>1\<rangle>
[PROOF STEP]
apply (induct rule: \<R>\<^sub>3_aux.induct)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>c\<^sub>1 mds mem\<^sub>1 \<Gamma> \<S> P c\<^sub>2 mem\<^sub>2 c \<Gamma>' \<S>' P'. \<lbrakk>\<langle>c\<^sub>1, mds, mem\<^sub>1\<rangle> \<R>\<^sup>1\<^bsub>\<Gamma>,\<S>,P\<^esub> \<langle>c\<^sub>2, mds, mem\<^sub>2\<rangle>; \<turnstile> \<Gamma>,\<S>,P {c} \<Gamma>',\<S>',P'\<rbrakk> \<Longrightarrow> \<langle>c\<^sub>2 ;; c, mds, mem\<^sub>2\<rangle> \<R>\<^sup>3\<^bsub>\<Gamma>',\<S>',P'\<^esub> \<langle>c\<^sub>1 ;; c, mds, mem\<^sub>1\<rangle>
 2. \<And>c\<^sub>1 mds mem\<^sub>1 \<Gamma> \<S> P c\<^sub>2 mem\<^sub>2 c \<Gamma>' \<S>' P'. \<lbrakk>\<langle>c\<^sub>1, mds, mem\<^sub>1\<rangle> \<R>\<^sup>3\<^bsub>\<Gamma>,\<S>,P\<^esub> \<langle>c\<^sub>2, mds, mem\<^sub>2\<rangle>; \<langle>c\<^sub>2, mds, mem\<^sub>2\<rangle> \<R>\<^sup>3\<^bsub>\<Gamma>,\<S>,P\<^esub> \<langle>c\<^sub>1, mds, mem\<^sub>1\<rangle>; \<turnstile> \<Gamma>,\<S>,P {c} \<Gamma>',\<S>',P'\<rbrakk> \<Longrightarrow> \<langle>c\<^sub>2 ;; c, mds, mem\<^sub>2\<rangle> \<R>\<^sup>3\<^bsub>\<Gamma>',\<S>',P'\<^esub> \<langle>c\<^sub>1 ;; c, mds, mem\<^sub>1\<rangle>
[PROOF STEP]
apply (metis (lifting) \<R>\<^sub>1_sym \<R>\<^sub>3_aux.intro\<^sub>1 symD)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>c\<^sub>1 mds mem\<^sub>1 \<Gamma> \<S> P c\<^sub>2 mem\<^sub>2 c \<Gamma>' \<S>' P'. \<lbrakk>\<langle>c\<^sub>1, mds, mem\<^sub>1\<rangle> \<R>\<^sup>3\<^bsub>\<Gamma>,\<S>,P\<^esub> \<langle>c\<^sub>2, mds, mem\<^sub>2\<rangle>; \<langle>c\<^sub>2, mds, mem\<^sub>2\<rangle> \<R>\<^sup>3\<^bsub>\<Gamma>,\<S>,P\<^esub> \<langle>c\<^sub>1, mds, mem\<^sub>1\<rangle>; \<turnstile> \<Gamma>,\<S>,P {c} \<Gamma>',\<S>',P'\<rbrakk> \<Longrightarrow> \<langle>c\<^sub>2 ;; c, mds, mem\<^sub>2\<rangle> \<R>\<^sup>3\<^bsub>\<Gamma>',\<S>',P'\<^esub> \<langle>c\<^sub>1 ;; c, mds, mem\<^sub>1\<rangle>
[PROOF STEP]
by (metis (lifting) \<R>\<^sub>3_aux.intro\<^sub>3)
[PROOF STATE]
proof (state)
this:
\<langle>c\<^sub>2, mds', mem\<^sub>2\<rangle> \<R>\<^sup>3\<^bsub>\<Gamma>,\<S>,P\<^esub> \<langle>c\<^sub>1, mds, mem\<^sub>1\<rangle>

goal:
No subgoals!
[PROOF STEP]
qed