[STATEMENT]
lemma map_pair_automaton:
  "pair_automaton (fmap_funs_ta f A) (fmap_funs_ta g B) =
   fmap_funs_ta (\<lambda>(a, b). (map_option f a, map_option g b)) (pair_automaton A B)" (is "?Ls = ?Rs")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pair_automaton (fmap_funs_ta f A) (fmap_funs_ta g B) = fmap_funs_ta (\<lambda>(a, b). (map_option f a, map_option g b)) (pair_automaton A B)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. pair_automaton (fmap_funs_ta f A) (fmap_funs_ta g B) = fmap_funs_ta (\<lambda>(a, b). (map_option f a, map_option g b)) (pair_automaton A B)
[PROOF STEP]
let ?ls = "pair_rule \<circ> map_prod (map_ta_rule id f) (map_ta_rule id g)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. pair_automaton (fmap_funs_ta f A) (fmap_funs_ta g B) = fmap_funs_ta (\<lambda>(a, b). (map_option f a, map_option g b)) (pair_automaton A B)
[PROOF STEP]
let ?rs = "map_ta_rule id (\<lambda>(a, b). (map_option f a, map_option g b)) \<circ> pair_rule"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. pair_automaton (fmap_funs_ta f A) (fmap_funs_ta g B) = fmap_funs_ta (\<lambda>(a, b). (map_option f a, map_option g b)) (pair_automaton A B)
[PROOF STEP]
have *: "(\<lambda>(a, b). (map_option f a, map_option g b)) \<circ> lift_Some_None = lift_Some_None \<circ> f"
    "(\<lambda>(a, b). (map_option f a, map_option g b)) \<circ> lift_None_Some = lift_None_Some \<circ> g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>(a, b). (map_option f a, map_option g b)) \<circ> lift_Some_None = lift_Some_None \<circ> f &&& (\<lambda>(a, b). (map_option f a, map_option g b)) \<circ> lift_None_Some = lift_None_Some \<circ> g
[PROOF STEP]
by (auto simp: comp_def)
[PROOF STATE]
proof (state)
this:
(\<lambda>(a, b). (map_option f a, map_option g b)) \<circ> lift_Some_None = lift_Some_None \<circ> f
(\<lambda>(a, b). (map_option f a, map_option g b)) \<circ> lift_None_Some = lift_None_Some \<circ> g

goal (1 subgoal):
 1. pair_automaton (fmap_funs_ta f A) (fmap_funs_ta g B) = fmap_funs_ta (\<lambda>(a, b). (map_option f a, map_option g b)) (pair_automaton A B)
[PROOF STEP]
have "?ls x = ?rs x" for x
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (pair_rule \<circ> map_prod (map_ta_rule id f) (map_ta_rule id g)) x = (map_ta_rule id (\<lambda>(a, b). (map_option f a, map_option g b)) \<circ> pair_rule) x
[PROOF STEP]
by (cases x) (auto simp: ta_rule.map_sel)
[PROOF STATE]
proof (state)
this:
(pair_rule \<circ> map_prod (map_ta_rule id f) (map_ta_rule id g)) ?x3 = (map_ta_rule id (\<lambda>(a, b). (map_option f a, map_option g b)) \<circ> pair_rule) ?x3

goal (1 subgoal):
 1. pair_automaton (fmap_funs_ta f A) (fmap_funs_ta g B) = fmap_funs_ta (\<lambda>(a, b). (map_option f a, map_option g b)) (pair_automaton A B)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(pair_rule \<circ> map_prod (map_ta_rule id f) (map_ta_rule id g)) ?x3 = (map_ta_rule id (\<lambda>(a, b). (map_option f a, map_option g b)) \<circ> pair_rule) ?x3
[PROOF STEP]
have [simp]: "?ls = ?rs"
[PROOF STATE]
proof (prove)
using this:
(pair_rule \<circ> map_prod (map_ta_rule id f) (map_ta_rule id g)) ?x3 = (map_ta_rule id (\<lambda>(a, b). (map_option f a, map_option g b)) \<circ> pair_rule) ?x3

