arithmetic_divisor_transform_convolution

Exact expanded first-order arithmetic statement

forall N F G U. (exists dst_positive_code_transform_source dst_positive_scale_transform_source dst_negative_code_transform_source dst_negative_scale_transform_source. (((F) = (((((dst_positive_code_transform_source) + (dst_positive_scale_transform_source)) * S ((dst_positive_code_transform_source) + (dst_positive_scale_transform_source)) + ((dst_positive_scale_transform_source) + (dst_positive_scale_transform_source))) + (((dst_negative_code_transform_source) + (dst_negative_scale_transform_source)) * S ((dst_negative_code_transform_source) + (dst_negative_scale_transform_source)) + ((dst_negative_scale_transform_source) + (dst_negative_scale_transform_source)))) * S ((((dst_positive_code_transform_source) + (dst_positive_scale_transform_source)) * S ((dst_positive_code_transform_source) + (dst_positive_scale_transform_source)) + ((dst_positive_scale_transform_source) + (dst_positive_scale_transform_source))) + (((dst_negative_code_transform_source) + (dst_negative_scale_transform_source)) * S ((dst_negative_code_transform_source) + (dst_negative_scale_transform_source)) + ((dst_negative_scale_transform_source) + (dst_negative_scale_transform_source)))) + ((((dst_negative_code_transform_source) + (dst_negative_scale_transform_source)) * S ((dst_negative_code_transform_source) + (dst_negative_scale_transform_source)) + ((dst_negative_scale_transform_source) + (dst_negative_scale_transform_source))) + (((dst_negative_code_transform_source) + (dst_negative_scale_transform_source)) * S ((dst_negative_code_transform_source) + (dst_negative_scale_transform_source)) + ((dst_negative_scale_transform_source) + (dst_negative_scale_transform_source)))))) /\ (forall dst_index_transform_source. (exists pvs_le_gap_transform_sourcedomain. pvs_le_gap_transform_sourcedomain + (dst_index_transform_source) = (N)) -> exists dst_positive_transform_source dst_negative_transform_source dst_value_transform_source. ((((exists ff_h_pvs_transform_sourceentrypositive. ff_h_pvs_transform_sourceentrypositive + S (dst_positive_transform_source) = S ((S (dst_index_transform_source)) * dst_positive_scale_transform_source)) /\ exists ff_q_pvs_transform_sourceentrypositive. dst_positive_code_transform_source = ff_q_pvs_transform_sourceentrypositive * S ((S (dst_index_transform_source)) * dst_positive_scale_transform_source) + (dst_positive_transform_source))) /\ (((((exists ff_h_pvs_transform_sourceentrynegative. ff_h_pvs_transform_sourceentrynegative + S (dst_negative_transform_source) = S ((S (dst_index_transform_source)) * dst_negative_scale_transform_source)) /\ exists ff_q_pvs_transform_sourceentrynegative. dst_negative_code_transform_source = ff_q_pvs_transform_sourceentrynegative * S ((S (dst_index_transform_source)) * dst_negative_scale_transform_source) + (dst_negative_transform_source))) /\ (exists ge_balance_positive_transform_sourceentryvalue ge_balance_negative_transform_sourceentryvalue. (((((dst_value_transform_source) = 2 * (ge_balance_positive_transform_sourceentryvalue) /\ (ge_balance_negative_transform_sourceentryvalue) = 0) \/ exists ge_signed_half_transform_sourceentryvaluedecode. (((dst_value_transform_source) = 2 * ge_signed_half_transform_sourceentryvaluedecode + 1 /\ (ge_balance_positive_transform_sourceentryvalue) = 0) /\ (ge_balance_negative_transform_sourceentryvalue) = S ge_signed_half_transform_sourceentryvaluedecode))) /\ ((dst_positive_transform_source) + ge_balance_negative_transform_sourceentryvalue = (dst_negative_transform_source) + ge_balance_positive_transform_sourceentryvalue))))))))) -> (exists dst_positive_code_transform_output dst_positive_scale_transform_output dst_negative_code_transform_output dst_negative_scale_transform_output. (((G) = (((((dst_positive_code_transform_output) + (dst_positive_scale_transform_output)) * S ((dst_positive_code_transform_output) + (dst_positive_scale_transform_output)) + ((dst_positive_scale_transform_output) + (dst_positive_scale_transform_output))) + (((dst_negative_code_transform_output) + (dst_negative_scale_transform_output)) * S ((dst_negative_code_transform_output) + (dst_negative_scale_transform_output)) + ((dst_negative_scale_transform_output) + (dst_negative_scale_transform_output)))) * S ((((dst_positive_code_transform_output) + (dst_positive_scale_transform_output)) * S ((dst_positive_code_transform_output) + (dst_positive_scale_transform_output)) + ((dst_positive_scale_transform_output) + (dst_positive_scale_transform_output))) + (((dst_negative_code_transform_output) + (dst_negative_scale_transform_output)) * S ((dst_negative_code_transform_output) + (dst_negative_scale_transform_output)) + ((dst_negative_scale_transform_output) + (dst_negative_scale_transform_output)))) + ((((dst_negative_code_transform_output) + (dst_negative_scale_transform_output)) * S ((dst_negative_code_transform_output) + (dst_negative_scale_transform_output)) + ((dst_negative_scale_transform_output) + (dst_negative_scale_transform_output))) + (((dst_negative_code_transform_output) + (dst_negative_scale_transform_output)) * S ((dst_negative_code_transform_output) + (dst_negative_scale_transform_output)) + ((dst_negative_scale_transform_output) + (dst_negative_scale_transform_output)))))) /\ (forall dst_index_transform_output. (exists pvs_le_gap_transform_outputdomain. pvs_le_gap_transform_outputdomain + (dst_index_transform_output) = (N)) -> exists dst_positive_transform_output dst_negative_transform_output dst_value_transform_output. ((((exists ff_h_pvs_transform_outputentrypositive. ff_h_pvs_transform_outputentrypositive + S (dst_positive_transform_output) = S ((S (dst_index_transform_output)) * dst_positive_scale_transform_output)) /\ exists ff_q_pvs_transform_outputentrypositive. dst_positive_code_transform_output = ff_q_pvs_transform_outputentrypositive * S ((S (dst_index_transform_output)) * dst_positive_scale_transform_output) + (dst_positive_transform_output))) /\ (((((exists ff_h_pvs_transform_outputentrynegative. ff_h_pvs_transform_outputentrynegative + S (dst_negative_transform_output) = S ((S (dst_index_transform_output)) * dst_negative_scale_transform_output)) /\ exists ff_q_pvs_transform_outputentrynegative. dst_negative_code_transform_output = ff_q_pvs_transform_outputentrynegative * S ((S (dst_index_transform_output)) * dst_negative_scale_transform_output) + (dst_negative_transform_output))) /\ (exists ge_balance_positive_transform_outputentryvalue ge_balance_negative_transform_outputentryvalue. (((((dst_value_transform_output) = 2 * (ge_balance_positive_transform_outputentryvalue) /\ (ge_balance_negative_transform_outputentryvalue) = 0) \/ exists ge_signed_half_transform_outputentryvaluedecode. (((dst_value_transform_output) = 2 * ge_signed_half_transform_outputentryvaluedecode + 1 /\ (ge_balance_positive_transform_outputentryvalue) = 0) /\ (ge_balance_negative_transform_outputentryvalue) = S ge_signed_half_transform_outputentryvaluedecode))) /\ ((dst_positive_transform_output) + ge_balance_negative_transform_outputentryvalue = (dst_negative_transform_output) + ge_balance_positive_transform_outputentryvalue))))))))) -> (((exists dst_positive_code_transform_onetable dst_positive_scale_transform_onetable dst_negative_code_transform_onetable dst_negative_scale_transform_onetable. (((U) = (((((dst_positive_code_transform_onetable) + (dst_positive_scale_transform_onetable)) * S ((dst_positive_code_transform_onetable) + (dst_positive_scale_transform_onetable)) + ((dst_positive_scale_transform_onetable) + (dst_positive_scale_transform_onetable))) + (((dst_negative_code_transform_onetable) + (dst_negative_scale_transform_onetable)) * S ((dst_negative_code_transform_onetable) + (dst_negative_scale_transform_onetable)) + ((dst_negative_scale_transform_onetable) + (dst_negative_scale_transform_onetable)))) * S ((((dst_positive_code_transform_onetable) + (dst_positive_scale_transform_onetable)) * S ((dst_positive_code_transform_onetable) + (dst_positive_scale_transform_onetable)) + ((dst_positive_scale_transform_onetable) + (dst_positive_scale_transform_onetable))) + (((dst_negative_code_transform_onetable) + (dst_negative_scale_transform_onetable)) * S ((dst_negative_code_transform_onetable) + (dst_negative_scale_transform_onetable)) + ((dst_negative_scale_transform_onetable) + (dst_negative_scale_transform_onetable)))) + ((((dst_negative_code_transform_onetable) + (dst_negative_scale_transform_onetable)) * S ((dst_negative_code_transform_onetable) + (dst_negative_scale_transform_onetable)) + ((dst_negative_scale_transform_onetable) + (dst_negative_scale_transform_onetable))) + (((dst_negative_code_transform_onetable) + (dst_negative_scale_transform_onetable)) * S ((dst_negative_code_transform_onetable) + (dst_negative_scale_transform_onetable)) + ((dst_negative_scale_transform_onetable) + (dst_negative_scale_transform_onetable)))))) /\ (forall dst_index_transform_onetable. (exists pvs_le_gap_transform_onetabledomain. pvs_le_gap_transform_onetabledomain + (dst_index_transform_onetable) = (N)) -> exists dst_positive_transform_onetable dst_negative_transform_onetable dst_value_transform_onetable. ((((exists ff_h_pvs_transform_onetableentrypositive. ff_h_pvs_transform_onetableentrypositive + S (dst_positive_transform_onetable) = S ((S (dst_index_transform_onetable)) * dst_positive_scale_transform_onetable)) /\ exists ff_q_pvs_transform_onetableentrypositive. dst_positive_code_transform_onetable = ff_q_pvs_transform_onetableentrypositive * S ((S (dst_index_transform_onetable)) * dst_positive_scale_transform_onetable) + (dst_positive_transform_onetable))) /\ (((((exists ff_h_pvs_transform_onetableentrynegative. ff_h_pvs_transform_onetableentrynegative + S (dst_negative_transform_onetable) = S ((S (dst_index_transform_onetable)) * dst_negative_scale_transform_onetable)) /\ exists ff_q_pvs_transform_onetableentrynegative. dst_negative_code_transform_onetable = ff_q_pvs_transform_onetableentrynegative * S ((S (dst_index_transform_onetable)) * dst_negative_scale_transform_onetable) + (dst_negative_transform_onetable))) /\ (exists ge_balance_positive_transform_onetableentryvalue ge_balance_negative_transform_onetableentryvalue. (((((dst_value_transform_onetable) = 2 * (ge_balance_positive_transform_onetableentryvalue) /\ (ge_balance_negative_transform_onetableentryvalue) = 0) \/ exists ge_signed_half_transform_onetableentryvaluedecode. (((dst_value_transform_onetable) = 2 * ge_signed_half_transform_onetableentryvaluedecode + 1 /\ (ge_balance_positive_transform_onetableentryvalue) = 0) /\ (ge_balance_negative_transform_onetableentryvalue) = S ge_signed_half_transform_onetableentryvaluedecode))) /\ ((dst_positive_transform_onetable) + ge_balance_negative_transform_onetableentryvalue = (dst_negative_transform_onetable) + ge_balance_positive_transform_onetableentryvalue))))))))) /\ (forall du_index_transform_one du_value_transform_one. ~(du_index_transform_one=0) -> (exists pvs_le_gap_transform_onebound. pvs_le_gap_transform_onebound + (du_index_transform_one) = (N)) -> (exists dst_positive_code_transform_oneentry dst_positive_scale_transform_oneentry dst_negative_code_transform_oneentry dst_negative_scale_transform_oneentry dst_positive_transform_oneentry dst_negative_transform_oneentry. (((U) = (((((dst_positive_code_transform_oneentry) + (dst_positive_scale_transform_oneentry)) * S ((dst_positive_code_transform_oneentry) + (dst_positive_scale_transform_oneentry)) + ((dst_positive_scale_transform_oneentry) + (dst_positive_scale_transform_oneentry))) + (((dst_negative_code_transform_oneentry) + (dst_negative_scale_transform_oneentry)) * S ((dst_negative_code_transform_oneentry) + (dst_negative_scale_transform_oneentry)) + ((dst_negative_scale_transform_oneentry) + (dst_negative_scale_transform_oneentry)))) * S ((((dst_positive_code_transform_oneentry) + (dst_positive_scale_transform_oneentry)) * S ((dst_positive_code_transform_oneentry) + (dst_positive_scale_transform_oneentry)) + ((dst_positive_scale_transform_oneentry) + (dst_positive_scale_transform_oneentry))) + (((dst_negative_code_transform_oneentry) + (dst_negative_scale_transform_oneentry)) * S ((dst_negative_code_transform_oneentry) + (dst_negative_scale_transform_oneentry)) + ((dst_negative_scale_transform_oneentry) + (dst_negative_scale_transform_oneentry)))) + ((((dst_negative_code_transform_oneentry) + (dst_negative_scale_transform_oneentry)) * S ((dst_negative_code_transform_oneentry) + (dst_negative_scale_transform_oneentry)) + ((dst_negative_scale_transform_oneentry) + (dst_negative_scale_transform_oneentry))) + (((dst_negative_code_transform_oneentry) + (dst_negative_scale_transform_oneentry)) * S ((dst_negative_code_transform_oneentry) + (dst_negative_scale_transform_oneentry)) + ((dst_negative_scale_transform_oneentry) + (dst_negative_scale_transform_oneentry)))))) /\ (((((exists ff_h_pvs_transform_oneentrypositive. ff_h_pvs_transform_oneentrypositive + S (dst_positive_transform_oneentry) = S ((S (du_index_transform_one)) * dst_positive_scale_transform_oneentry)) /\ exists ff_q_pvs_transform_oneentrypositive. dst_positive_code_transform_oneentry = ff_q_pvs_transform_oneentrypositive * S ((S (du_index_transform_one)) * dst_positive_scale_transform_oneentry) + (dst_positive_transform_oneentry))) /\ (((((exists ff_h_pvs_transform_oneentrynegative. ff_h_pvs_transform_oneentrynegative + S (dst_negative_transform_oneentry) = S ((S (du_index_transform_one)) * dst_negative_scale_transform_oneentry)) /\ exists ff_q_pvs_transform_oneentrynegative. dst_negative_code_transform_oneentry = ff_q_pvs_transform_oneentrynegative * S ((S (du_index_transform_one)) * dst_negative_scale_transform_oneentry) + (dst_negative_transform_oneentry))) /\ (exists ge_balance_positive_transform_oneentryvalue ge_balance_negative_transform_oneentryvalue. (((((du_value_transform_one) = 2 * (ge_balance_positive_transform_oneentryvalue) /\ (ge_balance_negative_transform_oneentryvalue) = 0) \/ exists ge_signed_half_transform_oneentryvaluedecode. (((du_value_transform_one) = 2 * ge_signed_half_transform_oneentryvaluedecode + 1 /\ (ge_balance_positive_transform_oneentryvalue) = 0) /\ (ge_balance_negative_transform_oneentryvalue) = S ge_signed_half_transform_oneentryvaluedecode))) /\ ((dst_positive_transform_oneentry) + ge_balance_negative_transform_oneentryvalue = (dst_negative_transform_oneentry) + ge_balance_positive_transform_oneentryvalue))))))))) -> du_value_transform_one=2))) -> (forall mi_index_transform_values mi_value_transform_values. ~(mi_index_transform_values=0) -> (exists pvs_le_gap_transform_valuesbound. pvs_le_gap_transform_valuesbound + (mi_index_transform_values) = (N)) -> (exists dst_positive_code_transform_valuesentry dst_positive_scale_transform_valuesentry dst_negative_code_transform_valuesentry dst_negative_scale_transform_valuesentry dst_positive_transform_valuesentry dst_negative_transform_valuesentry. (((G) = (((((dst_positive_code_transform_valuesentry) + (dst_positive_scale_transform_valuesentry)) * S ((dst_positive_code_transform_valuesentry) + (dst_positive_scale_transform_valuesentry)) + ((dst_positive_scale_transform_valuesentry) + (dst_positive_scale_transform_valuesentry))) + (((dst_negative_code_transform_valuesentry) + (dst_negative_scale_transform_valuesentry)) * S ((dst_negative_code_transform_valuesentry) + (dst_negative_scale_transform_valuesentry)) + ((dst_negative_scale_transform_valuesentry) + (dst_negative_scale_transform_valuesentry)))) * S ((((dst_positive_code_transform_valuesentry) + (dst_positive_scale_transform_valuesentry)) * S ((dst_positive_code_transform_valuesentry) + (dst_positive_scale_transform_valuesentry)) + ((dst_positive_scale_transform_valuesentry) + (dst_positive_scale_transform_valuesentry))) + (((dst_negative_code_transform_valuesentry) + (dst_negative_scale_transform_valuesentry)) * S ((dst_negative_code_transform_valuesentry) + (dst_negative_scale_transform_valuesentry)) + ((dst_negative_scale_transform_valuesentry) + (dst_negative_scale_transform_valuesentry)))) + ((((dst_negative_code_transform_valuesentry) + (dst_negative_scale_transform_valuesentry)) * S ((dst_negative_code_transform_valuesentry) + (dst_negative_scale_transform_valuesentry)) + ((dst_negative_scale_transform_valuesentry) + (dst_negative_scale_transform_valuesentry))) + (((dst_negative_code_transform_valuesentry) + (dst_negative_scale_transform_valuesentry)) * S ((dst_negative_code_transform_valuesentry) + (dst_negative_scale_transform_valuesentry)) + ((dst_negative_scale_transform_valuesentry) + (dst_negative_scale_transform_valuesentry)))))) /\ (((((exists ff_h_pvs_transform_valuesentrypositive. ff_h_pvs_transform_valuesentrypositive + S (dst_positive_transform_valuesentry) = S ((S (mi_index_transform_values)) * dst_positive_scale_transform_valuesentry)) /\ exists ff_q_pvs_transform_valuesentrypositive. dst_positive_code_transform_valuesentry = ff_q_pvs_transform_valuesentrypositive * S ((S (mi_index_transform_values)) * dst_positive_scale_transform_valuesentry) + (dst_positive_transform_valuesentry))) /\ (((((exists ff_h_pvs_transform_valuesentrynegative. ff_h_pvs_transform_valuesentrynegative + S (dst_negative_transform_valuesentry) = S ((S (mi_index_transform_values)) * dst_negative_scale_transform_valuesentry)) /\ exists ff_q_pvs_transform_valuesentrynegative. dst_negative_code_transform_valuesentry = ff_q_pvs_transform_valuesentrynegative * S ((S (mi_index_transform_values)) * dst_negative_scale_transform_valuesentry) + (dst_negative_transform_valuesentry))) /\ (exists ge_balance_positive_transform_valuesentryvalue ge_balance_negative_transform_valuesentryvalue. (((((mi_value_transform_values) = 2 * (ge_balance_positive_transform_valuesentryvalue) /\ (ge_balance_negative_transform_valuesentryvalue) = 0) \/ exists ge_signed_half_transform_valuesentryvaluedecode. (((mi_value_transform_values) = 2 * ge_signed_half_transform_valuesentryvaluedecode + 1 /\ (ge_balance_positive_transform_valuesentryvalue) = 0) /\ (ge_balance_negative_transform_valuesentryvalue) = S ge_signed_half_transform_valuesentryvaluedecode))) /\ ((dst_positive_transform_valuesentry) + ge_balance_negative_transform_valuesentryvalue = (dst_negative_transform_valuesentry) + ge_balance_positive_transform_valuesentryvalue))))))))) -> (((~((mi_index_transform_values)=0)) /\ (exists dm_mask_table_transform_valuessum. ((((exists dst_positive_code_transform_valuessummasktable dst_positive_scale_transform_valuessummasktable dst_negative_code_transform_valuessummasktable dst_negative_scale_transform_valuessummasktable. (((dm_mask_table_transform_valuessum) = (((((dst_positive_code_transform_valuessummasktable) + (dst_positive_scale_transform_valuessummasktable)) * S ((dst_positive_code_transform_valuessummasktable) + (dst_positive_scale_transform_valuessummasktable)) + ((dst_positive_scale_transform_valuessummasktable) + (dst_positive_scale_transform_valuessummasktable))) + (((dst_negative_code_transform_valuessummasktable) + (dst_negative_scale_transform_valuessummasktable)) * S ((dst_negative_code_transform_valuessummasktable) + (dst_negative_scale_transform_valuessummasktable)) + ((dst_negative_scale_transform_valuessummasktable) + (dst_negative_scale_transform_valuessummasktable)))) * S ((((dst_positive_code_transform_valuessummasktable) + (dst_positive_scale_transform_valuessummasktable)) * S ((dst_positive_code_transform_valuessummasktable) + (dst_positive_scale_transform_valuessummasktable)) + ((dst_positive_scale_transform_valuessummasktable) + (dst_positive_scale_transform_valuessummasktable))) + (((dst_negative_code_transform_valuessummasktable) + (dst_negative_scale_transform_valuessummasktable)) * S ((dst_negative_code_transform_valuessummasktable) + (dst_negative_scale_transform_valuessummasktable)) + ((dst_negative_scale_transform_valuessummasktable) + (dst_negative_scale_transform_valuessummasktable)))) + ((((dst_negative_code_transform_valuessummasktable) + (dst_negative_scale_transform_valuessummasktable)) * S ((dst_negative_code_transform_valuessummasktable) + (dst_negative_scale_transform_valuessummasktable)) + ((dst_negative_scale_transform_valuessummasktable) + (dst_negative_scale_transform_valuessummasktable))) + (((dst_negative_code_transform_valuessummasktable) + (dst_negative_scale_transform_valuessummasktable)) * S ((dst_negative_code_transform_valuessummasktable) + (dst_negative_scale_transform_valuessummasktable)) + ((dst_negative_scale_transform_valuessummasktable) + (dst_negative_scale_transform_valuessummasktable)))))) /\ (forall dst_index_transform_valuessummasktable. (exists pvs_le_gap_transform_valuessummasktabledomain. pvs_le_gap_transform_valuessummasktabledomain + (dst_index_transform_valuessummasktable) = (mi_index_transform_values)) -> exists dst_positive_transform_valuessummasktable dst_negative_transform_valuessummasktable dst_value_transform_valuessummasktable. ((((exists ff_h_pvs_transform_valuessummasktableentrypositive. ff_h_pvs_transform_valuessummasktableentrypositive + S (dst_positive_transform_valuessummasktable) = S ((S (dst_index_transform_valuessummasktable)) * dst_positive_scale_transform_valuessummasktable)) /\ exists ff_q_pvs_transform_valuessummasktableentrypositive. dst_positive_code_transform_valuessummasktable = ff_q_pvs_transform_valuessummasktableentrypositive * S ((S (dst_index_transform_valuessummasktable)) * dst_positive_scale_transform_valuessummasktable) + (dst_positive_transform_valuessummasktable))) /\ (((((exists ff_h_pvs_transform_valuessummasktableentrynegative. ff_h_pvs_transform_valuessummasktableentrynegative + S (dst_negative_transform_valuessummasktable) = S ((S (dst_index_transform_valuessummasktable)) * dst_negative_scale_transform_valuessummasktable)) /\ exists ff_q_pvs_transform_valuessummasktableentrynegative. dst_negative_code_transform_valuessummasktable = ff_q_pvs_transform_valuessummasktableentrynegative * S ((S (dst_index_transform_valuessummasktable)) * dst_negative_scale_transform_valuessummasktable) + (dst_negative_transform_valuessummasktable))) /\ (exists ge_balance_positive_transform_valuessummasktableentryvalue ge_balance_negative_transform_valuessummasktableentryvalue. (((((dst_value_transform_valuessummasktable) = 2 * (ge_balance_positive_transform_valuessummasktableentryvalue) /\ (ge_balance_negative_transform_valuessummasktableentryvalue) = 0) \/ exists ge_signed_half_transform_valuessummasktableentryvaluedecode. (((dst_value_transform_valuessummasktable) = 2 * ge_signed_half_transform_valuessummasktableentryvaluedecode + 1 /\ (ge_balance_positive_transform_valuessummasktableentryvalue) = 0) /\ (ge_balance_negative_transform_valuessummasktableentryvalue) = S ge_signed_half_transform_valuessummasktableentryvaluedecode))) /\ ((dst_positive_transform_valuessummasktable) + ge_balance_negative_transform_valuessummasktableentryvalue = (dst_negative_transform_valuessummasktable) + ge_balance_positive_transform_valuessummasktableentryvalue))))))))) /\ (forall dm_index_transform_valuessummask dm_value_transform_valuessummask. (exists pvs_le_gap_transform_valuessummaskdomain. pvs_le_gap_transform_valuessummaskdomain + (dm_index_transform_valuessummask) = (mi_index_transform_values)) -> (exists dst_positive_code_transform_valuessummasklookup dst_positive_scale_transform_valuessummasklookup dst_negative_code_transform_valuessummasklookup dst_negative_scale_transform_valuessummasklookup dst_positive_transform_valuessummasklookup dst_negative_transform_valuessummasklookup. (((dm_mask_table_transform_valuessum) = (((((dst_positive_code_transform_valuessummasklookup) + (dst_positive_scale_transform_valuessummasklookup)) * S ((dst_positive_code_transform_valuessummasklookup) + (dst_positive_scale_transform_valuessummasklookup)) + ((dst_positive_scale_transform_valuessummasklookup) + (dst_positive_scale_transform_valuessummasklookup))) + (((dst_negative_code_transform_valuessummasklookup) + (dst_negative_scale_transform_valuessummasklookup)) * S ((dst_negative_code_transform_valuessummasklookup) + (dst_negative_scale_transform_valuessummasklookup)) + ((dst_negative_scale_transform_valuessummasklookup) + (dst_negative_scale_transform_valuessummasklookup)))) * S ((((dst_positive_code_transform_valuessummasklookup) + (dst_positive_scale_transform_valuessummasklookup)) * S ((dst_positive_code_transform_valuessummasklookup) + (dst_positive_scale_transform_valuessummasklookup)) + ((dst_positive_scale_transform_valuessummasklookup) + (dst_positive_scale_transform_valuessummasklookup))) + (((dst_negative_code_transform_valuessummasklookup) + (dst_negative_scale_transform_valuessummasklookup)) * S ((dst_negative_code_transform_valuessummasklookup) + (dst_negative_scale_transform_valuessummasklookup)) + ((dst_negative_scale_transform_valuessummasklookup) + (dst_negative_scale_transform_valuessummasklookup)))) + ((((dst_negative_code_transform_valuessummasklookup) + (dst_negative_scale_transform_valuessummasklookup)) * S ((dst_negative_code_transform_valuessummasklookup) + (dst_negative_scale_transform_valuessummasklookup)) + ((dst_negative_scale_transform_valuessummasklookup) + (dst_negative_scale_transform_valuessummasklookup))) + (((dst_negative_code_transform_valuessummasklookup) + (dst_negative_scale_transform_valuessummasklookup)) * S ((dst_negative_code_transform_valuessummasklookup) + (dst_negative_scale_transform_valuessummasklookup)) + ((dst_negative_scale_transform_valuessummasklookup) + (dst_negative_scale_transform_valuessummasklookup)))))) /\ (((((exists ff_h_pvs_transform_valuessummasklookuppositive. ff_h_pvs_transform_valuessummasklookuppositive + S (dst_positive_transform_valuessummasklookup) = S ((S (dm_index_transform_valuessummask)) * dst_positive_scale_transform_valuessummasklookup)) /\ exists ff_q_pvs_transform_valuessummasklookuppositive. dst_positive_code_transform_valuessummasklookup = ff_q_pvs_transform_valuessummasklookuppositive * S ((S (dm_index_transform_valuessummask)) * dst_positive_scale_transform_valuessummasklookup) + (dst_positive_transform_valuessummasklookup))) /\ (((((exists ff_h_pvs_transform_valuessummasklookupnegative. ff_h_pvs_transform_valuessummasklookupnegative + S (dst_negative_transform_valuessummasklookup) = S ((S (dm_index_transform_valuessummask)) * dst_negative_scale_transform_valuessummasklookup)) /\ exists ff_q_pvs_transform_valuessummasklookupnegative. dst_negative_code_transform_valuessummasklookup = ff_q_pvs_transform_valuessummasklookupnegative * S ((S (dm_index_transform_valuessummask)) * dst_negative_scale_transform_valuessummasklookup) + (dst_negative_transform_valuessummasklookup))) /\ (exists ge_balance_positive_transform_valuessummasklookupvalue ge_balance_negative_transform_valuessummasklookupvalue. (((((dm_value_transform_valuessummask) = 2 * (ge_balance_positive_transform_valuessummasklookupvalue) /\ (ge_balance_negative_transform_valuessummasklookupvalue) = 0) \/ exists ge_signed_half_transform_valuessummasklookupvaluedecode. (((dm_value_transform_valuessummask) = 2 * ge_signed_half_transform_valuessummasklookupvaluedecode + 1 /\ (ge_balance_positive_transform_valuessummasklookupvalue) = 0) /\ (ge_balance_negative_transform_valuessummasklookupvalue) = S ge_signed_half_transform_valuessummasklookupvaluedecode))) /\ ((dst_positive_transform_valuessummasklookup) + ge_balance_negative_transform_valuessummasklookupvalue = (dst_negative_transform_valuessummasklookup) + ge_balance_positive_transform_valuessummasklookupvalue))))))))) -> ((((~((dm_index_transform_valuessummask)=0)) /\ (exists dm_quotient_transform_valuessummaskentry. (((mi_index_transform_values)=(dm_index_transform_valuessummask)*dm_quotient_transform_valuessummaskentry) /\ (exists dst_positive_code_transform_valuessummaskentryinput dst_positive_scale_transform_valuessummaskentryinput dst_negative_code_transform_valuessummaskentryinput dst_negative_scale_transform_valuessummaskentryinput dst_positive_transform_valuessummaskentryinput dst_negative_transform_valuessummaskentryinput. (((F) = (((((dst_positive_code_transform_valuessummaskentryinput) + (dst_positive_scale_transform_valuessummaskentryinput)) * S ((dst_positive_code_transform_valuessummaskentryinput) + (dst_positive_scale_transform_valuessummaskentryinput)) + ((dst_positive_scale_transform_valuessummaskentryinput) + (dst_positive_scale_transform_valuessummaskentryinput))) + (((dst_negative_code_transform_valuessummaskentryinput) + (dst_negative_scale_transform_valuessummaskentryinput)) * S ((dst_negative_code_transform_valuessummaskentryinput) + (dst_negative_scale_transform_valuessummaskentryinput)) + ((dst_negative_scale_transform_valuessummaskentryinput) + (dst_negative_scale_transform_valuessummaskentryinput)))) * S ((((dst_positive_code_transform_valuessummaskentryinput) + (dst_positive_scale_transform_valuessummaskentryinput)) * S ((dst_positive_code_transform_valuessummaskentryinput) + (dst_positive_scale_transform_valuessummaskentryinput)) + ((dst_positive_scale_transform_valuessummaskentryinput) + (dst_positive_scale_transform_valuessummaskentryinput))) + (((dst_negative_code_transform_valuessummaskentryinput) + (dst_negative_scale_transform_valuessummaskentryinput)) * S ((dst_negative_code_transform_valuessummaskentryinput) + (dst_negative_scale_transform_valuessummaskentryinput)) + ((dst_negative_scale_transform_valuessummaskentryinput) + (dst_negative_scale_transform_valuessummaskentryinput)))) + ((((dst_negative_code_transform_valuessummaskentryinput) + (dst_negative_scale_transform_valuessummaskentryinput)) * S ((dst_negative_code_transform_valuessummaskentryinput) + (dst_negative_scale_transform_valuessummaskentryinput)) + ((dst_negative_scale_transform_valuessummaskentryinput) + (dst_negative_scale_transform_valuessummaskentryinput))) + (((dst_negative_code_transform_valuessummaskentryinput) + (dst_negative_scale_transform_valuessummaskentryinput)) * S ((dst_negative_code_transform_valuessummaskentryinput) + (dst_negative_scale_transform_valuessummaskentryinput)) + ((dst_negative_scale_transform_valuessummaskentryinput) + (dst_negative_scale_transform_valuessummaskentryinput)))))) /\ (((((exists ff_h_pvs_transform_valuessummaskentryinputpositive. ff_h_pvs_transform_valuessummaskentryinputpositive + S (dst_positive_transform_valuessummaskentryinput) = S ((S (dm_index_transform_valuessummask)) * dst_positive_scale_transform_valuessummaskentryinput)) /\ exists ff_q_pvs_transform_valuessummaskentryinputpositive. dst_positive_code_transform_valuessummaskentryinput = ff_q_pvs_transform_valuessummaskentryinputpositive * S ((S (dm_index_transform_valuessummask)) * dst_positive_scale_transform_valuessummaskentryinput) + (dst_positive_transform_valuessummaskentryinput))) /\ (((((exists ff_h_pvs_transform_valuessummaskentryinputnegative. ff_h_pvs_transform_valuessummaskentryinputnegative + S (dst_negative_transform_valuessummaskentryinput) = S ((S (dm_index_transform_valuessummask)) * dst_negative_scale_transform_valuessummaskentryinput)) /\ exists ff_q_pvs_transform_valuessummaskentryinputnegative. dst_negative_code_transform_valuessummaskentryinput = ff_q_pvs_transform_valuessummaskentryinputnegative * S ((S (dm_index_transform_valuessummask)) * dst_negative_scale_transform_valuessummaskentryinput) + (dst_negative_transform_valuessummaskentryinput))) /\ (exists ge_balance_positive_transform_valuessummaskentryinputvalue ge_balance_negative_transform_valuessummaskentryinputvalue. (((((dm_value_transform_valuessummask) = 2 * (ge_balance_positive_transform_valuessummaskentryinputvalue) /\ (ge_balance_negative_transform_valuessummaskentryinputvalue) = 0) \/ exists ge_signed_half_transform_valuessummaskentryinputvaluedecode. (((dm_value_transform_valuessummask) = 2 * ge_signed_half_transform_valuessummaskentryinputvaluedecode + 1 /\ (ge_balance_positive_transform_valuessummaskentryinputvalue) = 0) /\ (ge_balance_negative_transform_valuessummaskentryinputvalue) = S ge_signed_half_transform_valuessummaskentryinputvaluedecode))) /\ ((dst_positive_transform_valuessummaskentryinput) + ge_balance_negative_transform_valuessummaskentryinputvalue = (dst_negative_transform_valuessummaskentryinput) + ge_balance_positive_transform_valuessummaskentryinputvalue))))))))))))) \/ ((((dm_index_transform_valuessummask)=0 \/ ~(exists pvs_factor_transform_valuessummaskentrynondivisor. (mi_index_transform_values) = (dm_index_transform_valuessummask) * pvs_factor_transform_valuessummaskentrynondivisor)) /\ ((dm_value_transform_valuessummask)=0))))))) /\ (exists dst_positive_code_transform_valuessumfold dst_positive_scale_transform_valuessumfold dst_negative_code_transform_valuessumfold dst_negative_scale_transform_valuessumfold dst_positive_sum_transform_valuessumfold dst_negative_sum_transform_valuessumfold. (((dm_mask_table_transform_valuessum) = (((((dst_positive_code_transform_valuessumfold) + (dst_positive_scale_transform_valuessumfold)) * S ((dst_positive_code_transform_valuessumfold) + (dst_positive_scale_transform_valuessumfold)) + ((dst_positive_scale_transform_valuessumfold) + (dst_positive_scale_transform_valuessumfold))) + (((dst_negative_code_transform_valuessumfold) + (dst_negative_scale_transform_valuessumfold)) * S ((dst_negative_code_transform_valuessumfold) + (dst_negative_scale_transform_valuessumfold)) + ((dst_negative_scale_transform_valuessumfold) + (dst_negative_scale_transform_valuessumfold)))) * S ((((dst_positive_code_transform_valuessumfold) + (dst_positive_scale_transform_valuessumfold)) * S ((dst_positive_code_transform_valuessumfold) + (dst_positive_scale_transform_valuessumfold)) + ((dst_positive_scale_transform_valuessumfold) + (dst_positive_scale_transform_valuessumfold))) + (((dst_negative_code_transform_valuessumfold) + (dst_negative_scale_transform_valuessumfold)) * S ((dst_negative_code_transform_valuessumfold) + (dst_negative_scale_transform_valuessumfold)) + ((dst_negative_scale_transform_valuessumfold) + (dst_negative_scale_transform_valuessumfold)))) + ((((dst_negative_code_transform_valuessumfold) + (dst_negative_scale_transform_valuessumfold)) * S ((dst_negative_code_transform_valuessumfold) + (dst_negative_scale_transform_valuessumfold)) + ((dst_negative_scale_transform_valuessumfold) + (dst_negative_scale_transform_valuessumfold))) + (((dst_negative_code_transform_valuessumfold) + (dst_negative_scale_transform_valuessumfold)) * S ((dst_negative_code_transform_valuessumfold) + (dst_negative_scale_transform_valuessumfold)) + ((dst_negative_scale_transform_valuessumfold) + (dst_negative_scale_transform_valuessumfold)))))) /\ (((exists fs_u_dst_transform_valuessumfoldpositive fs_v_dst_transform_valuessumfoldpositive. ((((exists fs_h_dst_transform_valuessumfoldpositive_body_start. fs_h_dst_transform_valuessumfoldpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_transform_valuessumfoldpositive)) /\ exists fs_q_dst_transform_valuessumfoldpositive_body_start. fs_u_dst_transform_valuessumfoldpositive = fs_q_dst_transform_valuessumfoldpositive_body_start * S ((S (0)) * fs_v_dst_transform_valuessumfoldpositive) + (0))) /\ ((((exists fs_h_dst_transform_valuessumfoldpositive_body_terminal. fs_h_dst_transform_valuessumfoldpositive_body_terminal + S (dst_positive_sum_transform_valuessumfold) = S ((S (S (mi_index_transform_values))) * fs_v_dst_transform_valuessumfoldpositive)) /\ exists fs_q_dst_transform_valuessumfoldpositive_body_terminal. fs_u_dst_transform_valuessumfoldpositive = fs_q_dst_transform_valuessumfoldpositive_body_terminal * S ((S (S (mi_index_transform_values))) * fs_v_dst_transform_valuessumfoldpositive) + (dst_positive_sum_transform_valuessumfold))) /\ forall fs_i_dst_transform_valuessumfoldpositive_body_steps. (exists fs_lt_dst_transform_valuessumfoldpositive_body_steps_bound. fs_lt_dst_transform_valuessumfoldpositive_body_steps_bound + S fs_i_dst_transform_valuessumfoldpositive_body_steps = S (mi_index_transform_values)) -> exists fs_a_dst_transform_valuessumfoldpositive_body_steps fs_r_dst_transform_valuessumfoldpositive_body_steps fs_s_dst_transform_valuessumfoldpositive_body_steps. ((((exists fs_h_dst_transform_valuessumfoldpositive_body_steps_summand. fs_h_dst_transform_valuessumfoldpositive_body_steps_summand + S (fs_a_dst_transform_valuessumfoldpositive_body_steps) = S ((S (fs_i_dst_transform_valuessumfoldpositive_body_steps)) * dst_positive_scale_transform_valuessumfold)) /\ exists fs_q_dst_transform_valuessumfoldpositive_body_steps_summand. dst_positive_code_transform_valuessumfold = fs_q_dst_transform_valuessumfoldpositive_body_steps_summand * S ((S (fs_i_dst_transform_valuessumfoldpositive_body_steps)) * dst_positive_scale_transform_valuessumfold) + (fs_a_dst_transform_valuessumfoldpositive_body_steps))) /\ ((((exists fs_h_dst_transform_valuessumfoldpositive_body_steps_partial. fs_h_dst_transform_valuessumfoldpositive_body_steps_partial + S (fs_r_dst_transform_valuessumfoldpositive_body_steps) = S ((S (fs_i_dst_transform_valuessumfoldpositive_body_steps)) * fs_v_dst_transform_valuessumfoldpositive)) /\ exists fs_q_dst_transform_valuessumfoldpositive_body_steps_partial. fs_u_dst_transform_valuessumfoldpositive = fs_q_dst_transform_valuessumfoldpositive_body_steps_partial * S ((S (fs_i_dst_transform_valuessumfoldpositive_body_steps)) * fs_v_dst_transform_valuessumfoldpositive) + (fs_r_dst_transform_valuessumfoldpositive_body_steps))) /\ ((((exists fs_h_dst_transform_valuessumfoldpositive_body_steps_successor. fs_h_dst_transform_valuessumfoldpositive_body_steps_successor + S (fs_s_dst_transform_valuessumfoldpositive_body_steps) = S ((S (S fs_i_dst_transform_valuessumfoldpositive_body_steps)) * fs_v_dst_transform_valuessumfoldpositive)) /\ exists fs_q_dst_transform_valuessumfoldpositive_body_steps_successor. fs_u_dst_transform_valuessumfoldpositive = fs_q_dst_transform_valuessumfoldpositive_body_steps_successor * S ((S (S fs_i_dst_transform_valuessumfoldpositive_body_steps)) * fs_v_dst_transform_valuessumfoldpositive) + (fs_s_dst_transform_valuessumfoldpositive_body_steps))) /\ fs_s_dst_transform_valuessumfoldpositive_body_steps = fs_r_dst_transform_valuessumfoldpositive_body_steps + fs_a_dst_transform_valuessumfoldpositive_body_steps)))))) /\ (((exists fs_u_dst_transform_valuessumfoldnegative fs_v_dst_transform_valuessumfoldnegative. ((((exists fs_h_dst_transform_valuessumfoldnegative_body_start. fs_h_dst_transform_valuessumfoldnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_transform_valuessumfoldnegative)) /\ exists fs_q_dst_transform_valuessumfoldnegative_body_start. fs_u_dst_transform_valuessumfoldnegative = fs_q_dst_transform_valuessumfoldnegative_body_start * S ((S (0)) * fs_v_dst_transform_valuessumfoldnegative) + (0))) /\ ((((exists fs_h_dst_transform_valuessumfoldnegative_body_terminal. fs_h_dst_transform_valuessumfoldnegative_body_terminal + S (dst_negative_sum_transform_valuessumfold) = S ((S (S (mi_index_transform_values))) * fs_v_dst_transform_valuessumfoldnegative)) /\ exists fs_q_dst_transform_valuessumfoldnegative_body_terminal. fs_u_dst_transform_valuessumfoldnegative = fs_q_dst_transform_valuessumfoldnegative_body_terminal * S ((S (S (mi_index_transform_values))) * fs_v_dst_transform_valuessumfoldnegative) + (dst_negative_sum_transform_valuessumfold))) /\ forall fs_i_dst_transform_valuessumfoldnegative_body_steps. (exists fs_lt_dst_transform_valuessumfoldnegative_body_steps_bound. fs_lt_dst_transform_valuessumfoldnegative_body_steps_bound + S fs_i_dst_transform_valuessumfoldnegative_body_steps = S (mi_index_transform_values)) -> exists fs_a_dst_transform_valuessumfoldnegative_body_steps fs_r_dst_transform_valuessumfoldnegative_body_steps fs_s_dst_transform_valuessumfoldnegative_body_steps. ((((exists fs_h_dst_transform_valuessumfoldnegative_body_steps_summand. fs_h_dst_transform_valuessumfoldnegative_body_steps_summand + S (fs_a_dst_transform_valuessumfoldnegative_body_steps) = S ((S (fs_i_dst_transform_valuessumfoldnegative_body_steps)) * dst_negative_scale_transform_valuessumfold)) /\ exists fs_q_dst_transform_valuessumfoldnegative_body_steps_summand. dst_negative_code_transform_valuessumfold = fs_q_dst_transform_valuessumfoldnegative_body_steps_summand * S ((S (fs_i_dst_transform_valuessumfoldnegative_body_steps)) * dst_negative_scale_transform_valuessumfold) + (fs_a_dst_transform_valuessumfoldnegative_body_steps))) /\ ((((exists fs_h_dst_transform_valuessumfoldnegative_body_steps_partial. fs_h_dst_transform_valuessumfoldnegative_body_steps_partial + S (fs_r_dst_transform_valuessumfoldnegative_body_steps) = S ((S (fs_i_dst_transform_valuessumfoldnegative_body_steps)) * fs_v_dst_transform_valuessumfoldnegative)) /\ exists fs_q_dst_transform_valuessumfoldnegative_body_steps_partial. fs_u_dst_transform_valuessumfoldnegative = fs_q_dst_transform_valuessumfoldnegative_body_steps_partial * S ((S (fs_i_dst_transform_valuessumfoldnegative_body_steps)) * fs_v_dst_transform_valuessumfoldnegative) + (fs_r_dst_transform_valuessumfoldnegative_body_steps))) /\ ((((exists fs_h_dst_transform_valuessumfoldnegative_body_steps_successor. fs_h_dst_transform_valuessumfoldnegative_body_steps_successor + S (fs_s_dst_transform_valuessumfoldnegative_body_steps) = S ((S (S fs_i_dst_transform_valuessumfoldnegative_body_steps)) * fs_v_dst_transform_valuessumfoldnegative)) /\ exists fs_q_dst_transform_valuessumfoldnegative_body_steps_successor. fs_u_dst_transform_valuessumfoldnegative = fs_q_dst_transform_valuessumfoldnegative_body_steps_successor * S ((S (S fs_i_dst_transform_valuessumfoldnegative_body_steps)) * fs_v_dst_transform_valuessumfoldnegative) + (fs_s_dst_transform_valuessumfoldnegative_body_steps))) /\ fs_s_dst_transform_valuessumfoldnegative_body_steps = fs_r_dst_transform_valuessumfoldnegative_body_steps + fs_a_dst_transform_valuessumfoldnegative_body_steps)))))) /\ (exists ge_balance_positive_transform_valuessumfoldresult ge_balance_negative_transform_valuessumfoldresult. (((((mi_value_transform_values) = 2 * (ge_balance_positive_transform_valuessumfoldresult) /\ (ge_balance_negative_transform_valuessumfoldresult) = 0) \/ exists ge_signed_half_transform_valuessumfoldresultdecode. (((mi_value_transform_values) = 2 * ge_signed_half_transform_valuessumfoldresultdecode + 1 /\ (ge_balance_positive_transform_valuessumfoldresult) = 0) /\ (ge_balance_negative_transform_valuessumfoldresult) = S ge_signed_half_transform_valuessumfoldresultdecode))) /\ ((dst_positive_sum_transform_valuessumfold) + ge_balance_negative_transform_valuessumfoldresult = (dst_negative_sum_transform_valuessumfold) + ge_balance_positive_transform_valuessumfoldresult)))))))))))))) -> (((exists dst_positive_code_transform_resultleft dst_positive_scale_transform_resultleft dst_negative_code_transform_resultleft dst_negative_scale_transform_resultleft. (((F) = (((((dst_positive_code_transform_resultleft) + (dst_positive_scale_transform_resultleft)) * S ((dst_positive_code_transform_resultleft) + (dst_positive_scale_transform_resultleft)) + ((dst_positive_scale_transform_resultleft) + (dst_positive_scale_transform_resultleft))) + (((dst_negative_code_transform_resultleft) + (dst_negative_scale_transform_resultleft)) * S ((dst_negative_code_transform_resultleft) + (dst_negative_scale_transform_resultleft)) + ((dst_negative_scale_transform_resultleft) + (dst_negative_scale_transform_resultleft)))) * S ((((dst_positive_code_transform_resultleft) + (dst_positive_scale_transform_resultleft)) * S ((dst_positive_code_transform_resultleft) + (dst_positive_scale_transform_resultleft)) + ((dst_positive_scale_transform_resultleft) + (dst_positive_scale_transform_resultleft))) + (((dst_negative_code_transform_resultleft) + (dst_negative_scale_transform_resultleft)) * S ((dst_negative_code_transform_resultleft) + (dst_negative_scale_transform_resultleft)) + ((dst_negative_scale_transform_resultleft) + (dst_negative_scale_transform_resultleft)))) + ((((dst_negative_code_transform_resultleft) + (dst_negative_scale_transform_resultleft)) * S ((dst_negative_code_transform_resultleft) + (dst_negative_scale_transform_resultleft)) + ((dst_negative_scale_transform_resultleft) + (dst_negative_scale_transform_resultleft))) + (((dst_negative_code_transform_resultleft) + (dst_negative_scale_transform_resultleft)) * S ((dst_negative_code_transform_resultleft) + (dst_negative_scale_transform_resultleft)) + ((dst_negative_scale_transform_resultleft) + (dst_negative_scale_transform_resultleft)))))) /\ (forall dst_index_transform_resultleft. (exists pvs_le_gap_transform_resultleftdomain. pvs_le_gap_transform_resultleftdomain + (dst_index_transform_resultleft) = (N)) -> exists dst_positive_transform_resultleft dst_negative_transform_resultleft dst_value_transform_resultleft. ((((exists ff_h_pvs_transform_resultleftentrypositive. ff_h_pvs_transform_resultleftentrypositive + S (dst_positive_transform_resultleft) = S ((S (dst_index_transform_resultleft)) * dst_positive_scale_transform_resultleft)) /\ exists ff_q_pvs_transform_resultleftentrypositive. dst_positive_code_transform_resultleft = ff_q_pvs_transform_resultleftentrypositive * S ((S (dst_index_transform_resultleft)) * dst_positive_scale_transform_resultleft) + (dst_positive_transform_resultleft))) /\ (((((exists ff_h_pvs_transform_resultleftentrynegative. ff_h_pvs_transform_resultleftentrynegative + S (dst_negative_transform_resultleft) = S ((S (dst_index_transform_resultleft)) * dst_negative_scale_transform_resultleft)) /\ exists ff_q_pvs_transform_resultleftentrynegative. dst_negative_code_transform_resultleft = ff_q_pvs_transform_resultleftentrynegative * S ((S (dst_index_transform_resultleft)) * dst_negative_scale_transform_resultleft) + (dst_negative_transform_resultleft))) /\ (exists ge_balance_positive_transform_resultleftentryvalue ge_balance_negative_transform_resultleftentryvalue. (((((dst_value_transform_resultleft) = 2 * (ge_balance_positive_transform_resultleftentryvalue) /\ (ge_balance_negative_transform_resultleftentryvalue) = 0) \/ exists ge_signed_half_transform_resultleftentryvaluedecode. (((dst_value_transform_resultleft) = 2 * ge_signed_half_transform_resultleftentryvaluedecode + 1 /\ (ge_balance_positive_transform_resultleftentryvalue) = 0) /\ (ge_balance_negative_transform_resultleftentryvalue) = S ge_signed_half_transform_resultleftentryvaluedecode))) /\ ((dst_positive_transform_resultleft) + ge_balance_negative_transform_resultleftentryvalue = (dst_negative_transform_resultleft) + ge_balance_positive_transform_resultleftentryvalue))))))))) /\ (((exists dst_positive_code_transform_resultright dst_positive_scale_transform_resultright dst_negative_code_transform_resultright dst_negative_scale_transform_resultright. (((U) = (((((dst_positive_code_transform_resultright) + (dst_positive_scale_transform_resultright)) * S ((dst_positive_code_transform_resultright) + (dst_positive_scale_transform_resultright)) + ((dst_positive_scale_transform_resultright) + (dst_positive_scale_transform_resultright))) + (((dst_negative_code_transform_resultright) + (dst_negative_scale_transform_resultright)) * S ((dst_negative_code_transform_resultright) + (dst_negative_scale_transform_resultright)) + ((dst_negative_scale_transform_resultright) + (dst_negative_scale_transform_resultright)))) * S ((((dst_positive_code_transform_resultright) + (dst_positive_scale_transform_resultright)) * S ((dst_positive_code_transform_resultright) + (dst_positive_scale_transform_resultright)) + ((dst_positive_scale_transform_resultright) + (dst_positive_scale_transform_resultright))) + (((dst_negative_code_transform_resultright) + (dst_negative_scale_transform_resultright)) * S ((dst_negative_code_transform_resultright) + (dst_negative_scale_transform_resultright)) + ((dst_negative_scale_transform_resultright) + (dst_negative_scale_transform_resultright)))) + ((((dst_negative_code_transform_resultright) + (dst_negative_scale_transform_resultright)) * S ((dst_negative_code_transform_resultright) + (dst_negative_scale_transform_resultright)) + ((dst_negative_scale_transform_resultright) + (dst_negative_scale_transform_resultright))) + (((dst_negative_code_transform_resultright) + (dst_negative_scale_transform_resultright)) * S ((dst_negative_code_transform_resultright) + (dst_negative_scale_transform_resultright)) + ((dst_negative_scale_transform_resultright) + (dst_negative_scale_transform_resultright)))))) /\ (forall dst_index_transform_resultright. (exists pvs_le_gap_transform_resultrightdomain. pvs_le_gap_transform_resultrightdomain + (dst_index_transform_resultright) = (N)) -> exists dst_positive_transform_resultright dst_negative_transform_resultright dst_value_transform_resultright. ((((exists ff_h_pvs_transform_resultrightentrypositive. ff_h_pvs_transform_resultrightentrypositive + S (dst_positive_transform_resultright) = S ((S (dst_index_transform_resultright)) * dst_positive_scale_transform_resultright)) /\ exists ff_q_pvs_transform_resultrightentrypositive. dst_positive_code_transform_resultright = ff_q_pvs_transform_resultrightentrypositive * S ((S (dst_index_transform_resultright)) * dst_positive_scale_transform_resultright) + (dst_positive_transform_resultright))) /\ (((((exists ff_h_pvs_transform_resultrightentrynegative. ff_h_pvs_transform_resultrightentrynegative + S (dst_negative_transform_resultright) = S ((S (dst_index_transform_resultright)) * dst_negative_scale_transform_resultright)) /\ exists ff_q_pvs_transform_resultrightentrynegative. dst_negative_code_transform_resultright = ff_q_pvs_transform_resultrightentrynegative * S ((S (dst_index_transform_resultright)) * dst_negative_scale_transform_resultright) + (dst_negative_transform_resultright))) /\ (exists ge_balance_positive_transform_resultrightentryvalue ge_balance_negative_transform_resultrightentryvalue. (((((dst_value_transform_resultright) = 2 * (ge_balance_positive_transform_resultrightentryvalue) /\ (ge_balance_negative_transform_resultrightentryvalue) = 0) \/ exists ge_signed_half_transform_resultrightentryvaluedecode. (((dst_value_transform_resultright) = 2 * ge_signed_half_transform_resultrightentryvaluedecode + 1 /\ (ge_balance_positive_transform_resultrightentryvalue) = 0) /\ (ge_balance_negative_transform_resultrightentryvalue) = S ge_signed_half_transform_resultrightentryvaluedecode))) /\ ((dst_positive_transform_resultright) + ge_balance_negative_transform_resultrightentryvalue = (dst_negative_transform_resultright) + ge_balance_positive_transform_resultrightentryvalue))))))))) /\ (((exists dst_positive_code_transform_resulttable dst_positive_scale_transform_resulttable dst_negative_code_transform_resulttable dst_negative_scale_transform_resulttable. (((G) = (((((dst_positive_code_transform_resulttable) + (dst_positive_scale_transform_resulttable)) * S ((dst_positive_code_transform_resulttable) + (dst_positive_scale_transform_resulttable)) + ((dst_positive_scale_transform_resulttable) + (dst_positive_scale_transform_resulttable))) + (((dst_negative_code_transform_resulttable) + (dst_negative_scale_transform_resulttable)) * S ((dst_negative_code_transform_resulttable) + (dst_negative_scale_transform_resulttable)) + ((dst_negative_scale_transform_resulttable) + (dst_negative_scale_transform_resulttable)))) * S ((((dst_positive_code_transform_resulttable) + (dst_positive_scale_transform_resulttable)) * S ((dst_positive_code_transform_resulttable) + (dst_positive_scale_transform_resulttable)) + ((dst_positive_scale_transform_resulttable) + (dst_positive_scale_transform_resulttable))) + (((dst_negative_code_transform_resulttable) + (dst_negative_scale_transform_resulttable)) * S ((dst_negative_code_transform_resulttable) + (dst_negative_scale_transform_resulttable)) + ((dst_negative_scale_transform_resulttable) + (dst_negative_scale_transform_resulttable)))) + ((((dst_negative_code_transform_resulttable) + (dst_negative_scale_transform_resulttable)) * S ((dst_negative_code_transform_resulttable) + (dst_negative_scale_transform_resulttable)) + ((dst_negative_scale_transform_resulttable) + (dst_negative_scale_transform_resulttable))) + (((dst_negative_code_transform_resulttable) + (dst_negative_scale_transform_resulttable)) * S ((dst_negative_code_transform_resulttable) + (dst_negative_scale_transform_resulttable)) + ((dst_negative_scale_transform_resulttable) + (dst_negative_scale_transform_resulttable)))))) /\ (forall dst_index_transform_resulttable. (exists pvs_le_gap_transform_resulttabledomain. pvs_le_gap_transform_resulttabledomain + (dst_index_transform_resulttable) = (N)) -> exists dst_positive_transform_resulttable dst_negative_transform_resulttable dst_value_transform_resulttable. ((((exists ff_h_pvs_transform_resulttableentrypositive. ff_h_pvs_transform_resulttableentrypositive + S (dst_positive_transform_resulttable) = S ((S (dst_index_transform_resulttable)) * dst_positive_scale_transform_resulttable)) /\ exists ff_q_pvs_transform_resulttableentrypositive. dst_positive_code_transform_resulttable = ff_q_pvs_transform_resulttableentrypositive * S ((S (dst_index_transform_resulttable)) * dst_positive_scale_transform_resulttable) + (dst_positive_transform_resulttable))) /\ (((((exists ff_h_pvs_transform_resulttableentrynegative. ff_h_pvs_transform_resulttableentrynegative + S (dst_negative_transform_resulttable) = S ((S (dst_index_transform_resulttable)) * dst_negative_scale_transform_resulttable)) /\ exists ff_q_pvs_transform_resulttableentrynegative. dst_negative_code_transform_resulttable = ff_q_pvs_transform_resulttableentrynegative * S ((S (dst_index_transform_resulttable)) * dst_negative_scale_transform_resulttable) + (dst_negative_transform_resulttable))) /\ (exists ge_balance_positive_transform_resulttableentryvalue ge_balance_negative_transform_resulttableentryvalue. (((((dst_value_transform_resulttable) = 2 * (ge_balance_positive_transform_resulttableentryvalue) /\ (ge_balance_negative_transform_resulttableentryvalue) = 0) \/ exists ge_signed_half_transform_resulttableentryvaluedecode. (((dst_value_transform_resulttable) = 2 * ge_signed_half_transform_resulttableentryvaluedecode + 1 /\ (ge_balance_positive_transform_resulttableentryvalue) = 0) /\ (ge_balance_negative_transform_resulttableentryvalue) = S ge_signed_half_transform_resulttableentryvaluedecode))) /\ ((dst_positive_transform_resulttable) + ge_balance_negative_transform_resulttableentryvalue = (dst_negative_transform_resulttable) + ge_balance_positive_transform_resulttableentryvalue))))))))) /\ (forall dc_input_transform_result dc_output_transform_result. ~(dc_input_transform_result=0) -> (exists pvs_le_gap_transform_resultdomain. pvs_le_gap_transform_resultdomain + (dc_input_transform_result) = (N)) -> (exists dst_positive_code_transform_resultlookup dst_positive_scale_transform_resultlookup dst_negative_code_transform_resultlookup dst_negative_scale_transform_resultlookup dst_positive_transform_resultlookup dst_negative_transform_resultlookup. (((G) = (((((dst_positive_code_transform_resultlookup) + (dst_positive_scale_transform_resultlookup)) * S ((dst_positive_code_transform_resultlookup) + (dst_positive_scale_transform_resultlookup)) + ((dst_positive_scale_transform_resultlookup) + (dst_positive_scale_transform_resultlookup))) + (((dst_negative_code_transform_resultlookup) + (dst_negative_scale_transform_resultlookup)) * S ((dst_negative_code_transform_resultlookup) + (dst_negative_scale_transform_resultlookup)) + ((dst_negative_scale_transform_resultlookup) + (dst_negative_scale_transform_resultlookup)))) * S ((((dst_positive_code_transform_resultlookup) + (dst_positive_scale_transform_resultlookup)) * S ((dst_positive_code_transform_resultlookup) + (dst_positive_scale_transform_resultlookup)) + ((dst_positive_scale_transform_resultlookup) + (dst_positive_scale_transform_resultlookup))) + (((dst_negative_code_transform_resultlookup) + (dst_negative_scale_transform_resultlookup)) * S ((dst_negative_code_transform_resultlookup) + (dst_negative_scale_transform_resultlookup)) + ((dst_negative_scale_transform_resultlookup) + (dst_negative_scale_transform_resultlookup)))) + ((((dst_negative_code_transform_resultlookup) + (dst_negative_scale_transform_resultlookup)) * S ((dst_negative_code_transform_resultlookup) + (dst_negative_scale_transform_resultlookup)) + ((dst_negative_scale_transform_resultlookup) + (dst_negative_scale_transform_resultlookup))) + (((dst_negative_code_transform_resultlookup) + (dst_negative_scale_transform_resultlookup)) * S ((dst_negative_code_transform_resultlookup) + (dst_negative_scale_transform_resultlookup)) + ((dst_negative_scale_transform_resultlookup) + (dst_negative_scale_transform_resultlookup)))))) /\ (((((exists ff_h_pvs_transform_resultlookuppositive. ff_h_pvs_transform_resultlookuppositive + S (dst_positive_transform_resultlookup) = S ((S (dc_input_transform_result)) * dst_positive_scale_transform_resultlookup)) /\ exists ff_q_pvs_transform_resultlookuppositive. dst_positive_code_transform_resultlookup = ff_q_pvs_transform_resultlookuppositive * S ((S (dc_input_transform_result)) * dst_positive_scale_transform_resultlookup) + (dst_positive_transform_resultlookup))) /\ (((((exists ff_h_pvs_transform_resultlookupnegative. ff_h_pvs_transform_resultlookupnegative + S (dst_negative_transform_resultlookup) = S ((S (dc_input_transform_result)) * dst_negative_scale_transform_resultlookup)) /\ exists ff_q_pvs_transform_resultlookupnegative. dst_negative_code_transform_resultlookup = ff_q_pvs_transform_resultlookupnegative * S ((S (dc_input_transform_result)) * dst_negative_scale_transform_resultlookup) + (dst_negative_transform_resultlookup))) /\ (exists ge_balance_positive_transform_resultlookupvalue ge_balance_negative_transform_resultlookupvalue. (((((dc_output_transform_result) = 2 * (ge_balance_positive_transform_resultlookupvalue) /\ (ge_balance_negative_transform_resultlookupvalue) = 0) \/ exists ge_signed_half_transform_resultlookupvaluedecode. (((dc_output_transform_result) = 2 * ge_signed_half_transform_resultlookupvaluedecode + 1 /\ (ge_balance_positive_transform_resultlookupvalue) = 0) /\ (ge_balance_negative_transform_resultlookupvalue) = S ge_signed_half_transform_resultlookupvaluedecode))) /\ ((dst_positive_transform_resultlookup) + ge_balance_negative_transform_resultlookupvalue = (dst_negative_transform_resultlookup) + ge_balance_positive_transform_resultlookupvalue))))))))) -> (((~((dc_input_transform_result)=0)) /\ (exists dc_mask_transform_resultvalue. ((((exists dst_positive_code_transform_resultvaluemasktable dst_positive_scale_transform_resultvaluemasktable dst_negative_code_transform_resultvaluemasktable dst_negative_scale_transform_resultvaluemasktable. (((dc_mask_transform_resultvalue) = (((((dst_positive_code_transform_resultvaluemasktable) + (dst_positive_scale_transform_resultvaluemasktable)) * S ((dst_positive_code_transform_resultvaluemasktable) + (dst_positive_scale_transform_resultvaluemasktable)) + ((dst_positive_scale_transform_resultvaluemasktable) + (dst_positive_scale_transform_resultvaluemasktable))) + (((dst_negative_code_transform_resultvaluemasktable) + (dst_negative_scale_transform_resultvaluemasktable)) * S ((dst_negative_code_transform_resultvaluemasktable) + (dst_negative_scale_transform_resultvaluemasktable)) + ((dst_negative_scale_transform_resultvaluemasktable) + (dst_negative_scale_transform_resultvaluemasktable)))) * S ((((dst_positive_code_transform_resultvaluemasktable) + (dst_positive_scale_transform_resultvaluemasktable)) * S ((dst_positive_code_transform_resultvaluemasktable) + (dst_positive_scale_transform_resultvaluemasktable)) + ((dst_positive_scale_transform_resultvaluemasktable) + (dst_positive_scale_transform_resultvaluemasktable))) + (((dst_negative_code_transform_resultvaluemasktable) + (dst_negative_scale_transform_resultvaluemasktable)) * S ((dst_negative_code_transform_resultvaluemasktable) + (dst_negative_scale_transform_resultvaluemasktable)) + ((dst_negative_scale_transform_resultvaluemasktable) + (dst_negative_scale_transform_resultvaluemasktable)))) + ((((dst_negative_code_transform_resultvaluemasktable) + (dst_negative_scale_transform_resultvaluemasktable)) * S ((dst_negative_code_transform_resultvaluemasktable) + (dst_negative_scale_transform_resultvaluemasktable)) + ((dst_negative_scale_transform_resultvaluemasktable) + (dst_negative_scale_transform_resultvaluemasktable))) + (((dst_negative_code_transform_resultvaluemasktable) + (dst_negative_scale_transform_resultvaluemasktable)) * S ((dst_negative_code_transform_resultvaluemasktable) + (dst_negative_scale_transform_resultvaluemasktable)) + ((dst_negative_scale_transform_resultvaluemasktable) + (dst_negative_scale_transform_resultvaluemasktable)))))) /\ (forall dst_index_transform_resultvaluemasktable. (exists pvs_le_gap_transform_resultvaluemasktabledomain. pvs_le_gap_transform_resultvaluemasktabledomain + (dst_index_transform_resultvaluemasktable) = (dc_input_transform_result)) -> exists dst_positive_transform_resultvaluemasktable dst_negative_transform_resultvaluemasktable dst_value_transform_resultvaluemasktable. ((((exists ff_h_pvs_transform_resultvaluemasktableentrypositive. ff_h_pvs_transform_resultvaluemasktableentrypositive + S (dst_positive_transform_resultvaluemasktable) = S ((S (dst_index_transform_resultvaluemasktable)) * dst_positive_scale_transform_resultvaluemasktable)) /\ exists ff_q_pvs_transform_resultvaluemasktableentrypositive. dst_positive_code_transform_resultvaluemasktable = ff_q_pvs_transform_resultvaluemasktableentrypositive * S ((S (dst_index_transform_resultvaluemasktable)) * dst_positive_scale_transform_resultvaluemasktable) + (dst_positive_transform_resultvaluemasktable))) /\ (((((exists ff_h_pvs_transform_resultvaluemasktableentrynegative. ff_h_pvs_transform_resultvaluemasktableentrynegative + S (dst_negative_transform_resultvaluemasktable) = S ((S (dst_index_transform_resultvaluemasktable)) * dst_negative_scale_transform_resultvaluemasktable)) /\ exists ff_q_pvs_transform_resultvaluemasktableentrynegative. dst_negative_code_transform_resultvaluemasktable = ff_q_pvs_transform_resultvaluemasktableentrynegative * S ((S (dst_index_transform_resultvaluemasktable)) * dst_negative_scale_transform_resultvaluemasktable) + (dst_negative_transform_resultvaluemasktable))) /\ (exists ge_balance_positive_transform_resultvaluemasktableentryvalue ge_balance_negative_transform_resultvaluemasktableentryvalue. (((((dst_value_transform_resultvaluemasktable) = 2 * (ge_balance_positive_transform_resultvaluemasktableentryvalue) /\ (ge_balance_negative_transform_resultvaluemasktableentryvalue) = 0) \/ exists ge_signed_half_transform_resultvaluemasktableentryvaluedecode. (((dst_value_transform_resultvaluemasktable) = 2 * ge_signed_half_transform_resultvaluemasktableentryvaluedecode + 1 /\ (ge_balance_positive_transform_resultvaluemasktableentryvalue) = 0) /\ (ge_balance_negative_transform_resultvaluemasktableentryvalue) = S ge_signed_half_transform_resultvaluemasktableentryvaluedecode))) /\ ((dst_positive_transform_resultvaluemasktable) + ge_balance_negative_transform_resultvaluemasktableentryvalue = (dst_negative_transform_resultvaluemasktable) + ge_balance_positive_transform_resultvaluemasktableentryvalue))))))))) /\ (forall dc_index_transform_resultvaluemask dc_value_transform_resultvaluemask. (exists pvs_le_gap_transform_resultvaluemaskdomain. pvs_le_gap_transform_resultvaluemaskdomain + (dc_index_transform_resultvaluemask) = (dc_input_transform_result)) -> (exists dst_positive_code_transform_resultvaluemasklookup dst_positive_scale_transform_resultvaluemasklookup dst_negative_code_transform_resultvaluemasklookup dst_negative_scale_transform_resultvaluemasklookup dst_positive_transform_resultvaluemasklookup dst_negative_transform_resultvaluemasklookup. (((dc_mask_transform_resultvalue) = (((((dst_positive_code_transform_resultvaluemasklookup) + (dst_positive_scale_transform_resultvaluemasklookup)) * S ((dst_positive_code_transform_resultvaluemasklookup) + (dst_positive_scale_transform_resultvaluemasklookup)) + ((dst_positive_scale_transform_resultvaluemasklookup) + (dst_positive_scale_transform_resultvaluemasklookup))) + (((dst_negative_code_transform_resultvaluemasklookup) + (dst_negative_scale_transform_resultvaluemasklookup)) * S ((dst_negative_code_transform_resultvaluemasklookup) + (dst_negative_scale_transform_resultvaluemasklookup)) + ((dst_negative_scale_transform_resultvaluemasklookup) + (dst_negative_scale_transform_resultvaluemasklookup)))) * S ((((dst_positive_code_transform_resultvaluemasklookup) + (dst_positive_scale_transform_resultvaluemasklookup)) * S ((dst_positive_code_transform_resultvaluemasklookup) + (dst_positive_scale_transform_resultvaluemasklookup)) + ((dst_positive_scale_transform_resultvaluemasklookup) + (dst_positive_scale_transform_resultvaluemasklookup))) + (((dst_negative_code_transform_resultvaluemasklookup) + (dst_negative_scale_transform_resultvaluemasklookup)) * S ((dst_negative_code_transform_resultvaluemasklookup) + (dst_negative_scale_transform_resultvaluemasklookup)) + ((dst_negative_scale_transform_resultvaluemasklookup) + (dst_negative_scale_transform_resultvaluemasklookup)))) + ((((dst_negative_code_transform_resultvaluemasklookup) + (dst_negative_scale_transform_resultvaluemasklookup)) * S ((dst_negative_code_transform_resultvaluemasklookup) + (dst_negative_scale_transform_resultvaluemasklookup)) + ((dst_negative_scale_transform_resultvaluemasklookup) + (dst_negative_scale_transform_resultvaluemasklookup))) + (((dst_negative_code_transform_resultvaluemasklookup) + (dst_negative_scale_transform_resultvaluemasklookup)) * S ((dst_negative_code_transform_resultvaluemasklookup) + (dst_negative_scale_transform_resultvaluemasklookup)) + ((dst_negative_scale_transform_resultvaluemasklookup) + (dst_negative_scale_transform_resultvaluemasklookup)))))) /\ (((((exists ff_h_pvs_transform_resultvaluemasklookuppositive. ff_h_pvs_transform_resultvaluemasklookuppositive + S (dst_positive_transform_resultvaluemasklookup) = S ((S (dc_index_transform_resultvaluemask)) * dst_positive_scale_transform_resultvaluemasklookup)) /\ exists ff_q_pvs_transform_resultvaluemasklookuppositive. dst_positive_code_transform_resultvaluemasklookup = ff_q_pvs_transform_resultvaluemasklookuppositive * S ((S (dc_index_transform_resultvaluemask)) * dst_positive_scale_transform_resultvaluemasklookup) + (dst_positive_transform_resultvaluemasklookup))) /\ (((((exists ff_h_pvs_transform_resultvaluemasklookupnegative. ff_h_pvs_transform_resultvaluemasklookupnegative + S (dst_negative_transform_resultvaluemasklookup) = S ((S (dc_index_transform_resultvaluemask)) * dst_negative_scale_transform_resultvaluemasklookup)) /\ exists ff_q_pvs_transform_resultvaluemasklookupnegative. dst_negative_code_transform_resultvaluemasklookup = ff_q_pvs_transform_resultvaluemasklookupnegative * S ((S (dc_index_transform_resultvaluemask)) * dst_negative_scale_transform_resultvaluemasklookup) + (dst_negative_transform_resultvaluemasklookup))) /\ (exists ge_balance_positive_transform_resultvaluemasklookupvalue ge_balance_negative_transform_resultvaluemasklookupvalue. (((((dc_value_transform_resultvaluemask) = 2 * (ge_balance_positive_transform_resultvaluemasklookupvalue) /\ (ge_balance_negative_transform_resultvaluemasklookupvalue) = 0) \/ exists ge_signed_half_transform_resultvaluemasklookupvaluedecode. (((dc_value_transform_resultvaluemask) = 2 * ge_signed_half_transform_resultvaluemasklookupvaluedecode + 1 /\ (ge_balance_positive_transform_resultvaluemasklookupvalue) = 0) /\ (ge_balance_negative_transform_resultvaluemasklookupvalue) = S ge_signed_half_transform_resultvaluemasklookupvaluedecode))) /\ ((dst_positive_transform_resultvaluemasklookup) + ge_balance_negative_transform_resultvaluemasklookupvalue = (dst_negative_transform_resultvaluemasklookup) + ge_balance_positive_transform_resultvaluemasklookupvalue))))))))) -> ((((~((dc_index_transform_resultvaluemask)=0)) /\ (exists dc_quotient_transform_resultvaluemaskentry dc_left_transform_resultvaluemaskentry dc_right_transform_resultvaluemaskentry. (((dc_input_transform_result)=(dc_index_transform_resultvaluemask)*dc_quotient_transform_resultvaluemaskentry) /\ (((exists dst_positive_code_transform_resultvaluemaskentryleft dst_positive_scale_transform_resultvaluemaskentryleft dst_negative_code_transform_resultvaluemaskentryleft dst_negative_scale_transform_resultvaluemaskentryleft dst_positive_transform_resultvaluemaskentryleft dst_negative_transform_resultvaluemaskentryleft. (((F) = (((((dst_positive_code_transform_resultvaluemaskentryleft) + (dst_positive_scale_transform_resultvaluemaskentryleft)) * S ((dst_positive_code_transform_resultvaluemaskentryleft) + (dst_positive_scale_transform_resultvaluemaskentryleft)) + ((dst_positive_scale_transform_resultvaluemaskentryleft) + (dst_positive_scale_transform_resultvaluemaskentryleft))) + (((dst_negative_code_transform_resultvaluemaskentryleft) + (dst_negative_scale_transform_resultvaluemaskentryleft)) * S ((dst_negative_code_transform_resultvaluemaskentryleft) + (dst_negative_scale_transform_resultvaluemaskentryleft)) + ((dst_negative_scale_transform_resultvaluemaskentryleft) + (dst_negative_scale_transform_resultvaluemaskentryleft)))) * S ((((dst_positive_code_transform_resultvaluemaskentryleft) + (dst_positive_scale_transform_resultvaluemaskentryleft)) * S ((dst_positive_code_transform_resultvaluemaskentryleft) + (dst_positive_scale_transform_resultvaluemaskentryleft)) + ((dst_positive_scale_transform_resultvaluemaskentryleft) + (dst_positive_scale_transform_resultvaluemaskentryleft))) + (((dst_negative_code_transform_resultvaluemaskentryleft) + (dst_negative_scale_transform_resultvaluemaskentryleft)) * S ((dst_negative_code_transform_resultvaluemaskentryleft) + (dst_negative_scale_transform_resultvaluemaskentryleft)) + ((dst_negative_scale_transform_resultvaluemaskentryleft) + (dst_negative_scale_transform_resultvaluemaskentryleft)))) + ((((dst_negative_code_transform_resultvaluemaskentryleft) + (dst_negative_scale_transform_resultvaluemaskentryleft)) * S ((dst_negative_code_transform_resultvaluemaskentryleft) + (dst_negative_scale_transform_resultvaluemaskentryleft)) + ((dst_negative_scale_transform_resultvaluemaskentryleft) + (dst_negative_scale_transform_resultvaluemaskentryleft))) + (((dst_negative_code_transform_resultvaluemaskentryleft) + (dst_negative_scale_transform_resultvaluemaskentryleft)) * S ((dst_negative_code_transform_resultvaluemaskentryleft) + (dst_negative_scale_transform_resultvaluemaskentryleft)) + ((dst_negative_scale_transform_resultvaluemaskentryleft) + (dst_negative_scale_transform_resultvaluemaskentryleft)))))) /\ (((((exists ff_h_pvs_transform_resultvaluemaskentryleftpositive. ff_h_pvs_transform_resultvaluemaskentryleftpositive + S (dst_positive_transform_resultvaluemaskentryleft) = S ((S (dc_index_transform_resultvaluemask)) * dst_positive_scale_transform_resultvaluemaskentryleft)) /\ exists ff_q_pvs_transform_resultvaluemaskentryleftpositive. dst_positive_code_transform_resultvaluemaskentryleft = ff_q_pvs_transform_resultvaluemaskentryleftpositive * S ((S (dc_index_transform_resultvaluemask)) * dst_positive_scale_transform_resultvaluemaskentryleft) + (dst_positive_transform_resultvaluemaskentryleft))) /\ (((((exists ff_h_pvs_transform_resultvaluemaskentryleftnegative. ff_h_pvs_transform_resultvaluemaskentryleftnegative + S (dst_negative_transform_resultvaluemaskentryleft) = S ((S (dc_index_transform_resultvaluemask)) * dst_negative_scale_transform_resultvaluemaskentryleft)) /\ exists ff_q_pvs_transform_resultvaluemaskentryleftnegative. dst_negative_code_transform_resultvaluemaskentryleft = ff_q_pvs_transform_resultvaluemaskentryleftnegative * S ((S (dc_index_transform_resultvaluemask)) * dst_negative_scale_transform_resultvaluemaskentryleft) + (dst_negative_transform_resultvaluemaskentryleft))) /\ (exists ge_balance_positive_transform_resultvaluemaskentryleftvalue ge_balance_negative_transform_resultvaluemaskentryleftvalue. (((((dc_left_transform_resultvaluemaskentry) = 2 * (ge_balance_positive_transform_resultvaluemaskentryleftvalue) /\ (ge_balance_negative_transform_resultvaluemaskentryleftvalue) = 0) \/ exists ge_signed_half_transform_resultvaluemaskentryleftvaluedecode. (((dc_left_transform_resultvaluemaskentry) = 2 * ge_signed_half_transform_resultvaluemaskentryleftvaluedecode + 1 /\ (ge_balance_positive_transform_resultvaluemaskentryleftvalue) = 0) /\ (ge_balance_negative_transform_resultvaluemaskentryleftvalue) = S ge_signed_half_transform_resultvaluemaskentryleftvaluedecode))) /\ ((dst_positive_transform_resultvaluemaskentryleft) + ge_balance_negative_transform_resultvaluemaskentryleftvalue = (dst_negative_transform_resultvaluemaskentryleft) + ge_balance_positive_transform_resultvaluemaskentryleftvalue))))))))) /\ (((exists dst_positive_code_transform_resultvaluemaskentryright dst_positive_scale_transform_resultvaluemaskentryright dst_negative_code_transform_resultvaluemaskentryright dst_negative_scale_transform_resultvaluemaskentryright dst_positive_transform_resultvaluemaskentryright dst_negative_transform_resultvaluemaskentryright. (((U) = (((((dst_positive_code_transform_resultvaluemaskentryright) + (dst_positive_scale_transform_resultvaluemaskentryright)) * S ((dst_positive_code_transform_resultvaluemaskentryright) + (dst_positive_scale_transform_resultvaluemaskentryright)) + ((dst_positive_scale_transform_resultvaluemaskentryright) + (dst_positive_scale_transform_resultvaluemaskentryright))) + (((dst_negative_code_transform_resultvaluemaskentryright) + (dst_negative_scale_transform_resultvaluemaskentryright)) * S ((dst_negative_code_transform_resultvaluemaskentryright) + (dst_negative_scale_transform_resultvaluemaskentryright)) + ((dst_negative_scale_transform_resultvaluemaskentryright) + (dst_negative_scale_transform_resultvaluemaskentryright)))) * S ((((dst_positive_code_transform_resultvaluemaskentryright) + (dst_positive_scale_transform_resultvaluemaskentryright)) * S ((dst_positive_code_transform_resultvaluemaskentryright) + (dst_positive_scale_transform_resultvaluemaskentryright)) + ((dst_positive_scale_transform_resultvaluemaskentryright) + (dst_positive_scale_transform_resultvaluemaskentryright))) + (((dst_negative_code_transform_resultvaluemaskentryright) + (dst_negative_scale_transform_resultvaluemaskentryright)) * S ((dst_negative_code_transform_resultvaluemaskentryright) + (dst_negative_scale_transform_resultvaluemaskentryright)) + ((dst_negative_scale_transform_resultvaluemaskentryright) + (dst_negative_scale_transform_resultvaluemaskentryright)))) + ((((dst_negative_code_transform_resultvaluemaskentryright) + (dst_negative_scale_transform_resultvaluemaskentryright)) * S ((dst_negative_code_transform_resultvaluemaskentryright) + (dst_negative_scale_transform_resultvaluemaskentryright)) + ((dst_negative_scale_transform_resultvaluemaskentryright) + (dst_negative_scale_transform_resultvaluemaskentryright))) + (((dst_negative_code_transform_resultvaluemaskentryright) + (dst_negative_scale_transform_resultvaluemaskentryright)) * S ((dst_negative_code_transform_resultvaluemaskentryright) + (dst_negative_scale_transform_resultvaluemaskentryright)) + ((dst_negative_scale_transform_resultvaluemaskentryright) + (dst_negative_scale_transform_resultvaluemaskentryright)))))) /\ (((((exists ff_h_pvs_transform_resultvaluemaskentryrightpositive. ff_h_pvs_transform_resultvaluemaskentryrightpositive + S (dst_positive_transform_resultvaluemaskentryright) = S ((S (dc_quotient_transform_resultvaluemaskentry)) * dst_positive_scale_transform_resultvaluemaskentryright)) /\ exists ff_q_pvs_transform_resultvaluemaskentryrightpositive. dst_positive_code_transform_resultvaluemaskentryright = ff_q_pvs_transform_resultvaluemaskentryrightpositive * S ((S (dc_quotient_transform_resultvaluemaskentry)) * dst_positive_scale_transform_resultvaluemaskentryright) + (dst_positive_transform_resultvaluemaskentryright))) /\ (((((exists ff_h_pvs_transform_resultvaluemaskentryrightnegative. ff_h_pvs_transform_resultvaluemaskentryrightnegative + S (dst_negative_transform_resultvaluemaskentryright) = S ((S (dc_quotient_transform_resultvaluemaskentry)) * dst_negative_scale_transform_resultvaluemaskentryright)) /\ exists ff_q_pvs_transform_resultvaluemaskentryrightnegative. dst_negative_code_transform_resultvaluemaskentryright = ff_q_pvs_transform_resultvaluemaskentryrightnegative * S ((S (dc_quotient_transform_resultvaluemaskentry)) * dst_negative_scale_transform_resultvaluemaskentryright) + (dst_negative_transform_resultvaluemaskentryright))) /\ (exists ge_balance_positive_transform_resultvaluemaskentryrightvalue ge_balance_negative_transform_resultvaluemaskentryrightvalue. (((((dc_right_transform_resultvaluemaskentry) = 2 * (ge_balance_positive_transform_resultvaluemaskentryrightvalue) /\ (ge_balance_negative_transform_resultvaluemaskentryrightvalue) = 0) \/ exists ge_signed_half_transform_resultvaluemaskentryrightvaluedecode. (((dc_right_transform_resultvaluemaskentry) = 2 * ge_signed_half_transform_resultvaluemaskentryrightvaluedecode + 1 /\ (ge_balance_positive_transform_resultvaluemaskentryrightvalue) = 0) /\ (ge_balance_negative_transform_resultvaluemaskentryrightvalue) = S ge_signed_half_transform_resultvaluemaskentryrightvaluedecode))) /\ ((dst_positive_transform_resultvaluemaskentryright) + ge_balance_negative_transform_resultvaluemaskentryrightvalue = (dst_negative_transform_resultvaluemaskentryright) + ge_balance_positive_transform_resultvaluemaskentryrightvalue))))))))) /\ (exists sto_ap_transform_resultvaluemaskentryproduct sto_an_transform_resultvaluemaskentryproduct sto_bp_transform_resultvaluemaskentryproduct sto_bn_transform_resultvaluemaskentryproduct sto_cp_transform_resultvaluemaskentryproduct sto_cn_transform_resultvaluemaskentryproduct. (((((dc_left_transform_resultvaluemaskentry) = 2 * (sto_ap_transform_resultvaluemaskentryproduct) /\ (sto_an_transform_resultvaluemaskentryproduct) = 0) \/ exists ge_signed_half_transform_resultvaluemaskentryproductleft. (((dc_left_transform_resultvaluemaskentry) = 2 * ge_signed_half_transform_resultvaluemaskentryproductleft + 1 /\ (sto_ap_transform_resultvaluemaskentryproduct) = 0) /\ (sto_an_transform_resultvaluemaskentryproduct) = S ge_signed_half_transform_resultvaluemaskentryproductleft))) /\ ((((((dc_right_transform_resultvaluemaskentry) = 2 * (sto_bp_transform_resultvaluemaskentryproduct) /\ (sto_bn_transform_resultvaluemaskentryproduct) = 0) \/ exists ge_signed_half_transform_resultvaluemaskentryproductright. (((dc_right_transform_resultvaluemaskentry) = 2 * ge_signed_half_transform_resultvaluemaskentryproductright + 1 /\ (sto_bp_transform_resultvaluemaskentryproduct) = 0) /\ (sto_bn_transform_resultvaluemaskentryproduct) = S ge_signed_half_transform_resultvaluemaskentryproductright))) /\ ((((((dc_value_transform_resultvaluemask) = 2 * (sto_cp_transform_resultvaluemaskentryproduct) /\ (sto_cn_transform_resultvaluemaskentryproduct) = 0) \/ exists ge_signed_half_transform_resultvaluemaskentryproductoutput. (((dc_value_transform_resultvaluemask) = 2 * ge_signed_half_transform_resultvaluemaskentryproductoutput + 1 /\ (sto_cp_transform_resultvaluemaskentryproduct) = 0) /\ (sto_cn_transform_resultvaluemaskentryproduct) = S ge_signed_half_transform_resultvaluemaskentryproductoutput))) /\ ((sto_ap_transform_resultvaluemaskentryproduct * sto_bp_transform_resultvaluemaskentryproduct + sto_an_transform_resultvaluemaskentryproduct * sto_bn_transform_resultvaluemaskentryproduct) + sto_cn_transform_resultvaluemaskentryproduct = (sto_ap_transform_resultvaluemaskentryproduct * sto_bn_transform_resultvaluemaskentryproduct + sto_an_transform_resultvaluemaskentryproduct * sto_bp_transform_resultvaluemaskentryproduct) + sto_cp_transform_resultvaluemaskentryproduct))))))))))))))) \/ ((((dc_index_transform_resultvaluemask)=0 \/ ~(exists pvs_factor_transform_resultvaluemaskentrynondivisor. (dc_input_transform_result) = (dc_index_transform_resultvaluemask) * pvs_factor_transform_resultvaluemaskentrynondivisor)) /\ ((dc_value_transform_resultvaluemask)=0))))))) /\ (exists dst_positive_code_transform_resultvaluefold dst_positive_scale_transform_resultvaluefold dst_negative_code_transform_resultvaluefold dst_negative_scale_transform_resultvaluefold dst_positive_sum_transform_resultvaluefold dst_negative_sum_transform_resultvaluefold. (((dc_mask_transform_resultvalue) = (((((dst_positive_code_transform_resultvaluefold) + (dst_positive_scale_transform_resultvaluefold)) * S ((dst_positive_code_transform_resultvaluefold) + (dst_positive_scale_transform_resultvaluefold)) + ((dst_positive_scale_transform_resultvaluefold) + (dst_positive_scale_transform_resultvaluefold))) + (((dst_negative_code_transform_resultvaluefold) + (dst_negative_scale_transform_resultvaluefold)) * S ((dst_negative_code_transform_resultvaluefold) + (dst_negative_scale_transform_resultvaluefold)) + ((dst_negative_scale_transform_resultvaluefold) + (dst_negative_scale_transform_resultvaluefold)))) * S ((((dst_positive_code_transform_resultvaluefold) + (dst_positive_scale_transform_resultvaluefold)) * S ((dst_positive_code_transform_resultvaluefold) + (dst_positive_scale_transform_resultvaluefold)) + ((dst_positive_scale_transform_resultvaluefold) + (dst_positive_scale_transform_resultvaluefold))) + (((dst_negative_code_transform_resultvaluefold) + (dst_negative_scale_transform_resultvaluefold)) * S ((dst_negative_code_transform_resultvaluefold) + (dst_negative_scale_transform_resultvaluefold)) + ((dst_negative_scale_transform_resultvaluefold) + (dst_negative_scale_transform_resultvaluefold)))) + ((((dst_negative_code_transform_resultvaluefold) + (dst_negative_scale_transform_resultvaluefold)) * S ((dst_negative_code_transform_resultvaluefold) + (dst_negative_scale_transform_resultvaluefold)) + ((dst_negative_scale_transform_resultvaluefold) + (dst_negative_scale_transform_resultvaluefold))) + (((dst_negative_code_transform_resultvaluefold) + (dst_negative_scale_transform_resultvaluefold)) * S ((dst_negative_code_transform_resultvaluefold) + (dst_negative_scale_transform_resultvaluefold)) + ((dst_negative_scale_transform_resultvaluefold) + (dst_negative_scale_transform_resultvaluefold)))))) /\ (((exists fs_u_dst_transform_resultvaluefoldpositive fs_v_dst_transform_resultvaluefoldpositive. ((((exists fs_h_dst_transform_resultvaluefoldpositive_body_start. fs_h_dst_transform_resultvaluefoldpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_transform_resultvaluefoldpositive)) /\ exists fs_q_dst_transform_resultvaluefoldpositive_body_start. fs_u_dst_transform_resultvaluefoldpositive = fs_q_dst_transform_resultvaluefoldpositive_body_start * S ((S (0)) * fs_v_dst_transform_resultvaluefoldpositive) + (0))) /\ ((((exists fs_h_dst_transform_resultvaluefoldpositive_body_terminal. fs_h_dst_transform_resultvaluefoldpositive_body_terminal + S (dst_positive_sum_transform_resultvaluefold) = S ((S (S (dc_input_transform_result))) * fs_v_dst_transform_resultvaluefoldpositive)) /\ exists fs_q_dst_transform_resultvaluefoldpositive_body_terminal. fs_u_dst_transform_resultvaluefoldpositive = fs_q_dst_transform_resultvaluefoldpositive_body_terminal * S ((S (S (dc_input_transform_result))) * fs_v_dst_transform_resultvaluefoldpositive) + (dst_positive_sum_transform_resultvaluefold))) /\ forall fs_i_dst_transform_resultvaluefoldpositive_body_steps. (exists fs_lt_dst_transform_resultvaluefoldpositive_body_steps_bound. fs_lt_dst_transform_resultvaluefoldpositive_body_steps_bound + S fs_i_dst_transform_resultvaluefoldpositive_body_steps = S (dc_input_transform_result)) -> exists fs_a_dst_transform_resultvaluefoldpositive_body_steps fs_r_dst_transform_resultvaluefoldpositive_body_steps fs_s_dst_transform_resultvaluefoldpositive_body_steps. ((((exists fs_h_dst_transform_resultvaluefoldpositive_body_steps_summand. fs_h_dst_transform_resultvaluefoldpositive_body_steps_summand + S (fs_a_dst_transform_resultvaluefoldpositive_body_steps) = S ((S (fs_i_dst_transform_resultvaluefoldpositive_body_steps)) * dst_positive_scale_transform_resultvaluefold)) /\ exists fs_q_dst_transform_resultvaluefoldpositive_body_steps_summand. dst_positive_code_transform_resultvaluefold = fs_q_dst_transform_resultvaluefoldpositive_body_steps_summand * S ((S (fs_i_dst_transform_resultvaluefoldpositive_body_steps)) * dst_positive_scale_transform_resultvaluefold) + (fs_a_dst_transform_resultvaluefoldpositive_body_steps))) /\ ((((exists fs_h_dst_transform_resultvaluefoldpositive_body_steps_partial. fs_h_dst_transform_resultvaluefoldpositive_body_steps_partial + S (fs_r_dst_transform_resultvaluefoldpositive_body_steps) = S ((S (fs_i_dst_transform_resultvaluefoldpositive_body_steps)) * fs_v_dst_transform_resultvaluefoldpositive)) /\ exists fs_q_dst_transform_resultvaluefoldpositive_body_steps_partial. fs_u_dst_transform_resultvaluefoldpositive = fs_q_dst_transform_resultvaluefoldpositive_body_steps_partial * S ((S (fs_i_dst_transform_resultvaluefoldpositive_body_steps)) * fs_v_dst_transform_resultvaluefoldpositive) + (fs_r_dst_transform_resultvaluefoldpositive_body_steps))) /\ ((((exists fs_h_dst_transform_resultvaluefoldpositive_body_steps_successor. fs_h_dst_transform_resultvaluefoldpositive_body_steps_successor + S (fs_s_dst_transform_resultvaluefoldpositive_body_steps) = S ((S (S fs_i_dst_transform_resultvaluefoldpositive_body_steps)) * fs_v_dst_transform_resultvaluefoldpositive)) /\ exists fs_q_dst_transform_resultvaluefoldpositive_body_steps_successor. fs_u_dst_transform_resultvaluefoldpositive = fs_q_dst_transform_resultvaluefoldpositive_body_steps_successor * S ((S (S fs_i_dst_transform_resultvaluefoldpositive_body_steps)) * fs_v_dst_transform_resultvaluefoldpositive) + (fs_s_dst_transform_resultvaluefoldpositive_body_steps))) /\ fs_s_dst_transform_resultvaluefoldpositive_body_steps = fs_r_dst_transform_resultvaluefoldpositive_body_steps + fs_a_dst_transform_resultvaluefoldpositive_body_steps)))))) /\ (((exists fs_u_dst_transform_resultvaluefoldnegative fs_v_dst_transform_resultvaluefoldnegative. ((((exists fs_h_dst_transform_resultvaluefoldnegative_body_start. fs_h_dst_transform_resultvaluefoldnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_transform_resultvaluefoldnegative)) /\ exists fs_q_dst_transform_resultvaluefoldnegative_body_start. fs_u_dst_transform_resultvaluefoldnegative = fs_q_dst_transform_resultvaluefoldnegative_body_start * S ((S (0)) * fs_v_dst_transform_resultvaluefoldnegative) + (0))) /\ ((((exists fs_h_dst_transform_resultvaluefoldnegative_body_terminal. fs_h_dst_transform_resultvaluefoldnegative_body_terminal + S (dst_negative_sum_transform_resultvaluefold) = S ((S (S (dc_input_transform_result))) * fs_v_dst_transform_resultvaluefoldnegative)) /\ exists fs_q_dst_transform_resultvaluefoldnegative_body_terminal. fs_u_dst_transform_resultvaluefoldnegative = fs_q_dst_transform_resultvaluefoldnegative_body_terminal * S ((S (S (dc_input_transform_result))) * fs_v_dst_transform_resultvaluefoldnegative) + (dst_negative_sum_transform_resultvaluefold))) /\ forall fs_i_dst_transform_resultvaluefoldnegative_body_steps. (exists fs_lt_dst_transform_resultvaluefoldnegative_body_steps_bound. fs_lt_dst_transform_resultvaluefoldnegative_body_steps_bound + S fs_i_dst_transform_resultvaluefoldnegative_body_steps = S (dc_input_transform_result)) -> exists fs_a_dst_transform_resultvaluefoldnegative_body_steps fs_r_dst_transform_resultvaluefoldnegative_body_steps fs_s_dst_transform_resultvaluefoldnegative_body_steps. ((((exists fs_h_dst_transform_resultvaluefoldnegative_body_steps_summand. fs_h_dst_transform_resultvaluefoldnegative_body_steps_summand + S (fs_a_dst_transform_resultvaluefoldnegative_body_steps) = S ((S (fs_i_dst_transform_resultvaluefoldnegative_body_steps)) * dst_negative_scale_transform_resultvaluefold)) /\ exists fs_q_dst_transform_resultvaluefoldnegative_body_steps_summand. dst_negative_code_transform_resultvaluefold = fs_q_dst_transform_resultvaluefoldnegative_body_steps_summand * S ((S (fs_i_dst_transform_resultvaluefoldnegative_body_steps)) * dst_negative_scale_transform_resultvaluefold) + (fs_a_dst_transform_resultvaluefoldnegative_body_steps))) /\ ((((exists fs_h_dst_transform_resultvaluefoldnegative_body_steps_partial. fs_h_dst_transform_resultvaluefoldnegative_body_steps_partial + S (fs_r_dst_transform_resultvaluefoldnegative_body_steps) = S ((S (fs_i_dst_transform_resultvaluefoldnegative_body_steps)) * fs_v_dst_transform_resultvaluefoldnegative)) /\ exists fs_q_dst_transform_resultvaluefoldnegative_body_steps_partial. fs_u_dst_transform_resultvaluefoldnegative = fs_q_dst_transform_resultvaluefoldnegative_body_steps_partial * S ((S (fs_i_dst_transform_resultvaluefoldnegative_body_steps)) * fs_v_dst_transform_resultvaluefoldnegative) + (fs_r_dst_transform_resultvaluefoldnegative_body_steps))) /\ ((((exists fs_h_dst_transform_resultvaluefoldnegative_body_steps_successor. fs_h_dst_transform_resultvaluefoldnegative_body_steps_successor + S (fs_s_dst_transform_resultvaluefoldnegative_body_steps) = S ((S (S fs_i_dst_transform_resultvaluefoldnegative_body_steps)) * fs_v_dst_transform_resultvaluefoldnegative)) /\ exists fs_q_dst_transform_resultvaluefoldnegative_body_steps_successor. fs_u_dst_transform_resultvaluefoldnegative = fs_q_dst_transform_resultvaluefoldnegative_body_steps_successor * S ((S (S fs_i_dst_transform_resultvaluefoldnegative_body_steps)) * fs_v_dst_transform_resultvaluefoldnegative) + (fs_s_dst_transform_resultvaluefoldnegative_body_steps))) /\ fs_s_dst_transform_resultvaluefoldnegative_body_steps = fs_r_dst_transform_resultvaluefoldnegative_body_steps + fs_a_dst_transform_resultvaluefoldnegative_body_steps)))))) /\ (exists ge_balance_positive_transform_resultvaluefoldresult ge_balance_negative_transform_resultvaluefoldresult. (((((dc_output_transform_result) = 2 * (ge_balance_positive_transform_resultvaluefoldresult) /\ (ge_balance_negative_transform_resultvaluefoldresult) = 0) \/ exists ge_signed_half_transform_resultvaluefoldresultdecode. (((dc_output_transform_result) = 2 * ge_signed_half_transform_resultvaluefoldresultdecode + 1 /\ (ge_balance_positive_transform_resultvaluefoldresult) = 0) /\ (ge_balance_negative_transform_resultvaluefoldresult) = S ge_signed_half_transform_resultvaluefoldresultdecode))) /\ ((dst_positive_sum_transform_resultvaluefold) + ge_balance_negative_transform_resultvaluefoldresult = (dst_negative_sum_transform_resultvaluefold) + ge_balance_positive_transform_resultvaluefoldresult))))))))))))))))))))