dirichlet_coprime_grid_support_reindex

Exact expanded first-order arithmetic statement

forall N F G m n A B T Q r s. (((((~((N)=0)) /\ (((exists dst_positive_code_reindex_dataFtable dst_positive_scale_reindex_dataFtable dst_negative_code_reindex_dataFtable dst_negative_scale_reindex_dataFtable. (((F) = (((((dst_positive_code_reindex_dataFtable) + (dst_positive_scale_reindex_dataFtable)) * S ((dst_positive_code_reindex_dataFtable) + (dst_positive_scale_reindex_dataFtable)) + ((dst_positive_scale_reindex_dataFtable) + (dst_positive_scale_reindex_dataFtable))) + (((dst_negative_code_reindex_dataFtable) + (dst_negative_scale_reindex_dataFtable)) * S ((dst_negative_code_reindex_dataFtable) + (dst_negative_scale_reindex_dataFtable)) + ((dst_negative_scale_reindex_dataFtable) + (dst_negative_scale_reindex_dataFtable)))) * S ((((dst_positive_code_reindex_dataFtable) + (dst_positive_scale_reindex_dataFtable)) * S ((dst_positive_code_reindex_dataFtable) + (dst_positive_scale_reindex_dataFtable)) + ((dst_positive_scale_reindex_dataFtable) + (dst_positive_scale_reindex_dataFtable))) + (((dst_negative_code_reindex_dataFtable) + (dst_negative_scale_reindex_dataFtable)) * S ((dst_negative_code_reindex_dataFtable) + (dst_negative_scale_reindex_dataFtable)) + ((dst_negative_scale_reindex_dataFtable) + (dst_negative_scale_reindex_dataFtable)))) + ((((dst_negative_code_reindex_dataFtable) + (dst_negative_scale_reindex_dataFtable)) * S ((dst_negative_code_reindex_dataFtable) + (dst_negative_scale_reindex_dataFtable)) + ((dst_negative_scale_reindex_dataFtable) + (dst_negative_scale_reindex_dataFtable))) + (((dst_negative_code_reindex_dataFtable) + (dst_negative_scale_reindex_dataFtable)) * S ((dst_negative_code_reindex_dataFtable) + (dst_negative_scale_reindex_dataFtable)) + ((dst_negative_scale_reindex_dataFtable) + (dst_negative_scale_reindex_dataFtable)))))) /\ (forall dst_index_reindex_dataFtable. (exists pvs_le_gap_reindex_dataFtabledomain. pvs_le_gap_reindex_dataFtabledomain + (dst_index_reindex_dataFtable) = (N)) -> exists dst_positive_reindex_dataFtable dst_negative_reindex_dataFtable dst_value_reindex_dataFtable. ((((exists ff_h_pvs_reindex_dataFtableentrypositive. ff_h_pvs_reindex_dataFtableentrypositive + S (dst_positive_reindex_dataFtable) = S ((S (dst_index_reindex_dataFtable)) * dst_positive_scale_reindex_dataFtable)) /\ exists ff_q_pvs_reindex_dataFtableentrypositive. dst_positive_code_reindex_dataFtable = ff_q_pvs_reindex_dataFtableentrypositive * S ((S (dst_index_reindex_dataFtable)) * dst_positive_scale_reindex_dataFtable) + (dst_positive_reindex_dataFtable))) /\ (((((exists ff_h_pvs_reindex_dataFtableentrynegative. ff_h_pvs_reindex_dataFtableentrynegative + S (dst_negative_reindex_dataFtable) = S ((S (dst_index_reindex_dataFtable)) * dst_negative_scale_reindex_dataFtable)) /\ exists ff_q_pvs_reindex_dataFtableentrynegative. dst_negative_code_reindex_dataFtable = ff_q_pvs_reindex_dataFtableentrynegative * S ((S (dst_index_reindex_dataFtable)) * dst_negative_scale_reindex_dataFtable) + (dst_negative_reindex_dataFtable))) /\ (exists ge_balance_positive_reindex_dataFtableentryvalue ge_balance_negative_reindex_dataFtableentryvalue. (((((dst_value_reindex_dataFtable) = 2 * (ge_balance_positive_reindex_dataFtableentryvalue) /\ (ge_balance_negative_reindex_dataFtableentryvalue) = 0) \/ exists ge_signed_half_reindex_dataFtableentryvaluedecode. (((dst_value_reindex_dataFtable) = 2 * ge_signed_half_reindex_dataFtableentryvaluedecode + 1 /\ (ge_balance_positive_reindex_dataFtableentryvalue) = 0) /\ (ge_balance_negative_reindex_dataFtableentryvalue) = S ge_signed_half_reindex_dataFtableentryvaluedecode))) /\ ((dst_positive_reindex_dataFtable) + ge_balance_negative_reindex_dataFtableentryvalue = (dst_negative_reindex_dataFtable) + ge_balance_positive_reindex_dataFtableentryvalue))))))))) /\ (((exists dst_positive_code_reindex_dataFone dst_positive_scale_reindex_dataFone dst_negative_code_reindex_dataFone dst_negative_scale_reindex_dataFone dst_positive_reindex_dataFone dst_negative_reindex_dataFone. (((F) = (((((dst_positive_code_reindex_dataFone) + (dst_positive_scale_reindex_dataFone)) * S ((dst_positive_code_reindex_dataFone) + (dst_positive_scale_reindex_dataFone)) + ((dst_positive_scale_reindex_dataFone) + (dst_positive_scale_reindex_dataFone))) + (((dst_negative_code_reindex_dataFone) + (dst_negative_scale_reindex_dataFone)) * S ((dst_negative_code_reindex_dataFone) + (dst_negative_scale_reindex_dataFone)) + ((dst_negative_scale_reindex_dataFone) + (dst_negative_scale_reindex_dataFone)))) * S ((((dst_positive_code_reindex_dataFone) + (dst_positive_scale_reindex_dataFone)) * S ((dst_positive_code_reindex_dataFone) + (dst_positive_scale_reindex_dataFone)) + ((dst_positive_scale_reindex_dataFone) + (dst_positive_scale_reindex_dataFone))) + (((dst_negative_code_reindex_dataFone) + (dst_negative_scale_reindex_dataFone)) * S ((dst_negative_code_reindex_dataFone) + (dst_negative_scale_reindex_dataFone)) + ((dst_negative_scale_reindex_dataFone) + (dst_negative_scale_reindex_dataFone)))) + ((((dst_negative_code_reindex_dataFone) + (dst_negative_scale_reindex_dataFone)) * S ((dst_negative_code_reindex_dataFone) + (dst_negative_scale_reindex_dataFone)) + ((dst_negative_scale_reindex_dataFone) + (dst_negative_scale_reindex_dataFone))) + (((dst_negative_code_reindex_dataFone) + (dst_negative_scale_reindex_dataFone)) * S ((dst_negative_code_reindex_dataFone) + (dst_negative_scale_reindex_dataFone)) + ((dst_negative_scale_reindex_dataFone) + (dst_negative_scale_reindex_dataFone)))))) /\ (((((exists ff_h_pvs_reindex_dataFonepositive. ff_h_pvs_reindex_dataFonepositive + S (dst_positive_reindex_dataFone) = S ((S (1)) * dst_positive_scale_reindex_dataFone)) /\ exists ff_q_pvs_reindex_dataFonepositive. dst_positive_code_reindex_dataFone = ff_q_pvs_reindex_dataFonepositive * S ((S (1)) * dst_positive_scale_reindex_dataFone) + (dst_positive_reindex_dataFone))) /\ (((((exists ff_h_pvs_reindex_dataFonenegative. ff_h_pvs_reindex_dataFonenegative + S (dst_negative_reindex_dataFone) = S ((S (1)) * dst_negative_scale_reindex_dataFone)) /\ exists ff_q_pvs_reindex_dataFonenegative. dst_negative_code_reindex_dataFone = ff_q_pvs_reindex_dataFonenegative * S ((S (1)) * dst_negative_scale_reindex_dataFone) + (dst_negative_reindex_dataFone))) /\ (exists ge_balance_positive_reindex_dataFonevalue ge_balance_negative_reindex_dataFonevalue. (((((2) = 2 * (ge_balance_positive_reindex_dataFonevalue) /\ (ge_balance_negative_reindex_dataFonevalue) = 0) \/ exists ge_signed_half_reindex_dataFonevaluedecode. (((2) = 2 * ge_signed_half_reindex_dataFonevaluedecode + 1 /\ (ge_balance_positive_reindex_dataFonevalue) = 0) /\ (ge_balance_negative_reindex_dataFonevalue) = S ge_signed_half_reindex_dataFonevaluedecode))) /\ ((dst_positive_reindex_dataFone) + ge_balance_negative_reindex_dataFonevalue = (dst_negative_reindex_dataFone) + ge_balance_positive_reindex_dataFonevalue))))))))) /\ (forall mp_a_reindex_dataF mp_b_reindex_dataF mp_x_reindex_dataF mp_y_reindex_dataF mp_z_reindex_dataF. ~(mp_a_reindex_dataF=0) -> ~(mp_b_reindex_dataF=0) -> (exists pvs_le_gap_reindex_dataFbound. pvs_le_gap_reindex_dataFbound + (mp_a_reindex_dataF*mp_b_reindex_dataF) = (N)) -> (forall frp_divisor_reindex_dataFcoprime. (exists frp_left_factor_reindex_dataFcoprime. mp_a_reindex_dataF = frp_divisor_reindex_dataFcoprime * frp_left_factor_reindex_dataFcoprime) -> (exists frp_right_factor_reindex_dataFcoprime. mp_b_reindex_dataF = frp_divisor_reindex_dataFcoprime * frp_right_factor_reindex_dataFcoprime) -> frp_divisor_reindex_dataFcoprime = 1) -> (exists dst_positive_code_reindex_dataFfirst dst_positive_scale_reindex_dataFfirst dst_negative_code_reindex_dataFfirst dst_negative_scale_reindex_dataFfirst dst_positive_reindex_dataFfirst dst_negative_reindex_dataFfirst. (((F) = (((((dst_positive_code_reindex_dataFfirst) + (dst_positive_scale_reindex_dataFfirst)) * S ((dst_positive_code_reindex_dataFfirst) + (dst_positive_scale_reindex_dataFfirst)) + ((dst_positive_scale_reindex_dataFfirst) + (dst_positive_scale_reindex_dataFfirst))) + (((dst_negative_code_reindex_dataFfirst) + (dst_negative_scale_reindex_dataFfirst)) * S ((dst_negative_code_reindex_dataFfirst) + (dst_negative_scale_reindex_dataFfirst)) + ((dst_negative_scale_reindex_dataFfirst) + (dst_negative_scale_reindex_dataFfirst)))) * S ((((dst_positive_code_reindex_dataFfirst) + (dst_positive_scale_reindex_dataFfirst)) * S ((dst_positive_code_reindex_dataFfirst) + (dst_positive_scale_reindex_dataFfirst)) + ((dst_positive_scale_reindex_dataFfirst) + (dst_positive_scale_reindex_dataFfirst))) + (((dst_negative_code_reindex_dataFfirst) + (dst_negative_scale_reindex_dataFfirst)) * S ((dst_negative_code_reindex_dataFfirst) + (dst_negative_scale_reindex_dataFfirst)) + ((dst_negative_scale_reindex_dataFfirst) + (dst_negative_scale_reindex_dataFfirst)))) + ((((dst_negative_code_reindex_dataFfirst) + (dst_negative_scale_reindex_dataFfirst)) * S ((dst_negative_code_reindex_dataFfirst) + (dst_negative_scale_reindex_dataFfirst)) + ((dst_negative_scale_reindex_dataFfirst) + (dst_negative_scale_reindex_dataFfirst))) + (((dst_negative_code_reindex_dataFfirst) + (dst_negative_scale_reindex_dataFfirst)) * S ((dst_negative_code_reindex_dataFfirst) + (dst_negative_scale_reindex_dataFfirst)) + ((dst_negative_scale_reindex_dataFfirst) + (dst_negative_scale_reindex_dataFfirst)))))) /\ (((((exists ff_h_pvs_reindex_dataFfirstpositive. ff_h_pvs_reindex_dataFfirstpositive + S (dst_positive_reindex_dataFfirst) = S ((S (mp_a_reindex_dataF)) * dst_positive_scale_reindex_dataFfirst)) /\ exists ff_q_pvs_reindex_dataFfirstpositive. dst_positive_code_reindex_dataFfirst = ff_q_pvs_reindex_dataFfirstpositive * S ((S (mp_a_reindex_dataF)) * dst_positive_scale_reindex_dataFfirst) + (dst_positive_reindex_dataFfirst))) /\ (((((exists ff_h_pvs_reindex_dataFfirstnegative. ff_h_pvs_reindex_dataFfirstnegative + S (dst_negative_reindex_dataFfirst) = S ((S (mp_a_reindex_dataF)) * dst_negative_scale_reindex_dataFfirst)) /\ exists ff_q_pvs_reindex_dataFfirstnegative. dst_negative_code_reindex_dataFfirst = ff_q_pvs_reindex_dataFfirstnegative * S ((S (mp_a_reindex_dataF)) * dst_negative_scale_reindex_dataFfirst) + (dst_negative_reindex_dataFfirst))) /\ (exists ge_balance_positive_reindex_dataFfirstvalue ge_balance_negative_reindex_dataFfirstvalue. (((((mp_x_reindex_dataF) = 2 * (ge_balance_positive_reindex_dataFfirstvalue) /\ (ge_balance_negative_reindex_dataFfirstvalue) = 0) \/ exists ge_signed_half_reindex_dataFfirstvaluedecode. (((mp_x_reindex_dataF) = 2 * ge_signed_half_reindex_dataFfirstvaluedecode + 1 /\ (ge_balance_positive_reindex_dataFfirstvalue) = 0) /\ (ge_balance_negative_reindex_dataFfirstvalue) = S ge_signed_half_reindex_dataFfirstvaluedecode))) /\ ((dst_positive_reindex_dataFfirst) + ge_balance_negative_reindex_dataFfirstvalue = (dst_negative_reindex_dataFfirst) + ge_balance_positive_reindex_dataFfirstvalue))))))))) -> (exists dst_positive_code_reindex_dataFsecond dst_positive_scale_reindex_dataFsecond dst_negative_code_reindex_dataFsecond dst_negative_scale_reindex_dataFsecond dst_positive_reindex_dataFsecond dst_negative_reindex_dataFsecond. (((F) = (((((dst_positive_code_reindex_dataFsecond) + (dst_positive_scale_reindex_dataFsecond)) * S ((dst_positive_code_reindex_dataFsecond) + (dst_positive_scale_reindex_dataFsecond)) + ((dst_positive_scale_reindex_dataFsecond) + (dst_positive_scale_reindex_dataFsecond))) + (((dst_negative_code_reindex_dataFsecond) + (dst_negative_scale_reindex_dataFsecond)) * S ((dst_negative_code_reindex_dataFsecond) + (dst_negative_scale_reindex_dataFsecond)) + ((dst_negative_scale_reindex_dataFsecond) + (dst_negative_scale_reindex_dataFsecond)))) * S ((((dst_positive_code_reindex_dataFsecond) + (dst_positive_scale_reindex_dataFsecond)) * S ((dst_positive_code_reindex_dataFsecond) + (dst_positive_scale_reindex_dataFsecond)) + ((dst_positive_scale_reindex_dataFsecond) + (dst_positive_scale_reindex_dataFsecond))) + (((dst_negative_code_reindex_dataFsecond) + (dst_negative_scale_reindex_dataFsecond)) * S ((dst_negative_code_reindex_dataFsecond) + (dst_negative_scale_reindex_dataFsecond)) + ((dst_negative_scale_reindex_dataFsecond) + (dst_negative_scale_reindex_dataFsecond)))) + ((((dst_negative_code_reindex_dataFsecond) + (dst_negative_scale_reindex_dataFsecond)) * S ((dst_negative_code_reindex_dataFsecond) + (dst_negative_scale_reindex_dataFsecond)) + ((dst_negative_scale_reindex_dataFsecond) + (dst_negative_scale_reindex_dataFsecond))) + (((dst_negative_code_reindex_dataFsecond) + (dst_negative_scale_reindex_dataFsecond)) * S ((dst_negative_code_reindex_dataFsecond) + (dst_negative_scale_reindex_dataFsecond)) + ((dst_negative_scale_reindex_dataFsecond) + (dst_negative_scale_reindex_dataFsecond)))))) /\ (((((exists ff_h_pvs_reindex_dataFsecondpositive. ff_h_pvs_reindex_dataFsecondpositive + S (dst_positive_reindex_dataFsecond) = S ((S (mp_b_reindex_dataF)) * dst_positive_scale_reindex_dataFsecond)) /\ exists ff_q_pvs_reindex_dataFsecondpositive. dst_positive_code_reindex_dataFsecond = ff_q_pvs_reindex_dataFsecondpositive * S ((S (mp_b_reindex_dataF)) * dst_positive_scale_reindex_dataFsecond) + (dst_positive_reindex_dataFsecond))) /\ (((((exists ff_h_pvs_reindex_dataFsecondnegative. ff_h_pvs_reindex_dataFsecondnegative + S (dst_negative_reindex_dataFsecond) = S ((S (mp_b_reindex_dataF)) * dst_negative_scale_reindex_dataFsecond)) /\ exists ff_q_pvs_reindex_dataFsecondnegative. dst_negative_code_reindex_dataFsecond = ff_q_pvs_reindex_dataFsecondnegative * S ((S (mp_b_reindex_dataF)) * dst_negative_scale_reindex_dataFsecond) + (dst_negative_reindex_dataFsecond))) /\ (exists ge_balance_positive_reindex_dataFsecondvalue ge_balance_negative_reindex_dataFsecondvalue. (((((mp_y_reindex_dataF) = 2 * (ge_balance_positive_reindex_dataFsecondvalue) /\ (ge_balance_negative_reindex_dataFsecondvalue) = 0) \/ exists ge_signed_half_reindex_dataFsecondvaluedecode. (((mp_y_reindex_dataF) = 2 * ge_signed_half_reindex_dataFsecondvaluedecode + 1 /\ (ge_balance_positive_reindex_dataFsecondvalue) = 0) /\ (ge_balance_negative_reindex_dataFsecondvalue) = S ge_signed_half_reindex_dataFsecondvaluedecode))) /\ ((dst_positive_reindex_dataFsecond) + ge_balance_negative_reindex_dataFsecondvalue = (dst_negative_reindex_dataFsecond) + ge_balance_positive_reindex_dataFsecondvalue))))))))) -> (exists dst_positive_code_reindex_dataFproduct dst_positive_scale_reindex_dataFproduct dst_negative_code_reindex_dataFproduct dst_negative_scale_reindex_dataFproduct dst_positive_reindex_dataFproduct dst_negative_reindex_dataFproduct. (((F) = (((((dst_positive_code_reindex_dataFproduct) + (dst_positive_scale_reindex_dataFproduct)) * S ((dst_positive_code_reindex_dataFproduct) + (dst_positive_scale_reindex_dataFproduct)) + ((dst_positive_scale_reindex_dataFproduct) + (dst_positive_scale_reindex_dataFproduct))) + (((dst_negative_code_reindex_dataFproduct) + (dst_negative_scale_reindex_dataFproduct)) * S ((dst_negative_code_reindex_dataFproduct) + (dst_negative_scale_reindex_dataFproduct)) + ((dst_negative_scale_reindex_dataFproduct) + (dst_negative_scale_reindex_dataFproduct)))) * S ((((dst_positive_code_reindex_dataFproduct) + (dst_positive_scale_reindex_dataFproduct)) * S ((dst_positive_code_reindex_dataFproduct) + (dst_positive_scale_reindex_dataFproduct)) + ((dst_positive_scale_reindex_dataFproduct) + (dst_positive_scale_reindex_dataFproduct))) + (((dst_negative_code_reindex_dataFproduct) + (dst_negative_scale_reindex_dataFproduct)) * S ((dst_negative_code_reindex_dataFproduct) + (dst_negative_scale_reindex_dataFproduct)) + ((dst_negative_scale_reindex_dataFproduct) + (dst_negative_scale_reindex_dataFproduct)))) + ((((dst_negative_code_reindex_dataFproduct) + (dst_negative_scale_reindex_dataFproduct)) * S ((dst_negative_code_reindex_dataFproduct) + (dst_negative_scale_reindex_dataFproduct)) + ((dst_negative_scale_reindex_dataFproduct) + (dst_negative_scale_reindex_dataFproduct))) + (((dst_negative_code_reindex_dataFproduct) + (dst_negative_scale_reindex_dataFproduct)) * S ((dst_negative_code_reindex_dataFproduct) + (dst_negative_scale_reindex_dataFproduct)) + ((dst_negative_scale_reindex_dataFproduct) + (dst_negative_scale_reindex_dataFproduct)))))) /\ (((((exists ff_h_pvs_reindex_dataFproductpositive. ff_h_pvs_reindex_dataFproductpositive + S (dst_positive_reindex_dataFproduct) = S ((S (mp_a_reindex_dataF*mp_b_reindex_dataF)) * dst_positive_scale_reindex_dataFproduct)) /\ exists ff_q_pvs_reindex_dataFproductpositive. dst_positive_code_reindex_dataFproduct = ff_q_pvs_reindex_dataFproductpositive * S ((S (mp_a_reindex_dataF*mp_b_reindex_dataF)) * dst_positive_scale_reindex_dataFproduct) + (dst_positive_reindex_dataFproduct))) /\ (((((exists ff_h_pvs_reindex_dataFproductnegative. ff_h_pvs_reindex_dataFproductnegative + S (dst_negative_reindex_dataFproduct) = S ((S (mp_a_reindex_dataF*mp_b_reindex_dataF)) * dst_negative_scale_reindex_dataFproduct)) /\ exists ff_q_pvs_reindex_dataFproductnegative. dst_negative_code_reindex_dataFproduct = ff_q_pvs_reindex_dataFproductnegative * S ((S (mp_a_reindex_dataF*mp_b_reindex_dataF)) * dst_negative_scale_reindex_dataFproduct) + (dst_negative_reindex_dataFproduct))) /\ (exists ge_balance_positive_reindex_dataFproductvalue ge_balance_negative_reindex_dataFproductvalue. (((((mp_z_reindex_dataF) = 2 * (ge_balance_positive_reindex_dataFproductvalue) /\ (ge_balance_negative_reindex_dataFproductvalue) = 0) \/ exists ge_signed_half_reindex_dataFproductvaluedecode. (((mp_z_reindex_dataF) = 2 * ge_signed_half_reindex_dataFproductvaluedecode + 1 /\ (ge_balance_positive_reindex_dataFproductvalue) = 0) /\ (ge_balance_negative_reindex_dataFproductvalue) = S ge_signed_half_reindex_dataFproductvaluedecode))) /\ ((dst_positive_reindex_dataFproduct) + ge_balance_negative_reindex_dataFproductvalue = (dst_negative_reindex_dataFproduct) + ge_balance_positive_reindex_dataFproductvalue))))))))) -> (exists sto_ap_reindex_dataFlaw sto_an_reindex_dataFlaw sto_bp_reindex_dataFlaw sto_bn_reindex_dataFlaw sto_cp_reindex_dataFlaw sto_cn_reindex_dataFlaw. (((((mp_x_reindex_dataF) = 2 * (sto_ap_reindex_dataFlaw) /\ (sto_an_reindex_dataFlaw) = 0) \/ exists ge_signed_half_reindex_dataFlawleft. (((mp_x_reindex_dataF) = 2 * ge_signed_half_reindex_dataFlawleft + 1 /\ (sto_ap_reindex_dataFlaw) = 0) /\ (sto_an_reindex_dataFlaw) = S ge_signed_half_reindex_dataFlawleft))) /\ ((((((mp_y_reindex_dataF) = 2 * (sto_bp_reindex_dataFlaw) /\ (sto_bn_reindex_dataFlaw) = 0) \/ exists ge_signed_half_reindex_dataFlawright. (((mp_y_reindex_dataF) = 2 * ge_signed_half_reindex_dataFlawright + 1 /\ (sto_bp_reindex_dataFlaw) = 0) /\ (sto_bn_reindex_dataFlaw) = S ge_signed_half_reindex_dataFlawright))) /\ ((((((mp_z_reindex_dataF) = 2 * (sto_cp_reindex_dataFlaw) /\ (sto_cn_reindex_dataFlaw) = 0) \/ exists ge_signed_half_reindex_dataFlawoutput. (((mp_z_reindex_dataF) = 2 * ge_signed_half_reindex_dataFlawoutput + 1 /\ (sto_cp_reindex_dataFlaw) = 0) /\ (sto_cn_reindex_dataFlaw) = S ge_signed_half_reindex_dataFlawoutput))) /\ ((sto_ap_reindex_dataFlaw * sto_bp_reindex_dataFlaw + sto_an_reindex_dataFlaw * sto_bn_reindex_dataFlaw) + sto_cn_reindex_dataFlaw = (sto_ap_reindex_dataFlaw * sto_bn_reindex_dataFlaw + sto_an_reindex_dataFlaw * sto_bp_reindex_dataFlaw) + sto_cp_reindex_dataFlaw)))))))))))))) /\ (((((~((N)=0)) /\ (((exists dst_positive_code_reindex_dataGtable dst_positive_scale_reindex_dataGtable dst_negative_code_reindex_dataGtable dst_negative_scale_reindex_dataGtable. (((G) = (((((dst_positive_code_reindex_dataGtable) + (dst_positive_scale_reindex_dataGtable)) * S ((dst_positive_code_reindex_dataGtable) + (dst_positive_scale_reindex_dataGtable)) + ((dst_positive_scale_reindex_dataGtable) + (dst_positive_scale_reindex_dataGtable))) + (((dst_negative_code_reindex_dataGtable) + (dst_negative_scale_reindex_dataGtable)) * S ((dst_negative_code_reindex_dataGtable) + (dst_negative_scale_reindex_dataGtable)) + ((dst_negative_scale_reindex_dataGtable) + (dst_negative_scale_reindex_dataGtable)))) * S ((((dst_positive_code_reindex_dataGtable) + (dst_positive_scale_reindex_dataGtable)) * S ((dst_positive_code_reindex_dataGtable) + (dst_positive_scale_reindex_dataGtable)) + ((dst_positive_scale_reindex_dataGtable) + (dst_positive_scale_reindex_dataGtable))) + (((dst_negative_code_reindex_dataGtable) + (dst_negative_scale_reindex_dataGtable)) * S ((dst_negative_code_reindex_dataGtable) + (dst_negative_scale_reindex_dataGtable)) + ((dst_negative_scale_reindex_dataGtable) + (dst_negative_scale_reindex_dataGtable)))) + ((((dst_negative_code_reindex_dataGtable) + (dst_negative_scale_reindex_dataGtable)) * S ((dst_negative_code_reindex_dataGtable) + (dst_negative_scale_reindex_dataGtable)) + ((dst_negative_scale_reindex_dataGtable) + (dst_negative_scale_reindex_dataGtable))) + (((dst_negative_code_reindex_dataGtable) + (dst_negative_scale_reindex_dataGtable)) * S ((dst_negative_code_reindex_dataGtable) + (dst_negative_scale_reindex_dataGtable)) + ((dst_negative_scale_reindex_dataGtable) + (dst_negative_scale_reindex_dataGtable)))))) /\ (forall dst_index_reindex_dataGtable. (exists pvs_le_gap_reindex_dataGtabledomain. pvs_le_gap_reindex_dataGtabledomain + (dst_index_reindex_dataGtable) = (N)) -> exists dst_positive_reindex_dataGtable dst_negative_reindex_dataGtable dst_value_reindex_dataGtable. ((((exists ff_h_pvs_reindex_dataGtableentrypositive. ff_h_pvs_reindex_dataGtableentrypositive + S (dst_positive_reindex_dataGtable) = S ((S (dst_index_reindex_dataGtable)) * dst_positive_scale_reindex_dataGtable)) /\ exists ff_q_pvs_reindex_dataGtableentrypositive. dst_positive_code_reindex_dataGtable = ff_q_pvs_reindex_dataGtableentrypositive * S ((S (dst_index_reindex_dataGtable)) * dst_positive_scale_reindex_dataGtable) + (dst_positive_reindex_dataGtable))) /\ (((((exists ff_h_pvs_reindex_dataGtableentrynegative. ff_h_pvs_reindex_dataGtableentrynegative + S (dst_negative_reindex_dataGtable) = S ((S (dst_index_reindex_dataGtable)) * dst_negative_scale_reindex_dataGtable)) /\ exists ff_q_pvs_reindex_dataGtableentrynegative. dst_negative_code_reindex_dataGtable = ff_q_pvs_reindex_dataGtableentrynegative * S ((S (dst_index_reindex_dataGtable)) * dst_negative_scale_reindex_dataGtable) + (dst_negative_reindex_dataGtable))) /\ (exists ge_balance_positive_reindex_dataGtableentryvalue ge_balance_negative_reindex_dataGtableentryvalue. (((((dst_value_reindex_dataGtable) = 2 * (ge_balance_positive_reindex_dataGtableentryvalue) /\ (ge_balance_negative_reindex_dataGtableentryvalue) = 0) \/ exists ge_signed_half_reindex_dataGtableentryvaluedecode. (((dst_value_reindex_dataGtable) = 2 * ge_signed_half_reindex_dataGtableentryvaluedecode + 1 /\ (ge_balance_positive_reindex_dataGtableentryvalue) = 0) /\ (ge_balance_negative_reindex_dataGtableentryvalue) = S ge_signed_half_reindex_dataGtableentryvaluedecode))) /\ ((dst_positive_reindex_dataGtable) + ge_balance_negative_reindex_dataGtableentryvalue = (dst_negative_reindex_dataGtable) + ge_balance_positive_reindex_dataGtableentryvalue))))))))) /\ (((exists dst_positive_code_reindex_dataGone dst_positive_scale_reindex_dataGone dst_negative_code_reindex_dataGone dst_negative_scale_reindex_dataGone dst_positive_reindex_dataGone dst_negative_reindex_dataGone. (((G) = (((((dst_positive_code_reindex_dataGone) + (dst_positive_scale_reindex_dataGone)) * S ((dst_positive_code_reindex_dataGone) + (dst_positive_scale_reindex_dataGone)) + ((dst_positive_scale_reindex_dataGone) + (dst_positive_scale_reindex_dataGone))) + (((dst_negative_code_reindex_dataGone) + (dst_negative_scale_reindex_dataGone)) * S ((dst_negative_code_reindex_dataGone) + (dst_negative_scale_reindex_dataGone)) + ((dst_negative_scale_reindex_dataGone) + (dst_negative_scale_reindex_dataGone)))) * S ((((dst_positive_code_reindex_dataGone) + (dst_positive_scale_reindex_dataGone)) * S ((dst_positive_code_reindex_dataGone) + (dst_positive_scale_reindex_dataGone)) + ((dst_positive_scale_reindex_dataGone) + (dst_positive_scale_reindex_dataGone))) + (((dst_negative_code_reindex_dataGone) + (dst_negative_scale_reindex_dataGone)) * S ((dst_negative_code_reindex_dataGone) + (dst_negative_scale_reindex_dataGone)) + ((dst_negative_scale_reindex_dataGone) + (dst_negative_scale_reindex_dataGone)))) + ((((dst_negative_code_reindex_dataGone) + (dst_negative_scale_reindex_dataGone)) * S ((dst_negative_code_reindex_dataGone) + (dst_negative_scale_reindex_dataGone)) + ((dst_negative_scale_reindex_dataGone) + (dst_negative_scale_reindex_dataGone))) + (((dst_negative_code_reindex_dataGone) + (dst_negative_scale_reindex_dataGone)) * S ((dst_negative_code_reindex_dataGone) + (dst_negative_scale_reindex_dataGone)) + ((dst_negative_scale_reindex_dataGone) + (dst_negative_scale_reindex_dataGone)))))) /\ (((((exists ff_h_pvs_reindex_dataGonepositive. ff_h_pvs_reindex_dataGonepositive + S (dst_positive_reindex_dataGone) = S ((S (1)) * dst_positive_scale_reindex_dataGone)) /\ exists ff_q_pvs_reindex_dataGonepositive. dst_positive_code_reindex_dataGone = ff_q_pvs_reindex_dataGonepositive * S ((S (1)) * dst_positive_scale_reindex_dataGone) + (dst_positive_reindex_dataGone))) /\ (((((exists ff_h_pvs_reindex_dataGonenegative. ff_h_pvs_reindex_dataGonenegative + S (dst_negative_reindex_dataGone) = S ((S (1)) * dst_negative_scale_reindex_dataGone)) /\ exists ff_q_pvs_reindex_dataGonenegative. dst_negative_code_reindex_dataGone = ff_q_pvs_reindex_dataGonenegative * S ((S (1)) * dst_negative_scale_reindex_dataGone) + (dst_negative_reindex_dataGone))) /\ (exists ge_balance_positive_reindex_dataGonevalue ge_balance_negative_reindex_dataGonevalue. (((((2) = 2 * (ge_balance_positive_reindex_dataGonevalue) /\ (ge_balance_negative_reindex_dataGonevalue) = 0) \/ exists ge_signed_half_reindex_dataGonevaluedecode. (((2) = 2 * ge_signed_half_reindex_dataGonevaluedecode + 1 /\ (ge_balance_positive_reindex_dataGonevalue) = 0) /\ (ge_balance_negative_reindex_dataGonevalue) = S ge_signed_half_reindex_dataGonevaluedecode))) /\ ((dst_positive_reindex_dataGone) + ge_balance_negative_reindex_dataGonevalue = (dst_negative_reindex_dataGone) + ge_balance_positive_reindex_dataGonevalue))))))))) /\ (forall mp_a_reindex_dataG mp_b_reindex_dataG mp_x_reindex_dataG mp_y_reindex_dataG mp_z_reindex_dataG. ~(mp_a_reindex_dataG=0) -> ~(mp_b_reindex_dataG=0) -> (exists pvs_le_gap_reindex_dataGbound. pvs_le_gap_reindex_dataGbound + (mp_a_reindex_dataG*mp_b_reindex_dataG) = (N)) -> (forall frp_divisor_reindex_dataGcoprime. (exists frp_left_factor_reindex_dataGcoprime. mp_a_reindex_dataG = frp_divisor_reindex_dataGcoprime * frp_left_factor_reindex_dataGcoprime) -> (exists frp_right_factor_reindex_dataGcoprime. mp_b_reindex_dataG = frp_divisor_reindex_dataGcoprime * frp_right_factor_reindex_dataGcoprime) -> frp_divisor_reindex_dataGcoprime = 1) -> (exists dst_positive_code_reindex_dataGfirst dst_positive_scale_reindex_dataGfirst dst_negative_code_reindex_dataGfirst dst_negative_scale_reindex_dataGfirst dst_positive_reindex_dataGfirst dst_negative_reindex_dataGfirst. (((G) = (((((dst_positive_code_reindex_dataGfirst) + (dst_positive_scale_reindex_dataGfirst)) * S ((dst_positive_code_reindex_dataGfirst) + (dst_positive_scale_reindex_dataGfirst)) + ((dst_positive_scale_reindex_dataGfirst) + (dst_positive_scale_reindex_dataGfirst))) + (((dst_negative_code_reindex_dataGfirst) + (dst_negative_scale_reindex_dataGfirst)) * S ((dst_negative_code_reindex_dataGfirst) + (dst_negative_scale_reindex_dataGfirst)) + ((dst_negative_scale_reindex_dataGfirst) + (dst_negative_scale_reindex_dataGfirst)))) * S ((((dst_positive_code_reindex_dataGfirst) + (dst_positive_scale_reindex_dataGfirst)) * S ((dst_positive_code_reindex_dataGfirst) + (dst_positive_scale_reindex_dataGfirst)) + ((dst_positive_scale_reindex_dataGfirst) + (dst_positive_scale_reindex_dataGfirst))) + (((dst_negative_code_reindex_dataGfirst) + (dst_negative_scale_reindex_dataGfirst)) * S ((dst_negative_code_reindex_dataGfirst) + (dst_negative_scale_reindex_dataGfirst)) + ((dst_negative_scale_reindex_dataGfirst) + (dst_negative_scale_reindex_dataGfirst)))) + ((((dst_negative_code_reindex_dataGfirst) + (dst_negative_scale_reindex_dataGfirst)) * S ((dst_negative_code_reindex_dataGfirst) + (dst_negative_scale_reindex_dataGfirst)) + ((dst_negative_scale_reindex_dataGfirst) + (dst_negative_scale_reindex_dataGfirst))) + (((dst_negative_code_reindex_dataGfirst) + (dst_negative_scale_reindex_dataGfirst)) * S ((dst_negative_code_reindex_dataGfirst) + (dst_negative_scale_reindex_dataGfirst)) + ((dst_negative_scale_reindex_dataGfirst) + (dst_negative_scale_reindex_dataGfirst)))))) /\ (((((exists ff_h_pvs_reindex_dataGfirstpositive. ff_h_pvs_reindex_dataGfirstpositive + S (dst_positive_reindex_dataGfirst) = S ((S (mp_a_reindex_dataG)) * dst_positive_scale_reindex_dataGfirst)) /\ exists ff_q_pvs_reindex_dataGfirstpositive. dst_positive_code_reindex_dataGfirst = ff_q_pvs_reindex_dataGfirstpositive * S ((S (mp_a_reindex_dataG)) * dst_positive_scale_reindex_dataGfirst) + (dst_positive_reindex_dataGfirst))) /\ (((((exists ff_h_pvs_reindex_dataGfirstnegative. ff_h_pvs_reindex_dataGfirstnegative + S (dst_negative_reindex_dataGfirst) = S ((S (mp_a_reindex_dataG)) * dst_negative_scale_reindex_dataGfirst)) /\ exists ff_q_pvs_reindex_dataGfirstnegative. dst_negative_code_reindex_dataGfirst = ff_q_pvs_reindex_dataGfirstnegative * S ((S (mp_a_reindex_dataG)) * dst_negative_scale_reindex_dataGfirst) + (dst_negative_reindex_dataGfirst))) /\ (exists ge_balance_positive_reindex_dataGfirstvalue ge_balance_negative_reindex_dataGfirstvalue. (((((mp_x_reindex_dataG) = 2 * (ge_balance_positive_reindex_dataGfirstvalue) /\ (ge_balance_negative_reindex_dataGfirstvalue) = 0) \/ exists ge_signed_half_reindex_dataGfirstvaluedecode. (((mp_x_reindex_dataG) = 2 * ge_signed_half_reindex_dataGfirstvaluedecode + 1 /\ (ge_balance_positive_reindex_dataGfirstvalue) = 0) /\ (ge_balance_negative_reindex_dataGfirstvalue) = S ge_signed_half_reindex_dataGfirstvaluedecode))) /\ ((dst_positive_reindex_dataGfirst) + ge_balance_negative_reindex_dataGfirstvalue = (dst_negative_reindex_dataGfirst) + ge_balance_positive_reindex_dataGfirstvalue))))))))) -> (exists dst_positive_code_reindex_dataGsecond dst_positive_scale_reindex_dataGsecond dst_negative_code_reindex_dataGsecond dst_negative_scale_reindex_dataGsecond dst_positive_reindex_dataGsecond dst_negative_reindex_dataGsecond. (((G) = (((((dst_positive_code_reindex_dataGsecond) + (dst_positive_scale_reindex_dataGsecond)) * S ((dst_positive_code_reindex_dataGsecond) + (dst_positive_scale_reindex_dataGsecond)) + ((dst_positive_scale_reindex_dataGsecond) + (dst_positive_scale_reindex_dataGsecond))) + (((dst_negative_code_reindex_dataGsecond) + (dst_negative_scale_reindex_dataGsecond)) * S ((dst_negative_code_reindex_dataGsecond) + (dst_negative_scale_reindex_dataGsecond)) + ((dst_negative_scale_reindex_dataGsecond) + (dst_negative_scale_reindex_dataGsecond)))) * S ((((dst_positive_code_reindex_dataGsecond) + (dst_positive_scale_reindex_dataGsecond)) * S ((dst_positive_code_reindex_dataGsecond) + (dst_positive_scale_reindex_dataGsecond)) + ((dst_positive_scale_reindex_dataGsecond) + (dst_positive_scale_reindex_dataGsecond))) + (((dst_negative_code_reindex_dataGsecond) + (dst_negative_scale_reindex_dataGsecond)) * S ((dst_negative_code_reindex_dataGsecond) + (dst_negative_scale_reindex_dataGsecond)) + ((dst_negative_scale_reindex_dataGsecond) + (dst_negative_scale_reindex_dataGsecond)))) + ((((dst_negative_code_reindex_dataGsecond) + (dst_negative_scale_reindex_dataGsecond)) * S ((dst_negative_code_reindex_dataGsecond) + (dst_negative_scale_reindex_dataGsecond)) + ((dst_negative_scale_reindex_dataGsecond) + (dst_negative_scale_reindex_dataGsecond))) + (((dst_negative_code_reindex_dataGsecond) + (dst_negative_scale_reindex_dataGsecond)) * S ((dst_negative_code_reindex_dataGsecond) + (dst_negative_scale_reindex_dataGsecond)) + ((dst_negative_scale_reindex_dataGsecond) + (dst_negative_scale_reindex_dataGsecond)))))) /\ (((((exists ff_h_pvs_reindex_dataGsecondpositive. ff_h_pvs_reindex_dataGsecondpositive + S (dst_positive_reindex_dataGsecond) = S ((S (mp_b_reindex_dataG)) * dst_positive_scale_reindex_dataGsecond)) /\ exists ff_q_pvs_reindex_dataGsecondpositive. dst_positive_code_reindex_dataGsecond = ff_q_pvs_reindex_dataGsecondpositive * S ((S (mp_b_reindex_dataG)) * dst_positive_scale_reindex_dataGsecond) + (dst_positive_reindex_dataGsecond))) /\ (((((exists ff_h_pvs_reindex_dataGsecondnegative. ff_h_pvs_reindex_dataGsecondnegative + S (dst_negative_reindex_dataGsecond) = S ((S (mp_b_reindex_dataG)) * dst_negative_scale_reindex_dataGsecond)) /\ exists ff_q_pvs_reindex_dataGsecondnegative. dst_negative_code_reindex_dataGsecond = ff_q_pvs_reindex_dataGsecondnegative * S ((S (mp_b_reindex_dataG)) * dst_negative_scale_reindex_dataGsecond) + (dst_negative_reindex_dataGsecond))) /\ (exists ge_balance_positive_reindex_dataGsecondvalue ge_balance_negative_reindex_dataGsecondvalue. (((((mp_y_reindex_dataG) = 2 * (ge_balance_positive_reindex_dataGsecondvalue) /\ (ge_balance_negative_reindex_dataGsecondvalue) = 0) \/ exists ge_signed_half_reindex_dataGsecondvaluedecode. (((mp_y_reindex_dataG) = 2 * ge_signed_half_reindex_dataGsecondvaluedecode + 1 /\ (ge_balance_positive_reindex_dataGsecondvalue) = 0) /\ (ge_balance_negative_reindex_dataGsecondvalue) = S ge_signed_half_reindex_dataGsecondvaluedecode))) /\ ((dst_positive_reindex_dataGsecond) + ge_balance_negative_reindex_dataGsecondvalue = (dst_negative_reindex_dataGsecond) + ge_balance_positive_reindex_dataGsecondvalue))))))))) -> (exists dst_positive_code_reindex_dataGproduct dst_positive_scale_reindex_dataGproduct dst_negative_code_reindex_dataGproduct dst_negative_scale_reindex_dataGproduct dst_positive_reindex_dataGproduct dst_negative_reindex_dataGproduct. (((G) = (((((dst_positive_code_reindex_dataGproduct) + (dst_positive_scale_reindex_dataGproduct)) * S ((dst_positive_code_reindex_dataGproduct) + (dst_positive_scale_reindex_dataGproduct)) + ((dst_positive_scale_reindex_dataGproduct) + (dst_positive_scale_reindex_dataGproduct))) + (((dst_negative_code_reindex_dataGproduct) + (dst_negative_scale_reindex_dataGproduct)) * S ((dst_negative_code_reindex_dataGproduct) + (dst_negative_scale_reindex_dataGproduct)) + ((dst_negative_scale_reindex_dataGproduct) + (dst_negative_scale_reindex_dataGproduct)))) * S ((((dst_positive_code_reindex_dataGproduct) + (dst_positive_scale_reindex_dataGproduct)) * S ((dst_positive_code_reindex_dataGproduct) + (dst_positive_scale_reindex_dataGproduct)) + ((dst_positive_scale_reindex_dataGproduct) + (dst_positive_scale_reindex_dataGproduct))) + (((dst_negative_code_reindex_dataGproduct) + (dst_negative_scale_reindex_dataGproduct)) * S ((dst_negative_code_reindex_dataGproduct) + (dst_negative_scale_reindex_dataGproduct)) + ((dst_negative_scale_reindex_dataGproduct) + (dst_negative_scale_reindex_dataGproduct)))) + ((((dst_negative_code_reindex_dataGproduct) + (dst_negative_scale_reindex_dataGproduct)) * S ((dst_negative_code_reindex_dataGproduct) + (dst_negative_scale_reindex_dataGproduct)) + ((dst_negative_scale_reindex_dataGproduct) + (dst_negative_scale_reindex_dataGproduct))) + (((dst_negative_code_reindex_dataGproduct) + (dst_negative_scale_reindex_dataGproduct)) * S ((dst_negative_code_reindex_dataGproduct) + (dst_negative_scale_reindex_dataGproduct)) + ((dst_negative_scale_reindex_dataGproduct) + (dst_negative_scale_reindex_dataGproduct)))))) /\ (((((exists ff_h_pvs_reindex_dataGproductpositive. ff_h_pvs_reindex_dataGproductpositive + S (dst_positive_reindex_dataGproduct) = S ((S (mp_a_reindex_dataG*mp_b_reindex_dataG)) * dst_positive_scale_reindex_dataGproduct)) /\ exists ff_q_pvs_reindex_dataGproductpositive. dst_positive_code_reindex_dataGproduct = ff_q_pvs_reindex_dataGproductpositive * S ((S (mp_a_reindex_dataG*mp_b_reindex_dataG)) * dst_positive_scale_reindex_dataGproduct) + (dst_positive_reindex_dataGproduct))) /\ (((((exists ff_h_pvs_reindex_dataGproductnegative. ff_h_pvs_reindex_dataGproductnegative + S (dst_negative_reindex_dataGproduct) = S ((S (mp_a_reindex_dataG*mp_b_reindex_dataG)) * dst_negative_scale_reindex_dataGproduct)) /\ exists ff_q_pvs_reindex_dataGproductnegative. dst_negative_code_reindex_dataGproduct = ff_q_pvs_reindex_dataGproductnegative * S ((S (mp_a_reindex_dataG*mp_b_reindex_dataG)) * dst_negative_scale_reindex_dataGproduct) + (dst_negative_reindex_dataGproduct))) /\ (exists ge_balance_positive_reindex_dataGproductvalue ge_balance_negative_reindex_dataGproductvalue. (((((mp_z_reindex_dataG) = 2 * (ge_balance_positive_reindex_dataGproductvalue) /\ (ge_balance_negative_reindex_dataGproductvalue) = 0) \/ exists ge_signed_half_reindex_dataGproductvaluedecode. (((mp_z_reindex_dataG) = 2 * ge_signed_half_reindex_dataGproductvaluedecode + 1 /\ (ge_balance_positive_reindex_dataGproductvalue) = 0) /\ (ge_balance_negative_reindex_dataGproductvalue) = S ge_signed_half_reindex_dataGproductvaluedecode))) /\ ((dst_positive_reindex_dataGproduct) + ge_balance_negative_reindex_dataGproductvalue = (dst_negative_reindex_dataGproduct) + ge_balance_positive_reindex_dataGproductvalue))))))))) -> (exists sto_ap_reindex_dataGlaw sto_an_reindex_dataGlaw sto_bp_reindex_dataGlaw sto_bn_reindex_dataGlaw sto_cp_reindex_dataGlaw sto_cn_reindex_dataGlaw. (((((mp_x_reindex_dataG) = 2 * (sto_ap_reindex_dataGlaw) /\ (sto_an_reindex_dataGlaw) = 0) \/ exists ge_signed_half_reindex_dataGlawleft. (((mp_x_reindex_dataG) = 2 * ge_signed_half_reindex_dataGlawleft + 1 /\ (sto_ap_reindex_dataGlaw) = 0) /\ (sto_an_reindex_dataGlaw) = S ge_signed_half_reindex_dataGlawleft))) /\ ((((((mp_y_reindex_dataG) = 2 * (sto_bp_reindex_dataGlaw) /\ (sto_bn_reindex_dataGlaw) = 0) \/ exists ge_signed_half_reindex_dataGlawright. (((mp_y_reindex_dataG) = 2 * ge_signed_half_reindex_dataGlawright + 1 /\ (sto_bp_reindex_dataGlaw) = 0) /\ (sto_bn_reindex_dataGlaw) = S ge_signed_half_reindex_dataGlawright))) /\ ((((((mp_z_reindex_dataG) = 2 * (sto_cp_reindex_dataGlaw) /\ (sto_cn_reindex_dataGlaw) = 0) \/ exists ge_signed_half_reindex_dataGlawoutput. (((mp_z_reindex_dataG) = 2 * ge_signed_half_reindex_dataGlawoutput + 1 /\ (sto_cp_reindex_dataGlaw) = 0) /\ (sto_cn_reindex_dataGlaw) = S ge_signed_half_reindex_dataGlawoutput))) /\ ((sto_ap_reindex_dataGlaw * sto_bp_reindex_dataGlaw + sto_an_reindex_dataGlaw * sto_bn_reindex_dataGlaw) + sto_cn_reindex_dataGlaw = (sto_ap_reindex_dataGlaw * sto_bn_reindex_dataGlaw + sto_an_reindex_dataGlaw * sto_bp_reindex_dataGlaw) + sto_cp_reindex_dataGlaw)))))))))))))) /\ (((~((m)=0)) /\ (((~((n)=0)) /\ (((exists pvs_le_gap_reindex_databound. pvs_le_gap_reindex_databound + ((m)*(n)) = (N)) /\ (((forall sfd_common_divisor_reindex_datacoprime. (exists pvs_factor_reindex_datacoprimeleft. (m) = (sfd_common_divisor_reindex_datacoprime) * pvs_factor_reindex_datacoprimeleft) -> (exists pvs_factor_reindex_datacoprimeright. (n) = (sfd_common_divisor_reindex_datacoprime) * pvs_factor_reindex_datacoprimeright) -> sfd_common_divisor_reindex_datacoprime = 1) /\ (((((exists dst_positive_code_reindex_datalefttable dst_positive_scale_reindex_datalefttable dst_negative_code_reindex_datalefttable dst_negative_scale_reindex_datalefttable. (((A) = (((((dst_positive_code_reindex_datalefttable) + (dst_positive_scale_reindex_datalefttable)) * S ((dst_positive_code_reindex_datalefttable) + (dst_positive_scale_reindex_datalefttable)) + ((dst_positive_scale_reindex_datalefttable) + (dst_positive_scale_reindex_datalefttable))) + (((dst_negative_code_reindex_datalefttable) + (dst_negative_scale_reindex_datalefttable)) * S ((dst_negative_code_reindex_datalefttable) + (dst_negative_scale_reindex_datalefttable)) + ((dst_negative_scale_reindex_datalefttable) + (dst_negative_scale_reindex_datalefttable)))) * S ((((dst_positive_code_reindex_datalefttable) + (dst_positive_scale_reindex_datalefttable)) * S ((dst_positive_code_reindex_datalefttable) + (dst_positive_scale_reindex_datalefttable)) + ((dst_positive_scale_reindex_datalefttable) + (dst_positive_scale_reindex_datalefttable))) + (((dst_negative_code_reindex_datalefttable) + (dst_negative_scale_reindex_datalefttable)) * S ((dst_negative_code_reindex_datalefttable) + (dst_negative_scale_reindex_datalefttable)) + ((dst_negative_scale_reindex_datalefttable) + (dst_negative_scale_reindex_datalefttable)))) + ((((dst_negative_code_reindex_datalefttable) + (dst_negative_scale_reindex_datalefttable)) * S ((dst_negative_code_reindex_datalefttable) + (dst_negative_scale_reindex_datalefttable)) + ((dst_negative_scale_reindex_datalefttable) + (dst_negative_scale_reindex_datalefttable))) + (((dst_negative_code_reindex_datalefttable) + (dst_negative_scale_reindex_datalefttable)) * S ((dst_negative_code_reindex_datalefttable) + (dst_negative_scale_reindex_datalefttable)) + ((dst_negative_scale_reindex_datalefttable) + (dst_negative_scale_reindex_datalefttable)))))) /\ (forall dst_index_reindex_datalefttable. (exists pvs_le_gap_reindex_datalefttabledomain. pvs_le_gap_reindex_datalefttabledomain + (dst_index_reindex_datalefttable) = (m)) -> exists dst_positive_reindex_datalefttable dst_negative_reindex_datalefttable dst_value_reindex_datalefttable. ((((exists ff_h_pvs_reindex_datalefttableentrypositive. ff_h_pvs_reindex_datalefttableentrypositive + S (dst_positive_reindex_datalefttable) = S ((S (dst_index_reindex_datalefttable)) * dst_positive_scale_reindex_datalefttable)) /\ exists ff_q_pvs_reindex_datalefttableentrypositive. dst_positive_code_reindex_datalefttable = ff_q_pvs_reindex_datalefttableentrypositive * S ((S (dst_index_reindex_datalefttable)) * dst_positive_scale_reindex_datalefttable) + (dst_positive_reindex_datalefttable))) /\ (((((exists ff_h_pvs_reindex_datalefttableentrynegative. ff_h_pvs_reindex_datalefttableentrynegative + S (dst_negative_reindex_datalefttable) = S ((S (dst_index_reindex_datalefttable)) * dst_negative_scale_reindex_datalefttable)) /\ exists ff_q_pvs_reindex_datalefttableentrynegative. dst_negative_code_reindex_datalefttable = ff_q_pvs_reindex_datalefttableentrynegative * S ((S (dst_index_reindex_datalefttable)) * dst_negative_scale_reindex_datalefttable) + (dst_negative_reindex_datalefttable))) /\ (exists ge_balance_positive_reindex_datalefttableentryvalue ge_balance_negative_reindex_datalefttableentryvalue. (((((dst_value_reindex_datalefttable) = 2 * (ge_balance_positive_reindex_datalefttableentryvalue) /\ (ge_balance_negative_reindex_datalefttableentryvalue) = 0) \/ exists ge_signed_half_reindex_datalefttableentryvaluedecode. (((dst_value_reindex_datalefttable) = 2 * ge_signed_half_reindex_datalefttableentryvaluedecode + 1 /\ (ge_balance_positive_reindex_datalefttableentryvalue) = 0) /\ (ge_balance_negative_reindex_datalefttableentryvalue) = S ge_signed_half_reindex_datalefttableentryvaluedecode))) /\ ((dst_positive_reindex_datalefttable) + ge_balance_negative_reindex_datalefttableentryvalue = (dst_negative_reindex_datalefttable) + ge_balance_positive_reindex_datalefttableentryvalue))))))))) /\ (forall dc_index_reindex_dataleft dc_value_reindex_dataleft. (exists pvs_le_gap_reindex_dataleftdomain. pvs_le_gap_reindex_dataleftdomain + (dc_index_reindex_dataleft) = (m)) -> (exists dst_positive_code_reindex_dataleftlookup dst_positive_scale_reindex_dataleftlookup dst_negative_code_reindex_dataleftlookup dst_negative_scale_reindex_dataleftlookup dst_positive_reindex_dataleftlookup dst_negative_reindex_dataleftlookup. (((A) = (((((dst_positive_code_reindex_dataleftlookup) + (dst_positive_scale_reindex_dataleftlookup)) * S ((dst_positive_code_reindex_dataleftlookup) + (dst_positive_scale_reindex_dataleftlookup)) + ((dst_positive_scale_reindex_dataleftlookup) + (dst_positive_scale_reindex_dataleftlookup))) + (((dst_negative_code_reindex_dataleftlookup) + (dst_negative_scale_reindex_dataleftlookup)) * S ((dst_negative_code_reindex_dataleftlookup) + (dst_negative_scale_reindex_dataleftlookup)) + ((dst_negative_scale_reindex_dataleftlookup) + (dst_negative_scale_reindex_dataleftlookup)))) * S ((((dst_positive_code_reindex_dataleftlookup) + (dst_positive_scale_reindex_dataleftlookup)) * S ((dst_positive_code_reindex_dataleftlookup) + (dst_positive_scale_reindex_dataleftlookup)) + ((dst_positive_scale_reindex_dataleftlookup) + (dst_positive_scale_reindex_dataleftlookup))) + (((dst_negative_code_reindex_dataleftlookup) + (dst_negative_scale_reindex_dataleftlookup)) * S ((dst_negative_code_reindex_dataleftlookup) + (dst_negative_scale_reindex_dataleftlookup)) + ((dst_negative_scale_reindex_dataleftlookup) + (dst_negative_scale_reindex_dataleftlookup)))) + ((((dst_negative_code_reindex_dataleftlookup) + (dst_negative_scale_reindex_dataleftlookup)) * S ((dst_negative_code_reindex_dataleftlookup) + (dst_negative_scale_reindex_dataleftlookup)) + ((dst_negative_scale_reindex_dataleftlookup) + (dst_negative_scale_reindex_dataleftlookup))) + (((dst_negative_code_reindex_dataleftlookup) + (dst_negative_scale_reindex_dataleftlookup)) * S ((dst_negative_code_reindex_dataleftlookup) + (dst_negative_scale_reindex_dataleftlookup)) + ((dst_negative_scale_reindex_dataleftlookup) + (dst_negative_scale_reindex_dataleftlookup)))))) /\ (((((exists ff_h_pvs_reindex_dataleftlookuppositive. ff_h_pvs_reindex_dataleftlookuppositive + S (dst_positive_reindex_dataleftlookup) = S ((S (dc_index_reindex_dataleft)) * dst_positive_scale_reindex_dataleftlookup)) /\ exists ff_q_pvs_reindex_dataleftlookuppositive. dst_positive_code_reindex_dataleftlookup = ff_q_pvs_reindex_dataleftlookuppositive * S ((S (dc_index_reindex_dataleft)) * dst_positive_scale_reindex_dataleftlookup) + (dst_positive_reindex_dataleftlookup))) /\ (((((exists ff_h_pvs_reindex_dataleftlookupnegative. ff_h_pvs_reindex_dataleftlookupnegative + S (dst_negative_reindex_dataleftlookup) = S ((S (dc_index_reindex_dataleft)) * dst_negative_scale_reindex_dataleftlookup)) /\ exists ff_q_pvs_reindex_dataleftlookupnegative. dst_negative_code_reindex_dataleftlookup = ff_q_pvs_reindex_dataleftlookupnegative * S ((S (dc_index_reindex_dataleft)) * dst_negative_scale_reindex_dataleftlookup) + (dst_negative_reindex_dataleftlookup))) /\ (exists ge_balance_positive_reindex_dataleftlookupvalue ge_balance_negative_reindex_dataleftlookupvalue. (((((dc_value_reindex_dataleft) = 2 * (ge_balance_positive_reindex_dataleftlookupvalue) /\ (ge_balance_negative_reindex_dataleftlookupvalue) = 0) \/ exists ge_signed_half_reindex_dataleftlookupvaluedecode. (((dc_value_reindex_dataleft) = 2 * ge_signed_half_reindex_dataleftlookupvaluedecode + 1 /\ (ge_balance_positive_reindex_dataleftlookupvalue) = 0) /\ (ge_balance_negative_reindex_dataleftlookupvalue) = S ge_signed_half_reindex_dataleftlookupvaluedecode))) /\ ((dst_positive_reindex_dataleftlookup) + ge_balance_negative_reindex_dataleftlookupvalue = (dst_negative_reindex_dataleftlookup) + ge_balance_positive_reindex_dataleftlookupvalue))))))))) -> ((((~((dc_index_reindex_dataleft)=0)) /\ (exists dc_quotient_reindex_dataleftentry dc_left_reindex_dataleftentry dc_right_reindex_dataleftentry. (((m)=(dc_index_reindex_dataleft)*dc_quotient_reindex_dataleftentry) /\ (((exists dst_positive_code_reindex_dataleftentryleft dst_positive_scale_reindex_dataleftentryleft dst_negative_code_reindex_dataleftentryleft dst_negative_scale_reindex_dataleftentryleft dst_positive_reindex_dataleftentryleft dst_negative_reindex_dataleftentryleft. (((F) = (((((dst_positive_code_reindex_dataleftentryleft) + (dst_positive_scale_reindex_dataleftentryleft)) * S ((dst_positive_code_reindex_dataleftentryleft) + (dst_positive_scale_reindex_dataleftentryleft)) + ((dst_positive_scale_reindex_dataleftentryleft) + (dst_positive_scale_reindex_dataleftentryleft))) + (((dst_negative_code_reindex_dataleftentryleft) + (dst_negative_scale_reindex_dataleftentryleft)) * S ((dst_negative_code_reindex_dataleftentryleft) + (dst_negative_scale_reindex_dataleftentryleft)) + ((dst_negative_scale_reindex_dataleftentryleft) + (dst_negative_scale_reindex_dataleftentryleft)))) * S ((((dst_positive_code_reindex_dataleftentryleft) + (dst_positive_scale_reindex_dataleftentryleft)) * S ((dst_positive_code_reindex_dataleftentryleft) + (dst_positive_scale_reindex_dataleftentryleft)) + ((dst_positive_scale_reindex_dataleftentryleft) + (dst_positive_scale_reindex_dataleftentryleft))) + (((dst_negative_code_reindex_dataleftentryleft) + (dst_negative_scale_reindex_dataleftentryleft)) * S ((dst_negative_code_reindex_dataleftentryleft) + (dst_negative_scale_reindex_dataleftentryleft)) + ((dst_negative_scale_reindex_dataleftentryleft) + (dst_negative_scale_reindex_dataleftentryleft)))) + ((((dst_negative_code_reindex_dataleftentryleft) + (dst_negative_scale_reindex_dataleftentryleft)) * S ((dst_negative_code_reindex_dataleftentryleft) + (dst_negative_scale_reindex_dataleftentryleft)) + ((dst_negative_scale_reindex_dataleftentryleft) + (dst_negative_scale_reindex_dataleftentryleft))) + (((dst_negative_code_reindex_dataleftentryleft) + (dst_negative_scale_reindex_dataleftentryleft)) * S ((dst_negative_code_reindex_dataleftentryleft) + (dst_negative_scale_reindex_dataleftentryleft)) + ((dst_negative_scale_reindex_dataleftentryleft) + (dst_negative_scale_reindex_dataleftentryleft)))))) /\ (((((exists ff_h_pvs_reindex_dataleftentryleftpositive. ff_h_pvs_reindex_dataleftentryleftpositive + S (dst_positive_reindex_dataleftentryleft) = S ((S (dc_index_reindex_dataleft)) * dst_positive_scale_reindex_dataleftentryleft)) /\ exists ff_q_pvs_reindex_dataleftentryleftpositive. dst_positive_code_reindex_dataleftentryleft = ff_q_pvs_reindex_dataleftentryleftpositive * S ((S (dc_index_reindex_dataleft)) * dst_positive_scale_reindex_dataleftentryleft) + (dst_positive_reindex_dataleftentryleft))) /\ (((((exists ff_h_pvs_reindex_dataleftentryleftnegative. ff_h_pvs_reindex_dataleftentryleftnegative + S (dst_negative_reindex_dataleftentryleft) = S ((S (dc_index_reindex_dataleft)) * dst_negative_scale_reindex_dataleftentryleft)) /\ exists ff_q_pvs_reindex_dataleftentryleftnegative. dst_negative_code_reindex_dataleftentryleft = ff_q_pvs_reindex_dataleftentryleftnegative * S ((S (dc_index_reindex_dataleft)) * dst_negative_scale_reindex_dataleftentryleft) + (dst_negative_reindex_dataleftentryleft))) /\ (exists ge_balance_positive_reindex_dataleftentryleftvalue ge_balance_negative_reindex_dataleftentryleftvalue. (((((dc_left_reindex_dataleftentry) = 2 * (ge_balance_positive_reindex_dataleftentryleftvalue) /\ (ge_balance_negative_reindex_dataleftentryleftvalue) = 0) \/ exists ge_signed_half_reindex_dataleftentryleftvaluedecode. (((dc_left_reindex_dataleftentry) = 2 * ge_signed_half_reindex_dataleftentryleftvaluedecode + 1 /\ (ge_balance_positive_reindex_dataleftentryleftvalue) = 0) /\ (ge_balance_negative_reindex_dataleftentryleftvalue) = S ge_signed_half_reindex_dataleftentryleftvaluedecode))) /\ ((dst_positive_reindex_dataleftentryleft) + ge_balance_negative_reindex_dataleftentryleftvalue = (dst_negative_reindex_dataleftentryleft) + ge_balance_positive_reindex_dataleftentryleftvalue))))))))) /\ (((exists dst_positive_code_reindex_dataleftentryright dst_positive_scale_reindex_dataleftentryright dst_negative_code_reindex_dataleftentryright dst_negative_scale_reindex_dataleftentryright dst_positive_reindex_dataleftentryright dst_negative_reindex_dataleftentryright. (((G) = (((((dst_positive_code_reindex_dataleftentryright) + (dst_positive_scale_reindex_dataleftentryright)) * S ((dst_positive_code_reindex_dataleftentryright) + (dst_positive_scale_reindex_dataleftentryright)) + ((dst_positive_scale_reindex_dataleftentryright) + (dst_positive_scale_reindex_dataleftentryright))) + (((dst_negative_code_reindex_dataleftentryright) + (dst_negative_scale_reindex_dataleftentryright)) * S ((dst_negative_code_reindex_dataleftentryright) + (dst_negative_scale_reindex_dataleftentryright)) + ((dst_negative_scale_reindex_dataleftentryright) + (dst_negative_scale_reindex_dataleftentryright)))) * S ((((dst_positive_code_reindex_dataleftentryright) + (dst_positive_scale_reindex_dataleftentryright)) * S ((dst_positive_code_reindex_dataleftentryright) + (dst_positive_scale_reindex_dataleftentryright)) + ((dst_positive_scale_reindex_dataleftentryright) + (dst_positive_scale_reindex_dataleftentryright))) + (((dst_negative_code_reindex_dataleftentryright) + (dst_negative_scale_reindex_dataleftentryright)) * S ((dst_negative_code_reindex_dataleftentryright) + (dst_negative_scale_reindex_dataleftentryright)) + ((dst_negative_scale_reindex_dataleftentryright) + (dst_negative_scale_reindex_dataleftentryright)))) + ((((dst_negative_code_reindex_dataleftentryright) + (dst_negative_scale_reindex_dataleftentryright)) * S ((dst_negative_code_reindex_dataleftentryright) + (dst_negative_scale_reindex_dataleftentryright)) + ((dst_negative_scale_reindex_dataleftentryright) + (dst_negative_scale_reindex_dataleftentryright))) + (((dst_negative_code_reindex_dataleftentryright) + (dst_negative_scale_reindex_dataleftentryright)) * S ((dst_negative_code_reindex_dataleftentryright) + (dst_negative_scale_reindex_dataleftentryright)) + ((dst_negative_scale_reindex_dataleftentryright) + (dst_negative_scale_reindex_dataleftentryright)))))) /\ (((((exists ff_h_pvs_reindex_dataleftentryrightpositive. ff_h_pvs_reindex_dataleftentryrightpositive + S (dst_positive_reindex_dataleftentryright) = S ((S (dc_quotient_reindex_dataleftentry)) * dst_positive_scale_reindex_dataleftentryright)) /\ exists ff_q_pvs_reindex_dataleftentryrightpositive. dst_positive_code_reindex_dataleftentryright = ff_q_pvs_reindex_dataleftentryrightpositive * S ((S (dc_quotient_reindex_dataleftentry)) * dst_positive_scale_reindex_dataleftentryright) + (dst_positive_reindex_dataleftentryright))) /\ (((((exists ff_h_pvs_reindex_dataleftentryrightnegative. ff_h_pvs_reindex_dataleftentryrightnegative + S (dst_negative_reindex_dataleftentryright) = S ((S (dc_quotient_reindex_dataleftentry)) * dst_negative_scale_reindex_dataleftentryright)) /\ exists ff_q_pvs_reindex_dataleftentryrightnegative. dst_negative_code_reindex_dataleftentryright = ff_q_pvs_reindex_dataleftentryrightnegative * S ((S (dc_quotient_reindex_dataleftentry)) * dst_negative_scale_reindex_dataleftentryright) + (dst_negative_reindex_dataleftentryright))) /\ (exists ge_balance_positive_reindex_dataleftentryrightvalue ge_balance_negative_reindex_dataleftentryrightvalue. (((((dc_right_reindex_dataleftentry) = 2 * (ge_balance_positive_reindex_dataleftentryrightvalue) /\ (ge_balance_negative_reindex_dataleftentryrightvalue) = 0) \/ exists ge_signed_half_reindex_dataleftentryrightvaluedecode. (((dc_right_reindex_dataleftentry) = 2 * ge_signed_half_reindex_dataleftentryrightvaluedecode + 1 /\ (ge_balance_positive_reindex_dataleftentryrightvalue) = 0) /\ (ge_balance_negative_reindex_dataleftentryrightvalue) = S ge_signed_half_reindex_dataleftentryrightvaluedecode))) /\ ((dst_positive_reindex_dataleftentryright) + ge_balance_negative_reindex_dataleftentryrightvalue = (dst_negative_reindex_dataleftentryright) + ge_balance_positive_reindex_dataleftentryrightvalue))))))))) /\ (exists sto_ap_reindex_dataleftentryproduct sto_an_reindex_dataleftentryproduct sto_bp_reindex_dataleftentryproduct sto_bn_reindex_dataleftentryproduct sto_cp_reindex_dataleftentryproduct sto_cn_reindex_dataleftentryproduct. (((((dc_left_reindex_dataleftentry) = 2 * (sto_ap_reindex_dataleftentryproduct) /\ (sto_an_reindex_dataleftentryproduct) = 0) \/ exists ge_signed_half_reindex_dataleftentryproductleft. (((dc_left_reindex_dataleftentry) = 2 * ge_signed_half_reindex_dataleftentryproductleft + 1 /\ (sto_ap_reindex_dataleftentryproduct) = 0) /\ (sto_an_reindex_dataleftentryproduct) = S ge_signed_half_reindex_dataleftentryproductleft))) /\ ((((((dc_right_reindex_dataleftentry) = 2 * (sto_bp_reindex_dataleftentryproduct) /\ (sto_bn_reindex_dataleftentryproduct) = 0) \/ exists ge_signed_half_reindex_dataleftentryproductright. (((dc_right_reindex_dataleftentry) = 2 * ge_signed_half_reindex_dataleftentryproductright + 1 /\ (sto_bp_reindex_dataleftentryproduct) = 0) /\ (sto_bn_reindex_dataleftentryproduct) = S ge_signed_half_reindex_dataleftentryproductright))) /\ ((((((dc_value_reindex_dataleft) = 2 * (sto_cp_reindex_dataleftentryproduct) /\ (sto_cn_reindex_dataleftentryproduct) = 0) \/ exists ge_signed_half_reindex_dataleftentryproductoutput. (((dc_value_reindex_dataleft) = 2 * ge_signed_half_reindex_dataleftentryproductoutput + 1 /\ (sto_cp_reindex_dataleftentryproduct) = 0) /\ (sto_cn_reindex_dataleftentryproduct) = S ge_signed_half_reindex_dataleftentryproductoutput))) /\ ((sto_ap_reindex_dataleftentryproduct * sto_bp_reindex_dataleftentryproduct + sto_an_reindex_dataleftentryproduct * sto_bn_reindex_dataleftentryproduct) + sto_cn_reindex_dataleftentryproduct = (sto_ap_reindex_dataleftentryproduct * sto_bn_reindex_dataleftentryproduct + sto_an_reindex_dataleftentryproduct * sto_bp_reindex_dataleftentryproduct) + sto_cp_reindex_dataleftentryproduct))))))))))))))) \/ ((((dc_index_reindex_dataleft)=0 \/ ~(exists pvs_factor_reindex_dataleftentrynondivisor. (m) = (dc_index_reindex_dataleft) * pvs_factor_reindex_dataleftentrynondivisor)) /\ ((dc_value_reindex_dataleft)=0))))))) /\ (((((exists dst_positive_code_reindex_datarighttable dst_positive_scale_reindex_datarighttable dst_negative_code_reindex_datarighttable dst_negative_scale_reindex_datarighttable. (((B) = (((((dst_positive_code_reindex_datarighttable) + (dst_positive_scale_reindex_datarighttable)) * S ((dst_positive_code_reindex_datarighttable) + (dst_positive_scale_reindex_datarighttable)) + ((dst_positive_scale_reindex_datarighttable) + (dst_positive_scale_reindex_datarighttable))) + (((dst_negative_code_reindex_datarighttable) + (dst_negative_scale_reindex_datarighttable)) * S ((dst_negative_code_reindex_datarighttable) + (dst_negative_scale_reindex_datarighttable)) + ((dst_negative_scale_reindex_datarighttable) + (dst_negative_scale_reindex_datarighttable)))) * S ((((dst_positive_code_reindex_datarighttable) + (dst_positive_scale_reindex_datarighttable)) * S ((dst_positive_code_reindex_datarighttable) + (dst_positive_scale_reindex_datarighttable)) + ((dst_positive_scale_reindex_datarighttable) + (dst_positive_scale_reindex_datarighttable))) + (((dst_negative_code_reindex_datarighttable) + (dst_negative_scale_reindex_datarighttable)) * S ((dst_negative_code_reindex_datarighttable) + (dst_negative_scale_reindex_datarighttable)) + ((dst_negative_scale_reindex_datarighttable) + (dst_negative_scale_reindex_datarighttable)))) + ((((dst_negative_code_reindex_datarighttable) + (dst_negative_scale_reindex_datarighttable)) * S ((dst_negative_code_reindex_datarighttable) + (dst_negative_scale_reindex_datarighttable)) + ((dst_negative_scale_reindex_datarighttable) + (dst_negative_scale_reindex_datarighttable))) + (((dst_negative_code_reindex_datarighttable) + (dst_negative_scale_reindex_datarighttable)) * S ((dst_negative_code_reindex_datarighttable) + (dst_negative_scale_reindex_datarighttable)) + ((dst_negative_scale_reindex_datarighttable) + (dst_negative_scale_reindex_datarighttable)))))) /\ (forall dst_index_reindex_datarighttable. (exists pvs_le_gap_reindex_datarighttabledomain. pvs_le_gap_reindex_datarighttabledomain + (dst_index_reindex_datarighttable) = (n)) -> exists dst_positive_reindex_datarighttable dst_negative_reindex_datarighttable dst_value_reindex_datarighttable. ((((exists ff_h_pvs_reindex_datarighttableentrypositive. ff_h_pvs_reindex_datarighttableentrypositive + S (dst_positive_reindex_datarighttable) = S ((S (dst_index_reindex_datarighttable)) * dst_positive_scale_reindex_datarighttable)) /\ exists ff_q_pvs_reindex_datarighttableentrypositive. dst_positive_code_reindex_datarighttable = ff_q_pvs_reindex_datarighttableentrypositive * S ((S (dst_index_reindex_datarighttable)) * dst_positive_scale_reindex_datarighttable) + (dst_positive_reindex_datarighttable))) /\ (((((exists ff_h_pvs_reindex_datarighttableentrynegative. ff_h_pvs_reindex_datarighttableentrynegative + S (dst_negative_reindex_datarighttable) = S ((S (dst_index_reindex_datarighttable)) * dst_negative_scale_reindex_datarighttable)) /\ exists ff_q_pvs_reindex_datarighttableentrynegative. dst_negative_code_reindex_datarighttable = ff_q_pvs_reindex_datarighttableentrynegative * S ((S (dst_index_reindex_datarighttable)) * dst_negative_scale_reindex_datarighttable) + (dst_negative_reindex_datarighttable))) /\ (exists ge_balance_positive_reindex_datarighttableentryvalue ge_balance_negative_reindex_datarighttableentryvalue. (((((dst_value_reindex_datarighttable) = 2 * (ge_balance_positive_reindex_datarighttableentryvalue) /\ (ge_balance_negative_reindex_datarighttableentryvalue) = 0) \/ exists ge_signed_half_reindex_datarighttableentryvaluedecode. (((dst_value_reindex_datarighttable) = 2 * ge_signed_half_reindex_datarighttableentryvaluedecode + 1 /\ (ge_balance_positive_reindex_datarighttableentryvalue) = 0) /\ (ge_balance_negative_reindex_datarighttableentryvalue) = S ge_signed_half_reindex_datarighttableentryvaluedecode))) /\ ((dst_positive_reindex_datarighttable) + ge_balance_negative_reindex_datarighttableentryvalue = (dst_negative_reindex_datarighttable) + ge_balance_positive_reindex_datarighttableentryvalue))))))))) /\ (forall dc_index_reindex_dataright dc_value_reindex_dataright. (exists pvs_le_gap_reindex_datarightdomain. pvs_le_gap_reindex_datarightdomain + (dc_index_reindex_dataright) = (n)) -> (exists dst_positive_code_reindex_datarightlookup dst_positive_scale_reindex_datarightlookup dst_negative_code_reindex_datarightlookup dst_negative_scale_reindex_datarightlookup dst_positive_reindex_datarightlookup dst_negative_reindex_datarightlookup. (((B) = (((((dst_positive_code_reindex_datarightlookup) + (dst_positive_scale_reindex_datarightlookup)) * S ((dst_positive_code_reindex_datarightlookup) + (dst_positive_scale_reindex_datarightlookup)) + ((dst_positive_scale_reindex_datarightlookup) + (dst_positive_scale_reindex_datarightlookup))) + (((dst_negative_code_reindex_datarightlookup) + (dst_negative_scale_reindex_datarightlookup)) * S ((dst_negative_code_reindex_datarightlookup) + (dst_negative_scale_reindex_datarightlookup)) + ((dst_negative_scale_reindex_datarightlookup) + (dst_negative_scale_reindex_datarightlookup)))) * S ((((dst_positive_code_reindex_datarightlookup) + (dst_positive_scale_reindex_datarightlookup)) * S ((dst_positive_code_reindex_datarightlookup) + (dst_positive_scale_reindex_datarightlookup)) + ((dst_positive_scale_reindex_datarightlookup) + (dst_positive_scale_reindex_datarightlookup))) + (((dst_negative_code_reindex_datarightlookup) + (dst_negative_scale_reindex_datarightlookup)) * S ((dst_negative_code_reindex_datarightlookup) + (dst_negative_scale_reindex_datarightlookup)) + ((dst_negative_scale_reindex_datarightlookup) + (dst_negative_scale_reindex_datarightlookup)))) + ((((dst_negative_code_reindex_datarightlookup) + (dst_negative_scale_reindex_datarightlookup)) * S ((dst_negative_code_reindex_datarightlookup) + (dst_negative_scale_reindex_datarightlookup)) + ((dst_negative_scale_reindex_datarightlookup) + (dst_negative_scale_reindex_datarightlookup))) + (((dst_negative_code_reindex_datarightlookup) + (dst_negative_scale_reindex_datarightlookup)) * S ((dst_negative_code_reindex_datarightlookup) + (dst_negative_scale_reindex_datarightlookup)) + ((dst_negative_scale_reindex_datarightlookup) + (dst_negative_scale_reindex_datarightlookup)))))) /\ (((((exists ff_h_pvs_reindex_datarightlookuppositive. ff_h_pvs_reindex_datarightlookuppositive + S (dst_positive_reindex_datarightlookup) = S ((S (dc_index_reindex_dataright)) * dst_positive_scale_reindex_datarightlookup)) /\ exists ff_q_pvs_reindex_datarightlookuppositive. dst_positive_code_reindex_datarightlookup = ff_q_pvs_reindex_datarightlookuppositive * S ((S (dc_index_reindex_dataright)) * dst_positive_scale_reindex_datarightlookup) + (dst_positive_reindex_datarightlookup))) /\ (((((exists ff_h_pvs_reindex_datarightlookupnegative. ff_h_pvs_reindex_datarightlookupnegative + S (dst_negative_reindex_datarightlookup) = S ((S (dc_index_reindex_dataright)) * dst_negative_scale_reindex_datarightlookup)) /\ exists ff_q_pvs_reindex_datarightlookupnegative. dst_negative_code_reindex_datarightlookup = ff_q_pvs_reindex_datarightlookupnegative * S ((S (dc_index_reindex_dataright)) * dst_negative_scale_reindex_datarightlookup) + (dst_negative_reindex_datarightlookup))) /\ (exists ge_balance_positive_reindex_datarightlookupvalue ge_balance_negative_reindex_datarightlookupvalue. (((((dc_value_reindex_dataright) = 2 * (ge_balance_positive_reindex_datarightlookupvalue) /\ (ge_balance_negative_reindex_datarightlookupvalue) = 0) \/ exists ge_signed_half_reindex_datarightlookupvaluedecode. (((dc_value_reindex_dataright) = 2 * ge_signed_half_reindex_datarightlookupvaluedecode + 1 /\ (ge_balance_positive_reindex_datarightlookupvalue) = 0) /\ (ge_balance_negative_reindex_datarightlookupvalue) = S ge_signed_half_reindex_datarightlookupvaluedecode))) /\ ((dst_positive_reindex_datarightlookup) + ge_balance_negative_reindex_datarightlookupvalue = (dst_negative_reindex_datarightlookup) + ge_balance_positive_reindex_datarightlookupvalue))))))))) -> ((((~((dc_index_reindex_dataright)=0)) /\ (exists dc_quotient_reindex_datarightentry dc_left_reindex_datarightentry dc_right_reindex_datarightentry. (((n)=(dc_index_reindex_dataright)*dc_quotient_reindex_datarightentry) /\ (((exists dst_positive_code_reindex_datarightentryleft dst_positive_scale_reindex_datarightentryleft dst_negative_code_reindex_datarightentryleft dst_negative_scale_reindex_datarightentryleft dst_positive_reindex_datarightentryleft dst_negative_reindex_datarightentryleft. (((F) = (((((dst_positive_code_reindex_datarightentryleft) + (dst_positive_scale_reindex_datarightentryleft)) * S ((dst_positive_code_reindex_datarightentryleft) + (dst_positive_scale_reindex_datarightentryleft)) + ((dst_positive_scale_reindex_datarightentryleft) + (dst_positive_scale_reindex_datarightentryleft))) + (((dst_negative_code_reindex_datarightentryleft) + (dst_negative_scale_reindex_datarightentryleft)) * S ((dst_negative_code_reindex_datarightentryleft) + (dst_negative_scale_reindex_datarightentryleft)) + ((dst_negative_scale_reindex_datarightentryleft) + (dst_negative_scale_reindex_datarightentryleft)))) * S ((((dst_positive_code_reindex_datarightentryleft) + (dst_positive_scale_reindex_datarightentryleft)) * S ((dst_positive_code_reindex_datarightentryleft) + (dst_positive_scale_reindex_datarightentryleft)) + ((dst_positive_scale_reindex_datarightentryleft) + (dst_positive_scale_reindex_datarightentryleft))) + (((dst_negative_code_reindex_datarightentryleft) + (dst_negative_scale_reindex_datarightentryleft)) * S ((dst_negative_code_reindex_datarightentryleft) + (dst_negative_scale_reindex_datarightentryleft)) + ((dst_negative_scale_reindex_datarightentryleft) + (dst_negative_scale_reindex_datarightentryleft)))) + ((((dst_negative_code_reindex_datarightentryleft) + (dst_negative_scale_reindex_datarightentryleft)) * S ((dst_negative_code_reindex_datarightentryleft) + (dst_negative_scale_reindex_datarightentryleft)) + ((dst_negative_scale_reindex_datarightentryleft) + (dst_negative_scale_reindex_datarightentryleft))) + (((dst_negative_code_reindex_datarightentryleft) + (dst_negative_scale_reindex_datarightentryleft)) * S ((dst_negative_code_reindex_datarightentryleft) + (dst_negative_scale_reindex_datarightentryleft)) + ((dst_negative_scale_reindex_datarightentryleft) + (dst_negative_scale_reindex_datarightentryleft)))))) /\ (((((exists ff_h_pvs_reindex_datarightentryleftpositive. ff_h_pvs_reindex_datarightentryleftpositive + S (dst_positive_reindex_datarightentryleft) = S ((S (dc_index_reindex_dataright)) * dst_positive_scale_reindex_datarightentryleft)) /\ exists ff_q_pvs_reindex_datarightentryleftpositive. dst_positive_code_reindex_datarightentryleft = ff_q_pvs_reindex_datarightentryleftpositive * S ((S (dc_index_reindex_dataright)) * dst_positive_scale_reindex_datarightentryleft) + (dst_positive_reindex_datarightentryleft))) /\ (((((exists ff_h_pvs_reindex_datarightentryleftnegative. ff_h_pvs_reindex_datarightentryleftnegative + S (dst_negative_reindex_datarightentryleft) = S ((S (dc_index_reindex_dataright)) * dst_negative_scale_reindex_datarightentryleft)) /\ exists ff_q_pvs_reindex_datarightentryleftnegative. dst_negative_code_reindex_datarightentryleft = ff_q_pvs_reindex_datarightentryleftnegative * S ((S (dc_index_reindex_dataright)) * dst_negative_scale_reindex_datarightentryleft) + (dst_negative_reindex_datarightentryleft))) /\ (exists ge_balance_positive_reindex_datarightentryleftvalue ge_balance_negative_reindex_datarightentryleftvalue. (((((dc_left_reindex_datarightentry) = 2 * (ge_balance_positive_reindex_datarightentryleftvalue) /\ (ge_balance_negative_reindex_datarightentryleftvalue) = 0) \/ exists ge_signed_half_reindex_datarightentryleftvaluedecode. (((dc_left_reindex_datarightentry) = 2 * ge_signed_half_reindex_datarightentryleftvaluedecode + 1 /\ (ge_balance_positive_reindex_datarightentryleftvalue) = 0) /\ (ge_balance_negative_reindex_datarightentryleftvalue) = S ge_signed_half_reindex_datarightentryleftvaluedecode))) /\ ((dst_positive_reindex_datarightentryleft) + ge_balance_negative_reindex_datarightentryleftvalue = (dst_negative_reindex_datarightentryleft) + ge_balance_positive_reindex_datarightentryleftvalue))))))))) /\ (((exists dst_positive_code_reindex_datarightentryright dst_positive_scale_reindex_datarightentryright dst_negative_code_reindex_datarightentryright dst_negative_scale_reindex_datarightentryright dst_positive_reindex_datarightentryright dst_negative_reindex_datarightentryright. (((G) = (((((dst_positive_code_reindex_datarightentryright) + (dst_positive_scale_reindex_datarightentryright)) * S ((dst_positive_code_reindex_datarightentryright) + (dst_positive_scale_reindex_datarightentryright)) + ((dst_positive_scale_reindex_datarightentryright) + (dst_positive_scale_reindex_datarightentryright))) + (((dst_negative_code_reindex_datarightentryright) + (dst_negative_scale_reindex_datarightentryright)) * S ((dst_negative_code_reindex_datarightentryright) + (dst_negative_scale_reindex_datarightentryright)) + ((dst_negative_scale_reindex_datarightentryright) + (dst_negative_scale_reindex_datarightentryright)))) * S ((((dst_positive_code_reindex_datarightentryright) + (dst_positive_scale_reindex_datarightentryright)) * S ((dst_positive_code_reindex_datarightentryright) + (dst_positive_scale_reindex_datarightentryright)) + ((dst_positive_scale_reindex_datarightentryright) + (dst_positive_scale_reindex_datarightentryright))) + (((dst_negative_code_reindex_datarightentryright) + (dst_negative_scale_reindex_datarightentryright)) * S ((dst_negative_code_reindex_datarightentryright) + (dst_negative_scale_reindex_datarightentryright)) + ((dst_negative_scale_reindex_datarightentryright) + (dst_negative_scale_reindex_datarightentryright)))) + ((((dst_negative_code_reindex_datarightentryright) + (dst_negative_scale_reindex_datarightentryright)) * S ((dst_negative_code_reindex_datarightentryright) + (dst_negative_scale_reindex_datarightentryright)) + ((dst_negative_scale_reindex_datarightentryright) + (dst_negative_scale_reindex_datarightentryright))) + (((dst_negative_code_reindex_datarightentryright) + (dst_negative_scale_reindex_datarightentryright)) * S ((dst_negative_code_reindex_datarightentryright) + (dst_negative_scale_reindex_datarightentryright)) + ((dst_negative_scale_reindex_datarightentryright) + (dst_negative_scale_reindex_datarightentryright)))))) /\ (((((exists ff_h_pvs_reindex_datarightentryrightpositive. ff_h_pvs_reindex_datarightentryrightpositive + S (dst_positive_reindex_datarightentryright) = S ((S (dc_quotient_reindex_datarightentry)) * dst_positive_scale_reindex_datarightentryright)) /\ exists ff_q_pvs_reindex_datarightentryrightpositive. dst_positive_code_reindex_datarightentryright = ff_q_pvs_reindex_datarightentryrightpositive * S ((S (dc_quotient_reindex_datarightentry)) * dst_positive_scale_reindex_datarightentryright) + (dst_positive_reindex_datarightentryright))) /\ (((((exists ff_h_pvs_reindex_datarightentryrightnegative. ff_h_pvs_reindex_datarightentryrightnegative + S (dst_negative_reindex_datarightentryright) = S ((S (dc_quotient_reindex_datarightentry)) * dst_negative_scale_reindex_datarightentryright)) /\ exists ff_q_pvs_reindex_datarightentryrightnegative. dst_negative_code_reindex_datarightentryright = ff_q_pvs_reindex_datarightentryrightnegative * S ((S (dc_quotient_reindex_datarightentry)) * dst_negative_scale_reindex_datarightentryright) + (dst_negative_reindex_datarightentryright))) /\ (exists ge_balance_positive_reindex_datarightentryrightvalue ge_balance_negative_reindex_datarightentryrightvalue. (((((dc_right_reindex_datarightentry) = 2 * (ge_balance_positive_reindex_datarightentryrightvalue) /\ (ge_balance_negative_reindex_datarightentryrightvalue) = 0) \/ exists ge_signed_half_reindex_datarightentryrightvaluedecode. (((dc_right_reindex_datarightentry) = 2 * ge_signed_half_reindex_datarightentryrightvaluedecode + 1 /\ (ge_balance_positive_reindex_datarightentryrightvalue) = 0) /\ (ge_balance_negative_reindex_datarightentryrightvalue) = S ge_signed_half_reindex_datarightentryrightvaluedecode))) /\ ((dst_positive_reindex_datarightentryright) + ge_balance_negative_reindex_datarightentryrightvalue = (dst_negative_reindex_datarightentryright) + ge_balance_positive_reindex_datarightentryrightvalue))))))))) /\ (exists sto_ap_reindex_datarightentryproduct sto_an_reindex_datarightentryproduct sto_bp_reindex_datarightentryproduct sto_bn_reindex_datarightentryproduct sto_cp_reindex_datarightentryproduct sto_cn_reindex_datarightentryproduct. (((((dc_left_reindex_datarightentry) = 2 * (sto_ap_reindex_datarightentryproduct) /\ (sto_an_reindex_datarightentryproduct) = 0) \/ exists ge_signed_half_reindex_datarightentryproductleft. (((dc_left_reindex_datarightentry) = 2 * ge_signed_half_reindex_datarightentryproductleft + 1 /\ (sto_ap_reindex_datarightentryproduct) = 0) /\ (sto_an_reindex_datarightentryproduct) = S ge_signed_half_reindex_datarightentryproductleft))) /\ ((((((dc_right_reindex_datarightentry) = 2 * (sto_bp_reindex_datarightentryproduct) /\ (sto_bn_reindex_datarightentryproduct) = 0) \/ exists ge_signed_half_reindex_datarightentryproductright. (((dc_right_reindex_datarightentry) = 2 * ge_signed_half_reindex_datarightentryproductright + 1 /\ (sto_bp_reindex_datarightentryproduct) = 0) /\ (sto_bn_reindex_datarightentryproduct) = S ge_signed_half_reindex_datarightentryproductright))) /\ ((((((dc_value_reindex_dataright) = 2 * (sto_cp_reindex_datarightentryproduct) /\ (sto_cn_reindex_datarightentryproduct) = 0) \/ exists ge_signed_half_reindex_datarightentryproductoutput. (((dc_value_reindex_dataright) = 2 * ge_signed_half_reindex_datarightentryproductoutput + 1 /\ (sto_cp_reindex_datarightentryproduct) = 0) /\ (sto_cn_reindex_datarightentryproduct) = S ge_signed_half_reindex_datarightentryproductoutput))) /\ ((sto_ap_reindex_datarightentryproduct * sto_bp_reindex_datarightentryproduct + sto_an_reindex_datarightentryproduct * sto_bn_reindex_datarightentryproduct) + sto_cn_reindex_datarightentryproduct = (sto_ap_reindex_datarightentryproduct * sto_bn_reindex_datarightentryproduct + sto_an_reindex_datarightentryproduct * sto_bp_reindex_datarightentryproduct) + sto_cp_reindex_datarightentryproduct))))))))))))))) \/ ((((dc_index_reindex_dataright)=0 \/ ~(exists pvs_factor_reindex_datarightentrynondivisor. (n) = (dc_index_reindex_dataright) * pvs_factor_reindex_datarightentrynondivisor)) /\ ((dc_value_reindex_dataright)=0))))))) /\ (((((exists dst_positive_code_reindex_datacartesianF dst_positive_scale_reindex_datacartesianF dst_negative_code_reindex_datacartesianF dst_negative_scale_reindex_datacartesianF. (((A) = (((((dst_positive_code_reindex_datacartesianF) + (dst_positive_scale_reindex_datacartesianF)) * S ((dst_positive_code_reindex_datacartesianF) + (dst_positive_scale_reindex_datacartesianF)) + ((dst_positive_scale_reindex_datacartesianF) + (dst_positive_scale_reindex_datacartesianF))) + (((dst_negative_code_reindex_datacartesianF) + (dst_negative_scale_reindex_datacartesianF)) * S ((dst_negative_code_reindex_datacartesianF) + (dst_negative_scale_reindex_datacartesianF)) + ((dst_negative_scale_reindex_datacartesianF) + (dst_negative_scale_reindex_datacartesianF)))) * S ((((dst_positive_code_reindex_datacartesianF) + (dst_positive_scale_reindex_datacartesianF)) * S ((dst_positive_code_reindex_datacartesianF) + (dst_positive_scale_reindex_datacartesianF)) + ((dst_positive_scale_reindex_datacartesianF) + (dst_positive_scale_reindex_datacartesianF))) + (((dst_negative_code_reindex_datacartesianF) + (dst_negative_scale_reindex_datacartesianF)) * S ((dst_negative_code_reindex_datacartesianF) + (dst_negative_scale_reindex_datacartesianF)) + ((dst_negative_scale_reindex_datacartesianF) + (dst_negative_scale_reindex_datacartesianF)))) + ((((dst_negative_code_reindex_datacartesianF) + (dst_negative_scale_reindex_datacartesianF)) * S ((dst_negative_code_reindex_datacartesianF) + (dst_negative_scale_reindex_datacartesianF)) + ((dst_negative_scale_reindex_datacartesianF) + (dst_negative_scale_reindex_datacartesianF))) + (((dst_negative_code_reindex_datacartesianF) + (dst_negative_scale_reindex_datacartesianF)) * S ((dst_negative_code_reindex_datacartesianF) + (dst_negative_scale_reindex_datacartesianF)) + ((dst_negative_scale_reindex_datacartesianF) + (dst_negative_scale_reindex_datacartesianF)))))) /\ (forall dst_index_reindex_datacartesianF. (exists pvs_le_gap_reindex_datacartesianFdomain. pvs_le_gap_reindex_datacartesianFdomain + (dst_index_reindex_datacartesianF) = (0)) -> exists dst_positive_reindex_datacartesianF dst_negative_reindex_datacartesianF dst_value_reindex_datacartesianF. ((((exists ff_h_pvs_reindex_datacartesianFentrypositive. ff_h_pvs_reindex_datacartesianFentrypositive + S (dst_positive_reindex_datacartesianF) = S ((S (dst_index_reindex_datacartesianF)) * dst_positive_scale_reindex_datacartesianF)) /\ exists ff_q_pvs_reindex_datacartesianFentrypositive. dst_positive_code_reindex_datacartesianF = ff_q_pvs_reindex_datacartesianFentrypositive * S ((S (dst_index_reindex_datacartesianF)) * dst_positive_scale_reindex_datacartesianF) + (dst_positive_reindex_datacartesianF))) /\ (((((exists ff_h_pvs_reindex_datacartesianFentrynegative. ff_h_pvs_reindex_datacartesianFentrynegative + S (dst_negative_reindex_datacartesianF) = S ((S (dst_index_reindex_datacartesianF)) * dst_negative_scale_reindex_datacartesianF)) /\ exists ff_q_pvs_reindex_datacartesianFentrynegative. dst_negative_code_reindex_datacartesianF = ff_q_pvs_reindex_datacartesianFentrynegative * S ((S (dst_index_reindex_datacartesianF)) * dst_negative_scale_reindex_datacartesianF) + (dst_negative_reindex_datacartesianF))) /\ (exists ge_balance_positive_reindex_datacartesianFentryvalue ge_balance_negative_reindex_datacartesianFentryvalue. (((((dst_value_reindex_datacartesianF) = 2 * (ge_balance_positive_reindex_datacartesianFentryvalue) /\ (ge_balance_negative_reindex_datacartesianFentryvalue) = 0) \/ exists ge_signed_half_reindex_datacartesianFentryvaluedecode. (((dst_value_reindex_datacartesianF) = 2 * ge_signed_half_reindex_datacartesianFentryvaluedecode + 1 /\ (ge_balance_positive_reindex_datacartesianFentryvalue) = 0) /\ (ge_balance_negative_reindex_datacartesianFentryvalue) = S ge_signed_half_reindex_datacartesianFentryvaluedecode))) /\ ((dst_positive_reindex_datacartesianF) + ge_balance_negative_reindex_datacartesianFentryvalue = (dst_negative_reindex_datacartesianF) + ge_balance_positive_reindex_datacartesianFentryvalue))))))))) /\ (((exists dst_positive_code_reindex_datacartesianG dst_positive_scale_reindex_datacartesianG dst_negative_code_reindex_datacartesianG dst_negative_scale_reindex_datacartesianG. (((B) = (((((dst_positive_code_reindex_datacartesianG) + (dst_positive_scale_reindex_datacartesianG)) * S ((dst_positive_code_reindex_datacartesianG) + (dst_positive_scale_reindex_datacartesianG)) + ((dst_positive_scale_reindex_datacartesianG) + (dst_positive_scale_reindex_datacartesianG))) + (((dst_negative_code_reindex_datacartesianG) + (dst_negative_scale_reindex_datacartesianG)) * S ((dst_negative_code_reindex_datacartesianG) + (dst_negative_scale_reindex_datacartesianG)) + ((dst_negative_scale_reindex_datacartesianG) + (dst_negative_scale_reindex_datacartesianG)))) * S ((((dst_positive_code_reindex_datacartesianG) + (dst_positive_scale_reindex_datacartesianG)) * S ((dst_positive_code_reindex_datacartesianG) + (dst_positive_scale_reindex_datacartesianG)) + ((dst_positive_scale_reindex_datacartesianG) + (dst_positive_scale_reindex_datacartesianG))) + (((dst_negative_code_reindex_datacartesianG) + (dst_negative_scale_reindex_datacartesianG)) * S ((dst_negative_code_reindex_datacartesianG) + (dst_negative_scale_reindex_datacartesianG)) + ((dst_negative_scale_reindex_datacartesianG) + (dst_negative_scale_reindex_datacartesianG)))) + ((((dst_negative_code_reindex_datacartesianG) + (dst_negative_scale_reindex_datacartesianG)) * S ((dst_negative_code_reindex_datacartesianG) + (dst_negative_scale_reindex_datacartesianG)) + ((dst_negative_scale_reindex_datacartesianG) + (dst_negative_scale_reindex_datacartesianG))) + (((dst_negative_code_reindex_datacartesianG) + (dst_negative_scale_reindex_datacartesianG)) * S ((dst_negative_code_reindex_datacartesianG) + (dst_negative_scale_reindex_datacartesianG)) + ((dst_negative_scale_reindex_datacartesianG) + (dst_negative_scale_reindex_datacartesianG)))))) /\ (forall dst_index_reindex_datacartesianG. (exists pvs_le_gap_reindex_datacartesianGdomain. pvs_le_gap_reindex_datacartesianGdomain + (dst_index_reindex_datacartesianG) = (0)) -> exists dst_positive_reindex_datacartesianG dst_negative_reindex_datacartesianG dst_value_reindex_datacartesianG. ((((exists ff_h_pvs_reindex_datacartesianGentrypositive. ff_h_pvs_reindex_datacartesianGentrypositive + S (dst_positive_reindex_datacartesianG) = S ((S (dst_index_reindex_datacartesianG)) * dst_positive_scale_reindex_datacartesianG)) /\ exists ff_q_pvs_reindex_datacartesianGentrypositive. dst_positive_code_reindex_datacartesianG = ff_q_pvs_reindex_datacartesianGentrypositive * S ((S (dst_index_reindex_datacartesianG)) * dst_positive_scale_reindex_datacartesianG) + (dst_positive_reindex_datacartesianG))) /\ (((((exists ff_h_pvs_reindex_datacartesianGentrynegative. ff_h_pvs_reindex_datacartesianGentrynegative + S (dst_negative_reindex_datacartesianG) = S ((S (dst_index_reindex_datacartesianG)) * dst_negative_scale_reindex_datacartesianG)) /\ exists ff_q_pvs_reindex_datacartesianGentrynegative. dst_negative_code_reindex_datacartesianG = ff_q_pvs_reindex_datacartesianGentrynegative * S ((S (dst_index_reindex_datacartesianG)) * dst_negative_scale_reindex_datacartesianG) + (dst_negative_reindex_datacartesianG))) /\ (exists ge_balance_positive_reindex_datacartesianGentryvalue ge_balance_negative_reindex_datacartesianGentryvalue. (((((dst_value_reindex_datacartesianG) = 2 * (ge_balance_positive_reindex_datacartesianGentryvalue) /\ (ge_balance_negative_reindex_datacartesianGentryvalue) = 0) \/ exists ge_signed_half_reindex_datacartesianGentryvaluedecode. (((dst_value_reindex_datacartesianG) = 2 * ge_signed_half_reindex_datacartesianGentryvaluedecode + 1 /\ (ge_balance_positive_reindex_datacartesianGentryvalue) = 0) /\ (ge_balance_negative_reindex_datacartesianGentryvalue) = S ge_signed_half_reindex_datacartesianGentryvaluedecode))) /\ ((dst_positive_reindex_datacartesianG) + ge_balance_negative_reindex_datacartesianGentryvalue = (dst_negative_reindex_datacartesianG) + ge_balance_positive_reindex_datacartesianGentryvalue))))))))) /\ (((exists dst_positive_code_reindex_datacartesianT dst_positive_scale_reindex_datacartesianT dst_negative_code_reindex_datacartesianT dst_negative_scale_reindex_datacartesianT. (((T) = (((((dst_positive_code_reindex_datacartesianT) + (dst_positive_scale_reindex_datacartesianT)) * S ((dst_positive_code_reindex_datacartesianT) + (dst_positive_scale_reindex_datacartesianT)) + ((dst_positive_scale_reindex_datacartesianT) + (dst_positive_scale_reindex_datacartesianT))) + (((dst_negative_code_reindex_datacartesianT) + (dst_negative_scale_reindex_datacartesianT)) * S ((dst_negative_code_reindex_datacartesianT) + (dst_negative_scale_reindex_datacartesianT)) + ((dst_negative_scale_reindex_datacartesianT) + (dst_negative_scale_reindex_datacartesianT)))) * S ((((dst_positive_code_reindex_datacartesianT) + (dst_positive_scale_reindex_datacartesianT)) * S ((dst_positive_code_reindex_datacartesianT) + (dst_positive_scale_reindex_datacartesianT)) + ((dst_positive_scale_reindex_datacartesianT) + (dst_positive_scale_reindex_datacartesianT))) + (((dst_negative_code_reindex_datacartesianT) + (dst_negative_scale_reindex_datacartesianT)) * S ((dst_negative_code_reindex_datacartesianT) + (dst_negative_scale_reindex_datacartesianT)) + ((dst_negative_scale_reindex_datacartesianT) + (dst_negative_scale_reindex_datacartesianT)))) + ((((dst_negative_code_reindex_datacartesianT) + (dst_negative_scale_reindex_datacartesianT)) * S ((dst_negative_code_reindex_datacartesianT) + (dst_negative_scale_reindex_datacartesianT)) + ((dst_negative_scale_reindex_datacartesianT) + (dst_negative_scale_reindex_datacartesianT))) + (((dst_negative_code_reindex_datacartesianT) + (dst_negative_scale_reindex_datacartesianT)) * S ((dst_negative_code_reindex_datacartesianT) + (dst_negative_scale_reindex_datacartesianT)) + ((dst_negative_scale_reindex_datacartesianT) + (dst_negative_scale_reindex_datacartesianT)))))) /\ (forall dst_index_reindex_datacartesianT. (exists pvs_le_gap_reindex_datacartesianTdomain. pvs_le_gap_reindex_datacartesianTdomain + (dst_index_reindex_datacartesianT) = ((S (m))*(S (n)))) -> exists dst_positive_reindex_datacartesianT dst_negative_reindex_datacartesianT dst_value_reindex_datacartesianT. ((((exists ff_h_pvs_reindex_datacartesianTentrypositive. ff_h_pvs_reindex_datacartesianTentrypositive + S (dst_positive_reindex_datacartesianT) = S ((S (dst_index_reindex_datacartesianT)) * dst_positive_scale_reindex_datacartesianT)) /\ exists ff_q_pvs_reindex_datacartesianTentrypositive. dst_positive_code_reindex_datacartesianT = ff_q_pvs_reindex_datacartesianTentrypositive * S ((S (dst_index_reindex_datacartesianT)) * dst_positive_scale_reindex_datacartesianT) + (dst_positive_reindex_datacartesianT))) /\ (((((exists ff_h_pvs_reindex_datacartesianTentrynegative. ff_h_pvs_reindex_datacartesianTentrynegative + S (dst_negative_reindex_datacartesianT) = S ((S (dst_index_reindex_datacartesianT)) * dst_negative_scale_reindex_datacartesianT)) /\ exists ff_q_pvs_reindex_datacartesianTentrynegative. dst_negative_code_reindex_datacartesianT = ff_q_pvs_reindex_datacartesianTentrynegative * S ((S (dst_index_reindex_datacartesianT)) * dst_negative_scale_reindex_datacartesianT) + (dst_negative_reindex_datacartesianT))) /\ (exists ge_balance_positive_reindex_datacartesianTentryvalue ge_balance_negative_reindex_datacartesianTentryvalue. (((((dst_value_reindex_datacartesianT) = 2 * (ge_balance_positive_reindex_datacartesianTentryvalue) /\ (ge_balance_negative_reindex_datacartesianTentryvalue) = 0) \/ exists ge_signed_half_reindex_datacartesianTentryvaluedecode. (((dst_value_reindex_datacartesianT) = 2 * ge_signed_half_reindex_datacartesianTentryvaluedecode + 1 /\ (ge_balance_positive_reindex_datacartesianTentryvalue) = 0) /\ (ge_balance_negative_reindex_datacartesianTentryvalue) = S ge_signed_half_reindex_datacartesianTentryvaluedecode))) /\ ((dst_positive_reindex_datacartesianT) + ge_balance_negative_reindex_datacartesianTentryvalue = (dst_negative_reindex_datacartesianT) + ge_balance_positive_reindex_datacartesianTentryvalue))))))))) /\ (forall scp_row_reindex_datacartesian scp_column_reindex_datacartesian scp_first_reindex_datacartesian scp_second_reindex_datacartesian scp_value_reindex_datacartesian. (exists pvs_gap_reindex_datacartesianrows. pvs_gap_reindex_datacartesianrows + S (scp_row_reindex_datacartesian) = (S (m))) -> (exists pvs_gap_reindex_datacartesiancolumns. pvs_gap_reindex_datacartesiancolumns + S (scp_column_reindex_datacartesian) = (S (n))) -> (exists dst_positive_code_reindex_datacartesianfirst dst_positive_scale_reindex_datacartesianfirst dst_negative_code_reindex_datacartesianfirst dst_negative_scale_reindex_datacartesianfirst dst_positive_reindex_datacartesianfirst dst_negative_reindex_datacartesianfirst. (((A) = (((((dst_positive_code_reindex_datacartesianfirst) + (dst_positive_scale_reindex_datacartesianfirst)) * S ((dst_positive_code_reindex_datacartesianfirst) + (dst_positive_scale_reindex_datacartesianfirst)) + ((dst_positive_scale_reindex_datacartesianfirst) + (dst_positive_scale_reindex_datacartesianfirst))) + (((dst_negative_code_reindex_datacartesianfirst) + (dst_negative_scale_reindex_datacartesianfirst)) * S ((dst_negative_code_reindex_datacartesianfirst) + (dst_negative_scale_reindex_datacartesianfirst)) + ((dst_negative_scale_reindex_datacartesianfirst) + (dst_negative_scale_reindex_datacartesianfirst)))) * S ((((dst_positive_code_reindex_datacartesianfirst) + (dst_positive_scale_reindex_datacartesianfirst)) * S ((dst_positive_code_reindex_datacartesianfirst) + (dst_positive_scale_reindex_datacartesianfirst)) + ((dst_positive_scale_reindex_datacartesianfirst) + (dst_positive_scale_reindex_datacartesianfirst))) + (((dst_negative_code_reindex_datacartesianfirst) + (dst_negative_scale_reindex_datacartesianfirst)) * S ((dst_negative_code_reindex_datacartesianfirst) + (dst_negative_scale_reindex_datacartesianfirst)) + ((dst_negative_scale_reindex_datacartesianfirst) + (dst_negative_scale_reindex_datacartesianfirst)))) + ((((dst_negative_code_reindex_datacartesianfirst) + (dst_negative_scale_reindex_datacartesianfirst)) * S ((dst_negative_code_reindex_datacartesianfirst) + (dst_negative_scale_reindex_datacartesianfirst)) + ((dst_negative_scale_reindex_datacartesianfirst) + (dst_negative_scale_reindex_datacartesianfirst))) + (((dst_negative_code_reindex_datacartesianfirst) + (dst_negative_scale_reindex_datacartesianfirst)) * S ((dst_negative_code_reindex_datacartesianfirst) + (dst_negative_scale_reindex_datacartesianfirst)) + ((dst_negative_scale_reindex_datacartesianfirst) + (dst_negative_scale_reindex_datacartesianfirst)))))) /\ (((((exists ff_h_pvs_reindex_datacartesianfirstpositive. ff_h_pvs_reindex_datacartesianfirstpositive + S (dst_positive_reindex_datacartesianfirst) = S ((S (scp_row_reindex_datacartesian)) * dst_positive_scale_reindex_datacartesianfirst)) /\ exists ff_q_pvs_reindex_datacartesianfirstpositive. dst_positive_code_reindex_datacartesianfirst = ff_q_pvs_reindex_datacartesianfirstpositive * S ((S (scp_row_reindex_datacartesian)) * dst_positive_scale_reindex_datacartesianfirst) + (dst_positive_reindex_datacartesianfirst))) /\ (((((exists ff_h_pvs_reindex_datacartesianfirstnegative. ff_h_pvs_reindex_datacartesianfirstnegative + S (dst_negative_reindex_datacartesianfirst) = S ((S (scp_row_reindex_datacartesian)) * dst_negative_scale_reindex_datacartesianfirst)) /\ exists ff_q_pvs_reindex_datacartesianfirstnegative. dst_negative_code_reindex_datacartesianfirst = ff_q_pvs_reindex_datacartesianfirstnegative * S ((S (scp_row_reindex_datacartesian)) * dst_negative_scale_reindex_datacartesianfirst) + (dst_negative_reindex_datacartesianfirst))) /\ (exists ge_balance_positive_reindex_datacartesianfirstvalue ge_balance_negative_reindex_datacartesianfirstvalue. (((((scp_first_reindex_datacartesian) = 2 * (ge_balance_positive_reindex_datacartesianfirstvalue) /\ (ge_balance_negative_reindex_datacartesianfirstvalue) = 0) \/ exists ge_signed_half_reindex_datacartesianfirstvaluedecode. (((scp_first_reindex_datacartesian) = 2 * ge_signed_half_reindex_datacartesianfirstvaluedecode + 1 /\ (ge_balance_positive_reindex_datacartesianfirstvalue) = 0) /\ (ge_balance_negative_reindex_datacartesianfirstvalue) = S ge_signed_half_reindex_datacartesianfirstvaluedecode))) /\ ((dst_positive_reindex_datacartesianfirst) + ge_balance_negative_reindex_datacartesianfirstvalue = (dst_negative_reindex_datacartesianfirst) + ge_balance_positive_reindex_datacartesianfirstvalue))))))))) -> (exists dst_positive_code_reindex_datacartesiansecond dst_positive_scale_reindex_datacartesiansecond dst_negative_code_reindex_datacartesiansecond dst_negative_scale_reindex_datacartesiansecond dst_positive_reindex_datacartesiansecond dst_negative_reindex_datacartesiansecond. (((B) = (((((dst_positive_code_reindex_datacartesiansecond) + (dst_positive_scale_reindex_datacartesiansecond)) * S ((dst_positive_code_reindex_datacartesiansecond) + (dst_positive_scale_reindex_datacartesiansecond)) + ((dst_positive_scale_reindex_datacartesiansecond) + (dst_positive_scale_reindex_datacartesiansecond))) + (((dst_negative_code_reindex_datacartesiansecond) + (dst_negative_scale_reindex_datacartesiansecond)) * S ((dst_negative_code_reindex_datacartesiansecond) + (dst_negative_scale_reindex_datacartesiansecond)) + ((dst_negative_scale_reindex_datacartesiansecond) + (dst_negative_scale_reindex_datacartesiansecond)))) * S ((((dst_positive_code_reindex_datacartesiansecond) + (dst_positive_scale_reindex_datacartesiansecond)) * S ((dst_positive_code_reindex_datacartesiansecond) + (dst_positive_scale_reindex_datacartesiansecond)) + ((dst_positive_scale_reindex_datacartesiansecond) + (dst_positive_scale_reindex_datacartesiansecond))) + (((dst_negative_code_reindex_datacartesiansecond) + (dst_negative_scale_reindex_datacartesiansecond)) * S ((dst_negative_code_reindex_datacartesiansecond) + (dst_negative_scale_reindex_datacartesiansecond)) + ((dst_negative_scale_reindex_datacartesiansecond) + (dst_negative_scale_reindex_datacartesiansecond)))) + ((((dst_negative_code_reindex_datacartesiansecond) + (dst_negative_scale_reindex_datacartesiansecond)) * S ((dst_negative_code_reindex_datacartesiansecond) + (dst_negative_scale_reindex_datacartesiansecond)) + ((dst_negative_scale_reindex_datacartesiansecond) + (dst_negative_scale_reindex_datacartesiansecond))) + (((dst_negative_code_reindex_datacartesiansecond) + (dst_negative_scale_reindex_datacartesiansecond)) * S ((dst_negative_code_reindex_datacartesiansecond) + (dst_negative_scale_reindex_datacartesiansecond)) + ((dst_negative_scale_reindex_datacartesiansecond) + (dst_negative_scale_reindex_datacartesiansecond)))))) /\ (((((exists ff_h_pvs_reindex_datacartesiansecondpositive. ff_h_pvs_reindex_datacartesiansecondpositive + S (dst_positive_reindex_datacartesiansecond) = S ((S (scp_column_reindex_datacartesian)) * dst_positive_scale_reindex_datacartesiansecond)) /\ exists ff_q_pvs_reindex_datacartesiansecondpositive. dst_positive_code_reindex_datacartesiansecond = ff_q_pvs_reindex_datacartesiansecondpositive * S ((S (scp_column_reindex_datacartesian)) * dst_positive_scale_reindex_datacartesiansecond) + (dst_positive_reindex_datacartesiansecond))) /\ (((((exists ff_h_pvs_reindex_datacartesiansecondnegative. ff_h_pvs_reindex_datacartesiansecondnegative + S (dst_negative_reindex_datacartesiansecond) = S ((S (scp_column_reindex_datacartesian)) * dst_negative_scale_reindex_datacartesiansecond)) /\ exists ff_q_pvs_reindex_datacartesiansecondnegative. dst_negative_code_reindex_datacartesiansecond = ff_q_pvs_reindex_datacartesiansecondnegative * S ((S (scp_column_reindex_datacartesian)) * dst_negative_scale_reindex_datacartesiansecond) + (dst_negative_reindex_datacartesiansecond))) /\ (exists ge_balance_positive_reindex_datacartesiansecondvalue ge_balance_negative_reindex_datacartesiansecondvalue. (((((scp_second_reindex_datacartesian) = 2 * (ge_balance_positive_reindex_datacartesiansecondvalue) /\ (ge_balance_negative_reindex_datacartesiansecondvalue) = 0) \/ exists ge_signed_half_reindex_datacartesiansecondvaluedecode. (((scp_second_reindex_datacartesian) = 2 * ge_signed_half_reindex_datacartesiansecondvaluedecode + 1 /\ (ge_balance_positive_reindex_datacartesiansecondvalue) = 0) /\ (ge_balance_negative_reindex_datacartesiansecondvalue) = S ge_signed_half_reindex_datacartesiansecondvaluedecode))) /\ ((dst_positive_reindex_datacartesiansecond) + ge_balance_negative_reindex_datacartesiansecondvalue = (dst_negative_reindex_datacartesiansecond) + ge_balance_positive_reindex_datacartesiansecondvalue))))))))) -> (exists dst_positive_code_reindex_datacartesianentry dst_positive_scale_reindex_datacartesianentry dst_negative_code_reindex_datacartesianentry dst_negative_scale_reindex_datacartesianentry dst_positive_reindex_datacartesianentry dst_negative_reindex_datacartesianentry. (((T) = (((((dst_positive_code_reindex_datacartesianentry) + (dst_positive_scale_reindex_datacartesianentry)) * S ((dst_positive_code_reindex_datacartesianentry) + (dst_positive_scale_reindex_datacartesianentry)) + ((dst_positive_scale_reindex_datacartesianentry) + (dst_positive_scale_reindex_datacartesianentry))) + (((dst_negative_code_reindex_datacartesianentry) + (dst_negative_scale_reindex_datacartesianentry)) * S ((dst_negative_code_reindex_datacartesianentry) + (dst_negative_scale_reindex_datacartesianentry)) + ((dst_negative_scale_reindex_datacartesianentry) + (dst_negative_scale_reindex_datacartesianentry)))) * S ((((dst_positive_code_reindex_datacartesianentry) + (dst_positive_scale_reindex_datacartesianentry)) * S ((dst_positive_code_reindex_datacartesianentry) + (dst_positive_scale_reindex_datacartesianentry)) + ((dst_positive_scale_reindex_datacartesianentry) + (dst_positive_scale_reindex_datacartesianentry))) + (((dst_negative_code_reindex_datacartesianentry) + (dst_negative_scale_reindex_datacartesianentry)) * S ((dst_negative_code_reindex_datacartesianentry) + (dst_negative_scale_reindex_datacartesianentry)) + ((dst_negative_scale_reindex_datacartesianentry) + (dst_negative_scale_reindex_datacartesianentry)))) + ((((dst_negative_code_reindex_datacartesianentry) + (dst_negative_scale_reindex_datacartesianentry)) * S ((dst_negative_code_reindex_datacartesianentry) + (dst_negative_scale_reindex_datacartesianentry)) + ((dst_negative_scale_reindex_datacartesianentry) + (dst_negative_scale_reindex_datacartesianentry))) + (((dst_negative_code_reindex_datacartesianentry) + (dst_negative_scale_reindex_datacartesianentry)) * S ((dst_negative_code_reindex_datacartesianentry) + (dst_negative_scale_reindex_datacartesianentry)) + ((dst_negative_scale_reindex_datacartesianentry) + (dst_negative_scale_reindex_datacartesianentry)))))) /\ (((((exists ff_h_pvs_reindex_datacartesianentrypositive. ff_h_pvs_reindex_datacartesianentrypositive + S (dst_positive_reindex_datacartesianentry) = S ((S (((S (n))*(scp_row_reindex_datacartesian)+(scp_column_reindex_datacartesian)))) * dst_positive_scale_reindex_datacartesianentry)) /\ exists ff_q_pvs_reindex_datacartesianentrypositive. dst_positive_code_reindex_datacartesianentry = ff_q_pvs_reindex_datacartesianentrypositive * S ((S (((S (n))*(scp_row_reindex_datacartesian)+(scp_column_reindex_datacartesian)))) * dst_positive_scale_reindex_datacartesianentry) + (dst_positive_reindex_datacartesianentry))) /\ (((((exists ff_h_pvs_reindex_datacartesianentrynegative. ff_h_pvs_reindex_datacartesianentrynegative + S (dst_negative_reindex_datacartesianentry) = S ((S (((S (n))*(scp_row_reindex_datacartesian)+(scp_column_reindex_datacartesian)))) * dst_negative_scale_reindex_datacartesianentry)) /\ exists ff_q_pvs_reindex_datacartesianentrynegative. dst_negative_code_reindex_datacartesianentry = ff_q_pvs_reindex_datacartesianentrynegative * S ((S (((S (n))*(scp_row_reindex_datacartesian)+(scp_column_reindex_datacartesian)))) * dst_negative_scale_reindex_datacartesianentry) + (dst_negative_reindex_datacartesianentry))) /\ (exists ge_balance_positive_reindex_datacartesianentryvalue ge_balance_negative_reindex_datacartesianentryvalue. (((((scp_value_reindex_datacartesian) = 2 * (ge_balance_positive_reindex_datacartesianentryvalue) /\ (ge_balance_negative_reindex_datacartesianentryvalue) = 0) \/ exists ge_signed_half_reindex_datacartesianentryvaluedecode. (((scp_value_reindex_datacartesian) = 2 * ge_signed_half_reindex_datacartesianentryvaluedecode + 1 /\ (ge_balance_positive_reindex_datacartesianentryvalue) = 0) /\ (ge_balance_negative_reindex_datacartesianentryvalue) = S ge_signed_half_reindex_datacartesianentryvaluedecode))) /\ ((dst_positive_reindex_datacartesianentry) + ge_balance_negative_reindex_datacartesianentryvalue = (dst_negative_reindex_datacartesianentry) + ge_balance_positive_reindex_datacartesianentryvalue))))))))) -> (exists sto_ap_reindex_datacartesianmultiply sto_an_reindex_datacartesianmultiply sto_bp_reindex_datacartesianmultiply sto_bn_reindex_datacartesianmultiply sto_cp_reindex_datacartesianmultiply sto_cn_reindex_datacartesianmultiply. (((((scp_first_reindex_datacartesian) = 2 * (sto_ap_reindex_datacartesianmultiply) /\ (sto_an_reindex_datacartesianmultiply) = 0) \/ exists ge_signed_half_reindex_datacartesianmultiplyleft. (((scp_first_reindex_datacartesian) = 2 * ge_signed_half_reindex_datacartesianmultiplyleft + 1 /\ (sto_ap_reindex_datacartesianmultiply) = 0) /\ (sto_an_reindex_datacartesianmultiply) = S ge_signed_half_reindex_datacartesianmultiplyleft))) /\ ((((((scp_second_reindex_datacartesian) = 2 * (sto_bp_reindex_datacartesianmultiply) /\ (sto_bn_reindex_datacartesianmultiply) = 0) \/ exists ge_signed_half_reindex_datacartesianmultiplyright. (((scp_second_reindex_datacartesian) = 2 * ge_signed_half_reindex_datacartesianmultiplyright + 1 /\ (sto_bp_reindex_datacartesianmultiply) = 0) /\ (sto_bn_reindex_datacartesianmultiply) = S ge_signed_half_reindex_datacartesianmultiplyright))) /\ ((((((scp_value_reindex_datacartesian) = 2 * (sto_cp_reindex_datacartesianmultiply) /\ (sto_cn_reindex_datacartesianmultiply) = 0) \/ exists ge_signed_half_reindex_datacartesianmultiplyoutput. (((scp_value_reindex_datacartesian) = 2 * ge_signed_half_reindex_datacartesianmultiplyoutput + 1 /\ (sto_cp_reindex_datacartesianmultiply) = 0) /\ (sto_cn_reindex_datacartesianmultiply) = S ge_signed_half_reindex_datacartesianmultiplyoutput))) /\ ((sto_ap_reindex_datacartesianmultiply * sto_bp_reindex_datacartesianmultiply + sto_an_reindex_datacartesianmultiply * sto_bn_reindex_datacartesianmultiply) + sto_cn_reindex_datacartesianmultiply = (sto_ap_reindex_datacartesianmultiply * sto_bn_reindex_datacartesianmultiply + sto_an_reindex_datacartesianmultiply * sto_bp_reindex_datacartesianmultiply) + sto_cp_reindex_datacartesianmultiply)))))))))))))) /\ (((((exists dst_positive_code_reindex_datatargettable dst_positive_scale_reindex_datatargettable dst_negative_code_reindex_datatargettable dst_negative_scale_reindex_datatargettable. (((Q) = (((((dst_positive_code_reindex_datatargettable) + (dst_positive_scale_reindex_datatargettable)) * S ((dst_positive_code_reindex_datatargettable) + (dst_positive_scale_reindex_datatargettable)) + ((dst_positive_scale_reindex_datatargettable) + (dst_positive_scale_reindex_datatargettable))) + (((dst_negative_code_reindex_datatargettable) + (dst_negative_scale_reindex_datatargettable)) * S ((dst_negative_code_reindex_datatargettable) + (dst_negative_scale_reindex_datatargettable)) + ((dst_negative_scale_reindex_datatargettable) + (dst_negative_scale_reindex_datatargettable)))) * S ((((dst_positive_code_reindex_datatargettable) + (dst_positive_scale_reindex_datatargettable)) * S ((dst_positive_code_reindex_datatargettable) + (dst_positive_scale_reindex_datatargettable)) + ((dst_positive_scale_reindex_datatargettable) + (dst_positive_scale_reindex_datatargettable))) + (((dst_negative_code_reindex_datatargettable) + (dst_negative_scale_reindex_datatargettable)) * S ((dst_negative_code_reindex_datatargettable) + (dst_negative_scale_reindex_datatargettable)) + ((dst_negative_scale_reindex_datatargettable) + (dst_negative_scale_reindex_datatargettable)))) + ((((dst_negative_code_reindex_datatargettable) + (dst_negative_scale_reindex_datatargettable)) * S ((dst_negative_code_reindex_datatargettable) + (dst_negative_scale_reindex_datatargettable)) + ((dst_negative_scale_reindex_datatargettable) + (dst_negative_scale_reindex_datatargettable))) + (((dst_negative_code_reindex_datatargettable) + (dst_negative_scale_reindex_datatargettable)) * S ((dst_negative_code_reindex_datatargettable) + (dst_negative_scale_reindex_datatargettable)) + ((dst_negative_scale_reindex_datatargettable) + (dst_negative_scale_reindex_datatargettable)))))) /\ (forall dst_index_reindex_datatargettable. (exists pvs_le_gap_reindex_datatargettabledomain. pvs_le_gap_reindex_datatargettabledomain + (dst_index_reindex_datatargettable) = ((m)*(n))) -> exists dst_positive_reindex_datatargettable dst_negative_reindex_datatargettable dst_value_reindex_datatargettable. ((((exists ff_h_pvs_reindex_datatargettableentrypositive. ff_h_pvs_reindex_datatargettableentrypositive + S (dst_positive_reindex_datatargettable) = S ((S (dst_index_reindex_datatargettable)) * dst_positive_scale_reindex_datatargettable)) /\ exists ff_q_pvs_reindex_datatargettableentrypositive. dst_positive_code_reindex_datatargettable = ff_q_pvs_reindex_datatargettableentrypositive * S ((S (dst_index_reindex_datatargettable)) * dst_positive_scale_reindex_datatargettable) + (dst_positive_reindex_datatargettable))) /\ (((((exists ff_h_pvs_reindex_datatargettableentrynegative. ff_h_pvs_reindex_datatargettableentrynegative + S (dst_negative_reindex_datatargettable) = S ((S (dst_index_reindex_datatargettable)) * dst_negative_scale_reindex_datatargettable)) /\ exists ff_q_pvs_reindex_datatargettableentrynegative. dst_negative_code_reindex_datatargettable = ff_q_pvs_reindex_datatargettableentrynegative * S ((S (dst_index_reindex_datatargettable)) * dst_negative_scale_reindex_datatargettable) + (dst_negative_reindex_datatargettable))) /\ (exists ge_balance_positive_reindex_datatargettableentryvalue ge_balance_negative_reindex_datatargettableentryvalue. (((((dst_value_reindex_datatargettable) = 2 * (ge_balance_positive_reindex_datatargettableentryvalue) /\ (ge_balance_negative_reindex_datatargettableentryvalue) = 0) \/ exists ge_signed_half_reindex_datatargettableentryvaluedecode. (((dst_value_reindex_datatargettable) = 2 * ge_signed_half_reindex_datatargettableentryvaluedecode + 1 /\ (ge_balance_positive_reindex_datatargettableentryvalue) = 0) /\ (ge_balance_negative_reindex_datatargettableentryvalue) = S ge_signed_half_reindex_datatargettableentryvaluedecode))) /\ ((dst_positive_reindex_datatargettable) + ge_balance_negative_reindex_datatargettableentryvalue = (dst_negative_reindex_datatargettable) + ge_balance_positive_reindex_datatargettableentryvalue))))))))) /\ (forall dc_index_reindex_datatarget dc_value_reindex_datatarget. (exists pvs_le_gap_reindex_datatargetdomain. pvs_le_gap_reindex_datatargetdomain + (dc_index_reindex_datatarget) = ((m)*(n))) -> (exists dst_positive_code_reindex_datatargetlookup dst_positive_scale_reindex_datatargetlookup dst_negative_code_reindex_datatargetlookup dst_negative_scale_reindex_datatargetlookup dst_positive_reindex_datatargetlookup dst_negative_reindex_datatargetlookup. (((Q) = (((((dst_positive_code_reindex_datatargetlookup) + (dst_positive_scale_reindex_datatargetlookup)) * S ((dst_positive_code_reindex_datatargetlookup) + (dst_positive_scale_reindex_datatargetlookup)) + ((dst_positive_scale_reindex_datatargetlookup) + (dst_positive_scale_reindex_datatargetlookup))) + (((dst_negative_code_reindex_datatargetlookup) + (dst_negative_scale_reindex_datatargetlookup)) * S ((dst_negative_code_reindex_datatargetlookup) + (dst_negative_scale_reindex_datatargetlookup)) + ((dst_negative_scale_reindex_datatargetlookup) + (dst_negative_scale_reindex_datatargetlookup)))) * S ((((dst_positive_code_reindex_datatargetlookup) + (dst_positive_scale_reindex_datatargetlookup)) * S ((dst_positive_code_reindex_datatargetlookup) + (dst_positive_scale_reindex_datatargetlookup)) + ((dst_positive_scale_reindex_datatargetlookup) + (dst_positive_scale_reindex_datatargetlookup))) + (((dst_negative_code_reindex_datatargetlookup) + (dst_negative_scale_reindex_datatargetlookup)) * S ((dst_negative_code_reindex_datatargetlookup) + (dst_negative_scale_reindex_datatargetlookup)) + ((dst_negative_scale_reindex_datatargetlookup) + (dst_negative_scale_reindex_datatargetlookup)))) + ((((dst_negative_code_reindex_datatargetlookup) + (dst_negative_scale_reindex_datatargetlookup)) * S ((dst_negative_code_reindex_datatargetlookup) + (dst_negative_scale_reindex_datatargetlookup)) + ((dst_negative_scale_reindex_datatargetlookup) + (dst_negative_scale_reindex_datatargetlookup))) + (((dst_negative_code_reindex_datatargetlookup) + (dst_negative_scale_reindex_datatargetlookup)) * S ((dst_negative_code_reindex_datatargetlookup) + (dst_negative_scale_reindex_datatargetlookup)) + ((dst_negative_scale_reindex_datatargetlookup) + (dst_negative_scale_reindex_datatargetlookup)))))) /\ (((((exists ff_h_pvs_reindex_datatargetlookuppositive. ff_h_pvs_reindex_datatargetlookuppositive + S (dst_positive_reindex_datatargetlookup) = S ((S (dc_index_reindex_datatarget)) * dst_positive_scale_reindex_datatargetlookup)) /\ exists ff_q_pvs_reindex_datatargetlookuppositive. dst_positive_code_reindex_datatargetlookup = ff_q_pvs_reindex_datatargetlookuppositive * S ((S (dc_index_reindex_datatarget)) * dst_positive_scale_reindex_datatargetlookup) + (dst_positive_reindex_datatargetlookup))) /\ (((((exists ff_h_pvs_reindex_datatargetlookupnegative. ff_h_pvs_reindex_datatargetlookupnegative + S (dst_negative_reindex_datatargetlookup) = S ((S (dc_index_reindex_datatarget)) * dst_negative_scale_reindex_datatargetlookup)) /\ exists ff_q_pvs_reindex_datatargetlookupnegative. dst_negative_code_reindex_datatargetlookup = ff_q_pvs_reindex_datatargetlookupnegative * S ((S (dc_index_reindex_datatarget)) * dst_negative_scale_reindex_datatargetlookup) + (dst_negative_reindex_datatargetlookup))) /\ (exists ge_balance_positive_reindex_datatargetlookupvalue ge_balance_negative_reindex_datatargetlookupvalue. (((((dc_value_reindex_datatarget) = 2 * (ge_balance_positive_reindex_datatargetlookupvalue) /\ (ge_balance_negative_reindex_datatargetlookupvalue) = 0) \/ exists ge_signed_half_reindex_datatargetlookupvaluedecode. (((dc_value_reindex_datatarget) = 2 * ge_signed_half_reindex_datatargetlookupvaluedecode + 1 /\ (ge_balance_positive_reindex_datatargetlookupvalue) = 0) /\ (ge_balance_negative_reindex_datatargetlookupvalue) = S ge_signed_half_reindex_datatargetlookupvaluedecode))) /\ ((dst_positive_reindex_datatargetlookup) + ge_balance_negative_reindex_datatargetlookupvalue = (dst_negative_reindex_datatargetlookup) + ge_balance_positive_reindex_datatargetlookupvalue))))))))) -> ((((~((dc_index_reindex_datatarget)=0)) /\ (exists dc_quotient_reindex_datatargetentry dc_left_reindex_datatargetentry dc_right_reindex_datatargetentry. ((((m)*(n))=(dc_index_reindex_datatarget)*dc_quotient_reindex_datatargetentry) /\ (((exists dst_positive_code_reindex_datatargetentryleft dst_positive_scale_reindex_datatargetentryleft dst_negative_code_reindex_datatargetentryleft dst_negative_scale_reindex_datatargetentryleft dst_positive_reindex_datatargetentryleft dst_negative_reindex_datatargetentryleft. (((F) = (((((dst_positive_code_reindex_datatargetentryleft) + (dst_positive_scale_reindex_datatargetentryleft)) * S ((dst_positive_code_reindex_datatargetentryleft) + (dst_positive_scale_reindex_datatargetentryleft)) + ((dst_positive_scale_reindex_datatargetentryleft) + (dst_positive_scale_reindex_datatargetentryleft))) + (((dst_negative_code_reindex_datatargetentryleft) + (dst_negative_scale_reindex_datatargetentryleft)) * S ((dst_negative_code_reindex_datatargetentryleft) + (dst_negative_scale_reindex_datatargetentryleft)) + ((dst_negative_scale_reindex_datatargetentryleft) + (dst_negative_scale_reindex_datatargetentryleft)))) * S ((((dst_positive_code_reindex_datatargetentryleft) + (dst_positive_scale_reindex_datatargetentryleft)) * S ((dst_positive_code_reindex_datatargetentryleft) + (dst_positive_scale_reindex_datatargetentryleft)) + ((dst_positive_scale_reindex_datatargetentryleft) + (dst_positive_scale_reindex_datatargetentryleft))) + (((dst_negative_code_reindex_datatargetentryleft) + (dst_negative_scale_reindex_datatargetentryleft)) * S ((dst_negative_code_reindex_datatargetentryleft) + (dst_negative_scale_reindex_datatargetentryleft)) + ((dst_negative_scale_reindex_datatargetentryleft) + (dst_negative_scale_reindex_datatargetentryleft)))) + ((((dst_negative_code_reindex_datatargetentryleft) + (dst_negative_scale_reindex_datatargetentryleft)) * S ((dst_negative_code_reindex_datatargetentryleft) + (dst_negative_scale_reindex_datatargetentryleft)) + ((dst_negative_scale_reindex_datatargetentryleft) + (dst_negative_scale_reindex_datatargetentryleft))) + (((dst_negative_code_reindex_datatargetentryleft) + (dst_negative_scale_reindex_datatargetentryleft)) * S ((dst_negative_code_reindex_datatargetentryleft) + (dst_negative_scale_reindex_datatargetentryleft)) + ((dst_negative_scale_reindex_datatargetentryleft) + (dst_negative_scale_reindex_datatargetentryleft)))))) /\ (((((exists ff_h_pvs_reindex_datatargetentryleftpositive. ff_h_pvs_reindex_datatargetentryleftpositive + S (dst_positive_reindex_datatargetentryleft) = S ((S (dc_index_reindex_datatarget)) * dst_positive_scale_reindex_datatargetentryleft)) /\ exists ff_q_pvs_reindex_datatargetentryleftpositive. dst_positive_code_reindex_datatargetentryleft = ff_q_pvs_reindex_datatargetentryleftpositive * S ((S (dc_index_reindex_datatarget)) * dst_positive_scale_reindex_datatargetentryleft) + (dst_positive_reindex_datatargetentryleft))) /\ (((((exists ff_h_pvs_reindex_datatargetentryleftnegative. ff_h_pvs_reindex_datatargetentryleftnegative + S (dst_negative_reindex_datatargetentryleft) = S ((S (dc_index_reindex_datatarget)) * dst_negative_scale_reindex_datatargetentryleft)) /\ exists ff_q_pvs_reindex_datatargetentryleftnegative. dst_negative_code_reindex_datatargetentryleft = ff_q_pvs_reindex_datatargetentryleftnegative * S ((S (dc_index_reindex_datatarget)) * dst_negative_scale_reindex_datatargetentryleft) + (dst_negative_reindex_datatargetentryleft))) /\ (exists ge_balance_positive_reindex_datatargetentryleftvalue ge_balance_negative_reindex_datatargetentryleftvalue. (((((dc_left_reindex_datatargetentry) = 2 * (ge_balance_positive_reindex_datatargetentryleftvalue) /\ (ge_balance_negative_reindex_datatargetentryleftvalue) = 0) \/ exists ge_signed_half_reindex_datatargetentryleftvaluedecode. (((dc_left_reindex_datatargetentry) = 2 * ge_signed_half_reindex_datatargetentryleftvaluedecode + 1 /\ (ge_balance_positive_reindex_datatargetentryleftvalue) = 0) /\ (ge_balance_negative_reindex_datatargetentryleftvalue) = S ge_signed_half_reindex_datatargetentryleftvaluedecode))) /\ ((dst_positive_reindex_datatargetentryleft) + ge_balance_negative_reindex_datatargetentryleftvalue = (dst_negative_reindex_datatargetentryleft) + ge_balance_positive_reindex_datatargetentryleftvalue))))))))) /\ (((exists dst_positive_code_reindex_datatargetentryright dst_positive_scale_reindex_datatargetentryright dst_negative_code_reindex_datatargetentryright dst_negative_scale_reindex_datatargetentryright dst_positive_reindex_datatargetentryright dst_negative_reindex_datatargetentryright. (((G) = (((((dst_positive_code_reindex_datatargetentryright) + (dst_positive_scale_reindex_datatargetentryright)) * S ((dst_positive_code_reindex_datatargetentryright) + (dst_positive_scale_reindex_datatargetentryright)) + ((dst_positive_scale_reindex_datatargetentryright) + (dst_positive_scale_reindex_datatargetentryright))) + (((dst_negative_code_reindex_datatargetentryright) + (dst_negative_scale_reindex_datatargetentryright)) * S ((dst_negative_code_reindex_datatargetentryright) + (dst_negative_scale_reindex_datatargetentryright)) + ((dst_negative_scale_reindex_datatargetentryright) + (dst_negative_scale_reindex_datatargetentryright)))) * S ((((dst_positive_code_reindex_datatargetentryright) + (dst_positive_scale_reindex_datatargetentryright)) * S ((dst_positive_code_reindex_datatargetentryright) + (dst_positive_scale_reindex_datatargetentryright)) + ((dst_positive_scale_reindex_datatargetentryright) + (dst_positive_scale_reindex_datatargetentryright))) + (((dst_negative_code_reindex_datatargetentryright) + (dst_negative_scale_reindex_datatargetentryright)) * S ((dst_negative_code_reindex_datatargetentryright) + (dst_negative_scale_reindex_datatargetentryright)) + ((dst_negative_scale_reindex_datatargetentryright) + (dst_negative_scale_reindex_datatargetentryright)))) + ((((dst_negative_code_reindex_datatargetentryright) + (dst_negative_scale_reindex_datatargetentryright)) * S ((dst_negative_code_reindex_datatargetentryright) + (dst_negative_scale_reindex_datatargetentryright)) + ((dst_negative_scale_reindex_datatargetentryright) + (dst_negative_scale_reindex_datatargetentryright))) + (((dst_negative_code_reindex_datatargetentryright) + (dst_negative_scale_reindex_datatargetentryright)) * S ((dst_negative_code_reindex_datatargetentryright) + (dst_negative_scale_reindex_datatargetentryright)) + ((dst_negative_scale_reindex_datatargetentryright) + (dst_negative_scale_reindex_datatargetentryright)))))) /\ (((((exists ff_h_pvs_reindex_datatargetentryrightpositive. ff_h_pvs_reindex_datatargetentryrightpositive + S (dst_positive_reindex_datatargetentryright) = S ((S (dc_quotient_reindex_datatargetentry)) * dst_positive_scale_reindex_datatargetentryright)) /\ exists ff_q_pvs_reindex_datatargetentryrightpositive. dst_positive_code_reindex_datatargetentryright = ff_q_pvs_reindex_datatargetentryrightpositive * S ((S (dc_quotient_reindex_datatargetentry)) * dst_positive_scale_reindex_datatargetentryright) + (dst_positive_reindex_datatargetentryright))) /\ (((((exists ff_h_pvs_reindex_datatargetentryrightnegative. ff_h_pvs_reindex_datatargetentryrightnegative + S (dst_negative_reindex_datatargetentryright) = S ((S (dc_quotient_reindex_datatargetentry)) * dst_negative_scale_reindex_datatargetentryright)) /\ exists ff_q_pvs_reindex_datatargetentryrightnegative. dst_negative_code_reindex_datatargetentryright = ff_q_pvs_reindex_datatargetentryrightnegative * S ((S (dc_quotient_reindex_datatargetentry)) * dst_negative_scale_reindex_datatargetentryright) + (dst_negative_reindex_datatargetentryright))) /\ (exists ge_balance_positive_reindex_datatargetentryrightvalue ge_balance_negative_reindex_datatargetentryrightvalue. (((((dc_right_reindex_datatargetentry) = 2 * (ge_balance_positive_reindex_datatargetentryrightvalue) /\ (ge_balance_negative_reindex_datatargetentryrightvalue) = 0) \/ exists ge_signed_half_reindex_datatargetentryrightvaluedecode. (((dc_right_reindex_datatargetentry) = 2 * ge_signed_half_reindex_datatargetentryrightvaluedecode + 1 /\ (ge_balance_positive_reindex_datatargetentryrightvalue) = 0) /\ (ge_balance_negative_reindex_datatargetentryrightvalue) = S ge_signed_half_reindex_datatargetentryrightvaluedecode))) /\ ((dst_positive_reindex_datatargetentryright) + ge_balance_negative_reindex_datatargetentryrightvalue = (dst_negative_reindex_datatargetentryright) + ge_balance_positive_reindex_datatargetentryrightvalue))))))))) /\ (exists sto_ap_reindex_datatargetentryproduct sto_an_reindex_datatargetentryproduct sto_bp_reindex_datatargetentryproduct sto_bn_reindex_datatargetentryproduct sto_cp_reindex_datatargetentryproduct sto_cn_reindex_datatargetentryproduct. (((((dc_left_reindex_datatargetentry) = 2 * (sto_ap_reindex_datatargetentryproduct) /\ (sto_an_reindex_datatargetentryproduct) = 0) \/ exists ge_signed_half_reindex_datatargetentryproductleft. (((dc_left_reindex_datatargetentry) = 2 * ge_signed_half_reindex_datatargetentryproductleft + 1 /\ (sto_ap_reindex_datatargetentryproduct) = 0) /\ (sto_an_reindex_datatargetentryproduct) = S ge_signed_half_reindex_datatargetentryproductleft))) /\ ((((((dc_right_reindex_datatargetentry) = 2 * (sto_bp_reindex_datatargetentryproduct) /\ (sto_bn_reindex_datatargetentryproduct) = 0) \/ exists ge_signed_half_reindex_datatargetentryproductright. (((dc_right_reindex_datatargetentry) = 2 * ge_signed_half_reindex_datatargetentryproductright + 1 /\ (sto_bp_reindex_datatargetentryproduct) = 0) /\ (sto_bn_reindex_datatargetentryproduct) = S ge_signed_half_reindex_datatargetentryproductright))) /\ ((((((dc_value_reindex_datatarget) = 2 * (sto_cp_reindex_datatargetentryproduct) /\ (sto_cn_reindex_datatargetentryproduct) = 0) \/ exists ge_signed_half_reindex_datatargetentryproductoutput. (((dc_value_reindex_datatarget) = 2 * ge_signed_half_reindex_datatargetentryproductoutput + 1 /\ (sto_cp_reindex_datatargetentryproduct) = 0) /\ (sto_cn_reindex_datatargetentryproduct) = S ge_signed_half_reindex_datatargetentryproductoutput))) /\ ((sto_ap_reindex_datatargetentryproduct * sto_bp_reindex_datatargetentryproduct + sto_an_reindex_datatargetentryproduct * sto_bn_reindex_datatargetentryproduct) + sto_cn_reindex_datatargetentryproduct = (sto_ap_reindex_datatargetentryproduct * sto_bn_reindex_datatargetentryproduct + sto_an_reindex_datatargetentryproduct * sto_bp_reindex_datatargetentryproduct) + sto_cp_reindex_datatargetentryproduct))))))))))))))) \/ ((((dc_index_reindex_datatarget)=0 \/ ~(exists pvs_factor_reindex_datatargetentrynondivisor. ((m)*(n)) = (dc_index_reindex_datatarget) * pvs_factor_reindex_datatargetentrynondivisor)) /\ ((dc_value_reindex_datatarget)=0))))))) /\ (((~((S (n))=0)) /\ (forall dpi_index_reindex_datamap dpi_row_reindex_datamap dpi_column_reindex_datamap. (exists pvs_gap_reindex_datamapwindow. pvs_gap_reindex_datamapwindow + S (dpi_index_reindex_datamap) = ((S (m))*(S (n)))) -> (exists pvs_gap_reindex_datamapremainder. pvs_gap_reindex_datamapremainder + S (dpi_column_reindex_datamap) = (S (n))) -> (dpi_index_reindex_datamap)=(S (n))*(dpi_row_reindex_datamap)+(dpi_column_reindex_datamap) -> (((exists ff_h_pvs_reindex_datamapvalue. ff_h_pvs_reindex_datamapvalue + S ((dpi_row_reindex_datamap)*(dpi_column_reindex_datamap)) = S ((S (dpi_index_reindex_datamap)) * s)) /\ exists ff_q_pvs_reindex_datamapvalue. r = ff_q_pvs_reindex_datamapvalue * S ((S (dpi_index_reindex_datamap)) * s) + ((dpi_row_reindex_datamap)*(dpi_column_reindex_datamap))))))))))))))))))))))))))) -> (((exists dst_positive_code_reindex_resultsource_table dst_positive_scale_reindex_resultsource_table dst_negative_code_reindex_resultsource_table dst_negative_scale_reindex_resultsource_table. (((T) = (((((dst_positive_code_reindex_resultsource_table) + (dst_positive_scale_reindex_resultsource_table)) * S ((dst_positive_code_reindex_resultsource_table) + (dst_positive_scale_reindex_resultsource_table)) + ((dst_positive_scale_reindex_resultsource_table) + (dst_positive_scale_reindex_resultsource_table))) + (((dst_negative_code_reindex_resultsource_table) + (dst_negative_scale_reindex_resultsource_table)) * S ((dst_negative_code_reindex_resultsource_table) + (dst_negative_scale_reindex_resultsource_table)) + ((dst_negative_scale_reindex_resultsource_table) + (dst_negative_scale_reindex_resultsource_table)))) * S ((((dst_positive_code_reindex_resultsource_table) + (dst_positive_scale_reindex_resultsource_table)) * S ((dst_positive_code_reindex_resultsource_table) + (dst_positive_scale_reindex_resultsource_table)) + ((dst_positive_scale_reindex_resultsource_table) + (dst_positive_scale_reindex_resultsource_table))) + (((dst_negative_code_reindex_resultsource_table) + (dst_negative_scale_reindex_resultsource_table)) * S ((dst_negative_code_reindex_resultsource_table) + (dst_negative_scale_reindex_resultsource_table)) + ((dst_negative_scale_reindex_resultsource_table) + (dst_negative_scale_reindex_resultsource_table)))) + ((((dst_negative_code_reindex_resultsource_table) + (dst_negative_scale_reindex_resultsource_table)) * S ((dst_negative_code_reindex_resultsource_table) + (dst_negative_scale_reindex_resultsource_table)) + ((dst_negative_scale_reindex_resultsource_table) + (dst_negative_scale_reindex_resultsource_table))) + (((dst_negative_code_reindex_resultsource_table) + (dst_negative_scale_reindex_resultsource_table)) * S ((dst_negative_code_reindex_resultsource_table) + (dst_negative_scale_reindex_resultsource_table)) + ((dst_negative_scale_reindex_resultsource_table) + (dst_negative_scale_reindex_resultsource_table)))))) /\ (forall dst_index_reindex_resultsource_table. (exists pvs_le_gap_reindex_resultsource_tabledomain. pvs_le_gap_reindex_resultsource_tabledomain + (dst_index_reindex_resultsource_table) = (0)) -> exists dst_positive_reindex_resultsource_table dst_negative_reindex_resultsource_table dst_value_reindex_resultsource_table. ((((exists ff_h_pvs_reindex_resultsource_tableentrypositive. ff_h_pvs_reindex_resultsource_tableentrypositive + S (dst_positive_reindex_resultsource_table) = S ((S (dst_index_reindex_resultsource_table)) * dst_positive_scale_reindex_resultsource_table)) /\ exists ff_q_pvs_reindex_resultsource_tableentrypositive. dst_positive_code_reindex_resultsource_table = ff_q_pvs_reindex_resultsource_tableentrypositive * S ((S (dst_index_reindex_resultsource_table)) * dst_positive_scale_reindex_resultsource_table) + (dst_positive_reindex_resultsource_table))) /\ (((((exists ff_h_pvs_reindex_resultsource_tableentrynegative. ff_h_pvs_reindex_resultsource_tableentrynegative + S (dst_negative_reindex_resultsource_table) = S ((S (dst_index_reindex_resultsource_table)) * dst_negative_scale_reindex_resultsource_table)) /\ exists ff_q_pvs_reindex_resultsource_tableentrynegative. dst_negative_code_reindex_resultsource_table = ff_q_pvs_reindex_resultsource_tableentrynegative * S ((S (dst_index_reindex_resultsource_table)) * dst_negative_scale_reindex_resultsource_table) + (dst_negative_reindex_resultsource_table))) /\ (exists ge_balance_positive_reindex_resultsource_tableentryvalue ge_balance_negative_reindex_resultsource_tableentryvalue. (((((dst_value_reindex_resultsource_table) = 2 * (ge_balance_positive_reindex_resultsource_tableentryvalue) /\ (ge_balance_negative_reindex_resultsource_tableentryvalue) = 0) \/ exists ge_signed_half_reindex_resultsource_tableentryvaluedecode. (((dst_value_reindex_resultsource_table) = 2 * ge_signed_half_reindex_resultsource_tableentryvaluedecode + 1 /\ (ge_balance_positive_reindex_resultsource_tableentryvalue) = 0) /\ (ge_balance_negative_reindex_resultsource_tableentryvalue) = S ge_signed_half_reindex_resultsource_tableentryvaluedecode))) /\ ((dst_positive_reindex_resultsource_table) + ge_balance_negative_reindex_resultsource_tableentryvalue = (dst_negative_reindex_resultsource_table) + ge_balance_positive_reindex_resultsource_tableentryvalue))))))))) /\ (((exists dst_positive_code_reindex_resulttarget_table dst_positive_scale_reindex_resulttarget_table dst_negative_code_reindex_resulttarget_table dst_negative_scale_reindex_resulttarget_table. (((Q) = (((((dst_positive_code_reindex_resulttarget_table) + (dst_positive_scale_reindex_resulttarget_table)) * S ((dst_positive_code_reindex_resulttarget_table) + (dst_positive_scale_reindex_resulttarget_table)) + ((dst_positive_scale_reindex_resulttarget_table) + (dst_positive_scale_reindex_resulttarget_table))) + (((dst_negative_code_reindex_resulttarget_table) + (dst_negative_scale_reindex_resulttarget_table)) * S ((dst_negative_code_reindex_resulttarget_table) + (dst_negative_scale_reindex_resulttarget_table)) + ((dst_negative_scale_reindex_resulttarget_table) + (dst_negative_scale_reindex_resulttarget_table)))) * S ((((dst_positive_code_reindex_resulttarget_table) + (dst_positive_scale_reindex_resulttarget_table)) * S ((dst_positive_code_reindex_resulttarget_table) + (dst_positive_scale_reindex_resulttarget_table)) + ((dst_positive_scale_reindex_resulttarget_table) + (dst_positive_scale_reindex_resulttarget_table))) + (((dst_negative_code_reindex_resulttarget_table) + (dst_negative_scale_reindex_resulttarget_table)) * S ((dst_negative_code_reindex_resulttarget_table) + (dst_negative_scale_reindex_resulttarget_table)) + ((dst_negative_scale_reindex_resulttarget_table) + (dst_negative_scale_reindex_resulttarget_table)))) + ((((dst_negative_code_reindex_resulttarget_table) + (dst_negative_scale_reindex_resulttarget_table)) * S ((dst_negative_code_reindex_resulttarget_table) + (dst_negative_scale_reindex_resulttarget_table)) + ((dst_negative_scale_reindex_resulttarget_table) + (dst_negative_scale_reindex_resulttarget_table))) + (((dst_negative_code_reindex_resulttarget_table) + (dst_negative_scale_reindex_resulttarget_table)) * S ((dst_negative_code_reindex_resulttarget_table) + (dst_negative_scale_reindex_resulttarget_table)) + ((dst_negative_scale_reindex_resulttarget_table) + (dst_negative_scale_reindex_resulttarget_table)))))) /\ (forall dst_index_reindex_resulttarget_table. (exists pvs_le_gap_reindex_resulttarget_tabledomain. pvs_le_gap_reindex_resulttarget_tabledomain + (dst_index_reindex_resulttarget_table) = (0)) -> exists dst_positive_reindex_resulttarget_table dst_negative_reindex_resulttarget_table dst_value_reindex_resulttarget_table. ((((exists ff_h_pvs_reindex_resulttarget_tableentrypositive. ff_h_pvs_reindex_resulttarget_tableentrypositive + S (dst_positive_reindex_resulttarget_table) = S ((S (dst_index_reindex_resulttarget_table)) * dst_positive_scale_reindex_resulttarget_table)) /\ exists ff_q_pvs_reindex_resulttarget_tableentrypositive. dst_positive_code_reindex_resulttarget_table = ff_q_pvs_reindex_resulttarget_tableentrypositive * S ((S (dst_index_reindex_resulttarget_table)) * dst_positive_scale_reindex_resulttarget_table) + (dst_positive_reindex_resulttarget_table))) /\ (((((exists ff_h_pvs_reindex_resulttarget_tableentrynegative. ff_h_pvs_reindex_resulttarget_tableentrynegative + S (dst_negative_reindex_resulttarget_table) = S ((S (dst_index_reindex_resulttarget_table)) * dst_negative_scale_reindex_resulttarget_table)) /\ exists ff_q_pvs_reindex_resulttarget_tableentrynegative. dst_negative_code_reindex_resulttarget_table = ff_q_pvs_reindex_resulttarget_tableentrynegative * S ((S (dst_index_reindex_resulttarget_table)) * dst_negative_scale_reindex_resulttarget_table) + (dst_negative_reindex_resulttarget_table))) /\ (exists ge_balance_positive_reindex_resulttarget_tableentryvalue ge_balance_negative_reindex_resulttarget_tableentryvalue. (((((dst_value_reindex_resulttarget_table) = 2 * (ge_balance_positive_reindex_resulttarget_tableentryvalue) /\ (ge_balance_negative_reindex_resulttarget_tableentryvalue) = 0) \/ exists ge_signed_half_reindex_resulttarget_tableentryvaluedecode. (((dst_value_reindex_resulttarget_table) = 2 * ge_signed_half_reindex_resulttarget_tableentryvaluedecode + 1 /\ (ge_balance_positive_reindex_resulttarget_tableentryvalue) = 0) /\ (ge_balance_negative_reindex_resulttarget_tableentryvalue) = S ge_signed_half_reindex_resulttarget_tableentryvaluedecode))) /\ ((dst_positive_reindex_resulttarget_table) + ge_balance_negative_reindex_resulttarget_tableentryvalue = (dst_negative_reindex_resulttarget_table) + ge_balance_positive_reindex_resulttarget_tableentryvalue))))))))) /\ (((forall ssr_source_reindex_resultpreserve ssr_value_reindex_resultpreserve. (exists pvs_gap_reindex_resultpreservesource_bound. pvs_gap_reindex_resultpreservesource_bound + S (ssr_source_reindex_resultpreserve) = ((S (m))*(S (n)))) -> (exists dst_positive_code_reindex_resultpreservesource_value dst_positive_scale_reindex_resultpreservesource_value dst_negative_code_reindex_resultpreservesource_value dst_negative_scale_reindex_resultpreservesource_value dst_positive_reindex_resultpreservesource_value dst_negative_reindex_resultpreservesource_value. (((T) = (((((dst_positive_code_reindex_resultpreservesource_value) + (dst_positive_scale_reindex_resultpreservesource_value)) * S ((dst_positive_code_reindex_resultpreservesource_value) + (dst_positive_scale_reindex_resultpreservesource_value)) + ((dst_positive_scale_reindex_resultpreservesource_value) + (dst_positive_scale_reindex_resultpreservesource_value))) + (((dst_negative_code_reindex_resultpreservesource_value) + (dst_negative_scale_reindex_resultpreservesource_value)) * S ((dst_negative_code_reindex_resultpreservesource_value) + (dst_negative_scale_reindex_resultpreservesource_value)) + ((dst_negative_scale_reindex_resultpreservesource_value) + (dst_negative_scale_reindex_resultpreservesource_value)))) * S ((((dst_positive_code_reindex_resultpreservesource_value) + (dst_positive_scale_reindex_resultpreservesource_value)) * S ((dst_positive_code_reindex_resultpreservesource_value) + (dst_positive_scale_reindex_resultpreservesource_value)) + ((dst_positive_scale_reindex_resultpreservesource_value) + (dst_positive_scale_reindex_resultpreservesource_value))) + (((dst_negative_code_reindex_resultpreservesource_value) + (dst_negative_scale_reindex_resultpreservesource_value)) * S ((dst_negative_code_reindex_resultpreservesource_value) + (dst_negative_scale_reindex_resultpreservesource_value)) + ((dst_negative_scale_reindex_resultpreservesource_value) + (dst_negative_scale_reindex_resultpreservesource_value)))) + ((((dst_negative_code_reindex_resultpreservesource_value) + (dst_negative_scale_reindex_resultpreservesource_value)) * S ((dst_negative_code_reindex_resultpreservesource_value) + (dst_negative_scale_reindex_resultpreservesource_value)) + ((dst_negative_scale_reindex_resultpreservesource_value) + (dst_negative_scale_reindex_resultpreservesource_value))) + (((dst_negative_code_reindex_resultpreservesource_value) + (dst_negative_scale_reindex_resultpreservesource_value)) * S ((dst_negative_code_reindex_resultpreservesource_value) + (dst_negative_scale_reindex_resultpreservesource_value)) + ((dst_negative_scale_reindex_resultpreservesource_value) + (dst_negative_scale_reindex_resultpreservesource_value)))))) /\ (((((exists ff_h_pvs_reindex_resultpreservesource_valuepositive. ff_h_pvs_reindex_resultpreservesource_valuepositive + S (dst_positive_reindex_resultpreservesource_value) = S ((S (ssr_source_reindex_resultpreserve)) * dst_positive_scale_reindex_resultpreservesource_value)) /\ exists ff_q_pvs_reindex_resultpreservesource_valuepositive. dst_positive_code_reindex_resultpreservesource_value = ff_q_pvs_reindex_resultpreservesource_valuepositive * S ((S (ssr_source_reindex_resultpreserve)) * dst_positive_scale_reindex_resultpreservesource_value) + (dst_positive_reindex_resultpreservesource_value))) /\ (((((exists ff_h_pvs_reindex_resultpreservesource_valuenegative. ff_h_pvs_reindex_resultpreservesource_valuenegative + S (dst_negative_reindex_resultpreservesource_value) = S ((S (ssr_source_reindex_resultpreserve)) * dst_negative_scale_reindex_resultpreservesource_value)) /\ exists ff_q_pvs_reindex_resultpreservesource_valuenegative. dst_negative_code_reindex_resultpreservesource_value = ff_q_pvs_reindex_resultpreservesource_valuenegative * S ((S (ssr_source_reindex_resultpreserve)) * dst_negative_scale_reindex_resultpreservesource_value) + (dst_negative_reindex_resultpreservesource_value))) /\ (exists ge_balance_positive_reindex_resultpreservesource_valuevalue ge_balance_negative_reindex_resultpreservesource_valuevalue. (((((ssr_value_reindex_resultpreserve) = 2 * (ge_balance_positive_reindex_resultpreservesource_valuevalue) /\ (ge_balance_negative_reindex_resultpreservesource_valuevalue) = 0) \/ exists ge_signed_half_reindex_resultpreservesource_valuevaluedecode. (((ssr_value_reindex_resultpreserve) = 2 * ge_signed_half_reindex_resultpreservesource_valuevaluedecode + 1 /\ (ge_balance_positive_reindex_resultpreservesource_valuevalue) = 0) /\ (ge_balance_negative_reindex_resultpreservesource_valuevalue) = S ge_signed_half_reindex_resultpreservesource_valuevaluedecode))) /\ ((dst_positive_reindex_resultpreservesource_value) + ge_balance_negative_reindex_resultpreservesource_valuevalue = (dst_negative_reindex_resultpreservesource_value) + ge_balance_positive_reindex_resultpreservesource_valuevalue))))))))) -> ~(ssr_value_reindex_resultpreserve=0) -> exists ssr_target_reindex_resultpreserve. ((((exists ff_h_pvs_reindex_resultpreservemap. ff_h_pvs_reindex_resultpreservemap + S (ssr_target_reindex_resultpreserve) = S ((S (ssr_source_reindex_resultpreserve)) * s)) /\ exists ff_q_pvs_reindex_resultpreservemap. r = ff_q_pvs_reindex_resultpreservemap * S ((S (ssr_source_reindex_resultpreserve)) * s) + (ssr_target_reindex_resultpreserve))) /\ (((exists pvs_gap_reindex_resultpreservetarget_bound. pvs_gap_reindex_resultpreservetarget_bound + S (ssr_target_reindex_resultpreserve) = (S (m*n))) /\ (exists dst_positive_code_reindex_resultpreservetarget_value dst_positive_scale_reindex_resultpreservetarget_value dst_negative_code_reindex_resultpreservetarget_value dst_negative_scale_reindex_resultpreservetarget_value dst_positive_reindex_resultpreservetarget_value dst_negative_reindex_resultpreservetarget_value. (((Q) = (((((dst_positive_code_reindex_resultpreservetarget_value) + (dst_positive_scale_reindex_resultpreservetarget_value)) * S ((dst_positive_code_reindex_resultpreservetarget_value) + (dst_positive_scale_reindex_resultpreservetarget_value)) + ((dst_positive_scale_reindex_resultpreservetarget_value) + (dst_positive_scale_reindex_resultpreservetarget_value))) + (((dst_negative_code_reindex_resultpreservetarget_value) + (dst_negative_scale_reindex_resultpreservetarget_value)) * S ((dst_negative_code_reindex_resultpreservetarget_value) + (dst_negative_scale_reindex_resultpreservetarget_value)) + ((dst_negative_scale_reindex_resultpreservetarget_value) + (dst_negative_scale_reindex_resultpreservetarget_value)))) * S ((((dst_positive_code_reindex_resultpreservetarget_value) + (dst_positive_scale_reindex_resultpreservetarget_value)) * S ((dst_positive_code_reindex_resultpreservetarget_value) + (dst_positive_scale_reindex_resultpreservetarget_value)) + ((dst_positive_scale_reindex_resultpreservetarget_value) + (dst_positive_scale_reindex_resultpreservetarget_value))) + (((dst_negative_code_reindex_resultpreservetarget_value) + (dst_negative_scale_reindex_resultpreservetarget_value)) * S ((dst_negative_code_reindex_resultpreservetarget_value) + (dst_negative_scale_reindex_resultpreservetarget_value)) + ((dst_negative_scale_reindex_resultpreservetarget_value) + (dst_negative_scale_reindex_resultpreservetarget_value)))) + ((((dst_negative_code_reindex_resultpreservetarget_value) + (dst_negative_scale_reindex_resultpreservetarget_value)) * S ((dst_negative_code_reindex_resultpreservetarget_value) + (dst_negative_scale_reindex_resultpreservetarget_value)) + ((dst_negative_scale_reindex_resultpreservetarget_value) + (dst_negative_scale_reindex_resultpreservetarget_value))) + (((dst_negative_code_reindex_resultpreservetarget_value) + (dst_negative_scale_reindex_resultpreservetarget_value)) * S ((dst_negative_code_reindex_resultpreservetarget_value) + (dst_negative_scale_reindex_resultpreservetarget_value)) + ((dst_negative_scale_reindex_resultpreservetarget_value) + (dst_negative_scale_reindex_resultpreservetarget_value)))))) /\ (((((exists ff_h_pvs_reindex_resultpreservetarget_valuepositive. ff_h_pvs_reindex_resultpreservetarget_valuepositive + S (dst_positive_reindex_resultpreservetarget_value) = S ((S (ssr_target_reindex_resultpreserve)) * dst_positive_scale_reindex_resultpreservetarget_value)) /\ exists ff_q_pvs_reindex_resultpreservetarget_valuepositive. dst_positive_code_reindex_resultpreservetarget_value = ff_q_pvs_reindex_resultpreservetarget_valuepositive * S ((S (ssr_target_reindex_resultpreserve)) * dst_positive_scale_reindex_resultpreservetarget_value) + (dst_positive_reindex_resultpreservetarget_value))) /\ (((((exists ff_h_pvs_reindex_resultpreservetarget_valuenegative. ff_h_pvs_reindex_resultpreservetarget_valuenegative + S (dst_negative_reindex_resultpreservetarget_value) = S ((S (ssr_target_reindex_resultpreserve)) * dst_negative_scale_reindex_resultpreservetarget_value)) /\ exists ff_q_pvs_reindex_resultpreservetarget_valuenegative. dst_negative_code_reindex_resultpreservetarget_value = ff_q_pvs_reindex_resultpreservetarget_valuenegative * S ((S (ssr_target_reindex_resultpreserve)) * dst_negative_scale_reindex_resultpreservetarget_value) + (dst_negative_reindex_resultpreservetarget_value))) /\ (exists ge_balance_positive_reindex_resultpreservetarget_valuevalue ge_balance_negative_reindex_resultpreservetarget_valuevalue. (((((ssr_value_reindex_resultpreserve) = 2 * (ge_balance_positive_reindex_resultpreservetarget_valuevalue) /\ (ge_balance_negative_reindex_resultpreservetarget_valuevalue) = 0) \/ exists ge_signed_half_reindex_resultpreservetarget_valuevaluedecode. (((ssr_value_reindex_resultpreserve) = 2 * ge_signed_half_reindex_resultpreservetarget_valuevaluedecode + 1 /\ (ge_balance_positive_reindex_resultpreservetarget_valuevalue) = 0) /\ (ge_balance_negative_reindex_resultpreservetarget_valuevalue) = S ge_signed_half_reindex_resultpreservetarget_valuevaluedecode))) /\ ((dst_positive_reindex_resultpreservetarget_value) + ge_balance_negative_reindex_resultpreservetarget_valuevalue = (dst_negative_reindex_resultpreservetarget_value) + ge_balance_positive_reindex_resultpreservetarget_valuevalue))))))))))))) /\ (((forall ssr_first_reindex_resultinjective ssr_second_reindex_resultinjective ssr_image_reindex_resultinjective ssr_a_reindex_resultinjective ssr_b_reindex_resultinjective. (exists pvs_gap_reindex_resultinjectivefirst_bound. pvs_gap_reindex_resultinjectivefirst_bound + S (ssr_first_reindex_resultinjective) = ((S (m))*(S (n)))) -> (exists pvs_gap_reindex_resultinjectivesecond_bound. pvs_gap_reindex_resultinjectivesecond_bound + S (ssr_second_reindex_resultinjective) = ((S (m))*(S (n)))) -> (exists dst_positive_code_reindex_resultinjectivefirst_value dst_positive_scale_reindex_resultinjectivefirst_value dst_negative_code_reindex_resultinjectivefirst_value dst_negative_scale_reindex_resultinjectivefirst_value dst_positive_reindex_resultinjectivefirst_value dst_negative_reindex_resultinjectivefirst_value. (((T) = (((((dst_positive_code_reindex_resultinjectivefirst_value) + (dst_positive_scale_reindex_resultinjectivefirst_value)) * S ((dst_positive_code_reindex_resultinjectivefirst_value) + (dst_positive_scale_reindex_resultinjectivefirst_value)) + ((dst_positive_scale_reindex_resultinjectivefirst_value) + (dst_positive_scale_reindex_resultinjectivefirst_value))) + (((dst_negative_code_reindex_resultinjectivefirst_value) + (dst_negative_scale_reindex_resultinjectivefirst_value)) * S ((dst_negative_code_reindex_resultinjectivefirst_value) + (dst_negative_scale_reindex_resultinjectivefirst_value)) + ((dst_negative_scale_reindex_resultinjectivefirst_value) + (dst_negative_scale_reindex_resultinjectivefirst_value)))) * S ((((dst_positive_code_reindex_resultinjectivefirst_value) + (dst_positive_scale_reindex_resultinjectivefirst_value)) * S ((dst_positive_code_reindex_resultinjectivefirst_value) + (dst_positive_scale_reindex_resultinjectivefirst_value)) + ((dst_positive_scale_reindex_resultinjectivefirst_value) + (dst_positive_scale_reindex_resultinjectivefirst_value))) + (((dst_negative_code_reindex_resultinjectivefirst_value) + (dst_negative_scale_reindex_resultinjectivefirst_value)) * S ((dst_negative_code_reindex_resultinjectivefirst_value) + (dst_negative_scale_reindex_resultinjectivefirst_value)) + ((dst_negative_scale_reindex_resultinjectivefirst_value) + (dst_negative_scale_reindex_resultinjectivefirst_value)))) + ((((dst_negative_code_reindex_resultinjectivefirst_value) + (dst_negative_scale_reindex_resultinjectivefirst_value)) * S ((dst_negative_code_reindex_resultinjectivefirst_value) + (dst_negative_scale_reindex_resultinjectivefirst_value)) + ((dst_negative_scale_reindex_resultinjectivefirst_value) + (dst_negative_scale_reindex_resultinjectivefirst_value))) + (((dst_negative_code_reindex_resultinjectivefirst_value) + (dst_negative_scale_reindex_resultinjectivefirst_value)) * S ((dst_negative_code_reindex_resultinjectivefirst_value) + (dst_negative_scale_reindex_resultinjectivefirst_value)) + ((dst_negative_scale_reindex_resultinjectivefirst_value) + (dst_negative_scale_reindex_resultinjectivefirst_value)))))) /\ (((((exists ff_h_pvs_reindex_resultinjectivefirst_valuepositive. ff_h_pvs_reindex_resultinjectivefirst_valuepositive + S (dst_positive_reindex_resultinjectivefirst_value) = S ((S (ssr_first_reindex_resultinjective)) * dst_positive_scale_reindex_resultinjectivefirst_value)) /\ exists ff_q_pvs_reindex_resultinjectivefirst_valuepositive. dst_positive_code_reindex_resultinjectivefirst_value = ff_q_pvs_reindex_resultinjectivefirst_valuepositive * S ((S (ssr_first_reindex_resultinjective)) * dst_positive_scale_reindex_resultinjectivefirst_value) + (dst_positive_reindex_resultinjectivefirst_value))) /\ (((((exists ff_h_pvs_reindex_resultinjectivefirst_valuenegative. ff_h_pvs_reindex_resultinjectivefirst_valuenegative + S (dst_negative_reindex_resultinjectivefirst_value) = S ((S (ssr_first_reindex_resultinjective)) * dst_negative_scale_reindex_resultinjectivefirst_value)) /\ exists ff_q_pvs_reindex_resultinjectivefirst_valuenegative. dst_negative_code_reindex_resultinjectivefirst_value = ff_q_pvs_reindex_resultinjectivefirst_valuenegative * S ((S (ssr_first_reindex_resultinjective)) * dst_negative_scale_reindex_resultinjectivefirst_value) + (dst_negative_reindex_resultinjectivefirst_value))) /\ (exists ge_balance_positive_reindex_resultinjectivefirst_valuevalue ge_balance_negative_reindex_resultinjectivefirst_valuevalue. (((((ssr_a_reindex_resultinjective) = 2 * (ge_balance_positive_reindex_resultinjectivefirst_valuevalue) /\ (ge_balance_negative_reindex_resultinjectivefirst_valuevalue) = 0) \/ exists ge_signed_half_reindex_resultinjectivefirst_valuevaluedecode. (((ssr_a_reindex_resultinjective) = 2 * ge_signed_half_reindex_resultinjectivefirst_valuevaluedecode + 1 /\ (ge_balance_positive_reindex_resultinjectivefirst_valuevalue) = 0) /\ (ge_balance_negative_reindex_resultinjectivefirst_valuevalue) = S ge_signed_half_reindex_resultinjectivefirst_valuevaluedecode))) /\ ((dst_positive_reindex_resultinjectivefirst_value) + ge_balance_negative_reindex_resultinjectivefirst_valuevalue = (dst_negative_reindex_resultinjectivefirst_value) + ge_balance_positive_reindex_resultinjectivefirst_valuevalue))))))))) -> ~(ssr_a_reindex_resultinjective=0) -> (exists dst_positive_code_reindex_resultinjectivesecond_value dst_positive_scale_reindex_resultinjectivesecond_value dst_negative_code_reindex_resultinjectivesecond_value dst_negative_scale_reindex_resultinjectivesecond_value dst_positive_reindex_resultinjectivesecond_value dst_negative_reindex_resultinjectivesecond_value. (((T) = (((((dst_positive_code_reindex_resultinjectivesecond_value) + (dst_positive_scale_reindex_resultinjectivesecond_value)) * S ((dst_positive_code_reindex_resultinjectivesecond_value) + (dst_positive_scale_reindex_resultinjectivesecond_value)) + ((dst_positive_scale_reindex_resultinjectivesecond_value) + (dst_positive_scale_reindex_resultinjectivesecond_value))) + (((dst_negative_code_reindex_resultinjectivesecond_value) + (dst_negative_scale_reindex_resultinjectivesecond_value)) * S ((dst_negative_code_reindex_resultinjectivesecond_value) + (dst_negative_scale_reindex_resultinjectivesecond_value)) + ((dst_negative_scale_reindex_resultinjectivesecond_value) + (dst_negative_scale_reindex_resultinjectivesecond_value)))) * S ((((dst_positive_code_reindex_resultinjectivesecond_value) + (dst_positive_scale_reindex_resultinjectivesecond_value)) * S ((dst_positive_code_reindex_resultinjectivesecond_value) + (dst_positive_scale_reindex_resultinjectivesecond_value)) + ((dst_positive_scale_reindex_resultinjectivesecond_value) + (dst_positive_scale_reindex_resultinjectivesecond_value))) + (((dst_negative_code_reindex_resultinjectivesecond_value) + (dst_negative_scale_reindex_resultinjectivesecond_value)) * S ((dst_negative_code_reindex_resultinjectivesecond_value) + (dst_negative_scale_reindex_resultinjectivesecond_value)) + ((dst_negative_scale_reindex_resultinjectivesecond_value) + (dst_negative_scale_reindex_resultinjectivesecond_value)))) + ((((dst_negative_code_reindex_resultinjectivesecond_value) + (dst_negative_scale_reindex_resultinjectivesecond_value)) * S ((dst_negative_code_reindex_resultinjectivesecond_value) + (dst_negative_scale_reindex_resultinjectivesecond_value)) + ((dst_negative_scale_reindex_resultinjectivesecond_value) + (dst_negative_scale_reindex_resultinjectivesecond_value))) + (((dst_negative_code_reindex_resultinjectivesecond_value) + (dst_negative_scale_reindex_resultinjectivesecond_value)) * S ((dst_negative_code_reindex_resultinjectivesecond_value) + (dst_negative_scale_reindex_resultinjectivesecond_value)) + ((dst_negative_scale_reindex_resultinjectivesecond_value) + (dst_negative_scale_reindex_resultinjectivesecond_value)))))) /\ (((((exists ff_h_pvs_reindex_resultinjectivesecond_valuepositive. ff_h_pvs_reindex_resultinjectivesecond_valuepositive + S (dst_positive_reindex_resultinjectivesecond_value) = S ((S (ssr_second_reindex_resultinjective)) * dst_positive_scale_reindex_resultinjectivesecond_value)) /\ exists ff_q_pvs_reindex_resultinjectivesecond_valuepositive. dst_positive_code_reindex_resultinjectivesecond_value = ff_q_pvs_reindex_resultinjectivesecond_valuepositive * S ((S (ssr_second_reindex_resultinjective)) * dst_positive_scale_reindex_resultinjectivesecond_value) + (dst_positive_reindex_resultinjectivesecond_value))) /\ (((((exists ff_h_pvs_reindex_resultinjectivesecond_valuenegative. ff_h_pvs_reindex_resultinjectivesecond_valuenegative + S (dst_negative_reindex_resultinjectivesecond_value) = S ((S (ssr_second_reindex_resultinjective)) * dst_negative_scale_reindex_resultinjectivesecond_value)) /\ exists ff_q_pvs_reindex_resultinjectivesecond_valuenegative. dst_negative_code_reindex_resultinjectivesecond_value = ff_q_pvs_reindex_resultinjectivesecond_valuenegative * S ((S (ssr_second_reindex_resultinjective)) * dst_negative_scale_reindex_resultinjectivesecond_value) + (dst_negative_reindex_resultinjectivesecond_value))) /\ (exists ge_balance_positive_reindex_resultinjectivesecond_valuevalue ge_balance_negative_reindex_resultinjectivesecond_valuevalue. (((((ssr_b_reindex_resultinjective) = 2 * (ge_balance_positive_reindex_resultinjectivesecond_valuevalue) /\ (ge_balance_negative_reindex_resultinjectivesecond_valuevalue) = 0) \/ exists ge_signed_half_reindex_resultinjectivesecond_valuevaluedecode. (((ssr_b_reindex_resultinjective) = 2 * ge_signed_half_reindex_resultinjectivesecond_valuevaluedecode + 1 /\ (ge_balance_positive_reindex_resultinjectivesecond_valuevalue) = 0) /\ (ge_balance_negative_reindex_resultinjectivesecond_valuevalue) = S ge_signed_half_reindex_resultinjectivesecond_valuevaluedecode))) /\ ((dst_positive_reindex_resultinjectivesecond_value) + ge_balance_negative_reindex_resultinjectivesecond_valuevalue = (dst_negative_reindex_resultinjectivesecond_value) + ge_balance_positive_reindex_resultinjectivesecond_valuevalue))))))))) -> ~(ssr_b_reindex_resultinjective=0) -> (((exists ff_h_pvs_reindex_resultinjectivefirst_map. ff_h_pvs_reindex_resultinjectivefirst_map + S (ssr_image_reindex_resultinjective) = S ((S (ssr_first_reindex_resultinjective)) * s)) /\ exists ff_q_pvs_reindex_resultinjectivefirst_map. r = ff_q_pvs_reindex_resultinjectivefirst_map * S ((S (ssr_first_reindex_resultinjective)) * s) + (ssr_image_reindex_resultinjective))) -> (((exists ff_h_pvs_reindex_resultinjectivesecond_map. ff_h_pvs_reindex_resultinjectivesecond_map + S (ssr_image_reindex_resultinjective) = S ((S (ssr_second_reindex_resultinjective)) * s)) /\ exists ff_q_pvs_reindex_resultinjectivesecond_map. r = ff_q_pvs_reindex_resultinjectivesecond_map * S ((S (ssr_second_reindex_resultinjective)) * s) + (ssr_image_reindex_resultinjective))) -> ssr_first_reindex_resultinjective=ssr_second_reindex_resultinjective) /\ (forall ssr_target_reindex_resultcover ssr_value_reindex_resultcover. (exists pvs_gap_reindex_resultcovertarget_bound. pvs_gap_reindex_resultcovertarget_bound + S (ssr_target_reindex_resultcover) = (S (m*n))) -> (exists dst_positive_code_reindex_resultcovertarget_value dst_positive_scale_reindex_resultcovertarget_value dst_negative_code_reindex_resultcovertarget_value dst_negative_scale_reindex_resultcovertarget_value dst_positive_reindex_resultcovertarget_value dst_negative_reindex_resultcovertarget_value. (((Q) = (((((dst_positive_code_reindex_resultcovertarget_value) + (dst_positive_scale_reindex_resultcovertarget_value)) * S ((dst_positive_code_reindex_resultcovertarget_value) + (dst_positive_scale_reindex_resultcovertarget_value)) + ((dst_positive_scale_reindex_resultcovertarget_value) + (dst_positive_scale_reindex_resultcovertarget_value))) + (((dst_negative_code_reindex_resultcovertarget_value) + (dst_negative_scale_reindex_resultcovertarget_value)) * S ((dst_negative_code_reindex_resultcovertarget_value) + (dst_negative_scale_reindex_resultcovertarget_value)) + ((dst_negative_scale_reindex_resultcovertarget_value) + (dst_negative_scale_reindex_resultcovertarget_value)))) * S ((((dst_positive_code_reindex_resultcovertarget_value) + (dst_positive_scale_reindex_resultcovertarget_value)) * S ((dst_positive_code_reindex_resultcovertarget_value) + (dst_positive_scale_reindex_resultcovertarget_value)) + ((dst_positive_scale_reindex_resultcovertarget_value) + (dst_positive_scale_reindex_resultcovertarget_value))) + (((dst_negative_code_reindex_resultcovertarget_value) + (dst_negative_scale_reindex_resultcovertarget_value)) * S ((dst_negative_code_reindex_resultcovertarget_value) + (dst_negative_scale_reindex_resultcovertarget_value)) + ((dst_negative_scale_reindex_resultcovertarget_value) + (dst_negative_scale_reindex_resultcovertarget_value)))) + ((((dst_negative_code_reindex_resultcovertarget_value) + (dst_negative_scale_reindex_resultcovertarget_value)) * S ((dst_negative_code_reindex_resultcovertarget_value) + (dst_negative_scale_reindex_resultcovertarget_value)) + ((dst_negative_scale_reindex_resultcovertarget_value) + (dst_negative_scale_reindex_resultcovertarget_value))) + (((dst_negative_code_reindex_resultcovertarget_value) + (dst_negative_scale_reindex_resultcovertarget_value)) * S ((dst_negative_code_reindex_resultcovertarget_value) + (dst_negative_scale_reindex_resultcovertarget_value)) + ((dst_negative_scale_reindex_resultcovertarget_value) + (dst_negative_scale_reindex_resultcovertarget_value)))))) /\ (((((exists ff_h_pvs_reindex_resultcovertarget_valuepositive. ff_h_pvs_reindex_resultcovertarget_valuepositive + S (dst_positive_reindex_resultcovertarget_value) = S ((S (ssr_target_reindex_resultcover)) * dst_positive_scale_reindex_resultcovertarget_value)) /\ exists ff_q_pvs_reindex_resultcovertarget_valuepositive. dst_positive_code_reindex_resultcovertarget_value = ff_q_pvs_reindex_resultcovertarget_valuepositive * S ((S (ssr_target_reindex_resultcover)) * dst_positive_scale_reindex_resultcovertarget_value) + (dst_positive_reindex_resultcovertarget_value))) /\ (((((exists ff_h_pvs_reindex_resultcovertarget_valuenegative. ff_h_pvs_reindex_resultcovertarget_valuenegative + S (dst_negative_reindex_resultcovertarget_value) = S ((S (ssr_target_reindex_resultcover)) * dst_negative_scale_reindex_resultcovertarget_value)) /\ exists ff_q_pvs_reindex_resultcovertarget_valuenegative. dst_negative_code_reindex_resultcovertarget_value = ff_q_pvs_reindex_resultcovertarget_valuenegative * S ((S (ssr_target_reindex_resultcover)) * dst_negative_scale_reindex_resultcovertarget_value) + (dst_negative_reindex_resultcovertarget_value))) /\ (exists ge_balance_positive_reindex_resultcovertarget_valuevalue ge_balance_negative_reindex_resultcovertarget_valuevalue. (((((ssr_value_reindex_resultcover) = 2 * (ge_balance_positive_reindex_resultcovertarget_valuevalue) /\ (ge_balance_negative_reindex_resultcovertarget_valuevalue) = 0) \/ exists ge_signed_half_reindex_resultcovertarget_valuevaluedecode. (((ssr_value_reindex_resultcover) = 2 * ge_signed_half_reindex_resultcovertarget_valuevaluedecode + 1 /\ (ge_balance_positive_reindex_resultcovertarget_valuevalue) = 0) /\ (ge_balance_negative_reindex_resultcovertarget_valuevalue) = S ge_signed_half_reindex_resultcovertarget_valuevaluedecode))) /\ ((dst_positive_reindex_resultcovertarget_value) + ge_balance_negative_reindex_resultcovertarget_valuevalue = (dst_negative_reindex_resultcovertarget_value) + ge_balance_positive_reindex_resultcovertarget_valuevalue))))))))) -> ~(ssr_value_reindex_resultcover=0) -> exists ssr_source_reindex_resultcover. ((exists pvs_gap_reindex_resultcoversource_bound. pvs_gap_reindex_resultcoversource_bound + S (ssr_source_reindex_resultcover) = ((S (m))*(S (n)))) /\ (((((exists ff_h_pvs_reindex_resultcovermap. ff_h_pvs_reindex_resultcovermap + S (ssr_target_reindex_resultcover) = S ((S (ssr_source_reindex_resultcover)) * s)) /\ exists ff_q_pvs_reindex_resultcovermap. r = ff_q_pvs_reindex_resultcovermap * S ((S (ssr_source_reindex_resultcover)) * s) + (ssr_target_reindex_resultcover))) /\ (exists dst_positive_code_reindex_resultcoversource_value dst_positive_scale_reindex_resultcoversource_value dst_negative_code_reindex_resultcoversource_value dst_negative_scale_reindex_resultcoversource_value dst_positive_reindex_resultcoversource_value dst_negative_reindex_resultcoversource_value. (((T) = (((((dst_positive_code_reindex_resultcoversource_value) + (dst_positive_scale_reindex_resultcoversource_value)) * S ((dst_positive_code_reindex_resultcoversource_value) + (dst_positive_scale_reindex_resultcoversource_value)) + ((dst_positive_scale_reindex_resultcoversource_value) + (dst_positive_scale_reindex_resultcoversource_value))) + (((dst_negative_code_reindex_resultcoversource_value) + (dst_negative_scale_reindex_resultcoversource_value)) * S ((dst_negative_code_reindex_resultcoversource_value) + (dst_negative_scale_reindex_resultcoversource_value)) + ((dst_negative_scale_reindex_resultcoversource_value) + (dst_negative_scale_reindex_resultcoversource_value)))) * S ((((dst_positive_code_reindex_resultcoversource_value) + (dst_positive_scale_reindex_resultcoversource_value)) * S ((dst_positive_code_reindex_resultcoversource_value) + (dst_positive_scale_reindex_resultcoversource_value)) + ((dst_positive_scale_reindex_resultcoversource_value) + (dst_positive_scale_reindex_resultcoversource_value))) + (((dst_negative_code_reindex_resultcoversource_value) + (dst_negative_scale_reindex_resultcoversource_value)) * S ((dst_negative_code_reindex_resultcoversource_value) + (dst_negative_scale_reindex_resultcoversource_value)) + ((dst_negative_scale_reindex_resultcoversource_value) + (dst_negative_scale_reindex_resultcoversource_value)))) + ((((dst_negative_code_reindex_resultcoversource_value) + (dst_negative_scale_reindex_resultcoversource_value)) * S ((dst_negative_code_reindex_resultcoversource_value) + (dst_negative_scale_reindex_resultcoversource_value)) + ((dst_negative_scale_reindex_resultcoversource_value) + (dst_negative_scale_reindex_resultcoversource_value))) + (((dst_negative_code_reindex_resultcoversource_value) + (dst_negative_scale_reindex_resultcoversource_value)) * S ((dst_negative_code_reindex_resultcoversource_value) + (dst_negative_scale_reindex_resultcoversource_value)) + ((dst_negative_scale_reindex_resultcoversource_value) + (dst_negative_scale_reindex_resultcoversource_value)))))) /\ (((((exists ff_h_pvs_reindex_resultcoversource_valuepositive. ff_h_pvs_reindex_resultcoversource_valuepositive + S (dst_positive_reindex_resultcoversource_value) = S ((S (ssr_source_reindex_resultcover)) * dst_positive_scale_reindex_resultcoversource_value)) /\ exists ff_q_pvs_reindex_resultcoversource_valuepositive. dst_positive_code_reindex_resultcoversource_value = ff_q_pvs_reindex_resultcoversource_valuepositive * S ((S (ssr_source_reindex_resultcover)) * dst_positive_scale_reindex_resultcoversource_value) + (dst_positive_reindex_resultcoversource_value))) /\ (((((exists ff_h_pvs_reindex_resultcoversource_valuenegative. ff_h_pvs_reindex_resultcoversource_valuenegative + S (dst_negative_reindex_resultcoversource_value) = S ((S (ssr_source_reindex_resultcover)) * dst_negative_scale_reindex_resultcoversource_value)) /\ exists ff_q_pvs_reindex_resultcoversource_valuenegative. dst_negative_code_reindex_resultcoversource_value = ff_q_pvs_reindex_resultcoversource_valuenegative * S ((S (ssr_source_reindex_resultcover)) * dst_negative_scale_reindex_resultcoversource_value) + (dst_negative_reindex_resultcoversource_value))) /\ (exists ge_balance_positive_reindex_resultcoversource_valuevalue ge_balance_negative_reindex_resultcoversource_valuevalue. (((((ssr_value_reindex_resultcover) = 2 * (ge_balance_positive_reindex_resultcoversource_valuevalue) /\ (ge_balance_negative_reindex_resultcoversource_valuevalue) = 0) \/ exists ge_signed_half_reindex_resultcoversource_valuevaluedecode. (((ssr_value_reindex_resultcover) = 2 * ge_signed_half_reindex_resultcoversource_valuevaluedecode + 1 /\ (ge_balance_positive_reindex_resultcoversource_valuevalue) = 0) /\ (ge_balance_negative_reindex_resultcoversource_valuevalue) = S ge_signed_half_reindex_resultcoversource_valuevaluedecode))) /\ ((dst_positive_reindex_resultcoversource_value) + ge_balance_negative_reindex_resultcoversource_valuevalue = (dst_negative_reindex_resultcoversource_value) + ge_balance_positive_reindex_resultcoversource_valuevalue)))))))))))))))))))))