[STATEMENT]
lemma (in strategic_space_2p) separable_case_DD: (* both player defect *)
  assumes "\<gamma> = 0"
  shows "\<phi>\<^sub>A = 0 \<and> \<theta>\<^sub>A = pi \<and> \<phi>\<^sub>B = 0 \<and> \<theta>\<^sub>B = pi \<longrightarrow> alice_payoff = 1 \<and> bob_payoff = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<phi>\<^sub>A = 0 \<and> \<theta>\<^sub>A = pi \<and> \<phi>\<^sub>B = 0 \<and> \<theta>\<^sub>B = pi \<longrightarrow> alice_payoff = 1 \<and> bob_payoff = 1
[PROOF STEP]
using alice_payoff_def bob_payoff_def cos_sin_squared_add_cpx psi_f_is_state
[PROOF STATE]
proof (prove)
using this:
alice_payoff \<equiv> 3 * (if state 2 (Tensor.mat_of_cols_list 4 [[complex_of_real (cos (\<gamma> / 2)) * (exp (\<i> * complex_of_real \<phi>\<^sub>A) * complex_of_real (cos (\<theta>\<^sub>A / 2)) * exp (\<i> * complex_of_real \<phi>\<^sub>B) * complex_of_real (cos (\<theta>\<^sub>B / 2)) * complex_of_real (cos (\<gamma> / 2)) + complex_of_real (sin (\<theta>\<^sub>A / 2) * sin (\<theta>\<^sub>B / 2)) * \<i> * complex_of_real (sin (\<gamma> / 2))) + - \<i> * complex_of_real (sin (\<gamma> / 2)) * (complex_of_real (sin (\<theta>\<^sub>A / 2) * sin (\<theta>\<^sub>B / 2) * cos (\<gamma> / 2)) + exp (- \<i> * complex_of_real \<phi>\<^sub>A) * complex_of_real (cos (\<theta>\<^sub>A / 2)) * exp (- \<i> * complex_of_real \<phi>\<^sub>B) * complex_of_real (cos (\<theta>\<^sub>B / 2)) * \<i> * complex_of_real (sin (\<gamma> / 2))), complex_of_real (cos (\<gamma> / 2)) * (exp (\<i> * complex_of_real \<phi>\<^sub>A) * complex_of_real (cos (\<theta>\<^sub>A / 2)) * complex_of_real (- sin (\<theta>\<^sub>B / 2)) * complex_of_real (cos (\<gamma> / 2)) + complex_of_real (sin (\<theta>\<^sub>A / 2)) * exp (- \<i> * complex_of_real \<phi>\<^sub>B) * complex_of_real (cos (\<theta>\<^sub>B / 2)) * \<i> * complex_of_real (sin (\<gamma> / 2))) + \<i> * complex_of_real (sin (\<gamma> / 2)) * (complex_of_real (- sin (\<theta>\<^sub>A / 2)) * exp (\<i> * complex_of_real \<phi>\<^sub>B) * complex_of_real (cos (\<theta>\<^sub>B / 2)) * complex_of_real (cos (\<gamma> / 2)) + exp (- \<i> * complex_of_real \<phi>\<^sub>A) * complex_of_real (cos (\<theta>\<^sub>A / 2)) * complex_of_real (sin (\<theta>\<^sub>B / 2)) * \<i> * complex_of_real (sin (\<gamma> / 2))), \<i> * complex_of_real (sin (\<gamma> / 2)) * (exp (\<i> * complex_of_real \<phi>\<^sub>A) * complex_of_real (cos (\<theta>\<^sub>A / 2)) * complex_of_real (- sin (\<theta>\<^sub>B / 2)) * complex_of_real (cos (\<gamma> / 2)) + complex_of_real (sin (\<theta>\<^sub>A / 2)) * exp (- \<i> * complex_of_real \<phi>\<^sub>B) * complex_of_real (cos (\<theta>\<^sub>B / 2)) * \<i> * complex_of_real (sin (\<gamma> / 2))) + complex_of_real (cos (\<gamma> / 2)) * (complex_of_real (- sin (\<theta>\<^sub>A / 2)) * exp (\<i> * complex_of_real \<phi>\<^sub>B) * complex_of_real (cos (\<theta>\<^sub>B / 2)) * complex_of_real (cos (\<gamma> / 2)) + exp (- \<i> * complex_of_real \<phi>\<^sub>A) * complex_of_real (cos (\<theta>\<^sub>A / 2)) * complex_of_real (sin (\<theta>\<^sub>B / 2)) * \<i> * complex_of_real (sin (\<gamma> / 2))), - \<i> * complex_of_real (sin (\<gamma> / 2)) * (exp (\<i> * complex_of_real \<phi>\<^sub>A) * complex_of_real (cos (\<theta>\<^sub>A / 2)) * exp (\<i> * complex_of_real \<phi>\<^sub>B) * complex_of_real (cos (\<theta>\<^sub>B / 2)) * complex_of_real (cos (\<gamma> / 2)) + complex_of_real (sin (\<theta>\<^sub>A / 2) * sin (\<theta>\<^sub>B / 2)) * \<i> * complex_of_real (sin (\<gamma> / 2))) + complex_of_real (cos (\<gamma> / 2)) * (complex_of_real (sin (\<theta>\<^sub>A / 2) * sin (\<theta>\<^sub>B / 2) * cos (\<gamma> / 2)) + exp (- \<i> * complex_of_real \<phi>\<^sub>A) * complex_of_real (cos (\<theta>\<^sub>A / 2)) * exp (- \<i> * complex_of_real \<phi>\<^sub>B) * complex_of_real (cos (\<theta>\<^sub>B / 2)) * \<i> * complex_of_real (sin (\<gamma> / 2)))]]) then (cmod (Tensor.mat_of_cols_list 4 [[complex_of_real (cos (\<gamma> / 2)) * (exp (\<i> * complex_of_real \<phi>\<^sub>A) * complex_of_real (cos (\<theta>\<^sub>A / 2)) * exp (\<i> * complex_of_real \<phi>\<^sub>B) * complex_of_real (cos (\<theta>\<^sub>B / 2)) * complex_of_real (cos (\<gamma> / 2)) + complex_of_real (sin (\<theta>\<^sub>A / 2) * sin (\<theta>\<^sub>B / 2)) * \<i> * complex_of_real (sin (\<gamma> / 2))) + - \<i> * complex_of_real (sin (\<gamma> / 2)) * (complex_of_real (sin (\<theta>\<^sub>A / 2) * sin (\<theta>\<^sub>B / 2) * cos (\<gamma> / 2)) + exp (- \<i> * complex_of_real \<phi>\<^sub>A) * complex_of_real (cos (\<theta>\<^sub>A / 2)) * exp (- \<i> * complex_of_real \<phi>\<^sub>B) * complex_of_real (cos (\<theta>\<^sub>B / 2)) * \<i> * complex_of_real (sin (\<gamma> / 2))), complex_of_real (cos (\<gamma> / 2)) * (exp (\<i> * complex_of_real \<phi>\<^sub>A) * complex_of_real (cos (\<theta>\<^sub>A / 2)) * complex_of_real (- sin (\<theta>\<^sub>B / 2)) * complex_of_real (cos (\<gamma> / 2)) + complex_of_real (sin (\<theta>\<^sub>A / 2)) * exp (- \<i> * complex_of_real \<phi>\<^sub>B) * complex_of_real (cos (\<theta>\<^sub>B / 2)) * \<i> * complex_of_real (sin (\<gamma> / 2))) + \<i> * complex_of_real (sin (\<gamma> / 2)) * (complex_of_real (- sin (\<theta>\<^sub>A / 2)) * exp (\<i> * complex_of_real \<phi>\<^sub>B) * complex_of_real (cos (\<theta>\<^sub>B / 2)) * complex_of_real (cos (\<gamma> / 2)) + exp (- \<i> * complex_of_real \<phi>\<^sub>A) * complex_of_real (cos (\<theta>\<^sub>A / 2)) * complex_of_real (sin (\<theta>\<^sub>B / 2)) * \<i> * complex_of_real (sin (\<gamma> / 2))), \<i> * complex_of_real (sin (\<gamma> / 2)) * (exp (\<i> * complex_of_real \<phi>\<^sub>A) * complex_of_real (cos (\<theta>\<^sub>A / 2)) * complex_of_real (- sin (\<theta>\<^sub>B / 2)) * complex_of_real (cos (\<gamma> / 2)) + complex_of_real (sin (\<theta>\<^sub>A / 2)) * exp (- \<i> * complex_of_real \<phi>\<^sub>B) * complex_of_real (cos (\<theta>\<^sub>B / 2)) * \<i> * complex_of_real (sin (\<gamma> / 2))) + complex_of_real (cos (\<gamma> / 2)) * (complex_of_real (- sin (\<theta>\<^sub>A / 2)) * exp (\<i> * complex_of_real \<phi>\<^sub>B) * complex_of_real (cos (\<theta>\<^sub>B / 2)) * complex_of_real (cos (\<gamma> / 2)) + exp (- \<i> * complex_of_real \<phi>\<^sub>A) * complex_of_real (cos (\<theta>\<^sub>A / 2)) * complex_of_real (sin (\<theta>\<^sub>B / 2)) * \<i> * complex_of_real (sin (\<gamma> / 2))), - \<i> * complex_of_real (sin (\<gamma> / 2)) * (exp (\<i> * complex_of_real \<phi>\<^sub>A) * complex_of_real (cos (\<theta>\<^sub>A / 2)) * exp (\<i> * complex_of_real \<phi>\<^sub>B) * complex_of_real (cos (\<theta>\<^sub>B / 2)) * complex_of_real (cos (\<gamma> / 2)) + complex_of_real (sin (\<theta>\<^sub>A / 2) * sin (\<theta>\<^sub>B / 2)) * \<i> * complex_of_real (sin (\<gamma> / 2))) + complex_of_real (cos (\<gamma> / 2)) * (complex_of_real (sin (\<theta>\<^sub>A / 2) * sin (\<theta>\<^sub>B / 2) * cos (\<gamma> / 2)) + exp (- \<i> * complex_of_real \<phi>\<^sub>A) * complex_of_real (cos (\<theta>\<^sub>A / 2)) * exp (- \<i> * complex_of_real \<phi>\<^sub>B) * complex_of_real (cos (\<theta>\<^sub>B / 2)) * \<i> * complex_of_real (sin (\<gamma> / 2)))]] $$ (0, 0)))\<^sup>2 else undefined) + 1 * (if state 2 (Tensor.mat_of_cols_list 4 [[complex_of_real (cos (\<gamma> / 2)) * (exp (\<i> * complex_of_real \<phi>\<^sub>A) * complex_of_real (cos (\<theta>\<^sub>A / 2)) * exp (\<i> * complex_of_real \<phi>\<^sub>B) * complex_of_real (cos (\<theta>\<^sub>B / 2)) * complex_of_real (cos (\<gamma> / 2)) + complex_of_real (sin (\<theta>\<^sub>A / 2) * sin (\<theta>\<^sub>B / 2)) * \<i> * complex_of_real (sin (\<gamma> / 2))) + - \<i> * complex_of_real (sin (\<gamma> / 2)) * (complex_of_real (sin (\<theta>\<^sub>A / 2) * sin (\<theta>\<^sub>B / 2) * cos (\<gamma> / 2)) + exp (- \<i> * complex_of_real \<phi>\<^sub>A) * complex_of_real (cos (\<theta>\<^sub>A / 2)) * exp (- \<i> * complex_of_real \<phi>\<^sub>B) * complex_of_real (cos (\<theta>\<^sub>B / 2)) * \<i> * complex_of_real (sin (\<gamma> / 2))), complex_of_real (cos (\<gamma> / 2)) * (exp (\<i> * complex_of_real \<phi>\<^sub>A) * complex_of_real (cos (\<theta>\<^sub>A / 2)) * complex_of_real (- sin (\<theta>\<^sub>B / 2)) * complex_of_real (cos (\<gamma> / 2)) + complex_of_real (sin (\<theta>\<^sub>A / 2)) * exp (- \<i> * complex_of_real \<phi>\<^sub>B) * complex_of_real (cos (\<theta>\<^sub>B / 2)) * \<i> * complex_of_real (sin (\<gamma> / 2))) + \<i> * complex_of_real (sin (\<gamma> / 2)) * (complex_of_real (- sin (\<theta>\<^sub>A / 2)) * exp (\<i> * complex_of_real \<phi>\<^sub>B) * complex_of_real (cos (\<theta>\<^sub>B / 2)) * complex_of_real (cos (\<gamma> / 2)) + exp (- \<i> * complex_of_real \<phi>\<^sub>A) * complex_of_real (cos (\<theta>\<^sub>A / 2)) * complex_of_real (sin (\<theta>\<^sub>B / 2)) * \<i> * complex_of_real (sin (\<gamma> / 2))), \<i> * complex_of_real (sin (\<gamma> / 2)) * (exp (\<i> * complex_of_real \<phi>\<^sub>A) * complex_of_real (cos (\<theta>\<^sub>A / 2)) * complex_of_real (- sin (\<theta>\<^sub>B / 2)) * complex_of_real (cos (\<gamma> / 2)) + complex_of_real (sin (\<theta>\<^sub>A / 2)) * exp (- \<i> * complex_of_real \<phi>\<^sub>B) * complex_of_real (cos (\<theta>\<^sub>B / 2)) * \<i> * complex_of_real (sin (\<gamma> / 2))) + complex_of_real (cos (\<gamma> / 2)) * (complex_of_real (- sin (\<theta>\<^sub>A / 2)) * exp (\<i> * complex_of_real \<phi>\<^sub>B) * complex_of_real (cos (\<theta>\<^sub>B / 2)) * complex_of_real (cos (\<gamma> / 2)) + exp (- \<i> * complex_of_real \<phi>\<^sub>A) * complex_of_real (cos (\<theta>\<^sub>A / 2)) * complex_of_real (sin (\<theta>\<^sub>B / 2)) * \<i> * complex_of_real (sin (\<gamma> / 2))), - \<i> * complex_of_real (sin (\<gamma> / 2)) * (exp (\<i> * complex_of_real \<phi>\<^sub>A) * complex_of_real (cos (\<theta>\<^sub>A / 2)) * exp (\<i> * complex_of_real \<phi>\<^sub>B) * complex_of_real (cos (\<theta>\<^sub>B / 2)) * complex_of_real (cos (\<gamma> / 2)) + complex_of_real (sin (\<theta>\<^sub>A / 2) * sin (\<theta>\<^sub>B / 2)) * \<i> * complex_of_real (sin (\<gamma> / 2))) + complex_of_real (cos (\<gamma> / 2)) * (complex_of_real (sin (\<theta>\<^sub>A / 2) * sin (\<theta>\<^sub>B / 2) * cos (\<gamma> / 2)) + exp (- \<i> * complex_of_real \<phi>\<^sub>A) * complex_of_real (cos (\<theta>\<^sub>A / 2)) * exp (- \<i> * complex_of_real \<phi>\<^sub>B) * complex_of_real (cos (\<theta>\<^sub>B / 2)) * \<i> * complex_of_real (sin (\<gamma> / 2)))]]) then (cmod (Tensor.mat_of_cols_list 4 [[complex_of_real (cos (\<gamma> / 2)) * (exp (\<i> * complex_of_real \<phi>\<^sub>A) * complex_of_real (cos (\<theta>\<^sub>A / 2)) * exp (\<i> * complex_of_real \<phi>\<^sub>B) * complex_of_real (cos (\<theta>\<^sub>B / 2)) * complex_of_real (cos (\<gamma> / 2)) + complex_of_real (sin (\<theta>\<^sub>A / 2) * sin (\<theta>\<^sub>B / 2)) * \<i> * complex_of_real (sin (\<gamma> / 2))) + - \<i> * complex_of_real (sin (\<gamma> / 2)) * (complex_of_real (sin (\<theta>\<^sub>A / 2) * sin (\<theta>\<^sub>B / 2) * cos (\<gamma> / 2)) + exp (- \<i> * complex_of_real \<phi>\<^sub>A) * complex_of_real (cos (\<theta>\<^sub>A / 2)) * exp (- \<i> * complex_of_real \<phi>\<^sub>B) * complex_of_real (cos (\<theta>\<^sub>B / 2)) * \<i> * complex_of_real (sin (\<gamma> / 2))), complex_of_real (cos (\<gamma> / 2)) * (exp (\<i> * complex_of_real \<phi>\<^sub>A) * complex_of_real (cos (\<theta>\<^sub>A / 2)) * complex_of_real (- sin (\<theta>\<^sub>B / 2)) * complex_of_real (cos (\<gamma> / 2)) + complex_of_real (sin (\<theta>\<^sub>A / 2)) * exp (- \<i> * complex_of_real \<phi>\<^sub>B) * complex_of_real (cos (\<theta>\<^sub>B / 2)) * \<i> * complex_of_real (sin (\<gamma> / 2))) + \<i> * complex_of_real (sin (\<gamma> / 2)) * (complex_of_real (- sin (\<theta>\<^sub>A / 2)) * exp (\<i> * complex_of_real \<phi>\<^sub>B) * complex_of_real (cos (\<theta>\<^sub>B / 2)) * complex_of_real (cos (\<gamma> / 2)) + exp (- \<i> * complex_of_real \<phi>\<^sub>A) * complex_of_real (cos (\<theta>\<^sub>A / 2)) * complex_of_real (sin (\<theta>\<^sub>B / 2)) * \<i> * complex_of_real (sin (\<gamma> / 2))), \<i> * complex_of_real (sin (\<gamma> / 2)) * (exp (\<i> * complex_of_real \<phi>\<^sub>A) * complex_of_real (cos (\<theta>\<^sub>A / 2)) * complex_of_real (- sin (\<theta>\<^sub>B / 2)) * complex_of_real (cos (\<gamma> / 2)) + complex_of_real (sin (\<theta>\<^sub>A / 2)) * exp (- \<i> * complex_of_real \<phi>\<^sub>B) * complex_of_real (cos (\<theta>\<^sub>B / 2)) * \<i> * complex_of_real (sin (\<gamma> / 2))) + complex_of_real (cos (\<gamma> / 2)) * (complex_of_real (- sin (\<theta>\<^sub>A / 2)) * exp (\<i> * complex_of_real \<phi>\<^sub>B) * complex_of_real (cos (\<theta>\<^sub>B / 2)) * complex_of_real (cos (\<gamma> / 2)) + exp (- \<i> * complex_of_real \<phi>\<^sub>A) * complex_of_real (cos (\<theta>\<^sub>A / 2)) * complex_of_real (sin (\<theta>\<^sub>B / 2)) * \<i> * complex_of_real (sin (\<gamma> / 2))), - \<i> * complex_of_real (sin (\<gamma> / 2)) * (exp (\<i> * complex_of_real \<phi>\<^sub>A) * complex_of_real (cos (\<theta>\<^sub>A / 2)) * exp (\<i> * complex_of_real \<phi>\<^sub>B) * complex_of_real (cos (\<theta>\<^sub>B / 2)) * complex_of_real (cos (\<gamma> / 2)) + complex_of_real (sin (\<theta>\<^sub>A / 2) * sin (\<theta>\<^sub>B / 2)) * \<i> * complex_of_real (sin (\<gamma> / 2))) + complex_of_real (cos (\<gamma> / 2)) * (complex_of_real (sin (\<theta>\<^sub>A / 2) * sin (\<theta>\<^sub>B / 2) * cos (\<gamma> / 2)) + exp (- \<i> * complex_of_real \<phi>\<^sub>A) * complex_of_real (cos (\<theta>\<^sub>A / 2)) * exp (- \<i> * complex_of_real \<phi>\<^sub>B) * complex_of_real (cos (\<theta>\<^sub>B / 2)) * \<i> * complex_of_real (sin (\<gamma> / 2)))]] $$ (3, 0)))\<^sup>2 else undefined) + 0 * (if state 2 (Tensor.mat_of_cols_list 4 [[complex_of_real (cos (\<gamma> / 2)) * (exp (\<i> * complex_of_real \<phi>\<^sub>A) * complex_of_real (cos (\<theta>\<^sub>A / 2)) * exp (\<i> * complex_of_real \<phi>\<^sub>B) * complex_of_real (cos (\<theta>\<^sub>B / 2)) * complex_of_real (cos (\<gamma> / 2)) + complex_of_real (sin (\<theta>\<^sub>A / 2) * sin (\<theta>\<^sub>B / 2)) * \<i> * complex_of_real (sin (\<gamma> / 2))) + - \<i> * complex_of_real (sin (\<gamma> / 2)) * (complex_of_real (sin (\<theta>\<^sub>A / 2) * sin (\<theta>\<^sub>B / 2) * cos (\<gamma> / 2)) + exp (- \<i> * complex_of_real \<phi>\<^sub>A) * complex_of_real (cos (\<theta>\<^sub>A / 2)) * exp (- \<i> * complex_of_real \<phi>\<^sub>B) * complex_of_real (cos (\<theta>\<^sub>B / 2)) * \<i> * complex_of_real (sin (\<gamma> / 2))), complex_of_real (cos (\<gamma> / 2)) * (exp (\<i> * complex_of_real \<phi>\<^sub>A) * complex_of_real (cos (\<theta>\<^sub>A / 2)) * complex_of_real (- sin (\<theta>\<^sub>B / 2)) * complex_of_real (cos (\<gamma> / 2)) + complex_of_real (sin (\<theta>\<^sub>A / 2)) * exp (- \<i> * complex_of_real \<phi>\<^sub>B) * complex_of_real (cos (\<theta>\<^sub>B / 2)) * \<i> * complex_of_real (sin (\<gamma> / 2))) + \<i> * complex_of_real (sin (\<gamma> / 2)) * (complex_of_real (- sin (\<theta>\<^sub>A / 2)) * exp (\<i> * complex_of_real \<phi>\<^sub>B) * complex_of_real (cos (\<theta>\<^sub>B / 2)) * complex_of_real (cos (\<gamma> / 2)) + exp (- \<i> * complex_of_real \<phi>\<^sub>A) * complex_of_real (cos (\<theta>\<^sub>A / 2)) * complex_of_real (sin (\<theta>\<^sub>B / 2)) * \<i> * complex_of_real (sin (\<gamma> / 2))), \<i> * complex_of_real (sin (\<gamma> / 2)) * (exp (\<i> * complex_of_real \<phi>\<^sub>A) * complex_of_real (cos (\<theta>\<^sub>A / 2)) * complex_of_real (- sin (\<theta>\<^sub>B / 2)) * complex_of_real (cos (\<gamma> / 2)) + complex_of_real (sin (\<theta>\<^sub>A / 2)) * exp (- \<i> * complex_of_real \<phi>\<^sub>B) * complex_of_real (cos (\<theta>\<^sub>B / 2)) * \<i> * complex_of_real (sin (\<gamma> / 2))) + complex_of_real (cos (\<gamma> / 2)) * (complex_of_real (- sin (\<theta>\<^sub>A / 2)) * exp (\<i> * complex_of_real \<phi>\<^sub>B) * complex_of_real (cos (\<theta>\<^sub>B / 2)) * complex_of_real (cos (\<gamma> / 2)) + exp (- \<i> * complex_of_real \<phi>\<^sub>A) * complex_of_real (cos (\<theta>\<^sub>A / 2)) * complex_of_real (sin (\<theta>\<^sub>B / 2)) * \<i> * complex_of_real (sin (\<gamma> / 2))), - \<i> * complex_of_real (sin (\<gamma> / 2)) * (exp (\<i> * complex_of_real \<phi>\<^sub>A) * complex_of_real (cos (\<theta>\<^sub>A / 2)) * exp (\<i> * complex_of_real \<phi>\<^sub>B) * complex_of_real (cos (\<theta>\<^sub>B / 2)) * complex_of_real (cos (\<gamma> / 2)) + complex_of_real (sin (\<theta>\<^sub>A / 2) * sin (\<theta>\<^sub>B / 2)) * \<i> * complex_of_real (sin (\<gamma> / 2))) + complex_of_real (cos (\<gamma> / 2)) * (complex_of_real (sin (\<theta>\<^sub>A / 2) * sin (\<theta>\<^sub>B / 2) * cos (\<gamma> / 2)) + exp (- \<i> * complex_of_real \<phi>\<^sub>A) * complex_of_real (cos (\<theta>\<^sub>A / 2)) * exp (- \<i> * complex_of_real \<phi>\<^sub>B) * complex_of_real (cos (\<theta>\<^sub>B / 2)) * \<i> * complex_of_real (sin (\<gamma> / 2)))]]) then (cmod (Tensor.mat_of_cols_list 4 [[complex_of_real (cos (\<gamma> / 2)) * (exp (\<i> * complex_of_real \<phi>\<^sub>A) * complex_of_real (cos (\<theta>\<^sub>A / 2)) * exp (\<i> * complex_of_real \<phi>\<^sub>B) * complex_of_real (cos (\<theta>\<^sub>B / 2)) * complex_of_real (cos (\<gamma> / 2)) + complex_of_real (sin (\<theta>\<^sub>A / 2) * sin (\<theta>\<^sub>B / 2)) * \<i> * complex_of_real (sin (\<gamma> / 2))) + - \<i> * complex_of_real (sin (\<gamma> / 2)) * (complex_of_real (sin (\<theta>\<^sub>A / 2) * sin (\<theta>\<^sub>B / 2) * cos (\<gamma> / 2)) + exp (- \<i> * complex_of_real \<phi>\<^sub>A) * complex_of_real (cos (\<theta>\<^sub>A / 2)) * exp (- \<i> * complex_of_real \<phi>\<^sub>B) * complex_of_real (cos (\<theta>\<^sub>B / 2)) * \<i> * complex_of_real (sin (\<gamma> / 2))), complex_of_real (cos (\<gamma> / 2)) * (exp (\<i> * complex_of_real \<phi>\<^sub>A) * complex_of_real (cos (\<theta>\<^sub>A / 2)) * complex_of_real (- sin (\<theta>\<^sub>B / 2)) * complex_of_real (cos (\<gamma> / 2)) + complex_of_real (sin (\<theta>\<^sub>A / 2)) * exp (- \<i> * complex_of_real \<phi>\<^sub>B) * complex_of_real (cos (\<theta>\<^sub>B / 2)) * \<i> * complex_of_real (sin (\<gamma> / 2))) + \<i> * complex_of_real (sin (\<gamma> / 2)) * (complex_of_real (- sin (\<theta>\<^sub>A / 2)) * exp (\<i> * complex_of_real \<phi>\<^sub>B) * complex_of_real (cos (\<theta>\<^sub>B / 2)) * complex_of_real (cos (\<gamma> / 2)) + exp (- \<i> * complex_of_real \<phi>\<^sub>A) * complex_of_real (cos (\<theta>\<^sub>A / 2)) * complex_of_real (sin (\<theta>\<^sub>B / 2)) * \<i> * complex_of_real (sin (\<gamma> / 2))), \<i> * complex_of_real (sin (\<gamma> / 2)) * (exp (\<i> * complex_of_real \<phi>\<^sub>A) * complex_of_real (cos (\<theta>\<^sub>A / 2)) * complex_of_real (- sin (\<theta>\<^sub>B / 2)) * complex_of_real (cos (\<gamma> / 2)) + complex_of_real (sin (\<theta>\<^sub>A / 2)) * exp (- \<i> * complex_of_real \<phi>\<^sub>B) * complex_of_real (cos (\<theta>\<^sub>B / 2)) * \<i> * complex_of_real (sin (\<gamma> / 2))) + complex_of_real (cos (\<gamma> / 2)) * (complex_of_real (- sin (\<theta>\<^sub>A / 2)) * exp (\<i> * complex_of_real \<phi>\<^sub>B) * complex_of_real (cos (\<theta>\<^sub>B / 2)) * complex_of_real (cos (\<gamma> / 2)) + exp (- \<i> * complex_of_real \<phi>\<^sub>A) * complex_of_real (cos (\<theta>\<^sub>A / 2)) * complex_of_real (sin (\<theta>\<^sub>B / 2)) * \<i> * complex_of_real (sin (\<gamma> / 2))), - \<i> * complex_of_real (sin (\<gamma> / 2)) * (exp (\<i> * complex_of_real \<phi>\<^sub>A) * complex_of_real (cos (\<theta>\<^sub>A / 2)) * exp (\<i> * complex_of_real \<phi>\<^sub>B) * complex_of_real (cos (\<theta>\<^sub>B / 2)) * complex_of_real (cos (\<gamma> / 2)) + complex_of_real (sin (\<theta>\<^sub>A / 2) * sin (\<theta>\<^sub>B / 2)) * \<i> * complex_of_real (sin (\<gamma> / 2))) + complex_of_real (cos (\<gamma> / 2)) * (complex_of_real (sin (\<theta>\<^sub>A / 2) * sin (\<theta>\<^sub>B / 2) * cos (\<gamma> / 2)) + exp (- \<i> * complex_of_real \<phi>\<^sub>A) * complex_of_real (cos (\<theta>\<^sub>A / 2)) * exp (- \<i> * complex_of_real \<phi>\<^sub>B) * complex_of_real (cos (\<theta>\<^sub>B / 2)) * \<i> * complex_of_real (sin (\<gamma> / 2)))]] $$ (1, 0)))\<^sup>2 else undefined) + 5 * (if state 2 (Tensor.mat_of_cols_list 4 [[complex_of_real (cos (\<gamma> / 2)) * (exp (\<i> * complex_of_real \<phi>\<^sub>A) * complex_of_real (cos (\<theta>\<^sub>A / 2)) * exp (\<i> * complex_of_real \<phi>\<^sub>B) * complex_of_real (cos (\<theta>\<^sub>B / 2)) * complex_of_real (cos (\<gamma> / 2)) + complex_of_real (sin (\<theta>\<^sub>A / 2) * sin (\<theta>\<^sub>B / 2)) * \<i> * complex_of_real (sin (\<gamma> / 2))) + - \<i> * complex_of_real (sin (\<gamma> / 2)) * (complex_of_real (sin (\<theta>\<^sub>A / 2) * sin (\<theta>\<^sub>B / 2) * cos (\<gamma> / 2)) + exp (- \<i> * complex_of_real \<phi>\<^sub>A) * complex_of_real (cos (\<theta>\<^sub>A / 2)) * exp (- \<i> * complex_of_real \<phi>\<^sub>B) * complex_of_real (cos (\<theta>\<^sub>B / 2)) * \<i> * complex_of_real (sin (\<gamma> / 2))), complex_of_real (cos (\<gamma> / 2)) * (exp (\<i> * complex_of_real \<phi>\<^sub>A) * complex_of_real (cos (\<theta>\<^sub>A / 2)) * complex_of_real (- sin (\<theta>\<^sub>B / 2)) * complex_of_real (cos (\<gamma> / 2)) + complex_of_real (sin (\<theta>\<^sub>A / 2)) * exp (- \<i> * complex_of_real \<phi>\<^sub>B) * complex_of_real (cos (\<theta>\<^sub>B / 2)) * \<i> * complex_of_real (sin (\<gamma> / 2))) + \<i> * complex_of_real (sin (\<gamma> / 2)) * (complex_of_real (- sin (\<theta>\<^sub>A / 2)) * exp (\<i> * complex_of_real \<phi>\<^sub>B) * complex_of_real (cos (\<theta>\<^sub>B / 2)) * complex_of_real (cos (\<gamma> / 2)) + exp (- \<i> * complex_of_real \<phi>\<^sub>A) * complex_of_real (cos (\<theta>\<^sub>A / 2)) * complex_of_real (sin (\<theta>\<^sub>B / 2)) * \<i> * complex_of_real (sin (\<gamma> / 2))), \<i> * complex_of_real (sin (\<gamma> / 2)) * (exp (\<i> * complex_of_real \<phi>\<^sub>A) * complex_of_real (cos (\<theta>\<^sub>A / 2)) * complex_of_real (- sin (\<theta>\<^sub>B / 2)) * complex_of_real (cos (\<gamma> / 2)) + complex_of_real (sin (\<theta>\<^sub>A / 2)) * exp (- \<i> * complex_of_real \<phi>\<^sub>B) * complex_of_real (cos (\<theta>\<^sub>B / 2)) * \<i> * complex_of_real (sin (\<gamma> / 2))) + complex_of_real (cos (\<gamma> / 2)) * (complex_of_real (- sin (\<theta>\<^sub>A / 2)) * exp (\<i> * complex_of_real \<phi>\<^sub>B) * complex_of_real (cos (\<theta>\<^sub>B / 2)) * complex_of_real (cos (\<gamma> / 2)) + exp (- \<i> * complex_of_real \<phi>\<^sub>A) * complex_of_real (cos (\<theta>\<^sub>A / 2)) * complex_of_real (sin (\<theta>\<^sub>B / 2)) * \<i> * complex_of_real (sin (\<gamma> / 2))), - \<i> * complex_of_real (sin (\<gamma> / 2)) * (exp (\<i> * complex_of_real \<phi>\<^sub>A) * complex_of_real (cos (\<theta>\<^sub>A / 2)) * exp (\<i> * complex_of_real \<phi>\<^sub>B) * complex_of_real (cos (\<theta>\<^sub>B / 2)) * complex_of_real (cos (\<gamma> / 2)) + complex_of_real (sin (\<theta>\<^sub>A / 2) * sin (\<theta>\<^sub>B / 2)) * \<i> * complex_of_real (sin (\<gamma> / 2))) + complex_of_real (cos (\<gamma> / 2)) * (complex_of_real (sin (\<theta>\<^sub>A / 2) * sin (\<theta>\<^sub>B / 2) * cos (\<gamma> / 2)) + exp (- \<i> * complex_of_real \<phi>\<^sub>A) * complex_of_real (cos (\<theta>\<^sub>A / 2)) * exp (- \<i> * complex_of_real \<phi>\<^sub>B) * complex_of_real (cos (\<theta>\<^sub>B / 2)) * \<i> * complex_of_real (sin (\<gamma> / 2)))]]) then (cmod (Tensor.mat_of_cols_list 4 [[complex_of_real (cos (\<gamma> / 2)) * (exp (\<i> * complex_of_real \<phi>\<^sub>A) * complex_of_real (cos (\<theta>\<^sub>A / 2)) * exp (\<i> * complex_of_real \<phi>\<^sub>B) * complex_of_real (cos (\<theta>\<^sub>B / 2)) * complex_of_real (cos (\<gamma> / 2)) + complex_of_real (sin (\<theta>\<^sub>A / 2) * sin (\<theta>\<^sub>B / 2)) * \<i> * complex_of_real (sin (\<gamma> / 2))) + - \<i> * complex_of_real (sin (\<gamma> / 2)) * (complex_of_real (sin (\<theta>\<^sub>A / 2) * sin (\<theta>\<^sub>B / 2) * cos (\<gamma> / 2)) + exp (- \<i> * complex_of_real \<phi>\<^sub>A) * complex_of_real (cos (\<theta>\<^sub>A / 2)) * exp (- \<i> * complex_of_real \<phi>\<^sub>B) * complex_of_real (cos (\<theta>\<^sub>B / 2)) * \<i> * complex_of_real (sin (\<gamma> / 2))), complex_of_real (cos (\<gamma> / 2)) * (exp (\<i> * complex_of_real \<phi>\<^sub>A) * complex_of_real (cos (\<theta>\<^sub>A / 2)) * complex_of_real (- sin (\<theta>\<^sub>B / 2)) * complex_of_real (cos (\<gamma> / 2)) + complex_of_real (sin (\<theta>\<^sub>A / 2)) * exp (- \<i> * complex_of_real \<phi>\<^sub>B) * complex_of_real (cos (\<theta>\<^sub>B / 2)) * \<i> * complex_of_real (sin (\<gamma> / 2))) + \<i> * complex_of_real (sin (\<gamma> / 2)) * (complex_of_real (- sin (\<theta>\<^sub>A / 2)) * exp (\<i> * complex_of_real \<phi>\<^sub>B) * complex_of_real (cos (\<theta>\<^sub>B / 2)) * complex_of_real (cos (\<gamma> / 2)) + exp (- \<i> * complex_of_real \<phi>\<^sub>A) * complex_of_real (cos (\<theta>\<^sub>A / 2)) * complex_of_real (sin (\<theta>\<^sub>B / 2)) * \<i> * complex_of_real (sin (\<gamma> / 2))), \<i> * complex_of_real (sin (\<gamma> / 2)) * (exp (\<i> * complex_of_real \<phi>\<^sub>A) * complex_of_real (cos (\<theta>\<^sub>A / 2)) * complex_of_real (- sin (\<theta>\<^sub>B / 2)) * complex_of_real (cos (\<gamma> / 2)) + complex_of_real (sin (\<theta>\<^sub>A / 2)) * exp (- \<i> * complex_of_real \<phi>\<^sub>B) * complex_of_real (cos (\<theta>\<^sub>B / 2)) * \<i> * complex_of_real (sin (\<gamma> / 2))) + complex_of_real (cos (\<gamma> / 2)) * (complex_of_real (- sin (\<theta>\<^sub>A / 2)) * exp (\<i> * complex_of_real \<phi>\<^sub>B) * complex_of_real (cos (\<theta>\<^sub>B / 2)) * complex_of_real (cos (\<gamma> / 2)) + exp (- \<i> * complex_of_real \<phi>\<^sub>A) * complex_of_real (cos (\<theta>\<^sub>A / 2)) * complex_of_real (sin (\<theta>\<^sub>B / 2)) * \<i> * complex_of_real (sin (\<gamma> / 2))), - \<i> * complex_of_real (sin (\<gamma> / 2)) * (exp (\<i> * complex_of_real \<phi>\<^sub>A) * complex_of_real (cos (\<theta>\<^sub>A / 2)) * exp (\<i> * complex_of_real \<phi>\<^sub>B) * complex_of_real (cos (\<theta>\<^sub>B / 2)) * complex_of_real (cos (\<gamma> / 2)) + complex_of_real (sin (\<theta>\<^sub>A / 2) * sin (\<theta>\<^sub>B / 2)) * \<i> * complex_of_real (sin (\<gamma> / 2))) + complex_of_real (cos (\<gamma> / 2)) * (complex_of_real (sin (\<theta>\<^sub>A / 2) * sin (\<theta>\<^sub>B / 2) * cos (\<gamma> / 2)) + exp (- \<i> * complex_of_real \<phi>\<^sub>A) * complex_of_real (cos (\<theta>\<^sub>A / 2)) * exp (- \<i> * complex_of_real \<phi>\<^sub>B) * complex_of_real (cos (\<theta>\<^sub>B / 2)) * \<i> * complex_of_real (sin (\<gamma> / 2)))]] $$ (2, 0)))\<^sup>2 else undefined)
bob_payoff \<equiv> 3 * (if state 2 (Tensor.mat_of_cols_list 4 [[complex_of_real (cos (\<gamma> / 2)) * (exp (\<i> * complex_of_real \<phi>\<^sub>A) * complex_of_real (cos (\<theta>\<^sub>A / 2)) * exp (\<i> * complex_of_real \<phi>\<^sub>B) * complex_of_real (cos (\<theta>\<^sub>B / 2)) * complex_of_real (cos (\<gamma> / 2)) + complex_of_real (sin (\<theta>\<^sub>A / 2) * sin (\<theta>\<^sub>B / 2)) * \<i> * complex_of_real (sin (\<gamma> / 2))) + - \<i> * complex_of_real (sin (\<gamma> / 2)) * (complex_of_real (sin (\<theta>\<^sub>A / 2) * sin (\<theta>\<^sub>B / 2) * cos (\<gamma> / 2)) + exp (- \<i> * complex_of_real \<phi>\<^sub>A) * complex_of_real (cos (\<theta>\<^sub>A / 2)) * exp (- \<i> * complex_of_real \<phi>\<^sub>B) * complex_of_real (cos (\<theta>\<^sub>B / 2)) * \<i> * complex_of_real (sin (\<gamma> / 2))), complex_of_real (cos (\<gamma> / 2)) * (exp (\<i> * complex_of_real \<phi>\<^sub>A) * complex_of_real (cos (\<theta>\<^sub>A / 2)) * complex_of_real (- sin (\<theta>\<^sub>B / 2)) * complex_of_real (cos (\<gamma> / 2)) + complex_of_real (sin (\<theta>\<^sub>A / 2)) * exp (- \<i> * complex_of_real \<phi>\<^sub>B) * complex_of_real (cos (\<theta>\<^sub>B / 2)) * \<i> * complex_of_real (sin (\<gamma> / 2))) + \<i> * complex_of_real (sin (\<gamma> / 2)) * (complex_of_real (- sin (\<theta>\<^sub>A / 2)) * exp (\<i> * complex_of_real \<phi>\<^sub>B) * complex_of_real (cos (\<theta>\<^sub>B / 2)) * complex_of_real (cos (\<gamma> / 2)) + exp (- \<i> * complex_of_real \<phi>\<^sub>A) * complex_of_real (cos (\<theta>\<^sub>A / 2)) * complex_of_real (sin (\<theta>\<^sub>B / 2)) * \<i> * complex_of_real (sin (\<gamma> / 2))), \<i> * complex_of_real (sin (\<gamma> / 2)) * (exp (\<i> * complex_of_real \<phi>\<^sub>A) * complex_of_real (cos (\<theta>\<^sub>A / 2)) * complex_of_real (- sin (\<theta>\<^sub>B / 2)) * complex_of_real (cos (\<gamma> / 2)) + complex_of_real (sin (\<theta>\<^sub>A / 2)) * exp (- \<i> * complex_of_real \<phi>\<^sub>B) * complex_of_real (cos (\<theta>\<^sub>B / 2)) * \<i> * complex_of_real (sin (\<gamma> / 2))) + complex_of_real (cos (\<gamma> / 2)) * (complex_of_real (- sin (\<theta>\<^sub>A / 2)) * exp (\<i> * complex_of_real \<phi>\<^sub>B) * complex_of_real (cos (\<theta>\<^sub>B / 2)) * complex_of_real (cos (\<gamma> / 2)) + exp (- \<i> * complex_of_real \<phi>\<^sub>A) * complex_of_real (cos (\<theta>\<^sub>A / 2)) * complex_of_real (sin (\<theta>\<^sub>B / 2)) * \<i> * complex_of_real (sin (\<gamma> / 2))), - \<i> * complex_of_real (sin (\<gamma> / 2)) * (exp (\<i> * complex_of_real \<phi>\<^sub>A) * complex_of_real (cos (\<theta>\<^sub>A / 2)) * exp (\<i> * complex_of_real \<phi>\<^sub>B) * complex_of_real (cos (\<theta>\<^sub>B / 2)) * complex_of_real (cos (\<gamma> / 2)) + complex_of_real (sin (\<theta>\<^sub>A / 2) * sin (\<theta>\<^sub>B / 2)) * \<i> * complex_of_real (sin (\<gamma> / 2))) + complex_of_real (cos (\<gamma> / 2)) * (complex_of_real (sin (\<theta>\<^sub>A / 2) * sin (\<theta>\<^sub>B / 2) * cos (\<gamma> / 2)) + exp (- \<i> * complex_of_real \<phi>\<^sub>A) * complex_of_real (cos (\<theta>\<^sub>A / 2)) * exp (- \<i> * complex_of_real \<phi>\<^sub>B) * complex_of_real (cos (\<theta>\<^sub>B / 2)) * \<i> * complex_of_real (sin (\<gamma> / 2)))]]) then (cmod (Tensor.mat_of_cols_list 4 [[complex_of_real (cos (\<gamma> / 2)) * (exp (\<i> * complex_of_real \<phi>\<^sub>A) * complex_of_real (cos (\<theta>\<^sub>A / 2)) * exp (\<i> * complex_of_real \<phi>\<^sub>B) * complex_of_real (cos (\<theta>\<^sub>B / 2)) * complex_of_real (cos (\<gamma> / 2)) + complex_of_real (sin (\<theta>\<^sub>A / 2) * sin (\<theta>\<^sub>B / 2)) * \<i> * complex_of_real (sin (\<gamma> / 2))) + - \<i> * complex_of_real (sin (\<gamma> / 2)) * (complex_of_real (sin (\<theta>\<^sub>A / 2) * sin (\<theta>\<^sub>B / 2) * cos (\<gamma> / 2)) + exp (- \<i> * complex_of_real \<phi>\<^sub>A) * complex_of_real (cos (\<theta>\<^sub>A / 2)) * exp (- \<i> * complex_of_real \<phi>\<^sub>B) * complex_of_real (cos (\<theta>\<^sub>B / 2)) * \<i> * complex_of_real (sin (\<gamma> / 2))), complex_of_real (cos (\<gamma> / 2)) * (exp (\<i> * complex_of_real \<phi>\<^sub>A) * complex_of_real (cos (\<theta>\<^sub>A / 2)) * complex_of_real (- sin (\<theta>\<^sub>B / 2)) * complex_of_real (cos (\<gamma> / 2)) + complex_of_real (sin (\<theta>\<^sub>A / 2)) * exp (- \<i> * complex_of_real \<phi>\<^sub>B) * complex_of_real (cos (\<theta>\<^sub>B / 2)) * \<i> * complex_of_real (sin (\<gamma> / 2))) + \<i> * complex_of_real (sin (\<gamma> / 2)) * (complex_of_real (- sin (\<theta>\<^sub>A / 2)) * exp (\<i> * complex_of_real \<phi>\<^sub>B) * complex_of_real (cos (\<theta>\<^sub>B / 2)) * complex_of_real (cos (\<gamma> / 2)) + exp (- \<i> * complex_of_real \<phi>\<^sub>A) * complex_of_real (cos (\<theta>\<^sub>A / 2)) * complex_of_real (sin (\<theta>\<^sub>B / 2)) * \<i> * complex_of_real (sin (\<gamma> / 2))), \<i> * complex_of_real (sin (\<gamma> / 2)) * (exp (\<i> * complex_of_real \<phi>\<^sub>A) * complex_of_real (cos (\<theta>\<^sub>A / 2)) * complex_of_real (- sin (\<theta>\<^sub>B / 2)) * complex_of_real (cos (\<gamma> / 2)) + complex_of_real (sin (\<theta>\<^sub>A / 2)) * exp (- \<i> * complex_of_real \<phi>\<^sub>B) * complex_of_real (cos (\<theta>\<^sub>B / 2)) * \<i> * complex_of_real (sin (\<gamma> / 2))) + complex_of_real (cos (\<gamma> / 2)) * (complex_of_real (- sin (\<theta>\<^sub>A / 2)) * exp (\<i> * complex_of_real \<phi>\<^sub>B) * complex_of_real (cos (\<theta>\<^sub>B / 2)) * complex_of_real (cos (\<gamma> / 2)) + exp (- \<i> * complex_of_real \<phi>\<^sub>A) * complex_of_real (cos (\<theta>\<^sub>A / 2)) * complex_of_real (sin (\<theta>\<^sub>B / 2)) * \<i> * complex_of_real (sin (\<gamma> / 2))), - \<i> * complex_of_real (sin (\<gamma> / 2)) * (exp (\<i> * complex_of_real \<phi>\<^sub>A) * complex_of_real (cos (\<theta>\<^sub>A / 2)) * exp (\<i> * complex_of_real \<phi>\<^sub>B) * complex_of_real (cos (\<theta>\<^sub>B / 2)) * complex_of_real (cos (\<gamma> / 2)) + complex_of_real (sin (\<theta>\<^sub>A / 2) * sin (\<theta>\<^sub>B / 2)) * \<i> * complex_of_real (sin (\<gamma> / 2))) + complex_of_real (cos (\<gamma> / 2)) * (complex_of_real (sin (\<theta>\<^sub>A / 2) * sin (\<theta>\<^sub>B / 2) * cos (\<gamma> / 2)) + exp (- \<i> * complex_of_real \<phi>\<^sub>A) * complex_of_real (cos (\<theta>\<^sub>A / 2)) * exp (- \<i> * complex_of_real \<phi>\<^sub>B) * complex_of_real (cos (\<theta>\<^sub>B / 2)) * \<i> * complex_of_real (sin (\<gamma> / 2)))]] $$ (0, 0)))\<^sup>2 else undefined) + 1 * (if state 2 (Tensor.mat_of_cols_list 4 [[complex_of_real (cos (\<gamma> / 2)) * (exp (\<i> * complex_of_real \<phi>\<^sub>A) * complex_of_real (cos (\<theta>\<^sub>A / 2)) * exp (\<i> * complex_of_real \<phi>\<^sub>B) * complex_of_real (cos (\<theta>\<^sub>B / 2)) * complex_of_real (cos (\<gamma> / 2)) + complex_of_real (sin (\<theta>\<^sub>A / 2) * sin (\<theta>\<^sub>B / 2)) * \<i> * complex_of_real (sin (\<gamma> / 2))) + - \<i> * complex_of_real (sin (\<gamma> / 2)) * (complex_of_real (sin (\<theta>\<^sub>A / 2) * sin (\<theta>\<^sub>B / 2) * cos (\<gamma> / 2)) + exp (- \<i> * complex_of_real \<phi>\<^sub>A) * complex_of_real (cos (\<theta>\<^sub>A / 2)) * exp (- \<i> * complex_of_real \<phi>\<^sub>B) * complex_of_real (cos (\<theta>\<^sub>B / 2)) * \<i> * complex_of_real (sin (\<gamma> / 2))), complex_of_real (cos (\<gamma> / 2)) * (exp (\<i> * complex_of_real \<phi>\<^sub>A) * complex_of_real (cos (\<theta>\<^sub>A / 2)) * complex_of_real (- sin (\<theta>\<^sub>B / 2)) * complex_of_real (cos (\<gamma> / 2)) + complex_of_real (sin (\<theta>\<^sub>A / 2)) * exp (- \<i> * complex_of_real \<phi>\<^sub>B) * complex_of_real (cos (\<theta>\<^sub>B / 2)) * \<i> * complex_of_real (sin (\<gamma> / 2))) + \<i> * complex_of_real (sin (\<gamma> / 2)) * (complex_of_real (- sin (\<theta>\<^sub>A / 2)) * exp (\<i> * complex_of_real \<phi>\<^sub>B) * complex_of_real (cos (\<theta>\<^sub>B / 2)) * complex_of_real (cos (\<gamma> / 2)) + exp (- \<i> * complex_of_real \<phi>\<^sub>A) * complex_of_real (cos (\<theta>\<^sub>A / 2)) * complex_of_real (sin (\<theta>\<^sub>B / 2)) * \<i> * complex_of_real (sin (\<gamma> / 2))), \<i> * complex_of_real (sin (\<gamma> / 2)) * (exp (\<i> * complex_of_real \<phi>\<^sub>A) * complex_of_real (cos (\<theta>\<^sub>A / 2)) * complex_of_real (- sin (\<theta>\<^sub>B / 2)) * complex_of_real (cos (\<gamma> / 2)) + complex_of_real (sin (\<theta>\<^sub>A / 2)) * exp (- \<i> * complex_of_real \<phi>\<^sub>B) * complex_of_real (cos (\<theta>\<^sub>B / 2)) * \<i> * complex_of_real (sin (\<gamma> / 2))) + complex_of_real (cos (\<gamma> / 2)) * (complex_of_real (- sin (\<theta>\<^sub>A / 2)) * exp (\<i> * complex_of_real \<phi>\<^sub>B) * complex_of_real (cos (\<theta>\<^sub>B / 2)) * complex_of_real (cos (\<gamma> / 2)) + exp (- \<i> * complex_of_real \<phi>\<^sub>A) * complex_of_real (cos (\<theta>\<^sub>A / 2)) * complex_of_real (sin (\<theta>\<^sub>B / 2)) * \<i> * complex_of_real (sin (\<gamma> / 2))), - \<i> * complex_of_real (sin (\<gamma> / 2)) * (exp (\<i> * complex_of_real \<phi>\<^sub>A) * complex_of_real (cos (\<theta>\<^sub>A / 2)) * exp (\<i> * complex_of_real \<phi>\<^sub>B) * complex_of_real (cos (\<theta>\<^sub>B / 2)) * complex_of_real (cos (\<gamma> / 2)) + complex_of_real (sin (\<theta>\<^sub>A / 2) * sin (\<theta>\<^sub>B / 2)) * \<i> * complex_of_real (sin (\<gamma> / 2))) + complex_of_real (cos (\<gamma> / 2)) * (complex_of_real (sin (\<theta>\<^sub>A / 2) * sin (\<theta>\<^sub>B / 2) * cos (\<gamma> / 2)) + exp (- \<i> * complex_of_real \<phi>\<^sub>A) * complex_of_real (cos (\<theta>\<^sub>A / 2)) * exp (- \<i> * complex_of_real \<phi>\<^sub>B) * complex_of_real (cos (\<theta>\<^sub>B / 2)) * \<i> * complex_of_real (sin (\<gamma> / 2)))]]) then (cmod (Tensor.mat_of_cols_list 4 [[complex_of_real (cos (\<gamma> / 2)) * (exp (\<i> * complex_of_real \<phi>\<^sub>A) * complex_of_real (cos (\<theta>\<^sub>A / 2)) * exp (\<i> * complex_of_real \<phi>\<^sub>B) * complex_of_real (cos (\<theta>\<^sub>B / 2)) * complex_of_real (cos (\<gamma> / 2)) + complex_of_real (sin (\<theta>\<^sub>A / 2) * sin (\<theta>\<^sub>B / 2)) * \<i> * complex_of_real (sin (\<gamma> / 2))) + - \<i> * complex_of_real (sin (\<gamma> / 2)) * (complex_of_real (sin (\<theta>\<^sub>A / 2) * sin (\<theta>\<^sub>B / 2) * cos (\<gamma> / 2)) + exp (- \<i> * complex_of_real \<phi>\<^sub>A) * complex_of_real (cos (\<theta>\<^sub>A / 2)) * exp (- \<i> * complex_of_real \<phi>\<^sub>B) * complex_of_real (cos (\<theta>\<^sub>B / 2)) * \<i> * complex_of_real (sin (\<gamma> / 2))), complex_of_real (cos (\<gamma> / 2)) * (exp (\<i> * complex_of_real \<phi>\<^sub>A) * complex_of_real (cos (\<theta>\<^sub>A / 2)) * complex_of_real (- sin (\<theta>\<^sub>B / 2)) * complex_of_real (cos (\<gamma> / 2)) + complex_of_real (sin (\<theta>\<^sub>A / 2)) * exp (- \<i> * complex_of_real \<phi>\<^sub>B) * complex_of_real (cos (\<theta>\<^sub>B / 2)) * \<i> * complex_of_real (sin (\<gamma> / 2))) + \<i> * complex_of_real (sin (\<gamma> / 2)) * (complex_of_real (- sin (\<theta>\<^sub>A / 2)) * exp (\<i> * complex_of_real \<phi>\<^sub>B) * complex_of_real (cos (\<theta>\<^sub>B / 2)) * complex_of_real (cos (\<gamma> / 2)) + exp (- \<i> * complex_of_real \<phi>\<^sub>A) * complex_of_real (cos (\<theta>\<^sub>A / 2)) * complex_of_real (sin (\<theta>\<^sub>B / 2)) * \<i> * complex_of_real (sin (\<gamma> / 2))), \<i> * complex_of_real (sin (\<gamma> / 2)) * (exp (\<i> * complex_of_real \<phi>\<^sub>A) * complex_of_real (cos (\<theta>\<^sub>A / 2)) * complex_of_real (- sin (\<theta>\<^sub>B / 2)) * complex_of_real (cos (\<gamma> / 2)) + complex_of_real (sin (\<theta>\<^sub>A / 2)) * exp (- \<i> * complex_of_real \<phi>\<^sub>B) * complex_of_real (cos (\<theta>\<^sub>B / 2)) * \<i> * complex_of_real (sin (\<gamma> / 2))) + complex_of_real (cos (\<gamma> / 2)) * (complex_of_real (- sin (\<theta>\<^sub>A / 2)) * exp (\<i> * complex_of_real \<phi>\<^sub>B) * complex_of_real (cos (\<theta>\<^sub>B / 2)) * complex_of_real (cos (\<gamma> / 2)) + exp (- \<i> * complex_of_real \<phi>\<^sub>A) * complex_of_real (cos (\<theta>\<^sub>A / 2)) * complex_of_real (sin (\<theta>\<^sub>B / 2)) * \<i> * complex_of_real (sin (\<gamma> / 2))), - \<i> * complex_of_real (sin (\<gamma> / 2)) * (exp (\<i> * complex_of_real \<phi>\<^sub>A) * complex_of_real (cos (\<theta>\<^sub>A / 2)) * exp (\<i> * complex_of_real \<phi>\<^sub>B) * complex_of_real (cos (\<theta>\<^sub>B / 2)) * complex_of_real (cos (\<gamma> / 2)) + complex_of_real (sin (\<theta>\<^sub>A / 2) * sin (\<theta>\<^sub>B / 2)) * \<i> * complex_of_real (sin (\<gamma> / 2))) + complex_of_real (cos (\<gamma> / 2)) * (complex_of_real (sin (\<theta>\<^sub>A / 2) * sin (\<theta>\<^sub>B / 2) * cos (\<gamma> / 2)) + exp (- \<i> * complex_of_real \<phi>\<^sub>A) * complex_of_real (cos (\<theta>\<^sub>A / 2)) * exp (- \<i> * complex_of_real \<phi>\<^sub>B) * complex_of_real (cos (\<theta>\<^sub>B / 2)) * \<i> * complex_of_real (sin (\<gamma> / 2)))]] $$ (3, 0)))\<^sup>2 else undefined) + 5 * (if state 2 (Tensor.mat_of_cols_list 4 [[complex_of_real (cos (\<gamma> / 2)) * (exp (\<i> * complex_of_real \<phi>\<^sub>A) * complex_of_real (cos (\<theta>\<^sub>A / 2)) * exp (\<i> * complex_of_real \<phi>\<^sub>B) * complex_of_real (cos (\<theta>\<^sub>B / 2)) * complex_of_real (cos (\<gamma> / 2)) + complex_of_real (sin (\<theta>\<^sub>A / 2) * sin (\<theta>\<^sub>B / 2)) * \<i> * complex_of_real (sin (\<gamma> / 2))) + - \<i> * complex_of_real (sin (\<gamma> / 2)) * (complex_of_real (sin (\<theta>\<^sub>A / 2) * sin (\<theta>\<^sub>B / 2) * cos (\<gamma> / 2)) + exp (- \<i> * complex_of_real \<phi>\<^sub>A) * complex_of_real (cos (\<theta>\<^sub>A / 2)) * exp (- \<i> * complex_of_real \<phi>\<^sub>B) * complex_of_real (cos (\<theta>\<^sub>B / 2)) * \<i> * complex_of_real (sin (\<gamma> / 2))), complex_of_real (cos (\<gamma> / 2)) * (exp (\<i> * complex_of_real \<phi>\<^sub>A) * complex_of_real (cos (\<theta>\<^sub>A / 2)) * complex_of_real (- sin (\<theta>\<^sub>B / 2)) * complex_of_real (cos (\<gamma> / 2)) + complex_of_real (sin (\<theta>\<^sub>A / 2)) * exp (- \<i> * complex_of_real \<phi>\<^sub>B) * complex_of_real (cos (\<theta>\<^sub>B / 2)) * \<i> * complex_of_real (sin (\<gamma> / 2))) + \<i> * complex_of_real (sin (\<gamma> / 2)) * (complex_of_real (- sin (\<theta>\<^sub>A / 2)) * exp (\<i> * complex_of_real \<phi>\<^sub>B) * complex_of_real (cos (\<theta>\<^sub>B / 2)) * complex_of_real (cos (\<gamma> / 2)) + exp (- \<i> * complex_of_real \<phi>\<^sub>A) * complex_of_real (cos (\<theta>\<^sub>A / 2)) * complex_of_real (sin (\<theta>\<^sub>B / 2)) * \<i> * complex_of_real (sin (\<gamma> / 2))), \<i> * complex_of_real (sin (\<gamma> / 2)) * (exp (\<i> * complex_of_real \<phi>\<^sub>A) * complex_of_real (cos (\<theta>\<^sub>A / 2)) * complex_of_real (- sin (\<theta>\<^sub>B / 2)) * complex_of_real (cos (\<gamma> / 2)) + complex_of_real (sin (\<theta>\<^sub>A / 2)) * exp (- \<i> * complex_of_real \<phi>\<^sub>B) * complex_of_real (cos (\<theta>\<^sub>B / 2)) * \<i> * complex_of_real (sin (\<gamma> / 2))) + complex_of_real (cos (\<gamma> / 2)) * (complex_of_real (- sin (\<theta>\<^sub>A / 2)) * exp (\<i> * complex_of_real \<phi>\<^sub>B) * complex_of_real (cos (\<theta>\<^sub>B / 2)) * complex_of_real (cos (\<gamma> / 2)) + exp (- \<i> * complex_of_real \<phi>\<^sub>A) * complex_of_real (cos (\<theta>\<^sub>A / 2)) * complex_of_real (sin (\<theta>\<^sub>B / 2)) * \<i> * complex_of_real (sin (\<gamma> / 2))), - \<i> * complex_of_real (sin (\<gamma> / 2)) * (exp (\<i> * complex_of_real \<phi>\<^sub>A) * complex_of_real (cos (\<theta>\<^sub>A / 2)) * exp (\<i> * complex_of_real \<phi>\<^sub>B) * complex_of_real (cos (\<theta>\<^sub>B / 2)) * complex_of_real (cos (\<gamma> / 2)) + complex_of_real (sin (\<theta>\<^sub>A / 2) * sin (\<theta>\<^sub>B / 2)) * \<i> * complex_of_real (sin (\<gamma> / 2))) + complex_of_real (cos (\<gamma> / 2)) * (complex_of_real (sin (\<theta>\<^sub>A / 2) * sin (\<theta>\<^sub>B / 2) * cos (\<gamma> / 2)) + exp (- \<i> * complex_of_real \<phi>\<^sub>A) * complex_of_real (cos (\<theta>\<^sub>A / 2)) * exp (- \<i> * complex_of_real \<phi>\<^sub>B) * complex_of_real (cos (\<theta>\<^sub>B / 2)) * \<i> * complex_of_real (sin (\<gamma> / 2)))]]) then (cmod (Tensor.mat_of_cols_list 4 [[complex_of_real (cos (\<gamma> / 2)) * (exp (\<i> * complex_of_real \<phi>\<^sub>A) * complex_of_real (cos (\<theta>\<^sub>A / 2)) * exp (\<i> * complex_of_real \<phi>\<^sub>B) * complex_of_real (cos (\<theta>\<^sub>B / 2)) * complex_of_real (cos (\<gamma> / 2)) + complex_of_real (sin (\<theta>\<^sub>A / 2) * sin (\<theta>\<^sub>B / 2)) * \<i> * complex_of_real (sin (\<gamma> / 2))) + - \<i> * complex_of_real (sin (\<gamma> / 2)) * (complex_of_real (sin (\<theta>\<^sub>A / 2) * sin (\<theta>\<^sub>B / 2) * cos (\<gamma> / 2)) + exp (- \<i> * complex_of_real \<phi>\<^sub>A) * complex_of_real (cos (\<theta>\<^sub>A / 2)) * exp (- \<i> * complex_of_real \<phi>\<^sub>B) * complex_of_real (cos (\<theta>\<^sub>B / 2)) * \<i> * complex_of_real (sin (\<gamma> / 2))), complex_of_real (cos (\<gamma> / 2)) * (exp (\<i> * complex_of_real \<phi>\<^sub>A) * complex_of_real (cos (\<theta>\<^sub>A / 2)) * complex_of_real (- sin (\<theta>\<^sub>B / 2)) * complex_of_real (cos (\<gamma> / 2)) + complex_of_real (sin (\<theta>\<^sub>A / 2)) * exp (- \<i> * complex_of_real \<phi>\<^sub>B) * complex_of_real (cos (\<theta>\<^sub>B / 2)) * \<i> * complex_of_real (sin (\<gamma> / 2))) + \<i> * complex_of_real (sin (\<gamma> / 2)) * (complex_of_real (- sin (\<theta>\<^sub>A / 2)) * exp (\<i> * complex_of_real \<phi>\<^sub>B) * complex_of_real (cos (\<theta>\<^sub>B / 2)) * complex_of_real (cos (\<gamma> / 2)) + exp (- \<i> * complex_of_real \<phi>\<^sub>A) * complex_of_real (cos (\<theta>\<^sub>A / 2)) * complex_of_real (sin (\<theta>\<^sub>B / 2)) * \<i> * complex_of_real (sin (\<gamma> / 2))), \<i> * complex_of_real (sin (\<gamma> / 2)) * (exp (\<i> * complex_of_real \<phi>\<^sub>A) * complex_of_real (cos (\<theta>\<^sub>A / 2)) * complex_of_real (- sin (\<theta>\<^sub>B / 2)) * complex_of_real (cos (\<gamma> / 2)) + complex_of_real (sin (\<theta>\<^sub>A / 2)) * exp (- \<i> * complex_of_real \<phi>\<^sub>B) * complex_of_real (cos (\<theta>\<^sub>B / 2)) * \<i> * complex_of_real (sin (\<gamma> / 2))) + complex_of_real (cos (\<gamma> / 2)) * (complex_of_real (- sin (\<theta>\<^sub>A / 2)) * exp (\<i> * complex_of_real \<phi>\<^sub>B) * complex_of_real (cos (\<theta>\<^sub>B / 2)) * complex_of_real (cos (\<gamma> / 2)) + exp (- \<i> * complex_of_real \<phi>\<^sub>A) * complex_of_real (cos (\<theta>\<^sub>A / 2)) * complex_of_real (sin (\<theta>\<^sub>B / 2)) * \<i> * complex_of_real (sin (\<gamma> / 2))), - \<i> * complex_of_real (sin (\<gamma> / 2)) * (exp (\<i> * complex_of_real \<phi>\<^sub>A) * complex_of_real (cos (\<theta>\<^sub>A / 2)) * exp (\<i> * complex_of_real \<phi>\<^sub>B) * complex_of_real (cos (\<theta>\<^sub>B / 2)) * complex_of_real (cos (\<gamma> / 2)) + complex_of_real (sin (\<theta>\<^sub>A / 2) * sin (\<theta>\<^sub>B / 2)) * \<i> * complex_of_real (sin (\<gamma> / 2))) + complex_of_real (cos (\<gamma> / 2)) * (complex_of_real (sin (\<theta>\<^sub>A / 2) * sin (\<theta>\<^sub>B / 2) * cos (\<gamma> / 2)) + exp (- \<i> * complex_of_real \<phi>\<^sub>A) * complex_of_real (cos (\<theta>\<^sub>A / 2)) * exp (- \<i> * complex_of_real \<phi>\<^sub>B) * complex_of_real (cos (\<theta>\<^sub>B / 2)) * \<i> * complex_of_real (sin (\<gamma> / 2)))]] $$ (1, 0)))\<^sup>2 else undefined) + 0 * (if state 2 (Tensor.mat_of_cols_list 4 [[complex_of_real (cos (\<gamma> / 2)) * (exp (\<i> * complex_of_real \<phi>\<^sub>A) * complex_of_real (cos (\<theta>\<^sub>A / 2)) * exp (\<i> * complex_of_real \<phi>\<^sub>B) * complex_of_real (cos (\<theta>\<^sub>B / 2)) * complex_of_real (cos (\<gamma> / 2)) + complex_of_real (sin (\<theta>\<^sub>A / 2) * sin (\<theta>\<^sub>B / 2)) * \<i> * complex_of_real (sin (\<gamma> / 2))) + - \<i> * complex_of_real (sin (\<gamma> / 2)) * (complex_of_real (sin (\<theta>\<^sub>A / 2) * sin (\<theta>\<^sub>B / 2) * cos (\<gamma> / 2)) + exp (- \<i> * complex_of_real \<phi>\<^sub>A) * complex_of_real (cos (\<theta>\<^sub>A / 2)) * exp (- \<i> * complex_of_real \<phi>\<^sub>B) * complex_of_real (cos (\<theta>\<^sub>B / 2)) * \<i> * complex_of_real (sin (\<gamma> / 2))), complex_of_real (cos (\<gamma> / 2)) * (exp (\<i> * complex_of_real \<phi>\<^sub>A) * complex_of_real (cos (\<theta>\<^sub>A / 2)) * complex_of_real (- sin (\<theta>\<^sub>B / 2)) * complex_of_real (cos (\<gamma> / 2)) + complex_of_real (sin (\<theta>\<^sub>A / 2)) * exp (- \<i> * complex_of_real \<phi>\<^sub>B) * complex_of_real (cos (\<theta>\<^sub>B / 2)) * \<i> * complex_of_real (sin (\<gamma> / 2))) + \<i> * complex_of_real (sin (\<gamma> / 2)) * (complex_of_real (- sin (\<theta>\<^sub>A / 2)) * exp (\<i> * complex_of_real \<phi>\<^sub>B) * complex_of_real (cos (\<theta>\<^sub>B / 2)) * complex_of_real (cos (\<gamma> / 2)) + exp (- \<i> * complex_of_real \<phi>\<^sub>A) * complex_of_real (cos (\<theta>\<^sub>A / 2)) * complex_of_real (sin (\<theta>\<^sub>B / 2)) * \<i> * complex_of_real (sin (\<gamma> / 2))), \<i> * complex_of_real (sin (\<gamma> / 2)) * (exp (\<i> * complex_of_real \<phi>\<^sub>A) * complex_of_real (cos (\<theta>\<^sub>A / 2)) * complex_of_real (- sin (\<theta>\<^sub>B / 2)) * complex_of_real (cos (\<gamma> / 2)) + complex_of_real (sin (\<theta>\<^sub>A / 2)) * exp (- \<i> * complex_of_real \<phi>\<^sub>B) * complex_of_real (cos (\<theta>\<^sub>B / 2)) * \<i> * complex_of_real (sin (\<gamma> / 2))) + complex_of_real (cos (\<gamma> / 2)) * (complex_of_real (- sin (\<theta>\<^sub>A / 2)) * exp (\<i> * complex_of_real \<phi>\<^sub>B) * complex_of_real (cos (\<theta>\<^sub>B / 2)) * complex_of_real (cos (\<gamma> / 2)) + exp (- \<i> * complex_of_real \<phi>\<^sub>A) * complex_of_real (cos (\<theta>\<^sub>A / 2)) * complex_of_real (sin (\<theta>\<^sub>B / 2)) * \<i> * complex_of_real (sin (\<gamma> / 2))), - \<i> * complex_of_real (sin (\<gamma> / 2)) * (exp (\<i> * complex_of_real \<phi>\<^sub>A) * complex_of_real (cos (\<theta>\<^sub>A / 2)) * exp (\<i> * complex_of_real \<phi>\<^sub>B) * complex_of_real (cos (\<theta>\<^sub>B / 2)) * complex_of_real (cos (\<gamma> / 2)) + complex_of_real (sin (\<theta>\<^sub>A / 2) * sin (\<theta>\<^sub>B / 2)) * \<i> * complex_of_real (sin (\<gamma> / 2))) + complex_of_real (cos (\<gamma> / 2)) * (complex_of_real (sin (\<theta>\<^sub>A / 2) * sin (\<theta>\<^sub>B / 2) * cos (\<gamma> / 2)) + exp (- \<i> * complex_of_real \<phi>\<^sub>A) * complex_of_real (cos (\<theta>\<^sub>A / 2)) * exp (- \<i> * complex_of_real \<phi>\<^sub>B) * complex_of_real (cos (\<theta>\<^sub>B / 2)) * \<i> * complex_of_real (sin (\<gamma> / 2)))]]) then (cmod (Tensor.mat_of_cols_list 4 [[complex_of_real (cos (\<gamma> / 2)) * (exp (\<i> * complex_of_real \<phi>\<^sub>A) * complex_of_real (cos (\<theta>\<^sub>A / 2)) * exp (\<i> * complex_of_real \<phi>\<^sub>B) * complex_of_real (cos (\<theta>\<^sub>B / 2)) * complex_of_real (cos (\<gamma> / 2)) + complex_of_real (sin (\<theta>\<^sub>A / 2) * sin (\<theta>\<^sub>B / 2)) * \<i> * complex_of_real (sin (\<gamma> / 2))) + - \<i> * complex_of_real (sin (\<gamma> / 2)) * (complex_of_real (sin (\<theta>\<^sub>A / 2) * sin (\<theta>\<^sub>B / 2) * cos (\<gamma> / 2)) + exp (- \<i> * complex_of_real \<phi>\<^sub>A) * complex_of_real (cos (\<theta>\<^sub>A / 2)) * exp (- \<i> * complex_of_real \<phi>\<^sub>B) * complex_of_real (cos (\<theta>\<^sub>B / 2)) * \<i> * complex_of_real (sin (\<gamma> / 2))), complex_of_real (cos (\<gamma> / 2)) * (exp (\<i> * complex_of_real \<phi>\<^sub>A) * complex_of_real (cos (\<theta>\<^sub>A / 2)) * complex_of_real (- sin (\<theta>\<^sub>B / 2)) * complex_of_real (cos (\<gamma> / 2)) + complex_of_real (sin (\<theta>\<^sub>A / 2)) * exp (- \<i> * complex_of_real \<phi>\<^sub>B) * complex_of_real (cos (\<theta>\<^sub>B / 2)) * \<i> * complex_of_real (sin (\<gamma> / 2))) + \<i> * complex_of_real (sin (\<gamma> / 2)) * (complex_of_real (- sin (\<theta>\<^sub>A / 2)) * exp (\<i> * complex_of_real \<phi>\<^sub>B) * complex_of_real (cos (\<theta>\<^sub>B / 2)) * complex_of_real (cos (\<gamma> / 2)) + exp (- \<i> * complex_of_real \<phi>\<^sub>A) * complex_of_real (cos (\<theta>\<^sub>A / 2)) * complex_of_real (sin (\<theta>\<^sub>B / 2)) * \<i> * complex_of_real (sin (\<gamma> / 2))), \<i> * complex_of_real (sin (\<gamma> / 2)) * (exp (\<i> * complex_of_real \<phi>\<^sub>A) * complex_of_real (cos (\<theta>\<^sub>A / 2)) * complex_of_real (- sin (\<theta>\<^sub>B / 2)) * complex_of_real (cos (\<gamma> / 2)) + complex_of_real (sin (\<theta>\<^sub>A / 2)) * exp (- \<i> * complex_of_real \<phi>\<^sub>B) * complex_of_real (cos (\<theta>\<^sub>B / 2)) * \<i> * complex_of_real (sin (\<gamma> / 2))) + complex_of_real (cos (\<gamma> / 2)) * (complex_of_real (- sin (\<theta>\<^sub>A / 2)) * exp (\<i> * complex_of_real \<phi>\<^sub>B) * complex_of_real (cos (\<theta>\<^sub>B / 2)) * complex_of_real (cos (\<gamma> / 2)) + exp (- \<i> * complex_of_real \<phi>\<^sub>A) * complex_of_real (cos (\<theta>\<^sub>A / 2)) * complex_of_real (sin (\<theta>\<^sub>B / 2)) * \<i> * complex_of_real (sin (\<gamma> / 2))), - \<i> * complex_of_real (sin (\<gamma> / 2)) * (exp (\<i> * complex_of_real \<phi>\<^sub>A) * complex_of_real (cos (\<theta>\<^sub>A / 2)) * exp (\<i> * complex_of_real \<phi>\<^sub>B) * complex_of_real (cos (\<theta>\<^sub>B / 2)) * complex_of_real (cos (\<gamma> / 2)) + complex_of_real (sin (\<theta>\<^sub>A / 2) * sin (\<theta>\<^sub>B / 2)) * \<i> * complex_of_real (sin (\<gamma> / 2))) + complex_of_real (cos (\<gamma> / 2)) * (complex_of_real (sin (\<theta>\<^sub>A / 2) * sin (\<theta>\<^sub>B / 2) * cos (\<gamma> / 2)) + exp (- \<i> * complex_of_real \<phi>\<^sub>A) * complex_of_real (cos (\<theta>\<^sub>A / 2)) * exp (- \<i> * complex_of_real \<phi>\<^sub>B) * complex_of_real (cos (\<theta>\<^sub>B / 2)) * \<i> * complex_of_real (sin (\<gamma> / 2)))]] $$ (2, 0)))\<^sup>2 else undefined)
complex_of_real (cos (?\<gamma> / 2)) * complex_of_real (cos (?\<gamma> / 2)) - \<i> * complex_of_real (sin (?\<gamma> / 2)) * (\<i> * complex_of_real (sin (?\<gamma> / 2))) = 1
state 2 (Tensor.mat_of_cols_list 4 [[complex_of_real (cos (\<gamma> / 2)) * (exp (\<i> * complex_of_real \<phi>\<^sub>A) * complex_of_real (cos (\<theta>\<^sub>A / 2)) * exp (\<i> * complex_of_real \<phi>\<^sub>B) * complex_of_real (cos (\<theta>\<^sub>B / 2)) * complex_of_real (cos (\<gamma> / 2)) + complex_of_real (sin (\<theta>\<^sub>A / 2) * sin (\<theta>\<^sub>B / 2)) * \<i> * complex_of_real (sin (\<gamma> / 2))) + - \<i> * complex_of_real (sin (\<gamma> / 2)) * (complex_of_real (sin (\<theta>\<^sub>A / 2) * sin (\<theta>\<^sub>B / 2) * cos (\<gamma> / 2)) + exp (- \<i> * complex_of_real \<phi>\<^sub>A) * complex_of_real (cos (\<theta>\<^sub>A / 2)) * exp (- \<i> * complex_of_real \<phi>\<^sub>B) * complex_of_real (cos (\<theta>\<^sub>B / 2)) * \<i> * complex_of_real (sin (\<gamma> / 2))), complex_of_real (cos (\<gamma> / 2)) * (exp (\<i> * complex_of_real \<phi>\<^sub>A) * complex_of_real (cos (\<theta>\<^sub>A / 2)) * complex_of_real (- sin (\<theta>\<^sub>B / 2)) * complex_of_real (cos (\<gamma> / 2)) + complex_of_real (sin (\<theta>\<^sub>A / 2)) * exp (- \<i> * complex_of_real \<phi>\<^sub>B) * complex_of_real (cos (\<theta>\<^sub>B / 2)) * \<i> * complex_of_real (sin (\<gamma> / 2))) + \<i> * complex_of_real (sin (\<gamma> / 2)) * (complex_of_real (- sin (\<theta>\<^sub>A / 2)) * exp (\<i> * complex_of_real \<phi>\<^sub>B) * complex_of_real (cos (\<theta>\<^sub>B / 2)) * complex_of_real (cos (\<gamma> / 2)) + exp (- \<i> * complex_of_real \<phi>\<^sub>A) * complex_of_real (cos (\<theta>\<^sub>A / 2)) * complex_of_real (sin (\<theta>\<^sub>B / 2)) * \<i> * complex_of_real (sin (\<gamma> / 2))), \<i> * complex_of_real (sin (\<gamma> / 2)) * (exp (\<i> * complex_of_real \<phi>\<^sub>A) * complex_of_real (cos (\<theta>\<^sub>A / 2)) * complex_of_real (- sin (\<theta>\<^sub>B / 2)) * complex_of_real (cos (\<gamma> / 2)) + complex_of_real (sin (\<theta>\<^sub>A / 2)) * exp (- \<i> * complex_of_real \<phi>\<^sub>B) * complex_of_real (cos (\<theta>\<^sub>B / 2)) * \<i> * complex_of_real (sin (\<gamma> / 2))) + complex_of_real (cos (\<gamma> / 2)) * (complex_of_real (- sin (\<theta>\<^sub>A / 2)) * exp (\<i> * complex_of_real \<phi>\<^sub>B) * complex_of_real (cos (\<theta>\<^sub>B / 2)) * complex_of_real (cos (\<gamma> / 2)) + exp (- \<i> * complex_of_real \<phi>\<^sub>A) * complex_of_real (cos (\<theta>\<^sub>A / 2)) * complex_of_real (sin (\<theta>\<^sub>B / 2)) * \<i> * complex_of_real (sin (\<gamma> / 2))), - \<i> * complex_of_real (sin (\<gamma> / 2)) * (exp (\<i> * complex_of_real \<phi>\<^sub>A) * complex_of_real (cos (\<theta>\<^sub>A / 2)) * exp (\<i> * complex_of_real \<phi>\<^sub>B) * complex_of_real (cos (\<theta>\<^sub>B / 2)) * complex_of_real (cos (\<gamma> / 2)) + complex_of_real (sin (\<theta>\<^sub>A / 2) * sin (\<theta>\<^sub>B / 2)) * \<i> * complex_of_real (sin (\<gamma> / 2))) + complex_of_real (cos (\<gamma> / 2)) * (complex_of_real (sin (\<theta>\<^sub>A / 2) * sin (\<theta>\<^sub>B / 2) * cos (\<gamma> / 2)) + exp (- \<i> * complex_of_real \<phi>\<^sub>A) * complex_of_real (cos (\<theta>\<^sub>A / 2)) * exp (- \<i> * complex_of_real \<phi>\<^sub>B) * complex_of_real (cos (\<theta>\<^sub>B / 2)) * \<i> * complex_of_real (sin (\<gamma> / 2)))]])

