signed_multiplicative_at_one_value

Exact expanded first-order arithmetic statement

forall N F z. (((~((N)=0)) /\ (((exists dst_positive_code_unique_one_sourcetable dst_positive_scale_unique_one_sourcetable dst_negative_code_unique_one_sourcetable dst_negative_scale_unique_one_sourcetable. (((F) = (((((dst_positive_code_unique_one_sourcetable) + (dst_positive_scale_unique_one_sourcetable)) * S ((dst_positive_code_unique_one_sourcetable) + (dst_positive_scale_unique_one_sourcetable)) + ((dst_positive_scale_unique_one_sourcetable) + (dst_positive_scale_unique_one_sourcetable))) + (((dst_negative_code_unique_one_sourcetable) + (dst_negative_scale_unique_one_sourcetable)) * S ((dst_negative_code_unique_one_sourcetable) + (dst_negative_scale_unique_one_sourcetable)) + ((dst_negative_scale_unique_one_sourcetable) + (dst_negative_scale_unique_one_sourcetable)))) * S ((((dst_positive_code_unique_one_sourcetable) + (dst_positive_scale_unique_one_sourcetable)) * S ((dst_positive_code_unique_one_sourcetable) + (dst_positive_scale_unique_one_sourcetable)) + ((dst_positive_scale_unique_one_sourcetable) + (dst_positive_scale_unique_one_sourcetable))) + (((dst_negative_code_unique_one_sourcetable) + (dst_negative_scale_unique_one_sourcetable)) * S ((dst_negative_code_unique_one_sourcetable) + (dst_negative_scale_unique_one_sourcetable)) + ((dst_negative_scale_unique_one_sourcetable) + (dst_negative_scale_unique_one_sourcetable)))) + ((((dst_negative_code_unique_one_sourcetable) + (dst_negative_scale_unique_one_sourcetable)) * S ((dst_negative_code_unique_one_sourcetable) + (dst_negative_scale_unique_one_sourcetable)) + ((dst_negative_scale_unique_one_sourcetable) + (dst_negative_scale_unique_one_sourcetable))) + (((dst_negative_code_unique_one_sourcetable) + (dst_negative_scale_unique_one_sourcetable)) * S ((dst_negative_code_unique_one_sourcetable) + (dst_negative_scale_unique_one_sourcetable)) + ((dst_negative_scale_unique_one_sourcetable) + (dst_negative_scale_unique_one_sourcetable)))))) /\ (forall dst_index_unique_one_sourcetable. (exists pvs_le_gap_unique_one_sourcetabledomain. pvs_le_gap_unique_one_sourcetabledomain + (dst_index_unique_one_sourcetable) = (N)) -> exists dst_positive_unique_one_sourcetable dst_negative_unique_one_sourcetable dst_value_unique_one_sourcetable. ((((exists ff_h_pvs_unique_one_sourcetableentrypositive. ff_h_pvs_unique_one_sourcetableentrypositive + S (dst_positive_unique_one_sourcetable) = S ((S (dst_index_unique_one_sourcetable)) * dst_positive_scale_unique_one_sourcetable)) /\ exists ff_q_pvs_unique_one_sourcetableentrypositive. dst_positive_code_unique_one_sourcetable = ff_q_pvs_unique_one_sourcetableentrypositive * S ((S (dst_index_unique_one_sourcetable)) * dst_positive_scale_unique_one_sourcetable) + (dst_positive_unique_one_sourcetable))) /\ (((((exists ff_h_pvs_unique_one_sourcetableentrynegative. ff_h_pvs_unique_one_sourcetableentrynegative + S (dst_negative_unique_one_sourcetable) = S ((S (dst_index_unique_one_sourcetable)) * dst_negative_scale_unique_one_sourcetable)) /\ exists ff_q_pvs_unique_one_sourcetableentrynegative. dst_negative_code_unique_one_sourcetable = ff_q_pvs_unique_one_sourcetableentrynegative * S ((S (dst_index_unique_one_sourcetable)) * dst_negative_scale_unique_one_sourcetable) + (dst_negative_unique_one_sourcetable))) /\ (exists ge_balance_positive_unique_one_sourcetableentryvalue ge_balance_negative_unique_one_sourcetableentryvalue. (((((dst_value_unique_one_sourcetable) = 2 * (ge_balance_positive_unique_one_sourcetableentryvalue) /\ (ge_balance_negative_unique_one_sourcetableentryvalue) = 0) \/ exists ge_signed_half_unique_one_sourcetableentryvaluedecode. (((dst_value_unique_one_sourcetable) = 2 * ge_signed_half_unique_one_sourcetableentryvaluedecode + 1 /\ (ge_balance_positive_unique_one_sourcetableentryvalue) = 0) /\ (ge_balance_negative_unique_one_sourcetableentryvalue) = S ge_signed_half_unique_one_sourcetableentryvaluedecode))) /\ ((dst_positive_unique_one_sourcetable) + ge_balance_negative_unique_one_sourcetableentryvalue = (dst_negative_unique_one_sourcetable) + ge_balance_positive_unique_one_sourcetableentryvalue))))))))) /\ (((exists dst_positive_code_unique_one_sourceone dst_positive_scale_unique_one_sourceone dst_negative_code_unique_one_sourceone dst_negative_scale_unique_one_sourceone dst_positive_unique_one_sourceone dst_negative_unique_one_sourceone. (((F) = (((((dst_positive_code_unique_one_sourceone) + (dst_positive_scale_unique_one_sourceone)) * S ((dst_positive_code_unique_one_sourceone) + (dst_positive_scale_unique_one_sourceone)) + ((dst_positive_scale_unique_one_sourceone) + (dst_positive_scale_unique_one_sourceone))) + (((dst_negative_code_unique_one_sourceone) + (dst_negative_scale_unique_one_sourceone)) * S ((dst_negative_code_unique_one_sourceone) + (dst_negative_scale_unique_one_sourceone)) + ((dst_negative_scale_unique_one_sourceone) + (dst_negative_scale_unique_one_sourceone)))) * S ((((dst_positive_code_unique_one_sourceone) + (dst_positive_scale_unique_one_sourceone)) * S ((dst_positive_code_unique_one_sourceone) + (dst_positive_scale_unique_one_sourceone)) + ((dst_positive_scale_unique_one_sourceone) + (dst_positive_scale_unique_one_sourceone))) + (((dst_negative_code_unique_one_sourceone) + (dst_negative_scale_unique_one_sourceone)) * S ((dst_negative_code_unique_one_sourceone) + (dst_negative_scale_unique_one_sourceone)) + ((dst_negative_scale_unique_one_sourceone) + (dst_negative_scale_unique_one_sourceone)))) + ((((dst_negative_code_unique_one_sourceone) + (dst_negative_scale_unique_one_sourceone)) * S ((dst_negative_code_unique_one_sourceone) + (dst_negative_scale_unique_one_sourceone)) + ((dst_negative_scale_unique_one_sourceone) + (dst_negative_scale_unique_one_sourceone))) + (((dst_negative_code_unique_one_sourceone) + (dst_negative_scale_unique_one_sourceone)) * S ((dst_negative_code_unique_one_sourceone) + (dst_negative_scale_unique_one_sourceone)) + ((dst_negative_scale_unique_one_sourceone) + (dst_negative_scale_unique_one_sourceone)))))) /\ (((((exists ff_h_pvs_unique_one_sourceonepositive. ff_h_pvs_unique_one_sourceonepositive + S (dst_positive_unique_one_sourceone) = S ((S (1)) * dst_positive_scale_unique_one_sourceone)) /\ exists ff_q_pvs_unique_one_sourceonepositive. dst_positive_code_unique_one_sourceone = ff_q_pvs_unique_one_sourceonepositive * S ((S (1)) * dst_positive_scale_unique_one_sourceone) + (dst_positive_unique_one_sourceone))) /\ (((((exists ff_h_pvs_unique_one_sourceonenegative. ff_h_pvs_unique_one_sourceonenegative + S (dst_negative_unique_one_sourceone) = S ((S (1)) * dst_negative_scale_unique_one_sourceone)) /\ exists ff_q_pvs_unique_one_sourceonenegative. dst_negative_code_unique_one_sourceone = ff_q_pvs_unique_one_sourceonenegative * S ((S (1)) * dst_negative_scale_unique_one_sourceone) + (dst_negative_unique_one_sourceone))) /\ (exists ge_balance_positive_unique_one_sourceonevalue ge_balance_negative_unique_one_sourceonevalue. (((((2) = 2 * (ge_balance_positive_unique_one_sourceonevalue) /\ (ge_balance_negative_unique_one_sourceonevalue) = 0) \/ exists ge_signed_half_unique_one_sourceonevaluedecode. (((2) = 2 * ge_signed_half_unique_one_sourceonevaluedecode + 1 /\ (ge_balance_positive_unique_one_sourceonevalue) = 0) /\ (ge_balance_negative_unique_one_sourceonevalue) = S ge_signed_half_unique_one_sourceonevaluedecode))) /\ ((dst_positive_unique_one_sourceone) + ge_balance_negative_unique_one_sourceonevalue = (dst_negative_unique_one_sourceone) + ge_balance_positive_unique_one_sourceonevalue))))))))) /\ (forall mp_a_unique_one_source mp_b_unique_one_source mp_x_unique_one_source mp_y_unique_one_source mp_z_unique_one_source. ~(mp_a_unique_one_source=0) -> ~(mp_b_unique_one_source=0) -> (exists pvs_le_gap_unique_one_sourcebound. pvs_le_gap_unique_one_sourcebound + (mp_a_unique_one_source*mp_b_unique_one_source) = (N)) -> (forall frp_divisor_unique_one_sourcecoprime. (exists frp_left_factor_unique_one_sourcecoprime. mp_a_unique_one_source = frp_divisor_unique_one_sourcecoprime * frp_left_factor_unique_one_sourcecoprime) -> (exists frp_right_factor_unique_one_sourcecoprime. mp_b_unique_one_source = frp_divisor_unique_one_sourcecoprime * frp_right_factor_unique_one_sourcecoprime) -> frp_divisor_unique_one_sourcecoprime = 1) -> (exists dst_positive_code_unique_one_sourcefirst dst_positive_scale_unique_one_sourcefirst dst_negative_code_unique_one_sourcefirst dst_negative_scale_unique_one_sourcefirst dst_positive_unique_one_sourcefirst dst_negative_unique_one_sourcefirst. (((F) = (((((dst_positive_code_unique_one_sourcefirst) + (dst_positive_scale_unique_one_sourcefirst)) * S ((dst_positive_code_unique_one_sourcefirst) + (dst_positive_scale_unique_one_sourcefirst)) + ((dst_positive_scale_unique_one_sourcefirst) + (dst_positive_scale_unique_one_sourcefirst))) + (((dst_negative_code_unique_one_sourcefirst) + (dst_negative_scale_unique_one_sourcefirst)) * S ((dst_negative_code_unique_one_sourcefirst) + (dst_negative_scale_unique_one_sourcefirst)) + ((dst_negative_scale_unique_one_sourcefirst) + (dst_negative_scale_unique_one_sourcefirst)))) * S ((((dst_positive_code_unique_one_sourcefirst) + (dst_positive_scale_unique_one_sourcefirst)) * S ((dst_positive_code_unique_one_sourcefirst) + (dst_positive_scale_unique_one_sourcefirst)) + ((dst_positive_scale_unique_one_sourcefirst) + (dst_positive_scale_unique_one_sourcefirst))) + (((dst_negative_code_unique_one_sourcefirst) + (dst_negative_scale_unique_one_sourcefirst)) * S ((dst_negative_code_unique_one_sourcefirst) + (dst_negative_scale_unique_one_sourcefirst)) + ((dst_negative_scale_unique_one_sourcefirst) + (dst_negative_scale_unique_one_sourcefirst)))) + ((((dst_negative_code_unique_one_sourcefirst) + (dst_negative_scale_unique_one_sourcefirst)) * S ((dst_negative_code_unique_one_sourcefirst) + (dst_negative_scale_unique_one_sourcefirst)) + ((dst_negative_scale_unique_one_sourcefirst) + (dst_negative_scale_unique_one_sourcefirst))) + (((dst_negative_code_unique_one_sourcefirst) + (dst_negative_scale_unique_one_sourcefirst)) * S ((dst_negative_code_unique_one_sourcefirst) + (dst_negative_scale_unique_one_sourcefirst)) + ((dst_negative_scale_unique_one_sourcefirst) + (dst_negative_scale_unique_one_sourcefirst)))))) /\ (((((exists ff_h_pvs_unique_one_sourcefirstpositive. ff_h_pvs_unique_one_sourcefirstpositive + S (dst_positive_unique_one_sourcefirst) = S ((S (mp_a_unique_one_source)) * dst_positive_scale_unique_one_sourcefirst)) /\ exists ff_q_pvs_unique_one_sourcefirstpositive. dst_positive_code_unique_one_sourcefirst = ff_q_pvs_unique_one_sourcefirstpositive * S ((S (mp_a_unique_one_source)) * dst_positive_scale_unique_one_sourcefirst) + (dst_positive_unique_one_sourcefirst))) /\ (((((exists ff_h_pvs_unique_one_sourcefirstnegative. ff_h_pvs_unique_one_sourcefirstnegative + S (dst_negative_unique_one_sourcefirst) = S ((S (mp_a_unique_one_source)) * dst_negative_scale_unique_one_sourcefirst)) /\ exists ff_q_pvs_unique_one_sourcefirstnegative. dst_negative_code_unique_one_sourcefirst = ff_q_pvs_unique_one_sourcefirstnegative * S ((S (mp_a_unique_one_source)) * dst_negative_scale_unique_one_sourcefirst) + (dst_negative_unique_one_sourcefirst))) /\ (exists ge_balance_positive_unique_one_sourcefirstvalue ge_balance_negative_unique_one_sourcefirstvalue. (((((mp_x_unique_one_source) = 2 * (ge_balance_positive_unique_one_sourcefirstvalue) /\ (ge_balance_negative_unique_one_sourcefirstvalue) = 0) \/ exists ge_signed_half_unique_one_sourcefirstvaluedecode. (((mp_x_unique_one_source) = 2 * ge_signed_half_unique_one_sourcefirstvaluedecode + 1 /\ (ge_balance_positive_unique_one_sourcefirstvalue) = 0) /\ (ge_balance_negative_unique_one_sourcefirstvalue) = S ge_signed_half_unique_one_sourcefirstvaluedecode))) /\ ((dst_positive_unique_one_sourcefirst) + ge_balance_negative_unique_one_sourcefirstvalue = (dst_negative_unique_one_sourcefirst) + ge_balance_positive_unique_one_sourcefirstvalue))))))))) -> (exists dst_positive_code_unique_one_sourcesecond dst_positive_scale_unique_one_sourcesecond dst_negative_code_unique_one_sourcesecond dst_negative_scale_unique_one_sourcesecond dst_positive_unique_one_sourcesecond dst_negative_unique_one_sourcesecond. (((F) = (((((dst_positive_code_unique_one_sourcesecond) + (dst_positive_scale_unique_one_sourcesecond)) * S ((dst_positive_code_unique_one_sourcesecond) + (dst_positive_scale_unique_one_sourcesecond)) + ((dst_positive_scale_unique_one_sourcesecond) + (dst_positive_scale_unique_one_sourcesecond))) + (((dst_negative_code_unique_one_sourcesecond) + (dst_negative_scale_unique_one_sourcesecond)) * S ((dst_negative_code_unique_one_sourcesecond) + (dst_negative_scale_unique_one_sourcesecond)) + ((dst_negative_scale_unique_one_sourcesecond) + (dst_negative_scale_unique_one_sourcesecond)))) * S ((((dst_positive_code_unique_one_sourcesecond) + (dst_positive_scale_unique_one_sourcesecond)) * S ((dst_positive_code_unique_one_sourcesecond) + (dst_positive_scale_unique_one_sourcesecond)) + ((dst_positive_scale_unique_one_sourcesecond) + (dst_positive_scale_unique_one_sourcesecond))) + (((dst_negative_code_unique_one_sourcesecond) + (dst_negative_scale_unique_one_sourcesecond)) * S ((dst_negative_code_unique_one_sourcesecond) + (dst_negative_scale_unique_one_sourcesecond)) + ((dst_negative_scale_unique_one_sourcesecond) + (dst_negative_scale_unique_one_sourcesecond)))) + ((((dst_negative_code_unique_one_sourcesecond) + (dst_negative_scale_unique_one_sourcesecond)) * S ((dst_negative_code_unique_one_sourcesecond) + (dst_negative_scale_unique_one_sourcesecond)) + ((dst_negative_scale_unique_one_sourcesecond) + (dst_negative_scale_unique_one_sourcesecond))) + (((dst_negative_code_unique_one_sourcesecond) + (dst_negative_scale_unique_one_sourcesecond)) * S ((dst_negative_code_unique_one_sourcesecond) + (dst_negative_scale_unique_one_sourcesecond)) + ((dst_negative_scale_unique_one_sourcesecond) + (dst_negative_scale_unique_one_sourcesecond)))))) /\ (((((exists ff_h_pvs_unique_one_sourcesecondpositive. ff_h_pvs_unique_one_sourcesecondpositive + S (dst_positive_unique_one_sourcesecond) = S ((S (mp_b_unique_one_source)) * dst_positive_scale_unique_one_sourcesecond)) /\ exists ff_q_pvs_unique_one_sourcesecondpositive. dst_positive_code_unique_one_sourcesecond = ff_q_pvs_unique_one_sourcesecondpositive * S ((S (mp_b_unique_one_source)) * dst_positive_scale_unique_one_sourcesecond) + (dst_positive_unique_one_sourcesecond))) /\ (((((exists ff_h_pvs_unique_one_sourcesecondnegative. ff_h_pvs_unique_one_sourcesecondnegative + S (dst_negative_unique_one_sourcesecond) = S ((S (mp_b_unique_one_source)) * dst_negative_scale_unique_one_sourcesecond)) /\ exists ff_q_pvs_unique_one_sourcesecondnegative. dst_negative_code_unique_one_sourcesecond = ff_q_pvs_unique_one_sourcesecondnegative * S ((S (mp_b_unique_one_source)) * dst_negative_scale_unique_one_sourcesecond) + (dst_negative_unique_one_sourcesecond))) /\ (exists ge_balance_positive_unique_one_sourcesecondvalue ge_balance_negative_unique_one_sourcesecondvalue. (((((mp_y_unique_one_source) = 2 * (ge_balance_positive_unique_one_sourcesecondvalue) /\ (ge_balance_negative_unique_one_sourcesecondvalue) = 0) \/ exists ge_signed_half_unique_one_sourcesecondvaluedecode. (((mp_y_unique_one_source) = 2 * ge_signed_half_unique_one_sourcesecondvaluedecode + 1 /\ (ge_balance_positive_unique_one_sourcesecondvalue) = 0) /\ (ge_balance_negative_unique_one_sourcesecondvalue) = S ge_signed_half_unique_one_sourcesecondvaluedecode))) /\ ((dst_positive_unique_one_sourcesecond) + ge_balance_negative_unique_one_sourcesecondvalue = (dst_negative_unique_one_sourcesecond) + ge_balance_positive_unique_one_sourcesecondvalue))))))))) -> (exists dst_positive_code_unique_one_sourceproduct dst_positive_scale_unique_one_sourceproduct dst_negative_code_unique_one_sourceproduct dst_negative_scale_unique_one_sourceproduct dst_positive_unique_one_sourceproduct dst_negative_unique_one_sourceproduct. (((F) = (((((dst_positive_code_unique_one_sourceproduct) + (dst_positive_scale_unique_one_sourceproduct)) * S ((dst_positive_code_unique_one_sourceproduct) + (dst_positive_scale_unique_one_sourceproduct)) + ((dst_positive_scale_unique_one_sourceproduct) + (dst_positive_scale_unique_one_sourceproduct))) + (((dst_negative_code_unique_one_sourceproduct) + (dst_negative_scale_unique_one_sourceproduct)) * S ((dst_negative_code_unique_one_sourceproduct) + (dst_negative_scale_unique_one_sourceproduct)) + ((dst_negative_scale_unique_one_sourceproduct) + (dst_negative_scale_unique_one_sourceproduct)))) * S ((((dst_positive_code_unique_one_sourceproduct) + (dst_positive_scale_unique_one_sourceproduct)) * S ((dst_positive_code_unique_one_sourceproduct) + (dst_positive_scale_unique_one_sourceproduct)) + ((dst_positive_scale_unique_one_sourceproduct) + (dst_positive_scale_unique_one_sourceproduct))) + (((dst_negative_code_unique_one_sourceproduct) + (dst_negative_scale_unique_one_sourceproduct)) * S ((dst_negative_code_unique_one_sourceproduct) + (dst_negative_scale_unique_one_sourceproduct)) + ((dst_negative_scale_unique_one_sourceproduct) + (dst_negative_scale_unique_one_sourceproduct)))) + ((((dst_negative_code_unique_one_sourceproduct) + (dst_negative_scale_unique_one_sourceproduct)) * S ((dst_negative_code_unique_one_sourceproduct) + (dst_negative_scale_unique_one_sourceproduct)) + ((dst_negative_scale_unique_one_sourceproduct) + (dst_negative_scale_unique_one_sourceproduct))) + (((dst_negative_code_unique_one_sourceproduct) + (dst_negative_scale_unique_one_sourceproduct)) * S ((dst_negative_code_unique_one_sourceproduct) + (dst_negative_scale_unique_one_sourceproduct)) + ((dst_negative_scale_unique_one_sourceproduct) + (dst_negative_scale_unique_one_sourceproduct)))))) /\ (((((exists ff_h_pvs_unique_one_sourceproductpositive. ff_h_pvs_unique_one_sourceproductpositive + S (dst_positive_unique_one_sourceproduct) = S ((S (mp_a_unique_one_source*mp_b_unique_one_source)) * dst_positive_scale_unique_one_sourceproduct)) /\ exists ff_q_pvs_unique_one_sourceproductpositive. dst_positive_code_unique_one_sourceproduct = ff_q_pvs_unique_one_sourceproductpositive * S ((S (mp_a_unique_one_source*mp_b_unique_one_source)) * dst_positive_scale_unique_one_sourceproduct) + (dst_positive_unique_one_sourceproduct))) /\ (((((exists ff_h_pvs_unique_one_sourceproductnegative. ff_h_pvs_unique_one_sourceproductnegative + S (dst_negative_unique_one_sourceproduct) = S ((S (mp_a_unique_one_source*mp_b_unique_one_source)) * dst_negative_scale_unique_one_sourceproduct)) /\ exists ff_q_pvs_unique_one_sourceproductnegative. dst_negative_code_unique_one_sourceproduct = ff_q_pvs_unique_one_sourceproductnegative * S ((S (mp_a_unique_one_source*mp_b_unique_one_source)) * dst_negative_scale_unique_one_sourceproduct) + (dst_negative_unique_one_sourceproduct))) /\ (exists ge_balance_positive_unique_one_sourceproductvalue ge_balance_negative_unique_one_sourceproductvalue. (((((mp_z_unique_one_source) = 2 * (ge_balance_positive_unique_one_sourceproductvalue) /\ (ge_balance_negative_unique_one_sourceproductvalue) = 0) \/ exists ge_signed_half_unique_one_sourceproductvaluedecode. (((mp_z_unique_one_source) = 2 * ge_signed_half_unique_one_sourceproductvaluedecode + 1 /\ (ge_balance_positive_unique_one_sourceproductvalue) = 0) /\ (ge_balance_negative_unique_one_sourceproductvalue) = S ge_signed_half_unique_one_sourceproductvaluedecode))) /\ ((dst_positive_unique_one_sourceproduct) + ge_balance_negative_unique_one_sourceproductvalue = (dst_negative_unique_one_sourceproduct) + ge_balance_positive_unique_one_sourceproductvalue))))))))) -> (exists sto_ap_unique_one_sourcelaw sto_an_unique_one_sourcelaw sto_bp_unique_one_sourcelaw sto_bn_unique_one_sourcelaw sto_cp_unique_one_sourcelaw sto_cn_unique_one_sourcelaw. (((((mp_x_unique_one_source) = 2 * (sto_ap_unique_one_sourcelaw) /\ (sto_an_unique_one_sourcelaw) = 0) \/ exists ge_signed_half_unique_one_sourcelawleft. (((mp_x_unique_one_source) = 2 * ge_signed_half_unique_one_sourcelawleft + 1 /\ (sto_ap_unique_one_sourcelaw) = 0) /\ (sto_an_unique_one_sourcelaw) = S ge_signed_half_unique_one_sourcelawleft))) /\ ((((((mp_y_unique_one_source) = 2 * (sto_bp_unique_one_sourcelaw) /\ (sto_bn_unique_one_sourcelaw) = 0) \/ exists ge_signed_half_unique_one_sourcelawright. (((mp_y_unique_one_source) = 2 * ge_signed_half_unique_one_sourcelawright + 1 /\ (sto_bp_unique_one_sourcelaw) = 0) /\ (sto_bn_unique_one_sourcelaw) = S ge_signed_half_unique_one_sourcelawright))) /\ ((((((mp_z_unique_one_source) = 2 * (sto_cp_unique_one_sourcelaw) /\ (sto_cn_unique_one_sourcelaw) = 0) \/ exists ge_signed_half_unique_one_sourcelawoutput. (((mp_z_unique_one_source) = 2 * ge_signed_half_unique_one_sourcelawoutput + 1 /\ (sto_cp_unique_one_sourcelaw) = 0) /\ (sto_cn_unique_one_sourcelaw) = S ge_signed_half_unique_one_sourcelawoutput))) /\ ((sto_ap_unique_one_sourcelaw * sto_bp_unique_one_sourcelaw + sto_an_unique_one_sourcelaw * sto_bn_unique_one_sourcelaw) + sto_cn_unique_one_sourcelaw = (sto_ap_unique_one_sourcelaw * sto_bn_unique_one_sourcelaw + sto_an_unique_one_sourcelaw * sto_bp_unique_one_sourcelaw) + sto_cp_unique_one_sourcelaw)))))))))))))) -> (exists dst_positive_code_unique_one_input dst_positive_scale_unique_one_input dst_negative_code_unique_one_input dst_negative_scale_unique_one_input dst_positive_unique_one_input dst_negative_unique_one_input. (((F) = (((((dst_positive_code_unique_one_input) + (dst_positive_scale_unique_one_input)) * S ((dst_positive_code_unique_one_input) + (dst_positive_scale_unique_one_input)) + ((dst_positive_scale_unique_one_input) + (dst_positive_scale_unique_one_input))) + (((dst_negative_code_unique_one_input) + (dst_negative_scale_unique_one_input)) * S ((dst_negative_code_unique_one_input) + (dst_negative_scale_unique_one_input)) + ((dst_negative_scale_unique_one_input) + (dst_negative_scale_unique_one_input)))) * S ((((dst_positive_code_unique_one_input) + (dst_positive_scale_unique_one_input)) * S ((dst_positive_code_unique_one_input) + (dst_positive_scale_unique_one_input)) + ((dst_positive_scale_unique_one_input) + (dst_positive_scale_unique_one_input))) + (((dst_negative_code_unique_one_input) + (dst_negative_scale_unique_one_input)) * S ((dst_negative_code_unique_one_input) + (dst_negative_scale_unique_one_input)) + ((dst_negative_scale_unique_one_input) + (dst_negative_scale_unique_one_input)))) + ((((dst_negative_code_unique_one_input) + (dst_negative_scale_unique_one_input)) * S ((dst_negative_code_unique_one_input) + (dst_negative_scale_unique_one_input)) + ((dst_negative_scale_unique_one_input) + (dst_negative_scale_unique_one_input))) + (((dst_negative_code_unique_one_input) + (dst_negative_scale_unique_one_input)) * S ((dst_negative_code_unique_one_input) + (dst_negative_scale_unique_one_input)) + ((dst_negative_scale_unique_one_input) + (dst_negative_scale_unique_one_input)))))) /\ (((((exists ff_h_pvs_unique_one_inputpositive. ff_h_pvs_unique_one_inputpositive + S (dst_positive_unique_one_input) = S ((S (1)) * dst_positive_scale_unique_one_input)) /\ exists ff_q_pvs_unique_one_inputpositive. dst_positive_code_unique_one_input = ff_q_pvs_unique_one_inputpositive * S ((S (1)) * dst_positive_scale_unique_one_input) + (dst_positive_unique_one_input))) /\ (((((exists ff_h_pvs_unique_one_inputnegative. ff_h_pvs_unique_one_inputnegative + S (dst_negative_unique_one_input) = S ((S (1)) * dst_negative_scale_unique_one_input)) /\ exists ff_q_pvs_unique_one_inputnegative. dst_negative_code_unique_one_input = ff_q_pvs_unique_one_inputnegative * S ((S (1)) * dst_negative_scale_unique_one_input) + (dst_negative_unique_one_input))) /\ (exists ge_balance_positive_unique_one_inputvalue ge_balance_negative_unique_one_inputvalue. (((((z) = 2 * (ge_balance_positive_unique_one_inputvalue) /\ (ge_balance_negative_unique_one_inputvalue) = 0) \/ exists ge_signed_half_unique_one_inputvaluedecode. (((z) = 2 * ge_signed_half_unique_one_inputvaluedecode + 1 /\ (ge_balance_positive_unique_one_inputvalue) = 0) /\ (ge_balance_negative_unique_one_inputvalue) = S ge_signed_half_unique_one_inputvaluedecode))) /\ ((dst_positive_unique_one_input) + ge_balance_negative_unique_one_inputvalue = (dst_negative_unique_one_input) + ge_balance_positive_unique_one_inputvalue))))))))) -> z=2