dirichlet_coprime_grid_support_preserving

Exact expanded first-order arithmetic statement

forall N F G m n A B T Q r s. (((((~((N)=0)) /\ (((exists dst_positive_code_preserve_dataFtable dst_positive_scale_preserve_dataFtable dst_negative_code_preserve_dataFtable dst_negative_scale_preserve_dataFtable. (((F) = (((((dst_positive_code_preserve_dataFtable) + (dst_positive_scale_preserve_dataFtable)) * S ((dst_positive_code_preserve_dataFtable) + (dst_positive_scale_preserve_dataFtable)) + ((dst_positive_scale_preserve_dataFtable) + (dst_positive_scale_preserve_dataFtable))) + (((dst_negative_code_preserve_dataFtable) + (dst_negative_scale_preserve_dataFtable)) * S ((dst_negative_code_preserve_dataFtable) + (dst_negative_scale_preserve_dataFtable)) + ((dst_negative_scale_preserve_dataFtable) + (dst_negative_scale_preserve_dataFtable)))) * S ((((dst_positive_code_preserve_dataFtable) + (dst_positive_scale_preserve_dataFtable)) * S ((dst_positive_code_preserve_dataFtable) + (dst_positive_scale_preserve_dataFtable)) + ((dst_positive_scale_preserve_dataFtable) + (dst_positive_scale_preserve_dataFtable))) + (((dst_negative_code_preserve_dataFtable) + (dst_negative_scale_preserve_dataFtable)) * S ((dst_negative_code_preserve_dataFtable) + (dst_negative_scale_preserve_dataFtable)) + ((dst_negative_scale_preserve_dataFtable) + (dst_negative_scale_preserve_dataFtable)))) + ((((dst_negative_code_preserve_dataFtable) + (dst_negative_scale_preserve_dataFtable)) * S ((dst_negative_code_preserve_dataFtable) + (dst_negative_scale_preserve_dataFtable)) + ((dst_negative_scale_preserve_dataFtable) + (dst_negative_scale_preserve_dataFtable))) + (((dst_negative_code_preserve_dataFtable) + (dst_negative_scale_preserve_dataFtable)) * S ((dst_negative_code_preserve_dataFtable) + (dst_negative_scale_preserve_dataFtable)) + ((dst_negative_scale_preserve_dataFtable) + (dst_negative_scale_preserve_dataFtable)))))) /\ (forall dst_index_preserve_dataFtable. (exists pvs_le_gap_preserve_dataFtabledomain. pvs_le_gap_preserve_dataFtabledomain + (dst_index_preserve_dataFtable) = (N)) -> exists dst_positive_preserve_dataFtable dst_negative_preserve_dataFtable dst_value_preserve_dataFtable. ((((exists ff_h_pvs_preserve_dataFtableentrypositive. ff_h_pvs_preserve_dataFtableentrypositive + S (dst_positive_preserve_dataFtable) = S ((S (dst_index_preserve_dataFtable)) * dst_positive_scale_preserve_dataFtable)) /\ exists ff_q_pvs_preserve_dataFtableentrypositive. dst_positive_code_preserve_dataFtable = ff_q_pvs_preserve_dataFtableentrypositive * S ((S (dst_index_preserve_dataFtable)) * dst_positive_scale_preserve_dataFtable) + (dst_positive_preserve_dataFtable))) /\ (((((exists ff_h_pvs_preserve_dataFtableentrynegative. ff_h_pvs_preserve_dataFtableentrynegative + S (dst_negative_preserve_dataFtable) = S ((S (dst_index_preserve_dataFtable)) * dst_negative_scale_preserve_dataFtable)) /\ exists ff_q_pvs_preserve_dataFtableentrynegative. dst_negative_code_preserve_dataFtable = ff_q_pvs_preserve_dataFtableentrynegative * S ((S (dst_index_preserve_dataFtable)) * dst_negative_scale_preserve_dataFtable) + (dst_negative_preserve_dataFtable))) /\ (exists ge_balance_positive_preserve_dataFtableentryvalue ge_balance_negative_preserve_dataFtableentryvalue. (((((dst_value_preserve_dataFtable) = 2 * (ge_balance_positive_preserve_dataFtableentryvalue) /\ (ge_balance_negative_preserve_dataFtableentryvalue) = 0) \/ exists ge_signed_half_preserve_dataFtableentryvaluedecode. (((dst_value_preserve_dataFtable) = 2 * ge_signed_half_preserve_dataFtableentryvaluedecode + 1 /\ (ge_balance_positive_preserve_dataFtableentryvalue) = 0) /\ (ge_balance_negative_preserve_dataFtableentryvalue) = S ge_signed_half_preserve_dataFtableentryvaluedecode))) /\ ((dst_positive_preserve_dataFtable) + ge_balance_negative_preserve_dataFtableentryvalue = (dst_negative_preserve_dataFtable) + ge_balance_positive_preserve_dataFtableentryvalue))))))))) /\ (((exists dst_positive_code_preserve_dataFone dst_positive_scale_preserve_dataFone dst_negative_code_preserve_dataFone dst_negative_scale_preserve_dataFone dst_positive_preserve_dataFone dst_negative_preserve_dataFone. (((F) = (((((dst_positive_code_preserve_dataFone) + (dst_positive_scale_preserve_dataFone)) * S ((dst_positive_code_preserve_dataFone) + (dst_positive_scale_preserve_dataFone)) + ((dst_positive_scale_preserve_dataFone) + (dst_positive_scale_preserve_dataFone))) + (((dst_negative_code_preserve_dataFone) + (dst_negative_scale_preserve_dataFone)) * S ((dst_negative_code_preserve_dataFone) + (dst_negative_scale_preserve_dataFone)) + ((dst_negative_scale_preserve_dataFone) + (dst_negative_scale_preserve_dataFone)))) * S ((((dst_positive_code_preserve_dataFone) + (dst_positive_scale_preserve_dataFone)) * S ((dst_positive_code_preserve_dataFone) + (dst_positive_scale_preserve_dataFone)) + ((dst_positive_scale_preserve_dataFone) + (dst_positive_scale_preserve_dataFone))) + (((dst_negative_code_preserve_dataFone) + (dst_negative_scale_preserve_dataFone)) * S ((dst_negative_code_preserve_dataFone) + (dst_negative_scale_preserve_dataFone)) + ((dst_negative_scale_preserve_dataFone) + (dst_negative_scale_preserve_dataFone)))) + ((((dst_negative_code_preserve_dataFone) + (dst_negative_scale_preserve_dataFone)) * S ((dst_negative_code_preserve_dataFone) + (dst_negative_scale_preserve_dataFone)) + ((dst_negative_scale_preserve_dataFone) + (dst_negative_scale_preserve_dataFone))) + (((dst_negative_code_preserve_dataFone) + (dst_negative_scale_preserve_dataFone)) * S ((dst_negative_code_preserve_dataFone) + (dst_negative_scale_preserve_dataFone)) + ((dst_negative_scale_preserve_dataFone) + (dst_negative_scale_preserve_dataFone)))))) /\ (((((exists ff_h_pvs_preserve_dataFonepositive. ff_h_pvs_preserve_dataFonepositive + S (dst_positive_preserve_dataFone) = S ((S (1)) * dst_positive_scale_preserve_dataFone)) /\ exists ff_q_pvs_preserve_dataFonepositive. dst_positive_code_preserve_dataFone = ff_q_pvs_preserve_dataFonepositive * S ((S (1)) * dst_positive_scale_preserve_dataFone) + (dst_positive_preserve_dataFone))) /\ (((((exists ff_h_pvs_preserve_dataFonenegative. ff_h_pvs_preserve_dataFonenegative + S (dst_negative_preserve_dataFone) = S ((S (1)) * dst_negative_scale_preserve_dataFone)) /\ exists ff_q_pvs_preserve_dataFonenegative. dst_negative_code_preserve_dataFone = ff_q_pvs_preserve_dataFonenegative * S ((S (1)) * dst_negative_scale_preserve_dataFone) + (dst_negative_preserve_dataFone))) /\ (exists ge_balance_positive_preserve_dataFonevalue ge_balance_negative_preserve_dataFonevalue. (((((2) = 2 * (ge_balance_positive_preserve_dataFonevalue) /\ (ge_balance_negative_preserve_dataFonevalue) = 0) \/ exists ge_signed_half_preserve_dataFonevaluedecode. (((2) = 2 * ge_signed_half_preserve_dataFonevaluedecode + 1 /\ (ge_balance_positive_preserve_dataFonevalue) = 0) /\ (ge_balance_negative_preserve_dataFonevalue) = S ge_signed_half_preserve_dataFonevaluedecode))) /\ ((dst_positive_preserve_dataFone) + ge_balance_negative_preserve_dataFonevalue = (dst_negative_preserve_dataFone) + ge_balance_positive_preserve_dataFonevalue))))))))) /\ (forall mp_a_preserve_dataF mp_b_preserve_dataF mp_x_preserve_dataF mp_y_preserve_dataF mp_z_preserve_dataF. ~(mp_a_preserve_dataF=0) -> ~(mp_b_preserve_dataF=0) -> (exists pvs_le_gap_preserve_dataFbound. pvs_le_gap_preserve_dataFbound + (mp_a_preserve_dataF*mp_b_preserve_dataF) = (N)) -> (forall frp_divisor_preserve_dataFcoprime. (exists frp_left_factor_preserve_dataFcoprime. mp_a_preserve_dataF = frp_divisor_preserve_dataFcoprime * frp_left_factor_preserve_dataFcoprime) -> (exists frp_right_factor_preserve_dataFcoprime. mp_b_preserve_dataF = frp_divisor_preserve_dataFcoprime * frp_right_factor_preserve_dataFcoprime) -> frp_divisor_preserve_dataFcoprime = 1) -> (exists dst_positive_code_preserve_dataFfirst dst_positive_scale_preserve_dataFfirst dst_negative_code_preserve_dataFfirst dst_negative_scale_preserve_dataFfirst dst_positive_preserve_dataFfirst dst_negative_preserve_dataFfirst. (((F) = (((((dst_positive_code_preserve_dataFfirst) + (dst_positive_scale_preserve_dataFfirst)) * S ((dst_positive_code_preserve_dataFfirst) + (dst_positive_scale_preserve_dataFfirst)) + ((dst_positive_scale_preserve_dataFfirst) + (dst_positive_scale_preserve_dataFfirst))) + (((dst_negative_code_preserve_dataFfirst) + (dst_negative_scale_preserve_dataFfirst)) * S ((dst_negative_code_preserve_dataFfirst) + (dst_negative_scale_preserve_dataFfirst)) + ((dst_negative_scale_preserve_dataFfirst) + (dst_negative_scale_preserve_dataFfirst)))) * S ((((dst_positive_code_preserve_dataFfirst) + (dst_positive_scale_preserve_dataFfirst)) * S ((dst_positive_code_preserve_dataFfirst) + (dst_positive_scale_preserve_dataFfirst)) + ((dst_positive_scale_preserve_dataFfirst) + (dst_positive_scale_preserve_dataFfirst))) + (((dst_negative_code_preserve_dataFfirst) + (dst_negative_scale_preserve_dataFfirst)) * S ((dst_negative_code_preserve_dataFfirst) + (dst_negative_scale_preserve_dataFfirst)) + ((dst_negative_scale_preserve_dataFfirst) + (dst_negative_scale_preserve_dataFfirst)))) + ((((dst_negative_code_preserve_dataFfirst) + (dst_negative_scale_preserve_dataFfirst)) * S ((dst_negative_code_preserve_dataFfirst) + (dst_negative_scale_preserve_dataFfirst)) + ((dst_negative_scale_preserve_dataFfirst) + (dst_negative_scale_preserve_dataFfirst))) + (((dst_negative_code_preserve_dataFfirst) + (dst_negative_scale_preserve_dataFfirst)) * S ((dst_negative_code_preserve_dataFfirst) + (dst_negative_scale_preserve_dataFfirst)) + ((dst_negative_scale_preserve_dataFfirst) + (dst_negative_scale_preserve_dataFfirst)))))) /\ (((((exists ff_h_pvs_preserve_dataFfirstpositive. ff_h_pvs_preserve_dataFfirstpositive + S (dst_positive_preserve_dataFfirst) = S ((S (mp_a_preserve_dataF)) * dst_positive_scale_preserve_dataFfirst)) /\ exists ff_q_pvs_preserve_dataFfirstpositive. dst_positive_code_preserve_dataFfirst = ff_q_pvs_preserve_dataFfirstpositive * S ((S (mp_a_preserve_dataF)) * dst_positive_scale_preserve_dataFfirst) + (dst_positive_preserve_dataFfirst))) /\ (((((exists ff_h_pvs_preserve_dataFfirstnegative. ff_h_pvs_preserve_dataFfirstnegative + S (dst_negative_preserve_dataFfirst) = S ((S (mp_a_preserve_dataF)) * dst_negative_scale_preserve_dataFfirst)) /\ exists ff_q_pvs_preserve_dataFfirstnegative. dst_negative_code_preserve_dataFfirst = ff_q_pvs_preserve_dataFfirstnegative * S ((S (mp_a_preserve_dataF)) * dst_negative_scale_preserve_dataFfirst) + (dst_negative_preserve_dataFfirst))) /\ (exists ge_balance_positive_preserve_dataFfirstvalue ge_balance_negative_preserve_dataFfirstvalue. (((((mp_x_preserve_dataF) = 2 * (ge_balance_positive_preserve_dataFfirstvalue) /\ (ge_balance_negative_preserve_dataFfirstvalue) = 0) \/ exists ge_signed_half_preserve_dataFfirstvaluedecode. (((mp_x_preserve_dataF) = 2 * ge_signed_half_preserve_dataFfirstvaluedecode + 1 /\ (ge_balance_positive_preserve_dataFfirstvalue) = 0) /\ (ge_balance_negative_preserve_dataFfirstvalue) = S ge_signed_half_preserve_dataFfirstvaluedecode))) /\ ((dst_positive_preserve_dataFfirst) + ge_balance_negative_preserve_dataFfirstvalue = (dst_negative_preserve_dataFfirst) + ge_balance_positive_preserve_dataFfirstvalue))))))))) -> (exists dst_positive_code_preserve_dataFsecond dst_positive_scale_preserve_dataFsecond dst_negative_code_preserve_dataFsecond dst_negative_scale_preserve_dataFsecond dst_positive_preserve_dataFsecond dst_negative_preserve_dataFsecond. (((F) = (((((dst_positive_code_preserve_dataFsecond) + (dst_positive_scale_preserve_dataFsecond)) * S ((dst_positive_code_preserve_dataFsecond) + (dst_positive_scale_preserve_dataFsecond)) + ((dst_positive_scale_preserve_dataFsecond) + (dst_positive_scale_preserve_dataFsecond))) + (((dst_negative_code_preserve_dataFsecond) + (dst_negative_scale_preserve_dataFsecond)) * S ((dst_negative_code_preserve_dataFsecond) + (dst_negative_scale_preserve_dataFsecond)) + ((dst_negative_scale_preserve_dataFsecond) + (dst_negative_scale_preserve_dataFsecond)))) * S ((((dst_positive_code_preserve_dataFsecond) + (dst_positive_scale_preserve_dataFsecond)) * S ((dst_positive_code_preserve_dataFsecond) + (dst_positive_scale_preserve_dataFsecond)) + ((dst_positive_scale_preserve_dataFsecond) + (dst_positive_scale_preserve_dataFsecond))) + (((dst_negative_code_preserve_dataFsecond) + (dst_negative_scale_preserve_dataFsecond)) * S ((dst_negative_code_preserve_dataFsecond) + (dst_negative_scale_preserve_dataFsecond)) + ((dst_negative_scale_preserve_dataFsecond) + (dst_negative_scale_preserve_dataFsecond)))) + ((((dst_negative_code_preserve_dataFsecond) + (dst_negative_scale_preserve_dataFsecond)) * S ((dst_negative_code_preserve_dataFsecond) + (dst_negative_scale_preserve_dataFsecond)) + ((dst_negative_scale_preserve_dataFsecond) + (dst_negative_scale_preserve_dataFsecond))) + (((dst_negative_code_preserve_dataFsecond) + (dst_negative_scale_preserve_dataFsecond)) * S ((dst_negative_code_preserve_dataFsecond) + (dst_negative_scale_preserve_dataFsecond)) + ((dst_negative_scale_preserve_dataFsecond) + (dst_negative_scale_preserve_dataFsecond)))))) /\ (((((exists ff_h_pvs_preserve_dataFsecondpositive. ff_h_pvs_preserve_dataFsecondpositive + S (dst_positive_preserve_dataFsecond) = S ((S (mp_b_preserve_dataF)) * dst_positive_scale_preserve_dataFsecond)) /\ exists ff_q_pvs_preserve_dataFsecondpositive. dst_positive_code_preserve_dataFsecond = ff_q_pvs_preserve_dataFsecondpositive * S ((S (mp_b_preserve_dataF)) * dst_positive_scale_preserve_dataFsecond) + (dst_positive_preserve_dataFsecond))) /\ (((((exists ff_h_pvs_preserve_dataFsecondnegative. ff_h_pvs_preserve_dataFsecondnegative + S (dst_negative_preserve_dataFsecond) = S ((S (mp_b_preserve_dataF)) * dst_negative_scale_preserve_dataFsecond)) /\ exists ff_q_pvs_preserve_dataFsecondnegative. dst_negative_code_preserve_dataFsecond = ff_q_pvs_preserve_dataFsecondnegative * S ((S (mp_b_preserve_dataF)) * dst_negative_scale_preserve_dataFsecond) + (dst_negative_preserve_dataFsecond))) /\ (exists ge_balance_positive_preserve_dataFsecondvalue ge_balance_negative_preserve_dataFsecondvalue. (((((mp_y_preserve_dataF) = 2 * (ge_balance_positive_preserve_dataFsecondvalue) /\ (ge_balance_negative_preserve_dataFsecondvalue) = 0) \/ exists ge_signed_half_preserve_dataFsecondvaluedecode. (((mp_y_preserve_dataF) = 2 * ge_signed_half_preserve_dataFsecondvaluedecode + 1 /\ (ge_balance_positive_preserve_dataFsecondvalue) = 0) /\ (ge_balance_negative_preserve_dataFsecondvalue) = S ge_signed_half_preserve_dataFsecondvaluedecode))) /\ ((dst_positive_preserve_dataFsecond) + ge_balance_negative_preserve_dataFsecondvalue = (dst_negative_preserve_dataFsecond) + ge_balance_positive_preserve_dataFsecondvalue))))))))) -> (exists dst_positive_code_preserve_dataFproduct dst_positive_scale_preserve_dataFproduct dst_negative_code_preserve_dataFproduct dst_negative_scale_preserve_dataFproduct dst_positive_preserve_dataFproduct dst_negative_preserve_dataFproduct. (((F) = (((((dst_positive_code_preserve_dataFproduct) + (dst_positive_scale_preserve_dataFproduct)) * S ((dst_positive_code_preserve_dataFproduct) + (dst_positive_scale_preserve_dataFproduct)) + ((dst_positive_scale_preserve_dataFproduct) + (dst_positive_scale_preserve_dataFproduct))) + (((dst_negative_code_preserve_dataFproduct) + (dst_negative_scale_preserve_dataFproduct)) * S ((dst_negative_code_preserve_dataFproduct) + (dst_negative_scale_preserve_dataFproduct)) + ((dst_negative_scale_preserve_dataFproduct) + (dst_negative_scale_preserve_dataFproduct)))) * S ((((dst_positive_code_preserve_dataFproduct) + (dst_positive_scale_preserve_dataFproduct)) * S ((dst_positive_code_preserve_dataFproduct) + (dst_positive_scale_preserve_dataFproduct)) + ((dst_positive_scale_preserve_dataFproduct) + (dst_positive_scale_preserve_dataFproduct))) + (((dst_negative_code_preserve_dataFproduct) + (dst_negative_scale_preserve_dataFproduct)) * S ((dst_negative_code_preserve_dataFproduct) + (dst_negative_scale_preserve_dataFproduct)) + ((dst_negative_scale_preserve_dataFproduct) + (dst_negative_scale_preserve_dataFproduct)))) + ((((dst_negative_code_preserve_dataFproduct) + (dst_negative_scale_preserve_dataFproduct)) * S ((dst_negative_code_preserve_dataFproduct) + (dst_negative_scale_preserve_dataFproduct)) + ((dst_negative_scale_preserve_dataFproduct) + (dst_negative_scale_preserve_dataFproduct))) + (((dst_negative_code_preserve_dataFproduct) + (dst_negative_scale_preserve_dataFproduct)) * S ((dst_negative_code_preserve_dataFproduct) + (dst_negative_scale_preserve_dataFproduct)) + ((dst_negative_scale_preserve_dataFproduct) + (dst_negative_scale_preserve_dataFproduct)))))) /\ (((((exists ff_h_pvs_preserve_dataFproductpositive. ff_h_pvs_preserve_dataFproductpositive + S (dst_positive_preserve_dataFproduct) = S ((S (mp_a_preserve_dataF*mp_b_preserve_dataF)) * dst_positive_scale_preserve_dataFproduct)) /\ exists ff_q_pvs_preserve_dataFproductpositive. dst_positive_code_preserve_dataFproduct = ff_q_pvs_preserve_dataFproductpositive * S ((S (mp_a_preserve_dataF*mp_b_preserve_dataF)) * dst_positive_scale_preserve_dataFproduct) + (dst_positive_preserve_dataFproduct))) /\ (((((exists ff_h_pvs_preserve_dataFproductnegative. ff_h_pvs_preserve_dataFproductnegative + S (dst_negative_preserve_dataFproduct) = S ((S (mp_a_preserve_dataF*mp_b_preserve_dataF)) * dst_negative_scale_preserve_dataFproduct)) /\ exists ff_q_pvs_preserve_dataFproductnegative. dst_negative_code_preserve_dataFproduct = ff_q_pvs_preserve_dataFproductnegative * S ((S (mp_a_preserve_dataF*mp_b_preserve_dataF)) * dst_negative_scale_preserve_dataFproduct) + (dst_negative_preserve_dataFproduct))) /\ (exists ge_balance_positive_preserve_dataFproductvalue ge_balance_negative_preserve_dataFproductvalue. (((((mp_z_preserve_dataF) = 2 * (ge_balance_positive_preserve_dataFproductvalue) /\ (ge_balance_negative_preserve_dataFproductvalue) = 0) \/ exists ge_signed_half_preserve_dataFproductvaluedecode. (((mp_z_preserve_dataF) = 2 * ge_signed_half_preserve_dataFproductvaluedecode + 1 /\ (ge_balance_positive_preserve_dataFproductvalue) = 0) /\ (ge_balance_negative_preserve_dataFproductvalue) = S ge_signed_half_preserve_dataFproductvaluedecode))) /\ ((dst_positive_preserve_dataFproduct) + ge_balance_negative_preserve_dataFproductvalue = (dst_negative_preserve_dataFproduct) + ge_balance_positive_preserve_dataFproductvalue))))))))) -> (exists sto_ap_preserve_dataFlaw sto_an_preserve_dataFlaw sto_bp_preserve_dataFlaw sto_bn_preserve_dataFlaw sto_cp_preserve_dataFlaw sto_cn_preserve_dataFlaw. (((((mp_x_preserve_dataF) = 2 * (sto_ap_preserve_dataFlaw) /\ (sto_an_preserve_dataFlaw) = 0) \/ exists ge_signed_half_preserve_dataFlawleft. (((mp_x_preserve_dataF) = 2 * ge_signed_half_preserve_dataFlawleft + 1 /\ (sto_ap_preserve_dataFlaw) = 0) /\ (sto_an_preserve_dataFlaw) = S ge_signed_half_preserve_dataFlawleft))) /\ ((((((mp_y_preserve_dataF) = 2 * (sto_bp_preserve_dataFlaw) /\ (sto_bn_preserve_dataFlaw) = 0) \/ exists ge_signed_half_preserve_dataFlawright. (((mp_y_preserve_dataF) = 2 * ge_signed_half_preserve_dataFlawright + 1 /\ (sto_bp_preserve_dataFlaw) = 0) /\ (sto_bn_preserve_dataFlaw) = S ge_signed_half_preserve_dataFlawright))) /\ ((((((mp_z_preserve_dataF) = 2 * (sto_cp_preserve_dataFlaw) /\ (sto_cn_preserve_dataFlaw) = 0) \/ exists ge_signed_half_preserve_dataFlawoutput. (((mp_z_preserve_dataF) = 2 * ge_signed_half_preserve_dataFlawoutput + 1 /\ (sto_cp_preserve_dataFlaw) = 0) /\ (sto_cn_preserve_dataFlaw) = S ge_signed_half_preserve_dataFlawoutput))) /\ ((sto_ap_preserve_dataFlaw * sto_bp_preserve_dataFlaw + sto_an_preserve_dataFlaw * sto_bn_preserve_dataFlaw) + sto_cn_preserve_dataFlaw = (sto_ap_preserve_dataFlaw * sto_bn_preserve_dataFlaw + sto_an_preserve_dataFlaw * sto_bp_preserve_dataFlaw) + sto_cp_preserve_dataFlaw)))))))))))))) /\ (((((~((N)=0)) /\ (((exists dst_positive_code_preserve_dataGtable dst_positive_scale_preserve_dataGtable dst_negative_code_preserve_dataGtable dst_negative_scale_preserve_dataGtable. (((G) = (((((dst_positive_code_preserve_dataGtable) + (dst_positive_scale_preserve_dataGtable)) * S ((dst_positive_code_preserve_dataGtable) + (dst_positive_scale_preserve_dataGtable)) + ((dst_positive_scale_preserve_dataGtable) + (dst_positive_scale_preserve_dataGtable))) + (((dst_negative_code_preserve_dataGtable) + (dst_negative_scale_preserve_dataGtable)) * S ((dst_negative_code_preserve_dataGtable) + (dst_negative_scale_preserve_dataGtable)) + ((dst_negative_scale_preserve_dataGtable) + (dst_negative_scale_preserve_dataGtable)))) * S ((((dst_positive_code_preserve_dataGtable) + (dst_positive_scale_preserve_dataGtable)) * S ((dst_positive_code_preserve_dataGtable) + (dst_positive_scale_preserve_dataGtable)) + ((dst_positive_scale_preserve_dataGtable) + (dst_positive_scale_preserve_dataGtable))) + (((dst_negative_code_preserve_dataGtable) + (dst_negative_scale_preserve_dataGtable)) * S ((dst_negative_code_preserve_dataGtable) + (dst_negative_scale_preserve_dataGtable)) + ((dst_negative_scale_preserve_dataGtable) + (dst_negative_scale_preserve_dataGtable)))) + ((((dst_negative_code_preserve_dataGtable) + (dst_negative_scale_preserve_dataGtable)) * S ((dst_negative_code_preserve_dataGtable) + (dst_negative_scale_preserve_dataGtable)) + ((dst_negative_scale_preserve_dataGtable) + (dst_negative_scale_preserve_dataGtable))) + (((dst_negative_code_preserve_dataGtable) + (dst_negative_scale_preserve_dataGtable)) * S ((dst_negative_code_preserve_dataGtable) + (dst_negative_scale_preserve_dataGtable)) + ((dst_negative_scale_preserve_dataGtable) + (dst_negative_scale_preserve_dataGtable)))))) /\ (forall dst_index_preserve_dataGtable. (exists pvs_le_gap_preserve_dataGtabledomain. pvs_le_gap_preserve_dataGtabledomain + (dst_index_preserve_dataGtable) = (N)) -> exists dst_positive_preserve_dataGtable dst_negative_preserve_dataGtable dst_value_preserve_dataGtable. ((((exists ff_h_pvs_preserve_dataGtableentrypositive. ff_h_pvs_preserve_dataGtableentrypositive + S (dst_positive_preserve_dataGtable) = S ((S (dst_index_preserve_dataGtable)) * dst_positive_scale_preserve_dataGtable)) /\ exists ff_q_pvs_preserve_dataGtableentrypositive. dst_positive_code_preserve_dataGtable = ff_q_pvs_preserve_dataGtableentrypositive * S ((S (dst_index_preserve_dataGtable)) * dst_positive_scale_preserve_dataGtable) + (dst_positive_preserve_dataGtable))) /\ (((((exists ff_h_pvs_preserve_dataGtableentrynegative. ff_h_pvs_preserve_dataGtableentrynegative + S (dst_negative_preserve_dataGtable) = S ((S (dst_index_preserve_dataGtable)) * dst_negative_scale_preserve_dataGtable)) /\ exists ff_q_pvs_preserve_dataGtableentrynegative. dst_negative_code_preserve_dataGtable = ff_q_pvs_preserve_dataGtableentrynegative * S ((S (dst_index_preserve_dataGtable)) * dst_negative_scale_preserve_dataGtable) + (dst_negative_preserve_dataGtable))) /\ (exists ge_balance_positive_preserve_dataGtableentryvalue ge_balance_negative_preserve_dataGtableentryvalue. (((((dst_value_preserve_dataGtable) = 2 * (ge_balance_positive_preserve_dataGtableentryvalue) /\ (ge_balance_negative_preserve_dataGtableentryvalue) = 0) \/ exists ge_signed_half_preserve_dataGtableentryvaluedecode. (((dst_value_preserve_dataGtable) = 2 * ge_signed_half_preserve_dataGtableentryvaluedecode + 1 /\ (ge_balance_positive_preserve_dataGtableentryvalue) = 0) /\ (ge_balance_negative_preserve_dataGtableentryvalue) = S ge_signed_half_preserve_dataGtableentryvaluedecode))) /\ ((dst_positive_preserve_dataGtable) + ge_balance_negative_preserve_dataGtableentryvalue = (dst_negative_preserve_dataGtable) + ge_balance_positive_preserve_dataGtableentryvalue))))))))) /\ (((exists dst_positive_code_preserve_dataGone dst_positive_scale_preserve_dataGone dst_negative_code_preserve_dataGone dst_negative_scale_preserve_dataGone dst_positive_preserve_dataGone dst_negative_preserve_dataGone. (((G) = (((((dst_positive_code_preserve_dataGone) + (dst_positive_scale_preserve_dataGone)) * S ((dst_positive_code_preserve_dataGone) + (dst_positive_scale_preserve_dataGone)) + ((dst_positive_scale_preserve_dataGone) + (dst_positive_scale_preserve_dataGone))) + (((dst_negative_code_preserve_dataGone) + (dst_negative_scale_preserve_dataGone)) * S ((dst_negative_code_preserve_dataGone) + (dst_negative_scale_preserve_dataGone)) + ((dst_negative_scale_preserve_dataGone) + (dst_negative_scale_preserve_dataGone)))) * S ((((dst_positive_code_preserve_dataGone) + (dst_positive_scale_preserve_dataGone)) * S ((dst_positive_code_preserve_dataGone) + (dst_positive_scale_preserve_dataGone)) + ((dst_positive_scale_preserve_dataGone) + (dst_positive_scale_preserve_dataGone))) + (((dst_negative_code_preserve_dataGone) + (dst_negative_scale_preserve_dataGone)) * S ((dst_negative_code_preserve_dataGone) + (dst_negative_scale_preserve_dataGone)) + ((dst_negative_scale_preserve_dataGone) + (dst_negative_scale_preserve_dataGone)))) + ((((dst_negative_code_preserve_dataGone) + (dst_negative_scale_preserve_dataGone)) * S ((dst_negative_code_preserve_dataGone) + (dst_negative_scale_preserve_dataGone)) + ((dst_negative_scale_preserve_dataGone) + (dst_negative_scale_preserve_dataGone))) + (((dst_negative_code_preserve_dataGone) + (dst_negative_scale_preserve_dataGone)) * S ((dst_negative_code_preserve_dataGone) + (dst_negative_scale_preserve_dataGone)) + ((dst_negative_scale_preserve_dataGone) + (dst_negative_scale_preserve_dataGone)))))) /\ (((((exists ff_h_pvs_preserve_dataGonepositive. ff_h_pvs_preserve_dataGonepositive + S (dst_positive_preserve_dataGone) = S ((S (1)) * dst_positive_scale_preserve_dataGone)) /\ exists ff_q_pvs_preserve_dataGonepositive. dst_positive_code_preserve_dataGone = ff_q_pvs_preserve_dataGonepositive * S ((S (1)) * dst_positive_scale_preserve_dataGone) + (dst_positive_preserve_dataGone))) /\ (((((exists ff_h_pvs_preserve_dataGonenegative. ff_h_pvs_preserve_dataGonenegative + S (dst_negative_preserve_dataGone) = S ((S (1)) * dst_negative_scale_preserve_dataGone)) /\ exists ff_q_pvs_preserve_dataGonenegative. dst_negative_code_preserve_dataGone = ff_q_pvs_preserve_dataGonenegative * S ((S (1)) * dst_negative_scale_preserve_dataGone) + (dst_negative_preserve_dataGone))) /\ (exists ge_balance_positive_preserve_dataGonevalue ge_balance_negative_preserve_dataGonevalue. (((((2) = 2 * (ge_balance_positive_preserve_dataGonevalue) /\ (ge_balance_negative_preserve_dataGonevalue) = 0) \/ exists ge_signed_half_preserve_dataGonevaluedecode. (((2) = 2 * ge_signed_half_preserve_dataGonevaluedecode + 1 /\ (ge_balance_positive_preserve_dataGonevalue) = 0) /\ (ge_balance_negative_preserve_dataGonevalue) = S ge_signed_half_preserve_dataGonevaluedecode))) /\ ((dst_positive_preserve_dataGone) + ge_balance_negative_preserve_dataGonevalue = (dst_negative_preserve_dataGone) + ge_balance_positive_preserve_dataGonevalue))))))))) /\ (forall mp_a_preserve_dataG mp_b_preserve_dataG mp_x_preserve_dataG mp_y_preserve_dataG mp_z_preserve_dataG. ~(mp_a_preserve_dataG=0) -> ~(mp_b_preserve_dataG=0) -> (exists pvs_le_gap_preserve_dataGbound. pvs_le_gap_preserve_dataGbound + (mp_a_preserve_dataG*mp_b_preserve_dataG) = (N)) -> (forall frp_divisor_preserve_dataGcoprime. (exists frp_left_factor_preserve_dataGcoprime. mp_a_preserve_dataG = frp_divisor_preserve_dataGcoprime * frp_left_factor_preserve_dataGcoprime) -> (exists frp_right_factor_preserve_dataGcoprime. mp_b_preserve_dataG = frp_divisor_preserve_dataGcoprime * frp_right_factor_preserve_dataGcoprime) -> frp_divisor_preserve_dataGcoprime = 1) -> (exists dst_positive_code_preserve_dataGfirst dst_positive_scale_preserve_dataGfirst dst_negative_code_preserve_dataGfirst dst_negative_scale_preserve_dataGfirst dst_positive_preserve_dataGfirst dst_negative_preserve_dataGfirst. (((G) = (((((dst_positive_code_preserve_dataGfirst) + (dst_positive_scale_preserve_dataGfirst)) * S ((dst_positive_code_preserve_dataGfirst) + (dst_positive_scale_preserve_dataGfirst)) + ((dst_positive_scale_preserve_dataGfirst) + (dst_positive_scale_preserve_dataGfirst))) + (((dst_negative_code_preserve_dataGfirst) + (dst_negative_scale_preserve_dataGfirst)) * S ((dst_negative_code_preserve_dataGfirst) + (dst_negative_scale_preserve_dataGfirst)) + ((dst_negative_scale_preserve_dataGfirst) + (dst_negative_scale_preserve_dataGfirst)))) * S ((((dst_positive_code_preserve_dataGfirst) + (dst_positive_scale_preserve_dataGfirst)) * S ((dst_positive_code_preserve_dataGfirst) + (dst_positive_scale_preserve_dataGfirst)) + ((dst_positive_scale_preserve_dataGfirst) + (dst_positive_scale_preserve_dataGfirst))) + (((dst_negative_code_preserve_dataGfirst) + (dst_negative_scale_preserve_dataGfirst)) * S ((dst_negative_code_preserve_dataGfirst) + (dst_negative_scale_preserve_dataGfirst)) + ((dst_negative_scale_preserve_dataGfirst) + (dst_negative_scale_preserve_dataGfirst)))) + ((((dst_negative_code_preserve_dataGfirst) + (dst_negative_scale_preserve_dataGfirst)) * S ((dst_negative_code_preserve_dataGfirst) + (dst_negative_scale_preserve_dataGfirst)) + ((dst_negative_scale_preserve_dataGfirst) + (dst_negative_scale_preserve_dataGfirst))) + (((dst_negative_code_preserve_dataGfirst) + (dst_negative_scale_preserve_dataGfirst)) * S ((dst_negative_code_preserve_dataGfirst) + (dst_negative_scale_preserve_dataGfirst)) + ((dst_negative_scale_preserve_dataGfirst) + (dst_negative_scale_preserve_dataGfirst)))))) /\ (((((exists ff_h_pvs_preserve_dataGfirstpositive. ff_h_pvs_preserve_dataGfirstpositive + S (dst_positive_preserve_dataGfirst) = S ((S (mp_a_preserve_dataG)) * dst_positive_scale_preserve_dataGfirst)) /\ exists ff_q_pvs_preserve_dataGfirstpositive. dst_positive_code_preserve_dataGfirst = ff_q_pvs_preserve_dataGfirstpositive * S ((S (mp_a_preserve_dataG)) * dst_positive_scale_preserve_dataGfirst) + (dst_positive_preserve_dataGfirst))) /\ (((((exists ff_h_pvs_preserve_dataGfirstnegative. ff_h_pvs_preserve_dataGfirstnegative + S (dst_negative_preserve_dataGfirst) = S ((S (mp_a_preserve_dataG)) * dst_negative_scale_preserve_dataGfirst)) /\ exists ff_q_pvs_preserve_dataGfirstnegative. dst_negative_code_preserve_dataGfirst = ff_q_pvs_preserve_dataGfirstnegative * S ((S (mp_a_preserve_dataG)) * dst_negative_scale_preserve_dataGfirst) + (dst_negative_preserve_dataGfirst))) /\ (exists ge_balance_positive_preserve_dataGfirstvalue ge_balance_negative_preserve_dataGfirstvalue. (((((mp_x_preserve_dataG) = 2 * (ge_balance_positive_preserve_dataGfirstvalue) /\ (ge_balance_negative_preserve_dataGfirstvalue) = 0) \/ exists ge_signed_half_preserve_dataGfirstvaluedecode. (((mp_x_preserve_dataG) = 2 * ge_signed_half_preserve_dataGfirstvaluedecode + 1 /\ (ge_balance_positive_preserve_dataGfirstvalue) = 0) /\ (ge_balance_negative_preserve_dataGfirstvalue) = S ge_signed_half_preserve_dataGfirstvaluedecode))) /\ ((dst_positive_preserve_dataGfirst) + ge_balance_negative_preserve_dataGfirstvalue = (dst_negative_preserve_dataGfirst) + ge_balance_positive_preserve_dataGfirstvalue))))))))) -> (exists dst_positive_code_preserve_dataGsecond dst_positive_scale_preserve_dataGsecond dst_negative_code_preserve_dataGsecond dst_negative_scale_preserve_dataGsecond dst_positive_preserve_dataGsecond dst_negative_preserve_dataGsecond. (((G) = (((((dst_positive_code_preserve_dataGsecond) + (dst_positive_scale_preserve_dataGsecond)) * S ((dst_positive_code_preserve_dataGsecond) + (dst_positive_scale_preserve_dataGsecond)) + ((dst_positive_scale_preserve_dataGsecond) + (dst_positive_scale_preserve_dataGsecond))) + (((dst_negative_code_preserve_dataGsecond) + (dst_negative_scale_preserve_dataGsecond)) * S ((dst_negative_code_preserve_dataGsecond) + (dst_negative_scale_preserve_dataGsecond)) + ((dst_negative_scale_preserve_dataGsecond) + (dst_negative_scale_preserve_dataGsecond)))) * S ((((dst_positive_code_preserve_dataGsecond) + (dst_positive_scale_preserve_dataGsecond)) * S ((dst_positive_code_preserve_dataGsecond) + (dst_positive_scale_preserve_dataGsecond)) + ((dst_positive_scale_preserve_dataGsecond) + (dst_positive_scale_preserve_dataGsecond))) + (((dst_negative_code_preserve_dataGsecond) + (dst_negative_scale_preserve_dataGsecond)) * S ((dst_negative_code_preserve_dataGsecond) + (dst_negative_scale_preserve_dataGsecond)) + ((dst_negative_scale_preserve_dataGsecond) + (dst_negative_scale_preserve_dataGsecond)))) + ((((dst_negative_code_preserve_dataGsecond) + (dst_negative_scale_preserve_dataGsecond)) * S ((dst_negative_code_preserve_dataGsecond) + (dst_negative_scale_preserve_dataGsecond)) + ((dst_negative_scale_preserve_dataGsecond) + (dst_negative_scale_preserve_dataGsecond))) + (((dst_negative_code_preserve_dataGsecond) + (dst_negative_scale_preserve_dataGsecond)) * S ((dst_negative_code_preserve_dataGsecond) + (dst_negative_scale_preserve_dataGsecond)) + ((dst_negative_scale_preserve_dataGsecond) + (dst_negative_scale_preserve_dataGsecond)))))) /\ (((((exists ff_h_pvs_preserve_dataGsecondpositive. ff_h_pvs_preserve_dataGsecondpositive + S (dst_positive_preserve_dataGsecond) = S ((S (mp_b_preserve_dataG)) * dst_positive_scale_preserve_dataGsecond)) /\ exists ff_q_pvs_preserve_dataGsecondpositive. dst_positive_code_preserve_dataGsecond = ff_q_pvs_preserve_dataGsecondpositive * S ((S (mp_b_preserve_dataG)) * dst_positive_scale_preserve_dataGsecond) + (dst_positive_preserve_dataGsecond))) /\ (((((exists ff_h_pvs_preserve_dataGsecondnegative. ff_h_pvs_preserve_dataGsecondnegative + S (dst_negative_preserve_dataGsecond) = S ((S (mp_b_preserve_dataG)) * dst_negative_scale_preserve_dataGsecond)) /\ exists ff_q_pvs_preserve_dataGsecondnegative. dst_negative_code_preserve_dataGsecond = ff_q_pvs_preserve_dataGsecondnegative * S ((S (mp_b_preserve_dataG)) * dst_negative_scale_preserve_dataGsecond) + (dst_negative_preserve_dataGsecond))) /\ (exists ge_balance_positive_preserve_dataGsecondvalue ge_balance_negative_preserve_dataGsecondvalue. (((((mp_y_preserve_dataG) = 2 * (ge_balance_positive_preserve_dataGsecondvalue) /\ (ge_balance_negative_preserve_dataGsecondvalue) = 0) \/ exists ge_signed_half_preserve_dataGsecondvaluedecode. (((mp_y_preserve_dataG) = 2 * ge_signed_half_preserve_dataGsecondvaluedecode + 1 /\ (ge_balance_positive_preserve_dataGsecondvalue) = 0) /\ (ge_balance_negative_preserve_dataGsecondvalue) = S ge_signed_half_preserve_dataGsecondvaluedecode))) /\ ((dst_positive_preserve_dataGsecond) + ge_balance_negative_preserve_dataGsecondvalue = (dst_negative_preserve_dataGsecond) + ge_balance_positive_preserve_dataGsecondvalue))))))))) -> (exists dst_positive_code_preserve_dataGproduct dst_positive_scale_preserve_dataGproduct dst_negative_code_preserve_dataGproduct dst_negative_scale_preserve_dataGproduct dst_positive_preserve_dataGproduct dst_negative_preserve_dataGproduct. (((G) = (((((dst_positive_code_preserve_dataGproduct) + (dst_positive_scale_preserve_dataGproduct)) * S ((dst_positive_code_preserve_dataGproduct) + (dst_positive_scale_preserve_dataGproduct)) + ((dst_positive_scale_preserve_dataGproduct) + (dst_positive_scale_preserve_dataGproduct))) + (((dst_negative_code_preserve_dataGproduct) + (dst_negative_scale_preserve_dataGproduct)) * S ((dst_negative_code_preserve_dataGproduct) + (dst_negative_scale_preserve_dataGproduct)) + ((dst_negative_scale_preserve_dataGproduct) + (dst_negative_scale_preserve_dataGproduct)))) * S ((((dst_positive_code_preserve_dataGproduct) + (dst_positive_scale_preserve_dataGproduct)) * S ((dst_positive_code_preserve_dataGproduct) + (dst_positive_scale_preserve_dataGproduct)) + ((dst_positive_scale_preserve_dataGproduct) + (dst_positive_scale_preserve_dataGproduct))) + (((dst_negative_code_preserve_dataGproduct) + (dst_negative_scale_preserve_dataGproduct)) * S ((dst_negative_code_preserve_dataGproduct) + (dst_negative_scale_preserve_dataGproduct)) + ((dst_negative_scale_preserve_dataGproduct) + (dst_negative_scale_preserve_dataGproduct)))) + ((((dst_negative_code_preserve_dataGproduct) + (dst_negative_scale_preserve_dataGproduct)) * S ((dst_negative_code_preserve_dataGproduct) + (dst_negative_scale_preserve_dataGproduct)) + ((dst_negative_scale_preserve_dataGproduct) + (dst_negative_scale_preserve_dataGproduct))) + (((dst_negative_code_preserve_dataGproduct) + (dst_negative_scale_preserve_dataGproduct)) * S ((dst_negative_code_preserve_dataGproduct) + (dst_negative_scale_preserve_dataGproduct)) + ((dst_negative_scale_preserve_dataGproduct) + (dst_negative_scale_preserve_dataGproduct)))))) /\ (((((exists ff_h_pvs_preserve_dataGproductpositive. ff_h_pvs_preserve_dataGproductpositive + S (dst_positive_preserve_dataGproduct) = S ((S (mp_a_preserve_dataG*mp_b_preserve_dataG)) * dst_positive_scale_preserve_dataGproduct)) /\ exists ff_q_pvs_preserve_dataGproductpositive. dst_positive_code_preserve_dataGproduct = ff_q_pvs_preserve_dataGproductpositive * S ((S (mp_a_preserve_dataG*mp_b_preserve_dataG)) * dst_positive_scale_preserve_dataGproduct) + (dst_positive_preserve_dataGproduct))) /\ (((((exists ff_h_pvs_preserve_dataGproductnegative. ff_h_pvs_preserve_dataGproductnegative + S (dst_negative_preserve_dataGproduct) = S ((S (mp_a_preserve_dataG*mp_b_preserve_dataG)) * dst_negative_scale_preserve_dataGproduct)) /\ exists ff_q_pvs_preserve_dataGproductnegative. dst_negative_code_preserve_dataGproduct = ff_q_pvs_preserve_dataGproductnegative * S ((S (mp_a_preserve_dataG*mp_b_preserve_dataG)) * dst_negative_scale_preserve_dataGproduct) + (dst_negative_preserve_dataGproduct))) /\ (exists ge_balance_positive_preserve_dataGproductvalue ge_balance_negative_preserve_dataGproductvalue. (((((mp_z_preserve_dataG) = 2 * (ge_balance_positive_preserve_dataGproductvalue) /\ (ge_balance_negative_preserve_dataGproductvalue) = 0) \/ exists ge_signed_half_preserve_dataGproductvaluedecode. (((mp_z_preserve_dataG) = 2 * ge_signed_half_preserve_dataGproductvaluedecode + 1 /\ (ge_balance_positive_preserve_dataGproductvalue) = 0) /\ (ge_balance_negative_preserve_dataGproductvalue) = S ge_signed_half_preserve_dataGproductvaluedecode))) /\ ((dst_positive_preserve_dataGproduct) + ge_balance_negative_preserve_dataGproductvalue = (dst_negative_preserve_dataGproduct) + ge_balance_positive_preserve_dataGproductvalue))))))))) -> (exists sto_ap_preserve_dataGlaw sto_an_preserve_dataGlaw sto_bp_preserve_dataGlaw sto_bn_preserve_dataGlaw sto_cp_preserve_dataGlaw sto_cn_preserve_dataGlaw. (((((mp_x_preserve_dataG) = 2 * (sto_ap_preserve_dataGlaw) /\ (sto_an_preserve_dataGlaw) = 0) \/ exists ge_signed_half_preserve_dataGlawleft. (((mp_x_preserve_dataG) = 2 * ge_signed_half_preserve_dataGlawleft + 1 /\ (sto_ap_preserve_dataGlaw) = 0) /\ (sto_an_preserve_dataGlaw) = S ge_signed_half_preserve_dataGlawleft))) /\ ((((((mp_y_preserve_dataG) = 2 * (sto_bp_preserve_dataGlaw) /\ (sto_bn_preserve_dataGlaw) = 0) \/ exists ge_signed_half_preserve_dataGlawright. (((mp_y_preserve_dataG) = 2 * ge_signed_half_preserve_dataGlawright + 1 /\ (sto_bp_preserve_dataGlaw) = 0) /\ (sto_bn_preserve_dataGlaw) = S ge_signed_half_preserve_dataGlawright))) /\ ((((((mp_z_preserve_dataG) = 2 * (sto_cp_preserve_dataGlaw) /\ (sto_cn_preserve_dataGlaw) = 0) \/ exists ge_signed_half_preserve_dataGlawoutput. (((mp_z_preserve_dataG) = 2 * ge_signed_half_preserve_dataGlawoutput + 1 /\ (sto_cp_preserve_dataGlaw) = 0) /\ (sto_cn_preserve_dataGlaw) = S ge_signed_half_preserve_dataGlawoutput))) /\ ((sto_ap_preserve_dataGlaw * sto_bp_preserve_dataGlaw + sto_an_preserve_dataGlaw * sto_bn_preserve_dataGlaw) + sto_cn_preserve_dataGlaw = (sto_ap_preserve_dataGlaw * sto_bn_preserve_dataGlaw + sto_an_preserve_dataGlaw * sto_bp_preserve_dataGlaw) + sto_cp_preserve_dataGlaw)))))))))))))) /\ (((~((m)=0)) /\ (((~((n)=0)) /\ (((exists pvs_le_gap_preserve_databound. pvs_le_gap_preserve_databound + ((m)*(n)) = (N)) /\ (((forall sfd_common_divisor_preserve_datacoprime. (exists pvs_factor_preserve_datacoprimeleft. (m) = (sfd_common_divisor_preserve_datacoprime) * pvs_factor_preserve_datacoprimeleft) -> (exists pvs_factor_preserve_datacoprimeright. (n) = (sfd_common_divisor_preserve_datacoprime) * pvs_factor_preserve_datacoprimeright) -> sfd_common_divisor_preserve_datacoprime = 1) /\ (((((exists dst_positive_code_preserve_datalefttable dst_positive_scale_preserve_datalefttable dst_negative_code_preserve_datalefttable dst_negative_scale_preserve_datalefttable. (((A) = (((((dst_positive_code_preserve_datalefttable) + (dst_positive_scale_preserve_datalefttable)) * S ((dst_positive_code_preserve_datalefttable) + (dst_positive_scale_preserve_datalefttable)) + ((dst_positive_scale_preserve_datalefttable) + (dst_positive_scale_preserve_datalefttable))) + (((dst_negative_code_preserve_datalefttable) + (dst_negative_scale_preserve_datalefttable)) * S ((dst_negative_code_preserve_datalefttable) + (dst_negative_scale_preserve_datalefttable)) + ((dst_negative_scale_preserve_datalefttable) + (dst_negative_scale_preserve_datalefttable)))) * S ((((dst_positive_code_preserve_datalefttable) + (dst_positive_scale_preserve_datalefttable)) * S ((dst_positive_code_preserve_datalefttable) + (dst_positive_scale_preserve_datalefttable)) + ((dst_positive_scale_preserve_datalefttable) + (dst_positive_scale_preserve_datalefttable))) + (((dst_negative_code_preserve_datalefttable) + (dst_negative_scale_preserve_datalefttable)) * S ((dst_negative_code_preserve_datalefttable) + (dst_negative_scale_preserve_datalefttable)) + ((dst_negative_scale_preserve_datalefttable) + (dst_negative_scale_preserve_datalefttable)))) + ((((dst_negative_code_preserve_datalefttable) + (dst_negative_scale_preserve_datalefttable)) * S ((dst_negative_code_preserve_datalefttable) + (dst_negative_scale_preserve_datalefttable)) + ((dst_negative_scale_preserve_datalefttable) + (dst_negative_scale_preserve_datalefttable))) + (((dst_negative_code_preserve_datalefttable) + (dst_negative_scale_preserve_datalefttable)) * S ((dst_negative_code_preserve_datalefttable) + (dst_negative_scale_preserve_datalefttable)) + ((dst_negative_scale_preserve_datalefttable) + (dst_negative_scale_preserve_datalefttable)))))) /\ (forall dst_index_preserve_datalefttable. (exists pvs_le_gap_preserve_datalefttabledomain. pvs_le_gap_preserve_datalefttabledomain + (dst_index_preserve_datalefttable) = (m)) -> exists dst_positive_preserve_datalefttable dst_negative_preserve_datalefttable dst_value_preserve_datalefttable. ((((exists ff_h_pvs_preserve_datalefttableentrypositive. ff_h_pvs_preserve_datalefttableentrypositive + S (dst_positive_preserve_datalefttable) = S ((S (dst_index_preserve_datalefttable)) * dst_positive_scale_preserve_datalefttable)) /\ exists ff_q_pvs_preserve_datalefttableentrypositive. dst_positive_code_preserve_datalefttable = ff_q_pvs_preserve_datalefttableentrypositive * S ((S (dst_index_preserve_datalefttable)) * dst_positive_scale_preserve_datalefttable) + (dst_positive_preserve_datalefttable))) /\ (((((exists ff_h_pvs_preserve_datalefttableentrynegative. ff_h_pvs_preserve_datalefttableentrynegative + S (dst_negative_preserve_datalefttable) = S ((S (dst_index_preserve_datalefttable)) * dst_negative_scale_preserve_datalefttable)) /\ exists ff_q_pvs_preserve_datalefttableentrynegative. dst_negative_code_preserve_datalefttable = ff_q_pvs_preserve_datalefttableentrynegative * S ((S (dst_index_preserve_datalefttable)) * dst_negative_scale_preserve_datalefttable) + (dst_negative_preserve_datalefttable))) /\ (exists ge_balance_positive_preserve_datalefttableentryvalue ge_balance_negative_preserve_datalefttableentryvalue. (((((dst_value_preserve_datalefttable) = 2 * (ge_balance_positive_preserve_datalefttableentryvalue) /\ (ge_balance_negative_preserve_datalefttableentryvalue) = 0) \/ exists ge_signed_half_preserve_datalefttableentryvaluedecode. (((dst_value_preserve_datalefttable) = 2 * ge_signed_half_preserve_datalefttableentryvaluedecode + 1 /\ (ge_balance_positive_preserve_datalefttableentryvalue) = 0) /\ (ge_balance_negative_preserve_datalefttableentryvalue) = S ge_signed_half_preserve_datalefttableentryvaluedecode))) /\ ((dst_positive_preserve_datalefttable) + ge_balance_negative_preserve_datalefttableentryvalue = (dst_negative_preserve_datalefttable) + ge_balance_positive_preserve_datalefttableentryvalue))))))))) /\ (forall dc_index_preserve_dataleft dc_value_preserve_dataleft. (exists pvs_le_gap_preserve_dataleftdomain. pvs_le_gap_preserve_dataleftdomain + (dc_index_preserve_dataleft) = (m)) -> (exists dst_positive_code_preserve_dataleftlookup dst_positive_scale_preserve_dataleftlookup dst_negative_code_preserve_dataleftlookup dst_negative_scale_preserve_dataleftlookup dst_positive_preserve_dataleftlookup dst_negative_preserve_dataleftlookup. (((A) = (((((dst_positive_code_preserve_dataleftlookup) + (dst_positive_scale_preserve_dataleftlookup)) * S ((dst_positive_code_preserve_dataleftlookup) + (dst_positive_scale_preserve_dataleftlookup)) + ((dst_positive_scale_preserve_dataleftlookup) + (dst_positive_scale_preserve_dataleftlookup))) + (((dst_negative_code_preserve_dataleftlookup) + (dst_negative_scale_preserve_dataleftlookup)) * S ((dst_negative_code_preserve_dataleftlookup) + (dst_negative_scale_preserve_dataleftlookup)) + ((dst_negative_scale_preserve_dataleftlookup) + (dst_negative_scale_preserve_dataleftlookup)))) * S ((((dst_positive_code_preserve_dataleftlookup) + (dst_positive_scale_preserve_dataleftlookup)) * S ((dst_positive_code_preserve_dataleftlookup) + (dst_positive_scale_preserve_dataleftlookup)) + ((dst_positive_scale_preserve_dataleftlookup) + (dst_positive_scale_preserve_dataleftlookup))) + (((dst_negative_code_preserve_dataleftlookup) + (dst_negative_scale_preserve_dataleftlookup)) * S ((dst_negative_code_preserve_dataleftlookup) + (dst_negative_scale_preserve_dataleftlookup)) + ((dst_negative_scale_preserve_dataleftlookup) + (dst_negative_scale_preserve_dataleftlookup)))) + ((((dst_negative_code_preserve_dataleftlookup) + (dst_negative_scale_preserve_dataleftlookup)) * S ((dst_negative_code_preserve_dataleftlookup) + (dst_negative_scale_preserve_dataleftlookup)) + ((dst_negative_scale_preserve_dataleftlookup) + (dst_negative_scale_preserve_dataleftlookup))) + (((dst_negative_code_preserve_dataleftlookup) + (dst_negative_scale_preserve_dataleftlookup)) * S ((dst_negative_code_preserve_dataleftlookup) + (dst_negative_scale_preserve_dataleftlookup)) + ((dst_negative_scale_preserve_dataleftlookup) + (dst_negative_scale_preserve_dataleftlookup)))))) /\ (((((exists ff_h_pvs_preserve_dataleftlookuppositive. ff_h_pvs_preserve_dataleftlookuppositive + S (dst_positive_preserve_dataleftlookup) = S ((S (dc_index_preserve_dataleft)) * dst_positive_scale_preserve_dataleftlookup)) /\ exists ff_q_pvs_preserve_dataleftlookuppositive. dst_positive_code_preserve_dataleftlookup = ff_q_pvs_preserve_dataleftlookuppositive * S ((S (dc_index_preserve_dataleft)) * dst_positive_scale_preserve_dataleftlookup) + (dst_positive_preserve_dataleftlookup))) /\ (((((exists ff_h_pvs_preserve_dataleftlookupnegative. ff_h_pvs_preserve_dataleftlookupnegative + S (dst_negative_preserve_dataleftlookup) = S ((S (dc_index_preserve_dataleft)) * dst_negative_scale_preserve_dataleftlookup)) /\ exists ff_q_pvs_preserve_dataleftlookupnegative. dst_negative_code_preserve_dataleftlookup = ff_q_pvs_preserve_dataleftlookupnegative * S ((S (dc_index_preserve_dataleft)) * dst_negative_scale_preserve_dataleftlookup) + (dst_negative_preserve_dataleftlookup))) /\ (exists ge_balance_positive_preserve_dataleftlookupvalue ge_balance_negative_preserve_dataleftlookupvalue. (((((dc_value_preserve_dataleft) = 2 * (ge_balance_positive_preserve_dataleftlookupvalue) /\ (ge_balance_negative_preserve_dataleftlookupvalue) = 0) \/ exists ge_signed_half_preserve_dataleftlookupvaluedecode. (((dc_value_preserve_dataleft) = 2 * ge_signed_half_preserve_dataleftlookupvaluedecode + 1 /\ (ge_balance_positive_preserve_dataleftlookupvalue) = 0) /\ (ge_balance_negative_preserve_dataleftlookupvalue) = S ge_signed_half_preserve_dataleftlookupvaluedecode))) /\ ((dst_positive_preserve_dataleftlookup) + ge_balance_negative_preserve_dataleftlookupvalue = (dst_negative_preserve_dataleftlookup) + ge_balance_positive_preserve_dataleftlookupvalue))))))))) -> ((((~((dc_index_preserve_dataleft)=0)) /\ (exists dc_quotient_preserve_dataleftentry dc_left_preserve_dataleftentry dc_right_preserve_dataleftentry. (((m)=(dc_index_preserve_dataleft)*dc_quotient_preserve_dataleftentry) /\ (((exists dst_positive_code_preserve_dataleftentryleft dst_positive_scale_preserve_dataleftentryleft dst_negative_code_preserve_dataleftentryleft dst_negative_scale_preserve_dataleftentryleft dst_positive_preserve_dataleftentryleft dst_negative_preserve_dataleftentryleft. (((F) = (((((dst_positive_code_preserve_dataleftentryleft) + (dst_positive_scale_preserve_dataleftentryleft)) * S ((dst_positive_code_preserve_dataleftentryleft) + (dst_positive_scale_preserve_dataleftentryleft)) + ((dst_positive_scale_preserve_dataleftentryleft) + (dst_positive_scale_preserve_dataleftentryleft))) + (((dst_negative_code_preserve_dataleftentryleft) + (dst_negative_scale_preserve_dataleftentryleft)) * S ((dst_negative_code_preserve_dataleftentryleft) + (dst_negative_scale_preserve_dataleftentryleft)) + ((dst_negative_scale_preserve_dataleftentryleft) + (dst_negative_scale_preserve_dataleftentryleft)))) * S ((((dst_positive_code_preserve_dataleftentryleft) + (dst_positive_scale_preserve_dataleftentryleft)) * S ((dst_positive_code_preserve_dataleftentryleft) + (dst_positive_scale_preserve_dataleftentryleft)) + ((dst_positive_scale_preserve_dataleftentryleft) + (dst_positive_scale_preserve_dataleftentryleft))) + (((dst_negative_code_preserve_dataleftentryleft) + (dst_negative_scale_preserve_dataleftentryleft)) * S ((dst_negative_code_preserve_dataleftentryleft) + (dst_negative_scale_preserve_dataleftentryleft)) + ((dst_negative_scale_preserve_dataleftentryleft) + (dst_negative_scale_preserve_dataleftentryleft)))) + ((((dst_negative_code_preserve_dataleftentryleft) + (dst_negative_scale_preserve_dataleftentryleft)) * S ((dst_negative_code_preserve_dataleftentryleft) + (dst_negative_scale_preserve_dataleftentryleft)) + ((dst_negative_scale_preserve_dataleftentryleft) + (dst_negative_scale_preserve_dataleftentryleft))) + (((dst_negative_code_preserve_dataleftentryleft) + (dst_negative_scale_preserve_dataleftentryleft)) * S ((dst_negative_code_preserve_dataleftentryleft) + (dst_negative_scale_preserve_dataleftentryleft)) + ((dst_negative_scale_preserve_dataleftentryleft) + (dst_negative_scale_preserve_dataleftentryleft)))))) /\ (((((exists ff_h_pvs_preserve_dataleftentryleftpositive. ff_h_pvs_preserve_dataleftentryleftpositive + S (dst_positive_preserve_dataleftentryleft) = S ((S (dc_index_preserve_dataleft)) * dst_positive_scale_preserve_dataleftentryleft)) /\ exists ff_q_pvs_preserve_dataleftentryleftpositive. dst_positive_code_preserve_dataleftentryleft = ff_q_pvs_preserve_dataleftentryleftpositive * S ((S (dc_index_preserve_dataleft)) * dst_positive_scale_preserve_dataleftentryleft) + (dst_positive_preserve_dataleftentryleft))) /\ (((((exists ff_h_pvs_preserve_dataleftentryleftnegative. ff_h_pvs_preserve_dataleftentryleftnegative + S (dst_negative_preserve_dataleftentryleft) = S ((S (dc_index_preserve_dataleft)) * dst_negative_scale_preserve_dataleftentryleft)) /\ exists ff_q_pvs_preserve_dataleftentryleftnegative. dst_negative_code_preserve_dataleftentryleft = ff_q_pvs_preserve_dataleftentryleftnegative * S ((S (dc_index_preserve_dataleft)) * dst_negative_scale_preserve_dataleftentryleft) + (dst_negative_preserve_dataleftentryleft))) /\ (exists ge_balance_positive_preserve_dataleftentryleftvalue ge_balance_negative_preserve_dataleftentryleftvalue. (((((dc_left_preserve_dataleftentry) = 2 * (ge_balance_positive_preserve_dataleftentryleftvalue) /\ (ge_balance_negative_preserve_dataleftentryleftvalue) = 0) \/ exists ge_signed_half_preserve_dataleftentryleftvaluedecode. (((dc_left_preserve_dataleftentry) = 2 * ge_signed_half_preserve_dataleftentryleftvaluedecode + 1 /\ (ge_balance_positive_preserve_dataleftentryleftvalue) = 0) /\ (ge_balance_negative_preserve_dataleftentryleftvalue) = S ge_signed_half_preserve_dataleftentryleftvaluedecode))) /\ ((dst_positive_preserve_dataleftentryleft) + ge_balance_negative_preserve_dataleftentryleftvalue = (dst_negative_preserve_dataleftentryleft) + ge_balance_positive_preserve_dataleftentryleftvalue))))))))) /\ (((exists dst_positive_code_preserve_dataleftentryright dst_positive_scale_preserve_dataleftentryright dst_negative_code_preserve_dataleftentryright dst_negative_scale_preserve_dataleftentryright dst_positive_preserve_dataleftentryright dst_negative_preserve_dataleftentryright. (((G) = (((((dst_positive_code_preserve_dataleftentryright) + (dst_positive_scale_preserve_dataleftentryright)) * S ((dst_positive_code_preserve_dataleftentryright) + (dst_positive_scale_preserve_dataleftentryright)) + ((dst_positive_scale_preserve_dataleftentryright) + (dst_positive_scale_preserve_dataleftentryright))) + (((dst_negative_code_preserve_dataleftentryright) + (dst_negative_scale_preserve_dataleftentryright)) * S ((dst_negative_code_preserve_dataleftentryright) + (dst_negative_scale_preserve_dataleftentryright)) + ((dst_negative_scale_preserve_dataleftentryright) + (dst_negative_scale_preserve_dataleftentryright)))) * S ((((dst_positive_code_preserve_dataleftentryright) + (dst_positive_scale_preserve_dataleftentryright)) * S ((dst_positive_code_preserve_dataleftentryright) + (dst_positive_scale_preserve_dataleftentryright)) + ((dst_positive_scale_preserve_dataleftentryright) + (dst_positive_scale_preserve_dataleftentryright))) + (((dst_negative_code_preserve_dataleftentryright) + (dst_negative_scale_preserve_dataleftentryright)) * S ((dst_negative_code_preserve_dataleftentryright) + (dst_negative_scale_preserve_dataleftentryright)) + ((dst_negative_scale_preserve_dataleftentryright) + (dst_negative_scale_preserve_dataleftentryright)))) + ((((dst_negative_code_preserve_dataleftentryright) + (dst_negative_scale_preserve_dataleftentryright)) * S ((dst_negative_code_preserve_dataleftentryright) + (dst_negative_scale_preserve_dataleftentryright)) + ((dst_negative_scale_preserve_dataleftentryright) + (dst_negative_scale_preserve_dataleftentryright))) + (((dst_negative_code_preserve_dataleftentryright) + (dst_negative_scale_preserve_dataleftentryright)) * S ((dst_negative_code_preserve_dataleftentryright) + (dst_negative_scale_preserve_dataleftentryright)) + ((dst_negative_scale_preserve_dataleftentryright) + (dst_negative_scale_preserve_dataleftentryright)))))) /\ (((((exists ff_h_pvs_preserve_dataleftentryrightpositive. ff_h_pvs_preserve_dataleftentryrightpositive + S (dst_positive_preserve_dataleftentryright) = S ((S (dc_quotient_preserve_dataleftentry)) * dst_positive_scale_preserve_dataleftentryright)) /\ exists ff_q_pvs_preserve_dataleftentryrightpositive. dst_positive_code_preserve_dataleftentryright = ff_q_pvs_preserve_dataleftentryrightpositive * S ((S (dc_quotient_preserve_dataleftentry)) * dst_positive_scale_preserve_dataleftentryright) + (dst_positive_preserve_dataleftentryright))) /\ (((((exists ff_h_pvs_preserve_dataleftentryrightnegative. ff_h_pvs_preserve_dataleftentryrightnegative + S (dst_negative_preserve_dataleftentryright) = S ((S (dc_quotient_preserve_dataleftentry)) * dst_negative_scale_preserve_dataleftentryright)) /\ exists ff_q_pvs_preserve_dataleftentryrightnegative. dst_negative_code_preserve_dataleftentryright = ff_q_pvs_preserve_dataleftentryrightnegative * S ((S (dc_quotient_preserve_dataleftentry)) * dst_negative_scale_preserve_dataleftentryright) + (dst_negative_preserve_dataleftentryright))) /\ (exists ge_balance_positive_preserve_dataleftentryrightvalue ge_balance_negative_preserve_dataleftentryrightvalue. (((((dc_right_preserve_dataleftentry) = 2 * (ge_balance_positive_preserve_dataleftentryrightvalue) /\ (ge_balance_negative_preserve_dataleftentryrightvalue) = 0) \/ exists ge_signed_half_preserve_dataleftentryrightvaluedecode. (((dc_right_preserve_dataleftentry) = 2 * ge_signed_half_preserve_dataleftentryrightvaluedecode + 1 /\ (ge_balance_positive_preserve_dataleftentryrightvalue) = 0) /\ (ge_balance_negative_preserve_dataleftentryrightvalue) = S ge_signed_half_preserve_dataleftentryrightvaluedecode))) /\ ((dst_positive_preserve_dataleftentryright) + ge_balance_negative_preserve_dataleftentryrightvalue = (dst_negative_preserve_dataleftentryright) + ge_balance_positive_preserve_dataleftentryrightvalue))))))))) /\ (exists sto_ap_preserve_dataleftentryproduct sto_an_preserve_dataleftentryproduct sto_bp_preserve_dataleftentryproduct sto_bn_preserve_dataleftentryproduct sto_cp_preserve_dataleftentryproduct sto_cn_preserve_dataleftentryproduct. (((((dc_left_preserve_dataleftentry) = 2 * (sto_ap_preserve_dataleftentryproduct) /\ (sto_an_preserve_dataleftentryproduct) = 0) \/ exists ge_signed_half_preserve_dataleftentryproductleft. (((dc_left_preserve_dataleftentry) = 2 * ge_signed_half_preserve_dataleftentryproductleft + 1 /\ (sto_ap_preserve_dataleftentryproduct) = 0) /\ (sto_an_preserve_dataleftentryproduct) = S ge_signed_half_preserve_dataleftentryproductleft))) /\ ((((((dc_right_preserve_dataleftentry) = 2 * (sto_bp_preserve_dataleftentryproduct) /\ (sto_bn_preserve_dataleftentryproduct) = 0) \/ exists ge_signed_half_preserve_dataleftentryproductright. (((dc_right_preserve_dataleftentry) = 2 * ge_signed_half_preserve_dataleftentryproductright + 1 /\ (sto_bp_preserve_dataleftentryproduct) = 0) /\ (sto_bn_preserve_dataleftentryproduct) = S ge_signed_half_preserve_dataleftentryproductright))) /\ ((((((dc_value_preserve_dataleft) = 2 * (sto_cp_preserve_dataleftentryproduct) /\ (sto_cn_preserve_dataleftentryproduct) = 0) \/ exists ge_signed_half_preserve_dataleftentryproductoutput. (((dc_value_preserve_dataleft) = 2 * ge_signed_half_preserve_dataleftentryproductoutput + 1 /\ (sto_cp_preserve_dataleftentryproduct) = 0) /\ (sto_cn_preserve_dataleftentryproduct) = S ge_signed_half_preserve_dataleftentryproductoutput))) /\ ((sto_ap_preserve_dataleftentryproduct * sto_bp_preserve_dataleftentryproduct + sto_an_preserve_dataleftentryproduct * sto_bn_preserve_dataleftentryproduct) + sto_cn_preserve_dataleftentryproduct = (sto_ap_preserve_dataleftentryproduct * sto_bn_preserve_dataleftentryproduct + sto_an_preserve_dataleftentryproduct * sto_bp_preserve_dataleftentryproduct) + sto_cp_preserve_dataleftentryproduct))))))))))))))) \/ ((((dc_index_preserve_dataleft)=0 \/ ~(exists pvs_factor_preserve_dataleftentrynondivisor. (m) = (dc_index_preserve_dataleft) * pvs_factor_preserve_dataleftentrynondivisor)) /\ ((dc_value_preserve_dataleft)=0))))))) /\ (((((exists dst_positive_code_preserve_datarighttable dst_positive_scale_preserve_datarighttable dst_negative_code_preserve_datarighttable dst_negative_scale_preserve_datarighttable. (((B) = (((((dst_positive_code_preserve_datarighttable) + (dst_positive_scale_preserve_datarighttable)) * S ((dst_positive_code_preserve_datarighttable) + (dst_positive_scale_preserve_datarighttable)) + ((dst_positive_scale_preserve_datarighttable) + (dst_positive_scale_preserve_datarighttable))) + (((dst_negative_code_preserve_datarighttable) + (dst_negative_scale_preserve_datarighttable)) * S ((dst_negative_code_preserve_datarighttable) + (dst_negative_scale_preserve_datarighttable)) + ((dst_negative_scale_preserve_datarighttable) + (dst_negative_scale_preserve_datarighttable)))) * S ((((dst_positive_code_preserve_datarighttable) + (dst_positive_scale_preserve_datarighttable)) * S ((dst_positive_code_preserve_datarighttable) + (dst_positive_scale_preserve_datarighttable)) + ((dst_positive_scale_preserve_datarighttable) + (dst_positive_scale_preserve_datarighttable))) + (((dst_negative_code_preserve_datarighttable) + (dst_negative_scale_preserve_datarighttable)) * S ((dst_negative_code_preserve_datarighttable) + (dst_negative_scale_preserve_datarighttable)) + ((dst_negative_scale_preserve_datarighttable) + (dst_negative_scale_preserve_datarighttable)))) + ((((dst_negative_code_preserve_datarighttable) + (dst_negative_scale_preserve_datarighttable)) * S ((dst_negative_code_preserve_datarighttable) + (dst_negative_scale_preserve_datarighttable)) + ((dst_negative_scale_preserve_datarighttable) + (dst_negative_scale_preserve_datarighttable))) + (((dst_negative_code_preserve_datarighttable) + (dst_negative_scale_preserve_datarighttable)) * S ((dst_negative_code_preserve_datarighttable) + (dst_negative_scale_preserve_datarighttable)) + ((dst_negative_scale_preserve_datarighttable) + (dst_negative_scale_preserve_datarighttable)))))) /\ (forall dst_index_preserve_datarighttable. (exists pvs_le_gap_preserve_datarighttabledomain. pvs_le_gap_preserve_datarighttabledomain + (dst_index_preserve_datarighttable) = (n)) -> exists dst_positive_preserve_datarighttable dst_negative_preserve_datarighttable dst_value_preserve_datarighttable. ((((exists ff_h_pvs_preserve_datarighttableentrypositive. ff_h_pvs_preserve_datarighttableentrypositive + S (dst_positive_preserve_datarighttable) = S ((S (dst_index_preserve_datarighttable)) * dst_positive_scale_preserve_datarighttable)) /\ exists ff_q_pvs_preserve_datarighttableentrypositive. dst_positive_code_preserve_datarighttable = ff_q_pvs_preserve_datarighttableentrypositive * S ((S (dst_index_preserve_datarighttable)) * dst_positive_scale_preserve_datarighttable) + (dst_positive_preserve_datarighttable))) /\ (((((exists ff_h_pvs_preserve_datarighttableentrynegative. ff_h_pvs_preserve_datarighttableentrynegative + S (dst_negative_preserve_datarighttable) = S ((S (dst_index_preserve_datarighttable)) * dst_negative_scale_preserve_datarighttable)) /\ exists ff_q_pvs_preserve_datarighttableentrynegative. dst_negative_code_preserve_datarighttable = ff_q_pvs_preserve_datarighttableentrynegative * S ((S (dst_index_preserve_datarighttable)) * dst_negative_scale_preserve_datarighttable) + (dst_negative_preserve_datarighttable))) /\ (exists ge_balance_positive_preserve_datarighttableentryvalue ge_balance_negative_preserve_datarighttableentryvalue. (((((dst_value_preserve_datarighttable) = 2 * (ge_balance_positive_preserve_datarighttableentryvalue) /\ (ge_balance_negative_preserve_datarighttableentryvalue) = 0) \/ exists ge_signed_half_preserve_datarighttableentryvaluedecode. (((dst_value_preserve_datarighttable) = 2 * ge_signed_half_preserve_datarighttableentryvaluedecode + 1 /\ (ge_balance_positive_preserve_datarighttableentryvalue) = 0) /\ (ge_balance_negative_preserve_datarighttableentryvalue) = S ge_signed_half_preserve_datarighttableentryvaluedecode))) /\ ((dst_positive_preserve_datarighttable) + ge_balance_negative_preserve_datarighttableentryvalue = (dst_negative_preserve_datarighttable) + ge_balance_positive_preserve_datarighttableentryvalue))))))))) /\ (forall dc_index_preserve_dataright dc_value_preserve_dataright. (exists pvs_le_gap_preserve_datarightdomain. pvs_le_gap_preserve_datarightdomain + (dc_index_preserve_dataright) = (n)) -> (exists dst_positive_code_preserve_datarightlookup dst_positive_scale_preserve_datarightlookup dst_negative_code_preserve_datarightlookup dst_negative_scale_preserve_datarightlookup dst_positive_preserve_datarightlookup dst_negative_preserve_datarightlookup. (((B) = (((((dst_positive_code_preserve_datarightlookup) + (dst_positive_scale_preserve_datarightlookup)) * S ((dst_positive_code_preserve_datarightlookup) + (dst_positive_scale_preserve_datarightlookup)) + ((dst_positive_scale_preserve_datarightlookup) + (dst_positive_scale_preserve_datarightlookup))) + (((dst_negative_code_preserve_datarightlookup) + (dst_negative_scale_preserve_datarightlookup)) * S ((dst_negative_code_preserve_datarightlookup) + (dst_negative_scale_preserve_datarightlookup)) + ((dst_negative_scale_preserve_datarightlookup) + (dst_negative_scale_preserve_datarightlookup)))) * S ((((dst_positive_code_preserve_datarightlookup) + (dst_positive_scale_preserve_datarightlookup)) * S ((dst_positive_code_preserve_datarightlookup) + (dst_positive_scale_preserve_datarightlookup)) + ((dst_positive_scale_preserve_datarightlookup) + (dst_positive_scale_preserve_datarightlookup))) + (((dst_negative_code_preserve_datarightlookup) + (dst_negative_scale_preserve_datarightlookup)) * S ((dst_negative_code_preserve_datarightlookup) + (dst_negative_scale_preserve_datarightlookup)) + ((dst_negative_scale_preserve_datarightlookup) + (dst_negative_scale_preserve_datarightlookup)))) + ((((dst_negative_code_preserve_datarightlookup) + (dst_negative_scale_preserve_datarightlookup)) * S ((dst_negative_code_preserve_datarightlookup) + (dst_negative_scale_preserve_datarightlookup)) + ((dst_negative_scale_preserve_datarightlookup) + (dst_negative_scale_preserve_datarightlookup))) + (((dst_negative_code_preserve_datarightlookup) + (dst_negative_scale_preserve_datarightlookup)) * S ((dst_negative_code_preserve_datarightlookup) + (dst_negative_scale_preserve_datarightlookup)) + ((dst_negative_scale_preserve_datarightlookup) + (dst_negative_scale_preserve_datarightlookup)))))) /\ (((((exists ff_h_pvs_preserve_datarightlookuppositive. ff_h_pvs_preserve_datarightlookuppositive + S (dst_positive_preserve_datarightlookup) = S ((S (dc_index_preserve_dataright)) * dst_positive_scale_preserve_datarightlookup)) /\ exists ff_q_pvs_preserve_datarightlookuppositive. dst_positive_code_preserve_datarightlookup = ff_q_pvs_preserve_datarightlookuppositive * S ((S (dc_index_preserve_dataright)) * dst_positive_scale_preserve_datarightlookup) + (dst_positive_preserve_datarightlookup))) /\ (((((exists ff_h_pvs_preserve_datarightlookupnegative. ff_h_pvs_preserve_datarightlookupnegative + S (dst_negative_preserve_datarightlookup) = S ((S (dc_index_preserve_dataright)) * dst_negative_scale_preserve_datarightlookup)) /\ exists ff_q_pvs_preserve_datarightlookupnegative. dst_negative_code_preserve_datarightlookup = ff_q_pvs_preserve_datarightlookupnegative * S ((S (dc_index_preserve_dataright)) * dst_negative_scale_preserve_datarightlookup) + (dst_negative_preserve_datarightlookup))) /\ (exists ge_balance_positive_preserve_datarightlookupvalue ge_balance_negative_preserve_datarightlookupvalue. (((((dc_value_preserve_dataright) = 2 * (ge_balance_positive_preserve_datarightlookupvalue) /\ (ge_balance_negative_preserve_datarightlookupvalue) = 0) \/ exists ge_signed_half_preserve_datarightlookupvaluedecode. (((dc_value_preserve_dataright) = 2 * ge_signed_half_preserve_datarightlookupvaluedecode + 1 /\ (ge_balance_positive_preserve_datarightlookupvalue) = 0) /\ (ge_balance_negative_preserve_datarightlookupvalue) = S ge_signed_half_preserve_datarightlookupvaluedecode))) /\ ((dst_positive_preserve_datarightlookup) + ge_balance_negative_preserve_datarightlookupvalue = (dst_negative_preserve_datarightlookup) + ge_balance_positive_preserve_datarightlookupvalue))))))))) -> ((((~((dc_index_preserve_dataright)=0)) /\ (exists dc_quotient_preserve_datarightentry dc_left_preserve_datarightentry dc_right_preserve_datarightentry. (((n)=(dc_index_preserve_dataright)*dc_quotient_preserve_datarightentry) /\ (((exists dst_positive_code_preserve_datarightentryleft dst_positive_scale_preserve_datarightentryleft dst_negative_code_preserve_datarightentryleft dst_negative_scale_preserve_datarightentryleft dst_positive_preserve_datarightentryleft dst_negative_preserve_datarightentryleft. (((F) = (((((dst_positive_code_preserve_datarightentryleft) + (dst_positive_scale_preserve_datarightentryleft)) * S ((dst_positive_code_preserve_datarightentryleft) + (dst_positive_scale_preserve_datarightentryleft)) + ((dst_positive_scale_preserve_datarightentryleft) + (dst_positive_scale_preserve_datarightentryleft))) + (((dst_negative_code_preserve_datarightentryleft) + (dst_negative_scale_preserve_datarightentryleft)) * S ((dst_negative_code_preserve_datarightentryleft) + (dst_negative_scale_preserve_datarightentryleft)) + ((dst_negative_scale_preserve_datarightentryleft) + (dst_negative_scale_preserve_datarightentryleft)))) * S ((((dst_positive_code_preserve_datarightentryleft) + (dst_positive_scale_preserve_datarightentryleft)) * S ((dst_positive_code_preserve_datarightentryleft) + (dst_positive_scale_preserve_datarightentryleft)) + ((dst_positive_scale_preserve_datarightentryleft) + (dst_positive_scale_preserve_datarightentryleft))) + (((dst_negative_code_preserve_datarightentryleft) + (dst_negative_scale_preserve_datarightentryleft)) * S ((dst_negative_code_preserve_datarightentryleft) + (dst_negative_scale_preserve_datarightentryleft)) + ((dst_negative_scale_preserve_datarightentryleft) + (dst_negative_scale_preserve_datarightentryleft)))) + ((((dst_negative_code_preserve_datarightentryleft) + (dst_negative_scale_preserve_datarightentryleft)) * S ((dst_negative_code_preserve_datarightentryleft) + (dst_negative_scale_preserve_datarightentryleft)) + ((dst_negative_scale_preserve_datarightentryleft) + (dst_negative_scale_preserve_datarightentryleft))) + (((dst_negative_code_preserve_datarightentryleft) + (dst_negative_scale_preserve_datarightentryleft)) * S ((dst_negative_code_preserve_datarightentryleft) + (dst_negative_scale_preserve_datarightentryleft)) + ((dst_negative_scale_preserve_datarightentryleft) + (dst_negative_scale_preserve_datarightentryleft)))))) /\ (((((exists ff_h_pvs_preserve_datarightentryleftpositive. ff_h_pvs_preserve_datarightentryleftpositive + S (dst_positive_preserve_datarightentryleft) = S ((S (dc_index_preserve_dataright)) * dst_positive_scale_preserve_datarightentryleft)) /\ exists ff_q_pvs_preserve_datarightentryleftpositive. dst_positive_code_preserve_datarightentryleft = ff_q_pvs_preserve_datarightentryleftpositive * S ((S (dc_index_preserve_dataright)) * dst_positive_scale_preserve_datarightentryleft) + (dst_positive_preserve_datarightentryleft))) /\ (((((exists ff_h_pvs_preserve_datarightentryleftnegative. ff_h_pvs_preserve_datarightentryleftnegative + S (dst_negative_preserve_datarightentryleft) = S ((S (dc_index_preserve_dataright)) * dst_negative_scale_preserve_datarightentryleft)) /\ exists ff_q_pvs_preserve_datarightentryleftnegative. dst_negative_code_preserve_datarightentryleft = ff_q_pvs_preserve_datarightentryleftnegative * S ((S (dc_index_preserve_dataright)) * dst_negative_scale_preserve_datarightentryleft) + (dst_negative_preserve_datarightentryleft))) /\ (exists ge_balance_positive_preserve_datarightentryleftvalue ge_balance_negative_preserve_datarightentryleftvalue. (((((dc_left_preserve_datarightentry) = 2 * (ge_balance_positive_preserve_datarightentryleftvalue) /\ (ge_balance_negative_preserve_datarightentryleftvalue) = 0) \/ exists ge_signed_half_preserve_datarightentryleftvaluedecode. (((dc_left_preserve_datarightentry) = 2 * ge_signed_half_preserve_datarightentryleftvaluedecode + 1 /\ (ge_balance_positive_preserve_datarightentryleftvalue) = 0) /\ (ge_balance_negative_preserve_datarightentryleftvalue) = S ge_signed_half_preserve_datarightentryleftvaluedecode))) /\ ((dst_positive_preserve_datarightentryleft) + ge_balance_negative_preserve_datarightentryleftvalue = (dst_negative_preserve_datarightentryleft) + ge_balance_positive_preserve_datarightentryleftvalue))))))))) /\ (((exists dst_positive_code_preserve_datarightentryright dst_positive_scale_preserve_datarightentryright dst_negative_code_preserve_datarightentryright dst_negative_scale_preserve_datarightentryright dst_positive_preserve_datarightentryright dst_negative_preserve_datarightentryright. (((G) = (((((dst_positive_code_preserve_datarightentryright) + (dst_positive_scale_preserve_datarightentryright)) * S ((dst_positive_code_preserve_datarightentryright) + (dst_positive_scale_preserve_datarightentryright)) + ((dst_positive_scale_preserve_datarightentryright) + (dst_positive_scale_preserve_datarightentryright))) + (((dst_negative_code_preserve_datarightentryright) + (dst_negative_scale_preserve_datarightentryright)) * S ((dst_negative_code_preserve_datarightentryright) + (dst_negative_scale_preserve_datarightentryright)) + ((dst_negative_scale_preserve_datarightentryright) + (dst_negative_scale_preserve_datarightentryright)))) * S ((((dst_positive_code_preserve_datarightentryright) + (dst_positive_scale_preserve_datarightentryright)) * S ((dst_positive_code_preserve_datarightentryright) + (dst_positive_scale_preserve_datarightentryright)) + ((dst_positive_scale_preserve_datarightentryright) + (dst_positive_scale_preserve_datarightentryright))) + (((dst_negative_code_preserve_datarightentryright) + (dst_negative_scale_preserve_datarightentryright)) * S ((dst_negative_code_preserve_datarightentryright) + (dst_negative_scale_preserve_datarightentryright)) + ((dst_negative_scale_preserve_datarightentryright) + (dst_negative_scale_preserve_datarightentryright)))) + ((((dst_negative_code_preserve_datarightentryright) + (dst_negative_scale_preserve_datarightentryright)) * S ((dst_negative_code_preserve_datarightentryright) + (dst_negative_scale_preserve_datarightentryright)) + ((dst_negative_scale_preserve_datarightentryright) + (dst_negative_scale_preserve_datarightentryright))) + (((dst_negative_code_preserve_datarightentryright) + (dst_negative_scale_preserve_datarightentryright)) * S ((dst_negative_code_preserve_datarightentryright) + (dst_negative_scale_preserve_datarightentryright)) + ((dst_negative_scale_preserve_datarightentryright) + (dst_negative_scale_preserve_datarightentryright)))))) /\ (((((exists ff_h_pvs_preserve_datarightentryrightpositive. ff_h_pvs_preserve_datarightentryrightpositive + S (dst_positive_preserve_datarightentryright) = S ((S (dc_quotient_preserve_datarightentry)) * dst_positive_scale_preserve_datarightentryright)) /\ exists ff_q_pvs_preserve_datarightentryrightpositive. dst_positive_code_preserve_datarightentryright = ff_q_pvs_preserve_datarightentryrightpositive * S ((S (dc_quotient_preserve_datarightentry)) * dst_positive_scale_preserve_datarightentryright) + (dst_positive_preserve_datarightentryright))) /\ (((((exists ff_h_pvs_preserve_datarightentryrightnegative. ff_h_pvs_preserve_datarightentryrightnegative + S (dst_negative_preserve_datarightentryright) = S ((S (dc_quotient_preserve_datarightentry)) * dst_negative_scale_preserve_datarightentryright)) /\ exists ff_q_pvs_preserve_datarightentryrightnegative. dst_negative_code_preserve_datarightentryright = ff_q_pvs_preserve_datarightentryrightnegative * S ((S (dc_quotient_preserve_datarightentry)) * dst_negative_scale_preserve_datarightentryright) + (dst_negative_preserve_datarightentryright))) /\ (exists ge_balance_positive_preserve_datarightentryrightvalue ge_balance_negative_preserve_datarightentryrightvalue. (((((dc_right_preserve_datarightentry) = 2 * (ge_balance_positive_preserve_datarightentryrightvalue) /\ (ge_balance_negative_preserve_datarightentryrightvalue) = 0) \/ exists ge_signed_half_preserve_datarightentryrightvaluedecode. (((dc_right_preserve_datarightentry) = 2 * ge_signed_half_preserve_datarightentryrightvaluedecode + 1 /\ (ge_balance_positive_preserve_datarightentryrightvalue) = 0) /\ (ge_balance_negative_preserve_datarightentryrightvalue) = S ge_signed_half_preserve_datarightentryrightvaluedecode))) /\ ((dst_positive_preserve_datarightentryright) + ge_balance_negative_preserve_datarightentryrightvalue = (dst_negative_preserve_datarightentryright) + ge_balance_positive_preserve_datarightentryrightvalue))))))))) /\ (exists sto_ap_preserve_datarightentryproduct sto_an_preserve_datarightentryproduct sto_bp_preserve_datarightentryproduct sto_bn_preserve_datarightentryproduct sto_cp_preserve_datarightentryproduct sto_cn_preserve_datarightentryproduct. (((((dc_left_preserve_datarightentry) = 2 * (sto_ap_preserve_datarightentryproduct) /\ (sto_an_preserve_datarightentryproduct) = 0) \/ exists ge_signed_half_preserve_datarightentryproductleft. (((dc_left_preserve_datarightentry) = 2 * ge_signed_half_preserve_datarightentryproductleft + 1 /\ (sto_ap_preserve_datarightentryproduct) = 0) /\ (sto_an_preserve_datarightentryproduct) = S ge_signed_half_preserve_datarightentryproductleft))) /\ ((((((dc_right_preserve_datarightentry) = 2 * (sto_bp_preserve_datarightentryproduct) /\ (sto_bn_preserve_datarightentryproduct) = 0) \/ exists ge_signed_half_preserve_datarightentryproductright. (((dc_right_preserve_datarightentry) = 2 * ge_signed_half_preserve_datarightentryproductright + 1 /\ (sto_bp_preserve_datarightentryproduct) = 0) /\ (sto_bn_preserve_datarightentryproduct) = S ge_signed_half_preserve_datarightentryproductright))) /\ ((((((dc_value_preserve_dataright) = 2 * (sto_cp_preserve_datarightentryproduct) /\ (sto_cn_preserve_datarightentryproduct) = 0) \/ exists ge_signed_half_preserve_datarightentryproductoutput. (((dc_value_preserve_dataright) = 2 * ge_signed_half_preserve_datarightentryproductoutput + 1 /\ (sto_cp_preserve_datarightentryproduct) = 0) /\ (sto_cn_preserve_datarightentryproduct) = S ge_signed_half_preserve_datarightentryproductoutput))) /\ ((sto_ap_preserve_datarightentryproduct * sto_bp_preserve_datarightentryproduct + sto_an_preserve_datarightentryproduct * sto_bn_preserve_datarightentryproduct) + sto_cn_preserve_datarightentryproduct = (sto_ap_preserve_datarightentryproduct * sto_bn_preserve_datarightentryproduct + sto_an_preserve_datarightentryproduct * sto_bp_preserve_datarightentryproduct) + sto_cp_preserve_datarightentryproduct))))))))))))))) \/ ((((dc_index_preserve_dataright)=0 \/ ~(exists pvs_factor_preserve_datarightentrynondivisor. (n) = (dc_index_preserve_dataright) * pvs_factor_preserve_datarightentrynondivisor)) /\ ((dc_value_preserve_dataright)=0))))))) /\ (((((exists dst_positive_code_preserve_datacartesianF dst_positive_scale_preserve_datacartesianF dst_negative_code_preserve_datacartesianF dst_negative_scale_preserve_datacartesianF. (((A) = (((((dst_positive_code_preserve_datacartesianF) + (dst_positive_scale_preserve_datacartesianF)) * S ((dst_positive_code_preserve_datacartesianF) + (dst_positive_scale_preserve_datacartesianF)) + ((dst_positive_scale_preserve_datacartesianF) + (dst_positive_scale_preserve_datacartesianF))) + (((dst_negative_code_preserve_datacartesianF) + (dst_negative_scale_preserve_datacartesianF)) * S ((dst_negative_code_preserve_datacartesianF) + (dst_negative_scale_preserve_datacartesianF)) + ((dst_negative_scale_preserve_datacartesianF) + (dst_negative_scale_preserve_datacartesianF)))) * S ((((dst_positive_code_preserve_datacartesianF) + (dst_positive_scale_preserve_datacartesianF)) * S ((dst_positive_code_preserve_datacartesianF) + (dst_positive_scale_preserve_datacartesianF)) + ((dst_positive_scale_preserve_datacartesianF) + (dst_positive_scale_preserve_datacartesianF))) + (((dst_negative_code_preserve_datacartesianF) + (dst_negative_scale_preserve_datacartesianF)) * S ((dst_negative_code_preserve_datacartesianF) + (dst_negative_scale_preserve_datacartesianF)) + ((dst_negative_scale_preserve_datacartesianF) + (dst_negative_scale_preserve_datacartesianF)))) + ((((dst_negative_code_preserve_datacartesianF) + (dst_negative_scale_preserve_datacartesianF)) * S ((dst_negative_code_preserve_datacartesianF) + (dst_negative_scale_preserve_datacartesianF)) + ((dst_negative_scale_preserve_datacartesianF) + (dst_negative_scale_preserve_datacartesianF))) + (((dst_negative_code_preserve_datacartesianF) + (dst_negative_scale_preserve_datacartesianF)) * S ((dst_negative_code_preserve_datacartesianF) + (dst_negative_scale_preserve_datacartesianF)) + ((dst_negative_scale_preserve_datacartesianF) + (dst_negative_scale_preserve_datacartesianF)))))) /\ (forall dst_index_preserve_datacartesianF. (exists pvs_le_gap_preserve_datacartesianFdomain. pvs_le_gap_preserve_datacartesianFdomain + (dst_index_preserve_datacartesianF) = (0)) -> exists dst_positive_preserve_datacartesianF dst_negative_preserve_datacartesianF dst_value_preserve_datacartesianF. ((((exists ff_h_pvs_preserve_datacartesianFentrypositive. ff_h_pvs_preserve_datacartesianFentrypositive + S (dst_positive_preserve_datacartesianF) = S ((S (dst_index_preserve_datacartesianF)) * dst_positive_scale_preserve_datacartesianF)) /\ exists ff_q_pvs_preserve_datacartesianFentrypositive. dst_positive_code_preserve_datacartesianF = ff_q_pvs_preserve_datacartesianFentrypositive * S ((S (dst_index_preserve_datacartesianF)) * dst_positive_scale_preserve_datacartesianF) + (dst_positive_preserve_datacartesianF))) /\ (((((exists ff_h_pvs_preserve_datacartesianFentrynegative. ff_h_pvs_preserve_datacartesianFentrynegative + S (dst_negative_preserve_datacartesianF) = S ((S (dst_index_preserve_datacartesianF)) * dst_negative_scale_preserve_datacartesianF)) /\ exists ff_q_pvs_preserve_datacartesianFentrynegative. dst_negative_code_preserve_datacartesianF = ff_q_pvs_preserve_datacartesianFentrynegative * S ((S (dst_index_preserve_datacartesianF)) * dst_negative_scale_preserve_datacartesianF) + (dst_negative_preserve_datacartesianF))) /\ (exists ge_balance_positive_preserve_datacartesianFentryvalue ge_balance_negative_preserve_datacartesianFentryvalue. (((((dst_value_preserve_datacartesianF) = 2 * (ge_balance_positive_preserve_datacartesianFentryvalue) /\ (ge_balance_negative_preserve_datacartesianFentryvalue) = 0) \/ exists ge_signed_half_preserve_datacartesianFentryvaluedecode. (((dst_value_preserve_datacartesianF) = 2 * ge_signed_half_preserve_datacartesianFentryvaluedecode + 1 /\ (ge_balance_positive_preserve_datacartesianFentryvalue) = 0) /\ (ge_balance_negative_preserve_datacartesianFentryvalue) = S ge_signed_half_preserve_datacartesianFentryvaluedecode))) /\ ((dst_positive_preserve_datacartesianF) + ge_balance_negative_preserve_datacartesianFentryvalue = (dst_negative_preserve_datacartesianF) + ge_balance_positive_preserve_datacartesianFentryvalue))))))))) /\ (((exists dst_positive_code_preserve_datacartesianG dst_positive_scale_preserve_datacartesianG dst_negative_code_preserve_datacartesianG dst_negative_scale_preserve_datacartesianG. (((B) = (((((dst_positive_code_preserve_datacartesianG) + (dst_positive_scale_preserve_datacartesianG)) * S ((dst_positive_code_preserve_datacartesianG) + (dst_positive_scale_preserve_datacartesianG)) + ((dst_positive_scale_preserve_datacartesianG) + (dst_positive_scale_preserve_datacartesianG))) + (((dst_negative_code_preserve_datacartesianG) + (dst_negative_scale_preserve_datacartesianG)) * S ((dst_negative_code_preserve_datacartesianG) + (dst_negative_scale_preserve_datacartesianG)) + ((dst_negative_scale_preserve_datacartesianG) + (dst_negative_scale_preserve_datacartesianG)))) * S ((((dst_positive_code_preserve_datacartesianG) + (dst_positive_scale_preserve_datacartesianG)) * S ((dst_positive_code_preserve_datacartesianG) + (dst_positive_scale_preserve_datacartesianG)) + ((dst_positive_scale_preserve_datacartesianG) + (dst_positive_scale_preserve_datacartesianG))) + (((dst_negative_code_preserve_datacartesianG) + (dst_negative_scale_preserve_datacartesianG)) * S ((dst_negative_code_preserve_datacartesianG) + (dst_negative_scale_preserve_datacartesianG)) + ((dst_negative_scale_preserve_datacartesianG) + (dst_negative_scale_preserve_datacartesianG)))) + ((((dst_negative_code_preserve_datacartesianG) + (dst_negative_scale_preserve_datacartesianG)) * S ((dst_negative_code_preserve_datacartesianG) + (dst_negative_scale_preserve_datacartesianG)) + ((dst_negative_scale_preserve_datacartesianG) + (dst_negative_scale_preserve_datacartesianG))) + (((dst_negative_code_preserve_datacartesianG) + (dst_negative_scale_preserve_datacartesianG)) * S ((dst_negative_code_preserve_datacartesianG) + (dst_negative_scale_preserve_datacartesianG)) + ((dst_negative_scale_preserve_datacartesianG) + (dst_negative_scale_preserve_datacartesianG)))))) /\ (forall dst_index_preserve_datacartesianG. (exists pvs_le_gap_preserve_datacartesianGdomain. pvs_le_gap_preserve_datacartesianGdomain + (dst_index_preserve_datacartesianG) = (0)) -> exists dst_positive_preserve_datacartesianG dst_negative_preserve_datacartesianG dst_value_preserve_datacartesianG. ((((exists ff_h_pvs_preserve_datacartesianGentrypositive. ff_h_pvs_preserve_datacartesianGentrypositive + S (dst_positive_preserve_datacartesianG) = S ((S (dst_index_preserve_datacartesianG)) * dst_positive_scale_preserve_datacartesianG)) /\ exists ff_q_pvs_preserve_datacartesianGentrypositive. dst_positive_code_preserve_datacartesianG = ff_q_pvs_preserve_datacartesianGentrypositive * S ((S (dst_index_preserve_datacartesianG)) * dst_positive_scale_preserve_datacartesianG) + (dst_positive_preserve_datacartesianG))) /\ (((((exists ff_h_pvs_preserve_datacartesianGentrynegative. ff_h_pvs_preserve_datacartesianGentrynegative + S (dst_negative_preserve_datacartesianG) = S ((S (dst_index_preserve_datacartesianG)) * dst_negative_scale_preserve_datacartesianG)) /\ exists ff_q_pvs_preserve_datacartesianGentrynegative. dst_negative_code_preserve_datacartesianG = ff_q_pvs_preserve_datacartesianGentrynegative * S ((S (dst_index_preserve_datacartesianG)) * dst_negative_scale_preserve_datacartesianG) + (dst_negative_preserve_datacartesianG))) /\ (exists ge_balance_positive_preserve_datacartesianGentryvalue ge_balance_negative_preserve_datacartesianGentryvalue. (((((dst_value_preserve_datacartesianG) = 2 * (ge_balance_positive_preserve_datacartesianGentryvalue) /\ (ge_balance_negative_preserve_datacartesianGentryvalue) = 0) \/ exists ge_signed_half_preserve_datacartesianGentryvaluedecode. (((dst_value_preserve_datacartesianG) = 2 * ge_signed_half_preserve_datacartesianGentryvaluedecode + 1 /\ (ge_balance_positive_preserve_datacartesianGentryvalue) = 0) /\ (ge_balance_negative_preserve_datacartesianGentryvalue) = S ge_signed_half_preserve_datacartesianGentryvaluedecode))) /\ ((dst_positive_preserve_datacartesianG) + ge_balance_negative_preserve_datacartesianGentryvalue = (dst_negative_preserve_datacartesianG) + ge_balance_positive_preserve_datacartesianGentryvalue))))))))) /\ (((exists dst_positive_code_preserve_datacartesianT dst_positive_scale_preserve_datacartesianT dst_negative_code_preserve_datacartesianT dst_negative_scale_preserve_datacartesianT. (((T) = (((((dst_positive_code_preserve_datacartesianT) + (dst_positive_scale_preserve_datacartesianT)) * S ((dst_positive_code_preserve_datacartesianT) + (dst_positive_scale_preserve_datacartesianT)) + ((dst_positive_scale_preserve_datacartesianT) + (dst_positive_scale_preserve_datacartesianT))) + (((dst_negative_code_preserve_datacartesianT) + (dst_negative_scale_preserve_datacartesianT)) * S ((dst_negative_code_preserve_datacartesianT) + (dst_negative_scale_preserve_datacartesianT)) + ((dst_negative_scale_preserve_datacartesianT) + (dst_negative_scale_preserve_datacartesianT)))) * S ((((dst_positive_code_preserve_datacartesianT) + (dst_positive_scale_preserve_datacartesianT)) * S ((dst_positive_code_preserve_datacartesianT) + (dst_positive_scale_preserve_datacartesianT)) + ((dst_positive_scale_preserve_datacartesianT) + (dst_positive_scale_preserve_datacartesianT))) + (((dst_negative_code_preserve_datacartesianT) + (dst_negative_scale_preserve_datacartesianT)) * S ((dst_negative_code_preserve_datacartesianT) + (dst_negative_scale_preserve_datacartesianT)) + ((dst_negative_scale_preserve_datacartesianT) + (dst_negative_scale_preserve_datacartesianT)))) + ((((dst_negative_code_preserve_datacartesianT) + (dst_negative_scale_preserve_datacartesianT)) * S ((dst_negative_code_preserve_datacartesianT) + (dst_negative_scale_preserve_datacartesianT)) + ((dst_negative_scale_preserve_datacartesianT) + (dst_negative_scale_preserve_datacartesianT))) + (((dst_negative_code_preserve_datacartesianT) + (dst_negative_scale_preserve_datacartesianT)) * S ((dst_negative_code_preserve_datacartesianT) + (dst_negative_scale_preserve_datacartesianT)) + ((dst_negative_scale_preserve_datacartesianT) + (dst_negative_scale_preserve_datacartesianT)))))) /\ (forall dst_index_preserve_datacartesianT. (exists pvs_le_gap_preserve_datacartesianTdomain. pvs_le_gap_preserve_datacartesianTdomain + (dst_index_preserve_datacartesianT) = ((S (m))*(S (n)))) -> exists dst_positive_preserve_datacartesianT dst_negative_preserve_datacartesianT dst_value_preserve_datacartesianT. ((((exists ff_h_pvs_preserve_datacartesianTentrypositive. ff_h_pvs_preserve_datacartesianTentrypositive + S (dst_positive_preserve_datacartesianT) = S ((S (dst_index_preserve_datacartesianT)) * dst_positive_scale_preserve_datacartesianT)) /\ exists ff_q_pvs_preserve_datacartesianTentrypositive. dst_positive_code_preserve_datacartesianT = ff_q_pvs_preserve_datacartesianTentrypositive * S ((S (dst_index_preserve_datacartesianT)) * dst_positive_scale_preserve_datacartesianT) + (dst_positive_preserve_datacartesianT))) /\ (((((exists ff_h_pvs_preserve_datacartesianTentrynegative. ff_h_pvs_preserve_datacartesianTentrynegative + S (dst_negative_preserve_datacartesianT) = S ((S (dst_index_preserve_datacartesianT)) * dst_negative_scale_preserve_datacartesianT)) /\ exists ff_q_pvs_preserve_datacartesianTentrynegative. dst_negative_code_preserve_datacartesianT = ff_q_pvs_preserve_datacartesianTentrynegative * S ((S (dst_index_preserve_datacartesianT)) * dst_negative_scale_preserve_datacartesianT) + (dst_negative_preserve_datacartesianT))) /\ (exists ge_balance_positive_preserve_datacartesianTentryvalue ge_balance_negative_preserve_datacartesianTentryvalue. (((((dst_value_preserve_datacartesianT) = 2 * (ge_balance_positive_preserve_datacartesianTentryvalue) /\ (ge_balance_negative_preserve_datacartesianTentryvalue) = 0) \/ exists ge_signed_half_preserve_datacartesianTentryvaluedecode. (((dst_value_preserve_datacartesianT) = 2 * ge_signed_half_preserve_datacartesianTentryvaluedecode + 1 /\ (ge_balance_positive_preserve_datacartesianTentryvalue) = 0) /\ (ge_balance_negative_preserve_datacartesianTentryvalue) = S ge_signed_half_preserve_datacartesianTentryvaluedecode))) /\ ((dst_positive_preserve_datacartesianT) + ge_balance_negative_preserve_datacartesianTentryvalue = (dst_negative_preserve_datacartesianT) + ge_balance_positive_preserve_datacartesianTentryvalue))))))))) /\ (forall scp_row_preserve_datacartesian scp_column_preserve_datacartesian scp_first_preserve_datacartesian scp_second_preserve_datacartesian scp_value_preserve_datacartesian. (exists pvs_gap_preserve_datacartesianrows. pvs_gap_preserve_datacartesianrows + S (scp_row_preserve_datacartesian) = (S (m))) -> (exists pvs_gap_preserve_datacartesiancolumns. pvs_gap_preserve_datacartesiancolumns + S (scp_column_preserve_datacartesian) = (S (n))) -> (exists dst_positive_code_preserve_datacartesianfirst dst_positive_scale_preserve_datacartesianfirst dst_negative_code_preserve_datacartesianfirst dst_negative_scale_preserve_datacartesianfirst dst_positive_preserve_datacartesianfirst dst_negative_preserve_datacartesianfirst. (((A) = (((((dst_positive_code_preserve_datacartesianfirst) + (dst_positive_scale_preserve_datacartesianfirst)) * S ((dst_positive_code_preserve_datacartesianfirst) + (dst_positive_scale_preserve_datacartesianfirst)) + ((dst_positive_scale_preserve_datacartesianfirst) + (dst_positive_scale_preserve_datacartesianfirst))) + (((dst_negative_code_preserve_datacartesianfirst) + (dst_negative_scale_preserve_datacartesianfirst)) * S ((dst_negative_code_preserve_datacartesianfirst) + (dst_negative_scale_preserve_datacartesianfirst)) + ((dst_negative_scale_preserve_datacartesianfirst) + (dst_negative_scale_preserve_datacartesianfirst)))) * S ((((dst_positive_code_preserve_datacartesianfirst) + (dst_positive_scale_preserve_datacartesianfirst)) * S ((dst_positive_code_preserve_datacartesianfirst) + (dst_positive_scale_preserve_datacartesianfirst)) + ((dst_positive_scale_preserve_datacartesianfirst) + (dst_positive_scale_preserve_datacartesianfirst))) + (((dst_negative_code_preserve_datacartesianfirst) + (dst_negative_scale_preserve_datacartesianfirst)) * S ((dst_negative_code_preserve_datacartesianfirst) + (dst_negative_scale_preserve_datacartesianfirst)) + ((dst_negative_scale_preserve_datacartesianfirst) + (dst_negative_scale_preserve_datacartesianfirst)))) + ((((dst_negative_code_preserve_datacartesianfirst) + (dst_negative_scale_preserve_datacartesianfirst)) * S ((dst_negative_code_preserve_datacartesianfirst) + (dst_negative_scale_preserve_datacartesianfirst)) + ((dst_negative_scale_preserve_datacartesianfirst) + (dst_negative_scale_preserve_datacartesianfirst))) + (((dst_negative_code_preserve_datacartesianfirst) + (dst_negative_scale_preserve_datacartesianfirst)) * S ((dst_negative_code_preserve_datacartesianfirst) + (dst_negative_scale_preserve_datacartesianfirst)) + ((dst_negative_scale_preserve_datacartesianfirst) + (dst_negative_scale_preserve_datacartesianfirst)))))) /\ (((((exists ff_h_pvs_preserve_datacartesianfirstpositive. ff_h_pvs_preserve_datacartesianfirstpositive + S (dst_positive_preserve_datacartesianfirst) = S ((S (scp_row_preserve_datacartesian)) * dst_positive_scale_preserve_datacartesianfirst)) /\ exists ff_q_pvs_preserve_datacartesianfirstpositive. dst_positive_code_preserve_datacartesianfirst = ff_q_pvs_preserve_datacartesianfirstpositive * S ((S (scp_row_preserve_datacartesian)) * dst_positive_scale_preserve_datacartesianfirst) + (dst_positive_preserve_datacartesianfirst))) /\ (((((exists ff_h_pvs_preserve_datacartesianfirstnegative. ff_h_pvs_preserve_datacartesianfirstnegative + S (dst_negative_preserve_datacartesianfirst) = S ((S (scp_row_preserve_datacartesian)) * dst_negative_scale_preserve_datacartesianfirst)) /\ exists ff_q_pvs_preserve_datacartesianfirstnegative. dst_negative_code_preserve_datacartesianfirst = ff_q_pvs_preserve_datacartesianfirstnegative * S ((S (scp_row_preserve_datacartesian)) * dst_negative_scale_preserve_datacartesianfirst) + (dst_negative_preserve_datacartesianfirst))) /\ (exists ge_balance_positive_preserve_datacartesianfirstvalue ge_balance_negative_preserve_datacartesianfirstvalue. (((((scp_first_preserve_datacartesian) = 2 * (ge_balance_positive_preserve_datacartesianfirstvalue) /\ (ge_balance_negative_preserve_datacartesianfirstvalue) = 0) \/ exists ge_signed_half_preserve_datacartesianfirstvaluedecode. (((scp_first_preserve_datacartesian) = 2 * ge_signed_half_preserve_datacartesianfirstvaluedecode + 1 /\ (ge_balance_positive_preserve_datacartesianfirstvalue) = 0) /\ (ge_balance_negative_preserve_datacartesianfirstvalue) = S ge_signed_half_preserve_datacartesianfirstvaluedecode))) /\ ((dst_positive_preserve_datacartesianfirst) + ge_balance_negative_preserve_datacartesianfirstvalue = (dst_negative_preserve_datacartesianfirst) + ge_balance_positive_preserve_datacartesianfirstvalue))))))))) -> (exists dst_positive_code_preserve_datacartesiansecond dst_positive_scale_preserve_datacartesiansecond dst_negative_code_preserve_datacartesiansecond dst_negative_scale_preserve_datacartesiansecond dst_positive_preserve_datacartesiansecond dst_negative_preserve_datacartesiansecond. (((B) = (((((dst_positive_code_preserve_datacartesiansecond) + (dst_positive_scale_preserve_datacartesiansecond)) * S ((dst_positive_code_preserve_datacartesiansecond) + (dst_positive_scale_preserve_datacartesiansecond)) + ((dst_positive_scale_preserve_datacartesiansecond) + (dst_positive_scale_preserve_datacartesiansecond))) + (((dst_negative_code_preserve_datacartesiansecond) + (dst_negative_scale_preserve_datacartesiansecond)) * S ((dst_negative_code_preserve_datacartesiansecond) + (dst_negative_scale_preserve_datacartesiansecond)) + ((dst_negative_scale_preserve_datacartesiansecond) + (dst_negative_scale_preserve_datacartesiansecond)))) * S ((((dst_positive_code_preserve_datacartesiansecond) + (dst_positive_scale_preserve_datacartesiansecond)) * S ((dst_positive_code_preserve_datacartesiansecond) + (dst_positive_scale_preserve_datacartesiansecond)) + ((dst_positive_scale_preserve_datacartesiansecond) + (dst_positive_scale_preserve_datacartesiansecond))) + (((dst_negative_code_preserve_datacartesiansecond) + (dst_negative_scale_preserve_datacartesiansecond)) * S ((dst_negative_code_preserve_datacartesiansecond) + (dst_negative_scale_preserve_datacartesiansecond)) + ((dst_negative_scale_preserve_datacartesiansecond) + (dst_negative_scale_preserve_datacartesiansecond)))) + ((((dst_negative_code_preserve_datacartesiansecond) + (dst_negative_scale_preserve_datacartesiansecond)) * S ((dst_negative_code_preserve_datacartesiansecond) + (dst_negative_scale_preserve_datacartesiansecond)) + ((dst_negative_scale_preserve_datacartesiansecond) + (dst_negative_scale_preserve_datacartesiansecond))) + (((dst_negative_code_preserve_datacartesiansecond) + (dst_negative_scale_preserve_datacartesiansecond)) * S ((dst_negative_code_preserve_datacartesiansecond) + (dst_negative_scale_preserve_datacartesiansecond)) + ((dst_negative_scale_preserve_datacartesiansecond) + (dst_negative_scale_preserve_datacartesiansecond)))))) /\ (((((exists ff_h_pvs_preserve_datacartesiansecondpositive. ff_h_pvs_preserve_datacartesiansecondpositive + S (dst_positive_preserve_datacartesiansecond) = S ((S (scp_column_preserve_datacartesian)) * dst_positive_scale_preserve_datacartesiansecond)) /\ exists ff_q_pvs_preserve_datacartesiansecondpositive. dst_positive_code_preserve_datacartesiansecond = ff_q_pvs_preserve_datacartesiansecondpositive * S ((S (scp_column_preserve_datacartesian)) * dst_positive_scale_preserve_datacartesiansecond) + (dst_positive_preserve_datacartesiansecond))) /\ (((((exists ff_h_pvs_preserve_datacartesiansecondnegative. ff_h_pvs_preserve_datacartesiansecondnegative + S (dst_negative_preserve_datacartesiansecond) = S ((S (scp_column_preserve_datacartesian)) * dst_negative_scale_preserve_datacartesiansecond)) /\ exists ff_q_pvs_preserve_datacartesiansecondnegative. dst_negative_code_preserve_datacartesiansecond = ff_q_pvs_preserve_datacartesiansecondnegative * S ((S (scp_column_preserve_datacartesian)) * dst_negative_scale_preserve_datacartesiansecond) + (dst_negative_preserve_datacartesiansecond))) /\ (exists ge_balance_positive_preserve_datacartesiansecondvalue ge_balance_negative_preserve_datacartesiansecondvalue. (((((scp_second_preserve_datacartesian) = 2 * (ge_balance_positive_preserve_datacartesiansecondvalue) /\ (ge_balance_negative_preserve_datacartesiansecondvalue) = 0) \/ exists ge_signed_half_preserve_datacartesiansecondvaluedecode. (((scp_second_preserve_datacartesian) = 2 * ge_signed_half_preserve_datacartesiansecondvaluedecode + 1 /\ (ge_balance_positive_preserve_datacartesiansecondvalue) = 0) /\ (ge_balance_negative_preserve_datacartesiansecondvalue) = S ge_signed_half_preserve_datacartesiansecondvaluedecode))) /\ ((dst_positive_preserve_datacartesiansecond) + ge_balance_negative_preserve_datacartesiansecondvalue = (dst_negative_preserve_datacartesiansecond) + ge_balance_positive_preserve_datacartesiansecondvalue))))))))) -> (exists dst_positive_code_preserve_datacartesianentry dst_positive_scale_preserve_datacartesianentry dst_negative_code_preserve_datacartesianentry dst_negative_scale_preserve_datacartesianentry dst_positive_preserve_datacartesianentry dst_negative_preserve_datacartesianentry. (((T) = (((((dst_positive_code_preserve_datacartesianentry) + (dst_positive_scale_preserve_datacartesianentry)) * S ((dst_positive_code_preserve_datacartesianentry) + (dst_positive_scale_preserve_datacartesianentry)) + ((dst_positive_scale_preserve_datacartesianentry) + (dst_positive_scale_preserve_datacartesianentry))) + (((dst_negative_code_preserve_datacartesianentry) + (dst_negative_scale_preserve_datacartesianentry)) * S ((dst_negative_code_preserve_datacartesianentry) + (dst_negative_scale_preserve_datacartesianentry)) + ((dst_negative_scale_preserve_datacartesianentry) + (dst_negative_scale_preserve_datacartesianentry)))) * S ((((dst_positive_code_preserve_datacartesianentry) + (dst_positive_scale_preserve_datacartesianentry)) * S ((dst_positive_code_preserve_datacartesianentry) + (dst_positive_scale_preserve_datacartesianentry)) + ((dst_positive_scale_preserve_datacartesianentry) + (dst_positive_scale_preserve_datacartesianentry))) + (((dst_negative_code_preserve_datacartesianentry) + (dst_negative_scale_preserve_datacartesianentry)) * S ((dst_negative_code_preserve_datacartesianentry) + (dst_negative_scale_preserve_datacartesianentry)) + ((dst_negative_scale_preserve_datacartesianentry) + (dst_negative_scale_preserve_datacartesianentry)))) + ((((dst_negative_code_preserve_datacartesianentry) + (dst_negative_scale_preserve_datacartesianentry)) * S ((dst_negative_code_preserve_datacartesianentry) + (dst_negative_scale_preserve_datacartesianentry)) + ((dst_negative_scale_preserve_datacartesianentry) + (dst_negative_scale_preserve_datacartesianentry))) + (((dst_negative_code_preserve_datacartesianentry) + (dst_negative_scale_preserve_datacartesianentry)) * S ((dst_negative_code_preserve_datacartesianentry) + (dst_negative_scale_preserve_datacartesianentry)) + ((dst_negative_scale_preserve_datacartesianentry) + (dst_negative_scale_preserve_datacartesianentry)))))) /\ (((((exists ff_h_pvs_preserve_datacartesianentrypositive. ff_h_pvs_preserve_datacartesianentrypositive + S (dst_positive_preserve_datacartesianentry) = S ((S (((S (n))*(scp_row_preserve_datacartesian)+(scp_column_preserve_datacartesian)))) * dst_positive_scale_preserve_datacartesianentry)) /\ exists ff_q_pvs_preserve_datacartesianentrypositive. dst_positive_code_preserve_datacartesianentry = ff_q_pvs_preserve_datacartesianentrypositive * S ((S (((S (n))*(scp_row_preserve_datacartesian)+(scp_column_preserve_datacartesian)))) * dst_positive_scale_preserve_datacartesianentry) + (dst_positive_preserve_datacartesianentry))) /\ (((((exists ff_h_pvs_preserve_datacartesianentrynegative. ff_h_pvs_preserve_datacartesianentrynegative + S (dst_negative_preserve_datacartesianentry) = S ((S (((S (n))*(scp_row_preserve_datacartesian)+(scp_column_preserve_datacartesian)))) * dst_negative_scale_preserve_datacartesianentry)) /\ exists ff_q_pvs_preserve_datacartesianentrynegative. dst_negative_code_preserve_datacartesianentry = ff_q_pvs_preserve_datacartesianentrynegative * S ((S (((S (n))*(scp_row_preserve_datacartesian)+(scp_column_preserve_datacartesian)))) * dst_negative_scale_preserve_datacartesianentry) + (dst_negative_preserve_datacartesianentry))) /\ (exists ge_balance_positive_preserve_datacartesianentryvalue ge_balance_negative_preserve_datacartesianentryvalue. (((((scp_value_preserve_datacartesian) = 2 * (ge_balance_positive_preserve_datacartesianentryvalue) /\ (ge_balance_negative_preserve_datacartesianentryvalue) = 0) \/ exists ge_signed_half_preserve_datacartesianentryvaluedecode. (((scp_value_preserve_datacartesian) = 2 * ge_signed_half_preserve_datacartesianentryvaluedecode + 1 /\ (ge_balance_positive_preserve_datacartesianentryvalue) = 0) /\ (ge_balance_negative_preserve_datacartesianentryvalue) = S ge_signed_half_preserve_datacartesianentryvaluedecode))) /\ ((dst_positive_preserve_datacartesianentry) + ge_balance_negative_preserve_datacartesianentryvalue = (dst_negative_preserve_datacartesianentry) + ge_balance_positive_preserve_datacartesianentryvalue))))))))) -> (exists sto_ap_preserve_datacartesianmultiply sto_an_preserve_datacartesianmultiply sto_bp_preserve_datacartesianmultiply sto_bn_preserve_datacartesianmultiply sto_cp_preserve_datacartesianmultiply sto_cn_preserve_datacartesianmultiply. (((((scp_first_preserve_datacartesian) = 2 * (sto_ap_preserve_datacartesianmultiply) /\ (sto_an_preserve_datacartesianmultiply) = 0) \/ exists ge_signed_half_preserve_datacartesianmultiplyleft. (((scp_first_preserve_datacartesian) = 2 * ge_signed_half_preserve_datacartesianmultiplyleft + 1 /\ (sto_ap_preserve_datacartesianmultiply) = 0) /\ (sto_an_preserve_datacartesianmultiply) = S ge_signed_half_preserve_datacartesianmultiplyleft))) /\ ((((((scp_second_preserve_datacartesian) = 2 * (sto_bp_preserve_datacartesianmultiply) /\ (sto_bn_preserve_datacartesianmultiply) = 0) \/ exists ge_signed_half_preserve_datacartesianmultiplyright. (((scp_second_preserve_datacartesian) = 2 * ge_signed_half_preserve_datacartesianmultiplyright + 1 /\ (sto_bp_preserve_datacartesianmultiply) = 0) /\ (sto_bn_preserve_datacartesianmultiply) = S ge_signed_half_preserve_datacartesianmultiplyright))) /\ ((((((scp_value_preserve_datacartesian) = 2 * (sto_cp_preserve_datacartesianmultiply) /\ (sto_cn_preserve_datacartesianmultiply) = 0) \/ exists ge_signed_half_preserve_datacartesianmultiplyoutput. (((scp_value_preserve_datacartesian) = 2 * ge_signed_half_preserve_datacartesianmultiplyoutput + 1 /\ (sto_cp_preserve_datacartesianmultiply) = 0) /\ (sto_cn_preserve_datacartesianmultiply) = S ge_signed_half_preserve_datacartesianmultiplyoutput))) /\ ((sto_ap_preserve_datacartesianmultiply * sto_bp_preserve_datacartesianmultiply + sto_an_preserve_datacartesianmultiply * sto_bn_preserve_datacartesianmultiply) + sto_cn_preserve_datacartesianmultiply = (sto_ap_preserve_datacartesianmultiply * sto_bn_preserve_datacartesianmultiply + sto_an_preserve_datacartesianmultiply * sto_bp_preserve_datacartesianmultiply) + sto_cp_preserve_datacartesianmultiply)))))))))))))) /\ (((((exists dst_positive_code_preserve_datatargettable dst_positive_scale_preserve_datatargettable dst_negative_code_preserve_datatargettable dst_negative_scale_preserve_datatargettable. (((Q) = (((((dst_positive_code_preserve_datatargettable) + (dst_positive_scale_preserve_datatargettable)) * S ((dst_positive_code_preserve_datatargettable) + (dst_positive_scale_preserve_datatargettable)) + ((dst_positive_scale_preserve_datatargettable) + (dst_positive_scale_preserve_datatargettable))) + (((dst_negative_code_preserve_datatargettable) + (dst_negative_scale_preserve_datatargettable)) * S ((dst_negative_code_preserve_datatargettable) + (dst_negative_scale_preserve_datatargettable)) + ((dst_negative_scale_preserve_datatargettable) + (dst_negative_scale_preserve_datatargettable)))) * S ((((dst_positive_code_preserve_datatargettable) + (dst_positive_scale_preserve_datatargettable)) * S ((dst_positive_code_preserve_datatargettable) + (dst_positive_scale_preserve_datatargettable)) + ((dst_positive_scale_preserve_datatargettable) + (dst_positive_scale_preserve_datatargettable))) + (((dst_negative_code_preserve_datatargettable) + (dst_negative_scale_preserve_datatargettable)) * S ((dst_negative_code_preserve_datatargettable) + (dst_negative_scale_preserve_datatargettable)) + ((dst_negative_scale_preserve_datatargettable) + (dst_negative_scale_preserve_datatargettable)))) + ((((dst_negative_code_preserve_datatargettable) + (dst_negative_scale_preserve_datatargettable)) * S ((dst_negative_code_preserve_datatargettable) + (dst_negative_scale_preserve_datatargettable)) + ((dst_negative_scale_preserve_datatargettable) + (dst_negative_scale_preserve_datatargettable))) + (((dst_negative_code_preserve_datatargettable) + (dst_negative_scale_preserve_datatargettable)) * S ((dst_negative_code_preserve_datatargettable) + (dst_negative_scale_preserve_datatargettable)) + ((dst_negative_scale_preserve_datatargettable) + (dst_negative_scale_preserve_datatargettable)))))) /\ (forall dst_index_preserve_datatargettable. (exists pvs_le_gap_preserve_datatargettabledomain. pvs_le_gap_preserve_datatargettabledomain + (dst_index_preserve_datatargettable) = ((m)*(n))) -> exists dst_positive_preserve_datatargettable dst_negative_preserve_datatargettable dst_value_preserve_datatargettable. ((((exists ff_h_pvs_preserve_datatargettableentrypositive. ff_h_pvs_preserve_datatargettableentrypositive + S (dst_positive_preserve_datatargettable) = S ((S (dst_index_preserve_datatargettable)) * dst_positive_scale_preserve_datatargettable)) /\ exists ff_q_pvs_preserve_datatargettableentrypositive. dst_positive_code_preserve_datatargettable = ff_q_pvs_preserve_datatargettableentrypositive * S ((S (dst_index_preserve_datatargettable)) * dst_positive_scale_preserve_datatargettable) + (dst_positive_preserve_datatargettable))) /\ (((((exists ff_h_pvs_preserve_datatargettableentrynegative. ff_h_pvs_preserve_datatargettableentrynegative + S (dst_negative_preserve_datatargettable) = S ((S (dst_index_preserve_datatargettable)) * dst_negative_scale_preserve_datatargettable)) /\ exists ff_q_pvs_preserve_datatargettableentrynegative. dst_negative_code_preserve_datatargettable = ff_q_pvs_preserve_datatargettableentrynegative * S ((S (dst_index_preserve_datatargettable)) * dst_negative_scale_preserve_datatargettable) + (dst_negative_preserve_datatargettable))) /\ (exists ge_balance_positive_preserve_datatargettableentryvalue ge_balance_negative_preserve_datatargettableentryvalue. (((((dst_value_preserve_datatargettable) = 2 * (ge_balance_positive_preserve_datatargettableentryvalue) /\ (ge_balance_negative_preserve_datatargettableentryvalue) = 0) \/ exists ge_signed_half_preserve_datatargettableentryvaluedecode. (((dst_value_preserve_datatargettable) = 2 * ge_signed_half_preserve_datatargettableentryvaluedecode + 1 /\ (ge_balance_positive_preserve_datatargettableentryvalue) = 0) /\ (ge_balance_negative_preserve_datatargettableentryvalue) = S ge_signed_half_preserve_datatargettableentryvaluedecode))) /\ ((dst_positive_preserve_datatargettable) + ge_balance_negative_preserve_datatargettableentryvalue = (dst_negative_preserve_datatargettable) + ge_balance_positive_preserve_datatargettableentryvalue))))))))) /\ (forall dc_index_preserve_datatarget dc_value_preserve_datatarget. (exists pvs_le_gap_preserve_datatargetdomain. pvs_le_gap_preserve_datatargetdomain + (dc_index_preserve_datatarget) = ((m)*(n))) -> (exists dst_positive_code_preserve_datatargetlookup dst_positive_scale_preserve_datatargetlookup dst_negative_code_preserve_datatargetlookup dst_negative_scale_preserve_datatargetlookup dst_positive_preserve_datatargetlookup dst_negative_preserve_datatargetlookup. (((Q) = (((((dst_positive_code_preserve_datatargetlookup) + (dst_positive_scale_preserve_datatargetlookup)) * S ((dst_positive_code_preserve_datatargetlookup) + (dst_positive_scale_preserve_datatargetlookup)) + ((dst_positive_scale_preserve_datatargetlookup) + (dst_positive_scale_preserve_datatargetlookup))) + (((dst_negative_code_preserve_datatargetlookup) + (dst_negative_scale_preserve_datatargetlookup)) * S ((dst_negative_code_preserve_datatargetlookup) + (dst_negative_scale_preserve_datatargetlookup)) + ((dst_negative_scale_preserve_datatargetlookup) + (dst_negative_scale_preserve_datatargetlookup)))) * S ((((dst_positive_code_preserve_datatargetlookup) + (dst_positive_scale_preserve_datatargetlookup)) * S ((dst_positive_code_preserve_datatargetlookup) + (dst_positive_scale_preserve_datatargetlookup)) + ((dst_positive_scale_preserve_datatargetlookup) + (dst_positive_scale_preserve_datatargetlookup))) + (((dst_negative_code_preserve_datatargetlookup) + (dst_negative_scale_preserve_datatargetlookup)) * S ((dst_negative_code_preserve_datatargetlookup) + (dst_negative_scale_preserve_datatargetlookup)) + ((dst_negative_scale_preserve_datatargetlookup) + (dst_negative_scale_preserve_datatargetlookup)))) + ((((dst_negative_code_preserve_datatargetlookup) + (dst_negative_scale_preserve_datatargetlookup)) * S ((dst_negative_code_preserve_datatargetlookup) + (dst_negative_scale_preserve_datatargetlookup)) + ((dst_negative_scale_preserve_datatargetlookup) + (dst_negative_scale_preserve_datatargetlookup))) + (((dst_negative_code_preserve_datatargetlookup) + (dst_negative_scale_preserve_datatargetlookup)) * S ((dst_negative_code_preserve_datatargetlookup) + (dst_negative_scale_preserve_datatargetlookup)) + ((dst_negative_scale_preserve_datatargetlookup) + (dst_negative_scale_preserve_datatargetlookup)))))) /\ (((((exists ff_h_pvs_preserve_datatargetlookuppositive. ff_h_pvs_preserve_datatargetlookuppositive + S (dst_positive_preserve_datatargetlookup) = S ((S (dc_index_preserve_datatarget)) * dst_positive_scale_preserve_datatargetlookup)) /\ exists ff_q_pvs_preserve_datatargetlookuppositive. dst_positive_code_preserve_datatargetlookup = ff_q_pvs_preserve_datatargetlookuppositive * S ((S (dc_index_preserve_datatarget)) * dst_positive_scale_preserve_datatargetlookup) + (dst_positive_preserve_datatargetlookup))) /\ (((((exists ff_h_pvs_preserve_datatargetlookupnegative. ff_h_pvs_preserve_datatargetlookupnegative + S (dst_negative_preserve_datatargetlookup) = S ((S (dc_index_preserve_datatarget)) * dst_negative_scale_preserve_datatargetlookup)) /\ exists ff_q_pvs_preserve_datatargetlookupnegative. dst_negative_code_preserve_datatargetlookup = ff_q_pvs_preserve_datatargetlookupnegative * S ((S (dc_index_preserve_datatarget)) * dst_negative_scale_preserve_datatargetlookup) + (dst_negative_preserve_datatargetlookup))) /\ (exists ge_balance_positive_preserve_datatargetlookupvalue ge_balance_negative_preserve_datatargetlookupvalue. (((((dc_value_preserve_datatarget) = 2 * (ge_balance_positive_preserve_datatargetlookupvalue) /\ (ge_balance_negative_preserve_datatargetlookupvalue) = 0) \/ exists ge_signed_half_preserve_datatargetlookupvaluedecode. (((dc_value_preserve_datatarget) = 2 * ge_signed_half_preserve_datatargetlookupvaluedecode + 1 /\ (ge_balance_positive_preserve_datatargetlookupvalue) = 0) /\ (ge_balance_negative_preserve_datatargetlookupvalue) = S ge_signed_half_preserve_datatargetlookupvaluedecode))) /\ ((dst_positive_preserve_datatargetlookup) + ge_balance_negative_preserve_datatargetlookupvalue = (dst_negative_preserve_datatargetlookup) + ge_balance_positive_preserve_datatargetlookupvalue))))))))) -> ((((~((dc_index_preserve_datatarget)=0)) /\ (exists dc_quotient_preserve_datatargetentry dc_left_preserve_datatargetentry dc_right_preserve_datatargetentry. ((((m)*(n))=(dc_index_preserve_datatarget)*dc_quotient_preserve_datatargetentry) /\ (((exists dst_positive_code_preserve_datatargetentryleft dst_positive_scale_preserve_datatargetentryleft dst_negative_code_preserve_datatargetentryleft dst_negative_scale_preserve_datatargetentryleft dst_positive_preserve_datatargetentryleft dst_negative_preserve_datatargetentryleft. (((F) = (((((dst_positive_code_preserve_datatargetentryleft) + (dst_positive_scale_preserve_datatargetentryleft)) * S ((dst_positive_code_preserve_datatargetentryleft) + (dst_positive_scale_preserve_datatargetentryleft)) + ((dst_positive_scale_preserve_datatargetentryleft) + (dst_positive_scale_preserve_datatargetentryleft))) + (((dst_negative_code_preserve_datatargetentryleft) + (dst_negative_scale_preserve_datatargetentryleft)) * S ((dst_negative_code_preserve_datatargetentryleft) + (dst_negative_scale_preserve_datatargetentryleft)) + ((dst_negative_scale_preserve_datatargetentryleft) + (dst_negative_scale_preserve_datatargetentryleft)))) * S ((((dst_positive_code_preserve_datatargetentryleft) + (dst_positive_scale_preserve_datatargetentryleft)) * S ((dst_positive_code_preserve_datatargetentryleft) + (dst_positive_scale_preserve_datatargetentryleft)) + ((dst_positive_scale_preserve_datatargetentryleft) + (dst_positive_scale_preserve_datatargetentryleft))) + (((dst_negative_code_preserve_datatargetentryleft) + (dst_negative_scale_preserve_datatargetentryleft)) * S ((dst_negative_code_preserve_datatargetentryleft) + (dst_negative_scale_preserve_datatargetentryleft)) + ((dst_negative_scale_preserve_datatargetentryleft) + (dst_negative_scale_preserve_datatargetentryleft)))) + ((((dst_negative_code_preserve_datatargetentryleft) + (dst_negative_scale_preserve_datatargetentryleft)) * S ((dst_negative_code_preserve_datatargetentryleft) + (dst_negative_scale_preserve_datatargetentryleft)) + ((dst_negative_scale_preserve_datatargetentryleft) + (dst_negative_scale_preserve_datatargetentryleft))) + (((dst_negative_code_preserve_datatargetentryleft) + (dst_negative_scale_preserve_datatargetentryleft)) * S ((dst_negative_code_preserve_datatargetentryleft) + (dst_negative_scale_preserve_datatargetentryleft)) + ((dst_negative_scale_preserve_datatargetentryleft) + (dst_negative_scale_preserve_datatargetentryleft)))))) /\ (((((exists ff_h_pvs_preserve_datatargetentryleftpositive. ff_h_pvs_preserve_datatargetentryleftpositive + S (dst_positive_preserve_datatargetentryleft) = S ((S (dc_index_preserve_datatarget)) * dst_positive_scale_preserve_datatargetentryleft)) /\ exists ff_q_pvs_preserve_datatargetentryleftpositive. dst_positive_code_preserve_datatargetentryleft = ff_q_pvs_preserve_datatargetentryleftpositive * S ((S (dc_index_preserve_datatarget)) * dst_positive_scale_preserve_datatargetentryleft) + (dst_positive_preserve_datatargetentryleft))) /\ (((((exists ff_h_pvs_preserve_datatargetentryleftnegative. ff_h_pvs_preserve_datatargetentryleftnegative + S (dst_negative_preserve_datatargetentryleft) = S ((S (dc_index_preserve_datatarget)) * dst_negative_scale_preserve_datatargetentryleft)) /\ exists ff_q_pvs_preserve_datatargetentryleftnegative. dst_negative_code_preserve_datatargetentryleft = ff_q_pvs_preserve_datatargetentryleftnegative * S ((S (dc_index_preserve_datatarget)) * dst_negative_scale_preserve_datatargetentryleft) + (dst_negative_preserve_datatargetentryleft))) /\ (exists ge_balance_positive_preserve_datatargetentryleftvalue ge_balance_negative_preserve_datatargetentryleftvalue. (((((dc_left_preserve_datatargetentry) = 2 * (ge_balance_positive_preserve_datatargetentryleftvalue) /\ (ge_balance_negative_preserve_datatargetentryleftvalue) = 0) \/ exists ge_signed_half_preserve_datatargetentryleftvaluedecode. (((dc_left_preserve_datatargetentry) = 2 * ge_signed_half_preserve_datatargetentryleftvaluedecode + 1 /\ (ge_balance_positive_preserve_datatargetentryleftvalue) = 0) /\ (ge_balance_negative_preserve_datatargetentryleftvalue) = S ge_signed_half_preserve_datatargetentryleftvaluedecode))) /\ ((dst_positive_preserve_datatargetentryleft) + ge_balance_negative_preserve_datatargetentryleftvalue = (dst_negative_preserve_datatargetentryleft) + ge_balance_positive_preserve_datatargetentryleftvalue))))))))) /\ (((exists dst_positive_code_preserve_datatargetentryright dst_positive_scale_preserve_datatargetentryright dst_negative_code_preserve_datatargetentryright dst_negative_scale_preserve_datatargetentryright dst_positive_preserve_datatargetentryright dst_negative_preserve_datatargetentryright. (((G) = (((((dst_positive_code_preserve_datatargetentryright) + (dst_positive_scale_preserve_datatargetentryright)) * S ((dst_positive_code_preserve_datatargetentryright) + (dst_positive_scale_preserve_datatargetentryright)) + ((dst_positive_scale_preserve_datatargetentryright) + (dst_positive_scale_preserve_datatargetentryright))) + (((dst_negative_code_preserve_datatargetentryright) + (dst_negative_scale_preserve_datatargetentryright)) * S ((dst_negative_code_preserve_datatargetentryright) + (dst_negative_scale_preserve_datatargetentryright)) + ((dst_negative_scale_preserve_datatargetentryright) + (dst_negative_scale_preserve_datatargetentryright)))) * S ((((dst_positive_code_preserve_datatargetentryright) + (dst_positive_scale_preserve_datatargetentryright)) * S ((dst_positive_code_preserve_datatargetentryright) + (dst_positive_scale_preserve_datatargetentryright)) + ((dst_positive_scale_preserve_datatargetentryright) + (dst_positive_scale_preserve_datatargetentryright))) + (((dst_negative_code_preserve_datatargetentryright) + (dst_negative_scale_preserve_datatargetentryright)) * S ((dst_negative_code_preserve_datatargetentryright) + (dst_negative_scale_preserve_datatargetentryright)) + ((dst_negative_scale_preserve_datatargetentryright) + (dst_negative_scale_preserve_datatargetentryright)))) + ((((dst_negative_code_preserve_datatargetentryright) + (dst_negative_scale_preserve_datatargetentryright)) * S ((dst_negative_code_preserve_datatargetentryright) + (dst_negative_scale_preserve_datatargetentryright)) + ((dst_negative_scale_preserve_datatargetentryright) + (dst_negative_scale_preserve_datatargetentryright))) + (((dst_negative_code_preserve_datatargetentryright) + (dst_negative_scale_preserve_datatargetentryright)) * S ((dst_negative_code_preserve_datatargetentryright) + (dst_negative_scale_preserve_datatargetentryright)) + ((dst_negative_scale_preserve_datatargetentryright) + (dst_negative_scale_preserve_datatargetentryright)))))) /\ (((((exists ff_h_pvs_preserve_datatargetentryrightpositive. ff_h_pvs_preserve_datatargetentryrightpositive + S (dst_positive_preserve_datatargetentryright) = S ((S (dc_quotient_preserve_datatargetentry)) * dst_positive_scale_preserve_datatargetentryright)) /\ exists ff_q_pvs_preserve_datatargetentryrightpositive. dst_positive_code_preserve_datatargetentryright = ff_q_pvs_preserve_datatargetentryrightpositive * S ((S (dc_quotient_preserve_datatargetentry)) * dst_positive_scale_preserve_datatargetentryright) + (dst_positive_preserve_datatargetentryright))) /\ (((((exists ff_h_pvs_preserve_datatargetentryrightnegative. ff_h_pvs_preserve_datatargetentryrightnegative + S (dst_negative_preserve_datatargetentryright) = S ((S (dc_quotient_preserve_datatargetentry)) * dst_negative_scale_preserve_datatargetentryright)) /\ exists ff_q_pvs_preserve_datatargetentryrightnegative. dst_negative_code_preserve_datatargetentryright = ff_q_pvs_preserve_datatargetentryrightnegative * S ((S (dc_quotient_preserve_datatargetentry)) * dst_negative_scale_preserve_datatargetentryright) + (dst_negative_preserve_datatargetentryright))) /\ (exists ge_balance_positive_preserve_datatargetentryrightvalue ge_balance_negative_preserve_datatargetentryrightvalue. (((((dc_right_preserve_datatargetentry) = 2 * (ge_balance_positive_preserve_datatargetentryrightvalue) /\ (ge_balance_negative_preserve_datatargetentryrightvalue) = 0) \/ exists ge_signed_half_preserve_datatargetentryrightvaluedecode. (((dc_right_preserve_datatargetentry) = 2 * ge_signed_half_preserve_datatargetentryrightvaluedecode + 1 /\ (ge_balance_positive_preserve_datatargetentryrightvalue) = 0) /\ (ge_balance_negative_preserve_datatargetentryrightvalue) = S ge_signed_half_preserve_datatargetentryrightvaluedecode))) /\ ((dst_positive_preserve_datatargetentryright) + ge_balance_negative_preserve_datatargetentryrightvalue = (dst_negative_preserve_datatargetentryright) + ge_balance_positive_preserve_datatargetentryrightvalue))))))))) /\ (exists sto_ap_preserve_datatargetentryproduct sto_an_preserve_datatargetentryproduct sto_bp_preserve_datatargetentryproduct sto_bn_preserve_datatargetentryproduct sto_cp_preserve_datatargetentryproduct sto_cn_preserve_datatargetentryproduct. (((((dc_left_preserve_datatargetentry) = 2 * (sto_ap_preserve_datatargetentryproduct) /\ (sto_an_preserve_datatargetentryproduct) = 0) \/ exists ge_signed_half_preserve_datatargetentryproductleft. (((dc_left_preserve_datatargetentry) = 2 * ge_signed_half_preserve_datatargetentryproductleft + 1 /\ (sto_ap_preserve_datatargetentryproduct) = 0) /\ (sto_an_preserve_datatargetentryproduct) = S ge_signed_half_preserve_datatargetentryproductleft))) /\ ((((((dc_right_preserve_datatargetentry) = 2 * (sto_bp_preserve_datatargetentryproduct) /\ (sto_bn_preserve_datatargetentryproduct) = 0) \/ exists ge_signed_half_preserve_datatargetentryproductright. (((dc_right_preserve_datatargetentry) = 2 * ge_signed_half_preserve_datatargetentryproductright + 1 /\ (sto_bp_preserve_datatargetentryproduct) = 0) /\ (sto_bn_preserve_datatargetentryproduct) = S ge_signed_half_preserve_datatargetentryproductright))) /\ ((((((dc_value_preserve_datatarget) = 2 * (sto_cp_preserve_datatargetentryproduct) /\ (sto_cn_preserve_datatargetentryproduct) = 0) \/ exists ge_signed_half_preserve_datatargetentryproductoutput. (((dc_value_preserve_datatarget) = 2 * ge_signed_half_preserve_datatargetentryproductoutput + 1 /\ (sto_cp_preserve_datatargetentryproduct) = 0) /\ (sto_cn_preserve_datatargetentryproduct) = S ge_signed_half_preserve_datatargetentryproductoutput))) /\ ((sto_ap_preserve_datatargetentryproduct * sto_bp_preserve_datatargetentryproduct + sto_an_preserve_datatargetentryproduct * sto_bn_preserve_datatargetentryproduct) + sto_cn_preserve_datatargetentryproduct = (sto_ap_preserve_datatargetentryproduct * sto_bn_preserve_datatargetentryproduct + sto_an_preserve_datatargetentryproduct * sto_bp_preserve_datatargetentryproduct) + sto_cp_preserve_datatargetentryproduct))))))))))))))) \/ ((((dc_index_preserve_datatarget)=0 \/ ~(exists pvs_factor_preserve_datatargetentrynondivisor. ((m)*(n)) = (dc_index_preserve_datatarget) * pvs_factor_preserve_datatargetentrynondivisor)) /\ ((dc_value_preserve_datatarget)=0))))))) /\ (((~((S (n))=0)) /\ (forall dpi_index_preserve_datamap dpi_row_preserve_datamap dpi_column_preserve_datamap. (exists pvs_gap_preserve_datamapwindow. pvs_gap_preserve_datamapwindow + S (dpi_index_preserve_datamap) = ((S (m))*(S (n)))) -> (exists pvs_gap_preserve_datamapremainder. pvs_gap_preserve_datamapremainder + S (dpi_column_preserve_datamap) = (S (n))) -> (dpi_index_preserve_datamap)=(S (n))*(dpi_row_preserve_datamap)+(dpi_column_preserve_datamap) -> (((exists ff_h_pvs_preserve_datamapvalue. ff_h_pvs_preserve_datamapvalue + S ((dpi_row_preserve_datamap)*(dpi_column_preserve_datamap)) = S ((S (dpi_index_preserve_datamap)) * s)) /\ exists ff_q_pvs_preserve_datamapvalue. r = ff_q_pvs_preserve_datamapvalue * S ((S (dpi_index_preserve_datamap)) * s) + ((dpi_row_preserve_datamap)*(dpi_column_preserve_datamap))))))))))))))))))))))))))) -> (forall ssr_source_preserve_result ssr_value_preserve_result. (exists pvs_gap_preserve_resultsource_bound. pvs_gap_preserve_resultsource_bound + S (ssr_source_preserve_result) = ((S (m))*(S (n)))) -> (exists dst_positive_code_preserve_resultsource_value dst_positive_scale_preserve_resultsource_value dst_negative_code_preserve_resultsource_value dst_negative_scale_preserve_resultsource_value dst_positive_preserve_resultsource_value dst_negative_preserve_resultsource_value. (((T) = (((((dst_positive_code_preserve_resultsource_value) + (dst_positive_scale_preserve_resultsource_value)) * S ((dst_positive_code_preserve_resultsource_value) + (dst_positive_scale_preserve_resultsource_value)) + ((dst_positive_scale_preserve_resultsource_value) + (dst_positive_scale_preserve_resultsource_value))) + (((dst_negative_code_preserve_resultsource_value) + (dst_negative_scale_preserve_resultsource_value)) * S ((dst_negative_code_preserve_resultsource_value) + (dst_negative_scale_preserve_resultsource_value)) + ((dst_negative_scale_preserve_resultsource_value) + (dst_negative_scale_preserve_resultsource_value)))) * S ((((dst_positive_code_preserve_resultsource_value) + (dst_positive_scale_preserve_resultsource_value)) * S ((dst_positive_code_preserve_resultsource_value) + (dst_positive_scale_preserve_resultsource_value)) + ((dst_positive_scale_preserve_resultsource_value) + (dst_positive_scale_preserve_resultsource_value))) + (((dst_negative_code_preserve_resultsource_value) + (dst_negative_scale_preserve_resultsource_value)) * S ((dst_negative_code_preserve_resultsource_value) + (dst_negative_scale_preserve_resultsource_value)) + ((dst_negative_scale_preserve_resultsource_value) + (dst_negative_scale_preserve_resultsource_value)))) + ((((dst_negative_code_preserve_resultsource_value) + (dst_negative_scale_preserve_resultsource_value)) * S ((dst_negative_code_preserve_resultsource_value) + (dst_negative_scale_preserve_resultsource_value)) + ((dst_negative_scale_preserve_resultsource_value) + (dst_negative_scale_preserve_resultsource_value))) + (((dst_negative_code_preserve_resultsource_value) + (dst_negative_scale_preserve_resultsource_value)) * S ((dst_negative_code_preserve_resultsource_value) + (dst_negative_scale_preserve_resultsource_value)) + ((dst_negative_scale_preserve_resultsource_value) + (dst_negative_scale_preserve_resultsource_value)))))) /\ (((((exists ff_h_pvs_preserve_resultsource_valuepositive. ff_h_pvs_preserve_resultsource_valuepositive + S (dst_positive_preserve_resultsource_value) = S ((S (ssr_source_preserve_result)) * dst_positive_scale_preserve_resultsource_value)) /\ exists ff_q_pvs_preserve_resultsource_valuepositive. dst_positive_code_preserve_resultsource_value = ff_q_pvs_preserve_resultsource_valuepositive * S ((S (ssr_source_preserve_result)) * dst_positive_scale_preserve_resultsource_value) + (dst_positive_preserve_resultsource_value))) /\ (((((exists ff_h_pvs_preserve_resultsource_valuenegative. ff_h_pvs_preserve_resultsource_valuenegative + S (dst_negative_preserve_resultsource_value) = S ((S (ssr_source_preserve_result)) * dst_negative_scale_preserve_resultsource_value)) /\ exists ff_q_pvs_preserve_resultsource_valuenegative. dst_negative_code_preserve_resultsource_value = ff_q_pvs_preserve_resultsource_valuenegative * S ((S (ssr_source_preserve_result)) * dst_negative_scale_preserve_resultsource_value) + (dst_negative_preserve_resultsource_value))) /\ (exists ge_balance_positive_preserve_resultsource_valuevalue ge_balance_negative_preserve_resultsource_valuevalue. (((((ssr_value_preserve_result) = 2 * (ge_balance_positive_preserve_resultsource_valuevalue) /\ (ge_balance_negative_preserve_resultsource_valuevalue) = 0) \/ exists ge_signed_half_preserve_resultsource_valuevaluedecode. (((ssr_value_preserve_result) = 2 * ge_signed_half_preserve_resultsource_valuevaluedecode + 1 /\ (ge_balance_positive_preserve_resultsource_valuevalue) = 0) /\ (ge_balance_negative_preserve_resultsource_valuevalue) = S ge_signed_half_preserve_resultsource_valuevaluedecode))) /\ ((dst_positive_preserve_resultsource_value) + ge_balance_negative_preserve_resultsource_valuevalue = (dst_negative_preserve_resultsource_value) + ge_balance_positive_preserve_resultsource_valuevalue))))))))) -> ~(ssr_value_preserve_result=0) -> exists ssr_target_preserve_result. ((((exists ff_h_pvs_preserve_resultmap. ff_h_pvs_preserve_resultmap + S (ssr_target_preserve_result) = S ((S (ssr_source_preserve_result)) * s)) /\ exists ff_q_pvs_preserve_resultmap. r = ff_q_pvs_preserve_resultmap * S ((S (ssr_source_preserve_result)) * s) + (ssr_target_preserve_result))) /\ (((exists pvs_gap_preserve_resulttarget_bound. pvs_gap_preserve_resulttarget_bound + S (ssr_target_preserve_result) = (S (m*n))) /\ (exists dst_positive_code_preserve_resulttarget_value dst_positive_scale_preserve_resulttarget_value dst_negative_code_preserve_resulttarget_value dst_negative_scale_preserve_resulttarget_value dst_positive_preserve_resulttarget_value dst_negative_preserve_resulttarget_value. (((Q) = (((((dst_positive_code_preserve_resulttarget_value) + (dst_positive_scale_preserve_resulttarget_value)) * S ((dst_positive_code_preserve_resulttarget_value) + (dst_positive_scale_preserve_resulttarget_value)) + ((dst_positive_scale_preserve_resulttarget_value) + (dst_positive_scale_preserve_resulttarget_value))) + (((dst_negative_code_preserve_resulttarget_value) + (dst_negative_scale_preserve_resulttarget_value)) * S ((dst_negative_code_preserve_resulttarget_value) + (dst_negative_scale_preserve_resulttarget_value)) + ((dst_negative_scale_preserve_resulttarget_value) + (dst_negative_scale_preserve_resulttarget_value)))) * S ((((dst_positive_code_preserve_resulttarget_value) + (dst_positive_scale_preserve_resulttarget_value)) * S ((dst_positive_code_preserve_resulttarget_value) + (dst_positive_scale_preserve_resulttarget_value)) + ((dst_positive_scale_preserve_resulttarget_value) + (dst_positive_scale_preserve_resulttarget_value))) + (((dst_negative_code_preserve_resulttarget_value) + (dst_negative_scale_preserve_resulttarget_value)) * S ((dst_negative_code_preserve_resulttarget_value) + (dst_negative_scale_preserve_resulttarget_value)) + ((dst_negative_scale_preserve_resulttarget_value) + (dst_negative_scale_preserve_resulttarget_value)))) + ((((dst_negative_code_preserve_resulttarget_value) + (dst_negative_scale_preserve_resulttarget_value)) * S ((dst_negative_code_preserve_resulttarget_value) + (dst_negative_scale_preserve_resulttarget_value)) + ((dst_negative_scale_preserve_resulttarget_value) + (dst_negative_scale_preserve_resulttarget_value))) + (((dst_negative_code_preserve_resulttarget_value) + (dst_negative_scale_preserve_resulttarget_value)) * S ((dst_negative_code_preserve_resulttarget_value) + (dst_negative_scale_preserve_resulttarget_value)) + ((dst_negative_scale_preserve_resulttarget_value) + (dst_negative_scale_preserve_resulttarget_value)))))) /\ (((((exists ff_h_pvs_preserve_resulttarget_valuepositive. ff_h_pvs_preserve_resulttarget_valuepositive + S (dst_positive_preserve_resulttarget_value) = S ((S (ssr_target_preserve_result)) * dst_positive_scale_preserve_resulttarget_value)) /\ exists ff_q_pvs_preserve_resulttarget_valuepositive. dst_positive_code_preserve_resulttarget_value = ff_q_pvs_preserve_resulttarget_valuepositive * S ((S (ssr_target_preserve_result)) * dst_positive_scale_preserve_resulttarget_value) + (dst_positive_preserve_resulttarget_value))) /\ (((((exists ff_h_pvs_preserve_resulttarget_valuenegative. ff_h_pvs_preserve_resulttarget_valuenegative + S (dst_negative_preserve_resulttarget_value) = S ((S (ssr_target_preserve_result)) * dst_negative_scale_preserve_resulttarget_value)) /\ exists ff_q_pvs_preserve_resulttarget_valuenegative. dst_negative_code_preserve_resulttarget_value = ff_q_pvs_preserve_resulttarget_valuenegative * S ((S (ssr_target_preserve_result)) * dst_negative_scale_preserve_resulttarget_value) + (dst_negative_preserve_resulttarget_value))) /\ (exists ge_balance_positive_preserve_resulttarget_valuevalue ge_balance_negative_preserve_resulttarget_valuevalue. (((((ssr_value_preserve_result) = 2 * (ge_balance_positive_preserve_resulttarget_valuevalue) /\ (ge_balance_negative_preserve_resulttarget_valuevalue) = 0) \/ exists ge_signed_half_preserve_resulttarget_valuevaluedecode. (((ssr_value_preserve_result) = 2 * ge_signed_half_preserve_resulttarget_valuevaluedecode + 1 /\ (ge_balance_positive_preserve_resulttarget_valuevalue) = 0) /\ (ge_balance_negative_preserve_resulttarget_valuevalue) = S ge_signed_half_preserve_resulttarget_valuevaluedecode))) /\ ((dst_positive_preserve_resulttarget_value) + ge_balance_negative_preserve_resulttarget_valuevalue = (dst_negative_preserve_resulttarget_value) + ge_balance_positive_preserve_resulttarget_valuevalue)))))))))))))