signed_multiplicative_intro

Exact expanded first-order arithmetic statement

forall N F. ~(N=0) -> (exists dst_positive_code_intro_table dst_positive_scale_intro_table dst_negative_code_intro_table dst_negative_scale_intro_table. (((F) = (((((dst_positive_code_intro_table) + (dst_positive_scale_intro_table)) * S ((dst_positive_code_intro_table) + (dst_positive_scale_intro_table)) + ((dst_positive_scale_intro_table) + (dst_positive_scale_intro_table))) + (((dst_negative_code_intro_table) + (dst_negative_scale_intro_table)) * S ((dst_negative_code_intro_table) + (dst_negative_scale_intro_table)) + ((dst_negative_scale_intro_table) + (dst_negative_scale_intro_table)))) * S ((((dst_positive_code_intro_table) + (dst_positive_scale_intro_table)) * S ((dst_positive_code_intro_table) + (dst_positive_scale_intro_table)) + ((dst_positive_scale_intro_table) + (dst_positive_scale_intro_table))) + (((dst_negative_code_intro_table) + (dst_negative_scale_intro_table)) * S ((dst_negative_code_intro_table) + (dst_negative_scale_intro_table)) + ((dst_negative_scale_intro_table) + (dst_negative_scale_intro_table)))) + ((((dst_negative_code_intro_table) + (dst_negative_scale_intro_table)) * S ((dst_negative_code_intro_table) + (dst_negative_scale_intro_table)) + ((dst_negative_scale_intro_table) + (dst_negative_scale_intro_table))) + (((dst_negative_code_intro_table) + (dst_negative_scale_intro_table)) * S ((dst_negative_code_intro_table) + (dst_negative_scale_intro_table)) + ((dst_negative_scale_intro_table) + (dst_negative_scale_intro_table)))))) /\ (forall dst_index_intro_table. (exists pvs_le_gap_intro_tabledomain. pvs_le_gap_intro_tabledomain + (dst_index_intro_table) = (N)) -> exists dst_positive_intro_table dst_negative_intro_table dst_value_intro_table. ((((exists ff_h_pvs_intro_tableentrypositive. ff_h_pvs_intro_tableentrypositive + S (dst_positive_intro_table) = S ((S (dst_index_intro_table)) * dst_positive_scale_intro_table)) /\ exists ff_q_pvs_intro_tableentrypositive. dst_positive_code_intro_table = ff_q_pvs_intro_tableentrypositive * S ((S (dst_index_intro_table)) * dst_positive_scale_intro_table) + (dst_positive_intro_table))) /\ (((((exists ff_h_pvs_intro_tableentrynegative. ff_h_pvs_intro_tableentrynegative + S (dst_negative_intro_table) = S ((S (dst_index_intro_table)) * dst_negative_scale_intro_table)) /\ exists ff_q_pvs_intro_tableentrynegative. dst_negative_code_intro_table = ff_q_pvs_intro_tableentrynegative * S ((S (dst_index_intro_table)) * dst_negative_scale_intro_table) + (dst_negative_intro_table))) /\ (exists ge_balance_positive_intro_tableentryvalue ge_balance_negative_intro_tableentryvalue. (((((dst_value_intro_table) = 2 * (ge_balance_positive_intro_tableentryvalue) /\ (ge_balance_negative_intro_tableentryvalue) = 0) \/ exists ge_signed_half_intro_tableentryvaluedecode. (((dst_value_intro_table) = 2 * ge_signed_half_intro_tableentryvaluedecode + 1 /\ (ge_balance_positive_intro_tableentryvalue) = 0) /\ (ge_balance_negative_intro_tableentryvalue) = S ge_signed_half_intro_tableentryvaluedecode))) /\ ((dst_positive_intro_table) + ge_balance_negative_intro_tableentryvalue = (dst_negative_intro_table) + ge_balance_positive_intro_tableentryvalue))))))))) -> (exists dst_positive_code_intro_one dst_positive_scale_intro_one dst_negative_code_intro_one dst_negative_scale_intro_one dst_positive_intro_one dst_negative_intro_one. (((F) = (((((dst_positive_code_intro_one) + (dst_positive_scale_intro_one)) * S ((dst_positive_code_intro_one) + (dst_positive_scale_intro_one)) + ((dst_positive_scale_intro_one) + (dst_positive_scale_intro_one))) + (((dst_negative_code_intro_one) + (dst_negative_scale_intro_one)) * S ((dst_negative_code_intro_one) + (dst_negative_scale_intro_one)) + ((dst_negative_scale_intro_one) + (dst_negative_scale_intro_one)))) * S ((((dst_positive_code_intro_one) + (dst_positive_scale_intro_one)) * S ((dst_positive_code_intro_one) + (dst_positive_scale_intro_one)) + ((dst_positive_scale_intro_one) + (dst_positive_scale_intro_one))) + (((dst_negative_code_intro_one) + (dst_negative_scale_intro_one)) * S ((dst_negative_code_intro_one) + (dst_negative_scale_intro_one)) + ((dst_negative_scale_intro_one) + (dst_negative_scale_intro_one)))) + ((((dst_negative_code_intro_one) + (dst_negative_scale_intro_one)) * S ((dst_negative_code_intro_one) + (dst_negative_scale_intro_one)) + ((dst_negative_scale_intro_one) + (dst_negative_scale_intro_one))) + (((dst_negative_code_intro_one) + (dst_negative_scale_intro_one)) * S ((dst_negative_code_intro_one) + (dst_negative_scale_intro_one)) + ((dst_negative_scale_intro_one) + (dst_negative_scale_intro_one)))))) /\ (((((exists ff_h_pvs_intro_onepositive. ff_h_pvs_intro_onepositive + S (dst_positive_intro_one) = S ((S (1)) * dst_positive_scale_intro_one)) /\ exists ff_q_pvs_intro_onepositive. dst_positive_code_intro_one = ff_q_pvs_intro_onepositive * S ((S (1)) * dst_positive_scale_intro_one) + (dst_positive_intro_one))) /\ (((((exists ff_h_pvs_intro_onenegative. ff_h_pvs_intro_onenegative + S (dst_negative_intro_one) = S ((S (1)) * dst_negative_scale_intro_one)) /\ exists ff_q_pvs_intro_onenegative. dst_negative_code_intro_one = ff_q_pvs_intro_onenegative * S ((S (1)) * dst_negative_scale_intro_one) + (dst_negative_intro_one))) /\ (exists ge_balance_positive_intro_onevalue ge_balance_negative_intro_onevalue. (((((2) = 2 * (ge_balance_positive_intro_onevalue) /\ (ge_balance_negative_intro_onevalue) = 0) \/ exists ge_signed_half_intro_onevaluedecode. (((2) = 2 * ge_signed_half_intro_onevaluedecode + 1 /\ (ge_balance_positive_intro_onevalue) = 0) /\ (ge_balance_negative_intro_onevalue) = S ge_signed_half_intro_onevaluedecode))) /\ ((dst_positive_intro_one) + ge_balance_negative_intro_onevalue = (dst_negative_intro_one) + ge_balance_positive_intro_onevalue))))))))) -> (forall a b x y z. ~(a=0) -> ~(b=0) -> (exists pvs_le_gap_intro_lawbound. pvs_le_gap_intro_lawbound + (a*b) = (N)) -> (forall frp_divisor_intro_lawcoprime. (exists frp_left_factor_intro_lawcoprime. a = frp_divisor_intro_lawcoprime * frp_left_factor_intro_lawcoprime) -> (exists frp_right_factor_intro_lawcoprime. b = frp_divisor_intro_lawcoprime * frp_right_factor_intro_lawcoprime) -> frp_divisor_intro_lawcoprime = 1) -> (exists dst_positive_code_intro_lawfirst dst_positive_scale_intro_lawfirst dst_negative_code_intro_lawfirst dst_negative_scale_intro_lawfirst dst_positive_intro_lawfirst dst_negative_intro_lawfirst. (((F) = (((((dst_positive_code_intro_lawfirst) + (dst_positive_scale_intro_lawfirst)) * S ((dst_positive_code_intro_lawfirst) + (dst_positive_scale_intro_lawfirst)) + ((dst_positive_scale_intro_lawfirst) + (dst_positive_scale_intro_lawfirst))) + (((dst_negative_code_intro_lawfirst) + (dst_negative_scale_intro_lawfirst)) * S ((dst_negative_code_intro_lawfirst) + (dst_negative_scale_intro_lawfirst)) + ((dst_negative_scale_intro_lawfirst) + (dst_negative_scale_intro_lawfirst)))) * S ((((dst_positive_code_intro_lawfirst) + (dst_positive_scale_intro_lawfirst)) * S ((dst_positive_code_intro_lawfirst) + (dst_positive_scale_intro_lawfirst)) + ((dst_positive_scale_intro_lawfirst) + (dst_positive_scale_intro_lawfirst))) + (((dst_negative_code_intro_lawfirst) + (dst_negative_scale_intro_lawfirst)) * S ((dst_negative_code_intro_lawfirst) + (dst_negative_scale_intro_lawfirst)) + ((dst_negative_scale_intro_lawfirst) + (dst_negative_scale_intro_lawfirst)))) + ((((dst_negative_code_intro_lawfirst) + (dst_negative_scale_intro_lawfirst)) * S ((dst_negative_code_intro_lawfirst) + (dst_negative_scale_intro_lawfirst)) + ((dst_negative_scale_intro_lawfirst) + (dst_negative_scale_intro_lawfirst))) + (((dst_negative_code_intro_lawfirst) + (dst_negative_scale_intro_lawfirst)) * S ((dst_negative_code_intro_lawfirst) + (dst_negative_scale_intro_lawfirst)) + ((dst_negative_scale_intro_lawfirst) + (dst_negative_scale_intro_lawfirst)))))) /\ (((((exists ff_h_pvs_intro_lawfirstpositive. ff_h_pvs_intro_lawfirstpositive + S (dst_positive_intro_lawfirst) = S ((S (a)) * dst_positive_scale_intro_lawfirst)) /\ exists ff_q_pvs_intro_lawfirstpositive. dst_positive_code_intro_lawfirst = ff_q_pvs_intro_lawfirstpositive * S ((S (a)) * dst_positive_scale_intro_lawfirst) + (dst_positive_intro_lawfirst))) /\ (((((exists ff_h_pvs_intro_lawfirstnegative. ff_h_pvs_intro_lawfirstnegative + S (dst_negative_intro_lawfirst) = S ((S (a)) * dst_negative_scale_intro_lawfirst)) /\ exists ff_q_pvs_intro_lawfirstnegative. dst_negative_code_intro_lawfirst = ff_q_pvs_intro_lawfirstnegative * S ((S (a)) * dst_negative_scale_intro_lawfirst) + (dst_negative_intro_lawfirst))) /\ (exists ge_balance_positive_intro_lawfirstvalue ge_balance_negative_intro_lawfirstvalue. (((((x) = 2 * (ge_balance_positive_intro_lawfirstvalue) /\ (ge_balance_negative_intro_lawfirstvalue) = 0) \/ exists ge_signed_half_intro_lawfirstvaluedecode. (((x) = 2 * ge_signed_half_intro_lawfirstvaluedecode + 1 /\ (ge_balance_positive_intro_lawfirstvalue) = 0) /\ (ge_balance_negative_intro_lawfirstvalue) = S ge_signed_half_intro_lawfirstvaluedecode))) /\ ((dst_positive_intro_lawfirst) + ge_balance_negative_intro_lawfirstvalue = (dst_negative_intro_lawfirst) + ge_balance_positive_intro_lawfirstvalue))))))))) -> (exists dst_positive_code_intro_lawsecond dst_positive_scale_intro_lawsecond dst_negative_code_intro_lawsecond dst_negative_scale_intro_lawsecond dst_positive_intro_lawsecond dst_negative_intro_lawsecond. (((F) = (((((dst_positive_code_intro_lawsecond) + (dst_positive_scale_intro_lawsecond)) * S ((dst_positive_code_intro_lawsecond) + (dst_positive_scale_intro_lawsecond)) + ((dst_positive_scale_intro_lawsecond) + (dst_positive_scale_intro_lawsecond))) + (((dst_negative_code_intro_lawsecond) + (dst_negative_scale_intro_lawsecond)) * S ((dst_negative_code_intro_lawsecond) + (dst_negative_scale_intro_lawsecond)) + ((dst_negative_scale_intro_lawsecond) + (dst_negative_scale_intro_lawsecond)))) * S ((((dst_positive_code_intro_lawsecond) + (dst_positive_scale_intro_lawsecond)) * S ((dst_positive_code_intro_lawsecond) + (dst_positive_scale_intro_lawsecond)) + ((dst_positive_scale_intro_lawsecond) + (dst_positive_scale_intro_lawsecond))) + (((dst_negative_code_intro_lawsecond) + (dst_negative_scale_intro_lawsecond)) * S ((dst_negative_code_intro_lawsecond) + (dst_negative_scale_intro_lawsecond)) + ((dst_negative_scale_intro_lawsecond) + (dst_negative_scale_intro_lawsecond)))) + ((((dst_negative_code_intro_lawsecond) + (dst_negative_scale_intro_lawsecond)) * S ((dst_negative_code_intro_lawsecond) + (dst_negative_scale_intro_lawsecond)) + ((dst_negative_scale_intro_lawsecond) + (dst_negative_scale_intro_lawsecond))) + (((dst_negative_code_intro_lawsecond) + (dst_negative_scale_intro_lawsecond)) * S ((dst_negative_code_intro_lawsecond) + (dst_negative_scale_intro_lawsecond)) + ((dst_negative_scale_intro_lawsecond) + (dst_negative_scale_intro_lawsecond)))))) /\ (((((exists ff_h_pvs_intro_lawsecondpositive. ff_h_pvs_intro_lawsecondpositive + S (dst_positive_intro_lawsecond) = S ((S (b)) * dst_positive_scale_intro_lawsecond)) /\ exists ff_q_pvs_intro_lawsecondpositive. dst_positive_code_intro_lawsecond = ff_q_pvs_intro_lawsecondpositive * S ((S (b)) * dst_positive_scale_intro_lawsecond) + (dst_positive_intro_lawsecond))) /\ (((((exists ff_h_pvs_intro_lawsecondnegative. ff_h_pvs_intro_lawsecondnegative + S (dst_negative_intro_lawsecond) = S ((S (b)) * dst_negative_scale_intro_lawsecond)) /\ exists ff_q_pvs_intro_lawsecondnegative. dst_negative_code_intro_lawsecond = ff_q_pvs_intro_lawsecondnegative * S ((S (b)) * dst_negative_scale_intro_lawsecond) + (dst_negative_intro_lawsecond))) /\ (exists ge_balance_positive_intro_lawsecondvalue ge_balance_negative_intro_lawsecondvalue. (((((y) = 2 * (ge_balance_positive_intro_lawsecondvalue) /\ (ge_balance_negative_intro_lawsecondvalue) = 0) \/ exists ge_signed_half_intro_lawsecondvaluedecode. (((y) = 2 * ge_signed_half_intro_lawsecondvaluedecode + 1 /\ (ge_balance_positive_intro_lawsecondvalue) = 0) /\ (ge_balance_negative_intro_lawsecondvalue) = S ge_signed_half_intro_lawsecondvaluedecode))) /\ ((dst_positive_intro_lawsecond) + ge_balance_negative_intro_lawsecondvalue = (dst_negative_intro_lawsecond) + ge_balance_positive_intro_lawsecondvalue))))))))) -> (exists dst_positive_code_intro_lawproduct dst_positive_scale_intro_lawproduct dst_negative_code_intro_lawproduct dst_negative_scale_intro_lawproduct dst_positive_intro_lawproduct dst_negative_intro_lawproduct. (((F) = (((((dst_positive_code_intro_lawproduct) + (dst_positive_scale_intro_lawproduct)) * S ((dst_positive_code_intro_lawproduct) + (dst_positive_scale_intro_lawproduct)) + ((dst_positive_scale_intro_lawproduct) + (dst_positive_scale_intro_lawproduct))) + (((dst_negative_code_intro_lawproduct) + (dst_negative_scale_intro_lawproduct)) * S ((dst_negative_code_intro_lawproduct) + (dst_negative_scale_intro_lawproduct)) + ((dst_negative_scale_intro_lawproduct) + (dst_negative_scale_intro_lawproduct)))) * S ((((dst_positive_code_intro_lawproduct) + (dst_positive_scale_intro_lawproduct)) * S ((dst_positive_code_intro_lawproduct) + (dst_positive_scale_intro_lawproduct)) + ((dst_positive_scale_intro_lawproduct) + (dst_positive_scale_intro_lawproduct))) + (((dst_negative_code_intro_lawproduct) + (dst_negative_scale_intro_lawproduct)) * S ((dst_negative_code_intro_lawproduct) + (dst_negative_scale_intro_lawproduct)) + ((dst_negative_scale_intro_lawproduct) + (dst_negative_scale_intro_lawproduct)))) + ((((dst_negative_code_intro_lawproduct) + (dst_negative_scale_intro_lawproduct)) * S ((dst_negative_code_intro_lawproduct) + (dst_negative_scale_intro_lawproduct)) + ((dst_negative_scale_intro_lawproduct) + (dst_negative_scale_intro_lawproduct))) + (((dst_negative_code_intro_lawproduct) + (dst_negative_scale_intro_lawproduct)) * S ((dst_negative_code_intro_lawproduct) + (dst_negative_scale_intro_lawproduct)) + ((dst_negative_scale_intro_lawproduct) + (dst_negative_scale_intro_lawproduct)))))) /\ (((((exists ff_h_pvs_intro_lawproductpositive. ff_h_pvs_intro_lawproductpositive + S (dst_positive_intro_lawproduct) = S ((S (a*b)) * dst_positive_scale_intro_lawproduct)) /\ exists ff_q_pvs_intro_lawproductpositive. dst_positive_code_intro_lawproduct = ff_q_pvs_intro_lawproductpositive * S ((S (a*b)) * dst_positive_scale_intro_lawproduct) + (dst_positive_intro_lawproduct))) /\ (((((exists ff_h_pvs_intro_lawproductnegative. ff_h_pvs_intro_lawproductnegative + S (dst_negative_intro_lawproduct) = S ((S (a*b)) * dst_negative_scale_intro_lawproduct)) /\ exists ff_q_pvs_intro_lawproductnegative. dst_negative_code_intro_lawproduct = ff_q_pvs_intro_lawproductnegative * S ((S (a*b)) * dst_negative_scale_intro_lawproduct) + (dst_negative_intro_lawproduct))) /\ (exists ge_balance_positive_intro_lawproductvalue ge_balance_negative_intro_lawproductvalue. (((((z) = 2 * (ge_balance_positive_intro_lawproductvalue) /\ (ge_balance_negative_intro_lawproductvalue) = 0) \/ exists ge_signed_half_intro_lawproductvaluedecode. (((z) = 2 * ge_signed_half_intro_lawproductvaluedecode + 1 /\ (ge_balance_positive_intro_lawproductvalue) = 0) /\ (ge_balance_negative_intro_lawproductvalue) = S ge_signed_half_intro_lawproductvaluedecode))) /\ ((dst_positive_intro_lawproduct) + ge_balance_negative_intro_lawproductvalue = (dst_negative_intro_lawproduct) + ge_balance_positive_intro_lawproductvalue))))))))) -> (exists sto_ap_intro_lawlaw sto_an_intro_lawlaw sto_bp_intro_lawlaw sto_bn_intro_lawlaw sto_cp_intro_lawlaw sto_cn_intro_lawlaw. (((((x) = 2 * (sto_ap_intro_lawlaw) /\ (sto_an_intro_lawlaw) = 0) \/ exists ge_signed_half_intro_lawlawleft. (((x) = 2 * ge_signed_half_intro_lawlawleft + 1 /\ (sto_ap_intro_lawlaw) = 0) /\ (sto_an_intro_lawlaw) = S ge_signed_half_intro_lawlawleft))) /\ ((((((y) = 2 * (sto_bp_intro_lawlaw) /\ (sto_bn_intro_lawlaw) = 0) \/ exists ge_signed_half_intro_lawlawright. (((y) = 2 * ge_signed_half_intro_lawlawright + 1 /\ (sto_bp_intro_lawlaw) = 0) /\ (sto_bn_intro_lawlaw) = S ge_signed_half_intro_lawlawright))) /\ ((((((z) = 2 * (sto_cp_intro_lawlaw) /\ (sto_cn_intro_lawlaw) = 0) \/ exists ge_signed_half_intro_lawlawoutput. (((z) = 2 * ge_signed_half_intro_lawlawoutput + 1 /\ (sto_cp_intro_lawlaw) = 0) /\ (sto_cn_intro_lawlaw) = S ge_signed_half_intro_lawlawoutput))) /\ ((sto_ap_intro_lawlaw * sto_bp_intro_lawlaw + sto_an_intro_lawlaw * sto_bn_intro_lawlaw) + sto_cn_intro_lawlaw = (sto_ap_intro_lawlaw * sto_bn_intro_lawlaw + sto_an_intro_lawlaw * sto_bp_intro_lawlaw) + sto_cp_intro_lawlaw)))))))) -> (((~((N)=0)) /\ (((exists dst_positive_code_intro_resulttable dst_positive_scale_intro_resulttable dst_negative_code_intro_resulttable dst_negative_scale_intro_resulttable. (((F) = (((((dst_positive_code_intro_resulttable) + (dst_positive_scale_intro_resulttable)) * S ((dst_positive_code_intro_resulttable) + (dst_positive_scale_intro_resulttable)) + ((dst_positive_scale_intro_resulttable) + (dst_positive_scale_intro_resulttable))) + (((dst_negative_code_intro_resulttable) + (dst_negative_scale_intro_resulttable)) * S ((dst_negative_code_intro_resulttable) + (dst_negative_scale_intro_resulttable)) + ((dst_negative_scale_intro_resulttable) + (dst_negative_scale_intro_resulttable)))) * S ((((dst_positive_code_intro_resulttable) + (dst_positive_scale_intro_resulttable)) * S ((dst_positive_code_intro_resulttable) + (dst_positive_scale_intro_resulttable)) + ((dst_positive_scale_intro_resulttable) + (dst_positive_scale_intro_resulttable))) + (((dst_negative_code_intro_resulttable) + (dst_negative_scale_intro_resulttable)) * S ((dst_negative_code_intro_resulttable) + (dst_negative_scale_intro_resulttable)) + ((dst_negative_scale_intro_resulttable) + (dst_negative_scale_intro_resulttable)))) + ((((dst_negative_code_intro_resulttable) + (dst_negative_scale_intro_resulttable)) * S ((dst_negative_code_intro_resulttable) + (dst_negative_scale_intro_resulttable)) + ((dst_negative_scale_intro_resulttable) + (dst_negative_scale_intro_resulttable))) + (((dst_negative_code_intro_resulttable) + (dst_negative_scale_intro_resulttable)) * S ((dst_negative_code_intro_resulttable) + (dst_negative_scale_intro_resulttable)) + ((dst_negative_scale_intro_resulttable) + (dst_negative_scale_intro_resulttable)))))) /\ (forall dst_index_intro_resulttable. (exists pvs_le_gap_intro_resulttabledomain. pvs_le_gap_intro_resulttabledomain + (dst_index_intro_resulttable) = (N)) -> exists dst_positive_intro_resulttable dst_negative_intro_resulttable dst_value_intro_resulttable. ((((exists ff_h_pvs_intro_resulttableentrypositive. ff_h_pvs_intro_resulttableentrypositive + S (dst_positive_intro_resulttable) = S ((S (dst_index_intro_resulttable)) * dst_positive_scale_intro_resulttable)) /\ exists ff_q_pvs_intro_resulttableentrypositive. dst_positive_code_intro_resulttable = ff_q_pvs_intro_resulttableentrypositive * S ((S (dst_index_intro_resulttable)) * dst_positive_scale_intro_resulttable) + (dst_positive_intro_resulttable))) /\ (((((exists ff_h_pvs_intro_resulttableentrynegative. ff_h_pvs_intro_resulttableentrynegative + S (dst_negative_intro_resulttable) = S ((S (dst_index_intro_resulttable)) * dst_negative_scale_intro_resulttable)) /\ exists ff_q_pvs_intro_resulttableentrynegative. dst_negative_code_intro_resulttable = ff_q_pvs_intro_resulttableentrynegative * S ((S (dst_index_intro_resulttable)) * dst_negative_scale_intro_resulttable) + (dst_negative_intro_resulttable))) /\ (exists ge_balance_positive_intro_resulttableentryvalue ge_balance_negative_intro_resulttableentryvalue. (((((dst_value_intro_resulttable) = 2 * (ge_balance_positive_intro_resulttableentryvalue) /\ (ge_balance_negative_intro_resulttableentryvalue) = 0) \/ exists ge_signed_half_intro_resulttableentryvaluedecode. (((dst_value_intro_resulttable) = 2 * ge_signed_half_intro_resulttableentryvaluedecode + 1 /\ (ge_balance_positive_intro_resulttableentryvalue) = 0) /\ (ge_balance_negative_intro_resulttableentryvalue) = S ge_signed_half_intro_resulttableentryvaluedecode))) /\ ((dst_positive_intro_resulttable) + ge_balance_negative_intro_resulttableentryvalue = (dst_negative_intro_resulttable) + ge_balance_positive_intro_resulttableentryvalue))))))))) /\ (((exists dst_positive_code_intro_resultone dst_positive_scale_intro_resultone dst_negative_code_intro_resultone dst_negative_scale_intro_resultone dst_positive_intro_resultone dst_negative_intro_resultone. (((F) = (((((dst_positive_code_intro_resultone) + (dst_positive_scale_intro_resultone)) * S ((dst_positive_code_intro_resultone) + (dst_positive_scale_intro_resultone)) + ((dst_positive_scale_intro_resultone) + (dst_positive_scale_intro_resultone))) + (((dst_negative_code_intro_resultone) + (dst_negative_scale_intro_resultone)) * S ((dst_negative_code_intro_resultone) + (dst_negative_scale_intro_resultone)) + ((dst_negative_scale_intro_resultone) + (dst_negative_scale_intro_resultone)))) * S ((((dst_positive_code_intro_resultone) + (dst_positive_scale_intro_resultone)) * S ((dst_positive_code_intro_resultone) + (dst_positive_scale_intro_resultone)) + ((dst_positive_scale_intro_resultone) + (dst_positive_scale_intro_resultone))) + (((dst_negative_code_intro_resultone) + (dst_negative_scale_intro_resultone)) * S ((dst_negative_code_intro_resultone) + (dst_negative_scale_intro_resultone)) + ((dst_negative_scale_intro_resultone) + (dst_negative_scale_intro_resultone)))) + ((((dst_negative_code_intro_resultone) + (dst_negative_scale_intro_resultone)) * S ((dst_negative_code_intro_resultone) + (dst_negative_scale_intro_resultone)) + ((dst_negative_scale_intro_resultone) + (dst_negative_scale_intro_resultone))) + (((dst_negative_code_intro_resultone) + (dst_negative_scale_intro_resultone)) * S ((dst_negative_code_intro_resultone) + (dst_negative_scale_intro_resultone)) + ((dst_negative_scale_intro_resultone) + (dst_negative_scale_intro_resultone)))))) /\ (((((exists ff_h_pvs_intro_resultonepositive. ff_h_pvs_intro_resultonepositive + S (dst_positive_intro_resultone) = S ((S (1)) * dst_positive_scale_intro_resultone)) /\ exists ff_q_pvs_intro_resultonepositive. dst_positive_code_intro_resultone = ff_q_pvs_intro_resultonepositive * S ((S (1)) * dst_positive_scale_intro_resultone) + (dst_positive_intro_resultone))) /\ (((((exists ff_h_pvs_intro_resultonenegative. ff_h_pvs_intro_resultonenegative + S (dst_negative_intro_resultone) = S ((S (1)) * dst_negative_scale_intro_resultone)) /\ exists ff_q_pvs_intro_resultonenegative. dst_negative_code_intro_resultone = ff_q_pvs_intro_resultonenegative * S ((S (1)) * dst_negative_scale_intro_resultone) + (dst_negative_intro_resultone))) /\ (exists ge_balance_positive_intro_resultonevalue ge_balance_negative_intro_resultonevalue. (((((2) = 2 * (ge_balance_positive_intro_resultonevalue) /\ (ge_balance_negative_intro_resultonevalue) = 0) \/ exists ge_signed_half_intro_resultonevaluedecode. (((2) = 2 * ge_signed_half_intro_resultonevaluedecode + 1 /\ (ge_balance_positive_intro_resultonevalue) = 0) /\ (ge_balance_negative_intro_resultonevalue) = S ge_signed_half_intro_resultonevaluedecode))) /\ ((dst_positive_intro_resultone) + ge_balance_negative_intro_resultonevalue = (dst_negative_intro_resultone) + ge_balance_positive_intro_resultonevalue))))))))) /\ (forall mp_a_intro_result mp_b_intro_result mp_x_intro_result mp_y_intro_result mp_z_intro_result. ~(mp_a_intro_result=0) -> ~(mp_b_intro_result=0) -> (exists pvs_le_gap_intro_resultbound. pvs_le_gap_intro_resultbound + (mp_a_intro_result*mp_b_intro_result) = (N)) -> (forall frp_divisor_intro_resultcoprime. (exists frp_left_factor_intro_resultcoprime. mp_a_intro_result = frp_divisor_intro_resultcoprime * frp_left_factor_intro_resultcoprime) -> (exists frp_right_factor_intro_resultcoprime. mp_b_intro_result = frp_divisor_intro_resultcoprime * frp_right_factor_intro_resultcoprime) -> frp_divisor_intro_resultcoprime = 1) -> (exists dst_positive_code_intro_resultfirst dst_positive_scale_intro_resultfirst dst_negative_code_intro_resultfirst dst_negative_scale_intro_resultfirst dst_positive_intro_resultfirst dst_negative_intro_resultfirst. (((F) = (((((dst_positive_code_intro_resultfirst) + (dst_positive_scale_intro_resultfirst)) * S ((dst_positive_code_intro_resultfirst) + (dst_positive_scale_intro_resultfirst)) + ((dst_positive_scale_intro_resultfirst) + (dst_positive_scale_intro_resultfirst))) + (((dst_negative_code_intro_resultfirst) + (dst_negative_scale_intro_resultfirst)) * S ((dst_negative_code_intro_resultfirst) + (dst_negative_scale_intro_resultfirst)) + ((dst_negative_scale_intro_resultfirst) + (dst_negative_scale_intro_resultfirst)))) * S ((((dst_positive_code_intro_resultfirst) + (dst_positive_scale_intro_resultfirst)) * S ((dst_positive_code_intro_resultfirst) + (dst_positive_scale_intro_resultfirst)) + ((dst_positive_scale_intro_resultfirst) + (dst_positive_scale_intro_resultfirst))) + (((dst_negative_code_intro_resultfirst) + (dst_negative_scale_intro_resultfirst)) * S ((dst_negative_code_intro_resultfirst) + (dst_negative_scale_intro_resultfirst)) + ((dst_negative_scale_intro_resultfirst) + (dst_negative_scale_intro_resultfirst)))) + ((((dst_negative_code_intro_resultfirst) + (dst_negative_scale_intro_resultfirst)) * S ((dst_negative_code_intro_resultfirst) + (dst_negative_scale_intro_resultfirst)) + ((dst_negative_scale_intro_resultfirst) + (dst_negative_scale_intro_resultfirst))) + (((dst_negative_code_intro_resultfirst) + (dst_negative_scale_intro_resultfirst)) * S ((dst_negative_code_intro_resultfirst) + (dst_negative_scale_intro_resultfirst)) + ((dst_negative_scale_intro_resultfirst) + (dst_negative_scale_intro_resultfirst)))))) /\ (((((exists ff_h_pvs_intro_resultfirstpositive. ff_h_pvs_intro_resultfirstpositive + S (dst_positive_intro_resultfirst) = S ((S (mp_a_intro_result)) * dst_positive_scale_intro_resultfirst)) /\ exists ff_q_pvs_intro_resultfirstpositive. dst_positive_code_intro_resultfirst = ff_q_pvs_intro_resultfirstpositive * S ((S (mp_a_intro_result)) * dst_positive_scale_intro_resultfirst) + (dst_positive_intro_resultfirst))) /\ (((((exists ff_h_pvs_intro_resultfirstnegative. ff_h_pvs_intro_resultfirstnegative + S (dst_negative_intro_resultfirst) = S ((S (mp_a_intro_result)) * dst_negative_scale_intro_resultfirst)) /\ exists ff_q_pvs_intro_resultfirstnegative. dst_negative_code_intro_resultfirst = ff_q_pvs_intro_resultfirstnegative * S ((S (mp_a_intro_result)) * dst_negative_scale_intro_resultfirst) + (dst_negative_intro_resultfirst))) /\ (exists ge_balance_positive_intro_resultfirstvalue ge_balance_negative_intro_resultfirstvalue. (((((mp_x_intro_result) = 2 * (ge_balance_positive_intro_resultfirstvalue) /\ (ge_balance_negative_intro_resultfirstvalue) = 0) \/ exists ge_signed_half_intro_resultfirstvaluedecode. (((mp_x_intro_result) = 2 * ge_signed_half_intro_resultfirstvaluedecode + 1 /\ (ge_balance_positive_intro_resultfirstvalue) = 0) /\ (ge_balance_negative_intro_resultfirstvalue) = S ge_signed_half_intro_resultfirstvaluedecode))) /\ ((dst_positive_intro_resultfirst) + ge_balance_negative_intro_resultfirstvalue = (dst_negative_intro_resultfirst) + ge_balance_positive_intro_resultfirstvalue))))))))) -> (exists dst_positive_code_intro_resultsecond dst_positive_scale_intro_resultsecond dst_negative_code_intro_resultsecond dst_negative_scale_intro_resultsecond dst_positive_intro_resultsecond dst_negative_intro_resultsecond. (((F) = (((((dst_positive_code_intro_resultsecond) + (dst_positive_scale_intro_resultsecond)) * S ((dst_positive_code_intro_resultsecond) + (dst_positive_scale_intro_resultsecond)) + ((dst_positive_scale_intro_resultsecond) + (dst_positive_scale_intro_resultsecond))) + (((dst_negative_code_intro_resultsecond) + (dst_negative_scale_intro_resultsecond)) * S ((dst_negative_code_intro_resultsecond) + (dst_negative_scale_intro_resultsecond)) + ((dst_negative_scale_intro_resultsecond) + (dst_negative_scale_intro_resultsecond)))) * S ((((dst_positive_code_intro_resultsecond) + (dst_positive_scale_intro_resultsecond)) * S ((dst_positive_code_intro_resultsecond) + (dst_positive_scale_intro_resultsecond)) + ((dst_positive_scale_intro_resultsecond) + (dst_positive_scale_intro_resultsecond))) + (((dst_negative_code_intro_resultsecond) + (dst_negative_scale_intro_resultsecond)) * S ((dst_negative_code_intro_resultsecond) + (dst_negative_scale_intro_resultsecond)) + ((dst_negative_scale_intro_resultsecond) + (dst_negative_scale_intro_resultsecond)))) + ((((dst_negative_code_intro_resultsecond) + (dst_negative_scale_intro_resultsecond)) * S ((dst_negative_code_intro_resultsecond) + (dst_negative_scale_intro_resultsecond)) + ((dst_negative_scale_intro_resultsecond) + (dst_negative_scale_intro_resultsecond))) + (((dst_negative_code_intro_resultsecond) + (dst_negative_scale_intro_resultsecond)) * S ((dst_negative_code_intro_resultsecond) + (dst_negative_scale_intro_resultsecond)) + ((dst_negative_scale_intro_resultsecond) + (dst_negative_scale_intro_resultsecond)))))) /\ (((((exists ff_h_pvs_intro_resultsecondpositive. ff_h_pvs_intro_resultsecondpositive + S (dst_positive_intro_resultsecond) = S ((S (mp_b_intro_result)) * dst_positive_scale_intro_resultsecond)) /\ exists ff_q_pvs_intro_resultsecondpositive. dst_positive_code_intro_resultsecond = ff_q_pvs_intro_resultsecondpositive * S ((S (mp_b_intro_result)) * dst_positive_scale_intro_resultsecond) + (dst_positive_intro_resultsecond))) /\ (((((exists ff_h_pvs_intro_resultsecondnegative. ff_h_pvs_intro_resultsecondnegative + S (dst_negative_intro_resultsecond) = S ((S (mp_b_intro_result)) * dst_negative_scale_intro_resultsecond)) /\ exists ff_q_pvs_intro_resultsecondnegative. dst_negative_code_intro_resultsecond = ff_q_pvs_intro_resultsecondnegative * S ((S (mp_b_intro_result)) * dst_negative_scale_intro_resultsecond) + (dst_negative_intro_resultsecond))) /\ (exists ge_balance_positive_intro_resultsecondvalue ge_balance_negative_intro_resultsecondvalue. (((((mp_y_intro_result) = 2 * (ge_balance_positive_intro_resultsecondvalue) /\ (ge_balance_negative_intro_resultsecondvalue) = 0) \/ exists ge_signed_half_intro_resultsecondvaluedecode. (((mp_y_intro_result) = 2 * ge_signed_half_intro_resultsecondvaluedecode + 1 /\ (ge_balance_positive_intro_resultsecondvalue) = 0) /\ (ge_balance_negative_intro_resultsecondvalue) = S ge_signed_half_intro_resultsecondvaluedecode))) /\ ((dst_positive_intro_resultsecond) + ge_balance_negative_intro_resultsecondvalue = (dst_negative_intro_resultsecond) + ge_balance_positive_intro_resultsecondvalue))))))))) -> (exists dst_positive_code_intro_resultproduct dst_positive_scale_intro_resultproduct dst_negative_code_intro_resultproduct dst_negative_scale_intro_resultproduct dst_positive_intro_resultproduct dst_negative_intro_resultproduct. (((F) = (((((dst_positive_code_intro_resultproduct) + (dst_positive_scale_intro_resultproduct)) * S ((dst_positive_code_intro_resultproduct) + (dst_positive_scale_intro_resultproduct)) + ((dst_positive_scale_intro_resultproduct) + (dst_positive_scale_intro_resultproduct))) + (((dst_negative_code_intro_resultproduct) + (dst_negative_scale_intro_resultproduct)) * S ((dst_negative_code_intro_resultproduct) + (dst_negative_scale_intro_resultproduct)) + ((dst_negative_scale_intro_resultproduct) + (dst_negative_scale_intro_resultproduct)))) * S ((((dst_positive_code_intro_resultproduct) + (dst_positive_scale_intro_resultproduct)) * S ((dst_positive_code_intro_resultproduct) + (dst_positive_scale_intro_resultproduct)) + ((dst_positive_scale_intro_resultproduct) + (dst_positive_scale_intro_resultproduct))) + (((dst_negative_code_intro_resultproduct) + (dst_negative_scale_intro_resultproduct)) * S ((dst_negative_code_intro_resultproduct) + (dst_negative_scale_intro_resultproduct)) + ((dst_negative_scale_intro_resultproduct) + (dst_negative_scale_intro_resultproduct)))) + ((((dst_negative_code_intro_resultproduct) + (dst_negative_scale_intro_resultproduct)) * S ((dst_negative_code_intro_resultproduct) + (dst_negative_scale_intro_resultproduct)) + ((dst_negative_scale_intro_resultproduct) + (dst_negative_scale_intro_resultproduct))) + (((dst_negative_code_intro_resultproduct) + (dst_negative_scale_intro_resultproduct)) * S ((dst_negative_code_intro_resultproduct) + (dst_negative_scale_intro_resultproduct)) + ((dst_negative_scale_intro_resultproduct) + (dst_negative_scale_intro_resultproduct)))))) /\ (((((exists ff_h_pvs_intro_resultproductpositive. ff_h_pvs_intro_resultproductpositive + S (dst_positive_intro_resultproduct) = S ((S (mp_a_intro_result*mp_b_intro_result)) * dst_positive_scale_intro_resultproduct)) /\ exists ff_q_pvs_intro_resultproductpositive. dst_positive_code_intro_resultproduct = ff_q_pvs_intro_resultproductpositive * S ((S (mp_a_intro_result*mp_b_intro_result)) * dst_positive_scale_intro_resultproduct) + (dst_positive_intro_resultproduct))) /\ (((((exists ff_h_pvs_intro_resultproductnegative. ff_h_pvs_intro_resultproductnegative + S (dst_negative_intro_resultproduct) = S ((S (mp_a_intro_result*mp_b_intro_result)) * dst_negative_scale_intro_resultproduct)) /\ exists ff_q_pvs_intro_resultproductnegative. dst_negative_code_intro_resultproduct = ff_q_pvs_intro_resultproductnegative * S ((S (mp_a_intro_result*mp_b_intro_result)) * dst_negative_scale_intro_resultproduct) + (dst_negative_intro_resultproduct))) /\ (exists ge_balance_positive_intro_resultproductvalue ge_balance_negative_intro_resultproductvalue. (((((mp_z_intro_result) = 2 * (ge_balance_positive_intro_resultproductvalue) /\ (ge_balance_negative_intro_resultproductvalue) = 0) \/ exists ge_signed_half_intro_resultproductvaluedecode. (((mp_z_intro_result) = 2 * ge_signed_half_intro_resultproductvaluedecode + 1 /\ (ge_balance_positive_intro_resultproductvalue) = 0) /\ (ge_balance_negative_intro_resultproductvalue) = S ge_signed_half_intro_resultproductvaluedecode))) /\ ((dst_positive_intro_resultproduct) + ge_balance_negative_intro_resultproductvalue = (dst_negative_intro_resultproduct) + ge_balance_positive_intro_resultproductvalue))))))))) -> (exists sto_ap_intro_resultlaw sto_an_intro_resultlaw sto_bp_intro_resultlaw sto_bn_intro_resultlaw sto_cp_intro_resultlaw sto_cn_intro_resultlaw. (((((mp_x_intro_result) = 2 * (sto_ap_intro_resultlaw) /\ (sto_an_intro_resultlaw) = 0) \/ exists ge_signed_half_intro_resultlawleft. (((mp_x_intro_result) = 2 * ge_signed_half_intro_resultlawleft + 1 /\ (sto_ap_intro_resultlaw) = 0) /\ (sto_an_intro_resultlaw) = S ge_signed_half_intro_resultlawleft))) /\ ((((((mp_y_intro_result) = 2 * (sto_bp_intro_resultlaw) /\ (sto_bn_intro_resultlaw) = 0) \/ exists ge_signed_half_intro_resultlawright. (((mp_y_intro_result) = 2 * ge_signed_half_intro_resultlawright + 1 /\ (sto_bp_intro_resultlaw) = 0) /\ (sto_bn_intro_resultlaw) = S ge_signed_half_intro_resultlawright))) /\ ((((((mp_z_intro_result) = 2 * (sto_cp_intro_resultlaw) /\ (sto_cn_intro_resultlaw) = 0) \/ exists ge_signed_half_intro_resultlawoutput. (((mp_z_intro_result) = 2 * ge_signed_half_intro_resultlawoutput + 1 /\ (sto_cp_intro_resultlaw) = 0) /\ (sto_cn_intro_resultlaw) = S ge_signed_half_intro_resultlawoutput))) /\ ((sto_ap_intro_resultlaw * sto_bp_intro_resultlaw + sto_an_intro_resultlaw * sto_bn_intro_resultlaw) + sto_cn_intro_resultlaw = (sto_ap_intro_resultlaw * sto_bn_intro_resultlaw + sto_an_intro_resultlaw * sto_bp_intro_resultlaw) + sto_cp_intro_resultlaw))))))))))))))