dirichlet_coprime_grid_nonzero_coordinates

Exact expanded first-order arithmetic statement

forall N F G m n A B T Q r s i z. (((((~((N)=0)) /\ (((exists dst_positive_code_active_dataFtable dst_positive_scale_active_dataFtable dst_negative_code_active_dataFtable dst_negative_scale_active_dataFtable. (((F) = (((((dst_positive_code_active_dataFtable) + (dst_positive_scale_active_dataFtable)) * S ((dst_positive_code_active_dataFtable) + (dst_positive_scale_active_dataFtable)) + ((dst_positive_scale_active_dataFtable) + (dst_positive_scale_active_dataFtable))) + (((dst_negative_code_active_dataFtable) + (dst_negative_scale_active_dataFtable)) * S ((dst_negative_code_active_dataFtable) + (dst_negative_scale_active_dataFtable)) + ((dst_negative_scale_active_dataFtable) + (dst_negative_scale_active_dataFtable)))) * S ((((dst_positive_code_active_dataFtable) + (dst_positive_scale_active_dataFtable)) * S ((dst_positive_code_active_dataFtable) + (dst_positive_scale_active_dataFtable)) + ((dst_positive_scale_active_dataFtable) + (dst_positive_scale_active_dataFtable))) + (((dst_negative_code_active_dataFtable) + (dst_negative_scale_active_dataFtable)) * S ((dst_negative_code_active_dataFtable) + (dst_negative_scale_active_dataFtable)) + ((dst_negative_scale_active_dataFtable) + (dst_negative_scale_active_dataFtable)))) + ((((dst_negative_code_active_dataFtable) + (dst_negative_scale_active_dataFtable)) * S ((dst_negative_code_active_dataFtable) + (dst_negative_scale_active_dataFtable)) + ((dst_negative_scale_active_dataFtable) + (dst_negative_scale_active_dataFtable))) + (((dst_negative_code_active_dataFtable) + (dst_negative_scale_active_dataFtable)) * S ((dst_negative_code_active_dataFtable) + (dst_negative_scale_active_dataFtable)) + ((dst_negative_scale_active_dataFtable) + (dst_negative_scale_active_dataFtable)))))) /\ (forall dst_index_active_dataFtable. (exists pvs_le_gap_active_dataFtabledomain. pvs_le_gap_active_dataFtabledomain + (dst_index_active_dataFtable) = (N)) -> exists dst_positive_active_dataFtable dst_negative_active_dataFtable dst_value_active_dataFtable. ((((exists ff_h_pvs_active_dataFtableentrypositive. ff_h_pvs_active_dataFtableentrypositive + S (dst_positive_active_dataFtable) = S ((S (dst_index_active_dataFtable)) * dst_positive_scale_active_dataFtable)) /\ exists ff_q_pvs_active_dataFtableentrypositive. dst_positive_code_active_dataFtable = ff_q_pvs_active_dataFtableentrypositive * S ((S (dst_index_active_dataFtable)) * dst_positive_scale_active_dataFtable) + (dst_positive_active_dataFtable))) /\ (((((exists ff_h_pvs_active_dataFtableentrynegative. ff_h_pvs_active_dataFtableentrynegative + S (dst_negative_active_dataFtable) = S ((S (dst_index_active_dataFtable)) * dst_negative_scale_active_dataFtable)) /\ exists ff_q_pvs_active_dataFtableentrynegative. dst_negative_code_active_dataFtable = ff_q_pvs_active_dataFtableentrynegative * S ((S (dst_index_active_dataFtable)) * dst_negative_scale_active_dataFtable) + (dst_negative_active_dataFtable))) /\ (exists ge_balance_positive_active_dataFtableentryvalue ge_balance_negative_active_dataFtableentryvalue. (((((dst_value_active_dataFtable) = 2 * (ge_balance_positive_active_dataFtableentryvalue) /\ (ge_balance_negative_active_dataFtableentryvalue) = 0) \/ exists ge_signed_half_active_dataFtableentryvaluedecode. (((dst_value_active_dataFtable) = 2 * ge_signed_half_active_dataFtableentryvaluedecode + 1 /\ (ge_balance_positive_active_dataFtableentryvalue) = 0) /\ (ge_balance_negative_active_dataFtableentryvalue) = S ge_signed_half_active_dataFtableentryvaluedecode))) /\ ((dst_positive_active_dataFtable) + ge_balance_negative_active_dataFtableentryvalue = (dst_negative_active_dataFtable) + ge_balance_positive_active_dataFtableentryvalue))))))))) /\ (((exists dst_positive_code_active_dataFone dst_positive_scale_active_dataFone dst_negative_code_active_dataFone dst_negative_scale_active_dataFone dst_positive_active_dataFone dst_negative_active_dataFone. (((F) = (((((dst_positive_code_active_dataFone) + (dst_positive_scale_active_dataFone)) * S ((dst_positive_code_active_dataFone) + (dst_positive_scale_active_dataFone)) + ((dst_positive_scale_active_dataFone) + (dst_positive_scale_active_dataFone))) + (((dst_negative_code_active_dataFone) + (dst_negative_scale_active_dataFone)) * S ((dst_negative_code_active_dataFone) + (dst_negative_scale_active_dataFone)) + ((dst_negative_scale_active_dataFone) + (dst_negative_scale_active_dataFone)))) * S ((((dst_positive_code_active_dataFone) + (dst_positive_scale_active_dataFone)) * S ((dst_positive_code_active_dataFone) + (dst_positive_scale_active_dataFone)) + ((dst_positive_scale_active_dataFone) + (dst_positive_scale_active_dataFone))) + (((dst_negative_code_active_dataFone) + (dst_negative_scale_active_dataFone)) * S ((dst_negative_code_active_dataFone) + (dst_negative_scale_active_dataFone)) + ((dst_negative_scale_active_dataFone) + (dst_negative_scale_active_dataFone)))) + ((((dst_negative_code_active_dataFone) + (dst_negative_scale_active_dataFone)) * S ((dst_negative_code_active_dataFone) + (dst_negative_scale_active_dataFone)) + ((dst_negative_scale_active_dataFone) + (dst_negative_scale_active_dataFone))) + (((dst_negative_code_active_dataFone) + (dst_negative_scale_active_dataFone)) * S ((dst_negative_code_active_dataFone) + (dst_negative_scale_active_dataFone)) + ((dst_negative_scale_active_dataFone) + (dst_negative_scale_active_dataFone)))))) /\ (((((exists ff_h_pvs_active_dataFonepositive. ff_h_pvs_active_dataFonepositive + S (dst_positive_active_dataFone) = S ((S (1)) * dst_positive_scale_active_dataFone)) /\ exists ff_q_pvs_active_dataFonepositive. dst_positive_code_active_dataFone = ff_q_pvs_active_dataFonepositive * S ((S (1)) * dst_positive_scale_active_dataFone) + (dst_positive_active_dataFone))) /\ (((((exists ff_h_pvs_active_dataFonenegative. ff_h_pvs_active_dataFonenegative + S (dst_negative_active_dataFone) = S ((S (1)) * dst_negative_scale_active_dataFone)) /\ exists ff_q_pvs_active_dataFonenegative. dst_negative_code_active_dataFone = ff_q_pvs_active_dataFonenegative * S ((S (1)) * dst_negative_scale_active_dataFone) + (dst_negative_active_dataFone))) /\ (exists ge_balance_positive_active_dataFonevalue ge_balance_negative_active_dataFonevalue. (((((2) = 2 * (ge_balance_positive_active_dataFonevalue) /\ (ge_balance_negative_active_dataFonevalue) = 0) \/ exists ge_signed_half_active_dataFonevaluedecode. (((2) = 2 * ge_signed_half_active_dataFonevaluedecode + 1 /\ (ge_balance_positive_active_dataFonevalue) = 0) /\ (ge_balance_negative_active_dataFonevalue) = S ge_signed_half_active_dataFonevaluedecode))) /\ ((dst_positive_active_dataFone) + ge_balance_negative_active_dataFonevalue = (dst_negative_active_dataFone) + ge_balance_positive_active_dataFonevalue))))))))) /\ (forall mp_a_active_dataF mp_b_active_dataF mp_x_active_dataF mp_y_active_dataF mp_z_active_dataF. ~(mp_a_active_dataF=0) -> ~(mp_b_active_dataF=0) -> (exists pvs_le_gap_active_dataFbound. pvs_le_gap_active_dataFbound + (mp_a_active_dataF*mp_b_active_dataF) = (N)) -> (forall frp_divisor_active_dataFcoprime. (exists frp_left_factor_active_dataFcoprime. mp_a_active_dataF = frp_divisor_active_dataFcoprime * frp_left_factor_active_dataFcoprime) -> (exists frp_right_factor_active_dataFcoprime. mp_b_active_dataF = frp_divisor_active_dataFcoprime * frp_right_factor_active_dataFcoprime) -> frp_divisor_active_dataFcoprime = 1) -> (exists dst_positive_code_active_dataFfirst dst_positive_scale_active_dataFfirst dst_negative_code_active_dataFfirst dst_negative_scale_active_dataFfirst dst_positive_active_dataFfirst dst_negative_active_dataFfirst. (((F) = (((((dst_positive_code_active_dataFfirst) + (dst_positive_scale_active_dataFfirst)) * S ((dst_positive_code_active_dataFfirst) + (dst_positive_scale_active_dataFfirst)) + ((dst_positive_scale_active_dataFfirst) + (dst_positive_scale_active_dataFfirst))) + (((dst_negative_code_active_dataFfirst) + (dst_negative_scale_active_dataFfirst)) * S ((dst_negative_code_active_dataFfirst) + (dst_negative_scale_active_dataFfirst)) + ((dst_negative_scale_active_dataFfirst) + (dst_negative_scale_active_dataFfirst)))) * S ((((dst_positive_code_active_dataFfirst) + (dst_positive_scale_active_dataFfirst)) * S ((dst_positive_code_active_dataFfirst) + (dst_positive_scale_active_dataFfirst)) + ((dst_positive_scale_active_dataFfirst) + (dst_positive_scale_active_dataFfirst))) + (((dst_negative_code_active_dataFfirst) + (dst_negative_scale_active_dataFfirst)) * S ((dst_negative_code_active_dataFfirst) + (dst_negative_scale_active_dataFfirst)) + ((dst_negative_scale_active_dataFfirst) + (dst_negative_scale_active_dataFfirst)))) + ((((dst_negative_code_active_dataFfirst) + (dst_negative_scale_active_dataFfirst)) * S ((dst_negative_code_active_dataFfirst) + (dst_negative_scale_active_dataFfirst)) + ((dst_negative_scale_active_dataFfirst) + (dst_negative_scale_active_dataFfirst))) + (((dst_negative_code_active_dataFfirst) + (dst_negative_scale_active_dataFfirst)) * S ((dst_negative_code_active_dataFfirst) + (dst_negative_scale_active_dataFfirst)) + ((dst_negative_scale_active_dataFfirst) + (dst_negative_scale_active_dataFfirst)))))) /\ (((((exists ff_h_pvs_active_dataFfirstpositive. ff_h_pvs_active_dataFfirstpositive + S (dst_positive_active_dataFfirst) = S ((S (mp_a_active_dataF)) * dst_positive_scale_active_dataFfirst)) /\ exists ff_q_pvs_active_dataFfirstpositive. dst_positive_code_active_dataFfirst = ff_q_pvs_active_dataFfirstpositive * S ((S (mp_a_active_dataF)) * dst_positive_scale_active_dataFfirst) + (dst_positive_active_dataFfirst))) /\ (((((exists ff_h_pvs_active_dataFfirstnegative. ff_h_pvs_active_dataFfirstnegative + S (dst_negative_active_dataFfirst) = S ((S (mp_a_active_dataF)) * dst_negative_scale_active_dataFfirst)) /\ exists ff_q_pvs_active_dataFfirstnegative. dst_negative_code_active_dataFfirst = ff_q_pvs_active_dataFfirstnegative * S ((S (mp_a_active_dataF)) * dst_negative_scale_active_dataFfirst) + (dst_negative_active_dataFfirst))) /\ (exists ge_balance_positive_active_dataFfirstvalue ge_balance_negative_active_dataFfirstvalue. (((((mp_x_active_dataF) = 2 * (ge_balance_positive_active_dataFfirstvalue) /\ (ge_balance_negative_active_dataFfirstvalue) = 0) \/ exists ge_signed_half_active_dataFfirstvaluedecode. (((mp_x_active_dataF) = 2 * ge_signed_half_active_dataFfirstvaluedecode + 1 /\ (ge_balance_positive_active_dataFfirstvalue) = 0) /\ (ge_balance_negative_active_dataFfirstvalue) = S ge_signed_half_active_dataFfirstvaluedecode))) /\ ((dst_positive_active_dataFfirst) + ge_balance_negative_active_dataFfirstvalue = (dst_negative_active_dataFfirst) + ge_balance_positive_active_dataFfirstvalue))))))))) -> (exists dst_positive_code_active_dataFsecond dst_positive_scale_active_dataFsecond dst_negative_code_active_dataFsecond dst_negative_scale_active_dataFsecond dst_positive_active_dataFsecond dst_negative_active_dataFsecond. (((F) = (((((dst_positive_code_active_dataFsecond) + (dst_positive_scale_active_dataFsecond)) * S ((dst_positive_code_active_dataFsecond) + (dst_positive_scale_active_dataFsecond)) + ((dst_positive_scale_active_dataFsecond) + (dst_positive_scale_active_dataFsecond))) + (((dst_negative_code_active_dataFsecond) + (dst_negative_scale_active_dataFsecond)) * S ((dst_negative_code_active_dataFsecond) + (dst_negative_scale_active_dataFsecond)) + ((dst_negative_scale_active_dataFsecond) + (dst_negative_scale_active_dataFsecond)))) * S ((((dst_positive_code_active_dataFsecond) + (dst_positive_scale_active_dataFsecond)) * S ((dst_positive_code_active_dataFsecond) + (dst_positive_scale_active_dataFsecond)) + ((dst_positive_scale_active_dataFsecond) + (dst_positive_scale_active_dataFsecond))) + (((dst_negative_code_active_dataFsecond) + (dst_negative_scale_active_dataFsecond)) * S ((dst_negative_code_active_dataFsecond) + (dst_negative_scale_active_dataFsecond)) + ((dst_negative_scale_active_dataFsecond) + (dst_negative_scale_active_dataFsecond)))) + ((((dst_negative_code_active_dataFsecond) + (dst_negative_scale_active_dataFsecond)) * S ((dst_negative_code_active_dataFsecond) + (dst_negative_scale_active_dataFsecond)) + ((dst_negative_scale_active_dataFsecond) + (dst_negative_scale_active_dataFsecond))) + (((dst_negative_code_active_dataFsecond) + (dst_negative_scale_active_dataFsecond)) * S ((dst_negative_code_active_dataFsecond) + (dst_negative_scale_active_dataFsecond)) + ((dst_negative_scale_active_dataFsecond) + (dst_negative_scale_active_dataFsecond)))))) /\ (((((exists ff_h_pvs_active_dataFsecondpositive. ff_h_pvs_active_dataFsecondpositive + S (dst_positive_active_dataFsecond) = S ((S (mp_b_active_dataF)) * dst_positive_scale_active_dataFsecond)) /\ exists ff_q_pvs_active_dataFsecondpositive. dst_positive_code_active_dataFsecond = ff_q_pvs_active_dataFsecondpositive * S ((S (mp_b_active_dataF)) * dst_positive_scale_active_dataFsecond) + (dst_positive_active_dataFsecond))) /\ (((((exists ff_h_pvs_active_dataFsecondnegative. ff_h_pvs_active_dataFsecondnegative + S (dst_negative_active_dataFsecond) = S ((S (mp_b_active_dataF)) * dst_negative_scale_active_dataFsecond)) /\ exists ff_q_pvs_active_dataFsecondnegative. dst_negative_code_active_dataFsecond = ff_q_pvs_active_dataFsecondnegative * S ((S (mp_b_active_dataF)) * dst_negative_scale_active_dataFsecond) + (dst_negative_active_dataFsecond))) /\ (exists ge_balance_positive_active_dataFsecondvalue ge_balance_negative_active_dataFsecondvalue. (((((mp_y_active_dataF) = 2 * (ge_balance_positive_active_dataFsecondvalue) /\ (ge_balance_negative_active_dataFsecondvalue) = 0) \/ exists ge_signed_half_active_dataFsecondvaluedecode. (((mp_y_active_dataF) = 2 * ge_signed_half_active_dataFsecondvaluedecode + 1 /\ (ge_balance_positive_active_dataFsecondvalue) = 0) /\ (ge_balance_negative_active_dataFsecondvalue) = S ge_signed_half_active_dataFsecondvaluedecode))) /\ ((dst_positive_active_dataFsecond) + ge_balance_negative_active_dataFsecondvalue = (dst_negative_active_dataFsecond) + ge_balance_positive_active_dataFsecondvalue))))))))) -> (exists dst_positive_code_active_dataFproduct dst_positive_scale_active_dataFproduct dst_negative_code_active_dataFproduct dst_negative_scale_active_dataFproduct dst_positive_active_dataFproduct dst_negative_active_dataFproduct. (((F) = (((((dst_positive_code_active_dataFproduct) + (dst_positive_scale_active_dataFproduct)) * S ((dst_positive_code_active_dataFproduct) + (dst_positive_scale_active_dataFproduct)) + ((dst_positive_scale_active_dataFproduct) + (dst_positive_scale_active_dataFproduct))) + (((dst_negative_code_active_dataFproduct) + (dst_negative_scale_active_dataFproduct)) * S ((dst_negative_code_active_dataFproduct) + (dst_negative_scale_active_dataFproduct)) + ((dst_negative_scale_active_dataFproduct) + (dst_negative_scale_active_dataFproduct)))) * S ((((dst_positive_code_active_dataFproduct) + (dst_positive_scale_active_dataFproduct)) * S ((dst_positive_code_active_dataFproduct) + (dst_positive_scale_active_dataFproduct)) + ((dst_positive_scale_active_dataFproduct) + (dst_positive_scale_active_dataFproduct))) + (((dst_negative_code_active_dataFproduct) + (dst_negative_scale_active_dataFproduct)) * S ((dst_negative_code_active_dataFproduct) + (dst_negative_scale_active_dataFproduct)) + ((dst_negative_scale_active_dataFproduct) + (dst_negative_scale_active_dataFproduct)))) + ((((dst_negative_code_active_dataFproduct) + (dst_negative_scale_active_dataFproduct)) * S ((dst_negative_code_active_dataFproduct) + (dst_negative_scale_active_dataFproduct)) + ((dst_negative_scale_active_dataFproduct) + (dst_negative_scale_active_dataFproduct))) + (((dst_negative_code_active_dataFproduct) + (dst_negative_scale_active_dataFproduct)) * S ((dst_negative_code_active_dataFproduct) + (dst_negative_scale_active_dataFproduct)) + ((dst_negative_scale_active_dataFproduct) + (dst_negative_scale_active_dataFproduct)))))) /\ (((((exists ff_h_pvs_active_dataFproductpositive. ff_h_pvs_active_dataFproductpositive + S (dst_positive_active_dataFproduct) = S ((S (mp_a_active_dataF*mp_b_active_dataF)) * dst_positive_scale_active_dataFproduct)) /\ exists ff_q_pvs_active_dataFproductpositive. dst_positive_code_active_dataFproduct = ff_q_pvs_active_dataFproductpositive * S ((S (mp_a_active_dataF*mp_b_active_dataF)) * dst_positive_scale_active_dataFproduct) + (dst_positive_active_dataFproduct))) /\ (((((exists ff_h_pvs_active_dataFproductnegative. ff_h_pvs_active_dataFproductnegative + S (dst_negative_active_dataFproduct) = S ((S (mp_a_active_dataF*mp_b_active_dataF)) * dst_negative_scale_active_dataFproduct)) /\ exists ff_q_pvs_active_dataFproductnegative. dst_negative_code_active_dataFproduct = ff_q_pvs_active_dataFproductnegative * S ((S (mp_a_active_dataF*mp_b_active_dataF)) * dst_negative_scale_active_dataFproduct) + (dst_negative_active_dataFproduct))) /\ (exists ge_balance_positive_active_dataFproductvalue ge_balance_negative_active_dataFproductvalue. (((((mp_z_active_dataF) = 2 * (ge_balance_positive_active_dataFproductvalue) /\ (ge_balance_negative_active_dataFproductvalue) = 0) \/ exists ge_signed_half_active_dataFproductvaluedecode. (((mp_z_active_dataF) = 2 * ge_signed_half_active_dataFproductvaluedecode + 1 /\ (ge_balance_positive_active_dataFproductvalue) = 0) /\ (ge_balance_negative_active_dataFproductvalue) = S ge_signed_half_active_dataFproductvaluedecode))) /\ ((dst_positive_active_dataFproduct) + ge_balance_negative_active_dataFproductvalue = (dst_negative_active_dataFproduct) + ge_balance_positive_active_dataFproductvalue))))))))) -> (exists sto_ap_active_dataFlaw sto_an_active_dataFlaw sto_bp_active_dataFlaw sto_bn_active_dataFlaw sto_cp_active_dataFlaw sto_cn_active_dataFlaw. (((((mp_x_active_dataF) = 2 * (sto_ap_active_dataFlaw) /\ (sto_an_active_dataFlaw) = 0) \/ exists ge_signed_half_active_dataFlawleft. (((mp_x_active_dataF) = 2 * ge_signed_half_active_dataFlawleft + 1 /\ (sto_ap_active_dataFlaw) = 0) /\ (sto_an_active_dataFlaw) = S ge_signed_half_active_dataFlawleft))) /\ ((((((mp_y_active_dataF) = 2 * (sto_bp_active_dataFlaw) /\ (sto_bn_active_dataFlaw) = 0) \/ exists ge_signed_half_active_dataFlawright. (((mp_y_active_dataF) = 2 * ge_signed_half_active_dataFlawright + 1 /\ (sto_bp_active_dataFlaw) = 0) /\ (sto_bn_active_dataFlaw) = S ge_signed_half_active_dataFlawright))) /\ ((((((mp_z_active_dataF) = 2 * (sto_cp_active_dataFlaw) /\ (sto_cn_active_dataFlaw) = 0) \/ exists ge_signed_half_active_dataFlawoutput. (((mp_z_active_dataF) = 2 * ge_signed_half_active_dataFlawoutput + 1 /\ (sto_cp_active_dataFlaw) = 0) /\ (sto_cn_active_dataFlaw) = S ge_signed_half_active_dataFlawoutput))) /\ ((sto_ap_active_dataFlaw * sto_bp_active_dataFlaw + sto_an_active_dataFlaw * sto_bn_active_dataFlaw) + sto_cn_active_dataFlaw = (sto_ap_active_dataFlaw * sto_bn_active_dataFlaw + sto_an_active_dataFlaw * sto_bp_active_dataFlaw) + sto_cp_active_dataFlaw)))))))))))))) /\ (((((~((N)=0)) /\ (((exists dst_positive_code_active_dataGtable dst_positive_scale_active_dataGtable dst_negative_code_active_dataGtable dst_negative_scale_active_dataGtable. (((G) = (((((dst_positive_code_active_dataGtable) + (dst_positive_scale_active_dataGtable)) * S ((dst_positive_code_active_dataGtable) + (dst_positive_scale_active_dataGtable)) + ((dst_positive_scale_active_dataGtable) + (dst_positive_scale_active_dataGtable))) + (((dst_negative_code_active_dataGtable) + (dst_negative_scale_active_dataGtable)) * S ((dst_negative_code_active_dataGtable) + (dst_negative_scale_active_dataGtable)) + ((dst_negative_scale_active_dataGtable) + (dst_negative_scale_active_dataGtable)))) * S ((((dst_positive_code_active_dataGtable) + (dst_positive_scale_active_dataGtable)) * S ((dst_positive_code_active_dataGtable) + (dst_positive_scale_active_dataGtable)) + ((dst_positive_scale_active_dataGtable) + (dst_positive_scale_active_dataGtable))) + (((dst_negative_code_active_dataGtable) + (dst_negative_scale_active_dataGtable)) * S ((dst_negative_code_active_dataGtable) + (dst_negative_scale_active_dataGtable)) + ((dst_negative_scale_active_dataGtable) + (dst_negative_scale_active_dataGtable)))) + ((((dst_negative_code_active_dataGtable) + (dst_negative_scale_active_dataGtable)) * S ((dst_negative_code_active_dataGtable) + (dst_negative_scale_active_dataGtable)) + ((dst_negative_scale_active_dataGtable) + (dst_negative_scale_active_dataGtable))) + (((dst_negative_code_active_dataGtable) + (dst_negative_scale_active_dataGtable)) * S ((dst_negative_code_active_dataGtable) + (dst_negative_scale_active_dataGtable)) + ((dst_negative_scale_active_dataGtable) + (dst_negative_scale_active_dataGtable)))))) /\ (forall dst_index_active_dataGtable. (exists pvs_le_gap_active_dataGtabledomain. pvs_le_gap_active_dataGtabledomain + (dst_index_active_dataGtable) = (N)) -> exists dst_positive_active_dataGtable dst_negative_active_dataGtable dst_value_active_dataGtable. ((((exists ff_h_pvs_active_dataGtableentrypositive. ff_h_pvs_active_dataGtableentrypositive + S (dst_positive_active_dataGtable) = S ((S (dst_index_active_dataGtable)) * dst_positive_scale_active_dataGtable)) /\ exists ff_q_pvs_active_dataGtableentrypositive. dst_positive_code_active_dataGtable = ff_q_pvs_active_dataGtableentrypositive * S ((S (dst_index_active_dataGtable)) * dst_positive_scale_active_dataGtable) + (dst_positive_active_dataGtable))) /\ (((((exists ff_h_pvs_active_dataGtableentrynegative. ff_h_pvs_active_dataGtableentrynegative + S (dst_negative_active_dataGtable) = S ((S (dst_index_active_dataGtable)) * dst_negative_scale_active_dataGtable)) /\ exists ff_q_pvs_active_dataGtableentrynegative. dst_negative_code_active_dataGtable = ff_q_pvs_active_dataGtableentrynegative * S ((S (dst_index_active_dataGtable)) * dst_negative_scale_active_dataGtable) + (dst_negative_active_dataGtable))) /\ (exists ge_balance_positive_active_dataGtableentryvalue ge_balance_negative_active_dataGtableentryvalue. (((((dst_value_active_dataGtable) = 2 * (ge_balance_positive_active_dataGtableentryvalue) /\ (ge_balance_negative_active_dataGtableentryvalue) = 0) \/ exists ge_signed_half_active_dataGtableentryvaluedecode. (((dst_value_active_dataGtable) = 2 * ge_signed_half_active_dataGtableentryvaluedecode + 1 /\ (ge_balance_positive_active_dataGtableentryvalue) = 0) /\ (ge_balance_negative_active_dataGtableentryvalue) = S ge_signed_half_active_dataGtableentryvaluedecode))) /\ ((dst_positive_active_dataGtable) + ge_balance_negative_active_dataGtableentryvalue = (dst_negative_active_dataGtable) + ge_balance_positive_active_dataGtableentryvalue))))))))) /\ (((exists dst_positive_code_active_dataGone dst_positive_scale_active_dataGone dst_negative_code_active_dataGone dst_negative_scale_active_dataGone dst_positive_active_dataGone dst_negative_active_dataGone. (((G) = (((((dst_positive_code_active_dataGone) + (dst_positive_scale_active_dataGone)) * S ((dst_positive_code_active_dataGone) + (dst_positive_scale_active_dataGone)) + ((dst_positive_scale_active_dataGone) + (dst_positive_scale_active_dataGone))) + (((dst_negative_code_active_dataGone) + (dst_negative_scale_active_dataGone)) * S ((dst_negative_code_active_dataGone) + (dst_negative_scale_active_dataGone)) + ((dst_negative_scale_active_dataGone) + (dst_negative_scale_active_dataGone)))) * S ((((dst_positive_code_active_dataGone) + (dst_positive_scale_active_dataGone)) * S ((dst_positive_code_active_dataGone) + (dst_positive_scale_active_dataGone)) + ((dst_positive_scale_active_dataGone) + (dst_positive_scale_active_dataGone))) + (((dst_negative_code_active_dataGone) + (dst_negative_scale_active_dataGone)) * S ((dst_negative_code_active_dataGone) + (dst_negative_scale_active_dataGone)) + ((dst_negative_scale_active_dataGone) + (dst_negative_scale_active_dataGone)))) + ((((dst_negative_code_active_dataGone) + (dst_negative_scale_active_dataGone)) * S ((dst_negative_code_active_dataGone) + (dst_negative_scale_active_dataGone)) + ((dst_negative_scale_active_dataGone) + (dst_negative_scale_active_dataGone))) + (((dst_negative_code_active_dataGone) + (dst_negative_scale_active_dataGone)) * S ((dst_negative_code_active_dataGone) + (dst_negative_scale_active_dataGone)) + ((dst_negative_scale_active_dataGone) + (dst_negative_scale_active_dataGone)))))) /\ (((((exists ff_h_pvs_active_dataGonepositive. ff_h_pvs_active_dataGonepositive + S (dst_positive_active_dataGone) = S ((S (1)) * dst_positive_scale_active_dataGone)) /\ exists ff_q_pvs_active_dataGonepositive. dst_positive_code_active_dataGone = ff_q_pvs_active_dataGonepositive * S ((S (1)) * dst_positive_scale_active_dataGone) + (dst_positive_active_dataGone))) /\ (((((exists ff_h_pvs_active_dataGonenegative. ff_h_pvs_active_dataGonenegative + S (dst_negative_active_dataGone) = S ((S (1)) * dst_negative_scale_active_dataGone)) /\ exists ff_q_pvs_active_dataGonenegative. dst_negative_code_active_dataGone = ff_q_pvs_active_dataGonenegative * S ((S (1)) * dst_negative_scale_active_dataGone) + (dst_negative_active_dataGone))) /\ (exists ge_balance_positive_active_dataGonevalue ge_balance_negative_active_dataGonevalue. (((((2) = 2 * (ge_balance_positive_active_dataGonevalue) /\ (ge_balance_negative_active_dataGonevalue) = 0) \/ exists ge_signed_half_active_dataGonevaluedecode. (((2) = 2 * ge_signed_half_active_dataGonevaluedecode + 1 /\ (ge_balance_positive_active_dataGonevalue) = 0) /\ (ge_balance_negative_active_dataGonevalue) = S ge_signed_half_active_dataGonevaluedecode))) /\ ((dst_positive_active_dataGone) + ge_balance_negative_active_dataGonevalue = (dst_negative_active_dataGone) + ge_balance_positive_active_dataGonevalue))))))))) /\ (forall mp_a_active_dataG mp_b_active_dataG mp_x_active_dataG mp_y_active_dataG mp_z_active_dataG. ~(mp_a_active_dataG=0) -> ~(mp_b_active_dataG=0) -> (exists pvs_le_gap_active_dataGbound. pvs_le_gap_active_dataGbound + (mp_a_active_dataG*mp_b_active_dataG) = (N)) -> (forall frp_divisor_active_dataGcoprime. (exists frp_left_factor_active_dataGcoprime. mp_a_active_dataG = frp_divisor_active_dataGcoprime * frp_left_factor_active_dataGcoprime) -> (exists frp_right_factor_active_dataGcoprime. mp_b_active_dataG = frp_divisor_active_dataGcoprime * frp_right_factor_active_dataGcoprime) -> frp_divisor_active_dataGcoprime = 1) -> (exists dst_positive_code_active_dataGfirst dst_positive_scale_active_dataGfirst dst_negative_code_active_dataGfirst dst_negative_scale_active_dataGfirst dst_positive_active_dataGfirst dst_negative_active_dataGfirst. (((G) = (((((dst_positive_code_active_dataGfirst) + (dst_positive_scale_active_dataGfirst)) * S ((dst_positive_code_active_dataGfirst) + (dst_positive_scale_active_dataGfirst)) + ((dst_positive_scale_active_dataGfirst) + (dst_positive_scale_active_dataGfirst))) + (((dst_negative_code_active_dataGfirst) + (dst_negative_scale_active_dataGfirst)) * S ((dst_negative_code_active_dataGfirst) + (dst_negative_scale_active_dataGfirst)) + ((dst_negative_scale_active_dataGfirst) + (dst_negative_scale_active_dataGfirst)))) * S ((((dst_positive_code_active_dataGfirst) + (dst_positive_scale_active_dataGfirst)) * S ((dst_positive_code_active_dataGfirst) + (dst_positive_scale_active_dataGfirst)) + ((dst_positive_scale_active_dataGfirst) + (dst_positive_scale_active_dataGfirst))) + (((dst_negative_code_active_dataGfirst) + (dst_negative_scale_active_dataGfirst)) * S ((dst_negative_code_active_dataGfirst) + (dst_negative_scale_active_dataGfirst)) + ((dst_negative_scale_active_dataGfirst) + (dst_negative_scale_active_dataGfirst)))) + ((((dst_negative_code_active_dataGfirst) + (dst_negative_scale_active_dataGfirst)) * S ((dst_negative_code_active_dataGfirst) + (dst_negative_scale_active_dataGfirst)) + ((dst_negative_scale_active_dataGfirst) + (dst_negative_scale_active_dataGfirst))) + (((dst_negative_code_active_dataGfirst) + (dst_negative_scale_active_dataGfirst)) * S ((dst_negative_code_active_dataGfirst) + (dst_negative_scale_active_dataGfirst)) + ((dst_negative_scale_active_dataGfirst) + (dst_negative_scale_active_dataGfirst)))))) /\ (((((exists ff_h_pvs_active_dataGfirstpositive. ff_h_pvs_active_dataGfirstpositive + S (dst_positive_active_dataGfirst) = S ((S (mp_a_active_dataG)) * dst_positive_scale_active_dataGfirst)) /\ exists ff_q_pvs_active_dataGfirstpositive. dst_positive_code_active_dataGfirst = ff_q_pvs_active_dataGfirstpositive * S ((S (mp_a_active_dataG)) * dst_positive_scale_active_dataGfirst) + (dst_positive_active_dataGfirst))) /\ (((((exists ff_h_pvs_active_dataGfirstnegative. ff_h_pvs_active_dataGfirstnegative + S (dst_negative_active_dataGfirst) = S ((S (mp_a_active_dataG)) * dst_negative_scale_active_dataGfirst)) /\ exists ff_q_pvs_active_dataGfirstnegative. dst_negative_code_active_dataGfirst = ff_q_pvs_active_dataGfirstnegative * S ((S (mp_a_active_dataG)) * dst_negative_scale_active_dataGfirst) + (dst_negative_active_dataGfirst))) /\ (exists ge_balance_positive_active_dataGfirstvalue ge_balance_negative_active_dataGfirstvalue. (((((mp_x_active_dataG) = 2 * (ge_balance_positive_active_dataGfirstvalue) /\ (ge_balance_negative_active_dataGfirstvalue) = 0) \/ exists ge_signed_half_active_dataGfirstvaluedecode. (((mp_x_active_dataG) = 2 * ge_signed_half_active_dataGfirstvaluedecode + 1 /\ (ge_balance_positive_active_dataGfirstvalue) = 0) /\ (ge_balance_negative_active_dataGfirstvalue) = S ge_signed_half_active_dataGfirstvaluedecode))) /\ ((dst_positive_active_dataGfirst) + ge_balance_negative_active_dataGfirstvalue = (dst_negative_active_dataGfirst) + ge_balance_positive_active_dataGfirstvalue))))))))) -> (exists dst_positive_code_active_dataGsecond dst_positive_scale_active_dataGsecond dst_negative_code_active_dataGsecond dst_negative_scale_active_dataGsecond dst_positive_active_dataGsecond dst_negative_active_dataGsecond. (((G) = (((((dst_positive_code_active_dataGsecond) + (dst_positive_scale_active_dataGsecond)) * S ((dst_positive_code_active_dataGsecond) + (dst_positive_scale_active_dataGsecond)) + ((dst_positive_scale_active_dataGsecond) + (dst_positive_scale_active_dataGsecond))) + (((dst_negative_code_active_dataGsecond) + (dst_negative_scale_active_dataGsecond)) * S ((dst_negative_code_active_dataGsecond) + (dst_negative_scale_active_dataGsecond)) + ((dst_negative_scale_active_dataGsecond) + (dst_negative_scale_active_dataGsecond)))) * S ((((dst_positive_code_active_dataGsecond) + (dst_positive_scale_active_dataGsecond)) * S ((dst_positive_code_active_dataGsecond) + (dst_positive_scale_active_dataGsecond)) + ((dst_positive_scale_active_dataGsecond) + (dst_positive_scale_active_dataGsecond))) + (((dst_negative_code_active_dataGsecond) + (dst_negative_scale_active_dataGsecond)) * S ((dst_negative_code_active_dataGsecond) + (dst_negative_scale_active_dataGsecond)) + ((dst_negative_scale_active_dataGsecond) + (dst_negative_scale_active_dataGsecond)))) + ((((dst_negative_code_active_dataGsecond) + (dst_negative_scale_active_dataGsecond)) * S ((dst_negative_code_active_dataGsecond) + (dst_negative_scale_active_dataGsecond)) + ((dst_negative_scale_active_dataGsecond) + (dst_negative_scale_active_dataGsecond))) + (((dst_negative_code_active_dataGsecond) + (dst_negative_scale_active_dataGsecond)) * S ((dst_negative_code_active_dataGsecond) + (dst_negative_scale_active_dataGsecond)) + ((dst_negative_scale_active_dataGsecond) + (dst_negative_scale_active_dataGsecond)))))) /\ (((((exists ff_h_pvs_active_dataGsecondpositive. ff_h_pvs_active_dataGsecondpositive + S (dst_positive_active_dataGsecond) = S ((S (mp_b_active_dataG)) * dst_positive_scale_active_dataGsecond)) /\ exists ff_q_pvs_active_dataGsecondpositive. dst_positive_code_active_dataGsecond = ff_q_pvs_active_dataGsecondpositive * S ((S (mp_b_active_dataG)) * dst_positive_scale_active_dataGsecond) + (dst_positive_active_dataGsecond))) /\ (((((exists ff_h_pvs_active_dataGsecondnegative. ff_h_pvs_active_dataGsecondnegative + S (dst_negative_active_dataGsecond) = S ((S (mp_b_active_dataG)) * dst_negative_scale_active_dataGsecond)) /\ exists ff_q_pvs_active_dataGsecondnegative. dst_negative_code_active_dataGsecond = ff_q_pvs_active_dataGsecondnegative * S ((S (mp_b_active_dataG)) * dst_negative_scale_active_dataGsecond) + (dst_negative_active_dataGsecond))) /\ (exists ge_balance_positive_active_dataGsecondvalue ge_balance_negative_active_dataGsecondvalue. (((((mp_y_active_dataG) = 2 * (ge_balance_positive_active_dataGsecondvalue) /\ (ge_balance_negative_active_dataGsecondvalue) = 0) \/ exists ge_signed_half_active_dataGsecondvaluedecode. (((mp_y_active_dataG) = 2 * ge_signed_half_active_dataGsecondvaluedecode + 1 /\ (ge_balance_positive_active_dataGsecondvalue) = 0) /\ (ge_balance_negative_active_dataGsecondvalue) = S ge_signed_half_active_dataGsecondvaluedecode))) /\ ((dst_positive_active_dataGsecond) + ge_balance_negative_active_dataGsecondvalue = (dst_negative_active_dataGsecond) + ge_balance_positive_active_dataGsecondvalue))))))))) -> (exists dst_positive_code_active_dataGproduct dst_positive_scale_active_dataGproduct dst_negative_code_active_dataGproduct dst_negative_scale_active_dataGproduct dst_positive_active_dataGproduct dst_negative_active_dataGproduct. (((G) = (((((dst_positive_code_active_dataGproduct) + (dst_positive_scale_active_dataGproduct)) * S ((dst_positive_code_active_dataGproduct) + (dst_positive_scale_active_dataGproduct)) + ((dst_positive_scale_active_dataGproduct) + (dst_positive_scale_active_dataGproduct))) + (((dst_negative_code_active_dataGproduct) + (dst_negative_scale_active_dataGproduct)) * S ((dst_negative_code_active_dataGproduct) + (dst_negative_scale_active_dataGproduct)) + ((dst_negative_scale_active_dataGproduct) + (dst_negative_scale_active_dataGproduct)))) * S ((((dst_positive_code_active_dataGproduct) + (dst_positive_scale_active_dataGproduct)) * S ((dst_positive_code_active_dataGproduct) + (dst_positive_scale_active_dataGproduct)) + ((dst_positive_scale_active_dataGproduct) + (dst_positive_scale_active_dataGproduct))) + (((dst_negative_code_active_dataGproduct) + (dst_negative_scale_active_dataGproduct)) * S ((dst_negative_code_active_dataGproduct) + (dst_negative_scale_active_dataGproduct)) + ((dst_negative_scale_active_dataGproduct) + (dst_negative_scale_active_dataGproduct)))) + ((((dst_negative_code_active_dataGproduct) + (dst_negative_scale_active_dataGproduct)) * S ((dst_negative_code_active_dataGproduct) + (dst_negative_scale_active_dataGproduct)) + ((dst_negative_scale_active_dataGproduct) + (dst_negative_scale_active_dataGproduct))) + (((dst_negative_code_active_dataGproduct) + (dst_negative_scale_active_dataGproduct)) * S ((dst_negative_code_active_dataGproduct) + (dst_negative_scale_active_dataGproduct)) + ((dst_negative_scale_active_dataGproduct) + (dst_negative_scale_active_dataGproduct)))))) /\ (((((exists ff_h_pvs_active_dataGproductpositive. ff_h_pvs_active_dataGproductpositive + S (dst_positive_active_dataGproduct) = S ((S (mp_a_active_dataG*mp_b_active_dataG)) * dst_positive_scale_active_dataGproduct)) /\ exists ff_q_pvs_active_dataGproductpositive. dst_positive_code_active_dataGproduct = ff_q_pvs_active_dataGproductpositive * S ((S (mp_a_active_dataG*mp_b_active_dataG)) * dst_positive_scale_active_dataGproduct) + (dst_positive_active_dataGproduct))) /\ (((((exists ff_h_pvs_active_dataGproductnegative. ff_h_pvs_active_dataGproductnegative + S (dst_negative_active_dataGproduct) = S ((S (mp_a_active_dataG*mp_b_active_dataG)) * dst_negative_scale_active_dataGproduct)) /\ exists ff_q_pvs_active_dataGproductnegative. dst_negative_code_active_dataGproduct = ff_q_pvs_active_dataGproductnegative * S ((S (mp_a_active_dataG*mp_b_active_dataG)) * dst_negative_scale_active_dataGproduct) + (dst_negative_active_dataGproduct))) /\ (exists ge_balance_positive_active_dataGproductvalue ge_balance_negative_active_dataGproductvalue. (((((mp_z_active_dataG) = 2 * (ge_balance_positive_active_dataGproductvalue) /\ (ge_balance_negative_active_dataGproductvalue) = 0) \/ exists ge_signed_half_active_dataGproductvaluedecode. (((mp_z_active_dataG) = 2 * ge_signed_half_active_dataGproductvaluedecode + 1 /\ (ge_balance_positive_active_dataGproductvalue) = 0) /\ (ge_balance_negative_active_dataGproductvalue) = S ge_signed_half_active_dataGproductvaluedecode))) /\ ((dst_positive_active_dataGproduct) + ge_balance_negative_active_dataGproductvalue = (dst_negative_active_dataGproduct) + ge_balance_positive_active_dataGproductvalue))))))))) -> (exists sto_ap_active_dataGlaw sto_an_active_dataGlaw sto_bp_active_dataGlaw sto_bn_active_dataGlaw sto_cp_active_dataGlaw sto_cn_active_dataGlaw. (((((mp_x_active_dataG) = 2 * (sto_ap_active_dataGlaw) /\ (sto_an_active_dataGlaw) = 0) \/ exists ge_signed_half_active_dataGlawleft. (((mp_x_active_dataG) = 2 * ge_signed_half_active_dataGlawleft + 1 /\ (sto_ap_active_dataGlaw) = 0) /\ (sto_an_active_dataGlaw) = S ge_signed_half_active_dataGlawleft))) /\ ((((((mp_y_active_dataG) = 2 * (sto_bp_active_dataGlaw) /\ (sto_bn_active_dataGlaw) = 0) \/ exists ge_signed_half_active_dataGlawright. (((mp_y_active_dataG) = 2 * ge_signed_half_active_dataGlawright + 1 /\ (sto_bp_active_dataGlaw) = 0) /\ (sto_bn_active_dataGlaw) = S ge_signed_half_active_dataGlawright))) /\ ((((((mp_z_active_dataG) = 2 * (sto_cp_active_dataGlaw) /\ (sto_cn_active_dataGlaw) = 0) \/ exists ge_signed_half_active_dataGlawoutput. (((mp_z_active_dataG) = 2 * ge_signed_half_active_dataGlawoutput + 1 /\ (sto_cp_active_dataGlaw) = 0) /\ (sto_cn_active_dataGlaw) = S ge_signed_half_active_dataGlawoutput))) /\ ((sto_ap_active_dataGlaw * sto_bp_active_dataGlaw + sto_an_active_dataGlaw * sto_bn_active_dataGlaw) + sto_cn_active_dataGlaw = (sto_ap_active_dataGlaw * sto_bn_active_dataGlaw + sto_an_active_dataGlaw * sto_bp_active_dataGlaw) + sto_cp_active_dataGlaw)))))))))))))) /\ (((~((m)=0)) /\ (((~((n)=0)) /\ (((exists pvs_le_gap_active_databound. pvs_le_gap_active_databound + ((m)*(n)) = (N)) /\ (((forall sfd_common_divisor_active_datacoprime. (exists pvs_factor_active_datacoprimeleft. (m) = (sfd_common_divisor_active_datacoprime) * pvs_factor_active_datacoprimeleft) -> (exists pvs_factor_active_datacoprimeright. (n) = (sfd_common_divisor_active_datacoprime) * pvs_factor_active_datacoprimeright) -> sfd_common_divisor_active_datacoprime = 1) /\ (((((exists dst_positive_code_active_datalefttable dst_positive_scale_active_datalefttable dst_negative_code_active_datalefttable dst_negative_scale_active_datalefttable. (((A) = (((((dst_positive_code_active_datalefttable) + (dst_positive_scale_active_datalefttable)) * S ((dst_positive_code_active_datalefttable) + (dst_positive_scale_active_datalefttable)) + ((dst_positive_scale_active_datalefttable) + (dst_positive_scale_active_datalefttable))) + (((dst_negative_code_active_datalefttable) + (dst_negative_scale_active_datalefttable)) * S ((dst_negative_code_active_datalefttable) + (dst_negative_scale_active_datalefttable)) + ((dst_negative_scale_active_datalefttable) + (dst_negative_scale_active_datalefttable)))) * S ((((dst_positive_code_active_datalefttable) + (dst_positive_scale_active_datalefttable)) * S ((dst_positive_code_active_datalefttable) + (dst_positive_scale_active_datalefttable)) + ((dst_positive_scale_active_datalefttable) + (dst_positive_scale_active_datalefttable))) + (((dst_negative_code_active_datalefttable) + (dst_negative_scale_active_datalefttable)) * S ((dst_negative_code_active_datalefttable) + (dst_negative_scale_active_datalefttable)) + ((dst_negative_scale_active_datalefttable) + (dst_negative_scale_active_datalefttable)))) + ((((dst_negative_code_active_datalefttable) + (dst_negative_scale_active_datalefttable)) * S ((dst_negative_code_active_datalefttable) + (dst_negative_scale_active_datalefttable)) + ((dst_negative_scale_active_datalefttable) + (dst_negative_scale_active_datalefttable))) + (((dst_negative_code_active_datalefttable) + (dst_negative_scale_active_datalefttable)) * S ((dst_negative_code_active_datalefttable) + (dst_negative_scale_active_datalefttable)) + ((dst_negative_scale_active_datalefttable) + (dst_negative_scale_active_datalefttable)))))) /\ (forall dst_index_active_datalefttable. (exists pvs_le_gap_active_datalefttabledomain. pvs_le_gap_active_datalefttabledomain + (dst_index_active_datalefttable) = (m)) -> exists dst_positive_active_datalefttable dst_negative_active_datalefttable dst_value_active_datalefttable. ((((exists ff_h_pvs_active_datalefttableentrypositive. ff_h_pvs_active_datalefttableentrypositive + S (dst_positive_active_datalefttable) = S ((S (dst_index_active_datalefttable)) * dst_positive_scale_active_datalefttable)) /\ exists ff_q_pvs_active_datalefttableentrypositive. dst_positive_code_active_datalefttable = ff_q_pvs_active_datalefttableentrypositive * S ((S (dst_index_active_datalefttable)) * dst_positive_scale_active_datalefttable) + (dst_positive_active_datalefttable))) /\ (((((exists ff_h_pvs_active_datalefttableentrynegative. ff_h_pvs_active_datalefttableentrynegative + S (dst_negative_active_datalefttable) = S ((S (dst_index_active_datalefttable)) * dst_negative_scale_active_datalefttable)) /\ exists ff_q_pvs_active_datalefttableentrynegative. dst_negative_code_active_datalefttable = ff_q_pvs_active_datalefttableentrynegative * S ((S (dst_index_active_datalefttable)) * dst_negative_scale_active_datalefttable) + (dst_negative_active_datalefttable))) /\ (exists ge_balance_positive_active_datalefttableentryvalue ge_balance_negative_active_datalefttableentryvalue. (((((dst_value_active_datalefttable) = 2 * (ge_balance_positive_active_datalefttableentryvalue) /\ (ge_balance_negative_active_datalefttableentryvalue) = 0) \/ exists ge_signed_half_active_datalefttableentryvaluedecode. (((dst_value_active_datalefttable) = 2 * ge_signed_half_active_datalefttableentryvaluedecode + 1 /\ (ge_balance_positive_active_datalefttableentryvalue) = 0) /\ (ge_balance_negative_active_datalefttableentryvalue) = S ge_signed_half_active_datalefttableentryvaluedecode))) /\ ((dst_positive_active_datalefttable) + ge_balance_negative_active_datalefttableentryvalue = (dst_negative_active_datalefttable) + ge_balance_positive_active_datalefttableentryvalue))))))))) /\ (forall dc_index_active_dataleft dc_value_active_dataleft. (exists pvs_le_gap_active_dataleftdomain. pvs_le_gap_active_dataleftdomain + (dc_index_active_dataleft) = (m)) -> (exists dst_positive_code_active_dataleftlookup dst_positive_scale_active_dataleftlookup dst_negative_code_active_dataleftlookup dst_negative_scale_active_dataleftlookup dst_positive_active_dataleftlookup dst_negative_active_dataleftlookup. (((A) = (((((dst_positive_code_active_dataleftlookup) + (dst_positive_scale_active_dataleftlookup)) * S ((dst_positive_code_active_dataleftlookup) + (dst_positive_scale_active_dataleftlookup)) + ((dst_positive_scale_active_dataleftlookup) + (dst_positive_scale_active_dataleftlookup))) + (((dst_negative_code_active_dataleftlookup) + (dst_negative_scale_active_dataleftlookup)) * S ((dst_negative_code_active_dataleftlookup) + (dst_negative_scale_active_dataleftlookup)) + ((dst_negative_scale_active_dataleftlookup) + (dst_negative_scale_active_dataleftlookup)))) * S ((((dst_positive_code_active_dataleftlookup) + (dst_positive_scale_active_dataleftlookup)) * S ((dst_positive_code_active_dataleftlookup) + (dst_positive_scale_active_dataleftlookup)) + ((dst_positive_scale_active_dataleftlookup) + (dst_positive_scale_active_dataleftlookup))) + (((dst_negative_code_active_dataleftlookup) + (dst_negative_scale_active_dataleftlookup)) * S ((dst_negative_code_active_dataleftlookup) + (dst_negative_scale_active_dataleftlookup)) + ((dst_negative_scale_active_dataleftlookup) + (dst_negative_scale_active_dataleftlookup)))) + ((((dst_negative_code_active_dataleftlookup) + (dst_negative_scale_active_dataleftlookup)) * S ((dst_negative_code_active_dataleftlookup) + (dst_negative_scale_active_dataleftlookup)) + ((dst_negative_scale_active_dataleftlookup) + (dst_negative_scale_active_dataleftlookup))) + (((dst_negative_code_active_dataleftlookup) + (dst_negative_scale_active_dataleftlookup)) * S ((dst_negative_code_active_dataleftlookup) + (dst_negative_scale_active_dataleftlookup)) + ((dst_negative_scale_active_dataleftlookup) + (dst_negative_scale_active_dataleftlookup)))))) /\ (((((exists ff_h_pvs_active_dataleftlookuppositive. ff_h_pvs_active_dataleftlookuppositive + S (dst_positive_active_dataleftlookup) = S ((S (dc_index_active_dataleft)) * dst_positive_scale_active_dataleftlookup)) /\ exists ff_q_pvs_active_dataleftlookuppositive. dst_positive_code_active_dataleftlookup = ff_q_pvs_active_dataleftlookuppositive * S ((S (dc_index_active_dataleft)) * dst_positive_scale_active_dataleftlookup) + (dst_positive_active_dataleftlookup))) /\ (((((exists ff_h_pvs_active_dataleftlookupnegative. ff_h_pvs_active_dataleftlookupnegative + S (dst_negative_active_dataleftlookup) = S ((S (dc_index_active_dataleft)) * dst_negative_scale_active_dataleftlookup)) /\ exists ff_q_pvs_active_dataleftlookupnegative. dst_negative_code_active_dataleftlookup = ff_q_pvs_active_dataleftlookupnegative * S ((S (dc_index_active_dataleft)) * dst_negative_scale_active_dataleftlookup) + (dst_negative_active_dataleftlookup))) /\ (exists ge_balance_positive_active_dataleftlookupvalue ge_balance_negative_active_dataleftlookupvalue. (((((dc_value_active_dataleft) = 2 * (ge_balance_positive_active_dataleftlookupvalue) /\ (ge_balance_negative_active_dataleftlookupvalue) = 0) \/ exists ge_signed_half_active_dataleftlookupvaluedecode. (((dc_value_active_dataleft) = 2 * ge_signed_half_active_dataleftlookupvaluedecode + 1 /\ (ge_balance_positive_active_dataleftlookupvalue) = 0) /\ (ge_balance_negative_active_dataleftlookupvalue) = S ge_signed_half_active_dataleftlookupvaluedecode))) /\ ((dst_positive_active_dataleftlookup) + ge_balance_negative_active_dataleftlookupvalue = (dst_negative_active_dataleftlookup) + ge_balance_positive_active_dataleftlookupvalue))))))))) -> ((((~((dc_index_active_dataleft)=0)) /\ (exists dc_quotient_active_dataleftentry dc_left_active_dataleftentry dc_right_active_dataleftentry. (((m)=(dc_index_active_dataleft)*dc_quotient_active_dataleftentry) /\ (((exists dst_positive_code_active_dataleftentryleft dst_positive_scale_active_dataleftentryleft dst_negative_code_active_dataleftentryleft dst_negative_scale_active_dataleftentryleft dst_positive_active_dataleftentryleft dst_negative_active_dataleftentryleft. (((F) = (((((dst_positive_code_active_dataleftentryleft) + (dst_positive_scale_active_dataleftentryleft)) * S ((dst_positive_code_active_dataleftentryleft) + (dst_positive_scale_active_dataleftentryleft)) + ((dst_positive_scale_active_dataleftentryleft) + (dst_positive_scale_active_dataleftentryleft))) + (((dst_negative_code_active_dataleftentryleft) + (dst_negative_scale_active_dataleftentryleft)) * S ((dst_negative_code_active_dataleftentryleft) + (dst_negative_scale_active_dataleftentryleft)) + ((dst_negative_scale_active_dataleftentryleft) + (dst_negative_scale_active_dataleftentryleft)))) * S ((((dst_positive_code_active_dataleftentryleft) + (dst_positive_scale_active_dataleftentryleft)) * S ((dst_positive_code_active_dataleftentryleft) + (dst_positive_scale_active_dataleftentryleft)) + ((dst_positive_scale_active_dataleftentryleft) + (dst_positive_scale_active_dataleftentryleft))) + (((dst_negative_code_active_dataleftentryleft) + (dst_negative_scale_active_dataleftentryleft)) * S ((dst_negative_code_active_dataleftentryleft) + (dst_negative_scale_active_dataleftentryleft)) + ((dst_negative_scale_active_dataleftentryleft) + (dst_negative_scale_active_dataleftentryleft)))) + ((((dst_negative_code_active_dataleftentryleft) + (dst_negative_scale_active_dataleftentryleft)) * S ((dst_negative_code_active_dataleftentryleft) + (dst_negative_scale_active_dataleftentryleft)) + ((dst_negative_scale_active_dataleftentryleft) + (dst_negative_scale_active_dataleftentryleft))) + (((dst_negative_code_active_dataleftentryleft) + (dst_negative_scale_active_dataleftentryleft)) * S ((dst_negative_code_active_dataleftentryleft) + (dst_negative_scale_active_dataleftentryleft)) + ((dst_negative_scale_active_dataleftentryleft) + (dst_negative_scale_active_dataleftentryleft)))))) /\ (((((exists ff_h_pvs_active_dataleftentryleftpositive. ff_h_pvs_active_dataleftentryleftpositive + S (dst_positive_active_dataleftentryleft) = S ((S (dc_index_active_dataleft)) * dst_positive_scale_active_dataleftentryleft)) /\ exists ff_q_pvs_active_dataleftentryleftpositive. dst_positive_code_active_dataleftentryleft = ff_q_pvs_active_dataleftentryleftpositive * S ((S (dc_index_active_dataleft)) * dst_positive_scale_active_dataleftentryleft) + (dst_positive_active_dataleftentryleft))) /\ (((((exists ff_h_pvs_active_dataleftentryleftnegative. ff_h_pvs_active_dataleftentryleftnegative + S (dst_negative_active_dataleftentryleft) = S ((S (dc_index_active_dataleft)) * dst_negative_scale_active_dataleftentryleft)) /\ exists ff_q_pvs_active_dataleftentryleftnegative. dst_negative_code_active_dataleftentryleft = ff_q_pvs_active_dataleftentryleftnegative * S ((S (dc_index_active_dataleft)) * dst_negative_scale_active_dataleftentryleft) + (dst_negative_active_dataleftentryleft))) /\ (exists ge_balance_positive_active_dataleftentryleftvalue ge_balance_negative_active_dataleftentryleftvalue. (((((dc_left_active_dataleftentry) = 2 * (ge_balance_positive_active_dataleftentryleftvalue) /\ (ge_balance_negative_active_dataleftentryleftvalue) = 0) \/ exists ge_signed_half_active_dataleftentryleftvaluedecode. (((dc_left_active_dataleftentry) = 2 * ge_signed_half_active_dataleftentryleftvaluedecode + 1 /\ (ge_balance_positive_active_dataleftentryleftvalue) = 0) /\ (ge_balance_negative_active_dataleftentryleftvalue) = S ge_signed_half_active_dataleftentryleftvaluedecode))) /\ ((dst_positive_active_dataleftentryleft) + ge_balance_negative_active_dataleftentryleftvalue = (dst_negative_active_dataleftentryleft) + ge_balance_positive_active_dataleftentryleftvalue))))))))) /\ (((exists dst_positive_code_active_dataleftentryright dst_positive_scale_active_dataleftentryright dst_negative_code_active_dataleftentryright dst_negative_scale_active_dataleftentryright dst_positive_active_dataleftentryright dst_negative_active_dataleftentryright. (((G) = (((((dst_positive_code_active_dataleftentryright) + (dst_positive_scale_active_dataleftentryright)) * S ((dst_positive_code_active_dataleftentryright) + (dst_positive_scale_active_dataleftentryright)) + ((dst_positive_scale_active_dataleftentryright) + (dst_positive_scale_active_dataleftentryright))) + (((dst_negative_code_active_dataleftentryright) + (dst_negative_scale_active_dataleftentryright)) * S ((dst_negative_code_active_dataleftentryright) + (dst_negative_scale_active_dataleftentryright)) + ((dst_negative_scale_active_dataleftentryright) + (dst_negative_scale_active_dataleftentryright)))) * S ((((dst_positive_code_active_dataleftentryright) + (dst_positive_scale_active_dataleftentryright)) * S ((dst_positive_code_active_dataleftentryright) + (dst_positive_scale_active_dataleftentryright)) + ((dst_positive_scale_active_dataleftentryright) + (dst_positive_scale_active_dataleftentryright))) + (((dst_negative_code_active_dataleftentryright) + (dst_negative_scale_active_dataleftentryright)) * S ((dst_negative_code_active_dataleftentryright) + (dst_negative_scale_active_dataleftentryright)) + ((dst_negative_scale_active_dataleftentryright) + (dst_negative_scale_active_dataleftentryright)))) + ((((dst_negative_code_active_dataleftentryright) + (dst_negative_scale_active_dataleftentryright)) * S ((dst_negative_code_active_dataleftentryright) + (dst_negative_scale_active_dataleftentryright)) + ((dst_negative_scale_active_dataleftentryright) + (dst_negative_scale_active_dataleftentryright))) + (((dst_negative_code_active_dataleftentryright) + (dst_negative_scale_active_dataleftentryright)) * S ((dst_negative_code_active_dataleftentryright) + (dst_negative_scale_active_dataleftentryright)) + ((dst_negative_scale_active_dataleftentryright) + (dst_negative_scale_active_dataleftentryright)))))) /\ (((((exists ff_h_pvs_active_dataleftentryrightpositive. ff_h_pvs_active_dataleftentryrightpositive + S (dst_positive_active_dataleftentryright) = S ((S (dc_quotient_active_dataleftentry)) * dst_positive_scale_active_dataleftentryright)) /\ exists ff_q_pvs_active_dataleftentryrightpositive. dst_positive_code_active_dataleftentryright = ff_q_pvs_active_dataleftentryrightpositive * S ((S (dc_quotient_active_dataleftentry)) * dst_positive_scale_active_dataleftentryright) + (dst_positive_active_dataleftentryright))) /\ (((((exists ff_h_pvs_active_dataleftentryrightnegative. ff_h_pvs_active_dataleftentryrightnegative + S (dst_negative_active_dataleftentryright) = S ((S (dc_quotient_active_dataleftentry)) * dst_negative_scale_active_dataleftentryright)) /\ exists ff_q_pvs_active_dataleftentryrightnegative. dst_negative_code_active_dataleftentryright = ff_q_pvs_active_dataleftentryrightnegative * S ((S (dc_quotient_active_dataleftentry)) * dst_negative_scale_active_dataleftentryright) + (dst_negative_active_dataleftentryright))) /\ (exists ge_balance_positive_active_dataleftentryrightvalue ge_balance_negative_active_dataleftentryrightvalue. (((((dc_right_active_dataleftentry) = 2 * (ge_balance_positive_active_dataleftentryrightvalue) /\ (ge_balance_negative_active_dataleftentryrightvalue) = 0) \/ exists ge_signed_half_active_dataleftentryrightvaluedecode. (((dc_right_active_dataleftentry) = 2 * ge_signed_half_active_dataleftentryrightvaluedecode + 1 /\ (ge_balance_positive_active_dataleftentryrightvalue) = 0) /\ (ge_balance_negative_active_dataleftentryrightvalue) = S ge_signed_half_active_dataleftentryrightvaluedecode))) /\ ((dst_positive_active_dataleftentryright) + ge_balance_negative_active_dataleftentryrightvalue = (dst_negative_active_dataleftentryright) + ge_balance_positive_active_dataleftentryrightvalue))))))))) /\ (exists sto_ap_active_dataleftentryproduct sto_an_active_dataleftentryproduct sto_bp_active_dataleftentryproduct sto_bn_active_dataleftentryproduct sto_cp_active_dataleftentryproduct sto_cn_active_dataleftentryproduct. (((((dc_left_active_dataleftentry) = 2 * (sto_ap_active_dataleftentryproduct) /\ (sto_an_active_dataleftentryproduct) = 0) \/ exists ge_signed_half_active_dataleftentryproductleft. (((dc_left_active_dataleftentry) = 2 * ge_signed_half_active_dataleftentryproductleft + 1 /\ (sto_ap_active_dataleftentryproduct) = 0) /\ (sto_an_active_dataleftentryproduct) = S ge_signed_half_active_dataleftentryproductleft))) /\ ((((((dc_right_active_dataleftentry) = 2 * (sto_bp_active_dataleftentryproduct) /\ (sto_bn_active_dataleftentryproduct) = 0) \/ exists ge_signed_half_active_dataleftentryproductright. (((dc_right_active_dataleftentry) = 2 * ge_signed_half_active_dataleftentryproductright + 1 /\ (sto_bp_active_dataleftentryproduct) = 0) /\ (sto_bn_active_dataleftentryproduct) = S ge_signed_half_active_dataleftentryproductright))) /\ ((((((dc_value_active_dataleft) = 2 * (sto_cp_active_dataleftentryproduct) /\ (sto_cn_active_dataleftentryproduct) = 0) \/ exists ge_signed_half_active_dataleftentryproductoutput. (((dc_value_active_dataleft) = 2 * ge_signed_half_active_dataleftentryproductoutput + 1 /\ (sto_cp_active_dataleftentryproduct) = 0) /\ (sto_cn_active_dataleftentryproduct) = S ge_signed_half_active_dataleftentryproductoutput))) /\ ((sto_ap_active_dataleftentryproduct * sto_bp_active_dataleftentryproduct + sto_an_active_dataleftentryproduct * sto_bn_active_dataleftentryproduct) + sto_cn_active_dataleftentryproduct = (sto_ap_active_dataleftentryproduct * sto_bn_active_dataleftentryproduct + sto_an_active_dataleftentryproduct * sto_bp_active_dataleftentryproduct) + sto_cp_active_dataleftentryproduct))))))))))))))) \/ ((((dc_index_active_dataleft)=0 \/ ~(exists pvs_factor_active_dataleftentrynondivisor. (m) = (dc_index_active_dataleft) * pvs_factor_active_dataleftentrynondivisor)) /\ ((dc_value_active_dataleft)=0))))))) /\ (((((exists dst_positive_code_active_datarighttable dst_positive_scale_active_datarighttable dst_negative_code_active_datarighttable dst_negative_scale_active_datarighttable. (((B) = (((((dst_positive_code_active_datarighttable) + (dst_positive_scale_active_datarighttable)) * S ((dst_positive_code_active_datarighttable) + (dst_positive_scale_active_datarighttable)) + ((dst_positive_scale_active_datarighttable) + (dst_positive_scale_active_datarighttable))) + (((dst_negative_code_active_datarighttable) + (dst_negative_scale_active_datarighttable)) * S ((dst_negative_code_active_datarighttable) + (dst_negative_scale_active_datarighttable)) + ((dst_negative_scale_active_datarighttable) + (dst_negative_scale_active_datarighttable)))) * S ((((dst_positive_code_active_datarighttable) + (dst_positive_scale_active_datarighttable)) * S ((dst_positive_code_active_datarighttable) + (dst_positive_scale_active_datarighttable)) + ((dst_positive_scale_active_datarighttable) + (dst_positive_scale_active_datarighttable))) + (((dst_negative_code_active_datarighttable) + (dst_negative_scale_active_datarighttable)) * S ((dst_negative_code_active_datarighttable) + (dst_negative_scale_active_datarighttable)) + ((dst_negative_scale_active_datarighttable) + (dst_negative_scale_active_datarighttable)))) + ((((dst_negative_code_active_datarighttable) + (dst_negative_scale_active_datarighttable)) * S ((dst_negative_code_active_datarighttable) + (dst_negative_scale_active_datarighttable)) + ((dst_negative_scale_active_datarighttable) + (dst_negative_scale_active_datarighttable))) + (((dst_negative_code_active_datarighttable) + (dst_negative_scale_active_datarighttable)) * S ((dst_negative_code_active_datarighttable) + (dst_negative_scale_active_datarighttable)) + ((dst_negative_scale_active_datarighttable) + (dst_negative_scale_active_datarighttable)))))) /\ (forall dst_index_active_datarighttable. (exists pvs_le_gap_active_datarighttabledomain. pvs_le_gap_active_datarighttabledomain + (dst_index_active_datarighttable) = (n)) -> exists dst_positive_active_datarighttable dst_negative_active_datarighttable dst_value_active_datarighttable. ((((exists ff_h_pvs_active_datarighttableentrypositive. ff_h_pvs_active_datarighttableentrypositive + S (dst_positive_active_datarighttable) = S ((S (dst_index_active_datarighttable)) * dst_positive_scale_active_datarighttable)) /\ exists ff_q_pvs_active_datarighttableentrypositive. dst_positive_code_active_datarighttable = ff_q_pvs_active_datarighttableentrypositive * S ((S (dst_index_active_datarighttable)) * dst_positive_scale_active_datarighttable) + (dst_positive_active_datarighttable))) /\ (((((exists ff_h_pvs_active_datarighttableentrynegative. ff_h_pvs_active_datarighttableentrynegative + S (dst_negative_active_datarighttable) = S ((S (dst_index_active_datarighttable)) * dst_negative_scale_active_datarighttable)) /\ exists ff_q_pvs_active_datarighttableentrynegative. dst_negative_code_active_datarighttable = ff_q_pvs_active_datarighttableentrynegative * S ((S (dst_index_active_datarighttable)) * dst_negative_scale_active_datarighttable) + (dst_negative_active_datarighttable))) /\ (exists ge_balance_positive_active_datarighttableentryvalue ge_balance_negative_active_datarighttableentryvalue. (((((dst_value_active_datarighttable) = 2 * (ge_balance_positive_active_datarighttableentryvalue) /\ (ge_balance_negative_active_datarighttableentryvalue) = 0) \/ exists ge_signed_half_active_datarighttableentryvaluedecode. (((dst_value_active_datarighttable) = 2 * ge_signed_half_active_datarighttableentryvaluedecode + 1 /\ (ge_balance_positive_active_datarighttableentryvalue) = 0) /\ (ge_balance_negative_active_datarighttableentryvalue) = S ge_signed_half_active_datarighttableentryvaluedecode))) /\ ((dst_positive_active_datarighttable) + ge_balance_negative_active_datarighttableentryvalue = (dst_negative_active_datarighttable) + ge_balance_positive_active_datarighttableentryvalue))))))))) /\ (forall dc_index_active_dataright dc_value_active_dataright. (exists pvs_le_gap_active_datarightdomain. pvs_le_gap_active_datarightdomain + (dc_index_active_dataright) = (n)) -> (exists dst_positive_code_active_datarightlookup dst_positive_scale_active_datarightlookup dst_negative_code_active_datarightlookup dst_negative_scale_active_datarightlookup dst_positive_active_datarightlookup dst_negative_active_datarightlookup. (((B) = (((((dst_positive_code_active_datarightlookup) + (dst_positive_scale_active_datarightlookup)) * S ((dst_positive_code_active_datarightlookup) + (dst_positive_scale_active_datarightlookup)) + ((dst_positive_scale_active_datarightlookup) + (dst_positive_scale_active_datarightlookup))) + (((dst_negative_code_active_datarightlookup) + (dst_negative_scale_active_datarightlookup)) * S ((dst_negative_code_active_datarightlookup) + (dst_negative_scale_active_datarightlookup)) + ((dst_negative_scale_active_datarightlookup) + (dst_negative_scale_active_datarightlookup)))) * S ((((dst_positive_code_active_datarightlookup) + (dst_positive_scale_active_datarightlookup)) * S ((dst_positive_code_active_datarightlookup) + (dst_positive_scale_active_datarightlookup)) + ((dst_positive_scale_active_datarightlookup) + (dst_positive_scale_active_datarightlookup))) + (((dst_negative_code_active_datarightlookup) + (dst_negative_scale_active_datarightlookup)) * S ((dst_negative_code_active_datarightlookup) + (dst_negative_scale_active_datarightlookup)) + ((dst_negative_scale_active_datarightlookup) + (dst_negative_scale_active_datarightlookup)))) + ((((dst_negative_code_active_datarightlookup) + (dst_negative_scale_active_datarightlookup)) * S ((dst_negative_code_active_datarightlookup) + (dst_negative_scale_active_datarightlookup)) + ((dst_negative_scale_active_datarightlookup) + (dst_negative_scale_active_datarightlookup))) + (((dst_negative_code_active_datarightlookup) + (dst_negative_scale_active_datarightlookup)) * S ((dst_negative_code_active_datarightlookup) + (dst_negative_scale_active_datarightlookup)) + ((dst_negative_scale_active_datarightlookup) + (dst_negative_scale_active_datarightlookup)))))) /\ (((((exists ff_h_pvs_active_datarightlookuppositive. ff_h_pvs_active_datarightlookuppositive + S (dst_positive_active_datarightlookup) = S ((S (dc_index_active_dataright)) * dst_positive_scale_active_datarightlookup)) /\ exists ff_q_pvs_active_datarightlookuppositive. dst_positive_code_active_datarightlookup = ff_q_pvs_active_datarightlookuppositive * S ((S (dc_index_active_dataright)) * dst_positive_scale_active_datarightlookup) + (dst_positive_active_datarightlookup))) /\ (((((exists ff_h_pvs_active_datarightlookupnegative. ff_h_pvs_active_datarightlookupnegative + S (dst_negative_active_datarightlookup) = S ((S (dc_index_active_dataright)) * dst_negative_scale_active_datarightlookup)) /\ exists ff_q_pvs_active_datarightlookupnegative. dst_negative_code_active_datarightlookup = ff_q_pvs_active_datarightlookupnegative * S ((S (dc_index_active_dataright)) * dst_negative_scale_active_datarightlookup) + (dst_negative_active_datarightlookup))) /\ (exists ge_balance_positive_active_datarightlookupvalue ge_balance_negative_active_datarightlookupvalue. (((((dc_value_active_dataright) = 2 * (ge_balance_positive_active_datarightlookupvalue) /\ (ge_balance_negative_active_datarightlookupvalue) = 0) \/ exists ge_signed_half_active_datarightlookupvaluedecode. (((dc_value_active_dataright) = 2 * ge_signed_half_active_datarightlookupvaluedecode + 1 /\ (ge_balance_positive_active_datarightlookupvalue) = 0) /\ (ge_balance_negative_active_datarightlookupvalue) = S ge_signed_half_active_datarightlookupvaluedecode))) /\ ((dst_positive_active_datarightlookup) + ge_balance_negative_active_datarightlookupvalue = (dst_negative_active_datarightlookup) + ge_balance_positive_active_datarightlookupvalue))))))))) -> ((((~((dc_index_active_dataright)=0)) /\ (exists dc_quotient_active_datarightentry dc_left_active_datarightentry dc_right_active_datarightentry. (((n)=(dc_index_active_dataright)*dc_quotient_active_datarightentry) /\ (((exists dst_positive_code_active_datarightentryleft dst_positive_scale_active_datarightentryleft dst_negative_code_active_datarightentryleft dst_negative_scale_active_datarightentryleft dst_positive_active_datarightentryleft dst_negative_active_datarightentryleft. (((F) = (((((dst_positive_code_active_datarightentryleft) + (dst_positive_scale_active_datarightentryleft)) * S ((dst_positive_code_active_datarightentryleft) + (dst_positive_scale_active_datarightentryleft)) + ((dst_positive_scale_active_datarightentryleft) + (dst_positive_scale_active_datarightentryleft))) + (((dst_negative_code_active_datarightentryleft) + (dst_negative_scale_active_datarightentryleft)) * S ((dst_negative_code_active_datarightentryleft) + (dst_negative_scale_active_datarightentryleft)) + ((dst_negative_scale_active_datarightentryleft) + (dst_negative_scale_active_datarightentryleft)))) * S ((((dst_positive_code_active_datarightentryleft) + (dst_positive_scale_active_datarightentryleft)) * S ((dst_positive_code_active_datarightentryleft) + (dst_positive_scale_active_datarightentryleft)) + ((dst_positive_scale_active_datarightentryleft) + (dst_positive_scale_active_datarightentryleft))) + (((dst_negative_code_active_datarightentryleft) + (dst_negative_scale_active_datarightentryleft)) * S ((dst_negative_code_active_datarightentryleft) + (dst_negative_scale_active_datarightentryleft)) + ((dst_negative_scale_active_datarightentryleft) + (dst_negative_scale_active_datarightentryleft)))) + ((((dst_negative_code_active_datarightentryleft) + (dst_negative_scale_active_datarightentryleft)) * S ((dst_negative_code_active_datarightentryleft) + (dst_negative_scale_active_datarightentryleft)) + ((dst_negative_scale_active_datarightentryleft) + (dst_negative_scale_active_datarightentryleft))) + (((dst_negative_code_active_datarightentryleft) + (dst_negative_scale_active_datarightentryleft)) * S ((dst_negative_code_active_datarightentryleft) + (dst_negative_scale_active_datarightentryleft)) + ((dst_negative_scale_active_datarightentryleft) + (dst_negative_scale_active_datarightentryleft)))))) /\ (((((exists ff_h_pvs_active_datarightentryleftpositive. ff_h_pvs_active_datarightentryleftpositive + S (dst_positive_active_datarightentryleft) = S ((S (dc_index_active_dataright)) * dst_positive_scale_active_datarightentryleft)) /\ exists ff_q_pvs_active_datarightentryleftpositive. dst_positive_code_active_datarightentryleft = ff_q_pvs_active_datarightentryleftpositive * S ((S (dc_index_active_dataright)) * dst_positive_scale_active_datarightentryleft) + (dst_positive_active_datarightentryleft))) /\ (((((exists ff_h_pvs_active_datarightentryleftnegative. ff_h_pvs_active_datarightentryleftnegative + S (dst_negative_active_datarightentryleft) = S ((S (dc_index_active_dataright)) * dst_negative_scale_active_datarightentryleft)) /\ exists ff_q_pvs_active_datarightentryleftnegative. dst_negative_code_active_datarightentryleft = ff_q_pvs_active_datarightentryleftnegative * S ((S (dc_index_active_dataright)) * dst_negative_scale_active_datarightentryleft) + (dst_negative_active_datarightentryleft))) /\ (exists ge_balance_positive_active_datarightentryleftvalue ge_balance_negative_active_datarightentryleftvalue. (((((dc_left_active_datarightentry) = 2 * (ge_balance_positive_active_datarightentryleftvalue) /\ (ge_balance_negative_active_datarightentryleftvalue) = 0) \/ exists ge_signed_half_active_datarightentryleftvaluedecode. (((dc_left_active_datarightentry) = 2 * ge_signed_half_active_datarightentryleftvaluedecode + 1 /\ (ge_balance_positive_active_datarightentryleftvalue) = 0) /\ (ge_balance_negative_active_datarightentryleftvalue) = S ge_signed_half_active_datarightentryleftvaluedecode))) /\ ((dst_positive_active_datarightentryleft) + ge_balance_negative_active_datarightentryleftvalue = (dst_negative_active_datarightentryleft) + ge_balance_positive_active_datarightentryleftvalue))))))))) /\ (((exists dst_positive_code_active_datarightentryright dst_positive_scale_active_datarightentryright dst_negative_code_active_datarightentryright dst_negative_scale_active_datarightentryright dst_positive_active_datarightentryright dst_negative_active_datarightentryright. (((G) = (((((dst_positive_code_active_datarightentryright) + (dst_positive_scale_active_datarightentryright)) * S ((dst_positive_code_active_datarightentryright) + (dst_positive_scale_active_datarightentryright)) + ((dst_positive_scale_active_datarightentryright) + (dst_positive_scale_active_datarightentryright))) + (((dst_negative_code_active_datarightentryright) + (dst_negative_scale_active_datarightentryright)) * S ((dst_negative_code_active_datarightentryright) + (dst_negative_scale_active_datarightentryright)) + ((dst_negative_scale_active_datarightentryright) + (dst_negative_scale_active_datarightentryright)))) * S ((((dst_positive_code_active_datarightentryright) + (dst_positive_scale_active_datarightentryright)) * S ((dst_positive_code_active_datarightentryright) + (dst_positive_scale_active_datarightentryright)) + ((dst_positive_scale_active_datarightentryright) + (dst_positive_scale_active_datarightentryright))) + (((dst_negative_code_active_datarightentryright) + (dst_negative_scale_active_datarightentryright)) * S ((dst_negative_code_active_datarightentryright) + (dst_negative_scale_active_datarightentryright)) + ((dst_negative_scale_active_datarightentryright) + (dst_negative_scale_active_datarightentryright)))) + ((((dst_negative_code_active_datarightentryright) + (dst_negative_scale_active_datarightentryright)) * S ((dst_negative_code_active_datarightentryright) + (dst_negative_scale_active_datarightentryright)) + ((dst_negative_scale_active_datarightentryright) + (dst_negative_scale_active_datarightentryright))) + (((dst_negative_code_active_datarightentryright) + (dst_negative_scale_active_datarightentryright)) * S ((dst_negative_code_active_datarightentryright) + (dst_negative_scale_active_datarightentryright)) + ((dst_negative_scale_active_datarightentryright) + (dst_negative_scale_active_datarightentryright)))))) /\ (((((exists ff_h_pvs_active_datarightentryrightpositive. ff_h_pvs_active_datarightentryrightpositive + S (dst_positive_active_datarightentryright) = S ((S (dc_quotient_active_datarightentry)) * dst_positive_scale_active_datarightentryright)) /\ exists ff_q_pvs_active_datarightentryrightpositive. dst_positive_code_active_datarightentryright = ff_q_pvs_active_datarightentryrightpositive * S ((S (dc_quotient_active_datarightentry)) * dst_positive_scale_active_datarightentryright) + (dst_positive_active_datarightentryright))) /\ (((((exists ff_h_pvs_active_datarightentryrightnegative. ff_h_pvs_active_datarightentryrightnegative + S (dst_negative_active_datarightentryright) = S ((S (dc_quotient_active_datarightentry)) * dst_negative_scale_active_datarightentryright)) /\ exists ff_q_pvs_active_datarightentryrightnegative. dst_negative_code_active_datarightentryright = ff_q_pvs_active_datarightentryrightnegative * S ((S (dc_quotient_active_datarightentry)) * dst_negative_scale_active_datarightentryright) + (dst_negative_active_datarightentryright))) /\ (exists ge_balance_positive_active_datarightentryrightvalue ge_balance_negative_active_datarightentryrightvalue. (((((dc_right_active_datarightentry) = 2 * (ge_balance_positive_active_datarightentryrightvalue) /\ (ge_balance_negative_active_datarightentryrightvalue) = 0) \/ exists ge_signed_half_active_datarightentryrightvaluedecode. (((dc_right_active_datarightentry) = 2 * ge_signed_half_active_datarightentryrightvaluedecode + 1 /\ (ge_balance_positive_active_datarightentryrightvalue) = 0) /\ (ge_balance_negative_active_datarightentryrightvalue) = S ge_signed_half_active_datarightentryrightvaluedecode))) /\ ((dst_positive_active_datarightentryright) + ge_balance_negative_active_datarightentryrightvalue = (dst_negative_active_datarightentryright) + ge_balance_positive_active_datarightentryrightvalue))))))))) /\ (exists sto_ap_active_datarightentryproduct sto_an_active_datarightentryproduct sto_bp_active_datarightentryproduct sto_bn_active_datarightentryproduct sto_cp_active_datarightentryproduct sto_cn_active_datarightentryproduct. (((((dc_left_active_datarightentry) = 2 * (sto_ap_active_datarightentryproduct) /\ (sto_an_active_datarightentryproduct) = 0) \/ exists ge_signed_half_active_datarightentryproductleft. (((dc_left_active_datarightentry) = 2 * ge_signed_half_active_datarightentryproductleft + 1 /\ (sto_ap_active_datarightentryproduct) = 0) /\ (sto_an_active_datarightentryproduct) = S ge_signed_half_active_datarightentryproductleft))) /\ ((((((dc_right_active_datarightentry) = 2 * (sto_bp_active_datarightentryproduct) /\ (sto_bn_active_datarightentryproduct) = 0) \/ exists ge_signed_half_active_datarightentryproductright. (((dc_right_active_datarightentry) = 2 * ge_signed_half_active_datarightentryproductright + 1 /\ (sto_bp_active_datarightentryproduct) = 0) /\ (sto_bn_active_datarightentryproduct) = S ge_signed_half_active_datarightentryproductright))) /\ ((((((dc_value_active_dataright) = 2 * (sto_cp_active_datarightentryproduct) /\ (sto_cn_active_datarightentryproduct) = 0) \/ exists ge_signed_half_active_datarightentryproductoutput. (((dc_value_active_dataright) = 2 * ge_signed_half_active_datarightentryproductoutput + 1 /\ (sto_cp_active_datarightentryproduct) = 0) /\ (sto_cn_active_datarightentryproduct) = S ge_signed_half_active_datarightentryproductoutput))) /\ ((sto_ap_active_datarightentryproduct * sto_bp_active_datarightentryproduct + sto_an_active_datarightentryproduct * sto_bn_active_datarightentryproduct) + sto_cn_active_datarightentryproduct = (sto_ap_active_datarightentryproduct * sto_bn_active_datarightentryproduct + sto_an_active_datarightentryproduct * sto_bp_active_datarightentryproduct) + sto_cp_active_datarightentryproduct))))))))))))))) \/ ((((dc_index_active_dataright)=0 \/ ~(exists pvs_factor_active_datarightentrynondivisor. (n) = (dc_index_active_dataright) * pvs_factor_active_datarightentrynondivisor)) /\ ((dc_value_active_dataright)=0))))))) /\ (((((exists dst_positive_code_active_datacartesianF dst_positive_scale_active_datacartesianF dst_negative_code_active_datacartesianF dst_negative_scale_active_datacartesianF. (((A) = (((((dst_positive_code_active_datacartesianF) + (dst_positive_scale_active_datacartesianF)) * S ((dst_positive_code_active_datacartesianF) + (dst_positive_scale_active_datacartesianF)) + ((dst_positive_scale_active_datacartesianF) + (dst_positive_scale_active_datacartesianF))) + (((dst_negative_code_active_datacartesianF) + (dst_negative_scale_active_datacartesianF)) * S ((dst_negative_code_active_datacartesianF) + (dst_negative_scale_active_datacartesianF)) + ((dst_negative_scale_active_datacartesianF) + (dst_negative_scale_active_datacartesianF)))) * S ((((dst_positive_code_active_datacartesianF) + (dst_positive_scale_active_datacartesianF)) * S ((dst_positive_code_active_datacartesianF) + (dst_positive_scale_active_datacartesianF)) + ((dst_positive_scale_active_datacartesianF) + (dst_positive_scale_active_datacartesianF))) + (((dst_negative_code_active_datacartesianF) + (dst_negative_scale_active_datacartesianF)) * S ((dst_negative_code_active_datacartesianF) + (dst_negative_scale_active_datacartesianF)) + ((dst_negative_scale_active_datacartesianF) + (dst_negative_scale_active_datacartesianF)))) + ((((dst_negative_code_active_datacartesianF) + (dst_negative_scale_active_datacartesianF)) * S ((dst_negative_code_active_datacartesianF) + (dst_negative_scale_active_datacartesianF)) + ((dst_negative_scale_active_datacartesianF) + (dst_negative_scale_active_datacartesianF))) + (((dst_negative_code_active_datacartesianF) + (dst_negative_scale_active_datacartesianF)) * S ((dst_negative_code_active_datacartesianF) + (dst_negative_scale_active_datacartesianF)) + ((dst_negative_scale_active_datacartesianF) + (dst_negative_scale_active_datacartesianF)))))) /\ (forall dst_index_active_datacartesianF. (exists pvs_le_gap_active_datacartesianFdomain. pvs_le_gap_active_datacartesianFdomain + (dst_index_active_datacartesianF) = (0)) -> exists dst_positive_active_datacartesianF dst_negative_active_datacartesianF dst_value_active_datacartesianF. ((((exists ff_h_pvs_active_datacartesianFentrypositive. ff_h_pvs_active_datacartesianFentrypositive + S (dst_positive_active_datacartesianF) = S ((S (dst_index_active_datacartesianF)) * dst_positive_scale_active_datacartesianF)) /\ exists ff_q_pvs_active_datacartesianFentrypositive. dst_positive_code_active_datacartesianF = ff_q_pvs_active_datacartesianFentrypositive * S ((S (dst_index_active_datacartesianF)) * dst_positive_scale_active_datacartesianF) + (dst_positive_active_datacartesianF))) /\ (((((exists ff_h_pvs_active_datacartesianFentrynegative. ff_h_pvs_active_datacartesianFentrynegative + S (dst_negative_active_datacartesianF) = S ((S (dst_index_active_datacartesianF)) * dst_negative_scale_active_datacartesianF)) /\ exists ff_q_pvs_active_datacartesianFentrynegative. dst_negative_code_active_datacartesianF = ff_q_pvs_active_datacartesianFentrynegative * S ((S (dst_index_active_datacartesianF)) * dst_negative_scale_active_datacartesianF) + (dst_negative_active_datacartesianF))) /\ (exists ge_balance_positive_active_datacartesianFentryvalue ge_balance_negative_active_datacartesianFentryvalue. (((((dst_value_active_datacartesianF) = 2 * (ge_balance_positive_active_datacartesianFentryvalue) /\ (ge_balance_negative_active_datacartesianFentryvalue) = 0) \/ exists ge_signed_half_active_datacartesianFentryvaluedecode. (((dst_value_active_datacartesianF) = 2 * ge_signed_half_active_datacartesianFentryvaluedecode + 1 /\ (ge_balance_positive_active_datacartesianFentryvalue) = 0) /\ (ge_balance_negative_active_datacartesianFentryvalue) = S ge_signed_half_active_datacartesianFentryvaluedecode))) /\ ((dst_positive_active_datacartesianF) + ge_balance_negative_active_datacartesianFentryvalue = (dst_negative_active_datacartesianF) + ge_balance_positive_active_datacartesianFentryvalue))))))))) /\ (((exists dst_positive_code_active_datacartesianG dst_positive_scale_active_datacartesianG dst_negative_code_active_datacartesianG dst_negative_scale_active_datacartesianG. (((B) = (((((dst_positive_code_active_datacartesianG) + (dst_positive_scale_active_datacartesianG)) * S ((dst_positive_code_active_datacartesianG) + (dst_positive_scale_active_datacartesianG)) + ((dst_positive_scale_active_datacartesianG) + (dst_positive_scale_active_datacartesianG))) + (((dst_negative_code_active_datacartesianG) + (dst_negative_scale_active_datacartesianG)) * S ((dst_negative_code_active_datacartesianG) + (dst_negative_scale_active_datacartesianG)) + ((dst_negative_scale_active_datacartesianG) + (dst_negative_scale_active_datacartesianG)))) * S ((((dst_positive_code_active_datacartesianG) + (dst_positive_scale_active_datacartesianG)) * S ((dst_positive_code_active_datacartesianG) + (dst_positive_scale_active_datacartesianG)) + ((dst_positive_scale_active_datacartesianG) + (dst_positive_scale_active_datacartesianG))) + (((dst_negative_code_active_datacartesianG) + (dst_negative_scale_active_datacartesianG)) * S ((dst_negative_code_active_datacartesianG) + (dst_negative_scale_active_datacartesianG)) + ((dst_negative_scale_active_datacartesianG) + (dst_negative_scale_active_datacartesianG)))) + ((((dst_negative_code_active_datacartesianG) + (dst_negative_scale_active_datacartesianG)) * S ((dst_negative_code_active_datacartesianG) + (dst_negative_scale_active_datacartesianG)) + ((dst_negative_scale_active_datacartesianG) + (dst_negative_scale_active_datacartesianG))) + (((dst_negative_code_active_datacartesianG) + (dst_negative_scale_active_datacartesianG)) * S ((dst_negative_code_active_datacartesianG) + (dst_negative_scale_active_datacartesianG)) + ((dst_negative_scale_active_datacartesianG) + (dst_negative_scale_active_datacartesianG)))))) /\ (forall dst_index_active_datacartesianG. (exists pvs_le_gap_active_datacartesianGdomain. pvs_le_gap_active_datacartesianGdomain + (dst_index_active_datacartesianG) = (0)) -> exists dst_positive_active_datacartesianG dst_negative_active_datacartesianG dst_value_active_datacartesianG. ((((exists ff_h_pvs_active_datacartesianGentrypositive. ff_h_pvs_active_datacartesianGentrypositive + S (dst_positive_active_datacartesianG) = S ((S (dst_index_active_datacartesianG)) * dst_positive_scale_active_datacartesianG)) /\ exists ff_q_pvs_active_datacartesianGentrypositive. dst_positive_code_active_datacartesianG = ff_q_pvs_active_datacartesianGentrypositive * S ((S (dst_index_active_datacartesianG)) * dst_positive_scale_active_datacartesianG) + (dst_positive_active_datacartesianG))) /\ (((((exists ff_h_pvs_active_datacartesianGentrynegative. ff_h_pvs_active_datacartesianGentrynegative + S (dst_negative_active_datacartesianG) = S ((S (dst_index_active_datacartesianG)) * dst_negative_scale_active_datacartesianG)) /\ exists ff_q_pvs_active_datacartesianGentrynegative. dst_negative_code_active_datacartesianG = ff_q_pvs_active_datacartesianGentrynegative * S ((S (dst_index_active_datacartesianG)) * dst_negative_scale_active_datacartesianG) + (dst_negative_active_datacartesianG))) /\ (exists ge_balance_positive_active_datacartesianGentryvalue ge_balance_negative_active_datacartesianGentryvalue. (((((dst_value_active_datacartesianG) = 2 * (ge_balance_positive_active_datacartesianGentryvalue) /\ (ge_balance_negative_active_datacartesianGentryvalue) = 0) \/ exists ge_signed_half_active_datacartesianGentryvaluedecode. (((dst_value_active_datacartesianG) = 2 * ge_signed_half_active_datacartesianGentryvaluedecode + 1 /\ (ge_balance_positive_active_datacartesianGentryvalue) = 0) /\ (ge_balance_negative_active_datacartesianGentryvalue) = S ge_signed_half_active_datacartesianGentryvaluedecode))) /\ ((dst_positive_active_datacartesianG) + ge_balance_negative_active_datacartesianGentryvalue = (dst_negative_active_datacartesianG) + ge_balance_positive_active_datacartesianGentryvalue))))))))) /\ (((exists dst_positive_code_active_datacartesianT dst_positive_scale_active_datacartesianT dst_negative_code_active_datacartesianT dst_negative_scale_active_datacartesianT. (((T) = (((((dst_positive_code_active_datacartesianT) + (dst_positive_scale_active_datacartesianT)) * S ((dst_positive_code_active_datacartesianT) + (dst_positive_scale_active_datacartesianT)) + ((dst_positive_scale_active_datacartesianT) + (dst_positive_scale_active_datacartesianT))) + (((dst_negative_code_active_datacartesianT) + (dst_negative_scale_active_datacartesianT)) * S ((dst_negative_code_active_datacartesianT) + (dst_negative_scale_active_datacartesianT)) + ((dst_negative_scale_active_datacartesianT) + (dst_negative_scale_active_datacartesianT)))) * S ((((dst_positive_code_active_datacartesianT) + (dst_positive_scale_active_datacartesianT)) * S ((dst_positive_code_active_datacartesianT) + (dst_positive_scale_active_datacartesianT)) + ((dst_positive_scale_active_datacartesianT) + (dst_positive_scale_active_datacartesianT))) + (((dst_negative_code_active_datacartesianT) + (dst_negative_scale_active_datacartesianT)) * S ((dst_negative_code_active_datacartesianT) + (dst_negative_scale_active_datacartesianT)) + ((dst_negative_scale_active_datacartesianT) + (dst_negative_scale_active_datacartesianT)))) + ((((dst_negative_code_active_datacartesianT) + (dst_negative_scale_active_datacartesianT)) * S ((dst_negative_code_active_datacartesianT) + (dst_negative_scale_active_datacartesianT)) + ((dst_negative_scale_active_datacartesianT) + (dst_negative_scale_active_datacartesianT))) + (((dst_negative_code_active_datacartesianT) + (dst_negative_scale_active_datacartesianT)) * S ((dst_negative_code_active_datacartesianT) + (dst_negative_scale_active_datacartesianT)) + ((dst_negative_scale_active_datacartesianT) + (dst_negative_scale_active_datacartesianT)))))) /\ (forall dst_index_active_datacartesianT. (exists pvs_le_gap_active_datacartesianTdomain. pvs_le_gap_active_datacartesianTdomain + (dst_index_active_datacartesianT) = ((S (m))*(S (n)))) -> exists dst_positive_active_datacartesianT dst_negative_active_datacartesianT dst_value_active_datacartesianT. ((((exists ff_h_pvs_active_datacartesianTentrypositive. ff_h_pvs_active_datacartesianTentrypositive + S (dst_positive_active_datacartesianT) = S ((S (dst_index_active_datacartesianT)) * dst_positive_scale_active_datacartesianT)) /\ exists ff_q_pvs_active_datacartesianTentrypositive. dst_positive_code_active_datacartesianT = ff_q_pvs_active_datacartesianTentrypositive * S ((S (dst_index_active_datacartesianT)) * dst_positive_scale_active_datacartesianT) + (dst_positive_active_datacartesianT))) /\ (((((exists ff_h_pvs_active_datacartesianTentrynegative. ff_h_pvs_active_datacartesianTentrynegative + S (dst_negative_active_datacartesianT) = S ((S (dst_index_active_datacartesianT)) * dst_negative_scale_active_datacartesianT)) /\ exists ff_q_pvs_active_datacartesianTentrynegative. dst_negative_code_active_datacartesianT = ff_q_pvs_active_datacartesianTentrynegative * S ((S (dst_index_active_datacartesianT)) * dst_negative_scale_active_datacartesianT) + (dst_negative_active_datacartesianT))) /\ (exists ge_balance_positive_active_datacartesianTentryvalue ge_balance_negative_active_datacartesianTentryvalue. (((((dst_value_active_datacartesianT) = 2 * (ge_balance_positive_active_datacartesianTentryvalue) /\ (ge_balance_negative_active_datacartesianTentryvalue) = 0) \/ exists ge_signed_half_active_datacartesianTentryvaluedecode. (((dst_value_active_datacartesianT) = 2 * ge_signed_half_active_datacartesianTentryvaluedecode + 1 /\ (ge_balance_positive_active_datacartesianTentryvalue) = 0) /\ (ge_balance_negative_active_datacartesianTentryvalue) = S ge_signed_half_active_datacartesianTentryvaluedecode))) /\ ((dst_positive_active_datacartesianT) + ge_balance_negative_active_datacartesianTentryvalue = (dst_negative_active_datacartesianT) + ge_balance_positive_active_datacartesianTentryvalue))))))))) /\ (forall scp_row_active_datacartesian scp_column_active_datacartesian scp_first_active_datacartesian scp_second_active_datacartesian scp_value_active_datacartesian. (exists pvs_gap_active_datacartesianrows. pvs_gap_active_datacartesianrows + S (scp_row_active_datacartesian) = (S (m))) -> (exists pvs_gap_active_datacartesiancolumns. pvs_gap_active_datacartesiancolumns + S (scp_column_active_datacartesian) = (S (n))) -> (exists dst_positive_code_active_datacartesianfirst dst_positive_scale_active_datacartesianfirst dst_negative_code_active_datacartesianfirst dst_negative_scale_active_datacartesianfirst dst_positive_active_datacartesianfirst dst_negative_active_datacartesianfirst. (((A) = (((((dst_positive_code_active_datacartesianfirst) + (dst_positive_scale_active_datacartesianfirst)) * S ((dst_positive_code_active_datacartesianfirst) + (dst_positive_scale_active_datacartesianfirst)) + ((dst_positive_scale_active_datacartesianfirst) + (dst_positive_scale_active_datacartesianfirst))) + (((dst_negative_code_active_datacartesianfirst) + (dst_negative_scale_active_datacartesianfirst)) * S ((dst_negative_code_active_datacartesianfirst) + (dst_negative_scale_active_datacartesianfirst)) + ((dst_negative_scale_active_datacartesianfirst) + (dst_negative_scale_active_datacartesianfirst)))) * S ((((dst_positive_code_active_datacartesianfirst) + (dst_positive_scale_active_datacartesianfirst)) * S ((dst_positive_code_active_datacartesianfirst) + (dst_positive_scale_active_datacartesianfirst)) + ((dst_positive_scale_active_datacartesianfirst) + (dst_positive_scale_active_datacartesianfirst))) + (((dst_negative_code_active_datacartesianfirst) + (dst_negative_scale_active_datacartesianfirst)) * S ((dst_negative_code_active_datacartesianfirst) + (dst_negative_scale_active_datacartesianfirst)) + ((dst_negative_scale_active_datacartesianfirst) + (dst_negative_scale_active_datacartesianfirst)))) + ((((dst_negative_code_active_datacartesianfirst) + (dst_negative_scale_active_datacartesianfirst)) * S ((dst_negative_code_active_datacartesianfirst) + (dst_negative_scale_active_datacartesianfirst)) + ((dst_negative_scale_active_datacartesianfirst) + (dst_negative_scale_active_datacartesianfirst))) + (((dst_negative_code_active_datacartesianfirst) + (dst_negative_scale_active_datacartesianfirst)) * S ((dst_negative_code_active_datacartesianfirst) + (dst_negative_scale_active_datacartesianfirst)) + ((dst_negative_scale_active_datacartesianfirst) + (dst_negative_scale_active_datacartesianfirst)))))) /\ (((((exists ff_h_pvs_active_datacartesianfirstpositive. ff_h_pvs_active_datacartesianfirstpositive + S (dst_positive_active_datacartesianfirst) = S ((S (scp_row_active_datacartesian)) * dst_positive_scale_active_datacartesianfirst)) /\ exists ff_q_pvs_active_datacartesianfirstpositive. dst_positive_code_active_datacartesianfirst = ff_q_pvs_active_datacartesianfirstpositive * S ((S (scp_row_active_datacartesian)) * dst_positive_scale_active_datacartesianfirst) + (dst_positive_active_datacartesianfirst))) /\ (((((exists ff_h_pvs_active_datacartesianfirstnegative. ff_h_pvs_active_datacartesianfirstnegative + S (dst_negative_active_datacartesianfirst) = S ((S (scp_row_active_datacartesian)) * dst_negative_scale_active_datacartesianfirst)) /\ exists ff_q_pvs_active_datacartesianfirstnegative. dst_negative_code_active_datacartesianfirst = ff_q_pvs_active_datacartesianfirstnegative * S ((S (scp_row_active_datacartesian)) * dst_negative_scale_active_datacartesianfirst) + (dst_negative_active_datacartesianfirst))) /\ (exists ge_balance_positive_active_datacartesianfirstvalue ge_balance_negative_active_datacartesianfirstvalue. (((((scp_first_active_datacartesian) = 2 * (ge_balance_positive_active_datacartesianfirstvalue) /\ (ge_balance_negative_active_datacartesianfirstvalue) = 0) \/ exists ge_signed_half_active_datacartesianfirstvaluedecode. (((scp_first_active_datacartesian) = 2 * ge_signed_half_active_datacartesianfirstvaluedecode + 1 /\ (ge_balance_positive_active_datacartesianfirstvalue) = 0) /\ (ge_balance_negative_active_datacartesianfirstvalue) = S ge_signed_half_active_datacartesianfirstvaluedecode))) /\ ((dst_positive_active_datacartesianfirst) + ge_balance_negative_active_datacartesianfirstvalue = (dst_negative_active_datacartesianfirst) + ge_balance_positive_active_datacartesianfirstvalue))))))))) -> (exists dst_positive_code_active_datacartesiansecond dst_positive_scale_active_datacartesiansecond dst_negative_code_active_datacartesiansecond dst_negative_scale_active_datacartesiansecond dst_positive_active_datacartesiansecond dst_negative_active_datacartesiansecond. (((B) = (((((dst_positive_code_active_datacartesiansecond) + (dst_positive_scale_active_datacartesiansecond)) * S ((dst_positive_code_active_datacartesiansecond) + (dst_positive_scale_active_datacartesiansecond)) + ((dst_positive_scale_active_datacartesiansecond) + (dst_positive_scale_active_datacartesiansecond))) + (((dst_negative_code_active_datacartesiansecond) + (dst_negative_scale_active_datacartesiansecond)) * S ((dst_negative_code_active_datacartesiansecond) + (dst_negative_scale_active_datacartesiansecond)) + ((dst_negative_scale_active_datacartesiansecond) + (dst_negative_scale_active_datacartesiansecond)))) * S ((((dst_positive_code_active_datacartesiansecond) + (dst_positive_scale_active_datacartesiansecond)) * S ((dst_positive_code_active_datacartesiansecond) + (dst_positive_scale_active_datacartesiansecond)) + ((dst_positive_scale_active_datacartesiansecond) + (dst_positive_scale_active_datacartesiansecond))) + (((dst_negative_code_active_datacartesiansecond) + (dst_negative_scale_active_datacartesiansecond)) * S ((dst_negative_code_active_datacartesiansecond) + (dst_negative_scale_active_datacartesiansecond)) + ((dst_negative_scale_active_datacartesiansecond) + (dst_negative_scale_active_datacartesiansecond)))) + ((((dst_negative_code_active_datacartesiansecond) + (dst_negative_scale_active_datacartesiansecond)) * S ((dst_negative_code_active_datacartesiansecond) + (dst_negative_scale_active_datacartesiansecond)) + ((dst_negative_scale_active_datacartesiansecond) + (dst_negative_scale_active_datacartesiansecond))) + (((dst_negative_code_active_datacartesiansecond) + (dst_negative_scale_active_datacartesiansecond)) * S ((dst_negative_code_active_datacartesiansecond) + (dst_negative_scale_active_datacartesiansecond)) + ((dst_negative_scale_active_datacartesiansecond) + (dst_negative_scale_active_datacartesiansecond)))))) /\ (((((exists ff_h_pvs_active_datacartesiansecondpositive. ff_h_pvs_active_datacartesiansecondpositive + S (dst_positive_active_datacartesiansecond) = S ((S (scp_column_active_datacartesian)) * dst_positive_scale_active_datacartesiansecond)) /\ exists ff_q_pvs_active_datacartesiansecondpositive. dst_positive_code_active_datacartesiansecond = ff_q_pvs_active_datacartesiansecondpositive * S ((S (scp_column_active_datacartesian)) * dst_positive_scale_active_datacartesiansecond) + (dst_positive_active_datacartesiansecond))) /\ (((((exists ff_h_pvs_active_datacartesiansecondnegative. ff_h_pvs_active_datacartesiansecondnegative + S (dst_negative_active_datacartesiansecond) = S ((S (scp_column_active_datacartesian)) * dst_negative_scale_active_datacartesiansecond)) /\ exists ff_q_pvs_active_datacartesiansecondnegative. dst_negative_code_active_datacartesiansecond = ff_q_pvs_active_datacartesiansecondnegative * S ((S (scp_column_active_datacartesian)) * dst_negative_scale_active_datacartesiansecond) + (dst_negative_active_datacartesiansecond))) /\ (exists ge_balance_positive_active_datacartesiansecondvalue ge_balance_negative_active_datacartesiansecondvalue. (((((scp_second_active_datacartesian) = 2 * (ge_balance_positive_active_datacartesiansecondvalue) /\ (ge_balance_negative_active_datacartesiansecondvalue) = 0) \/ exists ge_signed_half_active_datacartesiansecondvaluedecode. (((scp_second_active_datacartesian) = 2 * ge_signed_half_active_datacartesiansecondvaluedecode + 1 /\ (ge_balance_positive_active_datacartesiansecondvalue) = 0) /\ (ge_balance_negative_active_datacartesiansecondvalue) = S ge_signed_half_active_datacartesiansecondvaluedecode))) /\ ((dst_positive_active_datacartesiansecond) + ge_balance_negative_active_datacartesiansecondvalue = (dst_negative_active_datacartesiansecond) + ge_balance_positive_active_datacartesiansecondvalue))))))))) -> (exists dst_positive_code_active_datacartesianentry dst_positive_scale_active_datacartesianentry dst_negative_code_active_datacartesianentry dst_negative_scale_active_datacartesianentry dst_positive_active_datacartesianentry dst_negative_active_datacartesianentry. (((T) = (((((dst_positive_code_active_datacartesianentry) + (dst_positive_scale_active_datacartesianentry)) * S ((dst_positive_code_active_datacartesianentry) + (dst_positive_scale_active_datacartesianentry)) + ((dst_positive_scale_active_datacartesianentry) + (dst_positive_scale_active_datacartesianentry))) + (((dst_negative_code_active_datacartesianentry) + (dst_negative_scale_active_datacartesianentry)) * S ((dst_negative_code_active_datacartesianentry) + (dst_negative_scale_active_datacartesianentry)) + ((dst_negative_scale_active_datacartesianentry) + (dst_negative_scale_active_datacartesianentry)))) * S ((((dst_positive_code_active_datacartesianentry) + (dst_positive_scale_active_datacartesianentry)) * S ((dst_positive_code_active_datacartesianentry) + (dst_positive_scale_active_datacartesianentry)) + ((dst_positive_scale_active_datacartesianentry) + (dst_positive_scale_active_datacartesianentry))) + (((dst_negative_code_active_datacartesianentry) + (dst_negative_scale_active_datacartesianentry)) * S ((dst_negative_code_active_datacartesianentry) + (dst_negative_scale_active_datacartesianentry)) + ((dst_negative_scale_active_datacartesianentry) + (dst_negative_scale_active_datacartesianentry)))) + ((((dst_negative_code_active_datacartesianentry) + (dst_negative_scale_active_datacartesianentry)) * S ((dst_negative_code_active_datacartesianentry) + (dst_negative_scale_active_datacartesianentry)) + ((dst_negative_scale_active_datacartesianentry) + (dst_negative_scale_active_datacartesianentry))) + (((dst_negative_code_active_datacartesianentry) + (dst_negative_scale_active_datacartesianentry)) * S ((dst_negative_code_active_datacartesianentry) + (dst_negative_scale_active_datacartesianentry)) + ((dst_negative_scale_active_datacartesianentry) + (dst_negative_scale_active_datacartesianentry)))))) /\ (((((exists ff_h_pvs_active_datacartesianentrypositive. ff_h_pvs_active_datacartesianentrypositive + S (dst_positive_active_datacartesianentry) = S ((S (((S (n))*(scp_row_active_datacartesian)+(scp_column_active_datacartesian)))) * dst_positive_scale_active_datacartesianentry)) /\ exists ff_q_pvs_active_datacartesianentrypositive. dst_positive_code_active_datacartesianentry = ff_q_pvs_active_datacartesianentrypositive * S ((S (((S (n))*(scp_row_active_datacartesian)+(scp_column_active_datacartesian)))) * dst_positive_scale_active_datacartesianentry) + (dst_positive_active_datacartesianentry))) /\ (((((exists ff_h_pvs_active_datacartesianentrynegative. ff_h_pvs_active_datacartesianentrynegative + S (dst_negative_active_datacartesianentry) = S ((S (((S (n))*(scp_row_active_datacartesian)+(scp_column_active_datacartesian)))) * dst_negative_scale_active_datacartesianentry)) /\ exists ff_q_pvs_active_datacartesianentrynegative. dst_negative_code_active_datacartesianentry = ff_q_pvs_active_datacartesianentrynegative * S ((S (((S (n))*(scp_row_active_datacartesian)+(scp_column_active_datacartesian)))) * dst_negative_scale_active_datacartesianentry) + (dst_negative_active_datacartesianentry))) /\ (exists ge_balance_positive_active_datacartesianentryvalue ge_balance_negative_active_datacartesianentryvalue. (((((scp_value_active_datacartesian) = 2 * (ge_balance_positive_active_datacartesianentryvalue) /\ (ge_balance_negative_active_datacartesianentryvalue) = 0) \/ exists ge_signed_half_active_datacartesianentryvaluedecode. (((scp_value_active_datacartesian) = 2 * ge_signed_half_active_datacartesianentryvaluedecode + 1 /\ (ge_balance_positive_active_datacartesianentryvalue) = 0) /\ (ge_balance_negative_active_datacartesianentryvalue) = S ge_signed_half_active_datacartesianentryvaluedecode))) /\ ((dst_positive_active_datacartesianentry) + ge_balance_negative_active_datacartesianentryvalue = (dst_negative_active_datacartesianentry) + ge_balance_positive_active_datacartesianentryvalue))))))))) -> (exists sto_ap_active_datacartesianmultiply sto_an_active_datacartesianmultiply sto_bp_active_datacartesianmultiply sto_bn_active_datacartesianmultiply sto_cp_active_datacartesianmultiply sto_cn_active_datacartesianmultiply. (((((scp_first_active_datacartesian) = 2 * (sto_ap_active_datacartesianmultiply) /\ (sto_an_active_datacartesianmultiply) = 0) \/ exists ge_signed_half_active_datacartesianmultiplyleft. (((scp_first_active_datacartesian) = 2 * ge_signed_half_active_datacartesianmultiplyleft + 1 /\ (sto_ap_active_datacartesianmultiply) = 0) /\ (sto_an_active_datacartesianmultiply) = S ge_signed_half_active_datacartesianmultiplyleft))) /\ ((((((scp_second_active_datacartesian) = 2 * (sto_bp_active_datacartesianmultiply) /\ (sto_bn_active_datacartesianmultiply) = 0) \/ exists ge_signed_half_active_datacartesianmultiplyright. (((scp_second_active_datacartesian) = 2 * ge_signed_half_active_datacartesianmultiplyright + 1 /\ (sto_bp_active_datacartesianmultiply) = 0) /\ (sto_bn_active_datacartesianmultiply) = S ge_signed_half_active_datacartesianmultiplyright))) /\ ((((((scp_value_active_datacartesian) = 2 * (sto_cp_active_datacartesianmultiply) /\ (sto_cn_active_datacartesianmultiply) = 0) \/ exists ge_signed_half_active_datacartesianmultiplyoutput. (((scp_value_active_datacartesian) = 2 * ge_signed_half_active_datacartesianmultiplyoutput + 1 /\ (sto_cp_active_datacartesianmultiply) = 0) /\ (sto_cn_active_datacartesianmultiply) = S ge_signed_half_active_datacartesianmultiplyoutput))) /\ ((sto_ap_active_datacartesianmultiply * sto_bp_active_datacartesianmultiply + sto_an_active_datacartesianmultiply * sto_bn_active_datacartesianmultiply) + sto_cn_active_datacartesianmultiply = (sto_ap_active_datacartesianmultiply * sto_bn_active_datacartesianmultiply + sto_an_active_datacartesianmultiply * sto_bp_active_datacartesianmultiply) + sto_cp_active_datacartesianmultiply)))))))))))))) /\ (((((exists dst_positive_code_active_datatargettable dst_positive_scale_active_datatargettable dst_negative_code_active_datatargettable dst_negative_scale_active_datatargettable. (((Q) = (((((dst_positive_code_active_datatargettable) + (dst_positive_scale_active_datatargettable)) * S ((dst_positive_code_active_datatargettable) + (dst_positive_scale_active_datatargettable)) + ((dst_positive_scale_active_datatargettable) + (dst_positive_scale_active_datatargettable))) + (((dst_negative_code_active_datatargettable) + (dst_negative_scale_active_datatargettable)) * S ((dst_negative_code_active_datatargettable) + (dst_negative_scale_active_datatargettable)) + ((dst_negative_scale_active_datatargettable) + (dst_negative_scale_active_datatargettable)))) * S ((((dst_positive_code_active_datatargettable) + (dst_positive_scale_active_datatargettable)) * S ((dst_positive_code_active_datatargettable) + (dst_positive_scale_active_datatargettable)) + ((dst_positive_scale_active_datatargettable) + (dst_positive_scale_active_datatargettable))) + (((dst_negative_code_active_datatargettable) + (dst_negative_scale_active_datatargettable)) * S ((dst_negative_code_active_datatargettable) + (dst_negative_scale_active_datatargettable)) + ((dst_negative_scale_active_datatargettable) + (dst_negative_scale_active_datatargettable)))) + ((((dst_negative_code_active_datatargettable) + (dst_negative_scale_active_datatargettable)) * S ((dst_negative_code_active_datatargettable) + (dst_negative_scale_active_datatargettable)) + ((dst_negative_scale_active_datatargettable) + (dst_negative_scale_active_datatargettable))) + (((dst_negative_code_active_datatargettable) + (dst_negative_scale_active_datatargettable)) * S ((dst_negative_code_active_datatargettable) + (dst_negative_scale_active_datatargettable)) + ((dst_negative_scale_active_datatargettable) + (dst_negative_scale_active_datatargettable)))))) /\ (forall dst_index_active_datatargettable. (exists pvs_le_gap_active_datatargettabledomain. pvs_le_gap_active_datatargettabledomain + (dst_index_active_datatargettable) = ((m)*(n))) -> exists dst_positive_active_datatargettable dst_negative_active_datatargettable dst_value_active_datatargettable. ((((exists ff_h_pvs_active_datatargettableentrypositive. ff_h_pvs_active_datatargettableentrypositive + S (dst_positive_active_datatargettable) = S ((S (dst_index_active_datatargettable)) * dst_positive_scale_active_datatargettable)) /\ exists ff_q_pvs_active_datatargettableentrypositive. dst_positive_code_active_datatargettable = ff_q_pvs_active_datatargettableentrypositive * S ((S (dst_index_active_datatargettable)) * dst_positive_scale_active_datatargettable) + (dst_positive_active_datatargettable))) /\ (((((exists ff_h_pvs_active_datatargettableentrynegative. ff_h_pvs_active_datatargettableentrynegative + S (dst_negative_active_datatargettable) = S ((S (dst_index_active_datatargettable)) * dst_negative_scale_active_datatargettable)) /\ exists ff_q_pvs_active_datatargettableentrynegative. dst_negative_code_active_datatargettable = ff_q_pvs_active_datatargettableentrynegative * S ((S (dst_index_active_datatargettable)) * dst_negative_scale_active_datatargettable) + (dst_negative_active_datatargettable))) /\ (exists ge_balance_positive_active_datatargettableentryvalue ge_balance_negative_active_datatargettableentryvalue. (((((dst_value_active_datatargettable) = 2 * (ge_balance_positive_active_datatargettableentryvalue) /\ (ge_balance_negative_active_datatargettableentryvalue) = 0) \/ exists ge_signed_half_active_datatargettableentryvaluedecode. (((dst_value_active_datatargettable) = 2 * ge_signed_half_active_datatargettableentryvaluedecode + 1 /\ (ge_balance_positive_active_datatargettableentryvalue) = 0) /\ (ge_balance_negative_active_datatargettableentryvalue) = S ge_signed_half_active_datatargettableentryvaluedecode))) /\ ((dst_positive_active_datatargettable) + ge_balance_negative_active_datatargettableentryvalue = (dst_negative_active_datatargettable) + ge_balance_positive_active_datatargettableentryvalue))))))))) /\ (forall dc_index_active_datatarget dc_value_active_datatarget. (exists pvs_le_gap_active_datatargetdomain. pvs_le_gap_active_datatargetdomain + (dc_index_active_datatarget) = ((m)*(n))) -> (exists dst_positive_code_active_datatargetlookup dst_positive_scale_active_datatargetlookup dst_negative_code_active_datatargetlookup dst_negative_scale_active_datatargetlookup dst_positive_active_datatargetlookup dst_negative_active_datatargetlookup. (((Q) = (((((dst_positive_code_active_datatargetlookup) + (dst_positive_scale_active_datatargetlookup)) * S ((dst_positive_code_active_datatargetlookup) + (dst_positive_scale_active_datatargetlookup)) + ((dst_positive_scale_active_datatargetlookup) + (dst_positive_scale_active_datatargetlookup))) + (((dst_negative_code_active_datatargetlookup) + (dst_negative_scale_active_datatargetlookup)) * S ((dst_negative_code_active_datatargetlookup) + (dst_negative_scale_active_datatargetlookup)) + ((dst_negative_scale_active_datatargetlookup) + (dst_negative_scale_active_datatargetlookup)))) * S ((((dst_positive_code_active_datatargetlookup) + (dst_positive_scale_active_datatargetlookup)) * S ((dst_positive_code_active_datatargetlookup) + (dst_positive_scale_active_datatargetlookup)) + ((dst_positive_scale_active_datatargetlookup) + (dst_positive_scale_active_datatargetlookup))) + (((dst_negative_code_active_datatargetlookup) + (dst_negative_scale_active_datatargetlookup)) * S ((dst_negative_code_active_datatargetlookup) + (dst_negative_scale_active_datatargetlookup)) + ((dst_negative_scale_active_datatargetlookup) + (dst_negative_scale_active_datatargetlookup)))) + ((((dst_negative_code_active_datatargetlookup) + (dst_negative_scale_active_datatargetlookup)) * S ((dst_negative_code_active_datatargetlookup) + (dst_negative_scale_active_datatargetlookup)) + ((dst_negative_scale_active_datatargetlookup) + (dst_negative_scale_active_datatargetlookup))) + (((dst_negative_code_active_datatargetlookup) + (dst_negative_scale_active_datatargetlookup)) * S ((dst_negative_code_active_datatargetlookup) + (dst_negative_scale_active_datatargetlookup)) + ((dst_negative_scale_active_datatargetlookup) + (dst_negative_scale_active_datatargetlookup)))))) /\ (((((exists ff_h_pvs_active_datatargetlookuppositive. ff_h_pvs_active_datatargetlookuppositive + S (dst_positive_active_datatargetlookup) = S ((S (dc_index_active_datatarget)) * dst_positive_scale_active_datatargetlookup)) /\ exists ff_q_pvs_active_datatargetlookuppositive. dst_positive_code_active_datatargetlookup = ff_q_pvs_active_datatargetlookuppositive * S ((S (dc_index_active_datatarget)) * dst_positive_scale_active_datatargetlookup) + (dst_positive_active_datatargetlookup))) /\ (((((exists ff_h_pvs_active_datatargetlookupnegative. ff_h_pvs_active_datatargetlookupnegative + S (dst_negative_active_datatargetlookup) = S ((S (dc_index_active_datatarget)) * dst_negative_scale_active_datatargetlookup)) /\ exists ff_q_pvs_active_datatargetlookupnegative. dst_negative_code_active_datatargetlookup = ff_q_pvs_active_datatargetlookupnegative * S ((S (dc_index_active_datatarget)) * dst_negative_scale_active_datatargetlookup) + (dst_negative_active_datatargetlookup))) /\ (exists ge_balance_positive_active_datatargetlookupvalue ge_balance_negative_active_datatargetlookupvalue. (((((dc_value_active_datatarget) = 2 * (ge_balance_positive_active_datatargetlookupvalue) /\ (ge_balance_negative_active_datatargetlookupvalue) = 0) \/ exists ge_signed_half_active_datatargetlookupvaluedecode. (((dc_value_active_datatarget) = 2 * ge_signed_half_active_datatargetlookupvaluedecode + 1 /\ (ge_balance_positive_active_datatargetlookupvalue) = 0) /\ (ge_balance_negative_active_datatargetlookupvalue) = S ge_signed_half_active_datatargetlookupvaluedecode))) /\ ((dst_positive_active_datatargetlookup) + ge_balance_negative_active_datatargetlookupvalue = (dst_negative_active_datatargetlookup) + ge_balance_positive_active_datatargetlookupvalue))))))))) -> ((((~((dc_index_active_datatarget)=0)) /\ (exists dc_quotient_active_datatargetentry dc_left_active_datatargetentry dc_right_active_datatargetentry. ((((m)*(n))=(dc_index_active_datatarget)*dc_quotient_active_datatargetentry) /\ (((exists dst_positive_code_active_datatargetentryleft dst_positive_scale_active_datatargetentryleft dst_negative_code_active_datatargetentryleft dst_negative_scale_active_datatargetentryleft dst_positive_active_datatargetentryleft dst_negative_active_datatargetentryleft. (((F) = (((((dst_positive_code_active_datatargetentryleft) + (dst_positive_scale_active_datatargetentryleft)) * S ((dst_positive_code_active_datatargetentryleft) + (dst_positive_scale_active_datatargetentryleft)) + ((dst_positive_scale_active_datatargetentryleft) + (dst_positive_scale_active_datatargetentryleft))) + (((dst_negative_code_active_datatargetentryleft) + (dst_negative_scale_active_datatargetentryleft)) * S ((dst_negative_code_active_datatargetentryleft) + (dst_negative_scale_active_datatargetentryleft)) + ((dst_negative_scale_active_datatargetentryleft) + (dst_negative_scale_active_datatargetentryleft)))) * S ((((dst_positive_code_active_datatargetentryleft) + (dst_positive_scale_active_datatargetentryleft)) * S ((dst_positive_code_active_datatargetentryleft) + (dst_positive_scale_active_datatargetentryleft)) + ((dst_positive_scale_active_datatargetentryleft) + (dst_positive_scale_active_datatargetentryleft))) + (((dst_negative_code_active_datatargetentryleft) + (dst_negative_scale_active_datatargetentryleft)) * S ((dst_negative_code_active_datatargetentryleft) + (dst_negative_scale_active_datatargetentryleft)) + ((dst_negative_scale_active_datatargetentryleft) + (dst_negative_scale_active_datatargetentryleft)))) + ((((dst_negative_code_active_datatargetentryleft) + (dst_negative_scale_active_datatargetentryleft)) * S ((dst_negative_code_active_datatargetentryleft) + (dst_negative_scale_active_datatargetentryleft)) + ((dst_negative_scale_active_datatargetentryleft) + (dst_negative_scale_active_datatargetentryleft))) + (((dst_negative_code_active_datatargetentryleft) + (dst_negative_scale_active_datatargetentryleft)) * S ((dst_negative_code_active_datatargetentryleft) + (dst_negative_scale_active_datatargetentryleft)) + ((dst_negative_scale_active_datatargetentryleft) + (dst_negative_scale_active_datatargetentryleft)))))) /\ (((((exists ff_h_pvs_active_datatargetentryleftpositive. ff_h_pvs_active_datatargetentryleftpositive + S (dst_positive_active_datatargetentryleft) = S ((S (dc_index_active_datatarget)) * dst_positive_scale_active_datatargetentryleft)) /\ exists ff_q_pvs_active_datatargetentryleftpositive. dst_positive_code_active_datatargetentryleft = ff_q_pvs_active_datatargetentryleftpositive * S ((S (dc_index_active_datatarget)) * dst_positive_scale_active_datatargetentryleft) + (dst_positive_active_datatargetentryleft))) /\ (((((exists ff_h_pvs_active_datatargetentryleftnegative. ff_h_pvs_active_datatargetentryleftnegative + S (dst_negative_active_datatargetentryleft) = S ((S (dc_index_active_datatarget)) * dst_negative_scale_active_datatargetentryleft)) /\ exists ff_q_pvs_active_datatargetentryleftnegative. dst_negative_code_active_datatargetentryleft = ff_q_pvs_active_datatargetentryleftnegative * S ((S (dc_index_active_datatarget)) * dst_negative_scale_active_datatargetentryleft) + (dst_negative_active_datatargetentryleft))) /\ (exists ge_balance_positive_active_datatargetentryleftvalue ge_balance_negative_active_datatargetentryleftvalue. (((((dc_left_active_datatargetentry) = 2 * (ge_balance_positive_active_datatargetentryleftvalue) /\ (ge_balance_negative_active_datatargetentryleftvalue) = 0) \/ exists ge_signed_half_active_datatargetentryleftvaluedecode. (((dc_left_active_datatargetentry) = 2 * ge_signed_half_active_datatargetentryleftvaluedecode + 1 /\ (ge_balance_positive_active_datatargetentryleftvalue) = 0) /\ (ge_balance_negative_active_datatargetentryleftvalue) = S ge_signed_half_active_datatargetentryleftvaluedecode))) /\ ((dst_positive_active_datatargetentryleft) + ge_balance_negative_active_datatargetentryleftvalue = (dst_negative_active_datatargetentryleft) + ge_balance_positive_active_datatargetentryleftvalue))))))))) /\ (((exists dst_positive_code_active_datatargetentryright dst_positive_scale_active_datatargetentryright dst_negative_code_active_datatargetentryright dst_negative_scale_active_datatargetentryright dst_positive_active_datatargetentryright dst_negative_active_datatargetentryright. (((G) = (((((dst_positive_code_active_datatargetentryright) + (dst_positive_scale_active_datatargetentryright)) * S ((dst_positive_code_active_datatargetentryright) + (dst_positive_scale_active_datatargetentryright)) + ((dst_positive_scale_active_datatargetentryright) + (dst_positive_scale_active_datatargetentryright))) + (((dst_negative_code_active_datatargetentryright) + (dst_negative_scale_active_datatargetentryright)) * S ((dst_negative_code_active_datatargetentryright) + (dst_negative_scale_active_datatargetentryright)) + ((dst_negative_scale_active_datatargetentryright) + (dst_negative_scale_active_datatargetentryright)))) * S ((((dst_positive_code_active_datatargetentryright) + (dst_positive_scale_active_datatargetentryright)) * S ((dst_positive_code_active_datatargetentryright) + (dst_positive_scale_active_datatargetentryright)) + ((dst_positive_scale_active_datatargetentryright) + (dst_positive_scale_active_datatargetentryright))) + (((dst_negative_code_active_datatargetentryright) + (dst_negative_scale_active_datatargetentryright)) * S ((dst_negative_code_active_datatargetentryright) + (dst_negative_scale_active_datatargetentryright)) + ((dst_negative_scale_active_datatargetentryright) + (dst_negative_scale_active_datatargetentryright)))) + ((((dst_negative_code_active_datatargetentryright) + (dst_negative_scale_active_datatargetentryright)) * S ((dst_negative_code_active_datatargetentryright) + (dst_negative_scale_active_datatargetentryright)) + ((dst_negative_scale_active_datatargetentryright) + (dst_negative_scale_active_datatargetentryright))) + (((dst_negative_code_active_datatargetentryright) + (dst_negative_scale_active_datatargetentryright)) * S ((dst_negative_code_active_datatargetentryright) + (dst_negative_scale_active_datatargetentryright)) + ((dst_negative_scale_active_datatargetentryright) + (dst_negative_scale_active_datatargetentryright)))))) /\ (((((exists ff_h_pvs_active_datatargetentryrightpositive. ff_h_pvs_active_datatargetentryrightpositive + S (dst_positive_active_datatargetentryright) = S ((S (dc_quotient_active_datatargetentry)) * dst_positive_scale_active_datatargetentryright)) /\ exists ff_q_pvs_active_datatargetentryrightpositive. dst_positive_code_active_datatargetentryright = ff_q_pvs_active_datatargetentryrightpositive * S ((S (dc_quotient_active_datatargetentry)) * dst_positive_scale_active_datatargetentryright) + (dst_positive_active_datatargetentryright))) /\ (((((exists ff_h_pvs_active_datatargetentryrightnegative. ff_h_pvs_active_datatargetentryrightnegative + S (dst_negative_active_datatargetentryright) = S ((S (dc_quotient_active_datatargetentry)) * dst_negative_scale_active_datatargetentryright)) /\ exists ff_q_pvs_active_datatargetentryrightnegative. dst_negative_code_active_datatargetentryright = ff_q_pvs_active_datatargetentryrightnegative * S ((S (dc_quotient_active_datatargetentry)) * dst_negative_scale_active_datatargetentryright) + (dst_negative_active_datatargetentryright))) /\ (exists ge_balance_positive_active_datatargetentryrightvalue ge_balance_negative_active_datatargetentryrightvalue. (((((dc_right_active_datatargetentry) = 2 * (ge_balance_positive_active_datatargetentryrightvalue) /\ (ge_balance_negative_active_datatargetentryrightvalue) = 0) \/ exists ge_signed_half_active_datatargetentryrightvaluedecode. (((dc_right_active_datatargetentry) = 2 * ge_signed_half_active_datatargetentryrightvaluedecode + 1 /\ (ge_balance_positive_active_datatargetentryrightvalue) = 0) /\ (ge_balance_negative_active_datatargetentryrightvalue) = S ge_signed_half_active_datatargetentryrightvaluedecode))) /\ ((dst_positive_active_datatargetentryright) + ge_balance_negative_active_datatargetentryrightvalue = (dst_negative_active_datatargetentryright) + ge_balance_positive_active_datatargetentryrightvalue))))))))) /\ (exists sto_ap_active_datatargetentryproduct sto_an_active_datatargetentryproduct sto_bp_active_datatargetentryproduct sto_bn_active_datatargetentryproduct sto_cp_active_datatargetentryproduct sto_cn_active_datatargetentryproduct. (((((dc_left_active_datatargetentry) = 2 * (sto_ap_active_datatargetentryproduct) /\ (sto_an_active_datatargetentryproduct) = 0) \/ exists ge_signed_half_active_datatargetentryproductleft. (((dc_left_active_datatargetentry) = 2 * ge_signed_half_active_datatargetentryproductleft + 1 /\ (sto_ap_active_datatargetentryproduct) = 0) /\ (sto_an_active_datatargetentryproduct) = S ge_signed_half_active_datatargetentryproductleft))) /\ ((((((dc_right_active_datatargetentry) = 2 * (sto_bp_active_datatargetentryproduct) /\ (sto_bn_active_datatargetentryproduct) = 0) \/ exists ge_signed_half_active_datatargetentryproductright. (((dc_right_active_datatargetentry) = 2 * ge_signed_half_active_datatargetentryproductright + 1 /\ (sto_bp_active_datatargetentryproduct) = 0) /\ (sto_bn_active_datatargetentryproduct) = S ge_signed_half_active_datatargetentryproductright))) /\ ((((((dc_value_active_datatarget) = 2 * (sto_cp_active_datatargetentryproduct) /\ (sto_cn_active_datatargetentryproduct) = 0) \/ exists ge_signed_half_active_datatargetentryproductoutput. (((dc_value_active_datatarget) = 2 * ge_signed_half_active_datatargetentryproductoutput + 1 /\ (sto_cp_active_datatargetentryproduct) = 0) /\ (sto_cn_active_datatargetentryproduct) = S ge_signed_half_active_datatargetentryproductoutput))) /\ ((sto_ap_active_datatargetentryproduct * sto_bp_active_datatargetentryproduct + sto_an_active_datatargetentryproduct * sto_bn_active_datatargetentryproduct) + sto_cn_active_datatargetentryproduct = (sto_ap_active_datatargetentryproduct * sto_bn_active_datatargetentryproduct + sto_an_active_datatargetentryproduct * sto_bp_active_datatargetentryproduct) + sto_cp_active_datatargetentryproduct))))))))))))))) \/ ((((dc_index_active_datatarget)=0 \/ ~(exists pvs_factor_active_datatargetentrynondivisor. ((m)*(n)) = (dc_index_active_datatarget) * pvs_factor_active_datatargetentrynondivisor)) /\ ((dc_value_active_datatarget)=0))))))) /\ (((~((S (n))=0)) /\ (forall dpi_index_active_datamap dpi_row_active_datamap dpi_column_active_datamap. (exists pvs_gap_active_datamapwindow. pvs_gap_active_datamapwindow + S (dpi_index_active_datamap) = ((S (m))*(S (n)))) -> (exists pvs_gap_active_datamapremainder. pvs_gap_active_datamapremainder + S (dpi_column_active_datamap) = (S (n))) -> (dpi_index_active_datamap)=(S (n))*(dpi_row_active_datamap)+(dpi_column_active_datamap) -> (((exists ff_h_pvs_active_datamapvalue. ff_h_pvs_active_datamapvalue + S ((dpi_row_active_datamap)*(dpi_column_active_datamap)) = S ((S (dpi_index_active_datamap)) * s)) /\ exists ff_q_pvs_active_datamapvalue. r = ff_q_pvs_active_datamapvalue * S ((S (dpi_index_active_datamap)) * s) + ((dpi_row_active_datamap)*(dpi_column_active_datamap))))))))))))))))))))))))))) -> (exists pvs_gap_active_index. pvs_gap_active_index + S (i) = ((S (m))*(S (n)))) -> (exists dst_positive_code_active_lookup dst_positive_scale_active_lookup dst_negative_code_active_lookup dst_negative_scale_active_lookup dst_positive_active_lookup dst_negative_active_lookup. (((T) = (((((dst_positive_code_active_lookup) + (dst_positive_scale_active_lookup)) * S ((dst_positive_code_active_lookup) + (dst_positive_scale_active_lookup)) + ((dst_positive_scale_active_lookup) + (dst_positive_scale_active_lookup))) + (((dst_negative_code_active_lookup) + (dst_negative_scale_active_lookup)) * S ((dst_negative_code_active_lookup) + (dst_negative_scale_active_lookup)) + ((dst_negative_scale_active_lookup) + (dst_negative_scale_active_lookup)))) * S ((((dst_positive_code_active_lookup) + (dst_positive_scale_active_lookup)) * S ((dst_positive_code_active_lookup) + (dst_positive_scale_active_lookup)) + ((dst_positive_scale_active_lookup) + (dst_positive_scale_active_lookup))) + (((dst_negative_code_active_lookup) + (dst_negative_scale_active_lookup)) * S ((dst_negative_code_active_lookup) + (dst_negative_scale_active_lookup)) + ((dst_negative_scale_active_lookup) + (dst_negative_scale_active_lookup)))) + ((((dst_negative_code_active_lookup) + (dst_negative_scale_active_lookup)) * S ((dst_negative_code_active_lookup) + (dst_negative_scale_active_lookup)) + ((dst_negative_scale_active_lookup) + (dst_negative_scale_active_lookup))) + (((dst_negative_code_active_lookup) + (dst_negative_scale_active_lookup)) * S ((dst_negative_code_active_lookup) + (dst_negative_scale_active_lookup)) + ((dst_negative_scale_active_lookup) + (dst_negative_scale_active_lookup)))))) /\ (((((exists ff_h_pvs_active_lookuppositive. ff_h_pvs_active_lookuppositive + S (dst_positive_active_lookup) = S ((S (i)) * dst_positive_scale_active_lookup)) /\ exists ff_q_pvs_active_lookuppositive. dst_positive_code_active_lookup = ff_q_pvs_active_lookuppositive * S ((S (i)) * dst_positive_scale_active_lookup) + (dst_positive_active_lookup))) /\ (((((exists ff_h_pvs_active_lookupnegative. ff_h_pvs_active_lookupnegative + S (dst_negative_active_lookup) = S ((S (i)) * dst_negative_scale_active_lookup)) /\ exists ff_q_pvs_active_lookupnegative. dst_negative_code_active_lookup = ff_q_pvs_active_lookupnegative * S ((S (i)) * dst_negative_scale_active_lookup) + (dst_negative_active_lookup))) /\ (exists ge_balance_positive_active_lookupvalue ge_balance_negative_active_lookupvalue. (((((z) = 2 * (ge_balance_positive_active_lookupvalue) /\ (ge_balance_negative_active_lookupvalue) = 0) \/ exists ge_signed_half_active_lookupvaluedecode. (((z) = 2 * ge_signed_half_active_lookupvaluedecode + 1 /\ (ge_balance_positive_active_lookupvalue) = 0) /\ (ge_balance_negative_active_lookupvalue) = S ge_signed_half_active_lookupvaluedecode))) /\ ((dst_positive_active_lookup) + ge_balance_negative_active_lookupvalue = (dst_negative_active_lookup) + ge_balance_positive_active_lookupvalue))))))))) -> ~(z=0) -> exists d e a b. ((((i)=((S (n))*(d)+(e))) /\ (((exists pvs_gap_active_resultrow. pvs_gap_active_resultrow + S (d) = (S (m))) /\ (((exists pvs_gap_active_resultcolumn. pvs_gap_active_resultcolumn + S (e) = (S (n))) /\ (((((~((d)=0)) /\ (((~((e)=0)) /\ (((exists pvs_factor_active_resultpairleft. (m) = (d) * pvs_factor_active_resultpairleft) /\ (((exists pvs_factor_active_resultpairright. (n) = (e) * pvs_factor_active_resultpairright) /\ (((d)*(e))=(d)*(e)))))))))) /\ ((((((~((d)=0)) /\ (exists dc_quotient_active_resultleft dc_left_active_resultleft dc_right_active_resultleft. (((m)=(d)*dc_quotient_active_resultleft) /\ (((exists dst_positive_code_active_resultleftleft dst_positive_scale_active_resultleftleft dst_negative_code_active_resultleftleft dst_negative_scale_active_resultleftleft dst_positive_active_resultleftleft dst_negative_active_resultleftleft. (((F) = (((((dst_positive_code_active_resultleftleft) + (dst_positive_scale_active_resultleftleft)) * S ((dst_positive_code_active_resultleftleft) + (dst_positive_scale_active_resultleftleft)) + ((dst_positive_scale_active_resultleftleft) + (dst_positive_scale_active_resultleftleft))) + (((dst_negative_code_active_resultleftleft) + (dst_negative_scale_active_resultleftleft)) * S ((dst_negative_code_active_resultleftleft) + (dst_negative_scale_active_resultleftleft)) + ((dst_negative_scale_active_resultleftleft) + (dst_negative_scale_active_resultleftleft)))) * S ((((dst_positive_code_active_resultleftleft) + (dst_positive_scale_active_resultleftleft)) * S ((dst_positive_code_active_resultleftleft) + (dst_positive_scale_active_resultleftleft)) + ((dst_positive_scale_active_resultleftleft) + (dst_positive_scale_active_resultleftleft))) + (((dst_negative_code_active_resultleftleft) + (dst_negative_scale_active_resultleftleft)) * S ((dst_negative_code_active_resultleftleft) + (dst_negative_scale_active_resultleftleft)) + ((dst_negative_scale_active_resultleftleft) + (dst_negative_scale_active_resultleftleft)))) + ((((dst_negative_code_active_resultleftleft) + (dst_negative_scale_active_resultleftleft)) * S ((dst_negative_code_active_resultleftleft) + (dst_negative_scale_active_resultleftleft)) + ((dst_negative_scale_active_resultleftleft) + (dst_negative_scale_active_resultleftleft))) + (((dst_negative_code_active_resultleftleft) + (dst_negative_scale_active_resultleftleft)) * S ((dst_negative_code_active_resultleftleft) + (dst_negative_scale_active_resultleftleft)) + ((dst_negative_scale_active_resultleftleft) + (dst_negative_scale_active_resultleftleft)))))) /\ (((((exists ff_h_pvs_active_resultleftleftpositive. ff_h_pvs_active_resultleftleftpositive + S (dst_positive_active_resultleftleft) = S ((S (d)) * dst_positive_scale_active_resultleftleft)) /\ exists ff_q_pvs_active_resultleftleftpositive. dst_positive_code_active_resultleftleft = ff_q_pvs_active_resultleftleftpositive * S ((S (d)) * dst_positive_scale_active_resultleftleft) + (dst_positive_active_resultleftleft))) /\ (((((exists ff_h_pvs_active_resultleftleftnegative. ff_h_pvs_active_resultleftleftnegative + S (dst_negative_active_resultleftleft) = S ((S (d)) * dst_negative_scale_active_resultleftleft)) /\ exists ff_q_pvs_active_resultleftleftnegative. dst_negative_code_active_resultleftleft = ff_q_pvs_active_resultleftleftnegative * S ((S (d)) * dst_negative_scale_active_resultleftleft) + (dst_negative_active_resultleftleft))) /\ (exists ge_balance_positive_active_resultleftleftvalue ge_balance_negative_active_resultleftleftvalue. (((((dc_left_active_resultleft) = 2 * (ge_balance_positive_active_resultleftleftvalue) /\ (ge_balance_negative_active_resultleftleftvalue) = 0) \/ exists ge_signed_half_active_resultleftleftvaluedecode. (((dc_left_active_resultleft) = 2 * ge_signed_half_active_resultleftleftvaluedecode + 1 /\ (ge_balance_positive_active_resultleftleftvalue) = 0) /\ (ge_balance_negative_active_resultleftleftvalue) = S ge_signed_half_active_resultleftleftvaluedecode))) /\ ((dst_positive_active_resultleftleft) + ge_balance_negative_active_resultleftleftvalue = (dst_negative_active_resultleftleft) + ge_balance_positive_active_resultleftleftvalue))))))))) /\ (((exists dst_positive_code_active_resultleftright dst_positive_scale_active_resultleftright dst_negative_code_active_resultleftright dst_negative_scale_active_resultleftright dst_positive_active_resultleftright dst_negative_active_resultleftright. (((G) = (((((dst_positive_code_active_resultleftright) + (dst_positive_scale_active_resultleftright)) * S ((dst_positive_code_active_resultleftright) + (dst_positive_scale_active_resultleftright)) + ((dst_positive_scale_active_resultleftright) + (dst_positive_scale_active_resultleftright))) + (((dst_negative_code_active_resultleftright) + (dst_negative_scale_active_resultleftright)) * S ((dst_negative_code_active_resultleftright) + (dst_negative_scale_active_resultleftright)) + ((dst_negative_scale_active_resultleftright) + (dst_negative_scale_active_resultleftright)))) * S ((((dst_positive_code_active_resultleftright) + (dst_positive_scale_active_resultleftright)) * S ((dst_positive_code_active_resultleftright) + (dst_positive_scale_active_resultleftright)) + ((dst_positive_scale_active_resultleftright) + (dst_positive_scale_active_resultleftright))) + (((dst_negative_code_active_resultleftright) + (dst_negative_scale_active_resultleftright)) * S ((dst_negative_code_active_resultleftright) + (dst_negative_scale_active_resultleftright)) + ((dst_negative_scale_active_resultleftright) + (dst_negative_scale_active_resultleftright)))) + ((((dst_negative_code_active_resultleftright) + (dst_negative_scale_active_resultleftright)) * S ((dst_negative_code_active_resultleftright) + (dst_negative_scale_active_resultleftright)) + ((dst_negative_scale_active_resultleftright) + (dst_negative_scale_active_resultleftright))) + (((dst_negative_code_active_resultleftright) + (dst_negative_scale_active_resultleftright)) * S ((dst_negative_code_active_resultleftright) + (dst_negative_scale_active_resultleftright)) + ((dst_negative_scale_active_resultleftright) + (dst_negative_scale_active_resultleftright)))))) /\ (((((exists ff_h_pvs_active_resultleftrightpositive. ff_h_pvs_active_resultleftrightpositive + S (dst_positive_active_resultleftright) = S ((S (dc_quotient_active_resultleft)) * dst_positive_scale_active_resultleftright)) /\ exists ff_q_pvs_active_resultleftrightpositive. dst_positive_code_active_resultleftright = ff_q_pvs_active_resultleftrightpositive * S ((S (dc_quotient_active_resultleft)) * dst_positive_scale_active_resultleftright) + (dst_positive_active_resultleftright))) /\ (((((exists ff_h_pvs_active_resultleftrightnegative. ff_h_pvs_active_resultleftrightnegative + S (dst_negative_active_resultleftright) = S ((S (dc_quotient_active_resultleft)) * dst_negative_scale_active_resultleftright)) /\ exists ff_q_pvs_active_resultleftrightnegative. dst_negative_code_active_resultleftright = ff_q_pvs_active_resultleftrightnegative * S ((S (dc_quotient_active_resultleft)) * dst_negative_scale_active_resultleftright) + (dst_negative_active_resultleftright))) /\ (exists ge_balance_positive_active_resultleftrightvalue ge_balance_negative_active_resultleftrightvalue. (((((dc_right_active_resultleft) = 2 * (ge_balance_positive_active_resultleftrightvalue) /\ (ge_balance_negative_active_resultleftrightvalue) = 0) \/ exists ge_signed_half_active_resultleftrightvaluedecode. (((dc_right_active_resultleft) = 2 * ge_signed_half_active_resultleftrightvaluedecode + 1 /\ (ge_balance_positive_active_resultleftrightvalue) = 0) /\ (ge_balance_negative_active_resultleftrightvalue) = S ge_signed_half_active_resultleftrightvaluedecode))) /\ ((dst_positive_active_resultleftright) + ge_balance_negative_active_resultleftrightvalue = (dst_negative_active_resultleftright) + ge_balance_positive_active_resultleftrightvalue))))))))) /\ (exists sto_ap_active_resultleftproduct sto_an_active_resultleftproduct sto_bp_active_resultleftproduct sto_bn_active_resultleftproduct sto_cp_active_resultleftproduct sto_cn_active_resultleftproduct. (((((dc_left_active_resultleft) = 2 * (sto_ap_active_resultleftproduct) /\ (sto_an_active_resultleftproduct) = 0) \/ exists ge_signed_half_active_resultleftproductleft. (((dc_left_active_resultleft) = 2 * ge_signed_half_active_resultleftproductleft + 1 /\ (sto_ap_active_resultleftproduct) = 0) /\ (sto_an_active_resultleftproduct) = S ge_signed_half_active_resultleftproductleft))) /\ ((((((dc_right_active_resultleft) = 2 * (sto_bp_active_resultleftproduct) /\ (sto_bn_active_resultleftproduct) = 0) \/ exists ge_signed_half_active_resultleftproductright. (((dc_right_active_resultleft) = 2 * ge_signed_half_active_resultleftproductright + 1 /\ (sto_bp_active_resultleftproduct) = 0) /\ (sto_bn_active_resultleftproduct) = S ge_signed_half_active_resultleftproductright))) /\ ((((((a) = 2 * (sto_cp_active_resultleftproduct) /\ (sto_cn_active_resultleftproduct) = 0) \/ exists ge_signed_half_active_resultleftproductoutput. (((a) = 2 * ge_signed_half_active_resultleftproductoutput + 1 /\ (sto_cp_active_resultleftproduct) = 0) /\ (sto_cn_active_resultleftproduct) = S ge_signed_half_active_resultleftproductoutput))) /\ ((sto_ap_active_resultleftproduct * sto_bp_active_resultleftproduct + sto_an_active_resultleftproduct * sto_bn_active_resultleftproduct) + sto_cn_active_resultleftproduct = (sto_ap_active_resultleftproduct * sto_bn_active_resultleftproduct + sto_an_active_resultleftproduct * sto_bp_active_resultleftproduct) + sto_cp_active_resultleftproduct))))))))))))))) \/ ((((d)=0 \/ ~(exists pvs_factor_active_resultleftnondivisor. (m) = (d) * pvs_factor_active_resultleftnondivisor)) /\ ((a)=0)))) /\ ((((((~((e)=0)) /\ (exists dc_quotient_active_resultright dc_left_active_resultright dc_right_active_resultright. (((n)=(e)*dc_quotient_active_resultright) /\ (((exists dst_positive_code_active_resultrightleft dst_positive_scale_active_resultrightleft dst_negative_code_active_resultrightleft dst_negative_scale_active_resultrightleft dst_positive_active_resultrightleft dst_negative_active_resultrightleft. (((F) = (((((dst_positive_code_active_resultrightleft) + (dst_positive_scale_active_resultrightleft)) * S ((dst_positive_code_active_resultrightleft) + (dst_positive_scale_active_resultrightleft)) + ((dst_positive_scale_active_resultrightleft) + (dst_positive_scale_active_resultrightleft))) + (((dst_negative_code_active_resultrightleft) + (dst_negative_scale_active_resultrightleft)) * S ((dst_negative_code_active_resultrightleft) + (dst_negative_scale_active_resultrightleft)) + ((dst_negative_scale_active_resultrightleft) + (dst_negative_scale_active_resultrightleft)))) * S ((((dst_positive_code_active_resultrightleft) + (dst_positive_scale_active_resultrightleft)) * S ((dst_positive_code_active_resultrightleft) + (dst_positive_scale_active_resultrightleft)) + ((dst_positive_scale_active_resultrightleft) + (dst_positive_scale_active_resultrightleft))) + (((dst_negative_code_active_resultrightleft) + (dst_negative_scale_active_resultrightleft)) * S ((dst_negative_code_active_resultrightleft) + (dst_negative_scale_active_resultrightleft)) + ((dst_negative_scale_active_resultrightleft) + (dst_negative_scale_active_resultrightleft)))) + ((((dst_negative_code_active_resultrightleft) + (dst_negative_scale_active_resultrightleft)) * S ((dst_negative_code_active_resultrightleft) + (dst_negative_scale_active_resultrightleft)) + ((dst_negative_scale_active_resultrightleft) + (dst_negative_scale_active_resultrightleft))) + (((dst_negative_code_active_resultrightleft) + (dst_negative_scale_active_resultrightleft)) * S ((dst_negative_code_active_resultrightleft) + (dst_negative_scale_active_resultrightleft)) + ((dst_negative_scale_active_resultrightleft) + (dst_negative_scale_active_resultrightleft)))))) /\ (((((exists ff_h_pvs_active_resultrightleftpositive. ff_h_pvs_active_resultrightleftpositive + S (dst_positive_active_resultrightleft) = S ((S (e)) * dst_positive_scale_active_resultrightleft)) /\ exists ff_q_pvs_active_resultrightleftpositive. dst_positive_code_active_resultrightleft = ff_q_pvs_active_resultrightleftpositive * S ((S (e)) * dst_positive_scale_active_resultrightleft) + (dst_positive_active_resultrightleft))) /\ (((((exists ff_h_pvs_active_resultrightleftnegative. ff_h_pvs_active_resultrightleftnegative + S (dst_negative_active_resultrightleft) = S ((S (e)) * dst_negative_scale_active_resultrightleft)) /\ exists ff_q_pvs_active_resultrightleftnegative. dst_negative_code_active_resultrightleft = ff_q_pvs_active_resultrightleftnegative * S ((S (e)) * dst_negative_scale_active_resultrightleft) + (dst_negative_active_resultrightleft))) /\ (exists ge_balance_positive_active_resultrightleftvalue ge_balance_negative_active_resultrightleftvalue. (((((dc_left_active_resultright) = 2 * (ge_balance_positive_active_resultrightleftvalue) /\ (ge_balance_negative_active_resultrightleftvalue) = 0) \/ exists ge_signed_half_active_resultrightleftvaluedecode. (((dc_left_active_resultright) = 2 * ge_signed_half_active_resultrightleftvaluedecode + 1 /\ (ge_balance_positive_active_resultrightleftvalue) = 0) /\ (ge_balance_negative_active_resultrightleftvalue) = S ge_signed_half_active_resultrightleftvaluedecode))) /\ ((dst_positive_active_resultrightleft) + ge_balance_negative_active_resultrightleftvalue = (dst_negative_active_resultrightleft) + ge_balance_positive_active_resultrightleftvalue))))))))) /\ (((exists dst_positive_code_active_resultrightright dst_positive_scale_active_resultrightright dst_negative_code_active_resultrightright dst_negative_scale_active_resultrightright dst_positive_active_resultrightright dst_negative_active_resultrightright. (((G) = (((((dst_positive_code_active_resultrightright) + (dst_positive_scale_active_resultrightright)) * S ((dst_positive_code_active_resultrightright) + (dst_positive_scale_active_resultrightright)) + ((dst_positive_scale_active_resultrightright) + (dst_positive_scale_active_resultrightright))) + (((dst_negative_code_active_resultrightright) + (dst_negative_scale_active_resultrightright)) * S ((dst_negative_code_active_resultrightright) + (dst_negative_scale_active_resultrightright)) + ((dst_negative_scale_active_resultrightright) + (dst_negative_scale_active_resultrightright)))) * S ((((dst_positive_code_active_resultrightright) + (dst_positive_scale_active_resultrightright)) * S ((dst_positive_code_active_resultrightright) + (dst_positive_scale_active_resultrightright)) + ((dst_positive_scale_active_resultrightright) + (dst_positive_scale_active_resultrightright))) + (((dst_negative_code_active_resultrightright) + (dst_negative_scale_active_resultrightright)) * S ((dst_negative_code_active_resultrightright) + (dst_negative_scale_active_resultrightright)) + ((dst_negative_scale_active_resultrightright) + (dst_negative_scale_active_resultrightright)))) + ((((dst_negative_code_active_resultrightright) + (dst_negative_scale_active_resultrightright)) * S ((dst_negative_code_active_resultrightright) + (dst_negative_scale_active_resultrightright)) + ((dst_negative_scale_active_resultrightright) + (dst_negative_scale_active_resultrightright))) + (((dst_negative_code_active_resultrightright) + (dst_negative_scale_active_resultrightright)) * S ((dst_negative_code_active_resultrightright) + (dst_negative_scale_active_resultrightright)) + ((dst_negative_scale_active_resultrightright) + (dst_negative_scale_active_resultrightright)))))) /\ (((((exists ff_h_pvs_active_resultrightrightpositive. ff_h_pvs_active_resultrightrightpositive + S (dst_positive_active_resultrightright) = S ((S (dc_quotient_active_resultright)) * dst_positive_scale_active_resultrightright)) /\ exists ff_q_pvs_active_resultrightrightpositive. dst_positive_code_active_resultrightright = ff_q_pvs_active_resultrightrightpositive * S ((S (dc_quotient_active_resultright)) * dst_positive_scale_active_resultrightright) + (dst_positive_active_resultrightright))) /\ (((((exists ff_h_pvs_active_resultrightrightnegative. ff_h_pvs_active_resultrightrightnegative + S (dst_negative_active_resultrightright) = S ((S (dc_quotient_active_resultright)) * dst_negative_scale_active_resultrightright)) /\ exists ff_q_pvs_active_resultrightrightnegative. dst_negative_code_active_resultrightright = ff_q_pvs_active_resultrightrightnegative * S ((S (dc_quotient_active_resultright)) * dst_negative_scale_active_resultrightright) + (dst_negative_active_resultrightright))) /\ (exists ge_balance_positive_active_resultrightrightvalue ge_balance_negative_active_resultrightrightvalue. (((((dc_right_active_resultright) = 2 * (ge_balance_positive_active_resultrightrightvalue) /\ (ge_balance_negative_active_resultrightrightvalue) = 0) \/ exists ge_signed_half_active_resultrightrightvaluedecode. (((dc_right_active_resultright) = 2 * ge_signed_half_active_resultrightrightvaluedecode + 1 /\ (ge_balance_positive_active_resultrightrightvalue) = 0) /\ (ge_balance_negative_active_resultrightrightvalue) = S ge_signed_half_active_resultrightrightvaluedecode))) /\ ((dst_positive_active_resultrightright) + ge_balance_negative_active_resultrightrightvalue = (dst_negative_active_resultrightright) + ge_balance_positive_active_resultrightrightvalue))))))))) /\ (exists sto_ap_active_resultrightproduct sto_an_active_resultrightproduct sto_bp_active_resultrightproduct sto_bn_active_resultrightproduct sto_cp_active_resultrightproduct sto_cn_active_resultrightproduct. (((((dc_left_active_resultright) = 2 * (sto_ap_active_resultrightproduct) /\ (sto_an_active_resultrightproduct) = 0) \/ exists ge_signed_half_active_resultrightproductleft. (((dc_left_active_resultright) = 2 * ge_signed_half_active_resultrightproductleft + 1 /\ (sto_ap_active_resultrightproduct) = 0) /\ (sto_an_active_resultrightproduct) = S ge_signed_half_active_resultrightproductleft))) /\ ((((((dc_right_active_resultright) = 2 * (sto_bp_active_resultrightproduct) /\ (sto_bn_active_resultrightproduct) = 0) \/ exists ge_signed_half_active_resultrightproductright. (((dc_right_active_resultright) = 2 * ge_signed_half_active_resultrightproductright + 1 /\ (sto_bp_active_resultrightproduct) = 0) /\ (sto_bn_active_resultrightproduct) = S ge_signed_half_active_resultrightproductright))) /\ ((((((b) = 2 * (sto_cp_active_resultrightproduct) /\ (sto_cn_active_resultrightproduct) = 0) \/ exists ge_signed_half_active_resultrightproductoutput. (((b) = 2 * ge_signed_half_active_resultrightproductoutput + 1 /\ (sto_cp_active_resultrightproduct) = 0) /\ (sto_cn_active_resultrightproduct) = S ge_signed_half_active_resultrightproductoutput))) /\ ((sto_ap_active_resultrightproduct * sto_bp_active_resultrightproduct + sto_an_active_resultrightproduct * sto_bn_active_resultrightproduct) + sto_cn_active_resultrightproduct = (sto_ap_active_resultrightproduct * sto_bn_active_resultrightproduct + sto_an_active_resultrightproduct * sto_bp_active_resultrightproduct) + sto_cp_active_resultrightproduct))))))))))))))) \/ ((((e)=0 \/ ~(exists pvs_factor_active_resultrightnondivisor. (n) = (e) * pvs_factor_active_resultrightnondivisor)) /\ ((b)=0)))) /\ (exists sto_ap_active_resultproduct sto_an_active_resultproduct sto_bp_active_resultproduct sto_bn_active_resultproduct sto_cp_active_resultproduct sto_cn_active_resultproduct. (((((a) = 2 * (sto_ap_active_resultproduct) /\ (sto_an_active_resultproduct) = 0) \/ exists ge_signed_half_active_resultproductleft. (((a) = 2 * ge_signed_half_active_resultproductleft + 1 /\ (sto_ap_active_resultproduct) = 0) /\ (sto_an_active_resultproduct) = S ge_signed_half_active_resultproductleft))) /\ ((((((b) = 2 * (sto_bp_active_resultproduct) /\ (sto_bn_active_resultproduct) = 0) \/ exists ge_signed_half_active_resultproductright. (((b) = 2 * ge_signed_half_active_resultproductright + 1 /\ (sto_bp_active_resultproduct) = 0) /\ (sto_bn_active_resultproduct) = S ge_signed_half_active_resultproductright))) /\ ((((((z) = 2 * (sto_cp_active_resultproduct) /\ (sto_cn_active_resultproduct) = 0) \/ exists ge_signed_half_active_resultproductoutput. (((z) = 2 * ge_signed_half_active_resultproductoutput + 1 /\ (sto_cp_active_resultproduct) = 0) /\ (sto_cn_active_resultproduct) = S ge_signed_half_active_resultproductoutput))) /\ ((sto_ap_active_resultproduct * sto_bp_active_resultproduct + sto_an_active_resultproduct * sto_bn_active_resultproduct) + sto_cn_active_resultproduct = (sto_ap_active_resultproduct * sto_bn_active_resultproduct + sto_an_active_resultproduct * sto_bp_active_resultproduct) + sto_cp_active_resultproduct)))))))))))))))))))