signed_multiplicative_positive_extensional

Exact expanded first-order arithmetic statement

forall N F G. (((~((N)=0)) /\ (((exists dst_positive_code_extensional_sourcetable dst_positive_scale_extensional_sourcetable dst_negative_code_extensional_sourcetable dst_negative_scale_extensional_sourcetable. (((F) = (((((dst_positive_code_extensional_sourcetable) + (dst_positive_scale_extensional_sourcetable)) * S ((dst_positive_code_extensional_sourcetable) + (dst_positive_scale_extensional_sourcetable)) + ((dst_positive_scale_extensional_sourcetable) + (dst_positive_scale_extensional_sourcetable))) + (((dst_negative_code_extensional_sourcetable) + (dst_negative_scale_extensional_sourcetable)) * S ((dst_negative_code_extensional_sourcetable) + (dst_negative_scale_extensional_sourcetable)) + ((dst_negative_scale_extensional_sourcetable) + (dst_negative_scale_extensional_sourcetable)))) * S ((((dst_positive_code_extensional_sourcetable) + (dst_positive_scale_extensional_sourcetable)) * S ((dst_positive_code_extensional_sourcetable) + (dst_positive_scale_extensional_sourcetable)) + ((dst_positive_scale_extensional_sourcetable) + (dst_positive_scale_extensional_sourcetable))) + (((dst_negative_code_extensional_sourcetable) + (dst_negative_scale_extensional_sourcetable)) * S ((dst_negative_code_extensional_sourcetable) + (dst_negative_scale_extensional_sourcetable)) + ((dst_negative_scale_extensional_sourcetable) + (dst_negative_scale_extensional_sourcetable)))) + ((((dst_negative_code_extensional_sourcetable) + (dst_negative_scale_extensional_sourcetable)) * S ((dst_negative_code_extensional_sourcetable) + (dst_negative_scale_extensional_sourcetable)) + ((dst_negative_scale_extensional_sourcetable) + (dst_negative_scale_extensional_sourcetable))) + (((dst_negative_code_extensional_sourcetable) + (dst_negative_scale_extensional_sourcetable)) * S ((dst_negative_code_extensional_sourcetable) + (dst_negative_scale_extensional_sourcetable)) + ((dst_negative_scale_extensional_sourcetable) + (dst_negative_scale_extensional_sourcetable)))))) /\ (forall dst_index_extensional_sourcetable. (exists pvs_le_gap_extensional_sourcetabledomain. pvs_le_gap_extensional_sourcetabledomain + (dst_index_extensional_sourcetable) = (N)) -> exists dst_positive_extensional_sourcetable dst_negative_extensional_sourcetable dst_value_extensional_sourcetable. ((((exists ff_h_pvs_extensional_sourcetableentrypositive. ff_h_pvs_extensional_sourcetableentrypositive + S (dst_positive_extensional_sourcetable) = S ((S (dst_index_extensional_sourcetable)) * dst_positive_scale_extensional_sourcetable)) /\ exists ff_q_pvs_extensional_sourcetableentrypositive. dst_positive_code_extensional_sourcetable = ff_q_pvs_extensional_sourcetableentrypositive * S ((S (dst_index_extensional_sourcetable)) * dst_positive_scale_extensional_sourcetable) + (dst_positive_extensional_sourcetable))) /\ (((((exists ff_h_pvs_extensional_sourcetableentrynegative. ff_h_pvs_extensional_sourcetableentrynegative + S (dst_negative_extensional_sourcetable) = S ((S (dst_index_extensional_sourcetable)) * dst_negative_scale_extensional_sourcetable)) /\ exists ff_q_pvs_extensional_sourcetableentrynegative. dst_negative_code_extensional_sourcetable = ff_q_pvs_extensional_sourcetableentrynegative * S ((S (dst_index_extensional_sourcetable)) * dst_negative_scale_extensional_sourcetable) + (dst_negative_extensional_sourcetable))) /\ (exists ge_balance_positive_extensional_sourcetableentryvalue ge_balance_negative_extensional_sourcetableentryvalue. (((((dst_value_extensional_sourcetable) = 2 * (ge_balance_positive_extensional_sourcetableentryvalue) /\ (ge_balance_negative_extensional_sourcetableentryvalue) = 0) \/ exists ge_signed_half_extensional_sourcetableentryvaluedecode. (((dst_value_extensional_sourcetable) = 2 * ge_signed_half_extensional_sourcetableentryvaluedecode + 1 /\ (ge_balance_positive_extensional_sourcetableentryvalue) = 0) /\ (ge_balance_negative_extensional_sourcetableentryvalue) = S ge_signed_half_extensional_sourcetableentryvaluedecode))) /\ ((dst_positive_extensional_sourcetable) + ge_balance_negative_extensional_sourcetableentryvalue = (dst_negative_extensional_sourcetable) + ge_balance_positive_extensional_sourcetableentryvalue))))))))) /\ (((exists dst_positive_code_extensional_sourceone dst_positive_scale_extensional_sourceone dst_negative_code_extensional_sourceone dst_negative_scale_extensional_sourceone dst_positive_extensional_sourceone dst_negative_extensional_sourceone. (((F) = (((((dst_positive_code_extensional_sourceone) + (dst_positive_scale_extensional_sourceone)) * S ((dst_positive_code_extensional_sourceone) + (dst_positive_scale_extensional_sourceone)) + ((dst_positive_scale_extensional_sourceone) + (dst_positive_scale_extensional_sourceone))) + (((dst_negative_code_extensional_sourceone) + (dst_negative_scale_extensional_sourceone)) * S ((dst_negative_code_extensional_sourceone) + (dst_negative_scale_extensional_sourceone)) + ((dst_negative_scale_extensional_sourceone) + (dst_negative_scale_extensional_sourceone)))) * S ((((dst_positive_code_extensional_sourceone) + (dst_positive_scale_extensional_sourceone)) * S ((dst_positive_code_extensional_sourceone) + (dst_positive_scale_extensional_sourceone)) + ((dst_positive_scale_extensional_sourceone) + (dst_positive_scale_extensional_sourceone))) + (((dst_negative_code_extensional_sourceone) + (dst_negative_scale_extensional_sourceone)) * S ((dst_negative_code_extensional_sourceone) + (dst_negative_scale_extensional_sourceone)) + ((dst_negative_scale_extensional_sourceone) + (dst_negative_scale_extensional_sourceone)))) + ((((dst_negative_code_extensional_sourceone) + (dst_negative_scale_extensional_sourceone)) * S ((dst_negative_code_extensional_sourceone) + (dst_negative_scale_extensional_sourceone)) + ((dst_negative_scale_extensional_sourceone) + (dst_negative_scale_extensional_sourceone))) + (((dst_negative_code_extensional_sourceone) + (dst_negative_scale_extensional_sourceone)) * S ((dst_negative_code_extensional_sourceone) + (dst_negative_scale_extensional_sourceone)) + ((dst_negative_scale_extensional_sourceone) + (dst_negative_scale_extensional_sourceone)))))) /\ (((((exists ff_h_pvs_extensional_sourceonepositive. ff_h_pvs_extensional_sourceonepositive + S (dst_positive_extensional_sourceone) = S ((S (1)) * dst_positive_scale_extensional_sourceone)) /\ exists ff_q_pvs_extensional_sourceonepositive. dst_positive_code_extensional_sourceone = ff_q_pvs_extensional_sourceonepositive * S ((S (1)) * dst_positive_scale_extensional_sourceone) + (dst_positive_extensional_sourceone))) /\ (((((exists ff_h_pvs_extensional_sourceonenegative. ff_h_pvs_extensional_sourceonenegative + S (dst_negative_extensional_sourceone) = S ((S (1)) * dst_negative_scale_extensional_sourceone)) /\ exists ff_q_pvs_extensional_sourceonenegative. dst_negative_code_extensional_sourceone = ff_q_pvs_extensional_sourceonenegative * S ((S (1)) * dst_negative_scale_extensional_sourceone) + (dst_negative_extensional_sourceone))) /\ (exists ge_balance_positive_extensional_sourceonevalue ge_balance_negative_extensional_sourceonevalue. (((((2) = 2 * (ge_balance_positive_extensional_sourceonevalue) /\ (ge_balance_negative_extensional_sourceonevalue) = 0) \/ exists ge_signed_half_extensional_sourceonevaluedecode. (((2) = 2 * ge_signed_half_extensional_sourceonevaluedecode + 1 /\ (ge_balance_positive_extensional_sourceonevalue) = 0) /\ (ge_balance_negative_extensional_sourceonevalue) = S ge_signed_half_extensional_sourceonevaluedecode))) /\ ((dst_positive_extensional_sourceone) + ge_balance_negative_extensional_sourceonevalue = (dst_negative_extensional_sourceone) + ge_balance_positive_extensional_sourceonevalue))))))))) /\ (forall mp_a_extensional_source mp_b_extensional_source mp_x_extensional_source mp_y_extensional_source mp_z_extensional_source. ~(mp_a_extensional_source=0) -> ~(mp_b_extensional_source=0) -> (exists pvs_le_gap_extensional_sourcebound. pvs_le_gap_extensional_sourcebound + (mp_a_extensional_source*mp_b_extensional_source) = (N)) -> (forall frp_divisor_extensional_sourcecoprime. (exists frp_left_factor_extensional_sourcecoprime. mp_a_extensional_source = frp_divisor_extensional_sourcecoprime * frp_left_factor_extensional_sourcecoprime) -> (exists frp_right_factor_extensional_sourcecoprime. mp_b_extensional_source = frp_divisor_extensional_sourcecoprime * frp_right_factor_extensional_sourcecoprime) -> frp_divisor_extensional_sourcecoprime = 1) -> (exists dst_positive_code_extensional_sourcefirst dst_positive_scale_extensional_sourcefirst dst_negative_code_extensional_sourcefirst dst_negative_scale_extensional_sourcefirst dst_positive_extensional_sourcefirst dst_negative_extensional_sourcefirst. (((F) = (((((dst_positive_code_extensional_sourcefirst) + (dst_positive_scale_extensional_sourcefirst)) * S ((dst_positive_code_extensional_sourcefirst) + (dst_positive_scale_extensional_sourcefirst)) + ((dst_positive_scale_extensional_sourcefirst) + (dst_positive_scale_extensional_sourcefirst))) + (((dst_negative_code_extensional_sourcefirst) + (dst_negative_scale_extensional_sourcefirst)) * S ((dst_negative_code_extensional_sourcefirst) + (dst_negative_scale_extensional_sourcefirst)) + ((dst_negative_scale_extensional_sourcefirst) + (dst_negative_scale_extensional_sourcefirst)))) * S ((((dst_positive_code_extensional_sourcefirst) + (dst_positive_scale_extensional_sourcefirst)) * S ((dst_positive_code_extensional_sourcefirst) + (dst_positive_scale_extensional_sourcefirst)) + ((dst_positive_scale_extensional_sourcefirst) + (dst_positive_scale_extensional_sourcefirst))) + (((dst_negative_code_extensional_sourcefirst) + (dst_negative_scale_extensional_sourcefirst)) * S ((dst_negative_code_extensional_sourcefirst) + (dst_negative_scale_extensional_sourcefirst)) + ((dst_negative_scale_extensional_sourcefirst) + (dst_negative_scale_extensional_sourcefirst)))) + ((((dst_negative_code_extensional_sourcefirst) + (dst_negative_scale_extensional_sourcefirst)) * S ((dst_negative_code_extensional_sourcefirst) + (dst_negative_scale_extensional_sourcefirst)) + ((dst_negative_scale_extensional_sourcefirst) + (dst_negative_scale_extensional_sourcefirst))) + (((dst_negative_code_extensional_sourcefirst) + (dst_negative_scale_extensional_sourcefirst)) * S ((dst_negative_code_extensional_sourcefirst) + (dst_negative_scale_extensional_sourcefirst)) + ((dst_negative_scale_extensional_sourcefirst) + (dst_negative_scale_extensional_sourcefirst)))))) /\ (((((exists ff_h_pvs_extensional_sourcefirstpositive. ff_h_pvs_extensional_sourcefirstpositive + S (dst_positive_extensional_sourcefirst) = S ((S (mp_a_extensional_source)) * dst_positive_scale_extensional_sourcefirst)) /\ exists ff_q_pvs_extensional_sourcefirstpositive. dst_positive_code_extensional_sourcefirst = ff_q_pvs_extensional_sourcefirstpositive * S ((S (mp_a_extensional_source)) * dst_positive_scale_extensional_sourcefirst) + (dst_positive_extensional_sourcefirst))) /\ (((((exists ff_h_pvs_extensional_sourcefirstnegative. ff_h_pvs_extensional_sourcefirstnegative + S (dst_negative_extensional_sourcefirst) = S ((S (mp_a_extensional_source)) * dst_negative_scale_extensional_sourcefirst)) /\ exists ff_q_pvs_extensional_sourcefirstnegative. dst_negative_code_extensional_sourcefirst = ff_q_pvs_extensional_sourcefirstnegative * S ((S (mp_a_extensional_source)) * dst_negative_scale_extensional_sourcefirst) + (dst_negative_extensional_sourcefirst))) /\ (exists ge_balance_positive_extensional_sourcefirstvalue ge_balance_negative_extensional_sourcefirstvalue. (((((mp_x_extensional_source) = 2 * (ge_balance_positive_extensional_sourcefirstvalue) /\ (ge_balance_negative_extensional_sourcefirstvalue) = 0) \/ exists ge_signed_half_extensional_sourcefirstvaluedecode. (((mp_x_extensional_source) = 2 * ge_signed_half_extensional_sourcefirstvaluedecode + 1 /\ (ge_balance_positive_extensional_sourcefirstvalue) = 0) /\ (ge_balance_negative_extensional_sourcefirstvalue) = S ge_signed_half_extensional_sourcefirstvaluedecode))) /\ ((dst_positive_extensional_sourcefirst) + ge_balance_negative_extensional_sourcefirstvalue = (dst_negative_extensional_sourcefirst) + ge_balance_positive_extensional_sourcefirstvalue))))))))) -> (exists dst_positive_code_extensional_sourcesecond dst_positive_scale_extensional_sourcesecond dst_negative_code_extensional_sourcesecond dst_negative_scale_extensional_sourcesecond dst_positive_extensional_sourcesecond dst_negative_extensional_sourcesecond. (((F) = (((((dst_positive_code_extensional_sourcesecond) + (dst_positive_scale_extensional_sourcesecond)) * S ((dst_positive_code_extensional_sourcesecond) + (dst_positive_scale_extensional_sourcesecond)) + ((dst_positive_scale_extensional_sourcesecond) + (dst_positive_scale_extensional_sourcesecond))) + (((dst_negative_code_extensional_sourcesecond) + (dst_negative_scale_extensional_sourcesecond)) * S ((dst_negative_code_extensional_sourcesecond) + (dst_negative_scale_extensional_sourcesecond)) + ((dst_negative_scale_extensional_sourcesecond) + (dst_negative_scale_extensional_sourcesecond)))) * S ((((dst_positive_code_extensional_sourcesecond) + (dst_positive_scale_extensional_sourcesecond)) * S ((dst_positive_code_extensional_sourcesecond) + (dst_positive_scale_extensional_sourcesecond)) + ((dst_positive_scale_extensional_sourcesecond) + (dst_positive_scale_extensional_sourcesecond))) + (((dst_negative_code_extensional_sourcesecond) + (dst_negative_scale_extensional_sourcesecond)) * S ((dst_negative_code_extensional_sourcesecond) + (dst_negative_scale_extensional_sourcesecond)) + ((dst_negative_scale_extensional_sourcesecond) + (dst_negative_scale_extensional_sourcesecond)))) + ((((dst_negative_code_extensional_sourcesecond) + (dst_negative_scale_extensional_sourcesecond)) * S ((dst_negative_code_extensional_sourcesecond) + (dst_negative_scale_extensional_sourcesecond)) + ((dst_negative_scale_extensional_sourcesecond) + (dst_negative_scale_extensional_sourcesecond))) + (((dst_negative_code_extensional_sourcesecond) + (dst_negative_scale_extensional_sourcesecond)) * S ((dst_negative_code_extensional_sourcesecond) + (dst_negative_scale_extensional_sourcesecond)) + ((dst_negative_scale_extensional_sourcesecond) + (dst_negative_scale_extensional_sourcesecond)))))) /\ (((((exists ff_h_pvs_extensional_sourcesecondpositive. ff_h_pvs_extensional_sourcesecondpositive + S (dst_positive_extensional_sourcesecond) = S ((S (mp_b_extensional_source)) * dst_positive_scale_extensional_sourcesecond)) /\ exists ff_q_pvs_extensional_sourcesecondpositive. dst_positive_code_extensional_sourcesecond = ff_q_pvs_extensional_sourcesecondpositive * S ((S (mp_b_extensional_source)) * dst_positive_scale_extensional_sourcesecond) + (dst_positive_extensional_sourcesecond))) /\ (((((exists ff_h_pvs_extensional_sourcesecondnegative. ff_h_pvs_extensional_sourcesecondnegative + S (dst_negative_extensional_sourcesecond) = S ((S (mp_b_extensional_source)) * dst_negative_scale_extensional_sourcesecond)) /\ exists ff_q_pvs_extensional_sourcesecondnegative. dst_negative_code_extensional_sourcesecond = ff_q_pvs_extensional_sourcesecondnegative * S ((S (mp_b_extensional_source)) * dst_negative_scale_extensional_sourcesecond) + (dst_negative_extensional_sourcesecond))) /\ (exists ge_balance_positive_extensional_sourcesecondvalue ge_balance_negative_extensional_sourcesecondvalue. (((((mp_y_extensional_source) = 2 * (ge_balance_positive_extensional_sourcesecondvalue) /\ (ge_balance_negative_extensional_sourcesecondvalue) = 0) \/ exists ge_signed_half_extensional_sourcesecondvaluedecode. (((mp_y_extensional_source) = 2 * ge_signed_half_extensional_sourcesecondvaluedecode + 1 /\ (ge_balance_positive_extensional_sourcesecondvalue) = 0) /\ (ge_balance_negative_extensional_sourcesecondvalue) = S ge_signed_half_extensional_sourcesecondvaluedecode))) /\ ((dst_positive_extensional_sourcesecond) + ge_balance_negative_extensional_sourcesecondvalue = (dst_negative_extensional_sourcesecond) + ge_balance_positive_extensional_sourcesecondvalue))))))))) -> (exists dst_positive_code_extensional_sourceproduct dst_positive_scale_extensional_sourceproduct dst_negative_code_extensional_sourceproduct dst_negative_scale_extensional_sourceproduct dst_positive_extensional_sourceproduct dst_negative_extensional_sourceproduct. (((F) = (((((dst_positive_code_extensional_sourceproduct) + (dst_positive_scale_extensional_sourceproduct)) * S ((dst_positive_code_extensional_sourceproduct) + (dst_positive_scale_extensional_sourceproduct)) + ((dst_positive_scale_extensional_sourceproduct) + (dst_positive_scale_extensional_sourceproduct))) + (((dst_negative_code_extensional_sourceproduct) + (dst_negative_scale_extensional_sourceproduct)) * S ((dst_negative_code_extensional_sourceproduct) + (dst_negative_scale_extensional_sourceproduct)) + ((dst_negative_scale_extensional_sourceproduct) + (dst_negative_scale_extensional_sourceproduct)))) * S ((((dst_positive_code_extensional_sourceproduct) + (dst_positive_scale_extensional_sourceproduct)) * S ((dst_positive_code_extensional_sourceproduct) + (dst_positive_scale_extensional_sourceproduct)) + ((dst_positive_scale_extensional_sourceproduct) + (dst_positive_scale_extensional_sourceproduct))) + (((dst_negative_code_extensional_sourceproduct) + (dst_negative_scale_extensional_sourceproduct)) * S ((dst_negative_code_extensional_sourceproduct) + (dst_negative_scale_extensional_sourceproduct)) + ((dst_negative_scale_extensional_sourceproduct) + (dst_negative_scale_extensional_sourceproduct)))) + ((((dst_negative_code_extensional_sourceproduct) + (dst_negative_scale_extensional_sourceproduct)) * S ((dst_negative_code_extensional_sourceproduct) + (dst_negative_scale_extensional_sourceproduct)) + ((dst_negative_scale_extensional_sourceproduct) + (dst_negative_scale_extensional_sourceproduct))) + (((dst_negative_code_extensional_sourceproduct) + (dst_negative_scale_extensional_sourceproduct)) * S ((dst_negative_code_extensional_sourceproduct) + (dst_negative_scale_extensional_sourceproduct)) + ((dst_negative_scale_extensional_sourceproduct) + (dst_negative_scale_extensional_sourceproduct)))))) /\ (((((exists ff_h_pvs_extensional_sourceproductpositive. ff_h_pvs_extensional_sourceproductpositive + S (dst_positive_extensional_sourceproduct) = S ((S (mp_a_extensional_source*mp_b_extensional_source)) * dst_positive_scale_extensional_sourceproduct)) /\ exists ff_q_pvs_extensional_sourceproductpositive. dst_positive_code_extensional_sourceproduct = ff_q_pvs_extensional_sourceproductpositive * S ((S (mp_a_extensional_source*mp_b_extensional_source)) * dst_positive_scale_extensional_sourceproduct) + (dst_positive_extensional_sourceproduct))) /\ (((((exists ff_h_pvs_extensional_sourceproductnegative. ff_h_pvs_extensional_sourceproductnegative + S (dst_negative_extensional_sourceproduct) = S ((S (mp_a_extensional_source*mp_b_extensional_source)) * dst_negative_scale_extensional_sourceproduct)) /\ exists ff_q_pvs_extensional_sourceproductnegative. dst_negative_code_extensional_sourceproduct = ff_q_pvs_extensional_sourceproductnegative * S ((S (mp_a_extensional_source*mp_b_extensional_source)) * dst_negative_scale_extensional_sourceproduct) + (dst_negative_extensional_sourceproduct))) /\ (exists ge_balance_positive_extensional_sourceproductvalue ge_balance_negative_extensional_sourceproductvalue. (((((mp_z_extensional_source) = 2 * (ge_balance_positive_extensional_sourceproductvalue) /\ (ge_balance_negative_extensional_sourceproductvalue) = 0) \/ exists ge_signed_half_extensional_sourceproductvaluedecode. (((mp_z_extensional_source) = 2 * ge_signed_half_extensional_sourceproductvaluedecode + 1 /\ (ge_balance_positive_extensional_sourceproductvalue) = 0) /\ (ge_balance_negative_extensional_sourceproductvalue) = S ge_signed_half_extensional_sourceproductvaluedecode))) /\ ((dst_positive_extensional_sourceproduct) + ge_balance_negative_extensional_sourceproductvalue = (dst_negative_extensional_sourceproduct) + ge_balance_positive_extensional_sourceproductvalue))))))))) -> (exists sto_ap_extensional_sourcelaw sto_an_extensional_sourcelaw sto_bp_extensional_sourcelaw sto_bn_extensional_sourcelaw sto_cp_extensional_sourcelaw sto_cn_extensional_sourcelaw. (((((mp_x_extensional_source) = 2 * (sto_ap_extensional_sourcelaw) /\ (sto_an_extensional_sourcelaw) = 0) \/ exists ge_signed_half_extensional_sourcelawleft. (((mp_x_extensional_source) = 2 * ge_signed_half_extensional_sourcelawleft + 1 /\ (sto_ap_extensional_sourcelaw) = 0) /\ (sto_an_extensional_sourcelaw) = S ge_signed_half_extensional_sourcelawleft))) /\ ((((((mp_y_extensional_source) = 2 * (sto_bp_extensional_sourcelaw) /\ (sto_bn_extensional_sourcelaw) = 0) \/ exists ge_signed_half_extensional_sourcelawright. (((mp_y_extensional_source) = 2 * ge_signed_half_extensional_sourcelawright + 1 /\ (sto_bp_extensional_sourcelaw) = 0) /\ (sto_bn_extensional_sourcelaw) = S ge_signed_half_extensional_sourcelawright))) /\ ((((((mp_z_extensional_source) = 2 * (sto_cp_extensional_sourcelaw) /\ (sto_cn_extensional_sourcelaw) = 0) \/ exists ge_signed_half_extensional_sourcelawoutput. (((mp_z_extensional_source) = 2 * ge_signed_half_extensional_sourcelawoutput + 1 /\ (sto_cp_extensional_sourcelaw) = 0) /\ (sto_cn_extensional_sourcelaw) = S ge_signed_half_extensional_sourcelawoutput))) /\ ((sto_ap_extensional_sourcelaw * sto_bp_extensional_sourcelaw + sto_an_extensional_sourcelaw * sto_bn_extensional_sourcelaw) + sto_cn_extensional_sourcelaw = (sto_ap_extensional_sourcelaw * sto_bn_extensional_sourcelaw + sto_an_extensional_sourcelaw * sto_bp_extensional_sourcelaw) + sto_cp_extensional_sourcelaw)))))))))))))) -> (exists dst_positive_code_extensional_target_table dst_positive_scale_extensional_target_table dst_negative_code_extensional_target_table dst_negative_scale_extensional_target_table. (((G) = (((((dst_positive_code_extensional_target_table) + (dst_positive_scale_extensional_target_table)) * S ((dst_positive_code_extensional_target_table) + (dst_positive_scale_extensional_target_table)) + ((dst_positive_scale_extensional_target_table) + (dst_positive_scale_extensional_target_table))) + (((dst_negative_code_extensional_target_table) + (dst_negative_scale_extensional_target_table)) * S ((dst_negative_code_extensional_target_table) + (dst_negative_scale_extensional_target_table)) + ((dst_negative_scale_extensional_target_table) + (dst_negative_scale_extensional_target_table)))) * S ((((dst_positive_code_extensional_target_table) + (dst_positive_scale_extensional_target_table)) * S ((dst_positive_code_extensional_target_table) + (dst_positive_scale_extensional_target_table)) + ((dst_positive_scale_extensional_target_table) + (dst_positive_scale_extensional_target_table))) + (((dst_negative_code_extensional_target_table) + (dst_negative_scale_extensional_target_table)) * S ((dst_negative_code_extensional_target_table) + (dst_negative_scale_extensional_target_table)) + ((dst_negative_scale_extensional_target_table) + (dst_negative_scale_extensional_target_table)))) + ((((dst_negative_code_extensional_target_table) + (dst_negative_scale_extensional_target_table)) * S ((dst_negative_code_extensional_target_table) + (dst_negative_scale_extensional_target_table)) + ((dst_negative_scale_extensional_target_table) + (dst_negative_scale_extensional_target_table))) + (((dst_negative_code_extensional_target_table) + (dst_negative_scale_extensional_target_table)) * S ((dst_negative_code_extensional_target_table) + (dst_negative_scale_extensional_target_table)) + ((dst_negative_scale_extensional_target_table) + (dst_negative_scale_extensional_target_table)))))) /\ (forall dst_index_extensional_target_table. (exists pvs_le_gap_extensional_target_tabledomain. pvs_le_gap_extensional_target_tabledomain + (dst_index_extensional_target_table) = (N)) -> exists dst_positive_extensional_target_table dst_negative_extensional_target_table dst_value_extensional_target_table. ((((exists ff_h_pvs_extensional_target_tableentrypositive. ff_h_pvs_extensional_target_tableentrypositive + S (dst_positive_extensional_target_table) = S ((S (dst_index_extensional_target_table)) * dst_positive_scale_extensional_target_table)) /\ exists ff_q_pvs_extensional_target_tableentrypositive. dst_positive_code_extensional_target_table = ff_q_pvs_extensional_target_tableentrypositive * S ((S (dst_index_extensional_target_table)) * dst_positive_scale_extensional_target_table) + (dst_positive_extensional_target_table))) /\ (((((exists ff_h_pvs_extensional_target_tableentrynegative. ff_h_pvs_extensional_target_tableentrynegative + S (dst_negative_extensional_target_table) = S ((S (dst_index_extensional_target_table)) * dst_negative_scale_extensional_target_table)) /\ exists ff_q_pvs_extensional_target_tableentrynegative. dst_negative_code_extensional_target_table = ff_q_pvs_extensional_target_tableentrynegative * S ((S (dst_index_extensional_target_table)) * dst_negative_scale_extensional_target_table) + (dst_negative_extensional_target_table))) /\ (exists ge_balance_positive_extensional_target_tableentryvalue ge_balance_negative_extensional_target_tableentryvalue. (((((dst_value_extensional_target_table) = 2 * (ge_balance_positive_extensional_target_tableentryvalue) /\ (ge_balance_negative_extensional_target_tableentryvalue) = 0) \/ exists ge_signed_half_extensional_target_tableentryvaluedecode. (((dst_value_extensional_target_table) = 2 * ge_signed_half_extensional_target_tableentryvaluedecode + 1 /\ (ge_balance_positive_extensional_target_tableentryvalue) = 0) /\ (ge_balance_negative_extensional_target_tableentryvalue) = S ge_signed_half_extensional_target_tableentryvaluedecode))) /\ ((dst_positive_extensional_target_table) + ge_balance_negative_extensional_target_tableentryvalue = (dst_negative_extensional_target_table) + ge_balance_positive_extensional_target_tableentryvalue))))))))) -> (forall dm_index_extensional_equality dm_first_value_extensional_equality dm_second_value_extensional_equality. ~(dm_index_extensional_equality=0) -> (exists pvs_le_gap_extensional_equalitydomain. pvs_le_gap_extensional_equalitydomain + (dm_index_extensional_equality) = (N)) -> (exists dst_positive_code_extensional_equalityfirst dst_positive_scale_extensional_equalityfirst dst_negative_code_extensional_equalityfirst dst_negative_scale_extensional_equalityfirst dst_positive_extensional_equalityfirst dst_negative_extensional_equalityfirst. (((F) = (((((dst_positive_code_extensional_equalityfirst) + (dst_positive_scale_extensional_equalityfirst)) * S ((dst_positive_code_extensional_equalityfirst) + (dst_positive_scale_extensional_equalityfirst)) + ((dst_positive_scale_extensional_equalityfirst) + (dst_positive_scale_extensional_equalityfirst))) + (((dst_negative_code_extensional_equalityfirst) + (dst_negative_scale_extensional_equalityfirst)) * S ((dst_negative_code_extensional_equalityfirst) + (dst_negative_scale_extensional_equalityfirst)) + ((dst_negative_scale_extensional_equalityfirst) + (dst_negative_scale_extensional_equalityfirst)))) * S ((((dst_positive_code_extensional_equalityfirst) + (dst_positive_scale_extensional_equalityfirst)) * S ((dst_positive_code_extensional_equalityfirst) + (dst_positive_scale_extensional_equalityfirst)) + ((dst_positive_scale_extensional_equalityfirst) + (dst_positive_scale_extensional_equalityfirst))) + (((dst_negative_code_extensional_equalityfirst) + (dst_negative_scale_extensional_equalityfirst)) * S ((dst_negative_code_extensional_equalityfirst) + (dst_negative_scale_extensional_equalityfirst)) + ((dst_negative_scale_extensional_equalityfirst) + (dst_negative_scale_extensional_equalityfirst)))) + ((((dst_negative_code_extensional_equalityfirst) + (dst_negative_scale_extensional_equalityfirst)) * S ((dst_negative_code_extensional_equalityfirst) + (dst_negative_scale_extensional_equalityfirst)) + ((dst_negative_scale_extensional_equalityfirst) + (dst_negative_scale_extensional_equalityfirst))) + (((dst_negative_code_extensional_equalityfirst) + (dst_negative_scale_extensional_equalityfirst)) * S ((dst_negative_code_extensional_equalityfirst) + (dst_negative_scale_extensional_equalityfirst)) + ((dst_negative_scale_extensional_equalityfirst) + (dst_negative_scale_extensional_equalityfirst)))))) /\ (((((exists ff_h_pvs_extensional_equalityfirstpositive. ff_h_pvs_extensional_equalityfirstpositive + S (dst_positive_extensional_equalityfirst) = S ((S (dm_index_extensional_equality)) * dst_positive_scale_extensional_equalityfirst)) /\ exists ff_q_pvs_extensional_equalityfirstpositive. dst_positive_code_extensional_equalityfirst = ff_q_pvs_extensional_equalityfirstpositive * S ((S (dm_index_extensional_equality)) * dst_positive_scale_extensional_equalityfirst) + (dst_positive_extensional_equalityfirst))) /\ (((((exists ff_h_pvs_extensional_equalityfirstnegative. ff_h_pvs_extensional_equalityfirstnegative + S (dst_negative_extensional_equalityfirst) = S ((S (dm_index_extensional_equality)) * dst_negative_scale_extensional_equalityfirst)) /\ exists ff_q_pvs_extensional_equalityfirstnegative. dst_negative_code_extensional_equalityfirst = ff_q_pvs_extensional_equalityfirstnegative * S ((S (dm_index_extensional_equality)) * dst_negative_scale_extensional_equalityfirst) + (dst_negative_extensional_equalityfirst))) /\ (exists ge_balance_positive_extensional_equalityfirstvalue ge_balance_negative_extensional_equalityfirstvalue. (((((dm_first_value_extensional_equality) = 2 * (ge_balance_positive_extensional_equalityfirstvalue) /\ (ge_balance_negative_extensional_equalityfirstvalue) = 0) \/ exists ge_signed_half_extensional_equalityfirstvaluedecode. (((dm_first_value_extensional_equality) = 2 * ge_signed_half_extensional_equalityfirstvaluedecode + 1 /\ (ge_balance_positive_extensional_equalityfirstvalue) = 0) /\ (ge_balance_negative_extensional_equalityfirstvalue) = S ge_signed_half_extensional_equalityfirstvaluedecode))) /\ ((dst_positive_extensional_equalityfirst) + ge_balance_negative_extensional_equalityfirstvalue = (dst_negative_extensional_equalityfirst) + ge_balance_positive_extensional_equalityfirstvalue))))))))) -> (exists dst_positive_code_extensional_equalitysecond dst_positive_scale_extensional_equalitysecond dst_negative_code_extensional_equalitysecond dst_negative_scale_extensional_equalitysecond dst_positive_extensional_equalitysecond dst_negative_extensional_equalitysecond. (((G) = (((((dst_positive_code_extensional_equalitysecond) + (dst_positive_scale_extensional_equalitysecond)) * S ((dst_positive_code_extensional_equalitysecond) + (dst_positive_scale_extensional_equalitysecond)) + ((dst_positive_scale_extensional_equalitysecond) + (dst_positive_scale_extensional_equalitysecond))) + (((dst_negative_code_extensional_equalitysecond) + (dst_negative_scale_extensional_equalitysecond)) * S ((dst_negative_code_extensional_equalitysecond) + (dst_negative_scale_extensional_equalitysecond)) + ((dst_negative_scale_extensional_equalitysecond) + (dst_negative_scale_extensional_equalitysecond)))) * S ((((dst_positive_code_extensional_equalitysecond) + (dst_positive_scale_extensional_equalitysecond)) * S ((dst_positive_code_extensional_equalitysecond) + (dst_positive_scale_extensional_equalitysecond)) + ((dst_positive_scale_extensional_equalitysecond) + (dst_positive_scale_extensional_equalitysecond))) + (((dst_negative_code_extensional_equalitysecond) + (dst_negative_scale_extensional_equalitysecond)) * S ((dst_negative_code_extensional_equalitysecond) + (dst_negative_scale_extensional_equalitysecond)) + ((dst_negative_scale_extensional_equalitysecond) + (dst_negative_scale_extensional_equalitysecond)))) + ((((dst_negative_code_extensional_equalitysecond) + (dst_negative_scale_extensional_equalitysecond)) * S ((dst_negative_code_extensional_equalitysecond) + (dst_negative_scale_extensional_equalitysecond)) + ((dst_negative_scale_extensional_equalitysecond) + (dst_negative_scale_extensional_equalitysecond))) + (((dst_negative_code_extensional_equalitysecond) + (dst_negative_scale_extensional_equalitysecond)) * S ((dst_negative_code_extensional_equalitysecond) + (dst_negative_scale_extensional_equalitysecond)) + ((dst_negative_scale_extensional_equalitysecond) + (dst_negative_scale_extensional_equalitysecond)))))) /\ (((((exists ff_h_pvs_extensional_equalitysecondpositive. ff_h_pvs_extensional_equalitysecondpositive + S (dst_positive_extensional_equalitysecond) = S ((S (dm_index_extensional_equality)) * dst_positive_scale_extensional_equalitysecond)) /\ exists ff_q_pvs_extensional_equalitysecondpositive. dst_positive_code_extensional_equalitysecond = ff_q_pvs_extensional_equalitysecondpositive * S ((S (dm_index_extensional_equality)) * dst_positive_scale_extensional_equalitysecond) + (dst_positive_extensional_equalitysecond))) /\ (((((exists ff_h_pvs_extensional_equalitysecondnegative. ff_h_pvs_extensional_equalitysecondnegative + S (dst_negative_extensional_equalitysecond) = S ((S (dm_index_extensional_equality)) * dst_negative_scale_extensional_equalitysecond)) /\ exists ff_q_pvs_extensional_equalitysecondnegative. dst_negative_code_extensional_equalitysecond = ff_q_pvs_extensional_equalitysecondnegative * S ((S (dm_index_extensional_equality)) * dst_negative_scale_extensional_equalitysecond) + (dst_negative_extensional_equalitysecond))) /\ (exists ge_balance_positive_extensional_equalitysecondvalue ge_balance_negative_extensional_equalitysecondvalue. (((((dm_second_value_extensional_equality) = 2 * (ge_balance_positive_extensional_equalitysecondvalue) /\ (ge_balance_negative_extensional_equalitysecondvalue) = 0) \/ exists ge_signed_half_extensional_equalitysecondvaluedecode. (((dm_second_value_extensional_equality) = 2 * ge_signed_half_extensional_equalitysecondvaluedecode + 1 /\ (ge_balance_positive_extensional_equalitysecondvalue) = 0) /\ (ge_balance_negative_extensional_equalitysecondvalue) = S ge_signed_half_extensional_equalitysecondvaluedecode))) /\ ((dst_positive_extensional_equalitysecond) + ge_balance_negative_extensional_equalitysecondvalue = (dst_negative_extensional_equalitysecond) + ge_balance_positive_extensional_equalitysecondvalue))))))))) -> dm_first_value_extensional_equality=dm_second_value_extensional_equality) -> (((~((N)=0)) /\ (((exists dst_positive_code_extensional_targettable dst_positive_scale_extensional_targettable dst_negative_code_extensional_targettable dst_negative_scale_extensional_targettable. (((G) = (((((dst_positive_code_extensional_targettable) + (dst_positive_scale_extensional_targettable)) * S ((dst_positive_code_extensional_targettable) + (dst_positive_scale_extensional_targettable)) + ((dst_positive_scale_extensional_targettable) + (dst_positive_scale_extensional_targettable))) + (((dst_negative_code_extensional_targettable) + (dst_negative_scale_extensional_targettable)) * S ((dst_negative_code_extensional_targettable) + (dst_negative_scale_extensional_targettable)) + ((dst_negative_scale_extensional_targettable) + (dst_negative_scale_extensional_targettable)))) * S ((((dst_positive_code_extensional_targettable) + (dst_positive_scale_extensional_targettable)) * S ((dst_positive_code_extensional_targettable) + (dst_positive_scale_extensional_targettable)) + ((dst_positive_scale_extensional_targettable) + (dst_positive_scale_extensional_targettable))) + (((dst_negative_code_extensional_targettable) + (dst_negative_scale_extensional_targettable)) * S ((dst_negative_code_extensional_targettable) + (dst_negative_scale_extensional_targettable)) + ((dst_negative_scale_extensional_targettable) + (dst_negative_scale_extensional_targettable)))) + ((((dst_negative_code_extensional_targettable) + (dst_negative_scale_extensional_targettable)) * S ((dst_negative_code_extensional_targettable) + (dst_negative_scale_extensional_targettable)) + ((dst_negative_scale_extensional_targettable) + (dst_negative_scale_extensional_targettable))) + (((dst_negative_code_extensional_targettable) + (dst_negative_scale_extensional_targettable)) * S ((dst_negative_code_extensional_targettable) + (dst_negative_scale_extensional_targettable)) + ((dst_negative_scale_extensional_targettable) + (dst_negative_scale_extensional_targettable)))))) /\ (forall dst_index_extensional_targettable. (exists pvs_le_gap_extensional_targettabledomain. pvs_le_gap_extensional_targettabledomain + (dst_index_extensional_targettable) = (N)) -> exists dst_positive_extensional_targettable dst_negative_extensional_targettable dst_value_extensional_targettable. ((((exists ff_h_pvs_extensional_targettableentrypositive. ff_h_pvs_extensional_targettableentrypositive + S (dst_positive_extensional_targettable) = S ((S (dst_index_extensional_targettable)) * dst_positive_scale_extensional_targettable)) /\ exists ff_q_pvs_extensional_targettableentrypositive. dst_positive_code_extensional_targettable = ff_q_pvs_extensional_targettableentrypositive * S ((S (dst_index_extensional_targettable)) * dst_positive_scale_extensional_targettable) + (dst_positive_extensional_targettable))) /\ (((((exists ff_h_pvs_extensional_targettableentrynegative. ff_h_pvs_extensional_targettableentrynegative + S (dst_negative_extensional_targettable) = S ((S (dst_index_extensional_targettable)) * dst_negative_scale_extensional_targettable)) /\ exists ff_q_pvs_extensional_targettableentrynegative. dst_negative_code_extensional_targettable = ff_q_pvs_extensional_targettableentrynegative * S ((S (dst_index_extensional_targettable)) * dst_negative_scale_extensional_targettable) + (dst_negative_extensional_targettable))) /\ (exists ge_balance_positive_extensional_targettableentryvalue ge_balance_negative_extensional_targettableentryvalue. (((((dst_value_extensional_targettable) = 2 * (ge_balance_positive_extensional_targettableentryvalue) /\ (ge_balance_negative_extensional_targettableentryvalue) = 0) \/ exists ge_signed_half_extensional_targettableentryvaluedecode. (((dst_value_extensional_targettable) = 2 * ge_signed_half_extensional_targettableentryvaluedecode + 1 /\ (ge_balance_positive_extensional_targettableentryvalue) = 0) /\ (ge_balance_negative_extensional_targettableentryvalue) = S ge_signed_half_extensional_targettableentryvaluedecode))) /\ ((dst_positive_extensional_targettable) + ge_balance_negative_extensional_targettableentryvalue = (dst_negative_extensional_targettable) + ge_balance_positive_extensional_targettableentryvalue))))))))) /\ (((exists dst_positive_code_extensional_targetone dst_positive_scale_extensional_targetone dst_negative_code_extensional_targetone dst_negative_scale_extensional_targetone dst_positive_extensional_targetone dst_negative_extensional_targetone. (((G) = (((((dst_positive_code_extensional_targetone) + (dst_positive_scale_extensional_targetone)) * S ((dst_positive_code_extensional_targetone) + (dst_positive_scale_extensional_targetone)) + ((dst_positive_scale_extensional_targetone) + (dst_positive_scale_extensional_targetone))) + (((dst_negative_code_extensional_targetone) + (dst_negative_scale_extensional_targetone)) * S ((dst_negative_code_extensional_targetone) + (dst_negative_scale_extensional_targetone)) + ((dst_negative_scale_extensional_targetone) + (dst_negative_scale_extensional_targetone)))) * S ((((dst_positive_code_extensional_targetone) + (dst_positive_scale_extensional_targetone)) * S ((dst_positive_code_extensional_targetone) + (dst_positive_scale_extensional_targetone)) + ((dst_positive_scale_extensional_targetone) + (dst_positive_scale_extensional_targetone))) + (((dst_negative_code_extensional_targetone) + (dst_negative_scale_extensional_targetone)) * S ((dst_negative_code_extensional_targetone) + (dst_negative_scale_extensional_targetone)) + ((dst_negative_scale_extensional_targetone) + (dst_negative_scale_extensional_targetone)))) + ((((dst_negative_code_extensional_targetone) + (dst_negative_scale_extensional_targetone)) * S ((dst_negative_code_extensional_targetone) + (dst_negative_scale_extensional_targetone)) + ((dst_negative_scale_extensional_targetone) + (dst_negative_scale_extensional_targetone))) + (((dst_negative_code_extensional_targetone) + (dst_negative_scale_extensional_targetone)) * S ((dst_negative_code_extensional_targetone) + (dst_negative_scale_extensional_targetone)) + ((dst_negative_scale_extensional_targetone) + (dst_negative_scale_extensional_targetone)))))) /\ (((((exists ff_h_pvs_extensional_targetonepositive. ff_h_pvs_extensional_targetonepositive + S (dst_positive_extensional_targetone) = S ((S (1)) * dst_positive_scale_extensional_targetone)) /\ exists ff_q_pvs_extensional_targetonepositive. dst_positive_code_extensional_targetone = ff_q_pvs_extensional_targetonepositive * S ((S (1)) * dst_positive_scale_extensional_targetone) + (dst_positive_extensional_targetone))) /\ (((((exists ff_h_pvs_extensional_targetonenegative. ff_h_pvs_extensional_targetonenegative + S (dst_negative_extensional_targetone) = S ((S (1)) * dst_negative_scale_extensional_targetone)) /\ exists ff_q_pvs_extensional_targetonenegative. dst_negative_code_extensional_targetone = ff_q_pvs_extensional_targetonenegative * S ((S (1)) * dst_negative_scale_extensional_targetone) + (dst_negative_extensional_targetone))) /\ (exists ge_balance_positive_extensional_targetonevalue ge_balance_negative_extensional_targetonevalue. (((((2) = 2 * (ge_balance_positive_extensional_targetonevalue) /\ (ge_balance_negative_extensional_targetonevalue) = 0) \/ exists ge_signed_half_extensional_targetonevaluedecode. (((2) = 2 * ge_signed_half_extensional_targetonevaluedecode + 1 /\ (ge_balance_positive_extensional_targetonevalue) = 0) /\ (ge_balance_negative_extensional_targetonevalue) = S ge_signed_half_extensional_targetonevaluedecode))) /\ ((dst_positive_extensional_targetone) + ge_balance_negative_extensional_targetonevalue = (dst_negative_extensional_targetone) + ge_balance_positive_extensional_targetonevalue))))))))) /\ (forall mp_a_extensional_target mp_b_extensional_target mp_x_extensional_target mp_y_extensional_target mp_z_extensional_target. ~(mp_a_extensional_target=0) -> ~(mp_b_extensional_target=0) -> (exists pvs_le_gap_extensional_targetbound. pvs_le_gap_extensional_targetbound + (mp_a_extensional_target*mp_b_extensional_target) = (N)) -> (forall frp_divisor_extensional_targetcoprime. (exists frp_left_factor_extensional_targetcoprime. mp_a_extensional_target = frp_divisor_extensional_targetcoprime * frp_left_factor_extensional_targetcoprime) -> (exists frp_right_factor_extensional_targetcoprime. mp_b_extensional_target = frp_divisor_extensional_targetcoprime * frp_right_factor_extensional_targetcoprime) -> frp_divisor_extensional_targetcoprime = 1) -> (exists dst_positive_code_extensional_targetfirst dst_positive_scale_extensional_targetfirst dst_negative_code_extensional_targetfirst dst_negative_scale_extensional_targetfirst dst_positive_extensional_targetfirst dst_negative_extensional_targetfirst. (((G) = (((((dst_positive_code_extensional_targetfirst) + (dst_positive_scale_extensional_targetfirst)) * S ((dst_positive_code_extensional_targetfirst) + (dst_positive_scale_extensional_targetfirst)) + ((dst_positive_scale_extensional_targetfirst) + (dst_positive_scale_extensional_targetfirst))) + (((dst_negative_code_extensional_targetfirst) + (dst_negative_scale_extensional_targetfirst)) * S ((dst_negative_code_extensional_targetfirst) + (dst_negative_scale_extensional_targetfirst)) + ((dst_negative_scale_extensional_targetfirst) + (dst_negative_scale_extensional_targetfirst)))) * S ((((dst_positive_code_extensional_targetfirst) + (dst_positive_scale_extensional_targetfirst)) * S ((dst_positive_code_extensional_targetfirst) + (dst_positive_scale_extensional_targetfirst)) + ((dst_positive_scale_extensional_targetfirst) + (dst_positive_scale_extensional_targetfirst))) + (((dst_negative_code_extensional_targetfirst) + (dst_negative_scale_extensional_targetfirst)) * S ((dst_negative_code_extensional_targetfirst) + (dst_negative_scale_extensional_targetfirst)) + ((dst_negative_scale_extensional_targetfirst) + (dst_negative_scale_extensional_targetfirst)))) + ((((dst_negative_code_extensional_targetfirst) + (dst_negative_scale_extensional_targetfirst)) * S ((dst_negative_code_extensional_targetfirst) + (dst_negative_scale_extensional_targetfirst)) + ((dst_negative_scale_extensional_targetfirst) + (dst_negative_scale_extensional_targetfirst))) + (((dst_negative_code_extensional_targetfirst) + (dst_negative_scale_extensional_targetfirst)) * S ((dst_negative_code_extensional_targetfirst) + (dst_negative_scale_extensional_targetfirst)) + ((dst_negative_scale_extensional_targetfirst) + (dst_negative_scale_extensional_targetfirst)))))) /\ (((((exists ff_h_pvs_extensional_targetfirstpositive. ff_h_pvs_extensional_targetfirstpositive + S (dst_positive_extensional_targetfirst) = S ((S (mp_a_extensional_target)) * dst_positive_scale_extensional_targetfirst)) /\ exists ff_q_pvs_extensional_targetfirstpositive. dst_positive_code_extensional_targetfirst = ff_q_pvs_extensional_targetfirstpositive * S ((S (mp_a_extensional_target)) * dst_positive_scale_extensional_targetfirst) + (dst_positive_extensional_targetfirst))) /\ (((((exists ff_h_pvs_extensional_targetfirstnegative. ff_h_pvs_extensional_targetfirstnegative + S (dst_negative_extensional_targetfirst) = S ((S (mp_a_extensional_target)) * dst_negative_scale_extensional_targetfirst)) /\ exists ff_q_pvs_extensional_targetfirstnegative. dst_negative_code_extensional_targetfirst = ff_q_pvs_extensional_targetfirstnegative * S ((S (mp_a_extensional_target)) * dst_negative_scale_extensional_targetfirst) + (dst_negative_extensional_targetfirst))) /\ (exists ge_balance_positive_extensional_targetfirstvalue ge_balance_negative_extensional_targetfirstvalue. (((((mp_x_extensional_target) = 2 * (ge_balance_positive_extensional_targetfirstvalue) /\ (ge_balance_negative_extensional_targetfirstvalue) = 0) \/ exists ge_signed_half_extensional_targetfirstvaluedecode. (((mp_x_extensional_target) = 2 * ge_signed_half_extensional_targetfirstvaluedecode + 1 /\ (ge_balance_positive_extensional_targetfirstvalue) = 0) /\ (ge_balance_negative_extensional_targetfirstvalue) = S ge_signed_half_extensional_targetfirstvaluedecode))) /\ ((dst_positive_extensional_targetfirst) + ge_balance_negative_extensional_targetfirstvalue = (dst_negative_extensional_targetfirst) + ge_balance_positive_extensional_targetfirstvalue))))))))) -> (exists dst_positive_code_extensional_targetsecond dst_positive_scale_extensional_targetsecond dst_negative_code_extensional_targetsecond dst_negative_scale_extensional_targetsecond dst_positive_extensional_targetsecond dst_negative_extensional_targetsecond. (((G) = (((((dst_positive_code_extensional_targetsecond) + (dst_positive_scale_extensional_targetsecond)) * S ((dst_positive_code_extensional_targetsecond) + (dst_positive_scale_extensional_targetsecond)) + ((dst_positive_scale_extensional_targetsecond) + (dst_positive_scale_extensional_targetsecond))) + (((dst_negative_code_extensional_targetsecond) + (dst_negative_scale_extensional_targetsecond)) * S ((dst_negative_code_extensional_targetsecond) + (dst_negative_scale_extensional_targetsecond)) + ((dst_negative_scale_extensional_targetsecond) + (dst_negative_scale_extensional_targetsecond)))) * S ((((dst_positive_code_extensional_targetsecond) + (dst_positive_scale_extensional_targetsecond)) * S ((dst_positive_code_extensional_targetsecond) + (dst_positive_scale_extensional_targetsecond)) + ((dst_positive_scale_extensional_targetsecond) + (dst_positive_scale_extensional_targetsecond))) + (((dst_negative_code_extensional_targetsecond) + (dst_negative_scale_extensional_targetsecond)) * S ((dst_negative_code_extensional_targetsecond) + (dst_negative_scale_extensional_targetsecond)) + ((dst_negative_scale_extensional_targetsecond) + (dst_negative_scale_extensional_targetsecond)))) + ((((dst_negative_code_extensional_targetsecond) + (dst_negative_scale_extensional_targetsecond)) * S ((dst_negative_code_extensional_targetsecond) + (dst_negative_scale_extensional_targetsecond)) + ((dst_negative_scale_extensional_targetsecond) + (dst_negative_scale_extensional_targetsecond))) + (((dst_negative_code_extensional_targetsecond) + (dst_negative_scale_extensional_targetsecond)) * S ((dst_negative_code_extensional_targetsecond) + (dst_negative_scale_extensional_targetsecond)) + ((dst_negative_scale_extensional_targetsecond) + (dst_negative_scale_extensional_targetsecond)))))) /\ (((((exists ff_h_pvs_extensional_targetsecondpositive. ff_h_pvs_extensional_targetsecondpositive + S (dst_positive_extensional_targetsecond) = S ((S (mp_b_extensional_target)) * dst_positive_scale_extensional_targetsecond)) /\ exists ff_q_pvs_extensional_targetsecondpositive. dst_positive_code_extensional_targetsecond = ff_q_pvs_extensional_targetsecondpositive * S ((S (mp_b_extensional_target)) * dst_positive_scale_extensional_targetsecond) + (dst_positive_extensional_targetsecond))) /\ (((((exists ff_h_pvs_extensional_targetsecondnegative. ff_h_pvs_extensional_targetsecondnegative + S (dst_negative_extensional_targetsecond) = S ((S (mp_b_extensional_target)) * dst_negative_scale_extensional_targetsecond)) /\ exists ff_q_pvs_extensional_targetsecondnegative. dst_negative_code_extensional_targetsecond = ff_q_pvs_extensional_targetsecondnegative * S ((S (mp_b_extensional_target)) * dst_negative_scale_extensional_targetsecond) + (dst_negative_extensional_targetsecond))) /\ (exists ge_balance_positive_extensional_targetsecondvalue ge_balance_negative_extensional_targetsecondvalue. (((((mp_y_extensional_target) = 2 * (ge_balance_positive_extensional_targetsecondvalue) /\ (ge_balance_negative_extensional_targetsecondvalue) = 0) \/ exists ge_signed_half_extensional_targetsecondvaluedecode. (((mp_y_extensional_target) = 2 * ge_signed_half_extensional_targetsecondvaluedecode + 1 /\ (ge_balance_positive_extensional_targetsecondvalue) = 0) /\ (ge_balance_negative_extensional_targetsecondvalue) = S ge_signed_half_extensional_targetsecondvaluedecode))) /\ ((dst_positive_extensional_targetsecond) + ge_balance_negative_extensional_targetsecondvalue = (dst_negative_extensional_targetsecond) + ge_balance_positive_extensional_targetsecondvalue))))))))) -> (exists dst_positive_code_extensional_targetproduct dst_positive_scale_extensional_targetproduct dst_negative_code_extensional_targetproduct dst_negative_scale_extensional_targetproduct dst_positive_extensional_targetproduct dst_negative_extensional_targetproduct. (((G) = (((((dst_positive_code_extensional_targetproduct) + (dst_positive_scale_extensional_targetproduct)) * S ((dst_positive_code_extensional_targetproduct) + (dst_positive_scale_extensional_targetproduct)) + ((dst_positive_scale_extensional_targetproduct) + (dst_positive_scale_extensional_targetproduct))) + (((dst_negative_code_extensional_targetproduct) + (dst_negative_scale_extensional_targetproduct)) * S ((dst_negative_code_extensional_targetproduct) + (dst_negative_scale_extensional_targetproduct)) + ((dst_negative_scale_extensional_targetproduct) + (dst_negative_scale_extensional_targetproduct)))) * S ((((dst_positive_code_extensional_targetproduct) + (dst_positive_scale_extensional_targetproduct)) * S ((dst_positive_code_extensional_targetproduct) + (dst_positive_scale_extensional_targetproduct)) + ((dst_positive_scale_extensional_targetproduct) + (dst_positive_scale_extensional_targetproduct))) + (((dst_negative_code_extensional_targetproduct) + (dst_negative_scale_extensional_targetproduct)) * S ((dst_negative_code_extensional_targetproduct) + (dst_negative_scale_extensional_targetproduct)) + ((dst_negative_scale_extensional_targetproduct) + (dst_negative_scale_extensional_targetproduct)))) + ((((dst_negative_code_extensional_targetproduct) + (dst_negative_scale_extensional_targetproduct)) * S ((dst_negative_code_extensional_targetproduct) + (dst_negative_scale_extensional_targetproduct)) + ((dst_negative_scale_extensional_targetproduct) + (dst_negative_scale_extensional_targetproduct))) + (((dst_negative_code_extensional_targetproduct) + (dst_negative_scale_extensional_targetproduct)) * S ((dst_negative_code_extensional_targetproduct) + (dst_negative_scale_extensional_targetproduct)) + ((dst_negative_scale_extensional_targetproduct) + (dst_negative_scale_extensional_targetproduct)))))) /\ (((((exists ff_h_pvs_extensional_targetproductpositive. ff_h_pvs_extensional_targetproductpositive + S (dst_positive_extensional_targetproduct) = S ((S (mp_a_extensional_target*mp_b_extensional_target)) * dst_positive_scale_extensional_targetproduct)) /\ exists ff_q_pvs_extensional_targetproductpositive. dst_positive_code_extensional_targetproduct = ff_q_pvs_extensional_targetproductpositive * S ((S (mp_a_extensional_target*mp_b_extensional_target)) * dst_positive_scale_extensional_targetproduct) + (dst_positive_extensional_targetproduct))) /\ (((((exists ff_h_pvs_extensional_targetproductnegative. ff_h_pvs_extensional_targetproductnegative + S (dst_negative_extensional_targetproduct) = S ((S (mp_a_extensional_target*mp_b_extensional_target)) * dst_negative_scale_extensional_targetproduct)) /\ exists ff_q_pvs_extensional_targetproductnegative. dst_negative_code_extensional_targetproduct = ff_q_pvs_extensional_targetproductnegative * S ((S (mp_a_extensional_target*mp_b_extensional_target)) * dst_negative_scale_extensional_targetproduct) + (dst_negative_extensional_targetproduct))) /\ (exists ge_balance_positive_extensional_targetproductvalue ge_balance_negative_extensional_targetproductvalue. (((((mp_z_extensional_target) = 2 * (ge_balance_positive_extensional_targetproductvalue) /\ (ge_balance_negative_extensional_targetproductvalue) = 0) \/ exists ge_signed_half_extensional_targetproductvaluedecode. (((mp_z_extensional_target) = 2 * ge_signed_half_extensional_targetproductvaluedecode + 1 /\ (ge_balance_positive_extensional_targetproductvalue) = 0) /\ (ge_balance_negative_extensional_targetproductvalue) = S ge_signed_half_extensional_targetproductvaluedecode))) /\ ((dst_positive_extensional_targetproduct) + ge_balance_negative_extensional_targetproductvalue = (dst_negative_extensional_targetproduct) + ge_balance_positive_extensional_targetproductvalue))))))))) -> (exists sto_ap_extensional_targetlaw sto_an_extensional_targetlaw sto_bp_extensional_targetlaw sto_bn_extensional_targetlaw sto_cp_extensional_targetlaw sto_cn_extensional_targetlaw. (((((mp_x_extensional_target) = 2 * (sto_ap_extensional_targetlaw) /\ (sto_an_extensional_targetlaw) = 0) \/ exists ge_signed_half_extensional_targetlawleft. (((mp_x_extensional_target) = 2 * ge_signed_half_extensional_targetlawleft + 1 /\ (sto_ap_extensional_targetlaw) = 0) /\ (sto_an_extensional_targetlaw) = S ge_signed_half_extensional_targetlawleft))) /\ ((((((mp_y_extensional_target) = 2 * (sto_bp_extensional_targetlaw) /\ (sto_bn_extensional_targetlaw) = 0) \/ exists ge_signed_half_extensional_targetlawright. (((mp_y_extensional_target) = 2 * ge_signed_half_extensional_targetlawright + 1 /\ (sto_bp_extensional_targetlaw) = 0) /\ (sto_bn_extensional_targetlaw) = S ge_signed_half_extensional_targetlawright))) /\ ((((((mp_z_extensional_target) = 2 * (sto_cp_extensional_targetlaw) /\ (sto_cn_extensional_targetlaw) = 0) \/ exists ge_signed_half_extensional_targetlawoutput. (((mp_z_extensional_target) = 2 * ge_signed_half_extensional_targetlawoutput + 1 /\ (sto_cp_extensional_targetlaw) = 0) /\ (sto_cn_extensional_targetlaw) = S ge_signed_half_extensional_targetlawoutput))) /\ ((sto_ap_extensional_targetlaw * sto_bp_extensional_targetlaw + sto_an_extensional_targetlaw * sto_bn_extensional_targetlaw) + sto_cn_extensional_targetlaw = (sto_ap_extensional_targetlaw * sto_bn_extensional_targetlaw + sto_an_extensional_targetlaw * sto_bp_extensional_targetlaw) + sto_cp_extensional_targetlaw))))))))))))))