divisor_signed_table_at_from_components

Exact expanded first-order arithmetic statement

forall F pb pc nb nc i p n z. ((F) = (((((pb) + (pc)) * S ((pb) + (pc)) + ((pc) + (pc))) + (((nb) + (nc)) * S ((nb) + (nc)) + ((nc) + (nc)))) * S ((((pb) + (pc)) * S ((pb) + (pc)) + ((pc) + (pc))) + (((nb) + (nc)) * S ((nb) + (nc)) + ((nc) + (nc)))) + ((((nb) + (nc)) * S ((nb) + (nc)) + ((nc) + (nc))) + (((nb) + (nc)) * S ((nb) + (nc)) + ((nc) + (nc)))))) -> (((exists ff_h_pvs_entry_positive. ff_h_pvs_entry_positive + S (p) = S ((S (i)) * pc)) /\ exists ff_q_pvs_entry_positive. pb = ff_q_pvs_entry_positive * S ((S (i)) * pc) + (p))) -> (((exists ff_h_pvs_entry_negative. ff_h_pvs_entry_negative + S (n) = S ((S (i)) * nc)) /\ exists ff_q_pvs_entry_negative. nb = ff_q_pvs_entry_negative * S ((S (i)) * nc) + (n))) -> (exists ge_balance_positive_entry_balance ge_balance_negative_entry_balance. (((((z) = 2 * (ge_balance_positive_entry_balance) /\ (ge_balance_negative_entry_balance) = 0) \/ exists ge_signed_half_entry_balancedecode. (((z) = 2 * ge_signed_half_entry_balancedecode + 1 /\ (ge_balance_positive_entry_balance) = 0) /\ (ge_balance_negative_entry_balance) = S ge_signed_half_entry_balancedecode))) /\ ((p) + ge_balance_negative_entry_balance = (n) + ge_balance_positive_entry_balance))) -> (exists dst_positive_code_entry_result dst_positive_scale_entry_result dst_negative_code_entry_result dst_negative_scale_entry_result dst_positive_entry_result dst_negative_entry_result. (((F) = (((((dst_positive_code_entry_result) + (dst_positive_scale_entry_result)) * S ((dst_positive_code_entry_result) + (dst_positive_scale_entry_result)) + ((dst_positive_scale_entry_result) + (dst_positive_scale_entry_result))) + (((dst_negative_code_entry_result) + (dst_negative_scale_entry_result)) * S ((dst_negative_code_entry_result) + (dst_negative_scale_entry_result)) + ((dst_negative_scale_entry_result) + (dst_negative_scale_entry_result)))) * S ((((dst_positive_code_entry_result) + (dst_positive_scale_entry_result)) * S ((dst_positive_code_entry_result) + (dst_positive_scale_entry_result)) + ((dst_positive_scale_entry_result) + (dst_positive_scale_entry_result))) + (((dst_negative_code_entry_result) + (dst_negative_scale_entry_result)) * S ((dst_negative_code_entry_result) + (dst_negative_scale_entry_result)) + ((dst_negative_scale_entry_result) + (dst_negative_scale_entry_result)))) + ((((dst_negative_code_entry_result) + (dst_negative_scale_entry_result)) * S ((dst_negative_code_entry_result) + (dst_negative_scale_entry_result)) + ((dst_negative_scale_entry_result) + (dst_negative_scale_entry_result))) + (((dst_negative_code_entry_result) + (dst_negative_scale_entry_result)) * S ((dst_negative_code_entry_result) + (dst_negative_scale_entry_result)) + ((dst_negative_scale_entry_result) + (dst_negative_scale_entry_result)))))) /\ (((((exists ff_h_pvs_entry_resultpositive. ff_h_pvs_entry_resultpositive + S (dst_positive_entry_result) = S ((S (i)) * dst_positive_scale_entry_result)) /\ exists ff_q_pvs_entry_resultpositive. dst_positive_code_entry_result = ff_q_pvs_entry_resultpositive * S ((S (i)) * dst_positive_scale_entry_result) + (dst_positive_entry_result))) /\ (((((exists ff_h_pvs_entry_resultnegative. ff_h_pvs_entry_resultnegative + S (dst_negative_entry_result) = S ((S (i)) * dst_negative_scale_entry_result)) /\ exists ff_q_pvs_entry_resultnegative. dst_negative_code_entry_result = ff_q_pvs_entry_resultnegative * S ((S (i)) * dst_negative_scale_entry_result) + (dst_negative_entry_result))) /\ (exists ge_balance_positive_entry_resultvalue ge_balance_negative_entry_resultvalue. (((((z) = 2 * (ge_balance_positive_entry_resultvalue) /\ (ge_balance_negative_entry_resultvalue) = 0) \/ exists ge_signed_half_entry_resultvaluedecode. (((z) = 2 * ge_signed_half_entry_resultvaluedecode + 1 /\ (ge_balance_positive_entry_resultvalue) = 0) /\ (ge_balance_negative_entry_resultvalue) = S ge_signed_half_entry_resultvaluedecode))) /\ ((dst_positive_entry_result) + ge_balance_negative_entry_resultvalue = (dst_negative_entry_result) + ge_balance_positive_entry_resultvalue)))))))))