dirichlet_convolution_multiplicative_table

Exact expanded first-order arithmetic statement

forall N F G H. (((~((N)=0)) /\ (((exists dst_positive_code_table_firsttable dst_positive_scale_table_firsttable dst_negative_code_table_firsttable dst_negative_scale_table_firsttable. (((F) = (((((dst_positive_code_table_firsttable) + (dst_positive_scale_table_firsttable)) * S ((dst_positive_code_table_firsttable) + (dst_positive_scale_table_firsttable)) + ((dst_positive_scale_table_firsttable) + (dst_positive_scale_table_firsttable))) + (((dst_negative_code_table_firsttable) + (dst_negative_scale_table_firsttable)) * S ((dst_negative_code_table_firsttable) + (dst_negative_scale_table_firsttable)) + ((dst_negative_scale_table_firsttable) + (dst_negative_scale_table_firsttable)))) * S ((((dst_positive_code_table_firsttable) + (dst_positive_scale_table_firsttable)) * S ((dst_positive_code_table_firsttable) + (dst_positive_scale_table_firsttable)) + ((dst_positive_scale_table_firsttable) + (dst_positive_scale_table_firsttable))) + (((dst_negative_code_table_firsttable) + (dst_negative_scale_table_firsttable)) * S ((dst_negative_code_table_firsttable) + (dst_negative_scale_table_firsttable)) + ((dst_negative_scale_table_firsttable) + (dst_negative_scale_table_firsttable)))) + ((((dst_negative_code_table_firsttable) + (dst_negative_scale_table_firsttable)) * S ((dst_negative_code_table_firsttable) + (dst_negative_scale_table_firsttable)) + ((dst_negative_scale_table_firsttable) + (dst_negative_scale_table_firsttable))) + (((dst_negative_code_table_firsttable) + (dst_negative_scale_table_firsttable)) * S ((dst_negative_code_table_firsttable) + (dst_negative_scale_table_firsttable)) + ((dst_negative_scale_table_firsttable) + (dst_negative_scale_table_firsttable)))))) /\ (forall dst_index_table_firsttable. (exists pvs_le_gap_table_firsttabledomain. pvs_le_gap_table_firsttabledomain + (dst_index_table_firsttable) = (N)) -> exists dst_positive_table_firsttable dst_negative_table_firsttable dst_value_table_firsttable. ((((exists ff_h_pvs_table_firsttableentrypositive. ff_h_pvs_table_firsttableentrypositive + S (dst_positive_table_firsttable) = S ((S (dst_index_table_firsttable)) * dst_positive_scale_table_firsttable)) /\ exists ff_q_pvs_table_firsttableentrypositive. dst_positive_code_table_firsttable = ff_q_pvs_table_firsttableentrypositive * S ((S (dst_index_table_firsttable)) * dst_positive_scale_table_firsttable) + (dst_positive_table_firsttable))) /\ (((((exists ff_h_pvs_table_firsttableentrynegative. ff_h_pvs_table_firsttableentrynegative + S (dst_negative_table_firsttable) = S ((S (dst_index_table_firsttable)) * dst_negative_scale_table_firsttable)) /\ exists ff_q_pvs_table_firsttableentrynegative. dst_negative_code_table_firsttable = ff_q_pvs_table_firsttableentrynegative * S ((S (dst_index_table_firsttable)) * dst_negative_scale_table_firsttable) + (dst_negative_table_firsttable))) /\ (exists ge_balance_positive_table_firsttableentryvalue ge_balance_negative_table_firsttableentryvalue. (((((dst_value_table_firsttable) = 2 * (ge_balance_positive_table_firsttableentryvalue) /\ (ge_balance_negative_table_firsttableentryvalue) = 0) \/ exists ge_signed_half_table_firsttableentryvaluedecode. (((dst_value_table_firsttable) = 2 * ge_signed_half_table_firsttableentryvaluedecode + 1 /\ (ge_balance_positive_table_firsttableentryvalue) = 0) /\ (ge_balance_negative_table_firsttableentryvalue) = S ge_signed_half_table_firsttableentryvaluedecode))) /\ ((dst_positive_table_firsttable) + ge_balance_negative_table_firsttableentryvalue = (dst_negative_table_firsttable) + ge_balance_positive_table_firsttableentryvalue))))))))) /\ (((exists dst_positive_code_table_firstone dst_positive_scale_table_firstone dst_negative_code_table_firstone dst_negative_scale_table_firstone dst_positive_table_firstone dst_negative_table_firstone. (((F) = (((((dst_positive_code_table_firstone) + (dst_positive_scale_table_firstone)) * S ((dst_positive_code_table_firstone) + (dst_positive_scale_table_firstone)) + ((dst_positive_scale_table_firstone) + (dst_positive_scale_table_firstone))) + (((dst_negative_code_table_firstone) + (dst_negative_scale_table_firstone)) * S ((dst_negative_code_table_firstone) + (dst_negative_scale_table_firstone)) + ((dst_negative_scale_table_firstone) + (dst_negative_scale_table_firstone)))) * S ((((dst_positive_code_table_firstone) + (dst_positive_scale_table_firstone)) * S ((dst_positive_code_table_firstone) + (dst_positive_scale_table_firstone)) + ((dst_positive_scale_table_firstone) + (dst_positive_scale_table_firstone))) + (((dst_negative_code_table_firstone) + (dst_negative_scale_table_firstone)) * S ((dst_negative_code_table_firstone) + (dst_negative_scale_table_firstone)) + ((dst_negative_scale_table_firstone) + (dst_negative_scale_table_firstone)))) + ((((dst_negative_code_table_firstone) + (dst_negative_scale_table_firstone)) * S ((dst_negative_code_table_firstone) + (dst_negative_scale_table_firstone)) + ((dst_negative_scale_table_firstone) + (dst_negative_scale_table_firstone))) + (((dst_negative_code_table_firstone) + (dst_negative_scale_table_firstone)) * S ((dst_negative_code_table_firstone) + (dst_negative_scale_table_firstone)) + ((dst_negative_scale_table_firstone) + (dst_negative_scale_table_firstone)))))) /\ (((((exists ff_h_pvs_table_firstonepositive. ff_h_pvs_table_firstonepositive + S (dst_positive_table_firstone) = S ((S (1)) * dst_positive_scale_table_firstone)) /\ exists ff_q_pvs_table_firstonepositive. dst_positive_code_table_firstone = ff_q_pvs_table_firstonepositive * S ((S (1)) * dst_positive_scale_table_firstone) + (dst_positive_table_firstone))) /\ (((((exists ff_h_pvs_table_firstonenegative. ff_h_pvs_table_firstonenegative + S (dst_negative_table_firstone) = S ((S (1)) * dst_negative_scale_table_firstone)) /\ exists ff_q_pvs_table_firstonenegative. dst_negative_code_table_firstone = ff_q_pvs_table_firstonenegative * S ((S (1)) * dst_negative_scale_table_firstone) + (dst_negative_table_firstone))) /\ (exists ge_balance_positive_table_firstonevalue ge_balance_negative_table_firstonevalue. (((((2) = 2 * (ge_balance_positive_table_firstonevalue) /\ (ge_balance_negative_table_firstonevalue) = 0) \/ exists ge_signed_half_table_firstonevaluedecode. (((2) = 2 * ge_signed_half_table_firstonevaluedecode + 1 /\ (ge_balance_positive_table_firstonevalue) = 0) /\ (ge_balance_negative_table_firstonevalue) = S ge_signed_half_table_firstonevaluedecode))) /\ ((dst_positive_table_firstone) + ge_balance_negative_table_firstonevalue = (dst_negative_table_firstone) + ge_balance_positive_table_firstonevalue))))))))) /\ (forall mp_a_table_first mp_b_table_first mp_x_table_first mp_y_table_first mp_z_table_first. ~(mp_a_table_first=0) -> ~(mp_b_table_first=0) -> (exists pvs_le_gap_table_firstbound. pvs_le_gap_table_firstbound + (mp_a_table_first*mp_b_table_first) = (N)) -> (forall frp_divisor_table_firstcoprime. (exists frp_left_factor_table_firstcoprime. mp_a_table_first = frp_divisor_table_firstcoprime * frp_left_factor_table_firstcoprime) -> (exists frp_right_factor_table_firstcoprime. mp_b_table_first = frp_divisor_table_firstcoprime * frp_right_factor_table_firstcoprime) -> frp_divisor_table_firstcoprime = 1) -> (exists dst_positive_code_table_firstfirst dst_positive_scale_table_firstfirst dst_negative_code_table_firstfirst dst_negative_scale_table_firstfirst dst_positive_table_firstfirst dst_negative_table_firstfirst. (((F) = (((((dst_positive_code_table_firstfirst) + (dst_positive_scale_table_firstfirst)) * S ((dst_positive_code_table_firstfirst) + (dst_positive_scale_table_firstfirst)) + ((dst_positive_scale_table_firstfirst) + (dst_positive_scale_table_firstfirst))) + (((dst_negative_code_table_firstfirst) + (dst_negative_scale_table_firstfirst)) * S ((dst_negative_code_table_firstfirst) + (dst_negative_scale_table_firstfirst)) + ((dst_negative_scale_table_firstfirst) + (dst_negative_scale_table_firstfirst)))) * S ((((dst_positive_code_table_firstfirst) + (dst_positive_scale_table_firstfirst)) * S ((dst_positive_code_table_firstfirst) + (dst_positive_scale_table_firstfirst)) + ((dst_positive_scale_table_firstfirst) + (dst_positive_scale_table_firstfirst))) + (((dst_negative_code_table_firstfirst) + (dst_negative_scale_table_firstfirst)) * S ((dst_negative_code_table_firstfirst) + (dst_negative_scale_table_firstfirst)) + ((dst_negative_scale_table_firstfirst) + (dst_negative_scale_table_firstfirst)))) + ((((dst_negative_code_table_firstfirst) + (dst_negative_scale_table_firstfirst)) * S ((dst_negative_code_table_firstfirst) + (dst_negative_scale_table_firstfirst)) + ((dst_negative_scale_table_firstfirst) + (dst_negative_scale_table_firstfirst))) + (((dst_negative_code_table_firstfirst) + (dst_negative_scale_table_firstfirst)) * S ((dst_negative_code_table_firstfirst) + (dst_negative_scale_table_firstfirst)) + ((dst_negative_scale_table_firstfirst) + (dst_negative_scale_table_firstfirst)))))) /\ (((((exists ff_h_pvs_table_firstfirstpositive. ff_h_pvs_table_firstfirstpositive + S (dst_positive_table_firstfirst) = S ((S (mp_a_table_first)) * dst_positive_scale_table_firstfirst)) /\ exists ff_q_pvs_table_firstfirstpositive. dst_positive_code_table_firstfirst = ff_q_pvs_table_firstfirstpositive * S ((S (mp_a_table_first)) * dst_positive_scale_table_firstfirst) + (dst_positive_table_firstfirst))) /\ (((((exists ff_h_pvs_table_firstfirstnegative. ff_h_pvs_table_firstfirstnegative + S (dst_negative_table_firstfirst) = S ((S (mp_a_table_first)) * dst_negative_scale_table_firstfirst)) /\ exists ff_q_pvs_table_firstfirstnegative. dst_negative_code_table_firstfirst = ff_q_pvs_table_firstfirstnegative * S ((S (mp_a_table_first)) * dst_negative_scale_table_firstfirst) + (dst_negative_table_firstfirst))) /\ (exists ge_balance_positive_table_firstfirstvalue ge_balance_negative_table_firstfirstvalue. (((((mp_x_table_first) = 2 * (ge_balance_positive_table_firstfirstvalue) /\ (ge_balance_negative_table_firstfirstvalue) = 0) \/ exists ge_signed_half_table_firstfirstvaluedecode. (((mp_x_table_first) = 2 * ge_signed_half_table_firstfirstvaluedecode + 1 /\ (ge_balance_positive_table_firstfirstvalue) = 0) /\ (ge_balance_negative_table_firstfirstvalue) = S ge_signed_half_table_firstfirstvaluedecode))) /\ ((dst_positive_table_firstfirst) + ge_balance_negative_table_firstfirstvalue = (dst_negative_table_firstfirst) + ge_balance_positive_table_firstfirstvalue))))))))) -> (exists dst_positive_code_table_firstsecond dst_positive_scale_table_firstsecond dst_negative_code_table_firstsecond dst_negative_scale_table_firstsecond dst_positive_table_firstsecond dst_negative_table_firstsecond. (((F) = (((((dst_positive_code_table_firstsecond) + (dst_positive_scale_table_firstsecond)) * S ((dst_positive_code_table_firstsecond) + (dst_positive_scale_table_firstsecond)) + ((dst_positive_scale_table_firstsecond) + (dst_positive_scale_table_firstsecond))) + (((dst_negative_code_table_firstsecond) + (dst_negative_scale_table_firstsecond)) * S ((dst_negative_code_table_firstsecond) + (dst_negative_scale_table_firstsecond)) + ((dst_negative_scale_table_firstsecond) + (dst_negative_scale_table_firstsecond)))) * S ((((dst_positive_code_table_firstsecond) + (dst_positive_scale_table_firstsecond)) * S ((dst_positive_code_table_firstsecond) + (dst_positive_scale_table_firstsecond)) + ((dst_positive_scale_table_firstsecond) + (dst_positive_scale_table_firstsecond))) + (((dst_negative_code_table_firstsecond) + (dst_negative_scale_table_firstsecond)) * S ((dst_negative_code_table_firstsecond) + (dst_negative_scale_table_firstsecond)) + ((dst_negative_scale_table_firstsecond) + (dst_negative_scale_table_firstsecond)))) + ((((dst_negative_code_table_firstsecond) + (dst_negative_scale_table_firstsecond)) * S ((dst_negative_code_table_firstsecond) + (dst_negative_scale_table_firstsecond)) + ((dst_negative_scale_table_firstsecond) + (dst_negative_scale_table_firstsecond))) + (((dst_negative_code_table_firstsecond) + (dst_negative_scale_table_firstsecond)) * S ((dst_negative_code_table_firstsecond) + (dst_negative_scale_table_firstsecond)) + ((dst_negative_scale_table_firstsecond) + (dst_negative_scale_table_firstsecond)))))) /\ (((((exists ff_h_pvs_table_firstsecondpositive. ff_h_pvs_table_firstsecondpositive + S (dst_positive_table_firstsecond) = S ((S (mp_b_table_first)) * dst_positive_scale_table_firstsecond)) /\ exists ff_q_pvs_table_firstsecondpositive. dst_positive_code_table_firstsecond = ff_q_pvs_table_firstsecondpositive * S ((S (mp_b_table_first)) * dst_positive_scale_table_firstsecond) + (dst_positive_table_firstsecond))) /\ (((((exists ff_h_pvs_table_firstsecondnegative. ff_h_pvs_table_firstsecondnegative + S (dst_negative_table_firstsecond) = S ((S (mp_b_table_first)) * dst_negative_scale_table_firstsecond)) /\ exists ff_q_pvs_table_firstsecondnegative. dst_negative_code_table_firstsecond = ff_q_pvs_table_firstsecondnegative * S ((S (mp_b_table_first)) * dst_negative_scale_table_firstsecond) + (dst_negative_table_firstsecond))) /\ (exists ge_balance_positive_table_firstsecondvalue ge_balance_negative_table_firstsecondvalue. (((((mp_y_table_first) = 2 * (ge_balance_positive_table_firstsecondvalue) /\ (ge_balance_negative_table_firstsecondvalue) = 0) \/ exists ge_signed_half_table_firstsecondvaluedecode. (((mp_y_table_first) = 2 * ge_signed_half_table_firstsecondvaluedecode + 1 /\ (ge_balance_positive_table_firstsecondvalue) = 0) /\ (ge_balance_negative_table_firstsecondvalue) = S ge_signed_half_table_firstsecondvaluedecode))) /\ ((dst_positive_table_firstsecond) + ge_balance_negative_table_firstsecondvalue = (dst_negative_table_firstsecond) + ge_balance_positive_table_firstsecondvalue))))))))) -> (exists dst_positive_code_table_firstproduct dst_positive_scale_table_firstproduct dst_negative_code_table_firstproduct dst_negative_scale_table_firstproduct dst_positive_table_firstproduct dst_negative_table_firstproduct. (((F) = (((((dst_positive_code_table_firstproduct) + (dst_positive_scale_table_firstproduct)) * S ((dst_positive_code_table_firstproduct) + (dst_positive_scale_table_firstproduct)) + ((dst_positive_scale_table_firstproduct) + (dst_positive_scale_table_firstproduct))) + (((dst_negative_code_table_firstproduct) + (dst_negative_scale_table_firstproduct)) * S ((dst_negative_code_table_firstproduct) + (dst_negative_scale_table_firstproduct)) + ((dst_negative_scale_table_firstproduct) + (dst_negative_scale_table_firstproduct)))) * S ((((dst_positive_code_table_firstproduct) + (dst_positive_scale_table_firstproduct)) * S ((dst_positive_code_table_firstproduct) + (dst_positive_scale_table_firstproduct)) + ((dst_positive_scale_table_firstproduct) + (dst_positive_scale_table_firstproduct))) + (((dst_negative_code_table_firstproduct) + (dst_negative_scale_table_firstproduct)) * S ((dst_negative_code_table_firstproduct) + (dst_negative_scale_table_firstproduct)) + ((dst_negative_scale_table_firstproduct) + (dst_negative_scale_table_firstproduct)))) + ((((dst_negative_code_table_firstproduct) + (dst_negative_scale_table_firstproduct)) * S ((dst_negative_code_table_firstproduct) + (dst_negative_scale_table_firstproduct)) + ((dst_negative_scale_table_firstproduct) + (dst_negative_scale_table_firstproduct))) + (((dst_negative_code_table_firstproduct) + (dst_negative_scale_table_firstproduct)) * S ((dst_negative_code_table_firstproduct) + (dst_negative_scale_table_firstproduct)) + ((dst_negative_scale_table_firstproduct) + (dst_negative_scale_table_firstproduct)))))) /\ (((((exists ff_h_pvs_table_firstproductpositive. ff_h_pvs_table_firstproductpositive + S (dst_positive_table_firstproduct) = S ((S (mp_a_table_first*mp_b_table_first)) * dst_positive_scale_table_firstproduct)) /\ exists ff_q_pvs_table_firstproductpositive. dst_positive_code_table_firstproduct = ff_q_pvs_table_firstproductpositive * S ((S (mp_a_table_first*mp_b_table_first)) * dst_positive_scale_table_firstproduct) + (dst_positive_table_firstproduct))) /\ (((((exists ff_h_pvs_table_firstproductnegative. ff_h_pvs_table_firstproductnegative + S (dst_negative_table_firstproduct) = S ((S (mp_a_table_first*mp_b_table_first)) * dst_negative_scale_table_firstproduct)) /\ exists ff_q_pvs_table_firstproductnegative. dst_negative_code_table_firstproduct = ff_q_pvs_table_firstproductnegative * S ((S (mp_a_table_first*mp_b_table_first)) * dst_negative_scale_table_firstproduct) + (dst_negative_table_firstproduct))) /\ (exists ge_balance_positive_table_firstproductvalue ge_balance_negative_table_firstproductvalue. (((((mp_z_table_first) = 2 * (ge_balance_positive_table_firstproductvalue) /\ (ge_balance_negative_table_firstproductvalue) = 0) \/ exists ge_signed_half_table_firstproductvaluedecode. (((mp_z_table_first) = 2 * ge_signed_half_table_firstproductvaluedecode + 1 /\ (ge_balance_positive_table_firstproductvalue) = 0) /\ (ge_balance_negative_table_firstproductvalue) = S ge_signed_half_table_firstproductvaluedecode))) /\ ((dst_positive_table_firstproduct) + ge_balance_negative_table_firstproductvalue = (dst_negative_table_firstproduct) + ge_balance_positive_table_firstproductvalue))))))))) -> (exists sto_ap_table_firstlaw sto_an_table_firstlaw sto_bp_table_firstlaw sto_bn_table_firstlaw sto_cp_table_firstlaw sto_cn_table_firstlaw. (((((mp_x_table_first) = 2 * (sto_ap_table_firstlaw) /\ (sto_an_table_firstlaw) = 0) \/ exists ge_signed_half_table_firstlawleft. (((mp_x_table_first) = 2 * ge_signed_half_table_firstlawleft + 1 /\ (sto_ap_table_firstlaw) = 0) /\ (sto_an_table_firstlaw) = S ge_signed_half_table_firstlawleft))) /\ ((((((mp_y_table_first) = 2 * (sto_bp_table_firstlaw) /\ (sto_bn_table_firstlaw) = 0) \/ exists ge_signed_half_table_firstlawright. (((mp_y_table_first) = 2 * ge_signed_half_table_firstlawright + 1 /\ (sto_bp_table_firstlaw) = 0) /\ (sto_bn_table_firstlaw) = S ge_signed_half_table_firstlawright))) /\ ((((((mp_z_table_first) = 2 * (sto_cp_table_firstlaw) /\ (sto_cn_table_firstlaw) = 0) \/ exists ge_signed_half_table_firstlawoutput. (((mp_z_table_first) = 2 * ge_signed_half_table_firstlawoutput + 1 /\ (sto_cp_table_firstlaw) = 0) /\ (sto_cn_table_firstlaw) = S ge_signed_half_table_firstlawoutput))) /\ ((sto_ap_table_firstlaw * sto_bp_table_firstlaw + sto_an_table_firstlaw * sto_bn_table_firstlaw) + sto_cn_table_firstlaw = (sto_ap_table_firstlaw * sto_bn_table_firstlaw + sto_an_table_firstlaw * sto_bp_table_firstlaw) + sto_cp_table_firstlaw)))))))))))))) -> (((~((N)=0)) /\ (((exists dst_positive_code_table_secondtable dst_positive_scale_table_secondtable dst_negative_code_table_secondtable dst_negative_scale_table_secondtable. (((G) = (((((dst_positive_code_table_secondtable) + (dst_positive_scale_table_secondtable)) * S ((dst_positive_code_table_secondtable) + (dst_positive_scale_table_secondtable)) + ((dst_positive_scale_table_secondtable) + (dst_positive_scale_table_secondtable))) + (((dst_negative_code_table_secondtable) + (dst_negative_scale_table_secondtable)) * S ((dst_negative_code_table_secondtable) + (dst_negative_scale_table_secondtable)) + ((dst_negative_scale_table_secondtable) + (dst_negative_scale_table_secondtable)))) * S ((((dst_positive_code_table_secondtable) + (dst_positive_scale_table_secondtable)) * S ((dst_positive_code_table_secondtable) + (dst_positive_scale_table_secondtable)) + ((dst_positive_scale_table_secondtable) + (dst_positive_scale_table_secondtable))) + (((dst_negative_code_table_secondtable) + (dst_negative_scale_table_secondtable)) * S ((dst_negative_code_table_secondtable) + (dst_negative_scale_table_secondtable)) + ((dst_negative_scale_table_secondtable) + (dst_negative_scale_table_secondtable)))) + ((((dst_negative_code_table_secondtable) + (dst_negative_scale_table_secondtable)) * S ((dst_negative_code_table_secondtable) + (dst_negative_scale_table_secondtable)) + ((dst_negative_scale_table_secondtable) + (dst_negative_scale_table_secondtable))) + (((dst_negative_code_table_secondtable) + (dst_negative_scale_table_secondtable)) * S ((dst_negative_code_table_secondtable) + (dst_negative_scale_table_secondtable)) + ((dst_negative_scale_table_secondtable) + (dst_negative_scale_table_secondtable)))))) /\ (forall dst_index_table_secondtable. (exists pvs_le_gap_table_secondtabledomain. pvs_le_gap_table_secondtabledomain + (dst_index_table_secondtable) = (N)) -> exists dst_positive_table_secondtable dst_negative_table_secondtable dst_value_table_secondtable. ((((exists ff_h_pvs_table_secondtableentrypositive. ff_h_pvs_table_secondtableentrypositive + S (dst_positive_table_secondtable) = S ((S (dst_index_table_secondtable)) * dst_positive_scale_table_secondtable)) /\ exists ff_q_pvs_table_secondtableentrypositive. dst_positive_code_table_secondtable = ff_q_pvs_table_secondtableentrypositive * S ((S (dst_index_table_secondtable)) * dst_positive_scale_table_secondtable) + (dst_positive_table_secondtable))) /\ (((((exists ff_h_pvs_table_secondtableentrynegative. ff_h_pvs_table_secondtableentrynegative + S (dst_negative_table_secondtable) = S ((S (dst_index_table_secondtable)) * dst_negative_scale_table_secondtable)) /\ exists ff_q_pvs_table_secondtableentrynegative. dst_negative_code_table_secondtable = ff_q_pvs_table_secondtableentrynegative * S ((S (dst_index_table_secondtable)) * dst_negative_scale_table_secondtable) + (dst_negative_table_secondtable))) /\ (exists ge_balance_positive_table_secondtableentryvalue ge_balance_negative_table_secondtableentryvalue. (((((dst_value_table_secondtable) = 2 * (ge_balance_positive_table_secondtableentryvalue) /\ (ge_balance_negative_table_secondtableentryvalue) = 0) \/ exists ge_signed_half_table_secondtableentryvaluedecode. (((dst_value_table_secondtable) = 2 * ge_signed_half_table_secondtableentryvaluedecode + 1 /\ (ge_balance_positive_table_secondtableentryvalue) = 0) /\ (ge_balance_negative_table_secondtableentryvalue) = S ge_signed_half_table_secondtableentryvaluedecode))) /\ ((dst_positive_table_secondtable) + ge_balance_negative_table_secondtableentryvalue = (dst_negative_table_secondtable) + ge_balance_positive_table_secondtableentryvalue))))))))) /\ (((exists dst_positive_code_table_secondone dst_positive_scale_table_secondone dst_negative_code_table_secondone dst_negative_scale_table_secondone dst_positive_table_secondone dst_negative_table_secondone. (((G) = (((((dst_positive_code_table_secondone) + (dst_positive_scale_table_secondone)) * S ((dst_positive_code_table_secondone) + (dst_positive_scale_table_secondone)) + ((dst_positive_scale_table_secondone) + (dst_positive_scale_table_secondone))) + (((dst_negative_code_table_secondone) + (dst_negative_scale_table_secondone)) * S ((dst_negative_code_table_secondone) + (dst_negative_scale_table_secondone)) + ((dst_negative_scale_table_secondone) + (dst_negative_scale_table_secondone)))) * S ((((dst_positive_code_table_secondone) + (dst_positive_scale_table_secondone)) * S ((dst_positive_code_table_secondone) + (dst_positive_scale_table_secondone)) + ((dst_positive_scale_table_secondone) + (dst_positive_scale_table_secondone))) + (((dst_negative_code_table_secondone) + (dst_negative_scale_table_secondone)) * S ((dst_negative_code_table_secondone) + (dst_negative_scale_table_secondone)) + ((dst_negative_scale_table_secondone) + (dst_negative_scale_table_secondone)))) + ((((dst_negative_code_table_secondone) + (dst_negative_scale_table_secondone)) * S ((dst_negative_code_table_secondone) + (dst_negative_scale_table_secondone)) + ((dst_negative_scale_table_secondone) + (dst_negative_scale_table_secondone))) + (((dst_negative_code_table_secondone) + (dst_negative_scale_table_secondone)) * S ((dst_negative_code_table_secondone) + (dst_negative_scale_table_secondone)) + ((dst_negative_scale_table_secondone) + (dst_negative_scale_table_secondone)))))) /\ (((((exists ff_h_pvs_table_secondonepositive. ff_h_pvs_table_secondonepositive + S (dst_positive_table_secondone) = S ((S (1)) * dst_positive_scale_table_secondone)) /\ exists ff_q_pvs_table_secondonepositive. dst_positive_code_table_secondone = ff_q_pvs_table_secondonepositive * S ((S (1)) * dst_positive_scale_table_secondone) + (dst_positive_table_secondone))) /\ (((((exists ff_h_pvs_table_secondonenegative. ff_h_pvs_table_secondonenegative + S (dst_negative_table_secondone) = S ((S (1)) * dst_negative_scale_table_secondone)) /\ exists ff_q_pvs_table_secondonenegative. dst_negative_code_table_secondone = ff_q_pvs_table_secondonenegative * S ((S (1)) * dst_negative_scale_table_secondone) + (dst_negative_table_secondone))) /\ (exists ge_balance_positive_table_secondonevalue ge_balance_negative_table_secondonevalue. (((((2) = 2 * (ge_balance_positive_table_secondonevalue) /\ (ge_balance_negative_table_secondonevalue) = 0) \/ exists ge_signed_half_table_secondonevaluedecode. (((2) = 2 * ge_signed_half_table_secondonevaluedecode + 1 /\ (ge_balance_positive_table_secondonevalue) = 0) /\ (ge_balance_negative_table_secondonevalue) = S ge_signed_half_table_secondonevaluedecode))) /\ ((dst_positive_table_secondone) + ge_balance_negative_table_secondonevalue = (dst_negative_table_secondone) + ge_balance_positive_table_secondonevalue))))))))) /\ (forall mp_a_table_second mp_b_table_second mp_x_table_second mp_y_table_second mp_z_table_second. ~(mp_a_table_second=0) -> ~(mp_b_table_second=0) -> (exists pvs_le_gap_table_secondbound. pvs_le_gap_table_secondbound + (mp_a_table_second*mp_b_table_second) = (N)) -> (forall frp_divisor_table_secondcoprime. (exists frp_left_factor_table_secondcoprime. mp_a_table_second = frp_divisor_table_secondcoprime * frp_left_factor_table_secondcoprime) -> (exists frp_right_factor_table_secondcoprime. mp_b_table_second = frp_divisor_table_secondcoprime * frp_right_factor_table_secondcoprime) -> frp_divisor_table_secondcoprime = 1) -> (exists dst_positive_code_table_secondfirst dst_positive_scale_table_secondfirst dst_negative_code_table_secondfirst dst_negative_scale_table_secondfirst dst_positive_table_secondfirst dst_negative_table_secondfirst. (((G) = (((((dst_positive_code_table_secondfirst) + (dst_positive_scale_table_secondfirst)) * S ((dst_positive_code_table_secondfirst) + (dst_positive_scale_table_secondfirst)) + ((dst_positive_scale_table_secondfirst) + (dst_positive_scale_table_secondfirst))) + (((dst_negative_code_table_secondfirst) + (dst_negative_scale_table_secondfirst)) * S ((dst_negative_code_table_secondfirst) + (dst_negative_scale_table_secondfirst)) + ((dst_negative_scale_table_secondfirst) + (dst_negative_scale_table_secondfirst)))) * S ((((dst_positive_code_table_secondfirst) + (dst_positive_scale_table_secondfirst)) * S ((dst_positive_code_table_secondfirst) + (dst_positive_scale_table_secondfirst)) + ((dst_positive_scale_table_secondfirst) + (dst_positive_scale_table_secondfirst))) + (((dst_negative_code_table_secondfirst) + (dst_negative_scale_table_secondfirst)) * S ((dst_negative_code_table_secondfirst) + (dst_negative_scale_table_secondfirst)) + ((dst_negative_scale_table_secondfirst) + (dst_negative_scale_table_secondfirst)))) + ((((dst_negative_code_table_secondfirst) + (dst_negative_scale_table_secondfirst)) * S ((dst_negative_code_table_secondfirst) + (dst_negative_scale_table_secondfirst)) + ((dst_negative_scale_table_secondfirst) + (dst_negative_scale_table_secondfirst))) + (((dst_negative_code_table_secondfirst) + (dst_negative_scale_table_secondfirst)) * S ((dst_negative_code_table_secondfirst) + (dst_negative_scale_table_secondfirst)) + ((dst_negative_scale_table_secondfirst) + (dst_negative_scale_table_secondfirst)))))) /\ (((((exists ff_h_pvs_table_secondfirstpositive. ff_h_pvs_table_secondfirstpositive + S (dst_positive_table_secondfirst) = S ((S (mp_a_table_second)) * dst_positive_scale_table_secondfirst)) /\ exists ff_q_pvs_table_secondfirstpositive. dst_positive_code_table_secondfirst = ff_q_pvs_table_secondfirstpositive * S ((S (mp_a_table_second)) * dst_positive_scale_table_secondfirst) + (dst_positive_table_secondfirst))) /\ (((((exists ff_h_pvs_table_secondfirstnegative. ff_h_pvs_table_secondfirstnegative + S (dst_negative_table_secondfirst) = S ((S (mp_a_table_second)) * dst_negative_scale_table_secondfirst)) /\ exists ff_q_pvs_table_secondfirstnegative. dst_negative_code_table_secondfirst = ff_q_pvs_table_secondfirstnegative * S ((S (mp_a_table_second)) * dst_negative_scale_table_secondfirst) + (dst_negative_table_secondfirst))) /\ (exists ge_balance_positive_table_secondfirstvalue ge_balance_negative_table_secondfirstvalue. (((((mp_x_table_second) = 2 * (ge_balance_positive_table_secondfirstvalue) /\ (ge_balance_negative_table_secondfirstvalue) = 0) \/ exists ge_signed_half_table_secondfirstvaluedecode. (((mp_x_table_second) = 2 * ge_signed_half_table_secondfirstvaluedecode + 1 /\ (ge_balance_positive_table_secondfirstvalue) = 0) /\ (ge_balance_negative_table_secondfirstvalue) = S ge_signed_half_table_secondfirstvaluedecode))) /\ ((dst_positive_table_secondfirst) + ge_balance_negative_table_secondfirstvalue = (dst_negative_table_secondfirst) + ge_balance_positive_table_secondfirstvalue))))))))) -> (exists dst_positive_code_table_secondsecond dst_positive_scale_table_secondsecond dst_negative_code_table_secondsecond dst_negative_scale_table_secondsecond dst_positive_table_secondsecond dst_negative_table_secondsecond. (((G) = (((((dst_positive_code_table_secondsecond) + (dst_positive_scale_table_secondsecond)) * S ((dst_positive_code_table_secondsecond) + (dst_positive_scale_table_secondsecond)) + ((dst_positive_scale_table_secondsecond) + (dst_positive_scale_table_secondsecond))) + (((dst_negative_code_table_secondsecond) + (dst_negative_scale_table_secondsecond)) * S ((dst_negative_code_table_secondsecond) + (dst_negative_scale_table_secondsecond)) + ((dst_negative_scale_table_secondsecond) + (dst_negative_scale_table_secondsecond)))) * S ((((dst_positive_code_table_secondsecond) + (dst_positive_scale_table_secondsecond)) * S ((dst_positive_code_table_secondsecond) + (dst_positive_scale_table_secondsecond)) + ((dst_positive_scale_table_secondsecond) + (dst_positive_scale_table_secondsecond))) + (((dst_negative_code_table_secondsecond) + (dst_negative_scale_table_secondsecond)) * S ((dst_negative_code_table_secondsecond) + (dst_negative_scale_table_secondsecond)) + ((dst_negative_scale_table_secondsecond) + (dst_negative_scale_table_secondsecond)))) + ((((dst_negative_code_table_secondsecond) + (dst_negative_scale_table_secondsecond)) * S ((dst_negative_code_table_secondsecond) + (dst_negative_scale_table_secondsecond)) + ((dst_negative_scale_table_secondsecond) + (dst_negative_scale_table_secondsecond))) + (((dst_negative_code_table_secondsecond) + (dst_negative_scale_table_secondsecond)) * S ((dst_negative_code_table_secondsecond) + (dst_negative_scale_table_secondsecond)) + ((dst_negative_scale_table_secondsecond) + (dst_negative_scale_table_secondsecond)))))) /\ (((((exists ff_h_pvs_table_secondsecondpositive. ff_h_pvs_table_secondsecondpositive + S (dst_positive_table_secondsecond) = S ((S (mp_b_table_second)) * dst_positive_scale_table_secondsecond)) /\ exists ff_q_pvs_table_secondsecondpositive. dst_positive_code_table_secondsecond = ff_q_pvs_table_secondsecondpositive * S ((S (mp_b_table_second)) * dst_positive_scale_table_secondsecond) + (dst_positive_table_secondsecond))) /\ (((((exists ff_h_pvs_table_secondsecondnegative. ff_h_pvs_table_secondsecondnegative + S (dst_negative_table_secondsecond) = S ((S (mp_b_table_second)) * dst_negative_scale_table_secondsecond)) /\ exists ff_q_pvs_table_secondsecondnegative. dst_negative_code_table_secondsecond = ff_q_pvs_table_secondsecondnegative * S ((S (mp_b_table_second)) * dst_negative_scale_table_secondsecond) + (dst_negative_table_secondsecond))) /\ (exists ge_balance_positive_table_secondsecondvalue ge_balance_negative_table_secondsecondvalue. (((((mp_y_table_second) = 2 * (ge_balance_positive_table_secondsecondvalue) /\ (ge_balance_negative_table_secondsecondvalue) = 0) \/ exists ge_signed_half_table_secondsecondvaluedecode. (((mp_y_table_second) = 2 * ge_signed_half_table_secondsecondvaluedecode + 1 /\ (ge_balance_positive_table_secondsecondvalue) = 0) /\ (ge_balance_negative_table_secondsecondvalue) = S ge_signed_half_table_secondsecondvaluedecode))) /\ ((dst_positive_table_secondsecond) + ge_balance_negative_table_secondsecondvalue = (dst_negative_table_secondsecond) + ge_balance_positive_table_secondsecondvalue))))))))) -> (exists dst_positive_code_table_secondproduct dst_positive_scale_table_secondproduct dst_negative_code_table_secondproduct dst_negative_scale_table_secondproduct dst_positive_table_secondproduct dst_negative_table_secondproduct. (((G) = (((((dst_positive_code_table_secondproduct) + (dst_positive_scale_table_secondproduct)) * S ((dst_positive_code_table_secondproduct) + (dst_positive_scale_table_secondproduct)) + ((dst_positive_scale_table_secondproduct) + (dst_positive_scale_table_secondproduct))) + (((dst_negative_code_table_secondproduct) + (dst_negative_scale_table_secondproduct)) * S ((dst_negative_code_table_secondproduct) + (dst_negative_scale_table_secondproduct)) + ((dst_negative_scale_table_secondproduct) + (dst_negative_scale_table_secondproduct)))) * S ((((dst_positive_code_table_secondproduct) + (dst_positive_scale_table_secondproduct)) * S ((dst_positive_code_table_secondproduct) + (dst_positive_scale_table_secondproduct)) + ((dst_positive_scale_table_secondproduct) + (dst_positive_scale_table_secondproduct))) + (((dst_negative_code_table_secondproduct) + (dst_negative_scale_table_secondproduct)) * S ((dst_negative_code_table_secondproduct) + (dst_negative_scale_table_secondproduct)) + ((dst_negative_scale_table_secondproduct) + (dst_negative_scale_table_secondproduct)))) + ((((dst_negative_code_table_secondproduct) + (dst_negative_scale_table_secondproduct)) * S ((dst_negative_code_table_secondproduct) + (dst_negative_scale_table_secondproduct)) + ((dst_negative_scale_table_secondproduct) + (dst_negative_scale_table_secondproduct))) + (((dst_negative_code_table_secondproduct) + (dst_negative_scale_table_secondproduct)) * S ((dst_negative_code_table_secondproduct) + (dst_negative_scale_table_secondproduct)) + ((dst_negative_scale_table_secondproduct) + (dst_negative_scale_table_secondproduct)))))) /\ (((((exists ff_h_pvs_table_secondproductpositive. ff_h_pvs_table_secondproductpositive + S (dst_positive_table_secondproduct) = S ((S (mp_a_table_second*mp_b_table_second)) * dst_positive_scale_table_secondproduct)) /\ exists ff_q_pvs_table_secondproductpositive. dst_positive_code_table_secondproduct = ff_q_pvs_table_secondproductpositive * S ((S (mp_a_table_second*mp_b_table_second)) * dst_positive_scale_table_secondproduct) + (dst_positive_table_secondproduct))) /\ (((((exists ff_h_pvs_table_secondproductnegative. ff_h_pvs_table_secondproductnegative + S (dst_negative_table_secondproduct) = S ((S (mp_a_table_second*mp_b_table_second)) * dst_negative_scale_table_secondproduct)) /\ exists ff_q_pvs_table_secondproductnegative. dst_negative_code_table_secondproduct = ff_q_pvs_table_secondproductnegative * S ((S (mp_a_table_second*mp_b_table_second)) * dst_negative_scale_table_secondproduct) + (dst_negative_table_secondproduct))) /\ (exists ge_balance_positive_table_secondproductvalue ge_balance_negative_table_secondproductvalue. (((((mp_z_table_second) = 2 * (ge_balance_positive_table_secondproductvalue) /\ (ge_balance_negative_table_secondproductvalue) = 0) \/ exists ge_signed_half_table_secondproductvaluedecode. (((mp_z_table_second) = 2 * ge_signed_half_table_secondproductvaluedecode + 1 /\ (ge_balance_positive_table_secondproductvalue) = 0) /\ (ge_balance_negative_table_secondproductvalue) = S ge_signed_half_table_secondproductvaluedecode))) /\ ((dst_positive_table_secondproduct) + ge_balance_negative_table_secondproductvalue = (dst_negative_table_secondproduct) + ge_balance_positive_table_secondproductvalue))))))))) -> (exists sto_ap_table_secondlaw sto_an_table_secondlaw sto_bp_table_secondlaw sto_bn_table_secondlaw sto_cp_table_secondlaw sto_cn_table_secondlaw. (((((mp_x_table_second) = 2 * (sto_ap_table_secondlaw) /\ (sto_an_table_secondlaw) = 0) \/ exists ge_signed_half_table_secondlawleft. (((mp_x_table_second) = 2 * ge_signed_half_table_secondlawleft + 1 /\ (sto_ap_table_secondlaw) = 0) /\ (sto_an_table_secondlaw) = S ge_signed_half_table_secondlawleft))) /\ ((((((mp_y_table_second) = 2 * (sto_bp_table_secondlaw) /\ (sto_bn_table_secondlaw) = 0) \/ exists ge_signed_half_table_secondlawright. (((mp_y_table_second) = 2 * ge_signed_half_table_secondlawright + 1 /\ (sto_bp_table_secondlaw) = 0) /\ (sto_bn_table_secondlaw) = S ge_signed_half_table_secondlawright))) /\ ((((((mp_z_table_second) = 2 * (sto_cp_table_secondlaw) /\ (sto_cn_table_secondlaw) = 0) \/ exists ge_signed_half_table_secondlawoutput. (((mp_z_table_second) = 2 * ge_signed_half_table_secondlawoutput + 1 /\ (sto_cp_table_secondlaw) = 0) /\ (sto_cn_table_secondlaw) = S ge_signed_half_table_secondlawoutput))) /\ ((sto_ap_table_secondlaw * sto_bp_table_secondlaw + sto_an_table_secondlaw * sto_bn_table_secondlaw) + sto_cn_table_secondlaw = (sto_ap_table_secondlaw * sto_bn_table_secondlaw + sto_an_table_secondlaw * sto_bp_table_secondlaw) + sto_cp_table_secondlaw)))))))))))))) -> (((exists dst_positive_code_table_convolutionleft dst_positive_scale_table_convolutionleft dst_negative_code_table_convolutionleft dst_negative_scale_table_convolutionleft. (((F) = (((((dst_positive_code_table_convolutionleft) + (dst_positive_scale_table_convolutionleft)) * S ((dst_positive_code_table_convolutionleft) + (dst_positive_scale_table_convolutionleft)) + ((dst_positive_scale_table_convolutionleft) + (dst_positive_scale_table_convolutionleft))) + (((dst_negative_code_table_convolutionleft) + (dst_negative_scale_table_convolutionleft)) * S ((dst_negative_code_table_convolutionleft) + (dst_negative_scale_table_convolutionleft)) + ((dst_negative_scale_table_convolutionleft) + (dst_negative_scale_table_convolutionleft)))) * S ((((dst_positive_code_table_convolutionleft) + (dst_positive_scale_table_convolutionleft)) * S ((dst_positive_code_table_convolutionleft) + (dst_positive_scale_table_convolutionleft)) + ((dst_positive_scale_table_convolutionleft) + (dst_positive_scale_table_convolutionleft))) + (((dst_negative_code_table_convolutionleft) + (dst_negative_scale_table_convolutionleft)) * S ((dst_negative_code_table_convolutionleft) + (dst_negative_scale_table_convolutionleft)) + ((dst_negative_scale_table_convolutionleft) + (dst_negative_scale_table_convolutionleft)))) + ((((dst_negative_code_table_convolutionleft) + (dst_negative_scale_table_convolutionleft)) * S ((dst_negative_code_table_convolutionleft) + (dst_negative_scale_table_convolutionleft)) + ((dst_negative_scale_table_convolutionleft) + (dst_negative_scale_table_convolutionleft))) + (((dst_negative_code_table_convolutionleft) + (dst_negative_scale_table_convolutionleft)) * S ((dst_negative_code_table_convolutionleft) + (dst_negative_scale_table_convolutionleft)) + ((dst_negative_scale_table_convolutionleft) + (dst_negative_scale_table_convolutionleft)))))) /\ (forall dst_index_table_convolutionleft. (exists pvs_le_gap_table_convolutionleftdomain. pvs_le_gap_table_convolutionleftdomain + (dst_index_table_convolutionleft) = (N)) -> exists dst_positive_table_convolutionleft dst_negative_table_convolutionleft dst_value_table_convolutionleft. ((((exists ff_h_pvs_table_convolutionleftentrypositive. ff_h_pvs_table_convolutionleftentrypositive + S (dst_positive_table_convolutionleft) = S ((S (dst_index_table_convolutionleft)) * dst_positive_scale_table_convolutionleft)) /\ exists ff_q_pvs_table_convolutionleftentrypositive. dst_positive_code_table_convolutionleft = ff_q_pvs_table_convolutionleftentrypositive * S ((S (dst_index_table_convolutionleft)) * dst_positive_scale_table_convolutionleft) + (dst_positive_table_convolutionleft))) /\ (((((exists ff_h_pvs_table_convolutionleftentrynegative. ff_h_pvs_table_convolutionleftentrynegative + S (dst_negative_table_convolutionleft) = S ((S (dst_index_table_convolutionleft)) * dst_negative_scale_table_convolutionleft)) /\ exists ff_q_pvs_table_convolutionleftentrynegative. dst_negative_code_table_convolutionleft = ff_q_pvs_table_convolutionleftentrynegative * S ((S (dst_index_table_convolutionleft)) * dst_negative_scale_table_convolutionleft) + (dst_negative_table_convolutionleft))) /\ (exists ge_balance_positive_table_convolutionleftentryvalue ge_balance_negative_table_convolutionleftentryvalue. (((((dst_value_table_convolutionleft) = 2 * (ge_balance_positive_table_convolutionleftentryvalue) /\ (ge_balance_negative_table_convolutionleftentryvalue) = 0) \/ exists ge_signed_half_table_convolutionleftentryvaluedecode. (((dst_value_table_convolutionleft) = 2 * ge_signed_half_table_convolutionleftentryvaluedecode + 1 /\ (ge_balance_positive_table_convolutionleftentryvalue) = 0) /\ (ge_balance_negative_table_convolutionleftentryvalue) = S ge_signed_half_table_convolutionleftentryvaluedecode))) /\ ((dst_positive_table_convolutionleft) + ge_balance_negative_table_convolutionleftentryvalue = (dst_negative_table_convolutionleft) + ge_balance_positive_table_convolutionleftentryvalue))))))))) /\ (((exists dst_positive_code_table_convolutionright dst_positive_scale_table_convolutionright dst_negative_code_table_convolutionright dst_negative_scale_table_convolutionright. (((G) = (((((dst_positive_code_table_convolutionright) + (dst_positive_scale_table_convolutionright)) * S ((dst_positive_code_table_convolutionright) + (dst_positive_scale_table_convolutionright)) + ((dst_positive_scale_table_convolutionright) + (dst_positive_scale_table_convolutionright))) + (((dst_negative_code_table_convolutionright) + (dst_negative_scale_table_convolutionright)) * S ((dst_negative_code_table_convolutionright) + (dst_negative_scale_table_convolutionright)) + ((dst_negative_scale_table_convolutionright) + (dst_negative_scale_table_convolutionright)))) * S ((((dst_positive_code_table_convolutionright) + (dst_positive_scale_table_convolutionright)) * S ((dst_positive_code_table_convolutionright) + (dst_positive_scale_table_convolutionright)) + ((dst_positive_scale_table_convolutionright) + (dst_positive_scale_table_convolutionright))) + (((dst_negative_code_table_convolutionright) + (dst_negative_scale_table_convolutionright)) * S ((dst_negative_code_table_convolutionright) + (dst_negative_scale_table_convolutionright)) + ((dst_negative_scale_table_convolutionright) + (dst_negative_scale_table_convolutionright)))) + ((((dst_negative_code_table_convolutionright) + (dst_negative_scale_table_convolutionright)) * S ((dst_negative_code_table_convolutionright) + (dst_negative_scale_table_convolutionright)) + ((dst_negative_scale_table_convolutionright) + (dst_negative_scale_table_convolutionright))) + (((dst_negative_code_table_convolutionright) + (dst_negative_scale_table_convolutionright)) * S ((dst_negative_code_table_convolutionright) + (dst_negative_scale_table_convolutionright)) + ((dst_negative_scale_table_convolutionright) + (dst_negative_scale_table_convolutionright)))))) /\ (forall dst_index_table_convolutionright. (exists pvs_le_gap_table_convolutionrightdomain. pvs_le_gap_table_convolutionrightdomain + (dst_index_table_convolutionright) = (N)) -> exists dst_positive_table_convolutionright dst_negative_table_convolutionright dst_value_table_convolutionright. ((((exists ff_h_pvs_table_convolutionrightentrypositive. ff_h_pvs_table_convolutionrightentrypositive + S (dst_positive_table_convolutionright) = S ((S (dst_index_table_convolutionright)) * dst_positive_scale_table_convolutionright)) /\ exists ff_q_pvs_table_convolutionrightentrypositive. dst_positive_code_table_convolutionright = ff_q_pvs_table_convolutionrightentrypositive * S ((S (dst_index_table_convolutionright)) * dst_positive_scale_table_convolutionright) + (dst_positive_table_convolutionright))) /\ (((((exists ff_h_pvs_table_convolutionrightentrynegative. ff_h_pvs_table_convolutionrightentrynegative + S (dst_negative_table_convolutionright) = S ((S (dst_index_table_convolutionright)) * dst_negative_scale_table_convolutionright)) /\ exists ff_q_pvs_table_convolutionrightentrynegative. dst_negative_code_table_convolutionright = ff_q_pvs_table_convolutionrightentrynegative * S ((S (dst_index_table_convolutionright)) * dst_negative_scale_table_convolutionright) + (dst_negative_table_convolutionright))) /\ (exists ge_balance_positive_table_convolutionrightentryvalue ge_balance_negative_table_convolutionrightentryvalue. (((((dst_value_table_convolutionright) = 2 * (ge_balance_positive_table_convolutionrightentryvalue) /\ (ge_balance_negative_table_convolutionrightentryvalue) = 0) \/ exists ge_signed_half_table_convolutionrightentryvaluedecode. (((dst_value_table_convolutionright) = 2 * ge_signed_half_table_convolutionrightentryvaluedecode + 1 /\ (ge_balance_positive_table_convolutionrightentryvalue) = 0) /\ (ge_balance_negative_table_convolutionrightentryvalue) = S ge_signed_half_table_convolutionrightentryvaluedecode))) /\ ((dst_positive_table_convolutionright) + ge_balance_negative_table_convolutionrightentryvalue = (dst_negative_table_convolutionright) + ge_balance_positive_table_convolutionrightentryvalue))))))))) /\ (((exists dst_positive_code_table_convolutiontable dst_positive_scale_table_convolutiontable dst_negative_code_table_convolutiontable dst_negative_scale_table_convolutiontable. (((H) = (((((dst_positive_code_table_convolutiontable) + (dst_positive_scale_table_convolutiontable)) * S ((dst_positive_code_table_convolutiontable) + (dst_positive_scale_table_convolutiontable)) + ((dst_positive_scale_table_convolutiontable) + (dst_positive_scale_table_convolutiontable))) + (((dst_negative_code_table_convolutiontable) + (dst_negative_scale_table_convolutiontable)) * S ((dst_negative_code_table_convolutiontable) + (dst_negative_scale_table_convolutiontable)) + ((dst_negative_scale_table_convolutiontable) + (dst_negative_scale_table_convolutiontable)))) * S ((((dst_positive_code_table_convolutiontable) + (dst_positive_scale_table_convolutiontable)) * S ((dst_positive_code_table_convolutiontable) + (dst_positive_scale_table_convolutiontable)) + ((dst_positive_scale_table_convolutiontable) + (dst_positive_scale_table_convolutiontable))) + (((dst_negative_code_table_convolutiontable) + (dst_negative_scale_table_convolutiontable)) * S ((dst_negative_code_table_convolutiontable) + (dst_negative_scale_table_convolutiontable)) + ((dst_negative_scale_table_convolutiontable) + (dst_negative_scale_table_convolutiontable)))) + ((((dst_negative_code_table_convolutiontable) + (dst_negative_scale_table_convolutiontable)) * S ((dst_negative_code_table_convolutiontable) + (dst_negative_scale_table_convolutiontable)) + ((dst_negative_scale_table_convolutiontable) + (dst_negative_scale_table_convolutiontable))) + (((dst_negative_code_table_convolutiontable) + (dst_negative_scale_table_convolutiontable)) * S ((dst_negative_code_table_convolutiontable) + (dst_negative_scale_table_convolutiontable)) + ((dst_negative_scale_table_convolutiontable) + (dst_negative_scale_table_convolutiontable)))))) /\ (forall dst_index_table_convolutiontable. (exists pvs_le_gap_table_convolutiontabledomain. pvs_le_gap_table_convolutiontabledomain + (dst_index_table_convolutiontable) = (N)) -> exists dst_positive_table_convolutiontable dst_negative_table_convolutiontable dst_value_table_convolutiontable. ((((exists ff_h_pvs_table_convolutiontableentrypositive. ff_h_pvs_table_convolutiontableentrypositive + S (dst_positive_table_convolutiontable) = S ((S (dst_index_table_convolutiontable)) * dst_positive_scale_table_convolutiontable)) /\ exists ff_q_pvs_table_convolutiontableentrypositive. dst_positive_code_table_convolutiontable = ff_q_pvs_table_convolutiontableentrypositive * S ((S (dst_index_table_convolutiontable)) * dst_positive_scale_table_convolutiontable) + (dst_positive_table_convolutiontable))) /\ (((((exists ff_h_pvs_table_convolutiontableentrynegative. ff_h_pvs_table_convolutiontableentrynegative + S (dst_negative_table_convolutiontable) = S ((S (dst_index_table_convolutiontable)) * dst_negative_scale_table_convolutiontable)) /\ exists ff_q_pvs_table_convolutiontableentrynegative. dst_negative_code_table_convolutiontable = ff_q_pvs_table_convolutiontableentrynegative * S ((S (dst_index_table_convolutiontable)) * dst_negative_scale_table_convolutiontable) + (dst_negative_table_convolutiontable))) /\ (exists ge_balance_positive_table_convolutiontableentryvalue ge_balance_negative_table_convolutiontableentryvalue. (((((dst_value_table_convolutiontable) = 2 * (ge_balance_positive_table_convolutiontableentryvalue) /\ (ge_balance_negative_table_convolutiontableentryvalue) = 0) \/ exists ge_signed_half_table_convolutiontableentryvaluedecode. (((dst_value_table_convolutiontable) = 2 * ge_signed_half_table_convolutiontableentryvaluedecode + 1 /\ (ge_balance_positive_table_convolutiontableentryvalue) = 0) /\ (ge_balance_negative_table_convolutiontableentryvalue) = S ge_signed_half_table_convolutiontableentryvaluedecode))) /\ ((dst_positive_table_convolutiontable) + ge_balance_negative_table_convolutiontableentryvalue = (dst_negative_table_convolutiontable) + ge_balance_positive_table_convolutiontableentryvalue))))))))) /\ (forall dc_input_table_convolution dc_output_table_convolution. ~(dc_input_table_convolution=0) -> (exists pvs_le_gap_table_convolutiondomain. pvs_le_gap_table_convolutiondomain + (dc_input_table_convolution) = (N)) -> (exists dst_positive_code_table_convolutionlookup dst_positive_scale_table_convolutionlookup dst_negative_code_table_convolutionlookup dst_negative_scale_table_convolutionlookup dst_positive_table_convolutionlookup dst_negative_table_convolutionlookup. (((H) = (((((dst_positive_code_table_convolutionlookup) + (dst_positive_scale_table_convolutionlookup)) * S ((dst_positive_code_table_convolutionlookup) + (dst_positive_scale_table_convolutionlookup)) + ((dst_positive_scale_table_convolutionlookup) + (dst_positive_scale_table_convolutionlookup))) + (((dst_negative_code_table_convolutionlookup) + (dst_negative_scale_table_convolutionlookup)) * S ((dst_negative_code_table_convolutionlookup) + (dst_negative_scale_table_convolutionlookup)) + ((dst_negative_scale_table_convolutionlookup) + (dst_negative_scale_table_convolutionlookup)))) * S ((((dst_positive_code_table_convolutionlookup) + (dst_positive_scale_table_convolutionlookup)) * S ((dst_positive_code_table_convolutionlookup) + (dst_positive_scale_table_convolutionlookup)) + ((dst_positive_scale_table_convolutionlookup) + (dst_positive_scale_table_convolutionlookup))) + (((dst_negative_code_table_convolutionlookup) + (dst_negative_scale_table_convolutionlookup)) * S ((dst_negative_code_table_convolutionlookup) + (dst_negative_scale_table_convolutionlookup)) + ((dst_negative_scale_table_convolutionlookup) + (dst_negative_scale_table_convolutionlookup)))) + ((((dst_negative_code_table_convolutionlookup) + (dst_negative_scale_table_convolutionlookup)) * S ((dst_negative_code_table_convolutionlookup) + (dst_negative_scale_table_convolutionlookup)) + ((dst_negative_scale_table_convolutionlookup) + (dst_negative_scale_table_convolutionlookup))) + (((dst_negative_code_table_convolutionlookup) + (dst_negative_scale_table_convolutionlookup)) * S ((dst_negative_code_table_convolutionlookup) + (dst_negative_scale_table_convolutionlookup)) + ((dst_negative_scale_table_convolutionlookup) + (dst_negative_scale_table_convolutionlookup)))))) /\ (((((exists ff_h_pvs_table_convolutionlookuppositive. ff_h_pvs_table_convolutionlookuppositive + S (dst_positive_table_convolutionlookup) = S ((S (dc_input_table_convolution)) * dst_positive_scale_table_convolutionlookup)) /\ exists ff_q_pvs_table_convolutionlookuppositive. dst_positive_code_table_convolutionlookup = ff_q_pvs_table_convolutionlookuppositive * S ((S (dc_input_table_convolution)) * dst_positive_scale_table_convolutionlookup) + (dst_positive_table_convolutionlookup))) /\ (((((exists ff_h_pvs_table_convolutionlookupnegative. ff_h_pvs_table_convolutionlookupnegative + S (dst_negative_table_convolutionlookup) = S ((S (dc_input_table_convolution)) * dst_negative_scale_table_convolutionlookup)) /\ exists ff_q_pvs_table_convolutionlookupnegative. dst_negative_code_table_convolutionlookup = ff_q_pvs_table_convolutionlookupnegative * S ((S (dc_input_table_convolution)) * dst_negative_scale_table_convolutionlookup) + (dst_negative_table_convolutionlookup))) /\ (exists ge_balance_positive_table_convolutionlookupvalue ge_balance_negative_table_convolutionlookupvalue. (((((dc_output_table_convolution) = 2 * (ge_balance_positive_table_convolutionlookupvalue) /\ (ge_balance_negative_table_convolutionlookupvalue) = 0) \/ exists ge_signed_half_table_convolutionlookupvaluedecode. (((dc_output_table_convolution) = 2 * ge_signed_half_table_convolutionlookupvaluedecode + 1 /\ (ge_balance_positive_table_convolutionlookupvalue) = 0) /\ (ge_balance_negative_table_convolutionlookupvalue) = S ge_signed_half_table_convolutionlookupvaluedecode))) /\ ((dst_positive_table_convolutionlookup) + ge_balance_negative_table_convolutionlookupvalue = (dst_negative_table_convolutionlookup) + ge_balance_positive_table_convolutionlookupvalue))))))))) -> (((~((dc_input_table_convolution)=0)) /\ (exists dc_mask_table_convolutionvalue. ((((exists dst_positive_code_table_convolutionvaluemasktable dst_positive_scale_table_convolutionvaluemasktable dst_negative_code_table_convolutionvaluemasktable dst_negative_scale_table_convolutionvaluemasktable. (((dc_mask_table_convolutionvalue) = (((((dst_positive_code_table_convolutionvaluemasktable) + (dst_positive_scale_table_convolutionvaluemasktable)) * S ((dst_positive_code_table_convolutionvaluemasktable) + (dst_positive_scale_table_convolutionvaluemasktable)) + ((dst_positive_scale_table_convolutionvaluemasktable) + (dst_positive_scale_table_convolutionvaluemasktable))) + (((dst_negative_code_table_convolutionvaluemasktable) + (dst_negative_scale_table_convolutionvaluemasktable)) * S ((dst_negative_code_table_convolutionvaluemasktable) + (dst_negative_scale_table_convolutionvaluemasktable)) + ((dst_negative_scale_table_convolutionvaluemasktable) + (dst_negative_scale_table_convolutionvaluemasktable)))) * S ((((dst_positive_code_table_convolutionvaluemasktable) + (dst_positive_scale_table_convolutionvaluemasktable)) * S ((dst_positive_code_table_convolutionvaluemasktable) + (dst_positive_scale_table_convolutionvaluemasktable)) + ((dst_positive_scale_table_convolutionvaluemasktable) + (dst_positive_scale_table_convolutionvaluemasktable))) + (((dst_negative_code_table_convolutionvaluemasktable) + (dst_negative_scale_table_convolutionvaluemasktable)) * S ((dst_negative_code_table_convolutionvaluemasktable) + (dst_negative_scale_table_convolutionvaluemasktable)) + ((dst_negative_scale_table_convolutionvaluemasktable) + (dst_negative_scale_table_convolutionvaluemasktable)))) + ((((dst_negative_code_table_convolutionvaluemasktable) + (dst_negative_scale_table_convolutionvaluemasktable)) * S ((dst_negative_code_table_convolutionvaluemasktable) + (dst_negative_scale_table_convolutionvaluemasktable)) + ((dst_negative_scale_table_convolutionvaluemasktable) + (dst_negative_scale_table_convolutionvaluemasktable))) + (((dst_negative_code_table_convolutionvaluemasktable) + (dst_negative_scale_table_convolutionvaluemasktable)) * S ((dst_negative_code_table_convolutionvaluemasktable) + (dst_negative_scale_table_convolutionvaluemasktable)) + ((dst_negative_scale_table_convolutionvaluemasktable) + (dst_negative_scale_table_convolutionvaluemasktable)))))) /\ (forall dst_index_table_convolutionvaluemasktable. (exists pvs_le_gap_table_convolutionvaluemasktabledomain. pvs_le_gap_table_convolutionvaluemasktabledomain + (dst_index_table_convolutionvaluemasktable) = (dc_input_table_convolution)) -> exists dst_positive_table_convolutionvaluemasktable dst_negative_table_convolutionvaluemasktable dst_value_table_convolutionvaluemasktable. ((((exists ff_h_pvs_table_convolutionvaluemasktableentrypositive. ff_h_pvs_table_convolutionvaluemasktableentrypositive + S (dst_positive_table_convolutionvaluemasktable) = S ((S (dst_index_table_convolutionvaluemasktable)) * dst_positive_scale_table_convolutionvaluemasktable)) /\ exists ff_q_pvs_table_convolutionvaluemasktableentrypositive. dst_positive_code_table_convolutionvaluemasktable = ff_q_pvs_table_convolutionvaluemasktableentrypositive * S ((S (dst_index_table_convolutionvaluemasktable)) * dst_positive_scale_table_convolutionvaluemasktable) + (dst_positive_table_convolutionvaluemasktable))) /\ (((((exists ff_h_pvs_table_convolutionvaluemasktableentrynegative. ff_h_pvs_table_convolutionvaluemasktableentrynegative + S (dst_negative_table_convolutionvaluemasktable) = S ((S (dst_index_table_convolutionvaluemasktable)) * dst_negative_scale_table_convolutionvaluemasktable)) /\ exists ff_q_pvs_table_convolutionvaluemasktableentrynegative. dst_negative_code_table_convolutionvaluemasktable = ff_q_pvs_table_convolutionvaluemasktableentrynegative * S ((S (dst_index_table_convolutionvaluemasktable)) * dst_negative_scale_table_convolutionvaluemasktable) + (dst_negative_table_convolutionvaluemasktable))) /\ (exists ge_balance_positive_table_convolutionvaluemasktableentryvalue ge_balance_negative_table_convolutionvaluemasktableentryvalue. (((((dst_value_table_convolutionvaluemasktable) = 2 * (ge_balance_positive_table_convolutionvaluemasktableentryvalue) /\ (ge_balance_negative_table_convolutionvaluemasktableentryvalue) = 0) \/ exists ge_signed_half_table_convolutionvaluemasktableentryvaluedecode. (((dst_value_table_convolutionvaluemasktable) = 2 * ge_signed_half_table_convolutionvaluemasktableentryvaluedecode + 1 /\ (ge_balance_positive_table_convolutionvaluemasktableentryvalue) = 0) /\ (ge_balance_negative_table_convolutionvaluemasktableentryvalue) = S ge_signed_half_table_convolutionvaluemasktableentryvaluedecode))) /\ ((dst_positive_table_convolutionvaluemasktable) + ge_balance_negative_table_convolutionvaluemasktableentryvalue = (dst_negative_table_convolutionvaluemasktable) + ge_balance_positive_table_convolutionvaluemasktableentryvalue))))))))) /\ (forall dc_index_table_convolutionvaluemask dc_value_table_convolutionvaluemask. (exists pvs_le_gap_table_convolutionvaluemaskdomain. pvs_le_gap_table_convolutionvaluemaskdomain + (dc_index_table_convolutionvaluemask) = (dc_input_table_convolution)) -> (exists dst_positive_code_table_convolutionvaluemasklookup dst_positive_scale_table_convolutionvaluemasklookup dst_negative_code_table_convolutionvaluemasklookup dst_negative_scale_table_convolutionvaluemasklookup dst_positive_table_convolutionvaluemasklookup dst_negative_table_convolutionvaluemasklookup. (((dc_mask_table_convolutionvalue) = (((((dst_positive_code_table_convolutionvaluemasklookup) + (dst_positive_scale_table_convolutionvaluemasklookup)) * S ((dst_positive_code_table_convolutionvaluemasklookup) + (dst_positive_scale_table_convolutionvaluemasklookup)) + ((dst_positive_scale_table_convolutionvaluemasklookup) + (dst_positive_scale_table_convolutionvaluemasklookup))) + (((dst_negative_code_table_convolutionvaluemasklookup) + (dst_negative_scale_table_convolutionvaluemasklookup)) * S ((dst_negative_code_table_convolutionvaluemasklookup) + (dst_negative_scale_table_convolutionvaluemasklookup)) + ((dst_negative_scale_table_convolutionvaluemasklookup) + (dst_negative_scale_table_convolutionvaluemasklookup)))) * S ((((dst_positive_code_table_convolutionvaluemasklookup) + (dst_positive_scale_table_convolutionvaluemasklookup)) * S ((dst_positive_code_table_convolutionvaluemasklookup) + (dst_positive_scale_table_convolutionvaluemasklookup)) + ((dst_positive_scale_table_convolutionvaluemasklookup) + (dst_positive_scale_table_convolutionvaluemasklookup))) + (((dst_negative_code_table_convolutionvaluemasklookup) + (dst_negative_scale_table_convolutionvaluemasklookup)) * S ((dst_negative_code_table_convolutionvaluemasklookup) + (dst_negative_scale_table_convolutionvaluemasklookup)) + ((dst_negative_scale_table_convolutionvaluemasklookup) + (dst_negative_scale_table_convolutionvaluemasklookup)))) + ((((dst_negative_code_table_convolutionvaluemasklookup) + (dst_negative_scale_table_convolutionvaluemasklookup)) * S ((dst_negative_code_table_convolutionvaluemasklookup) + (dst_negative_scale_table_convolutionvaluemasklookup)) + ((dst_negative_scale_table_convolutionvaluemasklookup) + (dst_negative_scale_table_convolutionvaluemasklookup))) + (((dst_negative_code_table_convolutionvaluemasklookup) + (dst_negative_scale_table_convolutionvaluemasklookup)) * S ((dst_negative_code_table_convolutionvaluemasklookup) + (dst_negative_scale_table_convolutionvaluemasklookup)) + ((dst_negative_scale_table_convolutionvaluemasklookup) + (dst_negative_scale_table_convolutionvaluemasklookup)))))) /\ (((((exists ff_h_pvs_table_convolutionvaluemasklookuppositive. ff_h_pvs_table_convolutionvaluemasklookuppositive + S (dst_positive_table_convolutionvaluemasklookup) = S ((S (dc_index_table_convolutionvaluemask)) * dst_positive_scale_table_convolutionvaluemasklookup)) /\ exists ff_q_pvs_table_convolutionvaluemasklookuppositive. dst_positive_code_table_convolutionvaluemasklookup = ff_q_pvs_table_convolutionvaluemasklookuppositive * S ((S (dc_index_table_convolutionvaluemask)) * dst_positive_scale_table_convolutionvaluemasklookup) + (dst_positive_table_convolutionvaluemasklookup))) /\ (((((exists ff_h_pvs_table_convolutionvaluemasklookupnegative. ff_h_pvs_table_convolutionvaluemasklookupnegative + S (dst_negative_table_convolutionvaluemasklookup) = S ((S (dc_index_table_convolutionvaluemask)) * dst_negative_scale_table_convolutionvaluemasklookup)) /\ exists ff_q_pvs_table_convolutionvaluemasklookupnegative. dst_negative_code_table_convolutionvaluemasklookup = ff_q_pvs_table_convolutionvaluemasklookupnegative * S ((S (dc_index_table_convolutionvaluemask)) * dst_negative_scale_table_convolutionvaluemasklookup) + (dst_negative_table_convolutionvaluemasklookup))) /\ (exists ge_balance_positive_table_convolutionvaluemasklookupvalue ge_balance_negative_table_convolutionvaluemasklookupvalue. (((((dc_value_table_convolutionvaluemask) = 2 * (ge_balance_positive_table_convolutionvaluemasklookupvalue) /\ (ge_balance_negative_table_convolutionvaluemasklookupvalue) = 0) \/ exists ge_signed_half_table_convolutionvaluemasklookupvaluedecode. (((dc_value_table_convolutionvaluemask) = 2 * ge_signed_half_table_convolutionvaluemasklookupvaluedecode + 1 /\ (ge_balance_positive_table_convolutionvaluemasklookupvalue) = 0) /\ (ge_balance_negative_table_convolutionvaluemasklookupvalue) = S ge_signed_half_table_convolutionvaluemasklookupvaluedecode))) /\ ((dst_positive_table_convolutionvaluemasklookup) + ge_balance_negative_table_convolutionvaluemasklookupvalue = (dst_negative_table_convolutionvaluemasklookup) + ge_balance_positive_table_convolutionvaluemasklookupvalue))))))))) -> ((((~((dc_index_table_convolutionvaluemask)=0)) /\ (exists dc_quotient_table_convolutionvaluemaskentry dc_left_table_convolutionvaluemaskentry dc_right_table_convolutionvaluemaskentry. (((dc_input_table_convolution)=(dc_index_table_convolutionvaluemask)*dc_quotient_table_convolutionvaluemaskentry) /\ (((exists dst_positive_code_table_convolutionvaluemaskentryleft dst_positive_scale_table_convolutionvaluemaskentryleft dst_negative_code_table_convolutionvaluemaskentryleft dst_negative_scale_table_convolutionvaluemaskentryleft dst_positive_table_convolutionvaluemaskentryleft dst_negative_table_convolutionvaluemaskentryleft. (((F) = (((((dst_positive_code_table_convolutionvaluemaskentryleft) + (dst_positive_scale_table_convolutionvaluemaskentryleft)) * S ((dst_positive_code_table_convolutionvaluemaskentryleft) + (dst_positive_scale_table_convolutionvaluemaskentryleft)) + ((dst_positive_scale_table_convolutionvaluemaskentryleft) + (dst_positive_scale_table_convolutionvaluemaskentryleft))) + (((dst_negative_code_table_convolutionvaluemaskentryleft) + (dst_negative_scale_table_convolutionvaluemaskentryleft)) * S ((dst_negative_code_table_convolutionvaluemaskentryleft) + (dst_negative_scale_table_convolutionvaluemaskentryleft)) + ((dst_negative_scale_table_convolutionvaluemaskentryleft) + (dst_negative_scale_table_convolutionvaluemaskentryleft)))) * S ((((dst_positive_code_table_convolutionvaluemaskentryleft) + (dst_positive_scale_table_convolutionvaluemaskentryleft)) * S ((dst_positive_code_table_convolutionvaluemaskentryleft) + (dst_positive_scale_table_convolutionvaluemaskentryleft)) + ((dst_positive_scale_table_convolutionvaluemaskentryleft) + (dst_positive_scale_table_convolutionvaluemaskentryleft))) + (((dst_negative_code_table_convolutionvaluemaskentryleft) + (dst_negative_scale_table_convolutionvaluemaskentryleft)) * S ((dst_negative_code_table_convolutionvaluemaskentryleft) + (dst_negative_scale_table_convolutionvaluemaskentryleft)) + ((dst_negative_scale_table_convolutionvaluemaskentryleft) + (dst_negative_scale_table_convolutionvaluemaskentryleft)))) + ((((dst_negative_code_table_convolutionvaluemaskentryleft) + (dst_negative_scale_table_convolutionvaluemaskentryleft)) * S ((dst_negative_code_table_convolutionvaluemaskentryleft) + (dst_negative_scale_table_convolutionvaluemaskentryleft)) + ((dst_negative_scale_table_convolutionvaluemaskentryleft) + (dst_negative_scale_table_convolutionvaluemaskentryleft))) + (((dst_negative_code_table_convolutionvaluemaskentryleft) + (dst_negative_scale_table_convolutionvaluemaskentryleft)) * S ((dst_negative_code_table_convolutionvaluemaskentryleft) + (dst_negative_scale_table_convolutionvaluemaskentryleft)) + ((dst_negative_scale_table_convolutionvaluemaskentryleft) + (dst_negative_scale_table_convolutionvaluemaskentryleft)))))) /\ (((((exists ff_h_pvs_table_convolutionvaluemaskentryleftpositive. ff_h_pvs_table_convolutionvaluemaskentryleftpositive + S (dst_positive_table_convolutionvaluemaskentryleft) = S ((S (dc_index_table_convolutionvaluemask)) * dst_positive_scale_table_convolutionvaluemaskentryleft)) /\ exists ff_q_pvs_table_convolutionvaluemaskentryleftpositive. dst_positive_code_table_convolutionvaluemaskentryleft = ff_q_pvs_table_convolutionvaluemaskentryleftpositive * S ((S (dc_index_table_convolutionvaluemask)) * dst_positive_scale_table_convolutionvaluemaskentryleft) + (dst_positive_table_convolutionvaluemaskentryleft))) /\ (((((exists ff_h_pvs_table_convolutionvaluemaskentryleftnegative. ff_h_pvs_table_convolutionvaluemaskentryleftnegative + S (dst_negative_table_convolutionvaluemaskentryleft) = S ((S (dc_index_table_convolutionvaluemask)) * dst_negative_scale_table_convolutionvaluemaskentryleft)) /\ exists ff_q_pvs_table_convolutionvaluemaskentryleftnegative. dst_negative_code_table_convolutionvaluemaskentryleft = ff_q_pvs_table_convolutionvaluemaskentryleftnegative * S ((S (dc_index_table_convolutionvaluemask)) * dst_negative_scale_table_convolutionvaluemaskentryleft) + (dst_negative_table_convolutionvaluemaskentryleft))) /\ (exists ge_balance_positive_table_convolutionvaluemaskentryleftvalue ge_balance_negative_table_convolutionvaluemaskentryleftvalue. (((((dc_left_table_convolutionvaluemaskentry) = 2 * (ge_balance_positive_table_convolutionvaluemaskentryleftvalue) /\ (ge_balance_negative_table_convolutionvaluemaskentryleftvalue) = 0) \/ exists ge_signed_half_table_convolutionvaluemaskentryleftvaluedecode. (((dc_left_table_convolutionvaluemaskentry) = 2 * ge_signed_half_table_convolutionvaluemaskentryleftvaluedecode + 1 /\ (ge_balance_positive_table_convolutionvaluemaskentryleftvalue) = 0) /\ (ge_balance_negative_table_convolutionvaluemaskentryleftvalue) = S ge_signed_half_table_convolutionvaluemaskentryleftvaluedecode))) /\ ((dst_positive_table_convolutionvaluemaskentryleft) + ge_balance_negative_table_convolutionvaluemaskentryleftvalue = (dst_negative_table_convolutionvaluemaskentryleft) + ge_balance_positive_table_convolutionvaluemaskentryleftvalue))))))))) /\ (((exists dst_positive_code_table_convolutionvaluemaskentryright dst_positive_scale_table_convolutionvaluemaskentryright dst_negative_code_table_convolutionvaluemaskentryright dst_negative_scale_table_convolutionvaluemaskentryright dst_positive_table_convolutionvaluemaskentryright dst_negative_table_convolutionvaluemaskentryright. (((G) = (((((dst_positive_code_table_convolutionvaluemaskentryright) + (dst_positive_scale_table_convolutionvaluemaskentryright)) * S ((dst_positive_code_table_convolutionvaluemaskentryright) + (dst_positive_scale_table_convolutionvaluemaskentryright)) + ((dst_positive_scale_table_convolutionvaluemaskentryright) + (dst_positive_scale_table_convolutionvaluemaskentryright))) + (((dst_negative_code_table_convolutionvaluemaskentryright) + (dst_negative_scale_table_convolutionvaluemaskentryright)) * S ((dst_negative_code_table_convolutionvaluemaskentryright) + (dst_negative_scale_table_convolutionvaluemaskentryright)) + ((dst_negative_scale_table_convolutionvaluemaskentryright) + (dst_negative_scale_table_convolutionvaluemaskentryright)))) * S ((((dst_positive_code_table_convolutionvaluemaskentryright) + (dst_positive_scale_table_convolutionvaluemaskentryright)) * S ((dst_positive_code_table_convolutionvaluemaskentryright) + (dst_positive_scale_table_convolutionvaluemaskentryright)) + ((dst_positive_scale_table_convolutionvaluemaskentryright) + (dst_positive_scale_table_convolutionvaluemaskentryright))) + (((dst_negative_code_table_convolutionvaluemaskentryright) + (dst_negative_scale_table_convolutionvaluemaskentryright)) * S ((dst_negative_code_table_convolutionvaluemaskentryright) + (dst_negative_scale_table_convolutionvaluemaskentryright)) + ((dst_negative_scale_table_convolutionvaluemaskentryright) + (dst_negative_scale_table_convolutionvaluemaskentryright)))) + ((((dst_negative_code_table_convolutionvaluemaskentryright) + (dst_negative_scale_table_convolutionvaluemaskentryright)) * S ((dst_negative_code_table_convolutionvaluemaskentryright) + (dst_negative_scale_table_convolutionvaluemaskentryright)) + ((dst_negative_scale_table_convolutionvaluemaskentryright) + (dst_negative_scale_table_convolutionvaluemaskentryright))) + (((dst_negative_code_table_convolutionvaluemaskentryright) + (dst_negative_scale_table_convolutionvaluemaskentryright)) * S ((dst_negative_code_table_convolutionvaluemaskentryright) + (dst_negative_scale_table_convolutionvaluemaskentryright)) + ((dst_negative_scale_table_convolutionvaluemaskentryright) + (dst_negative_scale_table_convolutionvaluemaskentryright)))))) /\ (((((exists ff_h_pvs_table_convolutionvaluemaskentryrightpositive. ff_h_pvs_table_convolutionvaluemaskentryrightpositive + S (dst_positive_table_convolutionvaluemaskentryright) = S ((S (dc_quotient_table_convolutionvaluemaskentry)) * dst_positive_scale_table_convolutionvaluemaskentryright)) /\ exists ff_q_pvs_table_convolutionvaluemaskentryrightpositive. dst_positive_code_table_convolutionvaluemaskentryright = ff_q_pvs_table_convolutionvaluemaskentryrightpositive * S ((S (dc_quotient_table_convolutionvaluemaskentry)) * dst_positive_scale_table_convolutionvaluemaskentryright) + (dst_positive_table_convolutionvaluemaskentryright))) /\ (((((exists ff_h_pvs_table_convolutionvaluemaskentryrightnegative. ff_h_pvs_table_convolutionvaluemaskentryrightnegative + S (dst_negative_table_convolutionvaluemaskentryright) = S ((S (dc_quotient_table_convolutionvaluemaskentry)) * dst_negative_scale_table_convolutionvaluemaskentryright)) /\ exists ff_q_pvs_table_convolutionvaluemaskentryrightnegative. dst_negative_code_table_convolutionvaluemaskentryright = ff_q_pvs_table_convolutionvaluemaskentryrightnegative * S ((S (dc_quotient_table_convolutionvaluemaskentry)) * dst_negative_scale_table_convolutionvaluemaskentryright) + (dst_negative_table_convolutionvaluemaskentryright))) /\ (exists ge_balance_positive_table_convolutionvaluemaskentryrightvalue ge_balance_negative_table_convolutionvaluemaskentryrightvalue. (((((dc_right_table_convolutionvaluemaskentry) = 2 * (ge_balance_positive_table_convolutionvaluemaskentryrightvalue) /\ (ge_balance_negative_table_convolutionvaluemaskentryrightvalue) = 0) \/ exists ge_signed_half_table_convolutionvaluemaskentryrightvaluedecode. (((dc_right_table_convolutionvaluemaskentry) = 2 * ge_signed_half_table_convolutionvaluemaskentryrightvaluedecode + 1 /\ (ge_balance_positive_table_convolutionvaluemaskentryrightvalue) = 0) /\ (ge_balance_negative_table_convolutionvaluemaskentryrightvalue) = S ge_signed_half_table_convolutionvaluemaskentryrightvaluedecode))) /\ ((dst_positive_table_convolutionvaluemaskentryright) + ge_balance_negative_table_convolutionvaluemaskentryrightvalue = (dst_negative_table_convolutionvaluemaskentryright) + ge_balance_positive_table_convolutionvaluemaskentryrightvalue))))))))) /\ (exists sto_ap_table_convolutionvaluemaskentryproduct sto_an_table_convolutionvaluemaskentryproduct sto_bp_table_convolutionvaluemaskentryproduct sto_bn_table_convolutionvaluemaskentryproduct sto_cp_table_convolutionvaluemaskentryproduct sto_cn_table_convolutionvaluemaskentryproduct. (((((dc_left_table_convolutionvaluemaskentry) = 2 * (sto_ap_table_convolutionvaluemaskentryproduct) /\ (sto_an_table_convolutionvaluemaskentryproduct) = 0) \/ exists ge_signed_half_table_convolutionvaluemaskentryproductleft. (((dc_left_table_convolutionvaluemaskentry) = 2 * ge_signed_half_table_convolutionvaluemaskentryproductleft + 1 /\ (sto_ap_table_convolutionvaluemaskentryproduct) = 0) /\ (sto_an_table_convolutionvaluemaskentryproduct) = S ge_signed_half_table_convolutionvaluemaskentryproductleft))) /\ ((((((dc_right_table_convolutionvaluemaskentry) = 2 * (sto_bp_table_convolutionvaluemaskentryproduct) /\ (sto_bn_table_convolutionvaluemaskentryproduct) = 0) \/ exists ge_signed_half_table_convolutionvaluemaskentryproductright. (((dc_right_table_convolutionvaluemaskentry) = 2 * ge_signed_half_table_convolutionvaluemaskentryproductright + 1 /\ (sto_bp_table_convolutionvaluemaskentryproduct) = 0) /\ (sto_bn_table_convolutionvaluemaskentryproduct) = S ge_signed_half_table_convolutionvaluemaskentryproductright))) /\ ((((((dc_value_table_convolutionvaluemask) = 2 * (sto_cp_table_convolutionvaluemaskentryproduct) /\ (sto_cn_table_convolutionvaluemaskentryproduct) = 0) \/ exists ge_signed_half_table_convolutionvaluemaskentryproductoutput. (((dc_value_table_convolutionvaluemask) = 2 * ge_signed_half_table_convolutionvaluemaskentryproductoutput + 1 /\ (sto_cp_table_convolutionvaluemaskentryproduct) = 0) /\ (sto_cn_table_convolutionvaluemaskentryproduct) = S ge_signed_half_table_convolutionvaluemaskentryproductoutput))) /\ ((sto_ap_table_convolutionvaluemaskentryproduct * sto_bp_table_convolutionvaluemaskentryproduct + sto_an_table_convolutionvaluemaskentryproduct * sto_bn_table_convolutionvaluemaskentryproduct) + sto_cn_table_convolutionvaluemaskentryproduct = (sto_ap_table_convolutionvaluemaskentryproduct * sto_bn_table_convolutionvaluemaskentryproduct + sto_an_table_convolutionvaluemaskentryproduct * sto_bp_table_convolutionvaluemaskentryproduct) + sto_cp_table_convolutionvaluemaskentryproduct))))))))))))))) \/ ((((dc_index_table_convolutionvaluemask)=0 \/ ~(exists pvs_factor_table_convolutionvaluemaskentrynondivisor. (dc_input_table_convolution) = (dc_index_table_convolutionvaluemask) * pvs_factor_table_convolutionvaluemaskentrynondivisor)) /\ ((dc_value_table_convolutionvaluemask)=0))))))) /\ (exists dst_positive_code_table_convolutionvaluefold dst_positive_scale_table_convolutionvaluefold dst_negative_code_table_convolutionvaluefold dst_negative_scale_table_convolutionvaluefold dst_positive_sum_table_convolutionvaluefold dst_negative_sum_table_convolutionvaluefold. (((dc_mask_table_convolutionvalue) = (((((dst_positive_code_table_convolutionvaluefold) + (dst_positive_scale_table_convolutionvaluefold)) * S ((dst_positive_code_table_convolutionvaluefold) + (dst_positive_scale_table_convolutionvaluefold)) + ((dst_positive_scale_table_convolutionvaluefold) + (dst_positive_scale_table_convolutionvaluefold))) + (((dst_negative_code_table_convolutionvaluefold) + (dst_negative_scale_table_convolutionvaluefold)) * S ((dst_negative_code_table_convolutionvaluefold) + (dst_negative_scale_table_convolutionvaluefold)) + ((dst_negative_scale_table_convolutionvaluefold) + (dst_negative_scale_table_convolutionvaluefold)))) * S ((((dst_positive_code_table_convolutionvaluefold) + (dst_positive_scale_table_convolutionvaluefold)) * S ((dst_positive_code_table_convolutionvaluefold) + (dst_positive_scale_table_convolutionvaluefold)) + ((dst_positive_scale_table_convolutionvaluefold) + (dst_positive_scale_table_convolutionvaluefold))) + (((dst_negative_code_table_convolutionvaluefold) + (dst_negative_scale_table_convolutionvaluefold)) * S ((dst_negative_code_table_convolutionvaluefold) + (dst_negative_scale_table_convolutionvaluefold)) + ((dst_negative_scale_table_convolutionvaluefold) + (dst_negative_scale_table_convolutionvaluefold)))) + ((((dst_negative_code_table_convolutionvaluefold) + (dst_negative_scale_table_convolutionvaluefold)) * S ((dst_negative_code_table_convolutionvaluefold) + (dst_negative_scale_table_convolutionvaluefold)) + ((dst_negative_scale_table_convolutionvaluefold) + (dst_negative_scale_table_convolutionvaluefold))) + (((dst_negative_code_table_convolutionvaluefold) + (dst_negative_scale_table_convolutionvaluefold)) * S ((dst_negative_code_table_convolutionvaluefold) + (dst_negative_scale_table_convolutionvaluefold)) + ((dst_negative_scale_table_convolutionvaluefold) + (dst_negative_scale_table_convolutionvaluefold)))))) /\ (((exists fs_u_dst_table_convolutionvaluefoldpositive fs_v_dst_table_convolutionvaluefoldpositive. ((((exists fs_h_dst_table_convolutionvaluefoldpositive_body_start. fs_h_dst_table_convolutionvaluefoldpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_table_convolutionvaluefoldpositive)) /\ exists fs_q_dst_table_convolutionvaluefoldpositive_body_start. fs_u_dst_table_convolutionvaluefoldpositive = fs_q_dst_table_convolutionvaluefoldpositive_body_start * S ((S (0)) * fs_v_dst_table_convolutionvaluefoldpositive) + (0))) /\ ((((exists fs_h_dst_table_convolutionvaluefoldpositive_body_terminal. fs_h_dst_table_convolutionvaluefoldpositive_body_terminal + S (dst_positive_sum_table_convolutionvaluefold) = S ((S (S (dc_input_table_convolution))) * fs_v_dst_table_convolutionvaluefoldpositive)) /\ exists fs_q_dst_table_convolutionvaluefoldpositive_body_terminal. fs_u_dst_table_convolutionvaluefoldpositive = fs_q_dst_table_convolutionvaluefoldpositive_body_terminal * S ((S (S (dc_input_table_convolution))) * fs_v_dst_table_convolutionvaluefoldpositive) + (dst_positive_sum_table_convolutionvaluefold))) /\ forall fs_i_dst_table_convolutionvaluefoldpositive_body_steps. (exists fs_lt_dst_table_convolutionvaluefoldpositive_body_steps_bound. fs_lt_dst_table_convolutionvaluefoldpositive_body_steps_bound + S fs_i_dst_table_convolutionvaluefoldpositive_body_steps = S (dc_input_table_convolution)) -> exists fs_a_dst_table_convolutionvaluefoldpositive_body_steps fs_r_dst_table_convolutionvaluefoldpositive_body_steps fs_s_dst_table_convolutionvaluefoldpositive_body_steps. ((((exists fs_h_dst_table_convolutionvaluefoldpositive_body_steps_summand. fs_h_dst_table_convolutionvaluefoldpositive_body_steps_summand + S (fs_a_dst_table_convolutionvaluefoldpositive_body_steps) = S ((S (fs_i_dst_table_convolutionvaluefoldpositive_body_steps)) * dst_positive_scale_table_convolutionvaluefold)) /\ exists fs_q_dst_table_convolutionvaluefoldpositive_body_steps_summand. dst_positive_code_table_convolutionvaluefold = fs_q_dst_table_convolutionvaluefoldpositive_body_steps_summand * S ((S (fs_i_dst_table_convolutionvaluefoldpositive_body_steps)) * dst_positive_scale_table_convolutionvaluefold) + (fs_a_dst_table_convolutionvaluefoldpositive_body_steps))) /\ ((((exists fs_h_dst_table_convolutionvaluefoldpositive_body_steps_partial. fs_h_dst_table_convolutionvaluefoldpositive_body_steps_partial + S (fs_r_dst_table_convolutionvaluefoldpositive_body_steps) = S ((S (fs_i_dst_table_convolutionvaluefoldpositive_body_steps)) * fs_v_dst_table_convolutionvaluefoldpositive)) /\ exists fs_q_dst_table_convolutionvaluefoldpositive_body_steps_partial. fs_u_dst_table_convolutionvaluefoldpositive = fs_q_dst_table_convolutionvaluefoldpositive_body_steps_partial * S ((S (fs_i_dst_table_convolutionvaluefoldpositive_body_steps)) * fs_v_dst_table_convolutionvaluefoldpositive) + (fs_r_dst_table_convolutionvaluefoldpositive_body_steps))) /\ ((((exists fs_h_dst_table_convolutionvaluefoldpositive_body_steps_successor. fs_h_dst_table_convolutionvaluefoldpositive_body_steps_successor + S (fs_s_dst_table_convolutionvaluefoldpositive_body_steps) = S ((S (S fs_i_dst_table_convolutionvaluefoldpositive_body_steps)) * fs_v_dst_table_convolutionvaluefoldpositive)) /\ exists fs_q_dst_table_convolutionvaluefoldpositive_body_steps_successor. fs_u_dst_table_convolutionvaluefoldpositive = fs_q_dst_table_convolutionvaluefoldpositive_body_steps_successor * S ((S (S fs_i_dst_table_convolutionvaluefoldpositive_body_steps)) * fs_v_dst_table_convolutionvaluefoldpositive) + (fs_s_dst_table_convolutionvaluefoldpositive_body_steps))) /\ fs_s_dst_table_convolutionvaluefoldpositive_body_steps = fs_r_dst_table_convolutionvaluefoldpositive_body_steps + fs_a_dst_table_convolutionvaluefoldpositive_body_steps)))))) /\ (((exists fs_u_dst_table_convolutionvaluefoldnegative fs_v_dst_table_convolutionvaluefoldnegative. ((((exists fs_h_dst_table_convolutionvaluefoldnegative_body_start. fs_h_dst_table_convolutionvaluefoldnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_table_convolutionvaluefoldnegative)) /\ exists fs_q_dst_table_convolutionvaluefoldnegative_body_start. fs_u_dst_table_convolutionvaluefoldnegative = fs_q_dst_table_convolutionvaluefoldnegative_body_start * S ((S (0)) * fs_v_dst_table_convolutionvaluefoldnegative) + (0))) /\ ((((exists fs_h_dst_table_convolutionvaluefoldnegative_body_terminal. fs_h_dst_table_convolutionvaluefoldnegative_body_terminal + S (dst_negative_sum_table_convolutionvaluefold) = S ((S (S (dc_input_table_convolution))) * fs_v_dst_table_convolutionvaluefoldnegative)) /\ exists fs_q_dst_table_convolutionvaluefoldnegative_body_terminal. fs_u_dst_table_convolutionvaluefoldnegative = fs_q_dst_table_convolutionvaluefoldnegative_body_terminal * S ((S (S (dc_input_table_convolution))) * fs_v_dst_table_convolutionvaluefoldnegative) + (dst_negative_sum_table_convolutionvaluefold))) /\ forall fs_i_dst_table_convolutionvaluefoldnegative_body_steps. (exists fs_lt_dst_table_convolutionvaluefoldnegative_body_steps_bound. fs_lt_dst_table_convolutionvaluefoldnegative_body_steps_bound + S fs_i_dst_table_convolutionvaluefoldnegative_body_steps = S (dc_input_table_convolution)) -> exists fs_a_dst_table_convolutionvaluefoldnegative_body_steps fs_r_dst_table_convolutionvaluefoldnegative_body_steps fs_s_dst_table_convolutionvaluefoldnegative_body_steps. ((((exists fs_h_dst_table_convolutionvaluefoldnegative_body_steps_summand. fs_h_dst_table_convolutionvaluefoldnegative_body_steps_summand + S (fs_a_dst_table_convolutionvaluefoldnegative_body_steps) = S ((S (fs_i_dst_table_convolutionvaluefoldnegative_body_steps)) * dst_negative_scale_table_convolutionvaluefold)) /\ exists fs_q_dst_table_convolutionvaluefoldnegative_body_steps_summand. dst_negative_code_table_convolutionvaluefold = fs_q_dst_table_convolutionvaluefoldnegative_body_steps_summand * S ((S (fs_i_dst_table_convolutionvaluefoldnegative_body_steps)) * dst_negative_scale_table_convolutionvaluefold) + (fs_a_dst_table_convolutionvaluefoldnegative_body_steps))) /\ ((((exists fs_h_dst_table_convolutionvaluefoldnegative_body_steps_partial. fs_h_dst_table_convolutionvaluefoldnegative_body_steps_partial + S (fs_r_dst_table_convolutionvaluefoldnegative_body_steps) = S ((S (fs_i_dst_table_convolutionvaluefoldnegative_body_steps)) * fs_v_dst_table_convolutionvaluefoldnegative)) /\ exists fs_q_dst_table_convolutionvaluefoldnegative_body_steps_partial. fs_u_dst_table_convolutionvaluefoldnegative = fs_q_dst_table_convolutionvaluefoldnegative_body_steps_partial * S ((S (fs_i_dst_table_convolutionvaluefoldnegative_body_steps)) * fs_v_dst_table_convolutionvaluefoldnegative) + (fs_r_dst_table_convolutionvaluefoldnegative_body_steps))) /\ ((((exists fs_h_dst_table_convolutionvaluefoldnegative_body_steps_successor. fs_h_dst_table_convolutionvaluefoldnegative_body_steps_successor + S (fs_s_dst_table_convolutionvaluefoldnegative_body_steps) = S ((S (S fs_i_dst_table_convolutionvaluefoldnegative_body_steps)) * fs_v_dst_table_convolutionvaluefoldnegative)) /\ exists fs_q_dst_table_convolutionvaluefoldnegative_body_steps_successor. fs_u_dst_table_convolutionvaluefoldnegative = fs_q_dst_table_convolutionvaluefoldnegative_body_steps_successor * S ((S (S fs_i_dst_table_convolutionvaluefoldnegative_body_steps)) * fs_v_dst_table_convolutionvaluefoldnegative) + (fs_s_dst_table_convolutionvaluefoldnegative_body_steps))) /\ fs_s_dst_table_convolutionvaluefoldnegative_body_steps = fs_r_dst_table_convolutionvaluefoldnegative_body_steps + fs_a_dst_table_convolutionvaluefoldnegative_body_steps)))))) /\ (exists ge_balance_positive_table_convolutionvaluefoldresult ge_balance_negative_table_convolutionvaluefoldresult. (((((dc_output_table_convolution) = 2 * (ge_balance_positive_table_convolutionvaluefoldresult) /\ (ge_balance_negative_table_convolutionvaluefoldresult) = 0) \/ exists ge_signed_half_table_convolutionvaluefoldresultdecode. (((dc_output_table_convolution) = 2 * ge_signed_half_table_convolutionvaluefoldresultdecode + 1 /\ (ge_balance_positive_table_convolutionvaluefoldresult) = 0) /\ (ge_balance_negative_table_convolutionvaluefoldresult) = S ge_signed_half_table_convolutionvaluefoldresultdecode))) /\ ((dst_positive_sum_table_convolutionvaluefold) + ge_balance_negative_table_convolutionvaluefoldresult = (dst_negative_sum_table_convolutionvaluefold) + ge_balance_positive_table_convolutionvaluefoldresult)))))))))))))))))))) -> (((~((N)=0)) /\ (((exists dst_positive_code_table_resulttable dst_positive_scale_table_resulttable dst_negative_code_table_resulttable dst_negative_scale_table_resulttable. (((H) = (((((dst_positive_code_table_resulttable) + (dst_positive_scale_table_resulttable)) * S ((dst_positive_code_table_resulttable) + (dst_positive_scale_table_resulttable)) + ((dst_positive_scale_table_resulttable) + (dst_positive_scale_table_resulttable))) + (((dst_negative_code_table_resulttable) + (dst_negative_scale_table_resulttable)) * S ((dst_negative_code_table_resulttable) + (dst_negative_scale_table_resulttable)) + ((dst_negative_scale_table_resulttable) + (dst_negative_scale_table_resulttable)))) * S ((((dst_positive_code_table_resulttable) + (dst_positive_scale_table_resulttable)) * S ((dst_positive_code_table_resulttable) + (dst_positive_scale_table_resulttable)) + ((dst_positive_scale_table_resulttable) + (dst_positive_scale_table_resulttable))) + (((dst_negative_code_table_resulttable) + (dst_negative_scale_table_resulttable)) * S ((dst_negative_code_table_resulttable) + (dst_negative_scale_table_resulttable)) + ((dst_negative_scale_table_resulttable) + (dst_negative_scale_table_resulttable)))) + ((((dst_negative_code_table_resulttable) + (dst_negative_scale_table_resulttable)) * S ((dst_negative_code_table_resulttable) + (dst_negative_scale_table_resulttable)) + ((dst_negative_scale_table_resulttable) + (dst_negative_scale_table_resulttable))) + (((dst_negative_code_table_resulttable) + (dst_negative_scale_table_resulttable)) * S ((dst_negative_code_table_resulttable) + (dst_negative_scale_table_resulttable)) + ((dst_negative_scale_table_resulttable) + (dst_negative_scale_table_resulttable)))))) /\ (forall dst_index_table_resulttable. (exists pvs_le_gap_table_resulttabledomain. pvs_le_gap_table_resulttabledomain + (dst_index_table_resulttable) = (N)) -> exists dst_positive_table_resulttable dst_negative_table_resulttable dst_value_table_resulttable. ((((exists ff_h_pvs_table_resulttableentrypositive. ff_h_pvs_table_resulttableentrypositive + S (dst_positive_table_resulttable) = S ((S (dst_index_table_resulttable)) * dst_positive_scale_table_resulttable)) /\ exists ff_q_pvs_table_resulttableentrypositive. dst_positive_code_table_resulttable = ff_q_pvs_table_resulttableentrypositive * S ((S (dst_index_table_resulttable)) * dst_positive_scale_table_resulttable) + (dst_positive_table_resulttable))) /\ (((((exists ff_h_pvs_table_resulttableentrynegative. ff_h_pvs_table_resulttableentrynegative + S (dst_negative_table_resulttable) = S ((S (dst_index_table_resulttable)) * dst_negative_scale_table_resulttable)) /\ exists ff_q_pvs_table_resulttableentrynegative. dst_negative_code_table_resulttable = ff_q_pvs_table_resulttableentrynegative * S ((S (dst_index_table_resulttable)) * dst_negative_scale_table_resulttable) + (dst_negative_table_resulttable))) /\ (exists ge_balance_positive_table_resulttableentryvalue ge_balance_negative_table_resulttableentryvalue. (((((dst_value_table_resulttable) = 2 * (ge_balance_positive_table_resulttableentryvalue) /\ (ge_balance_negative_table_resulttableentryvalue) = 0) \/ exists ge_signed_half_table_resulttableentryvaluedecode. (((dst_value_table_resulttable) = 2 * ge_signed_half_table_resulttableentryvaluedecode + 1 /\ (ge_balance_positive_table_resulttableentryvalue) = 0) /\ (ge_balance_negative_table_resulttableentryvalue) = S ge_signed_half_table_resulttableentryvaluedecode))) /\ ((dst_positive_table_resulttable) + ge_balance_negative_table_resulttableentryvalue = (dst_negative_table_resulttable) + ge_balance_positive_table_resulttableentryvalue))))))))) /\ (((exists dst_positive_code_table_resultone dst_positive_scale_table_resultone dst_negative_code_table_resultone dst_negative_scale_table_resultone dst_positive_table_resultone dst_negative_table_resultone. (((H) = (((((dst_positive_code_table_resultone) + (dst_positive_scale_table_resultone)) * S ((dst_positive_code_table_resultone) + (dst_positive_scale_table_resultone)) + ((dst_positive_scale_table_resultone) + (dst_positive_scale_table_resultone))) + (((dst_negative_code_table_resultone) + (dst_negative_scale_table_resultone)) * S ((dst_negative_code_table_resultone) + (dst_negative_scale_table_resultone)) + ((dst_negative_scale_table_resultone) + (dst_negative_scale_table_resultone)))) * S ((((dst_positive_code_table_resultone) + (dst_positive_scale_table_resultone)) * S ((dst_positive_code_table_resultone) + (dst_positive_scale_table_resultone)) + ((dst_positive_scale_table_resultone) + (dst_positive_scale_table_resultone))) + (((dst_negative_code_table_resultone) + (dst_negative_scale_table_resultone)) * S ((dst_negative_code_table_resultone) + (dst_negative_scale_table_resultone)) + ((dst_negative_scale_table_resultone) + (dst_negative_scale_table_resultone)))) + ((((dst_negative_code_table_resultone) + (dst_negative_scale_table_resultone)) * S ((dst_negative_code_table_resultone) + (dst_negative_scale_table_resultone)) + ((dst_negative_scale_table_resultone) + (dst_negative_scale_table_resultone))) + (((dst_negative_code_table_resultone) + (dst_negative_scale_table_resultone)) * S ((dst_negative_code_table_resultone) + (dst_negative_scale_table_resultone)) + ((dst_negative_scale_table_resultone) + (dst_negative_scale_table_resultone)))))) /\ (((((exists ff_h_pvs_table_resultonepositive. ff_h_pvs_table_resultonepositive + S (dst_positive_table_resultone) = S ((S (1)) * dst_positive_scale_table_resultone)) /\ exists ff_q_pvs_table_resultonepositive. dst_positive_code_table_resultone = ff_q_pvs_table_resultonepositive * S ((S (1)) * dst_positive_scale_table_resultone) + (dst_positive_table_resultone))) /\ (((((exists ff_h_pvs_table_resultonenegative. ff_h_pvs_table_resultonenegative + S (dst_negative_table_resultone) = S ((S (1)) * dst_negative_scale_table_resultone)) /\ exists ff_q_pvs_table_resultonenegative. dst_negative_code_table_resultone = ff_q_pvs_table_resultonenegative * S ((S (1)) * dst_negative_scale_table_resultone) + (dst_negative_table_resultone))) /\ (exists ge_balance_positive_table_resultonevalue ge_balance_negative_table_resultonevalue. (((((2) = 2 * (ge_balance_positive_table_resultonevalue) /\ (ge_balance_negative_table_resultonevalue) = 0) \/ exists ge_signed_half_table_resultonevaluedecode. (((2) = 2 * ge_signed_half_table_resultonevaluedecode + 1 /\ (ge_balance_positive_table_resultonevalue) = 0) /\ (ge_balance_negative_table_resultonevalue) = S ge_signed_half_table_resultonevaluedecode))) /\ ((dst_positive_table_resultone) + ge_balance_negative_table_resultonevalue = (dst_negative_table_resultone) + ge_balance_positive_table_resultonevalue))))))))) /\ (forall mp_a_table_result mp_b_table_result mp_x_table_result mp_y_table_result mp_z_table_result. ~(mp_a_table_result=0) -> ~(mp_b_table_result=0) -> (exists pvs_le_gap_table_resultbound. pvs_le_gap_table_resultbound + (mp_a_table_result*mp_b_table_result) = (N)) -> (forall frp_divisor_table_resultcoprime. (exists frp_left_factor_table_resultcoprime. mp_a_table_result = frp_divisor_table_resultcoprime * frp_left_factor_table_resultcoprime) -> (exists frp_right_factor_table_resultcoprime. mp_b_table_result = frp_divisor_table_resultcoprime * frp_right_factor_table_resultcoprime) -> frp_divisor_table_resultcoprime = 1) -> (exists dst_positive_code_table_resultfirst dst_positive_scale_table_resultfirst dst_negative_code_table_resultfirst dst_negative_scale_table_resultfirst dst_positive_table_resultfirst dst_negative_table_resultfirst. (((H) = (((((dst_positive_code_table_resultfirst) + (dst_positive_scale_table_resultfirst)) * S ((dst_positive_code_table_resultfirst) + (dst_positive_scale_table_resultfirst)) + ((dst_positive_scale_table_resultfirst) + (dst_positive_scale_table_resultfirst))) + (((dst_negative_code_table_resultfirst) + (dst_negative_scale_table_resultfirst)) * S ((dst_negative_code_table_resultfirst) + (dst_negative_scale_table_resultfirst)) + ((dst_negative_scale_table_resultfirst) + (dst_negative_scale_table_resultfirst)))) * S ((((dst_positive_code_table_resultfirst) + (dst_positive_scale_table_resultfirst)) * S ((dst_positive_code_table_resultfirst) + (dst_positive_scale_table_resultfirst)) + ((dst_positive_scale_table_resultfirst) + (dst_positive_scale_table_resultfirst))) + (((dst_negative_code_table_resultfirst) + (dst_negative_scale_table_resultfirst)) * S ((dst_negative_code_table_resultfirst) + (dst_negative_scale_table_resultfirst)) + ((dst_negative_scale_table_resultfirst) + (dst_negative_scale_table_resultfirst)))) + ((((dst_negative_code_table_resultfirst) + (dst_negative_scale_table_resultfirst)) * S ((dst_negative_code_table_resultfirst) + (dst_negative_scale_table_resultfirst)) + ((dst_negative_scale_table_resultfirst) + (dst_negative_scale_table_resultfirst))) + (((dst_negative_code_table_resultfirst) + (dst_negative_scale_table_resultfirst)) * S ((dst_negative_code_table_resultfirst) + (dst_negative_scale_table_resultfirst)) + ((dst_negative_scale_table_resultfirst) + (dst_negative_scale_table_resultfirst)))))) /\ (((((exists ff_h_pvs_table_resultfirstpositive. ff_h_pvs_table_resultfirstpositive + S (dst_positive_table_resultfirst) = S ((S (mp_a_table_result)) * dst_positive_scale_table_resultfirst)) /\ exists ff_q_pvs_table_resultfirstpositive. dst_positive_code_table_resultfirst = ff_q_pvs_table_resultfirstpositive * S ((S (mp_a_table_result)) * dst_positive_scale_table_resultfirst) + (dst_positive_table_resultfirst))) /\ (((((exists ff_h_pvs_table_resultfirstnegative. ff_h_pvs_table_resultfirstnegative + S (dst_negative_table_resultfirst) = S ((S (mp_a_table_result)) * dst_negative_scale_table_resultfirst)) /\ exists ff_q_pvs_table_resultfirstnegative. dst_negative_code_table_resultfirst = ff_q_pvs_table_resultfirstnegative * S ((S (mp_a_table_result)) * dst_negative_scale_table_resultfirst) + (dst_negative_table_resultfirst))) /\ (exists ge_balance_positive_table_resultfirstvalue ge_balance_negative_table_resultfirstvalue. (((((mp_x_table_result) = 2 * (ge_balance_positive_table_resultfirstvalue) /\ (ge_balance_negative_table_resultfirstvalue) = 0) \/ exists ge_signed_half_table_resultfirstvaluedecode. (((mp_x_table_result) = 2 * ge_signed_half_table_resultfirstvaluedecode + 1 /\ (ge_balance_positive_table_resultfirstvalue) = 0) /\ (ge_balance_negative_table_resultfirstvalue) = S ge_signed_half_table_resultfirstvaluedecode))) /\ ((dst_positive_table_resultfirst) + ge_balance_negative_table_resultfirstvalue = (dst_negative_table_resultfirst) + ge_balance_positive_table_resultfirstvalue))))))))) -> (exists dst_positive_code_table_resultsecond dst_positive_scale_table_resultsecond dst_negative_code_table_resultsecond dst_negative_scale_table_resultsecond dst_positive_table_resultsecond dst_negative_table_resultsecond. (((H) = (((((dst_positive_code_table_resultsecond) + (dst_positive_scale_table_resultsecond)) * S ((dst_positive_code_table_resultsecond) + (dst_positive_scale_table_resultsecond)) + ((dst_positive_scale_table_resultsecond) + (dst_positive_scale_table_resultsecond))) + (((dst_negative_code_table_resultsecond) + (dst_negative_scale_table_resultsecond)) * S ((dst_negative_code_table_resultsecond) + (dst_negative_scale_table_resultsecond)) + ((dst_negative_scale_table_resultsecond) + (dst_negative_scale_table_resultsecond)))) * S ((((dst_positive_code_table_resultsecond) + (dst_positive_scale_table_resultsecond)) * S ((dst_positive_code_table_resultsecond) + (dst_positive_scale_table_resultsecond)) + ((dst_positive_scale_table_resultsecond) + (dst_positive_scale_table_resultsecond))) + (((dst_negative_code_table_resultsecond) + (dst_negative_scale_table_resultsecond)) * S ((dst_negative_code_table_resultsecond) + (dst_negative_scale_table_resultsecond)) + ((dst_negative_scale_table_resultsecond) + (dst_negative_scale_table_resultsecond)))) + ((((dst_negative_code_table_resultsecond) + (dst_negative_scale_table_resultsecond)) * S ((dst_negative_code_table_resultsecond) + (dst_negative_scale_table_resultsecond)) + ((dst_negative_scale_table_resultsecond) + (dst_negative_scale_table_resultsecond))) + (((dst_negative_code_table_resultsecond) + (dst_negative_scale_table_resultsecond)) * S ((dst_negative_code_table_resultsecond) + (dst_negative_scale_table_resultsecond)) + ((dst_negative_scale_table_resultsecond) + (dst_negative_scale_table_resultsecond)))))) /\ (((((exists ff_h_pvs_table_resultsecondpositive. ff_h_pvs_table_resultsecondpositive + S (dst_positive_table_resultsecond) = S ((S (mp_b_table_result)) * dst_positive_scale_table_resultsecond)) /\ exists ff_q_pvs_table_resultsecondpositive. dst_positive_code_table_resultsecond = ff_q_pvs_table_resultsecondpositive * S ((S (mp_b_table_result)) * dst_positive_scale_table_resultsecond) + (dst_positive_table_resultsecond))) /\ (((((exists ff_h_pvs_table_resultsecondnegative. ff_h_pvs_table_resultsecondnegative + S (dst_negative_table_resultsecond) = S ((S (mp_b_table_result)) * dst_negative_scale_table_resultsecond)) /\ exists ff_q_pvs_table_resultsecondnegative. dst_negative_code_table_resultsecond = ff_q_pvs_table_resultsecondnegative * S ((S (mp_b_table_result)) * dst_negative_scale_table_resultsecond) + (dst_negative_table_resultsecond))) /\ (exists ge_balance_positive_table_resultsecondvalue ge_balance_negative_table_resultsecondvalue. (((((mp_y_table_result) = 2 * (ge_balance_positive_table_resultsecondvalue) /\ (ge_balance_negative_table_resultsecondvalue) = 0) \/ exists ge_signed_half_table_resultsecondvaluedecode. (((mp_y_table_result) = 2 * ge_signed_half_table_resultsecondvaluedecode + 1 /\ (ge_balance_positive_table_resultsecondvalue) = 0) /\ (ge_balance_negative_table_resultsecondvalue) = S ge_signed_half_table_resultsecondvaluedecode))) /\ ((dst_positive_table_resultsecond) + ge_balance_negative_table_resultsecondvalue = (dst_negative_table_resultsecond) + ge_balance_positive_table_resultsecondvalue))))))))) -> (exists dst_positive_code_table_resultproduct dst_positive_scale_table_resultproduct dst_negative_code_table_resultproduct dst_negative_scale_table_resultproduct dst_positive_table_resultproduct dst_negative_table_resultproduct. (((H) = (((((dst_positive_code_table_resultproduct) + (dst_positive_scale_table_resultproduct)) * S ((dst_positive_code_table_resultproduct) + (dst_positive_scale_table_resultproduct)) + ((dst_positive_scale_table_resultproduct) + (dst_positive_scale_table_resultproduct))) + (((dst_negative_code_table_resultproduct) + (dst_negative_scale_table_resultproduct)) * S ((dst_negative_code_table_resultproduct) + (dst_negative_scale_table_resultproduct)) + ((dst_negative_scale_table_resultproduct) + (dst_negative_scale_table_resultproduct)))) * S ((((dst_positive_code_table_resultproduct) + (dst_positive_scale_table_resultproduct)) * S ((dst_positive_code_table_resultproduct) + (dst_positive_scale_table_resultproduct)) + ((dst_positive_scale_table_resultproduct) + (dst_positive_scale_table_resultproduct))) + (((dst_negative_code_table_resultproduct) + (dst_negative_scale_table_resultproduct)) * S ((dst_negative_code_table_resultproduct) + (dst_negative_scale_table_resultproduct)) + ((dst_negative_scale_table_resultproduct) + (dst_negative_scale_table_resultproduct)))) + ((((dst_negative_code_table_resultproduct) + (dst_negative_scale_table_resultproduct)) * S ((dst_negative_code_table_resultproduct) + (dst_negative_scale_table_resultproduct)) + ((dst_negative_scale_table_resultproduct) + (dst_negative_scale_table_resultproduct))) + (((dst_negative_code_table_resultproduct) + (dst_negative_scale_table_resultproduct)) * S ((dst_negative_code_table_resultproduct) + (dst_negative_scale_table_resultproduct)) + ((dst_negative_scale_table_resultproduct) + (dst_negative_scale_table_resultproduct)))))) /\ (((((exists ff_h_pvs_table_resultproductpositive. ff_h_pvs_table_resultproductpositive + S (dst_positive_table_resultproduct) = S ((S (mp_a_table_result*mp_b_table_result)) * dst_positive_scale_table_resultproduct)) /\ exists ff_q_pvs_table_resultproductpositive. dst_positive_code_table_resultproduct = ff_q_pvs_table_resultproductpositive * S ((S (mp_a_table_result*mp_b_table_result)) * dst_positive_scale_table_resultproduct) + (dst_positive_table_resultproduct))) /\ (((((exists ff_h_pvs_table_resultproductnegative. ff_h_pvs_table_resultproductnegative + S (dst_negative_table_resultproduct) = S ((S (mp_a_table_result*mp_b_table_result)) * dst_negative_scale_table_resultproduct)) /\ exists ff_q_pvs_table_resultproductnegative. dst_negative_code_table_resultproduct = ff_q_pvs_table_resultproductnegative * S ((S (mp_a_table_result*mp_b_table_result)) * dst_negative_scale_table_resultproduct) + (dst_negative_table_resultproduct))) /\ (exists ge_balance_positive_table_resultproductvalue ge_balance_negative_table_resultproductvalue. (((((mp_z_table_result) = 2 * (ge_balance_positive_table_resultproductvalue) /\ (ge_balance_negative_table_resultproductvalue) = 0) \/ exists ge_signed_half_table_resultproductvaluedecode. (((mp_z_table_result) = 2 * ge_signed_half_table_resultproductvaluedecode + 1 /\ (ge_balance_positive_table_resultproductvalue) = 0) /\ (ge_balance_negative_table_resultproductvalue) = S ge_signed_half_table_resultproductvaluedecode))) /\ ((dst_positive_table_resultproduct) + ge_balance_negative_table_resultproductvalue = (dst_negative_table_resultproduct) + ge_balance_positive_table_resultproductvalue))))))))) -> (exists sto_ap_table_resultlaw sto_an_table_resultlaw sto_bp_table_resultlaw sto_bn_table_resultlaw sto_cp_table_resultlaw sto_cn_table_resultlaw. (((((mp_x_table_result) = 2 * (sto_ap_table_resultlaw) /\ (sto_an_table_resultlaw) = 0) \/ exists ge_signed_half_table_resultlawleft. (((mp_x_table_result) = 2 * ge_signed_half_table_resultlawleft + 1 /\ (sto_ap_table_resultlaw) = 0) /\ (sto_an_table_resultlaw) = S ge_signed_half_table_resultlawleft))) /\ ((((((mp_y_table_result) = 2 * (sto_bp_table_resultlaw) /\ (sto_bn_table_resultlaw) = 0) \/ exists ge_signed_half_table_resultlawright. (((mp_y_table_result) = 2 * ge_signed_half_table_resultlawright + 1 /\ (sto_bp_table_resultlaw) = 0) /\ (sto_bn_table_resultlaw) = S ge_signed_half_table_resultlawright))) /\ ((((((mp_z_table_result) = 2 * (sto_cp_table_resultlaw) /\ (sto_cn_table_resultlaw) = 0) \/ exists ge_signed_half_table_resultlawoutput. (((mp_z_table_result) = 2 * ge_signed_half_table_resultlawoutput + 1 /\ (sto_cp_table_resultlaw) = 0) /\ (sto_cn_table_resultlaw) = S ge_signed_half_table_resultlawoutput))) /\ ((sto_ap_table_resultlaw * sto_bp_table_resultlaw + sto_an_table_resultlaw * sto_bn_table_resultlaw) + sto_cn_table_resultlaw = (sto_ap_table_resultlaw * sto_bn_table_resultlaw + sto_an_table_resultlaw * sto_bp_table_resultlaw) + sto_cp_table_resultlaw))))))))))))))