goal (1 subgoal):
 1. \<phi>\<^sub>A = 0 \<and> \<theta>\<^sub>A = pi \<and> \<phi>\<^sub>B = 0 \<and> \<theta>\<^sub>B = pi \<longrightarrow> alice_payoff = 1 \<and> bob_payoff = 1
[PROOF STEP]
by auto


[STATEMENT]
lemma shortestPath_transfer [transfer_rule]:
  assumes [transfer_rule]: "right_total G"
    and [transfer_rule]: "(G ===> (=)) \<alpha>e \<alpha>e2"
    and [transfer_rule]: "(G ===> (=)) \<alpha>n \<alpha>n2"
    and [transfer_rule]: "(G ===> (=)) invar invar2"
    and [transfer_rule]: "(G ===> (=)) inEdges' inEdges2"
    and [transfer_rule]: "(G ===> (=)) Entry Entry2"
  shows "(G ===> (=)) shortestPath (graph_Entry.shortestPath \<alpha>n2 invar2 inEdges2 Entry2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (G ===> (=)) shortestPath (graph_Entry.shortestPath \<alpha>n2 invar2 inEdges2 Entry2)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (G ===> (=)) shortestPath (graph_Entry.shortestPath \<alpha>n2 invar2 inEdges2 Entry2)
