dirichlet_multiplicative_pair_entry

Exact expanded first-order arithmetic statement

forall N F G m n d e left right total. (((~((N)=0)) /\ (((exists dst_positive_code_construct_Ftable dst_positive_scale_construct_Ftable dst_negative_code_construct_Ftable dst_negative_scale_construct_Ftable. (((F) = (((((dst_positive_code_construct_Ftable) + (dst_positive_scale_construct_Ftable)) * S ((dst_positive_code_construct_Ftable) + (dst_positive_scale_construct_Ftable)) + ((dst_positive_scale_construct_Ftable) + (dst_positive_scale_construct_Ftable))) + (((dst_negative_code_construct_Ftable) + (dst_negative_scale_construct_Ftable)) * S ((dst_negative_code_construct_Ftable) + (dst_negative_scale_construct_Ftable)) + ((dst_negative_scale_construct_Ftable) + (dst_negative_scale_construct_Ftable)))) * S ((((dst_positive_code_construct_Ftable) + (dst_positive_scale_construct_Ftable)) * S ((dst_positive_code_construct_Ftable) + (dst_positive_scale_construct_Ftable)) + ((dst_positive_scale_construct_Ftable) + (dst_positive_scale_construct_Ftable))) + (((dst_negative_code_construct_Ftable) + (dst_negative_scale_construct_Ftable)) * S ((dst_negative_code_construct_Ftable) + (dst_negative_scale_construct_Ftable)) + ((dst_negative_scale_construct_Ftable) + (dst_negative_scale_construct_Ftable)))) + ((((dst_negative_code_construct_Ftable) + (dst_negative_scale_construct_Ftable)) * S ((dst_negative_code_construct_Ftable) + (dst_negative_scale_construct_Ftable)) + ((dst_negative_scale_construct_Ftable) + (dst_negative_scale_construct_Ftable))) + (((dst_negative_code_construct_Ftable) + (dst_negative_scale_construct_Ftable)) * S ((dst_negative_code_construct_Ftable) + (dst_negative_scale_construct_Ftable)) + ((dst_negative_scale_construct_Ftable) + (dst_negative_scale_construct_Ftable)))))) /\ (forall dst_index_construct_Ftable. (exists pvs_le_gap_construct_Ftabledomain. pvs_le_gap_construct_Ftabledomain + (dst_index_construct_Ftable) = (N)) -> exists dst_positive_construct_Ftable dst_negative_construct_Ftable dst_value_construct_Ftable. ((((exists ff_h_pvs_construct_Ftableentrypositive. ff_h_pvs_construct_Ftableentrypositive + S (dst_positive_construct_Ftable) = S ((S (dst_index_construct_Ftable)) * dst_positive_scale_construct_Ftable)) /\ exists ff_q_pvs_construct_Ftableentrypositive. dst_positive_code_construct_Ftable = ff_q_pvs_construct_Ftableentrypositive * S ((S (dst_index_construct_Ftable)) * dst_positive_scale_construct_Ftable) + (dst_positive_construct_Ftable))) /\ (((((exists ff_h_pvs_construct_Ftableentrynegative. ff_h_pvs_construct_Ftableentrynegative + S (dst_negative_construct_Ftable) = S ((S (dst_index_construct_Ftable)) * dst_negative_scale_construct_Ftable)) /\ exists ff_q_pvs_construct_Ftableentrynegative. dst_negative_code_construct_Ftable = ff_q_pvs_construct_Ftableentrynegative * S ((S (dst_index_construct_Ftable)) * dst_negative_scale_construct_Ftable) + (dst_negative_construct_Ftable))) /\ (exists ge_balance_positive_construct_Ftableentryvalue ge_balance_negative_construct_Ftableentryvalue. (((((dst_value_construct_Ftable) = 2 * (ge_balance_positive_construct_Ftableentryvalue) /\ (ge_balance_negative_construct_Ftableentryvalue) = 0) \/ exists ge_signed_half_construct_Ftableentryvaluedecode. (((dst_value_construct_Ftable) = 2 * ge_signed_half_construct_Ftableentryvaluedecode + 1 /\ (ge_balance_positive_construct_Ftableentryvalue) = 0) /\ (ge_balance_negative_construct_Ftableentryvalue) = S ge_signed_half_construct_Ftableentryvaluedecode))) /\ ((dst_positive_construct_Ftable) + ge_balance_negative_construct_Ftableentryvalue = (dst_negative_construct_Ftable) + ge_balance_positive_construct_Ftableentryvalue))))))))) /\ (((exists dst_positive_code_construct_Fone dst_positive_scale_construct_Fone dst_negative_code_construct_Fone dst_negative_scale_construct_Fone dst_positive_construct_Fone dst_negative_construct_Fone. (((F) = (((((dst_positive_code_construct_Fone) + (dst_positive_scale_construct_Fone)) * S ((dst_positive_code_construct_Fone) + (dst_positive_scale_construct_Fone)) + ((dst_positive_scale_construct_Fone) + (dst_positive_scale_construct_Fone))) + (((dst_negative_code_construct_Fone) + (dst_negative_scale_construct_Fone)) * S ((dst_negative_code_construct_Fone) + (dst_negative_scale_construct_Fone)) + ((dst_negative_scale_construct_Fone) + (dst_negative_scale_construct_Fone)))) * S ((((dst_positive_code_construct_Fone) + (dst_positive_scale_construct_Fone)) * S ((dst_positive_code_construct_Fone) + (dst_positive_scale_construct_Fone)) + ((dst_positive_scale_construct_Fone) + (dst_positive_scale_construct_Fone))) + (((dst_negative_code_construct_Fone) + (dst_negative_scale_construct_Fone)) * S ((dst_negative_code_construct_Fone) + (dst_negative_scale_construct_Fone)) + ((dst_negative_scale_construct_Fone) + (dst_negative_scale_construct_Fone)))) + ((((dst_negative_code_construct_Fone) + (dst_negative_scale_construct_Fone)) * S ((dst_negative_code_construct_Fone) + (dst_negative_scale_construct_Fone)) + ((dst_negative_scale_construct_Fone) + (dst_negative_scale_construct_Fone))) + (((dst_negative_code_construct_Fone) + (dst_negative_scale_construct_Fone)) * S ((dst_negative_code_construct_Fone) + (dst_negative_scale_construct_Fone)) + ((dst_negative_scale_construct_Fone) + (dst_negative_scale_construct_Fone)))))) /\ (((((exists ff_h_pvs_construct_Fonepositive. ff_h_pvs_construct_Fonepositive + S (dst_positive_construct_Fone) = S ((S (1)) * dst_positive_scale_construct_Fone)) /\ exists ff_q_pvs_construct_Fonepositive. dst_positive_code_construct_Fone = ff_q_pvs_construct_Fonepositive * S ((S (1)) * dst_positive_scale_construct_Fone) + (dst_positive_construct_Fone))) /\ (((((exists ff_h_pvs_construct_Fonenegative. ff_h_pvs_construct_Fonenegative + S (dst_negative_construct_Fone) = S ((S (1)) * dst_negative_scale_construct_Fone)) /\ exists ff_q_pvs_construct_Fonenegative. dst_negative_code_construct_Fone = ff_q_pvs_construct_Fonenegative * S ((S (1)) * dst_negative_scale_construct_Fone) + (dst_negative_construct_Fone))) /\ (exists ge_balance_positive_construct_Fonevalue ge_balance_negative_construct_Fonevalue. (((((2) = 2 * (ge_balance_positive_construct_Fonevalue) /\ (ge_balance_negative_construct_Fonevalue) = 0) \/ exists ge_signed_half_construct_Fonevaluedecode. (((2) = 2 * ge_signed_half_construct_Fonevaluedecode + 1 /\ (ge_balance_positive_construct_Fonevalue) = 0) /\ (ge_balance_negative_construct_Fonevalue) = S ge_signed_half_construct_Fonevaluedecode))) /\ ((dst_positive_construct_Fone) + ge_balance_negative_construct_Fonevalue = (dst_negative_construct_Fone) + ge_balance_positive_construct_Fonevalue))))))))) /\ (forall mp_a_construct_F mp_b_construct_F mp_x_construct_F mp_y_construct_F mp_z_construct_F. ~(mp_a_construct_F=0) -> ~(mp_b_construct_F=0) -> (exists pvs_le_gap_construct_Fbound. pvs_le_gap_construct_Fbound + (mp_a_construct_F*mp_b_construct_F) = (N)) -> (forall frp_divisor_construct_Fcoprime. (exists frp_left_factor_construct_Fcoprime. mp_a_construct_F = frp_divisor_construct_Fcoprime * frp_left_factor_construct_Fcoprime) -> (exists frp_right_factor_construct_Fcoprime. mp_b_construct_F = frp_divisor_construct_Fcoprime * frp_right_factor_construct_Fcoprime) -> frp_divisor_construct_Fcoprime = 1) -> (exists dst_positive_code_construct_Ffirst dst_positive_scale_construct_Ffirst dst_negative_code_construct_Ffirst dst_negative_scale_construct_Ffirst dst_positive_construct_Ffirst dst_negative_construct_Ffirst. (((F) = (((((dst_positive_code_construct_Ffirst) + (dst_positive_scale_construct_Ffirst)) * S ((dst_positive_code_construct_Ffirst) + (dst_positive_scale_construct_Ffirst)) + ((dst_positive_scale_construct_Ffirst) + (dst_positive_scale_construct_Ffirst))) + (((dst_negative_code_construct_Ffirst) + (dst_negative_scale_construct_Ffirst)) * S ((dst_negative_code_construct_Ffirst) + (dst_negative_scale_construct_Ffirst)) + ((dst_negative_scale_construct_Ffirst) + (dst_negative_scale_construct_Ffirst)))) * S ((((dst_positive_code_construct_Ffirst) + (dst_positive_scale_construct_Ffirst)) * S ((dst_positive_code_construct_Ffirst) + (dst_positive_scale_construct_Ffirst)) + ((dst_positive_scale_construct_Ffirst) + (dst_positive_scale_construct_Ffirst))) + (((dst_negative_code_construct_Ffirst) + (dst_negative_scale_construct_Ffirst)) * S ((dst_negative_code_construct_Ffirst) + (dst_negative_scale_construct_Ffirst)) + ((dst_negative_scale_construct_Ffirst) + (dst_negative_scale_construct_Ffirst)))) + ((((dst_negative_code_construct_Ffirst) + (dst_negative_scale_construct_Ffirst)) * S ((dst_negative_code_construct_Ffirst) + (dst_negative_scale_construct_Ffirst)) + ((dst_negative_scale_construct_Ffirst) + (dst_negative_scale_construct_Ffirst))) + (((dst_negative_code_construct_Ffirst) + (dst_negative_scale_construct_Ffirst)) * S ((dst_negative_code_construct_Ffirst) + (dst_negative_scale_construct_Ffirst)) + ((dst_negative_scale_construct_Ffirst) + (dst_negative_scale_construct_Ffirst)))))) /\ (((((exists ff_h_pvs_construct_Ffirstpositive. ff_h_pvs_construct_Ffirstpositive + S (dst_positive_construct_Ffirst) = S ((S (mp_a_construct_F)) * dst_positive_scale_construct_Ffirst)) /\ exists ff_q_pvs_construct_Ffirstpositive. dst_positive_code_construct_Ffirst = ff_q_pvs_construct_Ffirstpositive * S ((S (mp_a_construct_F)) * dst_positive_scale_construct_Ffirst) + (dst_positive_construct_Ffirst))) /\ (((((exists ff_h_pvs_construct_Ffirstnegative. ff_h_pvs_construct_Ffirstnegative + S (dst_negative_construct_Ffirst) = S ((S (mp_a_construct_F)) * dst_negative_scale_construct_Ffirst)) /\ exists ff_q_pvs_construct_Ffirstnegative. dst_negative_code_construct_Ffirst = ff_q_pvs_construct_Ffirstnegative * S ((S (mp_a_construct_F)) * dst_negative_scale_construct_Ffirst) + (dst_negative_construct_Ffirst))) /\ (exists ge_balance_positive_construct_Ffirstvalue ge_balance_negative_construct_Ffirstvalue. (((((mp_x_construct_F) = 2 * (ge_balance_positive_construct_Ffirstvalue) /\ (ge_balance_negative_construct_Ffirstvalue) = 0) \/ exists ge_signed_half_construct_Ffirstvaluedecode. (((mp_x_construct_F) = 2 * ge_signed_half_construct_Ffirstvaluedecode + 1 /\ (ge_balance_positive_construct_Ffirstvalue) = 0) /\ (ge_balance_negative_construct_Ffirstvalue) = S ge_signed_half_construct_Ffirstvaluedecode))) /\ ((dst_positive_construct_Ffirst) + ge_balance_negative_construct_Ffirstvalue = (dst_negative_construct_Ffirst) + ge_balance_positive_construct_Ffirstvalue))))))))) -> (exists dst_positive_code_construct_Fsecond dst_positive_scale_construct_Fsecond dst_negative_code_construct_Fsecond dst_negative_scale_construct_Fsecond dst_positive_construct_Fsecond dst_negative_construct_Fsecond. (((F) = (((((dst_positive_code_construct_Fsecond) + (dst_positive_scale_construct_Fsecond)) * S ((dst_positive_code_construct_Fsecond) + (dst_positive_scale_construct_Fsecond)) + ((dst_positive_scale_construct_Fsecond) + (dst_positive_scale_construct_Fsecond))) + (((dst_negative_code_construct_Fsecond) + (dst_negative_scale_construct_Fsecond)) * S ((dst_negative_code_construct_Fsecond) + (dst_negative_scale_construct_Fsecond)) + ((dst_negative_scale_construct_Fsecond) + (dst_negative_scale_construct_Fsecond)))) * S ((((dst_positive_code_construct_Fsecond) + (dst_positive_scale_construct_Fsecond)) * S ((dst_positive_code_construct_Fsecond) + (dst_positive_scale_construct_Fsecond)) + ((dst_positive_scale_construct_Fsecond) + (dst_positive_scale_construct_Fsecond))) + (((dst_negative_code_construct_Fsecond) + (dst_negative_scale_construct_Fsecond)) * S ((dst_negative_code_construct_Fsecond) + (dst_negative_scale_construct_Fsecond)) + ((dst_negative_scale_construct_Fsecond) + (dst_negative_scale_construct_Fsecond)))) + ((((dst_negative_code_construct_Fsecond) + (dst_negative_scale_construct_Fsecond)) * S ((dst_negative_code_construct_Fsecond) + (dst_negative_scale_construct_Fsecond)) + ((dst_negative_scale_construct_Fsecond) + (dst_negative_scale_construct_Fsecond))) + (((dst_negative_code_construct_Fsecond) + (dst_negative_scale_construct_Fsecond)) * S ((dst_negative_code_construct_Fsecond) + (dst_negative_scale_construct_Fsecond)) + ((dst_negative_scale_construct_Fsecond) + (dst_negative_scale_construct_Fsecond)))))) /\ (((((exists ff_h_pvs_construct_Fsecondpositive. ff_h_pvs_construct_Fsecondpositive + S (dst_positive_construct_Fsecond) = S ((S (mp_b_construct_F)) * dst_positive_scale_construct_Fsecond)) /\ exists ff_q_pvs_construct_Fsecondpositive. dst_positive_code_construct_Fsecond = ff_q_pvs_construct_Fsecondpositive * S ((S (mp_b_construct_F)) * dst_positive_scale_construct_Fsecond) + (dst_positive_construct_Fsecond))) /\ (((((exists ff_h_pvs_construct_Fsecondnegative. ff_h_pvs_construct_Fsecondnegative + S (dst_negative_construct_Fsecond) = S ((S (mp_b_construct_F)) * dst_negative_scale_construct_Fsecond)) /\ exists ff_q_pvs_construct_Fsecondnegative. dst_negative_code_construct_Fsecond = ff_q_pvs_construct_Fsecondnegative * S ((S (mp_b_construct_F)) * dst_negative_scale_construct_Fsecond) + (dst_negative_construct_Fsecond))) /\ (exists ge_balance_positive_construct_Fsecondvalue ge_balance_negative_construct_Fsecondvalue. (((((mp_y_construct_F) = 2 * (ge_balance_positive_construct_Fsecondvalue) /\ (ge_balance_negative_construct_Fsecondvalue) = 0) \/ exists ge_signed_half_construct_Fsecondvaluedecode. (((mp_y_construct_F) = 2 * ge_signed_half_construct_Fsecondvaluedecode + 1 /\ (ge_balance_positive_construct_Fsecondvalue) = 0) /\ (ge_balance_negative_construct_Fsecondvalue) = S ge_signed_half_construct_Fsecondvaluedecode))) /\ ((dst_positive_construct_Fsecond) + ge_balance_negative_construct_Fsecondvalue = (dst_negative_construct_Fsecond) + ge_balance_positive_construct_Fsecondvalue))))))))) -> (exists dst_positive_code_construct_Fproduct dst_positive_scale_construct_Fproduct dst_negative_code_construct_Fproduct dst_negative_scale_construct_Fproduct dst_positive_construct_Fproduct dst_negative_construct_Fproduct. (((F) = (((((dst_positive_code_construct_Fproduct) + (dst_positive_scale_construct_Fproduct)) * S ((dst_positive_code_construct_Fproduct) + (dst_positive_scale_construct_Fproduct)) + ((dst_positive_scale_construct_Fproduct) + (dst_positive_scale_construct_Fproduct))) + (((dst_negative_code_construct_Fproduct) + (dst_negative_scale_construct_Fproduct)) * S ((dst_negative_code_construct_Fproduct) + (dst_negative_scale_construct_Fproduct)) + ((dst_negative_scale_construct_Fproduct) + (dst_negative_scale_construct_Fproduct)))) * S ((((dst_positive_code_construct_Fproduct) + (dst_positive_scale_construct_Fproduct)) * S ((dst_positive_code_construct_Fproduct) + (dst_positive_scale_construct_Fproduct)) + ((dst_positive_scale_construct_Fproduct) + (dst_positive_scale_construct_Fproduct))) + (((dst_negative_code_construct_Fproduct) + (dst_negative_scale_construct_Fproduct)) * S ((dst_negative_code_construct_Fproduct) + (dst_negative_scale_construct_Fproduct)) + ((dst_negative_scale_construct_Fproduct) + (dst_negative_scale_construct_Fproduct)))) + ((((dst_negative_code_construct_Fproduct) + (dst_negative_scale_construct_Fproduct)) * S ((dst_negative_code_construct_Fproduct) + (dst_negative_scale_construct_Fproduct)) + ((dst_negative_scale_construct_Fproduct) + (dst_negative_scale_construct_Fproduct))) + (((dst_negative_code_construct_Fproduct) + (dst_negative_scale_construct_Fproduct)) * S ((dst_negative_code_construct_Fproduct) + (dst_negative_scale_construct_Fproduct)) + ((dst_negative_scale_construct_Fproduct) + (dst_negative_scale_construct_Fproduct)))))) /\ (((((exists ff_h_pvs_construct_Fproductpositive. ff_h_pvs_construct_Fproductpositive + S (dst_positive_construct_Fproduct) = S ((S (mp_a_construct_F*mp_b_construct_F)) * dst_positive_scale_construct_Fproduct)) /\ exists ff_q_pvs_construct_Fproductpositive. dst_positive_code_construct_Fproduct = ff_q_pvs_construct_Fproductpositive * S ((S (mp_a_construct_F*mp_b_construct_F)) * dst_positive_scale_construct_Fproduct) + (dst_positive_construct_Fproduct))) /\ (((((exists ff_h_pvs_construct_Fproductnegative. ff_h_pvs_construct_Fproductnegative + S (dst_negative_construct_Fproduct) = S ((S (mp_a_construct_F*mp_b_construct_F)) * dst_negative_scale_construct_Fproduct)) /\ exists ff_q_pvs_construct_Fproductnegative. dst_negative_code_construct_Fproduct = ff_q_pvs_construct_Fproductnegative * S ((S (mp_a_construct_F*mp_b_construct_F)) * dst_negative_scale_construct_Fproduct) + (dst_negative_construct_Fproduct))) /\ (exists ge_balance_positive_construct_Fproductvalue ge_balance_negative_construct_Fproductvalue. (((((mp_z_construct_F) = 2 * (ge_balance_positive_construct_Fproductvalue) /\ (ge_balance_negative_construct_Fproductvalue) = 0) \/ exists ge_signed_half_construct_Fproductvaluedecode. (((mp_z_construct_F) = 2 * ge_signed_half_construct_Fproductvaluedecode + 1 /\ (ge_balance_positive_construct_Fproductvalue) = 0) /\ (ge_balance_negative_construct_Fproductvalue) = S ge_signed_half_construct_Fproductvaluedecode))) /\ ((dst_positive_construct_Fproduct) + ge_balance_negative_construct_Fproductvalue = (dst_negative_construct_Fproduct) + ge_balance_positive_construct_Fproductvalue))))))))) -> (exists sto_ap_construct_Flaw sto_an_construct_Flaw sto_bp_construct_Flaw sto_bn_construct_Flaw sto_cp_construct_Flaw sto_cn_construct_Flaw. (((((mp_x_construct_F) = 2 * (sto_ap_construct_Flaw) /\ (sto_an_construct_Flaw) = 0) \/ exists ge_signed_half_construct_Flawleft. (((mp_x_construct_F) = 2 * ge_signed_half_construct_Flawleft + 1 /\ (sto_ap_construct_Flaw) = 0) /\ (sto_an_construct_Flaw) = S ge_signed_half_construct_Flawleft))) /\ ((((((mp_y_construct_F) = 2 * (sto_bp_construct_Flaw) /\ (sto_bn_construct_Flaw) = 0) \/ exists ge_signed_half_construct_Flawright. (((mp_y_construct_F) = 2 * ge_signed_half_construct_Flawright + 1 /\ (sto_bp_construct_Flaw) = 0) /\ (sto_bn_construct_Flaw) = S ge_signed_half_construct_Flawright))) /\ ((((((mp_z_construct_F) = 2 * (sto_cp_construct_Flaw) /\ (sto_cn_construct_Flaw) = 0) \/ exists ge_signed_half_construct_Flawoutput. (((mp_z_construct_F) = 2 * ge_signed_half_construct_Flawoutput + 1 /\ (sto_cp_construct_Flaw) = 0) /\ (sto_cn_construct_Flaw) = S ge_signed_half_construct_Flawoutput))) /\ ((sto_ap_construct_Flaw * sto_bp_construct_Flaw + sto_an_construct_Flaw * sto_bn_construct_Flaw) + sto_cn_construct_Flaw = (sto_ap_construct_Flaw * sto_bn_construct_Flaw + sto_an_construct_Flaw * sto_bp_construct_Flaw) + sto_cp_construct_Flaw)))))))))))))) -> (((~((N)=0)) /\ (((exists dst_positive_code_construct_Gtable dst_positive_scale_construct_Gtable dst_negative_code_construct_Gtable dst_negative_scale_construct_Gtable. (((G) = (((((dst_positive_code_construct_Gtable) + (dst_positive_scale_construct_Gtable)) * S ((dst_positive_code_construct_Gtable) + (dst_positive_scale_construct_Gtable)) + ((dst_positive_scale_construct_Gtable) + (dst_positive_scale_construct_Gtable))) + (((dst_negative_code_construct_Gtable) + (dst_negative_scale_construct_Gtable)) * S ((dst_negative_code_construct_Gtable) + (dst_negative_scale_construct_Gtable)) + ((dst_negative_scale_construct_Gtable) + (dst_negative_scale_construct_Gtable)))) * S ((((dst_positive_code_construct_Gtable) + (dst_positive_scale_construct_Gtable)) * S ((dst_positive_code_construct_Gtable) + (dst_positive_scale_construct_Gtable)) + ((dst_positive_scale_construct_Gtable) + (dst_positive_scale_construct_Gtable))) + (((dst_negative_code_construct_Gtable) + (dst_negative_scale_construct_Gtable)) * S ((dst_negative_code_construct_Gtable) + (dst_negative_scale_construct_Gtable)) + ((dst_negative_scale_construct_Gtable) + (dst_negative_scale_construct_Gtable)))) + ((((dst_negative_code_construct_Gtable) + (dst_negative_scale_construct_Gtable)) * S ((dst_negative_code_construct_Gtable) + (dst_negative_scale_construct_Gtable)) + ((dst_negative_scale_construct_Gtable) + (dst_negative_scale_construct_Gtable))) + (((dst_negative_code_construct_Gtable) + (dst_negative_scale_construct_Gtable)) * S ((dst_negative_code_construct_Gtable) + (dst_negative_scale_construct_Gtable)) + ((dst_negative_scale_construct_Gtable) + (dst_negative_scale_construct_Gtable)))))) /\ (forall dst_index_construct_Gtable. (exists pvs_le_gap_construct_Gtabledomain. pvs_le_gap_construct_Gtabledomain + (dst_index_construct_Gtable) = (N)) -> exists dst_positive_construct_Gtable dst_negative_construct_Gtable dst_value_construct_Gtable. ((((exists ff_h_pvs_construct_Gtableentrypositive. ff_h_pvs_construct_Gtableentrypositive + S (dst_positive_construct_Gtable) = S ((S (dst_index_construct_Gtable)) * dst_positive_scale_construct_Gtable)) /\ exists ff_q_pvs_construct_Gtableentrypositive. dst_positive_code_construct_Gtable = ff_q_pvs_construct_Gtableentrypositive * S ((S (dst_index_construct_Gtable)) * dst_positive_scale_construct_Gtable) + (dst_positive_construct_Gtable))) /\ (((((exists ff_h_pvs_construct_Gtableentrynegative. ff_h_pvs_construct_Gtableentrynegative + S (dst_negative_construct_Gtable) = S ((S (dst_index_construct_Gtable)) * dst_negative_scale_construct_Gtable)) /\ exists ff_q_pvs_construct_Gtableentrynegative. dst_negative_code_construct_Gtable = ff_q_pvs_construct_Gtableentrynegative * S ((S (dst_index_construct_Gtable)) * dst_negative_scale_construct_Gtable) + (dst_negative_construct_Gtable))) /\ (exists ge_balance_positive_construct_Gtableentryvalue ge_balance_negative_construct_Gtableentryvalue. (((((dst_value_construct_Gtable) = 2 * (ge_balance_positive_construct_Gtableentryvalue) /\ (ge_balance_negative_construct_Gtableentryvalue) = 0) \/ exists ge_signed_half_construct_Gtableentryvaluedecode. (((dst_value_construct_Gtable) = 2 * ge_signed_half_construct_Gtableentryvaluedecode + 1 /\ (ge_balance_positive_construct_Gtableentryvalue) = 0) /\ (ge_balance_negative_construct_Gtableentryvalue) = S ge_signed_half_construct_Gtableentryvaluedecode))) /\ ((dst_positive_construct_Gtable) + ge_balance_negative_construct_Gtableentryvalue = (dst_negative_construct_Gtable) + ge_balance_positive_construct_Gtableentryvalue))))))))) /\ (((exists dst_positive_code_construct_Gone dst_positive_scale_construct_Gone dst_negative_code_construct_Gone dst_negative_scale_construct_Gone dst_positive_construct_Gone dst_negative_construct_Gone. (((G) = (((((dst_positive_code_construct_Gone) + (dst_positive_scale_construct_Gone)) * S ((dst_positive_code_construct_Gone) + (dst_positive_scale_construct_Gone)) + ((dst_positive_scale_construct_Gone) + (dst_positive_scale_construct_Gone))) + (((dst_negative_code_construct_Gone) + (dst_negative_scale_construct_Gone)) * S ((dst_negative_code_construct_Gone) + (dst_negative_scale_construct_Gone)) + ((dst_negative_scale_construct_Gone) + (dst_negative_scale_construct_Gone)))) * S ((((dst_positive_code_construct_Gone) + (dst_positive_scale_construct_Gone)) * S ((dst_positive_code_construct_Gone) + (dst_positive_scale_construct_Gone)) + ((dst_positive_scale_construct_Gone) + (dst_positive_scale_construct_Gone))) + (((dst_negative_code_construct_Gone) + (dst_negative_scale_construct_Gone)) * S ((dst_negative_code_construct_Gone) + (dst_negative_scale_construct_Gone)) + ((dst_negative_scale_construct_Gone) + (dst_negative_scale_construct_Gone)))) + ((((dst_negative_code_construct_Gone) + (dst_negative_scale_construct_Gone)) * S ((dst_negative_code_construct_Gone) + (dst_negative_scale_construct_Gone)) + ((dst_negative_scale_construct_Gone) + (dst_negative_scale_construct_Gone))) + (((dst_negative_code_construct_Gone) + (dst_negative_scale_construct_Gone)) * S ((dst_negative_code_construct_Gone) + (dst_negative_scale_construct_Gone)) + ((dst_negative_scale_construct_Gone) + (dst_negative_scale_construct_Gone)))))) /\ (((((exists ff_h_pvs_construct_Gonepositive. ff_h_pvs_construct_Gonepositive + S (dst_positive_construct_Gone) = S ((S (1)) * dst_positive_scale_construct_Gone)) /\ exists ff_q_pvs_construct_Gonepositive. dst_positive_code_construct_Gone = ff_q_pvs_construct_Gonepositive * S ((S (1)) * dst_positive_scale_construct_Gone) + (dst_positive_construct_Gone))) /\ (((((exists ff_h_pvs_construct_Gonenegative. ff_h_pvs_construct_Gonenegative + S (dst_negative_construct_Gone) = S ((S (1)) * dst_negative_scale_construct_Gone)) /\ exists ff_q_pvs_construct_Gonenegative. dst_negative_code_construct_Gone = ff_q_pvs_construct_Gonenegative * S ((S (1)) * dst_negative_scale_construct_Gone) + (dst_negative_construct_Gone))) /\ (exists ge_balance_positive_construct_Gonevalue ge_balance_negative_construct_Gonevalue. (((((2) = 2 * (ge_balance_positive_construct_Gonevalue) /\ (ge_balance_negative_construct_Gonevalue) = 0) \/ exists ge_signed_half_construct_Gonevaluedecode. (((2) = 2 * ge_signed_half_construct_Gonevaluedecode + 1 /\ (ge_balance_positive_construct_Gonevalue) = 0) /\ (ge_balance_negative_construct_Gonevalue) = S ge_signed_half_construct_Gonevaluedecode))) /\ ((dst_positive_construct_Gone) + ge_balance_negative_construct_Gonevalue = (dst_negative_construct_Gone) + ge_balance_positive_construct_Gonevalue))))))))) /\ (forall mp_a_construct_G mp_b_construct_G mp_x_construct_G mp_y_construct_G mp_z_construct_G. ~(mp_a_construct_G=0) -> ~(mp_b_construct_G=0) -> (exists pvs_le_gap_construct_Gbound. pvs_le_gap_construct_Gbound + (mp_a_construct_G*mp_b_construct_G) = (N)) -> (forall frp_divisor_construct_Gcoprime. (exists frp_left_factor_construct_Gcoprime. mp_a_construct_G = frp_divisor_construct_Gcoprime * frp_left_factor_construct_Gcoprime) -> (exists frp_right_factor_construct_Gcoprime. mp_b_construct_G = frp_divisor_construct_Gcoprime * frp_right_factor_construct_Gcoprime) -> frp_divisor_construct_Gcoprime = 1) -> (exists dst_positive_code_construct_Gfirst dst_positive_scale_construct_Gfirst dst_negative_code_construct_Gfirst dst_negative_scale_construct_Gfirst dst_positive_construct_Gfirst dst_negative_construct_Gfirst. (((G) = (((((dst_positive_code_construct_Gfirst) + (dst_positive_scale_construct_Gfirst)) * S ((dst_positive_code_construct_Gfirst) + (dst_positive_scale_construct_Gfirst)) + ((dst_positive_scale_construct_Gfirst) + (dst_positive_scale_construct_Gfirst))) + (((dst_negative_code_construct_Gfirst) + (dst_negative_scale_construct_Gfirst)) * S ((dst_negative_code_construct_Gfirst) + (dst_negative_scale_construct_Gfirst)) + ((dst_negative_scale_construct_Gfirst) + (dst_negative_scale_construct_Gfirst)))) * S ((((dst_positive_code_construct_Gfirst) + (dst_positive_scale_construct_Gfirst)) * S ((dst_positive_code_construct_Gfirst) + (dst_positive_scale_construct_Gfirst)) + ((dst_positive_scale_construct_Gfirst) + (dst_positive_scale_construct_Gfirst))) + (((dst_negative_code_construct_Gfirst) + (dst_negative_scale_construct_Gfirst)) * S ((dst_negative_code_construct_Gfirst) + (dst_negative_scale_construct_Gfirst)) + ((dst_negative_scale_construct_Gfirst) + (dst_negative_scale_construct_Gfirst)))) + ((((dst_negative_code_construct_Gfirst) + (dst_negative_scale_construct_Gfirst)) * S ((dst_negative_code_construct_Gfirst) + (dst_negative_scale_construct_Gfirst)) + ((dst_negative_scale_construct_Gfirst) + (dst_negative_scale_construct_Gfirst))) + (((dst_negative_code_construct_Gfirst) + (dst_negative_scale_construct_Gfirst)) * S ((dst_negative_code_construct_Gfirst) + (dst_negative_scale_construct_Gfirst)) + ((dst_negative_scale_construct_Gfirst) + (dst_negative_scale_construct_Gfirst)))))) /\ (((((exists ff_h_pvs_construct_Gfirstpositive. ff_h_pvs_construct_Gfirstpositive + S (dst_positive_construct_Gfirst) = S ((S (mp_a_construct_G)) * dst_positive_scale_construct_Gfirst)) /\ exists ff_q_pvs_construct_Gfirstpositive. dst_positive_code_construct_Gfirst = ff_q_pvs_construct_Gfirstpositive * S ((S (mp_a_construct_G)) * dst_positive_scale_construct_Gfirst) + (dst_positive_construct_Gfirst))) /\ (((((exists ff_h_pvs_construct_Gfirstnegative. ff_h_pvs_construct_Gfirstnegative + S (dst_negative_construct_Gfirst) = S ((S (mp_a_construct_G)) * dst_negative_scale_construct_Gfirst)) /\ exists ff_q_pvs_construct_Gfirstnegative. dst_negative_code_construct_Gfirst = ff_q_pvs_construct_Gfirstnegative * S ((S (mp_a_construct_G)) * dst_negative_scale_construct_Gfirst) + (dst_negative_construct_Gfirst))) /\ (exists ge_balance_positive_construct_Gfirstvalue ge_balance_negative_construct_Gfirstvalue. (((((mp_x_construct_G) = 2 * (ge_balance_positive_construct_Gfirstvalue) /\ (ge_balance_negative_construct_Gfirstvalue) = 0) \/ exists ge_signed_half_construct_Gfirstvaluedecode. (((mp_x_construct_G) = 2 * ge_signed_half_construct_Gfirstvaluedecode + 1 /\ (ge_balance_positive_construct_Gfirstvalue) = 0) /\ (ge_balance_negative_construct_Gfirstvalue) = S ge_signed_half_construct_Gfirstvaluedecode))) /\ ((dst_positive_construct_Gfirst) + ge_balance_negative_construct_Gfirstvalue = (dst_negative_construct_Gfirst) + ge_balance_positive_construct_Gfirstvalue))))))))) -> (exists dst_positive_code_construct_Gsecond dst_positive_scale_construct_Gsecond dst_negative_code_construct_Gsecond dst_negative_scale_construct_Gsecond dst_positive_construct_Gsecond dst_negative_construct_Gsecond. (((G) = (((((dst_positive_code_construct_Gsecond) + (dst_positive_scale_construct_Gsecond)) * S ((dst_positive_code_construct_Gsecond) + (dst_positive_scale_construct_Gsecond)) + ((dst_positive_scale_construct_Gsecond) + (dst_positive_scale_construct_Gsecond))) + (((dst_negative_code_construct_Gsecond) + (dst_negative_scale_construct_Gsecond)) * S ((dst_negative_code_construct_Gsecond) + (dst_negative_scale_construct_Gsecond)) + ((dst_negative_scale_construct_Gsecond) + (dst_negative_scale_construct_Gsecond)))) * S ((((dst_positive_code_construct_Gsecond) + (dst_positive_scale_construct_Gsecond)) * S ((dst_positive_code_construct_Gsecond) + (dst_positive_scale_construct_Gsecond)) + ((dst_positive_scale_construct_Gsecond) + (dst_positive_scale_construct_Gsecond))) + (((dst_negative_code_construct_Gsecond) + (dst_negative_scale_construct_Gsecond)) * S ((dst_negative_code_construct_Gsecond) + (dst_negative_scale_construct_Gsecond)) + ((dst_negative_scale_construct_Gsecond) + (dst_negative_scale_construct_Gsecond)))) + ((((dst_negative_code_construct_Gsecond) + (dst_negative_scale_construct_Gsecond)) * S ((dst_negative_code_construct_Gsecond) + (dst_negative_scale_construct_Gsecond)) + ((dst_negative_scale_construct_Gsecond) + (dst_negative_scale_construct_Gsecond))) + (((dst_negative_code_construct_Gsecond) + (dst_negative_scale_construct_Gsecond)) * S ((dst_negative_code_construct_Gsecond) + (dst_negative_scale_construct_Gsecond)) + ((dst_negative_scale_construct_Gsecond) + (dst_negative_scale_construct_Gsecond)))))) /\ (((((exists ff_h_pvs_construct_Gsecondpositive. ff_h_pvs_construct_Gsecondpositive + S (dst_positive_construct_Gsecond) = S ((S (mp_b_construct_G)) * dst_positive_scale_construct_Gsecond)) /\ exists ff_q_pvs_construct_Gsecondpositive. dst_positive_code_construct_Gsecond = ff_q_pvs_construct_Gsecondpositive * S ((S (mp_b_construct_G)) * dst_positive_scale_construct_Gsecond) + (dst_positive_construct_Gsecond))) /\ (((((exists ff_h_pvs_construct_Gsecondnegative. ff_h_pvs_construct_Gsecondnegative + S (dst_negative_construct_Gsecond) = S ((S (mp_b_construct_G)) * dst_negative_scale_construct_Gsecond)) /\ exists ff_q_pvs_construct_Gsecondnegative. dst_negative_code_construct_Gsecond = ff_q_pvs_construct_Gsecondnegative * S ((S (mp_b_construct_G)) * dst_negative_scale_construct_Gsecond) + (dst_negative_construct_Gsecond))) /\ (exists ge_balance_positive_construct_Gsecondvalue ge_balance_negative_construct_Gsecondvalue. (((((mp_y_construct_G) = 2 * (ge_balance_positive_construct_Gsecondvalue) /\ (ge_balance_negative_construct_Gsecondvalue) = 0) \/ exists ge_signed_half_construct_Gsecondvaluedecode. (((mp_y_construct_G) = 2 * ge_signed_half_construct_Gsecondvaluedecode + 1 /\ (ge_balance_positive_construct_Gsecondvalue) = 0) /\ (ge_balance_negative_construct_Gsecondvalue) = S ge_signed_half_construct_Gsecondvaluedecode))) /\ ((dst_positive_construct_Gsecond) + ge_balance_negative_construct_Gsecondvalue = (dst_negative_construct_Gsecond) + ge_balance_positive_construct_Gsecondvalue))))))))) -> (exists dst_positive_code_construct_Gproduct dst_positive_scale_construct_Gproduct dst_negative_code_construct_Gproduct dst_negative_scale_construct_Gproduct dst_positive_construct_Gproduct dst_negative_construct_Gproduct. (((G) = (((((dst_positive_code_construct_Gproduct) + (dst_positive_scale_construct_Gproduct)) * S ((dst_positive_code_construct_Gproduct) + (dst_positive_scale_construct_Gproduct)) + ((dst_positive_scale_construct_Gproduct) + (dst_positive_scale_construct_Gproduct))) + (((dst_negative_code_construct_Gproduct) + (dst_negative_scale_construct_Gproduct)) * S ((dst_negative_code_construct_Gproduct) + (dst_negative_scale_construct_Gproduct)) + ((dst_negative_scale_construct_Gproduct) + (dst_negative_scale_construct_Gproduct)))) * S ((((dst_positive_code_construct_Gproduct) + (dst_positive_scale_construct_Gproduct)) * S ((dst_positive_code_construct_Gproduct) + (dst_positive_scale_construct_Gproduct)) + ((dst_positive_scale_construct_Gproduct) + (dst_positive_scale_construct_Gproduct))) + (((dst_negative_code_construct_Gproduct) + (dst_negative_scale_construct_Gproduct)) * S ((dst_negative_code_construct_Gproduct) + (dst_negative_scale_construct_Gproduct)) + ((dst_negative_scale_construct_Gproduct) + (dst_negative_scale_construct_Gproduct)))) + ((((dst_negative_code_construct_Gproduct) + (dst_negative_scale_construct_Gproduct)) * S ((dst_negative_code_construct_Gproduct) + (dst_negative_scale_construct_Gproduct)) + ((dst_negative_scale_construct_Gproduct) + (dst_negative_scale_construct_Gproduct))) + (((dst_negative_code_construct_Gproduct) + (dst_negative_scale_construct_Gproduct)) * S ((dst_negative_code_construct_Gproduct) + (dst_negative_scale_construct_Gproduct)) + ((dst_negative_scale_construct_Gproduct) + (dst_negative_scale_construct_Gproduct)))))) /\ (((((exists ff_h_pvs_construct_Gproductpositive. ff_h_pvs_construct_Gproductpositive + S (dst_positive_construct_Gproduct) = S ((S (mp_a_construct_G*mp_b_construct_G)) * dst_positive_scale_construct_Gproduct)) /\ exists ff_q_pvs_construct_Gproductpositive. dst_positive_code_construct_Gproduct = ff_q_pvs_construct_Gproductpositive * S ((S (mp_a_construct_G*mp_b_construct_G)) * dst_positive_scale_construct_Gproduct) + (dst_positive_construct_Gproduct))) /\ (((((exists ff_h_pvs_construct_Gproductnegative. ff_h_pvs_construct_Gproductnegative + S (dst_negative_construct_Gproduct) = S ((S (mp_a_construct_G*mp_b_construct_G)) * dst_negative_scale_construct_Gproduct)) /\ exists ff_q_pvs_construct_Gproductnegative. dst_negative_code_construct_Gproduct = ff_q_pvs_construct_Gproductnegative * S ((S (mp_a_construct_G*mp_b_construct_G)) * dst_negative_scale_construct_Gproduct) + (dst_negative_construct_Gproduct))) /\ (exists ge_balance_positive_construct_Gproductvalue ge_balance_negative_construct_Gproductvalue. (((((mp_z_construct_G) = 2 * (ge_balance_positive_construct_Gproductvalue) /\ (ge_balance_negative_construct_Gproductvalue) = 0) \/ exists ge_signed_half_construct_Gproductvaluedecode. (((mp_z_construct_G) = 2 * ge_signed_half_construct_Gproductvaluedecode + 1 /\ (ge_balance_positive_construct_Gproductvalue) = 0) /\ (ge_balance_negative_construct_Gproductvalue) = S ge_signed_half_construct_Gproductvaluedecode))) /\ ((dst_positive_construct_Gproduct) + ge_balance_negative_construct_Gproductvalue = (dst_negative_construct_Gproduct) + ge_balance_positive_construct_Gproductvalue))))))))) -> (exists sto_ap_construct_Glaw sto_an_construct_Glaw sto_bp_construct_Glaw sto_bn_construct_Glaw sto_cp_construct_Glaw sto_cn_construct_Glaw. (((((mp_x_construct_G) = 2 * (sto_ap_construct_Glaw) /\ (sto_an_construct_Glaw) = 0) \/ exists ge_signed_half_construct_Glawleft. (((mp_x_construct_G) = 2 * ge_signed_half_construct_Glawleft + 1 /\ (sto_ap_construct_Glaw) = 0) /\ (sto_an_construct_Glaw) = S ge_signed_half_construct_Glawleft))) /\ ((((((mp_y_construct_G) = 2 * (sto_bp_construct_Glaw) /\ (sto_bn_construct_Glaw) = 0) \/ exists ge_signed_half_construct_Glawright. (((mp_y_construct_G) = 2 * ge_signed_half_construct_Glawright + 1 /\ (sto_bp_construct_Glaw) = 0) /\ (sto_bn_construct_Glaw) = S ge_signed_half_construct_Glawright))) /\ ((((((mp_z_construct_G) = 2 * (sto_cp_construct_Glaw) /\ (sto_cn_construct_Glaw) = 0) \/ exists ge_signed_half_construct_Glawoutput. (((mp_z_construct_G) = 2 * ge_signed_half_construct_Glawoutput + 1 /\ (sto_cp_construct_Glaw) = 0) /\ (sto_cn_construct_Glaw) = S ge_signed_half_construct_Glawoutput))) /\ ((sto_ap_construct_Glaw * sto_bp_construct_Glaw + sto_an_construct_Glaw * sto_bn_construct_Glaw) + sto_cn_construct_Glaw = (sto_ap_construct_Glaw * sto_bn_construct_Glaw + sto_an_construct_Glaw * sto_bp_construct_Glaw) + sto_cp_construct_Glaw)))))))))))))) -> (~(m=0)) -> (~(n=0)) -> (exists pvs_le_gap_construct_bound. pvs_le_gap_construct_bound + (m*n) = (N)) -> (forall sfd_common_divisor_construct_coprime. (exists pvs_factor_construct_coprimeleft. (m) = (sfd_common_divisor_construct_coprime) * pvs_factor_construct_coprimeleft) -> (exists pvs_factor_construct_coprimeright. (n) = (sfd_common_divisor_construct_coprime) * pvs_factor_construct_coprimeright) -> sfd_common_divisor_construct_coprime = 1) -> (((~((d)=0)) /\ (((~((e)=0)) /\ (((exists pvs_factor_construct_pairleft. (m) = (d) * pvs_factor_construct_pairleft) /\ (((exists pvs_factor_construct_pairright. (n) = (e) * pvs_factor_construct_pairright) /\ ((d*e)=(d)*(e)))))))))) -> ((((~((d)=0)) /\ (exists dc_quotient_construct_left dc_left_construct_left dc_right_construct_left. (((m)=(d)*dc_quotient_construct_left) /\ (((exists dst_positive_code_construct_leftleft dst_positive_scale_construct_leftleft dst_negative_code_construct_leftleft dst_negative_scale_construct_leftleft dst_positive_construct_leftleft dst_negative_construct_leftleft. (((F) = (((((dst_positive_code_construct_leftleft) + (dst_positive_scale_construct_leftleft)) * S ((dst_positive_code_construct_leftleft) + (dst_positive_scale_construct_leftleft)) + ((dst_positive_scale_construct_leftleft) + (dst_positive_scale_construct_leftleft))) + (((dst_negative_code_construct_leftleft) + (dst_negative_scale_construct_leftleft)) * S ((dst_negative_code_construct_leftleft) + (dst_negative_scale_construct_leftleft)) + ((dst_negative_scale_construct_leftleft) + (dst_negative_scale_construct_leftleft)))) * S ((((dst_positive_code_construct_leftleft) + (dst_positive_scale_construct_leftleft)) * S ((dst_positive_code_construct_leftleft) + (dst_positive_scale_construct_leftleft)) + ((dst_positive_scale_construct_leftleft) + (dst_positive_scale_construct_leftleft))) + (((dst_negative_code_construct_leftleft) + (dst_negative_scale_construct_leftleft)) * S ((dst_negative_code_construct_leftleft) + (dst_negative_scale_construct_leftleft)) + ((dst_negative_scale_construct_leftleft) + (dst_negative_scale_construct_leftleft)))) + ((((dst_negative_code_construct_leftleft) + (dst_negative_scale_construct_leftleft)) * S ((dst_negative_code_construct_leftleft) + (dst_negative_scale_construct_leftleft)) + ((dst_negative_scale_construct_leftleft) + (dst_negative_scale_construct_leftleft))) + (((dst_negative_code_construct_leftleft) + (dst_negative_scale_construct_leftleft)) * S ((dst_negative_code_construct_leftleft) + (dst_negative_scale_construct_leftleft)) + ((dst_negative_scale_construct_leftleft) + (dst_negative_scale_construct_leftleft)))))) /\ (((((exists ff_h_pvs_construct_leftleftpositive. ff_h_pvs_construct_leftleftpositive + S (dst_positive_construct_leftleft) = S ((S (d)) * dst_positive_scale_construct_leftleft)) /\ exists ff_q_pvs_construct_leftleftpositive. dst_positive_code_construct_leftleft = ff_q_pvs_construct_leftleftpositive * S ((S (d)) * dst_positive_scale_construct_leftleft) + (dst_positive_construct_leftleft))) /\ (((((exists ff_h_pvs_construct_leftleftnegative. ff_h_pvs_construct_leftleftnegative + S (dst_negative_construct_leftleft) = S ((S (d)) * dst_negative_scale_construct_leftleft)) /\ exists ff_q_pvs_construct_leftleftnegative. dst_negative_code_construct_leftleft = ff_q_pvs_construct_leftleftnegative * S ((S (d)) * dst_negative_scale_construct_leftleft) + (dst_negative_construct_leftleft))) /\ (exists ge_balance_positive_construct_leftleftvalue ge_balance_negative_construct_leftleftvalue. (((((dc_left_construct_left) = 2 * (ge_balance_positive_construct_leftleftvalue) /\ (ge_balance_negative_construct_leftleftvalue) = 0) \/ exists ge_signed_half_construct_leftleftvaluedecode. (((dc_left_construct_left) = 2 * ge_signed_half_construct_leftleftvaluedecode + 1 /\ (ge_balance_positive_construct_leftleftvalue) = 0) /\ (ge_balance_negative_construct_leftleftvalue) = S ge_signed_half_construct_leftleftvaluedecode))) /\ ((dst_positive_construct_leftleft) + ge_balance_negative_construct_leftleftvalue = (dst_negative_construct_leftleft) + ge_balance_positive_construct_leftleftvalue))))))))) /\ (((exists dst_positive_code_construct_leftright dst_positive_scale_construct_leftright dst_negative_code_construct_leftright dst_negative_scale_construct_leftright dst_positive_construct_leftright dst_negative_construct_leftright. (((G) = (((((dst_positive_code_construct_leftright) + (dst_positive_scale_construct_leftright)) * S ((dst_positive_code_construct_leftright) + (dst_positive_scale_construct_leftright)) + ((dst_positive_scale_construct_leftright) + (dst_positive_scale_construct_leftright))) + (((dst_negative_code_construct_leftright) + (dst_negative_scale_construct_leftright)) * S ((dst_negative_code_construct_leftright) + (dst_negative_scale_construct_leftright)) + ((dst_negative_scale_construct_leftright) + (dst_negative_scale_construct_leftright)))) * S ((((dst_positive_code_construct_leftright) + (dst_positive_scale_construct_leftright)) * S ((dst_positive_code_construct_leftright) + (dst_positive_scale_construct_leftright)) + ((dst_positive_scale_construct_leftright) + (dst_positive_scale_construct_leftright))) + (((dst_negative_code_construct_leftright) + (dst_negative_scale_construct_leftright)) * S ((dst_negative_code_construct_leftright) + (dst_negative_scale_construct_leftright)) + ((dst_negative_scale_construct_leftright) + (dst_negative_scale_construct_leftright)))) + ((((dst_negative_code_construct_leftright) + (dst_negative_scale_construct_leftright)) * S ((dst_negative_code_construct_leftright) + (dst_negative_scale_construct_leftright)) + ((dst_negative_scale_construct_leftright) + (dst_negative_scale_construct_leftright))) + (((dst_negative_code_construct_leftright) + (dst_negative_scale_construct_leftright)) * S ((dst_negative_code_construct_leftright) + (dst_negative_scale_construct_leftright)) + ((dst_negative_scale_construct_leftright) + (dst_negative_scale_construct_leftright)))))) /\ (((((exists ff_h_pvs_construct_leftrightpositive. ff_h_pvs_construct_leftrightpositive + S (dst_positive_construct_leftright) = S ((S (dc_quotient_construct_left)) * dst_positive_scale_construct_leftright)) /\ exists ff_q_pvs_construct_leftrightpositive. dst_positive_code_construct_leftright = ff_q_pvs_construct_leftrightpositive * S ((S (dc_quotient_construct_left)) * dst_positive_scale_construct_leftright) + (dst_positive_construct_leftright))) /\ (((((exists ff_h_pvs_construct_leftrightnegative. ff_h_pvs_construct_leftrightnegative + S (dst_negative_construct_leftright) = S ((S (dc_quotient_construct_left)) * dst_negative_scale_construct_leftright)) /\ exists ff_q_pvs_construct_leftrightnegative. dst_negative_code_construct_leftright = ff_q_pvs_construct_leftrightnegative * S ((S (dc_quotient_construct_left)) * dst_negative_scale_construct_leftright) + (dst_negative_construct_leftright))) /\ (exists ge_balance_positive_construct_leftrightvalue ge_balance_negative_construct_leftrightvalue. (((((dc_right_construct_left) = 2 * (ge_balance_positive_construct_leftrightvalue) /\ (ge_balance_negative_construct_leftrightvalue) = 0) \/ exists ge_signed_half_construct_leftrightvaluedecode. (((dc_right_construct_left) = 2 * ge_signed_half_construct_leftrightvaluedecode + 1 /\ (ge_balance_positive_construct_leftrightvalue) = 0) /\ (ge_balance_negative_construct_leftrightvalue) = S ge_signed_half_construct_leftrightvaluedecode))) /\ ((dst_positive_construct_leftright) + ge_balance_negative_construct_leftrightvalue = (dst_negative_construct_leftright) + ge_balance_positive_construct_leftrightvalue))))))))) /\ (exists sto_ap_construct_leftproduct sto_an_construct_leftproduct sto_bp_construct_leftproduct sto_bn_construct_leftproduct sto_cp_construct_leftproduct sto_cn_construct_leftproduct. (((((dc_left_construct_left) = 2 * (sto_ap_construct_leftproduct) /\ (sto_an_construct_leftproduct) = 0) \/ exists ge_signed_half_construct_leftproductleft. (((dc_left_construct_left) = 2 * ge_signed_half_construct_leftproductleft + 1 /\ (sto_ap_construct_leftproduct) = 0) /\ (sto_an_construct_leftproduct) = S ge_signed_half_construct_leftproductleft))) /\ ((((((dc_right_construct_left) = 2 * (sto_bp_construct_leftproduct) /\ (sto_bn_construct_leftproduct) = 0) \/ exists ge_signed_half_construct_leftproductright. (((dc_right_construct_left) = 2 * ge_signed_half_construct_leftproductright + 1 /\ (sto_bp_construct_leftproduct) = 0) /\ (sto_bn_construct_leftproduct) = S ge_signed_half_construct_leftproductright))) /\ ((((((left) = 2 * (sto_cp_construct_leftproduct) /\ (sto_cn_construct_leftproduct) = 0) \/ exists ge_signed_half_construct_leftproductoutput. (((left) = 2 * ge_signed_half_construct_leftproductoutput + 1 /\ (sto_cp_construct_leftproduct) = 0) /\ (sto_cn_construct_leftproduct) = S ge_signed_half_construct_leftproductoutput))) /\ ((sto_ap_construct_leftproduct * sto_bp_construct_leftproduct + sto_an_construct_leftproduct * sto_bn_construct_leftproduct) + sto_cn_construct_leftproduct = (sto_ap_construct_leftproduct * sto_bn_construct_leftproduct + sto_an_construct_leftproduct * sto_bp_construct_leftproduct) + sto_cp_construct_leftproduct))))))))))))))) \/ ((((d)=0 \/ ~(exists pvs_factor_construct_leftnondivisor. (m) = (d) * pvs_factor_construct_leftnondivisor)) /\ ((left)=0)))) -> ((((~((e)=0)) /\ (exists dc_quotient_construct_right dc_left_construct_right dc_right_construct_right. (((n)=(e)*dc_quotient_construct_right) /\ (((exists dst_positive_code_construct_rightleft dst_positive_scale_construct_rightleft dst_negative_code_construct_rightleft dst_negative_scale_construct_rightleft dst_positive_construct_rightleft dst_negative_construct_rightleft. (((F) = (((((dst_positive_code_construct_rightleft) + (dst_positive_scale_construct_rightleft)) * S ((dst_positive_code_construct_rightleft) + (dst_positive_scale_construct_rightleft)) + ((dst_positive_scale_construct_rightleft) + (dst_positive_scale_construct_rightleft))) + (((dst_negative_code_construct_rightleft) + (dst_negative_scale_construct_rightleft)) * S ((dst_negative_code_construct_rightleft) + (dst_negative_scale_construct_rightleft)) + ((dst_negative_scale_construct_rightleft) + (dst_negative_scale_construct_rightleft)))) * S ((((dst_positive_code_construct_rightleft) + (dst_positive_scale_construct_rightleft)) * S ((dst_positive_code_construct_rightleft) + (dst_positive_scale_construct_rightleft)) + ((dst_positive_scale_construct_rightleft) + (dst_positive_scale_construct_rightleft))) + (((dst_negative_code_construct_rightleft) + (dst_negative_scale_construct_rightleft)) * S ((dst_negative_code_construct_rightleft) + (dst_negative_scale_construct_rightleft)) + ((dst_negative_scale_construct_rightleft) + (dst_negative_scale_construct_rightleft)))) + ((((dst_negative_code_construct_rightleft) + (dst_negative_scale_construct_rightleft)) * S ((dst_negative_code_construct_rightleft) + (dst_negative_scale_construct_rightleft)) + ((dst_negative_scale_construct_rightleft) + (dst_negative_scale_construct_rightleft))) + (((dst_negative_code_construct_rightleft) + (dst_negative_scale_construct_rightleft)) * S ((dst_negative_code_construct_rightleft) + (dst_negative_scale_construct_rightleft)) + ((dst_negative_scale_construct_rightleft) + (dst_negative_scale_construct_rightleft)))))) /\ (((((exists ff_h_pvs_construct_rightleftpositive. ff_h_pvs_construct_rightleftpositive + S (dst_positive_construct_rightleft) = S ((S (e)) * dst_positive_scale_construct_rightleft)) /\ exists ff_q_pvs_construct_rightleftpositive. dst_positive_code_construct_rightleft = ff_q_pvs_construct_rightleftpositive * S ((S (e)) * dst_positive_scale_construct_rightleft) + (dst_positive_construct_rightleft))) /\ (((((exists ff_h_pvs_construct_rightleftnegative. ff_h_pvs_construct_rightleftnegative + S (dst_negative_construct_rightleft) = S ((S (e)) * dst_negative_scale_construct_rightleft)) /\ exists ff_q_pvs_construct_rightleftnegative. dst_negative_code_construct_rightleft = ff_q_pvs_construct_rightleftnegative * S ((S (e)) * dst_negative_scale_construct_rightleft) + (dst_negative_construct_rightleft))) /\ (exists ge_balance_positive_construct_rightleftvalue ge_balance_negative_construct_rightleftvalue. (((((dc_left_construct_right) = 2 * (ge_balance_positive_construct_rightleftvalue) /\ (ge_balance_negative_construct_rightleftvalue) = 0) \/ exists ge_signed_half_construct_rightleftvaluedecode. (((dc_left_construct_right) = 2 * ge_signed_half_construct_rightleftvaluedecode + 1 /\ (ge_balance_positive_construct_rightleftvalue) = 0) /\ (ge_balance_negative_construct_rightleftvalue) = S ge_signed_half_construct_rightleftvaluedecode))) /\ ((dst_positive_construct_rightleft) + ge_balance_negative_construct_rightleftvalue = (dst_negative_construct_rightleft) + ge_balance_positive_construct_rightleftvalue))))))))) /\ (((exists dst_positive_code_construct_rightright dst_positive_scale_construct_rightright dst_negative_code_construct_rightright dst_negative_scale_construct_rightright dst_positive_construct_rightright dst_negative_construct_rightright. (((G) = (((((dst_positive_code_construct_rightright) + (dst_positive_scale_construct_rightright)) * S ((dst_positive_code_construct_rightright) + (dst_positive_scale_construct_rightright)) + ((dst_positive_scale_construct_rightright) + (dst_positive_scale_construct_rightright))) + (((dst_negative_code_construct_rightright) + (dst_negative_scale_construct_rightright)) * S ((dst_negative_code_construct_rightright) + (dst_negative_scale_construct_rightright)) + ((dst_negative_scale_construct_rightright) + (dst_negative_scale_construct_rightright)))) * S ((((dst_positive_code_construct_rightright) + (dst_positive_scale_construct_rightright)) * S ((dst_positive_code_construct_rightright) + (dst_positive_scale_construct_rightright)) + ((dst_positive_scale_construct_rightright) + (dst_positive_scale_construct_rightright))) + (((dst_negative_code_construct_rightright) + (dst_negative_scale_construct_rightright)) * S ((dst_negative_code_construct_rightright) + (dst_negative_scale_construct_rightright)) + ((dst_negative_scale_construct_rightright) + (dst_negative_scale_construct_rightright)))) + ((((dst_negative_code_construct_rightright) + (dst_negative_scale_construct_rightright)) * S ((dst_negative_code_construct_rightright) + (dst_negative_scale_construct_rightright)) + ((dst_negative_scale_construct_rightright) + (dst_negative_scale_construct_rightright))) + (((dst_negative_code_construct_rightright) + (dst_negative_scale_construct_rightright)) * S ((dst_negative_code_construct_rightright) + (dst_negative_scale_construct_rightright)) + ((dst_negative_scale_construct_rightright) + (dst_negative_scale_construct_rightright)))))) /\ (((((exists ff_h_pvs_construct_rightrightpositive. ff_h_pvs_construct_rightrightpositive + S (dst_positive_construct_rightright) = S ((S (dc_quotient_construct_right)) * dst_positive_scale_construct_rightright)) /\ exists ff_q_pvs_construct_rightrightpositive. dst_positive_code_construct_rightright = ff_q_pvs_construct_rightrightpositive * S ((S (dc_quotient_construct_right)) * dst_positive_scale_construct_rightright) + (dst_positive_construct_rightright))) /\ (((((exists ff_h_pvs_construct_rightrightnegative. ff_h_pvs_construct_rightrightnegative + S (dst_negative_construct_rightright) = S ((S (dc_quotient_construct_right)) * dst_negative_scale_construct_rightright)) /\ exists ff_q_pvs_construct_rightrightnegative. dst_negative_code_construct_rightright = ff_q_pvs_construct_rightrightnegative * S ((S (dc_quotient_construct_right)) * dst_negative_scale_construct_rightright) + (dst_negative_construct_rightright))) /\ (exists ge_balance_positive_construct_rightrightvalue ge_balance_negative_construct_rightrightvalue. (((((dc_right_construct_right) = 2 * (ge_balance_positive_construct_rightrightvalue) /\ (ge_balance_negative_construct_rightrightvalue) = 0) \/ exists ge_signed_half_construct_rightrightvaluedecode. (((dc_right_construct_right) = 2 * ge_signed_half_construct_rightrightvaluedecode + 1 /\ (ge_balance_positive_construct_rightrightvalue) = 0) /\ (ge_balance_negative_construct_rightrightvalue) = S ge_signed_half_construct_rightrightvaluedecode))) /\ ((dst_positive_construct_rightright) + ge_balance_negative_construct_rightrightvalue = (dst_negative_construct_rightright) + ge_balance_positive_construct_rightrightvalue))))))))) /\ (exists sto_ap_construct_rightproduct sto_an_construct_rightproduct sto_bp_construct_rightproduct sto_bn_construct_rightproduct sto_cp_construct_rightproduct sto_cn_construct_rightproduct. (((((dc_left_construct_right) = 2 * (sto_ap_construct_rightproduct) /\ (sto_an_construct_rightproduct) = 0) \/ exists ge_signed_half_construct_rightproductleft. (((dc_left_construct_right) = 2 * ge_signed_half_construct_rightproductleft + 1 /\ (sto_ap_construct_rightproduct) = 0) /\ (sto_an_construct_rightproduct) = S ge_signed_half_construct_rightproductleft))) /\ ((((((dc_right_construct_right) = 2 * (sto_bp_construct_rightproduct) /\ (sto_bn_construct_rightproduct) = 0) \/ exists ge_signed_half_construct_rightproductright. (((dc_right_construct_right) = 2 * ge_signed_half_construct_rightproductright + 1 /\ (sto_bp_construct_rightproduct) = 0) /\ (sto_bn_construct_rightproduct) = S ge_signed_half_construct_rightproductright))) /\ ((((((right) = 2 * (sto_cp_construct_rightproduct) /\ (sto_cn_construct_rightproduct) = 0) \/ exists ge_signed_half_construct_rightproductoutput. (((right) = 2 * ge_signed_half_construct_rightproductoutput + 1 /\ (sto_cp_construct_rightproduct) = 0) /\ (sto_cn_construct_rightproduct) = S ge_signed_half_construct_rightproductoutput))) /\ ((sto_ap_construct_rightproduct * sto_bp_construct_rightproduct + sto_an_construct_rightproduct * sto_bn_construct_rightproduct) + sto_cn_construct_rightproduct = (sto_ap_construct_rightproduct * sto_bn_construct_rightproduct + sto_an_construct_rightproduct * sto_bp_construct_rightproduct) + sto_cp_construct_rightproduct))))))))))))))) \/ ((((e)=0 \/ ~(exists pvs_factor_construct_rightnondivisor. (n) = (e) * pvs_factor_construct_rightnondivisor)) /\ ((right)=0)))) -> (exists sto_ap_construct_product sto_an_construct_product sto_bp_construct_product sto_bn_construct_product sto_cp_construct_product sto_cn_construct_product. (((((left) = 2 * (sto_ap_construct_product) /\ (sto_an_construct_product) = 0) \/ exists ge_signed_half_construct_productleft. (((left) = 2 * ge_signed_half_construct_productleft + 1 /\ (sto_ap_construct_product) = 0) /\ (sto_an_construct_product) = S ge_signed_half_construct_productleft))) /\ ((((((right) = 2 * (sto_bp_construct_product) /\ (sto_bn_construct_product) = 0) \/ exists ge_signed_half_construct_productright. (((right) = 2 * ge_signed_half_construct_productright + 1 /\ (sto_bp_construct_product) = 0) /\ (sto_bn_construct_product) = S ge_signed_half_construct_productright))) /\ ((((((total) = 2 * (sto_cp_construct_product) /\ (sto_cn_construct_product) = 0) \/ exists ge_signed_half_construct_productoutput. (((total) = 2 * ge_signed_half_construct_productoutput + 1 /\ (sto_cp_construct_product) = 0) /\ (sto_cn_construct_product) = S ge_signed_half_construct_productoutput))) /\ ((sto_ap_construct_product * sto_bp_construct_product + sto_an_construct_product * sto_bn_construct_product) + sto_cn_construct_product = (sto_ap_construct_product * sto_bn_construct_product + sto_an_construct_product * sto_bp_construct_product) + sto_cp_construct_product))))))) -> ((((~((d*e)=0)) /\ (exists dc_quotient_construct_result dc_left_construct_result dc_right_construct_result. (((m*n)=(d*e)*dc_quotient_construct_result) /\ (((exists dst_positive_code_construct_resultleft dst_positive_scale_construct_resultleft dst_negative_code_construct_resultleft dst_negative_scale_construct_resultleft dst_positive_construct_resultleft dst_negative_construct_resultleft. (((F) = (((((dst_positive_code_construct_resultleft) + (dst_positive_scale_construct_resultleft)) * S ((dst_positive_code_construct_resultleft) + (dst_positive_scale_construct_resultleft)) + ((dst_positive_scale_construct_resultleft) + (dst_positive_scale_construct_resultleft))) + (((dst_negative_code_construct_resultleft) + (dst_negative_scale_construct_resultleft)) * S ((dst_negative_code_construct_resultleft) + (dst_negative_scale_construct_resultleft)) + ((dst_negative_scale_construct_resultleft) + (dst_negative_scale_construct_resultleft)))) * S ((((dst_positive_code_construct_resultleft) + (dst_positive_scale_construct_resultleft)) * S ((dst_positive_code_construct_resultleft) + (dst_positive_scale_construct_resultleft)) + ((dst_positive_scale_construct_resultleft) + (dst_positive_scale_construct_resultleft))) + (((dst_negative_code_construct_resultleft) + (dst_negative_scale_construct_resultleft)) * S ((dst_negative_code_construct_resultleft) + (dst_negative_scale_construct_resultleft)) + ((dst_negative_scale_construct_resultleft) + (dst_negative_scale_construct_resultleft)))) + ((((dst_negative_code_construct_resultleft) + (dst_negative_scale_construct_resultleft)) * S ((dst_negative_code_construct_resultleft) + (dst_negative_scale_construct_resultleft)) + ((dst_negative_scale_construct_resultleft) + (dst_negative_scale_construct_resultleft))) + (((dst_negative_code_construct_resultleft) + (dst_negative_scale_construct_resultleft)) * S ((dst_negative_code_construct_resultleft) + (dst_negative_scale_construct_resultleft)) + ((dst_negative_scale_construct_resultleft) + (dst_negative_scale_construct_resultleft)))))) /\ (((((exists ff_h_pvs_construct_resultleftpositive. ff_h_pvs_construct_resultleftpositive + S (dst_positive_construct_resultleft) = S ((S (d*e)) * dst_positive_scale_construct_resultleft)) /\ exists ff_q_pvs_construct_resultleftpositive. dst_positive_code_construct_resultleft = ff_q_pvs_construct_resultleftpositive * S ((S (d*e)) * dst_positive_scale_construct_resultleft) + (dst_positive_construct_resultleft))) /\ (((((exists ff_h_pvs_construct_resultleftnegative. ff_h_pvs_construct_resultleftnegative + S (dst_negative_construct_resultleft) = S ((S (d*e)) * dst_negative_scale_construct_resultleft)) /\ exists ff_q_pvs_construct_resultleftnegative. dst_negative_code_construct_resultleft = ff_q_pvs_construct_resultleftnegative * S ((S (d*e)) * dst_negative_scale_construct_resultleft) + (dst_negative_construct_resultleft))) /\ (exists ge_balance_positive_construct_resultleftvalue ge_balance_negative_construct_resultleftvalue. (((((dc_left_construct_result) = 2 * (ge_balance_positive_construct_resultleftvalue) /\ (ge_balance_negative_construct_resultleftvalue) = 0) \/ exists ge_signed_half_construct_resultleftvaluedecode. (((dc_left_construct_result) = 2 * ge_signed_half_construct_resultleftvaluedecode + 1 /\ (ge_balance_positive_construct_resultleftvalue) = 0) /\ (ge_balance_negative_construct_resultleftvalue) = S ge_signed_half_construct_resultleftvaluedecode))) /\ ((dst_positive_construct_resultleft) + ge_balance_negative_construct_resultleftvalue = (dst_negative_construct_resultleft) + ge_balance_positive_construct_resultleftvalue))))))))) /\ (((exists dst_positive_code_construct_resultright dst_positive_scale_construct_resultright dst_negative_code_construct_resultright dst_negative_scale_construct_resultright dst_positive_construct_resultright dst_negative_construct_resultright. (((G) = (((((dst_positive_code_construct_resultright) + (dst_positive_scale_construct_resultright)) * S ((dst_positive_code_construct_resultright) + (dst_positive_scale_construct_resultright)) + ((dst_positive_scale_construct_resultright) + (dst_positive_scale_construct_resultright))) + (((dst_negative_code_construct_resultright) + (dst_negative_scale_construct_resultright)) * S ((dst_negative_code_construct_resultright) + (dst_negative_scale_construct_resultright)) + ((dst_negative_scale_construct_resultright) + (dst_negative_scale_construct_resultright)))) * S ((((dst_positive_code_construct_resultright) + (dst_positive_scale_construct_resultright)) * S ((dst_positive_code_construct_resultright) + (dst_positive_scale_construct_resultright)) + ((dst_positive_scale_construct_resultright) + (dst_positive_scale_construct_resultright))) + (((dst_negative_code_construct_resultright) + (dst_negative_scale_construct_resultright)) * S ((dst_negative_code_construct_resultright) + (dst_negative_scale_construct_resultright)) + ((dst_negative_scale_construct_resultright) + (dst_negative_scale_construct_resultright)))) + ((((dst_negative_code_construct_resultright) + (dst_negative_scale_construct_resultright)) * S ((dst_negative_code_construct_resultright) + (dst_negative_scale_construct_resultright)) + ((dst_negative_scale_construct_resultright) + (dst_negative_scale_construct_resultright))) + (((dst_negative_code_construct_resultright) + (dst_negative_scale_construct_resultright)) * S ((dst_negative_code_construct_resultright) + (dst_negative_scale_construct_resultright)) + ((dst_negative_scale_construct_resultright) + (dst_negative_scale_construct_resultright)))))) /\ (((((exists ff_h_pvs_construct_resultrightpositive. ff_h_pvs_construct_resultrightpositive + S (dst_positive_construct_resultright) = S ((S (dc_quotient_construct_result)) * dst_positive_scale_construct_resultright)) /\ exists ff_q_pvs_construct_resultrightpositive. dst_positive_code_construct_resultright = ff_q_pvs_construct_resultrightpositive * S ((S (dc_quotient_construct_result)) * dst_positive_scale_construct_resultright) + (dst_positive_construct_resultright))) /\ (((((exists ff_h_pvs_construct_resultrightnegative. ff_h_pvs_construct_resultrightnegative + S (dst_negative_construct_resultright) = S ((S (dc_quotient_construct_result)) * dst_negative_scale_construct_resultright)) /\ exists ff_q_pvs_construct_resultrightnegative. dst_negative_code_construct_resultright = ff_q_pvs_construct_resultrightnegative * S ((S (dc_quotient_construct_result)) * dst_negative_scale_construct_resultright) + (dst_negative_construct_resultright))) /\ (exists ge_balance_positive_construct_resultrightvalue ge_balance_negative_construct_resultrightvalue. (((((dc_right_construct_result) = 2 * (ge_balance_positive_construct_resultrightvalue) /\ (ge_balance_negative_construct_resultrightvalue) = 0) \/ exists ge_signed_half_construct_resultrightvaluedecode. (((dc_right_construct_result) = 2 * ge_signed_half_construct_resultrightvaluedecode + 1 /\ (ge_balance_positive_construct_resultrightvalue) = 0) /\ (ge_balance_negative_construct_resultrightvalue) = S ge_signed_half_construct_resultrightvaluedecode))) /\ ((dst_positive_construct_resultright) + ge_balance_negative_construct_resultrightvalue = (dst_negative_construct_resultright) + ge_balance_positive_construct_resultrightvalue))))))))) /\ (exists sto_ap_construct_resultproduct sto_an_construct_resultproduct sto_bp_construct_resultproduct sto_bn_construct_resultproduct sto_cp_construct_resultproduct sto_cn_construct_resultproduct. (((((dc_left_construct_result) = 2 * (sto_ap_construct_resultproduct) /\ (sto_an_construct_resultproduct) = 0) \/ exists ge_signed_half_construct_resultproductleft. (((dc_left_construct_result) = 2 * ge_signed_half_construct_resultproductleft + 1 /\ (sto_ap_construct_resultproduct) = 0) /\ (sto_an_construct_resultproduct) = S ge_signed_half_construct_resultproductleft))) /\ ((((((dc_right_construct_result) = 2 * (sto_bp_construct_resultproduct) /\ (sto_bn_construct_resultproduct) = 0) \/ exists ge_signed_half_construct_resultproductright. (((dc_right_construct_result) = 2 * ge_signed_half_construct_resultproductright + 1 /\ (sto_bp_construct_resultproduct) = 0) /\ (sto_bn_construct_resultproduct) = S ge_signed_half_construct_resultproductright))) /\ ((((((total) = 2 * (sto_cp_construct_resultproduct) /\ (sto_cn_construct_resultproduct) = 0) \/ exists ge_signed_half_construct_resultproductoutput. (((total) = 2 * ge_signed_half_construct_resultproductoutput + 1 /\ (sto_cp_construct_resultproduct) = 0) /\ (sto_cn_construct_resultproduct) = S ge_signed_half_construct_resultproductoutput))) /\ ((sto_ap_construct_resultproduct * sto_bp_construct_resultproduct + sto_an_construct_resultproduct * sto_bn_construct_resultproduct) + sto_cn_construct_resultproduct = (sto_ap_construct_resultproduct * sto_bn_construct_resultproduct + sto_an_construct_resultproduct * sto_bp_construct_resultproduct) + sto_cp_construct_resultproduct))))))))))))))) \/ ((((d*e)=0 \/ ~(exists pvs_factor_construct_resultnondivisor. (m*n) = (d*e) * pvs_factor_construct_resultnondivisor)) /\ ((total)=0))))