signed_multiplicative_normalized

Exact expanded first-order arithmetic statement

forall N F. (((~((N)=0)) /\ (((exists dst_positive_code_signed_multiplicative_normalizedtable dst_positive_scale_signed_multiplicative_normalizedtable dst_negative_code_signed_multiplicative_normalizedtable dst_negative_scale_signed_multiplicative_normalizedtable. (((F) = (((((dst_positive_code_signed_multiplicative_normalizedtable) + (dst_positive_scale_signed_multiplicative_normalizedtable)) * S ((dst_positive_code_signed_multiplicative_normalizedtable) + (dst_positive_scale_signed_multiplicative_normalizedtable)) + ((dst_positive_scale_signed_multiplicative_normalizedtable) + (dst_positive_scale_signed_multiplicative_normalizedtable))) + (((dst_negative_code_signed_multiplicative_normalizedtable) + (dst_negative_scale_signed_multiplicative_normalizedtable)) * S ((dst_negative_code_signed_multiplicative_normalizedtable) + (dst_negative_scale_signed_multiplicative_normalizedtable)) + ((dst_negative_scale_signed_multiplicative_normalizedtable) + (dst_negative_scale_signed_multiplicative_normalizedtable)))) * S ((((dst_positive_code_signed_multiplicative_normalizedtable) + (dst_positive_scale_signed_multiplicative_normalizedtable)) * S ((dst_positive_code_signed_multiplicative_normalizedtable) + (dst_positive_scale_signed_multiplicative_normalizedtable)) + ((dst_positive_scale_signed_multiplicative_normalizedtable) + (dst_positive_scale_signed_multiplicative_normalizedtable))) + (((dst_negative_code_signed_multiplicative_normalizedtable) + (dst_negative_scale_signed_multiplicative_normalizedtable)) * S ((dst_negative_code_signed_multiplicative_normalizedtable) + (dst_negative_scale_signed_multiplicative_normalizedtable)) + ((dst_negative_scale_signed_multiplicative_normalizedtable) + (dst_negative_scale_signed_multiplicative_normalizedtable)))) + ((((dst_negative_code_signed_multiplicative_normalizedtable) + (dst_negative_scale_signed_multiplicative_normalizedtable)) * S ((dst_negative_code_signed_multiplicative_normalizedtable) + (dst_negative_scale_signed_multiplicative_normalizedtable)) + ((dst_negative_scale_signed_multiplicative_normalizedtable) + (dst_negative_scale_signed_multiplicative_normalizedtable))) + (((dst_negative_code_signed_multiplicative_normalizedtable) + (dst_negative_scale_signed_multiplicative_normalizedtable)) * S ((dst_negative_code_signed_multiplicative_normalizedtable) + (dst_negative_scale_signed_multiplicative_normalizedtable)) + ((dst_negative_scale_signed_multiplicative_normalizedtable) + (dst_negative_scale_signed_multiplicative_normalizedtable)))))) /\ (forall dst_index_signed_multiplicative_normalizedtable. (exists pvs_le_gap_signed_multiplicative_normalizedtabledomain. pvs_le_gap_signed_multiplicative_normalizedtabledomain + (dst_index_signed_multiplicative_normalizedtable) = (N)) -> exists dst_positive_signed_multiplicative_normalizedtable dst_negative_signed_multiplicative_normalizedtable dst_value_signed_multiplicative_normalizedtable. ((((exists ff_h_pvs_signed_multiplicative_normalizedtableentrypositive. ff_h_pvs_signed_multiplicative_normalizedtableentrypositive + S (dst_positive_signed_multiplicative_normalizedtable) = S ((S (dst_index_signed_multiplicative_normalizedtable)) * dst_positive_scale_signed_multiplicative_normalizedtable)) /\ exists ff_q_pvs_signed_multiplicative_normalizedtableentrypositive. dst_positive_code_signed_multiplicative_normalizedtable = ff_q_pvs_signed_multiplicative_normalizedtableentrypositive * S ((S (dst_index_signed_multiplicative_normalizedtable)) * dst_positive_scale_signed_multiplicative_normalizedtable) + (dst_positive_signed_multiplicative_normalizedtable))) /\ (((((exists ff_h_pvs_signed_multiplicative_normalizedtableentrynegative. ff_h_pvs_signed_multiplicative_normalizedtableentrynegative + S (dst_negative_signed_multiplicative_normalizedtable) = S ((S (dst_index_signed_multiplicative_normalizedtable)) * dst_negative_scale_signed_multiplicative_normalizedtable)) /\ exists ff_q_pvs_signed_multiplicative_normalizedtableentrynegative. dst_negative_code_signed_multiplicative_normalizedtable = ff_q_pvs_signed_multiplicative_normalizedtableentrynegative * S ((S (dst_index_signed_multiplicative_normalizedtable)) * dst_negative_scale_signed_multiplicative_normalizedtable) + (dst_negative_signed_multiplicative_normalizedtable))) /\ (exists ge_balance_positive_signed_multiplicative_normalizedtableentryvalue ge_balance_negative_signed_multiplicative_normalizedtableentryvalue. (((((dst_value_signed_multiplicative_normalizedtable) = 2 * (ge_balance_positive_signed_multiplicative_normalizedtableentryvalue) /\ (ge_balance_negative_signed_multiplicative_normalizedtableentryvalue) = 0) \/ exists ge_signed_half_signed_multiplicative_normalizedtableentryvaluedecode. (((dst_value_signed_multiplicative_normalizedtable) = 2 * ge_signed_half_signed_multiplicative_normalizedtableentryvaluedecode + 1 /\ (ge_balance_positive_signed_multiplicative_normalizedtableentryvalue) = 0) /\ (ge_balance_negative_signed_multiplicative_normalizedtableentryvalue) = S ge_signed_half_signed_multiplicative_normalizedtableentryvaluedecode))) /\ ((dst_positive_signed_multiplicative_normalizedtable) + ge_balance_negative_signed_multiplicative_normalizedtableentryvalue = (dst_negative_signed_multiplicative_normalizedtable) + ge_balance_positive_signed_multiplicative_normalizedtableentryvalue))))))))) /\ (((exists dst_positive_code_signed_multiplicative_normalizedone dst_positive_scale_signed_multiplicative_normalizedone dst_negative_code_signed_multiplicative_normalizedone dst_negative_scale_signed_multiplicative_normalizedone dst_positive_signed_multiplicative_normalizedone dst_negative_signed_multiplicative_normalizedone. (((F) = (((((dst_positive_code_signed_multiplicative_normalizedone) + (dst_positive_scale_signed_multiplicative_normalizedone)) * S ((dst_positive_code_signed_multiplicative_normalizedone) + (dst_positive_scale_signed_multiplicative_normalizedone)) + ((dst_positive_scale_signed_multiplicative_normalizedone) + (dst_positive_scale_signed_multiplicative_normalizedone))) + (((dst_negative_code_signed_multiplicative_normalizedone) + (dst_negative_scale_signed_multiplicative_normalizedone)) * S ((dst_negative_code_signed_multiplicative_normalizedone) + (dst_negative_scale_signed_multiplicative_normalizedone)) + ((dst_negative_scale_signed_multiplicative_normalizedone) + (dst_negative_scale_signed_multiplicative_normalizedone)))) * S ((((dst_positive_code_signed_multiplicative_normalizedone) + (dst_positive_scale_signed_multiplicative_normalizedone)) * S ((dst_positive_code_signed_multiplicative_normalizedone) + (dst_positive_scale_signed_multiplicative_normalizedone)) + ((dst_positive_scale_signed_multiplicative_normalizedone) + (dst_positive_scale_signed_multiplicative_normalizedone))) + (((dst_negative_code_signed_multiplicative_normalizedone) + (dst_negative_scale_signed_multiplicative_normalizedone)) * S ((dst_negative_code_signed_multiplicative_normalizedone) + (dst_negative_scale_signed_multiplicative_normalizedone)) + ((dst_negative_scale_signed_multiplicative_normalizedone) + (dst_negative_scale_signed_multiplicative_normalizedone)))) + ((((dst_negative_code_signed_multiplicative_normalizedone) + (dst_negative_scale_signed_multiplicative_normalizedone)) * S ((dst_negative_code_signed_multiplicative_normalizedone) + (dst_negative_scale_signed_multiplicative_normalizedone)) + ((dst_negative_scale_signed_multiplicative_normalizedone) + (dst_negative_scale_signed_multiplicative_normalizedone))) + (((dst_negative_code_signed_multiplicative_normalizedone) + (dst_negative_scale_signed_multiplicative_normalizedone)) * S ((dst_negative_code_signed_multiplicative_normalizedone) + (dst_negative_scale_signed_multiplicative_normalizedone)) + ((dst_negative_scale_signed_multiplicative_normalizedone) + (dst_negative_scale_signed_multiplicative_normalizedone)))))) /\ (((((exists ff_h_pvs_signed_multiplicative_normalizedonepositive. ff_h_pvs_signed_multiplicative_normalizedonepositive + S (dst_positive_signed_multiplicative_normalizedone) = S ((S (1)) * dst_positive_scale_signed_multiplicative_normalizedone)) /\ exists ff_q_pvs_signed_multiplicative_normalizedonepositive. dst_positive_code_signed_multiplicative_normalizedone = ff_q_pvs_signed_multiplicative_normalizedonepositive * S ((S (1)) * dst_positive_scale_signed_multiplicative_normalizedone) + (dst_positive_signed_multiplicative_normalizedone))) /\ (((((exists ff_h_pvs_signed_multiplicative_normalizedonenegative. ff_h_pvs_signed_multiplicative_normalizedonenegative + S (dst_negative_signed_multiplicative_normalizedone) = S ((S (1)) * dst_negative_scale_signed_multiplicative_normalizedone)) /\ exists ff_q_pvs_signed_multiplicative_normalizedonenegative. dst_negative_code_signed_multiplicative_normalizedone = ff_q_pvs_signed_multiplicative_normalizedonenegative * S ((S (1)) * dst_negative_scale_signed_multiplicative_normalizedone) + (dst_negative_signed_multiplicative_normalizedone))) /\ (exists ge_balance_positive_signed_multiplicative_normalizedonevalue ge_balance_negative_signed_multiplicative_normalizedonevalue. (((((2) = 2 * (ge_balance_positive_signed_multiplicative_normalizedonevalue) /\ (ge_balance_negative_signed_multiplicative_normalizedonevalue) = 0) \/ exists ge_signed_half_signed_multiplicative_normalizedonevaluedecode. (((2) = 2 * ge_signed_half_signed_multiplicative_normalizedonevaluedecode + 1 /\ (ge_balance_positive_signed_multiplicative_normalizedonevalue) = 0) /\ (ge_balance_negative_signed_multiplicative_normalizedonevalue) = S ge_signed_half_signed_multiplicative_normalizedonevaluedecode))) /\ ((dst_positive_signed_multiplicative_normalizedone) + ge_balance_negative_signed_multiplicative_normalizedonevalue = (dst_negative_signed_multiplicative_normalizedone) + ge_balance_positive_signed_multiplicative_normalizedonevalue))))))))) /\ (forall mp_a_signed_multiplicative_normalized mp_b_signed_multiplicative_normalized mp_x_signed_multiplicative_normalized mp_y_signed_multiplicative_normalized mp_z_signed_multiplicative_normalized. ~(mp_a_signed_multiplicative_normalized=0) -> ~(mp_b_signed_multiplicative_normalized=0) -> (exists pvs_le_gap_signed_multiplicative_normalizedbound. pvs_le_gap_signed_multiplicative_normalizedbound + (mp_a_signed_multiplicative_normalized*mp_b_signed_multiplicative_normalized) = (N)) -> (forall frp_divisor_signed_multiplicative_normalizedcoprime. (exists frp_left_factor_signed_multiplicative_normalizedcoprime. mp_a_signed_multiplicative_normalized = frp_divisor_signed_multiplicative_normalizedcoprime * frp_left_factor_signed_multiplicative_normalizedcoprime) -> (exists frp_right_factor_signed_multiplicative_normalizedcoprime. mp_b_signed_multiplicative_normalized = frp_divisor_signed_multiplicative_normalizedcoprime * frp_right_factor_signed_multiplicative_normalizedcoprime) -> frp_divisor_signed_multiplicative_normalizedcoprime = 1) -> (exists dst_positive_code_signed_multiplicative_normalizedfirst dst_positive_scale_signed_multiplicative_normalizedfirst dst_negative_code_signed_multiplicative_normalizedfirst dst_negative_scale_signed_multiplicative_normalizedfirst dst_positive_signed_multiplicative_normalizedfirst dst_negative_signed_multiplicative_normalizedfirst. (((F) = (((((dst_positive_code_signed_multiplicative_normalizedfirst) + (dst_positive_scale_signed_multiplicative_normalizedfirst)) * S ((dst_positive_code_signed_multiplicative_normalizedfirst) + (dst_positive_scale_signed_multiplicative_normalizedfirst)) + ((dst_positive_scale_signed_multiplicative_normalizedfirst) + (dst_positive_scale_signed_multiplicative_normalizedfirst))) + (((dst_negative_code_signed_multiplicative_normalizedfirst) + (dst_negative_scale_signed_multiplicative_normalizedfirst)) * S ((dst_negative_code_signed_multiplicative_normalizedfirst) + (dst_negative_scale_signed_multiplicative_normalizedfirst)) + ((dst_negative_scale_signed_multiplicative_normalizedfirst) + (dst_negative_scale_signed_multiplicative_normalizedfirst)))) * S ((((dst_positive_code_signed_multiplicative_normalizedfirst) + (dst_positive_scale_signed_multiplicative_normalizedfirst)) * S ((dst_positive_code_signed_multiplicative_normalizedfirst) + (dst_positive_scale_signed_multiplicative_normalizedfirst)) + ((dst_positive_scale_signed_multiplicative_normalizedfirst) + (dst_positive_scale_signed_multiplicative_normalizedfirst))) + (((dst_negative_code_signed_multiplicative_normalizedfirst) + (dst_negative_scale_signed_multiplicative_normalizedfirst)) * S ((dst_negative_code_signed_multiplicative_normalizedfirst) + (dst_negative_scale_signed_multiplicative_normalizedfirst)) + ((dst_negative_scale_signed_multiplicative_normalizedfirst) + (dst_negative_scale_signed_multiplicative_normalizedfirst)))) + ((((dst_negative_code_signed_multiplicative_normalizedfirst) + (dst_negative_scale_signed_multiplicative_normalizedfirst)) * S ((dst_negative_code_signed_multiplicative_normalizedfirst) + (dst_negative_scale_signed_multiplicative_normalizedfirst)) + ((dst_negative_scale_signed_multiplicative_normalizedfirst) + (dst_negative_scale_signed_multiplicative_normalizedfirst))) + (((dst_negative_code_signed_multiplicative_normalizedfirst) + (dst_negative_scale_signed_multiplicative_normalizedfirst)) * S ((dst_negative_code_signed_multiplicative_normalizedfirst) + (dst_negative_scale_signed_multiplicative_normalizedfirst)) + ((dst_negative_scale_signed_multiplicative_normalizedfirst) + (dst_negative_scale_signed_multiplicative_normalizedfirst)))))) /\ (((((exists ff_h_pvs_signed_multiplicative_normalizedfirstpositive. ff_h_pvs_signed_multiplicative_normalizedfirstpositive + S (dst_positive_signed_multiplicative_normalizedfirst) = S ((S (mp_a_signed_multiplicative_normalized)) * dst_positive_scale_signed_multiplicative_normalizedfirst)) /\ exists ff_q_pvs_signed_multiplicative_normalizedfirstpositive. dst_positive_code_signed_multiplicative_normalizedfirst = ff_q_pvs_signed_multiplicative_normalizedfirstpositive * S ((S (mp_a_signed_multiplicative_normalized)) * dst_positive_scale_signed_multiplicative_normalizedfirst) + (dst_positive_signed_multiplicative_normalizedfirst))) /\ (((((exists ff_h_pvs_signed_multiplicative_normalizedfirstnegative. ff_h_pvs_signed_multiplicative_normalizedfirstnegative + S (dst_negative_signed_multiplicative_normalizedfirst) = S ((S (mp_a_signed_multiplicative_normalized)) * dst_negative_scale_signed_multiplicative_normalizedfirst)) /\ exists ff_q_pvs_signed_multiplicative_normalizedfirstnegative. dst_negative_code_signed_multiplicative_normalizedfirst = ff_q_pvs_signed_multiplicative_normalizedfirstnegative * S ((S (mp_a_signed_multiplicative_normalized)) * dst_negative_scale_signed_multiplicative_normalizedfirst) + (dst_negative_signed_multiplicative_normalizedfirst))) /\ (exists ge_balance_positive_signed_multiplicative_normalizedfirstvalue ge_balance_negative_signed_multiplicative_normalizedfirstvalue. (((((mp_x_signed_multiplicative_normalized) = 2 * (ge_balance_positive_signed_multiplicative_normalizedfirstvalue) /\ (ge_balance_negative_signed_multiplicative_normalizedfirstvalue) = 0) \/ exists ge_signed_half_signed_multiplicative_normalizedfirstvaluedecode. (((mp_x_signed_multiplicative_normalized) = 2 * ge_signed_half_signed_multiplicative_normalizedfirstvaluedecode + 1 /\ (ge_balance_positive_signed_multiplicative_normalizedfirstvalue) = 0) /\ (ge_balance_negative_signed_multiplicative_normalizedfirstvalue) = S ge_signed_half_signed_multiplicative_normalizedfirstvaluedecode))) /\ ((dst_positive_signed_multiplicative_normalizedfirst) + ge_balance_negative_signed_multiplicative_normalizedfirstvalue = (dst_negative_signed_multiplicative_normalizedfirst) + ge_balance_positive_signed_multiplicative_normalizedfirstvalue))))))))) -> (exists dst_positive_code_signed_multiplicative_normalizedsecond dst_positive_scale_signed_multiplicative_normalizedsecond dst_negative_code_signed_multiplicative_normalizedsecond dst_negative_scale_signed_multiplicative_normalizedsecond dst_positive_signed_multiplicative_normalizedsecond dst_negative_signed_multiplicative_normalizedsecond. (((F) = (((((dst_positive_code_signed_multiplicative_normalizedsecond) + (dst_positive_scale_signed_multiplicative_normalizedsecond)) * S ((dst_positive_code_signed_multiplicative_normalizedsecond) + (dst_positive_scale_signed_multiplicative_normalizedsecond)) + ((dst_positive_scale_signed_multiplicative_normalizedsecond) + (dst_positive_scale_signed_multiplicative_normalizedsecond))) + (((dst_negative_code_signed_multiplicative_normalizedsecond) + (dst_negative_scale_signed_multiplicative_normalizedsecond)) * S ((dst_negative_code_signed_multiplicative_normalizedsecond) + (dst_negative_scale_signed_multiplicative_normalizedsecond)) + ((dst_negative_scale_signed_multiplicative_normalizedsecond) + (dst_negative_scale_signed_multiplicative_normalizedsecond)))) * S ((((dst_positive_code_signed_multiplicative_normalizedsecond) + (dst_positive_scale_signed_multiplicative_normalizedsecond)) * S ((dst_positive_code_signed_multiplicative_normalizedsecond) + (dst_positive_scale_signed_multiplicative_normalizedsecond)) + ((dst_positive_scale_signed_multiplicative_normalizedsecond) + (dst_positive_scale_signed_multiplicative_normalizedsecond))) + (((dst_negative_code_signed_multiplicative_normalizedsecond) + (dst_negative_scale_signed_multiplicative_normalizedsecond)) * S ((dst_negative_code_signed_multiplicative_normalizedsecond) + (dst_negative_scale_signed_multiplicative_normalizedsecond)) + ((dst_negative_scale_signed_multiplicative_normalizedsecond) + (dst_negative_scale_signed_multiplicative_normalizedsecond)))) + ((((dst_negative_code_signed_multiplicative_normalizedsecond) + (dst_negative_scale_signed_multiplicative_normalizedsecond)) * S ((dst_negative_code_signed_multiplicative_normalizedsecond) + (dst_negative_scale_signed_multiplicative_normalizedsecond)) + ((dst_negative_scale_signed_multiplicative_normalizedsecond) + (dst_negative_scale_signed_multiplicative_normalizedsecond))) + (((dst_negative_code_signed_multiplicative_normalizedsecond) + (dst_negative_scale_signed_multiplicative_normalizedsecond)) * S ((dst_negative_code_signed_multiplicative_normalizedsecond) + (dst_negative_scale_signed_multiplicative_normalizedsecond)) + ((dst_negative_scale_signed_multiplicative_normalizedsecond) + (dst_negative_scale_signed_multiplicative_normalizedsecond)))))) /\ (((((exists ff_h_pvs_signed_multiplicative_normalizedsecondpositive. ff_h_pvs_signed_multiplicative_normalizedsecondpositive + S (dst_positive_signed_multiplicative_normalizedsecond) = S ((S (mp_b_signed_multiplicative_normalized)) * dst_positive_scale_signed_multiplicative_normalizedsecond)) /\ exists ff_q_pvs_signed_multiplicative_normalizedsecondpositive. dst_positive_code_signed_multiplicative_normalizedsecond = ff_q_pvs_signed_multiplicative_normalizedsecondpositive * S ((S (mp_b_signed_multiplicative_normalized)) * dst_positive_scale_signed_multiplicative_normalizedsecond) + (dst_positive_signed_multiplicative_normalizedsecond))) /\ (((((exists ff_h_pvs_signed_multiplicative_normalizedsecondnegative. ff_h_pvs_signed_multiplicative_normalizedsecondnegative + S (dst_negative_signed_multiplicative_normalizedsecond) = S ((S (mp_b_signed_multiplicative_normalized)) * dst_negative_scale_signed_multiplicative_normalizedsecond)) /\ exists ff_q_pvs_signed_multiplicative_normalizedsecondnegative. dst_negative_code_signed_multiplicative_normalizedsecond = ff_q_pvs_signed_multiplicative_normalizedsecondnegative * S ((S (mp_b_signed_multiplicative_normalized)) * dst_negative_scale_signed_multiplicative_normalizedsecond) + (dst_negative_signed_multiplicative_normalizedsecond))) /\ (exists ge_balance_positive_signed_multiplicative_normalizedsecondvalue ge_balance_negative_signed_multiplicative_normalizedsecondvalue. (((((mp_y_signed_multiplicative_normalized) = 2 * (ge_balance_positive_signed_multiplicative_normalizedsecondvalue) /\ (ge_balance_negative_signed_multiplicative_normalizedsecondvalue) = 0) \/ exists ge_signed_half_signed_multiplicative_normalizedsecondvaluedecode. (((mp_y_signed_multiplicative_normalized) = 2 * ge_signed_half_signed_multiplicative_normalizedsecondvaluedecode + 1 /\ (ge_balance_positive_signed_multiplicative_normalizedsecondvalue) = 0) /\ (ge_balance_negative_signed_multiplicative_normalizedsecondvalue) = S ge_signed_half_signed_multiplicative_normalizedsecondvaluedecode))) /\ ((dst_positive_signed_multiplicative_normalizedsecond) + ge_balance_negative_signed_multiplicative_normalizedsecondvalue = (dst_negative_signed_multiplicative_normalizedsecond) + ge_balance_positive_signed_multiplicative_normalizedsecondvalue))))))))) -> (exists dst_positive_code_signed_multiplicative_normalizedproduct dst_positive_scale_signed_multiplicative_normalizedproduct dst_negative_code_signed_multiplicative_normalizedproduct dst_negative_scale_signed_multiplicative_normalizedproduct dst_positive_signed_multiplicative_normalizedproduct dst_negative_signed_multiplicative_normalizedproduct. (((F) = (((((dst_positive_code_signed_multiplicative_normalizedproduct) + (dst_positive_scale_signed_multiplicative_normalizedproduct)) * S ((dst_positive_code_signed_multiplicative_normalizedproduct) + (dst_positive_scale_signed_multiplicative_normalizedproduct)) + ((dst_positive_scale_signed_multiplicative_normalizedproduct) + (dst_positive_scale_signed_multiplicative_normalizedproduct))) + (((dst_negative_code_signed_multiplicative_normalizedproduct) + (dst_negative_scale_signed_multiplicative_normalizedproduct)) * S ((dst_negative_code_signed_multiplicative_normalizedproduct) + (dst_negative_scale_signed_multiplicative_normalizedproduct)) + ((dst_negative_scale_signed_multiplicative_normalizedproduct) + (dst_negative_scale_signed_multiplicative_normalizedproduct)))) * S ((((dst_positive_code_signed_multiplicative_normalizedproduct) + (dst_positive_scale_signed_multiplicative_normalizedproduct)) * S ((dst_positive_code_signed_multiplicative_normalizedproduct) + (dst_positive_scale_signed_multiplicative_normalizedproduct)) + ((dst_positive_scale_signed_multiplicative_normalizedproduct) + (dst_positive_scale_signed_multiplicative_normalizedproduct))) + (((dst_negative_code_signed_multiplicative_normalizedproduct) + (dst_negative_scale_signed_multiplicative_normalizedproduct)) * S ((dst_negative_code_signed_multiplicative_normalizedproduct) + (dst_negative_scale_signed_multiplicative_normalizedproduct)) + ((dst_negative_scale_signed_multiplicative_normalizedproduct) + (dst_negative_scale_signed_multiplicative_normalizedproduct)))) + ((((dst_negative_code_signed_multiplicative_normalizedproduct) + (dst_negative_scale_signed_multiplicative_normalizedproduct)) * S ((dst_negative_code_signed_multiplicative_normalizedproduct) + (dst_negative_scale_signed_multiplicative_normalizedproduct)) + ((dst_negative_scale_signed_multiplicative_normalizedproduct) + (dst_negative_scale_signed_multiplicative_normalizedproduct))) + (((dst_negative_code_signed_multiplicative_normalizedproduct) + (dst_negative_scale_signed_multiplicative_normalizedproduct)) * S ((dst_negative_code_signed_multiplicative_normalizedproduct) + (dst_negative_scale_signed_multiplicative_normalizedproduct)) + ((dst_negative_scale_signed_multiplicative_normalizedproduct) + (dst_negative_scale_signed_multiplicative_normalizedproduct)))))) /\ (((((exists ff_h_pvs_signed_multiplicative_normalizedproductpositive. ff_h_pvs_signed_multiplicative_normalizedproductpositive + S (dst_positive_signed_multiplicative_normalizedproduct) = S ((S (mp_a_signed_multiplicative_normalized*mp_b_signed_multiplicative_normalized)) * dst_positive_scale_signed_multiplicative_normalizedproduct)) /\ exists ff_q_pvs_signed_multiplicative_normalizedproductpositive. dst_positive_code_signed_multiplicative_normalizedproduct = ff_q_pvs_signed_multiplicative_normalizedproductpositive * S ((S (mp_a_signed_multiplicative_normalized*mp_b_signed_multiplicative_normalized)) * dst_positive_scale_signed_multiplicative_normalizedproduct) + (dst_positive_signed_multiplicative_normalizedproduct))) /\ (((((exists ff_h_pvs_signed_multiplicative_normalizedproductnegative. ff_h_pvs_signed_multiplicative_normalizedproductnegative + S (dst_negative_signed_multiplicative_normalizedproduct) = S ((S (mp_a_signed_multiplicative_normalized*mp_b_signed_multiplicative_normalized)) * dst_negative_scale_signed_multiplicative_normalizedproduct)) /\ exists ff_q_pvs_signed_multiplicative_normalizedproductnegative. dst_negative_code_signed_multiplicative_normalizedproduct = ff_q_pvs_signed_multiplicative_normalizedproductnegative * S ((S (mp_a_signed_multiplicative_normalized*mp_b_signed_multiplicative_normalized)) * dst_negative_scale_signed_multiplicative_normalizedproduct) + (dst_negative_signed_multiplicative_normalizedproduct))) /\ (exists ge_balance_positive_signed_multiplicative_normalizedproductvalue ge_balance_negative_signed_multiplicative_normalizedproductvalue. (((((mp_z_signed_multiplicative_normalized) = 2 * (ge_balance_positive_signed_multiplicative_normalizedproductvalue) /\ (ge_balance_negative_signed_multiplicative_normalizedproductvalue) = 0) \/ exists ge_signed_half_signed_multiplicative_normalizedproductvaluedecode. (((mp_z_signed_multiplicative_normalized) = 2 * ge_signed_half_signed_multiplicative_normalizedproductvaluedecode + 1 /\ (ge_balance_positive_signed_multiplicative_normalizedproductvalue) = 0) /\ (ge_balance_negative_signed_multiplicative_normalizedproductvalue) = S ge_signed_half_signed_multiplicative_normalizedproductvaluedecode))) /\ ((dst_positive_signed_multiplicative_normalizedproduct) + ge_balance_negative_signed_multiplicative_normalizedproductvalue = (dst_negative_signed_multiplicative_normalizedproduct) + ge_balance_positive_signed_multiplicative_normalizedproductvalue))))))))) -> (exists sto_ap_signed_multiplicative_normalizedlaw sto_an_signed_multiplicative_normalizedlaw sto_bp_signed_multiplicative_normalizedlaw sto_bn_signed_multiplicative_normalizedlaw sto_cp_signed_multiplicative_normalizedlaw sto_cn_signed_multiplicative_normalizedlaw. (((((mp_x_signed_multiplicative_normalized) = 2 * (sto_ap_signed_multiplicative_normalizedlaw) /\ (sto_an_signed_multiplicative_normalizedlaw) = 0) \/ exists ge_signed_half_signed_multiplicative_normalizedlawleft. (((mp_x_signed_multiplicative_normalized) = 2 * ge_signed_half_signed_multiplicative_normalizedlawleft + 1 /\ (sto_ap_signed_multiplicative_normalizedlaw) = 0) /\ (sto_an_signed_multiplicative_normalizedlaw) = S ge_signed_half_signed_multiplicative_normalizedlawleft))) /\ ((((((mp_y_signed_multiplicative_normalized) = 2 * (sto_bp_signed_multiplicative_normalizedlaw) /\ (sto_bn_signed_multiplicative_normalizedlaw) = 0) \/ exists ge_signed_half_signed_multiplicative_normalizedlawright. (((mp_y_signed_multiplicative_normalized) = 2 * ge_signed_half_signed_multiplicative_normalizedlawright + 1 /\ (sto_bp_signed_multiplicative_normalizedlaw) = 0) /\ (sto_bn_signed_multiplicative_normalizedlaw) = S ge_signed_half_signed_multiplicative_normalizedlawright))) /\ ((((((mp_z_signed_multiplicative_normalized) = 2 * (sto_cp_signed_multiplicative_normalizedlaw) /\ (sto_cn_signed_multiplicative_normalizedlaw) = 0) \/ exists ge_signed_half_signed_multiplicative_normalizedlawoutput. (((mp_z_signed_multiplicative_normalized) = 2 * ge_signed_half_signed_multiplicative_normalizedlawoutput + 1 /\ (sto_cp_signed_multiplicative_normalizedlaw) = 0) /\ (sto_cn_signed_multiplicative_normalizedlaw) = S ge_signed_half_signed_multiplicative_normalizedlawoutput))) /\ ((sto_ap_signed_multiplicative_normalizedlaw * sto_bp_signed_multiplicative_normalizedlaw + sto_an_signed_multiplicative_normalizedlaw * sto_bn_signed_multiplicative_normalizedlaw) + sto_cn_signed_multiplicative_normalizedlaw = (sto_ap_signed_multiplicative_normalizedlaw * sto_bn_signed_multiplicative_normalizedlaw + sto_an_signed_multiplicative_normalizedlaw * sto_bp_signed_multiplicative_normalizedlaw) + sto_cp_signed_multiplicative_normalizedlaw)))))))))))))) -> (exists dst_positive_code_project_one dst_positive_scale_project_one dst_negative_code_project_one dst_negative_scale_project_one dst_positive_project_one dst_negative_project_one. (((F) = (((((dst_positive_code_project_one) + (dst_positive_scale_project_one)) * S ((dst_positive_code_project_one) + (dst_positive_scale_project_one)) + ((dst_positive_scale_project_one) + (dst_positive_scale_project_one))) + (((dst_negative_code_project_one) + (dst_negative_scale_project_one)) * S ((dst_negative_code_project_one) + (dst_negative_scale_project_one)) + ((dst_negative_scale_project_one) + (dst_negative_scale_project_one)))) * S ((((dst_positive_code_project_one) + (dst_positive_scale_project_one)) * S ((dst_positive_code_project_one) + (dst_positive_scale_project_one)) + ((dst_positive_scale_project_one) + (dst_positive_scale_project_one))) + (((dst_negative_code_project_one) + (dst_negative_scale_project_one)) * S ((dst_negative_code_project_one) + (dst_negative_scale_project_one)) + ((dst_negative_scale_project_one) + (dst_negative_scale_project_one)))) + ((((dst_negative_code_project_one) + (dst_negative_scale_project_one)) * S ((dst_negative_code_project_one) + (dst_negative_scale_project_one)) + ((dst_negative_scale_project_one) + (dst_negative_scale_project_one))) + (((dst_negative_code_project_one) + (dst_negative_scale_project_one)) * S ((dst_negative_code_project_one) + (dst_negative_scale_project_one)) + ((dst_negative_scale_project_one) + (dst_negative_scale_project_one)))))) /\ (((((exists ff_h_pvs_project_onepositive. ff_h_pvs_project_onepositive + S (dst_positive_project_one) = S ((S (1)) * dst_positive_scale_project_one)) /\ exists ff_q_pvs_project_onepositive. dst_positive_code_project_one = ff_q_pvs_project_onepositive * S ((S (1)) * dst_positive_scale_project_one) + (dst_positive_project_one))) /\ (((((exists ff_h_pvs_project_onenegative. ff_h_pvs_project_onenegative + S (dst_negative_project_one) = S ((S (1)) * dst_negative_scale_project_one)) /\ exists ff_q_pvs_project_onenegative. dst_negative_code_project_one = ff_q_pvs_project_onenegative * S ((S (1)) * dst_negative_scale_project_one) + (dst_negative_project_one))) /\ (exists ge_balance_positive_project_onevalue ge_balance_negative_project_onevalue. (((((2) = 2 * (ge_balance_positive_project_onevalue) /\ (ge_balance_negative_project_onevalue) = 0) \/ exists ge_signed_half_project_onevaluedecode. (((2) = 2 * ge_signed_half_project_onevaluedecode + 1 /\ (ge_balance_positive_project_onevalue) = 0) /\ (ge_balance_negative_project_onevalue) = S ge_signed_half_project_onevaluedecode))) /\ ((dst_positive_project_one) + ge_balance_negative_project_onevalue = (dst_negative_project_one) + ge_balance_positive_project_onevalue)))))))))