[PROOF STEP]
interpret gE2: graph_Entry \<alpha>e2 \<alpha>n2 invar2 inEdges2 Entry2
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. graph_Entry \<alpha>e2 \<alpha>n2 invar2 inEdges2 Entry2
[PROOF STEP]
by transfer' unfold_locales
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (G ===> (=)) shortestPath gE2.shortestPath
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (G ===> (=)) shortestPath gE2.shortestPath
[PROOF STEP]
unfolding shortestPath_def [abs_def] gE2.shortestPath_def [abs_def]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (G ===> (=)) (\<lambda>g n. LEAST l. \<exists>ns. length ns = l \<and> g \<turnstile> Entry g-ns\<rightarrow>n) (\<lambda>g n. LEAST l. \<exists>ns. length ns = l \<and> gE2.path2 g (Entry2 g) ns n)
[PROOF STEP]
by transfer_prover
[PROOF STATE]
proof (state)
this:
(G ===> (=)) shortestPath gE2.shortestPath

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma pass_ATC_io_fail :
  assumes "\<not>pass_ATC M A FS"
  and     "is_ATC A"
  and     "observable M"
  and     "(inputs A) \<subseteq> (inputs M)"
shows "initial A \<in> FS \<or> (\<exists> io ioA ioM . io@[ioA] \<in> L A
                          \<and> io@[ioM] \<in> L M
                          \<and> fst ioA = fst ioM
                          \<and> (io@[ioM] \<notin> L A \<or> io_targets A (io@[ioM]) (initial A) \<inter> FS \<noteq> {}))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. FSM.initial A \<in> FS \<or> (\<exists>io ioA ioM. io @ [ioA] \<in> L A \<and> io @ [ioM] \<in> L M \<and> fst ioA = fst ioM \<and> (io @ [ioM] \<notin> L A \<or> io_targets A (io @ [ioM]) (FSM.initial A) \<inter> FS \<noteq> {}))