goal (1 subgoal):
 1. pair_rule \<circ> map_prod (map_ta_rule id f) (map_ta_rule id g) = map_ta_rule id (\<lambda>(a, b). (map_option f a, map_option g b)) \<circ> pair_rule
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
pair_rule \<circ> map_prod (map_ta_rule id f) (map_ta_rule id g) = map_ta_rule id (\<lambda>(a, b). (map_option f a, map_option g b)) \<circ> pair_rule

goal (1 subgoal):
 1. pair_automaton (fmap_funs_ta f A) (fmap_funs_ta g B) = fmap_funs_ta (\<lambda>(a, b). (map_option f a, map_option g b)) (pair_automaton A B)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
pair_rule \<circ> map_prod (map_ta_rule id f) (map_ta_rule id g) = map_ta_rule id (\<lambda>(a, b). (map_option f a, map_option g b)) \<circ> pair_rule
[PROOF STEP]
have "rules ?Ls = rules ?Rs"
[PROOF STATE]
proof (prove)
using this:
pair_rule \<circ> map_prod (map_ta_rule id f) (map_ta_rule id g) = map_ta_rule id (\<lambda>(a, b). (map_option f a, map_option g b)) \<circ> pair_rule

goal (1 subgoal):
 1. rules (pair_automaton (fmap_funs_ta f A) (fmap_funs_ta g B)) = rules (fmap_funs_ta (\<lambda>(a, b). (map_option f a, map_option g b)) (pair_automaton A B))
[PROOF STEP]
unfolding pair_automaton_def fmap_funs_ta_def
[PROOF STATE]
proof (prove)
using this:
pair_rule \<circ> map_prod (map_ta_rule id f) (map_ta_rule id g) = map_ta_rule id (\<lambda>(a, b). (map_option f a, map_option g b)) \<circ> pair_rule

