signed_multiplicative_table

Exact expanded first-order arithmetic statement

forall N F. (((~((N)=0)) /\ (((exists dst_positive_code_signed_multiplicative_tabletable dst_positive_scale_signed_multiplicative_tabletable dst_negative_code_signed_multiplicative_tabletable dst_negative_scale_signed_multiplicative_tabletable. (((F) = (((((dst_positive_code_signed_multiplicative_tabletable) + (dst_positive_scale_signed_multiplicative_tabletable)) * S ((dst_positive_code_signed_multiplicative_tabletable) + (dst_positive_scale_signed_multiplicative_tabletable)) + ((dst_positive_scale_signed_multiplicative_tabletable) + (dst_positive_scale_signed_multiplicative_tabletable))) + (((dst_negative_code_signed_multiplicative_tabletable) + (dst_negative_scale_signed_multiplicative_tabletable)) * S ((dst_negative_code_signed_multiplicative_tabletable) + (dst_negative_scale_signed_multiplicative_tabletable)) + ((dst_negative_scale_signed_multiplicative_tabletable) + (dst_negative_scale_signed_multiplicative_tabletable)))) * S ((((dst_positive_code_signed_multiplicative_tabletable) + (dst_positive_scale_signed_multiplicative_tabletable)) * S ((dst_positive_code_signed_multiplicative_tabletable) + (dst_positive_scale_signed_multiplicative_tabletable)) + ((dst_positive_scale_signed_multiplicative_tabletable) + (dst_positive_scale_signed_multiplicative_tabletable))) + (((dst_negative_code_signed_multiplicative_tabletable) + (dst_negative_scale_signed_multiplicative_tabletable)) * S ((dst_negative_code_signed_multiplicative_tabletable) + (dst_negative_scale_signed_multiplicative_tabletable)) + ((dst_negative_scale_signed_multiplicative_tabletable) + (dst_negative_scale_signed_multiplicative_tabletable)))) + ((((dst_negative_code_signed_multiplicative_tabletable) + (dst_negative_scale_signed_multiplicative_tabletable)) * S ((dst_negative_code_signed_multiplicative_tabletable) + (dst_negative_scale_signed_multiplicative_tabletable)) + ((dst_negative_scale_signed_multiplicative_tabletable) + (dst_negative_scale_signed_multiplicative_tabletable))) + (((dst_negative_code_signed_multiplicative_tabletable) + (dst_negative_scale_signed_multiplicative_tabletable)) * S ((dst_negative_code_signed_multiplicative_tabletable) + (dst_negative_scale_signed_multiplicative_tabletable)) + ((dst_negative_scale_signed_multiplicative_tabletable) + (dst_negative_scale_signed_multiplicative_tabletable)))))) /\ (forall dst_index_signed_multiplicative_tabletable. (exists pvs_le_gap_signed_multiplicative_tabletabledomain. pvs_le_gap_signed_multiplicative_tabletabledomain + (dst_index_signed_multiplicative_tabletable) = (N)) -> exists dst_positive_signed_multiplicative_tabletable dst_negative_signed_multiplicative_tabletable dst_value_signed_multiplicative_tabletable. ((((exists ff_h_pvs_signed_multiplicative_tabletableentrypositive. ff_h_pvs_signed_multiplicative_tabletableentrypositive + S (dst_positive_signed_multiplicative_tabletable) = S ((S (dst_index_signed_multiplicative_tabletable)) * dst_positive_scale_signed_multiplicative_tabletable)) /\ exists ff_q_pvs_signed_multiplicative_tabletableentrypositive. dst_positive_code_signed_multiplicative_tabletable = ff_q_pvs_signed_multiplicative_tabletableentrypositive * S ((S (dst_index_signed_multiplicative_tabletable)) * dst_positive_scale_signed_multiplicative_tabletable) + (dst_positive_signed_multiplicative_tabletable))) /\ (((((exists ff_h_pvs_signed_multiplicative_tabletableentrynegative. ff_h_pvs_signed_multiplicative_tabletableentrynegative + S (dst_negative_signed_multiplicative_tabletable) = S ((S (dst_index_signed_multiplicative_tabletable)) * dst_negative_scale_signed_multiplicative_tabletable)) /\ exists ff_q_pvs_signed_multiplicative_tabletableentrynegative. dst_negative_code_signed_multiplicative_tabletable = ff_q_pvs_signed_multiplicative_tabletableentrynegative * S ((S (dst_index_signed_multiplicative_tabletable)) * dst_negative_scale_signed_multiplicative_tabletable) + (dst_negative_signed_multiplicative_tabletable))) /\ (exists ge_balance_positive_signed_multiplicative_tabletableentryvalue ge_balance_negative_signed_multiplicative_tabletableentryvalue. (((((dst_value_signed_multiplicative_tabletable) = 2 * (ge_balance_positive_signed_multiplicative_tabletableentryvalue) /\ (ge_balance_negative_signed_multiplicative_tabletableentryvalue) = 0) \/ exists ge_signed_half_signed_multiplicative_tabletableentryvaluedecode. (((dst_value_signed_multiplicative_tabletable) = 2 * ge_signed_half_signed_multiplicative_tabletableentryvaluedecode + 1 /\ (ge_balance_positive_signed_multiplicative_tabletableentryvalue) = 0) /\ (ge_balance_negative_signed_multiplicative_tabletableentryvalue) = S ge_signed_half_signed_multiplicative_tabletableentryvaluedecode))) /\ ((dst_positive_signed_multiplicative_tabletable) + ge_balance_negative_signed_multiplicative_tabletableentryvalue = (dst_negative_signed_multiplicative_tabletable) + ge_balance_positive_signed_multiplicative_tabletableentryvalue))))))))) /\ (((exists dst_positive_code_signed_multiplicative_tableone dst_positive_scale_signed_multiplicative_tableone dst_negative_code_signed_multiplicative_tableone dst_negative_scale_signed_multiplicative_tableone dst_positive_signed_multiplicative_tableone dst_negative_signed_multiplicative_tableone. (((F) = (((((dst_positive_code_signed_multiplicative_tableone) + (dst_positive_scale_signed_multiplicative_tableone)) * S ((dst_positive_code_signed_multiplicative_tableone) + (dst_positive_scale_signed_multiplicative_tableone)) + ((dst_positive_scale_signed_multiplicative_tableone) + (dst_positive_scale_signed_multiplicative_tableone))) + (((dst_negative_code_signed_multiplicative_tableone) + (dst_negative_scale_signed_multiplicative_tableone)) * S ((dst_negative_code_signed_multiplicative_tableone) + (dst_negative_scale_signed_multiplicative_tableone)) + ((dst_negative_scale_signed_multiplicative_tableone) + (dst_negative_scale_signed_multiplicative_tableone)))) * S ((((dst_positive_code_signed_multiplicative_tableone) + (dst_positive_scale_signed_multiplicative_tableone)) * S ((dst_positive_code_signed_multiplicative_tableone) + (dst_positive_scale_signed_multiplicative_tableone)) + ((dst_positive_scale_signed_multiplicative_tableone) + (dst_positive_scale_signed_multiplicative_tableone))) + (((dst_negative_code_signed_multiplicative_tableone) + (dst_negative_scale_signed_multiplicative_tableone)) * S ((dst_negative_code_signed_multiplicative_tableone) + (dst_negative_scale_signed_multiplicative_tableone)) + ((dst_negative_scale_signed_multiplicative_tableone) + (dst_negative_scale_signed_multiplicative_tableone)))) + ((((dst_negative_code_signed_multiplicative_tableone) + (dst_negative_scale_signed_multiplicative_tableone)) * S ((dst_negative_code_signed_multiplicative_tableone) + (dst_negative_scale_signed_multiplicative_tableone)) + ((dst_negative_scale_signed_multiplicative_tableone) + (dst_negative_scale_signed_multiplicative_tableone))) + (((dst_negative_code_signed_multiplicative_tableone) + (dst_negative_scale_signed_multiplicative_tableone)) * S ((dst_negative_code_signed_multiplicative_tableone) + (dst_negative_scale_signed_multiplicative_tableone)) + ((dst_negative_scale_signed_multiplicative_tableone) + (dst_negative_scale_signed_multiplicative_tableone)))))) /\ (((((exists ff_h_pvs_signed_multiplicative_tableonepositive. ff_h_pvs_signed_multiplicative_tableonepositive + S (dst_positive_signed_multiplicative_tableone) = S ((S (1)) * dst_positive_scale_signed_multiplicative_tableone)) /\ exists ff_q_pvs_signed_multiplicative_tableonepositive. dst_positive_code_signed_multiplicative_tableone = ff_q_pvs_signed_multiplicative_tableonepositive * S ((S (1)) * dst_positive_scale_signed_multiplicative_tableone) + (dst_positive_signed_multiplicative_tableone))) /\ (((((exists ff_h_pvs_signed_multiplicative_tableonenegative. ff_h_pvs_signed_multiplicative_tableonenegative + S (dst_negative_signed_multiplicative_tableone) = S ((S (1)) * dst_negative_scale_signed_multiplicative_tableone)) /\ exists ff_q_pvs_signed_multiplicative_tableonenegative. dst_negative_code_signed_multiplicative_tableone = ff_q_pvs_signed_multiplicative_tableonenegative * S ((S (1)) * dst_negative_scale_signed_multiplicative_tableone) + (dst_negative_signed_multiplicative_tableone))) /\ (exists ge_balance_positive_signed_multiplicative_tableonevalue ge_balance_negative_signed_multiplicative_tableonevalue. (((((2) = 2 * (ge_balance_positive_signed_multiplicative_tableonevalue) /\ (ge_balance_negative_signed_multiplicative_tableonevalue) = 0) \/ exists ge_signed_half_signed_multiplicative_tableonevaluedecode. (((2) = 2 * ge_signed_half_signed_multiplicative_tableonevaluedecode + 1 /\ (ge_balance_positive_signed_multiplicative_tableonevalue) = 0) /\ (ge_balance_negative_signed_multiplicative_tableonevalue) = S ge_signed_half_signed_multiplicative_tableonevaluedecode))) /\ ((dst_positive_signed_multiplicative_tableone) + ge_balance_negative_signed_multiplicative_tableonevalue = (dst_negative_signed_multiplicative_tableone) + ge_balance_positive_signed_multiplicative_tableonevalue))))))))) /\ (forall mp_a_signed_multiplicative_table mp_b_signed_multiplicative_table mp_x_signed_multiplicative_table mp_y_signed_multiplicative_table mp_z_signed_multiplicative_table. ~(mp_a_signed_multiplicative_table=0) -> ~(mp_b_signed_multiplicative_table=0) -> (exists pvs_le_gap_signed_multiplicative_tablebound. pvs_le_gap_signed_multiplicative_tablebound + (mp_a_signed_multiplicative_table*mp_b_signed_multiplicative_table) = (N)) -> (forall frp_divisor_signed_multiplicative_tablecoprime. (exists frp_left_factor_signed_multiplicative_tablecoprime. mp_a_signed_multiplicative_table = frp_divisor_signed_multiplicative_tablecoprime * frp_left_factor_signed_multiplicative_tablecoprime) -> (exists frp_right_factor_signed_multiplicative_tablecoprime. mp_b_signed_multiplicative_table = frp_divisor_signed_multiplicative_tablecoprime * frp_right_factor_signed_multiplicative_tablecoprime) -> frp_divisor_signed_multiplicative_tablecoprime = 1) -> (exists dst_positive_code_signed_multiplicative_tablefirst dst_positive_scale_signed_multiplicative_tablefirst dst_negative_code_signed_multiplicative_tablefirst dst_negative_scale_signed_multiplicative_tablefirst dst_positive_signed_multiplicative_tablefirst dst_negative_signed_multiplicative_tablefirst. (((F) = (((((dst_positive_code_signed_multiplicative_tablefirst) + (dst_positive_scale_signed_multiplicative_tablefirst)) * S ((dst_positive_code_signed_multiplicative_tablefirst) + (dst_positive_scale_signed_multiplicative_tablefirst)) + ((dst_positive_scale_signed_multiplicative_tablefirst) + (dst_positive_scale_signed_multiplicative_tablefirst))) + (((dst_negative_code_signed_multiplicative_tablefirst) + (dst_negative_scale_signed_multiplicative_tablefirst)) * S ((dst_negative_code_signed_multiplicative_tablefirst) + (dst_negative_scale_signed_multiplicative_tablefirst)) + ((dst_negative_scale_signed_multiplicative_tablefirst) + (dst_negative_scale_signed_multiplicative_tablefirst)))) * S ((((dst_positive_code_signed_multiplicative_tablefirst) + (dst_positive_scale_signed_multiplicative_tablefirst)) * S ((dst_positive_code_signed_multiplicative_tablefirst) + (dst_positive_scale_signed_multiplicative_tablefirst)) + ((dst_positive_scale_signed_multiplicative_tablefirst) + (dst_positive_scale_signed_multiplicative_tablefirst))) + (((dst_negative_code_signed_multiplicative_tablefirst) + (dst_negative_scale_signed_multiplicative_tablefirst)) * S ((dst_negative_code_signed_multiplicative_tablefirst) + (dst_negative_scale_signed_multiplicative_tablefirst)) + ((dst_negative_scale_signed_multiplicative_tablefirst) + (dst_negative_scale_signed_multiplicative_tablefirst)))) + ((((dst_negative_code_signed_multiplicative_tablefirst) + (dst_negative_scale_signed_multiplicative_tablefirst)) * S ((dst_negative_code_signed_multiplicative_tablefirst) + (dst_negative_scale_signed_multiplicative_tablefirst)) + ((dst_negative_scale_signed_multiplicative_tablefirst) + (dst_negative_scale_signed_multiplicative_tablefirst))) + (((dst_negative_code_signed_multiplicative_tablefirst) + (dst_negative_scale_signed_multiplicative_tablefirst)) * S ((dst_negative_code_signed_multiplicative_tablefirst) + (dst_negative_scale_signed_multiplicative_tablefirst)) + ((dst_negative_scale_signed_multiplicative_tablefirst) + (dst_negative_scale_signed_multiplicative_tablefirst)))))) /\ (((((exists ff_h_pvs_signed_multiplicative_tablefirstpositive. ff_h_pvs_signed_multiplicative_tablefirstpositive + S (dst_positive_signed_multiplicative_tablefirst) = S ((S (mp_a_signed_multiplicative_table)) * dst_positive_scale_signed_multiplicative_tablefirst)) /\ exists ff_q_pvs_signed_multiplicative_tablefirstpositive. dst_positive_code_signed_multiplicative_tablefirst = ff_q_pvs_signed_multiplicative_tablefirstpositive * S ((S (mp_a_signed_multiplicative_table)) * dst_positive_scale_signed_multiplicative_tablefirst) + (dst_positive_signed_multiplicative_tablefirst))) /\ (((((exists ff_h_pvs_signed_multiplicative_tablefirstnegative. ff_h_pvs_signed_multiplicative_tablefirstnegative + S (dst_negative_signed_multiplicative_tablefirst) = S ((S (mp_a_signed_multiplicative_table)) * dst_negative_scale_signed_multiplicative_tablefirst)) /\ exists ff_q_pvs_signed_multiplicative_tablefirstnegative. dst_negative_code_signed_multiplicative_tablefirst = ff_q_pvs_signed_multiplicative_tablefirstnegative * S ((S (mp_a_signed_multiplicative_table)) * dst_negative_scale_signed_multiplicative_tablefirst) + (dst_negative_signed_multiplicative_tablefirst))) /\ (exists ge_balance_positive_signed_multiplicative_tablefirstvalue ge_balance_negative_signed_multiplicative_tablefirstvalue. (((((mp_x_signed_multiplicative_table) = 2 * (ge_balance_positive_signed_multiplicative_tablefirstvalue) /\ (ge_balance_negative_signed_multiplicative_tablefirstvalue) = 0) \/ exists ge_signed_half_signed_multiplicative_tablefirstvaluedecode. (((mp_x_signed_multiplicative_table) = 2 * ge_signed_half_signed_multiplicative_tablefirstvaluedecode + 1 /\ (ge_balance_positive_signed_multiplicative_tablefirstvalue) = 0) /\ (ge_balance_negative_signed_multiplicative_tablefirstvalue) = S ge_signed_half_signed_multiplicative_tablefirstvaluedecode))) /\ ((dst_positive_signed_multiplicative_tablefirst) + ge_balance_negative_signed_multiplicative_tablefirstvalue = (dst_negative_signed_multiplicative_tablefirst) + ge_balance_positive_signed_multiplicative_tablefirstvalue))))))))) -> (exists dst_positive_code_signed_multiplicative_tablesecond dst_positive_scale_signed_multiplicative_tablesecond dst_negative_code_signed_multiplicative_tablesecond dst_negative_scale_signed_multiplicative_tablesecond dst_positive_signed_multiplicative_tablesecond dst_negative_signed_multiplicative_tablesecond. (((F) = (((((dst_positive_code_signed_multiplicative_tablesecond) + (dst_positive_scale_signed_multiplicative_tablesecond)) * S ((dst_positive_code_signed_multiplicative_tablesecond) + (dst_positive_scale_signed_multiplicative_tablesecond)) + ((dst_positive_scale_signed_multiplicative_tablesecond) + (dst_positive_scale_signed_multiplicative_tablesecond))) + (((dst_negative_code_signed_multiplicative_tablesecond) + (dst_negative_scale_signed_multiplicative_tablesecond)) * S ((dst_negative_code_signed_multiplicative_tablesecond) + (dst_negative_scale_signed_multiplicative_tablesecond)) + ((dst_negative_scale_signed_multiplicative_tablesecond) + (dst_negative_scale_signed_multiplicative_tablesecond)))) * S ((((dst_positive_code_signed_multiplicative_tablesecond) + (dst_positive_scale_signed_multiplicative_tablesecond)) * S ((dst_positive_code_signed_multiplicative_tablesecond) + (dst_positive_scale_signed_multiplicative_tablesecond)) + ((dst_positive_scale_signed_multiplicative_tablesecond) + (dst_positive_scale_signed_multiplicative_tablesecond))) + (((dst_negative_code_signed_multiplicative_tablesecond) + (dst_negative_scale_signed_multiplicative_tablesecond)) * S ((dst_negative_code_signed_multiplicative_tablesecond) + (dst_negative_scale_signed_multiplicative_tablesecond)) + ((dst_negative_scale_signed_multiplicative_tablesecond) + (dst_negative_scale_signed_multiplicative_tablesecond)))) + ((((dst_negative_code_signed_multiplicative_tablesecond) + (dst_negative_scale_signed_multiplicative_tablesecond)) * S ((dst_negative_code_signed_multiplicative_tablesecond) + (dst_negative_scale_signed_multiplicative_tablesecond)) + ((dst_negative_scale_signed_multiplicative_tablesecond) + (dst_negative_scale_signed_multiplicative_tablesecond))) + (((dst_negative_code_signed_multiplicative_tablesecond) + (dst_negative_scale_signed_multiplicative_tablesecond)) * S ((dst_negative_code_signed_multiplicative_tablesecond) + (dst_negative_scale_signed_multiplicative_tablesecond)) + ((dst_negative_scale_signed_multiplicative_tablesecond) + (dst_negative_scale_signed_multiplicative_tablesecond)))))) /\ (((((exists ff_h_pvs_signed_multiplicative_tablesecondpositive. ff_h_pvs_signed_multiplicative_tablesecondpositive + S (dst_positive_signed_multiplicative_tablesecond) = S ((S (mp_b_signed_multiplicative_table)) * dst_positive_scale_signed_multiplicative_tablesecond)) /\ exists ff_q_pvs_signed_multiplicative_tablesecondpositive. dst_positive_code_signed_multiplicative_tablesecond = ff_q_pvs_signed_multiplicative_tablesecondpositive * S ((S (mp_b_signed_multiplicative_table)) * dst_positive_scale_signed_multiplicative_tablesecond) + (dst_positive_signed_multiplicative_tablesecond))) /\ (((((exists ff_h_pvs_signed_multiplicative_tablesecondnegative. ff_h_pvs_signed_multiplicative_tablesecondnegative + S (dst_negative_signed_multiplicative_tablesecond) = S ((S (mp_b_signed_multiplicative_table)) * dst_negative_scale_signed_multiplicative_tablesecond)) /\ exists ff_q_pvs_signed_multiplicative_tablesecondnegative. dst_negative_code_signed_multiplicative_tablesecond = ff_q_pvs_signed_multiplicative_tablesecondnegative * S ((S (mp_b_signed_multiplicative_table)) * dst_negative_scale_signed_multiplicative_tablesecond) + (dst_negative_signed_multiplicative_tablesecond))) /\ (exists ge_balance_positive_signed_multiplicative_tablesecondvalue ge_balance_negative_signed_multiplicative_tablesecondvalue. (((((mp_y_signed_multiplicative_table) = 2 * (ge_balance_positive_signed_multiplicative_tablesecondvalue) /\ (ge_balance_negative_signed_multiplicative_tablesecondvalue) = 0) \/ exists ge_signed_half_signed_multiplicative_tablesecondvaluedecode. (((mp_y_signed_multiplicative_table) = 2 * ge_signed_half_signed_multiplicative_tablesecondvaluedecode + 1 /\ (ge_balance_positive_signed_multiplicative_tablesecondvalue) = 0) /\ (ge_balance_negative_signed_multiplicative_tablesecondvalue) = S ge_signed_half_signed_multiplicative_tablesecondvaluedecode))) /\ ((dst_positive_signed_multiplicative_tablesecond) + ge_balance_negative_signed_multiplicative_tablesecondvalue = (dst_negative_signed_multiplicative_tablesecond) + ge_balance_positive_signed_multiplicative_tablesecondvalue))))))))) -> (exists dst_positive_code_signed_multiplicative_tableproduct dst_positive_scale_signed_multiplicative_tableproduct dst_negative_code_signed_multiplicative_tableproduct dst_negative_scale_signed_multiplicative_tableproduct dst_positive_signed_multiplicative_tableproduct dst_negative_signed_multiplicative_tableproduct. (((F) = (((((dst_positive_code_signed_multiplicative_tableproduct) + (dst_positive_scale_signed_multiplicative_tableproduct)) * S ((dst_positive_code_signed_multiplicative_tableproduct) + (dst_positive_scale_signed_multiplicative_tableproduct)) + ((dst_positive_scale_signed_multiplicative_tableproduct) + (dst_positive_scale_signed_multiplicative_tableproduct))) + (((dst_negative_code_signed_multiplicative_tableproduct) + (dst_negative_scale_signed_multiplicative_tableproduct)) * S ((dst_negative_code_signed_multiplicative_tableproduct) + (dst_negative_scale_signed_multiplicative_tableproduct)) + ((dst_negative_scale_signed_multiplicative_tableproduct) + (dst_negative_scale_signed_multiplicative_tableproduct)))) * S ((((dst_positive_code_signed_multiplicative_tableproduct) + (dst_positive_scale_signed_multiplicative_tableproduct)) * S ((dst_positive_code_signed_multiplicative_tableproduct) + (dst_positive_scale_signed_multiplicative_tableproduct)) + ((dst_positive_scale_signed_multiplicative_tableproduct) + (dst_positive_scale_signed_multiplicative_tableproduct))) + (((dst_negative_code_signed_multiplicative_tableproduct) + (dst_negative_scale_signed_multiplicative_tableproduct)) * S ((dst_negative_code_signed_multiplicative_tableproduct) + (dst_negative_scale_signed_multiplicative_tableproduct)) + ((dst_negative_scale_signed_multiplicative_tableproduct) + (dst_negative_scale_signed_multiplicative_tableproduct)))) + ((((dst_negative_code_signed_multiplicative_tableproduct) + (dst_negative_scale_signed_multiplicative_tableproduct)) * S ((dst_negative_code_signed_multiplicative_tableproduct) + (dst_negative_scale_signed_multiplicative_tableproduct)) + ((dst_negative_scale_signed_multiplicative_tableproduct) + (dst_negative_scale_signed_multiplicative_tableproduct))) + (((dst_negative_code_signed_multiplicative_tableproduct) + (dst_negative_scale_signed_multiplicative_tableproduct)) * S ((dst_negative_code_signed_multiplicative_tableproduct) + (dst_negative_scale_signed_multiplicative_tableproduct)) + ((dst_negative_scale_signed_multiplicative_tableproduct) + (dst_negative_scale_signed_multiplicative_tableproduct)))))) /\ (((((exists ff_h_pvs_signed_multiplicative_tableproductpositive. ff_h_pvs_signed_multiplicative_tableproductpositive + S (dst_positive_signed_multiplicative_tableproduct) = S ((S (mp_a_signed_multiplicative_table*mp_b_signed_multiplicative_table)) * dst_positive_scale_signed_multiplicative_tableproduct)) /\ exists ff_q_pvs_signed_multiplicative_tableproductpositive. dst_positive_code_signed_multiplicative_tableproduct = ff_q_pvs_signed_multiplicative_tableproductpositive * S ((S (mp_a_signed_multiplicative_table*mp_b_signed_multiplicative_table)) * dst_positive_scale_signed_multiplicative_tableproduct) + (dst_positive_signed_multiplicative_tableproduct))) /\ (((((exists ff_h_pvs_signed_multiplicative_tableproductnegative. ff_h_pvs_signed_multiplicative_tableproductnegative + S (dst_negative_signed_multiplicative_tableproduct) = S ((S (mp_a_signed_multiplicative_table*mp_b_signed_multiplicative_table)) * dst_negative_scale_signed_multiplicative_tableproduct)) /\ exists ff_q_pvs_signed_multiplicative_tableproductnegative. dst_negative_code_signed_multiplicative_tableproduct = ff_q_pvs_signed_multiplicative_tableproductnegative * S ((S (mp_a_signed_multiplicative_table*mp_b_signed_multiplicative_table)) * dst_negative_scale_signed_multiplicative_tableproduct) + (dst_negative_signed_multiplicative_tableproduct))) /\ (exists ge_balance_positive_signed_multiplicative_tableproductvalue ge_balance_negative_signed_multiplicative_tableproductvalue. (((((mp_z_signed_multiplicative_table) = 2 * (ge_balance_positive_signed_multiplicative_tableproductvalue) /\ (ge_balance_negative_signed_multiplicative_tableproductvalue) = 0) \/ exists ge_signed_half_signed_multiplicative_tableproductvaluedecode. (((mp_z_signed_multiplicative_table) = 2 * ge_signed_half_signed_multiplicative_tableproductvaluedecode + 1 /\ (ge_balance_positive_signed_multiplicative_tableproductvalue) = 0) /\ (ge_balance_negative_signed_multiplicative_tableproductvalue) = S ge_signed_half_signed_multiplicative_tableproductvaluedecode))) /\ ((dst_positive_signed_multiplicative_tableproduct) + ge_balance_negative_signed_multiplicative_tableproductvalue = (dst_negative_signed_multiplicative_tableproduct) + ge_balance_positive_signed_multiplicative_tableproductvalue))))))))) -> (exists sto_ap_signed_multiplicative_tablelaw sto_an_signed_multiplicative_tablelaw sto_bp_signed_multiplicative_tablelaw sto_bn_signed_multiplicative_tablelaw sto_cp_signed_multiplicative_tablelaw sto_cn_signed_multiplicative_tablelaw. (((((mp_x_signed_multiplicative_table) = 2 * (sto_ap_signed_multiplicative_tablelaw) /\ (sto_an_signed_multiplicative_tablelaw) = 0) \/ exists ge_signed_half_signed_multiplicative_tablelawleft. (((mp_x_signed_multiplicative_table) = 2 * ge_signed_half_signed_multiplicative_tablelawleft + 1 /\ (sto_ap_signed_multiplicative_tablelaw) = 0) /\ (sto_an_signed_multiplicative_tablelaw) = S ge_signed_half_signed_multiplicative_tablelawleft))) /\ ((((((mp_y_signed_multiplicative_table) = 2 * (sto_bp_signed_multiplicative_tablelaw) /\ (sto_bn_signed_multiplicative_tablelaw) = 0) \/ exists ge_signed_half_signed_multiplicative_tablelawright. (((mp_y_signed_multiplicative_table) = 2 * ge_signed_half_signed_multiplicative_tablelawright + 1 /\ (sto_bp_signed_multiplicative_tablelaw) = 0) /\ (sto_bn_signed_multiplicative_tablelaw) = S ge_signed_half_signed_multiplicative_tablelawright))) /\ ((((((mp_z_signed_multiplicative_table) = 2 * (sto_cp_signed_multiplicative_tablelaw) /\ (sto_cn_signed_multiplicative_tablelaw) = 0) \/ exists ge_signed_half_signed_multiplicative_tablelawoutput. (((mp_z_signed_multiplicative_table) = 2 * ge_signed_half_signed_multiplicative_tablelawoutput + 1 /\ (sto_cp_signed_multiplicative_tablelaw) = 0) /\ (sto_cn_signed_multiplicative_tablelaw) = S ge_signed_half_signed_multiplicative_tablelawoutput))) /\ ((sto_ap_signed_multiplicative_tablelaw * sto_bp_signed_multiplicative_tablelaw + sto_an_signed_multiplicative_tablelaw * sto_bn_signed_multiplicative_tablelaw) + sto_cn_signed_multiplicative_tablelaw = (sto_ap_signed_multiplicative_tablelaw * sto_bn_signed_multiplicative_tablelaw + sto_an_signed_multiplicative_tablelaw * sto_bp_signed_multiplicative_tablelaw) + sto_cp_signed_multiplicative_tablelaw)))))))))))))) -> (exists dst_positive_code_project_table dst_positive_scale_project_table dst_negative_code_project_table dst_negative_scale_project_table. (((F) = (((((dst_positive_code_project_table) + (dst_positive_scale_project_table)) * S ((dst_positive_code_project_table) + (dst_positive_scale_project_table)) + ((dst_positive_scale_project_table) + (dst_positive_scale_project_table))) + (((dst_negative_code_project_table) + (dst_negative_scale_project_table)) * S ((dst_negative_code_project_table) + (dst_negative_scale_project_table)) + ((dst_negative_scale_project_table) + (dst_negative_scale_project_table)))) * S ((((dst_positive_code_project_table) + (dst_positive_scale_project_table)) * S ((dst_positive_code_project_table) + (dst_positive_scale_project_table)) + ((dst_positive_scale_project_table) + (dst_positive_scale_project_table))) + (((dst_negative_code_project_table) + (dst_negative_scale_project_table)) * S ((dst_negative_code_project_table) + (dst_negative_scale_project_table)) + ((dst_negative_scale_project_table) + (dst_negative_scale_project_table)))) + ((((dst_negative_code_project_table) + (dst_negative_scale_project_table)) * S ((dst_negative_code_project_table) + (dst_negative_scale_project_table)) + ((dst_negative_scale_project_table) + (dst_negative_scale_project_table))) + (((dst_negative_code_project_table) + (dst_negative_scale_project_table)) * S ((dst_negative_code_project_table) + (dst_negative_scale_project_table)) + ((dst_negative_scale_project_table) + (dst_negative_scale_project_table)))))) /\ (forall dst_index_project_table. (exists pvs_le_gap_project_tabledomain. pvs_le_gap_project_tabledomain + (dst_index_project_table) = (N)) -> exists dst_positive_project_table dst_negative_project_table dst_value_project_table. ((((exists ff_h_pvs_project_tableentrypositive. ff_h_pvs_project_tableentrypositive + S (dst_positive_project_table) = S ((S (dst_index_project_table)) * dst_positive_scale_project_table)) /\ exists ff_q_pvs_project_tableentrypositive. dst_positive_code_project_table = ff_q_pvs_project_tableentrypositive * S ((S (dst_index_project_table)) * dst_positive_scale_project_table) + (dst_positive_project_table))) /\ (((((exists ff_h_pvs_project_tableentrynegative. ff_h_pvs_project_tableentrynegative + S (dst_negative_project_table) = S ((S (dst_index_project_table)) * dst_negative_scale_project_table)) /\ exists ff_q_pvs_project_tableentrynegative. dst_negative_code_project_table = ff_q_pvs_project_tableentrynegative * S ((S (dst_index_project_table)) * dst_negative_scale_project_table) + (dst_negative_project_table))) /\ (exists ge_balance_positive_project_tableentryvalue ge_balance_negative_project_tableentryvalue. (((((dst_value_project_table) = 2 * (ge_balance_positive_project_tableentryvalue) /\ (ge_balance_negative_project_tableentryvalue) = 0) \/ exists ge_signed_half_project_tableentryvaluedecode. (((dst_value_project_table) = 2 * ge_signed_half_project_tableentryvaluedecode + 1 /\ (ge_balance_positive_project_tableentryvalue) = 0) /\ (ge_balance_negative_project_tableentryvalue) = S ge_signed_half_project_tableentryvaluedecode))) /\ ((dst_positive_project_table) + ge_balance_negative_project_tableentryvalue = (dst_negative_project_table) + ge_balance_positive_project_tableentryvalue)))))))))