signed_multiplicative_restrict

Exact expanded first-order arithmetic statement

forall N K F. (((~((N)=0)) /\ (((exists dst_positive_code_restrict_sourcetable dst_positive_scale_restrict_sourcetable dst_negative_code_restrict_sourcetable dst_negative_scale_restrict_sourcetable. (((F) = (((((dst_positive_code_restrict_sourcetable) + (dst_positive_scale_restrict_sourcetable)) * S ((dst_positive_code_restrict_sourcetable) + (dst_positive_scale_restrict_sourcetable)) + ((dst_positive_scale_restrict_sourcetable) + (dst_positive_scale_restrict_sourcetable))) + (((dst_negative_code_restrict_sourcetable) + (dst_negative_scale_restrict_sourcetable)) * S ((dst_negative_code_restrict_sourcetable) + (dst_negative_scale_restrict_sourcetable)) + ((dst_negative_scale_restrict_sourcetable) + (dst_negative_scale_restrict_sourcetable)))) * S ((((dst_positive_code_restrict_sourcetable) + (dst_positive_scale_restrict_sourcetable)) * S ((dst_positive_code_restrict_sourcetable) + (dst_positive_scale_restrict_sourcetable)) + ((dst_positive_scale_restrict_sourcetable) + (dst_positive_scale_restrict_sourcetable))) + (((dst_negative_code_restrict_sourcetable) + (dst_negative_scale_restrict_sourcetable)) * S ((dst_negative_code_restrict_sourcetable) + (dst_negative_scale_restrict_sourcetable)) + ((dst_negative_scale_restrict_sourcetable) + (dst_negative_scale_restrict_sourcetable)))) + ((((dst_negative_code_restrict_sourcetable) + (dst_negative_scale_restrict_sourcetable)) * S ((dst_negative_code_restrict_sourcetable) + (dst_negative_scale_restrict_sourcetable)) + ((dst_negative_scale_restrict_sourcetable) + (dst_negative_scale_restrict_sourcetable))) + (((dst_negative_code_restrict_sourcetable) + (dst_negative_scale_restrict_sourcetable)) * S ((dst_negative_code_restrict_sourcetable) + (dst_negative_scale_restrict_sourcetable)) + ((dst_negative_scale_restrict_sourcetable) + (dst_negative_scale_restrict_sourcetable)))))) /\ (forall dst_index_restrict_sourcetable. (exists pvs_le_gap_restrict_sourcetabledomain. pvs_le_gap_restrict_sourcetabledomain + (dst_index_restrict_sourcetable) = (N)) -> exists dst_positive_restrict_sourcetable dst_negative_restrict_sourcetable dst_value_restrict_sourcetable. ((((exists ff_h_pvs_restrict_sourcetableentrypositive. ff_h_pvs_restrict_sourcetableentrypositive + S (dst_positive_restrict_sourcetable) = S ((S (dst_index_restrict_sourcetable)) * dst_positive_scale_restrict_sourcetable)) /\ exists ff_q_pvs_restrict_sourcetableentrypositive. dst_positive_code_restrict_sourcetable = ff_q_pvs_restrict_sourcetableentrypositive * S ((S (dst_index_restrict_sourcetable)) * dst_positive_scale_restrict_sourcetable) + (dst_positive_restrict_sourcetable))) /\ (((((exists ff_h_pvs_restrict_sourcetableentrynegative. ff_h_pvs_restrict_sourcetableentrynegative + S (dst_negative_restrict_sourcetable) = S ((S (dst_index_restrict_sourcetable)) * dst_negative_scale_restrict_sourcetable)) /\ exists ff_q_pvs_restrict_sourcetableentrynegative. dst_negative_code_restrict_sourcetable = ff_q_pvs_restrict_sourcetableentrynegative * S ((S (dst_index_restrict_sourcetable)) * dst_negative_scale_restrict_sourcetable) + (dst_negative_restrict_sourcetable))) /\ (exists ge_balance_positive_restrict_sourcetableentryvalue ge_balance_negative_restrict_sourcetableentryvalue. (((((dst_value_restrict_sourcetable) = 2 * (ge_balance_positive_restrict_sourcetableentryvalue) /\ (ge_balance_negative_restrict_sourcetableentryvalue) = 0) \/ exists ge_signed_half_restrict_sourcetableentryvaluedecode. (((dst_value_restrict_sourcetable) = 2 * ge_signed_half_restrict_sourcetableentryvaluedecode + 1 /\ (ge_balance_positive_restrict_sourcetableentryvalue) = 0) /\ (ge_balance_negative_restrict_sourcetableentryvalue) = S ge_signed_half_restrict_sourcetableentryvaluedecode))) /\ ((dst_positive_restrict_sourcetable) + ge_balance_negative_restrict_sourcetableentryvalue = (dst_negative_restrict_sourcetable) + ge_balance_positive_restrict_sourcetableentryvalue))))))))) /\ (((exists dst_positive_code_restrict_sourceone dst_positive_scale_restrict_sourceone dst_negative_code_restrict_sourceone dst_negative_scale_restrict_sourceone dst_positive_restrict_sourceone dst_negative_restrict_sourceone. (((F) = (((((dst_positive_code_restrict_sourceone) + (dst_positive_scale_restrict_sourceone)) * S ((dst_positive_code_restrict_sourceone) + (dst_positive_scale_restrict_sourceone)) + ((dst_positive_scale_restrict_sourceone) + (dst_positive_scale_restrict_sourceone))) + (((dst_negative_code_restrict_sourceone) + (dst_negative_scale_restrict_sourceone)) * S ((dst_negative_code_restrict_sourceone) + (dst_negative_scale_restrict_sourceone)) + ((dst_negative_scale_restrict_sourceone) + (dst_negative_scale_restrict_sourceone)))) * S ((((dst_positive_code_restrict_sourceone) + (dst_positive_scale_restrict_sourceone)) * S ((dst_positive_code_restrict_sourceone) + (dst_positive_scale_restrict_sourceone)) + ((dst_positive_scale_restrict_sourceone) + (dst_positive_scale_restrict_sourceone))) + (((dst_negative_code_restrict_sourceone) + (dst_negative_scale_restrict_sourceone)) * S ((dst_negative_code_restrict_sourceone) + (dst_negative_scale_restrict_sourceone)) + ((dst_negative_scale_restrict_sourceone) + (dst_negative_scale_restrict_sourceone)))) + ((((dst_negative_code_restrict_sourceone) + (dst_negative_scale_restrict_sourceone)) * S ((dst_negative_code_restrict_sourceone) + (dst_negative_scale_restrict_sourceone)) + ((dst_negative_scale_restrict_sourceone) + (dst_negative_scale_restrict_sourceone))) + (((dst_negative_code_restrict_sourceone) + (dst_negative_scale_restrict_sourceone)) * S ((dst_negative_code_restrict_sourceone) + (dst_negative_scale_restrict_sourceone)) + ((dst_negative_scale_restrict_sourceone) + (dst_negative_scale_restrict_sourceone)))))) /\ (((((exists ff_h_pvs_restrict_sourceonepositive. ff_h_pvs_restrict_sourceonepositive + S (dst_positive_restrict_sourceone) = S ((S (1)) * dst_positive_scale_restrict_sourceone)) /\ exists ff_q_pvs_restrict_sourceonepositive. dst_positive_code_restrict_sourceone = ff_q_pvs_restrict_sourceonepositive * S ((S (1)) * dst_positive_scale_restrict_sourceone) + (dst_positive_restrict_sourceone))) /\ (((((exists ff_h_pvs_restrict_sourceonenegative. ff_h_pvs_restrict_sourceonenegative + S (dst_negative_restrict_sourceone) = S ((S (1)) * dst_negative_scale_restrict_sourceone)) /\ exists ff_q_pvs_restrict_sourceonenegative. dst_negative_code_restrict_sourceone = ff_q_pvs_restrict_sourceonenegative * S ((S (1)) * dst_negative_scale_restrict_sourceone) + (dst_negative_restrict_sourceone))) /\ (exists ge_balance_positive_restrict_sourceonevalue ge_balance_negative_restrict_sourceonevalue. (((((2) = 2 * (ge_balance_positive_restrict_sourceonevalue) /\ (ge_balance_negative_restrict_sourceonevalue) = 0) \/ exists ge_signed_half_restrict_sourceonevaluedecode. (((2) = 2 * ge_signed_half_restrict_sourceonevaluedecode + 1 /\ (ge_balance_positive_restrict_sourceonevalue) = 0) /\ (ge_balance_negative_restrict_sourceonevalue) = S ge_signed_half_restrict_sourceonevaluedecode))) /\ ((dst_positive_restrict_sourceone) + ge_balance_negative_restrict_sourceonevalue = (dst_negative_restrict_sourceone) + ge_balance_positive_restrict_sourceonevalue))))))))) /\ (forall mp_a_restrict_source mp_b_restrict_source mp_x_restrict_source mp_y_restrict_source mp_z_restrict_source. ~(mp_a_restrict_source=0) -> ~(mp_b_restrict_source=0) -> (exists pvs_le_gap_restrict_sourcebound. pvs_le_gap_restrict_sourcebound + (mp_a_restrict_source*mp_b_restrict_source) = (N)) -> (forall frp_divisor_restrict_sourcecoprime. (exists frp_left_factor_restrict_sourcecoprime. mp_a_restrict_source = frp_divisor_restrict_sourcecoprime * frp_left_factor_restrict_sourcecoprime) -> (exists frp_right_factor_restrict_sourcecoprime. mp_b_restrict_source = frp_divisor_restrict_sourcecoprime * frp_right_factor_restrict_sourcecoprime) -> frp_divisor_restrict_sourcecoprime = 1) -> (exists dst_positive_code_restrict_sourcefirst dst_positive_scale_restrict_sourcefirst dst_negative_code_restrict_sourcefirst dst_negative_scale_restrict_sourcefirst dst_positive_restrict_sourcefirst dst_negative_restrict_sourcefirst. (((F) = (((((dst_positive_code_restrict_sourcefirst) + (dst_positive_scale_restrict_sourcefirst)) * S ((dst_positive_code_restrict_sourcefirst) + (dst_positive_scale_restrict_sourcefirst)) + ((dst_positive_scale_restrict_sourcefirst) + (dst_positive_scale_restrict_sourcefirst))) + (((dst_negative_code_restrict_sourcefirst) + (dst_negative_scale_restrict_sourcefirst)) * S ((dst_negative_code_restrict_sourcefirst) + (dst_negative_scale_restrict_sourcefirst)) + ((dst_negative_scale_restrict_sourcefirst) + (dst_negative_scale_restrict_sourcefirst)))) * S ((((dst_positive_code_restrict_sourcefirst) + (dst_positive_scale_restrict_sourcefirst)) * S ((dst_positive_code_restrict_sourcefirst) + (dst_positive_scale_restrict_sourcefirst)) + ((dst_positive_scale_restrict_sourcefirst) + (dst_positive_scale_restrict_sourcefirst))) + (((dst_negative_code_restrict_sourcefirst) + (dst_negative_scale_restrict_sourcefirst)) * S ((dst_negative_code_restrict_sourcefirst) + (dst_negative_scale_restrict_sourcefirst)) + ((dst_negative_scale_restrict_sourcefirst) + (dst_negative_scale_restrict_sourcefirst)))) + ((((dst_negative_code_restrict_sourcefirst) + (dst_negative_scale_restrict_sourcefirst)) * S ((dst_negative_code_restrict_sourcefirst) + (dst_negative_scale_restrict_sourcefirst)) + ((dst_negative_scale_restrict_sourcefirst) + (dst_negative_scale_restrict_sourcefirst))) + (((dst_negative_code_restrict_sourcefirst) + (dst_negative_scale_restrict_sourcefirst)) * S ((dst_negative_code_restrict_sourcefirst) + (dst_negative_scale_restrict_sourcefirst)) + ((dst_negative_scale_restrict_sourcefirst) + (dst_negative_scale_restrict_sourcefirst)))))) /\ (((((exists ff_h_pvs_restrict_sourcefirstpositive. ff_h_pvs_restrict_sourcefirstpositive + S (dst_positive_restrict_sourcefirst) = S ((S (mp_a_restrict_source)) * dst_positive_scale_restrict_sourcefirst)) /\ exists ff_q_pvs_restrict_sourcefirstpositive. dst_positive_code_restrict_sourcefirst = ff_q_pvs_restrict_sourcefirstpositive * S ((S (mp_a_restrict_source)) * dst_positive_scale_restrict_sourcefirst) + (dst_positive_restrict_sourcefirst))) /\ (((((exists ff_h_pvs_restrict_sourcefirstnegative. ff_h_pvs_restrict_sourcefirstnegative + S (dst_negative_restrict_sourcefirst) = S ((S (mp_a_restrict_source)) * dst_negative_scale_restrict_sourcefirst)) /\ exists ff_q_pvs_restrict_sourcefirstnegative. dst_negative_code_restrict_sourcefirst = ff_q_pvs_restrict_sourcefirstnegative * S ((S (mp_a_restrict_source)) * dst_negative_scale_restrict_sourcefirst) + (dst_negative_restrict_sourcefirst))) /\ (exists ge_balance_positive_restrict_sourcefirstvalue ge_balance_negative_restrict_sourcefirstvalue. (((((mp_x_restrict_source) = 2 * (ge_balance_positive_restrict_sourcefirstvalue) /\ (ge_balance_negative_restrict_sourcefirstvalue) = 0) \/ exists ge_signed_half_restrict_sourcefirstvaluedecode. (((mp_x_restrict_source) = 2 * ge_signed_half_restrict_sourcefirstvaluedecode + 1 /\ (ge_balance_positive_restrict_sourcefirstvalue) = 0) /\ (ge_balance_negative_restrict_sourcefirstvalue) = S ge_signed_half_restrict_sourcefirstvaluedecode))) /\ ((dst_positive_restrict_sourcefirst) + ge_balance_negative_restrict_sourcefirstvalue = (dst_negative_restrict_sourcefirst) + ge_balance_positive_restrict_sourcefirstvalue))))))))) -> (exists dst_positive_code_restrict_sourcesecond dst_positive_scale_restrict_sourcesecond dst_negative_code_restrict_sourcesecond dst_negative_scale_restrict_sourcesecond dst_positive_restrict_sourcesecond dst_negative_restrict_sourcesecond. (((F) = (((((dst_positive_code_restrict_sourcesecond) + (dst_positive_scale_restrict_sourcesecond)) * S ((dst_positive_code_restrict_sourcesecond) + (dst_positive_scale_restrict_sourcesecond)) + ((dst_positive_scale_restrict_sourcesecond) + (dst_positive_scale_restrict_sourcesecond))) + (((dst_negative_code_restrict_sourcesecond) + (dst_negative_scale_restrict_sourcesecond)) * S ((dst_negative_code_restrict_sourcesecond) + (dst_negative_scale_restrict_sourcesecond)) + ((dst_negative_scale_restrict_sourcesecond) + (dst_negative_scale_restrict_sourcesecond)))) * S ((((dst_positive_code_restrict_sourcesecond) + (dst_positive_scale_restrict_sourcesecond)) * S ((dst_positive_code_restrict_sourcesecond) + (dst_positive_scale_restrict_sourcesecond)) + ((dst_positive_scale_restrict_sourcesecond) + (dst_positive_scale_restrict_sourcesecond))) + (((dst_negative_code_restrict_sourcesecond) + (dst_negative_scale_restrict_sourcesecond)) * S ((dst_negative_code_restrict_sourcesecond) + (dst_negative_scale_restrict_sourcesecond)) + ((dst_negative_scale_restrict_sourcesecond) + (dst_negative_scale_restrict_sourcesecond)))) + ((((dst_negative_code_restrict_sourcesecond) + (dst_negative_scale_restrict_sourcesecond)) * S ((dst_negative_code_restrict_sourcesecond) + (dst_negative_scale_restrict_sourcesecond)) + ((dst_negative_scale_restrict_sourcesecond) + (dst_negative_scale_restrict_sourcesecond))) + (((dst_negative_code_restrict_sourcesecond) + (dst_negative_scale_restrict_sourcesecond)) * S ((dst_negative_code_restrict_sourcesecond) + (dst_negative_scale_restrict_sourcesecond)) + ((dst_negative_scale_restrict_sourcesecond) + (dst_negative_scale_restrict_sourcesecond)))))) /\ (((((exists ff_h_pvs_restrict_sourcesecondpositive. ff_h_pvs_restrict_sourcesecondpositive + S (dst_positive_restrict_sourcesecond) = S ((S (mp_b_restrict_source)) * dst_positive_scale_restrict_sourcesecond)) /\ exists ff_q_pvs_restrict_sourcesecondpositive. dst_positive_code_restrict_sourcesecond = ff_q_pvs_restrict_sourcesecondpositive * S ((S (mp_b_restrict_source)) * dst_positive_scale_restrict_sourcesecond) + (dst_positive_restrict_sourcesecond))) /\ (((((exists ff_h_pvs_restrict_sourcesecondnegative. ff_h_pvs_restrict_sourcesecondnegative + S (dst_negative_restrict_sourcesecond) = S ((S (mp_b_restrict_source)) * dst_negative_scale_restrict_sourcesecond)) /\ exists ff_q_pvs_restrict_sourcesecondnegative. dst_negative_code_restrict_sourcesecond = ff_q_pvs_restrict_sourcesecondnegative * S ((S (mp_b_restrict_source)) * dst_negative_scale_restrict_sourcesecond) + (dst_negative_restrict_sourcesecond))) /\ (exists ge_balance_positive_restrict_sourcesecondvalue ge_balance_negative_restrict_sourcesecondvalue. (((((mp_y_restrict_source) = 2 * (ge_balance_positive_restrict_sourcesecondvalue) /\ (ge_balance_negative_restrict_sourcesecondvalue) = 0) \/ exists ge_signed_half_restrict_sourcesecondvaluedecode. (((mp_y_restrict_source) = 2 * ge_signed_half_restrict_sourcesecondvaluedecode + 1 /\ (ge_balance_positive_restrict_sourcesecondvalue) = 0) /\ (ge_balance_negative_restrict_sourcesecondvalue) = S ge_signed_half_restrict_sourcesecondvaluedecode))) /\ ((dst_positive_restrict_sourcesecond) + ge_balance_negative_restrict_sourcesecondvalue = (dst_negative_restrict_sourcesecond) + ge_balance_positive_restrict_sourcesecondvalue))))))))) -> (exists dst_positive_code_restrict_sourceproduct dst_positive_scale_restrict_sourceproduct dst_negative_code_restrict_sourceproduct dst_negative_scale_restrict_sourceproduct dst_positive_restrict_sourceproduct dst_negative_restrict_sourceproduct. (((F) = (((((dst_positive_code_restrict_sourceproduct) + (dst_positive_scale_restrict_sourceproduct)) * S ((dst_positive_code_restrict_sourceproduct) + (dst_positive_scale_restrict_sourceproduct)) + ((dst_positive_scale_restrict_sourceproduct) + (dst_positive_scale_restrict_sourceproduct))) + (((dst_negative_code_restrict_sourceproduct) + (dst_negative_scale_restrict_sourceproduct)) * S ((dst_negative_code_restrict_sourceproduct) + (dst_negative_scale_restrict_sourceproduct)) + ((dst_negative_scale_restrict_sourceproduct) + (dst_negative_scale_restrict_sourceproduct)))) * S ((((dst_positive_code_restrict_sourceproduct) + (dst_positive_scale_restrict_sourceproduct)) * S ((dst_positive_code_restrict_sourceproduct) + (dst_positive_scale_restrict_sourceproduct)) + ((dst_positive_scale_restrict_sourceproduct) + (dst_positive_scale_restrict_sourceproduct))) + (((dst_negative_code_restrict_sourceproduct) + (dst_negative_scale_restrict_sourceproduct)) * S ((dst_negative_code_restrict_sourceproduct) + (dst_negative_scale_restrict_sourceproduct)) + ((dst_negative_scale_restrict_sourceproduct) + (dst_negative_scale_restrict_sourceproduct)))) + ((((dst_negative_code_restrict_sourceproduct) + (dst_negative_scale_restrict_sourceproduct)) * S ((dst_negative_code_restrict_sourceproduct) + (dst_negative_scale_restrict_sourceproduct)) + ((dst_negative_scale_restrict_sourceproduct) + (dst_negative_scale_restrict_sourceproduct))) + (((dst_negative_code_restrict_sourceproduct) + (dst_negative_scale_restrict_sourceproduct)) * S ((dst_negative_code_restrict_sourceproduct) + (dst_negative_scale_restrict_sourceproduct)) + ((dst_negative_scale_restrict_sourceproduct) + (dst_negative_scale_restrict_sourceproduct)))))) /\ (((((exists ff_h_pvs_restrict_sourceproductpositive. ff_h_pvs_restrict_sourceproductpositive + S (dst_positive_restrict_sourceproduct) = S ((S (mp_a_restrict_source*mp_b_restrict_source)) * dst_positive_scale_restrict_sourceproduct)) /\ exists ff_q_pvs_restrict_sourceproductpositive. dst_positive_code_restrict_sourceproduct = ff_q_pvs_restrict_sourceproductpositive * S ((S (mp_a_restrict_source*mp_b_restrict_source)) * dst_positive_scale_restrict_sourceproduct) + (dst_positive_restrict_sourceproduct))) /\ (((((exists ff_h_pvs_restrict_sourceproductnegative. ff_h_pvs_restrict_sourceproductnegative + S (dst_negative_restrict_sourceproduct) = S ((S (mp_a_restrict_source*mp_b_restrict_source)) * dst_negative_scale_restrict_sourceproduct)) /\ exists ff_q_pvs_restrict_sourceproductnegative. dst_negative_code_restrict_sourceproduct = ff_q_pvs_restrict_sourceproductnegative * S ((S (mp_a_restrict_source*mp_b_restrict_source)) * dst_negative_scale_restrict_sourceproduct) + (dst_negative_restrict_sourceproduct))) /\ (exists ge_balance_positive_restrict_sourceproductvalue ge_balance_negative_restrict_sourceproductvalue. (((((mp_z_restrict_source) = 2 * (ge_balance_positive_restrict_sourceproductvalue) /\ (ge_balance_negative_restrict_sourceproductvalue) = 0) \/ exists ge_signed_half_restrict_sourceproductvaluedecode. (((mp_z_restrict_source) = 2 * ge_signed_half_restrict_sourceproductvaluedecode + 1 /\ (ge_balance_positive_restrict_sourceproductvalue) = 0) /\ (ge_balance_negative_restrict_sourceproductvalue) = S ge_signed_half_restrict_sourceproductvaluedecode))) /\ ((dst_positive_restrict_sourceproduct) + ge_balance_negative_restrict_sourceproductvalue = (dst_negative_restrict_sourceproduct) + ge_balance_positive_restrict_sourceproductvalue))))))))) -> (exists sto_ap_restrict_sourcelaw sto_an_restrict_sourcelaw sto_bp_restrict_sourcelaw sto_bn_restrict_sourcelaw sto_cp_restrict_sourcelaw sto_cn_restrict_sourcelaw. (((((mp_x_restrict_source) = 2 * (sto_ap_restrict_sourcelaw) /\ (sto_an_restrict_sourcelaw) = 0) \/ exists ge_signed_half_restrict_sourcelawleft. (((mp_x_restrict_source) = 2 * ge_signed_half_restrict_sourcelawleft + 1 /\ (sto_ap_restrict_sourcelaw) = 0) /\ (sto_an_restrict_sourcelaw) = S ge_signed_half_restrict_sourcelawleft))) /\ ((((((mp_y_restrict_source) = 2 * (sto_bp_restrict_sourcelaw) /\ (sto_bn_restrict_sourcelaw) = 0) \/ exists ge_signed_half_restrict_sourcelawright. (((mp_y_restrict_source) = 2 * ge_signed_half_restrict_sourcelawright + 1 /\ (sto_bp_restrict_sourcelaw) = 0) /\ (sto_bn_restrict_sourcelaw) = S ge_signed_half_restrict_sourcelawright))) /\ ((((((mp_z_restrict_source) = 2 * (sto_cp_restrict_sourcelaw) /\ (sto_cn_restrict_sourcelaw) = 0) \/ exists ge_signed_half_restrict_sourcelawoutput. (((mp_z_restrict_source) = 2 * ge_signed_half_restrict_sourcelawoutput + 1 /\ (sto_cp_restrict_sourcelaw) = 0) /\ (sto_cn_restrict_sourcelaw) = S ge_signed_half_restrict_sourcelawoutput))) /\ ((sto_ap_restrict_sourcelaw * sto_bp_restrict_sourcelaw + sto_an_restrict_sourcelaw * sto_bn_restrict_sourcelaw) + sto_cn_restrict_sourcelaw = (sto_ap_restrict_sourcelaw * sto_bn_restrict_sourcelaw + sto_an_restrict_sourcelaw * sto_bp_restrict_sourcelaw) + sto_cp_restrict_sourcelaw)))))))))))))) -> ~(K=0) -> (exists pvs_le_gap_restrict_bound. pvs_le_gap_restrict_bound + (K) = (N)) -> (((~((K)=0)) /\ (((exists dst_positive_code_restrict_targettable dst_positive_scale_restrict_targettable dst_negative_code_restrict_targettable dst_negative_scale_restrict_targettable. (((F) = (((((dst_positive_code_restrict_targettable) + (dst_positive_scale_restrict_targettable)) * S ((dst_positive_code_restrict_targettable) + (dst_positive_scale_restrict_targettable)) + ((dst_positive_scale_restrict_targettable) + (dst_positive_scale_restrict_targettable))) + (((dst_negative_code_restrict_targettable) + (dst_negative_scale_restrict_targettable)) * S ((dst_negative_code_restrict_targettable) + (dst_negative_scale_restrict_targettable)) + ((dst_negative_scale_restrict_targettable) + (dst_negative_scale_restrict_targettable)))) * S ((((dst_positive_code_restrict_targettable) + (dst_positive_scale_restrict_targettable)) * S ((dst_positive_code_restrict_targettable) + (dst_positive_scale_restrict_targettable)) + ((dst_positive_scale_restrict_targettable) + (dst_positive_scale_restrict_targettable))) + (((dst_negative_code_restrict_targettable) + (dst_negative_scale_restrict_targettable)) * S ((dst_negative_code_restrict_targettable) + (dst_negative_scale_restrict_targettable)) + ((dst_negative_scale_restrict_targettable) + (dst_negative_scale_restrict_targettable)))) + ((((dst_negative_code_restrict_targettable) + (dst_negative_scale_restrict_targettable)) * S ((dst_negative_code_restrict_targettable) + (dst_negative_scale_restrict_targettable)) + ((dst_negative_scale_restrict_targettable) + (dst_negative_scale_restrict_targettable))) + (((dst_negative_code_restrict_targettable) + (dst_negative_scale_restrict_targettable)) * S ((dst_negative_code_restrict_targettable) + (dst_negative_scale_restrict_targettable)) + ((dst_negative_scale_restrict_targettable) + (dst_negative_scale_restrict_targettable)))))) /\ (forall dst_index_restrict_targettable. (exists pvs_le_gap_restrict_targettabledomain. pvs_le_gap_restrict_targettabledomain + (dst_index_restrict_targettable) = (K)) -> exists dst_positive_restrict_targettable dst_negative_restrict_targettable dst_value_restrict_targettable. ((((exists ff_h_pvs_restrict_targettableentrypositive. ff_h_pvs_restrict_targettableentrypositive + S (dst_positive_restrict_targettable) = S ((S (dst_index_restrict_targettable)) * dst_positive_scale_restrict_targettable)) /\ exists ff_q_pvs_restrict_targettableentrypositive. dst_positive_code_restrict_targettable = ff_q_pvs_restrict_targettableentrypositive * S ((S (dst_index_restrict_targettable)) * dst_positive_scale_restrict_targettable) + (dst_positive_restrict_targettable))) /\ (((((exists ff_h_pvs_restrict_targettableentrynegative. ff_h_pvs_restrict_targettableentrynegative + S (dst_negative_restrict_targettable) = S ((S (dst_index_restrict_targettable)) * dst_negative_scale_restrict_targettable)) /\ exists ff_q_pvs_restrict_targettableentrynegative. dst_negative_code_restrict_targettable = ff_q_pvs_restrict_targettableentrynegative * S ((S (dst_index_restrict_targettable)) * dst_negative_scale_restrict_targettable) + (dst_negative_restrict_targettable))) /\ (exists ge_balance_positive_restrict_targettableentryvalue ge_balance_negative_restrict_targettableentryvalue. (((((dst_value_restrict_targettable) = 2 * (ge_balance_positive_restrict_targettableentryvalue) /\ (ge_balance_negative_restrict_targettableentryvalue) = 0) \/ exists ge_signed_half_restrict_targettableentryvaluedecode. (((dst_value_restrict_targettable) = 2 * ge_signed_half_restrict_targettableentryvaluedecode + 1 /\ (ge_balance_positive_restrict_targettableentryvalue) = 0) /\ (ge_balance_negative_restrict_targettableentryvalue) = S ge_signed_half_restrict_targettableentryvaluedecode))) /\ ((dst_positive_restrict_targettable) + ge_balance_negative_restrict_targettableentryvalue = (dst_negative_restrict_targettable) + ge_balance_positive_restrict_targettableentryvalue))))))))) /\ (((exists dst_positive_code_restrict_targetone dst_positive_scale_restrict_targetone dst_negative_code_restrict_targetone dst_negative_scale_restrict_targetone dst_positive_restrict_targetone dst_negative_restrict_targetone. (((F) = (((((dst_positive_code_restrict_targetone) + (dst_positive_scale_restrict_targetone)) * S ((dst_positive_code_restrict_targetone) + (dst_positive_scale_restrict_targetone)) + ((dst_positive_scale_restrict_targetone) + (dst_positive_scale_restrict_targetone))) + (((dst_negative_code_restrict_targetone) + (dst_negative_scale_restrict_targetone)) * S ((dst_negative_code_restrict_targetone) + (dst_negative_scale_restrict_targetone)) + ((dst_negative_scale_restrict_targetone) + (dst_negative_scale_restrict_targetone)))) * S ((((dst_positive_code_restrict_targetone) + (dst_positive_scale_restrict_targetone)) * S ((dst_positive_code_restrict_targetone) + (dst_positive_scale_restrict_targetone)) + ((dst_positive_scale_restrict_targetone) + (dst_positive_scale_restrict_targetone))) + (((dst_negative_code_restrict_targetone) + (dst_negative_scale_restrict_targetone)) * S ((dst_negative_code_restrict_targetone) + (dst_negative_scale_restrict_targetone)) + ((dst_negative_scale_restrict_targetone) + (dst_negative_scale_restrict_targetone)))) + ((((dst_negative_code_restrict_targetone) + (dst_negative_scale_restrict_targetone)) * S ((dst_negative_code_restrict_targetone) + (dst_negative_scale_restrict_targetone)) + ((dst_negative_scale_restrict_targetone) + (dst_negative_scale_restrict_targetone))) + (((dst_negative_code_restrict_targetone) + (dst_negative_scale_restrict_targetone)) * S ((dst_negative_code_restrict_targetone) + (dst_negative_scale_restrict_targetone)) + ((dst_negative_scale_restrict_targetone) + (dst_negative_scale_restrict_targetone)))))) /\ (((((exists ff_h_pvs_restrict_targetonepositive. ff_h_pvs_restrict_targetonepositive + S (dst_positive_restrict_targetone) = S ((S (1)) * dst_positive_scale_restrict_targetone)) /\ exists ff_q_pvs_restrict_targetonepositive. dst_positive_code_restrict_targetone = ff_q_pvs_restrict_targetonepositive * S ((S (1)) * dst_positive_scale_restrict_targetone) + (dst_positive_restrict_targetone))) /\ (((((exists ff_h_pvs_restrict_targetonenegative. ff_h_pvs_restrict_targetonenegative + S (dst_negative_restrict_targetone) = S ((S (1)) * dst_negative_scale_restrict_targetone)) /\ exists ff_q_pvs_restrict_targetonenegative. dst_negative_code_restrict_targetone = ff_q_pvs_restrict_targetonenegative * S ((S (1)) * dst_negative_scale_restrict_targetone) + (dst_negative_restrict_targetone))) /\ (exists ge_balance_positive_restrict_targetonevalue ge_balance_negative_restrict_targetonevalue. (((((2) = 2 * (ge_balance_positive_restrict_targetonevalue) /\ (ge_balance_negative_restrict_targetonevalue) = 0) \/ exists ge_signed_half_restrict_targetonevaluedecode. (((2) = 2 * ge_signed_half_restrict_targetonevaluedecode + 1 /\ (ge_balance_positive_restrict_targetonevalue) = 0) /\ (ge_balance_negative_restrict_targetonevalue) = S ge_signed_half_restrict_targetonevaluedecode))) /\ ((dst_positive_restrict_targetone) + ge_balance_negative_restrict_targetonevalue = (dst_negative_restrict_targetone) + ge_balance_positive_restrict_targetonevalue))))))))) /\ (forall mp_a_restrict_target mp_b_restrict_target mp_x_restrict_target mp_y_restrict_target mp_z_restrict_target. ~(mp_a_restrict_target=0) -> ~(mp_b_restrict_target=0) -> (exists pvs_le_gap_restrict_targetbound. pvs_le_gap_restrict_targetbound + (mp_a_restrict_target*mp_b_restrict_target) = (K)) -> (forall frp_divisor_restrict_targetcoprime. (exists frp_left_factor_restrict_targetcoprime. mp_a_restrict_target = frp_divisor_restrict_targetcoprime * frp_left_factor_restrict_targetcoprime) -> (exists frp_right_factor_restrict_targetcoprime. mp_b_restrict_target = frp_divisor_restrict_targetcoprime * frp_right_factor_restrict_targetcoprime) -> frp_divisor_restrict_targetcoprime = 1) -> (exists dst_positive_code_restrict_targetfirst dst_positive_scale_restrict_targetfirst dst_negative_code_restrict_targetfirst dst_negative_scale_restrict_targetfirst dst_positive_restrict_targetfirst dst_negative_restrict_targetfirst. (((F) = (((((dst_positive_code_restrict_targetfirst) + (dst_positive_scale_restrict_targetfirst)) * S ((dst_positive_code_restrict_targetfirst) + (dst_positive_scale_restrict_targetfirst)) + ((dst_positive_scale_restrict_targetfirst) + (dst_positive_scale_restrict_targetfirst))) + (((dst_negative_code_restrict_targetfirst) + (dst_negative_scale_restrict_targetfirst)) * S ((dst_negative_code_restrict_targetfirst) + (dst_negative_scale_restrict_targetfirst)) + ((dst_negative_scale_restrict_targetfirst) + (dst_negative_scale_restrict_targetfirst)))) * S ((((dst_positive_code_restrict_targetfirst) + (dst_positive_scale_restrict_targetfirst)) * S ((dst_positive_code_restrict_targetfirst) + (dst_positive_scale_restrict_targetfirst)) + ((dst_positive_scale_restrict_targetfirst) + (dst_positive_scale_restrict_targetfirst))) + (((dst_negative_code_restrict_targetfirst) + (dst_negative_scale_restrict_targetfirst)) * S ((dst_negative_code_restrict_targetfirst) + (dst_negative_scale_restrict_targetfirst)) + ((dst_negative_scale_restrict_targetfirst) + (dst_negative_scale_restrict_targetfirst)))) + ((((dst_negative_code_restrict_targetfirst) + (dst_negative_scale_restrict_targetfirst)) * S ((dst_negative_code_restrict_targetfirst) + (dst_negative_scale_restrict_targetfirst)) + ((dst_negative_scale_restrict_targetfirst) + (dst_negative_scale_restrict_targetfirst))) + (((dst_negative_code_restrict_targetfirst) + (dst_negative_scale_restrict_targetfirst)) * S ((dst_negative_code_restrict_targetfirst) + (dst_negative_scale_restrict_targetfirst)) + ((dst_negative_scale_restrict_targetfirst) + (dst_negative_scale_restrict_targetfirst)))))) /\ (((((exists ff_h_pvs_restrict_targetfirstpositive. ff_h_pvs_restrict_targetfirstpositive + S (dst_positive_restrict_targetfirst) = S ((S (mp_a_restrict_target)) * dst_positive_scale_restrict_targetfirst)) /\ exists ff_q_pvs_restrict_targetfirstpositive. dst_positive_code_restrict_targetfirst = ff_q_pvs_restrict_targetfirstpositive * S ((S (mp_a_restrict_target)) * dst_positive_scale_restrict_targetfirst) + (dst_positive_restrict_targetfirst))) /\ (((((exists ff_h_pvs_restrict_targetfirstnegative. ff_h_pvs_restrict_targetfirstnegative + S (dst_negative_restrict_targetfirst) = S ((S (mp_a_restrict_target)) * dst_negative_scale_restrict_targetfirst)) /\ exists ff_q_pvs_restrict_targetfirstnegative. dst_negative_code_restrict_targetfirst = ff_q_pvs_restrict_targetfirstnegative * S ((S (mp_a_restrict_target)) * dst_negative_scale_restrict_targetfirst) + (dst_negative_restrict_targetfirst))) /\ (exists ge_balance_positive_restrict_targetfirstvalue ge_balance_negative_restrict_targetfirstvalue. (((((mp_x_restrict_target) = 2 * (ge_balance_positive_restrict_targetfirstvalue) /\ (ge_balance_negative_restrict_targetfirstvalue) = 0) \/ exists ge_signed_half_restrict_targetfirstvaluedecode. (((mp_x_restrict_target) = 2 * ge_signed_half_restrict_targetfirstvaluedecode + 1 /\ (ge_balance_positive_restrict_targetfirstvalue) = 0) /\ (ge_balance_negative_restrict_targetfirstvalue) = S ge_signed_half_restrict_targetfirstvaluedecode))) /\ ((dst_positive_restrict_targetfirst) + ge_balance_negative_restrict_targetfirstvalue = (dst_negative_restrict_targetfirst) + ge_balance_positive_restrict_targetfirstvalue))))))))) -> (exists dst_positive_code_restrict_targetsecond dst_positive_scale_restrict_targetsecond dst_negative_code_restrict_targetsecond dst_negative_scale_restrict_targetsecond dst_positive_restrict_targetsecond dst_negative_restrict_targetsecond. (((F) = (((((dst_positive_code_restrict_targetsecond) + (dst_positive_scale_restrict_targetsecond)) * S ((dst_positive_code_restrict_targetsecond) + (dst_positive_scale_restrict_targetsecond)) + ((dst_positive_scale_restrict_targetsecond) + (dst_positive_scale_restrict_targetsecond))) + (((dst_negative_code_restrict_targetsecond) + (dst_negative_scale_restrict_targetsecond)) * S ((dst_negative_code_restrict_targetsecond) + (dst_negative_scale_restrict_targetsecond)) + ((dst_negative_scale_restrict_targetsecond) + (dst_negative_scale_restrict_targetsecond)))) * S ((((dst_positive_code_restrict_targetsecond) + (dst_positive_scale_restrict_targetsecond)) * S ((dst_positive_code_restrict_targetsecond) + (dst_positive_scale_restrict_targetsecond)) + ((dst_positive_scale_restrict_targetsecond) + (dst_positive_scale_restrict_targetsecond))) + (((dst_negative_code_restrict_targetsecond) + (dst_negative_scale_restrict_targetsecond)) * S ((dst_negative_code_restrict_targetsecond) + (dst_negative_scale_restrict_targetsecond)) + ((dst_negative_scale_restrict_targetsecond) + (dst_negative_scale_restrict_targetsecond)))) + ((((dst_negative_code_restrict_targetsecond) + (dst_negative_scale_restrict_targetsecond)) * S ((dst_negative_code_restrict_targetsecond) + (dst_negative_scale_restrict_targetsecond)) + ((dst_negative_scale_restrict_targetsecond) + (dst_negative_scale_restrict_targetsecond))) + (((dst_negative_code_restrict_targetsecond) + (dst_negative_scale_restrict_targetsecond)) * S ((dst_negative_code_restrict_targetsecond) + (dst_negative_scale_restrict_targetsecond)) + ((dst_negative_scale_restrict_targetsecond) + (dst_negative_scale_restrict_targetsecond)))))) /\ (((((exists ff_h_pvs_restrict_targetsecondpositive. ff_h_pvs_restrict_targetsecondpositive + S (dst_positive_restrict_targetsecond) = S ((S (mp_b_restrict_target)) * dst_positive_scale_restrict_targetsecond)) /\ exists ff_q_pvs_restrict_targetsecondpositive. dst_positive_code_restrict_targetsecond = ff_q_pvs_restrict_targetsecondpositive * S ((S (mp_b_restrict_target)) * dst_positive_scale_restrict_targetsecond) + (dst_positive_restrict_targetsecond))) /\ (((((exists ff_h_pvs_restrict_targetsecondnegative. ff_h_pvs_restrict_targetsecondnegative + S (dst_negative_restrict_targetsecond) = S ((S (mp_b_restrict_target)) * dst_negative_scale_restrict_targetsecond)) /\ exists ff_q_pvs_restrict_targetsecondnegative. dst_negative_code_restrict_targetsecond = ff_q_pvs_restrict_targetsecondnegative * S ((S (mp_b_restrict_target)) * dst_negative_scale_restrict_targetsecond) + (dst_negative_restrict_targetsecond))) /\ (exists ge_balance_positive_restrict_targetsecondvalue ge_balance_negative_restrict_targetsecondvalue. (((((mp_y_restrict_target) = 2 * (ge_balance_positive_restrict_targetsecondvalue) /\ (ge_balance_negative_restrict_targetsecondvalue) = 0) \/ exists ge_signed_half_restrict_targetsecondvaluedecode. (((mp_y_restrict_target) = 2 * ge_signed_half_restrict_targetsecondvaluedecode + 1 /\ (ge_balance_positive_restrict_targetsecondvalue) = 0) /\ (ge_balance_negative_restrict_targetsecondvalue) = S ge_signed_half_restrict_targetsecondvaluedecode))) /\ ((dst_positive_restrict_targetsecond) + ge_balance_negative_restrict_targetsecondvalue = (dst_negative_restrict_targetsecond) + ge_balance_positive_restrict_targetsecondvalue))))))))) -> (exists dst_positive_code_restrict_targetproduct dst_positive_scale_restrict_targetproduct dst_negative_code_restrict_targetproduct dst_negative_scale_restrict_targetproduct dst_positive_restrict_targetproduct dst_negative_restrict_targetproduct. (((F) = (((((dst_positive_code_restrict_targetproduct) + (dst_positive_scale_restrict_targetproduct)) * S ((dst_positive_code_restrict_targetproduct) + (dst_positive_scale_restrict_targetproduct)) + ((dst_positive_scale_restrict_targetproduct) + (dst_positive_scale_restrict_targetproduct))) + (((dst_negative_code_restrict_targetproduct) + (dst_negative_scale_restrict_targetproduct)) * S ((dst_negative_code_restrict_targetproduct) + (dst_negative_scale_restrict_targetproduct)) + ((dst_negative_scale_restrict_targetproduct) + (dst_negative_scale_restrict_targetproduct)))) * S ((((dst_positive_code_restrict_targetproduct) + (dst_positive_scale_restrict_targetproduct)) * S ((dst_positive_code_restrict_targetproduct) + (dst_positive_scale_restrict_targetproduct)) + ((dst_positive_scale_restrict_targetproduct) + (dst_positive_scale_restrict_targetproduct))) + (((dst_negative_code_restrict_targetproduct) + (dst_negative_scale_restrict_targetproduct)) * S ((dst_negative_code_restrict_targetproduct) + (dst_negative_scale_restrict_targetproduct)) + ((dst_negative_scale_restrict_targetproduct) + (dst_negative_scale_restrict_targetproduct)))) + ((((dst_negative_code_restrict_targetproduct) + (dst_negative_scale_restrict_targetproduct)) * S ((dst_negative_code_restrict_targetproduct) + (dst_negative_scale_restrict_targetproduct)) + ((dst_negative_scale_restrict_targetproduct) + (dst_negative_scale_restrict_targetproduct))) + (((dst_negative_code_restrict_targetproduct) + (dst_negative_scale_restrict_targetproduct)) * S ((dst_negative_code_restrict_targetproduct) + (dst_negative_scale_restrict_targetproduct)) + ((dst_negative_scale_restrict_targetproduct) + (dst_negative_scale_restrict_targetproduct)))))) /\ (((((exists ff_h_pvs_restrict_targetproductpositive. ff_h_pvs_restrict_targetproductpositive + S (dst_positive_restrict_targetproduct) = S ((S (mp_a_restrict_target*mp_b_restrict_target)) * dst_positive_scale_restrict_targetproduct)) /\ exists ff_q_pvs_restrict_targetproductpositive. dst_positive_code_restrict_targetproduct = ff_q_pvs_restrict_targetproductpositive * S ((S (mp_a_restrict_target*mp_b_restrict_target)) * dst_positive_scale_restrict_targetproduct) + (dst_positive_restrict_targetproduct))) /\ (((((exists ff_h_pvs_restrict_targetproductnegative. ff_h_pvs_restrict_targetproductnegative + S (dst_negative_restrict_targetproduct) = S ((S (mp_a_restrict_target*mp_b_restrict_target)) * dst_negative_scale_restrict_targetproduct)) /\ exists ff_q_pvs_restrict_targetproductnegative. dst_negative_code_restrict_targetproduct = ff_q_pvs_restrict_targetproductnegative * S ((S (mp_a_restrict_target*mp_b_restrict_target)) * dst_negative_scale_restrict_targetproduct) + (dst_negative_restrict_targetproduct))) /\ (exists ge_balance_positive_restrict_targetproductvalue ge_balance_negative_restrict_targetproductvalue. (((((mp_z_restrict_target) = 2 * (ge_balance_positive_restrict_targetproductvalue) /\ (ge_balance_negative_restrict_targetproductvalue) = 0) \/ exists ge_signed_half_restrict_targetproductvaluedecode. (((mp_z_restrict_target) = 2 * ge_signed_half_restrict_targetproductvaluedecode + 1 /\ (ge_balance_positive_restrict_targetproductvalue) = 0) /\ (ge_balance_negative_restrict_targetproductvalue) = S ge_signed_half_restrict_targetproductvaluedecode))) /\ ((dst_positive_restrict_targetproduct) + ge_balance_negative_restrict_targetproductvalue = (dst_negative_restrict_targetproduct) + ge_balance_positive_restrict_targetproductvalue))))))))) -> (exists sto_ap_restrict_targetlaw sto_an_restrict_targetlaw sto_bp_restrict_targetlaw sto_bn_restrict_targetlaw sto_cp_restrict_targetlaw sto_cn_restrict_targetlaw. (((((mp_x_restrict_target) = 2 * (sto_ap_restrict_targetlaw) /\ (sto_an_restrict_targetlaw) = 0) \/ exists ge_signed_half_restrict_targetlawleft. (((mp_x_restrict_target) = 2 * ge_signed_half_restrict_targetlawleft + 1 /\ (sto_ap_restrict_targetlaw) = 0) /\ (sto_an_restrict_targetlaw) = S ge_signed_half_restrict_targetlawleft))) /\ ((((((mp_y_restrict_target) = 2 * (sto_bp_restrict_targetlaw) /\ (sto_bn_restrict_targetlaw) = 0) \/ exists ge_signed_half_restrict_targetlawright. (((mp_y_restrict_target) = 2 * ge_signed_half_restrict_targetlawright + 1 /\ (sto_bp_restrict_targetlaw) = 0) /\ (sto_bn_restrict_targetlaw) = S ge_signed_half_restrict_targetlawright))) /\ ((((((mp_z_restrict_target) = 2 * (sto_cp_restrict_targetlaw) /\ (sto_cn_restrict_targetlaw) = 0) \/ exists ge_signed_half_restrict_targetlawoutput. (((mp_z_restrict_target) = 2 * ge_signed_half_restrict_targetlawoutput + 1 /\ (sto_cp_restrict_targetlaw) = 0) /\ (sto_cn_restrict_targetlaw) = S ge_signed_half_restrict_targetlawoutput))) /\ ((sto_ap_restrict_targetlaw * sto_bp_restrict_targetlaw + sto_an_restrict_targetlaw * sto_bn_restrict_targetlaw) + sto_cn_restrict_targetlaw = (sto_ap_restrict_targetlaw * sto_bn_restrict_targetlaw + sto_an_restrict_targetlaw * sto_bp_restrict_targetlaw) + sto_cp_restrict_targetlaw))))))))))))))