[PROOF STEP]
using pass_ATC'_io_fail[OF _ assms(2-4)]
[PROOF STATE]
proof (prove)
using this:
\<not> pass_ATC' M A ?FS ?k \<Longrightarrow> FSM.initial A \<in> ?FS \<or> (\<exists>io ioA ioM. io @ [ioA] \<in> L A \<and> io @ [ioM] \<in> L M \<and> fst ioA = fst ioM \<and> (io @ [ioM] \<notin> L A \<or> io_targets A (io @ [ioM]) (FSM.initial A) \<inter> ?FS \<noteq> {}))

goal (1 subgoal):
 1. FSM.initial A \<in> FS \<or> (\<exists>io ioA ioM. io @ [ioA] \<in> L A \<and> io @ [ioM] \<in> L M \<and> fst ioA = fst ioM \<and> (io @ [ioM] \<notin> L A \<or> io_targets A (io @ [ioM]) (FSM.initial A) \<inter> FS \<noteq> {}))
[PROOF STEP]
using assms(1)
[PROOF STATE]
proof (prove)
using this:
\<not> pass_ATC' M A ?FS ?k \<Longrightarrow> FSM.initial A \<in> ?FS \<or> (\<exists>io ioA ioM. io @ [ioA] \<in> L A \<and> io @ [ioM] \<in> L M \<and> fst ioA = fst ioM \<and> (io @ [ioM] \<notin> L A \<or> io_targets A (io @ [ioM]) (FSM.initial A) \<inter> ?FS \<noteq> {}))
\<not> pass_ATC M A FS

