[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