[STATEMENT]
lemma spr_ii_sim: "sim SPR.MC spr_ii_simMC spr_ii_sim"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sim SPR.MC spr_ii_simMC spr_ii_sim
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sim SPR.MC spr_ii_simMC spr_ii_sim
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. sim_range SPR.MC spr_ii_simMC spr_ii_sim
 2. sim_val SPR.MC spr_ii_simMC spr_ii_sim
 3. sim_f SPR.MC spr_ii_simMC spr_ii_sim
 4. sim_r SPR.MC spr_ii_simMC spr_ii_sim
[PROOF STEP]
show "sim_range SPR.MC spr_ii_simMC spr_ii_sim"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sim_range SPR.MC spr_ii_simMC spr_ii_sim
[PROOF STEP]
by (rule sim_rangeI) (simp_all add: spr_ii_sim_def)
[PROOF STATE]
proof (state)
this:
sim_range SPR.MC spr_ii_simMC spr_ii_sim

goal (3 subgoals):
 1. sim_val SPR.MC spr_ii_simMC spr_ii_sim
 2. sim_f SPR.MC spr_ii_simMC spr_ii_sim
 3. sim_r SPR.MC spr_ii_simMC spr_ii_sim
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. sim_val SPR.MC spr_ii_simMC spr_ii_sim
 2. sim_f SPR.MC spr_ii_simMC spr_ii_sim
 3. sim_r SPR.MC spr_ii_simMC spr_ii_sim
[PROOF STEP]
show "sim_val SPR.MC spr_ii_simMC spr_ii_sim"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sim_val SPR.MC spr_ii_simMC spr_ii_sim
[PROOF STEP]
by (rule sim_valI) simp
[PROOF STATE]
proof (state)
this:
sim_val SPR.MC spr_ii_simMC spr_ii_sim

goal (2 subgoals):
 1. sim_f SPR.MC spr_ii_simMC spr_ii_sim
 2. sim_r SPR.MC spr_ii_simMC spr_ii_sim
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. sim_f SPR.MC spr_ii_simMC spr_ii_sim
 2. sim_r SPR.MC spr_ii_simMC spr_ii_sim
[PROOF STEP]
show "sim_f SPR.MC spr_ii_simMC spr_ii_sim"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sim_f SPR.MC spr_ii_simMC spr_ii_sim
[PROOF STEP]
unfolding spr_ii_simRels_def spr_ii_sim_def mkKripke_def SPR.mkM_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sim_f \<lparr>worlds = SPR.jkbpC, relations = \<lambda>a. {(t, t'). {t, t'} \<subseteq> SPR.jkbpC \<and> spr_jview a t = spr_jview a t'}, valuation = envVal \<circ> tLast\<rparr> \<lparr>worlds = (\<lambda>t. (tObsC_ii_abs t, tLast t)) ` SPR.jkbpC, relations = \<lambda>a. Restr {(s, s') |s s'. envObs a (snd s) = envObs a (snd s') \<and> fst s = fst s'} ((\<lambda>t. (tObsC_ii_abs t, tLast t)) ` SPR.jkbpC), valuation = spr_ii_simVal\<rparr> (\<lambda>t. (tObsC_ii_abs t, tLast t))
[PROOF STEP]
by (rule sim_fI, auto simp del: split_paired_Ex)
[PROOF STATE]
proof (state)
this:
sim_f SPR.MC spr_ii_simMC spr_ii_sim

goal (1 subgoal):
 1. sim_r SPR.MC spr_ii_simMC spr_ii_sim
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. sim_r SPR.MC spr_ii_simMC spr_ii_sim
[PROOF STEP]
show "sim_r SPR.MC spr_ii_simMC spr_ii_sim"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sim_r SPR.MC spr_ii_simMC spr_ii_sim
[PROOF STEP]
by (rule spr_ii_sim_r)
[PROOF STATE]
proof (state)
this:
sim_r SPR.MC spr_ii_simMC spr_ii_sim

goal:
No subgoals!
[PROOF STEP]
qed