[STATEMENT]
lemma run_abstraction_correct:
  "run (delta \<Sigma>) (initial \<phi>) w = abstract_state o (run (delta\<^sub>C \<Sigma>) (initial\<^sub>C \<phi>) w)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. run (delta \<Sigma>) (initial \<phi>) w = abstract_state \<circ> run (delta\<^sub>C \<Sigma>) (initial\<^sub>C \<phi>) w
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. run (delta \<Sigma>) (initial \<phi>) w = abstract_state \<circ> run (delta\<^sub>C \<Sigma>) (initial\<^sub>C \<phi>) w
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. run (delta \<Sigma>) (initial \<phi>) w = abstract_state \<circ> run (delta\<^sub>C \<Sigma>) (initial\<^sub>C \<phi>) w
[PROOF STEP]
fix i
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. run (delta \<Sigma>) (initial \<phi>) w = abstract_state \<circ> run (delta\<^sub>C \<Sigma>) (initial\<^sub>C \<phi>) w
[PROOF STEP]
let ?\<delta>\<^sub>2 = "\<Delta>\<^sub>\<times> (\<lambda>\<chi>. semi_mojmir_def.step \<Sigma> \<delta>\<^sub>M (q\<^sub>0\<^sub>M (theG \<chi>)))"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. run (delta \<Sigma>) (initial \<phi>) w = abstract_state \<circ> run (delta\<^sub>C \<Sigma>) (initial\<^sub>C \<phi>) w
[PROOF STEP]
let ?q\<^sub>2 = "\<iota>\<^sub>\<times> (\<^bold>G \<phi>) (\<lambda>\<chi>. semi_mojmir_def.initial (q\<^sub>0\<^sub>M (theG \<chi>)))"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. run (delta \<Sigma>) (initial \<phi>) w = abstract_state \<circ> run (delta\<^sub>C \<Sigma>) (initial\<^sub>C \<phi>) w
[PROOF STEP]
let ?\<delta>\<^sub>2' = "\<up>\<Delta>\<^sub>\<times> (nxt \<Sigma> \<delta>\<^sub>M o q\<^sub>0\<^sub>M o theG)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. run (delta \<Sigma>) (initial \<phi>) w = abstract_state \<circ> run (delta\<^sub>C \<Sigma>) (initial\<^sub>C \<phi>) w
[PROOF STEP]
let ?q\<^sub>2' = "Mapping.tabulate (G_list \<phi>) (init o q\<^sub>0\<^sub>M o theG)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. run (delta \<Sigma>) (initial \<phi>) w = abstract_state \<circ> run (delta\<^sub>C \<Sigma>) (initial\<^sub>C \<phi>) w
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. run (delta \<Sigma>) (initial \<phi>) w = abstract_state \<circ> run (delta\<^sub>C \<Sigma>) (initial\<^sub>C \<phi>) w
[PROOF STEP]
fix q
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. run (delta \<Sigma>) (initial \<phi>) w = abstract_state \<circ> run (delta\<^sub>C \<Sigma>) (initial\<^sub>C \<phi>) w
[PROOF STEP]
assume "q \<notin> \<^bold>G \<phi>"
[PROOF STATE]
proof (state)
this:
q \<notin> \<^bold>G \<phi>

goal (1 subgoal):
 1. run (delta \<Sigma>) (initial \<phi>) w = abstract_state \<circ> run (delta\<^sub>C \<Sigma>) (initial\<^sub>C \<phi>) w
[PROOF STEP]
hence "?q\<^sub>2 q = None" and "Mapping.lookup (run ?\<delta>\<^sub>2' ?q\<^sub>2' w i) q = None"
[PROOF STATE]
proof (prove)
using this:
q \<notin> \<^bold>G \<phi>

goal (1 subgoal):
 1. \<iota>\<^sub>\<times> (\<^bold>G \<phi>) (\<lambda>\<chi>. semi_mojmir_def.initial (q\<^sub>0\<^sub>M (theG \<chi>))) q = None &&& Mapping.lookup (run (\<up>\<Delta>\<^sub>\<times> (nxt \<Sigma> \<delta>\<^sub>M \<circ> q\<^sub>0\<^sub>M \<circ> theG)) (Mapping.tabulate (G_list \<phi>) (init \<circ> q\<^sub>0\<^sub>M \<circ> theG)) w i) q = None
[PROOF STEP]
using G_eq_G_list product_abs_run_None
[PROOF STATE]
proof (prove)
using this:
q \<notin> \<^bold>G \<phi>
\<^bold>G ?\<phi> = set (G_list ?\<phi>)
Mapping.lookup ?\<iota>\<^sub>m ?k = None \<Longrightarrow> Mapping.lookup (run (\<up>\<Delta>\<^sub>\<times> ?\<delta>\<^sub>m) ?\<iota>\<^sub>m ?w ?i) ?k = None

goal (1 subgoal):
 1. \<iota>\<^sub>\<times> (\<^bold>G \<phi>) (\<lambda>\<chi>. semi_mojmir_def.initial (q\<^sub>0\<^sub>M (theG \<chi>))) q = None &&& Mapping.lookup (run (\<up>\<Delta>\<^sub>\<times> (nxt \<Sigma> \<delta>\<^sub>M \<circ> q\<^sub>0\<^sub>M \<circ> theG)) (Mapping.tabulate (G_list \<phi>) (init \<circ> q\<^sub>0\<^sub>M \<circ> theG)) w i) q = None
[PROOF STEP]
by (simp, metis domIff keys_dom_lookup keys_tabulate)
[PROOF STATE]
proof (state)
this:
\<iota>\<^sub>\<times> (\<^bold>G \<phi>) (\<lambda>\<chi>. semi_mojmir_def.initial (q\<^sub>0\<^sub>M (theG \<chi>))) q = None
Mapping.lookup (run (\<up>\<Delta>\<^sub>\<times> (nxt \<Sigma> \<delta>\<^sub>M \<circ> q\<^sub>0\<^sub>M \<circ> theG)) (Mapping.tabulate (G_list \<phi>) (init \<circ> q\<^sub>0\<^sub>M \<circ> theG)) w i) q = None

goal (1 subgoal):
 1. run (delta \<Sigma>) (initial \<phi>) w = abstract_state \<circ> run (delta\<^sub>C \<Sigma>) (initial\<^sub>C \<phi>) w
[PROOF STEP]
hence "run ?\<delta>\<^sub>2 ?q\<^sub>2 w i q = (\<lambda>m. (map_option rk) o (Mapping.lookup m)) (run ?\<delta>\<^sub>2' ?q\<^sub>2' w i) q"
[PROOF STATE]
proof (prove)
using this:
\<iota>\<^sub>\<times> (\<^bold>G \<phi>) (\<lambda>\<chi>. semi_mojmir_def.initial (q\<^sub>0\<^sub>M (theG \<chi>))) q = None
Mapping.lookup (run (\<up>\<Delta>\<^sub>\<times> (nxt \<Sigma> \<delta>\<^sub>M \<circ> q\<^sub>0\<^sub>M \<circ> theG)) (Mapping.tabulate (G_list \<phi>) (init \<circ> q\<^sub>0\<^sub>M \<circ> theG)) w i) q = None

goal (1 subgoal):
 1. run (\<Delta>\<^sub>\<times> (\<lambda>\<chi>. semi_mojmir_def.step \<Sigma> \<delta>\<^sub>M (q\<^sub>0\<^sub>M (theG \<chi>)))) (\<iota>\<^sub>\<times> (\<^bold>G \<phi>) (\<lambda>\<chi>. semi_mojmir_def.initial (q\<^sub>0\<^sub>M (theG \<chi>)))) w i q = (map_option rk \<circ> Mapping.lookup (run (\<up>\<Delta>\<^sub>\<times> (nxt \<Sigma> \<delta>\<^sub>M \<circ> q\<^sub>0\<^sub>M \<circ> theG)) (Mapping.tabulate (G_list \<phi>) (init \<circ> q\<^sub>0\<^sub>M \<circ> theG)) w i)) q
[PROOF STEP]
using product_run_None
[PROOF STATE]
proof (prove)
using this:
\<iota>\<^sub>\<times> (\<^bold>G \<phi>) (\<lambda>\<chi>. semi_mojmir_def.initial (q\<^sub>0\<^sub>M (theG \<chi>))) q = None
Mapping.lookup (run (\<up>\<Delta>\<^sub>\<times> (nxt \<Sigma> \<delta>\<^sub>M \<circ> q\<^sub>0\<^sub>M \<circ> theG)) (Mapping.tabulate (G_list \<phi>) (init \<circ> q\<^sub>0\<^sub>M \<circ> theG)) w i) q = None
?\<iota>\<^sub>m ?k = None \<Longrightarrow> run (\<Delta>\<^sub>\<times> ?\<delta>\<^sub>m) ?\<iota>\<^sub>m ?w ?i ?k = None

goal (1 subgoal):
 1. run (\<Delta>\<^sub>\<times> (\<lambda>\<chi>. semi_mojmir_def.step \<Sigma> \<delta>\<^sub>M (q\<^sub>0\<^sub>M (theG \<chi>)))) (\<iota>\<^sub>\<times> (\<^bold>G \<phi>) (\<lambda>\<chi>. semi_mojmir_def.initial (q\<^sub>0\<^sub>M (theG \<chi>)))) w i q = (map_option rk \<circ> Mapping.lookup (run (\<up>\<Delta>\<^sub>\<times> (nxt \<Sigma> \<delta>\<^sub>M \<circ> q\<^sub>0\<^sub>M \<circ> theG)) (Mapping.tabulate (G_list \<phi>) (init \<circ> q\<^sub>0\<^sub>M \<circ> theG)) w i)) q
[PROOF STEP]
by (simp del: nxt.simps rk.simps)
[PROOF STATE]
proof (state)
this:
run (\<Delta>\<^sub>\<times> (\<lambda>\<chi>. semi_mojmir_def.step \<Sigma> \<delta>\<^sub>M (q\<^sub>0\<^sub>M (theG \<chi>)))) (\<iota>\<^sub>\<times> (\<^bold>G \<phi>) (\<lambda>\<chi>. semi_mojmir_def.initial (q\<^sub>0\<^sub>M (theG \<chi>)))) w i q = (map_option rk \<circ> Mapping.lookup (run (\<up>\<Delta>\<^sub>\<times> (nxt \<Sigma> \<delta>\<^sub>M \<circ> q\<^sub>0\<^sub>M \<circ> theG)) (Mapping.tabulate (G_list \<phi>) (init \<circ> q\<^sub>0\<^sub>M \<circ> theG)) w i)) q

goal (1 subgoal):
 1. run (delta \<Sigma>) (initial \<phi>) w = abstract_state \<circ> run (delta\<^sub>C \<Sigma>) (initial\<^sub>C \<phi>) w
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?q19 \<notin> \<^bold>G \<phi> \<Longrightarrow> run (\<Delta>\<^sub>\<times> (\<lambda>\<chi>. semi_mojmir_def.step \<Sigma> \<delta>\<^sub>M (q\<^sub>0\<^sub>M (theG \<chi>)))) (\<iota>\<^sub>\<times> (\<^bold>G \<phi>) (\<lambda>\<chi>. semi_mojmir_def.initial (q\<^sub>0\<^sub>M (theG \<chi>)))) w i ?q19 = (map_option rk \<circ> Mapping.lookup (run (\<up>\<Delta>\<^sub>\<times> (nxt \<Sigma> \<delta>\<^sub>M \<circ> q\<^sub>0\<^sub>M \<circ> theG)) (Mapping.tabulate (G_list \<phi>) (init \<circ> q\<^sub>0\<^sub>M \<circ> theG)) w i)) ?q19

goal (1 subgoal):
 1. run (delta \<Sigma>) (initial \<phi>) w = abstract_state \<circ> run (delta\<^sub>C \<Sigma>) (initial\<^sub>C \<phi>) w
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
?q19 \<notin> \<^bold>G \<phi> \<Longrightarrow> run (\<Delta>\<^sub>\<times> (\<lambda>\<chi>. semi_mojmir_def.step \<Sigma> \<delta>\<^sub>M (q\<^sub>0\<^sub>M (theG \<chi>)))) (\<iota>\<^sub>\<times> (\<^bold>G \<phi>) (\<lambda>\<chi>. semi_mojmir_def.initial (q\<^sub>0\<^sub>M (theG \<chi>)))) w i ?q19 = (map_option rk \<circ> Mapping.lookup (run (\<up>\<Delta>\<^sub>\<times> (nxt \<Sigma> \<delta>\<^sub>M \<circ> q\<^sub>0\<^sub>M \<circ> theG)) (Mapping.tabulate (G_list \<phi>) (init \<circ> q\<^sub>0\<^sub>M \<circ> theG)) w i)) ?q19

goal (1 subgoal):
 1. run (delta \<Sigma>) (initial \<phi>) w = abstract_state \<circ> run (delta\<^sub>C \<Sigma>) (initial\<^sub>C \<phi>) w
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
?q19 \<notin> \<^bold>G \<phi> \<Longrightarrow> run (\<Delta>\<^sub>\<times> (\<lambda>\<chi>. semi_mojmir_def.step \<Sigma> \<delta>\<^sub>M (q\<^sub>0\<^sub>M (theG \<chi>)))) (\<iota>\<^sub>\<times> (\<^bold>G \<phi>) (\<lambda>\<chi>. semi_mojmir_def.initial (q\<^sub>0\<^sub>M (theG \<chi>)))) w i ?q19 = (map_option rk \<circ> Mapping.lookup (run (\<up>\<Delta>\<^sub>\<times> (nxt \<Sigma> \<delta>\<^sub>M \<circ> q\<^sub>0\<^sub>M \<circ> theG)) (Mapping.tabulate (G_list \<phi>) (init \<circ> q\<^sub>0\<^sub>M \<circ> theG)) w i)) ?q19

goal (1 subgoal):
 1. run (delta \<Sigma>) (initial \<phi>) w = abstract_state \<circ> run (delta\<^sub>C \<Sigma>) (initial\<^sub>C \<phi>) w
[PROOF STEP]
fix q j
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. run (delta \<Sigma>) (initial \<phi>) w = abstract_state \<circ> run (delta\<^sub>C \<Sigma>) (initial\<^sub>C \<phi>) w
[PROOF STEP]
assume "q \<in> \<^bold>G \<phi>"
[PROOF STATE]
proof (state)
this:
q \<in> \<^bold>G \<phi>

goal (1 subgoal):
 1. run (delta \<Sigma>) (initial \<phi>) w = abstract_state \<circ> run (delta\<^sub>C \<Sigma>) (initial\<^sub>C \<phi>) w
[PROOF STEP]
hence init: "?q\<^sub>2 q = Some (semi_mojmir_def.initial (q\<^sub>0\<^sub>M (theG q)))"
        and "Mapping.lookup (run ?\<delta>\<^sub>2' ?q\<^sub>2' w i) q = Some (run ((nxt \<Sigma> \<delta>\<^sub>M \<circ> q\<^sub>0\<^sub>M \<circ> theG) q) ((init \<circ> q\<^sub>0\<^sub>M \<circ> theG) q) w i)"
[PROOF STATE]
proof (prove)
using this:
q \<in> \<^bold>G \<phi>

goal (1 subgoal):
 1. \<iota>\<^sub>\<times> (\<^bold>G \<phi>) (\<lambda>\<chi>. semi_mojmir_def.initial (q\<^sub>0\<^sub>M (theG \<chi>))) q = Some (semi_mojmir_def.initial (q\<^sub>0\<^sub>M (theG q))) &&& Mapping.lookup (run (\<up>\<Delta>\<^sub>\<times> (nxt \<Sigma> \<delta>\<^sub>M \<circ> q\<^sub>0\<^sub>M \<circ> theG)) (Mapping.tabulate (G_list \<phi>) (init \<circ> q\<^sub>0\<^sub>M \<circ> theG)) w i) q = Some (run ((nxt \<Sigma> \<delta>\<^sub>M \<circ> q\<^sub>0\<^sub>M \<circ> theG) q) ((init \<circ> q\<^sub>0\<^sub>M \<circ> theG) q) w i)
[PROOF STEP]
apply (simp del: nxt.simps)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Mapping.lookup (run (\<up>\<Delta>\<^sub>\<times> (nxt \<Sigma> \<delta>\<^sub>M \<circ> q\<^sub>0\<^sub>M \<circ> theG)) (Mapping.tabulate (G_list \<phi>) (init \<circ> q\<^sub>0\<^sub>M \<circ> theG)) w i) q = Some (run ((nxt \<Sigma> \<delta>\<^sub>M \<circ> q\<^sub>0\<^sub>M \<circ> theG) q) ((init \<circ> q\<^sub>0\<^sub>M \<circ> theG) q) w i)
[PROOF STEP]
apply (metis G_eq_G_list \<open>q \<in> \<^bold>G \<phi>\<close> lookup_tabulate product_abs_run_Some)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
\<iota>\<^sub>\<times> (\<^bold>G \<phi>) (\<lambda>\<chi>. semi_mojmir_def.initial (q\<^sub>0\<^sub>M (theG \<chi>))) q = Some (semi_mojmir_def.initial (q\<^sub>0\<^sub>M (theG q)))
Mapping.lookup (run (\<up>\<Delta>\<^sub>\<times> (nxt \<Sigma> \<delta>\<^sub>M \<circ> q\<^sub>0\<^sub>M \<circ> theG)) (Mapping.tabulate (G_list \<phi>) (init \<circ> q\<^sub>0\<^sub>M \<circ> theG)) w i) q = Some (run ((nxt \<Sigma> \<delta>\<^sub>M \<circ> q\<^sub>0\<^sub>M \<circ> theG) q) ((init \<circ> q\<^sub>0\<^sub>M \<circ> theG) q) w i)

goal (1 subgoal):
 1. run (delta \<Sigma>) (initial \<phi>) w = abstract_state \<circ> run (delta\<^sub>C \<Sigma>) (initial\<^sub>C \<phi>) w
[PROOF STEP]
hence "run ?\<delta>\<^sub>2 ?q\<^sub>2 w i q = (\<lambda>m. (map_option rk) o (Mapping.lookup m)) (run ?\<delta>\<^sub>2' ?q\<^sub>2' w i) q"
[PROOF STATE]
proof (prove)
using this:
\<iota>\<^sub>\<times> (\<^bold>G \<phi>) (\<lambda>\<chi>. semi_mojmir_def.initial (q\<^sub>0\<^sub>M (theG \<chi>))) q = Some (semi_mojmir_def.initial (q\<^sub>0\<^sub>M (theG q)))
Mapping.lookup (run (\<up>\<Delta>\<^sub>\<times> (nxt \<Sigma> \<delta>\<^sub>M \<circ> q\<^sub>0\<^sub>M \<circ> theG)) (Mapping.tabulate (G_list \<phi>) (init \<circ> q\<^sub>0\<^sub>M \<circ> theG)) w i) q = Some (run ((nxt \<Sigma> \<delta>\<^sub>M \<circ> q\<^sub>0\<^sub>M \<circ> theG) q) ((init \<circ> q\<^sub>0\<^sub>M \<circ> theG) q) w i)

