divisor_signed_table_reindex_functional

Exact expanded first-order arithmetic statement

forall F G H pb pc nb nc r s 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)))))) -> (forall dsr_index_functional_first dsr_image_functional_first dsr_value_functional_first. (exists pvs_gap_functional_firstbound. pvs_gap_functional_firstbound + S (dsr_index_functional_first) = (l)) -> (((exists ff_h_pvs_functional_firstmap. ff_h_pvs_functional_firstmap + S (dsr_image_functional_first) = S ((S (dsr_index_functional_first)) * s)) /\ exists ff_q_pvs_functional_firstmap. r = ff_q_pvs_functional_firstmap * S ((S (dsr_index_functional_first)) * s) + (dsr_image_functional_first))) -> (exists dst_positive_code_functional_firstsource dst_positive_scale_functional_firstsource dst_negative_code_functional_firstsource dst_negative_scale_functional_firstsource dst_positive_functional_firstsource dst_negative_functional_firstsource. (((F) = (((((dst_positive_code_functional_firstsource) + (dst_positive_scale_functional_firstsource)) * S ((dst_positive_code_functional_firstsource) + (dst_positive_scale_functional_firstsource)) + ((dst_positive_scale_functional_firstsource) + (dst_positive_scale_functional_firstsource))) + (((dst_negative_code_functional_firstsource) + (dst_negative_scale_functional_firstsource)) * S ((dst_negative_code_functional_firstsource) + (dst_negative_scale_functional_firstsource)) + ((dst_negative_scale_functional_firstsource) + (dst_negative_scale_functional_firstsource)))) * S ((((dst_positive_code_functional_firstsource) + (dst_positive_scale_functional_firstsource)) * S ((dst_positive_code_functional_firstsource) + (dst_positive_scale_functional_firstsource)) + ((dst_positive_scale_functional_firstsource) + (dst_positive_scale_functional_firstsource))) + (((dst_negative_code_functional_firstsource) + (dst_negative_scale_functional_firstsource)) * S ((dst_negative_code_functional_firstsource) + (dst_negative_scale_functional_firstsource)) + ((dst_negative_scale_functional_firstsource) + (dst_negative_scale_functional_firstsource)))) + ((((dst_negative_code_functional_firstsource) + (dst_negative_scale_functional_firstsource)) * S ((dst_negative_code_functional_firstsource) + (dst_negative_scale_functional_firstsource)) + ((dst_negative_scale_functional_firstsource) + (dst_negative_scale_functional_firstsource))) + (((dst_negative_code_functional_firstsource) + (dst_negative_scale_functional_firstsource)) * S ((dst_negative_code_functional_firstsource) + (dst_negative_scale_functional_firstsource)) + ((dst_negative_scale_functional_firstsource) + (dst_negative_scale_functional_firstsource)))))) /\ (((((exists ff_h_pvs_functional_firstsourcepositive. ff_h_pvs_functional_firstsourcepositive + S (dst_positive_functional_firstsource) = S ((S (dsr_image_functional_first)) * dst_positive_scale_functional_firstsource)) /\ exists ff_q_pvs_functional_firstsourcepositive. dst_positive_code_functional_firstsource = ff_q_pvs_functional_firstsourcepositive * S ((S (dsr_image_functional_first)) * dst_positive_scale_functional_firstsource) + (dst_positive_functional_firstsource))) /\ (((((exists ff_h_pvs_functional_firstsourcenegative. ff_h_pvs_functional_firstsourcenegative + S (dst_negative_functional_firstsource) = S ((S (dsr_image_functional_first)) * dst_negative_scale_functional_firstsource)) /\ exists ff_q_pvs_functional_firstsourcenegative. dst_negative_code_functional_firstsource = ff_q_pvs_functional_firstsourcenegative * S ((S (dsr_image_functional_first)) * dst_negative_scale_functional_firstsource) + (dst_negative_functional_firstsource))) /\ (exists ge_balance_positive_functional_firstsourcevalue ge_balance_negative_functional_firstsourcevalue. (((((dsr_value_functional_first) = 2 * (ge_balance_positive_functional_firstsourcevalue) /\ (ge_balance_negative_functional_firstsourcevalue) = 0) \/ exists ge_signed_half_functional_firstsourcevaluedecode. (((dsr_value_functional_first) = 2 * ge_signed_half_functional_firstsourcevaluedecode + 1 /\ (ge_balance_positive_functional_firstsourcevalue) = 0) /\ (ge_balance_negative_functional_firstsourcevalue) = S ge_signed_half_functional_firstsourcevaluedecode))) /\ ((dst_positive_functional_firstsource) + ge_balance_negative_functional_firstsourcevalue = (dst_negative_functional_firstsource) + ge_balance_positive_functional_firstsourcevalue))))))))) -> (exists dst_positive_code_functional_firsttarget dst_positive_scale_functional_firsttarget dst_negative_code_functional_firsttarget dst_negative_scale_functional_firsttarget dst_positive_functional_firsttarget dst_negative_functional_firsttarget. (((G) = (((((dst_positive_code_functional_firsttarget) + (dst_positive_scale_functional_firsttarget)) * S ((dst_positive_code_functional_firsttarget) + (dst_positive_scale_functional_firsttarget)) + ((dst_positive_scale_functional_firsttarget) + (dst_positive_scale_functional_firsttarget))) + (((dst_negative_code_functional_firsttarget) + (dst_negative_scale_functional_firsttarget)) * S ((dst_negative_code_functional_firsttarget) + (dst_negative_scale_functional_firsttarget)) + ((dst_negative_scale_functional_firsttarget) + (dst_negative_scale_functional_firsttarget)))) * S ((((dst_positive_code_functional_firsttarget) + (dst_positive_scale_functional_firsttarget)) * S ((dst_positive_code_functional_firsttarget) + (dst_positive_scale_functional_firsttarget)) + ((dst_positive_scale_functional_firsttarget) + (dst_positive_scale_functional_firsttarget))) + (((dst_negative_code_functional_firsttarget) + (dst_negative_scale_functional_firsttarget)) * S ((dst_negative_code_functional_firsttarget) + (dst_negative_scale_functional_firsttarget)) + ((dst_negative_scale_functional_firsttarget) + (dst_negative_scale_functional_firsttarget)))) + ((((dst_negative_code_functional_firsttarget) + (dst_negative_scale_functional_firsttarget)) * S ((dst_negative_code_functional_firsttarget) + (dst_negative_scale_functional_firsttarget)) + ((dst_negative_scale_functional_firsttarget) + (dst_negative_scale_functional_firsttarget))) + (((dst_negative_code_functional_firsttarget) + (dst_negative_scale_functional_firsttarget)) * S ((dst_negative_code_functional_firsttarget) + (dst_negative_scale_functional_firsttarget)) + ((dst_negative_scale_functional_firsttarget) + (dst_negative_scale_functional_firsttarget)))))) /\ (((((exists ff_h_pvs_functional_firsttargetpositive. ff_h_pvs_functional_firsttargetpositive + S (dst_positive_functional_firsttarget) = S ((S (dsr_index_functional_first)) * dst_positive_scale_functional_firsttarget)) /\ exists ff_q_pvs_functional_firsttargetpositive. dst_positive_code_functional_firsttarget = ff_q_pvs_functional_firsttargetpositive * S ((S (dsr_index_functional_first)) * dst_positive_scale_functional_firsttarget) + (dst_positive_functional_firsttarget))) /\ (((((exists ff_h_pvs_functional_firsttargetnegative. ff_h_pvs_functional_firsttargetnegative + S (dst_negative_functional_firsttarget) = S ((S (dsr_index_functional_first)) * dst_negative_scale_functional_firsttarget)) /\ exists ff_q_pvs_functional_firsttargetnegative. dst_negative_code_functional_firsttarget = ff_q_pvs_functional_firsttargetnegative * S ((S (dsr_index_functional_first)) * dst_negative_scale_functional_firsttarget) + (dst_negative_functional_firsttarget))) /\ (exists ge_balance_positive_functional_firsttargetvalue ge_balance_negative_functional_firsttargetvalue. (((((dsr_value_functional_first) = 2 * (ge_balance_positive_functional_firsttargetvalue) /\ (ge_balance_negative_functional_firsttargetvalue) = 0) \/ exists ge_signed_half_functional_firsttargetvaluedecode. (((dsr_value_functional_first) = 2 * ge_signed_half_functional_firsttargetvaluedecode + 1 /\ (ge_balance_positive_functional_firsttargetvalue) = 0) /\ (ge_balance_negative_functional_firsttargetvalue) = S ge_signed_half_functional_firsttargetvaluedecode))) /\ ((dst_positive_functional_firsttarget) + ge_balance_negative_functional_firsttargetvalue = (dst_negative_functional_firsttarget) + ge_balance_positive_functional_firsttargetvalue)))))))))) -> (forall dsr_index_functional_second dsr_image_functional_second dsr_value_functional_second. (exists pvs_gap_functional_secondbound. pvs_gap_functional_secondbound + S (dsr_index_functional_second) = (l)) -> (((exists ff_h_pvs_functional_secondmap. ff_h_pvs_functional_secondmap + S (dsr_image_functional_second) = S ((S (dsr_index_functional_second)) * s)) /\ exists ff_q_pvs_functional_secondmap. r = ff_q_pvs_functional_secondmap * S ((S (dsr_index_functional_second)) * s) + (dsr_image_functional_second))) -> (exists dst_positive_code_functional_secondsource dst_positive_scale_functional_secondsource dst_negative_code_functional_secondsource dst_negative_scale_functional_secondsource dst_positive_functional_secondsource dst_negative_functional_secondsource. (((F) = (((((dst_positive_code_functional_secondsource) + (dst_positive_scale_functional_secondsource)) * S ((dst_positive_code_functional_secondsource) + (dst_positive_scale_functional_secondsource)) + ((dst_positive_scale_functional_secondsource) + (dst_positive_scale_functional_secondsource))) + (((dst_negative_code_functional_secondsource) + (dst_negative_scale_functional_secondsource)) * S ((dst_negative_code_functional_secondsource) + (dst_negative_scale_functional_secondsource)) + ((dst_negative_scale_functional_secondsource) + (dst_negative_scale_functional_secondsource)))) * S ((((dst_positive_code_functional_secondsource) + (dst_positive_scale_functional_secondsource)) * S ((dst_positive_code_functional_secondsource) + (dst_positive_scale_functional_secondsource)) + ((dst_positive_scale_functional_secondsource) + (dst_positive_scale_functional_secondsource))) + (((dst_negative_code_functional_secondsource) + (dst_negative_scale_functional_secondsource)) * S ((dst_negative_code_functional_secondsource) + (dst_negative_scale_functional_secondsource)) + ((dst_negative_scale_functional_secondsource) + (dst_negative_scale_functional_secondsource)))) + ((((dst_negative_code_functional_secondsource) + (dst_negative_scale_functional_secondsource)) * S ((dst_negative_code_functional_secondsource) + (dst_negative_scale_functional_secondsource)) + ((dst_negative_scale_functional_secondsource) + (dst_negative_scale_functional_secondsource))) + (((dst_negative_code_functional_secondsource) + (dst_negative_scale_functional_secondsource)) * S ((dst_negative_code_functional_secondsource) + (dst_negative_scale_functional_secondsource)) + ((dst_negative_scale_functional_secondsource) + (dst_negative_scale_functional_secondsource)))))) /\ (((((exists ff_h_pvs_functional_secondsourcepositive. ff_h_pvs_functional_secondsourcepositive + S (dst_positive_functional_secondsource) = S ((S (dsr_image_functional_second)) * dst_positive_scale_functional_secondsource)) /\ exists ff_q_pvs_functional_secondsourcepositive. dst_positive_code_functional_secondsource = ff_q_pvs_functional_secondsourcepositive * S ((S (dsr_image_functional_second)) * dst_positive_scale_functional_secondsource) + (dst_positive_functional_secondsource))) /\ (((((exists ff_h_pvs_functional_secondsourcenegative. ff_h_pvs_functional_secondsourcenegative + S (dst_negative_functional_secondsource) = S ((S (dsr_image_functional_second)) * dst_negative_scale_functional_secondsource)) /\ exists ff_q_pvs_functional_secondsourcenegative. dst_negative_code_functional_secondsource = ff_q_pvs_functional_secondsourcenegative * S ((S (dsr_image_functional_second)) * dst_negative_scale_functional_secondsource) + (dst_negative_functional_secondsource))) /\ (exists ge_balance_positive_functional_secondsourcevalue ge_balance_negative_functional_secondsourcevalue. (((((dsr_value_functional_second) = 2 * (ge_balance_positive_functional_secondsourcevalue) /\ (ge_balance_negative_functional_secondsourcevalue) = 0) \/ exists ge_signed_half_functional_secondsourcevaluedecode. (((dsr_value_functional_second) = 2 * ge_signed_half_functional_secondsourcevaluedecode + 1 /\ (ge_balance_positive_functional_secondsourcevalue) = 0) /\ (ge_balance_negative_functional_secondsourcevalue) = S ge_signed_half_functional_secondsourcevaluedecode))) /\ ((dst_positive_functional_secondsource) + ge_balance_negative_functional_secondsourcevalue = (dst_negative_functional_secondsource) + ge_balance_positive_functional_secondsourcevalue))))))))) -> (exists dst_positive_code_functional_secondtarget dst_positive_scale_functional_secondtarget dst_negative_code_functional_secondtarget dst_negative_scale_functional_secondtarget dst_positive_functional_secondtarget dst_negative_functional_secondtarget. (((H) = (((((dst_positive_code_functional_secondtarget) + (dst_positive_scale_functional_secondtarget)) * S ((dst_positive_code_functional_secondtarget) + (dst_positive_scale_functional_secondtarget)) + ((dst_positive_scale_functional_secondtarget) + (dst_positive_scale_functional_secondtarget))) + (((dst_negative_code_functional_secondtarget) + (dst_negative_scale_functional_secondtarget)) * S ((dst_negative_code_functional_secondtarget) + (dst_negative_scale_functional_secondtarget)) + ((dst_negative_scale_functional_secondtarget) + (dst_negative_scale_functional_secondtarget)))) * S ((((dst_positive_code_functional_secondtarget) + (dst_positive_scale_functional_secondtarget)) * S ((dst_positive_code_functional_secondtarget) + (dst_positive_scale_functional_secondtarget)) + ((dst_positive_scale_functional_secondtarget) + (dst_positive_scale_functional_secondtarget))) + (((dst_negative_code_functional_secondtarget) + (dst_negative_scale_functional_secondtarget)) * S ((dst_negative_code_functional_secondtarget) + (dst_negative_scale_functional_secondtarget)) + ((dst_negative_scale_functional_secondtarget) + (dst_negative_scale_functional_secondtarget)))) + ((((dst_negative_code_functional_secondtarget) + (dst_negative_scale_functional_secondtarget)) * S ((dst_negative_code_functional_secondtarget) + (dst_negative_scale_functional_secondtarget)) + ((dst_negative_scale_functional_secondtarget) + (dst_negative_scale_functional_secondtarget))) + (((dst_negative_code_functional_secondtarget) + (dst_negative_scale_functional_secondtarget)) * S ((dst_negative_code_functional_secondtarget) + (dst_negative_scale_functional_secondtarget)) + ((dst_negative_scale_functional_secondtarget) + (dst_negative_scale_functional_secondtarget)))))) /\ (((((exists ff_h_pvs_functional_secondtargetpositive. ff_h_pvs_functional_secondtargetpositive + S (dst_positive_functional_secondtarget) = S ((S (dsr_index_functional_second)) * dst_positive_scale_functional_secondtarget)) /\ exists ff_q_pvs_functional_secondtargetpositive. dst_positive_code_functional_secondtarget = ff_q_pvs_functional_secondtargetpositive * S ((S (dsr_index_functional_second)) * dst_positive_scale_functional_secondtarget) + (dst_positive_functional_secondtarget))) /\ (((((exists ff_h_pvs_functional_secondtargetnegative. ff_h_pvs_functional_secondtargetnegative + S (dst_negative_functional_secondtarget) = S ((S (dsr_index_functional_second)) * dst_negative_scale_functional_secondtarget)) /\ exists ff_q_pvs_functional_secondtargetnegative. dst_negative_code_functional_secondtarget = ff_q_pvs_functional_secondtargetnegative * S ((S (dsr_index_functional_second)) * dst_negative_scale_functional_secondtarget) + (dst_negative_functional_secondtarget))) /\ (exists ge_balance_positive_functional_secondtargetvalue ge_balance_negative_functional_secondtargetvalue. (((((dsr_value_functional_second) = 2 * (ge_balance_positive_functional_secondtargetvalue) /\ (ge_balance_negative_functional_secondtargetvalue) = 0) \/ exists ge_signed_half_functional_secondtargetvaluedecode. (((dsr_value_functional_second) = 2 * ge_signed_half_functional_secondtargetvaluedecode + 1 /\ (ge_balance_positive_functional_secondtargetvalue) = 0) /\ (ge_balance_negative_functional_secondtargetvalue) = S ge_signed_half_functional_secondtargetvaluedecode))) /\ ((dst_positive_functional_secondtarget) + ge_balance_negative_functional_secondtargetvalue = (dst_negative_functional_secondtarget) + ge_balance_positive_functional_secondtargetvalue)))))))))) -> (forall dst_index_functional_result dst_first_functional_result dst_second_functional_result. (exists pvs_gap_functional_resultbound. pvs_gap_functional_resultbound + S (dst_index_functional_result) = (l)) -> (exists dst_positive_code_functional_resultfirst dst_positive_scale_functional_resultfirst dst_negative_code_functional_resultfirst dst_negative_scale_functional_resultfirst dst_positive_functional_resultfirst dst_negative_functional_resultfirst. (((G) = (((((dst_positive_code_functional_resultfirst) + (dst_positive_scale_functional_resultfirst)) * S ((dst_positive_code_functional_resultfirst) + (dst_positive_scale_functional_resultfirst)) + ((dst_positive_scale_functional_resultfirst) + (dst_positive_scale_functional_resultfirst))) + (((dst_negative_code_functional_resultfirst) + (dst_negative_scale_functional_resultfirst)) * S ((dst_negative_code_functional_resultfirst) + (dst_negative_scale_functional_resultfirst)) + ((dst_negative_scale_functional_resultfirst) + (dst_negative_scale_functional_resultfirst)))) * S ((((dst_positive_code_functional_resultfirst) + (dst_positive_scale_functional_resultfirst)) * S ((dst_positive_code_functional_resultfirst) + (dst_positive_scale_functional_resultfirst)) + ((dst_positive_scale_functional_resultfirst) + (dst_positive_scale_functional_resultfirst))) + (((dst_negative_code_functional_resultfirst) + (dst_negative_scale_functional_resultfirst)) * S ((dst_negative_code_functional_resultfirst) + (dst_negative_scale_functional_resultfirst)) + ((dst_negative_scale_functional_resultfirst) + (dst_negative_scale_functional_resultfirst)))) + ((((dst_negative_code_functional_resultfirst) + (dst_negative_scale_functional_resultfirst)) * S ((dst_negative_code_functional_resultfirst) + (dst_negative_scale_functional_resultfirst)) + ((dst_negative_scale_functional_resultfirst) + (dst_negative_scale_functional_resultfirst))) + (((dst_negative_code_functional_resultfirst) + (dst_negative_scale_functional_resultfirst)) * S ((dst_negative_code_functional_resultfirst) + (dst_negative_scale_functional_resultfirst)) + ((dst_negative_scale_functional_resultfirst) + (dst_negative_scale_functional_resultfirst)))))) /\ (((((exists ff_h_pvs_functional_resultfirstpositive. ff_h_pvs_functional_resultfirstpositive + S (dst_positive_functional_resultfirst) = S ((S (dst_index_functional_result)) * dst_positive_scale_functional_resultfirst)) /\ exists ff_q_pvs_functional_resultfirstpositive. dst_positive_code_functional_resultfirst = ff_q_pvs_functional_resultfirstpositive * S ((S (dst_index_functional_result)) * dst_positive_scale_functional_resultfirst) + (dst_positive_functional_resultfirst))) /\ (((((exists ff_h_pvs_functional_resultfirstnegative. ff_h_pvs_functional_resultfirstnegative + S (dst_negative_functional_resultfirst) = S ((S (dst_index_functional_result)) * dst_negative_scale_functional_resultfirst)) /\ exists ff_q_pvs_functional_resultfirstnegative. dst_negative_code_functional_resultfirst = ff_q_pvs_functional_resultfirstnegative * S ((S (dst_index_functional_result)) * dst_negative_scale_functional_resultfirst) + (dst_negative_functional_resultfirst))) /\ (exists ge_balance_positive_functional_resultfirstvalue ge_balance_negative_functional_resultfirstvalue. (((((dst_first_functional_result) = 2 * (ge_balance_positive_functional_resultfirstvalue) /\ (ge_balance_negative_functional_resultfirstvalue) = 0) \/ exists ge_signed_half_functional_resultfirstvaluedecode. (((dst_first_functional_result) = 2 * ge_signed_half_functional_resultfirstvaluedecode + 1 /\ (ge_balance_positive_functional_resultfirstvalue) = 0) /\ (ge_balance_negative_functional_resultfirstvalue) = S ge_signed_half_functional_resultfirstvaluedecode))) /\ ((dst_positive_functional_resultfirst) + ge_balance_negative_functional_resultfirstvalue = (dst_negative_functional_resultfirst) + ge_balance_positive_functional_resultfirstvalue))))))))) -> (exists dst_positive_code_functional_resultsecond dst_positive_scale_functional_resultsecond dst_negative_code_functional_resultsecond dst_negative_scale_functional_resultsecond dst_positive_functional_resultsecond dst_negative_functional_resultsecond. (((H) = (((((dst_positive_code_functional_resultsecond) + (dst_positive_scale_functional_resultsecond)) * S ((dst_positive_code_functional_resultsecond) + (dst_positive_scale_functional_resultsecond)) + ((dst_positive_scale_functional_resultsecond) + (dst_positive_scale_functional_resultsecond))) + (((dst_negative_code_functional_resultsecond) + (dst_negative_scale_functional_resultsecond)) * S ((dst_negative_code_functional_resultsecond) + (dst_negative_scale_functional_resultsecond)) + ((dst_negative_scale_functional_resultsecond) + (dst_negative_scale_functional_resultsecond)))) * S ((((dst_positive_code_functional_resultsecond) + (dst_positive_scale_functional_resultsecond)) * S ((dst_positive_code_functional_resultsecond) + (dst_positive_scale_functional_resultsecond)) + ((dst_positive_scale_functional_resultsecond) + (dst_positive_scale_functional_resultsecond))) + (((dst_negative_code_functional_resultsecond) + (dst_negative_scale_functional_resultsecond)) * S ((dst_negative_code_functional_resultsecond) + (dst_negative_scale_functional_resultsecond)) + ((dst_negative_scale_functional_resultsecond) + (dst_negative_scale_functional_resultsecond)))) + ((((dst_negative_code_functional_resultsecond) + (dst_negative_scale_functional_resultsecond)) * S ((dst_negative_code_functional_resultsecond) + (dst_negative_scale_functional_resultsecond)) + ((dst_negative_scale_functional_resultsecond) + (dst_negative_scale_functional_resultsecond))) + (((dst_negative_code_functional_resultsecond) + (dst_negative_scale_functional_resultsecond)) * S ((dst_negative_code_functional_resultsecond) + (dst_negative_scale_functional_resultsecond)) + ((dst_negative_scale_functional_resultsecond) + (dst_negative_scale_functional_resultsecond)))))) /\ (((((exists ff_h_pvs_functional_resultsecondpositive. ff_h_pvs_functional_resultsecondpositive + S (dst_positive_functional_resultsecond) = S ((S (dst_index_functional_result)) * dst_positive_scale_functional_resultsecond)) /\ exists ff_q_pvs_functional_resultsecondpositive. dst_positive_code_functional_resultsecond = ff_q_pvs_functional_resultsecondpositive * S ((S (dst_index_functional_result)) * dst_positive_scale_functional_resultsecond) + (dst_positive_functional_resultsecond))) /\ (((((exists ff_h_pvs_functional_resultsecondnegative. ff_h_pvs_functional_resultsecondnegative + S (dst_negative_functional_resultsecond) = S ((S (dst_index_functional_result)) * dst_negative_scale_functional_resultsecond)) /\ exists ff_q_pvs_functional_resultsecondnegative. dst_negative_code_functional_resultsecond = ff_q_pvs_functional_resultsecondnegative * S ((S (dst_index_functional_result)) * dst_negative_scale_functional_resultsecond) + (dst_negative_functional_resultsecond))) /\ (exists ge_balance_positive_functional_resultsecondvalue ge_balance_negative_functional_resultsecondvalue. (((((dst_second_functional_result) = 2 * (ge_balance_positive_functional_resultsecondvalue) /\ (ge_balance_negative_functional_resultsecondvalue) = 0) \/ exists ge_signed_half_functional_resultsecondvaluedecode. (((dst_second_functional_result) = 2 * ge_signed_half_functional_resultsecondvaluedecode + 1 /\ (ge_balance_positive_functional_resultsecondvalue) = 0) /\ (ge_balance_negative_functional_resultsecondvalue) = S ge_signed_half_functional_resultsecondvaluedecode))) /\ ((dst_positive_functional_resultsecond) + ge_balance_negative_functional_resultsecondvalue = (dst_negative_functional_resultsecond) + ge_balance_positive_functional_resultsecondvalue))))))))) -> dst_first_functional_result = dst_second_functional_result)