euler_unit_count_product_balance

forall l a m b c d e t P Q w. (exists eut_code_eu_balance_count eut_scale_eu_balance_count. (forall eut_index_eu_balance_count_mask. (exists eut_gap_eu_balance_count_mask_bound. eut_gap_eu_balance_count_mask_bound + S (eut_index_eu_balance_count_mask) = (l)) -> exists eut_bit_eu_balance_count_mask. (((exists fs_h_eut_eu_balance_count_mask_entry. fs_h_eut_eu_balance_count_mask_entry + S (eut_bit_eu_balance_count_mask) = S ((S (eut_index_eu_balance_count_mask)) * eut_scale_eu_balance_count)) /\ exists fs_q_eut_eu_balance_count_mask_entry. eut_code_eu_balance_count = fs_q_eut_eu_balance_count_mask_entry * S ((S (eut_index_eu_balance_count_mask)) * eut_scale_eu_balance_count) + (eut_bit_eu_balance_count_mask))) /\ ((((forall eut_divisor_eu_balance_count_mask_choice_coprime. (exists eut_left_eu_balance_count_mask_choice_coprime. (eut_index_eu_balance_count_mask) = eut_divisor_eu_balance_count_mask_choice_coprime * eut_left_eu_balance_count_mask_choice_coprime) -> (exists eut_right_eu_balance_count_mask_choice_coprime. (m) = eut_divisor_eu_balance_count_mask_choice_coprime * eut_right_eu_balance_count_mask_choice_coprime) -> eut_divisor_eu_balance_count_mask_choice_coprime = 1) /\ (eut_bit_eu_balance_count_mask) = 1) \/ (~(forall eut_divisor_eu_balance_count_mask_choice_coprime. (exists eut_left_eu_balance_count_mask_choice_coprime. (eut_index_eu_balance_count_mask) = eut_divisor_eu_balance_count_mask_choice_coprime * eut_left_eu_balance_count_mask_choice_coprime) -> (exists eut_right_eu_balance_count_mask_choice_coprime. (m) = eut_divisor_eu_balance_count_mask_choice_coprime * eut_right_eu_balance_count_mask_choice_coprime) -> eut_divisor_eu_balance_count_mask_choice_coprime = 1) /\ (eut_bit_eu_balance_count_mask) = 0)))) /\ (exists fs_u_eut_eu_balance_count_sum fs_v_eut_eu_balance_count_sum. ((((exists fs_h_eut_eu_balance_count_sum_body_start. fs_h_eut_eu_balance_count_sum_body_start + S (0) = S ((S (0)) * fs_v_eut_eu_balance_count_sum)) /\ exists fs_q_eut_eu_balance_count_sum_body_start. fs_u_eut_eu_balance_count_sum = fs_q_eut_eu_balance_count_sum_body_start * S ((S (0)) * fs_v_eut_eu_balance_count_sum) + (0))) /\ ((((exists fs_h_eut_eu_balance_count_sum_body_terminal. fs_h_eut_eu_balance_count_sum_body_terminal + S (t) = S ((S (l)) * fs_v_eut_eu_balance_count_sum)) /\ exists fs_q_eut_eu_balance_count_sum_body_terminal. fs_u_eut_eu_balance_count_sum = fs_q_eut_eu_balance_count_sum_body_terminal * S ((S (l)) * fs_v_eut_eu_balance_count_sum) + (t))) /\ forall fs_i_eut_eu_balance_count_sum_body_steps. (exists fs_lt_eut_eu_balance_count_sum_body_steps_bound. fs_lt_eut_eu_balance_count_sum_body_steps_bound + S fs_i_eut_eu_balance_count_sum_body_steps = l) -> exists fs_a_eut_eu_balance_count_sum_body_steps fs_r_eut_eu_balance_count_sum_body_steps fs_s_eut_eu_balance_count_sum_body_steps. ((((exists fs_h_eut_eu_balance_count_sum_body_steps_summand. fs_h_eut_eu_balance_count_sum_body_steps_summand + S (fs_a_eut_eu_balance_count_sum_body_steps) = S ((S (fs_i_eut_eu_balance_count_sum_body_steps)) * eut_scale_eu_balance_count)) /\ exists fs_q_eut_eu_balance_count_sum_body_steps_summand. eut_code_eu_balance_count = fs_q_eut_eu_balance_count_sum_body_steps_summand * S ((S (fs_i_eut_eu_balance_count_sum_body_steps)) * eut_scale_eu_balance_count) + (fs_a_eut_eu_balance_count_sum_body_steps))) /\ ((((exists fs_h_eut_eu_balance_count_sum_body_steps_partial. fs_h_eut_eu_balance_count_sum_body_steps_partial + S (fs_r_eut_eu_balance_count_sum_body_steps) = S ((S (fs_i_eut_eu_balance_count_sum_body_steps)) * fs_v_eut_eu_balance_count_sum)) /\ exists fs_q_eut_eu_balance_count_sum_body_steps_partial. fs_u_eut_eu_balance_count_sum = fs_q_eut_eu_balance_count_sum_body_steps_partial * S ((S (fs_i_eut_eu_balance_count_sum_body_steps)) * fs_v_eut_eu_balance_count_sum) + (fs_r_eut_eu_balance_count_sum_body_steps))) /\ ((((exists fs_h_eut_eu_balance_count_sum_body_steps_successor. fs_h_eut_eu_balance_count_sum_body_steps_successor + S (fs_s_eut_eu_balance_count_sum_body_steps) = S ((S (S fs_i_eut_eu_balance_count_sum_body_steps)) * fs_v_eut_eu_balance_count_sum)) /\ exists fs_q_eut_eu_balance_count_sum_body_steps_successor. fs_u_eut_eu_balance_count_sum = fs_q_eut_eu_balance_count_sum_body_steps_successor * S ((S (S fs_i_eut_eu_balance_count_sum_body_steps)) * fs_v_eut_eu_balance_count_sum) + (fs_s_eut_eu_balance_count_sum_body_steps))) /\ fs_s_eut_eu_balance_count_sum_body_steps = fs_r_eut_eu_balance_count_sum_body_steps + fs_a_eut_eu_balance_count_sum_body_steps))))))) -> (forall eu_scale_index_balance_scale eu_scale_source_balance_scale eu_scale_target_balance_scale. (exists eut_gap_eu_balance_scale_index. eut_gap_eu_balance_scale_index + S (eu_scale_index_balance_scale) = (l)) -> (((exists fs_h_eu_balance_scale_source. fs_h_eu_balance_scale_source + S (eu_scale_source_balance_scale) = S ((S (eu_scale_index_balance_scale)) * c)) /\ exists fs_q_eu_balance_scale_source. b = fs_q_eu_balance_scale_source * S ((S (eu_scale_index_balance_scale)) * c) + (eu_scale_source_balance_scale))) -> (((exists fs_h_eu_balance_scale_target. fs_h_eu_balance_scale_target + S (eu_scale_target_balance_scale) = S ((S (eu_scale_index_balance_scale)) * e)) /\ exists fs_q_eu_balance_scale_target. d = fs_q_eu_balance_scale_target * S ((S (eu_scale_index_balance_scale)) * e) + (eu_scale_target_balance_scale))) -> (((forall eut_divisor_eu_balance_scale_unit. (exists eut_left_eu_balance_scale_unit. (eu_scale_index_balance_scale) = eut_divisor_eu_balance_scale_unit * eut_left_eu_balance_scale_unit) -> (exists eut_right_eu_balance_scale_unit. (m) = eut_divisor_eu_balance_scale_unit * eut_right_eu_balance_scale_unit) -> eut_divisor_eu_balance_scale_unit = 1) -> (exists eu_mod_left_balance_scale_scaled eu_mod_right_balance_scale_scaled. ((a)*eu_scale_source_balance_scale) + (m) * eu_mod_left_balance_scale_scaled = (eu_scale_target_balance_scale) + (m) * eu_mod_right_balance_scale_scaled)) /\ (~(forall eut_divisor_eu_balance_scale_unit. (exists eut_left_eu_balance_scale_unit. (eu_scale_index_balance_scale) = eut_divisor_eu_balance_scale_unit * eut_left_eu_balance_scale_unit) -> (exists eut_right_eu_balance_scale_unit. (m) = eut_divisor_eu_balance_scale_unit * eut_right_eu_balance_scale_unit) -> eut_divisor_eu_balance_scale_unit = 1) -> (exists eu_mod_left_balance_scale_unchanged eu_mod_right_balance_scale_unchanged. (eu_scale_source_balance_scale) + (m) * eu_mod_left_balance_scale_unchanged = (eu_scale_target_balance_scale) + (m) * eu_mod_right_balance_scale_unchanged)))) -> (exists ff_u_fsat_eu_balance_source ff_v_fsat_eu_balance_source. ((((exists ff_h_fsat_eu_balance_source_start. ff_h_fsat_eu_balance_source_start + S (1) = S ((S (0)) * ff_v_fsat_eu_balance_source)) /\ exists ff_q_fsat_eu_balance_source_start. ff_u_fsat_eu_balance_source = ff_q_fsat_eu_balance_source_start * S ((S (0)) * ff_v_fsat_eu_balance_source) + (1))) /\ ((((exists ff_h_fsat_eu_balance_source_terminal. ff_h_fsat_eu_balance_source_terminal + S (P) = S ((S (l)) * ff_v_fsat_eu_balance_source)) /\ exists ff_q_fsat_eu_balance_source_terminal. ff_u_fsat_eu_balance_source = ff_q_fsat_eu_balance_source_terminal * S ((S (l)) * ff_v_fsat_eu_balance_source) + (P))) /\ forall ff_i_fsat_eu_balance_source. (exists ff_lt_fsat_eu_balance_source_bound. ff_lt_fsat_eu_balance_source_bound + S ff_i_fsat_eu_balance_source = l) -> exists ff_p_fsat_eu_balance_source ff_r_fsat_eu_balance_source ff_s_fsat_eu_balance_source. ((((exists ff_h_fsat_eu_balance_source_factor. ff_h_fsat_eu_balance_source_factor + S (ff_p_fsat_eu_balance_source) = S ((S (ff_i_fsat_eu_balance_source)) * c)) /\ exists ff_q_fsat_eu_balance_source_factor. b = ff_q_fsat_eu_balance_source_factor * S ((S (ff_i_fsat_eu_balance_source)) * c) + (ff_p_fsat_eu_balance_source))) /\ ((((exists ff_h_fsat_eu_balance_source_partial. ff_h_fsat_eu_balance_source_partial + S (ff_r_fsat_eu_balance_source) = S ((S (ff_i_fsat_eu_balance_source)) * ff_v_fsat_eu_balance_source)) /\ exists ff_q_fsat_eu_balance_source_partial. ff_u_fsat_eu_balance_source = ff_q_fsat_eu_balance_source_partial * S ((S (ff_i_fsat_eu_balance_source)) * ff_v_fsat_eu_balance_source) + (ff_r_fsat_eu_balance_source))) /\ ((((exists ff_h_fsat_eu_balance_source_successor. ff_h_fsat_eu_balance_source_successor + S (ff_s_fsat_eu_balance_source) = S ((S (S ff_i_fsat_eu_balance_source)) * ff_v_fsat_eu_balance_source)) /\ exists ff_q_fsat_eu_balance_source_successor. ff_u_fsat_eu_balance_source = ff_q_fsat_eu_balance_source_successor * S ((S (S ff_i_fsat_eu_balance_source)) * ff_v_fsat_eu_balance_source) + (ff_s_fsat_eu_balance_source))) /\ ff_s_fsat_eu_balance_source = ff_r_fsat_eu_balance_source * ff_p_fsat_eu_balance_source)))))) -> (exists ff_u_fsat_eu_balance_target ff_v_fsat_eu_balance_target. ((((exists ff_h_fsat_eu_balance_target_start. ff_h_fsat_eu_balance_target_start + S (1) = S ((S (0)) * ff_v_fsat_eu_balance_target)) /\ exists ff_q_fsat_eu_balance_target_start. ff_u_fsat_eu_balance_target = ff_q_fsat_eu_balance_target_start * S ((S (0)) * ff_v_fsat_eu_balance_target) + (1))) /\ ((((exists ff_h_fsat_eu_balance_target_terminal. ff_h_fsat_eu_balance_target_terminal + S (Q) = S ((S (l)) * ff_v_fsat_eu_balance_target)) /\ exists ff_q_fsat_eu_balance_target_terminal. ff_u_fsat_eu_balance_target = ff_q_fsat_eu_balance_target_terminal * S ((S (l)) * ff_v_fsat_eu_balance_target) + (Q))) /\ forall ff_i_fsat_eu_balance_target. (exists ff_lt_fsat_eu_balance_target_bound. ff_lt_fsat_eu_balance_target_bound + S ff_i_fsat_eu_balance_target = l) -> exists ff_p_fsat_eu_balance_target ff_r_fsat_eu_balance_target ff_s_fsat_eu_balance_target. ((((exists ff_h_fsat_eu_balance_target_factor. ff_h_fsat_eu_balance_target_factor + S (ff_p_fsat_eu_balance_target) = S ((S (ff_i_fsat_eu_balance_target)) * e)) /\ exists ff_q_fsat_eu_balance_target_factor. d = ff_q_fsat_eu_balance_target_factor * S ((S (ff_i_fsat_eu_balance_target)) * e) + (ff_p_fsat_eu_balance_target))) /\ ((((exists ff_h_fsat_eu_balance_target_partial. ff_h_fsat_eu_balance_target_partial + S (ff_r_fsat_eu_balance_target) = S ((S (ff_i_fsat_eu_balance_target)) * ff_v_fsat_eu_balance_target)) /\ exists ff_q_fsat_eu_balance_target_partial. ff_u_fsat_eu_balance_target = ff_q_fsat_eu_balance_target_partial * S ((S (ff_i_fsat_eu_balance_target)) * ff_v_fsat_eu_balance_target) + (ff_r_fsat_eu_balance_target))) /\ ((((exists ff_h_fsat_eu_balance_target_successor. ff_h_fsat_eu_balance_target_successor + S (ff_s_fsat_eu_balance_target) = S ((S (S ff_i_fsat_eu_balance_target)) * ff_v_fsat_eu_balance_target)) /\ exists ff_q_fsat_eu_balance_target_successor. ff_u_fsat_eu_balance_target = ff_q_fsat_eu_balance_target_successor * S ((S (S ff_i_fsat_eu_balance_target)) * ff_v_fsat_eu_balance_target) + (ff_s_fsat_eu_balance_target))) /\ ff_s_fsat_eu_balance_target = ff_r_fsat_eu_balance_target * ff_p_fsat_eu_balance_target)))))) -> (exists pa_b_euta_eu_balance_power pa_c_euta_eu_balance_power. ((forall pa_i_euta_eu_balance_power_repeat. (exists pa_lt_euta_eu_balance_power_repeat_bound. pa_lt_euta_eu_balance_power_repeat_bound + S pa_i_euta_eu_balance_power_repeat = t) -> (((exists pa_h_euta_eu_balance_power_repeat_decoded. pa_h_euta_eu_balance_power_repeat_decoded + S (a) = S ((S (pa_i_euta_eu_balance_power_repeat)) * pa_c_euta_eu_balance_power)) /\ exists pa_q_euta_eu_balance_power_repeat_decoded. pa_b_euta_eu_balance_power = pa_q_euta_eu_balance_power_repeat_decoded * S ((S (pa_i_euta_eu_balance_power_repeat)) * pa_c_euta_eu_balance_power) + (a)))) /\ (exists pa_u_euta_eu_balance_power_product pa_v_euta_eu_balance_power_product. ((((exists pa_h_euta_eu_balance_power_product_start. pa_h_euta_eu_balance_power_product_start + S (1) = S ((S (0)) * pa_v_euta_eu_balance_power_product)) /\ exists pa_q_euta_eu_balance_power_product_start. pa_u_euta_eu_balance_power_product = pa_q_euta_eu_balance_power_product_start * S ((S (0)) * pa_v_euta_eu_balance_power_product) + (1))) /\ ((((exists pa_h_euta_eu_balance_power_product_terminal. pa_h_euta_eu_balance_power_product_terminal + S (w) = S ((S (t)) * pa_v_euta_eu_balance_power_product)) /\ exists pa_q_euta_eu_balance_power_product_terminal. pa_u_euta_eu_balance_power_product = pa_q_euta_eu_balance_power_product_terminal * S ((S (t)) * pa_v_euta_eu_balance_power_product) + (w))) /\ forall pa_i_euta_eu_balance_power_product. (exists pa_lt_euta_eu_balance_power_product_bound. pa_lt_euta_eu_balance_power_product_bound + S pa_i_euta_eu_balance_power_product = t) -> exists pa_p_euta_eu_balance_power_product pa_r_euta_eu_balance_power_product pa_s_euta_eu_balance_power_product. ((((exists pa_h_euta_eu_balance_power_product_factor. pa_h_euta_eu_balance_power_product_factor + S (pa_p_euta_eu_balance_power_product) = S ((S (pa_i_euta_eu_balance_power_product)) * pa_c_euta_eu_balance_power)) /\ exists pa_q_euta_eu_balance_power_product_factor. pa_b_euta_eu_balance_power = pa_q_euta_eu_balance_power_product_factor * S ((S (pa_i_euta_eu_balance_power_product)) * pa_c_euta_eu_balance_power) + (pa_p_euta_eu_balance_power_product))) /\ ((((exists pa_h_euta_eu_balance_power_product_partial. pa_h_euta_eu_balance_power_product_partial + S (pa_r_euta_eu_balance_power_product) = S ((S (pa_i_euta_eu_balance_power_product)) * pa_v_euta_eu_balance_power_product)) /\ exists pa_q_euta_eu_balance_power_product_partial. pa_u_euta_eu_balance_power_product = pa_q_euta_eu_balance_power_product_partial * S ((S (pa_i_euta_eu_balance_power_product)) * pa_v_euta_eu_balance_power_product) + (pa_r_euta_eu_balance_power_product))) /\ ((((exists pa_h_euta_eu_balance_power_product_successor. pa_h_euta_eu_balance_power_product_successor + S (pa_s_euta_eu_balance_power_product) = S ((S (S pa_i_euta_eu_balance_power_product)) * pa_v_euta_eu_balance_power_product)) /\ exists pa_q_euta_eu_balance_power_product_successor. pa_u_euta_eu_balance_power_product = pa_q_euta_eu_balance_power_product_successor * S ((S (S pa_i_euta_eu_balance_power_product)) * pa_v_euta_eu_balance_power_product) + (pa_s_euta_eu_balance_power_product))) /\ pa_s_euta_eu_balance_power_product = pa_r_euta_eu_balance_power_product * pa_p_euta_eu_balance_power_product)))))))) -> (exists eu_mod_left_balance_result eu_mod_right_balance_result. (w*P) + (m) * eu_mod_left_balance_result = (Q) + (m) * eu_mod_right_balance_result)