signed_multiplicative_zero_excluded

Exact expanded first-order arithmetic statement

forall F. ~(((~((0)=0)) /\ (((exists dst_positive_code_empty_excludedtable dst_positive_scale_empty_excludedtable dst_negative_code_empty_excludedtable dst_negative_scale_empty_excludedtable. (((F) = (((((dst_positive_code_empty_excludedtable) + (dst_positive_scale_empty_excludedtable)) * S ((dst_positive_code_empty_excludedtable) + (dst_positive_scale_empty_excludedtable)) + ((dst_positive_scale_empty_excludedtable) + (dst_positive_scale_empty_excludedtable))) + (((dst_negative_code_empty_excludedtable) + (dst_negative_scale_empty_excludedtable)) * S ((dst_negative_code_empty_excludedtable) + (dst_negative_scale_empty_excludedtable)) + ((dst_negative_scale_empty_excludedtable) + (dst_negative_scale_empty_excludedtable)))) * S ((((dst_positive_code_empty_excludedtable) + (dst_positive_scale_empty_excludedtable)) * S ((dst_positive_code_empty_excludedtable) + (dst_positive_scale_empty_excludedtable)) + ((dst_positive_scale_empty_excludedtable) + (dst_positive_scale_empty_excludedtable))) + (((dst_negative_code_empty_excludedtable) + (dst_negative_scale_empty_excludedtable)) * S ((dst_negative_code_empty_excludedtable) + (dst_negative_scale_empty_excludedtable)) + ((dst_negative_scale_empty_excludedtable) + (dst_negative_scale_empty_excludedtable)))) + ((((dst_negative_code_empty_excludedtable) + (dst_negative_scale_empty_excludedtable)) * S ((dst_negative_code_empty_excludedtable) + (dst_negative_scale_empty_excludedtable)) + ((dst_negative_scale_empty_excludedtable) + (dst_negative_scale_empty_excludedtable))) + (((dst_negative_code_empty_excludedtable) + (dst_negative_scale_empty_excludedtable)) * S ((dst_negative_code_empty_excludedtable) + (dst_negative_scale_empty_excludedtable)) + ((dst_negative_scale_empty_excludedtable) + (dst_negative_scale_empty_excludedtable)))))) /\ (forall dst_index_empty_excludedtable. (exists pvs_le_gap_empty_excludedtabledomain. pvs_le_gap_empty_excludedtabledomain + (dst_index_empty_excludedtable) = (0)) -> exists dst_positive_empty_excludedtable dst_negative_empty_excludedtable dst_value_empty_excludedtable. ((((exists ff_h_pvs_empty_excludedtableentrypositive. ff_h_pvs_empty_excludedtableentrypositive + S (dst_positive_empty_excludedtable) = S ((S (dst_index_empty_excludedtable)) * dst_positive_scale_empty_excludedtable)) /\ exists ff_q_pvs_empty_excludedtableentrypositive. dst_positive_code_empty_excludedtable = ff_q_pvs_empty_excludedtableentrypositive * S ((S (dst_index_empty_excludedtable)) * dst_positive_scale_empty_excludedtable) + (dst_positive_empty_excludedtable))) /\ (((((exists ff_h_pvs_empty_excludedtableentrynegative. ff_h_pvs_empty_excludedtableentrynegative + S (dst_negative_empty_excludedtable) = S ((S (dst_index_empty_excludedtable)) * dst_negative_scale_empty_excludedtable)) /\ exists ff_q_pvs_empty_excludedtableentrynegative. dst_negative_code_empty_excludedtable = ff_q_pvs_empty_excludedtableentrynegative * S ((S (dst_index_empty_excludedtable)) * dst_negative_scale_empty_excludedtable) + (dst_negative_empty_excludedtable))) /\ (exists ge_balance_positive_empty_excludedtableentryvalue ge_balance_negative_empty_excludedtableentryvalue. (((((dst_value_empty_excludedtable) = 2 * (ge_balance_positive_empty_excludedtableentryvalue) /\ (ge_balance_negative_empty_excludedtableentryvalue) = 0) \/ exists ge_signed_half_empty_excludedtableentryvaluedecode. (((dst_value_empty_excludedtable) = 2 * ge_signed_half_empty_excludedtableentryvaluedecode + 1 /\ (ge_balance_positive_empty_excludedtableentryvalue) = 0) /\ (ge_balance_negative_empty_excludedtableentryvalue) = S ge_signed_half_empty_excludedtableentryvaluedecode))) /\ ((dst_positive_empty_excludedtable) + ge_balance_negative_empty_excludedtableentryvalue = (dst_negative_empty_excludedtable) + ge_balance_positive_empty_excludedtableentryvalue))))))))) /\ (((exists dst_positive_code_empty_excludedone dst_positive_scale_empty_excludedone dst_negative_code_empty_excludedone dst_negative_scale_empty_excludedone dst_positive_empty_excludedone dst_negative_empty_excludedone. (((F) = (((((dst_positive_code_empty_excludedone) + (dst_positive_scale_empty_excludedone)) * S ((dst_positive_code_empty_excludedone) + (dst_positive_scale_empty_excludedone)) + ((dst_positive_scale_empty_excludedone) + (dst_positive_scale_empty_excludedone))) + (((dst_negative_code_empty_excludedone) + (dst_negative_scale_empty_excludedone)) * S ((dst_negative_code_empty_excludedone) + (dst_negative_scale_empty_excludedone)) + ((dst_negative_scale_empty_excludedone) + (dst_negative_scale_empty_excludedone)))) * S ((((dst_positive_code_empty_excludedone) + (dst_positive_scale_empty_excludedone)) * S ((dst_positive_code_empty_excludedone) + (dst_positive_scale_empty_excludedone)) + ((dst_positive_scale_empty_excludedone) + (dst_positive_scale_empty_excludedone))) + (((dst_negative_code_empty_excludedone) + (dst_negative_scale_empty_excludedone)) * S ((dst_negative_code_empty_excludedone) + (dst_negative_scale_empty_excludedone)) + ((dst_negative_scale_empty_excludedone) + (dst_negative_scale_empty_excludedone)))) + ((((dst_negative_code_empty_excludedone) + (dst_negative_scale_empty_excludedone)) * S ((dst_negative_code_empty_excludedone) + (dst_negative_scale_empty_excludedone)) + ((dst_negative_scale_empty_excludedone) + (dst_negative_scale_empty_excludedone))) + (((dst_negative_code_empty_excludedone) + (dst_negative_scale_empty_excludedone)) * S ((dst_negative_code_empty_excludedone) + (dst_negative_scale_empty_excludedone)) + ((dst_negative_scale_empty_excludedone) + (dst_negative_scale_empty_excludedone)))))) /\ (((((exists ff_h_pvs_empty_excludedonepositive. ff_h_pvs_empty_excludedonepositive + S (dst_positive_empty_excludedone) = S ((S (1)) * dst_positive_scale_empty_excludedone)) /\ exists ff_q_pvs_empty_excludedonepositive. dst_positive_code_empty_excludedone = ff_q_pvs_empty_excludedonepositive * S ((S (1)) * dst_positive_scale_empty_excludedone) + (dst_positive_empty_excludedone))) /\ (((((exists ff_h_pvs_empty_excludedonenegative. ff_h_pvs_empty_excludedonenegative + S (dst_negative_empty_excludedone) = S ((S (1)) * dst_negative_scale_empty_excludedone)) /\ exists ff_q_pvs_empty_excludedonenegative. dst_negative_code_empty_excludedone = ff_q_pvs_empty_excludedonenegative * S ((S (1)) * dst_negative_scale_empty_excludedone) + (dst_negative_empty_excludedone))) /\ (exists ge_balance_positive_empty_excludedonevalue ge_balance_negative_empty_excludedonevalue. (((((2) = 2 * (ge_balance_positive_empty_excludedonevalue) /\ (ge_balance_negative_empty_excludedonevalue) = 0) \/ exists ge_signed_half_empty_excludedonevaluedecode. (((2) = 2 * ge_signed_half_empty_excludedonevaluedecode + 1 /\ (ge_balance_positive_empty_excludedonevalue) = 0) /\ (ge_balance_negative_empty_excludedonevalue) = S ge_signed_half_empty_excludedonevaluedecode))) /\ ((dst_positive_empty_excludedone) + ge_balance_negative_empty_excludedonevalue = (dst_negative_empty_excludedone) + ge_balance_positive_empty_excludedonevalue))))))))) /\ (forall mp_a_empty_excluded mp_b_empty_excluded mp_x_empty_excluded mp_y_empty_excluded mp_z_empty_excluded. ~(mp_a_empty_excluded=0) -> ~(mp_b_empty_excluded=0) -> (exists pvs_le_gap_empty_excludedbound. pvs_le_gap_empty_excludedbound + (mp_a_empty_excluded*mp_b_empty_excluded) = (0)) -> (forall frp_divisor_empty_excludedcoprime. (exists frp_left_factor_empty_excludedcoprime. mp_a_empty_excluded = frp_divisor_empty_excludedcoprime * frp_left_factor_empty_excludedcoprime) -> (exists frp_right_factor_empty_excludedcoprime. mp_b_empty_excluded = frp_divisor_empty_excludedcoprime * frp_right_factor_empty_excludedcoprime) -> frp_divisor_empty_excludedcoprime = 1) -> (exists dst_positive_code_empty_excludedfirst dst_positive_scale_empty_excludedfirst dst_negative_code_empty_excludedfirst dst_negative_scale_empty_excludedfirst dst_positive_empty_excludedfirst dst_negative_empty_excludedfirst. (((F) = (((((dst_positive_code_empty_excludedfirst) + (dst_positive_scale_empty_excludedfirst)) * S ((dst_positive_code_empty_excludedfirst) + (dst_positive_scale_empty_excludedfirst)) + ((dst_positive_scale_empty_excludedfirst) + (dst_positive_scale_empty_excludedfirst))) + (((dst_negative_code_empty_excludedfirst) + (dst_negative_scale_empty_excludedfirst)) * S ((dst_negative_code_empty_excludedfirst) + (dst_negative_scale_empty_excludedfirst)) + ((dst_negative_scale_empty_excludedfirst) + (dst_negative_scale_empty_excludedfirst)))) * S ((((dst_positive_code_empty_excludedfirst) + (dst_positive_scale_empty_excludedfirst)) * S ((dst_positive_code_empty_excludedfirst) + (dst_positive_scale_empty_excludedfirst)) + ((dst_positive_scale_empty_excludedfirst) + (dst_positive_scale_empty_excludedfirst))) + (((dst_negative_code_empty_excludedfirst) + (dst_negative_scale_empty_excludedfirst)) * S ((dst_negative_code_empty_excludedfirst) + (dst_negative_scale_empty_excludedfirst)) + ((dst_negative_scale_empty_excludedfirst) + (dst_negative_scale_empty_excludedfirst)))) + ((((dst_negative_code_empty_excludedfirst) + (dst_negative_scale_empty_excludedfirst)) * S ((dst_negative_code_empty_excludedfirst) + (dst_negative_scale_empty_excludedfirst)) + ((dst_negative_scale_empty_excludedfirst) + (dst_negative_scale_empty_excludedfirst))) + (((dst_negative_code_empty_excludedfirst) + (dst_negative_scale_empty_excludedfirst)) * S ((dst_negative_code_empty_excludedfirst) + (dst_negative_scale_empty_excludedfirst)) + ((dst_negative_scale_empty_excludedfirst) + (dst_negative_scale_empty_excludedfirst)))))) /\ (((((exists ff_h_pvs_empty_excludedfirstpositive. ff_h_pvs_empty_excludedfirstpositive + S (dst_positive_empty_excludedfirst) = S ((S (mp_a_empty_excluded)) * dst_positive_scale_empty_excludedfirst)) /\ exists ff_q_pvs_empty_excludedfirstpositive. dst_positive_code_empty_excludedfirst = ff_q_pvs_empty_excludedfirstpositive * S ((S (mp_a_empty_excluded)) * dst_positive_scale_empty_excludedfirst) + (dst_positive_empty_excludedfirst))) /\ (((((exists ff_h_pvs_empty_excludedfirstnegative. ff_h_pvs_empty_excludedfirstnegative + S (dst_negative_empty_excludedfirst) = S ((S (mp_a_empty_excluded)) * dst_negative_scale_empty_excludedfirst)) /\ exists ff_q_pvs_empty_excludedfirstnegative. dst_negative_code_empty_excludedfirst = ff_q_pvs_empty_excludedfirstnegative * S ((S (mp_a_empty_excluded)) * dst_negative_scale_empty_excludedfirst) + (dst_negative_empty_excludedfirst))) /\ (exists ge_balance_positive_empty_excludedfirstvalue ge_balance_negative_empty_excludedfirstvalue. (((((mp_x_empty_excluded) = 2 * (ge_balance_positive_empty_excludedfirstvalue) /\ (ge_balance_negative_empty_excludedfirstvalue) = 0) \/ exists ge_signed_half_empty_excludedfirstvaluedecode. (((mp_x_empty_excluded) = 2 * ge_signed_half_empty_excludedfirstvaluedecode + 1 /\ (ge_balance_positive_empty_excludedfirstvalue) = 0) /\ (ge_balance_negative_empty_excludedfirstvalue) = S ge_signed_half_empty_excludedfirstvaluedecode))) /\ ((dst_positive_empty_excludedfirst) + ge_balance_negative_empty_excludedfirstvalue = (dst_negative_empty_excludedfirst) + ge_balance_positive_empty_excludedfirstvalue))))))))) -> (exists dst_positive_code_empty_excludedsecond dst_positive_scale_empty_excludedsecond dst_negative_code_empty_excludedsecond dst_negative_scale_empty_excludedsecond dst_positive_empty_excludedsecond dst_negative_empty_excludedsecond. (((F) = (((((dst_positive_code_empty_excludedsecond) + (dst_positive_scale_empty_excludedsecond)) * S ((dst_positive_code_empty_excludedsecond) + (dst_positive_scale_empty_excludedsecond)) + ((dst_positive_scale_empty_excludedsecond) + (dst_positive_scale_empty_excludedsecond))) + (((dst_negative_code_empty_excludedsecond) + (dst_negative_scale_empty_excludedsecond)) * S ((dst_negative_code_empty_excludedsecond) + (dst_negative_scale_empty_excludedsecond)) + ((dst_negative_scale_empty_excludedsecond) + (dst_negative_scale_empty_excludedsecond)))) * S ((((dst_positive_code_empty_excludedsecond) + (dst_positive_scale_empty_excludedsecond)) * S ((dst_positive_code_empty_excludedsecond) + (dst_positive_scale_empty_excludedsecond)) + ((dst_positive_scale_empty_excludedsecond) + (dst_positive_scale_empty_excludedsecond))) + (((dst_negative_code_empty_excludedsecond) + (dst_negative_scale_empty_excludedsecond)) * S ((dst_negative_code_empty_excludedsecond) + (dst_negative_scale_empty_excludedsecond)) + ((dst_negative_scale_empty_excludedsecond) + (dst_negative_scale_empty_excludedsecond)))) + ((((dst_negative_code_empty_excludedsecond) + (dst_negative_scale_empty_excludedsecond)) * S ((dst_negative_code_empty_excludedsecond) + (dst_negative_scale_empty_excludedsecond)) + ((dst_negative_scale_empty_excludedsecond) + (dst_negative_scale_empty_excludedsecond))) + (((dst_negative_code_empty_excludedsecond) + (dst_negative_scale_empty_excludedsecond)) * S ((dst_negative_code_empty_excludedsecond) + (dst_negative_scale_empty_excludedsecond)) + ((dst_negative_scale_empty_excludedsecond) + (dst_negative_scale_empty_excludedsecond)))))) /\ (((((exists ff_h_pvs_empty_excludedsecondpositive. ff_h_pvs_empty_excludedsecondpositive + S (dst_positive_empty_excludedsecond) = S ((S (mp_b_empty_excluded)) * dst_positive_scale_empty_excludedsecond)) /\ exists ff_q_pvs_empty_excludedsecondpositive. dst_positive_code_empty_excludedsecond = ff_q_pvs_empty_excludedsecondpositive * S ((S (mp_b_empty_excluded)) * dst_positive_scale_empty_excludedsecond) + (dst_positive_empty_excludedsecond))) /\ (((((exists ff_h_pvs_empty_excludedsecondnegative. ff_h_pvs_empty_excludedsecondnegative + S (dst_negative_empty_excludedsecond) = S ((S (mp_b_empty_excluded)) * dst_negative_scale_empty_excludedsecond)) /\ exists ff_q_pvs_empty_excludedsecondnegative. dst_negative_code_empty_excludedsecond = ff_q_pvs_empty_excludedsecondnegative * S ((S (mp_b_empty_excluded)) * dst_negative_scale_empty_excludedsecond) + (dst_negative_empty_excludedsecond))) /\ (exists ge_balance_positive_empty_excludedsecondvalue ge_balance_negative_empty_excludedsecondvalue. (((((mp_y_empty_excluded) = 2 * (ge_balance_positive_empty_excludedsecondvalue) /\ (ge_balance_negative_empty_excludedsecondvalue) = 0) \/ exists ge_signed_half_empty_excludedsecondvaluedecode. (((mp_y_empty_excluded) = 2 * ge_signed_half_empty_excludedsecondvaluedecode + 1 /\ (ge_balance_positive_empty_excludedsecondvalue) = 0) /\ (ge_balance_negative_empty_excludedsecondvalue) = S ge_signed_half_empty_excludedsecondvaluedecode))) /\ ((dst_positive_empty_excludedsecond) + ge_balance_negative_empty_excludedsecondvalue = (dst_negative_empty_excludedsecond) + ge_balance_positive_empty_excludedsecondvalue))))))))) -> (exists dst_positive_code_empty_excludedproduct dst_positive_scale_empty_excludedproduct dst_negative_code_empty_excludedproduct dst_negative_scale_empty_excludedproduct dst_positive_empty_excludedproduct dst_negative_empty_excludedproduct. (((F) = (((((dst_positive_code_empty_excludedproduct) + (dst_positive_scale_empty_excludedproduct)) * S ((dst_positive_code_empty_excludedproduct) + (dst_positive_scale_empty_excludedproduct)) + ((dst_positive_scale_empty_excludedproduct) + (dst_positive_scale_empty_excludedproduct))) + (((dst_negative_code_empty_excludedproduct) + (dst_negative_scale_empty_excludedproduct)) * S ((dst_negative_code_empty_excludedproduct) + (dst_negative_scale_empty_excludedproduct)) + ((dst_negative_scale_empty_excludedproduct) + (dst_negative_scale_empty_excludedproduct)))) * S ((((dst_positive_code_empty_excludedproduct) + (dst_positive_scale_empty_excludedproduct)) * S ((dst_positive_code_empty_excludedproduct) + (dst_positive_scale_empty_excludedproduct)) + ((dst_positive_scale_empty_excludedproduct) + (dst_positive_scale_empty_excludedproduct))) + (((dst_negative_code_empty_excludedproduct) + (dst_negative_scale_empty_excludedproduct)) * S ((dst_negative_code_empty_excludedproduct) + (dst_negative_scale_empty_excludedproduct)) + ((dst_negative_scale_empty_excludedproduct) + (dst_negative_scale_empty_excludedproduct)))) + ((((dst_negative_code_empty_excludedproduct) + (dst_negative_scale_empty_excludedproduct)) * S ((dst_negative_code_empty_excludedproduct) + (dst_negative_scale_empty_excludedproduct)) + ((dst_negative_scale_empty_excludedproduct) + (dst_negative_scale_empty_excludedproduct))) + (((dst_negative_code_empty_excludedproduct) + (dst_negative_scale_empty_excludedproduct)) * S ((dst_negative_code_empty_excludedproduct) + (dst_negative_scale_empty_excludedproduct)) + ((dst_negative_scale_empty_excludedproduct) + (dst_negative_scale_empty_excludedproduct)))))) /\ (((((exists ff_h_pvs_empty_excludedproductpositive. ff_h_pvs_empty_excludedproductpositive + S (dst_positive_empty_excludedproduct) = S ((S (mp_a_empty_excluded*mp_b_empty_excluded)) * dst_positive_scale_empty_excludedproduct)) /\ exists ff_q_pvs_empty_excludedproductpositive. dst_positive_code_empty_excludedproduct = ff_q_pvs_empty_excludedproductpositive * S ((S (mp_a_empty_excluded*mp_b_empty_excluded)) * dst_positive_scale_empty_excludedproduct) + (dst_positive_empty_excludedproduct))) /\ (((((exists ff_h_pvs_empty_excludedproductnegative. ff_h_pvs_empty_excludedproductnegative + S (dst_negative_empty_excludedproduct) = S ((S (mp_a_empty_excluded*mp_b_empty_excluded)) * dst_negative_scale_empty_excludedproduct)) /\ exists ff_q_pvs_empty_excludedproductnegative. dst_negative_code_empty_excludedproduct = ff_q_pvs_empty_excludedproductnegative * S ((S (mp_a_empty_excluded*mp_b_empty_excluded)) * dst_negative_scale_empty_excludedproduct) + (dst_negative_empty_excludedproduct))) /\ (exists ge_balance_positive_empty_excludedproductvalue ge_balance_negative_empty_excludedproductvalue. (((((mp_z_empty_excluded) = 2 * (ge_balance_positive_empty_excludedproductvalue) /\ (ge_balance_negative_empty_excludedproductvalue) = 0) \/ exists ge_signed_half_empty_excludedproductvaluedecode. (((mp_z_empty_excluded) = 2 * ge_signed_half_empty_excludedproductvaluedecode + 1 /\ (ge_balance_positive_empty_excludedproductvalue) = 0) /\ (ge_balance_negative_empty_excludedproductvalue) = S ge_signed_half_empty_excludedproductvaluedecode))) /\ ((dst_positive_empty_excludedproduct) + ge_balance_negative_empty_excludedproductvalue = (dst_negative_empty_excludedproduct) + ge_balance_positive_empty_excludedproductvalue))))))))) -> (exists sto_ap_empty_excludedlaw sto_an_empty_excludedlaw sto_bp_empty_excludedlaw sto_bn_empty_excludedlaw sto_cp_empty_excludedlaw sto_cn_empty_excludedlaw. (((((mp_x_empty_excluded) = 2 * (sto_ap_empty_excludedlaw) /\ (sto_an_empty_excludedlaw) = 0) \/ exists ge_signed_half_empty_excludedlawleft. (((mp_x_empty_excluded) = 2 * ge_signed_half_empty_excludedlawleft + 1 /\ (sto_ap_empty_excludedlaw) = 0) /\ (sto_an_empty_excludedlaw) = S ge_signed_half_empty_excludedlawleft))) /\ ((((((mp_y_empty_excluded) = 2 * (sto_bp_empty_excludedlaw) /\ (sto_bn_empty_excludedlaw) = 0) \/ exists ge_signed_half_empty_excludedlawright. (((mp_y_empty_excluded) = 2 * ge_signed_half_empty_excludedlawright + 1 /\ (sto_bp_empty_excludedlaw) = 0) /\ (sto_bn_empty_excludedlaw) = S ge_signed_half_empty_excludedlawright))) /\ ((((((mp_z_empty_excluded) = 2 * (sto_cp_empty_excludedlaw) /\ (sto_cn_empty_excludedlaw) = 0) \/ exists ge_signed_half_empty_excludedlawoutput. (((mp_z_empty_excluded) = 2 * ge_signed_half_empty_excludedlawoutput + 1 /\ (sto_cp_empty_excludedlaw) = 0) /\ (sto_cn_empty_excludedlaw) = S ge_signed_half_empty_excludedlawoutput))) /\ ((sto_ap_empty_excludedlaw * sto_bp_empty_excludedlaw + sto_an_empty_excludedlaw * sto_bn_empty_excludedlaw) + sto_cn_empty_excludedlaw = (sto_ap_empty_excludedlaw * sto_bn_empty_excludedlaw + sto_an_empty_excludedlaw * sto_bp_empty_excludedlaw) + sto_cp_empty_excludedlaw))))))))))))))