arithmetic_signed_table_component_prefix_preserved

forall F G pb pc nb nc qb qc mb mc l. ((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)))))) -> ((G) = (((((qb) + (qc)) * S ((qb) + (qc)) + ((qc) + (qc))) + (((mb) + (mc)) * S ((mb) + (mc)) + ((mc) + (mc)))) * S ((((qb) + (qc)) * S ((qb) + (qc)) + ((qc) + (qc))) + (((mb) + (mc)) * S ((mb) + (mc)) + ((mc) + (mc)))) + ((((mb) + (mc)) * S ((mb) + (mc)) + ((mc) + (mc))) + (((mb) + (mc)) * S ((mb) + (mc)) + ((mc) + (mc)))))) -> (forall pfp_i_pvs_preserve_positive pfp_a_pvs_preserve_positive. (exists pfp_gap_pvs_preserve_positivebound. pfp_gap_pvs_preserve_positivebound + S (pfp_i_pvs_preserve_positive) = (l)) -> (((exists ff_h_pfp_pvs_preserve_positiveold. ff_h_pfp_pvs_preserve_positiveold + S (pfp_a_pvs_preserve_positive) = S ((S (pfp_i_pvs_preserve_positive)) * pc)) /\ exists ff_q_pfp_pvs_preserve_positiveold. pb = ff_q_pfp_pvs_preserve_positiveold * S ((S (pfp_i_pvs_preserve_positive)) * pc) + (pfp_a_pvs_preserve_positive))) -> (((exists ff_h_pfp_pvs_preserve_positivenew. ff_h_pfp_pvs_preserve_positivenew + S (pfp_a_pvs_preserve_positive) = S ((S (pfp_i_pvs_preserve_positive)) * qc)) /\ exists ff_q_pfp_pvs_preserve_positivenew. qb = ff_q_pfp_pvs_preserve_positivenew * S ((S (pfp_i_pvs_preserve_positive)) * qc) + (pfp_a_pvs_preserve_positive)))) -> (forall pfp_i_pvs_preserve_negative pfp_a_pvs_preserve_negative. (exists pfp_gap_pvs_preserve_negativebound. pfp_gap_pvs_preserve_negativebound + S (pfp_i_pvs_preserve_negative) = (l)) -> (((exists ff_h_pfp_pvs_preserve_negativeold. ff_h_pfp_pvs_preserve_negativeold + S (pfp_a_pvs_preserve_negative) = S ((S (pfp_i_pvs_preserve_negative)) * nc)) /\ exists ff_q_pfp_pvs_preserve_negativeold. nb = ff_q_pfp_pvs_preserve_negativeold * S ((S (pfp_i_pvs_preserve_negative)) * nc) + (pfp_a_pvs_preserve_negative))) -> (((exists ff_h_pfp_pvs_preserve_negativenew. ff_h_pfp_pvs_preserve_negativenew + S (pfp_a_pvs_preserve_negative) = S ((S (pfp_i_pvs_preserve_negative)) * mc)) /\ exists ff_q_pfp_pvs_preserve_negativenew. mb = ff_q_pfp_pvs_preserve_negativenew * S ((S (pfp_i_pvs_preserve_negative)) * mc) + (pfp_a_pvs_preserve_negative)))) -> (forall dst_index_preserve_result dst_first_preserve_result dst_second_preserve_result. (exists pvs_gap_preserve_resultbound. pvs_gap_preserve_resultbound + S (dst_index_preserve_result) = (l)) -> (exists dst_positive_code_preserve_resultfirst dst_positive_scale_preserve_resultfirst dst_negative_code_preserve_resultfirst dst_negative_scale_preserve_resultfirst dst_positive_preserve_resultfirst dst_negative_preserve_resultfirst. (((F) = (((((dst_positive_code_preserve_resultfirst) + (dst_positive_scale_preserve_resultfirst)) * S ((dst_positive_code_preserve_resultfirst) + (dst_positive_scale_preserve_resultfirst)) + ((dst_positive_scale_preserve_resultfirst) + (dst_positive_scale_preserve_resultfirst))) + (((dst_negative_code_preserve_resultfirst) + (dst_negative_scale_preserve_resultfirst)) * S ((dst_negative_code_preserve_resultfirst) + (dst_negative_scale_preserve_resultfirst)) + ((dst_negative_scale_preserve_resultfirst) + (dst_negative_scale_preserve_resultfirst)))) * S ((((dst_positive_code_preserve_resultfirst) + (dst_positive_scale_preserve_resultfirst)) * S ((dst_positive_code_preserve_resultfirst) + (dst_positive_scale_preserve_resultfirst)) + ((dst_positive_scale_preserve_resultfirst) + (dst_positive_scale_preserve_resultfirst))) + (((dst_negative_code_preserve_resultfirst) + (dst_negative_scale_preserve_resultfirst)) * S ((dst_negative_code_preserve_resultfirst) + (dst_negative_scale_preserve_resultfirst)) + ((dst_negative_scale_preserve_resultfirst) + (dst_negative_scale_preserve_resultfirst)))) + ((((dst_negative_code_preserve_resultfirst) + (dst_negative_scale_preserve_resultfirst)) * S ((dst_negative_code_preserve_resultfirst) + (dst_negative_scale_preserve_resultfirst)) + ((dst_negative_scale_preserve_resultfirst) + (dst_negative_scale_preserve_resultfirst))) + (((dst_negative_code_preserve_resultfirst) + (dst_negative_scale_preserve_resultfirst)) * S ((dst_negative_code_preserve_resultfirst) + (dst_negative_scale_preserve_resultfirst)) + ((dst_negative_scale_preserve_resultfirst) + (dst_negative_scale_preserve_resultfirst)))))) /\ (((((exists ff_h_pvs_preserve_resultfirstpositive. ff_h_pvs_preserve_resultfirstpositive + S (dst_positive_preserve_resultfirst) = S ((S (dst_index_preserve_result)) * dst_positive_scale_preserve_resultfirst)) /\ exists ff_q_pvs_preserve_resultfirstpositive. dst_positive_code_preserve_resultfirst = ff_q_pvs_preserve_resultfirstpositive * S ((S (dst_index_preserve_result)) * dst_positive_scale_preserve_resultfirst) + (dst_positive_preserve_resultfirst))) /\ (((((exists ff_h_pvs_preserve_resultfirstnegative. ff_h_pvs_preserve_resultfirstnegative + S (dst_negative_preserve_resultfirst) = S ((S (dst_index_preserve_result)) * dst_negative_scale_preserve_resultfirst)) /\ exists ff_q_pvs_preserve_resultfirstnegative. dst_negative_code_preserve_resultfirst = ff_q_pvs_preserve_resultfirstnegative * S ((S (dst_index_preserve_result)) * dst_negative_scale_preserve_resultfirst) + (dst_negative_preserve_resultfirst))) /\ (exists ge_balance_positive_preserve_resultfirstvalue ge_balance_negative_preserve_resultfirstvalue. (((((dst_first_preserve_result) = 2 * (ge_balance_positive_preserve_resultfirstvalue) /\ (ge_balance_negative_preserve_resultfirstvalue) = 0) \/ exists ge_signed_half_preserve_resultfirstvaluedecode. (((dst_first_preserve_result) = 2 * ge_signed_half_preserve_resultfirstvaluedecode + 1 /\ (ge_balance_positive_preserve_resultfirstvalue) = 0) /\ (ge_balance_negative_preserve_resultfirstvalue) = S ge_signed_half_preserve_resultfirstvaluedecode))) /\ ((dst_positive_preserve_resultfirst) + ge_balance_negative_preserve_resultfirstvalue = (dst_negative_preserve_resultfirst) + ge_balance_positive_preserve_resultfirstvalue))))))))) -> (exists dst_positive_code_preserve_resultsecond dst_positive_scale_preserve_resultsecond dst_negative_code_preserve_resultsecond dst_negative_scale_preserve_resultsecond dst_positive_preserve_resultsecond dst_negative_preserve_resultsecond. (((G) = (((((dst_positive_code_preserve_resultsecond) + (dst_positive_scale_preserve_resultsecond)) * S ((dst_positive_code_preserve_resultsecond) + (dst_positive_scale_preserve_resultsecond)) + ((dst_positive_scale_preserve_resultsecond) + (dst_positive_scale_preserve_resultsecond))) + (((dst_negative_code_preserve_resultsecond) + (dst_negative_scale_preserve_resultsecond)) * S ((dst_negative_code_preserve_resultsecond) + (dst_negative_scale_preserve_resultsecond)) + ((dst_negative_scale_preserve_resultsecond) + (dst_negative_scale_preserve_resultsecond)))) * S ((((dst_positive_code_preserve_resultsecond) + (dst_positive_scale_preserve_resultsecond)) * S ((dst_positive_code_preserve_resultsecond) + (dst_positive_scale_preserve_resultsecond)) + ((dst_positive_scale_preserve_resultsecond) + (dst_positive_scale_preserve_resultsecond))) + (((dst_negative_code_preserve_resultsecond) + (dst_negative_scale_preserve_resultsecond)) * S ((dst_negative_code_preserve_resultsecond) + (dst_negative_scale_preserve_resultsecond)) + ((dst_negative_scale_preserve_resultsecond) + (dst_negative_scale_preserve_resultsecond)))) + ((((dst_negative_code_preserve_resultsecond) + (dst_negative_scale_preserve_resultsecond)) * S ((dst_negative_code_preserve_resultsecond) + (dst_negative_scale_preserve_resultsecond)) + ((dst_negative_scale_preserve_resultsecond) + (dst_negative_scale_preserve_resultsecond))) + (((dst_negative_code_preserve_resultsecond) + (dst_negative_scale_preserve_resultsecond)) * S ((dst_negative_code_preserve_resultsecond) + (dst_negative_scale_preserve_resultsecond)) + ((dst_negative_scale_preserve_resultsecond) + (dst_negative_scale_preserve_resultsecond)))))) /\ (((((exists ff_h_pvs_preserve_resultsecondpositive. ff_h_pvs_preserve_resultsecondpositive + S (dst_positive_preserve_resultsecond) = S ((S (dst_index_preserve_result)) * dst_positive_scale_preserve_resultsecond)) /\ exists ff_q_pvs_preserve_resultsecondpositive. dst_positive_code_preserve_resultsecond = ff_q_pvs_preserve_resultsecondpositive * S ((S (dst_index_preserve_result)) * dst_positive_scale_preserve_resultsecond) + (dst_positive_preserve_resultsecond))) /\ (((((exists ff_h_pvs_preserve_resultsecondnegative. ff_h_pvs_preserve_resultsecondnegative + S (dst_negative_preserve_resultsecond) = S ((S (dst_index_preserve_result)) * dst_negative_scale_preserve_resultsecond)) /\ exists ff_q_pvs_preserve_resultsecondnegative. dst_negative_code_preserve_resultsecond = ff_q_pvs_preserve_resultsecondnegative * S ((S (dst_index_preserve_result)) * dst_negative_scale_preserve_resultsecond) + (dst_negative_preserve_resultsecond))) /\ (exists ge_balance_positive_preserve_resultsecondvalue ge_balance_negative_preserve_resultsecondvalue. (((((dst_second_preserve_result) = 2 * (ge_balance_positive_preserve_resultsecondvalue) /\ (ge_balance_negative_preserve_resultsecondvalue) = 0) \/ exists ge_signed_half_preserve_resultsecondvaluedecode. (((dst_second_preserve_result) = 2 * ge_signed_half_preserve_resultsecondvaluedecode + 1 /\ (ge_balance_positive_preserve_resultsecondvalue) = 0) /\ (ge_balance_negative_preserve_resultsecondvalue) = S ge_signed_half_preserve_resultsecondvaluedecode))) /\ ((dst_positive_preserve_resultsecond) + ge_balance_negative_preserve_resultsecondvalue = (dst_negative_preserve_resultsecond) + ge_balance_positive_preserve_resultsecondvalue))))))))) -> dst_first_preserve_result = dst_second_preserve_result)