goal (1 subgoal):
 1. FSM.initial A \<in> FS \<or> (\<exists>io ioA ioM. io @ [ioA] \<in> L A \<and> io @ [ioM] \<in> L M \<and> fst ioA = fst ioM \<and> (io @ [ioM] \<notin> L A \<or> io_targets A (io @ [ioM]) (FSM.initial A) \<inter> FS \<noteq> {}))
[PROOF STEP]
by auto


[STATEMENT]
lemma sum_vec_vNil[simp]: "sum_vec vNil = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum_vec vNil = (0::'a)
[PROOF STEP]
by (simp add: sum_vec_def)


[STATEMENT]
lemma set_nongens_impl: "set (nongens_impl Q) = nongens Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (nongens_impl Q) = nongens Q
[PROOF STEP]
by (auto simp: nongens_def nongens_impl_def set_gen_impl simp flip: List.set_empty)


[STATEMENT]
lemma ab_mod_f0:
  "a = 0 \<or> b = 0" if "a * b mod f = 0"
    and a: "degree a < degree f"
    and b: "degree b < degree f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a = 0 \<or> b = 0
[PROOF STEP]
using that f_dvd_ab
[PROOF STATE]
proof (prove)
using this:
a * b mod f = 0
degree a < degree f
degree b < degree f
\<lbrakk>f dvd ?a * ?b; degree ?a < degree f; degree ?b < degree f\<rbrakk> \<Longrightarrow> ?a = 0 \<or> ?b = 0