goal (1 subgoal):
 1. run (\<Delta>\<^sub>\<times> (\<lambda>\<chi>. semi_mojmir_def.step \<Sigma> \<delta>\<^sub>M (q\<^sub>0\<^sub>M (theG \<chi>)))) (\<iota>\<^sub>\<times> (\<^bold>G \<phi>) (\<lambda>\<chi>. semi_mojmir_def.initial (q\<^sub>0\<^sub>M (theG \<chi>)))) w i q = (map_option rk \<circ> Mapping.lookup (run (\<up>\<Delta>\<^sub>\<times> (nxt \<Sigma> \<delta>\<^sub>M \<circ> q\<^sub>0\<^sub>M \<circ> theG)) (Mapping.tabulate (G_list \<phi>) (init \<circ> q\<^sub>0\<^sub>M \<circ> theG)) w i)) q
[PROOF STEP]
unfolding product_run_Some[of "\<iota>\<^sub>\<times> (\<^bold>G \<phi>) (\<lambda>\<chi>. semi_mojmir_def.initial (q\<^sub>0\<^sub>M (theG \<chi>)))" q, OF init]
[PROOF STATE]
proof (prove)
using this:
\<iota>\<^sub>\<times> (\<^bold>G \<phi>) (\<lambda>\<chi>. semi_mojmir_def.initial (q\<^sub>0\<^sub>M (theG \<chi>))) q = Some (semi_mojmir_def.initial (q\<^sub>0\<^sub>M (theG q)))
Mapping.lookup (run (\<up>\<Delta>\<^sub>\<times> (nxt \<Sigma> \<delta>\<^sub>M \<circ> q\<^sub>0\<^sub>M \<circ> theG)) (Mapping.tabulate (G_list \<phi>) (init \<circ> q\<^sub>0\<^sub>M \<circ> theG)) w i) q = Some (run ((nxt \<Sigma> \<delta>\<^sub>M \<circ> q\<^sub>0\<^sub>M \<circ> theG) q) ((init \<circ> q\<^sub>0\<^sub>M \<circ> theG) q) w i)

goal (1 subgoal):
 1. Some (run (semi_mojmir_def.step \<Sigma> \<delta>\<^sub>M (q\<^sub>0\<^sub>M (theG q))) (semi_mojmir_def.initial (q\<^sub>0\<^sub>M (theG q))) w i) = (map_option rk \<circ> Mapping.lookup (run (\<up>\<Delta>\<^sub>\<times> (nxt \<Sigma> \<delta>\<^sub>M \<circ> q\<^sub>0\<^sub>M \<circ> theG)) (Mapping.tabulate (G_list \<phi>) (init \<circ> q\<^sub>0\<^sub>M \<circ> theG)) w i)) q
[PROOF STEP]
by (simp del: product.simps nxt.simps rk.simps; unfold map_of_map semi_mojmir.nxt_run_step_run[OF semi_mojmir]; simp)
[PROOF STATE]
proof (state)
this:
run (\<Delta>\<^sub>\<times> (\<lambda>\<chi>. semi_mojmir_def.step \<Sigma> \<delta>\<^sub>M (q\<^sub>0\<^sub>M (theG \<chi>)))) (\<iota>\<^sub>\<times> (\<^bold>G \<phi>) (\<lambda>\<chi>. semi_mojmir_def.initial (q\<^sub>0\<^sub>M (theG \<chi>)))) w i q = (map_option rk \<circ> Mapping.lookup (run (\<up>\<Delta>\<^sub>\<times> (nxt \<Sigma> \<delta>\<^sub>M \<circ> q\<^sub>0\<^sub>M \<circ> theG)) (Mapping.tabulate (G_list \<phi>) (init \<circ> q\<^sub>0\<^sub>M \<circ> theG)) w i)) q

goal (1 subgoal):
 1. run (delta \<Sigma>) (initial \<phi>) w = abstract_state \<circ> run (delta\<^sub>C \<Sigma>) (initial\<^sub>C \<phi>) w
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?q19 \<in> \<^bold>G \<phi> \<Longrightarrow> run (\<Delta>\<^sub>\<times> (\<lambda>\<chi>. semi_mojmir_def.step \<Sigma> \<delta>\<^sub>M (q\<^sub>0\<^sub>M (theG \<chi>)))) (\<iota>\<^sub>\<times> (\<^bold>G \<phi>) (\<lambda>\<chi>. semi_mojmir_def.initial (q\<^sub>0\<^sub>M (theG \<chi>)))) w i ?q19 = (map_option rk \<circ> Mapping.lookup (run (\<up>\<Delta>\<^sub>\<times> (nxt \<Sigma> \<delta>\<^sub>M \<circ> q\<^sub>0\<^sub>M \<circ> theG)) (Mapping.tabulate (G_list \<phi>) (init \<circ> q\<^sub>0\<^sub>M \<circ> theG)) w i)) ?q19

goal (1 subgoal):
 1. run (delta \<Sigma>) (initial \<phi>) w = abstract_state \<circ> run (delta\<^sub>C \<Sigma>) (initial\<^sub>C \<phi>) w
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
?q19 \<notin> \<^bold>G \<phi> \<Longrightarrow> run (\<Delta>\<^sub>\<times> (\<lambda>\<chi>. semi_mojmir_def.step \<Sigma> \<delta>\<^sub>M (q\<^sub>0\<^sub>M (theG \<chi>)))) (\<iota>\<^sub>\<times> (\<^bold>G \<phi>) (\<lambda>\<chi>. semi_mojmir_def.initial (q\<^sub>0\<^sub>M (theG \<chi>)))) w i ?q19 = (map_option rk \<circ> Mapping.lookup (run (\<up>\<Delta>\<^sub>\<times> (nxt \<Sigma> \<delta>\<^sub>M \<circ> q\<^sub>0\<^sub>M \<circ> theG)) (Mapping.tabulate (G_list \<phi>) (init \<circ> q\<^sub>0\<^sub>M \<circ> theG)) w i)) ?q19
?q19 \<in> \<^bold>G \<phi> \<Longrightarrow> run (\<Delta>\<^sub>\<times> (\<lambda>\<chi>. semi_mojmir_def.step \<Sigma> \<delta>\<^sub>M (q\<^sub>0\<^sub>M (theG \<chi>)))) (\<iota>\<^sub>\<times> (\<^bold>G \<phi>) (\<lambda>\<chi>. semi_mojmir_def.initial (q\<^sub>0\<^sub>M (theG \<chi>)))) w i ?q19 = (map_option rk \<circ> Mapping.lookup (run (\<up>\<Delta>\<^sub>\<times> (nxt \<Sigma> \<delta>\<^sub>M \<circ> q\<^sub>0\<^sub>M \<circ> theG)) (Mapping.tabulate (G_list \<phi>) (init \<circ> q\<^sub>0\<^sub>M \<circ> theG)) w i)) ?q19
[PROOF STEP]
have "run ?\<delta>\<^sub>2 ?q\<^sub>2 w i = (\<lambda>m. (map_option rk) o (Mapping.lookup m)) (run ?\<delta>\<^sub>2' ?q\<^sub>2' w i)"
[PROOF STATE]
proof (prove)
using this:
?q19 \<notin> \<^bold>G \<phi> \<Longrightarrow> run (\<Delta>\<^sub>\<times> (\<lambda>\<chi>. semi_mojmir_def.step \<Sigma> \<delta>\<^sub>M (q\<^sub>0\<^sub>M (theG \<chi>)))) (\<iota>\<^sub>\<times> (\<^bold>G \<phi>) (\<lambda>\<chi>. semi_mojmir_def.initial (q\<^sub>0\<^sub>M (theG \<chi>)))) w i ?q19 = (map_option rk \<circ> Mapping.lookup (run (\<up>\<Delta>\<^sub>\<times> (nxt \<Sigma> \<delta>\<^sub>M \<circ> q\<^sub>0\<^sub>M \<circ> theG)) (Mapping.tabulate (G_list \<phi>) (init \<circ> q\<^sub>0\<^sub>M \<circ> theG)) w i)) ?q19
?q19 \<in> \<^bold>G \<phi> \<Longrightarrow> run (\<Delta>\<^sub>\<times> (\<lambda>\<chi>. semi_mojmir_def.step \<Sigma> \<delta>\<^sub>M (q\<^sub>0\<^sub>M (theG \<chi>)))) (\<iota>\<^sub>\<times> (\<^bold>G \<phi>) (\<lambda>\<chi>. semi_mojmir_def.initial (q\<^sub>0\<^sub>M (theG \<chi>)))) w i ?q19 = (map_option rk \<circ> Mapping.lookup (run (\<up>\<Delta>\<^sub>\<times> (nxt \<Sigma> \<delta>\<^sub>M \<circ> q\<^sub>0\<^sub>M \<circ> theG)) (Mapping.tabulate (G_list \<phi>) (init \<circ> q\<^sub>0\<^sub>M \<circ> theG)) w i)) ?q19

goal (1 subgoal):
 1. run (\<Delta>\<^sub>\<times> (\<lambda>\<chi>. semi_mojmir_def.step \<Sigma> \<delta>\<^sub>M (q\<^sub>0\<^sub>M (theG \<chi>)))) (\<iota>\<^sub>\<times> (\<^bold>G \<phi>) (\<lambda>\<chi>. semi_mojmir_def.initial (q\<^sub>0\<^sub>M (theG \<chi>)))) w i = map_option rk \<circ> Mapping.lookup (run (\<up>\<Delta>\<^sub>\<times> (nxt \<Sigma> \<delta>\<^sub>M \<circ> q\<^sub>0\<^sub>M \<circ> theG)) (Mapping.tabulate (G_list \<phi>) (init \<circ> q\<^sub>0\<^sub>M \<circ> theG)) w i)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
run (\<Delta>\<^sub>\<times> (\<lambda>\<chi>. semi_mojmir_def.step \<Sigma> \<delta>\<^sub>M (q\<^sub>0\<^sub>M (theG \<chi>)))) (\<iota>\<^sub>\<times> (\<^bold>G \<phi>) (\<lambda>\<chi>. semi_mojmir_def.initial (q\<^sub>0\<^sub>M (theG \<chi>)))) w i = map_option rk \<circ> Mapping.lookup (run (\<up>\<Delta>\<^sub>\<times> (nxt \<Sigma> \<delta>\<^sub>M \<circ> q\<^sub>0\<^sub>M \<circ> theG)) (Mapping.tabulate (G_list \<phi>) (init \<circ> q\<^sub>0\<^sub>M \<circ> theG)) w i)

goal (1 subgoal):
 1. run (delta \<Sigma>) (initial \<phi>) w = abstract_state \<circ> run (delta\<^sub>C \<Sigma>) (initial\<^sub>C \<phi>) w
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
run (\<Delta>\<^sub>\<times> (\<lambda>\<chi>. semi_mojmir_def.step \<Sigma> \<delta>\<^sub>M (q\<^sub>0\<^sub>M (theG \<chi>)))) (\<iota>\<^sub>\<times> (\<^bold>G \<phi>) (\<lambda>\<chi>. semi_mojmir_def.initial (q\<^sub>0\<^sub>M (theG \<chi>)))) w ?i19 = map_option rk \<circ> Mapping.lookup (run (\<up>\<Delta>\<^sub>\<times> (nxt \<Sigma> \<delta>\<^sub>M \<circ> q\<^sub>0\<^sub>M \<circ> theG)) (Mapping.tabulate (G_list \<phi>) (init \<circ> q\<^sub>0\<^sub>M \<circ> theG)) w ?i19)

goal (1 subgoal):
 1. run (delta \<Sigma>) (initial \<phi>) w = abstract_state \<circ> run (delta\<^sub>C \<Sigma>) (initial\<^sub>C \<phi>) w
[PROOF STEP]
hence "\<And>i. run (delta \<Sigma>) (initial \<phi>) w i = abstract_state (run (delta\<^sub>C \<Sigma>) (initial\<^sub>C \<phi>) w i)"
[PROOF STATE]
proof (prove)
using this:
run (\<Delta>\<^sub>\<times> (\<lambda>\<chi>. semi_mojmir_def.step \<Sigma> \<delta>\<^sub>M (q\<^sub>0\<^sub>M (theG \<chi>)))) (\<iota>\<^sub>\<times> (\<^bold>G \<phi>) (\<lambda>\<chi>. semi_mojmir_def.initial (q\<^sub>0\<^sub>M (theG \<chi>)))) w ?i19 = map_option rk \<circ> Mapping.lookup (run (\<up>\<Delta>\<^sub>\<times> (nxt \<Sigma> \<delta>\<^sub>M \<circ> q\<^sub>0\<^sub>M \<circ> theG)) (Mapping.tabulate (G_list \<phi>) (init \<circ> q\<^sub>0\<^sub>M \<circ> theG)) w ?i19)

goal (1 subgoal):
 1. \<And>i. run (delta \<Sigma>) (initial \<phi>) w i = abstract_state (run (delta\<^sub>C \<Sigma>) (initial\<^sub>C \<phi>) w i)
[PROOF STEP]
using finite_\<Sigma> bounded_w
[PROOF STATE]
proof (prove)
using this:
run (\<Delta>\<^sub>\<times> (\<lambda>\<chi>. semi_mojmir_def.step \<Sigma> \<delta>\<^sub>M (q\<^sub>0\<^sub>M (theG \<chi>)))) (\<iota>\<^sub>\<times> (\<^bold>G \<phi>) (\<lambda>\<chi>. semi_mojmir_def.initial (q\<^sub>0\<^sub>M (theG \<chi>)))) w ?i19 = map_option rk \<circ> Mapping.lookup (run (\<up>\<Delta>\<^sub>\<times> (nxt \<Sigma> \<delta>\<^sub>M \<circ> q\<^sub>0\<^sub>M \<circ> theG)) (Mapping.tabulate (G_list \<phi>) (init \<circ> q\<^sub>0\<^sub>M \<circ> theG)) w ?i19)
finite \<Sigma>
range w \<subseteq> \<Sigma>

goal (1 subgoal):
 1. \<And>i. run (delta \<Sigma>) (initial \<phi>) w i = abstract_state (run (delta\<^sub>C \<Sigma>) (initial\<^sub>C \<phi>) w i)
[PROOF STEP]
by (simp add: simple_product_run comp_def del: simple_product.simps)
[PROOF STATE]
proof (state)
this:
run (delta \<Sigma>) (initial \<phi>) w ?i17 = abstract_state (run (delta\<^sub>C \<Sigma>) (initial\<^sub>C \<phi>) w ?i17)

goal (1 subgoal):
 1. run (delta \<Sigma>) (initial \<phi>) w = abstract_state \<circ> run (delta\<^sub>C \<Sigma>) (initial\<^sub>C \<phi>) w
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
run (delta \<Sigma>) (initial \<phi>) w ?i17 = abstract_state (run (delta\<^sub>C \<Sigma>) (initial\<^sub>C \<phi>) w ?i17)

goal (1 subgoal):
 1. run (delta \<Sigma>) (initial \<phi>) w = abstract_state \<circ> run (delta\<^sub>C \<Sigma>) (initial\<^sub>C \<phi>) w
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
run (delta \<Sigma>) (initial \<phi>) w = abstract_state \<circ> run (delta\<^sub>C \<Sigma>) (initial\<^sub>C \<phi>) w

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma
  assumes "t \<in> reach\<^sub>t \<Sigma> (delta\<^sub>C \<Sigma>) (initial\<^sub>C \<phi>)"
  assumes "\<chi> \<in> \<^bold>G \<phi>"
  shows Acc_fin\<^sub>C_correct:
    "abstract_transition t \<in> Acc_fin \<Sigma> \<pi> \<chi> \<longleftrightarrow> Acc_fin\<^sub>C \<Sigma> (Mapping.Mapping \<pi>) \<chi> t" (is ?t1)
    and Acc_inf\<^sub>C_correct:
    "abstract_transition t \<in> Acc_inf \<pi> \<chi> \<longleftrightarrow> Acc_inf\<^sub>C (Mapping.Mapping \<pi>) \<chi> t" (is ?t2)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (abstract_transition t \<in> Acc_fin \<Sigma> \<pi> \<chi>) = Acc_fin\<^sub>C \<Sigma> (mapping.Mapping \<pi>) \<chi> t &&& (abstract_transition t \<in> Acc_inf \<pi> \<chi>) = Acc_inf\<^sub>C (mapping.Mapping \<pi>) \<chi> t
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. (abstract_transition t \<in> Acc_fin \<Sigma> \<pi> \<chi>) = Acc_fin\<^sub>C \<Sigma> (mapping.Mapping \<pi>) \<chi> t
 2. (abstract_transition t \<in> Acc_inf \<pi> \<chi>) = Acc_inf\<^sub>C (mapping.Mapping \<pi>) \<chi> t
