divisor_signed_table_reindex_from_components

Exact expanded first-order arithmetic statement

forall F G pb pc nb nc qb qc mb mc 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)))))) -> ((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 fms_i_component_datapositive fms_j_component_datapositive fms_v_component_datapositive. (exists fms_gap_component_datapositive. fms_gap_component_datapositive + S (fms_i_component_datapositive) = (l)) -> (((exists fs_h_fms_component_datapositive_index. fs_h_fms_component_datapositive_index + S (fms_j_component_datapositive) = S ((S (fms_i_component_datapositive)) * s)) /\ exists fs_q_fms_component_datapositive_index. r = fs_q_fms_component_datapositive_index * S ((S (fms_i_component_datapositive)) * s) + (fms_j_component_datapositive))) -> (((exists fs_h_fms_component_datapositive_source. fs_h_fms_component_datapositive_source + S (fms_v_component_datapositive) = S ((S (fms_j_component_datapositive)) * pc)) /\ exists fs_q_fms_component_datapositive_source. pb = fs_q_fms_component_datapositive_source * S ((S (fms_j_component_datapositive)) * pc) + (fms_v_component_datapositive))) -> (((exists fs_h_fms_component_datapositive_target. fs_h_fms_component_datapositive_target + S (fms_v_component_datapositive) = S ((S (fms_i_component_datapositive)) * qc)) /\ exists fs_q_fms_component_datapositive_target. qb = fs_q_fms_component_datapositive_target * S ((S (fms_i_component_datapositive)) * qc) + (fms_v_component_datapositive)))) /\ (forall fms_i_component_datanegative fms_j_component_datanegative fms_v_component_datanegative. (exists fms_gap_component_datanegative. fms_gap_component_datanegative + S (fms_i_component_datanegative) = (l)) -> (((exists fs_h_fms_component_datanegative_index. fs_h_fms_component_datanegative_index + S (fms_j_component_datanegative) = S ((S (fms_i_component_datanegative)) * s)) /\ exists fs_q_fms_component_datanegative_index. r = fs_q_fms_component_datanegative_index * S ((S (fms_i_component_datanegative)) * s) + (fms_j_component_datanegative))) -> (((exists fs_h_fms_component_datanegative_source. fs_h_fms_component_datanegative_source + S (fms_v_component_datanegative) = S ((S (fms_j_component_datanegative)) * nc)) /\ exists fs_q_fms_component_datanegative_source. nb = fs_q_fms_component_datanegative_source * S ((S (fms_j_component_datanegative)) * nc) + (fms_v_component_datanegative))) -> (((exists fs_h_fms_component_datanegative_target. fs_h_fms_component_datanegative_target + S (fms_v_component_datanegative) = S ((S (fms_i_component_datanegative)) * mc)) /\ exists fs_q_fms_component_datanegative_target. mb = fs_q_fms_component_datanegative_target * S ((S (fms_i_component_datanegative)) * mc) + (fms_v_component_datanegative)))))) -> (forall dsr_index_component_result dsr_image_component_result dsr_value_component_result. (exists pvs_gap_component_resultbound. pvs_gap_component_resultbound + S (dsr_index_component_result) = (l)) -> (((exists ff_h_pvs_component_resultmap. ff_h_pvs_component_resultmap + S (dsr_image_component_result) = S ((S (dsr_index_component_result)) * s)) /\ exists ff_q_pvs_component_resultmap. r = ff_q_pvs_component_resultmap * S ((S (dsr_index_component_result)) * s) + (dsr_image_component_result))) -> (exists dst_positive_code_component_resultsource dst_positive_scale_component_resultsource dst_negative_code_component_resultsource dst_negative_scale_component_resultsource dst_positive_component_resultsource dst_negative_component_resultsource. (((F) = (((((dst_positive_code_component_resultsource) + (dst_positive_scale_component_resultsource)) * S ((dst_positive_code_component_resultsource) + (dst_positive_scale_component_resultsource)) + ((dst_positive_scale_component_resultsource) + (dst_positive_scale_component_resultsource))) + (((dst_negative_code_component_resultsource) + (dst_negative_scale_component_resultsource)) * S ((dst_negative_code_component_resultsource) + (dst_negative_scale_component_resultsource)) + ((dst_negative_scale_component_resultsource) + (dst_negative_scale_component_resultsource)))) * S ((((dst_positive_code_component_resultsource) + (dst_positive_scale_component_resultsource)) * S ((dst_positive_code_component_resultsource) + (dst_positive_scale_component_resultsource)) + ((dst_positive_scale_component_resultsource) + (dst_positive_scale_component_resultsource))) + (((dst_negative_code_component_resultsource) + (dst_negative_scale_component_resultsource)) * S ((dst_negative_code_component_resultsource) + (dst_negative_scale_component_resultsource)) + ((dst_negative_scale_component_resultsource) + (dst_negative_scale_component_resultsource)))) + ((((dst_negative_code_component_resultsource) + (dst_negative_scale_component_resultsource)) * S ((dst_negative_code_component_resultsource) + (dst_negative_scale_component_resultsource)) + ((dst_negative_scale_component_resultsource) + (dst_negative_scale_component_resultsource))) + (((dst_negative_code_component_resultsource) + (dst_negative_scale_component_resultsource)) * S ((dst_negative_code_component_resultsource) + (dst_negative_scale_component_resultsource)) + ((dst_negative_scale_component_resultsource) + (dst_negative_scale_component_resultsource)))))) /\ (((((exists ff_h_pvs_component_resultsourcepositive. ff_h_pvs_component_resultsourcepositive + S (dst_positive_component_resultsource) = S ((S (dsr_image_component_result)) * dst_positive_scale_component_resultsource)) /\ exists ff_q_pvs_component_resultsourcepositive. dst_positive_code_component_resultsource = ff_q_pvs_component_resultsourcepositive * S ((S (dsr_image_component_result)) * dst_positive_scale_component_resultsource) + (dst_positive_component_resultsource))) /\ (((((exists ff_h_pvs_component_resultsourcenegative. ff_h_pvs_component_resultsourcenegative + S (dst_negative_component_resultsource) = S ((S (dsr_image_component_result)) * dst_negative_scale_component_resultsource)) /\ exists ff_q_pvs_component_resultsourcenegative. dst_negative_code_component_resultsource = ff_q_pvs_component_resultsourcenegative * S ((S (dsr_image_component_result)) * dst_negative_scale_component_resultsource) + (dst_negative_component_resultsource))) /\ (exists ge_balance_positive_component_resultsourcevalue ge_balance_negative_component_resultsourcevalue. (((((dsr_value_component_result) = 2 * (ge_balance_positive_component_resultsourcevalue) /\ (ge_balance_negative_component_resultsourcevalue) = 0) \/ exists ge_signed_half_component_resultsourcevaluedecode. (((dsr_value_component_result) = 2 * ge_signed_half_component_resultsourcevaluedecode + 1 /\ (ge_balance_positive_component_resultsourcevalue) = 0) /\ (ge_balance_negative_component_resultsourcevalue) = S ge_signed_half_component_resultsourcevaluedecode))) /\ ((dst_positive_component_resultsource) + ge_balance_negative_component_resultsourcevalue = (dst_negative_component_resultsource) + ge_balance_positive_component_resultsourcevalue))))))))) -> (exists dst_positive_code_component_resulttarget dst_positive_scale_component_resulttarget dst_negative_code_component_resulttarget dst_negative_scale_component_resulttarget dst_positive_component_resulttarget dst_negative_component_resulttarget. (((G) = (((((dst_positive_code_component_resulttarget) + (dst_positive_scale_component_resulttarget)) * S ((dst_positive_code_component_resulttarget) + (dst_positive_scale_component_resulttarget)) + ((dst_positive_scale_component_resulttarget) + (dst_positive_scale_component_resulttarget))) + (((dst_negative_code_component_resulttarget) + (dst_negative_scale_component_resulttarget)) * S ((dst_negative_code_component_resulttarget) + (dst_negative_scale_component_resulttarget)) + ((dst_negative_scale_component_resulttarget) + (dst_negative_scale_component_resulttarget)))) * S ((((dst_positive_code_component_resulttarget) + (dst_positive_scale_component_resulttarget)) * S ((dst_positive_code_component_resulttarget) + (dst_positive_scale_component_resulttarget)) + ((dst_positive_scale_component_resulttarget) + (dst_positive_scale_component_resulttarget))) + (((dst_negative_code_component_resulttarget) + (dst_negative_scale_component_resulttarget)) * S ((dst_negative_code_component_resulttarget) + (dst_negative_scale_component_resulttarget)) + ((dst_negative_scale_component_resulttarget) + (dst_negative_scale_component_resulttarget)))) + ((((dst_negative_code_component_resulttarget) + (dst_negative_scale_component_resulttarget)) * S ((dst_negative_code_component_resulttarget) + (dst_negative_scale_component_resulttarget)) + ((dst_negative_scale_component_resulttarget) + (dst_negative_scale_component_resulttarget))) + (((dst_negative_code_component_resulttarget) + (dst_negative_scale_component_resulttarget)) * S ((dst_negative_code_component_resulttarget) + (dst_negative_scale_component_resulttarget)) + ((dst_negative_scale_component_resulttarget) + (dst_negative_scale_component_resulttarget)))))) /\ (((((exists ff_h_pvs_component_resulttargetpositive. ff_h_pvs_component_resulttargetpositive + S (dst_positive_component_resulttarget) = S ((S (dsr_index_component_result)) * dst_positive_scale_component_resulttarget)) /\ exists ff_q_pvs_component_resulttargetpositive. dst_positive_code_component_resulttarget = ff_q_pvs_component_resulttargetpositive * S ((S (dsr_index_component_result)) * dst_positive_scale_component_resulttarget) + (dst_positive_component_resulttarget))) /\ (((((exists ff_h_pvs_component_resulttargetnegative. ff_h_pvs_component_resulttargetnegative + S (dst_negative_component_resulttarget) = S ((S (dsr_index_component_result)) * dst_negative_scale_component_resulttarget)) /\ exists ff_q_pvs_component_resulttargetnegative. dst_negative_code_component_resulttarget = ff_q_pvs_component_resulttargetnegative * S ((S (dsr_index_component_result)) * dst_negative_scale_component_resulttarget) + (dst_negative_component_resulttarget))) /\ (exists ge_balance_positive_component_resulttargetvalue ge_balance_negative_component_resulttargetvalue. (((((dsr_value_component_result) = 2 * (ge_balance_positive_component_resulttargetvalue) /\ (ge_balance_negative_component_resulttargetvalue) = 0) \/ exists ge_signed_half_component_resulttargetvaluedecode. (((dsr_value_component_result) = 2 * ge_signed_half_component_resulttargetvaluedecode + 1 /\ (ge_balance_positive_component_resulttargetvalue) = 0) /\ (ge_balance_negative_component_resulttargetvalue) = S ge_signed_half_component_resulttargetvaluedecode))) /\ ((dst_positive_component_resulttarget) + ge_balance_negative_component_resulttargetvalue = (dst_negative_component_resulttarget) + ge_balance_positive_component_resulttargetvalue))))))))))