goal (1 subgoal):
 1. a = 0 \<or> b = 0
[PROOF STEP]
by auto


[STATEMENT]
lemma validD_L: \<open>\<tturnstile> \<phi> \<Longrightarrow> \<phi> \<in> Cn(A)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<tturnstile> \<phi> \<Longrightarrow> \<phi> \<in> Cn A
[PROOF STEP]
using monotonicity_L valid_def infer_def
[PROOF STATE]
proof (prove)
using this:
?A \<subseteq> ?B \<Longrightarrow> Cn ?A \<subseteq> Cn ?B
\<tturnstile> ?\<phi> \<equiv> {} \<turnstile> ?\<phi>
?A \<turnstile> ?\<phi> \<equiv> ?\<phi> \<in> Cn ?A

goal (1 subgoal):
 1. \<tturnstile> \<phi> \<Longrightarrow> \<phi> \<in> Cn A
[PROOF STEP]
by fastforce


[STATEMENT]
lemma eeqButPID_update_post:
assumes "eeqButPID ntcs ntcs1"
shows "eeqButPID (ntcs (pid := ntc)) (ntcs1 (pid := ntc))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eeqButPID (ntcs(pid := ntc)) (ntcs1(pid := ntc))
[PROOF STEP]
using eeqButPID_not_PID[OF assms]
[PROOF STATE]
proof (prove)
using this:
?pid \<noteq> PID \<Longrightarrow> ntcs ?pid = ntcs1 ?pid

goal (1 subgoal):
 1. eeqButPID (ntcs(pid := ntc)) (ntcs1(pid := ntc))
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
?pid \<noteq> PID \<Longrightarrow> ntcs ?pid = ntcs1 ?pid
eeqButPID ntcs ntcs1

goal (1 subgoal):
 1. eeqButPID (ntcs(pid := ntc)) (ntcs1(pid := ntc))
[PROOF STEP]
unfolding eeqButPID_def
[PROOF STATE]
proof (prove)
using this:
?pid \<noteq> PID \<Longrightarrow> ntcs ?pid = ntcs1 ?pid
\<forall>pid. pid \<noteq> PID \<longrightarrow> ntcs pid = ntcs1 pid

goal (1 subgoal):
 1. \<forall>pida. pida \<noteq> PID \<longrightarrow> (ntcs(pid := ntc)) pida = (ntcs1(pid := ntc)) pida
[PROOF STEP]
by auto


[STATEMENT]
lemma nan_not_finite[simp]: "is_nan x \<Longrightarrow> \<not> is_finite x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_nan x \<Longrightarrow> \<not> is_finite x
[PROOF STEP]
using float_distinct_finite(1)
[PROOF STATE]
proof (prove)
using this:
\<not> (is_nan ?a \<and> is_finite ?a)

goal (1 subgoal):
 1. is_nan x \<Longrightarrow> \<not> is_finite x
[PROOF STEP]
by blast


[STATEMENT]
lemma lemAddOverScale:
  shows "a**u \<oplus> b**u = (a+b)**u"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a ** u \<oplus> b ** u = (a + b) ** u
[PROOF STEP]
by (simp add: semiring_normalization_rules(1))


[STATEMENT]
lemma lemDirectionReverse:
    shows "from q to p = vecNegate (from p to q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. from q to p = ~ from p to q
[PROOF STEP]
by simp


[STATEMENT]
lemma interaction_any_bounded_converter_parallel_converter' [interaction_bound]:
  assumes "interaction_any_bounded_converter conv1 n"
    and "interaction_any_bounded_converter conv2 m"
  shows "interaction_any_bounded_converter (parallel_converter conv1 conv2) (max n m)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. interaction_any_bounded_converter (parallel_converter conv1 conv2) (max n m)
[PROOF STEP]
by(rule interaction_any_bounded_converter_parallel_converter; rule assms[THEN interaction_any_bounded_converter_mono]; simp)


[STATEMENT]
lemma norm_pre_pure_rule2:
  "\<lbrakk> b \<Longrightarrow> <emp> f <Q> \<rbrakk> \<Longrightarrow> <\<up>b> f <Q>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (b \<Longrightarrow> <emp> f <Q>) \<Longrightarrow> <\<up> b> f <Q>
[PROOF STEP]
by simp


[STATEMENT]
lemma case_list_rule:
  "\<lbrakk> l=[] \<Longrightarrow> <P> fn <Q>; \<And>x xs. l=x#xs \<Longrightarrow> <P> fc x xs <Q> \<rbrakk> \<Longrightarrow>
  <P> case_list fn fc l <Q>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>l = [] \<Longrightarrow> <P> fn <Q>; \<And>x xs. l = x # xs \<Longrightarrow> <P> fc x xs <Q>\<rbrakk> \<Longrightarrow> <P> case l of [] \<Rightarrow> fn | x # xa \<Rightarrow> fc x xa <Q>
[PROOF STEP]
by (auto split: list.split)


[STATEMENT]
lemma rule_sub_remark_8:
    assumes "\<And>v.[\<^bold>\<A>\<phi> \<^bold>\<equiv> \<phi> in v]"
        and "[\<^bold>\<box>(\<^bold>\<A>\<phi>) in v]"
    shows "[\<^bold>\<box>(\<phi>) in v]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [\<^bold>\<box>\<phi> in v]
[PROOF STEP]
apply (insert assms)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>v. [\<^bold>\<A>\<phi> \<^bold>\<equiv> \<phi> in v]; [\<^bold>\<box>\<^bold>\<A>\<phi> in v]\<rbrakk> \<Longrightarrow> [\<^bold>\<box>\<phi> in v]
[PROOF STEP]
apply PLM_autosubst
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<And>v. [\<^bold>\<A>\<phi> \<^bold>\<equiv> \<phi> in v]; [\<^bold>\<box>\<^bold>\<A>\<phi> in v]\<rbrakk> \<Longrightarrow> \<forall>v. [\<^bold>\<A>\<phi> \<^bold>\<equiv> \<phi> in v]
 2. \<lbrakk>\<And>v. [\<^bold>\<A>\<phi> \<^bold>\<equiv> \<phi> in v]; [\<^bold>\<box>\<^bold>\<A>\<phi> in v]\<rbrakk> \<Longrightarrow> [\<^bold>\<box>\<^bold>\<A>\<phi> in v]
[PROOF STEP]
by auto


[STATEMENT]
lemma en_eq_4[PLM]:
    "[(\<lbrace>x,F\<rbrace> \<^bold>\<equiv> \<lbrace>y,G\<rbrace>) \<^bold>\<equiv> (\<^bold>\<box>\<lbrace>x,F\<rbrace> \<^bold>\<equiv> \<^bold>\<box>\<lbrace>y,G\<rbrace>) in v]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [\<lbrace>x,F\<rbrace> \<^bold>\<equiv> \<lbrace>y,G\<rbrace> \<^bold>\<equiv> (\<^bold>\<box>\<lbrace>x,F\<rbrace> \<^bold>\<equiv> \<^bold>\<box>\<lbrace>y,G\<rbrace>) in v]
[PROOF STEP]
by (metis CP en_eq_2 "\<^bold>\<equiv>I" "\<^bold>\<equiv>E"(1) "\<^bold>\<equiv>E"(2))


[STATEMENT]
lemma get_child_nodes_new_element:
  "ptr' \<noteq> cast new_element_ptr \<Longrightarrow> h \<turnstile> new_element \<rightarrow>\<^sub>r new_element_ptr \<Longrightarrow> h \<turnstile> new_element \<rightarrow>\<^sub>h h'
     \<Longrightarrow> r \<in> get_child_nodes_locs ptr' \<Longrightarrow> r h h'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ptr' \<noteq> cast\<^sub>e\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r new_element_ptr; h \<turnstile> new_element \<rightarrow>\<^sub>r new_element_ptr; h \<turnstile> new_element \<rightarrow>\<^sub>h h'; r \<in> get_child_nodes_locs ptr'\<rbrakk> \<Longrightarrow> r h h'
[PROOF STEP]
by (auto simp add: get_child_nodes_locs_def CD.get_child_nodes_locs_def new_element_get_M\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t new_element_get_M\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t
      new_element_get_M\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t new_element_get_M\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t split: prod.splits if_splits option.splits
      elim!: bind_returns_result_E bind_returns_heap_E intro: is_element_ptr_kind_obtains)