[PROOF STEP]
obtain x y \<nu> z z' where t_def [simp]: "t = ((x, y), \<nu>, (z, z'))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>x y \<nu> z z'. t = ((x, y), \<nu>, z, z') \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis prod.collapse)
[PROOF STATE]
proof (state)
this:
t = ((x, y), \<nu>, z, z')

goal (2 subgoals):
 1. (abstract_transition t \<in> Acc_fin \<Sigma> \<pi> \<chi>) = Acc_fin\<^sub>C \<Sigma> (mapping.Mapping \<pi>) \<chi> t
 2. (abstract_transition t \<in> Acc_inf \<pi> \<chi>) = Acc_inf\<^sub>C (mapping.Mapping \<pi>) \<chi> t
[PROOF STEP]
have "(x, y) \<in> reach \<Sigma> (delta\<^sub>C \<Sigma>) (initial\<^sub>C \<phi>)"
    and "(z, z') \<in> reach \<Sigma> (delta\<^sub>C \<Sigma>) (initial\<^sub>C \<phi>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x, y) \<in> reach \<Sigma> (delta\<^sub>C \<Sigma>) (initial\<^sub>C \<phi>) &&& (z, z') \<in> reach \<Sigma> (delta\<^sub>C \<Sigma>) (initial\<^sub>C \<phi>)
[PROOF STEP]
using assms(1)
[PROOF STATE]
proof (prove)
using this:
t \<in> reach\<^sub>t \<Sigma> (delta\<^sub>C \<Sigma>) (initial\<^sub>C \<phi>)

goal (1 subgoal):
 1. (x, y) \<in> reach \<Sigma> (delta\<^sub>C \<Sigma>) (initial\<^sub>C \<phi>) &&& (z, z') \<in> reach \<Sigma> (delta\<^sub>C \<Sigma>) (initial\<^sub>C \<phi>)
[PROOF STEP]
unfolding reach\<^sub>t_def reach_def run\<^sub>t.simps t_def
[PROOF STATE]
proof (prove)
using this:
((x, y), \<nu>, z, z') \<in> {(run (delta\<^sub>C \<Sigma>) (initial\<^sub>C \<phi>) w n, w n, run (delta\<^sub>C \<Sigma>) (initial\<^sub>C \<phi>) w (Suc n)) |w n. range w \<subseteq> \<Sigma>}

goal (1 subgoal):
 1. (x, y) \<in> {run (delta\<^sub>C \<Sigma>) (initial\<^sub>C \<phi>) w n |w n. range w \<subseteq> \<Sigma>} &&& (z, z') \<in> {run (delta\<^sub>C \<Sigma>) (initial\<^sub>C \<phi>) w n |w n. range w \<subseteq> \<Sigma>}
[PROOF STEP]
by blast+
[PROOF STATE]
proof (state)
this:
(x, y) \<in> reach \<Sigma> (delta\<^sub>C \<Sigma>) (initial\<^sub>C \<phi>)
(z, z') \<in> reach \<Sigma> (delta\<^sub>C \<Sigma>) (initial\<^sub>C \<phi>)

goal (2 subgoals):
 1. (abstract_transition t \<in> Acc_fin \<Sigma> \<pi> \<chi>) = Acc_fin\<^sub>C \<Sigma> (mapping.Mapping \<pi>) \<chi> t
 2. (abstract_transition t \<in> Acc_inf \<pi> \<chi>) = Acc_inf\<^sub>C (mapping.Mapping \<pi>) \<chi> t
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(x, y) \<in> reach \<Sigma> (delta\<^sub>C \<Sigma>) (initial\<^sub>C \<phi>)
(z, z') \<in> reach \<Sigma> (delta\<^sub>C \<Sigma>) (initial\<^sub>C \<phi>)
[PROOF STEP]
obtain m m' where [simp]: "Mapping.lookup y \<chi> = Some m"
    and "Mapping.lookup y \<chi> \<noteq> None"
    and [simp]: "Mapping.lookup z' \<chi> = Some m'"
[PROOF STATE]
proof (prove)
using this:
(x, y) \<in> reach \<Sigma> (delta\<^sub>C \<Sigma>) (initial\<^sub>C \<phi>)
(z, z') \<in> reach \<Sigma> (delta\<^sub>C \<Sigma>) (initial\<^sub>C \<phi>)

goal (1 subgoal):
 1. (\<And>m m'. \<lbrakk>Mapping.lookup y \<chi> = Some m; Mapping.lookup y \<chi> \<noteq> None; Mapping.lookup z' \<chi> = Some m'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms(2)
[PROOF STATE]
proof (prove)
using this:
(x, y) \<in> reach \<Sigma> (delta\<^sub>C \<Sigma>) (initial\<^sub>C \<phi>)
(z, z') \<in> reach \<Sigma> (delta\<^sub>C \<Sigma>) (initial\<^sub>C \<phi>)
\<chi> \<in> \<^bold>G \<phi>

goal (1 subgoal):
 1. (\<And>m m'. \<lbrakk>Mapping.lookup y \<chi> = Some m; Mapping.lookup y \<chi> \<noteq> None; Mapping.lookup z' \<chi> = Some m'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (blast dest: reach_delta_initial)+
[PROOF STATE]
proof (state)
this:
Mapping.lookup y \<chi> = Some m
Mapping.lookup y \<chi> \<noteq> None
Mapping.lookup z' \<chi> = Some m'

goal (2 subgoals):
 1. (abstract_transition t \<in> Acc_fin \<Sigma> \<pi> \<chi>) = Acc_fin\<^sub>C \<Sigma> (mapping.Mapping \<pi>) \<chi> t
 2. (abstract_transition t \<in> Acc_inf \<pi> \<chi>) = Acc_inf\<^sub>C (mapping.Mapping \<pi>) \<chi> t
[PROOF STEP]
have FF [simp]: "fail_filt \<Sigma> \<delta>\<^sub>M (q\<^sub>0\<^sub>M (theG \<chi>)) (ltl_prop_entails_abs (dom \<pi>)) (the (Mapping.lookup y \<chi>), \<nu>, [])
    = ((the (map_option rk (Mapping.lookup y \<chi>)), \<nu>, (\<lambda>x. Some 0)) \<in> mojmir_to_rabin_def.fail\<^sub>R \<Sigma> \<delta>\<^sub>M (q\<^sub>0\<^sub>M (theG \<chi>)) {q. dom \<pi> \<up>\<Turnstile>\<^sub>P q})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fail_filt \<Sigma> \<delta>\<^sub>M (q\<^sub>0\<^sub>M (theG \<chi>)) (ltl_prop_entails_abs (dom \<pi>)) (the (Mapping.lookup y \<chi>), \<nu>, []) = ((the (map_option rk (Mapping.lookup y \<chi>)), \<nu>, \<lambda>x. Some 0) \<in> mojmir_to_rabin_def.fail\<^sub>R \<Sigma> \<delta>\<^sub>M (q\<^sub>0\<^sub>M (theG \<chi>)) {q. dom \<pi> \<up>\<Turnstile>\<^sub>P q})
[PROOF STEP]
unfolding option.map_sel[OF \<open>Mapping.lookup y \<chi> \<noteq> None\<close>] fail_filt_eq[where y = "[]", symmetric]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fail_filt \<Sigma> \<delta>\<^sub>M (q\<^sub>0\<^sub>M (theG \<chi>)) (ltl_prop_entails_abs (dom \<pi>)) (the (Mapping.lookup y \<chi>), \<nu>, []) = fail_filt \<Sigma> \<delta>\<^sub>M (q\<^sub>0\<^sub>M (theG \<chi>)) (ltl_prop_entails_abs (dom \<pi>)) (the (Mapping.lookup y \<chi>), \<nu>, [])
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
fail_filt \<Sigma> \<delta>\<^sub>M (q\<^sub>0\<^sub>M (theG \<chi>)) (ltl_prop_entails_abs (dom \<pi>)) (the (Mapping.lookup y \<chi>), \<nu>, []) = ((the (map_option rk (Mapping.lookup y \<chi>)), \<nu>, \<lambda>x. Some 0) \<in> mojmir_to_rabin_def.fail\<^sub>R \<Sigma> \<delta>\<^sub>M (q\<^sub>0\<^sub>M (theG \<chi>)) {q. dom \<pi> \<up>\<Turnstile>\<^sub>P q})

goal (2 subgoals):
 1. (abstract_transition t \<in> Acc_fin \<Sigma> \<pi> \<chi>) = Acc_fin\<^sub>C \<Sigma> (mapping.Mapping \<pi>) \<chi> t
 2. (abstract_transition t \<in> Acc_inf \<pi> \<chi>) = Acc_inf\<^sub>C (mapping.Mapping \<pi>) \<chi> t
[PROOF STEP]
have MF [simp]: "\<And>i. merge_filt \<delta>\<^sub>M (q\<^sub>0\<^sub>M (theG \<chi>)) (ltl_prop_entails_abs (dom \<pi>)) i (the (Mapping.lookup y \<chi>), \<nu>, [])
    = ((the (map_option rk (Mapping.lookup y \<chi>)), \<nu>, (\<lambda>x. Some 0)) \<in> mojmir_to_rabin_def.merge\<^sub>R \<delta>\<^sub>M (q\<^sub>0\<^sub>M (theG \<chi>)) {q. dom \<pi> \<up>\<Turnstile>\<^sub>P q} i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i. merge_filt \<delta>\<^sub>M (q\<^sub>0\<^sub>M (theG \<chi>)) (ltl_prop_entails_abs (dom \<pi>)) i (the (Mapping.lookup y \<chi>), \<nu>, []) = ((the (map_option rk (Mapping.lookup y \<chi>)), \<nu>, \<lambda>x. Some 0) \<in> mojmir_to_rabin_def.merge\<^sub>R \<delta>\<^sub>M (q\<^sub>0\<^sub>M (theG \<chi>)) {q. dom \<pi> \<up>\<Turnstile>\<^sub>P q} i)
[PROOF STEP]
unfolding option.map_sel[OF \<open>Mapping.lookup y \<chi> \<noteq> None\<close>] merge_filt_eq[where y = "[]", symmetric]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i. merge_filt \<delta>\<^sub>M (q\<^sub>0\<^sub>M (theG \<chi>)) (ltl_prop_entails_abs (dom \<pi>)) i (the (Mapping.lookup y \<chi>), \<nu>, []) = merge_filt \<delta>\<^sub>M (q\<^sub>0\<^sub>M (theG \<chi>)) (ltl_prop_entails_abs (dom \<pi>)) i (the (Mapping.lookup y \<chi>), \<nu>, [])
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
merge_filt \<delta>\<^sub>M (q\<^sub>0\<^sub>M (theG \<chi>)) (ltl_prop_entails_abs (dom \<pi>)) ?i17 (the (Mapping.lookup y \<chi>), \<nu>, []) = ((the (map_option rk (Mapping.lookup y \<chi>)), \<nu>, \<lambda>x. Some 0) \<in> mojmir_to_rabin_def.merge\<^sub>R \<delta>\<^sub>M (q\<^sub>0\<^sub>M (theG \<chi>)) {q. dom \<pi> \<up>\<Turnstile>\<^sub>P q} ?i17)

goal (2 subgoals):
 1. (abstract_transition t \<in> Acc_fin \<Sigma> \<pi> \<chi>) = Acc_fin\<^sub>C \<Sigma> (mapping.Mapping \<pi>) \<chi> t
 2. (abstract_transition t \<in> Acc_inf \<pi> \<chi>) = Acc_inf\<^sub>C (mapping.Mapping \<pi>) \<chi> t
[PROOF STEP]
have SF [simp]: "\<And>i. succeed_filt \<delta>\<^sub>M (q\<^sub>0\<^sub>M (theG \<chi>)) (ltl_prop_entails_abs (dom \<pi>)) i (the (Mapping.lookup y \<chi>), \<nu>, [])
    = ((the (map_option rk (Mapping.lookup y \<chi>)), \<nu>, (\<lambda>x. Some 0)) \<in> mojmir_to_rabin_def.succeed\<^sub>R \<delta>\<^sub>M (q\<^sub>0\<^sub>M (theG \<chi>)) {q. dom \<pi> \<up>\<Turnstile>\<^sub>P q} i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i. succeed_filt \<delta>\<^sub>M (q\<^sub>0\<^sub>M (theG \<chi>)) (ltl_prop_entails_abs (dom \<pi>)) i (the (Mapping.lookup y \<chi>), \<nu>, []) = ((the (map_option rk (Mapping.lookup y \<chi>)), \<nu>, \<lambda>x. Some 0) \<in> mojmir_to_rabin_def.succeed\<^sub>R \<delta>\<^sub>M (q\<^sub>0\<^sub>M (theG \<chi>)) {q. dom \<pi> \<up>\<Turnstile>\<^sub>P q} i)
[PROOF STEP]
unfolding option.map_sel[OF \<open>Mapping.lookup y \<chi> \<noteq> None\<close>] succeed_filt_eq[where y = "[]", symmetric]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i. succeed_filt \<delta>\<^sub>M (q\<^sub>0\<^sub>M (theG \<chi>)) (ltl_prop_entails_abs (dom \<pi>)) i (the (Mapping.lookup y \<chi>), \<nu>, []) = succeed_filt \<delta>\<^sub>M (q\<^sub>0\<^sub>M (theG \<chi>)) (ltl_prop_entails_abs (dom \<pi>)) i (the (Mapping.lookup y \<chi>), \<nu>, [])
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
succeed_filt \<delta>\<^sub>M (q\<^sub>0\<^sub>M (theG \<chi>)) (ltl_prop_entails_abs (dom \<pi>)) ?i17 (the (Mapping.lookup y \<chi>), \<nu>, []) = ((the (map_option rk (Mapping.lookup y \<chi>)), \<nu>, \<lambda>x. Some 0) \<in> mojmir_to_rabin_def.succeed\<^sub>R \<delta>\<^sub>M (q\<^sub>0\<^sub>M (theG \<chi>)) {q. dom \<pi> \<up>\<Turnstile>\<^sub>P q} ?i17)

goal (2 subgoals):
 1. (abstract_transition t \<in> Acc_fin \<Sigma> \<pi> \<chi>) = Acc_fin\<^sub>C \<Sigma> (mapping.Mapping \<pi>) \<chi> t
 2. (abstract_transition t \<in> Acc_inf \<pi> \<chi>) = Acc_inf\<^sub>C (mapping.Mapping \<pi>) \<chi> t
[PROOF STEP]
note mojmir_to_rabin_def.fail\<^sub>R_def [simp]
[PROOF STATE]
proof (state)
this:
mojmir_to_rabin_def.fail\<^sub>R ?\<Sigma> ?\<delta> ?q\<^sub>0 ?F = {uu_. \<exists>r \<nu> s q q'. uu_ = (r, \<nu>, s) \<and> r q \<noteq> None \<and> q' = ?\<delta> q \<nu> \<and> q' \<notin> ?F \<and> semi_mojmir_def.sink ?\<Sigma> ?\<delta> ?q\<^sub>0 q'}

goal (2 subgoals):
 1. (abstract_transition t \<in> Acc_fin \<Sigma> \<pi> \<chi>) = Acc_fin\<^sub>C \<Sigma> (mapping.Mapping \<pi>) \<chi> t
 2. (abstract_transition t \<in> Acc_inf \<pi> \<chi>) = Acc_inf\<^sub>C (mapping.Mapping \<pi>) \<chi> t
[PROOF STEP]
note mojmir_to_rabin_def.merge\<^sub>R_def [simp]
[PROOF STATE]
proof (state)
this:
mojmir_to_rabin_def.merge\<^sub>R ?\<delta> ?q\<^sub>0 ?F ?i = {uu_. \<exists>r \<nu> s q q' j. uu_ = (r, \<nu>, s) \<and> r q = Some j \<and> j < ?i \<and> q' = ?\<delta> q \<nu> \<and> ((\<exists>q''. q' = ?\<delta> q'' \<nu> \<and> r q'' \<noteq> None \<and> q'' \<noteq> q) \<or> q' = ?q\<^sub>0) \<and> q' \<notin> ?F}

goal (2 subgoals):
 1. (abstract_transition t \<in> Acc_fin \<Sigma> \<pi> \<chi>) = Acc_fin\<^sub>C \<Sigma> (mapping.Mapping \<pi>) \<chi> t
 2. (abstract_transition t \<in> Acc_inf \<pi> \<chi>) = Acc_inf\<^sub>C (mapping.Mapping \<pi>) \<chi> t
[PROOF STEP]
note mojmir_to_rabin_def.succeed\<^sub>R_def [simp]
[PROOF STATE]
proof (state)
this:
mojmir_to_rabin_def.succeed\<^sub>R ?\<delta> ?q\<^sub>0 ?F ?i = {uu_. \<exists>r \<nu> s q. uu_ = (r, \<nu>, s) \<and> r q = Some ?i \<and> q \<notin> ?F - {?q\<^sub>0} \<and> ?\<delta> q \<nu> \<in> ?F}

goal (2 subgoals):
 1. (abstract_transition t \<in> Acc_fin \<Sigma> \<pi> \<chi>) = Acc_fin\<^sub>C \<Sigma> (mapping.Mapping \<pi>) \<chi> t
 2. (abstract_transition t \<in> Acc_inf \<pi> \<chi>) = Acc_inf\<^sub>C (mapping.Mapping \<pi>) \<chi> t
[PROOF STEP]
show ?t1 and ?t2
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (abstract_transition t \<in> Acc_fin \<Sigma> \<pi> \<chi>) = Acc_fin\<^sub>C \<Sigma> (mapping.Mapping \<pi>) \<chi> t &&& (abstract_transition t \<in> Acc_inf \<pi> \<chi>) = Acc_inf\<^sub>C (mapping.Mapping \<pi>) \<chi> t
[PROOF STEP]
by (simp_all add: Let_def keys.abs_eq lookup.abs_eq del: rk.simps)
       (rule; metis option.distinct(1) option.sel option.collapse rk_facts(1))+
[PROOF STATE]
proof (state)
this:
(abstract_transition t \<in> Acc_fin \<Sigma> \<pi> \<chi>) = Acc_fin\<^sub>C \<Sigma> (mapping.Mapping \<pi>) \<chi> t
(abstract_transition t \<in> Acc_inf \<pi> \<chi>) = Acc_inf\<^sub>C (mapping.Mapping \<pi>) \<chi> t

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem ltl_to_generalized_rabin\<^sub>C_correct:
  assumes "\<Sigma> = set \<Sigma>'"
  shows "accept\<^sub>G\<^sub>R (ltl_to_generalized_rabin \<Sigma> \<phi>) w \<longleftrightarrow> accept\<^sub>G\<^sub>R_LTS (ltl_to_generalized_rabin\<^sub>C \<Sigma>' \<phi>) w"
  (is "?lhs \<longleftrightarrow> ?rhs")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. accept\<^sub>G\<^sub>R (\<A> \<Sigma> \<phi>) w = accept\<^sub>G\<^sub>R_LTS (ltl_to_generalized_rabin\<^sub>C \<Sigma>' \<phi>) w
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. accept\<^sub>G\<^sub>R (\<A> \<Sigma> \<phi>) w \<Longrightarrow> accept\<^sub>G\<^sub>R_LTS (ltl_to_generalized_rabin\<^sub>C \<Sigma>' \<phi>) w
 2. accept\<^sub>G\<^sub>R_LTS (ltl_to_generalized_rabin\<^sub>C \<Sigma>' \<phi>) w \<Longrightarrow> accept\<^sub>G\<^sub>R (\<A> \<Sigma> \<phi>) w
[PROOF STEP]
let ?\<delta> = "delta \<Sigma>"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. accept\<^sub>G\<^sub>R (\<A> \<Sigma> \<phi>) w \<Longrightarrow> accept\<^sub>G\<^sub>R_LTS (ltl_to_generalized_rabin\<^sub>C \<Sigma>' \<phi>) w
 2. accept\<^sub>G\<^sub>R_LTS (ltl_to_generalized_rabin\<^sub>C \<Sigma>' \<phi>) w \<Longrightarrow> accept\<^sub>G\<^sub>R (\<A> \<Sigma> \<phi>) w
[PROOF STEP]
let ?q\<^sub>0 = "initial \<phi>"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. accept\<^sub>G\<^sub>R (\<A> \<Sigma> \<phi>) w \<Longrightarrow> accept\<^sub>G\<^sub>R_LTS (ltl_to_generalized_rabin\<^sub>C \<Sigma>' \<phi>) w
 2. accept\<^sub>G\<^sub>R_LTS (ltl_to_generalized_rabin\<^sub>C \<Sigma>' \<phi>) w \<Longrightarrow> accept\<^sub>G\<^sub>R (\<A> \<Sigma> \<phi>) w
[PROOF STEP]
let ?\<delta>\<^sub>C = "delta\<^sub>C \<Sigma>"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. accept\<^sub>G\<^sub>R (\<A> \<Sigma> \<phi>) w \<Longrightarrow> accept\<^sub>G\<^sub>R_LTS (ltl_to_generalized_rabin\<^sub>C \<Sigma>' \<phi>) w
 2. accept\<^sub>G\<^sub>R_LTS (ltl_to_generalized_rabin\<^sub>C \<Sigma>' \<phi>) w \<Longrightarrow> accept\<^sub>G\<^sub>R (\<A> \<Sigma> \<phi>) w
[PROOF STEP]
let ?q\<^sub>0\<^sub>C = "initial\<^sub>C \<phi>"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. accept\<^sub>G\<^sub>R (\<A> \<Sigma> \<phi>) w \<Longrightarrow> accept\<^sub>G\<^sub>R_LTS (ltl_to_generalized_rabin\<^sub>C \<Sigma>' \<phi>) w
 2. accept\<^sub>G\<^sub>R_LTS (ltl_to_generalized_rabin\<^sub>C \<Sigma>' \<phi>) w \<Longrightarrow> accept\<^sub>G\<^sub>R (\<A> \<Sigma> \<phi>) w
[PROOF STEP]
let ?reach\<^sub>C = "reach\<^sub>t \<Sigma> (delta\<^sub>C \<Sigma>) (initial\<^sub>C \<phi>)"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. accept\<^sub>G\<^sub>R (\<A> \<Sigma> \<phi>) w \<Longrightarrow> accept\<^sub>G\<^sub>R_LTS (ltl_to_generalized_rabin\<^sub>C \<Sigma>' \<phi>) w
 2. accept\<^sub>G\<^sub>R_LTS (ltl_to_generalized_rabin\<^sub>C \<Sigma>' \<phi>) w \<Longrightarrow> accept\<^sub>G\<^sub>R (\<A> \<Sigma> \<phi>) w
[PROOF STEP]
note reachable_transitions\<^sub>C_simp[simp] = reachable_transitions\<^sub>C_eq[OF assms]
[PROOF STATE]
proof (state)
this:
reachable_transitions\<^sub>C \<Sigma>' ?\<phi> = reach\<^sub>t \<Sigma> (delta\<^sub>C \<Sigma>) (initial\<^sub>C ?\<phi>)

goal (2 subgoals):
 1. accept\<^sub>G\<^sub>R (\<A> \<Sigma> \<phi>) w \<Longrightarrow> accept\<^sub>G\<^sub>R_LTS (ltl_to_generalized_rabin\<^sub>C \<Sigma>' \<phi>) w
 2. accept\<^sub>G\<^sub>R_LTS (ltl_to_generalized_rabin\<^sub>C \<Sigma>' \<phi>) w \<Longrightarrow> accept\<^sub>G\<^sub>R (\<A> \<Sigma> \<phi>) w
[PROOF STEP]
note max_rank_of\<^sub>C_simp[simp] = max_rank_of\<^sub>C_eq[OF assms]
[PROOF STATE]
proof (state)
this:
max_rank_of\<^sub>C \<Sigma>' ?\<psi> = max_rank_of \<Sigma> ?\<psi>

goal (2 subgoals):
 1. accept\<^sub>G\<^sub>R (\<A> \<Sigma> \<phi>) w \<Longrightarrow> accept\<^sub>G\<^sub>R_LTS (ltl_to_generalized_rabin\<^sub>C \<Sigma>' \<phi>) w
 2. accept\<^sub>G\<^sub>R_LTS (ltl_to_generalized_rabin\<^sub>C \<Sigma>' \<phi>) w \<Longrightarrow> accept\<^sub>G\<^sub>R (\<A> \<Sigma> \<phi>) w
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
max_rank_of\<^sub>C \<Sigma>' ?\<psi> = max_rank_of \<Sigma> ?\<psi>

goal (2 subgoals):
 1. accept\<^sub>G\<^sub>R (\<A> \<Sigma> \<phi>) w \<Longrightarrow> accept\<^sub>G\<^sub>R_LTS (ltl_to_generalized_rabin\<^sub>C \<Sigma>' \<phi>) w
 2. accept\<^sub>G\<^sub>R_LTS (ltl_to_generalized_rabin\<^sub>C \<Sigma>' \<phi>) w \<Longrightarrow> accept\<^sub>G\<^sub>R (\<A> \<Sigma> \<phi>) w
[PROOF STEP]
fix \<pi> :: "'a ltl \<Rightarrow> nat option"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. accept\<^sub>G\<^sub>R (\<A> \<Sigma> \<phi>) w \<Longrightarrow> accept\<^sub>G\<^sub>R_LTS (ltl_to_generalized_rabin\<^sub>C \<Sigma>' \<phi>) w
 2. accept\<^sub>G\<^sub>R_LTS (ltl_to_generalized_rabin\<^sub>C \<Sigma>' \<phi>) w \<Longrightarrow> accept\<^sub>G\<^sub>R (\<A> \<Sigma> \<phi>) w
[PROOF STEP]
assume \<pi>_wellformed: "dom \<pi> \<subseteq> \<^bold>G \<phi>"
[PROOF STATE]
proof (state)
this:
dom \<pi> \<subseteq> \<^bold>G \<phi>

goal (2 subgoals):
 1. accept\<^sub>G\<^sub>R (\<A> \<Sigma> \<phi>) w \<Longrightarrow> accept\<^sub>G\<^sub>R_LTS (ltl_to_generalized_rabin\<^sub>C \<Sigma>' \<phi>) w
 2. accept\<^sub>G\<^sub>R_LTS (ltl_to_generalized_rabin\<^sub>C \<Sigma>' \<phi>) w \<Longrightarrow> accept\<^sub>G\<^sub>R (\<A> \<Sigma> \<phi>) w
[PROOF STEP]
let ?F = "(M_fin \<pi> \<union> \<Union>{Acc_fin \<Sigma> \<pi> \<chi> | \<chi>. \<chi> \<in> dom \<pi>}, {Acc_inf \<pi> \<chi> | \<chi>. \<chi> \<in> dom \<pi>})"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. accept\<^sub>G\<^sub>R (\<A> \<Sigma> \<phi>) w \<Longrightarrow> accept\<^sub>G\<^sub>R_LTS (ltl_to_generalized_rabin\<^sub>C \<Sigma>' \<phi>) w
 2. accept\<^sub>G\<^sub>R_LTS (ltl_to_generalized_rabin\<^sub>C \<Sigma>' \<phi>) w \<Longrightarrow> accept\<^sub>G\<^sub>R (\<A> \<Sigma> \<phi>) w
[PROOF STEP]
let ?fin = "{t. M_fin\<^sub>C \<phi> (Mapping.Mapping \<pi>) t} \<union> {t. \<exists>\<chi> \<in> dom \<pi>. Acc_fin\<^sub>C \<Sigma> (Mapping.Mapping \<pi>) \<chi> t}"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. accept\<^sub>G\<^sub>R (\<A> \<Sigma> \<phi>) w \<Longrightarrow> accept\<^sub>G\<^sub>R_LTS (ltl_to_generalized_rabin\<^sub>C \<Sigma>' \<phi>) w
 2. accept\<^sub>G\<^sub>R_LTS (ltl_to_generalized_rabin\<^sub>C \<Sigma>' \<phi>) w \<Longrightarrow> accept\<^sub>G\<^sub>R (\<A> \<Sigma> \<phi>) w
[PROOF STEP]
let ?inf = "{{t. Acc_inf\<^sub>C (Mapping.Mapping \<pi>) \<chi> t} | \<chi>. \<chi> \<in> dom \<pi>}"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. accept\<^sub>G\<^sub>R (\<A> \<Sigma> \<phi>) w \<Longrightarrow> accept\<^sub>G\<^sub>R_LTS (ltl_to_generalized_rabin\<^sub>C \<Sigma>' \<phi>) w
 2. accept\<^sub>G\<^sub>R_LTS (ltl_to_generalized_rabin\<^sub>C \<Sigma>' \<phi>) w \<Longrightarrow> accept\<^sub>G\<^sub>R (\<A> \<Sigma> \<phi>) w
[PROOF STEP]
have finite_reach': "finite (reach\<^sub>t \<Sigma> (delta \<Sigma>) (initial \<phi>))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (reach\<^sub>t \<Sigma> (delta \<Sigma>) (initial \<phi>))
[PROOF STEP]
by (meson finite_reach finite_\<Sigma> finite_reach\<^sub>t)
[PROOF STATE]
proof (state)
this:
finite (reach\<^sub>t \<Sigma> (delta \<Sigma>) (initial \<phi>))

goal (2 subgoals):
 1. accept\<^sub>G\<^sub>R (\<A> \<Sigma> \<phi>) w \<Longrightarrow> accept\<^sub>G\<^sub>R_LTS (ltl_to_generalized_rabin\<^sub>C \<Sigma>' \<phi>) w
 2. accept\<^sub>G\<^sub>R_LTS (ltl_to_generalized_rabin\<^sub>C \<Sigma>' \<phi>) w \<Longrightarrow> accept\<^sub>G\<^sub>R (\<A> \<Sigma> \<phi>) w
[PROOF STEP]
have run_abstraction_correct':
      "run\<^sub>t (delta \<Sigma>) (initial \<phi>) w = abstract_transition o (run\<^sub>t (delta\<^sub>C \<Sigma>) (initial\<^sub>C \<phi>) w)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. run\<^sub>t (delta \<Sigma>) (initial \<phi>) w = abstract_transition \<circ> run\<^sub>t (delta\<^sub>C \<Sigma>) (initial\<^sub>C \<phi>) w
[PROOF STEP]
using run_abstraction_correct comp_def
[PROOF STATE]
proof (prove)
using this:
run (delta \<Sigma>) (initial ?\<phi>) w = abstract_state \<circ> run (delta\<^sub>C \<Sigma>) (initial\<^sub>C ?\<phi>) w
?f \<circ> ?g = (\<lambda>x. ?f (?g x))

goal (1 subgoal):
 1. run\<^sub>t (delta \<Sigma>) (initial \<phi>) w = abstract_transition \<circ> run\<^sub>t (delta\<^sub>C \<Sigma>) (initial\<^sub>C \<phi>) w
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
run\<^sub>t (delta \<Sigma>) (initial \<phi>) w = abstract_transition \<circ> run\<^sub>t (delta\<^sub>C \<Sigma>) (initial\<^sub>C \<phi>) w

goal (2 subgoals):
 1. accept\<^sub>G\<^sub>R (\<A> \<Sigma> \<phi>) w \<Longrightarrow> accept\<^sub>G\<^sub>R_LTS (ltl_to_generalized_rabin\<^sub>C \<Sigma>' \<phi>) w
 2. accept\<^sub>G\<^sub>R_LTS (ltl_to_generalized_rabin\<^sub>C \<Sigma>' \<phi>) w \<Longrightarrow> accept\<^sub>G\<^sub>R (\<A> \<Sigma> \<phi>) w
[PROOF STEP]
have "accepting_pair\<^sub>G\<^sub>R ?\<delta> ?q\<^sub>0 ?F w \<longleftrightarrow> accepting_pair\<^sub>G\<^sub>R ?\<delta>\<^sub>C  ?q\<^sub>0\<^sub>C (?fin, ?inf) w" (is "?l \<longleftrightarrow> _")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. accepting_pair\<^sub>G\<^sub>R (delta \<Sigma>) (initial \<phi>) (M_fin \<pi> \<union> \<Union> {Acc_fin \<Sigma> \<pi> \<chi> |\<chi>. \<chi> \<in> dom \<pi>}, {Acc_inf \<pi> \<chi> |\<chi>. \<chi> \<in> dom \<pi>}) w = accepting_pair\<^sub>G\<^sub>R (delta\<^sub>C \<Sigma>) (initial\<^sub>C \<phi>) ({t. M_fin\<^sub>C \<phi> (mapping.Mapping \<pi>) t} \<union> {t. \<exists>\<chi>\<in>dom \<pi>. Acc_fin\<^sub>C \<Sigma> (mapping.Mapping \<pi>) \<chi> t}, {{t. Acc_inf\<^sub>C (mapping.Mapping \<pi>) \<chi> t} |\<chi>. \<chi> \<in> dom \<pi>}) w
[PROOF STEP]
by (rule accepting_pair\<^sub>G\<^sub>R_abstract[OF finite_reach' finite_reach\<^sub>C bounded_w];
          insert \<open>dom \<pi> \<subseteq> \<^bold>G \<phi>\<close> M_fin\<^sub>C_correct Acc_fin\<^sub>C_correct Acc_inf\<^sub>C_correct run_abstraction_correct'; blast)
[PROOF STATE]
proof (state)
this:
accepting_pair\<^sub>G\<^sub>R (delta \<Sigma>) (initial \<phi>) (M_fin \<pi> \<union> \<Union> {Acc_fin \<Sigma> \<pi> \<chi> |\<chi>. \<chi> \<in> dom \<pi>}, {Acc_inf \<pi> \<chi> |\<chi>. \<chi> \<in> dom \<pi>}) w = accepting_pair\<^sub>G\<^sub>R (delta\<^sub>C \<Sigma>) (initial\<^sub>C \<phi>) ({t. M_fin\<^sub>C \<phi> (mapping.Mapping \<pi>) t} \<union> {t. \<exists>\<chi>\<in>dom \<pi>. Acc_fin\<^sub>C \<Sigma> (mapping.Mapping \<pi>) \<chi> t}, {{t. Acc_inf\<^sub>C (mapping.Mapping \<pi>) \<chi> t} |\<chi>. \<chi> \<in> dom \<pi>}) w

goal (2 subgoals):
 1. accept\<^sub>G\<^sub>R (\<A> \<Sigma> \<phi>) w \<Longrightarrow> accept\<^sub>G\<^sub>R_LTS (ltl_to_generalized_rabin\<^sub>C \<Sigma>' \<phi>) w
 2. accept\<^sub>G\<^sub>R_LTS (ltl_to_generalized_rabin\<^sub>C \<Sigma>' \<phi>) w \<Longrightarrow> accept\<^sub>G\<^sub>R (\<A> \<Sigma> \<phi>) w
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
accepting_pair\<^sub>G\<^sub>R (delta \<Sigma>) (initial \<phi>) (M_fin \<pi> \<union> \<Union> {Acc_fin \<Sigma> \<pi> \<chi> |\<chi>. \<chi> \<in> dom \<pi>}, {Acc_inf \<pi> \<chi> |\<chi>. \<chi> \<in> dom \<pi>}) w = accepting_pair\<^sub>G\<^sub>R (delta\<^sub>C \<Sigma>) (initial\<^sub>C \<phi>) ({t. M_fin\<^sub>C \<phi> (mapping.Mapping \<pi>) t} \<union> {t. \<exists>\<chi>\<in>dom \<pi>. Acc_fin\<^sub>C \<Sigma> (mapping.Mapping \<pi>) \<chi> t}, {{t. Acc_inf\<^sub>C (mapping.Mapping \<pi>) \<chi> t} |\<chi>. \<chi> \<in> dom \<pi>}) w

goal (2 subgoals):
 1. accept\<^sub>G\<^sub>R (\<A> \<Sigma> \<phi>) w \<Longrightarrow> accept\<^sub>G\<^sub>R_LTS (ltl_to_generalized_rabin\<^sub>C \<Sigma>' \<phi>) w
 2. accept\<^sub>G\<^sub>R_LTS (ltl_to_generalized_rabin\<^sub>C \<Sigma>' \<phi>) w \<Longrightarrow> accept\<^sub>G\<^sub>R (\<A> \<Sigma> \<phi>) w
[PROOF STEP]
have "\<dots> \<longleftrightarrow> accepting_pair\<^sub>G\<^sub>R_LTS ?reach\<^sub>C ?q\<^sub>0\<^sub>C (?fin \<inter> ?reach\<^sub>C, (\<lambda>I. I \<inter> ?reach\<^sub>C) ` ?inf) w" (is "_ \<longleftrightarrow> ?r")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. accepting_pair\<^sub>G\<^sub>R (delta\<^sub>C \<Sigma>) (initial\<^sub>C \<phi>) ({t. M_fin\<^sub>C \<phi> (mapping.Mapping \<pi>) t} \<union> {t. \<exists>\<chi>\<in>dom \<pi>. Acc_fin\<^sub>C \<Sigma> (mapping.Mapping \<pi>) \<chi> t}, {{t. Acc_inf\<^sub>C (mapping.Mapping \<pi>) \<chi> t} |\<chi>. \<chi> \<in> dom \<pi>}) w = accepting_pair\<^sub>G\<^sub>R_LTS (reach\<^sub>t \<Sigma> (delta\<^sub>C \<Sigma>) (initial\<^sub>C \<phi>)) (initial\<^sub>C \<phi>) (({t. M_fin\<^sub>C \<phi> (mapping.Mapping \<pi>) t} \<union> {t. \<exists>\<chi>\<in>dom \<pi>. Acc_fin\<^sub>C \<Sigma> (mapping.Mapping \<pi>) \<chi> t}) \<inter> reach\<^sub>t \<Sigma> (delta\<^sub>C \<Sigma>) (initial\<^sub>C \<phi>), (\<lambda>I. I \<inter> reach\<^sub>t \<Sigma> (delta\<^sub>C \<Sigma>) (initial\<^sub>C \<phi>)) ` {{t. Acc_inf\<^sub>C (mapping.Mapping \<pi>) \<chi> t} |\<chi>. \<chi> \<in> dom \<pi>}) w
[PROOF STEP]
using bounded_w
[PROOF STATE]
proof (prove)
using this:
range w \<subseteq> \<Sigma>

goal (1 subgoal):
 1. accepting_pair\<^sub>G\<^sub>R (delta\<^sub>C \<Sigma>) (initial\<^sub>C \<phi>) ({t. M_fin\<^sub>C \<phi> (mapping.Mapping \<pi>) t} \<union> {t. \<exists>\<chi>\<in>dom \<pi>. Acc_fin\<^sub>C \<Sigma> (mapping.Mapping \<pi>) \<chi> t}, {{t. Acc_inf\<^sub>C (mapping.Mapping \<pi>) \<chi> t} |\<chi>. \<chi> \<in> dom \<pi>}) w = accepting_pair\<^sub>G\<^sub>R_LTS (reach\<^sub>t \<Sigma> (delta\<^sub>C \<Sigma>) (initial\<^sub>C \<phi>)) (initial\<^sub>C \<phi>) (({t. M_fin\<^sub>C \<phi> (mapping.Mapping \<pi>) t} \<union> {t. \<exists>\<chi>\<in>dom \<pi>. Acc_fin\<^sub>C \<Sigma> (mapping.Mapping \<pi>) \<chi> t}) \<inter> reach\<^sub>t \<Sigma> (delta\<^sub>C \<Sigma>) (initial\<^sub>C \<phi>), (\<lambda>I. I \<inter> reach\<^sub>t \<Sigma> (delta\<^sub>C \<Sigma>) (initial\<^sub>C \<phi>)) ` {{t. Acc_inf\<^sub>C (mapping.Mapping \<pi>) \<chi> t} |\<chi>. \<chi> \<in> dom \<pi>}) w
[PROOF STEP]
by (simp only: accepting_pair\<^sub>G\<^sub>R_LTS[symmetric] accepting_pair\<^sub>G\<^sub>R_restrict[symmetric])
[PROOF STATE]
proof (state)
this:
accepting_pair\<^sub>G\<^sub>R (delta\<^sub>C \<Sigma>) (initial\<^sub>C \<phi>) ({t. M_fin\<^sub>C \<phi> (mapping.Mapping \<pi>) t} \<union> {t. \<exists>\<chi>\<in>dom \<pi>. Acc_fin\<^sub>C \<Sigma> (mapping.Mapping \<pi>) \<chi> t}, {{t. Acc_inf\<^sub>C (mapping.Mapping \<pi>) \<chi> t} |\<chi>. \<chi> \<in> dom \<pi>}) w = accepting_pair\<^sub>G\<^sub>R_LTS (reach\<^sub>t \<Sigma> (delta\<^sub>C \<Sigma>) (initial\<^sub>C \<phi>)) (initial\<^sub>C \<phi>) (({t. M_fin\<^sub>C \<phi> (mapping.Mapping \<pi>) t} \<union> {t. \<exists>\<chi>\<in>dom \<pi>. Acc_fin\<^sub>C \<Sigma> (mapping.Mapping \<pi>) \<chi> t}) \<inter> reach\<^sub>t \<Sigma> (delta\<^sub>C \<Sigma>) (initial\<^sub>C \<phi>), (\<lambda>I. I \<inter> reach\<^sub>t \<Sigma> (delta\<^sub>C \<Sigma>) (initial\<^sub>C \<phi>)) ` {{t. Acc_inf\<^sub>C (mapping.Mapping \<pi>) \<chi> t} |\<chi>. \<chi> \<in> dom \<pi>}) w

goal (2 subgoals):
 1. accept\<^sub>G\<^sub>R (\<A> \<Sigma> \<phi>) w \<Longrightarrow> accept\<^sub>G\<^sub>R_LTS (ltl_to_generalized_rabin\<^sub>C \<Sigma>' \<phi>) w
 2. accept\<^sub>G\<^sub>R_LTS (ltl_to_generalized_rabin\<^sub>C \<Sigma>' \<phi>) w \<Longrightarrow> accept\<^sub>G\<^sub>R (\<A> \<Sigma> \<phi>) w
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
accepting_pair\<^sub>G\<^sub>R (delta \<Sigma>) (initial \<phi>) (M_fin \<pi> \<union> \<Union> {Acc_fin \<Sigma> \<pi> \<chi> |\<chi>. \<chi> \<in> dom \<pi>}, {Acc_inf \<pi> \<chi> |\<chi>. \<chi> \<in> dom \<pi>}) w = accepting_pair\<^sub>G\<^sub>R_LTS (reach\<^sub>t \<Sigma> (delta\<^sub>C \<Sigma>) (initial\<^sub>C \<phi>)) (initial\<^sub>C \<phi>) (({t. M_fin\<^sub>C \<phi> (mapping.Mapping \<pi>) t} \<union> {t. \<exists>\<chi>\<in>dom \<pi>. Acc_fin\<^sub>C \<Sigma> (mapping.Mapping \<pi>) \<chi> t}) \<inter> reach\<^sub>t \<Sigma> (delta\<^sub>C \<Sigma>) (initial\<^sub>C \<phi>), (\<lambda>I. I \<inter> reach\<^sub>t \<Sigma> (delta\<^sub>C \<Sigma>) (initial\<^sub>C \<phi>)) ` {{t. Acc_inf\<^sub>C (mapping.Mapping \<pi>) \<chi> t} |\<chi>. \<chi> \<in> dom \<pi>}) w
[PROOF STEP]
have "?l \<longleftrightarrow> ?r"
[PROOF STATE]
proof (prove)
using this:
accepting_pair\<^sub>G\<^sub>R (delta \<Sigma>) (initial \<phi>) (M_fin \<pi> \<union> \<Union> {Acc_fin \<Sigma> \<pi> \<chi> |\<chi>. \<chi> \<in> dom \<pi>}, {Acc_inf \<pi> \<chi> |\<chi>. \<chi> \<in> dom \<pi>}) w = accepting_pair\<^sub>G\<^sub>R_LTS (reach\<^sub>t \<Sigma> (delta\<^sub>C \<Sigma>) (initial\<^sub>C \<phi>)) (initial\<^sub>C \<phi>) (({t. M_fin\<^sub>C \<phi> (mapping.Mapping \<pi>) t} \<union> {t. \<exists>\<chi>\<in>dom \<pi>. Acc_fin\<^sub>C \<Sigma> (mapping.Mapping \<pi>) \<chi> t}) \<inter> reach\<^sub>t \<Sigma> (delta\<^sub>C \<Sigma>) (initial\<^sub>C \<phi>), (\<lambda>I. I \<inter> reach\<^sub>t \<Sigma> (delta\<^sub>C \<Sigma>) (initial\<^sub>C \<phi>)) ` {{t. Acc_inf\<^sub>C (mapping.Mapping \<pi>) \<chi> t} |\<chi>. \<chi> \<in> dom \<pi>}) w

goal (1 subgoal):
 1. accepting_pair\<^sub>G\<^sub>R (delta \<Sigma>) (initial \<phi>) (M_fin \<pi> \<union> \<Union> {Acc_fin \<Sigma> \<pi> \<chi> |\<chi>. \<chi> \<in> dom \<pi>}, {Acc_inf \<pi> \<chi> |\<chi>. \<chi> \<in> dom \<pi>}) w = accepting_pair\<^sub>G\<^sub>R_LTS (reach\<^sub>t \<Sigma> (delta\<^sub>C \<Sigma>) (initial\<^sub>C \<phi>)) (initial\<^sub>C \<phi>) (({t. M_fin\<^sub>C \<phi> (mapping.Mapping \<pi>) t} \<union> {t. \<exists>\<chi>\<in>dom \<pi>. Acc_fin\<^sub>C \<Sigma> (mapping.Mapping \<pi>) \<chi> t}) \<inter> reach\<^sub>t \<Sigma> (delta\<^sub>C \<Sigma>) (initial\<^sub>C \<phi>), (\<lambda>I. I \<inter> reach\<^sub>t \<Sigma> (delta\<^sub>C \<Sigma>) (initial\<^sub>C \<phi>)) ` {{t. Acc_inf\<^sub>C (mapping.Mapping \<pi>) \<chi> t} |\<chi>. \<chi> \<in> dom \<pi>}) w
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
accepting_pair\<^sub>G\<^sub>R (delta \<Sigma>) (initial \<phi>) (M_fin \<pi> \<union> \<Union> {Acc_fin \<Sigma> \<pi> \<chi> |\<chi>. \<chi> \<in> dom \<pi>}, {Acc_inf \<pi> \<chi> |\<chi>. \<chi> \<in> dom \<pi>}) w = accepting_pair\<^sub>G\<^sub>R_LTS (reach\<^sub>t \<Sigma> (delta\<^sub>C \<Sigma>) (initial\<^sub>C \<phi>)) (initial\<^sub>C \<phi>) (({t. M_fin\<^sub>C \<phi> (mapping.Mapping \<pi>) t} \<union> {t. \<exists>\<chi>\<in>dom \<pi>. Acc_fin\<^sub>C \<Sigma> (mapping.Mapping \<pi>) \<chi> t}) \<inter> reach\<^sub>t \<Sigma> (delta\<^sub>C \<Sigma>) (initial\<^sub>C \<phi>), (\<lambda>I. I \<inter> reach\<^sub>t \<Sigma> (delta\<^sub>C \<Sigma>) (initial\<^sub>C \<phi>)) ` {{t. Acc_inf\<^sub>C (mapping.Mapping \<pi>) \<chi> t} |\<chi>. \<chi> \<in> dom \<pi>}) w

goal (2 subgoals):
 1. accept\<^sub>G\<^sub>R (\<A> \<Sigma> \<phi>) w \<Longrightarrow> accept\<^sub>G\<^sub>R_LTS (ltl_to_generalized_rabin\<^sub>C \<Sigma>' \<phi>) w
 2. accept\<^sub>G\<^sub>R_LTS (ltl_to_generalized_rabin\<^sub>C \<Sigma>' \<phi>) w \<Longrightarrow> accept\<^sub>G\<^sub>R (\<A> \<Sigma> \<phi>) w
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
dom ?\<pi>19 \<subseteq> \<^bold>G \<phi> \<Longrightarrow> accepting_pair\<^sub>G\<^sub>R (delta \<Sigma>) (initial \<phi>) (M_fin ?\<pi>19 \<union> \<Union> {Acc_fin \<Sigma> ?\<pi>19 \<chi> |\<chi>. \<chi> \<in> dom ?\<pi>19}, {Acc_inf ?\<pi>19 \<chi> |\<chi>. \<chi> \<in> dom ?\<pi>19}) w = accepting_pair\<^sub>G\<^sub>R_LTS (reach\<^sub>t \<Sigma> (delta\<^sub>C \<Sigma>) (initial\<^sub>C \<phi>)) (initial\<^sub>C \<phi>) (({t. M_fin\<^sub>C \<phi> (mapping.Mapping ?\<pi>19) t} \<union> {t. \<exists>\<chi>\<in>dom ?\<pi>19. Acc_fin\<^sub>C \<Sigma> (mapping.Mapping ?\<pi>19) \<chi> t}) \<inter> reach\<^sub>t \<Sigma> (delta\<^sub>C \<Sigma>) (initial\<^sub>C \<phi>), (\<lambda>I. I \<inter> reach\<^sub>t \<Sigma> (delta\<^sub>C \<Sigma>) (initial\<^sub>C \<phi>)) ` {{t. Acc_inf\<^sub>C (mapping.Mapping ?\<pi>19) \<chi> t} |\<chi>. \<chi> \<in> dom ?\<pi>19}) w

goal (2 subgoals):
 1. accept\<^sub>G\<^sub>R (\<A> \<Sigma> \<phi>) w \<Longrightarrow> accept\<^sub>G\<^sub>R_LTS (ltl_to_generalized_rabin\<^sub>C \<Sigma>' \<phi>) w
 2. accept\<^sub>G\<^sub>R_LTS (ltl_to_generalized_rabin\<^sub>C \<Sigma>' \<phi>) w \<Longrightarrow> accept\<^sub>G\<^sub>R (\<A> \<Sigma> \<phi>) w
[PROOF STEP]
note X = this
[PROOF STATE]
proof (state)
this:
dom ?\<pi>19 \<subseteq> \<^bold>G \<phi> \<Longrightarrow> accepting_pair\<^sub>G\<^sub>R (delta \<Sigma>) (initial \<phi>) (M_fin ?\<pi>19 \<union> \<Union> {Acc_fin \<Sigma> ?\<pi>19 \<chi> |\<chi>. \<chi> \<in> dom ?\<pi>19}, {Acc_inf ?\<pi>19 \<chi> |\<chi>. \<chi> \<in> dom ?\<pi>19}) w = accepting_pair\<^sub>G\<^sub>R_LTS (reach\<^sub>t \<Sigma> (delta\<^sub>C \<Sigma>) (initial\<^sub>C \<phi>)) (initial\<^sub>C \<phi>) (({t. M_fin\<^sub>C \<phi> (mapping.Mapping ?\<pi>19) t} \<union> {t. \<exists>\<chi>\<in>dom ?\<pi>19. Acc_fin\<^sub>C \<Sigma> (mapping.Mapping ?\<pi>19) \<chi> t}) \<inter> reach\<^sub>t \<Sigma> (delta\<^sub>C \<Sigma>) (initial\<^sub>C \<phi>), (\<lambda>I. I \<inter> reach\<^sub>t \<Sigma> (delta\<^sub>C \<Sigma>) (initial\<^sub>C \<phi>)) ` {{t. Acc_inf\<^sub>C (mapping.Mapping ?\<pi>19) \<chi> t} |\<chi>. \<chi> \<in> dom ?\<pi>19}) w

goal (2 subgoals):
 1. accept\<^sub>G\<^sub>R (\<A> \<Sigma> \<phi>) w \<Longrightarrow> accept\<^sub>G\<^sub>R_LTS (ltl_to_generalized_rabin\<^sub>C \<Sigma>' \<phi>) w
 2. accept\<^sub>G\<^sub>R_LTS (ltl_to_generalized_rabin\<^sub>C \<Sigma>' \<phi>) w \<Longrightarrow> accept\<^sub>G\<^sub>R (\<A> \<Sigma> \<phi>) w
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
dom ?\<pi>19 \<subseteq> \<^bold>G \<phi> \<Longrightarrow> accepting_pair\<^sub>G\<^sub>R (delta \<Sigma>) (initial \<phi>) (M_fin ?\<pi>19 \<union> \<Union> {Acc_fin \<Sigma> ?\<pi>19 \<chi> |\<chi>. \<chi> \<in> dom ?\<pi>19}, {Acc_inf ?\<pi>19 \<chi> |\<chi>. \<chi> \<in> dom ?\<pi>19}) w = accepting_pair\<^sub>G\<^sub>R_LTS (reach\<^sub>t \<Sigma> (delta\<^sub>C \<Sigma>) (initial\<^sub>C \<phi>)) (initial\<^sub>C \<phi>) (({t. M_fin\<^sub>C \<phi> (mapping.Mapping ?\<pi>19) t} \<union> {t. \<exists>\<chi>\<in>dom ?\<pi>19. Acc_fin\<^sub>C \<Sigma> (mapping.Mapping ?\<pi>19) \<chi> t}) \<inter> reach\<^sub>t \<Sigma> (delta\<^sub>C \<Sigma>) (initial\<^sub>C \<phi>), (\<lambda>I. I \<inter> reach\<^sub>t \<Sigma> (delta\<^sub>C \<Sigma>) (initial\<^sub>C \<phi>)) ` {{t. Acc_inf\<^sub>C (mapping.Mapping ?\<pi>19) \<chi> t} |\<chi>. \<chi> \<in> dom ?\<pi>19}) w

goal (2 subgoals):
 1. accept\<^sub>G\<^sub>R (\<A> \<Sigma> \<phi>) w \<Longrightarrow> accept\<^sub>G\<^sub>R_LTS (ltl_to_generalized_rabin\<^sub>C \<Sigma>' \<phi>) w
 2. accept\<^sub>G\<^sub>R_LTS (ltl_to_generalized_rabin\<^sub>C \<Sigma>' \<phi>) w \<Longrightarrow> accept\<^sub>G\<^sub>R (\<A> \<Sigma> \<phi>) w
[PROOF STEP]
assume ?lhs
[PROOF STATE]
proof (state)
this:
accept\<^sub>G\<^sub>R (\<A> \<Sigma> \<phi>) w

goal (2 subgoals):
 1. accept\<^sub>G\<^sub>R (\<A> \<Sigma> \<phi>) w \<Longrightarrow> accept\<^sub>G\<^sub>R_LTS (ltl_to_generalized_rabin\<^sub>C \<Sigma>' \<phi>) w
 2. accept\<^sub>G\<^sub>R_LTS (ltl_to_generalized_rabin\<^sub>C \<Sigma>' \<phi>) w \<Longrightarrow> accept\<^sub>G\<^sub>R (\<A> \<Sigma> \<phi>) w
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
accept\<^sub>G\<^sub>R (\<A> \<Sigma> \<phi>) w
[PROOF STEP]
obtain \<pi> where 1: "dom \<pi> \<subseteq> \<^bold>G \<phi>"
      and 2: "\<And>\<chi>. \<chi> \<in> dom \<pi> \<Longrightarrow> the (\<pi> \<chi>) < max_rank_of \<Sigma> \<chi>"
      and 3: "accepting_pair\<^sub>G\<^sub>R (delta \<Sigma>) (initial \<phi>) (M_fin \<pi> \<union> \<Union>{Acc_fin \<Sigma> \<pi> \<chi> |\<chi>. \<chi> \<in> dom \<pi>}, {Acc_inf \<pi> \<chi> |\<chi>. \<chi> \<in> dom \<pi>}) w"
[PROOF STATE]
proof (prove)
using this:
accept\<^sub>G\<^sub>R (\<A> \<Sigma> \<phi>) w

goal (1 subgoal):
 1. (\<And>\<pi>. \<lbrakk>dom \<pi> \<subseteq> \<^bold>G \<phi>; \<And>\<chi>. \<chi> \<in> dom \<pi> \<Longrightarrow> the (\<pi> \<chi>) < max_rank_of \<Sigma> \<chi>; accepting_pair\<^sub>G\<^sub>R (delta \<Sigma>) (initial \<phi>) (M_fin \<pi> \<union> \<Union> {Acc_fin \<Sigma> \<pi> \<chi> |\<chi>. \<chi> \<in> dom \<pi>}, {Acc_inf \<pi> \<chi> |\<chi>. \<chi> \<in> dom \<pi>}) w\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
dom \<pi> \<subseteq> \<^bold>G \<phi>
?\<chi>17 \<in> dom \<pi> \<Longrightarrow> the (\<pi> ?\<chi>17) < max_rank_of \<Sigma> ?\<chi>17
accepting_pair\<^sub>G\<^sub>R (delta \<Sigma>) (initial \<phi>) (M_fin \<pi> \<union> \<Union> {Acc_fin \<Sigma> \<pi> \<chi> |\<chi>. \<chi> \<in> dom \<pi>}, {Acc_inf \<pi> \<chi> |\<chi>. \<chi> \<in> dom \<pi>}) w

goal (2 subgoals):
 1. accept\<^sub>G\<^sub>R (\<A> \<Sigma> \<phi>) w \<Longrightarrow> accept\<^sub>G\<^sub>R_LTS (ltl_to_generalized_rabin\<^sub>C \<Sigma>' \<phi>) w
 2. accept\<^sub>G\<^sub>R_LTS (ltl_to_generalized_rabin\<^sub>C \<Sigma>' \<phi>) w \<Longrightarrow> accept\<^sub>G\<^sub>R (\<A> \<Sigma> \<phi>) w
[PROOF STEP]
define \<pi>' where "\<pi>' = Mapping.Mapping \<pi>"
[PROOF STATE]
proof (state)
this:
\<pi>' = mapping.Mapping \<pi>

goal (2 subgoals):
 1. accept\<^sub>G\<^sub>R (\<A> \<Sigma> \<phi>) w \<Longrightarrow> accept\<^sub>G\<^sub>R_LTS (ltl_to_generalized_rabin\<^sub>C \<Sigma>' \<phi>) w
 2. accept\<^sub>G\<^sub>R_LTS (ltl_to_generalized_rabin\<^sub>C \<Sigma>' \<phi>) w \<Longrightarrow> accept\<^sub>G\<^sub>R (\<A> \<Sigma> \<phi>) w
[PROOF STEP]
have "dom \<pi> = Mapping.keys \<pi>'" and "\<pi> = Mapping.lookup \<pi>'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dom \<pi> = Mapping.keys \<pi>' &&& \<pi> = Mapping.lookup \<pi>'
[PROOF STEP]
by (simp_all add: keys.abs_eq lookup.abs_eq \<pi>'_def)
[PROOF STATE]
proof (state)
this:
dom \<pi> = Mapping.keys \<pi>'
\<pi> = Mapping.lookup \<pi>'

goal (2 subgoals):
 1. accept\<^sub>G\<^sub>R (\<A> \<Sigma> \<phi>) w \<Longrightarrow> accept\<^sub>G\<^sub>R_LTS (ltl_to_generalized_rabin\<^sub>C \<Sigma>' \<phi>) w
 2. accept\<^sub>G\<^sub>R_LTS (ltl_to_generalized_rabin\<^sub>C \<Sigma>' \<phi>) w \<Longrightarrow> accept\<^sub>G\<^sub>R (\<A> \<Sigma> \<phi>) w
[PROOF STEP]
have acc_pair_LTS: "accepting_pair\<^sub>G\<^sub>R_LTS ?reach\<^sub>C ?q\<^sub>0\<^sub>C (({t. M_fin\<^sub>C \<phi> \<pi>' t} \<union> {t. \<exists>\<chi> \<in> Mapping.keys \<pi>'. Acc_fin\<^sub>C \<Sigma> \<pi>' \<chi> t}) \<inter> ?reach\<^sub>C,
        (\<lambda>I. I \<inter> ?reach\<^sub>C) ` {{t. Acc_inf\<^sub>C \<pi>' \<chi> t} | \<chi>. \<chi> \<in> Mapping.keys \<pi>'}) w"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. accepting_pair\<^sub>G\<^sub>R_LTS (reach\<^sub>t \<Sigma> (delta\<^sub>C \<Sigma>) (initial\<^sub>C \<phi>)) (initial\<^sub>C \<phi>) (({t. M_fin\<^sub>C \<phi> \<pi>' t} \<union> {t. \<exists>\<chi>\<in>Mapping.keys \<pi>'. Acc_fin\<^sub>C \<Sigma> \<pi>' \<chi> t}) \<inter> reach\<^sub>t \<Sigma> (delta\<^sub>C \<Sigma>) (initial\<^sub>C \<phi>), (\<lambda>I. I \<inter> reach\<^sub>t \<Sigma> (delta\<^sub>C \<Sigma>) (initial\<^sub>C \<phi>)) ` {{t. Acc_inf\<^sub>C \<pi>' \<chi> t} |\<chi>. \<chi> \<in> Mapping.keys \<pi>'}) w
[PROOF STEP]
using 3
[PROOF STATE]
proof (prove)
using this:
accepting_pair\<^sub>G\<^sub>R (delta \<Sigma>) (initial \<phi>) (M_fin \<pi> \<union> \<Union> {Acc_fin \<Sigma> \<pi> \<chi> |\<chi>. \<chi> \<in> dom \<pi>}, {Acc_inf \<pi> \<chi> |\<chi>. \<chi> \<in> dom \<pi>}) w

goal (1 subgoal):
 1. accepting_pair\<^sub>G\<^sub>R_LTS (reach\<^sub>t \<Sigma> (delta\<^sub>C \<Sigma>) (initial\<^sub>C \<phi>)) (initial\<^sub>C \<phi>) (({t. M_fin\<^sub>C \<phi> \<pi>' t} \<union> {t. \<exists>\<chi>\<in>Mapping.keys \<pi>'. Acc_fin\<^sub>C \<Sigma> \<pi>' \<chi> t}) \<inter> reach\<^sub>t \<Sigma> (delta\<^sub>C \<Sigma>) (initial\<^sub>C \<phi>), (\<lambda>I. I \<inter> reach\<^sub>t \<Sigma> (delta\<^sub>C \<Sigma>) (initial\<^sub>C \<phi>)) ` {{t. Acc_inf\<^sub>C \<pi>' \<chi> t} |\<chi>. \<chi> \<in> Mapping.keys \<pi>'}) w
[PROOF STEP]
unfolding X[OF 1]
[PROOF STATE]
proof (prove)
using this:
accepting_pair\<^sub>G\<^sub>R_LTS (reach\<^sub>t \<Sigma> (delta\<^sub>C \<Sigma>) (initial\<^sub>C \<phi>)) (initial\<^sub>C \<phi>) ((Collect (M_fin\<^sub>C \<phi> (mapping.Mapping \<pi>)) \<union> {t. \<exists>\<chi>\<in>dom \<pi>. Acc_fin\<^sub>C \<Sigma> (mapping.Mapping \<pi>) \<chi> t}) \<inter> reach\<^sub>t \<Sigma> (delta\<^sub>C \<Sigma>) (initial\<^sub>C \<phi>), (\<lambda>I. I \<inter> reach\<^sub>t \<Sigma> (delta\<^sub>C \<Sigma>) (initial\<^sub>C \<phi>)) ` {Collect (Acc_inf\<^sub>C (mapping.Mapping \<pi>) \<chi>) |\<chi>. \<chi> \<in> dom \<pi>}) w

goal (1 subgoal):
 1. accepting_pair\<^sub>G\<^sub>R_LTS (reach\<^sub>t \<Sigma> (delta\<^sub>C \<Sigma>) (initial\<^sub>C \<phi>)) (initial\<^sub>C \<phi>) (({t. M_fin\<^sub>C \<phi> \<pi>' t} \<union> {t. \<exists>\<chi>\<in>Mapping.keys \<pi>'. Acc_fin\<^sub>C \<Sigma> \<pi>' \<chi> t}) \<inter> reach\<^sub>t \<Sigma> (delta\<^sub>C \<Sigma>) (initial\<^sub>C \<phi>), (\<lambda>I. I \<inter> reach\<^sub>t \<Sigma> (delta\<^sub>C \<Sigma>) (initial\<^sub>C \<phi>)) ` {{t. Acc_inf\<^sub>C \<pi>' \<chi> t} |\<chi>. \<chi> \<in> Mapping.keys \<pi>'}) w
[PROOF STEP]
unfolding \<open>dom \<pi> = Mapping.keys \<pi>'\<close> \<pi>'_def[symmetric]
[PROOF STATE]
proof (prove)
using this:
accepting_pair\<^sub>G\<^sub>R_LTS (reach\<^sub>t \<Sigma> (delta\<^sub>C \<Sigma>) (initial\<^sub>C \<phi>)) (initial\<^sub>C \<phi>) ((Collect (M_fin\<^sub>C \<phi> \<pi>') \<union> {t. \<exists>\<chi>\<in>Mapping.keys \<pi>'. Acc_fin\<^sub>C \<Sigma> \<pi>' \<chi> t}) \<inter> reach\<^sub>t \<Sigma> (delta\<^sub>C \<Sigma>) (initial\<^sub>C \<phi>), (\<lambda>I. I \<inter> reach\<^sub>t \<Sigma> (delta\<^sub>C \<Sigma>) (initial\<^sub>C \<phi>)) ` {Collect (Acc_inf\<^sub>C \<pi>' \<chi>) |\<chi>. \<chi> \<in> Mapping.keys \<pi>'}) w

goal (1 subgoal):
 1. accepting_pair\<^sub>G\<^sub>R_LTS (reach\<^sub>t \<Sigma> (delta\<^sub>C \<Sigma>) (initial\<^sub>C \<phi>)) (initial\<^sub>C \<phi>) (({t. M_fin\<^sub>C \<phi> \<pi>' t} \<union> {t. \<exists>\<chi>\<in>Mapping.keys \<pi>'. Acc_fin\<^sub>C \<Sigma> \<pi>' \<chi> t}) \<inter> reach\<^sub>t \<Sigma> (delta\<^sub>C \<Sigma>) (initial\<^sub>C \<phi>), (\<lambda>I. I \<inter> reach\<^sub>t \<Sigma> (delta\<^sub>C \<Sigma>) (initial\<^sub>C \<phi>)) ` {{t. Acc_inf\<^sub>C \<pi>' \<chi> t} |\<chi>. \<chi> \<in> Mapping.keys \<pi>'}) w
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
accepting_pair\<^sub>G\<^sub>R_LTS (reach\<^sub>t \<Sigma> (delta\<^sub>C \<Sigma>) (initial\<^sub>C \<phi>)) (initial\<^sub>C \<phi>) (({t. M_fin\<^sub>C \<phi> \<pi>' t} \<union> {t. \<exists>\<chi>\<in>Mapping.keys \<pi>'. Acc_fin\<^sub>C \<Sigma> \<pi>' \<chi> t}) \<inter> reach\<^sub>t \<Sigma> (delta\<^sub>C \<Sigma>) (initial\<^sub>C \<phi>), (\<lambda>I. I \<inter> reach\<^sub>t \<Sigma> (delta\<^sub>C \<Sigma>) (initial\<^sub>C \<phi>)) ` {{t. Acc_inf\<^sub>C \<pi>' \<chi> t} |\<chi>. \<chi> \<in> Mapping.keys \<pi>'}) w

goal (2 subgoals):
 1. accept\<^sub>G\<^sub>R (\<A> \<Sigma> \<phi>) w \<Longrightarrow> accept\<^sub>G\<^sub>R_LTS (ltl_to_generalized_rabin\<^sub>C \<Sigma>' \<phi>) w
 2. accept\<^sub>G\<^sub>R_LTS (ltl_to_generalized_rabin\<^sub>C \<Sigma>' \<phi>) w \<Longrightarrow> accept\<^sub>G\<^sub>R (\<A> \<Sigma> \<phi>) w
[PROOF STEP]
show ?rhs
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. accept\<^sub>G\<^sub>R_LTS (ltl_to_generalized_rabin\<^sub>C \<Sigma>' \<phi>) w
[PROOF STEP]
apply (unfold ltl_to_generalized_rabin\<^sub>C.simps Let_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. accept\<^sub>G\<^sub>R_LTS (reachable_transitions\<^sub>C \<Sigma>' \<phi>, initial\<^sub>C \<phi>, (\<lambda>\<pi>. (Set.filter (\<lambda>t. M_fin\<^sub>C \<phi> \<pi> t \<or> (\<exists>\<chi>\<in>Mapping.keys \<pi>. Acc_fin\<^sub>C (set \<Sigma>') \<pi> \<chi> t)) (reachable_transitions\<^sub>C \<Sigma>' \<phi>), (\<lambda>\<chi>. Set.filter (Acc_inf\<^sub>C \<pi> \<chi>) (reachable_transitions\<^sub>C \<Sigma>' \<phi>)) ` Mapping.keys \<pi>)) ` mappings\<^sub>C \<Sigma>' \<phi>) w
[PROOF STEP]
apply (intro accept\<^sub>G\<^sub>R_LTS_I)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. accepting_pair\<^sub>G\<^sub>R_LTS (reachable_transitions\<^sub>C \<Sigma>' \<phi>) (initial\<^sub>C \<phi>) (?F, ?\<I>) w
 2. (?F, ?\<I>) \<in> (\<lambda>\<pi>. (Set.filter (\<lambda>t. M_fin\<^sub>C \<phi> \<pi> t \<or> (\<exists>\<chi>\<in>Mapping.keys \<pi>. Acc_fin\<^sub>C (set \<Sigma>') \<pi> \<chi> t)) (reachable_transitions\<^sub>C \<Sigma>' \<phi>), (\<lambda>\<chi>. Set.filter (Acc_inf\<^sub>C \<pi> \<chi>) (reachable_transitions\<^sub>C \<Sigma>' \<phi>)) ` Mapping.keys \<pi>)) ` mappings\<^sub>C \<Sigma>' \<phi>
[PROOF STEP]
apply (insert acc_pair_LTS; auto simp add: assms[symmetric] mappings\<^sub>C_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (({t. M_fin\<^sub>C \<phi> \<pi>' t} \<union> {t. \<exists>\<chi>\<in>Mapping.keys \<pi>'. Acc_fin\<^sub>C \<Sigma> \<pi>' \<chi> t}) \<inter> reach\<^sub>t \<Sigma> (\<lambda>(q\<^sub>1, q\<^sub>2) \<nu>. (\<delta> q\<^sub>1 \<nu>, \<up>\<Delta>\<^sub>\<times> (nxt \<Sigma> \<delta>\<^sub>M \<circ> q\<^sub>0\<^sub>M \<circ> theG) q\<^sub>2 \<nu>)) (q\<^sub>0 \<phi>, Mapping.tabulate (G_list \<phi>) (init \<circ> q\<^sub>0\<^sub>M \<circ> theG)), (\<lambda>x. x \<inter> reach\<^sub>t \<Sigma> (\<lambda>(q\<^sub>1, q\<^sub>2) \<nu>. (\<delta> q\<^sub>1 \<nu>, \<up>\<Delta>\<^sub>\<times> (nxt \<Sigma> \<delta>\<^sub>M \<circ> q\<^sub>0\<^sub>M \<circ> theG) q\<^sub>2 \<nu>)) (q\<^sub>0 \<phi>, Mapping.tabulate (G_list \<phi>) (init \<circ> q\<^sub>0\<^sub>M \<circ> theG))) ` {{t. Acc_inf\<^sub>C \<pi>' \<chi> t} |\<chi>. \<chi> \<in> Mapping.keys \<pi>'}) \<in> (\<lambda>\<pi>. (Set.filter (\<lambda>t. M_fin\<^sub>C \<phi> \<pi> t \<or> (\<exists>\<chi>\<in>Mapping.keys \<pi>. Acc_fin\<^sub>C (set \<Sigma>') \<pi> \<chi> t)) (reachable_transitions\<^sub>C \<Sigma>' \<phi>), (\<lambda>\<chi>. Set.filter (Acc_inf\<^sub>C \<pi> \<chi>) (reachable_transitions\<^sub>C \<Sigma>' \<phi>)) ` Mapping.keys \<pi>)) ` mappings\<^sub>C \<Sigma>' \<phi>
[PROOF STEP]
apply (insert 1 2; unfold  \<open>dom \<pi> = Mapping.keys \<pi>'\<close>; unfold \<open>\<pi> = Mapping.lookup \<pi>'\<close>)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Mapping.keys \<pi>' \<subseteq> \<^bold>G \<phi>; \<And>\<chi>. \<chi> \<in> Mapping.keys \<pi>' \<Longrightarrow> the (Mapping.lookup \<pi>' \<chi>) < max_rank_of \<Sigma> \<chi>\<rbrakk> \<Longrightarrow> (({t. M_fin\<^sub>C \<phi> \<pi>' t} \<union> {t. \<exists>\<chi>\<in>Mapping.keys \<pi>'. Acc_fin\<^sub>C \<Sigma> \<pi>' \<chi> t}) \<inter> reach\<^sub>t \<Sigma> (\<lambda>(q\<^sub>1, q\<^sub>2) \<nu>. (\<delta> q\<^sub>1 \<nu>, \<up>\<Delta>\<^sub>\<times> (nxt \<Sigma> \<delta>\<^sub>M \<circ> q\<^sub>0\<^sub>M \<circ> theG) q\<^sub>2 \<nu>)) (q\<^sub>0 \<phi>, Mapping.tabulate (G_list \<phi>) (init \<circ> q\<^sub>0\<^sub>M \<circ> theG)), (\<lambda>x. x \<inter> reach\<^sub>t \<Sigma> (\<lambda>(q\<^sub>1, q\<^sub>2) \<nu>. (\<delta> q\<^sub>1 \<nu>, \<up>\<Delta>\<^sub>\<times> (nxt \<Sigma> \<delta>\<^sub>M \<circ> q\<^sub>0\<^sub>M \<circ> theG) q\<^sub>2 \<nu>)) (q\<^sub>0 \<phi>, Mapping.tabulate (G_list \<phi>) (init \<circ> q\<^sub>0\<^sub>M \<circ> theG))) ` {{t. Acc_inf\<^sub>C \<pi>' \<chi> t} |\<chi>. \<chi> \<in> Mapping.keys \<pi>'}) \<in> (\<lambda>\<pi>. (Set.filter (\<lambda>t. M_fin\<^sub>C \<phi> \<pi> t \<or> (\<exists>\<chi>\<in>Mapping.keys \<pi>. Acc_fin\<^sub>C (set \<Sigma>') \<pi> \<chi> t)) (reachable_transitions\<^sub>C \<Sigma>' \<phi>), (\<lambda>\<chi>. Set.filter (Acc_inf\<^sub>C \<pi> \<chi>) (reachable_transitions\<^sub>C \<Sigma>' \<phi>)) ` Mapping.keys \<pi>)) ` mappings\<^sub>C \<Sigma>' \<phi>
[PROOF STEP]
by (auto simp add: assms[symmetric] Set.filter_def image_def mappings\<^sub>C_def)
[PROOF STATE]
proof (state)
this:
accept\<^sub>G\<^sub>R_LTS (ltl_to_generalized_rabin\<^sub>C \<Sigma>' \<phi>) w

goal (1 subgoal):
 1. accept\<^sub>G\<^sub>R_LTS (ltl_to_generalized_rabin\<^sub>C \<Sigma>' \<phi>) w \<Longrightarrow> accept\<^sub>G\<^sub>R (\<A> \<Sigma> \<phi>) w
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
accept\<^sub>G\<^sub>R (\<A> \<Sigma> \<phi>) w \<Longrightarrow> accept\<^sub>G\<^sub>R_LTS (ltl_to_generalized_rabin\<^sub>C \<Sigma>' \<phi>) w

goal (1 subgoal):
 1. accept\<^sub>G\<^sub>R_LTS (ltl_to_generalized_rabin\<^sub>C \<Sigma>' \<phi>) w \<Longrightarrow> accept\<^sub>G\<^sub>R (\<A> \<Sigma> \<phi>) w
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
accept\<^sub>G\<^sub>R (\<A> \<Sigma> \<phi>) w \<Longrightarrow> accept\<^sub>G\<^sub>R_LTS (ltl_to_generalized_rabin\<^sub>C \<Sigma>' \<phi>) w

goal (1 subgoal):
 1. accept\<^sub>G\<^sub>R_LTS (ltl_to_generalized_rabin\<^sub>C \<Sigma>' \<phi>) w \<Longrightarrow> accept\<^sub>G\<^sub>R (\<A> \<Sigma> \<phi>) w
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
accept\<^sub>G\<^sub>R (\<A> \<Sigma> \<phi>) w \<Longrightarrow> accept\<^sub>G\<^sub>R_LTS (ltl_to_generalized_rabin\<^sub>C \<Sigma>' \<phi>) w

goal (1 subgoal):
 1. accept\<^sub>G\<^sub>R_LTS (ltl_to_generalized_rabin\<^sub>C \<Sigma>' \<phi>) w \<Longrightarrow> accept\<^sub>G\<^sub>R (\<A> \<Sigma> \<phi>) w
[PROOF STEP]
assume ?rhs
[PROOF STATE]
proof (state)
this:
accept\<^sub>G\<^sub>R_LTS (ltl_to_generalized_rabin\<^sub>C \<Sigma>' \<phi>) w

goal (1 subgoal):
 1. accept\<^sub>G\<^sub>R_LTS (ltl_to_generalized_rabin\<^sub>C \<Sigma>' \<phi>) w \<Longrightarrow> accept\<^sub>G\<^sub>R (\<A> \<Sigma> \<phi>) w
[PROOF STEP]
obtain Fin Inf where "(Fin, Inf) \<in> snd (snd (ltl_to_generalized_rabin\<^sub>C \<Sigma>' \<phi>))"
      and 4: "accepting_pair\<^sub>G\<^sub>R_LTS ?reach\<^sub>C (initial\<^sub>C \<phi>) (Fin, Inf) w"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>Fin Inf. \<lbrakk>(Fin, Inf) \<in> snd (snd (ltl_to_generalized_rabin\<^sub>C \<Sigma>' \<phi>)); accepting_pair\<^sub>G\<^sub>R_LTS (reach\<^sub>t \<Sigma> (delta\<^sub>C \<Sigma>) (initial\<^sub>C \<phi>)) (initial\<^sub>C \<phi>) (Fin, Inf) w\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using accept\<^sub>G\<^sub>R_LTS_E[OF \<open>?rhs\<close>]
[PROOF STATE]
proof (prove)
using this:
(\<And>F I. \<lbrakk>(F, I) \<in> snd (snd (ltl_to_generalized_rabin\<^sub>C \<Sigma>' \<phi>)); accepting_pair\<^sub>G\<^sub>R_LTS (fst (ltl_to_generalized_rabin\<^sub>C \<Sigma>' \<phi>)) (fst (snd (ltl_to_generalized_rabin\<^sub>C \<Sigma>' \<phi>))) (F, I) w\<rbrakk> \<Longrightarrow> ?thesis) \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. (\<And>Fin Inf. \<lbrakk>(Fin, Inf) \<in> snd (snd (ltl_to_generalized_rabin\<^sub>C \<Sigma>' \<phi>)); accepting_pair\<^sub>G\<^sub>R_LTS (reach\<^sub>t \<Sigma> (delta\<^sub>C \<Sigma>) (initial\<^sub>C \<phi>)) (initial\<^sub>C \<phi>) (Fin, Inf) w\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
apply (simp add: Let_def assms del: accept\<^sub>G\<^sub>R_LTS.simps)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>Fin Inf. \<lbrakk>(Fin, Inf) \<in> (\<lambda>x. (Set.filter (\<lambda>t. M_fin\<^sub>C \<phi> x t \<or> (\<exists>\<chi>\<in>Mapping.keys x. Acc_fin\<^sub>C (set \<Sigma>') x \<chi> t)) (reach\<^sub>t (set \<Sigma>') (\<lambda>(q\<^sub>1, q\<^sub>2) \<nu>. (\<delta> q\<^sub>1 \<nu>, \<up>\<Delta>\<^sub>\<times> (nxt (set \<Sigma>') \<delta>\<^sub>M \<circ> q\<^sub>0\<^sub>M \<circ> theG) q\<^sub>2 \<nu>)) (q\<^sub>0 \<phi>, Mapping.tabulate (G_list \<phi>) (init \<circ> q\<^sub>0\<^sub>M \<circ> theG))), (\<lambda>\<chi>. Set.filter (Acc_inf\<^sub>C x \<chi>) (reach\<^sub>t (set \<Sigma>') (\<lambda>(q\<^sub>1, q\<^sub>2) \<nu>. (\<delta> q\<^sub>1 \<nu>, \<up>\<Delta>\<^sub>\<times> (nxt (set \<Sigma>') \<delta>\<^sub>M \<circ> q\<^sub>0\<^sub>M \<circ> theG) q\<^sub>2 \<nu>)) (q\<^sub>0 \<phi>, Mapping.tabulate (G_list \<phi>) (init \<circ> q\<^sub>0\<^sub>M \<circ> theG)))) ` Mapping.keys x)) ` mappings\<^sub>C \<Sigma>' \<phi>; accepting_pair\<^sub>G\<^sub>R_LTS (reach\<^sub>t (set \<Sigma>') (\<lambda>(q\<^sub>1, q\<^sub>2) \<nu>. (\<delta> q\<^sub>1 \<nu>, \<up>\<Delta>\<^sub>\<times> (nxt (set \<Sigma>') \<delta>\<^sub>M \<circ> q\<^sub>0\<^sub>M \<circ> theG) q\<^sub>2 \<nu>)) (q\<^sub>0 \<phi>, Mapping.tabulate (G_list \<phi>) (init \<circ> q\<^sub>0\<^sub>M \<circ> theG))) (q\<^sub>0 \<phi>, Mapping.tabulate (G_list \<phi>) (init \<circ> q\<^sub>0\<^sub>M \<circ> theG)) (Fin, Inf) w\<rbrakk> \<Longrightarrow> thesis; \<And>thesis. (\<And>F I. \<lbrakk>(F, I) \<in> (\<lambda>x. (Set.filter (\<lambda>t. M_fin\<^sub>C \<phi> x t \<or> (\<exists>\<chi>\<in>Mapping.keys x. Acc_fin\<^sub>C (set \<Sigma>') x \<chi> t)) (reach\<^sub>t (set \<Sigma>') (\<lambda>(q\<^sub>1, q\<^sub>2) \<nu>. (\<delta> q\<^sub>1 \<nu>, \<up>\<Delta>\<^sub>\<times> (nxt (set \<Sigma>') \<delta>\<^sub>M \<circ> q\<^sub>0\<^sub>M \<circ> theG) q\<^sub>2 \<nu>)) (q\<^sub>0 \<phi>, Mapping.tabulate (G_list \<phi>) (init \<circ> q\<^sub>0\<^sub>M \<circ> theG))), (\<lambda>\<chi>. Set.filter (Acc_inf\<^sub>C x \<chi>) (reach\<^sub>t (set \<Sigma>') (\<lambda>(q\<^sub>1, q\<^sub>2) \<nu>. (\<delta> q\<^sub>1 \<nu>, \<up>\<Delta>\<^sub>\<times> (nxt (set \<Sigma>') \<delta>\<^sub>M \<circ> q\<^sub>0\<^sub>M \<circ> theG) q\<^sub>2 \<nu>)) (q\<^sub>0 \<phi>, Mapping.tabulate (G_list \<phi>) (init \<circ> q\<^sub>0\<^sub>M \<circ> theG)))) ` Mapping.keys x)) ` mappings\<^sub>C \<Sigma>' \<phi>; accepting_pair\<^sub>G\<^sub>R_LTS (reach\<^sub>t (set \<Sigma>') (\<lambda>(q\<^sub>1, q\<^sub>2) \<nu>. (\<delta> q\<^sub>1 \<nu>, \<up>\<Delta>\<^sub>\<times> (nxt (set \<Sigma>') \<delta>\<^sub>M \<circ> q\<^sub>0\<^sub>M \<circ> theG) q\<^sub>2 \<nu>)) (q\<^sub>0 \<phi>, Mapping.tabulate (G_list \<phi>) (init \<circ> q\<^sub>0\<^sub>M \<circ> theG))) (q\<^sub>0 \<phi>, Mapping.tabulate (G_list \<phi>) (init \<circ> q\<^sub>0\<^sub>M \<circ> theG)) (F, I) w\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(Fin, Inf) \<in> snd (snd (ltl_to_generalized_rabin\<^sub>C \<Sigma>' \<phi>))
accepting_pair\<^sub>G\<^sub>R_LTS (reach\<^sub>t \<Sigma> (delta\<^sub>C \<Sigma>) (initial\<^sub>C \<phi>)) (initial\<^sub>C \<phi>) (Fin, Inf) w

goal (1 subgoal):
 1. accept\<^sub>G\<^sub>R_LTS (ltl_to_generalized_rabin\<^sub>C \<Sigma>' \<phi>) w \<Longrightarrow> accept\<^sub>G\<^sub>R (\<A> \<Sigma> \<phi>) w
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(Fin, Inf) \<in> snd (snd (ltl_to_generalized_rabin\<^sub>C \<Sigma>' \<phi>))
accepting_pair\<^sub>G\<^sub>R_LTS (reach\<^sub>t \<Sigma> (delta\<^sub>C \<Sigma>) (initial\<^sub>C \<phi>)) (initial\<^sub>C \<phi>) (Fin, Inf) w
[PROOF STEP]
obtain \<pi> where Y: "(Fin, Inf) = (Set.filter (\<lambda>t. M_fin\<^sub>C \<phi> \<pi> t \<or> (\<exists>\<chi> \<in> Mapping.keys \<pi>. Acc_fin\<^sub>C \<Sigma> \<pi> \<chi> t)) ?reach\<^sub>C,
        (\<lambda>\<chi>. Set.filter (Acc_inf\<^sub>C \<pi> \<chi>) ?reach\<^sub>C) ` (Mapping.keys \<pi>))"
        and 1: "Mapping.keys \<pi> \<subseteq> \<^bold>G \<phi>" and 2: "\<And>\<chi>. \<chi> \<in> Mapping.keys \<pi> \<Longrightarrow> the (Mapping.lookup \<pi> \<chi>) < max_rank_of \<Sigma> \<chi>"
[PROOF STATE]
proof (prove)
using this:
(Fin, Inf) \<in> snd (snd (ltl_to_generalized_rabin\<^sub>C \<Sigma>' \<phi>))
accepting_pair\<^sub>G\<^sub>R_LTS (reach\<^sub>t \<Sigma> (delta\<^sub>C \<Sigma>) (initial\<^sub>C \<phi>)) (initial\<^sub>C \<phi>) (Fin, Inf) w

goal (1 subgoal):
 1. (\<And>\<pi>. \<lbrakk>(Fin, Inf) = (Set.filter (\<lambda>t. M_fin\<^sub>C \<phi> \<pi> t \<or> (\<exists>\<chi>\<in>Mapping.keys \<pi>. Acc_fin\<^sub>C \<Sigma> \<pi> \<chi> t)) (reach\<^sub>t \<Sigma> (delta\<^sub>C \<Sigma>) (initial\<^sub>C \<phi>)), (\<lambda>\<chi>. Set.filter (Acc_inf\<^sub>C \<pi> \<chi>) (reach\<^sub>t \<Sigma> (delta\<^sub>C \<Sigma>) (initial\<^sub>C \<phi>))) ` Mapping.keys \<pi>); Mapping.keys \<pi> \<subseteq> \<^bold>G \<phi>; \<And>\<chi>. \<chi> \<in> Mapping.keys \<pi> \<Longrightarrow> the (Mapping.lookup \<pi> \<chi>) < max_rank_of \<Sigma> \<chi>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding ltl_to_generalized_rabin\<^sub>C.simps Let_def fst_conv snd_conv mappings\<^sub>C_def assms reachable_transitions\<^sub>C_simp max_rank_of\<^sub>C_simp
[PROOF STATE]
proof (prove)
using this:
(Fin, Inf) \<in> (\<lambda>\<pi>. (Set.filter (\<lambda>t. M_fin\<^sub>C \<phi> \<pi> t \<or> (\<exists>\<chi>\<in>Mapping.keys \<pi>. Acc_fin\<^sub>C (set \<Sigma>') \<pi> \<chi> t)) (reach\<^sub>t (set \<Sigma>') (delta\<^sub>C (set \<Sigma>')) (initial\<^sub>C \<phi>)), (\<lambda>\<chi>. Set.filter (Acc_inf\<^sub>C \<pi> \<chi>) (reach\<^sub>t (set \<Sigma>') (delta\<^sub>C (set \<Sigma>')) (initial\<^sub>C \<phi>))) ` Mapping.keys \<pi>)) ` {\<pi>. Mapping.keys \<pi> \<subseteq> \<^bold>G \<phi> \<and> (\<forall>\<chi>\<in>Mapping.keys \<pi>. the (Mapping.lookup \<pi> \<chi>) < max_rank_of (set \<Sigma>') \<chi>)}
accepting_pair\<^sub>G\<^sub>R_LTS (reach\<^sub>t (set \<Sigma>') (delta\<^sub>C (set \<Sigma>')) (initial\<^sub>C \<phi>)) (initial\<^sub>C \<phi>) (Fin, Inf) w

goal (1 subgoal):
 1. (\<And>\<pi>. \<lbrakk>(Fin, Inf) = (Set.filter (\<lambda>t. M_fin\<^sub>C \<phi> \<pi> t \<or> (\<exists>\<chi>\<in>Mapping.keys \<pi>. Acc_fin\<^sub>C (set \<Sigma>') \<pi> \<chi> t)) (reach\<^sub>t (set \<Sigma>') (delta\<^sub>C (set \<Sigma>')) (initial\<^sub>C \<phi>)), (\<lambda>\<chi>. Set.filter (Acc_inf\<^sub>C \<pi> \<chi>) (reach\<^sub>t (set \<Sigma>') (delta\<^sub>C (set \<Sigma>')) (initial\<^sub>C \<phi>))) ` Mapping.keys \<pi>); Mapping.keys \<pi> \<subseteq> \<^bold>G \<phi>; \<And>\<chi>. \<chi> \<in> Mapping.keys \<pi> \<Longrightarrow> the (Mapping.lookup \<pi> \<chi>) < max_rank_of (set \<Sigma>') \<chi>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(Fin, Inf) = (Set.filter (\<lambda>t. M_fin\<^sub>C \<phi> \<pi> t \<or> (\<exists>\<chi>\<in>Mapping.keys \<pi>. Acc_fin\<^sub>C \<Sigma> \<pi> \<chi> t)) (reach\<^sub>t \<Sigma> (delta\<^sub>C \<Sigma>) (initial\<^sub>C \<phi>)), (\<lambda>\<chi>. Set.filter (Acc_inf\<^sub>C \<pi> \<chi>) (reach\<^sub>t \<Sigma> (delta\<^sub>C \<Sigma>) (initial\<^sub>C \<phi>))) ` Mapping.keys \<pi>)
Mapping.keys \<pi> \<subseteq> \<^bold>G \<phi>
?\<chi>17 \<in> Mapping.keys \<pi> \<Longrightarrow> the (Mapping.lookup \<pi> ?\<chi>17) < max_rank_of \<Sigma> ?\<chi>17

goal (1 subgoal):
 1. accept\<^sub>G\<^sub>R_LTS (ltl_to_generalized_rabin\<^sub>C \<Sigma>' \<phi>) w \<Longrightarrow> accept\<^sub>G\<^sub>R (\<A> \<Sigma> \<phi>) w
[PROOF STEP]
define \<pi>' where "\<pi>' = Mapping.rep \<pi>"
[PROOF STATE]
proof (state)
this:
\<pi>' = mapping.rep \<pi>

goal (1 subgoal):
 1. accept\<^sub>G\<^sub>R_LTS (ltl_to_generalized_rabin\<^sub>C \<Sigma>' \<phi>) w \<Longrightarrow> accept\<^sub>G\<^sub>R (\<A> \<Sigma> \<phi>) w
[PROOF STEP]
have "dom \<pi>' = Mapping.keys \<pi>" and "Mapping.Mapping \<pi>' = \<pi>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dom \<pi>' = Mapping.keys \<pi> &&& mapping.Mapping \<pi>' = \<pi>
[PROOF STEP]
by (simp_all add: \<pi>'_def mapping.rep_inverse keys.rep_eq)
[PROOF STATE]
proof (state)
this:
dom \<pi>' = Mapping.keys \<pi>
mapping.Mapping \<pi>' = \<pi>

goal (1 subgoal):
 1. accept\<^sub>G\<^sub>R_LTS (ltl_to_generalized_rabin\<^sub>C \<Sigma>' \<phi>) w \<Longrightarrow> accept\<^sub>G\<^sub>R (\<A> \<Sigma> \<phi>) w
[PROOF STEP]
have 1: "dom \<pi>' \<subseteq> \<^bold>G \<phi>" and 2: "\<And>\<chi>. \<chi> \<in> dom \<pi>' \<Longrightarrow> the (\<pi>' \<chi>) < max_rank_of \<Sigma> \<chi>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dom \<pi>' \<subseteq> \<^bold>G \<phi> &&& (\<And>\<chi>. \<chi> \<in> dom \<pi>' \<Longrightarrow> the (\<pi>' \<chi>) < max_rank_of \<Sigma> \<chi>)
[PROOF STEP]
using 1 2
[PROOF STATE]
proof (prove)
using this:
Mapping.keys \<pi> \<subseteq> \<^bold>G \<phi>
?\<chi>17 \<in> Mapping.keys \<pi> \<Longrightarrow> the (Mapping.lookup \<pi> ?\<chi>17) < max_rank_of \<Sigma> ?\<chi>17

goal (1 subgoal):
 1. dom \<pi>' \<subseteq> \<^bold>G \<phi> &&& (\<And>\<chi>. \<chi> \<in> dom \<pi>' \<Longrightarrow> the (\<pi>' \<chi>) < max_rank_of \<Sigma> \<chi>)
[PROOF STEP]
unfolding  \<pi>'_def Mapping.keys.rep_eq Mapping.mapping.rep_inverse
[PROOF STATE]
proof (prove)
using this:
dom (mapping.rep \<pi>) \<subseteq> \<^bold>G \<phi>
?\<chi>17 \<in> dom (mapping.rep \<pi>) \<Longrightarrow> the (Mapping.lookup \<pi> ?\<chi>17) < max_rank_of \<Sigma> ?\<chi>17

goal (1 subgoal):
 1. dom (mapping.rep \<pi>) \<subseteq> \<^bold>G \<phi> &&& (\<And>\<chi>. \<chi> \<in> dom (mapping.rep \<pi>) \<Longrightarrow> the (mapping.rep \<pi> \<chi>) < max_rank_of \<Sigma> \<chi>)
[PROOF STEP]
by (simp add: lookup.rep_eq)+
[PROOF STATE]
proof (state)
this:
dom \<pi>' \<subseteq> \<^bold>G \<phi>
?\<chi>17 \<in> dom \<pi>' \<Longrightarrow> the (\<pi>' ?\<chi>17) < max_rank_of \<Sigma> ?\<chi>17

goal (1 subgoal):
 1. accept\<^sub>G\<^sub>R_LTS (ltl_to_generalized_rabin\<^sub>C \<Sigma>' \<phi>) w \<Longrightarrow> accept\<^sub>G\<^sub>R (\<A> \<Sigma> \<phi>) w
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
dom \<pi>' \<subseteq> \<^bold>G \<phi>
?\<chi>17 \<in> dom \<pi>' \<Longrightarrow> the (\<pi>' ?\<chi>17) < max_rank_of \<Sigma> ?\<chi>17

goal (1 subgoal):
 1. accept\<^sub>G\<^sub>R_LTS (ltl_to_generalized_rabin\<^sub>C \<Sigma>' \<phi>) w \<Longrightarrow> accept\<^sub>G\<^sub>R (\<A> \<Sigma> \<phi>) w
[PROOF STEP]
have "({a \<in> reach\<^sub>t \<Sigma> (delta\<^sub>C \<Sigma>) (initial\<^sub>C \<phi>). M_fin\<^sub>C \<phi> \<pi> a \<or> (\<exists>\<chi>\<in>Mapping.keys \<pi>. Acc_fin\<^sub>C \<Sigma> \<pi> \<chi> a)}, {y. \<exists>x\<in>Mapping.keys \<pi>. y = {a \<in> reach\<^sub>t \<Sigma> (delta\<^sub>C \<Sigma>) (initial\<^sub>C \<phi>). Acc_inf\<^sub>C \<pi> x a}})
      = ((Collect (M_fin\<^sub>C \<phi> \<pi>) \<union> {t. \<exists>\<chi>\<in>Mapping.keys \<pi>. Acc_fin\<^sub>C \<Sigma> \<pi> \<chi> t}) \<inter> reach\<^sub>t \<Sigma> (delta\<^sub>C \<Sigma>) (initial\<^sub>C \<phi>), {y. \<exists>x\<in>{Collect (Acc_inf\<^sub>C \<pi> \<chi>) |\<chi>. \<chi> \<in> Mapping.keys \<pi>}. y = x \<inter> reach\<^sub>t \<Sigma> (delta\<^sub>C \<Sigma>) (initial\<^sub>C \<phi>)})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ({a \<in> reach\<^sub>t \<Sigma> (delta\<^sub>C \<Sigma>) (initial\<^sub>C \<phi>). M_fin\<^sub>C \<phi> \<pi> a \<or> (\<exists>\<chi>\<in>Mapping.keys \<pi>. Acc_fin\<^sub>C \<Sigma> \<pi> \<chi> a)}, {y. \<exists>x\<in>Mapping.keys \<pi>. y = {a \<in> reach\<^sub>t \<Sigma> (delta\<^sub>C \<Sigma>) (initial\<^sub>C \<phi>). Acc_inf\<^sub>C \<pi> x a}}) = ((Collect (M_fin\<^sub>C \<phi> \<pi>) \<union> {t. \<exists>\<chi>\<in>Mapping.keys \<pi>. Acc_fin\<^sub>C \<Sigma> \<pi> \<chi> t}) \<inter> reach\<^sub>t \<Sigma> (delta\<^sub>C \<Sigma>) (initial\<^sub>C \<phi>), {y. \<exists>x\<in>{Collect (Acc_inf\<^sub>C \<pi> \<chi>) |\<chi>. \<chi> \<in> Mapping.keys \<pi>}. y = x \<inter> reach\<^sub>t \<Sigma> (delta\<^sub>C \<Sigma>) (initial\<^sub>C \<phi>)})
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
({a \<in> reach\<^sub>t \<Sigma> (delta\<^sub>C \<Sigma>) (initial\<^sub>C \<phi>). M_fin\<^sub>C \<phi> \<pi> a \<or> (\<exists>\<chi>\<in>Mapping.keys \<pi>. Acc_fin\<^sub>C \<Sigma> \<pi> \<chi> a)}, {y. \<exists>x\<in>Mapping.keys \<pi>. y = {a \<in> reach\<^sub>t \<Sigma> (delta\<^sub>C \<Sigma>) (initial\<^sub>C \<phi>). Acc_inf\<^sub>C \<pi> x a}}) = ((Collect (M_fin\<^sub>C \<phi> \<pi>) \<union> {t. \<exists>\<chi>\<in>Mapping.keys \<pi>. Acc_fin\<^sub>C \<Sigma> \<pi> \<chi> t}) \<inter> reach\<^sub>t \<Sigma> (delta\<^sub>C \<Sigma>) (initial\<^sub>C \<phi>), {y. \<exists>x\<in>{Collect (Acc_inf\<^sub>C \<pi> \<chi>) |\<chi>. \<chi> \<in> Mapping.keys \<pi>}. y = x \<inter> reach\<^sub>t \<Sigma> (delta\<^sub>C \<Sigma>) (initial\<^sub>C \<phi>)})

goal (1 subgoal):
 1. accept\<^sub>G\<^sub>R_LTS (ltl_to_generalized_rabin\<^sub>C \<Sigma>' \<phi>) w \<Longrightarrow> accept\<^sub>G\<^sub>R (\<A> \<Sigma> \<phi>) w
[PROOF STEP]
hence "accepting_pair\<^sub>G\<^sub>R (delta \<Sigma>) (initial \<phi>) (M_fin \<pi>' \<union> \<Union>{Acc_fin \<Sigma> \<pi>' \<chi> | \<chi>. \<chi> \<in> dom \<pi>'}, {Acc_inf \<pi>' \<chi> | \<chi>. \<chi> \<in> dom \<pi>'}) w"
[PROOF STATE]
proof (prove)
using this:
({a \<in> reach\<^sub>t \<Sigma> (delta\<^sub>C \<Sigma>) (initial\<^sub>C \<phi>). M_fin\<^sub>C \<phi> \<pi> a \<or> (\<exists>\<chi>\<in>Mapping.keys \<pi>. Acc_fin\<^sub>C \<Sigma> \<pi> \<chi> a)}, {y. \<exists>x\<in>Mapping.keys \<pi>. y = {a \<in> reach\<^sub>t \<Sigma> (delta\<^sub>C \<Sigma>) (initial\<^sub>C \<phi>). Acc_inf\<^sub>C \<pi> x a}}) = ((Collect (M_fin\<^sub>C \<phi> \<pi>) \<union> {t. \<exists>\<chi>\<in>Mapping.keys \<pi>. Acc_fin\<^sub>C \<Sigma> \<pi> \<chi> t}) \<inter> reach\<^sub>t \<Sigma> (delta\<^sub>C \<Sigma>) (initial\<^sub>C \<phi>), {y. \<exists>x\<in>{Collect (Acc_inf\<^sub>C \<pi> \<chi>) |\<chi>. \<chi> \<in> Mapping.keys \<pi>}. y = x \<inter> reach\<^sub>t \<Sigma> (delta\<^sub>C \<Sigma>) (initial\<^sub>C \<phi>)})

goal (1 subgoal):
 1. accepting_pair\<^sub>G\<^sub>R (delta \<Sigma>) (initial \<phi>) (M_fin \<pi>' \<union> \<Union> {Acc_fin \<Sigma> \<pi>' \<chi> |\<chi>. \<chi> \<in> dom \<pi>'}, {Acc_inf \<pi>' \<chi> |\<chi>. \<chi> \<in> dom \<pi>'}) w
[PROOF STEP]
unfolding X[OF 1]
[PROOF STATE]
proof (prove)
using this:
({a \<in> reach\<^sub>t \<Sigma> (delta\<^sub>C \<Sigma>) (initial\<^sub>C \<phi>). M_fin\<^sub>C \<phi> \<pi> a \<or> (\<exists>\<chi>\<in>Mapping.keys \<pi>. Acc_fin\<^sub>C \<Sigma> \<pi> \<chi> a)}, {y. \<exists>x\<in>Mapping.keys \<pi>. y = {a \<in> reach\<^sub>t \<Sigma> (delta\<^sub>C \<Sigma>) (initial\<^sub>C \<phi>). Acc_inf\<^sub>C \<pi> x a}}) = ((Collect (M_fin\<^sub>C \<phi> \<pi>) \<union> {t. \<exists>\<chi>\<in>Mapping.keys \<pi>. Acc_fin\<^sub>C \<Sigma> \<pi> \<chi> t}) \<inter> reach\<^sub>t \<Sigma> (delta\<^sub>C \<Sigma>) (initial\<^sub>C \<phi>), {y. \<exists>x\<in>{Collect (Acc_inf\<^sub>C \<pi> \<chi>) |\<chi>. \<chi> \<in> Mapping.keys \<pi>}. y = x \<inter> reach\<^sub>t \<Sigma> (delta\<^sub>C \<Sigma>) (initial\<^sub>C \<phi>)})

goal (1 subgoal):
 1. accepting_pair\<^sub>G\<^sub>R_LTS (reach\<^sub>t \<Sigma> (delta\<^sub>C \<Sigma>) (initial\<^sub>C \<phi>)) (initial\<^sub>C \<phi>) ((Collect (M_fin\<^sub>C \<phi> (mapping.Mapping \<pi>')) \<union> {t. \<exists>\<chi>\<in>dom \<pi>'. Acc_fin\<^sub>C \<Sigma> (mapping.Mapping \<pi>') \<chi> t}) \<inter> reach\<^sub>t \<Sigma> (delta\<^sub>C \<Sigma>) (initial\<^sub>C \<phi>), (\<lambda>I. I \<inter> reach\<^sub>t \<Sigma> (delta\<^sub>C \<Sigma>) (initial\<^sub>C \<phi>)) ` {Collect (Acc_inf\<^sub>C (mapping.Mapping \<pi>') \<chi>) |\<chi>. \<chi> \<in> dom \<pi>'}) w
[PROOF STEP]
using 4
[PROOF STATE]
proof (prove)
using this:
({a \<in> reach\<^sub>t \<Sigma> (delta\<^sub>C \<Sigma>) (initial\<^sub>C \<phi>). M_fin\<^sub>C \<phi> \<pi> a \<or> (\<exists>\<chi>\<in>Mapping.keys \<pi>. Acc_fin\<^sub>C \<Sigma> \<pi> \<chi> a)}, {y. \<exists>x\<in>Mapping.keys \<pi>. y = {a \<in> reach\<^sub>t \<Sigma> (delta\<^sub>C \<Sigma>) (initial\<^sub>C \<phi>). Acc_inf\<^sub>C \<pi> x a}}) = ((Collect (M_fin\<^sub>C \<phi> \<pi>) \<union> {t. \<exists>\<chi>\<in>Mapping.keys \<pi>. Acc_fin\<^sub>C \<Sigma> \<pi> \<chi> t}) \<inter> reach\<^sub>t \<Sigma> (delta\<^sub>C \<Sigma>) (initial\<^sub>C \<phi>), {y. \<exists>x\<in>{Collect (Acc_inf\<^sub>C \<pi> \<chi>) |\<chi>. \<chi> \<in> Mapping.keys \<pi>}. y = x \<inter> reach\<^sub>t \<Sigma> (delta\<^sub>C \<Sigma>) (initial\<^sub>C \<phi>)})
accepting_pair\<^sub>G\<^sub>R_LTS (reach\<^sub>t \<Sigma> (delta\<^sub>C \<Sigma>) (initial\<^sub>C \<phi>)) (initial\<^sub>C \<phi>) (Fin, Inf) w

goal (1 subgoal):
 1. accepting_pair\<^sub>G\<^sub>R_LTS (reach\<^sub>t \<Sigma> (delta\<^sub>C \<Sigma>) (initial\<^sub>C \<phi>)) (initial\<^sub>C \<phi>) ((Collect (M_fin\<^sub>C \<phi> (mapping.Mapping \<pi>')) \<union> {t. \<exists>\<chi>\<in>dom \<pi>'. Acc_fin\<^sub>C \<Sigma> (mapping.Mapping \<pi>') \<chi> t}) \<inter> reach\<^sub>t \<Sigma> (delta\<^sub>C \<Sigma>) (initial\<^sub>C \<phi>), (\<lambda>I. I \<inter> reach\<^sub>t \<Sigma> (delta\<^sub>C \<Sigma>) (initial\<^sub>C \<phi>)) ` {Collect (Acc_inf\<^sub>C (mapping.Mapping \<pi>') \<chi>) |\<chi>. \<chi> \<in> dom \<pi>'}) w
[PROOF STEP]
unfolding Y Set.filter_def
[PROOF STATE]
proof (prove)
using this:
({a \<in> reach\<^sub>t \<Sigma> (delta\<^sub>C \<Sigma>) (initial\<^sub>C \<phi>). M_fin\<^sub>C \<phi> \<pi> a \<or> (\<exists>\<chi>\<in>Mapping.keys \<pi>. Acc_fin\<^sub>C \<Sigma> \<pi> \<chi> a)}, {y. \<exists>x\<in>Mapping.keys \<pi>. y = {a \<in> reach\<^sub>t \<Sigma> (delta\<^sub>C \<Sigma>) (initial\<^sub>C \<phi>). Acc_inf\<^sub>C \<pi> x a}}) = ((Collect (M_fin\<^sub>C \<phi> \<pi>) \<union> {t. \<exists>\<chi>\<in>Mapping.keys \<pi>. Acc_fin\<^sub>C \<Sigma> \<pi> \<chi> t}) \<inter> reach\<^sub>t \<Sigma> (delta\<^sub>C \<Sigma>) (initial\<^sub>C \<phi>), {y. \<exists>x\<in>{Collect (Acc_inf\<^sub>C \<pi> \<chi>) |\<chi>. \<chi> \<in> Mapping.keys \<pi>}. y = x \<inter> reach\<^sub>t \<Sigma> (delta\<^sub>C \<Sigma>) (initial\<^sub>C \<phi>)})
accepting_pair\<^sub>G\<^sub>R_LTS (reach\<^sub>t \<Sigma> (delta\<^sub>C \<Sigma>) (initial\<^sub>C \<phi>)) (initial\<^sub>C \<phi>) ({a \<in> reach\<^sub>t \<Sigma> (delta\<^sub>C \<Sigma>) (initial\<^sub>C \<phi>). M_fin\<^sub>C \<phi> \<pi> a \<or> (\<exists>\<chi>\<in>Mapping.keys \<pi>. Acc_fin\<^sub>C \<Sigma> \<pi> \<chi> a)}, (\<lambda>\<chi>. {a \<in> reach\<^sub>t \<Sigma> (delta\<^sub>C \<Sigma>) (initial\<^sub>C \<phi>). Acc_inf\<^sub>C \<pi> \<chi> a}) ` Mapping.keys \<pi>) w

goal (1 subgoal):
 1. accepting_pair\<^sub>G\<^sub>R_LTS (reach\<^sub>t \<Sigma> (delta\<^sub>C \<Sigma>) (initial\<^sub>C \<phi>)) (initial\<^sub>C \<phi>) ((Collect (M_fin\<^sub>C \<phi> (mapping.Mapping \<pi>')) \<union> {t. \<exists>\<chi>\<in>dom \<pi>'. Acc_fin\<^sub>C \<Sigma> (mapping.Mapping \<pi>') \<chi> t}) \<inter> reach\<^sub>t \<Sigma> (delta\<^sub>C \<Sigma>) (initial\<^sub>C \<phi>), (\<lambda>I. I \<inter> reach\<^sub>t \<Sigma> (delta\<^sub>C \<Sigma>) (initial\<^sub>C \<phi>)) ` {Collect (Acc_inf\<^sub>C (mapping.Mapping \<pi>') \<chi>) |\<chi>. \<chi> \<in> dom \<pi>'}) w
[PROOF STEP]
unfolding \<open>dom \<pi>' = Mapping.keys \<pi>\<close> \<open>Mapping.Mapping \<pi>' = \<pi>\<close> image_def
[PROOF STATE]
proof (prove)
using this:
({a \<in> reach\<^sub>t \<Sigma> (delta\<^sub>C \<Sigma>) (initial\<^sub>C \<phi>). M_fin\<^sub>C \<phi> \<pi> a \<or> (\<exists>\<chi>\<in>Mapping.keys \<pi>. Acc_fin\<^sub>C \<Sigma> \<pi> \<chi> a)}, {y. \<exists>x\<in>Mapping.keys \<pi>. y = {a \<in> reach\<^sub>t \<Sigma> (delta\<^sub>C \<Sigma>) (initial\<^sub>C \<phi>). Acc_inf\<^sub>C \<pi> x a}}) = ((Collect (M_fin\<^sub>C \<phi> \<pi>) \<union> {t. \<exists>\<chi>\<in>Mapping.keys \<pi>. Acc_fin\<^sub>C \<Sigma> \<pi> \<chi> t}) \<inter> reach\<^sub>t \<Sigma> (delta\<^sub>C \<Sigma>) (initial\<^sub>C \<phi>), {y. \<exists>x\<in>{Collect (Acc_inf\<^sub>C \<pi> \<chi>) |\<chi>. \<chi> \<in> Mapping.keys \<pi>}. y = x \<inter> reach\<^sub>t \<Sigma> (delta\<^sub>C \<Sigma>) (initial\<^sub>C \<phi>)})
accepting_pair\<^sub>G\<^sub>R_LTS (reach\<^sub>t \<Sigma> (delta\<^sub>C \<Sigma>) (initial\<^sub>C \<phi>)) (initial\<^sub>C \<phi>) ({a \<in> reach\<^sub>t \<Sigma> (delta\<^sub>C \<Sigma>) (initial\<^sub>C \<phi>). M_fin\<^sub>C \<phi> \<pi> a \<or> (\<exists>\<chi>\<in>Mapping.keys \<pi>. Acc_fin\<^sub>C \<Sigma> \<pi> \<chi> a)}, {y. \<exists>x\<in>Mapping.keys \<pi>. y = {a \<in> reach\<^sub>t \<Sigma> (delta\<^sub>C \<Sigma>) (initial\<^sub>C \<phi>). Acc_inf\<^sub>C \<pi> x a}}) w

goal (1 subgoal):
 1. accepting_pair\<^sub>G\<^sub>R_LTS (reach\<^sub>t \<Sigma> (delta\<^sub>C \<Sigma>) (initial\<^sub>C \<phi>)) (initial\<^sub>C \<phi>) ((Collect (M_fin\<^sub>C \<phi> \<pi>) \<union> {t. \<exists>\<chi>\<in>Mapping.keys \<pi>. Acc_fin\<^sub>C \<Sigma> \<pi> \<chi> t}) \<inter> reach\<^sub>t \<Sigma> (delta\<^sub>C \<Sigma>) (initial\<^sub>C \<phi>), {y. \<exists>x\<in>{Collect (Acc_inf\<^sub>C \<pi> \<chi>) |\<chi>. \<chi> \<in> Mapping.keys \<pi>}. y = x \<inter> reach\<^sub>t \<Sigma> (delta\<^sub>C \<Sigma>) (initial\<^sub>C \<phi>)}) w
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
accepting_pair\<^sub>G\<^sub>R (delta \<Sigma>) (initial \<phi>) (M_fin \<pi>' \<union> \<Union> {Acc_fin \<Sigma> \<pi>' \<chi> |\<chi>. \<chi> \<in> dom \<pi>'}, {Acc_inf \<pi>' \<chi> |\<chi>. \<chi> \<in> dom \<pi>'}) w

goal (1 subgoal):
 1. accept\<^sub>G\<^sub>R_LTS (ltl_to_generalized_rabin\<^sub>C \<Sigma>' \<phi>) w \<Longrightarrow> accept\<^sub>G\<^sub>R (\<A> \<Sigma> \<phi>) w
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
dom \<pi>' \<subseteq> \<^bold>G \<phi>
?\<chi>17 \<in> dom \<pi>' \<Longrightarrow> the (\<pi>' ?\<chi>17) < max_rank_of \<Sigma> ?\<chi>17
accepting_pair\<^sub>G\<^sub>R (delta \<Sigma>) (initial \<phi>) (M_fin \<pi>' \<union> \<Union> {Acc_fin \<Sigma> \<pi>' \<chi> |\<chi>. \<chi> \<in> dom \<pi>'}, {Acc_inf \<pi>' \<chi> |\<chi>. \<chi> \<in> dom \<pi>'}) w
[PROOF STEP]
show ?lhs
[PROOF STATE]
proof (prove)
using this:
dom \<pi>' \<subseteq> \<^bold>G \<phi>
?\<chi>17 \<in> dom \<pi>' \<Longrightarrow> the (\<pi>' ?\<chi>17) < max_rank_of \<Sigma> ?\<chi>17
accepting_pair\<^sub>G\<^sub>R (delta \<Sigma>) (initial \<phi>) (M_fin \<pi>' \<union> \<Union> {Acc_fin \<Sigma> \<pi>' \<chi> |\<chi>. \<chi> \<in> dom \<pi>'}, {Acc_inf \<pi>' \<chi> |\<chi>. \<chi> \<in> dom \<pi>'}) w

goal (1 subgoal):
 1. accept\<^sub>G\<^sub>R (\<A> \<Sigma> \<phi>) w
[PROOF STEP]
unfolding ltl_to_generalized_rabin.simps
[PROOF STATE]
proof (prove)
using this:
dom \<pi>' \<subseteq> \<^bold>G \<phi>
?\<chi>17 \<in> dom \<pi>' \<Longrightarrow> the (\<pi>' ?\<chi>17) < max_rank_of \<Sigma> ?\<chi>17
accepting_pair\<^sub>G\<^sub>R (delta \<Sigma>) (initial \<phi>) (M_fin \<pi>' \<union> \<Union> {Acc_fin \<Sigma> \<pi>' \<chi> |\<chi>. \<chi> \<in> dom \<pi>'}, {Acc_inf \<pi>' \<chi> |\<chi>. \<chi> \<in> dom \<pi>'}) w

goal (1 subgoal):
 1. accept\<^sub>G\<^sub>R (delta \<Sigma>, initial \<phi>, rabin_pairs \<Sigma> \<phi>) w
[PROOF STEP]
by (intro Rabin.accept\<^sub>G\<^sub>R_I, blast; auto)
[PROOF STATE]
proof (state)
this:
accept\<^sub>G\<^sub>R (\<A> \<Sigma> \<phi>) w

goal:
No subgoals!
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
accept\<^sub>G\<^sub>R_LTS (ltl_to_generalized_rabin\<^sub>C \<Sigma>' \<phi>) w \<Longrightarrow> accept\<^sub>G\<^sub>R (\<A> \<Sigma> \<phi>) w

goal:
No subgoals!
[PROOF STEP]
qed