[STATEMENT]
lemma inst_cswitch_consistency:
  assumes "rvpeq u s t"
  shows "rvpeq u (rcswitch n s) (rcswitch n t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rvpeq u (rcswitch n s) (rcswitch n t)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. rvpeq u (rcswitch n s) (rcswitch n t)
[PROOF STEP]
have 1: "vpeq (partition u) (\<down>s) \<down>(rcswitch n s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vpeq (Step.partition u) \<down> s \<down> rcswitch n s
[PROOF STEP]
using rstate_invariant cswitch_consistency_and_respect cswitch_preserves_invariants
[PROOF STATE]
proof (prove)
using this:
atomic_step_invariant \<down> ?s
atomic_step_invariant ?s \<Longrightarrow> vpeq ?u ?s (?s\<lparr>current := ?new_current\<rparr>)
atomic_step_invariant ?s \<Longrightarrow> atomic_step_invariant (?s\<lparr>current := ?new_current\<rparr>)

goal (1 subgoal):
 1. vpeq (Step.partition u) \<down> s \<down> rcswitch n s
[PROOF STEP]
unfolding rcswitch_def
[PROOF STATE]
proof (prove)
using this:
atomic_step_invariant \<down> ?s
atomic_step_invariant ?s \<Longrightarrow> vpeq ?u ?s (?s\<lparr>current := ?new_current\<rparr>)
atomic_step_invariant ?s \<Longrightarrow> atomic_step_invariant (?s\<lparr>current := ?new_current\<rparr>)

goal (1 subgoal):
 1. vpeq (Step.partition u) \<down> s \<down> \<up> \<down> s\<lparr>current := Eps rinvariant\<rparr>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
vpeq (Step.partition u) \<down> s \<down> rcswitch n s

goal (1 subgoal):
 1. rvpeq u (rcswitch n s) (rcswitch n t)
[PROOF STEP]
have 2: "vpeq (partition u) (\<down>t) \<down>(rcswitch n t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vpeq (Step.partition u) \<down> t \<down> rcswitch n t
[PROOF STEP]
using rstate_invariant cswitch_consistency_and_respect cswitch_preserves_invariants
[PROOF STATE]
proof (prove)
using this:
atomic_step_invariant \<down> ?s
atomic_step_invariant ?s \<Longrightarrow> vpeq ?u ?s (?s\<lparr>current := ?new_current\<rparr>)
atomic_step_invariant ?s \<Longrightarrow> atomic_step_invariant (?s\<lparr>current := ?new_current\<rparr>)

goal (1 subgoal):
 1. vpeq (Step.partition u) \<down> t \<down> rcswitch n t
[PROOF STEP]
unfolding rcswitch_def
[PROOF STATE]
proof (prove)
using this:
atomic_step_invariant \<down> ?s
atomic_step_invariant ?s \<Longrightarrow> vpeq ?u ?s (?s\<lparr>current := ?new_current\<rparr>)
atomic_step_invariant ?s \<Longrightarrow> atomic_step_invariant (?s\<lparr>current := ?new_current\<rparr>)

goal (1 subgoal):
 1. vpeq (Step.partition u) \<down> t \<down> \<up> \<down> t\<lparr>current := Eps rinvariant\<rparr>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
vpeq (Step.partition u) \<down> t \<down> rcswitch n t

goal (1 subgoal):
 1. rvpeq u (rcswitch n s) (rcswitch n t)
[PROOF STEP]
from 1 2 assms
[PROOF STATE]
proof (chain)
picking this:
vpeq (Step.partition u) \<down> s \<down> rcswitch n s
vpeq (Step.partition u) \<down> t \<down> rcswitch n t
rvpeq u s t
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
vpeq (Step.partition u) \<down> s \<down> rcswitch n s
vpeq (Step.partition u) \<down> t \<down> rcswitch n t
rvpeq u s t

goal (1 subgoal):
 1. rvpeq u (rcswitch n s) (rcswitch n t)
[PROOF STEP]
unfolding rvpeq_def
[PROOF STATE]
proof (prove)
using this:
vpeq (Step.partition u) \<down> s \<down> rcswitch n s
vpeq (Step.partition u) \<down> t \<down> rcswitch n t
vpeq (Step.partition u) \<down> s \<down> t

goal (1 subgoal):
 1. vpeq (Step.partition u) \<down> rcswitch n s \<down> rcswitch n t
[PROOF STEP]
using vpeq_rel
[PROOF STATE]
proof (prove)
using this:
vpeq (Step.partition u) \<down> s \<down> rcswitch n s
vpeq (Step.partition u) \<down> t \<down> rcswitch n t
vpeq (Step.partition u) \<down> s \<down> t
vpeq ?u ?s ?s
vpeq ?u ?s ?t \<Longrightarrow> vpeq ?u ?t ?s
\<lbrakk>vpeq ?u ?s1.0 ?s2.0; vpeq ?u ?s2.0 ?s3.0\<rbrakk> \<Longrightarrow> vpeq ?u ?s1.0 ?s3.0

goal (1 subgoal):
 1. vpeq (Step.partition u) \<down> rcswitch n s \<down> rcswitch n t
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
rvpeq u (rcswitch n s) (rcswitch n t)

goal:
No subgoals!
[PROOF STEP]
qed