[STATEMENT]
lemma set_shadow_root_ok: "type_wf h \<Longrightarrow> element_ptr |\<in>| element_ptr_kinds h \<Longrightarrow> h \<turnstile> ok (set_shadow_root element_ptr tag)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>type_wf h; element_ptr |\<in>| element_ptr_kinds h\<rbrakk> \<Longrightarrow> h \<turnstile> ok set_shadow_root element_ptr tag
[PROOF STEP]
apply(unfold type_wf_impl)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ShadowRootClass.type_wf h; element_ptr |\<in>| element_ptr_kinds h\<rbrakk> \<Longrightarrow> h \<turnstile> ok set_shadow_root element_ptr tag
[PROOF STEP]
unfolding set_shadow_root_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ShadowRootClass.type_wf h; element_ptr |\<in>| element_ptr_kinds h\<rbrakk> \<Longrightarrow> h \<turnstile> ok put_M\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t element_ptr shadow_root_opt_update tag
[PROOF STEP]
using get_M\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_ok put_M\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_ok
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>ShadowRootClass.type_wf ?h; ?ptr |\<in>| element_ptr_kinds ?h\<rbrakk> \<Longrightarrow> ?h \<turnstile> ok get_M\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t ?ptr ?getter
\<lbrakk>ShadowRootClass.type_wf ?h; ?ptr |\<in>| element_ptr_kinds ?h\<rbrakk> \<Longrightarrow> ?h \<turnstile> ok put_M\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t ?ptr ?setter ?v

goal (1 subgoal):
 1. \<lbrakk>ShadowRootClass.type_wf h; element_ptr |\<in>| element_ptr_kinds h\<rbrakk> \<Longrightarrow> h \<turnstile> ok put_M\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t element_ptr shadow_root_opt_update tag
[PROOF STEP]
by (simp add: ShadowRootMonad.put_M\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_ok)


[STATEMENT]
lemma set_mode_types_preserved:
  assumes "w \<in> set_mode_locs element_ptr"
  assumes "h \<turnstile> w \<rightarrow>\<^sub>h h'"
  shows "type_wf h = type_wf h'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. type_wf h = type_wf h'
[PROOF STEP]
apply(unfold type_wf_impl)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ShadowRootClass.type_wf h = ShadowRootClass.type_wf h'
[PROOF STEP]
using assms(1) type_wf_preserved[OF writes_singleton2 assms(2)]
[PROOF STATE]
proof (prove)
using this:
w \<in> set_mode_locs element_ptr
\<lbrakk>\<And>h h' wa. \<lbrakk>wa \<in> {w}; h \<turnstile> wa \<rightarrow>\<^sub>h h'\<rbrakk> \<Longrightarrow> \<forall>object_ptr. preserved (get_M\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t object_ptr RObject.nothing) h h'; \<And>h h' wa. \<lbrakk>wa \<in> {w}; h \<turnstile> wa \<rightarrow>\<^sub>h h'\<rbrakk> \<Longrightarrow> \<forall>node_ptr. preserved (get_M\<^sub>N\<^sub>o\<^sub>d\<^sub>e node_ptr RNode.nothing) h h'; \<And>h h' wa. \<lbrakk>wa \<in> {w}; h \<turnstile> wa \<rightarrow>\<^sub>h h'\<rbrakk> \<Longrightarrow> \<forall>element_ptr. preserved (get_M\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t element_ptr RElement.nothing) h h'; \<And>h h' wa. \<lbrakk>wa \<in> {w}; h \<turnstile> wa \<rightarrow>\<^sub>h h'\<rbrakk> \<Longrightarrow> \<forall>character_data_ptr. preserved (get_M\<^sub>C\<^sub>h\<^sub>a\<^sub>r\<^sub>a\<^sub>c\<^sub>t\<^sub>e\<^sub>r\<^sub>D\<^sub>a\<^sub>t\<^sub>a character_data_ptr RCharacterData.nothing) h h'; \<And>h h' wa. \<lbrakk>wa \<in> {w}; h \<turnstile> wa \<rightarrow>\<^sub>h h'\<rbrakk> \<Longrightarrow> \<forall>document_ptr. preserved (get_M\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t document_ptr RDocument.nothing) h h'; \<And>h h' wa. \<lbrakk>wa \<in> {w}; h \<turnstile> wa \<rightarrow>\<^sub>h h'\<rbrakk> \<Longrightarrow> \<forall>shadow_root_ptr. preserved (get_M\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t shadow_root_ptr RShadowRoot.nothing) h h'\<rbrakk> \<Longrightarrow> ShadowRootClass.type_wf h = ShadowRootClass.type_wf h'

goal (1 subgoal):
 1. ShadowRootClass.type_wf h = ShadowRootClass.type_wf h'
[PROOF STEP]
by(auto simp add: all_args_def set_mode_locs_def split: if_splits)


[STATEMENT]
lemma get_root_node_si_root_in_heap:
  assumes "heap_is_wellformed h" and "type_wf h" and "known_ptrs h"
  assumes "h \<turnstile> get_root_node_si ptr \<rightarrow>\<^sub>r root"
  shows "root |\<in>| object_ptr_kinds h"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. root |\<in>| object_ptr_kinds h
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
heap_is_wellformed h
type_wf h
known_ptrs h
h \<turnstile> get_root_node_si ptr \<rightarrow>\<^sub>r root

goal (1 subgoal):
 1. root |\<in>| object_ptr_kinds h
[PROOF STEP]
apply(auto simp add: get_root_node_si_def elim!: bind_returns_result_E2)[1]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>heap_is_wellformed h; type_wf h; known_ptrs h; h \<turnstile> get_ancestors_si ptr \<rightarrow>\<^sub>r x; root = last x\<rbrakk> \<Longrightarrow> last x |\<in>| object_ptr_kinds h
[PROOF STEP]
by (simp add: get_ancestors_si_never_empty get_ancestors_si_ptrs_in_heap)


[STATEMENT]
lemma type_less_x_Real_intro [intro]:
  "\<tau> = UnlimitedNatural \<Longrightarrow> \<tau> < Real"
  "\<tau> = Integer \<Longrightarrow> \<tau> < Real"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<tau> = UnlimitedNatural \<Longrightarrow> \<tau> < Real) &&& (\<tau> = Integer \<Longrightarrow> \<tau> < Real)
[PROOF STEP]
unfolding less_basic_type_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<tau> = UnlimitedNatural \<Longrightarrow> (\<sqsubset>\<^sub>B)\<^sup>+\<^sup>+ \<tau> Real) &&& (\<tau> = Integer \<Longrightarrow> (\<sqsubset>\<^sub>B)\<^sup>+\<^sup>+ \<tau> Real)
[PROOF STEP]
by (rule rtranclp_into_tranclp2, auto)


[STATEMENT]
lemma type_less_eq_x_Integer_intro [intro]:
  "\<tau> = UnlimitedNatural \<Longrightarrow> \<tau> \<le> Integer"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<tau> = UnlimitedNatural \<Longrightarrow> \<tau> \<le> Integer
[PROOF STEP]
using order.order_iff_strict
[PROOF STATE]
proof (prove)
using this:
(?a \<le> ?b) = (?a < ?b \<or> ?a = ?b)

goal (1 subgoal):
 1. \<tau> = UnlimitedNatural \<Longrightarrow> \<tau> \<le> Integer
[PROOF STEP]
by auto


[STATEMENT]
lemma (in is_cat_coequalizer) is_cat_equalizer_op'[cat_op_intros]:
  assumes "\<CC>' = op_cat \<CC>"
  shows "op_ntcf \<epsilon> : E <\<^sub>C\<^sub>F\<^sub>.\<^sub>e\<^sub>q (\<aa>,\<bb>,F,F') : \<Up>\<^sub>C \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. op_ntcf \<epsilon> : E <\<^sub>C\<^sub>F\<^sub>.\<^sub>e\<^sub>q (\<aa>,\<bb>,F,F') : \<Up>\<^sub>C \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>'
