signed_multiplicative_product_values_exist

Exact expanded first-order arithmetic statement

forall N F a b. (((~((N)=0)) /\ (((exists dst_positive_code_values_sourcetable dst_positive_scale_values_sourcetable dst_negative_code_values_sourcetable dst_negative_scale_values_sourcetable. (((F) = (((((dst_positive_code_values_sourcetable) + (dst_positive_scale_values_sourcetable)) * S ((dst_positive_code_values_sourcetable) + (dst_positive_scale_values_sourcetable)) + ((dst_positive_scale_values_sourcetable) + (dst_positive_scale_values_sourcetable))) + (((dst_negative_code_values_sourcetable) + (dst_negative_scale_values_sourcetable)) * S ((dst_negative_code_values_sourcetable) + (dst_negative_scale_values_sourcetable)) + ((dst_negative_scale_values_sourcetable) + (dst_negative_scale_values_sourcetable)))) * S ((((dst_positive_code_values_sourcetable) + (dst_positive_scale_values_sourcetable)) * S ((dst_positive_code_values_sourcetable) + (dst_positive_scale_values_sourcetable)) + ((dst_positive_scale_values_sourcetable) + (dst_positive_scale_values_sourcetable))) + (((dst_negative_code_values_sourcetable) + (dst_negative_scale_values_sourcetable)) * S ((dst_negative_code_values_sourcetable) + (dst_negative_scale_values_sourcetable)) + ((dst_negative_scale_values_sourcetable) + (dst_negative_scale_values_sourcetable)))) + ((((dst_negative_code_values_sourcetable) + (dst_negative_scale_values_sourcetable)) * S ((dst_negative_code_values_sourcetable) + (dst_negative_scale_values_sourcetable)) + ((dst_negative_scale_values_sourcetable) + (dst_negative_scale_values_sourcetable))) + (((dst_negative_code_values_sourcetable) + (dst_negative_scale_values_sourcetable)) * S ((dst_negative_code_values_sourcetable) + (dst_negative_scale_values_sourcetable)) + ((dst_negative_scale_values_sourcetable) + (dst_negative_scale_values_sourcetable)))))) /\ (forall dst_index_values_sourcetable. (exists pvs_le_gap_values_sourcetabledomain. pvs_le_gap_values_sourcetabledomain + (dst_index_values_sourcetable) = (N)) -> exists dst_positive_values_sourcetable dst_negative_values_sourcetable dst_value_values_sourcetable. ((((exists ff_h_pvs_values_sourcetableentrypositive. ff_h_pvs_values_sourcetableentrypositive + S (dst_positive_values_sourcetable) = S ((S (dst_index_values_sourcetable)) * dst_positive_scale_values_sourcetable)) /\ exists ff_q_pvs_values_sourcetableentrypositive. dst_positive_code_values_sourcetable = ff_q_pvs_values_sourcetableentrypositive * S ((S (dst_index_values_sourcetable)) * dst_positive_scale_values_sourcetable) + (dst_positive_values_sourcetable))) /\ (((((exists ff_h_pvs_values_sourcetableentrynegative. ff_h_pvs_values_sourcetableentrynegative + S (dst_negative_values_sourcetable) = S ((S (dst_index_values_sourcetable)) * dst_negative_scale_values_sourcetable)) /\ exists ff_q_pvs_values_sourcetableentrynegative. dst_negative_code_values_sourcetable = ff_q_pvs_values_sourcetableentrynegative * S ((S (dst_index_values_sourcetable)) * dst_negative_scale_values_sourcetable) + (dst_negative_values_sourcetable))) /\ (exists ge_balance_positive_values_sourcetableentryvalue ge_balance_negative_values_sourcetableentryvalue. (((((dst_value_values_sourcetable) = 2 * (ge_balance_positive_values_sourcetableentryvalue) /\ (ge_balance_negative_values_sourcetableentryvalue) = 0) \/ exists ge_signed_half_values_sourcetableentryvaluedecode. (((dst_value_values_sourcetable) = 2 * ge_signed_half_values_sourcetableentryvaluedecode + 1 /\ (ge_balance_positive_values_sourcetableentryvalue) = 0) /\ (ge_balance_negative_values_sourcetableentryvalue) = S ge_signed_half_values_sourcetableentryvaluedecode))) /\ ((dst_positive_values_sourcetable) + ge_balance_negative_values_sourcetableentryvalue = (dst_negative_values_sourcetable) + ge_balance_positive_values_sourcetableentryvalue))))))))) /\ (((exists dst_positive_code_values_sourceone dst_positive_scale_values_sourceone dst_negative_code_values_sourceone dst_negative_scale_values_sourceone dst_positive_values_sourceone dst_negative_values_sourceone. (((F) = (((((dst_positive_code_values_sourceone) + (dst_positive_scale_values_sourceone)) * S ((dst_positive_code_values_sourceone) + (dst_positive_scale_values_sourceone)) + ((dst_positive_scale_values_sourceone) + (dst_positive_scale_values_sourceone))) + (((dst_negative_code_values_sourceone) + (dst_negative_scale_values_sourceone)) * S ((dst_negative_code_values_sourceone) + (dst_negative_scale_values_sourceone)) + ((dst_negative_scale_values_sourceone) + (dst_negative_scale_values_sourceone)))) * S ((((dst_positive_code_values_sourceone) + (dst_positive_scale_values_sourceone)) * S ((dst_positive_code_values_sourceone) + (dst_positive_scale_values_sourceone)) + ((dst_positive_scale_values_sourceone) + (dst_positive_scale_values_sourceone))) + (((dst_negative_code_values_sourceone) + (dst_negative_scale_values_sourceone)) * S ((dst_negative_code_values_sourceone) + (dst_negative_scale_values_sourceone)) + ((dst_negative_scale_values_sourceone) + (dst_negative_scale_values_sourceone)))) + ((((dst_negative_code_values_sourceone) + (dst_negative_scale_values_sourceone)) * S ((dst_negative_code_values_sourceone) + (dst_negative_scale_values_sourceone)) + ((dst_negative_scale_values_sourceone) + (dst_negative_scale_values_sourceone))) + (((dst_negative_code_values_sourceone) + (dst_negative_scale_values_sourceone)) * S ((dst_negative_code_values_sourceone) + (dst_negative_scale_values_sourceone)) + ((dst_negative_scale_values_sourceone) + (dst_negative_scale_values_sourceone)))))) /\ (((((exists ff_h_pvs_values_sourceonepositive. ff_h_pvs_values_sourceonepositive + S (dst_positive_values_sourceone) = S ((S (1)) * dst_positive_scale_values_sourceone)) /\ exists ff_q_pvs_values_sourceonepositive. dst_positive_code_values_sourceone = ff_q_pvs_values_sourceonepositive * S ((S (1)) * dst_positive_scale_values_sourceone) + (dst_positive_values_sourceone))) /\ (((((exists ff_h_pvs_values_sourceonenegative. ff_h_pvs_values_sourceonenegative + S (dst_negative_values_sourceone) = S ((S (1)) * dst_negative_scale_values_sourceone)) /\ exists ff_q_pvs_values_sourceonenegative. dst_negative_code_values_sourceone = ff_q_pvs_values_sourceonenegative * S ((S (1)) * dst_negative_scale_values_sourceone) + (dst_negative_values_sourceone))) /\ (exists ge_balance_positive_values_sourceonevalue ge_balance_negative_values_sourceonevalue. (((((2) = 2 * (ge_balance_positive_values_sourceonevalue) /\ (ge_balance_negative_values_sourceonevalue) = 0) \/ exists ge_signed_half_values_sourceonevaluedecode. (((2) = 2 * ge_signed_half_values_sourceonevaluedecode + 1 /\ (ge_balance_positive_values_sourceonevalue) = 0) /\ (ge_balance_negative_values_sourceonevalue) = S ge_signed_half_values_sourceonevaluedecode))) /\ ((dst_positive_values_sourceone) + ge_balance_negative_values_sourceonevalue = (dst_negative_values_sourceone) + ge_balance_positive_values_sourceonevalue))))))))) /\ (forall mp_a_values_source mp_b_values_source mp_x_values_source mp_y_values_source mp_z_values_source. ~(mp_a_values_source=0) -> ~(mp_b_values_source=0) -> (exists pvs_le_gap_values_sourcebound. pvs_le_gap_values_sourcebound + (mp_a_values_source*mp_b_values_source) = (N)) -> (forall frp_divisor_values_sourcecoprime. (exists frp_left_factor_values_sourcecoprime. mp_a_values_source = frp_divisor_values_sourcecoprime * frp_left_factor_values_sourcecoprime) -> (exists frp_right_factor_values_sourcecoprime. mp_b_values_source = frp_divisor_values_sourcecoprime * frp_right_factor_values_sourcecoprime) -> frp_divisor_values_sourcecoprime = 1) -> (exists dst_positive_code_values_sourcefirst dst_positive_scale_values_sourcefirst dst_negative_code_values_sourcefirst dst_negative_scale_values_sourcefirst dst_positive_values_sourcefirst dst_negative_values_sourcefirst. (((F) = (((((dst_positive_code_values_sourcefirst) + (dst_positive_scale_values_sourcefirst)) * S ((dst_positive_code_values_sourcefirst) + (dst_positive_scale_values_sourcefirst)) + ((dst_positive_scale_values_sourcefirst) + (dst_positive_scale_values_sourcefirst))) + (((dst_negative_code_values_sourcefirst) + (dst_negative_scale_values_sourcefirst)) * S ((dst_negative_code_values_sourcefirst) + (dst_negative_scale_values_sourcefirst)) + ((dst_negative_scale_values_sourcefirst) + (dst_negative_scale_values_sourcefirst)))) * S ((((dst_positive_code_values_sourcefirst) + (dst_positive_scale_values_sourcefirst)) * S ((dst_positive_code_values_sourcefirst) + (dst_positive_scale_values_sourcefirst)) + ((dst_positive_scale_values_sourcefirst) + (dst_positive_scale_values_sourcefirst))) + (((dst_negative_code_values_sourcefirst) + (dst_negative_scale_values_sourcefirst)) * S ((dst_negative_code_values_sourcefirst) + (dst_negative_scale_values_sourcefirst)) + ((dst_negative_scale_values_sourcefirst) + (dst_negative_scale_values_sourcefirst)))) + ((((dst_negative_code_values_sourcefirst) + (dst_negative_scale_values_sourcefirst)) * S ((dst_negative_code_values_sourcefirst) + (dst_negative_scale_values_sourcefirst)) + ((dst_negative_scale_values_sourcefirst) + (dst_negative_scale_values_sourcefirst))) + (((dst_negative_code_values_sourcefirst) + (dst_negative_scale_values_sourcefirst)) * S ((dst_negative_code_values_sourcefirst) + (dst_negative_scale_values_sourcefirst)) + ((dst_negative_scale_values_sourcefirst) + (dst_negative_scale_values_sourcefirst)))))) /\ (((((exists ff_h_pvs_values_sourcefirstpositive. ff_h_pvs_values_sourcefirstpositive + S (dst_positive_values_sourcefirst) = S ((S (mp_a_values_source)) * dst_positive_scale_values_sourcefirst)) /\ exists ff_q_pvs_values_sourcefirstpositive. dst_positive_code_values_sourcefirst = ff_q_pvs_values_sourcefirstpositive * S ((S (mp_a_values_source)) * dst_positive_scale_values_sourcefirst) + (dst_positive_values_sourcefirst))) /\ (((((exists ff_h_pvs_values_sourcefirstnegative. ff_h_pvs_values_sourcefirstnegative + S (dst_negative_values_sourcefirst) = S ((S (mp_a_values_source)) * dst_negative_scale_values_sourcefirst)) /\ exists ff_q_pvs_values_sourcefirstnegative. dst_negative_code_values_sourcefirst = ff_q_pvs_values_sourcefirstnegative * S ((S (mp_a_values_source)) * dst_negative_scale_values_sourcefirst) + (dst_negative_values_sourcefirst))) /\ (exists ge_balance_positive_values_sourcefirstvalue ge_balance_negative_values_sourcefirstvalue. (((((mp_x_values_source) = 2 * (ge_balance_positive_values_sourcefirstvalue) /\ (ge_balance_negative_values_sourcefirstvalue) = 0) \/ exists ge_signed_half_values_sourcefirstvaluedecode. (((mp_x_values_source) = 2 * ge_signed_half_values_sourcefirstvaluedecode + 1 /\ (ge_balance_positive_values_sourcefirstvalue) = 0) /\ (ge_balance_negative_values_sourcefirstvalue) = S ge_signed_half_values_sourcefirstvaluedecode))) /\ ((dst_positive_values_sourcefirst) + ge_balance_negative_values_sourcefirstvalue = (dst_negative_values_sourcefirst) + ge_balance_positive_values_sourcefirstvalue))))))))) -> (exists dst_positive_code_values_sourcesecond dst_positive_scale_values_sourcesecond dst_negative_code_values_sourcesecond dst_negative_scale_values_sourcesecond dst_positive_values_sourcesecond dst_negative_values_sourcesecond. (((F) = (((((dst_positive_code_values_sourcesecond) + (dst_positive_scale_values_sourcesecond)) * S ((dst_positive_code_values_sourcesecond) + (dst_positive_scale_values_sourcesecond)) + ((dst_positive_scale_values_sourcesecond) + (dst_positive_scale_values_sourcesecond))) + (((dst_negative_code_values_sourcesecond) + (dst_negative_scale_values_sourcesecond)) * S ((dst_negative_code_values_sourcesecond) + (dst_negative_scale_values_sourcesecond)) + ((dst_negative_scale_values_sourcesecond) + (dst_negative_scale_values_sourcesecond)))) * S ((((dst_positive_code_values_sourcesecond) + (dst_positive_scale_values_sourcesecond)) * S ((dst_positive_code_values_sourcesecond) + (dst_positive_scale_values_sourcesecond)) + ((dst_positive_scale_values_sourcesecond) + (dst_positive_scale_values_sourcesecond))) + (((dst_negative_code_values_sourcesecond) + (dst_negative_scale_values_sourcesecond)) * S ((dst_negative_code_values_sourcesecond) + (dst_negative_scale_values_sourcesecond)) + ((dst_negative_scale_values_sourcesecond) + (dst_negative_scale_values_sourcesecond)))) + ((((dst_negative_code_values_sourcesecond) + (dst_negative_scale_values_sourcesecond)) * S ((dst_negative_code_values_sourcesecond) + (dst_negative_scale_values_sourcesecond)) + ((dst_negative_scale_values_sourcesecond) + (dst_negative_scale_values_sourcesecond))) + (((dst_negative_code_values_sourcesecond) + (dst_negative_scale_values_sourcesecond)) * S ((dst_negative_code_values_sourcesecond) + (dst_negative_scale_values_sourcesecond)) + ((dst_negative_scale_values_sourcesecond) + (dst_negative_scale_values_sourcesecond)))))) /\ (((((exists ff_h_pvs_values_sourcesecondpositive. ff_h_pvs_values_sourcesecondpositive + S (dst_positive_values_sourcesecond) = S ((S (mp_b_values_source)) * dst_positive_scale_values_sourcesecond)) /\ exists ff_q_pvs_values_sourcesecondpositive. dst_positive_code_values_sourcesecond = ff_q_pvs_values_sourcesecondpositive * S ((S (mp_b_values_source)) * dst_positive_scale_values_sourcesecond) + (dst_positive_values_sourcesecond))) /\ (((((exists ff_h_pvs_values_sourcesecondnegative. ff_h_pvs_values_sourcesecondnegative + S (dst_negative_values_sourcesecond) = S ((S (mp_b_values_source)) * dst_negative_scale_values_sourcesecond)) /\ exists ff_q_pvs_values_sourcesecondnegative. dst_negative_code_values_sourcesecond = ff_q_pvs_values_sourcesecondnegative * S ((S (mp_b_values_source)) * dst_negative_scale_values_sourcesecond) + (dst_negative_values_sourcesecond))) /\ (exists ge_balance_positive_values_sourcesecondvalue ge_balance_negative_values_sourcesecondvalue. (((((mp_y_values_source) = 2 * (ge_balance_positive_values_sourcesecondvalue) /\ (ge_balance_negative_values_sourcesecondvalue) = 0) \/ exists ge_signed_half_values_sourcesecondvaluedecode. (((mp_y_values_source) = 2 * ge_signed_half_values_sourcesecondvaluedecode + 1 /\ (ge_balance_positive_values_sourcesecondvalue) = 0) /\ (ge_balance_negative_values_sourcesecondvalue) = S ge_signed_half_values_sourcesecondvaluedecode))) /\ ((dst_positive_values_sourcesecond) + ge_balance_negative_values_sourcesecondvalue = (dst_negative_values_sourcesecond) + ge_balance_positive_values_sourcesecondvalue))))))))) -> (exists dst_positive_code_values_sourceproduct dst_positive_scale_values_sourceproduct dst_negative_code_values_sourceproduct dst_negative_scale_values_sourceproduct dst_positive_values_sourceproduct dst_negative_values_sourceproduct. (((F) = (((((dst_positive_code_values_sourceproduct) + (dst_positive_scale_values_sourceproduct)) * S ((dst_positive_code_values_sourceproduct) + (dst_positive_scale_values_sourceproduct)) + ((dst_positive_scale_values_sourceproduct) + (dst_positive_scale_values_sourceproduct))) + (((dst_negative_code_values_sourceproduct) + (dst_negative_scale_values_sourceproduct)) * S ((dst_negative_code_values_sourceproduct) + (dst_negative_scale_values_sourceproduct)) + ((dst_negative_scale_values_sourceproduct) + (dst_negative_scale_values_sourceproduct)))) * S ((((dst_positive_code_values_sourceproduct) + (dst_positive_scale_values_sourceproduct)) * S ((dst_positive_code_values_sourceproduct) + (dst_positive_scale_values_sourceproduct)) + ((dst_positive_scale_values_sourceproduct) + (dst_positive_scale_values_sourceproduct))) + (((dst_negative_code_values_sourceproduct) + (dst_negative_scale_values_sourceproduct)) * S ((dst_negative_code_values_sourceproduct) + (dst_negative_scale_values_sourceproduct)) + ((dst_negative_scale_values_sourceproduct) + (dst_negative_scale_values_sourceproduct)))) + ((((dst_negative_code_values_sourceproduct) + (dst_negative_scale_values_sourceproduct)) * S ((dst_negative_code_values_sourceproduct) + (dst_negative_scale_values_sourceproduct)) + ((dst_negative_scale_values_sourceproduct) + (dst_negative_scale_values_sourceproduct))) + (((dst_negative_code_values_sourceproduct) + (dst_negative_scale_values_sourceproduct)) * S ((dst_negative_code_values_sourceproduct) + (dst_negative_scale_values_sourceproduct)) + ((dst_negative_scale_values_sourceproduct) + (dst_negative_scale_values_sourceproduct)))))) /\ (((((exists ff_h_pvs_values_sourceproductpositive. ff_h_pvs_values_sourceproductpositive + S (dst_positive_values_sourceproduct) = S ((S (mp_a_values_source*mp_b_values_source)) * dst_positive_scale_values_sourceproduct)) /\ exists ff_q_pvs_values_sourceproductpositive. dst_positive_code_values_sourceproduct = ff_q_pvs_values_sourceproductpositive * S ((S (mp_a_values_source*mp_b_values_source)) * dst_positive_scale_values_sourceproduct) + (dst_positive_values_sourceproduct))) /\ (((((exists ff_h_pvs_values_sourceproductnegative. ff_h_pvs_values_sourceproductnegative + S (dst_negative_values_sourceproduct) = S ((S (mp_a_values_source*mp_b_values_source)) * dst_negative_scale_values_sourceproduct)) /\ exists ff_q_pvs_values_sourceproductnegative. dst_negative_code_values_sourceproduct = ff_q_pvs_values_sourceproductnegative * S ((S (mp_a_values_source*mp_b_values_source)) * dst_negative_scale_values_sourceproduct) + (dst_negative_values_sourceproduct))) /\ (exists ge_balance_positive_values_sourceproductvalue ge_balance_negative_values_sourceproductvalue. (((((mp_z_values_source) = 2 * (ge_balance_positive_values_sourceproductvalue) /\ (ge_balance_negative_values_sourceproductvalue) = 0) \/ exists ge_signed_half_values_sourceproductvaluedecode. (((mp_z_values_source) = 2 * ge_signed_half_values_sourceproductvaluedecode + 1 /\ (ge_balance_positive_values_sourceproductvalue) = 0) /\ (ge_balance_negative_values_sourceproductvalue) = S ge_signed_half_values_sourceproductvaluedecode))) /\ ((dst_positive_values_sourceproduct) + ge_balance_negative_values_sourceproductvalue = (dst_negative_values_sourceproduct) + ge_balance_positive_values_sourceproductvalue))))))))) -> (exists sto_ap_values_sourcelaw sto_an_values_sourcelaw sto_bp_values_sourcelaw sto_bn_values_sourcelaw sto_cp_values_sourcelaw sto_cn_values_sourcelaw. (((((mp_x_values_source) = 2 * (sto_ap_values_sourcelaw) /\ (sto_an_values_sourcelaw) = 0) \/ exists ge_signed_half_values_sourcelawleft. (((mp_x_values_source) = 2 * ge_signed_half_values_sourcelawleft + 1 /\ (sto_ap_values_sourcelaw) = 0) /\ (sto_an_values_sourcelaw) = S ge_signed_half_values_sourcelawleft))) /\ ((((((mp_y_values_source) = 2 * (sto_bp_values_sourcelaw) /\ (sto_bn_values_sourcelaw) = 0) \/ exists ge_signed_half_values_sourcelawright. (((mp_y_values_source) = 2 * ge_signed_half_values_sourcelawright + 1 /\ (sto_bp_values_sourcelaw) = 0) /\ (sto_bn_values_sourcelaw) = S ge_signed_half_values_sourcelawright))) /\ ((((((mp_z_values_source) = 2 * (sto_cp_values_sourcelaw) /\ (sto_cn_values_sourcelaw) = 0) \/ exists ge_signed_half_values_sourcelawoutput. (((mp_z_values_source) = 2 * ge_signed_half_values_sourcelawoutput + 1 /\ (sto_cp_values_sourcelaw) = 0) /\ (sto_cn_values_sourcelaw) = S ge_signed_half_values_sourcelawoutput))) /\ ((sto_ap_values_sourcelaw * sto_bp_values_sourcelaw + sto_an_values_sourcelaw * sto_bn_values_sourcelaw) + sto_cn_values_sourcelaw = (sto_ap_values_sourcelaw * sto_bn_values_sourcelaw + sto_an_values_sourcelaw * sto_bp_values_sourcelaw) + sto_cp_values_sourcelaw)))))))))))))) -> ~(a=0) -> ~(b=0) -> (exists pvs_le_gap_values_bound. pvs_le_gap_values_bound + (a*b) = (N)) -> (forall frp_divisor_values_coprime. (exists frp_left_factor_values_coprime. a = frp_divisor_values_coprime * frp_left_factor_values_coprime) -> (exists frp_right_factor_values_coprime. b = frp_divisor_values_coprime * frp_right_factor_values_coprime) -> frp_divisor_values_coprime = 1) -> exists x y z. ((exists dst_positive_code_values_first dst_positive_scale_values_first dst_negative_code_values_first dst_negative_scale_values_first dst_positive_values_first dst_negative_values_first. (((F) = (((((dst_positive_code_values_first) + (dst_positive_scale_values_first)) * S ((dst_positive_code_values_first) + (dst_positive_scale_values_first)) + ((dst_positive_scale_values_first) + (dst_positive_scale_values_first))) + (((dst_negative_code_values_first) + (dst_negative_scale_values_first)) * S ((dst_negative_code_values_first) + (dst_negative_scale_values_first)) + ((dst_negative_scale_values_first) + (dst_negative_scale_values_first)))) * S ((((dst_positive_code_values_first) + (dst_positive_scale_values_first)) * S ((dst_positive_code_values_first) + (dst_positive_scale_values_first)) + ((dst_positive_scale_values_first) + (dst_positive_scale_values_first))) + (((dst_negative_code_values_first) + (dst_negative_scale_values_first)) * S ((dst_negative_code_values_first) + (dst_negative_scale_values_first)) + ((dst_negative_scale_values_first) + (dst_negative_scale_values_first)))) + ((((dst_negative_code_values_first) + (dst_negative_scale_values_first)) * S ((dst_negative_code_values_first) + (dst_negative_scale_values_first)) + ((dst_negative_scale_values_first) + (dst_negative_scale_values_first))) + (((dst_negative_code_values_first) + (dst_negative_scale_values_first)) * S ((dst_negative_code_values_first) + (dst_negative_scale_values_first)) + ((dst_negative_scale_values_first) + (dst_negative_scale_values_first)))))) /\ (((((exists ff_h_pvs_values_firstpositive. ff_h_pvs_values_firstpositive + S (dst_positive_values_first) = S ((S (a)) * dst_positive_scale_values_first)) /\ exists ff_q_pvs_values_firstpositive. dst_positive_code_values_first = ff_q_pvs_values_firstpositive * S ((S (a)) * dst_positive_scale_values_first) + (dst_positive_values_first))) /\ (((((exists ff_h_pvs_values_firstnegative. ff_h_pvs_values_firstnegative + S (dst_negative_values_first) = S ((S (a)) * dst_negative_scale_values_first)) /\ exists ff_q_pvs_values_firstnegative. dst_negative_code_values_first = ff_q_pvs_values_firstnegative * S ((S (a)) * dst_negative_scale_values_first) + (dst_negative_values_first))) /\ (exists ge_balance_positive_values_firstvalue ge_balance_negative_values_firstvalue. (((((x) = 2 * (ge_balance_positive_values_firstvalue) /\ (ge_balance_negative_values_firstvalue) = 0) \/ exists ge_signed_half_values_firstvaluedecode. (((x) = 2 * ge_signed_half_values_firstvaluedecode + 1 /\ (ge_balance_positive_values_firstvalue) = 0) /\ (ge_balance_negative_values_firstvalue) = S ge_signed_half_values_firstvaluedecode))) /\ ((dst_positive_values_first) + ge_balance_negative_values_firstvalue = (dst_negative_values_first) + ge_balance_positive_values_firstvalue))))))))) /\ (((exists dst_positive_code_values_second dst_positive_scale_values_second dst_negative_code_values_second dst_negative_scale_values_second dst_positive_values_second dst_negative_values_second. (((F) = (((((dst_positive_code_values_second) + (dst_positive_scale_values_second)) * S ((dst_positive_code_values_second) + (dst_positive_scale_values_second)) + ((dst_positive_scale_values_second) + (dst_positive_scale_values_second))) + (((dst_negative_code_values_second) + (dst_negative_scale_values_second)) * S ((dst_negative_code_values_second) + (dst_negative_scale_values_second)) + ((dst_negative_scale_values_second) + (dst_negative_scale_values_second)))) * S ((((dst_positive_code_values_second) + (dst_positive_scale_values_second)) * S ((dst_positive_code_values_second) + (dst_positive_scale_values_second)) + ((dst_positive_scale_values_second) + (dst_positive_scale_values_second))) + (((dst_negative_code_values_second) + (dst_negative_scale_values_second)) * S ((dst_negative_code_values_second) + (dst_negative_scale_values_second)) + ((dst_negative_scale_values_second) + (dst_negative_scale_values_second)))) + ((((dst_negative_code_values_second) + (dst_negative_scale_values_second)) * S ((dst_negative_code_values_second) + (dst_negative_scale_values_second)) + ((dst_negative_scale_values_second) + (dst_negative_scale_values_second))) + (((dst_negative_code_values_second) + (dst_negative_scale_values_second)) * S ((dst_negative_code_values_second) + (dst_negative_scale_values_second)) + ((dst_negative_scale_values_second) + (dst_negative_scale_values_second)))))) /\ (((((exists ff_h_pvs_values_secondpositive. ff_h_pvs_values_secondpositive + S (dst_positive_values_second) = S ((S (b)) * dst_positive_scale_values_second)) /\ exists ff_q_pvs_values_secondpositive. dst_positive_code_values_second = ff_q_pvs_values_secondpositive * S ((S (b)) * dst_positive_scale_values_second) + (dst_positive_values_second))) /\ (((((exists ff_h_pvs_values_secondnegative. ff_h_pvs_values_secondnegative + S (dst_negative_values_second) = S ((S (b)) * dst_negative_scale_values_second)) /\ exists ff_q_pvs_values_secondnegative. dst_negative_code_values_second = ff_q_pvs_values_secondnegative * S ((S (b)) * dst_negative_scale_values_second) + (dst_negative_values_second))) /\ (exists ge_balance_positive_values_secondvalue ge_balance_negative_values_secondvalue. (((((y) = 2 * (ge_balance_positive_values_secondvalue) /\ (ge_balance_negative_values_secondvalue) = 0) \/ exists ge_signed_half_values_secondvaluedecode. (((y) = 2 * ge_signed_half_values_secondvaluedecode + 1 /\ (ge_balance_positive_values_secondvalue) = 0) /\ (ge_balance_negative_values_secondvalue) = S ge_signed_half_values_secondvaluedecode))) /\ ((dst_positive_values_second) + ge_balance_negative_values_secondvalue = (dst_negative_values_second) + ge_balance_positive_values_secondvalue))))))))) /\ (((exists dst_positive_code_values_product dst_positive_scale_values_product dst_negative_code_values_product dst_negative_scale_values_product dst_positive_values_product dst_negative_values_product. (((F) = (((((dst_positive_code_values_product) + (dst_positive_scale_values_product)) * S ((dst_positive_code_values_product) + (dst_positive_scale_values_product)) + ((dst_positive_scale_values_product) + (dst_positive_scale_values_product))) + (((dst_negative_code_values_product) + (dst_negative_scale_values_product)) * S ((dst_negative_code_values_product) + (dst_negative_scale_values_product)) + ((dst_negative_scale_values_product) + (dst_negative_scale_values_product)))) * S ((((dst_positive_code_values_product) + (dst_positive_scale_values_product)) * S ((dst_positive_code_values_product) + (dst_positive_scale_values_product)) + ((dst_positive_scale_values_product) + (dst_positive_scale_values_product))) + (((dst_negative_code_values_product) + (dst_negative_scale_values_product)) * S ((dst_negative_code_values_product) + (dst_negative_scale_values_product)) + ((dst_negative_scale_values_product) + (dst_negative_scale_values_product)))) + ((((dst_negative_code_values_product) + (dst_negative_scale_values_product)) * S ((dst_negative_code_values_product) + (dst_negative_scale_values_product)) + ((dst_negative_scale_values_product) + (dst_negative_scale_values_product))) + (((dst_negative_code_values_product) + (dst_negative_scale_values_product)) * S ((dst_negative_code_values_product) + (dst_negative_scale_values_product)) + ((dst_negative_scale_values_product) + (dst_negative_scale_values_product)))))) /\ (((((exists ff_h_pvs_values_productpositive. ff_h_pvs_values_productpositive + S (dst_positive_values_product) = S ((S (a*b)) * dst_positive_scale_values_product)) /\ exists ff_q_pvs_values_productpositive. dst_positive_code_values_product = ff_q_pvs_values_productpositive * S ((S (a*b)) * dst_positive_scale_values_product) + (dst_positive_values_product))) /\ (((((exists ff_h_pvs_values_productnegative. ff_h_pvs_values_productnegative + S (dst_negative_values_product) = S ((S (a*b)) * dst_negative_scale_values_product)) /\ exists ff_q_pvs_values_productnegative. dst_negative_code_values_product = ff_q_pvs_values_productnegative * S ((S (a*b)) * dst_negative_scale_values_product) + (dst_negative_values_product))) /\ (exists ge_balance_positive_values_productvalue ge_balance_negative_values_productvalue. (((((z) = 2 * (ge_balance_positive_values_productvalue) /\ (ge_balance_negative_values_productvalue) = 0) \/ exists ge_signed_half_values_productvaluedecode. (((z) = 2 * ge_signed_half_values_productvaluedecode + 1 /\ (ge_balance_positive_values_productvalue) = 0) /\ (ge_balance_negative_values_productvalue) = S ge_signed_half_values_productvaluedecode))) /\ ((dst_positive_values_product) + ge_balance_negative_values_productvalue = (dst_negative_values_product) + ge_balance_positive_values_productvalue))))))))) /\ (exists sto_ap_values_law sto_an_values_law sto_bp_values_law sto_bn_values_law sto_cp_values_law sto_cn_values_law. (((((x) = 2 * (sto_ap_values_law) /\ (sto_an_values_law) = 0) \/ exists ge_signed_half_values_lawleft. (((x) = 2 * ge_signed_half_values_lawleft + 1 /\ (sto_ap_values_law) = 0) /\ (sto_an_values_law) = S ge_signed_half_values_lawleft))) /\ ((((((y) = 2 * (sto_bp_values_law) /\ (sto_bn_values_law) = 0) \/ exists ge_signed_half_values_lawright. (((y) = 2 * ge_signed_half_values_lawright + 1 /\ (sto_bp_values_law) = 0) /\ (sto_bn_values_law) = S ge_signed_half_values_lawright))) /\ ((((((z) = 2 * (sto_cp_values_law) /\ (sto_cn_values_law) = 0) \/ exists ge_signed_half_values_lawoutput. (((z) = 2 * ge_signed_half_values_lawoutput + 1 /\ (sto_cp_values_law) = 0) /\ (sto_cn_values_law) = S ge_signed_half_values_lawoutput))) /\ ((sto_ap_values_law * sto_bp_values_law + sto_an_values_law * sto_bn_values_law) + sto_cn_values_law = (sto_ap_values_law * sto_bn_values_law + sto_an_values_law * sto_bp_values_law) + sto_cp_values_law))))))))))))