signed_cartesian_flat_prefix_append

Exact expanded first-order arithmetic statement

forall F G n l T z. (((exists dst_positive_code_prefix_append_beforetable dst_positive_scale_prefix_append_beforetable dst_negative_code_prefix_append_beforetable dst_negative_scale_prefix_append_beforetable. (((T) = (((((dst_positive_code_prefix_append_beforetable) + (dst_positive_scale_prefix_append_beforetable)) * S ((dst_positive_code_prefix_append_beforetable) + (dst_positive_scale_prefix_append_beforetable)) + ((dst_positive_scale_prefix_append_beforetable) + (dst_positive_scale_prefix_append_beforetable))) + (((dst_negative_code_prefix_append_beforetable) + (dst_negative_scale_prefix_append_beforetable)) * S ((dst_negative_code_prefix_append_beforetable) + (dst_negative_scale_prefix_append_beforetable)) + ((dst_negative_scale_prefix_append_beforetable) + (dst_negative_scale_prefix_append_beforetable)))) * S ((((dst_positive_code_prefix_append_beforetable) + (dst_positive_scale_prefix_append_beforetable)) * S ((dst_positive_code_prefix_append_beforetable) + (dst_positive_scale_prefix_append_beforetable)) + ((dst_positive_scale_prefix_append_beforetable) + (dst_positive_scale_prefix_append_beforetable))) + (((dst_negative_code_prefix_append_beforetable) + (dst_negative_scale_prefix_append_beforetable)) * S ((dst_negative_code_prefix_append_beforetable) + (dst_negative_scale_prefix_append_beforetable)) + ((dst_negative_scale_prefix_append_beforetable) + (dst_negative_scale_prefix_append_beforetable)))) + ((((dst_negative_code_prefix_append_beforetable) + (dst_negative_scale_prefix_append_beforetable)) * S ((dst_negative_code_prefix_append_beforetable) + (dst_negative_scale_prefix_append_beforetable)) + ((dst_negative_scale_prefix_append_beforetable) + (dst_negative_scale_prefix_append_beforetable))) + (((dst_negative_code_prefix_append_beforetable) + (dst_negative_scale_prefix_append_beforetable)) * S ((dst_negative_code_prefix_append_beforetable) + (dst_negative_scale_prefix_append_beforetable)) + ((dst_negative_scale_prefix_append_beforetable) + (dst_negative_scale_prefix_append_beforetable)))))) /\ (forall dst_index_prefix_append_beforetable. (exists pvs_le_gap_prefix_append_beforetabledomain. pvs_le_gap_prefix_append_beforetabledomain + (dst_index_prefix_append_beforetable) = (l)) -> exists dst_positive_prefix_append_beforetable dst_negative_prefix_append_beforetable dst_value_prefix_append_beforetable. ((((exists ff_h_pvs_prefix_append_beforetableentrypositive. ff_h_pvs_prefix_append_beforetableentrypositive + S (dst_positive_prefix_append_beforetable) = S ((S (dst_index_prefix_append_beforetable)) * dst_positive_scale_prefix_append_beforetable)) /\ exists ff_q_pvs_prefix_append_beforetableentrypositive. dst_positive_code_prefix_append_beforetable = ff_q_pvs_prefix_append_beforetableentrypositive * S ((S (dst_index_prefix_append_beforetable)) * dst_positive_scale_prefix_append_beforetable) + (dst_positive_prefix_append_beforetable))) /\ (((((exists ff_h_pvs_prefix_append_beforetableentrynegative. ff_h_pvs_prefix_append_beforetableentrynegative + S (dst_negative_prefix_append_beforetable) = S ((S (dst_index_prefix_append_beforetable)) * dst_negative_scale_prefix_append_beforetable)) /\ exists ff_q_pvs_prefix_append_beforetableentrynegative. dst_negative_code_prefix_append_beforetable = ff_q_pvs_prefix_append_beforetableentrynegative * S ((S (dst_index_prefix_append_beforetable)) * dst_negative_scale_prefix_append_beforetable) + (dst_negative_prefix_append_beforetable))) /\ (exists ge_balance_positive_prefix_append_beforetableentryvalue ge_balance_negative_prefix_append_beforetableentryvalue. (((((dst_value_prefix_append_beforetable) = 2 * (ge_balance_positive_prefix_append_beforetableentryvalue) /\ (ge_balance_negative_prefix_append_beforetableentryvalue) = 0) \/ exists ge_signed_half_prefix_append_beforetableentryvaluedecode. (((dst_value_prefix_append_beforetable) = 2 * ge_signed_half_prefix_append_beforetableentryvaluedecode + 1 /\ (ge_balance_positive_prefix_append_beforetableentryvalue) = 0) /\ (ge_balance_negative_prefix_append_beforetableentryvalue) = S ge_signed_half_prefix_append_beforetableentryvaluedecode))) /\ ((dst_positive_prefix_append_beforetable) + ge_balance_negative_prefix_append_beforetableentryvalue = (dst_negative_prefix_append_beforetable) + ge_balance_positive_prefix_append_beforetableentryvalue))))))))) /\ (forall scp_flat_index_prefix_append_before scp_flat_value_prefix_append_before. (exists pvs_le_gap_prefix_append_beforebound. pvs_le_gap_prefix_append_beforebound + (scp_flat_index_prefix_append_before) = (l)) -> (exists dst_positive_code_prefix_append_beforeentry dst_positive_scale_prefix_append_beforeentry dst_negative_code_prefix_append_beforeentry dst_negative_scale_prefix_append_beforeentry dst_positive_prefix_append_beforeentry dst_negative_prefix_append_beforeentry. (((T) = (((((dst_positive_code_prefix_append_beforeentry) + (dst_positive_scale_prefix_append_beforeentry)) * S ((dst_positive_code_prefix_append_beforeentry) + (dst_positive_scale_prefix_append_beforeentry)) + ((dst_positive_scale_prefix_append_beforeentry) + (dst_positive_scale_prefix_append_beforeentry))) + (((dst_negative_code_prefix_append_beforeentry) + (dst_negative_scale_prefix_append_beforeentry)) * S ((dst_negative_code_prefix_append_beforeentry) + (dst_negative_scale_prefix_append_beforeentry)) + ((dst_negative_scale_prefix_append_beforeentry) + (dst_negative_scale_prefix_append_beforeentry)))) * S ((((dst_positive_code_prefix_append_beforeentry) + (dst_positive_scale_prefix_append_beforeentry)) * S ((dst_positive_code_prefix_append_beforeentry) + (dst_positive_scale_prefix_append_beforeentry)) + ((dst_positive_scale_prefix_append_beforeentry) + (dst_positive_scale_prefix_append_beforeentry))) + (((dst_negative_code_prefix_append_beforeentry) + (dst_negative_scale_prefix_append_beforeentry)) * S ((dst_negative_code_prefix_append_beforeentry) + (dst_negative_scale_prefix_append_beforeentry)) + ((dst_negative_scale_prefix_append_beforeentry) + (dst_negative_scale_prefix_append_beforeentry)))) + ((((dst_negative_code_prefix_append_beforeentry) + (dst_negative_scale_prefix_append_beforeentry)) * S ((dst_negative_code_prefix_append_beforeentry) + (dst_negative_scale_prefix_append_beforeentry)) + ((dst_negative_scale_prefix_append_beforeentry) + (dst_negative_scale_prefix_append_beforeentry))) + (((dst_negative_code_prefix_append_beforeentry) + (dst_negative_scale_prefix_append_beforeentry)) * S ((dst_negative_code_prefix_append_beforeentry) + (dst_negative_scale_prefix_append_beforeentry)) + ((dst_negative_scale_prefix_append_beforeentry) + (dst_negative_scale_prefix_append_beforeentry)))))) /\ (((((exists ff_h_pvs_prefix_append_beforeentrypositive. ff_h_pvs_prefix_append_beforeentrypositive + S (dst_positive_prefix_append_beforeentry) = S ((S (scp_flat_index_prefix_append_before)) * dst_positive_scale_prefix_append_beforeentry)) /\ exists ff_q_pvs_prefix_append_beforeentrypositive. dst_positive_code_prefix_append_beforeentry = ff_q_pvs_prefix_append_beforeentrypositive * S ((S (scp_flat_index_prefix_append_before)) * dst_positive_scale_prefix_append_beforeentry) + (dst_positive_prefix_append_beforeentry))) /\ (((((exists ff_h_pvs_prefix_append_beforeentrynegative. ff_h_pvs_prefix_append_beforeentrynegative + S (dst_negative_prefix_append_beforeentry) = S ((S (scp_flat_index_prefix_append_before)) * dst_negative_scale_prefix_append_beforeentry)) /\ exists ff_q_pvs_prefix_append_beforeentrynegative. dst_negative_code_prefix_append_beforeentry = ff_q_pvs_prefix_append_beforeentrynegative * S ((S (scp_flat_index_prefix_append_before)) * dst_negative_scale_prefix_append_beforeentry) + (dst_negative_prefix_append_beforeentry))) /\ (exists ge_balance_positive_prefix_append_beforeentryvalue ge_balance_negative_prefix_append_beforeentryvalue. (((((scp_flat_value_prefix_append_before) = 2 * (ge_balance_positive_prefix_append_beforeentryvalue) /\ (ge_balance_negative_prefix_append_beforeentryvalue) = 0) \/ exists ge_signed_half_prefix_append_beforeentryvaluedecode. (((scp_flat_value_prefix_append_before) = 2 * ge_signed_half_prefix_append_beforeentryvaluedecode + 1 /\ (ge_balance_positive_prefix_append_beforeentryvalue) = 0) /\ (ge_balance_negative_prefix_append_beforeentryvalue) = S ge_signed_half_prefix_append_beforeentryvaluedecode))) /\ ((dst_positive_prefix_append_beforeentry) + ge_balance_negative_prefix_append_beforeentryvalue = (dst_negative_prefix_append_beforeentry) + ge_balance_positive_prefix_append_beforeentryvalue))))))))) -> (exists scp_flat_row_prefix_append_beforeproduct scp_flat_column_prefix_append_beforeproduct scp_flat_first_prefix_append_beforeproduct scp_flat_second_prefix_append_beforeproduct. (((scp_flat_index_prefix_append_before)=((n)*(scp_flat_row_prefix_append_beforeproduct)+(scp_flat_column_prefix_append_beforeproduct))) /\ (((exists pvs_gap_prefix_append_beforeproductremainder. pvs_gap_prefix_append_beforeproductremainder + S (scp_flat_column_prefix_append_beforeproduct) = (n)) /\ (((exists dst_positive_code_prefix_append_beforeproductF dst_positive_scale_prefix_append_beforeproductF dst_negative_code_prefix_append_beforeproductF dst_negative_scale_prefix_append_beforeproductF dst_positive_prefix_append_beforeproductF dst_negative_prefix_append_beforeproductF. (((F) = (((((dst_positive_code_prefix_append_beforeproductF) + (dst_positive_scale_prefix_append_beforeproductF)) * S ((dst_positive_code_prefix_append_beforeproductF) + (dst_positive_scale_prefix_append_beforeproductF)) + ((dst_positive_scale_prefix_append_beforeproductF) + (dst_positive_scale_prefix_append_beforeproductF))) + (((dst_negative_code_prefix_append_beforeproductF) + (dst_negative_scale_prefix_append_beforeproductF)) * S ((dst_negative_code_prefix_append_beforeproductF) + (dst_negative_scale_prefix_append_beforeproductF)) + ((dst_negative_scale_prefix_append_beforeproductF) + (dst_negative_scale_prefix_append_beforeproductF)))) * S ((((dst_positive_code_prefix_append_beforeproductF) + (dst_positive_scale_prefix_append_beforeproductF)) * S ((dst_positive_code_prefix_append_beforeproductF) + (dst_positive_scale_prefix_append_beforeproductF)) + ((dst_positive_scale_prefix_append_beforeproductF) + (dst_positive_scale_prefix_append_beforeproductF))) + (((dst_negative_code_prefix_append_beforeproductF) + (dst_negative_scale_prefix_append_beforeproductF)) * S ((dst_negative_code_prefix_append_beforeproductF) + (dst_negative_scale_prefix_append_beforeproductF)) + ((dst_negative_scale_prefix_append_beforeproductF) + (dst_negative_scale_prefix_append_beforeproductF)))) + ((((dst_negative_code_prefix_append_beforeproductF) + (dst_negative_scale_prefix_append_beforeproductF)) * S ((dst_negative_code_prefix_append_beforeproductF) + (dst_negative_scale_prefix_append_beforeproductF)) + ((dst_negative_scale_prefix_append_beforeproductF) + (dst_negative_scale_prefix_append_beforeproductF))) + (((dst_negative_code_prefix_append_beforeproductF) + (dst_negative_scale_prefix_append_beforeproductF)) * S ((dst_negative_code_prefix_append_beforeproductF) + (dst_negative_scale_prefix_append_beforeproductF)) + ((dst_negative_scale_prefix_append_beforeproductF) + (dst_negative_scale_prefix_append_beforeproductF)))))) /\ (((((exists ff_h_pvs_prefix_append_beforeproductFpositive. ff_h_pvs_prefix_append_beforeproductFpositive + S (dst_positive_prefix_append_beforeproductF) = S ((S (scp_flat_row_prefix_append_beforeproduct)) * dst_positive_scale_prefix_append_beforeproductF)) /\ exists ff_q_pvs_prefix_append_beforeproductFpositive. dst_positive_code_prefix_append_beforeproductF = ff_q_pvs_prefix_append_beforeproductFpositive * S ((S (scp_flat_row_prefix_append_beforeproduct)) * dst_positive_scale_prefix_append_beforeproductF) + (dst_positive_prefix_append_beforeproductF))) /\ (((((exists ff_h_pvs_prefix_append_beforeproductFnegative. ff_h_pvs_prefix_append_beforeproductFnegative + S (dst_negative_prefix_append_beforeproductF) = S ((S (scp_flat_row_prefix_append_beforeproduct)) * dst_negative_scale_prefix_append_beforeproductF)) /\ exists ff_q_pvs_prefix_append_beforeproductFnegative. dst_negative_code_prefix_append_beforeproductF = ff_q_pvs_prefix_append_beforeproductFnegative * S ((S (scp_flat_row_prefix_append_beforeproduct)) * dst_negative_scale_prefix_append_beforeproductF) + (dst_negative_prefix_append_beforeproductF))) /\ (exists ge_balance_positive_prefix_append_beforeproductFvalue ge_balance_negative_prefix_append_beforeproductFvalue. (((((scp_flat_first_prefix_append_beforeproduct) = 2 * (ge_balance_positive_prefix_append_beforeproductFvalue) /\ (ge_balance_negative_prefix_append_beforeproductFvalue) = 0) \/ exists ge_signed_half_prefix_append_beforeproductFvaluedecode. (((scp_flat_first_prefix_append_beforeproduct) = 2 * ge_signed_half_prefix_append_beforeproductFvaluedecode + 1 /\ (ge_balance_positive_prefix_append_beforeproductFvalue) = 0) /\ (ge_balance_negative_prefix_append_beforeproductFvalue) = S ge_signed_half_prefix_append_beforeproductFvaluedecode))) /\ ((dst_positive_prefix_append_beforeproductF) + ge_balance_negative_prefix_append_beforeproductFvalue = (dst_negative_prefix_append_beforeproductF) + ge_balance_positive_prefix_append_beforeproductFvalue))))))))) /\ (((exists dst_positive_code_prefix_append_beforeproductG dst_positive_scale_prefix_append_beforeproductG dst_negative_code_prefix_append_beforeproductG dst_negative_scale_prefix_append_beforeproductG dst_positive_prefix_append_beforeproductG dst_negative_prefix_append_beforeproductG. (((G) = (((((dst_positive_code_prefix_append_beforeproductG) + (dst_positive_scale_prefix_append_beforeproductG)) * S ((dst_positive_code_prefix_append_beforeproductG) + (dst_positive_scale_prefix_append_beforeproductG)) + ((dst_positive_scale_prefix_append_beforeproductG) + (dst_positive_scale_prefix_append_beforeproductG))) + (((dst_negative_code_prefix_append_beforeproductG) + (dst_negative_scale_prefix_append_beforeproductG)) * S ((dst_negative_code_prefix_append_beforeproductG) + (dst_negative_scale_prefix_append_beforeproductG)) + ((dst_negative_scale_prefix_append_beforeproductG) + (dst_negative_scale_prefix_append_beforeproductG)))) * S ((((dst_positive_code_prefix_append_beforeproductG) + (dst_positive_scale_prefix_append_beforeproductG)) * S ((dst_positive_code_prefix_append_beforeproductG) + (dst_positive_scale_prefix_append_beforeproductG)) + ((dst_positive_scale_prefix_append_beforeproductG) + (dst_positive_scale_prefix_append_beforeproductG))) + (((dst_negative_code_prefix_append_beforeproductG) + (dst_negative_scale_prefix_append_beforeproductG)) * S ((dst_negative_code_prefix_append_beforeproductG) + (dst_negative_scale_prefix_append_beforeproductG)) + ((dst_negative_scale_prefix_append_beforeproductG) + (dst_negative_scale_prefix_append_beforeproductG)))) + ((((dst_negative_code_prefix_append_beforeproductG) + (dst_negative_scale_prefix_append_beforeproductG)) * S ((dst_negative_code_prefix_append_beforeproductG) + (dst_negative_scale_prefix_append_beforeproductG)) + ((dst_negative_scale_prefix_append_beforeproductG) + (dst_negative_scale_prefix_append_beforeproductG))) + (((dst_negative_code_prefix_append_beforeproductG) + (dst_negative_scale_prefix_append_beforeproductG)) * S ((dst_negative_code_prefix_append_beforeproductG) + (dst_negative_scale_prefix_append_beforeproductG)) + ((dst_negative_scale_prefix_append_beforeproductG) + (dst_negative_scale_prefix_append_beforeproductG)))))) /\ (((((exists ff_h_pvs_prefix_append_beforeproductGpositive. ff_h_pvs_prefix_append_beforeproductGpositive + S (dst_positive_prefix_append_beforeproductG) = S ((S (scp_flat_column_prefix_append_beforeproduct)) * dst_positive_scale_prefix_append_beforeproductG)) /\ exists ff_q_pvs_prefix_append_beforeproductGpositive. dst_positive_code_prefix_append_beforeproductG = ff_q_pvs_prefix_append_beforeproductGpositive * S ((S (scp_flat_column_prefix_append_beforeproduct)) * dst_positive_scale_prefix_append_beforeproductG) + (dst_positive_prefix_append_beforeproductG))) /\ (((((exists ff_h_pvs_prefix_append_beforeproductGnegative. ff_h_pvs_prefix_append_beforeproductGnegative + S (dst_negative_prefix_append_beforeproductG) = S ((S (scp_flat_column_prefix_append_beforeproduct)) * dst_negative_scale_prefix_append_beforeproductG)) /\ exists ff_q_pvs_prefix_append_beforeproductGnegative. dst_negative_code_prefix_append_beforeproductG = ff_q_pvs_prefix_append_beforeproductGnegative * S ((S (scp_flat_column_prefix_append_beforeproduct)) * dst_negative_scale_prefix_append_beforeproductG) + (dst_negative_prefix_append_beforeproductG))) /\ (exists ge_balance_positive_prefix_append_beforeproductGvalue ge_balance_negative_prefix_append_beforeproductGvalue. (((((scp_flat_second_prefix_append_beforeproduct) = 2 * (ge_balance_positive_prefix_append_beforeproductGvalue) /\ (ge_balance_negative_prefix_append_beforeproductGvalue) = 0) \/ exists ge_signed_half_prefix_append_beforeproductGvaluedecode. (((scp_flat_second_prefix_append_beforeproduct) = 2 * ge_signed_half_prefix_append_beforeproductGvaluedecode + 1 /\ (ge_balance_positive_prefix_append_beforeproductGvalue) = 0) /\ (ge_balance_negative_prefix_append_beforeproductGvalue) = S ge_signed_half_prefix_append_beforeproductGvaluedecode))) /\ ((dst_positive_prefix_append_beforeproductG) + ge_balance_negative_prefix_append_beforeproductGvalue = (dst_negative_prefix_append_beforeproductG) + ge_balance_positive_prefix_append_beforeproductGvalue))))))))) /\ (exists sto_ap_prefix_append_beforeproductvalue sto_an_prefix_append_beforeproductvalue sto_bp_prefix_append_beforeproductvalue sto_bn_prefix_append_beforeproductvalue sto_cp_prefix_append_beforeproductvalue sto_cn_prefix_append_beforeproductvalue. (((((scp_flat_first_prefix_append_beforeproduct) = 2 * (sto_ap_prefix_append_beforeproductvalue) /\ (sto_an_prefix_append_beforeproductvalue) = 0) \/ exists ge_signed_half_prefix_append_beforeproductvalueleft. (((scp_flat_first_prefix_append_beforeproduct) = 2 * ge_signed_half_prefix_append_beforeproductvalueleft + 1 /\ (sto_ap_prefix_append_beforeproductvalue) = 0) /\ (sto_an_prefix_append_beforeproductvalue) = S ge_signed_half_prefix_append_beforeproductvalueleft))) /\ ((((((scp_flat_second_prefix_append_beforeproduct) = 2 * (sto_bp_prefix_append_beforeproductvalue) /\ (sto_bn_prefix_append_beforeproductvalue) = 0) \/ exists ge_signed_half_prefix_append_beforeproductvalueright. (((scp_flat_second_prefix_append_beforeproduct) = 2 * ge_signed_half_prefix_append_beforeproductvalueright + 1 /\ (sto_bp_prefix_append_beforeproductvalue) = 0) /\ (sto_bn_prefix_append_beforeproductvalue) = S ge_signed_half_prefix_append_beforeproductvalueright))) /\ ((((((scp_flat_value_prefix_append_before) = 2 * (sto_cp_prefix_append_beforeproductvalue) /\ (sto_cn_prefix_append_beforeproductvalue) = 0) \/ exists ge_signed_half_prefix_append_beforeproductvalueoutput. (((scp_flat_value_prefix_append_before) = 2 * ge_signed_half_prefix_append_beforeproductvalueoutput + 1 /\ (sto_cp_prefix_append_beforeproductvalue) = 0) /\ (sto_cn_prefix_append_beforeproductvalue) = S ge_signed_half_prefix_append_beforeproductvalueoutput))) /\ ((sto_ap_prefix_append_beforeproductvalue * sto_bp_prefix_append_beforeproductvalue + sto_an_prefix_append_beforeproductvalue * sto_bn_prefix_append_beforeproductvalue) + sto_cn_prefix_append_beforeproductvalue = (sto_ap_prefix_append_beforeproductvalue * sto_bn_prefix_append_beforeproductvalue + sto_an_prefix_append_beforeproductvalue * sto_bp_prefix_append_beforeproductvalue) + sto_cp_prefix_append_beforeproductvalue)))))))))))))))))) -> (exists scp_flat_row_prefix_append_value scp_flat_column_prefix_append_value scp_flat_first_prefix_append_value scp_flat_second_prefix_append_value. (((S l)=((n)*(scp_flat_row_prefix_append_value)+(scp_flat_column_prefix_append_value))) /\ (((exists pvs_gap_prefix_append_valueremainder. pvs_gap_prefix_append_valueremainder + S (scp_flat_column_prefix_append_value) = (n)) /\ (((exists dst_positive_code_prefix_append_valueF dst_positive_scale_prefix_append_valueF dst_negative_code_prefix_append_valueF dst_negative_scale_prefix_append_valueF dst_positive_prefix_append_valueF dst_negative_prefix_append_valueF. (((F) = (((((dst_positive_code_prefix_append_valueF) + (dst_positive_scale_prefix_append_valueF)) * S ((dst_positive_code_prefix_append_valueF) + (dst_positive_scale_prefix_append_valueF)) + ((dst_positive_scale_prefix_append_valueF) + (dst_positive_scale_prefix_append_valueF))) + (((dst_negative_code_prefix_append_valueF) + (dst_negative_scale_prefix_append_valueF)) * S ((dst_negative_code_prefix_append_valueF) + (dst_negative_scale_prefix_append_valueF)) + ((dst_negative_scale_prefix_append_valueF) + (dst_negative_scale_prefix_append_valueF)))) * S ((((dst_positive_code_prefix_append_valueF) + (dst_positive_scale_prefix_append_valueF)) * S ((dst_positive_code_prefix_append_valueF) + (dst_positive_scale_prefix_append_valueF)) + ((dst_positive_scale_prefix_append_valueF) + (dst_positive_scale_prefix_append_valueF))) + (((dst_negative_code_prefix_append_valueF) + (dst_negative_scale_prefix_append_valueF)) * S ((dst_negative_code_prefix_append_valueF) + (dst_negative_scale_prefix_append_valueF)) + ((dst_negative_scale_prefix_append_valueF) + (dst_negative_scale_prefix_append_valueF)))) + ((((dst_negative_code_prefix_append_valueF) + (dst_negative_scale_prefix_append_valueF)) * S ((dst_negative_code_prefix_append_valueF) + (dst_negative_scale_prefix_append_valueF)) + ((dst_negative_scale_prefix_append_valueF) + (dst_negative_scale_prefix_append_valueF))) + (((dst_negative_code_prefix_append_valueF) + (dst_negative_scale_prefix_append_valueF)) * S ((dst_negative_code_prefix_append_valueF) + (dst_negative_scale_prefix_append_valueF)) + ((dst_negative_scale_prefix_append_valueF) + (dst_negative_scale_prefix_append_valueF)))))) /\ (((((exists ff_h_pvs_prefix_append_valueFpositive. ff_h_pvs_prefix_append_valueFpositive + S (dst_positive_prefix_append_valueF) = S ((S (scp_flat_row_prefix_append_value)) * dst_positive_scale_prefix_append_valueF)) /\ exists ff_q_pvs_prefix_append_valueFpositive. dst_positive_code_prefix_append_valueF = ff_q_pvs_prefix_append_valueFpositive * S ((S (scp_flat_row_prefix_append_value)) * dst_positive_scale_prefix_append_valueF) + (dst_positive_prefix_append_valueF))) /\ (((((exists ff_h_pvs_prefix_append_valueFnegative. ff_h_pvs_prefix_append_valueFnegative + S (dst_negative_prefix_append_valueF) = S ((S (scp_flat_row_prefix_append_value)) * dst_negative_scale_prefix_append_valueF)) /\ exists ff_q_pvs_prefix_append_valueFnegative. dst_negative_code_prefix_append_valueF = ff_q_pvs_prefix_append_valueFnegative * S ((S (scp_flat_row_prefix_append_value)) * dst_negative_scale_prefix_append_valueF) + (dst_negative_prefix_append_valueF))) /\ (exists ge_balance_positive_prefix_append_valueFvalue ge_balance_negative_prefix_append_valueFvalue. (((((scp_flat_first_prefix_append_value) = 2 * (ge_balance_positive_prefix_append_valueFvalue) /\ (ge_balance_negative_prefix_append_valueFvalue) = 0) \/ exists ge_signed_half_prefix_append_valueFvaluedecode. (((scp_flat_first_prefix_append_value) = 2 * ge_signed_half_prefix_append_valueFvaluedecode + 1 /\ (ge_balance_positive_prefix_append_valueFvalue) = 0) /\ (ge_balance_negative_prefix_append_valueFvalue) = S ge_signed_half_prefix_append_valueFvaluedecode))) /\ ((dst_positive_prefix_append_valueF) + ge_balance_negative_prefix_append_valueFvalue = (dst_negative_prefix_append_valueF) + ge_balance_positive_prefix_append_valueFvalue))))))))) /\ (((exists dst_positive_code_prefix_append_valueG dst_positive_scale_prefix_append_valueG dst_negative_code_prefix_append_valueG dst_negative_scale_prefix_append_valueG dst_positive_prefix_append_valueG dst_negative_prefix_append_valueG. (((G) = (((((dst_positive_code_prefix_append_valueG) + (dst_positive_scale_prefix_append_valueG)) * S ((dst_positive_code_prefix_append_valueG) + (dst_positive_scale_prefix_append_valueG)) + ((dst_positive_scale_prefix_append_valueG) + (dst_positive_scale_prefix_append_valueG))) + (((dst_negative_code_prefix_append_valueG) + (dst_negative_scale_prefix_append_valueG)) * S ((dst_negative_code_prefix_append_valueG) + (dst_negative_scale_prefix_append_valueG)) + ((dst_negative_scale_prefix_append_valueG) + (dst_negative_scale_prefix_append_valueG)))) * S ((((dst_positive_code_prefix_append_valueG) + (dst_positive_scale_prefix_append_valueG)) * S ((dst_positive_code_prefix_append_valueG) + (dst_positive_scale_prefix_append_valueG)) + ((dst_positive_scale_prefix_append_valueG) + (dst_positive_scale_prefix_append_valueG))) + (((dst_negative_code_prefix_append_valueG) + (dst_negative_scale_prefix_append_valueG)) * S ((dst_negative_code_prefix_append_valueG) + (dst_negative_scale_prefix_append_valueG)) + ((dst_negative_scale_prefix_append_valueG) + (dst_negative_scale_prefix_append_valueG)))) + ((((dst_negative_code_prefix_append_valueG) + (dst_negative_scale_prefix_append_valueG)) * S ((dst_negative_code_prefix_append_valueG) + (dst_negative_scale_prefix_append_valueG)) + ((dst_negative_scale_prefix_append_valueG) + (dst_negative_scale_prefix_append_valueG))) + (((dst_negative_code_prefix_append_valueG) + (dst_negative_scale_prefix_append_valueG)) * S ((dst_negative_code_prefix_append_valueG) + (dst_negative_scale_prefix_append_valueG)) + ((dst_negative_scale_prefix_append_valueG) + (dst_negative_scale_prefix_append_valueG)))))) /\ (((((exists ff_h_pvs_prefix_append_valueGpositive. ff_h_pvs_prefix_append_valueGpositive + S (dst_positive_prefix_append_valueG) = S ((S (scp_flat_column_prefix_append_value)) * dst_positive_scale_prefix_append_valueG)) /\ exists ff_q_pvs_prefix_append_valueGpositive. dst_positive_code_prefix_append_valueG = ff_q_pvs_prefix_append_valueGpositive * S ((S (scp_flat_column_prefix_append_value)) * dst_positive_scale_prefix_append_valueG) + (dst_positive_prefix_append_valueG))) /\ (((((exists ff_h_pvs_prefix_append_valueGnegative. ff_h_pvs_prefix_append_valueGnegative + S (dst_negative_prefix_append_valueG) = S ((S (scp_flat_column_prefix_append_value)) * dst_negative_scale_prefix_append_valueG)) /\ exists ff_q_pvs_prefix_append_valueGnegative. dst_negative_code_prefix_append_valueG = ff_q_pvs_prefix_append_valueGnegative * S ((S (scp_flat_column_prefix_append_value)) * dst_negative_scale_prefix_append_valueG) + (dst_negative_prefix_append_valueG))) /\ (exists ge_balance_positive_prefix_append_valueGvalue ge_balance_negative_prefix_append_valueGvalue. (((((scp_flat_second_prefix_append_value) = 2 * (ge_balance_positive_prefix_append_valueGvalue) /\ (ge_balance_negative_prefix_append_valueGvalue) = 0) \/ exists ge_signed_half_prefix_append_valueGvaluedecode. (((scp_flat_second_prefix_append_value) = 2 * ge_signed_half_prefix_append_valueGvaluedecode + 1 /\ (ge_balance_positive_prefix_append_valueGvalue) = 0) /\ (ge_balance_negative_prefix_append_valueGvalue) = S ge_signed_half_prefix_append_valueGvaluedecode))) /\ ((dst_positive_prefix_append_valueG) + ge_balance_negative_prefix_append_valueGvalue = (dst_negative_prefix_append_valueG) + ge_balance_positive_prefix_append_valueGvalue))))))))) /\ (exists sto_ap_prefix_append_valuevalue sto_an_prefix_append_valuevalue sto_bp_prefix_append_valuevalue sto_bn_prefix_append_valuevalue sto_cp_prefix_append_valuevalue sto_cn_prefix_append_valuevalue. (((((scp_flat_first_prefix_append_value) = 2 * (sto_ap_prefix_append_valuevalue) /\ (sto_an_prefix_append_valuevalue) = 0) \/ exists ge_signed_half_prefix_append_valuevalueleft. (((scp_flat_first_prefix_append_value) = 2 * ge_signed_half_prefix_append_valuevalueleft + 1 /\ (sto_ap_prefix_append_valuevalue) = 0) /\ (sto_an_prefix_append_valuevalue) = S ge_signed_half_prefix_append_valuevalueleft))) /\ ((((((scp_flat_second_prefix_append_value) = 2 * (sto_bp_prefix_append_valuevalue) /\ (sto_bn_prefix_append_valuevalue) = 0) \/ exists ge_signed_half_prefix_append_valuevalueright. (((scp_flat_second_prefix_append_value) = 2 * ge_signed_half_prefix_append_valuevalueright + 1 /\ (sto_bp_prefix_append_valuevalue) = 0) /\ (sto_bn_prefix_append_valuevalue) = S ge_signed_half_prefix_append_valuevalueright))) /\ ((((((z) = 2 * (sto_cp_prefix_append_valuevalue) /\ (sto_cn_prefix_append_valuevalue) = 0) \/ exists ge_signed_half_prefix_append_valuevalueoutput. (((z) = 2 * ge_signed_half_prefix_append_valuevalueoutput + 1 /\ (sto_cp_prefix_append_valuevalue) = 0) /\ (sto_cn_prefix_append_valuevalue) = S ge_signed_half_prefix_append_valuevalueoutput))) /\ ((sto_ap_prefix_append_valuevalue * sto_bp_prefix_append_valuevalue + sto_an_prefix_append_valuevalue * sto_bn_prefix_append_valuevalue) + sto_cn_prefix_append_valuevalue = (sto_ap_prefix_append_valuevalue * sto_bn_prefix_append_valuevalue + sto_an_prefix_append_valuevalue * sto_bp_prefix_append_valuevalue) + sto_cp_prefix_append_valuevalue))))))))))))))) -> exists U. ((((exists dst_positive_code_prefix_append_aftertable dst_positive_scale_prefix_append_aftertable dst_negative_code_prefix_append_aftertable dst_negative_scale_prefix_append_aftertable. (((U) = (((((dst_positive_code_prefix_append_aftertable) + (dst_positive_scale_prefix_append_aftertable)) * S ((dst_positive_code_prefix_append_aftertable) + (dst_positive_scale_prefix_append_aftertable)) + ((dst_positive_scale_prefix_append_aftertable) + (dst_positive_scale_prefix_append_aftertable))) + (((dst_negative_code_prefix_append_aftertable) + (dst_negative_scale_prefix_append_aftertable)) * S ((dst_negative_code_prefix_append_aftertable) + (dst_negative_scale_prefix_append_aftertable)) + ((dst_negative_scale_prefix_append_aftertable) + (dst_negative_scale_prefix_append_aftertable)))) * S ((((dst_positive_code_prefix_append_aftertable) + (dst_positive_scale_prefix_append_aftertable)) * S ((dst_positive_code_prefix_append_aftertable) + (dst_positive_scale_prefix_append_aftertable)) + ((dst_positive_scale_prefix_append_aftertable) + (dst_positive_scale_prefix_append_aftertable))) + (((dst_negative_code_prefix_append_aftertable) + (dst_negative_scale_prefix_append_aftertable)) * S ((dst_negative_code_prefix_append_aftertable) + (dst_negative_scale_prefix_append_aftertable)) + ((dst_negative_scale_prefix_append_aftertable) + (dst_negative_scale_prefix_append_aftertable)))) + ((((dst_negative_code_prefix_append_aftertable) + (dst_negative_scale_prefix_append_aftertable)) * S ((dst_negative_code_prefix_append_aftertable) + (dst_negative_scale_prefix_append_aftertable)) + ((dst_negative_scale_prefix_append_aftertable) + (dst_negative_scale_prefix_append_aftertable))) + (((dst_negative_code_prefix_append_aftertable) + (dst_negative_scale_prefix_append_aftertable)) * S ((dst_negative_code_prefix_append_aftertable) + (dst_negative_scale_prefix_append_aftertable)) + ((dst_negative_scale_prefix_append_aftertable) + (dst_negative_scale_prefix_append_aftertable)))))) /\ (forall dst_index_prefix_append_aftertable. (exists pvs_le_gap_prefix_append_aftertabledomain. pvs_le_gap_prefix_append_aftertabledomain + (dst_index_prefix_append_aftertable) = (S l)) -> exists dst_positive_prefix_append_aftertable dst_negative_prefix_append_aftertable dst_value_prefix_append_aftertable. ((((exists ff_h_pvs_prefix_append_aftertableentrypositive. ff_h_pvs_prefix_append_aftertableentrypositive + S (dst_positive_prefix_append_aftertable) = S ((S (dst_index_prefix_append_aftertable)) * dst_positive_scale_prefix_append_aftertable)) /\ exists ff_q_pvs_prefix_append_aftertableentrypositive. dst_positive_code_prefix_append_aftertable = ff_q_pvs_prefix_append_aftertableentrypositive * S ((S (dst_index_prefix_append_aftertable)) * dst_positive_scale_prefix_append_aftertable) + (dst_positive_prefix_append_aftertable))) /\ (((((exists ff_h_pvs_prefix_append_aftertableentrynegative. ff_h_pvs_prefix_append_aftertableentrynegative + S (dst_negative_prefix_append_aftertable) = S ((S (dst_index_prefix_append_aftertable)) * dst_negative_scale_prefix_append_aftertable)) /\ exists ff_q_pvs_prefix_append_aftertableentrynegative. dst_negative_code_prefix_append_aftertable = ff_q_pvs_prefix_append_aftertableentrynegative * S ((S (dst_index_prefix_append_aftertable)) * dst_negative_scale_prefix_append_aftertable) + (dst_negative_prefix_append_aftertable))) /\ (exists ge_balance_positive_prefix_append_aftertableentryvalue ge_balance_negative_prefix_append_aftertableentryvalue. (((((dst_value_prefix_append_aftertable) = 2 * (ge_balance_positive_prefix_append_aftertableentryvalue) /\ (ge_balance_negative_prefix_append_aftertableentryvalue) = 0) \/ exists ge_signed_half_prefix_append_aftertableentryvaluedecode. (((dst_value_prefix_append_aftertable) = 2 * ge_signed_half_prefix_append_aftertableentryvaluedecode + 1 /\ (ge_balance_positive_prefix_append_aftertableentryvalue) = 0) /\ (ge_balance_negative_prefix_append_aftertableentryvalue) = S ge_signed_half_prefix_append_aftertableentryvaluedecode))) /\ ((dst_positive_prefix_append_aftertable) + ge_balance_negative_prefix_append_aftertableentryvalue = (dst_negative_prefix_append_aftertable) + ge_balance_positive_prefix_append_aftertableentryvalue))))))))) /\ (forall scp_flat_index_prefix_append_after scp_flat_value_prefix_append_after. (exists pvs_le_gap_prefix_append_afterbound. pvs_le_gap_prefix_append_afterbound + (scp_flat_index_prefix_append_after) = (S l)) -> (exists dst_positive_code_prefix_append_afterentry dst_positive_scale_prefix_append_afterentry dst_negative_code_prefix_append_afterentry dst_negative_scale_prefix_append_afterentry dst_positive_prefix_append_afterentry dst_negative_prefix_append_afterentry. (((U) = (((((dst_positive_code_prefix_append_afterentry) + (dst_positive_scale_prefix_append_afterentry)) * S ((dst_positive_code_prefix_append_afterentry) + (dst_positive_scale_prefix_append_afterentry)) + ((dst_positive_scale_prefix_append_afterentry) + (dst_positive_scale_prefix_append_afterentry))) + (((dst_negative_code_prefix_append_afterentry) + (dst_negative_scale_prefix_append_afterentry)) * S ((dst_negative_code_prefix_append_afterentry) + (dst_negative_scale_prefix_append_afterentry)) + ((dst_negative_scale_prefix_append_afterentry) + (dst_negative_scale_prefix_append_afterentry)))) * S ((((dst_positive_code_prefix_append_afterentry) + (dst_positive_scale_prefix_append_afterentry)) * S ((dst_positive_code_prefix_append_afterentry) + (dst_positive_scale_prefix_append_afterentry)) + ((dst_positive_scale_prefix_append_afterentry) + (dst_positive_scale_prefix_append_afterentry))) + (((dst_negative_code_prefix_append_afterentry) + (dst_negative_scale_prefix_append_afterentry)) * S ((dst_negative_code_prefix_append_afterentry) + (dst_negative_scale_prefix_append_afterentry)) + ((dst_negative_scale_prefix_append_afterentry) + (dst_negative_scale_prefix_append_afterentry)))) + ((((dst_negative_code_prefix_append_afterentry) + (dst_negative_scale_prefix_append_afterentry)) * S ((dst_negative_code_prefix_append_afterentry) + (dst_negative_scale_prefix_append_afterentry)) + ((dst_negative_scale_prefix_append_afterentry) + (dst_negative_scale_prefix_append_afterentry))) + (((dst_negative_code_prefix_append_afterentry) + (dst_negative_scale_prefix_append_afterentry)) * S ((dst_negative_code_prefix_append_afterentry) + (dst_negative_scale_prefix_append_afterentry)) + ((dst_negative_scale_prefix_append_afterentry) + (dst_negative_scale_prefix_append_afterentry)))))) /\ (((((exists ff_h_pvs_prefix_append_afterentrypositive. ff_h_pvs_prefix_append_afterentrypositive + S (dst_positive_prefix_append_afterentry) = S ((S (scp_flat_index_prefix_append_after)) * dst_positive_scale_prefix_append_afterentry)) /\ exists ff_q_pvs_prefix_append_afterentrypositive. dst_positive_code_prefix_append_afterentry = ff_q_pvs_prefix_append_afterentrypositive * S ((S (scp_flat_index_prefix_append_after)) * dst_positive_scale_prefix_append_afterentry) + (dst_positive_prefix_append_afterentry))) /\ (((((exists ff_h_pvs_prefix_append_afterentrynegative. ff_h_pvs_prefix_append_afterentrynegative + S (dst_negative_prefix_append_afterentry) = S ((S (scp_flat_index_prefix_append_after)) * dst_negative_scale_prefix_append_afterentry)) /\ exists ff_q_pvs_prefix_append_afterentrynegative. dst_negative_code_prefix_append_afterentry = ff_q_pvs_prefix_append_afterentrynegative * S ((S (scp_flat_index_prefix_append_after)) * dst_negative_scale_prefix_append_afterentry) + (dst_negative_prefix_append_afterentry))) /\ (exists ge_balance_positive_prefix_append_afterentryvalue ge_balance_negative_prefix_append_afterentryvalue. (((((scp_flat_value_prefix_append_after) = 2 * (ge_balance_positive_prefix_append_afterentryvalue) /\ (ge_balance_negative_prefix_append_afterentryvalue) = 0) \/ exists ge_signed_half_prefix_append_afterentryvaluedecode. (((scp_flat_value_prefix_append_after) = 2 * ge_signed_half_prefix_append_afterentryvaluedecode + 1 /\ (ge_balance_positive_prefix_append_afterentryvalue) = 0) /\ (ge_balance_negative_prefix_append_afterentryvalue) = S ge_signed_half_prefix_append_afterentryvaluedecode))) /\ ((dst_positive_prefix_append_afterentry) + ge_balance_negative_prefix_append_afterentryvalue = (dst_negative_prefix_append_afterentry) + ge_balance_positive_prefix_append_afterentryvalue))))))))) -> (exists scp_flat_row_prefix_append_afterproduct scp_flat_column_prefix_append_afterproduct scp_flat_first_prefix_append_afterproduct scp_flat_second_prefix_append_afterproduct. (((scp_flat_index_prefix_append_after)=((n)*(scp_flat_row_prefix_append_afterproduct)+(scp_flat_column_prefix_append_afterproduct))) /\ (((exists pvs_gap_prefix_append_afterproductremainder. pvs_gap_prefix_append_afterproductremainder + S (scp_flat_column_prefix_append_afterproduct) = (n)) /\ (((exists dst_positive_code_prefix_append_afterproductF dst_positive_scale_prefix_append_afterproductF dst_negative_code_prefix_append_afterproductF dst_negative_scale_prefix_append_afterproductF dst_positive_prefix_append_afterproductF dst_negative_prefix_append_afterproductF. (((F) = (((((dst_positive_code_prefix_append_afterproductF) + (dst_positive_scale_prefix_append_afterproductF)) * S ((dst_positive_code_prefix_append_afterproductF) + (dst_positive_scale_prefix_append_afterproductF)) + ((dst_positive_scale_prefix_append_afterproductF) + (dst_positive_scale_prefix_append_afterproductF))) + (((dst_negative_code_prefix_append_afterproductF) + (dst_negative_scale_prefix_append_afterproductF)) * S ((dst_negative_code_prefix_append_afterproductF) + (dst_negative_scale_prefix_append_afterproductF)) + ((dst_negative_scale_prefix_append_afterproductF) + (dst_negative_scale_prefix_append_afterproductF)))) * S ((((dst_positive_code_prefix_append_afterproductF) + (dst_positive_scale_prefix_append_afterproductF)) * S ((dst_positive_code_prefix_append_afterproductF) + (dst_positive_scale_prefix_append_afterproductF)) + ((dst_positive_scale_prefix_append_afterproductF) + (dst_positive_scale_prefix_append_afterproductF))) + (((dst_negative_code_prefix_append_afterproductF) + (dst_negative_scale_prefix_append_afterproductF)) * S ((dst_negative_code_prefix_append_afterproductF) + (dst_negative_scale_prefix_append_afterproductF)) + ((dst_negative_scale_prefix_append_afterproductF) + (dst_negative_scale_prefix_append_afterproductF)))) + ((((dst_negative_code_prefix_append_afterproductF) + (dst_negative_scale_prefix_append_afterproductF)) * S ((dst_negative_code_prefix_append_afterproductF) + (dst_negative_scale_prefix_append_afterproductF)) + ((dst_negative_scale_prefix_append_afterproductF) + (dst_negative_scale_prefix_append_afterproductF))) + (((dst_negative_code_prefix_append_afterproductF) + (dst_negative_scale_prefix_append_afterproductF)) * S ((dst_negative_code_prefix_append_afterproductF) + (dst_negative_scale_prefix_append_afterproductF)) + ((dst_negative_scale_prefix_append_afterproductF) + (dst_negative_scale_prefix_append_afterproductF)))))) /\ (((((exists ff_h_pvs_prefix_append_afterproductFpositive. ff_h_pvs_prefix_append_afterproductFpositive + S (dst_positive_prefix_append_afterproductF) = S ((S (scp_flat_row_prefix_append_afterproduct)) * dst_positive_scale_prefix_append_afterproductF)) /\ exists ff_q_pvs_prefix_append_afterproductFpositive. dst_positive_code_prefix_append_afterproductF = ff_q_pvs_prefix_append_afterproductFpositive * S ((S (scp_flat_row_prefix_append_afterproduct)) * dst_positive_scale_prefix_append_afterproductF) + (dst_positive_prefix_append_afterproductF))) /\ (((((exists ff_h_pvs_prefix_append_afterproductFnegative. ff_h_pvs_prefix_append_afterproductFnegative + S (dst_negative_prefix_append_afterproductF) = S ((S (scp_flat_row_prefix_append_afterproduct)) * dst_negative_scale_prefix_append_afterproductF)) /\ exists ff_q_pvs_prefix_append_afterproductFnegative. dst_negative_code_prefix_append_afterproductF = ff_q_pvs_prefix_append_afterproductFnegative * S ((S (scp_flat_row_prefix_append_afterproduct)) * dst_negative_scale_prefix_append_afterproductF) + (dst_negative_prefix_append_afterproductF))) /\ (exists ge_balance_positive_prefix_append_afterproductFvalue ge_balance_negative_prefix_append_afterproductFvalue. (((((scp_flat_first_prefix_append_afterproduct) = 2 * (ge_balance_positive_prefix_append_afterproductFvalue) /\ (ge_balance_negative_prefix_append_afterproductFvalue) = 0) \/ exists ge_signed_half_prefix_append_afterproductFvaluedecode. (((scp_flat_first_prefix_append_afterproduct) = 2 * ge_signed_half_prefix_append_afterproductFvaluedecode + 1 /\ (ge_balance_positive_prefix_append_afterproductFvalue) = 0) /\ (ge_balance_negative_prefix_append_afterproductFvalue) = S ge_signed_half_prefix_append_afterproductFvaluedecode))) /\ ((dst_positive_prefix_append_afterproductF) + ge_balance_negative_prefix_append_afterproductFvalue = (dst_negative_prefix_append_afterproductF) + ge_balance_positive_prefix_append_afterproductFvalue))))))))) /\ (((exists dst_positive_code_prefix_append_afterproductG dst_positive_scale_prefix_append_afterproductG dst_negative_code_prefix_append_afterproductG dst_negative_scale_prefix_append_afterproductG dst_positive_prefix_append_afterproductG dst_negative_prefix_append_afterproductG. (((G) = (((((dst_positive_code_prefix_append_afterproductG) + (dst_positive_scale_prefix_append_afterproductG)) * S ((dst_positive_code_prefix_append_afterproductG) + (dst_positive_scale_prefix_append_afterproductG)) + ((dst_positive_scale_prefix_append_afterproductG) + (dst_positive_scale_prefix_append_afterproductG))) + (((dst_negative_code_prefix_append_afterproductG) + (dst_negative_scale_prefix_append_afterproductG)) * S ((dst_negative_code_prefix_append_afterproductG) + (dst_negative_scale_prefix_append_afterproductG)) + ((dst_negative_scale_prefix_append_afterproductG) + (dst_negative_scale_prefix_append_afterproductG)))) * S ((((dst_positive_code_prefix_append_afterproductG) + (dst_positive_scale_prefix_append_afterproductG)) * S ((dst_positive_code_prefix_append_afterproductG) + (dst_positive_scale_prefix_append_afterproductG)) + ((dst_positive_scale_prefix_append_afterproductG) + (dst_positive_scale_prefix_append_afterproductG))) + (((dst_negative_code_prefix_append_afterproductG) + (dst_negative_scale_prefix_append_afterproductG)) * S ((dst_negative_code_prefix_append_afterproductG) + (dst_negative_scale_prefix_append_afterproductG)) + ((dst_negative_scale_prefix_append_afterproductG) + (dst_negative_scale_prefix_append_afterproductG)))) + ((((dst_negative_code_prefix_append_afterproductG) + (dst_negative_scale_prefix_append_afterproductG)) * S ((dst_negative_code_prefix_append_afterproductG) + (dst_negative_scale_prefix_append_afterproductG)) + ((dst_negative_scale_prefix_append_afterproductG) + (dst_negative_scale_prefix_append_afterproductG))) + (((dst_negative_code_prefix_append_afterproductG) + (dst_negative_scale_prefix_append_afterproductG)) * S ((dst_negative_code_prefix_append_afterproductG) + (dst_negative_scale_prefix_append_afterproductG)) + ((dst_negative_scale_prefix_append_afterproductG) + (dst_negative_scale_prefix_append_afterproductG)))))) /\ (((((exists ff_h_pvs_prefix_append_afterproductGpositive. ff_h_pvs_prefix_append_afterproductGpositive + S (dst_positive_prefix_append_afterproductG) = S ((S (scp_flat_column_prefix_append_afterproduct)) * dst_positive_scale_prefix_append_afterproductG)) /\ exists ff_q_pvs_prefix_append_afterproductGpositive. dst_positive_code_prefix_append_afterproductG = ff_q_pvs_prefix_append_afterproductGpositive * S ((S (scp_flat_column_prefix_append_afterproduct)) * dst_positive_scale_prefix_append_afterproductG) + (dst_positive_prefix_append_afterproductG))) /\ (((((exists ff_h_pvs_prefix_append_afterproductGnegative. ff_h_pvs_prefix_append_afterproductGnegative + S (dst_negative_prefix_append_afterproductG) = S ((S (scp_flat_column_prefix_append_afterproduct)) * dst_negative_scale_prefix_append_afterproductG)) /\ exists ff_q_pvs_prefix_append_afterproductGnegative. dst_negative_code_prefix_append_afterproductG = ff_q_pvs_prefix_append_afterproductGnegative * S ((S (scp_flat_column_prefix_append_afterproduct)) * dst_negative_scale_prefix_append_afterproductG) + (dst_negative_prefix_append_afterproductG))) /\ (exists ge_balance_positive_prefix_append_afterproductGvalue ge_balance_negative_prefix_append_afterproductGvalue. (((((scp_flat_second_prefix_append_afterproduct) = 2 * (ge_balance_positive_prefix_append_afterproductGvalue) /\ (ge_balance_negative_prefix_append_afterproductGvalue) = 0) \/ exists ge_signed_half_prefix_append_afterproductGvaluedecode. (((scp_flat_second_prefix_append_afterproduct) = 2 * ge_signed_half_prefix_append_afterproductGvaluedecode + 1 /\ (ge_balance_positive_prefix_append_afterproductGvalue) = 0) /\ (ge_balance_negative_prefix_append_afterproductGvalue) = S ge_signed_half_prefix_append_afterproductGvaluedecode))) /\ ((dst_positive_prefix_append_afterproductG) + ge_balance_negative_prefix_append_afterproductGvalue = (dst_negative_prefix_append_afterproductG) + ge_balance_positive_prefix_append_afterproductGvalue))))))))) /\ (exists sto_ap_prefix_append_afterproductvalue sto_an_prefix_append_afterproductvalue sto_bp_prefix_append_afterproductvalue sto_bn_prefix_append_afterproductvalue sto_cp_prefix_append_afterproductvalue sto_cn_prefix_append_afterproductvalue. (((((scp_flat_first_prefix_append_afterproduct) = 2 * (sto_ap_prefix_append_afterproductvalue) /\ (sto_an_prefix_append_afterproductvalue) = 0) \/ exists ge_signed_half_prefix_append_afterproductvalueleft. (((scp_flat_first_prefix_append_afterproduct) = 2 * ge_signed_half_prefix_append_afterproductvalueleft + 1 /\ (sto_ap_prefix_append_afterproductvalue) = 0) /\ (sto_an_prefix_append_afterproductvalue) = S ge_signed_half_prefix_append_afterproductvalueleft))) /\ ((((((scp_flat_second_prefix_append_afterproduct) = 2 * (sto_bp_prefix_append_afterproductvalue) /\ (sto_bn_prefix_append_afterproductvalue) = 0) \/ exists ge_signed_half_prefix_append_afterproductvalueright. (((scp_flat_second_prefix_append_afterproduct) = 2 * ge_signed_half_prefix_append_afterproductvalueright + 1 /\ (sto_bp_prefix_append_afterproductvalue) = 0) /\ (sto_bn_prefix_append_afterproductvalue) = S ge_signed_half_prefix_append_afterproductvalueright))) /\ ((((((scp_flat_value_prefix_append_after) = 2 * (sto_cp_prefix_append_afterproductvalue) /\ (sto_cn_prefix_append_afterproductvalue) = 0) \/ exists ge_signed_half_prefix_append_afterproductvalueoutput. (((scp_flat_value_prefix_append_after) = 2 * ge_signed_half_prefix_append_afterproductvalueoutput + 1 /\ (sto_cp_prefix_append_afterproductvalue) = 0) /\ (sto_cn_prefix_append_afterproductvalue) = S ge_signed_half_prefix_append_afterproductvalueoutput))) /\ ((sto_ap_prefix_append_afterproductvalue * sto_bp_prefix_append_afterproductvalue + sto_an_prefix_append_afterproductvalue * sto_bn_prefix_append_afterproductvalue) + sto_cn_prefix_append_afterproductvalue = (sto_ap_prefix_append_afterproductvalue * sto_bn_prefix_append_afterproductvalue + sto_an_prefix_append_afterproductvalue * sto_bp_prefix_append_afterproductvalue) + sto_cp_prefix_append_afterproductvalue)))))))))))))))))) /\ (forall dst_index_prefix_append_equal dst_first_prefix_append_equal dst_second_prefix_append_equal. (exists pvs_gap_prefix_append_equalbound. pvs_gap_prefix_append_equalbound + S (dst_index_prefix_append_equal) = (S l)) -> (exists dst_positive_code_prefix_append_equalfirst dst_positive_scale_prefix_append_equalfirst dst_negative_code_prefix_append_equalfirst dst_negative_scale_prefix_append_equalfirst dst_positive_prefix_append_equalfirst dst_negative_prefix_append_equalfirst. (((T) = (((((dst_positive_code_prefix_append_equalfirst) + (dst_positive_scale_prefix_append_equalfirst)) * S ((dst_positive_code_prefix_append_equalfirst) + (dst_positive_scale_prefix_append_equalfirst)) + ((dst_positive_scale_prefix_append_equalfirst) + (dst_positive_scale_prefix_append_equalfirst))) + (((dst_negative_code_prefix_append_equalfirst) + (dst_negative_scale_prefix_append_equalfirst)) * S ((dst_negative_code_prefix_append_equalfirst) + (dst_negative_scale_prefix_append_equalfirst)) + ((dst_negative_scale_prefix_append_equalfirst) + (dst_negative_scale_prefix_append_equalfirst)))) * S ((((dst_positive_code_prefix_append_equalfirst) + (dst_positive_scale_prefix_append_equalfirst)) * S ((dst_positive_code_prefix_append_equalfirst) + (dst_positive_scale_prefix_append_equalfirst)) + ((dst_positive_scale_prefix_append_equalfirst) + (dst_positive_scale_prefix_append_equalfirst))) + (((dst_negative_code_prefix_append_equalfirst) + (dst_negative_scale_prefix_append_equalfirst)) * S ((dst_negative_code_prefix_append_equalfirst) + (dst_negative_scale_prefix_append_equalfirst)) + ((dst_negative_scale_prefix_append_equalfirst) + (dst_negative_scale_prefix_append_equalfirst)))) + ((((dst_negative_code_prefix_append_equalfirst) + (dst_negative_scale_prefix_append_equalfirst)) * S ((dst_negative_code_prefix_append_equalfirst) + (dst_negative_scale_prefix_append_equalfirst)) + ((dst_negative_scale_prefix_append_equalfirst) + (dst_negative_scale_prefix_append_equalfirst))) + (((dst_negative_code_prefix_append_equalfirst) + (dst_negative_scale_prefix_append_equalfirst)) * S ((dst_negative_code_prefix_append_equalfirst) + (dst_negative_scale_prefix_append_equalfirst)) + ((dst_negative_scale_prefix_append_equalfirst) + (dst_negative_scale_prefix_append_equalfirst)))))) /\ (((((exists ff_h_pvs_prefix_append_equalfirstpositive. ff_h_pvs_prefix_append_equalfirstpositive + S (dst_positive_prefix_append_equalfirst) = S ((S (dst_index_prefix_append_equal)) * dst_positive_scale_prefix_append_equalfirst)) /\ exists ff_q_pvs_prefix_append_equalfirstpositive. dst_positive_code_prefix_append_equalfirst = ff_q_pvs_prefix_append_equalfirstpositive * S ((S (dst_index_prefix_append_equal)) * dst_positive_scale_prefix_append_equalfirst) + (dst_positive_prefix_append_equalfirst))) /\ (((((exists ff_h_pvs_prefix_append_equalfirstnegative. ff_h_pvs_prefix_append_equalfirstnegative + S (dst_negative_prefix_append_equalfirst) = S ((S (dst_index_prefix_append_equal)) * dst_negative_scale_prefix_append_equalfirst)) /\ exists ff_q_pvs_prefix_append_equalfirstnegative. dst_negative_code_prefix_append_equalfirst = ff_q_pvs_prefix_append_equalfirstnegative * S ((S (dst_index_prefix_append_equal)) * dst_negative_scale_prefix_append_equalfirst) + (dst_negative_prefix_append_equalfirst))) /\ (exists ge_balance_positive_prefix_append_equalfirstvalue ge_balance_negative_prefix_append_equalfirstvalue. (((((dst_first_prefix_append_equal) = 2 * (ge_balance_positive_prefix_append_equalfirstvalue) /\ (ge_balance_negative_prefix_append_equalfirstvalue) = 0) \/ exists ge_signed_half_prefix_append_equalfirstvaluedecode. (((dst_first_prefix_append_equal) = 2 * ge_signed_half_prefix_append_equalfirstvaluedecode + 1 /\ (ge_balance_positive_prefix_append_equalfirstvalue) = 0) /\ (ge_balance_negative_prefix_append_equalfirstvalue) = S ge_signed_half_prefix_append_equalfirstvaluedecode))) /\ ((dst_positive_prefix_append_equalfirst) + ge_balance_negative_prefix_append_equalfirstvalue = (dst_negative_prefix_append_equalfirst) + ge_balance_positive_prefix_append_equalfirstvalue))))))))) -> (exists dst_positive_code_prefix_append_equalsecond dst_positive_scale_prefix_append_equalsecond dst_negative_code_prefix_append_equalsecond dst_negative_scale_prefix_append_equalsecond dst_positive_prefix_append_equalsecond dst_negative_prefix_append_equalsecond. (((U) = (((((dst_positive_code_prefix_append_equalsecond) + (dst_positive_scale_prefix_append_equalsecond)) * S ((dst_positive_code_prefix_append_equalsecond) + (dst_positive_scale_prefix_append_equalsecond)) + ((dst_positive_scale_prefix_append_equalsecond) + (dst_positive_scale_prefix_append_equalsecond))) + (((dst_negative_code_prefix_append_equalsecond) + (dst_negative_scale_prefix_append_equalsecond)) * S ((dst_negative_code_prefix_append_equalsecond) + (dst_negative_scale_prefix_append_equalsecond)) + ((dst_negative_scale_prefix_append_equalsecond) + (dst_negative_scale_prefix_append_equalsecond)))) * S ((((dst_positive_code_prefix_append_equalsecond) + (dst_positive_scale_prefix_append_equalsecond)) * S ((dst_positive_code_prefix_append_equalsecond) + (dst_positive_scale_prefix_append_equalsecond)) + ((dst_positive_scale_prefix_append_equalsecond) + (dst_positive_scale_prefix_append_equalsecond))) + (((dst_negative_code_prefix_append_equalsecond) + (dst_negative_scale_prefix_append_equalsecond)) * S ((dst_negative_code_prefix_append_equalsecond) + (dst_negative_scale_prefix_append_equalsecond)) + ((dst_negative_scale_prefix_append_equalsecond) + (dst_negative_scale_prefix_append_equalsecond)))) + ((((dst_negative_code_prefix_append_equalsecond) + (dst_negative_scale_prefix_append_equalsecond)) * S ((dst_negative_code_prefix_append_equalsecond) + (dst_negative_scale_prefix_append_equalsecond)) + ((dst_negative_scale_prefix_append_equalsecond) + (dst_negative_scale_prefix_append_equalsecond))) + (((dst_negative_code_prefix_append_equalsecond) + (dst_negative_scale_prefix_append_equalsecond)) * S ((dst_negative_code_prefix_append_equalsecond) + (dst_negative_scale_prefix_append_equalsecond)) + ((dst_negative_scale_prefix_append_equalsecond) + (dst_negative_scale_prefix_append_equalsecond)))))) /\ (((((exists ff_h_pvs_prefix_append_equalsecondpositive. ff_h_pvs_prefix_append_equalsecondpositive + S (dst_positive_prefix_append_equalsecond) = S ((S (dst_index_prefix_append_equal)) * dst_positive_scale_prefix_append_equalsecond)) /\ exists ff_q_pvs_prefix_append_equalsecondpositive. dst_positive_code_prefix_append_equalsecond = ff_q_pvs_prefix_append_equalsecondpositive * S ((S (dst_index_prefix_append_equal)) * dst_positive_scale_prefix_append_equalsecond) + (dst_positive_prefix_append_equalsecond))) /\ (((((exists ff_h_pvs_prefix_append_equalsecondnegative. ff_h_pvs_prefix_append_equalsecondnegative + S (dst_negative_prefix_append_equalsecond) = S ((S (dst_index_prefix_append_equal)) * dst_negative_scale_prefix_append_equalsecond)) /\ exists ff_q_pvs_prefix_append_equalsecondnegative. dst_negative_code_prefix_append_equalsecond = ff_q_pvs_prefix_append_equalsecondnegative * S ((S (dst_index_prefix_append_equal)) * dst_negative_scale_prefix_append_equalsecond) + (dst_negative_prefix_append_equalsecond))) /\ (exists ge_balance_positive_prefix_append_equalsecondvalue ge_balance_negative_prefix_append_equalsecondvalue. (((((dst_second_prefix_append_equal) = 2 * (ge_balance_positive_prefix_append_equalsecondvalue) /\ (ge_balance_negative_prefix_append_equalsecondvalue) = 0) \/ exists ge_signed_half_prefix_append_equalsecondvaluedecode. (((dst_second_prefix_append_equal) = 2 * ge_signed_half_prefix_append_equalsecondvaluedecode + 1 /\ (ge_balance_positive_prefix_append_equalsecondvalue) = 0) /\ (ge_balance_negative_prefix_append_equalsecondvalue) = S ge_signed_half_prefix_append_equalsecondvaluedecode))) /\ ((dst_positive_prefix_append_equalsecond) + ge_balance_negative_prefix_append_equalsecondvalue = (dst_negative_prefix_append_equalsecond) + ge_balance_positive_prefix_append_equalsecondvalue))))))))) -> dst_first_prefix_append_equal = dst_second_prefix_append_equal))