goal (1 subgoal):
 1. rules (TA (map_ta_rule lift_Some_None lift_Some_None |`| rules (TA (map_ta_rule id f |`| rules A) (eps A)) |\<union>| map_ta_rule lift_None_Some lift_None_Some |`| rules (TA (map_ta_rule id g |`| rules B) (eps B)) |\<union>| pair_rule |`| (rules (TA (map_ta_rule id f |`| rules A) (eps A)) |\<times>| rules (TA (map_ta_rule id g |`| rules B) (eps B)))) (pair_eps (TA (map_ta_rule id f |`| rules A) (eps A)) (TA (map_ta_rule id g |`| rules B) (eps B)) |\<union>| map_both prod.swap |`| pair_eps (TA (map_ta_rule id g |`| rules B) (eps B)) (TA (map_ta_rule id f |`| rules A) (eps A)))) = rules (TA (map_ta_rule id (\<lambda>(a, b). (map_option f a, map_option g b)) |`| rules (TA (map_ta_rule lift_Some_None lift_Some_None |`| rules A |\<union>| map_ta_rule lift_None_Some lift_None_Some |`| rules B |\<union>| pair_rule |`| (rules A |\<times>| rules B)) (pair_eps A B |\<union>| map_both prod.swap |`| pair_eps B A))) (eps (TA (map_ta_rule lift_Some_None lift_Some_None |`| rules A |\<union>| map_ta_rule lift_None_Some lift_None_Some |`| rules B |\<union>| pair_rule |`| (rules A |\<times>| rules B)) (pair_eps A B |\<union>| map_both prod.swap |`| pair_eps B A))))
[PROOF STEP]
by (simp add: fimage_funion map_ta_rule_comp * map_prod_ftimes)
[PROOF STATE]
proof (state)
this:
rules (pair_automaton (fmap_funs_ta f A) (fmap_funs_ta g B)) = rules (fmap_funs_ta (\<lambda>(a, b). (map_option f a, map_option g b)) (pair_automaton A B))

goal (1 subgoal):
 1. pair_automaton (fmap_funs_ta f A) (fmap_funs_ta g B) = fmap_funs_ta (\<lambda>(a, b). (map_option f a, map_option g b)) (pair_automaton A B)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
rules (pair_automaton (fmap_funs_ta f A) (fmap_funs_ta g B)) = rules (fmap_funs_ta (\<lambda>(a, b). (map_option f a, map_option g b)) (pair_automaton A B))

goal (1 subgoal):
 1. pair_automaton (fmap_funs_ta f A) (fmap_funs_ta g B) = fmap_funs_ta (\<lambda>(a, b). (map_option f a, map_option g b)) (pair_automaton A B)
[PROOF STEP]
have "eps ?Ls = eps ?Rs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eps (pair_automaton (fmap_funs_ta f A) (fmap_funs_ta g B)) = eps (fmap_funs_ta (\<lambda>(a, b). (map_option f a, map_option g b)) (pair_automaton A B))
[PROOF STEP]
unfolding pair_automaton_def fmap_funs_ta_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eps (TA (map_ta_rule lift_Some_None lift_Some_None |`| rules (TA (map_ta_rule id f |`| rules A) (eps A)) |\<union>| map_ta_rule lift_None_Some lift_None_Some |`| rules (TA (map_ta_rule id g |`| rules B) (eps B)) |\<union>| pair_rule |`| (rules (TA (map_ta_rule id f |`| rules A) (eps A)) |\<times>| rules (TA (map_ta_rule id g |`| rules B) (eps B)))) (pair_eps (TA (map_ta_rule id f |`| rules A) (eps A)) (TA (map_ta_rule id g |`| rules B) (eps B)) |\<union>| map_both prod.swap |`| pair_eps (TA (map_ta_rule id g |`| rules B) (eps B)) (TA (map_ta_rule id f |`| rules A) (eps A)))) = eps (TA (map_ta_rule id (\<lambda>(a, b). (map_option f a, map_option g b)) |`| rules (TA (map_ta_rule lift_Some_None lift_Some_None |`| rules A |\<union>| map_ta_rule lift_None_Some lift_None_Some |`| rules B |\<union>| pair_rule |`| (rules A |\<times>| rules B)) (pair_eps A B |\<union>| map_both prod.swap |`| pair_eps B A))) (eps (TA (map_ta_rule lift_Some_None lift_Some_None |`| rules A |\<union>| map_ta_rule lift_None_Some lift_None_Some |`| rules B |\<union>| pair_rule |`| (rules A |\<times>| rules B)) (pair_eps A B |\<union>| map_both prod.swap |`| pair_eps B A))))
[PROOF STEP]
by (simp add: fimage_funion \<Q>_def)
[PROOF STATE]
proof (state)
this:
eps (pair_automaton (fmap_funs_ta f A) (fmap_funs_ta g B)) = eps (fmap_funs_ta (\<lambda>(a, b). (map_option f a, map_option g b)) (pair_automaton A B))

goal (1 subgoal):
 1. pair_automaton (fmap_funs_ta f A) (fmap_funs_ta g B) = fmap_funs_ta (\<lambda>(a, b). (map_option f a, map_option g b)) (pair_automaton A B)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
rules (pair_automaton (fmap_funs_ta f A) (fmap_funs_ta g B)) = rules (fmap_funs_ta (\<lambda>(a, b). (map_option f a, map_option g b)) (pair_automaton A B))
eps (pair_automaton (fmap_funs_ta f A) (fmap_funs_ta g B)) = eps (fmap_funs_ta (\<lambda>(a, b). (map_option f a, map_option g b)) (pair_automaton A B))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
rules (pair_automaton (fmap_funs_ta f A) (fmap_funs_ta g B)) = rules (fmap_funs_ta (\<lambda>(a, b). (map_option f a, map_option g b)) (pair_automaton A B))
eps (pair_automaton (fmap_funs_ta f A) (fmap_funs_ta g B)) = eps (fmap_funs_ta (\<lambda>(a, b). (map_option f a, map_option g b)) (pair_automaton A B))

goal (1 subgoal):
 1. pair_automaton (fmap_funs_ta f A) (fmap_funs_ta g B) = fmap_funs_ta (\<lambda>(a, b). (map_option f a, map_option g b)) (pair_automaton A B)
[PROOF STEP]
by (intro TA_equalityI) simp
[PROOF STATE]
proof (state)
this:
pair_automaton (fmap_funs_ta f A) (fmap_funs_ta g B) = fmap_funs_ta (\<lambda>(a, b). (map_option f a, map_option g b)) (pair_automaton A B)

goal:
No subgoals!
[PROOF STEP]
qed