[PROOF STEP]
unfolding assms
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. op_ntcf \<epsilon> : E <\<^sub>C\<^sub>F\<^sub>.\<^sub>e\<^sub>q (\<aa>,\<bb>,F,F') : \<Up>\<^sub>C \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> op_cat \<CC>
[PROOF STEP]
by (rule is_cat_equalizer_op)


[STATEMENT]
lemma (in category) cat_cf_parallel_\<bb>\<aa>:
  assumes "vsv F'"
    and "F \<in>\<^sub>\<circ> Vset \<alpha>"
    and "\<D>\<^sub>\<circ> F' = F"
    and "\<And>\<ff>. \<ff> \<in>\<^sub>\<circ> F \<Longrightarrow> F'\<lparr>\<ff>\<rparr> : \<bb> \<mapsto>\<^bsub>\<CC>\<^esub> \<aa>"
    and "\<aa> \<in>\<^sub>\<circ> \<CC>\<lparr>Obj\<rparr>"
    and "\<bb> \<in>\<^sub>\<circ> \<CC>\<lparr>Obj\<rparr>"
  shows "cf_parallel \<alpha> (\<bb>\<^sub>P\<^sub>L F) (\<aa>\<^sub>P\<^sub>L F) F \<bb> \<aa> F' \<CC>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cf_parallel \<alpha> (\<bb>\<^sub>P\<^sub>L F) (\<aa>\<^sub>P\<^sub>L F) F \<bb> \<aa> F' \<CC>
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. cf_parallel \<alpha> (\<bb>\<^sub>P\<^sub>L F) (\<aa>\<^sub>P\<^sub>L F) F \<bb> \<aa> F' \<CC>
[PROOF STEP]
have "\<aa>\<^sub>P\<^sub>L F \<in>\<^sub>\<circ> Vset \<alpha>" "\<bb>\<^sub>P\<^sub>L F \<in>\<^sub>\<circ> Vset \<alpha>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<aa>\<^sub>P\<^sub>L F \<in>\<^sub>\<circ> Vset \<alpha> &&& \<bb>\<^sub>P\<^sub>L F \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
by (simp_all add: Axiom_of_Pairing \<bb>\<^sub>P\<^sub>L_def \<aa>\<^sub>P\<^sub>L_def assms(2))
[PROOF STATE]
proof (state)
this:
\<aa>\<^sub>P\<^sub>L F \<in>\<^sub>\<circ> Vset \<alpha>
\<bb>\<^sub>P\<^sub>L F \<in>\<^sub>\<circ> Vset \<alpha>

goal (1 subgoal):
 1. cf_parallel \<alpha> (\<bb>\<^sub>P\<^sub>L F) (\<aa>\<^sub>P\<^sub>L F) F \<bb> \<aa> F' \<CC>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<aa>\<^sub>P\<^sub>L F \<in>\<^sub>\<circ> Vset \<alpha>
\<bb>\<^sub>P\<^sub>L F \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<aa>\<^sub>P\<^sub>L F \<in>\<^sub>\<circ> Vset \<alpha>
\<bb>\<^sub>P\<^sub>L F \<in>\<^sub>\<circ> Vset \<alpha>

goal (1 subgoal):
 1. cf_parallel \<alpha> (\<bb>\<^sub>P\<^sub>L F) (\<aa>\<^sub>P\<^sub>L F) F \<bb> \<aa> F' \<CC>
[PROOF STEP]
by (intro cf_parallelI cat_parallelI)
      (simp_all add: assms cat_parallel_cs_intros cat_cs_intros)
[PROOF STATE]
proof (state)
this:
cf_parallel \<alpha> (\<bb>\<^sub>P\<^sub>L F) (\<aa>\<^sub>P\<^sub>L F) F \<bb> \<aa> F' \<CC>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma cat_cone_cf_par_2_eps_NTMap_app:
  assumes "\<epsilon> :
    E <\<^sub>C\<^sub>F\<^sub>.\<^sub>c\<^sub>o\<^sub>n\<^sub>e \<up>\<up>\<rightarrow>\<up>\<up>\<^sub>C\<^sub>F \<CC> \<aa>\<^sub>P\<^sub>L\<^sub>2 \<bb>\<^sub>P\<^sub>L\<^sub>2 \<gg>\<^sub>P\<^sub>L \<ff>\<^sub>P\<^sub>L \<aa> \<bb> \<gg> \<ff> : \<up>\<up>\<^sub>C \<aa>\<^sub>P\<^sub>L\<^sub>2 \<bb>\<^sub>P\<^sub>L\<^sub>2 \<gg>\<^sub>P\<^sub>L \<ff>\<^sub>P\<^sub>L \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>"
    and "\<gg> : \<aa> \<mapsto>\<^bsub>\<CC>\<^esub> \<bb>"
    and "\<ff> : \<aa> \<mapsto>\<^bsub>\<CC>\<^esub> \<bb>"
  shows
    "\<epsilon>\<lparr>NTMap\<rparr>\<lparr>\<bb>\<^sub>P\<^sub>L\<^sub>2\<rparr> = \<gg> \<circ>\<^sub>A\<^bsub>\<CC>\<^esub> \<epsilon>\<lparr>NTMap\<rparr>\<lparr>\<aa>\<^sub>P\<^sub>L\<^sub>2\<rparr>"
    "\<epsilon>\<lparr>NTMap\<rparr>\<lparr>\<bb>\<^sub>P\<^sub>L\<^sub>2\<rparr> = \<ff> \<circ>\<^sub>A\<^bsub>\<CC>\<^esub> \<epsilon>\<lparr>NTMap\<rparr>\<lparr>\<aa>\<^sub>P\<^sub>L\<^sub>2\<rparr>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<epsilon>\<lparr>NTMap\<rparr>\<lparr>\<bb>\<^sub>P\<^sub>L\<^sub>2\<rparr> = \<gg> \<circ>\<^sub>A\<^bsub>\<CC>\<^esub> \<epsilon>\<lparr>NTMap\<rparr>\<lparr>\<aa>\<^sub>P\<^sub>L\<^sub>2\<rparr> &&& \<epsilon>\<lparr>NTMap\<rparr>\<lparr>\<bb>\<^sub>P\<^sub>L\<^sub>2\<rparr> = \<ff> \<circ>\<^sub>A\<^bsub>\<CC>\<^esub> \<epsilon>\<lparr>NTMap\<rparr>\<lparr>\<aa>\<^sub>P\<^sub>L\<^sub>2\<rparr>
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<epsilon>\<lparr>NTMap\<rparr>\<lparr>\<bb>\<^sub>P\<^sub>L\<^sub>2\<rparr> = \<gg> \<circ>\<^sub>A\<^bsub>\<CC>\<^esub> \<epsilon>\<lparr>NTMap\<rparr>\<lparr>\<aa>\<^sub>P\<^sub>L\<^sub>2\<rparr>
 2. \<epsilon>\<lparr>NTMap\<rparr>\<lparr>\<bb>\<^sub>P\<^sub>L\<^sub>2\<rparr> = \<ff> \<circ>\<^sub>A\<^bsub>\<CC>\<^esub> \<epsilon>\<lparr>NTMap\<rparr>\<lparr>\<aa>\<^sub>P\<^sub>L\<^sub>2\<rparr>
[PROOF STEP]
let ?II = \<open>\<up>\<up>\<^sub>C \<aa>\<^sub>P\<^sub>L\<^sub>2 \<bb>\<^sub>P\<^sub>L\<^sub>2 \<gg>\<^sub>P\<^sub>L \<ff>\<^sub>P\<^sub>L\<close>
    and ?II_II = \<open>\<up>\<up>\<rightarrow>\<up>\<up>\<^sub>C\<^sub>F \<CC> \<aa>\<^sub>P\<^sub>L\<^sub>2 \<bb>\<^sub>P\<^sub>L\<^sub>2 \<gg>\<^sub>P\<^sub>L \<ff>\<^sub>P\<^sub>L \<aa> \<bb> \<gg> \<ff>\<close>
    and ?F = \<open>set {\<gg>\<^sub>P\<^sub>L, \<ff>\<^sub>P\<^sub>L}\<close>
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<epsilon>\<lparr>NTMap\<rparr>\<lparr>\<bb>\<^sub>P\<^sub>L\<^sub>2\<rparr> = \<gg> \<circ>\<^sub>A\<^bsub>\<CC>\<^esub> \<epsilon>\<lparr>NTMap\<rparr>\<lparr>\<aa>\<^sub>P\<^sub>L\<^sub>2\<rparr>
 2. \<epsilon>\<lparr>NTMap\<rparr>\<lparr>\<bb>\<^sub>P\<^sub>L\<^sub>2\<rparr> = \<ff> \<circ>\<^sub>A\<^bsub>\<CC>\<^esub> \<epsilon>\<lparr>NTMap\<rparr>\<lparr>\<aa>\<^sub>P\<^sub>L\<^sub>2\<rparr>
[PROOF STEP]
interpret \<epsilon>: is_cat_cone \<alpha> E ?II \<CC> ?II_II \<epsilon>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<epsilon> : E <\<^sub>C\<^sub>F\<^sub>.\<^sub>c\<^sub>o\<^sub>n\<^sub>e \<up>\<up>\<rightarrow>\<up>\<up>\<^sub>C\<^sub>F \<CC> \<aa>\<^sub>P\<^sub>L\<^sub>2 \<bb>\<^sub>P\<^sub>L\<^sub>2 \<gg>\<^sub>P\<^sub>L \<ff>\<^sub>P\<^sub>L \<aa> \<bb> \<gg> \<ff> : \<up>\<up>\<^sub>C \<aa>\<^sub>P\<^sub>L\<^sub>2 \<bb>\<^sub>P\<^sub>L\<^sub>2 \<gg>\<^sub>P\<^sub>L \<ff>\<^sub>P\<^sub>L \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>
[PROOF STEP]
by (rule assms(1))
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<epsilon>\<lparr>NTMap\<rparr>\<lparr>\<bb>\<^sub>P\<^sub>L\<^sub>2\<rparr> = \<gg> \<circ>\<^sub>A\<^bsub>\<CC>\<^esub> \<epsilon>\<lparr>NTMap\<rparr>\<lparr>\<aa>\<^sub>P\<^sub>L\<^sub>2\<rparr>
 2. \<epsilon>\<lparr>NTMap\<rparr>\<lparr>\<bb>\<^sub>P\<^sub>L\<^sub>2\<rparr> = \<ff> \<circ>\<^sub>A\<^bsub>\<CC>\<^esub> \<epsilon>\<lparr>NTMap\<rparr>\<lparr>\<aa>\<^sub>P\<^sub>L\<^sub>2\<rparr>
[PROOF STEP]
from \<epsilon>.cat_PL2_\<ff> \<epsilon>.cat_PL2_\<gg>
[PROOF STATE]
proof (chain)
picking this:
\<ff>\<^sub>P\<^sub>L \<in>\<^sub>\<circ> Vset \<alpha>
\<gg>\<^sub>P\<^sub>L \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
have \<gg>\<ff>: "?F \<in>\<^sub>\<circ> Vset \<alpha>"
[PROOF STATE]
proof (prove)
using this:
\<ff>\<^sub>P\<^sub>L \<in>\<^sub>\<circ> Vset \<alpha>
\<gg>\<^sub>P\<^sub>L \<in>\<^sub>\<circ> Vset \<alpha>

goal (1 subgoal):
 1. ZFC_in_HOL.set {\<gg>\<^sub>P\<^sub>L, \<ff>\<^sub>P\<^sub>L} \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
by (intro Limit_vdoubleton_in_VsetI)  auto
[PROOF STATE]
proof (state)
this:
ZFC_in_HOL.set {\<gg>\<^sub>P\<^sub>L, \<ff>\<^sub>P\<^sub>L} \<in>\<^sub>\<circ> Vset \<alpha>

goal (2 subgoals):
 1. \<epsilon>\<lparr>NTMap\<rparr>\<lparr>\<bb>\<^sub>P\<^sub>L\<^sub>2\<rparr> = \<gg> \<circ>\<^sub>A\<^bsub>\<CC>\<^esub> \<epsilon>\<lparr>NTMap\<rparr>\<lparr>\<aa>\<^sub>P\<^sub>L\<^sub>2\<rparr>
 2. \<epsilon>\<lparr>NTMap\<rparr>\<lparr>\<bb>\<^sub>P\<^sub>L\<^sub>2\<rparr> = \<ff> \<circ>\<^sub>A\<^bsub>\<CC>\<^esub> \<epsilon>\<lparr>NTMap\<rparr>\<lparr>\<aa>\<^sub>P\<^sub>L\<^sub>2\<rparr>
[PROOF STEP]
from assms(2,3)
[PROOF STATE]
proof (chain)
picking this:
\<gg> : \<aa> \<mapsto>\<^bsub>\<CC>\<^esub> \<bb>
\<ff> : \<aa> \<mapsto>\<^bsub>\<CC>\<^esub> \<bb>
[PROOF STEP]
have
    "(\<And>\<ff>'. \<ff>' \<in>\<^sub>\<circ> ?F \<Longrightarrow> (\<lambda>f\<in>\<^sub>\<circ>?F. (f = \<ff>\<^sub>P\<^sub>L ? \<ff> : \<gg>))\<lparr>\<ff>'\<rparr> : \<aa> \<mapsto>\<^bsub>\<CC>\<^esub> \<bb>)"
[PROOF STATE]
proof (prove)
using this:
\<gg> : \<aa> \<mapsto>\<^bsub>\<CC>\<^esub> \<bb>
\<ff> : \<aa> \<mapsto>\<^bsub>\<CC>\<^esub> \<bb>

goal (1 subgoal):
 1. \<And>\<ff>'. \<ff>' \<in>\<^sub>\<circ> ZFC_in_HOL.set {\<gg>\<^sub>P\<^sub>L, \<ff>\<^sub>P\<^sub>L} \<Longrightarrow> (\<lambda>f\<in>\<^sub>\<circ>ZFC_in_HOL.set {\<gg>\<^sub>P\<^sub>L, \<ff>\<^sub>P\<^sub>L}. if f = \<ff>\<^sub>P\<^sub>L \<Rightarrow> \<ff> | otherwise \<Rightarrow> \<gg>)\<lparr>\<ff>'\<rparr> : \<aa> \<mapsto>\<^bsub>\<CC>\<^esub> \<bb>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
?\<ff>' \<in>\<^sub>\<circ> ZFC_in_HOL.set {\<gg>\<^sub>P\<^sub>L, \<ff>\<^sub>P\<^sub>L} \<Longrightarrow> (\<lambda>f\<in>\<^sub>\<circ>ZFC_in_HOL.set {\<gg>\<^sub>P\<^sub>L, \<ff>\<^sub>P\<^sub>L}. if f = \<ff>\<^sub>P\<^sub>L \<Rightarrow> \<ff> | otherwise \<Rightarrow> \<gg>)\<lparr>?\<ff>'\<rparr> : \<aa> \<mapsto>\<^bsub>\<CC>\<^esub> \<bb>

goal (2 subgoals):
 1. \<epsilon>\<lparr>NTMap\<rparr>\<lparr>\<bb>\<^sub>P\<^sub>L\<^sub>2\<rparr> = \<gg> \<circ>\<^sub>A\<^bsub>\<CC>\<^esub> \<epsilon>\<lparr>NTMap\<rparr>\<lparr>\<aa>\<^sub>P\<^sub>L\<^sub>2\<rparr>
 2. \<epsilon>\<lparr>NTMap\<rparr>\<lparr>\<bb>\<^sub>P\<^sub>L\<^sub>2\<rparr> = \<ff> \<circ>\<^sub>A\<^bsub>\<CC>\<^esub> \<epsilon>\<lparr>NTMap\<rparr>\<lparr>\<aa>\<^sub>P\<^sub>L\<^sub>2\<rparr>
[PROOF STEP]
note cat_cone_cf_par_eps_NTMap_app = cat_cone_cf_par_eps_NTMap_app
      [
        OF
          assms(1)[
            unfolded
              the_cat_parallel_2_def the_cf_parallel_2_def \<aa>\<^sub>P\<^sub>L\<^sub>2_def \<bb>\<^sub>P\<^sub>L\<^sub>2_def
            ],
        folded \<aa>\<^sub>P\<^sub>L\<^sub>2_def \<bb>\<^sub>P\<^sub>L\<^sub>2_def, OF _ \<gg>\<ff> _ this,
        simplified
      ]
[PROOF STATE]
proof (state)
this:
?\<ff> = \<gg>\<^sub>P\<^sub>L \<or> ?\<ff> = \<ff>\<^sub>P\<^sub>L \<Longrightarrow> \<epsilon>\<lparr>NTMap\<rparr>\<lparr>\<bb>\<^sub>P\<^sub>L\<^sub>2\<rparr> = (\<lambda>f\<in>\<^sub>\<circ>ZFC_in_HOL.set {\<gg>\<^sub>P\<^sub>L, \<ff>\<^sub>P\<^sub>L}. if f = \<ff>\<^sub>P\<^sub>L \<Rightarrow> \<ff> | otherwise \<Rightarrow> \<gg>)\<lparr>?\<ff>\<rparr> \<circ>\<^sub>A\<^bsub>\<CC>\<^esub> \<epsilon>\<lparr>NTMap\<rparr>\<lparr>\<aa>\<^sub>P\<^sub>L\<^sub>2\<rparr>

goal (2 subgoals):
 1. \<epsilon>\<lparr>NTMap\<rparr>\<lparr>\<bb>\<^sub>P\<^sub>L\<^sub>2\<rparr> = \<gg> \<circ>\<^sub>A\<^bsub>\<CC>\<^esub> \<epsilon>\<lparr>NTMap\<rparr>\<lparr>\<aa>\<^sub>P\<^sub>L\<^sub>2\<rparr>
 2. \<epsilon>\<lparr>NTMap\<rparr>\<lparr>\<bb>\<^sub>P\<^sub>L\<^sub>2\<rparr> = \<ff> \<circ>\<^sub>A\<^bsub>\<CC>\<^esub> \<epsilon>\<lparr>NTMap\<rparr>\<lparr>\<aa>\<^sub>P\<^sub>L\<^sub>2\<rparr>
[PROOF STEP]
from
    cat_cone_cf_par_eps_NTMap_app[of \<gg>\<^sub>P\<^sub>L, simplified]
    cat_cone_cf_par_eps_NTMap_app[of \<ff>\<^sub>P\<^sub>L, simplified]
    cat_PL2_\<gg>\<ff>
[PROOF STATE]
proof (chain)
picking this:
\<epsilon>\<lparr>NTMap\<rparr>\<lparr>\<bb>\<^sub>P\<^sub>L\<^sub>2\<rparr> = (if \<gg>\<^sub>P\<^sub>L = \<ff>\<^sub>P\<^sub>L \<Rightarrow> \<ff> | otherwise \<Rightarrow> \<gg>) \<circ>\<^sub>A\<^bsub>\<CC>\<^esub> \<epsilon>\<lparr>NTMap\<rparr>\<lparr>\<aa>\<^sub>P\<^sub>L\<^sub>2\<rparr>
\<epsilon>\<lparr>NTMap\<rparr>\<lparr>\<bb>\<^sub>P\<^sub>L\<^sub>2\<rparr> = \<ff> \<circ>\<^sub>A\<^bsub>\<CC>\<^esub> \<epsilon>\<lparr>NTMap\<rparr>\<lparr>\<aa>\<^sub>P\<^sub>L\<^sub>2\<rparr>
\<gg>\<^sub>P\<^sub>L \<noteq> \<ff>\<^sub>P\<^sub>L
[PROOF STEP]
show
    "\<epsilon>\<lparr>NTMap\<rparr>\<lparr>\<bb>\<^sub>P\<^sub>L\<^sub>2\<rparr> = \<gg> \<circ>\<^sub>A\<^bsub>\<CC>\<^esub> \<epsilon>\<lparr>NTMap\<rparr>\<lparr>\<aa>\<^sub>P\<^sub>L\<^sub>2\<rparr>"
    "\<epsilon>\<lparr>NTMap\<rparr>\<lparr>\<bb>\<^sub>P\<^sub>L\<^sub>2\<rparr> = \<ff> \<circ>\<^sub>A\<^bsub>\<CC>\<^esub> \<epsilon>\<lparr>NTMap\<rparr>\<lparr>\<aa>\<^sub>P\<^sub>L\<^sub>2\<rparr>"
[PROOF STATE]
proof (prove)
using this:
\<epsilon>\<lparr>NTMap\<rparr>\<lparr>\<bb>\<^sub>P\<^sub>L\<^sub>2\<rparr> = (if \<gg>\<^sub>P\<^sub>L = \<ff>\<^sub>P\<^sub>L \<Rightarrow> \<ff> | otherwise \<Rightarrow> \<gg>) \<circ>\<^sub>A\<^bsub>\<CC>\<^esub> \<epsilon>\<lparr>NTMap\<rparr>\<lparr>\<aa>\<^sub>P\<^sub>L\<^sub>2\<rparr>
\<epsilon>\<lparr>NTMap\<rparr>\<lparr>\<bb>\<^sub>P\<^sub>L\<^sub>2\<rparr> = \<ff> \<circ>\<^sub>A\<^bsub>\<CC>\<^esub> \<epsilon>\<lparr>NTMap\<rparr>\<lparr>\<aa>\<^sub>P\<^sub>L\<^sub>2\<rparr>
\<gg>\<^sub>P\<^sub>L \<noteq> \<ff>\<^sub>P\<^sub>L

goal (1 subgoal):
 1. \<epsilon>\<lparr>NTMap\<rparr>\<lparr>\<bb>\<^sub>P\<^sub>L\<^sub>2\<rparr> = \<gg> \<circ>\<^sub>A\<^bsub>\<CC>\<^esub> \<epsilon>\<lparr>NTMap\<rparr>\<lparr>\<aa>\<^sub>P\<^sub>L\<^sub>2\<rparr> &&& \<epsilon>\<lparr>NTMap\<rparr>\<lparr>\<bb>\<^sub>P\<^sub>L\<^sub>2\<rparr> = \<ff> \<circ>\<^sub>A\<^bsub>\<CC>\<^esub> \<epsilon>\<lparr>NTMap\<rparr>\<lparr>\<aa>\<^sub>P\<^sub>L\<^sub>2\<rparr>
[PROOF STEP]
by fastforce+
[PROOF STATE]
proof (state)
this:
\<epsilon>\<lparr>NTMap\<rparr>\<lparr>\<bb>\<^sub>P\<^sub>L\<^sub>2\<rparr> = \<gg> \<circ>\<^sub>A\<^bsub>\<CC>\<^esub> \<epsilon>\<lparr>NTMap\<rparr>\<lparr>\<aa>\<^sub>P\<^sub>L\<^sub>2\<rparr>
\<epsilon>\<lparr>NTMap\<rparr>\<lparr>\<bb>\<^sub>P\<^sub>L\<^sub>2\<rparr> = \<ff> \<circ>\<^sub>A\<^bsub>\<CC>\<^esub> \<epsilon>\<lparr>NTMap\<rparr>\<lparr>\<aa>\<^sub>P\<^sub>L\<^sub>2\<rparr>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma Bex_image [reversal_rule]: assumes "(g \<circ> f) ` A = A" shows "Bex (f ` A) (P \<circ> g) = Bex A P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Bex (f ` A) (P \<circ> g) = Bex A P
[PROOF STEP]
unfolding Bex_image_comp[symmetric] image_comp \<open>(g \<circ> f) ` A = A\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Bex A P = Bex A P
[PROOF STEP]
..

  \<comment> \<open>\<^const>\<open>insert\<close>\<close>


[STATEMENT]
lemma path_concatenation_cycle_free:
  assumes "forward_terminating_path x"
      and "backward_terminating_path y"
      and "end_points x = start_points y"
      and "x;1 \<cdot> y\<^sup>T;1 = 0"
    shows "path (x+y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. path (x + y)
[PROOF STEP]
apply (rule path_concatenation,simp_all add: assms)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x ; 1 \<cdot> (x\<^sup>T ; 1 + y ; 1) \<cdot> y\<^sup>T ; 1 = 0
[PROOF STEP]
by (metis assms(4) inf.left_commute inf_bot_right inf_commute)