signed_multiplicative_nonempty

Exact expanded first-order arithmetic statement

forall N F. (((~((N)=0)) /\ (((exists dst_positive_code_signed_multiplicative_nonemptytable dst_positive_scale_signed_multiplicative_nonemptytable dst_negative_code_signed_multiplicative_nonemptytable dst_negative_scale_signed_multiplicative_nonemptytable. (((F) = (((((dst_positive_code_signed_multiplicative_nonemptytable) + (dst_positive_scale_signed_multiplicative_nonemptytable)) * S ((dst_positive_code_signed_multiplicative_nonemptytable) + (dst_positive_scale_signed_multiplicative_nonemptytable)) + ((dst_positive_scale_signed_multiplicative_nonemptytable) + (dst_positive_scale_signed_multiplicative_nonemptytable))) + (((dst_negative_code_signed_multiplicative_nonemptytable) + (dst_negative_scale_signed_multiplicative_nonemptytable)) * S ((dst_negative_code_signed_multiplicative_nonemptytable) + (dst_negative_scale_signed_multiplicative_nonemptytable)) + ((dst_negative_scale_signed_multiplicative_nonemptytable) + (dst_negative_scale_signed_multiplicative_nonemptytable)))) * S ((((dst_positive_code_signed_multiplicative_nonemptytable) + (dst_positive_scale_signed_multiplicative_nonemptytable)) * S ((dst_positive_code_signed_multiplicative_nonemptytable) + (dst_positive_scale_signed_multiplicative_nonemptytable)) + ((dst_positive_scale_signed_multiplicative_nonemptytable) + (dst_positive_scale_signed_multiplicative_nonemptytable))) + (((dst_negative_code_signed_multiplicative_nonemptytable) + (dst_negative_scale_signed_multiplicative_nonemptytable)) * S ((dst_negative_code_signed_multiplicative_nonemptytable) + (dst_negative_scale_signed_multiplicative_nonemptytable)) + ((dst_negative_scale_signed_multiplicative_nonemptytable) + (dst_negative_scale_signed_multiplicative_nonemptytable)))) + ((((dst_negative_code_signed_multiplicative_nonemptytable) + (dst_negative_scale_signed_multiplicative_nonemptytable)) * S ((dst_negative_code_signed_multiplicative_nonemptytable) + (dst_negative_scale_signed_multiplicative_nonemptytable)) + ((dst_negative_scale_signed_multiplicative_nonemptytable) + (dst_negative_scale_signed_multiplicative_nonemptytable))) + (((dst_negative_code_signed_multiplicative_nonemptytable) + (dst_negative_scale_signed_multiplicative_nonemptytable)) * S ((dst_negative_code_signed_multiplicative_nonemptytable) + (dst_negative_scale_signed_multiplicative_nonemptytable)) + ((dst_negative_scale_signed_multiplicative_nonemptytable) + (dst_negative_scale_signed_multiplicative_nonemptytable)))))) /\ (forall dst_index_signed_multiplicative_nonemptytable. (exists pvs_le_gap_signed_multiplicative_nonemptytabledomain. pvs_le_gap_signed_multiplicative_nonemptytabledomain + (dst_index_signed_multiplicative_nonemptytable) = (N)) -> exists dst_positive_signed_multiplicative_nonemptytable dst_negative_signed_multiplicative_nonemptytable dst_value_signed_multiplicative_nonemptytable. ((((exists ff_h_pvs_signed_multiplicative_nonemptytableentrypositive. ff_h_pvs_signed_multiplicative_nonemptytableentrypositive + S (dst_positive_signed_multiplicative_nonemptytable) = S ((S (dst_index_signed_multiplicative_nonemptytable)) * dst_positive_scale_signed_multiplicative_nonemptytable)) /\ exists ff_q_pvs_signed_multiplicative_nonemptytableentrypositive. dst_positive_code_signed_multiplicative_nonemptytable = ff_q_pvs_signed_multiplicative_nonemptytableentrypositive * S ((S (dst_index_signed_multiplicative_nonemptytable)) * dst_positive_scale_signed_multiplicative_nonemptytable) + (dst_positive_signed_multiplicative_nonemptytable))) /\ (((((exists ff_h_pvs_signed_multiplicative_nonemptytableentrynegative. ff_h_pvs_signed_multiplicative_nonemptytableentrynegative + S (dst_negative_signed_multiplicative_nonemptytable) = S ((S (dst_index_signed_multiplicative_nonemptytable)) * dst_negative_scale_signed_multiplicative_nonemptytable)) /\ exists ff_q_pvs_signed_multiplicative_nonemptytableentrynegative. dst_negative_code_signed_multiplicative_nonemptytable = ff_q_pvs_signed_multiplicative_nonemptytableentrynegative * S ((S (dst_index_signed_multiplicative_nonemptytable)) * dst_negative_scale_signed_multiplicative_nonemptytable) + (dst_negative_signed_multiplicative_nonemptytable))) /\ (exists ge_balance_positive_signed_multiplicative_nonemptytableentryvalue ge_balance_negative_signed_multiplicative_nonemptytableentryvalue. (((((dst_value_signed_multiplicative_nonemptytable) = 2 * (ge_balance_positive_signed_multiplicative_nonemptytableentryvalue) /\ (ge_balance_negative_signed_multiplicative_nonemptytableentryvalue) = 0) \/ exists ge_signed_half_signed_multiplicative_nonemptytableentryvaluedecode. (((dst_value_signed_multiplicative_nonemptytable) = 2 * ge_signed_half_signed_multiplicative_nonemptytableentryvaluedecode + 1 /\ (ge_balance_positive_signed_multiplicative_nonemptytableentryvalue) = 0) /\ (ge_balance_negative_signed_multiplicative_nonemptytableentryvalue) = S ge_signed_half_signed_multiplicative_nonemptytableentryvaluedecode))) /\ ((dst_positive_signed_multiplicative_nonemptytable) + ge_balance_negative_signed_multiplicative_nonemptytableentryvalue = (dst_negative_signed_multiplicative_nonemptytable) + ge_balance_positive_signed_multiplicative_nonemptytableentryvalue))))))))) /\ (((exists dst_positive_code_signed_multiplicative_nonemptyone dst_positive_scale_signed_multiplicative_nonemptyone dst_negative_code_signed_multiplicative_nonemptyone dst_negative_scale_signed_multiplicative_nonemptyone dst_positive_signed_multiplicative_nonemptyone dst_negative_signed_multiplicative_nonemptyone. (((F) = (((((dst_positive_code_signed_multiplicative_nonemptyone) + (dst_positive_scale_signed_multiplicative_nonemptyone)) * S ((dst_positive_code_signed_multiplicative_nonemptyone) + (dst_positive_scale_signed_multiplicative_nonemptyone)) + ((dst_positive_scale_signed_multiplicative_nonemptyone) + (dst_positive_scale_signed_multiplicative_nonemptyone))) + (((dst_negative_code_signed_multiplicative_nonemptyone) + (dst_negative_scale_signed_multiplicative_nonemptyone)) * S ((dst_negative_code_signed_multiplicative_nonemptyone) + (dst_negative_scale_signed_multiplicative_nonemptyone)) + ((dst_negative_scale_signed_multiplicative_nonemptyone) + (dst_negative_scale_signed_multiplicative_nonemptyone)))) * S ((((dst_positive_code_signed_multiplicative_nonemptyone) + (dst_positive_scale_signed_multiplicative_nonemptyone)) * S ((dst_positive_code_signed_multiplicative_nonemptyone) + (dst_positive_scale_signed_multiplicative_nonemptyone)) + ((dst_positive_scale_signed_multiplicative_nonemptyone) + (dst_positive_scale_signed_multiplicative_nonemptyone))) + (((dst_negative_code_signed_multiplicative_nonemptyone) + (dst_negative_scale_signed_multiplicative_nonemptyone)) * S ((dst_negative_code_signed_multiplicative_nonemptyone) + (dst_negative_scale_signed_multiplicative_nonemptyone)) + ((dst_negative_scale_signed_multiplicative_nonemptyone) + (dst_negative_scale_signed_multiplicative_nonemptyone)))) + ((((dst_negative_code_signed_multiplicative_nonemptyone) + (dst_negative_scale_signed_multiplicative_nonemptyone)) * S ((dst_negative_code_signed_multiplicative_nonemptyone) + (dst_negative_scale_signed_multiplicative_nonemptyone)) + ((dst_negative_scale_signed_multiplicative_nonemptyone) + (dst_negative_scale_signed_multiplicative_nonemptyone))) + (((dst_negative_code_signed_multiplicative_nonemptyone) + (dst_negative_scale_signed_multiplicative_nonemptyone)) * S ((dst_negative_code_signed_multiplicative_nonemptyone) + (dst_negative_scale_signed_multiplicative_nonemptyone)) + ((dst_negative_scale_signed_multiplicative_nonemptyone) + (dst_negative_scale_signed_multiplicative_nonemptyone)))))) /\ (((((exists ff_h_pvs_signed_multiplicative_nonemptyonepositive. ff_h_pvs_signed_multiplicative_nonemptyonepositive + S (dst_positive_signed_multiplicative_nonemptyone) = S ((S (1)) * dst_positive_scale_signed_multiplicative_nonemptyone)) /\ exists ff_q_pvs_signed_multiplicative_nonemptyonepositive. dst_positive_code_signed_multiplicative_nonemptyone = ff_q_pvs_signed_multiplicative_nonemptyonepositive * S ((S (1)) * dst_positive_scale_signed_multiplicative_nonemptyone) + (dst_positive_signed_multiplicative_nonemptyone))) /\ (((((exists ff_h_pvs_signed_multiplicative_nonemptyonenegative. ff_h_pvs_signed_multiplicative_nonemptyonenegative + S (dst_negative_signed_multiplicative_nonemptyone) = S ((S (1)) * dst_negative_scale_signed_multiplicative_nonemptyone)) /\ exists ff_q_pvs_signed_multiplicative_nonemptyonenegative. dst_negative_code_signed_multiplicative_nonemptyone = ff_q_pvs_signed_multiplicative_nonemptyonenegative * S ((S (1)) * dst_negative_scale_signed_multiplicative_nonemptyone) + (dst_negative_signed_multiplicative_nonemptyone))) /\ (exists ge_balance_positive_signed_multiplicative_nonemptyonevalue ge_balance_negative_signed_multiplicative_nonemptyonevalue. (((((2) = 2 * (ge_balance_positive_signed_multiplicative_nonemptyonevalue) /\ (ge_balance_negative_signed_multiplicative_nonemptyonevalue) = 0) \/ exists ge_signed_half_signed_multiplicative_nonemptyonevaluedecode. (((2) = 2 * ge_signed_half_signed_multiplicative_nonemptyonevaluedecode + 1 /\ (ge_balance_positive_signed_multiplicative_nonemptyonevalue) = 0) /\ (ge_balance_negative_signed_multiplicative_nonemptyonevalue) = S ge_signed_half_signed_multiplicative_nonemptyonevaluedecode))) /\ ((dst_positive_signed_multiplicative_nonemptyone) + ge_balance_negative_signed_multiplicative_nonemptyonevalue = (dst_negative_signed_multiplicative_nonemptyone) + ge_balance_positive_signed_multiplicative_nonemptyonevalue))))))))) /\ (forall mp_a_signed_multiplicative_nonempty mp_b_signed_multiplicative_nonempty mp_x_signed_multiplicative_nonempty mp_y_signed_multiplicative_nonempty mp_z_signed_multiplicative_nonempty. ~(mp_a_signed_multiplicative_nonempty=0) -> ~(mp_b_signed_multiplicative_nonempty=0) -> (exists pvs_le_gap_signed_multiplicative_nonemptybound. pvs_le_gap_signed_multiplicative_nonemptybound + (mp_a_signed_multiplicative_nonempty*mp_b_signed_multiplicative_nonempty) = (N)) -> (forall frp_divisor_signed_multiplicative_nonemptycoprime. (exists frp_left_factor_signed_multiplicative_nonemptycoprime. mp_a_signed_multiplicative_nonempty = frp_divisor_signed_multiplicative_nonemptycoprime * frp_left_factor_signed_multiplicative_nonemptycoprime) -> (exists frp_right_factor_signed_multiplicative_nonemptycoprime. mp_b_signed_multiplicative_nonempty = frp_divisor_signed_multiplicative_nonemptycoprime * frp_right_factor_signed_multiplicative_nonemptycoprime) -> frp_divisor_signed_multiplicative_nonemptycoprime = 1) -> (exists dst_positive_code_signed_multiplicative_nonemptyfirst dst_positive_scale_signed_multiplicative_nonemptyfirst dst_negative_code_signed_multiplicative_nonemptyfirst dst_negative_scale_signed_multiplicative_nonemptyfirst dst_positive_signed_multiplicative_nonemptyfirst dst_negative_signed_multiplicative_nonemptyfirst. (((F) = (((((dst_positive_code_signed_multiplicative_nonemptyfirst) + (dst_positive_scale_signed_multiplicative_nonemptyfirst)) * S ((dst_positive_code_signed_multiplicative_nonemptyfirst) + (dst_positive_scale_signed_multiplicative_nonemptyfirst)) + ((dst_positive_scale_signed_multiplicative_nonemptyfirst) + (dst_positive_scale_signed_multiplicative_nonemptyfirst))) + (((dst_negative_code_signed_multiplicative_nonemptyfirst) + (dst_negative_scale_signed_multiplicative_nonemptyfirst)) * S ((dst_negative_code_signed_multiplicative_nonemptyfirst) + (dst_negative_scale_signed_multiplicative_nonemptyfirst)) + ((dst_negative_scale_signed_multiplicative_nonemptyfirst) + (dst_negative_scale_signed_multiplicative_nonemptyfirst)))) * S ((((dst_positive_code_signed_multiplicative_nonemptyfirst) + (dst_positive_scale_signed_multiplicative_nonemptyfirst)) * S ((dst_positive_code_signed_multiplicative_nonemptyfirst) + (dst_positive_scale_signed_multiplicative_nonemptyfirst)) + ((dst_positive_scale_signed_multiplicative_nonemptyfirst) + (dst_positive_scale_signed_multiplicative_nonemptyfirst))) + (((dst_negative_code_signed_multiplicative_nonemptyfirst) + (dst_negative_scale_signed_multiplicative_nonemptyfirst)) * S ((dst_negative_code_signed_multiplicative_nonemptyfirst) + (dst_negative_scale_signed_multiplicative_nonemptyfirst)) + ((dst_negative_scale_signed_multiplicative_nonemptyfirst) + (dst_negative_scale_signed_multiplicative_nonemptyfirst)))) + ((((dst_negative_code_signed_multiplicative_nonemptyfirst) + (dst_negative_scale_signed_multiplicative_nonemptyfirst)) * S ((dst_negative_code_signed_multiplicative_nonemptyfirst) + (dst_negative_scale_signed_multiplicative_nonemptyfirst)) + ((dst_negative_scale_signed_multiplicative_nonemptyfirst) + (dst_negative_scale_signed_multiplicative_nonemptyfirst))) + (((dst_negative_code_signed_multiplicative_nonemptyfirst) + (dst_negative_scale_signed_multiplicative_nonemptyfirst)) * S ((dst_negative_code_signed_multiplicative_nonemptyfirst) + (dst_negative_scale_signed_multiplicative_nonemptyfirst)) + ((dst_negative_scale_signed_multiplicative_nonemptyfirst) + (dst_negative_scale_signed_multiplicative_nonemptyfirst)))))) /\ (((((exists ff_h_pvs_signed_multiplicative_nonemptyfirstpositive. ff_h_pvs_signed_multiplicative_nonemptyfirstpositive + S (dst_positive_signed_multiplicative_nonemptyfirst) = S ((S (mp_a_signed_multiplicative_nonempty)) * dst_positive_scale_signed_multiplicative_nonemptyfirst)) /\ exists ff_q_pvs_signed_multiplicative_nonemptyfirstpositive. dst_positive_code_signed_multiplicative_nonemptyfirst = ff_q_pvs_signed_multiplicative_nonemptyfirstpositive * S ((S (mp_a_signed_multiplicative_nonempty)) * dst_positive_scale_signed_multiplicative_nonemptyfirst) + (dst_positive_signed_multiplicative_nonemptyfirst))) /\ (((((exists ff_h_pvs_signed_multiplicative_nonemptyfirstnegative. ff_h_pvs_signed_multiplicative_nonemptyfirstnegative + S (dst_negative_signed_multiplicative_nonemptyfirst) = S ((S (mp_a_signed_multiplicative_nonempty)) * dst_negative_scale_signed_multiplicative_nonemptyfirst)) /\ exists ff_q_pvs_signed_multiplicative_nonemptyfirstnegative. dst_negative_code_signed_multiplicative_nonemptyfirst = ff_q_pvs_signed_multiplicative_nonemptyfirstnegative * S ((S (mp_a_signed_multiplicative_nonempty)) * dst_negative_scale_signed_multiplicative_nonemptyfirst) + (dst_negative_signed_multiplicative_nonemptyfirst))) /\ (exists ge_balance_positive_signed_multiplicative_nonemptyfirstvalue ge_balance_negative_signed_multiplicative_nonemptyfirstvalue. (((((mp_x_signed_multiplicative_nonempty) = 2 * (ge_balance_positive_signed_multiplicative_nonemptyfirstvalue) /\ (ge_balance_negative_signed_multiplicative_nonemptyfirstvalue) = 0) \/ exists ge_signed_half_signed_multiplicative_nonemptyfirstvaluedecode. (((mp_x_signed_multiplicative_nonempty) = 2 * ge_signed_half_signed_multiplicative_nonemptyfirstvaluedecode + 1 /\ (ge_balance_positive_signed_multiplicative_nonemptyfirstvalue) = 0) /\ (ge_balance_negative_signed_multiplicative_nonemptyfirstvalue) = S ge_signed_half_signed_multiplicative_nonemptyfirstvaluedecode))) /\ ((dst_positive_signed_multiplicative_nonemptyfirst) + ge_balance_negative_signed_multiplicative_nonemptyfirstvalue = (dst_negative_signed_multiplicative_nonemptyfirst) + ge_balance_positive_signed_multiplicative_nonemptyfirstvalue))))))))) -> (exists dst_positive_code_signed_multiplicative_nonemptysecond dst_positive_scale_signed_multiplicative_nonemptysecond dst_negative_code_signed_multiplicative_nonemptysecond dst_negative_scale_signed_multiplicative_nonemptysecond dst_positive_signed_multiplicative_nonemptysecond dst_negative_signed_multiplicative_nonemptysecond. (((F) = (((((dst_positive_code_signed_multiplicative_nonemptysecond) + (dst_positive_scale_signed_multiplicative_nonemptysecond)) * S ((dst_positive_code_signed_multiplicative_nonemptysecond) + (dst_positive_scale_signed_multiplicative_nonemptysecond)) + ((dst_positive_scale_signed_multiplicative_nonemptysecond) + (dst_positive_scale_signed_multiplicative_nonemptysecond))) + (((dst_negative_code_signed_multiplicative_nonemptysecond) + (dst_negative_scale_signed_multiplicative_nonemptysecond)) * S ((dst_negative_code_signed_multiplicative_nonemptysecond) + (dst_negative_scale_signed_multiplicative_nonemptysecond)) + ((dst_negative_scale_signed_multiplicative_nonemptysecond) + (dst_negative_scale_signed_multiplicative_nonemptysecond)))) * S ((((dst_positive_code_signed_multiplicative_nonemptysecond) + (dst_positive_scale_signed_multiplicative_nonemptysecond)) * S ((dst_positive_code_signed_multiplicative_nonemptysecond) + (dst_positive_scale_signed_multiplicative_nonemptysecond)) + ((dst_positive_scale_signed_multiplicative_nonemptysecond) + (dst_positive_scale_signed_multiplicative_nonemptysecond))) + (((dst_negative_code_signed_multiplicative_nonemptysecond) + (dst_negative_scale_signed_multiplicative_nonemptysecond)) * S ((dst_negative_code_signed_multiplicative_nonemptysecond) + (dst_negative_scale_signed_multiplicative_nonemptysecond)) + ((dst_negative_scale_signed_multiplicative_nonemptysecond) + (dst_negative_scale_signed_multiplicative_nonemptysecond)))) + ((((dst_negative_code_signed_multiplicative_nonemptysecond) + (dst_negative_scale_signed_multiplicative_nonemptysecond)) * S ((dst_negative_code_signed_multiplicative_nonemptysecond) + (dst_negative_scale_signed_multiplicative_nonemptysecond)) + ((dst_negative_scale_signed_multiplicative_nonemptysecond) + (dst_negative_scale_signed_multiplicative_nonemptysecond))) + (((dst_negative_code_signed_multiplicative_nonemptysecond) + (dst_negative_scale_signed_multiplicative_nonemptysecond)) * S ((dst_negative_code_signed_multiplicative_nonemptysecond) + (dst_negative_scale_signed_multiplicative_nonemptysecond)) + ((dst_negative_scale_signed_multiplicative_nonemptysecond) + (dst_negative_scale_signed_multiplicative_nonemptysecond)))))) /\ (((((exists ff_h_pvs_signed_multiplicative_nonemptysecondpositive. ff_h_pvs_signed_multiplicative_nonemptysecondpositive + S (dst_positive_signed_multiplicative_nonemptysecond) = S ((S (mp_b_signed_multiplicative_nonempty)) * dst_positive_scale_signed_multiplicative_nonemptysecond)) /\ exists ff_q_pvs_signed_multiplicative_nonemptysecondpositive. dst_positive_code_signed_multiplicative_nonemptysecond = ff_q_pvs_signed_multiplicative_nonemptysecondpositive * S ((S (mp_b_signed_multiplicative_nonempty)) * dst_positive_scale_signed_multiplicative_nonemptysecond) + (dst_positive_signed_multiplicative_nonemptysecond))) /\ (((((exists ff_h_pvs_signed_multiplicative_nonemptysecondnegative. ff_h_pvs_signed_multiplicative_nonemptysecondnegative + S (dst_negative_signed_multiplicative_nonemptysecond) = S ((S (mp_b_signed_multiplicative_nonempty)) * dst_negative_scale_signed_multiplicative_nonemptysecond)) /\ exists ff_q_pvs_signed_multiplicative_nonemptysecondnegative. dst_negative_code_signed_multiplicative_nonemptysecond = ff_q_pvs_signed_multiplicative_nonemptysecondnegative * S ((S (mp_b_signed_multiplicative_nonempty)) * dst_negative_scale_signed_multiplicative_nonemptysecond) + (dst_negative_signed_multiplicative_nonemptysecond))) /\ (exists ge_balance_positive_signed_multiplicative_nonemptysecondvalue ge_balance_negative_signed_multiplicative_nonemptysecondvalue. (((((mp_y_signed_multiplicative_nonempty) = 2 * (ge_balance_positive_signed_multiplicative_nonemptysecondvalue) /\ (ge_balance_negative_signed_multiplicative_nonemptysecondvalue) = 0) \/ exists ge_signed_half_signed_multiplicative_nonemptysecondvaluedecode. (((mp_y_signed_multiplicative_nonempty) = 2 * ge_signed_half_signed_multiplicative_nonemptysecondvaluedecode + 1 /\ (ge_balance_positive_signed_multiplicative_nonemptysecondvalue) = 0) /\ (ge_balance_negative_signed_multiplicative_nonemptysecondvalue) = S ge_signed_half_signed_multiplicative_nonemptysecondvaluedecode))) /\ ((dst_positive_signed_multiplicative_nonemptysecond) + ge_balance_negative_signed_multiplicative_nonemptysecondvalue = (dst_negative_signed_multiplicative_nonemptysecond) + ge_balance_positive_signed_multiplicative_nonemptysecondvalue))))))))) -> (exists dst_positive_code_signed_multiplicative_nonemptyproduct dst_positive_scale_signed_multiplicative_nonemptyproduct dst_negative_code_signed_multiplicative_nonemptyproduct dst_negative_scale_signed_multiplicative_nonemptyproduct dst_positive_signed_multiplicative_nonemptyproduct dst_negative_signed_multiplicative_nonemptyproduct. (((F) = (((((dst_positive_code_signed_multiplicative_nonemptyproduct) + (dst_positive_scale_signed_multiplicative_nonemptyproduct)) * S ((dst_positive_code_signed_multiplicative_nonemptyproduct) + (dst_positive_scale_signed_multiplicative_nonemptyproduct)) + ((dst_positive_scale_signed_multiplicative_nonemptyproduct) + (dst_positive_scale_signed_multiplicative_nonemptyproduct))) + (((dst_negative_code_signed_multiplicative_nonemptyproduct) + (dst_negative_scale_signed_multiplicative_nonemptyproduct)) * S ((dst_negative_code_signed_multiplicative_nonemptyproduct) + (dst_negative_scale_signed_multiplicative_nonemptyproduct)) + ((dst_negative_scale_signed_multiplicative_nonemptyproduct) + (dst_negative_scale_signed_multiplicative_nonemptyproduct)))) * S ((((dst_positive_code_signed_multiplicative_nonemptyproduct) + (dst_positive_scale_signed_multiplicative_nonemptyproduct)) * S ((dst_positive_code_signed_multiplicative_nonemptyproduct) + (dst_positive_scale_signed_multiplicative_nonemptyproduct)) + ((dst_positive_scale_signed_multiplicative_nonemptyproduct) + (dst_positive_scale_signed_multiplicative_nonemptyproduct))) + (((dst_negative_code_signed_multiplicative_nonemptyproduct) + (dst_negative_scale_signed_multiplicative_nonemptyproduct)) * S ((dst_negative_code_signed_multiplicative_nonemptyproduct) + (dst_negative_scale_signed_multiplicative_nonemptyproduct)) + ((dst_negative_scale_signed_multiplicative_nonemptyproduct) + (dst_negative_scale_signed_multiplicative_nonemptyproduct)))) + ((((dst_negative_code_signed_multiplicative_nonemptyproduct) + (dst_negative_scale_signed_multiplicative_nonemptyproduct)) * S ((dst_negative_code_signed_multiplicative_nonemptyproduct) + (dst_negative_scale_signed_multiplicative_nonemptyproduct)) + ((dst_negative_scale_signed_multiplicative_nonemptyproduct) + (dst_negative_scale_signed_multiplicative_nonemptyproduct))) + (((dst_negative_code_signed_multiplicative_nonemptyproduct) + (dst_negative_scale_signed_multiplicative_nonemptyproduct)) * S ((dst_negative_code_signed_multiplicative_nonemptyproduct) + (dst_negative_scale_signed_multiplicative_nonemptyproduct)) + ((dst_negative_scale_signed_multiplicative_nonemptyproduct) + (dst_negative_scale_signed_multiplicative_nonemptyproduct)))))) /\ (((((exists ff_h_pvs_signed_multiplicative_nonemptyproductpositive. ff_h_pvs_signed_multiplicative_nonemptyproductpositive + S (dst_positive_signed_multiplicative_nonemptyproduct) = S ((S (mp_a_signed_multiplicative_nonempty*mp_b_signed_multiplicative_nonempty)) * dst_positive_scale_signed_multiplicative_nonemptyproduct)) /\ exists ff_q_pvs_signed_multiplicative_nonemptyproductpositive. dst_positive_code_signed_multiplicative_nonemptyproduct = ff_q_pvs_signed_multiplicative_nonemptyproductpositive * S ((S (mp_a_signed_multiplicative_nonempty*mp_b_signed_multiplicative_nonempty)) * dst_positive_scale_signed_multiplicative_nonemptyproduct) + (dst_positive_signed_multiplicative_nonemptyproduct))) /\ (((((exists ff_h_pvs_signed_multiplicative_nonemptyproductnegative. ff_h_pvs_signed_multiplicative_nonemptyproductnegative + S (dst_negative_signed_multiplicative_nonemptyproduct) = S ((S (mp_a_signed_multiplicative_nonempty*mp_b_signed_multiplicative_nonempty)) * dst_negative_scale_signed_multiplicative_nonemptyproduct)) /\ exists ff_q_pvs_signed_multiplicative_nonemptyproductnegative. dst_negative_code_signed_multiplicative_nonemptyproduct = ff_q_pvs_signed_multiplicative_nonemptyproductnegative * S ((S (mp_a_signed_multiplicative_nonempty*mp_b_signed_multiplicative_nonempty)) * dst_negative_scale_signed_multiplicative_nonemptyproduct) + (dst_negative_signed_multiplicative_nonemptyproduct))) /\ (exists ge_balance_positive_signed_multiplicative_nonemptyproductvalue ge_balance_negative_signed_multiplicative_nonemptyproductvalue. (((((mp_z_signed_multiplicative_nonempty) = 2 * (ge_balance_positive_signed_multiplicative_nonemptyproductvalue) /\ (ge_balance_negative_signed_multiplicative_nonemptyproductvalue) = 0) \/ exists ge_signed_half_signed_multiplicative_nonemptyproductvaluedecode. (((mp_z_signed_multiplicative_nonempty) = 2 * ge_signed_half_signed_multiplicative_nonemptyproductvaluedecode + 1 /\ (ge_balance_positive_signed_multiplicative_nonemptyproductvalue) = 0) /\ (ge_balance_negative_signed_multiplicative_nonemptyproductvalue) = S ge_signed_half_signed_multiplicative_nonemptyproductvaluedecode))) /\ ((dst_positive_signed_multiplicative_nonemptyproduct) + ge_balance_negative_signed_multiplicative_nonemptyproductvalue = (dst_negative_signed_multiplicative_nonemptyproduct) + ge_balance_positive_signed_multiplicative_nonemptyproductvalue))))))))) -> (exists sto_ap_signed_multiplicative_nonemptylaw sto_an_signed_multiplicative_nonemptylaw sto_bp_signed_multiplicative_nonemptylaw sto_bn_signed_multiplicative_nonemptylaw sto_cp_signed_multiplicative_nonemptylaw sto_cn_signed_multiplicative_nonemptylaw. (((((mp_x_signed_multiplicative_nonempty) = 2 * (sto_ap_signed_multiplicative_nonemptylaw) /\ (sto_an_signed_multiplicative_nonemptylaw) = 0) \/ exists ge_signed_half_signed_multiplicative_nonemptylawleft. (((mp_x_signed_multiplicative_nonempty) = 2 * ge_signed_half_signed_multiplicative_nonemptylawleft + 1 /\ (sto_ap_signed_multiplicative_nonemptylaw) = 0) /\ (sto_an_signed_multiplicative_nonemptylaw) = S ge_signed_half_signed_multiplicative_nonemptylawleft))) /\ ((((((mp_y_signed_multiplicative_nonempty) = 2 * (sto_bp_signed_multiplicative_nonemptylaw) /\ (sto_bn_signed_multiplicative_nonemptylaw) = 0) \/ exists ge_signed_half_signed_multiplicative_nonemptylawright. (((mp_y_signed_multiplicative_nonempty) = 2 * ge_signed_half_signed_multiplicative_nonemptylawright + 1 /\ (sto_bp_signed_multiplicative_nonemptylaw) = 0) /\ (sto_bn_signed_multiplicative_nonemptylaw) = S ge_signed_half_signed_multiplicative_nonemptylawright))) /\ ((((((mp_z_signed_multiplicative_nonempty) = 2 * (sto_cp_signed_multiplicative_nonemptylaw) /\ (sto_cn_signed_multiplicative_nonemptylaw) = 0) \/ exists ge_signed_half_signed_multiplicative_nonemptylawoutput. (((mp_z_signed_multiplicative_nonempty) = 2 * ge_signed_half_signed_multiplicative_nonemptylawoutput + 1 /\ (sto_cp_signed_multiplicative_nonemptylaw) = 0) /\ (sto_cn_signed_multiplicative_nonemptylaw) = S ge_signed_half_signed_multiplicative_nonemptylawoutput))) /\ ((sto_ap_signed_multiplicative_nonemptylaw * sto_bp_signed_multiplicative_nonemptylaw + sto_an_signed_multiplicative_nonemptylaw * sto_bn_signed_multiplicative_nonemptylaw) + sto_cn_signed_multiplicative_nonemptylaw = (sto_ap_signed_multiplicative_nonemptylaw * sto_bn_signed_multiplicative_nonemptylaw + sto_an_signed_multiplicative_nonemptylaw * sto_bp_signed_multiplicative_nonemptylaw) + sto_cp_signed_multiplicative_nonemptylaw)))))))))))))) -> (~(N=0))