dirichlet_coprime_grid_support_injective

Exact expanded first-order arithmetic statement

forall N F G m n A B T Q r s. (((((~((N)=0)) /\ (((exists dst_positive_code_injective_dataFtable dst_positive_scale_injective_dataFtable dst_negative_code_injective_dataFtable dst_negative_scale_injective_dataFtable. (((F) = (((((dst_positive_code_injective_dataFtable) + (dst_positive_scale_injective_dataFtable)) * S ((dst_positive_code_injective_dataFtable) + (dst_positive_scale_injective_dataFtable)) + ((dst_positive_scale_injective_dataFtable) + (dst_positive_scale_injective_dataFtable))) + (((dst_negative_code_injective_dataFtable) + (dst_negative_scale_injective_dataFtable)) * S ((dst_negative_code_injective_dataFtable) + (dst_negative_scale_injective_dataFtable)) + ((dst_negative_scale_injective_dataFtable) + (dst_negative_scale_injective_dataFtable)))) * S ((((dst_positive_code_injective_dataFtable) + (dst_positive_scale_injective_dataFtable)) * S ((dst_positive_code_injective_dataFtable) + (dst_positive_scale_injective_dataFtable)) + ((dst_positive_scale_injective_dataFtable) + (dst_positive_scale_injective_dataFtable))) + (((dst_negative_code_injective_dataFtable) + (dst_negative_scale_injective_dataFtable)) * S ((dst_negative_code_injective_dataFtable) + (dst_negative_scale_injective_dataFtable)) + ((dst_negative_scale_injective_dataFtable) + (dst_negative_scale_injective_dataFtable)))) + ((((dst_negative_code_injective_dataFtable) + (dst_negative_scale_injective_dataFtable)) * S ((dst_negative_code_injective_dataFtable) + (dst_negative_scale_injective_dataFtable)) + ((dst_negative_scale_injective_dataFtable) + (dst_negative_scale_injective_dataFtable))) + (((dst_negative_code_injective_dataFtable) + (dst_negative_scale_injective_dataFtable)) * S ((dst_negative_code_injective_dataFtable) + (dst_negative_scale_injective_dataFtable)) + ((dst_negative_scale_injective_dataFtable) + (dst_negative_scale_injective_dataFtable)))))) /\ (forall dst_index_injective_dataFtable. (exists pvs_le_gap_injective_dataFtabledomain. pvs_le_gap_injective_dataFtabledomain + (dst_index_injective_dataFtable) = (N)) -> exists dst_positive_injective_dataFtable dst_negative_injective_dataFtable dst_value_injective_dataFtable. ((((exists ff_h_pvs_injective_dataFtableentrypositive. ff_h_pvs_injective_dataFtableentrypositive + S (dst_positive_injective_dataFtable) = S ((S (dst_index_injective_dataFtable)) * dst_positive_scale_injective_dataFtable)) /\ exists ff_q_pvs_injective_dataFtableentrypositive. dst_positive_code_injective_dataFtable = ff_q_pvs_injective_dataFtableentrypositive * S ((S (dst_index_injective_dataFtable)) * dst_positive_scale_injective_dataFtable) + (dst_positive_injective_dataFtable))) /\ (((((exists ff_h_pvs_injective_dataFtableentrynegative. ff_h_pvs_injective_dataFtableentrynegative + S (dst_negative_injective_dataFtable) = S ((S (dst_index_injective_dataFtable)) * dst_negative_scale_injective_dataFtable)) /\ exists ff_q_pvs_injective_dataFtableentrynegative. dst_negative_code_injective_dataFtable = ff_q_pvs_injective_dataFtableentrynegative * S ((S (dst_index_injective_dataFtable)) * dst_negative_scale_injective_dataFtable) + (dst_negative_injective_dataFtable))) /\ (exists ge_balance_positive_injective_dataFtableentryvalue ge_balance_negative_injective_dataFtableentryvalue. (((((dst_value_injective_dataFtable) = 2 * (ge_balance_positive_injective_dataFtableentryvalue) /\ (ge_balance_negative_injective_dataFtableentryvalue) = 0) \/ exists ge_signed_half_injective_dataFtableentryvaluedecode. (((dst_value_injective_dataFtable) = 2 * ge_signed_half_injective_dataFtableentryvaluedecode + 1 /\ (ge_balance_positive_injective_dataFtableentryvalue) = 0) /\ (ge_balance_negative_injective_dataFtableentryvalue) = S ge_signed_half_injective_dataFtableentryvaluedecode))) /\ ((dst_positive_injective_dataFtable) + ge_balance_negative_injective_dataFtableentryvalue = (dst_negative_injective_dataFtable) + ge_balance_positive_injective_dataFtableentryvalue))))))))) /\ (((exists dst_positive_code_injective_dataFone dst_positive_scale_injective_dataFone dst_negative_code_injective_dataFone dst_negative_scale_injective_dataFone dst_positive_injective_dataFone dst_negative_injective_dataFone. (((F) = (((((dst_positive_code_injective_dataFone) + (dst_positive_scale_injective_dataFone)) * S ((dst_positive_code_injective_dataFone) + (dst_positive_scale_injective_dataFone)) + ((dst_positive_scale_injective_dataFone) + (dst_positive_scale_injective_dataFone))) + (((dst_negative_code_injective_dataFone) + (dst_negative_scale_injective_dataFone)) * S ((dst_negative_code_injective_dataFone) + (dst_negative_scale_injective_dataFone)) + ((dst_negative_scale_injective_dataFone) + (dst_negative_scale_injective_dataFone)))) * S ((((dst_positive_code_injective_dataFone) + (dst_positive_scale_injective_dataFone)) * S ((dst_positive_code_injective_dataFone) + (dst_positive_scale_injective_dataFone)) + ((dst_positive_scale_injective_dataFone) + (dst_positive_scale_injective_dataFone))) + (((dst_negative_code_injective_dataFone) + (dst_negative_scale_injective_dataFone)) * S ((dst_negative_code_injective_dataFone) + (dst_negative_scale_injective_dataFone)) + ((dst_negative_scale_injective_dataFone) + (dst_negative_scale_injective_dataFone)))) + ((((dst_negative_code_injective_dataFone) + (dst_negative_scale_injective_dataFone)) * S ((dst_negative_code_injective_dataFone) + (dst_negative_scale_injective_dataFone)) + ((dst_negative_scale_injective_dataFone) + (dst_negative_scale_injective_dataFone))) + (((dst_negative_code_injective_dataFone) + (dst_negative_scale_injective_dataFone)) * S ((dst_negative_code_injective_dataFone) + (dst_negative_scale_injective_dataFone)) + ((dst_negative_scale_injective_dataFone) + (dst_negative_scale_injective_dataFone)))))) /\ (((((exists ff_h_pvs_injective_dataFonepositive. ff_h_pvs_injective_dataFonepositive + S (dst_positive_injective_dataFone) = S ((S (1)) * dst_positive_scale_injective_dataFone)) /\ exists ff_q_pvs_injective_dataFonepositive. dst_positive_code_injective_dataFone = ff_q_pvs_injective_dataFonepositive * S ((S (1)) * dst_positive_scale_injective_dataFone) + (dst_positive_injective_dataFone))) /\ (((((exists ff_h_pvs_injective_dataFonenegative. ff_h_pvs_injective_dataFonenegative + S (dst_negative_injective_dataFone) = S ((S (1)) * dst_negative_scale_injective_dataFone)) /\ exists ff_q_pvs_injective_dataFonenegative. dst_negative_code_injective_dataFone = ff_q_pvs_injective_dataFonenegative * S ((S (1)) * dst_negative_scale_injective_dataFone) + (dst_negative_injective_dataFone))) /\ (exists ge_balance_positive_injective_dataFonevalue ge_balance_negative_injective_dataFonevalue. (((((2) = 2 * (ge_balance_positive_injective_dataFonevalue) /\ (ge_balance_negative_injective_dataFonevalue) = 0) \/ exists ge_signed_half_injective_dataFonevaluedecode. (((2) = 2 * ge_signed_half_injective_dataFonevaluedecode + 1 /\ (ge_balance_positive_injective_dataFonevalue) = 0) /\ (ge_balance_negative_injective_dataFonevalue) = S ge_signed_half_injective_dataFonevaluedecode))) /\ ((dst_positive_injective_dataFone) + ge_balance_negative_injective_dataFonevalue = (dst_negative_injective_dataFone) + ge_balance_positive_injective_dataFonevalue))))))))) /\ (forall mp_a_injective_dataF mp_b_injective_dataF mp_x_injective_dataF mp_y_injective_dataF mp_z_injective_dataF. ~(mp_a_injective_dataF=0) -> ~(mp_b_injective_dataF=0) -> (exists pvs_le_gap_injective_dataFbound. pvs_le_gap_injective_dataFbound + (mp_a_injective_dataF*mp_b_injective_dataF) = (N)) -> (forall frp_divisor_injective_dataFcoprime. (exists frp_left_factor_injective_dataFcoprime. mp_a_injective_dataF = frp_divisor_injective_dataFcoprime * frp_left_factor_injective_dataFcoprime) -> (exists frp_right_factor_injective_dataFcoprime. mp_b_injective_dataF = frp_divisor_injective_dataFcoprime * frp_right_factor_injective_dataFcoprime) -> frp_divisor_injective_dataFcoprime = 1) -> (exists dst_positive_code_injective_dataFfirst dst_positive_scale_injective_dataFfirst dst_negative_code_injective_dataFfirst dst_negative_scale_injective_dataFfirst dst_positive_injective_dataFfirst dst_negative_injective_dataFfirst. (((F) = (((((dst_positive_code_injective_dataFfirst) + (dst_positive_scale_injective_dataFfirst)) * S ((dst_positive_code_injective_dataFfirst) + (dst_positive_scale_injective_dataFfirst)) + ((dst_positive_scale_injective_dataFfirst) + (dst_positive_scale_injective_dataFfirst))) + (((dst_negative_code_injective_dataFfirst) + (dst_negative_scale_injective_dataFfirst)) * S ((dst_negative_code_injective_dataFfirst) + (dst_negative_scale_injective_dataFfirst)) + ((dst_negative_scale_injective_dataFfirst) + (dst_negative_scale_injective_dataFfirst)))) * S ((((dst_positive_code_injective_dataFfirst) + (dst_positive_scale_injective_dataFfirst)) * S ((dst_positive_code_injective_dataFfirst) + (dst_positive_scale_injective_dataFfirst)) + ((dst_positive_scale_injective_dataFfirst) + (dst_positive_scale_injective_dataFfirst))) + (((dst_negative_code_injective_dataFfirst) + (dst_negative_scale_injective_dataFfirst)) * S ((dst_negative_code_injective_dataFfirst) + (dst_negative_scale_injective_dataFfirst)) + ((dst_negative_scale_injective_dataFfirst) + (dst_negative_scale_injective_dataFfirst)))) + ((((dst_negative_code_injective_dataFfirst) + (dst_negative_scale_injective_dataFfirst)) * S ((dst_negative_code_injective_dataFfirst) + (dst_negative_scale_injective_dataFfirst)) + ((dst_negative_scale_injective_dataFfirst) + (dst_negative_scale_injective_dataFfirst))) + (((dst_negative_code_injective_dataFfirst) + (dst_negative_scale_injective_dataFfirst)) * S ((dst_negative_code_injective_dataFfirst) + (dst_negative_scale_injective_dataFfirst)) + ((dst_negative_scale_injective_dataFfirst) + (dst_negative_scale_injective_dataFfirst)))))) /\ (((((exists ff_h_pvs_injective_dataFfirstpositive. ff_h_pvs_injective_dataFfirstpositive + S (dst_positive_injective_dataFfirst) = S ((S (mp_a_injective_dataF)) * dst_positive_scale_injective_dataFfirst)) /\ exists ff_q_pvs_injective_dataFfirstpositive. dst_positive_code_injective_dataFfirst = ff_q_pvs_injective_dataFfirstpositive * S ((S (mp_a_injective_dataF)) * dst_positive_scale_injective_dataFfirst) + (dst_positive_injective_dataFfirst))) /\ (((((exists ff_h_pvs_injective_dataFfirstnegative. ff_h_pvs_injective_dataFfirstnegative + S (dst_negative_injective_dataFfirst) = S ((S (mp_a_injective_dataF)) * dst_negative_scale_injective_dataFfirst)) /\ exists ff_q_pvs_injective_dataFfirstnegative. dst_negative_code_injective_dataFfirst = ff_q_pvs_injective_dataFfirstnegative * S ((S (mp_a_injective_dataF)) * dst_negative_scale_injective_dataFfirst) + (dst_negative_injective_dataFfirst))) /\ (exists ge_balance_positive_injective_dataFfirstvalue ge_balance_negative_injective_dataFfirstvalue. (((((mp_x_injective_dataF) = 2 * (ge_balance_positive_injective_dataFfirstvalue) /\ (ge_balance_negative_injective_dataFfirstvalue) = 0) \/ exists ge_signed_half_injective_dataFfirstvaluedecode. (((mp_x_injective_dataF) = 2 * ge_signed_half_injective_dataFfirstvaluedecode + 1 /\ (ge_balance_positive_injective_dataFfirstvalue) = 0) /\ (ge_balance_negative_injective_dataFfirstvalue) = S ge_signed_half_injective_dataFfirstvaluedecode))) /\ ((dst_positive_injective_dataFfirst) + ge_balance_negative_injective_dataFfirstvalue = (dst_negative_injective_dataFfirst) + ge_balance_positive_injective_dataFfirstvalue))))))))) -> (exists dst_positive_code_injective_dataFsecond dst_positive_scale_injective_dataFsecond dst_negative_code_injective_dataFsecond dst_negative_scale_injective_dataFsecond dst_positive_injective_dataFsecond dst_negative_injective_dataFsecond. (((F) = (((((dst_positive_code_injective_dataFsecond) + (dst_positive_scale_injective_dataFsecond)) * S ((dst_positive_code_injective_dataFsecond) + (dst_positive_scale_injective_dataFsecond)) + ((dst_positive_scale_injective_dataFsecond) + (dst_positive_scale_injective_dataFsecond))) + (((dst_negative_code_injective_dataFsecond) + (dst_negative_scale_injective_dataFsecond)) * S ((dst_negative_code_injective_dataFsecond) + (dst_negative_scale_injective_dataFsecond)) + ((dst_negative_scale_injective_dataFsecond) + (dst_negative_scale_injective_dataFsecond)))) * S ((((dst_positive_code_injective_dataFsecond) + (dst_positive_scale_injective_dataFsecond)) * S ((dst_positive_code_injective_dataFsecond) + (dst_positive_scale_injective_dataFsecond)) + ((dst_positive_scale_injective_dataFsecond) + (dst_positive_scale_injective_dataFsecond))) + (((dst_negative_code_injective_dataFsecond) + (dst_negative_scale_injective_dataFsecond)) * S ((dst_negative_code_injective_dataFsecond) + (dst_negative_scale_injective_dataFsecond)) + ((dst_negative_scale_injective_dataFsecond) + (dst_negative_scale_injective_dataFsecond)))) + ((((dst_negative_code_injective_dataFsecond) + (dst_negative_scale_injective_dataFsecond)) * S ((dst_negative_code_injective_dataFsecond) + (dst_negative_scale_injective_dataFsecond)) + ((dst_negative_scale_injective_dataFsecond) + (dst_negative_scale_injective_dataFsecond))) + (((dst_negative_code_injective_dataFsecond) + (dst_negative_scale_injective_dataFsecond)) * S ((dst_negative_code_injective_dataFsecond) + (dst_negative_scale_injective_dataFsecond)) + ((dst_negative_scale_injective_dataFsecond) + (dst_negative_scale_injective_dataFsecond)))))) /\ (((((exists ff_h_pvs_injective_dataFsecondpositive. ff_h_pvs_injective_dataFsecondpositive + S (dst_positive_injective_dataFsecond) = S ((S (mp_b_injective_dataF)) * dst_positive_scale_injective_dataFsecond)) /\ exists ff_q_pvs_injective_dataFsecondpositive. dst_positive_code_injective_dataFsecond = ff_q_pvs_injective_dataFsecondpositive * S ((S (mp_b_injective_dataF)) * dst_positive_scale_injective_dataFsecond) + (dst_positive_injective_dataFsecond))) /\ (((((exists ff_h_pvs_injective_dataFsecondnegative. ff_h_pvs_injective_dataFsecondnegative + S (dst_negative_injective_dataFsecond) = S ((S (mp_b_injective_dataF)) * dst_negative_scale_injective_dataFsecond)) /\ exists ff_q_pvs_injective_dataFsecondnegative. dst_negative_code_injective_dataFsecond = ff_q_pvs_injective_dataFsecondnegative * S ((S (mp_b_injective_dataF)) * dst_negative_scale_injective_dataFsecond) + (dst_negative_injective_dataFsecond))) /\ (exists ge_balance_positive_injective_dataFsecondvalue ge_balance_negative_injective_dataFsecondvalue. (((((mp_y_injective_dataF) = 2 * (ge_balance_positive_injective_dataFsecondvalue) /\ (ge_balance_negative_injective_dataFsecondvalue) = 0) \/ exists ge_signed_half_injective_dataFsecondvaluedecode. (((mp_y_injective_dataF) = 2 * ge_signed_half_injective_dataFsecondvaluedecode + 1 /\ (ge_balance_positive_injective_dataFsecondvalue) = 0) /\ (ge_balance_negative_injective_dataFsecondvalue) = S ge_signed_half_injective_dataFsecondvaluedecode))) /\ ((dst_positive_injective_dataFsecond) + ge_balance_negative_injective_dataFsecondvalue = (dst_negative_injective_dataFsecond) + ge_balance_positive_injective_dataFsecondvalue))))))))) -> (exists dst_positive_code_injective_dataFproduct dst_positive_scale_injective_dataFproduct dst_negative_code_injective_dataFproduct dst_negative_scale_injective_dataFproduct dst_positive_injective_dataFproduct dst_negative_injective_dataFproduct. (((F) = (((((dst_positive_code_injective_dataFproduct) + (dst_positive_scale_injective_dataFproduct)) * S ((dst_positive_code_injective_dataFproduct) + (dst_positive_scale_injective_dataFproduct)) + ((dst_positive_scale_injective_dataFproduct) + (dst_positive_scale_injective_dataFproduct))) + (((dst_negative_code_injective_dataFproduct) + (dst_negative_scale_injective_dataFproduct)) * S ((dst_negative_code_injective_dataFproduct) + (dst_negative_scale_injective_dataFproduct)) + ((dst_negative_scale_injective_dataFproduct) + (dst_negative_scale_injective_dataFproduct)))) * S ((((dst_positive_code_injective_dataFproduct) + (dst_positive_scale_injective_dataFproduct)) * S ((dst_positive_code_injective_dataFproduct) + (dst_positive_scale_injective_dataFproduct)) + ((dst_positive_scale_injective_dataFproduct) + (dst_positive_scale_injective_dataFproduct))) + (((dst_negative_code_injective_dataFproduct) + (dst_negative_scale_injective_dataFproduct)) * S ((dst_negative_code_injective_dataFproduct) + (dst_negative_scale_injective_dataFproduct)) + ((dst_negative_scale_injective_dataFproduct) + (dst_negative_scale_injective_dataFproduct)))) + ((((dst_negative_code_injective_dataFproduct) + (dst_negative_scale_injective_dataFproduct)) * S ((dst_negative_code_injective_dataFproduct) + (dst_negative_scale_injective_dataFproduct)) + ((dst_negative_scale_injective_dataFproduct) + (dst_negative_scale_injective_dataFproduct))) + (((dst_negative_code_injective_dataFproduct) + (dst_negative_scale_injective_dataFproduct)) * S ((dst_negative_code_injective_dataFproduct) + (dst_negative_scale_injective_dataFproduct)) + ((dst_negative_scale_injective_dataFproduct) + (dst_negative_scale_injective_dataFproduct)))))) /\ (((((exists ff_h_pvs_injective_dataFproductpositive. ff_h_pvs_injective_dataFproductpositive + S (dst_positive_injective_dataFproduct) = S ((S (mp_a_injective_dataF*mp_b_injective_dataF)) * dst_positive_scale_injective_dataFproduct)) /\ exists ff_q_pvs_injective_dataFproductpositive. dst_positive_code_injective_dataFproduct = ff_q_pvs_injective_dataFproductpositive * S ((S (mp_a_injective_dataF*mp_b_injective_dataF)) * dst_positive_scale_injective_dataFproduct) + (dst_positive_injective_dataFproduct))) /\ (((((exists ff_h_pvs_injective_dataFproductnegative. ff_h_pvs_injective_dataFproductnegative + S (dst_negative_injective_dataFproduct) = S ((S (mp_a_injective_dataF*mp_b_injective_dataF)) * dst_negative_scale_injective_dataFproduct)) /\ exists ff_q_pvs_injective_dataFproductnegative. dst_negative_code_injective_dataFproduct = ff_q_pvs_injective_dataFproductnegative * S ((S (mp_a_injective_dataF*mp_b_injective_dataF)) * dst_negative_scale_injective_dataFproduct) + (dst_negative_injective_dataFproduct))) /\ (exists ge_balance_positive_injective_dataFproductvalue ge_balance_negative_injective_dataFproductvalue. (((((mp_z_injective_dataF) = 2 * (ge_balance_positive_injective_dataFproductvalue) /\ (ge_balance_negative_injective_dataFproductvalue) = 0) \/ exists ge_signed_half_injective_dataFproductvaluedecode. (((mp_z_injective_dataF) = 2 * ge_signed_half_injective_dataFproductvaluedecode + 1 /\ (ge_balance_positive_injective_dataFproductvalue) = 0) /\ (ge_balance_negative_injective_dataFproductvalue) = S ge_signed_half_injective_dataFproductvaluedecode))) /\ ((dst_positive_injective_dataFproduct) + ge_balance_negative_injective_dataFproductvalue = (dst_negative_injective_dataFproduct) + ge_balance_positive_injective_dataFproductvalue))))))))) -> (exists sto_ap_injective_dataFlaw sto_an_injective_dataFlaw sto_bp_injective_dataFlaw sto_bn_injective_dataFlaw sto_cp_injective_dataFlaw sto_cn_injective_dataFlaw. (((((mp_x_injective_dataF) = 2 * (sto_ap_injective_dataFlaw) /\ (sto_an_injective_dataFlaw) = 0) \/ exists ge_signed_half_injective_dataFlawleft. (((mp_x_injective_dataF) = 2 * ge_signed_half_injective_dataFlawleft + 1 /\ (sto_ap_injective_dataFlaw) = 0) /\ (sto_an_injective_dataFlaw) = S ge_signed_half_injective_dataFlawleft))) /\ ((((((mp_y_injective_dataF) = 2 * (sto_bp_injective_dataFlaw) /\ (sto_bn_injective_dataFlaw) = 0) \/ exists ge_signed_half_injective_dataFlawright. (((mp_y_injective_dataF) = 2 * ge_signed_half_injective_dataFlawright + 1 /\ (sto_bp_injective_dataFlaw) = 0) /\ (sto_bn_injective_dataFlaw) = S ge_signed_half_injective_dataFlawright))) /\ ((((((mp_z_injective_dataF) = 2 * (sto_cp_injective_dataFlaw) /\ (sto_cn_injective_dataFlaw) = 0) \/ exists ge_signed_half_injective_dataFlawoutput. (((mp_z_injective_dataF) = 2 * ge_signed_half_injective_dataFlawoutput + 1 /\ (sto_cp_injective_dataFlaw) = 0) /\ (sto_cn_injective_dataFlaw) = S ge_signed_half_injective_dataFlawoutput))) /\ ((sto_ap_injective_dataFlaw * sto_bp_injective_dataFlaw + sto_an_injective_dataFlaw * sto_bn_injective_dataFlaw) + sto_cn_injective_dataFlaw = (sto_ap_injective_dataFlaw * sto_bn_injective_dataFlaw + sto_an_injective_dataFlaw * sto_bp_injective_dataFlaw) + sto_cp_injective_dataFlaw)))))))))))))) /\ (((((~((N)=0)) /\ (((exists dst_positive_code_injective_dataGtable dst_positive_scale_injective_dataGtable dst_negative_code_injective_dataGtable dst_negative_scale_injective_dataGtable. (((G) = (((((dst_positive_code_injective_dataGtable) + (dst_positive_scale_injective_dataGtable)) * S ((dst_positive_code_injective_dataGtable) + (dst_positive_scale_injective_dataGtable)) + ((dst_positive_scale_injective_dataGtable) + (dst_positive_scale_injective_dataGtable))) + (((dst_negative_code_injective_dataGtable) + (dst_negative_scale_injective_dataGtable)) * S ((dst_negative_code_injective_dataGtable) + (dst_negative_scale_injective_dataGtable)) + ((dst_negative_scale_injective_dataGtable) + (dst_negative_scale_injective_dataGtable)))) * S ((((dst_positive_code_injective_dataGtable) + (dst_positive_scale_injective_dataGtable)) * S ((dst_positive_code_injective_dataGtable) + (dst_positive_scale_injective_dataGtable)) + ((dst_positive_scale_injective_dataGtable) + (dst_positive_scale_injective_dataGtable))) + (((dst_negative_code_injective_dataGtable) + (dst_negative_scale_injective_dataGtable)) * S ((dst_negative_code_injective_dataGtable) + (dst_negative_scale_injective_dataGtable)) + ((dst_negative_scale_injective_dataGtable) + (dst_negative_scale_injective_dataGtable)))) + ((((dst_negative_code_injective_dataGtable) + (dst_negative_scale_injective_dataGtable)) * S ((dst_negative_code_injective_dataGtable) + (dst_negative_scale_injective_dataGtable)) + ((dst_negative_scale_injective_dataGtable) + (dst_negative_scale_injective_dataGtable))) + (((dst_negative_code_injective_dataGtable) + (dst_negative_scale_injective_dataGtable)) * S ((dst_negative_code_injective_dataGtable) + (dst_negative_scale_injective_dataGtable)) + ((dst_negative_scale_injective_dataGtable) + (dst_negative_scale_injective_dataGtable)))))) /\ (forall dst_index_injective_dataGtable. (exists pvs_le_gap_injective_dataGtabledomain. pvs_le_gap_injective_dataGtabledomain + (dst_index_injective_dataGtable) = (N)) -> exists dst_positive_injective_dataGtable dst_negative_injective_dataGtable dst_value_injective_dataGtable. ((((exists ff_h_pvs_injective_dataGtableentrypositive. ff_h_pvs_injective_dataGtableentrypositive + S (dst_positive_injective_dataGtable) = S ((S (dst_index_injective_dataGtable)) * dst_positive_scale_injective_dataGtable)) /\ exists ff_q_pvs_injective_dataGtableentrypositive. dst_positive_code_injective_dataGtable = ff_q_pvs_injective_dataGtableentrypositive * S ((S (dst_index_injective_dataGtable)) * dst_positive_scale_injective_dataGtable) + (dst_positive_injective_dataGtable))) /\ (((((exists ff_h_pvs_injective_dataGtableentrynegative. ff_h_pvs_injective_dataGtableentrynegative + S (dst_negative_injective_dataGtable) = S ((S (dst_index_injective_dataGtable)) * dst_negative_scale_injective_dataGtable)) /\ exists ff_q_pvs_injective_dataGtableentrynegative. dst_negative_code_injective_dataGtable = ff_q_pvs_injective_dataGtableentrynegative * S ((S (dst_index_injective_dataGtable)) * dst_negative_scale_injective_dataGtable) + (dst_negative_injective_dataGtable))) /\ (exists ge_balance_positive_injective_dataGtableentryvalue ge_balance_negative_injective_dataGtableentryvalue. (((((dst_value_injective_dataGtable) = 2 * (ge_balance_positive_injective_dataGtableentryvalue) /\ (ge_balance_negative_injective_dataGtableentryvalue) = 0) \/ exists ge_signed_half_injective_dataGtableentryvaluedecode. (((dst_value_injective_dataGtable) = 2 * ge_signed_half_injective_dataGtableentryvaluedecode + 1 /\ (ge_balance_positive_injective_dataGtableentryvalue) = 0) /\ (ge_balance_negative_injective_dataGtableentryvalue) = S ge_signed_half_injective_dataGtableentryvaluedecode))) /\ ((dst_positive_injective_dataGtable) + ge_balance_negative_injective_dataGtableentryvalue = (dst_negative_injective_dataGtable) + ge_balance_positive_injective_dataGtableentryvalue))))))))) /\ (((exists dst_positive_code_injective_dataGone dst_positive_scale_injective_dataGone dst_negative_code_injective_dataGone dst_negative_scale_injective_dataGone dst_positive_injective_dataGone dst_negative_injective_dataGone. (((G) = (((((dst_positive_code_injective_dataGone) + (dst_positive_scale_injective_dataGone)) * S ((dst_positive_code_injective_dataGone) + (dst_positive_scale_injective_dataGone)) + ((dst_positive_scale_injective_dataGone) + (dst_positive_scale_injective_dataGone))) + (((dst_negative_code_injective_dataGone) + (dst_negative_scale_injective_dataGone)) * S ((dst_negative_code_injective_dataGone) + (dst_negative_scale_injective_dataGone)) + ((dst_negative_scale_injective_dataGone) + (dst_negative_scale_injective_dataGone)))) * S ((((dst_positive_code_injective_dataGone) + (dst_positive_scale_injective_dataGone)) * S ((dst_positive_code_injective_dataGone) + (dst_positive_scale_injective_dataGone)) + ((dst_positive_scale_injective_dataGone) + (dst_positive_scale_injective_dataGone))) + (((dst_negative_code_injective_dataGone) + (dst_negative_scale_injective_dataGone)) * S ((dst_negative_code_injective_dataGone) + (dst_negative_scale_injective_dataGone)) + ((dst_negative_scale_injective_dataGone) + (dst_negative_scale_injective_dataGone)))) + ((((dst_negative_code_injective_dataGone) + (dst_negative_scale_injective_dataGone)) * S ((dst_negative_code_injective_dataGone) + (dst_negative_scale_injective_dataGone)) + ((dst_negative_scale_injective_dataGone) + (dst_negative_scale_injective_dataGone))) + (((dst_negative_code_injective_dataGone) + (dst_negative_scale_injective_dataGone)) * S ((dst_negative_code_injective_dataGone) + (dst_negative_scale_injective_dataGone)) + ((dst_negative_scale_injective_dataGone) + (dst_negative_scale_injective_dataGone)))))) /\ (((((exists ff_h_pvs_injective_dataGonepositive. ff_h_pvs_injective_dataGonepositive + S (dst_positive_injective_dataGone) = S ((S (1)) * dst_positive_scale_injective_dataGone)) /\ exists ff_q_pvs_injective_dataGonepositive. dst_positive_code_injective_dataGone = ff_q_pvs_injective_dataGonepositive * S ((S (1)) * dst_positive_scale_injective_dataGone) + (dst_positive_injective_dataGone))) /\ (((((exists ff_h_pvs_injective_dataGonenegative. ff_h_pvs_injective_dataGonenegative + S (dst_negative_injective_dataGone) = S ((S (1)) * dst_negative_scale_injective_dataGone)) /\ exists ff_q_pvs_injective_dataGonenegative. dst_negative_code_injective_dataGone = ff_q_pvs_injective_dataGonenegative * S ((S (1)) * dst_negative_scale_injective_dataGone) + (dst_negative_injective_dataGone))) /\ (exists ge_balance_positive_injective_dataGonevalue ge_balance_negative_injective_dataGonevalue. (((((2) = 2 * (ge_balance_positive_injective_dataGonevalue) /\ (ge_balance_negative_injective_dataGonevalue) = 0) \/ exists ge_signed_half_injective_dataGonevaluedecode. (((2) = 2 * ge_signed_half_injective_dataGonevaluedecode + 1 /\ (ge_balance_positive_injective_dataGonevalue) = 0) /\ (ge_balance_negative_injective_dataGonevalue) = S ge_signed_half_injective_dataGonevaluedecode))) /\ ((dst_positive_injective_dataGone) + ge_balance_negative_injective_dataGonevalue = (dst_negative_injective_dataGone) + ge_balance_positive_injective_dataGonevalue))))))))) /\ (forall mp_a_injective_dataG mp_b_injective_dataG mp_x_injective_dataG mp_y_injective_dataG mp_z_injective_dataG. ~(mp_a_injective_dataG=0) -> ~(mp_b_injective_dataG=0) -> (exists pvs_le_gap_injective_dataGbound. pvs_le_gap_injective_dataGbound + (mp_a_injective_dataG*mp_b_injective_dataG) = (N)) -> (forall frp_divisor_injective_dataGcoprime. (exists frp_left_factor_injective_dataGcoprime. mp_a_injective_dataG = frp_divisor_injective_dataGcoprime * frp_left_factor_injective_dataGcoprime) -> (exists frp_right_factor_injective_dataGcoprime. mp_b_injective_dataG = frp_divisor_injective_dataGcoprime * frp_right_factor_injective_dataGcoprime) -> frp_divisor_injective_dataGcoprime = 1) -> (exists dst_positive_code_injective_dataGfirst dst_positive_scale_injective_dataGfirst dst_negative_code_injective_dataGfirst dst_negative_scale_injective_dataGfirst dst_positive_injective_dataGfirst dst_negative_injective_dataGfirst. (((G) = (((((dst_positive_code_injective_dataGfirst) + (dst_positive_scale_injective_dataGfirst)) * S ((dst_positive_code_injective_dataGfirst) + (dst_positive_scale_injective_dataGfirst)) + ((dst_positive_scale_injective_dataGfirst) + (dst_positive_scale_injective_dataGfirst))) + (((dst_negative_code_injective_dataGfirst) + (dst_negative_scale_injective_dataGfirst)) * S ((dst_negative_code_injective_dataGfirst) + (dst_negative_scale_injective_dataGfirst)) + ((dst_negative_scale_injective_dataGfirst) + (dst_negative_scale_injective_dataGfirst)))) * S ((((dst_positive_code_injective_dataGfirst) + (dst_positive_scale_injective_dataGfirst)) * S ((dst_positive_code_injective_dataGfirst) + (dst_positive_scale_injective_dataGfirst)) + ((dst_positive_scale_injective_dataGfirst) + (dst_positive_scale_injective_dataGfirst))) + (((dst_negative_code_injective_dataGfirst) + (dst_negative_scale_injective_dataGfirst)) * S ((dst_negative_code_injective_dataGfirst) + (dst_negative_scale_injective_dataGfirst)) + ((dst_negative_scale_injective_dataGfirst) + (dst_negative_scale_injective_dataGfirst)))) + ((((dst_negative_code_injective_dataGfirst) + (dst_negative_scale_injective_dataGfirst)) * S ((dst_negative_code_injective_dataGfirst) + (dst_negative_scale_injective_dataGfirst)) + ((dst_negative_scale_injective_dataGfirst) + (dst_negative_scale_injective_dataGfirst))) + (((dst_negative_code_injective_dataGfirst) + (dst_negative_scale_injective_dataGfirst)) * S ((dst_negative_code_injective_dataGfirst) + (dst_negative_scale_injective_dataGfirst)) + ((dst_negative_scale_injective_dataGfirst) + (dst_negative_scale_injective_dataGfirst)))))) /\ (((((exists ff_h_pvs_injective_dataGfirstpositive. ff_h_pvs_injective_dataGfirstpositive + S (dst_positive_injective_dataGfirst) = S ((S (mp_a_injective_dataG)) * dst_positive_scale_injective_dataGfirst)) /\ exists ff_q_pvs_injective_dataGfirstpositive. dst_positive_code_injective_dataGfirst = ff_q_pvs_injective_dataGfirstpositive * S ((S (mp_a_injective_dataG)) * dst_positive_scale_injective_dataGfirst) + (dst_positive_injective_dataGfirst))) /\ (((((exists ff_h_pvs_injective_dataGfirstnegative. ff_h_pvs_injective_dataGfirstnegative + S (dst_negative_injective_dataGfirst) = S ((S (mp_a_injective_dataG)) * dst_negative_scale_injective_dataGfirst)) /\ exists ff_q_pvs_injective_dataGfirstnegative. dst_negative_code_injective_dataGfirst = ff_q_pvs_injective_dataGfirstnegative * S ((S (mp_a_injective_dataG)) * dst_negative_scale_injective_dataGfirst) + (dst_negative_injective_dataGfirst))) /\ (exists ge_balance_positive_injective_dataGfirstvalue ge_balance_negative_injective_dataGfirstvalue. (((((mp_x_injective_dataG) = 2 * (ge_balance_positive_injective_dataGfirstvalue) /\ (ge_balance_negative_injective_dataGfirstvalue) = 0) \/ exists ge_signed_half_injective_dataGfirstvaluedecode. (((mp_x_injective_dataG) = 2 * ge_signed_half_injective_dataGfirstvaluedecode + 1 /\ (ge_balance_positive_injective_dataGfirstvalue) = 0) /\ (ge_balance_negative_injective_dataGfirstvalue) = S ge_signed_half_injective_dataGfirstvaluedecode))) /\ ((dst_positive_injective_dataGfirst) + ge_balance_negative_injective_dataGfirstvalue = (dst_negative_injective_dataGfirst) + ge_balance_positive_injective_dataGfirstvalue))))))))) -> (exists dst_positive_code_injective_dataGsecond dst_positive_scale_injective_dataGsecond dst_negative_code_injective_dataGsecond dst_negative_scale_injective_dataGsecond dst_positive_injective_dataGsecond dst_negative_injective_dataGsecond. (((G) = (((((dst_positive_code_injective_dataGsecond) + (dst_positive_scale_injective_dataGsecond)) * S ((dst_positive_code_injective_dataGsecond) + (dst_positive_scale_injective_dataGsecond)) + ((dst_positive_scale_injective_dataGsecond) + (dst_positive_scale_injective_dataGsecond))) + (((dst_negative_code_injective_dataGsecond) + (dst_negative_scale_injective_dataGsecond)) * S ((dst_negative_code_injective_dataGsecond) + (dst_negative_scale_injective_dataGsecond)) + ((dst_negative_scale_injective_dataGsecond) + (dst_negative_scale_injective_dataGsecond)))) * S ((((dst_positive_code_injective_dataGsecond) + (dst_positive_scale_injective_dataGsecond)) * S ((dst_positive_code_injective_dataGsecond) + (dst_positive_scale_injective_dataGsecond)) + ((dst_positive_scale_injective_dataGsecond) + (dst_positive_scale_injective_dataGsecond))) + (((dst_negative_code_injective_dataGsecond) + (dst_negative_scale_injective_dataGsecond)) * S ((dst_negative_code_injective_dataGsecond) + (dst_negative_scale_injective_dataGsecond)) + ((dst_negative_scale_injective_dataGsecond) + (dst_negative_scale_injective_dataGsecond)))) + ((((dst_negative_code_injective_dataGsecond) + (dst_negative_scale_injective_dataGsecond)) * S ((dst_negative_code_injective_dataGsecond) + (dst_negative_scale_injective_dataGsecond)) + ((dst_negative_scale_injective_dataGsecond) + (dst_negative_scale_injective_dataGsecond))) + (((dst_negative_code_injective_dataGsecond) + (dst_negative_scale_injective_dataGsecond)) * S ((dst_negative_code_injective_dataGsecond) + (dst_negative_scale_injective_dataGsecond)) + ((dst_negative_scale_injective_dataGsecond) + (dst_negative_scale_injective_dataGsecond)))))) /\ (((((exists ff_h_pvs_injective_dataGsecondpositive. ff_h_pvs_injective_dataGsecondpositive + S (dst_positive_injective_dataGsecond) = S ((S (mp_b_injective_dataG)) * dst_positive_scale_injective_dataGsecond)) /\ exists ff_q_pvs_injective_dataGsecondpositive. dst_positive_code_injective_dataGsecond = ff_q_pvs_injective_dataGsecondpositive * S ((S (mp_b_injective_dataG)) * dst_positive_scale_injective_dataGsecond) + (dst_positive_injective_dataGsecond))) /\ (((((exists ff_h_pvs_injective_dataGsecondnegative. ff_h_pvs_injective_dataGsecondnegative + S (dst_negative_injective_dataGsecond) = S ((S (mp_b_injective_dataG)) * dst_negative_scale_injective_dataGsecond)) /\ exists ff_q_pvs_injective_dataGsecondnegative. dst_negative_code_injective_dataGsecond = ff_q_pvs_injective_dataGsecondnegative * S ((S (mp_b_injective_dataG)) * dst_negative_scale_injective_dataGsecond) + (dst_negative_injective_dataGsecond))) /\ (exists ge_balance_positive_injective_dataGsecondvalue ge_balance_negative_injective_dataGsecondvalue. (((((mp_y_injective_dataG) = 2 * (ge_balance_positive_injective_dataGsecondvalue) /\ (ge_balance_negative_injective_dataGsecondvalue) = 0) \/ exists ge_signed_half_injective_dataGsecondvaluedecode. (((mp_y_injective_dataG) = 2 * ge_signed_half_injective_dataGsecondvaluedecode + 1 /\ (ge_balance_positive_injective_dataGsecondvalue) = 0) /\ (ge_balance_negative_injective_dataGsecondvalue) = S ge_signed_half_injective_dataGsecondvaluedecode))) /\ ((dst_positive_injective_dataGsecond) + ge_balance_negative_injective_dataGsecondvalue = (dst_negative_injective_dataGsecond) + ge_balance_positive_injective_dataGsecondvalue))))))))) -> (exists dst_positive_code_injective_dataGproduct dst_positive_scale_injective_dataGproduct dst_negative_code_injective_dataGproduct dst_negative_scale_injective_dataGproduct dst_positive_injective_dataGproduct dst_negative_injective_dataGproduct. (((G) = (((((dst_positive_code_injective_dataGproduct) + (dst_positive_scale_injective_dataGproduct)) * S ((dst_positive_code_injective_dataGproduct) + (dst_positive_scale_injective_dataGproduct)) + ((dst_positive_scale_injective_dataGproduct) + (dst_positive_scale_injective_dataGproduct))) + (((dst_negative_code_injective_dataGproduct) + (dst_negative_scale_injective_dataGproduct)) * S ((dst_negative_code_injective_dataGproduct) + (dst_negative_scale_injective_dataGproduct)) + ((dst_negative_scale_injective_dataGproduct) + (dst_negative_scale_injective_dataGproduct)))) * S ((((dst_positive_code_injective_dataGproduct) + (dst_positive_scale_injective_dataGproduct)) * S ((dst_positive_code_injective_dataGproduct) + (dst_positive_scale_injective_dataGproduct)) + ((dst_positive_scale_injective_dataGproduct) + (dst_positive_scale_injective_dataGproduct))) + (((dst_negative_code_injective_dataGproduct) + (dst_negative_scale_injective_dataGproduct)) * S ((dst_negative_code_injective_dataGproduct) + (dst_negative_scale_injective_dataGproduct)) + ((dst_negative_scale_injective_dataGproduct) + (dst_negative_scale_injective_dataGproduct)))) + ((((dst_negative_code_injective_dataGproduct) + (dst_negative_scale_injective_dataGproduct)) * S ((dst_negative_code_injective_dataGproduct) + (dst_negative_scale_injective_dataGproduct)) + ((dst_negative_scale_injective_dataGproduct) + (dst_negative_scale_injective_dataGproduct))) + (((dst_negative_code_injective_dataGproduct) + (dst_negative_scale_injective_dataGproduct)) * S ((dst_negative_code_injective_dataGproduct) + (dst_negative_scale_injective_dataGproduct)) + ((dst_negative_scale_injective_dataGproduct) + (dst_negative_scale_injective_dataGproduct)))))) /\ (((((exists ff_h_pvs_injective_dataGproductpositive. ff_h_pvs_injective_dataGproductpositive + S (dst_positive_injective_dataGproduct) = S ((S (mp_a_injective_dataG*mp_b_injective_dataG)) * dst_positive_scale_injective_dataGproduct)) /\ exists ff_q_pvs_injective_dataGproductpositive. dst_positive_code_injective_dataGproduct = ff_q_pvs_injective_dataGproductpositive * S ((S (mp_a_injective_dataG*mp_b_injective_dataG)) * dst_positive_scale_injective_dataGproduct) + (dst_positive_injective_dataGproduct))) /\ (((((exists ff_h_pvs_injective_dataGproductnegative. ff_h_pvs_injective_dataGproductnegative + S (dst_negative_injective_dataGproduct) = S ((S (mp_a_injective_dataG*mp_b_injective_dataG)) * dst_negative_scale_injective_dataGproduct)) /\ exists ff_q_pvs_injective_dataGproductnegative. dst_negative_code_injective_dataGproduct = ff_q_pvs_injective_dataGproductnegative * S ((S (mp_a_injective_dataG*mp_b_injective_dataG)) * dst_negative_scale_injective_dataGproduct) + (dst_negative_injective_dataGproduct))) /\ (exists ge_balance_positive_injective_dataGproductvalue ge_balance_negative_injective_dataGproductvalue. (((((mp_z_injective_dataG) = 2 * (ge_balance_positive_injective_dataGproductvalue) /\ (ge_balance_negative_injective_dataGproductvalue) = 0) \/ exists ge_signed_half_injective_dataGproductvaluedecode. (((mp_z_injective_dataG) = 2 * ge_signed_half_injective_dataGproductvaluedecode + 1 /\ (ge_balance_positive_injective_dataGproductvalue) = 0) /\ (ge_balance_negative_injective_dataGproductvalue) = S ge_signed_half_injective_dataGproductvaluedecode))) /\ ((dst_positive_injective_dataGproduct) + ge_balance_negative_injective_dataGproductvalue = (dst_negative_injective_dataGproduct) + ge_balance_positive_injective_dataGproductvalue))))))))) -> (exists sto_ap_injective_dataGlaw sto_an_injective_dataGlaw sto_bp_injective_dataGlaw sto_bn_injective_dataGlaw sto_cp_injective_dataGlaw sto_cn_injective_dataGlaw. (((((mp_x_injective_dataG) = 2 * (sto_ap_injective_dataGlaw) /\ (sto_an_injective_dataGlaw) = 0) \/ exists ge_signed_half_injective_dataGlawleft. (((mp_x_injective_dataG) = 2 * ge_signed_half_injective_dataGlawleft + 1 /\ (sto_ap_injective_dataGlaw) = 0) /\ (sto_an_injective_dataGlaw) = S ge_signed_half_injective_dataGlawleft))) /\ ((((((mp_y_injective_dataG) = 2 * (sto_bp_injective_dataGlaw) /\ (sto_bn_injective_dataGlaw) = 0) \/ exists ge_signed_half_injective_dataGlawright. (((mp_y_injective_dataG) = 2 * ge_signed_half_injective_dataGlawright + 1 /\ (sto_bp_injective_dataGlaw) = 0) /\ (sto_bn_injective_dataGlaw) = S ge_signed_half_injective_dataGlawright))) /\ ((((((mp_z_injective_dataG) = 2 * (sto_cp_injective_dataGlaw) /\ (sto_cn_injective_dataGlaw) = 0) \/ exists ge_signed_half_injective_dataGlawoutput. (((mp_z_injective_dataG) = 2 * ge_signed_half_injective_dataGlawoutput + 1 /\ (sto_cp_injective_dataGlaw) = 0) /\ (sto_cn_injective_dataGlaw) = S ge_signed_half_injective_dataGlawoutput))) /\ ((sto_ap_injective_dataGlaw * sto_bp_injective_dataGlaw + sto_an_injective_dataGlaw * sto_bn_injective_dataGlaw) + sto_cn_injective_dataGlaw = (sto_ap_injective_dataGlaw * sto_bn_injective_dataGlaw + sto_an_injective_dataGlaw * sto_bp_injective_dataGlaw) + sto_cp_injective_dataGlaw)))))))))))))) /\ (((~((m)=0)) /\ (((~((n)=0)) /\ (((exists pvs_le_gap_injective_databound. pvs_le_gap_injective_databound + ((m)*(n)) = (N)) /\ (((forall sfd_common_divisor_injective_datacoprime. (exists pvs_factor_injective_datacoprimeleft. (m) = (sfd_common_divisor_injective_datacoprime) * pvs_factor_injective_datacoprimeleft) -> (exists pvs_factor_injective_datacoprimeright. (n) = (sfd_common_divisor_injective_datacoprime) * pvs_factor_injective_datacoprimeright) -> sfd_common_divisor_injective_datacoprime = 1) /\ (((((exists dst_positive_code_injective_datalefttable dst_positive_scale_injective_datalefttable dst_negative_code_injective_datalefttable dst_negative_scale_injective_datalefttable. (((A) = (((((dst_positive_code_injective_datalefttable) + (dst_positive_scale_injective_datalefttable)) * S ((dst_positive_code_injective_datalefttable) + (dst_positive_scale_injective_datalefttable)) + ((dst_positive_scale_injective_datalefttable) + (dst_positive_scale_injective_datalefttable))) + (((dst_negative_code_injective_datalefttable) + (dst_negative_scale_injective_datalefttable)) * S ((dst_negative_code_injective_datalefttable) + (dst_negative_scale_injective_datalefttable)) + ((dst_negative_scale_injective_datalefttable) + (dst_negative_scale_injective_datalefttable)))) * S ((((dst_positive_code_injective_datalefttable) + (dst_positive_scale_injective_datalefttable)) * S ((dst_positive_code_injective_datalefttable) + (dst_positive_scale_injective_datalefttable)) + ((dst_positive_scale_injective_datalefttable) + (dst_positive_scale_injective_datalefttable))) + (((dst_negative_code_injective_datalefttable) + (dst_negative_scale_injective_datalefttable)) * S ((dst_negative_code_injective_datalefttable) + (dst_negative_scale_injective_datalefttable)) + ((dst_negative_scale_injective_datalefttable) + (dst_negative_scale_injective_datalefttable)))) + ((((dst_negative_code_injective_datalefttable) + (dst_negative_scale_injective_datalefttable)) * S ((dst_negative_code_injective_datalefttable) + (dst_negative_scale_injective_datalefttable)) + ((dst_negative_scale_injective_datalefttable) + (dst_negative_scale_injective_datalefttable))) + (((dst_negative_code_injective_datalefttable) + (dst_negative_scale_injective_datalefttable)) * S ((dst_negative_code_injective_datalefttable) + (dst_negative_scale_injective_datalefttable)) + ((dst_negative_scale_injective_datalefttable) + (dst_negative_scale_injective_datalefttable)))))) /\ (forall dst_index_injective_datalefttable. (exists pvs_le_gap_injective_datalefttabledomain. pvs_le_gap_injective_datalefttabledomain + (dst_index_injective_datalefttable) = (m)) -> exists dst_positive_injective_datalefttable dst_negative_injective_datalefttable dst_value_injective_datalefttable. ((((exists ff_h_pvs_injective_datalefttableentrypositive. ff_h_pvs_injective_datalefttableentrypositive + S (dst_positive_injective_datalefttable) = S ((S (dst_index_injective_datalefttable)) * dst_positive_scale_injective_datalefttable)) /\ exists ff_q_pvs_injective_datalefttableentrypositive. dst_positive_code_injective_datalefttable = ff_q_pvs_injective_datalefttableentrypositive * S ((S (dst_index_injective_datalefttable)) * dst_positive_scale_injective_datalefttable) + (dst_positive_injective_datalefttable))) /\ (((((exists ff_h_pvs_injective_datalefttableentrynegative. ff_h_pvs_injective_datalefttableentrynegative + S (dst_negative_injective_datalefttable) = S ((S (dst_index_injective_datalefttable)) * dst_negative_scale_injective_datalefttable)) /\ exists ff_q_pvs_injective_datalefttableentrynegative. dst_negative_code_injective_datalefttable = ff_q_pvs_injective_datalefttableentrynegative * S ((S (dst_index_injective_datalefttable)) * dst_negative_scale_injective_datalefttable) + (dst_negative_injective_datalefttable))) /\ (exists ge_balance_positive_injective_datalefttableentryvalue ge_balance_negative_injective_datalefttableentryvalue. (((((dst_value_injective_datalefttable) = 2 * (ge_balance_positive_injective_datalefttableentryvalue) /\ (ge_balance_negative_injective_datalefttableentryvalue) = 0) \/ exists ge_signed_half_injective_datalefttableentryvaluedecode. (((dst_value_injective_datalefttable) = 2 * ge_signed_half_injective_datalefttableentryvaluedecode + 1 /\ (ge_balance_positive_injective_datalefttableentryvalue) = 0) /\ (ge_balance_negative_injective_datalefttableentryvalue) = S ge_signed_half_injective_datalefttableentryvaluedecode))) /\ ((dst_positive_injective_datalefttable) + ge_balance_negative_injective_datalefttableentryvalue = (dst_negative_injective_datalefttable) + ge_balance_positive_injective_datalefttableentryvalue))))))))) /\ (forall dc_index_injective_dataleft dc_value_injective_dataleft. (exists pvs_le_gap_injective_dataleftdomain. pvs_le_gap_injective_dataleftdomain + (dc_index_injective_dataleft) = (m)) -> (exists dst_positive_code_injective_dataleftlookup dst_positive_scale_injective_dataleftlookup dst_negative_code_injective_dataleftlookup dst_negative_scale_injective_dataleftlookup dst_positive_injective_dataleftlookup dst_negative_injective_dataleftlookup. (((A) = (((((dst_positive_code_injective_dataleftlookup) + (dst_positive_scale_injective_dataleftlookup)) * S ((dst_positive_code_injective_dataleftlookup) + (dst_positive_scale_injective_dataleftlookup)) + ((dst_positive_scale_injective_dataleftlookup) + (dst_positive_scale_injective_dataleftlookup))) + (((dst_negative_code_injective_dataleftlookup) + (dst_negative_scale_injective_dataleftlookup)) * S ((dst_negative_code_injective_dataleftlookup) + (dst_negative_scale_injective_dataleftlookup)) + ((dst_negative_scale_injective_dataleftlookup) + (dst_negative_scale_injective_dataleftlookup)))) * S ((((dst_positive_code_injective_dataleftlookup) + (dst_positive_scale_injective_dataleftlookup)) * S ((dst_positive_code_injective_dataleftlookup) + (dst_positive_scale_injective_dataleftlookup)) + ((dst_positive_scale_injective_dataleftlookup) + (dst_positive_scale_injective_dataleftlookup))) + (((dst_negative_code_injective_dataleftlookup) + (dst_negative_scale_injective_dataleftlookup)) * S ((dst_negative_code_injective_dataleftlookup) + (dst_negative_scale_injective_dataleftlookup)) + ((dst_negative_scale_injective_dataleftlookup) + (dst_negative_scale_injective_dataleftlookup)))) + ((((dst_negative_code_injective_dataleftlookup) + (dst_negative_scale_injective_dataleftlookup)) * S ((dst_negative_code_injective_dataleftlookup) + (dst_negative_scale_injective_dataleftlookup)) + ((dst_negative_scale_injective_dataleftlookup) + (dst_negative_scale_injective_dataleftlookup))) + (((dst_negative_code_injective_dataleftlookup) + (dst_negative_scale_injective_dataleftlookup)) * S ((dst_negative_code_injective_dataleftlookup) + (dst_negative_scale_injective_dataleftlookup)) + ((dst_negative_scale_injective_dataleftlookup) + (dst_negative_scale_injective_dataleftlookup)))))) /\ (((((exists ff_h_pvs_injective_dataleftlookuppositive. ff_h_pvs_injective_dataleftlookuppositive + S (dst_positive_injective_dataleftlookup) = S ((S (dc_index_injective_dataleft)) * dst_positive_scale_injective_dataleftlookup)) /\ exists ff_q_pvs_injective_dataleftlookuppositive. dst_positive_code_injective_dataleftlookup = ff_q_pvs_injective_dataleftlookuppositive * S ((S (dc_index_injective_dataleft)) * dst_positive_scale_injective_dataleftlookup) + (dst_positive_injective_dataleftlookup))) /\ (((((exists ff_h_pvs_injective_dataleftlookupnegative. ff_h_pvs_injective_dataleftlookupnegative + S (dst_negative_injective_dataleftlookup) = S ((S (dc_index_injective_dataleft)) * dst_negative_scale_injective_dataleftlookup)) /\ exists ff_q_pvs_injective_dataleftlookupnegative. dst_negative_code_injective_dataleftlookup = ff_q_pvs_injective_dataleftlookupnegative * S ((S (dc_index_injective_dataleft)) * dst_negative_scale_injective_dataleftlookup) + (dst_negative_injective_dataleftlookup))) /\ (exists ge_balance_positive_injective_dataleftlookupvalue ge_balance_negative_injective_dataleftlookupvalue. (((((dc_value_injective_dataleft) = 2 * (ge_balance_positive_injective_dataleftlookupvalue) /\ (ge_balance_negative_injective_dataleftlookupvalue) = 0) \/ exists ge_signed_half_injective_dataleftlookupvaluedecode. (((dc_value_injective_dataleft) = 2 * ge_signed_half_injective_dataleftlookupvaluedecode + 1 /\ (ge_balance_positive_injective_dataleftlookupvalue) = 0) /\ (ge_balance_negative_injective_dataleftlookupvalue) = S ge_signed_half_injective_dataleftlookupvaluedecode))) /\ ((dst_positive_injective_dataleftlookup) + ge_balance_negative_injective_dataleftlookupvalue = (dst_negative_injective_dataleftlookup) + ge_balance_positive_injective_dataleftlookupvalue))))))))) -> ((((~((dc_index_injective_dataleft)=0)) /\ (exists dc_quotient_injective_dataleftentry dc_left_injective_dataleftentry dc_right_injective_dataleftentry. (((m)=(dc_index_injective_dataleft)*dc_quotient_injective_dataleftentry) /\ (((exists dst_positive_code_injective_dataleftentryleft dst_positive_scale_injective_dataleftentryleft dst_negative_code_injective_dataleftentryleft dst_negative_scale_injective_dataleftentryleft dst_positive_injective_dataleftentryleft dst_negative_injective_dataleftentryleft. (((F) = (((((dst_positive_code_injective_dataleftentryleft) + (dst_positive_scale_injective_dataleftentryleft)) * S ((dst_positive_code_injective_dataleftentryleft) + (dst_positive_scale_injective_dataleftentryleft)) + ((dst_positive_scale_injective_dataleftentryleft) + (dst_positive_scale_injective_dataleftentryleft))) + (((dst_negative_code_injective_dataleftentryleft) + (dst_negative_scale_injective_dataleftentryleft)) * S ((dst_negative_code_injective_dataleftentryleft) + (dst_negative_scale_injective_dataleftentryleft)) + ((dst_negative_scale_injective_dataleftentryleft) + (dst_negative_scale_injective_dataleftentryleft)))) * S ((((dst_positive_code_injective_dataleftentryleft) + (dst_positive_scale_injective_dataleftentryleft)) * S ((dst_positive_code_injective_dataleftentryleft) + (dst_positive_scale_injective_dataleftentryleft)) + ((dst_positive_scale_injective_dataleftentryleft) + (dst_positive_scale_injective_dataleftentryleft))) + (((dst_negative_code_injective_dataleftentryleft) + (dst_negative_scale_injective_dataleftentryleft)) * S ((dst_negative_code_injective_dataleftentryleft) + (dst_negative_scale_injective_dataleftentryleft)) + ((dst_negative_scale_injective_dataleftentryleft) + (dst_negative_scale_injective_dataleftentryleft)))) + ((((dst_negative_code_injective_dataleftentryleft) + (dst_negative_scale_injective_dataleftentryleft)) * S ((dst_negative_code_injective_dataleftentryleft) + (dst_negative_scale_injective_dataleftentryleft)) + ((dst_negative_scale_injective_dataleftentryleft) + (dst_negative_scale_injective_dataleftentryleft))) + (((dst_negative_code_injective_dataleftentryleft) + (dst_negative_scale_injective_dataleftentryleft)) * S ((dst_negative_code_injective_dataleftentryleft) + (dst_negative_scale_injective_dataleftentryleft)) + ((dst_negative_scale_injective_dataleftentryleft) + (dst_negative_scale_injective_dataleftentryleft)))))) /\ (((((exists ff_h_pvs_injective_dataleftentryleftpositive. ff_h_pvs_injective_dataleftentryleftpositive + S (dst_positive_injective_dataleftentryleft) = S ((S (dc_index_injective_dataleft)) * dst_positive_scale_injective_dataleftentryleft)) /\ exists ff_q_pvs_injective_dataleftentryleftpositive. dst_positive_code_injective_dataleftentryleft = ff_q_pvs_injective_dataleftentryleftpositive * S ((S (dc_index_injective_dataleft)) * dst_positive_scale_injective_dataleftentryleft) + (dst_positive_injective_dataleftentryleft))) /\ (((((exists ff_h_pvs_injective_dataleftentryleftnegative. ff_h_pvs_injective_dataleftentryleftnegative + S (dst_negative_injective_dataleftentryleft) = S ((S (dc_index_injective_dataleft)) * dst_negative_scale_injective_dataleftentryleft)) /\ exists ff_q_pvs_injective_dataleftentryleftnegative. dst_negative_code_injective_dataleftentryleft = ff_q_pvs_injective_dataleftentryleftnegative * S ((S (dc_index_injective_dataleft)) * dst_negative_scale_injective_dataleftentryleft) + (dst_negative_injective_dataleftentryleft))) /\ (exists ge_balance_positive_injective_dataleftentryleftvalue ge_balance_negative_injective_dataleftentryleftvalue. (((((dc_left_injective_dataleftentry) = 2 * (ge_balance_positive_injective_dataleftentryleftvalue) /\ (ge_balance_negative_injective_dataleftentryleftvalue) = 0) \/ exists ge_signed_half_injective_dataleftentryleftvaluedecode. (((dc_left_injective_dataleftentry) = 2 * ge_signed_half_injective_dataleftentryleftvaluedecode + 1 /\ (ge_balance_positive_injective_dataleftentryleftvalue) = 0) /\ (ge_balance_negative_injective_dataleftentryleftvalue) = S ge_signed_half_injective_dataleftentryleftvaluedecode))) /\ ((dst_positive_injective_dataleftentryleft) + ge_balance_negative_injective_dataleftentryleftvalue = (dst_negative_injective_dataleftentryleft) + ge_balance_positive_injective_dataleftentryleftvalue))))))))) /\ (((exists dst_positive_code_injective_dataleftentryright dst_positive_scale_injective_dataleftentryright dst_negative_code_injective_dataleftentryright dst_negative_scale_injective_dataleftentryright dst_positive_injective_dataleftentryright dst_negative_injective_dataleftentryright. (((G) = (((((dst_positive_code_injective_dataleftentryright) + (dst_positive_scale_injective_dataleftentryright)) * S ((dst_positive_code_injective_dataleftentryright) + (dst_positive_scale_injective_dataleftentryright)) + ((dst_positive_scale_injective_dataleftentryright) + (dst_positive_scale_injective_dataleftentryright))) + (((dst_negative_code_injective_dataleftentryright) + (dst_negative_scale_injective_dataleftentryright)) * S ((dst_negative_code_injective_dataleftentryright) + (dst_negative_scale_injective_dataleftentryright)) + ((dst_negative_scale_injective_dataleftentryright) + (dst_negative_scale_injective_dataleftentryright)))) * S ((((dst_positive_code_injective_dataleftentryright) + (dst_positive_scale_injective_dataleftentryright)) * S ((dst_positive_code_injective_dataleftentryright) + (dst_positive_scale_injective_dataleftentryright)) + ((dst_positive_scale_injective_dataleftentryright) + (dst_positive_scale_injective_dataleftentryright))) + (((dst_negative_code_injective_dataleftentryright) + (dst_negative_scale_injective_dataleftentryright)) * S ((dst_negative_code_injective_dataleftentryright) + (dst_negative_scale_injective_dataleftentryright)) + ((dst_negative_scale_injective_dataleftentryright) + (dst_negative_scale_injective_dataleftentryright)))) + ((((dst_negative_code_injective_dataleftentryright) + (dst_negative_scale_injective_dataleftentryright)) * S ((dst_negative_code_injective_dataleftentryright) + (dst_negative_scale_injective_dataleftentryright)) + ((dst_negative_scale_injective_dataleftentryright) + (dst_negative_scale_injective_dataleftentryright))) + (((dst_negative_code_injective_dataleftentryright) + (dst_negative_scale_injective_dataleftentryright)) * S ((dst_negative_code_injective_dataleftentryright) + (dst_negative_scale_injective_dataleftentryright)) + ((dst_negative_scale_injective_dataleftentryright) + (dst_negative_scale_injective_dataleftentryright)))))) /\ (((((exists ff_h_pvs_injective_dataleftentryrightpositive. ff_h_pvs_injective_dataleftentryrightpositive + S (dst_positive_injective_dataleftentryright) = S ((S (dc_quotient_injective_dataleftentry)) * dst_positive_scale_injective_dataleftentryright)) /\ exists ff_q_pvs_injective_dataleftentryrightpositive. dst_positive_code_injective_dataleftentryright = ff_q_pvs_injective_dataleftentryrightpositive * S ((S (dc_quotient_injective_dataleftentry)) * dst_positive_scale_injective_dataleftentryright) + (dst_positive_injective_dataleftentryright))) /\ (((((exists ff_h_pvs_injective_dataleftentryrightnegative. ff_h_pvs_injective_dataleftentryrightnegative + S (dst_negative_injective_dataleftentryright) = S ((S (dc_quotient_injective_dataleftentry)) * dst_negative_scale_injective_dataleftentryright)) /\ exists ff_q_pvs_injective_dataleftentryrightnegative. dst_negative_code_injective_dataleftentryright = ff_q_pvs_injective_dataleftentryrightnegative * S ((S (dc_quotient_injective_dataleftentry)) * dst_negative_scale_injective_dataleftentryright) + (dst_negative_injective_dataleftentryright))) /\ (exists ge_balance_positive_injective_dataleftentryrightvalue ge_balance_negative_injective_dataleftentryrightvalue. (((((dc_right_injective_dataleftentry) = 2 * (ge_balance_positive_injective_dataleftentryrightvalue) /\ (ge_balance_negative_injective_dataleftentryrightvalue) = 0) \/ exists ge_signed_half_injective_dataleftentryrightvaluedecode. (((dc_right_injective_dataleftentry) = 2 * ge_signed_half_injective_dataleftentryrightvaluedecode + 1 /\ (ge_balance_positive_injective_dataleftentryrightvalue) = 0) /\ (ge_balance_negative_injective_dataleftentryrightvalue) = S ge_signed_half_injective_dataleftentryrightvaluedecode))) /\ ((dst_positive_injective_dataleftentryright) + ge_balance_negative_injective_dataleftentryrightvalue = (dst_negative_injective_dataleftentryright) + ge_balance_positive_injective_dataleftentryrightvalue))))))))) /\ (exists sto_ap_injective_dataleftentryproduct sto_an_injective_dataleftentryproduct sto_bp_injective_dataleftentryproduct sto_bn_injective_dataleftentryproduct sto_cp_injective_dataleftentryproduct sto_cn_injective_dataleftentryproduct. (((((dc_left_injective_dataleftentry) = 2 * (sto_ap_injective_dataleftentryproduct) /\ (sto_an_injective_dataleftentryproduct) = 0) \/ exists ge_signed_half_injective_dataleftentryproductleft. (((dc_left_injective_dataleftentry) = 2 * ge_signed_half_injective_dataleftentryproductleft + 1 /\ (sto_ap_injective_dataleftentryproduct) = 0) /\ (sto_an_injective_dataleftentryproduct) = S ge_signed_half_injective_dataleftentryproductleft))) /\ ((((((dc_right_injective_dataleftentry) = 2 * (sto_bp_injective_dataleftentryproduct) /\ (sto_bn_injective_dataleftentryproduct) = 0) \/ exists ge_signed_half_injective_dataleftentryproductright. (((dc_right_injective_dataleftentry) = 2 * ge_signed_half_injective_dataleftentryproductright + 1 /\ (sto_bp_injective_dataleftentryproduct) = 0) /\ (sto_bn_injective_dataleftentryproduct) = S ge_signed_half_injective_dataleftentryproductright))) /\ ((((((dc_value_injective_dataleft) = 2 * (sto_cp_injective_dataleftentryproduct) /\ (sto_cn_injective_dataleftentryproduct) = 0) \/ exists ge_signed_half_injective_dataleftentryproductoutput. (((dc_value_injective_dataleft) = 2 * ge_signed_half_injective_dataleftentryproductoutput + 1 /\ (sto_cp_injective_dataleftentryproduct) = 0) /\ (sto_cn_injective_dataleftentryproduct) = S ge_signed_half_injective_dataleftentryproductoutput))) /\ ((sto_ap_injective_dataleftentryproduct * sto_bp_injective_dataleftentryproduct + sto_an_injective_dataleftentryproduct * sto_bn_injective_dataleftentryproduct) + sto_cn_injective_dataleftentryproduct = (sto_ap_injective_dataleftentryproduct * sto_bn_injective_dataleftentryproduct + sto_an_injective_dataleftentryproduct * sto_bp_injective_dataleftentryproduct) + sto_cp_injective_dataleftentryproduct))))))))))))))) \/ ((((dc_index_injective_dataleft)=0 \/ ~(exists pvs_factor_injective_dataleftentrynondivisor. (m) = (dc_index_injective_dataleft) * pvs_factor_injective_dataleftentrynondivisor)) /\ ((dc_value_injective_dataleft)=0))))))) /\ (((((exists dst_positive_code_injective_datarighttable dst_positive_scale_injective_datarighttable dst_negative_code_injective_datarighttable dst_negative_scale_injective_datarighttable. (((B) = (((((dst_positive_code_injective_datarighttable) + (dst_positive_scale_injective_datarighttable)) * S ((dst_positive_code_injective_datarighttable) + (dst_positive_scale_injective_datarighttable)) + ((dst_positive_scale_injective_datarighttable) + (dst_positive_scale_injective_datarighttable))) + (((dst_negative_code_injective_datarighttable) + (dst_negative_scale_injective_datarighttable)) * S ((dst_negative_code_injective_datarighttable) + (dst_negative_scale_injective_datarighttable)) + ((dst_negative_scale_injective_datarighttable) + (dst_negative_scale_injective_datarighttable)))) * S ((((dst_positive_code_injective_datarighttable) + (dst_positive_scale_injective_datarighttable)) * S ((dst_positive_code_injective_datarighttable) + (dst_positive_scale_injective_datarighttable)) + ((dst_positive_scale_injective_datarighttable) + (dst_positive_scale_injective_datarighttable))) + (((dst_negative_code_injective_datarighttable) + (dst_negative_scale_injective_datarighttable)) * S ((dst_negative_code_injective_datarighttable) + (dst_negative_scale_injective_datarighttable)) + ((dst_negative_scale_injective_datarighttable) + (dst_negative_scale_injective_datarighttable)))) + ((((dst_negative_code_injective_datarighttable) + (dst_negative_scale_injective_datarighttable)) * S ((dst_negative_code_injective_datarighttable) + (dst_negative_scale_injective_datarighttable)) + ((dst_negative_scale_injective_datarighttable) + (dst_negative_scale_injective_datarighttable))) + (((dst_negative_code_injective_datarighttable) + (dst_negative_scale_injective_datarighttable)) * S ((dst_negative_code_injective_datarighttable) + (dst_negative_scale_injective_datarighttable)) + ((dst_negative_scale_injective_datarighttable) + (dst_negative_scale_injective_datarighttable)))))) /\ (forall dst_index_injective_datarighttable. (exists pvs_le_gap_injective_datarighttabledomain. pvs_le_gap_injective_datarighttabledomain + (dst_index_injective_datarighttable) = (n)) -> exists dst_positive_injective_datarighttable dst_negative_injective_datarighttable dst_value_injective_datarighttable. ((((exists ff_h_pvs_injective_datarighttableentrypositive. ff_h_pvs_injective_datarighttableentrypositive + S (dst_positive_injective_datarighttable) = S ((S (dst_index_injective_datarighttable)) * dst_positive_scale_injective_datarighttable)) /\ exists ff_q_pvs_injective_datarighttableentrypositive. dst_positive_code_injective_datarighttable = ff_q_pvs_injective_datarighttableentrypositive * S ((S (dst_index_injective_datarighttable)) * dst_positive_scale_injective_datarighttable) + (dst_positive_injective_datarighttable))) /\ (((((exists ff_h_pvs_injective_datarighttableentrynegative. ff_h_pvs_injective_datarighttableentrynegative + S (dst_negative_injective_datarighttable) = S ((S (dst_index_injective_datarighttable)) * dst_negative_scale_injective_datarighttable)) /\ exists ff_q_pvs_injective_datarighttableentrynegative. dst_negative_code_injective_datarighttable = ff_q_pvs_injective_datarighttableentrynegative * S ((S (dst_index_injective_datarighttable)) * dst_negative_scale_injective_datarighttable) + (dst_negative_injective_datarighttable))) /\ (exists ge_balance_positive_injective_datarighttableentryvalue ge_balance_negative_injective_datarighttableentryvalue. (((((dst_value_injective_datarighttable) = 2 * (ge_balance_positive_injective_datarighttableentryvalue) /\ (ge_balance_negative_injective_datarighttableentryvalue) = 0) \/ exists ge_signed_half_injective_datarighttableentryvaluedecode. (((dst_value_injective_datarighttable) = 2 * ge_signed_half_injective_datarighttableentryvaluedecode + 1 /\ (ge_balance_positive_injective_datarighttableentryvalue) = 0) /\ (ge_balance_negative_injective_datarighttableentryvalue) = S ge_signed_half_injective_datarighttableentryvaluedecode))) /\ ((dst_positive_injective_datarighttable) + ge_balance_negative_injective_datarighttableentryvalue = (dst_negative_injective_datarighttable) + ge_balance_positive_injective_datarighttableentryvalue))))))))) /\ (forall dc_index_injective_dataright dc_value_injective_dataright. (exists pvs_le_gap_injective_datarightdomain. pvs_le_gap_injective_datarightdomain + (dc_index_injective_dataright) = (n)) -> (exists dst_positive_code_injective_datarightlookup dst_positive_scale_injective_datarightlookup dst_negative_code_injective_datarightlookup dst_negative_scale_injective_datarightlookup dst_positive_injective_datarightlookup dst_negative_injective_datarightlookup. (((B) = (((((dst_positive_code_injective_datarightlookup) + (dst_positive_scale_injective_datarightlookup)) * S ((dst_positive_code_injective_datarightlookup) + (dst_positive_scale_injective_datarightlookup)) + ((dst_positive_scale_injective_datarightlookup) + (dst_positive_scale_injective_datarightlookup))) + (((dst_negative_code_injective_datarightlookup) + (dst_negative_scale_injective_datarightlookup)) * S ((dst_negative_code_injective_datarightlookup) + (dst_negative_scale_injective_datarightlookup)) + ((dst_negative_scale_injective_datarightlookup) + (dst_negative_scale_injective_datarightlookup)))) * S ((((dst_positive_code_injective_datarightlookup) + (dst_positive_scale_injective_datarightlookup)) * S ((dst_positive_code_injective_datarightlookup) + (dst_positive_scale_injective_datarightlookup)) + ((dst_positive_scale_injective_datarightlookup) + (dst_positive_scale_injective_datarightlookup))) + (((dst_negative_code_injective_datarightlookup) + (dst_negative_scale_injective_datarightlookup)) * S ((dst_negative_code_injective_datarightlookup) + (dst_negative_scale_injective_datarightlookup)) + ((dst_negative_scale_injective_datarightlookup) + (dst_negative_scale_injective_datarightlookup)))) + ((((dst_negative_code_injective_datarightlookup) + (dst_negative_scale_injective_datarightlookup)) * S ((dst_negative_code_injective_datarightlookup) + (dst_negative_scale_injective_datarightlookup)) + ((dst_negative_scale_injective_datarightlookup) + (dst_negative_scale_injective_datarightlookup))) + (((dst_negative_code_injective_datarightlookup) + (dst_negative_scale_injective_datarightlookup)) * S ((dst_negative_code_injective_datarightlookup) + (dst_negative_scale_injective_datarightlookup)) + ((dst_negative_scale_injective_datarightlookup) + (dst_negative_scale_injective_datarightlookup)))))) /\ (((((exists ff_h_pvs_injective_datarightlookuppositive. ff_h_pvs_injective_datarightlookuppositive + S (dst_positive_injective_datarightlookup) = S ((S (dc_index_injective_dataright)) * dst_positive_scale_injective_datarightlookup)) /\ exists ff_q_pvs_injective_datarightlookuppositive. dst_positive_code_injective_datarightlookup = ff_q_pvs_injective_datarightlookuppositive * S ((S (dc_index_injective_dataright)) * dst_positive_scale_injective_datarightlookup) + (dst_positive_injective_datarightlookup))) /\ (((((exists ff_h_pvs_injective_datarightlookupnegative. ff_h_pvs_injective_datarightlookupnegative + S (dst_negative_injective_datarightlookup) = S ((S (dc_index_injective_dataright)) * dst_negative_scale_injective_datarightlookup)) /\ exists ff_q_pvs_injective_datarightlookupnegative. dst_negative_code_injective_datarightlookup = ff_q_pvs_injective_datarightlookupnegative * S ((S (dc_index_injective_dataright)) * dst_negative_scale_injective_datarightlookup) + (dst_negative_injective_datarightlookup))) /\ (exists ge_balance_positive_injective_datarightlookupvalue ge_balance_negative_injective_datarightlookupvalue. (((((dc_value_injective_dataright) = 2 * (ge_balance_positive_injective_datarightlookupvalue) /\ (ge_balance_negative_injective_datarightlookupvalue) = 0) \/ exists ge_signed_half_injective_datarightlookupvaluedecode. (((dc_value_injective_dataright) = 2 * ge_signed_half_injective_datarightlookupvaluedecode + 1 /\ (ge_balance_positive_injective_datarightlookupvalue) = 0) /\ (ge_balance_negative_injective_datarightlookupvalue) = S ge_signed_half_injective_datarightlookupvaluedecode))) /\ ((dst_positive_injective_datarightlookup) + ge_balance_negative_injective_datarightlookupvalue = (dst_negative_injective_datarightlookup) + ge_balance_positive_injective_datarightlookupvalue))))))))) -> ((((~((dc_index_injective_dataright)=0)) /\ (exists dc_quotient_injective_datarightentry dc_left_injective_datarightentry dc_right_injective_datarightentry. (((n)=(dc_index_injective_dataright)*dc_quotient_injective_datarightentry) /\ (((exists dst_positive_code_injective_datarightentryleft dst_positive_scale_injective_datarightentryleft dst_negative_code_injective_datarightentryleft dst_negative_scale_injective_datarightentryleft dst_positive_injective_datarightentryleft dst_negative_injective_datarightentryleft. (((F) = (((((dst_positive_code_injective_datarightentryleft) + (dst_positive_scale_injective_datarightentryleft)) * S ((dst_positive_code_injective_datarightentryleft) + (dst_positive_scale_injective_datarightentryleft)) + ((dst_positive_scale_injective_datarightentryleft) + (dst_positive_scale_injective_datarightentryleft))) + (((dst_negative_code_injective_datarightentryleft) + (dst_negative_scale_injective_datarightentryleft)) * S ((dst_negative_code_injective_datarightentryleft) + (dst_negative_scale_injective_datarightentryleft)) + ((dst_negative_scale_injective_datarightentryleft) + (dst_negative_scale_injective_datarightentryleft)))) * S ((((dst_positive_code_injective_datarightentryleft) + (dst_positive_scale_injective_datarightentryleft)) * S ((dst_positive_code_injective_datarightentryleft) + (dst_positive_scale_injective_datarightentryleft)) + ((dst_positive_scale_injective_datarightentryleft) + (dst_positive_scale_injective_datarightentryleft))) + (((dst_negative_code_injective_datarightentryleft) + (dst_negative_scale_injective_datarightentryleft)) * S ((dst_negative_code_injective_datarightentryleft) + (dst_negative_scale_injective_datarightentryleft)) + ((dst_negative_scale_injective_datarightentryleft) + (dst_negative_scale_injective_datarightentryleft)))) + ((((dst_negative_code_injective_datarightentryleft) + (dst_negative_scale_injective_datarightentryleft)) * S ((dst_negative_code_injective_datarightentryleft) + (dst_negative_scale_injective_datarightentryleft)) + ((dst_negative_scale_injective_datarightentryleft) + (dst_negative_scale_injective_datarightentryleft))) + (((dst_negative_code_injective_datarightentryleft) + (dst_negative_scale_injective_datarightentryleft)) * S ((dst_negative_code_injective_datarightentryleft) + (dst_negative_scale_injective_datarightentryleft)) + ((dst_negative_scale_injective_datarightentryleft) + (dst_negative_scale_injective_datarightentryleft)))))) /\ (((((exists ff_h_pvs_injective_datarightentryleftpositive. ff_h_pvs_injective_datarightentryleftpositive + S (dst_positive_injective_datarightentryleft) = S ((S (dc_index_injective_dataright)) * dst_positive_scale_injective_datarightentryleft)) /\ exists ff_q_pvs_injective_datarightentryleftpositive. dst_positive_code_injective_datarightentryleft = ff_q_pvs_injective_datarightentryleftpositive * S ((S (dc_index_injective_dataright)) * dst_positive_scale_injective_datarightentryleft) + (dst_positive_injective_datarightentryleft))) /\ (((((exists ff_h_pvs_injective_datarightentryleftnegative. ff_h_pvs_injective_datarightentryleftnegative + S (dst_negative_injective_datarightentryleft) = S ((S (dc_index_injective_dataright)) * dst_negative_scale_injective_datarightentryleft)) /\ exists ff_q_pvs_injective_datarightentryleftnegative. dst_negative_code_injective_datarightentryleft = ff_q_pvs_injective_datarightentryleftnegative * S ((S (dc_index_injective_dataright)) * dst_negative_scale_injective_datarightentryleft) + (dst_negative_injective_datarightentryleft))) /\ (exists ge_balance_positive_injective_datarightentryleftvalue ge_balance_negative_injective_datarightentryleftvalue. (((((dc_left_injective_datarightentry) = 2 * (ge_balance_positive_injective_datarightentryleftvalue) /\ (ge_balance_negative_injective_datarightentryleftvalue) = 0) \/ exists ge_signed_half_injective_datarightentryleftvaluedecode. (((dc_left_injective_datarightentry) = 2 * ge_signed_half_injective_datarightentryleftvaluedecode + 1 /\ (ge_balance_positive_injective_datarightentryleftvalue) = 0) /\ (ge_balance_negative_injective_datarightentryleftvalue) = S ge_signed_half_injective_datarightentryleftvaluedecode))) /\ ((dst_positive_injective_datarightentryleft) + ge_balance_negative_injective_datarightentryleftvalue = (dst_negative_injective_datarightentryleft) + ge_balance_positive_injective_datarightentryleftvalue))))))))) /\ (((exists dst_positive_code_injective_datarightentryright dst_positive_scale_injective_datarightentryright dst_negative_code_injective_datarightentryright dst_negative_scale_injective_datarightentryright dst_positive_injective_datarightentryright dst_negative_injective_datarightentryright. (((G) = (((((dst_positive_code_injective_datarightentryright) + (dst_positive_scale_injective_datarightentryright)) * S ((dst_positive_code_injective_datarightentryright) + (dst_positive_scale_injective_datarightentryright)) + ((dst_positive_scale_injective_datarightentryright) + (dst_positive_scale_injective_datarightentryright))) + (((dst_negative_code_injective_datarightentryright) + (dst_negative_scale_injective_datarightentryright)) * S ((dst_negative_code_injective_datarightentryright) + (dst_negative_scale_injective_datarightentryright)) + ((dst_negative_scale_injective_datarightentryright) + (dst_negative_scale_injective_datarightentryright)))) * S ((((dst_positive_code_injective_datarightentryright) + (dst_positive_scale_injective_datarightentryright)) * S ((dst_positive_code_injective_datarightentryright) + (dst_positive_scale_injective_datarightentryright)) + ((dst_positive_scale_injective_datarightentryright) + (dst_positive_scale_injective_datarightentryright))) + (((dst_negative_code_injective_datarightentryright) + (dst_negative_scale_injective_datarightentryright)) * S ((dst_negative_code_injective_datarightentryright) + (dst_negative_scale_injective_datarightentryright)) + ((dst_negative_scale_injective_datarightentryright) + (dst_negative_scale_injective_datarightentryright)))) + ((((dst_negative_code_injective_datarightentryright) + (dst_negative_scale_injective_datarightentryright)) * S ((dst_negative_code_injective_datarightentryright) + (dst_negative_scale_injective_datarightentryright)) + ((dst_negative_scale_injective_datarightentryright) + (dst_negative_scale_injective_datarightentryright))) + (((dst_negative_code_injective_datarightentryright) + (dst_negative_scale_injective_datarightentryright)) * S ((dst_negative_code_injective_datarightentryright) + (dst_negative_scale_injective_datarightentryright)) + ((dst_negative_scale_injective_datarightentryright) + (dst_negative_scale_injective_datarightentryright)))))) /\ (((((exists ff_h_pvs_injective_datarightentryrightpositive. ff_h_pvs_injective_datarightentryrightpositive + S (dst_positive_injective_datarightentryright) = S ((S (dc_quotient_injective_datarightentry)) * dst_positive_scale_injective_datarightentryright)) /\ exists ff_q_pvs_injective_datarightentryrightpositive. dst_positive_code_injective_datarightentryright = ff_q_pvs_injective_datarightentryrightpositive * S ((S (dc_quotient_injective_datarightentry)) * dst_positive_scale_injective_datarightentryright) + (dst_positive_injective_datarightentryright))) /\ (((((exists ff_h_pvs_injective_datarightentryrightnegative. ff_h_pvs_injective_datarightentryrightnegative + S (dst_negative_injective_datarightentryright) = S ((S (dc_quotient_injective_datarightentry)) * dst_negative_scale_injective_datarightentryright)) /\ exists ff_q_pvs_injective_datarightentryrightnegative. dst_negative_code_injective_datarightentryright = ff_q_pvs_injective_datarightentryrightnegative * S ((S (dc_quotient_injective_datarightentry)) * dst_negative_scale_injective_datarightentryright) + (dst_negative_injective_datarightentryright))) /\ (exists ge_balance_positive_injective_datarightentryrightvalue ge_balance_negative_injective_datarightentryrightvalue. (((((dc_right_injective_datarightentry) = 2 * (ge_balance_positive_injective_datarightentryrightvalue) /\ (ge_balance_negative_injective_datarightentryrightvalue) = 0) \/ exists ge_signed_half_injective_datarightentryrightvaluedecode. (((dc_right_injective_datarightentry) = 2 * ge_signed_half_injective_datarightentryrightvaluedecode + 1 /\ (ge_balance_positive_injective_datarightentryrightvalue) = 0) /\ (ge_balance_negative_injective_datarightentryrightvalue) = S ge_signed_half_injective_datarightentryrightvaluedecode))) /\ ((dst_positive_injective_datarightentryright) + ge_balance_negative_injective_datarightentryrightvalue = (dst_negative_injective_datarightentryright) + ge_balance_positive_injective_datarightentryrightvalue))))))))) /\ (exists sto_ap_injective_datarightentryproduct sto_an_injective_datarightentryproduct sto_bp_injective_datarightentryproduct sto_bn_injective_datarightentryproduct sto_cp_injective_datarightentryproduct sto_cn_injective_datarightentryproduct. (((((dc_left_injective_datarightentry) = 2 * (sto_ap_injective_datarightentryproduct) /\ (sto_an_injective_datarightentryproduct) = 0) \/ exists ge_signed_half_injective_datarightentryproductleft. (((dc_left_injective_datarightentry) = 2 * ge_signed_half_injective_datarightentryproductleft + 1 /\ (sto_ap_injective_datarightentryproduct) = 0) /\ (sto_an_injective_datarightentryproduct) = S ge_signed_half_injective_datarightentryproductleft))) /\ ((((((dc_right_injective_datarightentry) = 2 * (sto_bp_injective_datarightentryproduct) /\ (sto_bn_injective_datarightentryproduct) = 0) \/ exists ge_signed_half_injective_datarightentryproductright. (((dc_right_injective_datarightentry) = 2 * ge_signed_half_injective_datarightentryproductright + 1 /\ (sto_bp_injective_datarightentryproduct) = 0) /\ (sto_bn_injective_datarightentryproduct) = S ge_signed_half_injective_datarightentryproductright))) /\ ((((((dc_value_injective_dataright) = 2 * (sto_cp_injective_datarightentryproduct) /\ (sto_cn_injective_datarightentryproduct) = 0) \/ exists ge_signed_half_injective_datarightentryproductoutput. (((dc_value_injective_dataright) = 2 * ge_signed_half_injective_datarightentryproductoutput + 1 /\ (sto_cp_injective_datarightentryproduct) = 0) /\ (sto_cn_injective_datarightentryproduct) = S ge_signed_half_injective_datarightentryproductoutput))) /\ ((sto_ap_injective_datarightentryproduct * sto_bp_injective_datarightentryproduct + sto_an_injective_datarightentryproduct * sto_bn_injective_datarightentryproduct) + sto_cn_injective_datarightentryproduct = (sto_ap_injective_datarightentryproduct * sto_bn_injective_datarightentryproduct + sto_an_injective_datarightentryproduct * sto_bp_injective_datarightentryproduct) + sto_cp_injective_datarightentryproduct))))))))))))))) \/ ((((dc_index_injective_dataright)=0 \/ ~(exists pvs_factor_injective_datarightentrynondivisor. (n) = (dc_index_injective_dataright) * pvs_factor_injective_datarightentrynondivisor)) /\ ((dc_value_injective_dataright)=0))))))) /\ (((((exists dst_positive_code_injective_datacartesianF dst_positive_scale_injective_datacartesianF dst_negative_code_injective_datacartesianF dst_negative_scale_injective_datacartesianF. (((A) = (((((dst_positive_code_injective_datacartesianF) + (dst_positive_scale_injective_datacartesianF)) * S ((dst_positive_code_injective_datacartesianF) + (dst_positive_scale_injective_datacartesianF)) + ((dst_positive_scale_injective_datacartesianF) + (dst_positive_scale_injective_datacartesianF))) + (((dst_negative_code_injective_datacartesianF) + (dst_negative_scale_injective_datacartesianF)) * S ((dst_negative_code_injective_datacartesianF) + (dst_negative_scale_injective_datacartesianF)) + ((dst_negative_scale_injective_datacartesianF) + (dst_negative_scale_injective_datacartesianF)))) * S ((((dst_positive_code_injective_datacartesianF) + (dst_positive_scale_injective_datacartesianF)) * S ((dst_positive_code_injective_datacartesianF) + (dst_positive_scale_injective_datacartesianF)) + ((dst_positive_scale_injective_datacartesianF) + (dst_positive_scale_injective_datacartesianF))) + (((dst_negative_code_injective_datacartesianF) + (dst_negative_scale_injective_datacartesianF)) * S ((dst_negative_code_injective_datacartesianF) + (dst_negative_scale_injective_datacartesianF)) + ((dst_negative_scale_injective_datacartesianF) + (dst_negative_scale_injective_datacartesianF)))) + ((((dst_negative_code_injective_datacartesianF) + (dst_negative_scale_injective_datacartesianF)) * S ((dst_negative_code_injective_datacartesianF) + (dst_negative_scale_injective_datacartesianF)) + ((dst_negative_scale_injective_datacartesianF) + (dst_negative_scale_injective_datacartesianF))) + (((dst_negative_code_injective_datacartesianF) + (dst_negative_scale_injective_datacartesianF)) * S ((dst_negative_code_injective_datacartesianF) + (dst_negative_scale_injective_datacartesianF)) + ((dst_negative_scale_injective_datacartesianF) + (dst_negative_scale_injective_datacartesianF)))))) /\ (forall dst_index_injective_datacartesianF. (exists pvs_le_gap_injective_datacartesianFdomain. pvs_le_gap_injective_datacartesianFdomain + (dst_index_injective_datacartesianF) = (0)) -> exists dst_positive_injective_datacartesianF dst_negative_injective_datacartesianF dst_value_injective_datacartesianF. ((((exists ff_h_pvs_injective_datacartesianFentrypositive. ff_h_pvs_injective_datacartesianFentrypositive + S (dst_positive_injective_datacartesianF) = S ((S (dst_index_injective_datacartesianF)) * dst_positive_scale_injective_datacartesianF)) /\ exists ff_q_pvs_injective_datacartesianFentrypositive. dst_positive_code_injective_datacartesianF = ff_q_pvs_injective_datacartesianFentrypositive * S ((S (dst_index_injective_datacartesianF)) * dst_positive_scale_injective_datacartesianF) + (dst_positive_injective_datacartesianF))) /\ (((((exists ff_h_pvs_injective_datacartesianFentrynegative. ff_h_pvs_injective_datacartesianFentrynegative + S (dst_negative_injective_datacartesianF) = S ((S (dst_index_injective_datacartesianF)) * dst_negative_scale_injective_datacartesianF)) /\ exists ff_q_pvs_injective_datacartesianFentrynegative. dst_negative_code_injective_datacartesianF = ff_q_pvs_injective_datacartesianFentrynegative * S ((S (dst_index_injective_datacartesianF)) * dst_negative_scale_injective_datacartesianF) + (dst_negative_injective_datacartesianF))) /\ (exists ge_balance_positive_injective_datacartesianFentryvalue ge_balance_negative_injective_datacartesianFentryvalue. (((((dst_value_injective_datacartesianF) = 2 * (ge_balance_positive_injective_datacartesianFentryvalue) /\ (ge_balance_negative_injective_datacartesianFentryvalue) = 0) \/ exists ge_signed_half_injective_datacartesianFentryvaluedecode. (((dst_value_injective_datacartesianF) = 2 * ge_signed_half_injective_datacartesianFentryvaluedecode + 1 /\ (ge_balance_positive_injective_datacartesianFentryvalue) = 0) /\ (ge_balance_negative_injective_datacartesianFentryvalue) = S ge_signed_half_injective_datacartesianFentryvaluedecode))) /\ ((dst_positive_injective_datacartesianF) + ge_balance_negative_injective_datacartesianFentryvalue = (dst_negative_injective_datacartesianF) + ge_balance_positive_injective_datacartesianFentryvalue))))))))) /\ (((exists dst_positive_code_injective_datacartesianG dst_positive_scale_injective_datacartesianG dst_negative_code_injective_datacartesianG dst_negative_scale_injective_datacartesianG. (((B) = (((((dst_positive_code_injective_datacartesianG) + (dst_positive_scale_injective_datacartesianG)) * S ((dst_positive_code_injective_datacartesianG) + (dst_positive_scale_injective_datacartesianG)) + ((dst_positive_scale_injective_datacartesianG) + (dst_positive_scale_injective_datacartesianG))) + (((dst_negative_code_injective_datacartesianG) + (dst_negative_scale_injective_datacartesianG)) * S ((dst_negative_code_injective_datacartesianG) + (dst_negative_scale_injective_datacartesianG)) + ((dst_negative_scale_injective_datacartesianG) + (dst_negative_scale_injective_datacartesianG)))) * S ((((dst_positive_code_injective_datacartesianG) + (dst_positive_scale_injective_datacartesianG)) * S ((dst_positive_code_injective_datacartesianG) + (dst_positive_scale_injective_datacartesianG)) + ((dst_positive_scale_injective_datacartesianG) + (dst_positive_scale_injective_datacartesianG))) + (((dst_negative_code_injective_datacartesianG) + (dst_negative_scale_injective_datacartesianG)) * S ((dst_negative_code_injective_datacartesianG) + (dst_negative_scale_injective_datacartesianG)) + ((dst_negative_scale_injective_datacartesianG) + (dst_negative_scale_injective_datacartesianG)))) + ((((dst_negative_code_injective_datacartesianG) + (dst_negative_scale_injective_datacartesianG)) * S ((dst_negative_code_injective_datacartesianG) + (dst_negative_scale_injective_datacartesianG)) + ((dst_negative_scale_injective_datacartesianG) + (dst_negative_scale_injective_datacartesianG))) + (((dst_negative_code_injective_datacartesianG) + (dst_negative_scale_injective_datacartesianG)) * S ((dst_negative_code_injective_datacartesianG) + (dst_negative_scale_injective_datacartesianG)) + ((dst_negative_scale_injective_datacartesianG) + (dst_negative_scale_injective_datacartesianG)))))) /\ (forall dst_index_injective_datacartesianG. (exists pvs_le_gap_injective_datacartesianGdomain. pvs_le_gap_injective_datacartesianGdomain + (dst_index_injective_datacartesianG) = (0)) -> exists dst_positive_injective_datacartesianG dst_negative_injective_datacartesianG dst_value_injective_datacartesianG. ((((exists ff_h_pvs_injective_datacartesianGentrypositive. ff_h_pvs_injective_datacartesianGentrypositive + S (dst_positive_injective_datacartesianG) = S ((S (dst_index_injective_datacartesianG)) * dst_positive_scale_injective_datacartesianG)) /\ exists ff_q_pvs_injective_datacartesianGentrypositive. dst_positive_code_injective_datacartesianG = ff_q_pvs_injective_datacartesianGentrypositive * S ((S (dst_index_injective_datacartesianG)) * dst_positive_scale_injective_datacartesianG) + (dst_positive_injective_datacartesianG))) /\ (((((exists ff_h_pvs_injective_datacartesianGentrynegative. ff_h_pvs_injective_datacartesianGentrynegative + S (dst_negative_injective_datacartesianG) = S ((S (dst_index_injective_datacartesianG)) * dst_negative_scale_injective_datacartesianG)) /\ exists ff_q_pvs_injective_datacartesianGentrynegative. dst_negative_code_injective_datacartesianG = ff_q_pvs_injective_datacartesianGentrynegative * S ((S (dst_index_injective_datacartesianG)) * dst_negative_scale_injective_datacartesianG) + (dst_negative_injective_datacartesianG))) /\ (exists ge_balance_positive_injective_datacartesianGentryvalue ge_balance_negative_injective_datacartesianGentryvalue. (((((dst_value_injective_datacartesianG) = 2 * (ge_balance_positive_injective_datacartesianGentryvalue) /\ (ge_balance_negative_injective_datacartesianGentryvalue) = 0) \/ exists ge_signed_half_injective_datacartesianGentryvaluedecode. (((dst_value_injective_datacartesianG) = 2 * ge_signed_half_injective_datacartesianGentryvaluedecode + 1 /\ (ge_balance_positive_injective_datacartesianGentryvalue) = 0) /\ (ge_balance_negative_injective_datacartesianGentryvalue) = S ge_signed_half_injective_datacartesianGentryvaluedecode))) /\ ((dst_positive_injective_datacartesianG) + ge_balance_negative_injective_datacartesianGentryvalue = (dst_negative_injective_datacartesianG) + ge_balance_positive_injective_datacartesianGentryvalue))))))))) /\ (((exists dst_positive_code_injective_datacartesianT dst_positive_scale_injective_datacartesianT dst_negative_code_injective_datacartesianT dst_negative_scale_injective_datacartesianT. (((T) = (((((dst_positive_code_injective_datacartesianT) + (dst_positive_scale_injective_datacartesianT)) * S ((dst_positive_code_injective_datacartesianT) + (dst_positive_scale_injective_datacartesianT)) + ((dst_positive_scale_injective_datacartesianT) + (dst_positive_scale_injective_datacartesianT))) + (((dst_negative_code_injective_datacartesianT) + (dst_negative_scale_injective_datacartesianT)) * S ((dst_negative_code_injective_datacartesianT) + (dst_negative_scale_injective_datacartesianT)) + ((dst_negative_scale_injective_datacartesianT) + (dst_negative_scale_injective_datacartesianT)))) * S ((((dst_positive_code_injective_datacartesianT) + (dst_positive_scale_injective_datacartesianT)) * S ((dst_positive_code_injective_datacartesianT) + (dst_positive_scale_injective_datacartesianT)) + ((dst_positive_scale_injective_datacartesianT) + (dst_positive_scale_injective_datacartesianT))) + (((dst_negative_code_injective_datacartesianT) + (dst_negative_scale_injective_datacartesianT)) * S ((dst_negative_code_injective_datacartesianT) + (dst_negative_scale_injective_datacartesianT)) + ((dst_negative_scale_injective_datacartesianT) + (dst_negative_scale_injective_datacartesianT)))) + ((((dst_negative_code_injective_datacartesianT) + (dst_negative_scale_injective_datacartesianT)) * S ((dst_negative_code_injective_datacartesianT) + (dst_negative_scale_injective_datacartesianT)) + ((dst_negative_scale_injective_datacartesianT) + (dst_negative_scale_injective_datacartesianT))) + (((dst_negative_code_injective_datacartesianT) + (dst_negative_scale_injective_datacartesianT)) * S ((dst_negative_code_injective_datacartesianT) + (dst_negative_scale_injective_datacartesianT)) + ((dst_negative_scale_injective_datacartesianT) + (dst_negative_scale_injective_datacartesianT)))))) /\ (forall dst_index_injective_datacartesianT. (exists pvs_le_gap_injective_datacartesianTdomain. pvs_le_gap_injective_datacartesianTdomain + (dst_index_injective_datacartesianT) = ((S (m))*(S (n)))) -> exists dst_positive_injective_datacartesianT dst_negative_injective_datacartesianT dst_value_injective_datacartesianT. ((((exists ff_h_pvs_injective_datacartesianTentrypositive. ff_h_pvs_injective_datacartesianTentrypositive + S (dst_positive_injective_datacartesianT) = S ((S (dst_index_injective_datacartesianT)) * dst_positive_scale_injective_datacartesianT)) /\ exists ff_q_pvs_injective_datacartesianTentrypositive. dst_positive_code_injective_datacartesianT = ff_q_pvs_injective_datacartesianTentrypositive * S ((S (dst_index_injective_datacartesianT)) * dst_positive_scale_injective_datacartesianT) + (dst_positive_injective_datacartesianT))) /\ (((((exists ff_h_pvs_injective_datacartesianTentrynegative. ff_h_pvs_injective_datacartesianTentrynegative + S (dst_negative_injective_datacartesianT) = S ((S (dst_index_injective_datacartesianT)) * dst_negative_scale_injective_datacartesianT)) /\ exists ff_q_pvs_injective_datacartesianTentrynegative. dst_negative_code_injective_datacartesianT = ff_q_pvs_injective_datacartesianTentrynegative * S ((S (dst_index_injective_datacartesianT)) * dst_negative_scale_injective_datacartesianT) + (dst_negative_injective_datacartesianT))) /\ (exists ge_balance_positive_injective_datacartesianTentryvalue ge_balance_negative_injective_datacartesianTentryvalue. (((((dst_value_injective_datacartesianT) = 2 * (ge_balance_positive_injective_datacartesianTentryvalue) /\ (ge_balance_negative_injective_datacartesianTentryvalue) = 0) \/ exists ge_signed_half_injective_datacartesianTentryvaluedecode. (((dst_value_injective_datacartesianT) = 2 * ge_signed_half_injective_datacartesianTentryvaluedecode + 1 /\ (ge_balance_positive_injective_datacartesianTentryvalue) = 0) /\ (ge_balance_negative_injective_datacartesianTentryvalue) = S ge_signed_half_injective_datacartesianTentryvaluedecode))) /\ ((dst_positive_injective_datacartesianT) + ge_balance_negative_injective_datacartesianTentryvalue = (dst_negative_injective_datacartesianT) + ge_balance_positive_injective_datacartesianTentryvalue))))))))) /\ (forall scp_row_injective_datacartesian scp_column_injective_datacartesian scp_first_injective_datacartesian scp_second_injective_datacartesian scp_value_injective_datacartesian. (exists pvs_gap_injective_datacartesianrows. pvs_gap_injective_datacartesianrows + S (scp_row_injective_datacartesian) = (S (m))) -> (exists pvs_gap_injective_datacartesiancolumns. pvs_gap_injective_datacartesiancolumns + S (scp_column_injective_datacartesian) = (S (n))) -> (exists dst_positive_code_injective_datacartesianfirst dst_positive_scale_injective_datacartesianfirst dst_negative_code_injective_datacartesianfirst dst_negative_scale_injective_datacartesianfirst dst_positive_injective_datacartesianfirst dst_negative_injective_datacartesianfirst. (((A) = (((((dst_positive_code_injective_datacartesianfirst) + (dst_positive_scale_injective_datacartesianfirst)) * S ((dst_positive_code_injective_datacartesianfirst) + (dst_positive_scale_injective_datacartesianfirst)) + ((dst_positive_scale_injective_datacartesianfirst) + (dst_positive_scale_injective_datacartesianfirst))) + (((dst_negative_code_injective_datacartesianfirst) + (dst_negative_scale_injective_datacartesianfirst)) * S ((dst_negative_code_injective_datacartesianfirst) + (dst_negative_scale_injective_datacartesianfirst)) + ((dst_negative_scale_injective_datacartesianfirst) + (dst_negative_scale_injective_datacartesianfirst)))) * S ((((dst_positive_code_injective_datacartesianfirst) + (dst_positive_scale_injective_datacartesianfirst)) * S ((dst_positive_code_injective_datacartesianfirst) + (dst_positive_scale_injective_datacartesianfirst)) + ((dst_positive_scale_injective_datacartesianfirst) + (dst_positive_scale_injective_datacartesianfirst))) + (((dst_negative_code_injective_datacartesianfirst) + (dst_negative_scale_injective_datacartesianfirst)) * S ((dst_negative_code_injective_datacartesianfirst) + (dst_negative_scale_injective_datacartesianfirst)) + ((dst_negative_scale_injective_datacartesianfirst) + (dst_negative_scale_injective_datacartesianfirst)))) + ((((dst_negative_code_injective_datacartesianfirst) + (dst_negative_scale_injective_datacartesianfirst)) * S ((dst_negative_code_injective_datacartesianfirst) + (dst_negative_scale_injective_datacartesianfirst)) + ((dst_negative_scale_injective_datacartesianfirst) + (dst_negative_scale_injective_datacartesianfirst))) + (((dst_negative_code_injective_datacartesianfirst) + (dst_negative_scale_injective_datacartesianfirst)) * S ((dst_negative_code_injective_datacartesianfirst) + (dst_negative_scale_injective_datacartesianfirst)) + ((dst_negative_scale_injective_datacartesianfirst) + (dst_negative_scale_injective_datacartesianfirst)))))) /\ (((((exists ff_h_pvs_injective_datacartesianfirstpositive. ff_h_pvs_injective_datacartesianfirstpositive + S (dst_positive_injective_datacartesianfirst) = S ((S (scp_row_injective_datacartesian)) * dst_positive_scale_injective_datacartesianfirst)) /\ exists ff_q_pvs_injective_datacartesianfirstpositive. dst_positive_code_injective_datacartesianfirst = ff_q_pvs_injective_datacartesianfirstpositive * S ((S (scp_row_injective_datacartesian)) * dst_positive_scale_injective_datacartesianfirst) + (dst_positive_injective_datacartesianfirst))) /\ (((((exists ff_h_pvs_injective_datacartesianfirstnegative. ff_h_pvs_injective_datacartesianfirstnegative + S (dst_negative_injective_datacartesianfirst) = S ((S (scp_row_injective_datacartesian)) * dst_negative_scale_injective_datacartesianfirst)) /\ exists ff_q_pvs_injective_datacartesianfirstnegative. dst_negative_code_injective_datacartesianfirst = ff_q_pvs_injective_datacartesianfirstnegative * S ((S (scp_row_injective_datacartesian)) * dst_negative_scale_injective_datacartesianfirst) + (dst_negative_injective_datacartesianfirst))) /\ (exists ge_balance_positive_injective_datacartesianfirstvalue ge_balance_negative_injective_datacartesianfirstvalue. (((((scp_first_injective_datacartesian) = 2 * (ge_balance_positive_injective_datacartesianfirstvalue) /\ (ge_balance_negative_injective_datacartesianfirstvalue) = 0) \/ exists ge_signed_half_injective_datacartesianfirstvaluedecode. (((scp_first_injective_datacartesian) = 2 * ge_signed_half_injective_datacartesianfirstvaluedecode + 1 /\ (ge_balance_positive_injective_datacartesianfirstvalue) = 0) /\ (ge_balance_negative_injective_datacartesianfirstvalue) = S ge_signed_half_injective_datacartesianfirstvaluedecode))) /\ ((dst_positive_injective_datacartesianfirst) + ge_balance_negative_injective_datacartesianfirstvalue = (dst_negative_injective_datacartesianfirst) + ge_balance_positive_injective_datacartesianfirstvalue))))))))) -> (exists dst_positive_code_injective_datacartesiansecond dst_positive_scale_injective_datacartesiansecond dst_negative_code_injective_datacartesiansecond dst_negative_scale_injective_datacartesiansecond dst_positive_injective_datacartesiansecond dst_negative_injective_datacartesiansecond. (((B) = (((((dst_positive_code_injective_datacartesiansecond) + (dst_positive_scale_injective_datacartesiansecond)) * S ((dst_positive_code_injective_datacartesiansecond) + (dst_positive_scale_injective_datacartesiansecond)) + ((dst_positive_scale_injective_datacartesiansecond) + (dst_positive_scale_injective_datacartesiansecond))) + (((dst_negative_code_injective_datacartesiansecond) + (dst_negative_scale_injective_datacartesiansecond)) * S ((dst_negative_code_injective_datacartesiansecond) + (dst_negative_scale_injective_datacartesiansecond)) + ((dst_negative_scale_injective_datacartesiansecond) + (dst_negative_scale_injective_datacartesiansecond)))) * S ((((dst_positive_code_injective_datacartesiansecond) + (dst_positive_scale_injective_datacartesiansecond)) * S ((dst_positive_code_injective_datacartesiansecond) + (dst_positive_scale_injective_datacartesiansecond)) + ((dst_positive_scale_injective_datacartesiansecond) + (dst_positive_scale_injective_datacartesiansecond))) + (((dst_negative_code_injective_datacartesiansecond) + (dst_negative_scale_injective_datacartesiansecond)) * S ((dst_negative_code_injective_datacartesiansecond) + (dst_negative_scale_injective_datacartesiansecond)) + ((dst_negative_scale_injective_datacartesiansecond) + (dst_negative_scale_injective_datacartesiansecond)))) + ((((dst_negative_code_injective_datacartesiansecond) + (dst_negative_scale_injective_datacartesiansecond)) * S ((dst_negative_code_injective_datacartesiansecond) + (dst_negative_scale_injective_datacartesiansecond)) + ((dst_negative_scale_injective_datacartesiansecond) + (dst_negative_scale_injective_datacartesiansecond))) + (((dst_negative_code_injective_datacartesiansecond) + (dst_negative_scale_injective_datacartesiansecond)) * S ((dst_negative_code_injective_datacartesiansecond) + (dst_negative_scale_injective_datacartesiansecond)) + ((dst_negative_scale_injective_datacartesiansecond) + (dst_negative_scale_injective_datacartesiansecond)))))) /\ (((((exists ff_h_pvs_injective_datacartesiansecondpositive. ff_h_pvs_injective_datacartesiansecondpositive + S (dst_positive_injective_datacartesiansecond) = S ((S (scp_column_injective_datacartesian)) * dst_positive_scale_injective_datacartesiansecond)) /\ exists ff_q_pvs_injective_datacartesiansecondpositive. dst_positive_code_injective_datacartesiansecond = ff_q_pvs_injective_datacartesiansecondpositive * S ((S (scp_column_injective_datacartesian)) * dst_positive_scale_injective_datacartesiansecond) + (dst_positive_injective_datacartesiansecond))) /\ (((((exists ff_h_pvs_injective_datacartesiansecondnegative. ff_h_pvs_injective_datacartesiansecondnegative + S (dst_negative_injective_datacartesiansecond) = S ((S (scp_column_injective_datacartesian)) * dst_negative_scale_injective_datacartesiansecond)) /\ exists ff_q_pvs_injective_datacartesiansecondnegative. dst_negative_code_injective_datacartesiansecond = ff_q_pvs_injective_datacartesiansecondnegative * S ((S (scp_column_injective_datacartesian)) * dst_negative_scale_injective_datacartesiansecond) + (dst_negative_injective_datacartesiansecond))) /\ (exists ge_balance_positive_injective_datacartesiansecondvalue ge_balance_negative_injective_datacartesiansecondvalue. (((((scp_second_injective_datacartesian) = 2 * (ge_balance_positive_injective_datacartesiansecondvalue) /\ (ge_balance_negative_injective_datacartesiansecondvalue) = 0) \/ exists ge_signed_half_injective_datacartesiansecondvaluedecode. (((scp_second_injective_datacartesian) = 2 * ge_signed_half_injective_datacartesiansecondvaluedecode + 1 /\ (ge_balance_positive_injective_datacartesiansecondvalue) = 0) /\ (ge_balance_negative_injective_datacartesiansecondvalue) = S ge_signed_half_injective_datacartesiansecondvaluedecode))) /\ ((dst_positive_injective_datacartesiansecond) + ge_balance_negative_injective_datacartesiansecondvalue = (dst_negative_injective_datacartesiansecond) + ge_balance_positive_injective_datacartesiansecondvalue))))))))) -> (exists dst_positive_code_injective_datacartesianentry dst_positive_scale_injective_datacartesianentry dst_negative_code_injective_datacartesianentry dst_negative_scale_injective_datacartesianentry dst_positive_injective_datacartesianentry dst_negative_injective_datacartesianentry. (((T) = (((((dst_positive_code_injective_datacartesianentry) + (dst_positive_scale_injective_datacartesianentry)) * S ((dst_positive_code_injective_datacartesianentry) + (dst_positive_scale_injective_datacartesianentry)) + ((dst_positive_scale_injective_datacartesianentry) + (dst_positive_scale_injective_datacartesianentry))) + (((dst_negative_code_injective_datacartesianentry) + (dst_negative_scale_injective_datacartesianentry)) * S ((dst_negative_code_injective_datacartesianentry) + (dst_negative_scale_injective_datacartesianentry)) + ((dst_negative_scale_injective_datacartesianentry) + (dst_negative_scale_injective_datacartesianentry)))) * S ((((dst_positive_code_injective_datacartesianentry) + (dst_positive_scale_injective_datacartesianentry)) * S ((dst_positive_code_injective_datacartesianentry) + (dst_positive_scale_injective_datacartesianentry)) + ((dst_positive_scale_injective_datacartesianentry) + (dst_positive_scale_injective_datacartesianentry))) + (((dst_negative_code_injective_datacartesianentry) + (dst_negative_scale_injective_datacartesianentry)) * S ((dst_negative_code_injective_datacartesianentry) + (dst_negative_scale_injective_datacartesianentry)) + ((dst_negative_scale_injective_datacartesianentry) + (dst_negative_scale_injective_datacartesianentry)))) + ((((dst_negative_code_injective_datacartesianentry) + (dst_negative_scale_injective_datacartesianentry)) * S ((dst_negative_code_injective_datacartesianentry) + (dst_negative_scale_injective_datacartesianentry)) + ((dst_negative_scale_injective_datacartesianentry) + (dst_negative_scale_injective_datacartesianentry))) + (((dst_negative_code_injective_datacartesianentry) + (dst_negative_scale_injective_datacartesianentry)) * S ((dst_negative_code_injective_datacartesianentry) + (dst_negative_scale_injective_datacartesianentry)) + ((dst_negative_scale_injective_datacartesianentry) + (dst_negative_scale_injective_datacartesianentry)))))) /\ (((((exists ff_h_pvs_injective_datacartesianentrypositive. ff_h_pvs_injective_datacartesianentrypositive + S (dst_positive_injective_datacartesianentry) = S ((S (((S (n))*(scp_row_injective_datacartesian)+(scp_column_injective_datacartesian)))) * dst_positive_scale_injective_datacartesianentry)) /\ exists ff_q_pvs_injective_datacartesianentrypositive. dst_positive_code_injective_datacartesianentry = ff_q_pvs_injective_datacartesianentrypositive * S ((S (((S (n))*(scp_row_injective_datacartesian)+(scp_column_injective_datacartesian)))) * dst_positive_scale_injective_datacartesianentry) + (dst_positive_injective_datacartesianentry))) /\ (((((exists ff_h_pvs_injective_datacartesianentrynegative. ff_h_pvs_injective_datacartesianentrynegative + S (dst_negative_injective_datacartesianentry) = S ((S (((S (n))*(scp_row_injective_datacartesian)+(scp_column_injective_datacartesian)))) * dst_negative_scale_injective_datacartesianentry)) /\ exists ff_q_pvs_injective_datacartesianentrynegative. dst_negative_code_injective_datacartesianentry = ff_q_pvs_injective_datacartesianentrynegative * S ((S (((S (n))*(scp_row_injective_datacartesian)+(scp_column_injective_datacartesian)))) * dst_negative_scale_injective_datacartesianentry) + (dst_negative_injective_datacartesianentry))) /\ (exists ge_balance_positive_injective_datacartesianentryvalue ge_balance_negative_injective_datacartesianentryvalue. (((((scp_value_injective_datacartesian) = 2 * (ge_balance_positive_injective_datacartesianentryvalue) /\ (ge_balance_negative_injective_datacartesianentryvalue) = 0) \/ exists ge_signed_half_injective_datacartesianentryvaluedecode. (((scp_value_injective_datacartesian) = 2 * ge_signed_half_injective_datacartesianentryvaluedecode + 1 /\ (ge_balance_positive_injective_datacartesianentryvalue) = 0) /\ (ge_balance_negative_injective_datacartesianentryvalue) = S ge_signed_half_injective_datacartesianentryvaluedecode))) /\ ((dst_positive_injective_datacartesianentry) + ge_balance_negative_injective_datacartesianentryvalue = (dst_negative_injective_datacartesianentry) + ge_balance_positive_injective_datacartesianentryvalue))))))))) -> (exists sto_ap_injective_datacartesianmultiply sto_an_injective_datacartesianmultiply sto_bp_injective_datacartesianmultiply sto_bn_injective_datacartesianmultiply sto_cp_injective_datacartesianmultiply sto_cn_injective_datacartesianmultiply. (((((scp_first_injective_datacartesian) = 2 * (sto_ap_injective_datacartesianmultiply) /\ (sto_an_injective_datacartesianmultiply) = 0) \/ exists ge_signed_half_injective_datacartesianmultiplyleft. (((scp_first_injective_datacartesian) = 2 * ge_signed_half_injective_datacartesianmultiplyleft + 1 /\ (sto_ap_injective_datacartesianmultiply) = 0) /\ (sto_an_injective_datacartesianmultiply) = S ge_signed_half_injective_datacartesianmultiplyleft))) /\ ((((((scp_second_injective_datacartesian) = 2 * (sto_bp_injective_datacartesianmultiply) /\ (sto_bn_injective_datacartesianmultiply) = 0) \/ exists ge_signed_half_injective_datacartesianmultiplyright. (((scp_second_injective_datacartesian) = 2 * ge_signed_half_injective_datacartesianmultiplyright + 1 /\ (sto_bp_injective_datacartesianmultiply) = 0) /\ (sto_bn_injective_datacartesianmultiply) = S ge_signed_half_injective_datacartesianmultiplyright))) /\ ((((((scp_value_injective_datacartesian) = 2 * (sto_cp_injective_datacartesianmultiply) /\ (sto_cn_injective_datacartesianmultiply) = 0) \/ exists ge_signed_half_injective_datacartesianmultiplyoutput. (((scp_value_injective_datacartesian) = 2 * ge_signed_half_injective_datacartesianmultiplyoutput + 1 /\ (sto_cp_injective_datacartesianmultiply) = 0) /\ (sto_cn_injective_datacartesianmultiply) = S ge_signed_half_injective_datacartesianmultiplyoutput))) /\ ((sto_ap_injective_datacartesianmultiply * sto_bp_injective_datacartesianmultiply + sto_an_injective_datacartesianmultiply * sto_bn_injective_datacartesianmultiply) + sto_cn_injective_datacartesianmultiply = (sto_ap_injective_datacartesianmultiply * sto_bn_injective_datacartesianmultiply + sto_an_injective_datacartesianmultiply * sto_bp_injective_datacartesianmultiply) + sto_cp_injective_datacartesianmultiply)))))))))))))) /\ (((((exists dst_positive_code_injective_datatargettable dst_positive_scale_injective_datatargettable dst_negative_code_injective_datatargettable dst_negative_scale_injective_datatargettable. (((Q) = (((((dst_positive_code_injective_datatargettable) + (dst_positive_scale_injective_datatargettable)) * S ((dst_positive_code_injective_datatargettable) + (dst_positive_scale_injective_datatargettable)) + ((dst_positive_scale_injective_datatargettable) + (dst_positive_scale_injective_datatargettable))) + (((dst_negative_code_injective_datatargettable) + (dst_negative_scale_injective_datatargettable)) * S ((dst_negative_code_injective_datatargettable) + (dst_negative_scale_injective_datatargettable)) + ((dst_negative_scale_injective_datatargettable) + (dst_negative_scale_injective_datatargettable)))) * S ((((dst_positive_code_injective_datatargettable) + (dst_positive_scale_injective_datatargettable)) * S ((dst_positive_code_injective_datatargettable) + (dst_positive_scale_injective_datatargettable)) + ((dst_positive_scale_injective_datatargettable) + (dst_positive_scale_injective_datatargettable))) + (((dst_negative_code_injective_datatargettable) + (dst_negative_scale_injective_datatargettable)) * S ((dst_negative_code_injective_datatargettable) + (dst_negative_scale_injective_datatargettable)) + ((dst_negative_scale_injective_datatargettable) + (dst_negative_scale_injective_datatargettable)))) + ((((dst_negative_code_injective_datatargettable) + (dst_negative_scale_injective_datatargettable)) * S ((dst_negative_code_injective_datatargettable) + (dst_negative_scale_injective_datatargettable)) + ((dst_negative_scale_injective_datatargettable) + (dst_negative_scale_injective_datatargettable))) + (((dst_negative_code_injective_datatargettable) + (dst_negative_scale_injective_datatargettable)) * S ((dst_negative_code_injective_datatargettable) + (dst_negative_scale_injective_datatargettable)) + ((dst_negative_scale_injective_datatargettable) + (dst_negative_scale_injective_datatargettable)))))) /\ (forall dst_index_injective_datatargettable. (exists pvs_le_gap_injective_datatargettabledomain. pvs_le_gap_injective_datatargettabledomain + (dst_index_injective_datatargettable) = ((m)*(n))) -> exists dst_positive_injective_datatargettable dst_negative_injective_datatargettable dst_value_injective_datatargettable. ((((exists ff_h_pvs_injective_datatargettableentrypositive. ff_h_pvs_injective_datatargettableentrypositive + S (dst_positive_injective_datatargettable) = S ((S (dst_index_injective_datatargettable)) * dst_positive_scale_injective_datatargettable)) /\ exists ff_q_pvs_injective_datatargettableentrypositive. dst_positive_code_injective_datatargettable = ff_q_pvs_injective_datatargettableentrypositive * S ((S (dst_index_injective_datatargettable)) * dst_positive_scale_injective_datatargettable) + (dst_positive_injective_datatargettable))) /\ (((((exists ff_h_pvs_injective_datatargettableentrynegative. ff_h_pvs_injective_datatargettableentrynegative + S (dst_negative_injective_datatargettable) = S ((S (dst_index_injective_datatargettable)) * dst_negative_scale_injective_datatargettable)) /\ exists ff_q_pvs_injective_datatargettableentrynegative. dst_negative_code_injective_datatargettable = ff_q_pvs_injective_datatargettableentrynegative * S ((S (dst_index_injective_datatargettable)) * dst_negative_scale_injective_datatargettable) + (dst_negative_injective_datatargettable))) /\ (exists ge_balance_positive_injective_datatargettableentryvalue ge_balance_negative_injective_datatargettableentryvalue. (((((dst_value_injective_datatargettable) = 2 * (ge_balance_positive_injective_datatargettableentryvalue) /\ (ge_balance_negative_injective_datatargettableentryvalue) = 0) \/ exists ge_signed_half_injective_datatargettableentryvaluedecode. (((dst_value_injective_datatargettable) = 2 * ge_signed_half_injective_datatargettableentryvaluedecode + 1 /\ (ge_balance_positive_injective_datatargettableentryvalue) = 0) /\ (ge_balance_negative_injective_datatargettableentryvalue) = S ge_signed_half_injective_datatargettableentryvaluedecode))) /\ ((dst_positive_injective_datatargettable) + ge_balance_negative_injective_datatargettableentryvalue = (dst_negative_injective_datatargettable) + ge_balance_positive_injective_datatargettableentryvalue))))))))) /\ (forall dc_index_injective_datatarget dc_value_injective_datatarget. (exists pvs_le_gap_injective_datatargetdomain. pvs_le_gap_injective_datatargetdomain + (dc_index_injective_datatarget) = ((m)*(n))) -> (exists dst_positive_code_injective_datatargetlookup dst_positive_scale_injective_datatargetlookup dst_negative_code_injective_datatargetlookup dst_negative_scale_injective_datatargetlookup dst_positive_injective_datatargetlookup dst_negative_injective_datatargetlookup. (((Q) = (((((dst_positive_code_injective_datatargetlookup) + (dst_positive_scale_injective_datatargetlookup)) * S ((dst_positive_code_injective_datatargetlookup) + (dst_positive_scale_injective_datatargetlookup)) + ((dst_positive_scale_injective_datatargetlookup) + (dst_positive_scale_injective_datatargetlookup))) + (((dst_negative_code_injective_datatargetlookup) + (dst_negative_scale_injective_datatargetlookup)) * S ((dst_negative_code_injective_datatargetlookup) + (dst_negative_scale_injective_datatargetlookup)) + ((dst_negative_scale_injective_datatargetlookup) + (dst_negative_scale_injective_datatargetlookup)))) * S ((((dst_positive_code_injective_datatargetlookup) + (dst_positive_scale_injective_datatargetlookup)) * S ((dst_positive_code_injective_datatargetlookup) + (dst_positive_scale_injective_datatargetlookup)) + ((dst_positive_scale_injective_datatargetlookup) + (dst_positive_scale_injective_datatargetlookup))) + (((dst_negative_code_injective_datatargetlookup) + (dst_negative_scale_injective_datatargetlookup)) * S ((dst_negative_code_injective_datatargetlookup) + (dst_negative_scale_injective_datatargetlookup)) + ((dst_negative_scale_injective_datatargetlookup) + (dst_negative_scale_injective_datatargetlookup)))) + ((((dst_negative_code_injective_datatargetlookup) + (dst_negative_scale_injective_datatargetlookup)) * S ((dst_negative_code_injective_datatargetlookup) + (dst_negative_scale_injective_datatargetlookup)) + ((dst_negative_scale_injective_datatargetlookup) + (dst_negative_scale_injective_datatargetlookup))) + (((dst_negative_code_injective_datatargetlookup) + (dst_negative_scale_injective_datatargetlookup)) * S ((dst_negative_code_injective_datatargetlookup) + (dst_negative_scale_injective_datatargetlookup)) + ((dst_negative_scale_injective_datatargetlookup) + (dst_negative_scale_injective_datatargetlookup)))))) /\ (((((exists ff_h_pvs_injective_datatargetlookuppositive. ff_h_pvs_injective_datatargetlookuppositive + S (dst_positive_injective_datatargetlookup) = S ((S (dc_index_injective_datatarget)) * dst_positive_scale_injective_datatargetlookup)) /\ exists ff_q_pvs_injective_datatargetlookuppositive. dst_positive_code_injective_datatargetlookup = ff_q_pvs_injective_datatargetlookuppositive * S ((S (dc_index_injective_datatarget)) * dst_positive_scale_injective_datatargetlookup) + (dst_positive_injective_datatargetlookup))) /\ (((((exists ff_h_pvs_injective_datatargetlookupnegative. ff_h_pvs_injective_datatargetlookupnegative + S (dst_negative_injective_datatargetlookup) = S ((S (dc_index_injective_datatarget)) * dst_negative_scale_injective_datatargetlookup)) /\ exists ff_q_pvs_injective_datatargetlookupnegative. dst_negative_code_injective_datatargetlookup = ff_q_pvs_injective_datatargetlookupnegative * S ((S (dc_index_injective_datatarget)) * dst_negative_scale_injective_datatargetlookup) + (dst_negative_injective_datatargetlookup))) /\ (exists ge_balance_positive_injective_datatargetlookupvalue ge_balance_negative_injective_datatargetlookupvalue. (((((dc_value_injective_datatarget) = 2 * (ge_balance_positive_injective_datatargetlookupvalue) /\ (ge_balance_negative_injective_datatargetlookupvalue) = 0) \/ exists ge_signed_half_injective_datatargetlookupvaluedecode. (((dc_value_injective_datatarget) = 2 * ge_signed_half_injective_datatargetlookupvaluedecode + 1 /\ (ge_balance_positive_injective_datatargetlookupvalue) = 0) /\ (ge_balance_negative_injective_datatargetlookupvalue) = S ge_signed_half_injective_datatargetlookupvaluedecode))) /\ ((dst_positive_injective_datatargetlookup) + ge_balance_negative_injective_datatargetlookupvalue = (dst_negative_injective_datatargetlookup) + ge_balance_positive_injective_datatargetlookupvalue))))))))) -> ((((~((dc_index_injective_datatarget)=0)) /\ (exists dc_quotient_injective_datatargetentry dc_left_injective_datatargetentry dc_right_injective_datatargetentry. ((((m)*(n))=(dc_index_injective_datatarget)*dc_quotient_injective_datatargetentry) /\ (((exists dst_positive_code_injective_datatargetentryleft dst_positive_scale_injective_datatargetentryleft dst_negative_code_injective_datatargetentryleft dst_negative_scale_injective_datatargetentryleft dst_positive_injective_datatargetentryleft dst_negative_injective_datatargetentryleft. (((F) = (((((dst_positive_code_injective_datatargetentryleft) + (dst_positive_scale_injective_datatargetentryleft)) * S ((dst_positive_code_injective_datatargetentryleft) + (dst_positive_scale_injective_datatargetentryleft)) + ((dst_positive_scale_injective_datatargetentryleft) + (dst_positive_scale_injective_datatargetentryleft))) + (((dst_negative_code_injective_datatargetentryleft) + (dst_negative_scale_injective_datatargetentryleft)) * S ((dst_negative_code_injective_datatargetentryleft) + (dst_negative_scale_injective_datatargetentryleft)) + ((dst_negative_scale_injective_datatargetentryleft) + (dst_negative_scale_injective_datatargetentryleft)))) * S ((((dst_positive_code_injective_datatargetentryleft) + (dst_positive_scale_injective_datatargetentryleft)) * S ((dst_positive_code_injective_datatargetentryleft) + (dst_positive_scale_injective_datatargetentryleft)) + ((dst_positive_scale_injective_datatargetentryleft) + (dst_positive_scale_injective_datatargetentryleft))) + (((dst_negative_code_injective_datatargetentryleft) + (dst_negative_scale_injective_datatargetentryleft)) * S ((dst_negative_code_injective_datatargetentryleft) + (dst_negative_scale_injective_datatargetentryleft)) + ((dst_negative_scale_injective_datatargetentryleft) + (dst_negative_scale_injective_datatargetentryleft)))) + ((((dst_negative_code_injective_datatargetentryleft) + (dst_negative_scale_injective_datatargetentryleft)) * S ((dst_negative_code_injective_datatargetentryleft) + (dst_negative_scale_injective_datatargetentryleft)) + ((dst_negative_scale_injective_datatargetentryleft) + (dst_negative_scale_injective_datatargetentryleft))) + (((dst_negative_code_injective_datatargetentryleft) + (dst_negative_scale_injective_datatargetentryleft)) * S ((dst_negative_code_injective_datatargetentryleft) + (dst_negative_scale_injective_datatargetentryleft)) + ((dst_negative_scale_injective_datatargetentryleft) + (dst_negative_scale_injective_datatargetentryleft)))))) /\ (((((exists ff_h_pvs_injective_datatargetentryleftpositive. ff_h_pvs_injective_datatargetentryleftpositive + S (dst_positive_injective_datatargetentryleft) = S ((S (dc_index_injective_datatarget)) * dst_positive_scale_injective_datatargetentryleft)) /\ exists ff_q_pvs_injective_datatargetentryleftpositive. dst_positive_code_injective_datatargetentryleft = ff_q_pvs_injective_datatargetentryleftpositive * S ((S (dc_index_injective_datatarget)) * dst_positive_scale_injective_datatargetentryleft) + (dst_positive_injective_datatargetentryleft))) /\ (((((exists ff_h_pvs_injective_datatargetentryleftnegative. ff_h_pvs_injective_datatargetentryleftnegative + S (dst_negative_injective_datatargetentryleft) = S ((S (dc_index_injective_datatarget)) * dst_negative_scale_injective_datatargetentryleft)) /\ exists ff_q_pvs_injective_datatargetentryleftnegative. dst_negative_code_injective_datatargetentryleft = ff_q_pvs_injective_datatargetentryleftnegative * S ((S (dc_index_injective_datatarget)) * dst_negative_scale_injective_datatargetentryleft) + (dst_negative_injective_datatargetentryleft))) /\ (exists ge_balance_positive_injective_datatargetentryleftvalue ge_balance_negative_injective_datatargetentryleftvalue. (((((dc_left_injective_datatargetentry) = 2 * (ge_balance_positive_injective_datatargetentryleftvalue) /\ (ge_balance_negative_injective_datatargetentryleftvalue) = 0) \/ exists ge_signed_half_injective_datatargetentryleftvaluedecode. (((dc_left_injective_datatargetentry) = 2 * ge_signed_half_injective_datatargetentryleftvaluedecode + 1 /\ (ge_balance_positive_injective_datatargetentryleftvalue) = 0) /\ (ge_balance_negative_injective_datatargetentryleftvalue) = S ge_signed_half_injective_datatargetentryleftvaluedecode))) /\ ((dst_positive_injective_datatargetentryleft) + ge_balance_negative_injective_datatargetentryleftvalue = (dst_negative_injective_datatargetentryleft) + ge_balance_positive_injective_datatargetentryleftvalue))))))))) /\ (((exists dst_positive_code_injective_datatargetentryright dst_positive_scale_injective_datatargetentryright dst_negative_code_injective_datatargetentryright dst_negative_scale_injective_datatargetentryright dst_positive_injective_datatargetentryright dst_negative_injective_datatargetentryright. (((G) = (((((dst_positive_code_injective_datatargetentryright) + (dst_positive_scale_injective_datatargetentryright)) * S ((dst_positive_code_injective_datatargetentryright) + (dst_positive_scale_injective_datatargetentryright)) + ((dst_positive_scale_injective_datatargetentryright) + (dst_positive_scale_injective_datatargetentryright))) + (((dst_negative_code_injective_datatargetentryright) + (dst_negative_scale_injective_datatargetentryright)) * S ((dst_negative_code_injective_datatargetentryright) + (dst_negative_scale_injective_datatargetentryright)) + ((dst_negative_scale_injective_datatargetentryright) + (dst_negative_scale_injective_datatargetentryright)))) * S ((((dst_positive_code_injective_datatargetentryright) + (dst_positive_scale_injective_datatargetentryright)) * S ((dst_positive_code_injective_datatargetentryright) + (dst_positive_scale_injective_datatargetentryright)) + ((dst_positive_scale_injective_datatargetentryright) + (dst_positive_scale_injective_datatargetentryright))) + (((dst_negative_code_injective_datatargetentryright) + (dst_negative_scale_injective_datatargetentryright)) * S ((dst_negative_code_injective_datatargetentryright) + (dst_negative_scale_injective_datatargetentryright)) + ((dst_negative_scale_injective_datatargetentryright) + (dst_negative_scale_injective_datatargetentryright)))) + ((((dst_negative_code_injective_datatargetentryright) + (dst_negative_scale_injective_datatargetentryright)) * S ((dst_negative_code_injective_datatargetentryright) + (dst_negative_scale_injective_datatargetentryright)) + ((dst_negative_scale_injective_datatargetentryright) + (dst_negative_scale_injective_datatargetentryright))) + (((dst_negative_code_injective_datatargetentryright) + (dst_negative_scale_injective_datatargetentryright)) * S ((dst_negative_code_injective_datatargetentryright) + (dst_negative_scale_injective_datatargetentryright)) + ((dst_negative_scale_injective_datatargetentryright) + (dst_negative_scale_injective_datatargetentryright)))))) /\ (((((exists ff_h_pvs_injective_datatargetentryrightpositive. ff_h_pvs_injective_datatargetentryrightpositive + S (dst_positive_injective_datatargetentryright) = S ((S (dc_quotient_injective_datatargetentry)) * dst_positive_scale_injective_datatargetentryright)) /\ exists ff_q_pvs_injective_datatargetentryrightpositive. dst_positive_code_injective_datatargetentryright = ff_q_pvs_injective_datatargetentryrightpositive * S ((S (dc_quotient_injective_datatargetentry)) * dst_positive_scale_injective_datatargetentryright) + (dst_positive_injective_datatargetentryright))) /\ (((((exists ff_h_pvs_injective_datatargetentryrightnegative. ff_h_pvs_injective_datatargetentryrightnegative + S (dst_negative_injective_datatargetentryright) = S ((S (dc_quotient_injective_datatargetentry)) * dst_negative_scale_injective_datatargetentryright)) /\ exists ff_q_pvs_injective_datatargetentryrightnegative. dst_negative_code_injective_datatargetentryright = ff_q_pvs_injective_datatargetentryrightnegative * S ((S (dc_quotient_injective_datatargetentry)) * dst_negative_scale_injective_datatargetentryright) + (dst_negative_injective_datatargetentryright))) /\ (exists ge_balance_positive_injective_datatargetentryrightvalue ge_balance_negative_injective_datatargetentryrightvalue. (((((dc_right_injective_datatargetentry) = 2 * (ge_balance_positive_injective_datatargetentryrightvalue) /\ (ge_balance_negative_injective_datatargetentryrightvalue) = 0) \/ exists ge_signed_half_injective_datatargetentryrightvaluedecode. (((dc_right_injective_datatargetentry) = 2 * ge_signed_half_injective_datatargetentryrightvaluedecode + 1 /\ (ge_balance_positive_injective_datatargetentryrightvalue) = 0) /\ (ge_balance_negative_injective_datatargetentryrightvalue) = S ge_signed_half_injective_datatargetentryrightvaluedecode))) /\ ((dst_positive_injective_datatargetentryright) + ge_balance_negative_injective_datatargetentryrightvalue = (dst_negative_injective_datatargetentryright) + ge_balance_positive_injective_datatargetentryrightvalue))))))))) /\ (exists sto_ap_injective_datatargetentryproduct sto_an_injective_datatargetentryproduct sto_bp_injective_datatargetentryproduct sto_bn_injective_datatargetentryproduct sto_cp_injective_datatargetentryproduct sto_cn_injective_datatargetentryproduct. (((((dc_left_injective_datatargetentry) = 2 * (sto_ap_injective_datatargetentryproduct) /\ (sto_an_injective_datatargetentryproduct) = 0) \/ exists ge_signed_half_injective_datatargetentryproductleft. (((dc_left_injective_datatargetentry) = 2 * ge_signed_half_injective_datatargetentryproductleft + 1 /\ (sto_ap_injective_datatargetentryproduct) = 0) /\ (sto_an_injective_datatargetentryproduct) = S ge_signed_half_injective_datatargetentryproductleft))) /\ ((((((dc_right_injective_datatargetentry) = 2 * (sto_bp_injective_datatargetentryproduct) /\ (sto_bn_injective_datatargetentryproduct) = 0) \/ exists ge_signed_half_injective_datatargetentryproductright. (((dc_right_injective_datatargetentry) = 2 * ge_signed_half_injective_datatargetentryproductright + 1 /\ (sto_bp_injective_datatargetentryproduct) = 0) /\ (sto_bn_injective_datatargetentryproduct) = S ge_signed_half_injective_datatargetentryproductright))) /\ ((((((dc_value_injective_datatarget) = 2 * (sto_cp_injective_datatargetentryproduct) /\ (sto_cn_injective_datatargetentryproduct) = 0) \/ exists ge_signed_half_injective_datatargetentryproductoutput. (((dc_value_injective_datatarget) = 2 * ge_signed_half_injective_datatargetentryproductoutput + 1 /\ (sto_cp_injective_datatargetentryproduct) = 0) /\ (sto_cn_injective_datatargetentryproduct) = S ge_signed_half_injective_datatargetentryproductoutput))) /\ ((sto_ap_injective_datatargetentryproduct * sto_bp_injective_datatargetentryproduct + sto_an_injective_datatargetentryproduct * sto_bn_injective_datatargetentryproduct) + sto_cn_injective_datatargetentryproduct = (sto_ap_injective_datatargetentryproduct * sto_bn_injective_datatargetentryproduct + sto_an_injective_datatargetentryproduct * sto_bp_injective_datatargetentryproduct) + sto_cp_injective_datatargetentryproduct))))))))))))))) \/ ((((dc_index_injective_datatarget)=0 \/ ~(exists pvs_factor_injective_datatargetentrynondivisor. ((m)*(n)) = (dc_index_injective_datatarget) * pvs_factor_injective_datatargetentrynondivisor)) /\ ((dc_value_injective_datatarget)=0))))))) /\ (((~((S (n))=0)) /\ (forall dpi_index_injective_datamap dpi_row_injective_datamap dpi_column_injective_datamap. (exists pvs_gap_injective_datamapwindow. pvs_gap_injective_datamapwindow + S (dpi_index_injective_datamap) = ((S (m))*(S (n)))) -> (exists pvs_gap_injective_datamapremainder. pvs_gap_injective_datamapremainder + S (dpi_column_injective_datamap) = (S (n))) -> (dpi_index_injective_datamap)=(S (n))*(dpi_row_injective_datamap)+(dpi_column_injective_datamap) -> (((exists ff_h_pvs_injective_datamapvalue. ff_h_pvs_injective_datamapvalue + S ((dpi_row_injective_datamap)*(dpi_column_injective_datamap)) = S ((S (dpi_index_injective_datamap)) * s)) /\ exists ff_q_pvs_injective_datamapvalue. r = ff_q_pvs_injective_datamapvalue * S ((S (dpi_index_injective_datamap)) * s) + ((dpi_row_injective_datamap)*(dpi_column_injective_datamap))))))))))))))))))))))))))) -> (forall ssr_first_injective_result ssr_second_injective_result ssr_image_injective_result ssr_a_injective_result ssr_b_injective_result. (exists pvs_gap_injective_resultfirst_bound. pvs_gap_injective_resultfirst_bound + S (ssr_first_injective_result) = ((S (m))*(S (n)))) -> (exists pvs_gap_injective_resultsecond_bound. pvs_gap_injective_resultsecond_bound + S (ssr_second_injective_result) = ((S (m))*(S (n)))) -> (exists dst_positive_code_injective_resultfirst_value dst_positive_scale_injective_resultfirst_value dst_negative_code_injective_resultfirst_value dst_negative_scale_injective_resultfirst_value dst_positive_injective_resultfirst_value dst_negative_injective_resultfirst_value. (((T) = (((((dst_positive_code_injective_resultfirst_value) + (dst_positive_scale_injective_resultfirst_value)) * S ((dst_positive_code_injective_resultfirst_value) + (dst_positive_scale_injective_resultfirst_value)) + ((dst_positive_scale_injective_resultfirst_value) + (dst_positive_scale_injective_resultfirst_value))) + (((dst_negative_code_injective_resultfirst_value) + (dst_negative_scale_injective_resultfirst_value)) * S ((dst_negative_code_injective_resultfirst_value) + (dst_negative_scale_injective_resultfirst_value)) + ((dst_negative_scale_injective_resultfirst_value) + (dst_negative_scale_injective_resultfirst_value)))) * S ((((dst_positive_code_injective_resultfirst_value) + (dst_positive_scale_injective_resultfirst_value)) * S ((dst_positive_code_injective_resultfirst_value) + (dst_positive_scale_injective_resultfirst_value)) + ((dst_positive_scale_injective_resultfirst_value) + (dst_positive_scale_injective_resultfirst_value))) + (((dst_negative_code_injective_resultfirst_value) + (dst_negative_scale_injective_resultfirst_value)) * S ((dst_negative_code_injective_resultfirst_value) + (dst_negative_scale_injective_resultfirst_value)) + ((dst_negative_scale_injective_resultfirst_value) + (dst_negative_scale_injective_resultfirst_value)))) + ((((dst_negative_code_injective_resultfirst_value) + (dst_negative_scale_injective_resultfirst_value)) * S ((dst_negative_code_injective_resultfirst_value) + (dst_negative_scale_injective_resultfirst_value)) + ((dst_negative_scale_injective_resultfirst_value) + (dst_negative_scale_injective_resultfirst_value))) + (((dst_negative_code_injective_resultfirst_value) + (dst_negative_scale_injective_resultfirst_value)) * S ((dst_negative_code_injective_resultfirst_value) + (dst_negative_scale_injective_resultfirst_value)) + ((dst_negative_scale_injective_resultfirst_value) + (dst_negative_scale_injective_resultfirst_value)))))) /\ (((((exists ff_h_pvs_injective_resultfirst_valuepositive. ff_h_pvs_injective_resultfirst_valuepositive + S (dst_positive_injective_resultfirst_value) = S ((S (ssr_first_injective_result)) * dst_positive_scale_injective_resultfirst_value)) /\ exists ff_q_pvs_injective_resultfirst_valuepositive. dst_positive_code_injective_resultfirst_value = ff_q_pvs_injective_resultfirst_valuepositive * S ((S (ssr_first_injective_result)) * dst_positive_scale_injective_resultfirst_value) + (dst_positive_injective_resultfirst_value))) /\ (((((exists ff_h_pvs_injective_resultfirst_valuenegative. ff_h_pvs_injective_resultfirst_valuenegative + S (dst_negative_injective_resultfirst_value) = S ((S (ssr_first_injective_result)) * dst_negative_scale_injective_resultfirst_value)) /\ exists ff_q_pvs_injective_resultfirst_valuenegative. dst_negative_code_injective_resultfirst_value = ff_q_pvs_injective_resultfirst_valuenegative * S ((S (ssr_first_injective_result)) * dst_negative_scale_injective_resultfirst_value) + (dst_negative_injective_resultfirst_value))) /\ (exists ge_balance_positive_injective_resultfirst_valuevalue ge_balance_negative_injective_resultfirst_valuevalue. (((((ssr_a_injective_result) = 2 * (ge_balance_positive_injective_resultfirst_valuevalue) /\ (ge_balance_negative_injective_resultfirst_valuevalue) = 0) \/ exists ge_signed_half_injective_resultfirst_valuevaluedecode. (((ssr_a_injective_result) = 2 * ge_signed_half_injective_resultfirst_valuevaluedecode + 1 /\ (ge_balance_positive_injective_resultfirst_valuevalue) = 0) /\ (ge_balance_negative_injective_resultfirst_valuevalue) = S ge_signed_half_injective_resultfirst_valuevaluedecode))) /\ ((dst_positive_injective_resultfirst_value) + ge_balance_negative_injective_resultfirst_valuevalue = (dst_negative_injective_resultfirst_value) + ge_balance_positive_injective_resultfirst_valuevalue))))))))) -> ~(ssr_a_injective_result=0) -> (exists dst_positive_code_injective_resultsecond_value dst_positive_scale_injective_resultsecond_value dst_negative_code_injective_resultsecond_value dst_negative_scale_injective_resultsecond_value dst_positive_injective_resultsecond_value dst_negative_injective_resultsecond_value. (((T) = (((((dst_positive_code_injective_resultsecond_value) + (dst_positive_scale_injective_resultsecond_value)) * S ((dst_positive_code_injective_resultsecond_value) + (dst_positive_scale_injective_resultsecond_value)) + ((dst_positive_scale_injective_resultsecond_value) + (dst_positive_scale_injective_resultsecond_value))) + (((dst_negative_code_injective_resultsecond_value) + (dst_negative_scale_injective_resultsecond_value)) * S ((dst_negative_code_injective_resultsecond_value) + (dst_negative_scale_injective_resultsecond_value)) + ((dst_negative_scale_injective_resultsecond_value) + (dst_negative_scale_injective_resultsecond_value)))) * S ((((dst_positive_code_injective_resultsecond_value) + (dst_positive_scale_injective_resultsecond_value)) * S ((dst_positive_code_injective_resultsecond_value) + (dst_positive_scale_injective_resultsecond_value)) + ((dst_positive_scale_injective_resultsecond_value) + (dst_positive_scale_injective_resultsecond_value))) + (((dst_negative_code_injective_resultsecond_value) + (dst_negative_scale_injective_resultsecond_value)) * S ((dst_negative_code_injective_resultsecond_value) + (dst_negative_scale_injective_resultsecond_value)) + ((dst_negative_scale_injective_resultsecond_value) + (dst_negative_scale_injective_resultsecond_value)))) + ((((dst_negative_code_injective_resultsecond_value) + (dst_negative_scale_injective_resultsecond_value)) * S ((dst_negative_code_injective_resultsecond_value) + (dst_negative_scale_injective_resultsecond_value)) + ((dst_negative_scale_injective_resultsecond_value) + (dst_negative_scale_injective_resultsecond_value))) + (((dst_negative_code_injective_resultsecond_value) + (dst_negative_scale_injective_resultsecond_value)) * S ((dst_negative_code_injective_resultsecond_value) + (dst_negative_scale_injective_resultsecond_value)) + ((dst_negative_scale_injective_resultsecond_value) + (dst_negative_scale_injective_resultsecond_value)))))) /\ (((((exists ff_h_pvs_injective_resultsecond_valuepositive. ff_h_pvs_injective_resultsecond_valuepositive + S (dst_positive_injective_resultsecond_value) = S ((S (ssr_second_injective_result)) * dst_positive_scale_injective_resultsecond_value)) /\ exists ff_q_pvs_injective_resultsecond_valuepositive. dst_positive_code_injective_resultsecond_value = ff_q_pvs_injective_resultsecond_valuepositive * S ((S (ssr_second_injective_result)) * dst_positive_scale_injective_resultsecond_value) + (dst_positive_injective_resultsecond_value))) /\ (((((exists ff_h_pvs_injective_resultsecond_valuenegative. ff_h_pvs_injective_resultsecond_valuenegative + S (dst_negative_injective_resultsecond_value) = S ((S (ssr_second_injective_result)) * dst_negative_scale_injective_resultsecond_value)) /\ exists ff_q_pvs_injective_resultsecond_valuenegative. dst_negative_code_injective_resultsecond_value = ff_q_pvs_injective_resultsecond_valuenegative * S ((S (ssr_second_injective_result)) * dst_negative_scale_injective_resultsecond_value) + (dst_negative_injective_resultsecond_value))) /\ (exists ge_balance_positive_injective_resultsecond_valuevalue ge_balance_negative_injective_resultsecond_valuevalue. (((((ssr_b_injective_result) = 2 * (ge_balance_positive_injective_resultsecond_valuevalue) /\ (ge_balance_negative_injective_resultsecond_valuevalue) = 0) \/ exists ge_signed_half_injective_resultsecond_valuevaluedecode. (((ssr_b_injective_result) = 2 * ge_signed_half_injective_resultsecond_valuevaluedecode + 1 /\ (ge_balance_positive_injective_resultsecond_valuevalue) = 0) /\ (ge_balance_negative_injective_resultsecond_valuevalue) = S ge_signed_half_injective_resultsecond_valuevaluedecode))) /\ ((dst_positive_injective_resultsecond_value) + ge_balance_negative_injective_resultsecond_valuevalue = (dst_negative_injective_resultsecond_value) + ge_balance_positive_injective_resultsecond_valuevalue))))))))) -> ~(ssr_b_injective_result=0) -> (((exists ff_h_pvs_injective_resultfirst_map. ff_h_pvs_injective_resultfirst_map + S (ssr_image_injective_result) = S ((S (ssr_first_injective_result)) * s)) /\ exists ff_q_pvs_injective_resultfirst_map. r = ff_q_pvs_injective_resultfirst_map * S ((S (ssr_first_injective_result)) * s) + (ssr_image_injective_result))) -> (((exists ff_h_pvs_injective_resultsecond_map. ff_h_pvs_injective_resultsecond_map + S (ssr_image_injective_result) = S ((S (ssr_second_injective_result)) * s)) /\ exists ff_q_pvs_injective_resultsecond_map. r = ff_q_pvs_injective_resultsecond_map * S ((S (ssr_second_injective_result)) * s) + (ssr_image_injective_result))) -> ssr_first_injective_result=ssr_second_injective_result)