signed_support_incidence_from_flat_prefix

Exact expanded first-order arithmetic statement

forall A r s L M T. (exists dst_positive_code_grid_input_table dst_positive_scale_grid_input_table dst_negative_code_grid_input_table dst_negative_scale_grid_input_table. (((A) = (((((dst_positive_code_grid_input_table) + (dst_positive_scale_grid_input_table)) * S ((dst_positive_code_grid_input_table) + (dst_positive_scale_grid_input_table)) + ((dst_positive_scale_grid_input_table) + (dst_positive_scale_grid_input_table))) + (((dst_negative_code_grid_input_table) + (dst_negative_scale_grid_input_table)) * S ((dst_negative_code_grid_input_table) + (dst_negative_scale_grid_input_table)) + ((dst_negative_scale_grid_input_table) + (dst_negative_scale_grid_input_table)))) * S ((((dst_positive_code_grid_input_table) + (dst_positive_scale_grid_input_table)) * S ((dst_positive_code_grid_input_table) + (dst_positive_scale_grid_input_table)) + ((dst_positive_scale_grid_input_table) + (dst_positive_scale_grid_input_table))) + (((dst_negative_code_grid_input_table) + (dst_negative_scale_grid_input_table)) * S ((dst_negative_code_grid_input_table) + (dst_negative_scale_grid_input_table)) + ((dst_negative_scale_grid_input_table) + (dst_negative_scale_grid_input_table)))) + ((((dst_negative_code_grid_input_table) + (dst_negative_scale_grid_input_table)) * S ((dst_negative_code_grid_input_table) + (dst_negative_scale_grid_input_table)) + ((dst_negative_scale_grid_input_table) + (dst_negative_scale_grid_input_table))) + (((dst_negative_code_grid_input_table) + (dst_negative_scale_grid_input_table)) * S ((dst_negative_code_grid_input_table) + (dst_negative_scale_grid_input_table)) + ((dst_negative_scale_grid_input_table) + (dst_negative_scale_grid_input_table)))))) /\ (forall dst_index_grid_input_table. (exists pvs_le_gap_grid_input_tabledomain. pvs_le_gap_grid_input_tabledomain + (dst_index_grid_input_table) = (0)) -> exists dst_positive_grid_input_table dst_negative_grid_input_table dst_value_grid_input_table. ((((exists ff_h_pvs_grid_input_tableentrypositive. ff_h_pvs_grid_input_tableentrypositive + S (dst_positive_grid_input_table) = S ((S (dst_index_grid_input_table)) * dst_positive_scale_grid_input_table)) /\ exists ff_q_pvs_grid_input_tableentrypositive. dst_positive_code_grid_input_table = ff_q_pvs_grid_input_tableentrypositive * S ((S (dst_index_grid_input_table)) * dst_positive_scale_grid_input_table) + (dst_positive_grid_input_table))) /\ (((((exists ff_h_pvs_grid_input_tableentrynegative. ff_h_pvs_grid_input_tableentrynegative + S (dst_negative_grid_input_table) = S ((S (dst_index_grid_input_table)) * dst_negative_scale_grid_input_table)) /\ exists ff_q_pvs_grid_input_tableentrynegative. dst_negative_code_grid_input_table = ff_q_pvs_grid_input_tableentrynegative * S ((S (dst_index_grid_input_table)) * dst_negative_scale_grid_input_table) + (dst_negative_grid_input_table))) /\ (exists ge_balance_positive_grid_input_tableentryvalue ge_balance_negative_grid_input_tableentryvalue. (((((dst_value_grid_input_table) = 2 * (ge_balance_positive_grid_input_tableentryvalue) /\ (ge_balance_negative_grid_input_tableentryvalue) = 0) \/ exists ge_signed_half_grid_input_tableentryvaluedecode. (((dst_value_grid_input_table) = 2 * ge_signed_half_grid_input_tableentryvaluedecode + 1 /\ (ge_balance_positive_grid_input_tableentryvalue) = 0) /\ (ge_balance_negative_grid_input_tableentryvalue) = S ge_signed_half_grid_input_tableentryvaluedecode))) /\ ((dst_positive_grid_input_table) + ge_balance_negative_grid_input_tableentryvalue = (dst_negative_grid_input_table) + ge_balance_positive_grid_input_tableentryvalue))))))))) -> (((exists dst_positive_code_grid_input_prefixtable dst_positive_scale_grid_input_prefixtable dst_negative_code_grid_input_prefixtable dst_negative_scale_grid_input_prefixtable. (((T) = (((((dst_positive_code_grid_input_prefixtable) + (dst_positive_scale_grid_input_prefixtable)) * S ((dst_positive_code_grid_input_prefixtable) + (dst_positive_scale_grid_input_prefixtable)) + ((dst_positive_scale_grid_input_prefixtable) + (dst_positive_scale_grid_input_prefixtable))) + (((dst_negative_code_grid_input_prefixtable) + (dst_negative_scale_grid_input_prefixtable)) * S ((dst_negative_code_grid_input_prefixtable) + (dst_negative_scale_grid_input_prefixtable)) + ((dst_negative_scale_grid_input_prefixtable) + (dst_negative_scale_grid_input_prefixtable)))) * S ((((dst_positive_code_grid_input_prefixtable) + (dst_positive_scale_grid_input_prefixtable)) * S ((dst_positive_code_grid_input_prefixtable) + (dst_positive_scale_grid_input_prefixtable)) + ((dst_positive_scale_grid_input_prefixtable) + (dst_positive_scale_grid_input_prefixtable))) + (((dst_negative_code_grid_input_prefixtable) + (dst_negative_scale_grid_input_prefixtable)) * S ((dst_negative_code_grid_input_prefixtable) + (dst_negative_scale_grid_input_prefixtable)) + ((dst_negative_scale_grid_input_prefixtable) + (dst_negative_scale_grid_input_prefixtable)))) + ((((dst_negative_code_grid_input_prefixtable) + (dst_negative_scale_grid_input_prefixtable)) * S ((dst_negative_code_grid_input_prefixtable) + (dst_negative_scale_grid_input_prefixtable)) + ((dst_negative_scale_grid_input_prefixtable) + (dst_negative_scale_grid_input_prefixtable))) + (((dst_negative_code_grid_input_prefixtable) + (dst_negative_scale_grid_input_prefixtable)) * S ((dst_negative_code_grid_input_prefixtable) + (dst_negative_scale_grid_input_prefixtable)) + ((dst_negative_scale_grid_input_prefixtable) + (dst_negative_scale_grid_input_prefixtable)))))) /\ (forall dst_index_grid_input_prefixtable. (exists pvs_le_gap_grid_input_prefixtabledomain. pvs_le_gap_grid_input_prefixtabledomain + (dst_index_grid_input_prefixtable) = (L*(S M))) -> exists dst_positive_grid_input_prefixtable dst_negative_grid_input_prefixtable dst_value_grid_input_prefixtable. ((((exists ff_h_pvs_grid_input_prefixtableentrypositive. ff_h_pvs_grid_input_prefixtableentrypositive + S (dst_positive_grid_input_prefixtable) = S ((S (dst_index_grid_input_prefixtable)) * dst_positive_scale_grid_input_prefixtable)) /\ exists ff_q_pvs_grid_input_prefixtableentrypositive. dst_positive_code_grid_input_prefixtable = ff_q_pvs_grid_input_prefixtableentrypositive * S ((S (dst_index_grid_input_prefixtable)) * dst_positive_scale_grid_input_prefixtable) + (dst_positive_grid_input_prefixtable))) /\ (((((exists ff_h_pvs_grid_input_prefixtableentrynegative. ff_h_pvs_grid_input_prefixtableentrynegative + S (dst_negative_grid_input_prefixtable) = S ((S (dst_index_grid_input_prefixtable)) * dst_negative_scale_grid_input_prefixtable)) /\ exists ff_q_pvs_grid_input_prefixtableentrynegative. dst_negative_code_grid_input_prefixtable = ff_q_pvs_grid_input_prefixtableentrynegative * S ((S (dst_index_grid_input_prefixtable)) * dst_negative_scale_grid_input_prefixtable) + (dst_negative_grid_input_prefixtable))) /\ (exists ge_balance_positive_grid_input_prefixtableentryvalue ge_balance_negative_grid_input_prefixtableentryvalue. (((((dst_value_grid_input_prefixtable) = 2 * (ge_balance_positive_grid_input_prefixtableentryvalue) /\ (ge_balance_negative_grid_input_prefixtableentryvalue) = 0) \/ exists ge_signed_half_grid_input_prefixtableentryvaluedecode. (((dst_value_grid_input_prefixtable) = 2 * ge_signed_half_grid_input_prefixtableentryvaluedecode + 1 /\ (ge_balance_positive_grid_input_prefixtableentryvalue) = 0) /\ (ge_balance_negative_grid_input_prefixtableentryvalue) = S ge_signed_half_grid_input_prefixtableentryvaluedecode))) /\ ((dst_positive_grid_input_prefixtable) + ge_balance_negative_grid_input_prefixtableentryvalue = (dst_negative_grid_input_prefixtable) + ge_balance_positive_grid_input_prefixtableentryvalue))))))))) /\ (forall ssr_prefix_index_grid_input_prefix ssr_prefix_value_grid_input_prefix. (exists pvs_le_gap_grid_input_prefixbound. pvs_le_gap_grid_input_prefixbound + (ssr_prefix_index_grid_input_prefix) = (L*(S M))) -> (exists dst_positive_code_grid_input_prefixlookup dst_positive_scale_grid_input_prefixlookup dst_negative_code_grid_input_prefixlookup dst_negative_scale_grid_input_prefixlookup dst_positive_grid_input_prefixlookup dst_negative_grid_input_prefixlookup. (((T) = (((((dst_positive_code_grid_input_prefixlookup) + (dst_positive_scale_grid_input_prefixlookup)) * S ((dst_positive_code_grid_input_prefixlookup) + (dst_positive_scale_grid_input_prefixlookup)) + ((dst_positive_scale_grid_input_prefixlookup) + (dst_positive_scale_grid_input_prefixlookup))) + (((dst_negative_code_grid_input_prefixlookup) + (dst_negative_scale_grid_input_prefixlookup)) * S ((dst_negative_code_grid_input_prefixlookup) + (dst_negative_scale_grid_input_prefixlookup)) + ((dst_negative_scale_grid_input_prefixlookup) + (dst_negative_scale_grid_input_prefixlookup)))) * S ((((dst_positive_code_grid_input_prefixlookup) + (dst_positive_scale_grid_input_prefixlookup)) * S ((dst_positive_code_grid_input_prefixlookup) + (dst_positive_scale_grid_input_prefixlookup)) + ((dst_positive_scale_grid_input_prefixlookup) + (dst_positive_scale_grid_input_prefixlookup))) + (((dst_negative_code_grid_input_prefixlookup) + (dst_negative_scale_grid_input_prefixlookup)) * S ((dst_negative_code_grid_input_prefixlookup) + (dst_negative_scale_grid_input_prefixlookup)) + ((dst_negative_scale_grid_input_prefixlookup) + (dst_negative_scale_grid_input_prefixlookup)))) + ((((dst_negative_code_grid_input_prefixlookup) + (dst_negative_scale_grid_input_prefixlookup)) * S ((dst_negative_code_grid_input_prefixlookup) + (dst_negative_scale_grid_input_prefixlookup)) + ((dst_negative_scale_grid_input_prefixlookup) + (dst_negative_scale_grid_input_prefixlookup))) + (((dst_negative_code_grid_input_prefixlookup) + (dst_negative_scale_grid_input_prefixlookup)) * S ((dst_negative_code_grid_input_prefixlookup) + (dst_negative_scale_grid_input_prefixlookup)) + ((dst_negative_scale_grid_input_prefixlookup) + (dst_negative_scale_grid_input_prefixlookup)))))) /\ (((((exists ff_h_pvs_grid_input_prefixlookuppositive. ff_h_pvs_grid_input_prefixlookuppositive + S (dst_positive_grid_input_prefixlookup) = S ((S (ssr_prefix_index_grid_input_prefix)) * dst_positive_scale_grid_input_prefixlookup)) /\ exists ff_q_pvs_grid_input_prefixlookuppositive. dst_positive_code_grid_input_prefixlookup = ff_q_pvs_grid_input_prefixlookuppositive * S ((S (ssr_prefix_index_grid_input_prefix)) * dst_positive_scale_grid_input_prefixlookup) + (dst_positive_grid_input_prefixlookup))) /\ (((((exists ff_h_pvs_grid_input_prefixlookupnegative. ff_h_pvs_grid_input_prefixlookupnegative + S (dst_negative_grid_input_prefixlookup) = S ((S (ssr_prefix_index_grid_input_prefix)) * dst_negative_scale_grid_input_prefixlookup)) /\ exists ff_q_pvs_grid_input_prefixlookupnegative. dst_negative_code_grid_input_prefixlookup = ff_q_pvs_grid_input_prefixlookupnegative * S ((S (ssr_prefix_index_grid_input_prefix)) * dst_negative_scale_grid_input_prefixlookup) + (dst_negative_grid_input_prefixlookup))) /\ (exists ge_balance_positive_grid_input_prefixlookupvalue ge_balance_negative_grid_input_prefixlookupvalue. (((((ssr_prefix_value_grid_input_prefix) = 2 * (ge_balance_positive_grid_input_prefixlookupvalue) /\ (ge_balance_negative_grid_input_prefixlookupvalue) = 0) \/ exists ge_signed_half_grid_input_prefixlookupvaluedecode. (((ssr_prefix_value_grid_input_prefix) = 2 * ge_signed_half_grid_input_prefixlookupvaluedecode + 1 /\ (ge_balance_positive_grid_input_prefixlookupvalue) = 0) /\ (ge_balance_negative_grid_input_prefixlookupvalue) = S ge_signed_half_grid_input_prefixlookupvaluedecode))) /\ ((dst_positive_grid_input_prefixlookup) + ge_balance_negative_grid_input_prefixlookupvalue = (dst_negative_grid_input_prefixlookup) + ge_balance_positive_grid_input_prefixlookupvalue))))))))) -> (exists ssr_flat_row_grid_input_prefixentry ssr_flat_column_grid_input_prefixentry. (((ssr_prefix_index_grid_input_prefix)=(((S (M))*(ssr_flat_row_grid_input_prefixentry)+(ssr_flat_column_grid_input_prefixentry)))) /\ (((exists pvs_gap_grid_input_prefixentryremainder. pvs_gap_grid_input_prefixentryremainder + S (ssr_flat_column_grid_input_prefixentry) = (S (M))) /\ (exists ssr_entry_value_grid_input_prefixentryentry ssr_entry_image_grid_input_prefixentryentry. ((exists dst_positive_code_grid_input_prefixentryentrysource dst_positive_scale_grid_input_prefixentryentrysource dst_negative_code_grid_input_prefixentryentrysource dst_negative_scale_grid_input_prefixentryentrysource dst_positive_grid_input_prefixentryentrysource dst_negative_grid_input_prefixentryentrysource. (((A) = (((((dst_positive_code_grid_input_prefixentryentrysource) + (dst_positive_scale_grid_input_prefixentryentrysource)) * S ((dst_positive_code_grid_input_prefixentryentrysource) + (dst_positive_scale_grid_input_prefixentryentrysource)) + ((dst_positive_scale_grid_input_prefixentryentrysource) + (dst_positive_scale_grid_input_prefixentryentrysource))) + (((dst_negative_code_grid_input_prefixentryentrysource) + (dst_negative_scale_grid_input_prefixentryentrysource)) * S ((dst_negative_code_grid_input_prefixentryentrysource) + (dst_negative_scale_grid_input_prefixentryentrysource)) + ((dst_negative_scale_grid_input_prefixentryentrysource) + (dst_negative_scale_grid_input_prefixentryentrysource)))) * S ((((dst_positive_code_grid_input_prefixentryentrysource) + (dst_positive_scale_grid_input_prefixentryentrysource)) * S ((dst_positive_code_grid_input_prefixentryentrysource) + (dst_positive_scale_grid_input_prefixentryentrysource)) + ((dst_positive_scale_grid_input_prefixentryentrysource) + (dst_positive_scale_grid_input_prefixentryentrysource))) + (((dst_negative_code_grid_input_prefixentryentrysource) + (dst_negative_scale_grid_input_prefixentryentrysource)) * S ((dst_negative_code_grid_input_prefixentryentrysource) + (dst_negative_scale_grid_input_prefixentryentrysource)) + ((dst_negative_scale_grid_input_prefixentryentrysource) + (dst_negative_scale_grid_input_prefixentryentrysource)))) + ((((dst_negative_code_grid_input_prefixentryentrysource) + (dst_negative_scale_grid_input_prefixentryentrysource)) * S ((dst_negative_code_grid_input_prefixentryentrysource) + (dst_negative_scale_grid_input_prefixentryentrysource)) + ((dst_negative_scale_grid_input_prefixentryentrysource) + (dst_negative_scale_grid_input_prefixentryentrysource))) + (((dst_negative_code_grid_input_prefixentryentrysource) + (dst_negative_scale_grid_input_prefixentryentrysource)) * S ((dst_negative_code_grid_input_prefixentryentrysource) + (dst_negative_scale_grid_input_prefixentryentrysource)) + ((dst_negative_scale_grid_input_prefixentryentrysource) + (dst_negative_scale_grid_input_prefixentryentrysource)))))) /\ (((((exists ff_h_pvs_grid_input_prefixentryentrysourcepositive. ff_h_pvs_grid_input_prefixentryentrysourcepositive + S (dst_positive_grid_input_prefixentryentrysource) = S ((S (ssr_flat_row_grid_input_prefixentry)) * dst_positive_scale_grid_input_prefixentryentrysource)) /\ exists ff_q_pvs_grid_input_prefixentryentrysourcepositive. dst_positive_code_grid_input_prefixentryentrysource = ff_q_pvs_grid_input_prefixentryentrysourcepositive * S ((S (ssr_flat_row_grid_input_prefixentry)) * dst_positive_scale_grid_input_prefixentryentrysource) + (dst_positive_grid_input_prefixentryentrysource))) /\ (((((exists ff_h_pvs_grid_input_prefixentryentrysourcenegative. ff_h_pvs_grid_input_prefixentryentrysourcenegative + S (dst_negative_grid_input_prefixentryentrysource) = S ((S (ssr_flat_row_grid_input_prefixentry)) * dst_negative_scale_grid_input_prefixentryentrysource)) /\ exists ff_q_pvs_grid_input_prefixentryentrysourcenegative. dst_negative_code_grid_input_prefixentryentrysource = ff_q_pvs_grid_input_prefixentryentrysourcenegative * S ((S (ssr_flat_row_grid_input_prefixentry)) * dst_negative_scale_grid_input_prefixentryentrysource) + (dst_negative_grid_input_prefixentryentrysource))) /\ (exists ge_balance_positive_grid_input_prefixentryentrysourcevalue ge_balance_negative_grid_input_prefixentryentrysourcevalue. (((((ssr_entry_value_grid_input_prefixentryentry) = 2 * (ge_balance_positive_grid_input_prefixentryentrysourcevalue) /\ (ge_balance_negative_grid_input_prefixentryentrysourcevalue) = 0) \/ exists ge_signed_half_grid_input_prefixentryentrysourcevaluedecode. (((ssr_entry_value_grid_input_prefixentryentry) = 2 * ge_signed_half_grid_input_prefixentryentrysourcevaluedecode + 1 /\ (ge_balance_positive_grid_input_prefixentryentrysourcevalue) = 0) /\ (ge_balance_negative_grid_input_prefixentryentrysourcevalue) = S ge_signed_half_grid_input_prefixentryentrysourcevaluedecode))) /\ ((dst_positive_grid_input_prefixentryentrysource) + ge_balance_negative_grid_input_prefixentryentrysourcevalue = (dst_negative_grid_input_prefixentryentrysource) + ge_balance_positive_grid_input_prefixentryentrysourcevalue))))))))) /\ (((((exists ff_h_pvs_grid_input_prefixentryentrymap. ff_h_pvs_grid_input_prefixentryentrymap + S (ssr_entry_image_grid_input_prefixentryentry) = S ((S (ssr_flat_row_grid_input_prefixentry)) * s)) /\ exists ff_q_pvs_grid_input_prefixentryentrymap. r = ff_q_pvs_grid_input_prefixentryentrymap * S ((S (ssr_flat_row_grid_input_prefixentry)) * s) + (ssr_entry_image_grid_input_prefixentryentry))) /\ (((((ssr_flat_column_grid_input_prefixentry)=(ssr_entry_image_grid_input_prefixentryentry)) /\ ((ssr_prefix_value_grid_input_prefix)=(ssr_entry_value_grid_input_prefixentryentry)))) \/ (((~((ssr_flat_column_grid_input_prefixentry)=(ssr_entry_image_grid_input_prefixentryentry))) /\ ((ssr_prefix_value_grid_input_prefix)=0))))))))))))))) -> (((exists dst_positive_code_grid_outputsource dst_positive_scale_grid_outputsource dst_negative_code_grid_outputsource dst_negative_scale_grid_outputsource. (((A) = (((((dst_positive_code_grid_outputsource) + (dst_positive_scale_grid_outputsource)) * S ((dst_positive_code_grid_outputsource) + (dst_positive_scale_grid_outputsource)) + ((dst_positive_scale_grid_outputsource) + (dst_positive_scale_grid_outputsource))) + (((dst_negative_code_grid_outputsource) + (dst_negative_scale_grid_outputsource)) * S ((dst_negative_code_grid_outputsource) + (dst_negative_scale_grid_outputsource)) + ((dst_negative_scale_grid_outputsource) + (dst_negative_scale_grid_outputsource)))) * S ((((dst_positive_code_grid_outputsource) + (dst_positive_scale_grid_outputsource)) * S ((dst_positive_code_grid_outputsource) + (dst_positive_scale_grid_outputsource)) + ((dst_positive_scale_grid_outputsource) + (dst_positive_scale_grid_outputsource))) + (((dst_negative_code_grid_outputsource) + (dst_negative_scale_grid_outputsource)) * S ((dst_negative_code_grid_outputsource) + (dst_negative_scale_grid_outputsource)) + ((dst_negative_scale_grid_outputsource) + (dst_negative_scale_grid_outputsource)))) + ((((dst_negative_code_grid_outputsource) + (dst_negative_scale_grid_outputsource)) * S ((dst_negative_code_grid_outputsource) + (dst_negative_scale_grid_outputsource)) + ((dst_negative_scale_grid_outputsource) + (dst_negative_scale_grid_outputsource))) + (((dst_negative_code_grid_outputsource) + (dst_negative_scale_grid_outputsource)) * S ((dst_negative_code_grid_outputsource) + (dst_negative_scale_grid_outputsource)) + ((dst_negative_scale_grid_outputsource) + (dst_negative_scale_grid_outputsource)))))) /\ (forall dst_index_grid_outputsource. (exists pvs_le_gap_grid_outputsourcedomain. pvs_le_gap_grid_outputsourcedomain + (dst_index_grid_outputsource) = (0)) -> exists dst_positive_grid_outputsource dst_negative_grid_outputsource dst_value_grid_outputsource. ((((exists ff_h_pvs_grid_outputsourceentrypositive. ff_h_pvs_grid_outputsourceentrypositive + S (dst_positive_grid_outputsource) = S ((S (dst_index_grid_outputsource)) * dst_positive_scale_grid_outputsource)) /\ exists ff_q_pvs_grid_outputsourceentrypositive. dst_positive_code_grid_outputsource = ff_q_pvs_grid_outputsourceentrypositive * S ((S (dst_index_grid_outputsource)) * dst_positive_scale_grid_outputsource) + (dst_positive_grid_outputsource))) /\ (((((exists ff_h_pvs_grid_outputsourceentrynegative. ff_h_pvs_grid_outputsourceentrynegative + S (dst_negative_grid_outputsource) = S ((S (dst_index_grid_outputsource)) * dst_negative_scale_grid_outputsource)) /\ exists ff_q_pvs_grid_outputsourceentrynegative. dst_negative_code_grid_outputsource = ff_q_pvs_grid_outputsourceentrynegative * S ((S (dst_index_grid_outputsource)) * dst_negative_scale_grid_outputsource) + (dst_negative_grid_outputsource))) /\ (exists ge_balance_positive_grid_outputsourceentryvalue ge_balance_negative_grid_outputsourceentryvalue. (((((dst_value_grid_outputsource) = 2 * (ge_balance_positive_grid_outputsourceentryvalue) /\ (ge_balance_negative_grid_outputsourceentryvalue) = 0) \/ exists ge_signed_half_grid_outputsourceentryvaluedecode. (((dst_value_grid_outputsource) = 2 * ge_signed_half_grid_outputsourceentryvaluedecode + 1 /\ (ge_balance_positive_grid_outputsourceentryvalue) = 0) /\ (ge_balance_negative_grid_outputsourceentryvalue) = S ge_signed_half_grid_outputsourceentryvaluedecode))) /\ ((dst_positive_grid_outputsource) + ge_balance_negative_grid_outputsourceentryvalue = (dst_negative_grid_outputsource) + ge_balance_positive_grid_outputsourceentryvalue))))))))) /\ (((exists dst_positive_code_grid_outputtable dst_positive_scale_grid_outputtable dst_negative_code_grid_outputtable dst_negative_scale_grid_outputtable. (((T) = (((((dst_positive_code_grid_outputtable) + (dst_positive_scale_grid_outputtable)) * S ((dst_positive_code_grid_outputtable) + (dst_positive_scale_grid_outputtable)) + ((dst_positive_scale_grid_outputtable) + (dst_positive_scale_grid_outputtable))) + (((dst_negative_code_grid_outputtable) + (dst_negative_scale_grid_outputtable)) * S ((dst_negative_code_grid_outputtable) + (dst_negative_scale_grid_outputtable)) + ((dst_negative_scale_grid_outputtable) + (dst_negative_scale_grid_outputtable)))) * S ((((dst_positive_code_grid_outputtable) + (dst_positive_scale_grid_outputtable)) * S ((dst_positive_code_grid_outputtable) + (dst_positive_scale_grid_outputtable)) + ((dst_positive_scale_grid_outputtable) + (dst_positive_scale_grid_outputtable))) + (((dst_negative_code_grid_outputtable) + (dst_negative_scale_grid_outputtable)) * S ((dst_negative_code_grid_outputtable) + (dst_negative_scale_grid_outputtable)) + ((dst_negative_scale_grid_outputtable) + (dst_negative_scale_grid_outputtable)))) + ((((dst_negative_code_grid_outputtable) + (dst_negative_scale_grid_outputtable)) * S ((dst_negative_code_grid_outputtable) + (dst_negative_scale_grid_outputtable)) + ((dst_negative_scale_grid_outputtable) + (dst_negative_scale_grid_outputtable))) + (((dst_negative_code_grid_outputtable) + (dst_negative_scale_grid_outputtable)) * S ((dst_negative_code_grid_outputtable) + (dst_negative_scale_grid_outputtable)) + ((dst_negative_scale_grid_outputtable) + (dst_negative_scale_grid_outputtable)))))) /\ (forall dst_index_grid_outputtable. (exists pvs_le_gap_grid_outputtabledomain. pvs_le_gap_grid_outputtabledomain + (dst_index_grid_outputtable) = ((L)*(S (M)))) -> exists dst_positive_grid_outputtable dst_negative_grid_outputtable dst_value_grid_outputtable. ((((exists ff_h_pvs_grid_outputtableentrypositive. ff_h_pvs_grid_outputtableentrypositive + S (dst_positive_grid_outputtable) = S ((S (dst_index_grid_outputtable)) * dst_positive_scale_grid_outputtable)) /\ exists ff_q_pvs_grid_outputtableentrypositive. dst_positive_code_grid_outputtable = ff_q_pvs_grid_outputtableentrypositive * S ((S (dst_index_grid_outputtable)) * dst_positive_scale_grid_outputtable) + (dst_positive_grid_outputtable))) /\ (((((exists ff_h_pvs_grid_outputtableentrynegative. ff_h_pvs_grid_outputtableentrynegative + S (dst_negative_grid_outputtable) = S ((S (dst_index_grid_outputtable)) * dst_negative_scale_grid_outputtable)) /\ exists ff_q_pvs_grid_outputtableentrynegative. dst_negative_code_grid_outputtable = ff_q_pvs_grid_outputtableentrynegative * S ((S (dst_index_grid_outputtable)) * dst_negative_scale_grid_outputtable) + (dst_negative_grid_outputtable))) /\ (exists ge_balance_positive_grid_outputtableentryvalue ge_balance_negative_grid_outputtableentryvalue. (((((dst_value_grid_outputtable) = 2 * (ge_balance_positive_grid_outputtableentryvalue) /\ (ge_balance_negative_grid_outputtableentryvalue) = 0) \/ exists ge_signed_half_grid_outputtableentryvaluedecode. (((dst_value_grid_outputtable) = 2 * ge_signed_half_grid_outputtableentryvaluedecode + 1 /\ (ge_balance_positive_grid_outputtableentryvalue) = 0) /\ (ge_balance_negative_grid_outputtableentryvalue) = S ge_signed_half_grid_outputtableentryvaluedecode))) /\ ((dst_positive_grid_outputtable) + ge_balance_negative_grid_outputtableentryvalue = (dst_negative_grid_outputtable) + ge_balance_positive_grid_outputtableentryvalue))))))))) /\ (forall ssr_grid_row_grid_output ssr_grid_column_grid_output ssr_grid_value_grid_output. (exists pvs_gap_grid_outputrow_bound. pvs_gap_grid_outputrow_bound + S (ssr_grid_row_grid_output) = (L)) -> (exists pvs_gap_grid_outputcolumn_bound. pvs_gap_grid_outputcolumn_bound + S (ssr_grid_column_grid_output) = (M)) -> (exists dst_positive_code_grid_outputlookup dst_positive_scale_grid_outputlookup dst_negative_code_grid_outputlookup dst_negative_scale_grid_outputlookup dst_positive_grid_outputlookup dst_negative_grid_outputlookup. (((T) = (((((dst_positive_code_grid_outputlookup) + (dst_positive_scale_grid_outputlookup)) * S ((dst_positive_code_grid_outputlookup) + (dst_positive_scale_grid_outputlookup)) + ((dst_positive_scale_grid_outputlookup) + (dst_positive_scale_grid_outputlookup))) + (((dst_negative_code_grid_outputlookup) + (dst_negative_scale_grid_outputlookup)) * S ((dst_negative_code_grid_outputlookup) + (dst_negative_scale_grid_outputlookup)) + ((dst_negative_scale_grid_outputlookup) + (dst_negative_scale_grid_outputlookup)))) * S ((((dst_positive_code_grid_outputlookup) + (dst_positive_scale_grid_outputlookup)) * S ((dst_positive_code_grid_outputlookup) + (dst_positive_scale_grid_outputlookup)) + ((dst_positive_scale_grid_outputlookup) + (dst_positive_scale_grid_outputlookup))) + (((dst_negative_code_grid_outputlookup) + (dst_negative_scale_grid_outputlookup)) * S ((dst_negative_code_grid_outputlookup) + (dst_negative_scale_grid_outputlookup)) + ((dst_negative_scale_grid_outputlookup) + (dst_negative_scale_grid_outputlookup)))) + ((((dst_negative_code_grid_outputlookup) + (dst_negative_scale_grid_outputlookup)) * S ((dst_negative_code_grid_outputlookup) + (dst_negative_scale_grid_outputlookup)) + ((dst_negative_scale_grid_outputlookup) + (dst_negative_scale_grid_outputlookup))) + (((dst_negative_code_grid_outputlookup) + (dst_negative_scale_grid_outputlookup)) * S ((dst_negative_code_grid_outputlookup) + (dst_negative_scale_grid_outputlookup)) + ((dst_negative_scale_grid_outputlookup) + (dst_negative_scale_grid_outputlookup)))))) /\ (((((exists ff_h_pvs_grid_outputlookuppositive. ff_h_pvs_grid_outputlookuppositive + S (dst_positive_grid_outputlookup) = S ((S (((S (M))*(ssr_grid_row_grid_output)+(ssr_grid_column_grid_output)))) * dst_positive_scale_grid_outputlookup)) /\ exists ff_q_pvs_grid_outputlookuppositive. dst_positive_code_grid_outputlookup = ff_q_pvs_grid_outputlookuppositive * S ((S (((S (M))*(ssr_grid_row_grid_output)+(ssr_grid_column_grid_output)))) * dst_positive_scale_grid_outputlookup) + (dst_positive_grid_outputlookup))) /\ (((((exists ff_h_pvs_grid_outputlookupnegative. ff_h_pvs_grid_outputlookupnegative + S (dst_negative_grid_outputlookup) = S ((S (((S (M))*(ssr_grid_row_grid_output)+(ssr_grid_column_grid_output)))) * dst_negative_scale_grid_outputlookup)) /\ exists ff_q_pvs_grid_outputlookupnegative. dst_negative_code_grid_outputlookup = ff_q_pvs_grid_outputlookupnegative * S ((S (((S (M))*(ssr_grid_row_grid_output)+(ssr_grid_column_grid_output)))) * dst_negative_scale_grid_outputlookup) + (dst_negative_grid_outputlookup))) /\ (exists ge_balance_positive_grid_outputlookupvalue ge_balance_negative_grid_outputlookupvalue. (((((ssr_grid_value_grid_output) = 2 * (ge_balance_positive_grid_outputlookupvalue) /\ (ge_balance_negative_grid_outputlookupvalue) = 0) \/ exists ge_signed_half_grid_outputlookupvaluedecode. (((ssr_grid_value_grid_output) = 2 * ge_signed_half_grid_outputlookupvaluedecode + 1 /\ (ge_balance_positive_grid_outputlookupvalue) = 0) /\ (ge_balance_negative_grid_outputlookupvalue) = S ge_signed_half_grid_outputlookupvaluedecode))) /\ ((dst_positive_grid_outputlookup) + ge_balance_negative_grid_outputlookupvalue = (dst_negative_grid_outputlookup) + ge_balance_positive_grid_outputlookupvalue))))))))) -> (exists ssr_entry_value_grid_outputentry ssr_entry_image_grid_outputentry. ((exists dst_positive_code_grid_outputentrysource dst_positive_scale_grid_outputentrysource dst_negative_code_grid_outputentrysource dst_negative_scale_grid_outputentrysource dst_positive_grid_outputentrysource dst_negative_grid_outputentrysource. (((A) = (((((dst_positive_code_grid_outputentrysource) + (dst_positive_scale_grid_outputentrysource)) * S ((dst_positive_code_grid_outputentrysource) + (dst_positive_scale_grid_outputentrysource)) + ((dst_positive_scale_grid_outputentrysource) + (dst_positive_scale_grid_outputentrysource))) + (((dst_negative_code_grid_outputentrysource) + (dst_negative_scale_grid_outputentrysource)) * S ((dst_negative_code_grid_outputentrysource) + (dst_negative_scale_grid_outputentrysource)) + ((dst_negative_scale_grid_outputentrysource) + (dst_negative_scale_grid_outputentrysource)))) * S ((((dst_positive_code_grid_outputentrysource) + (dst_positive_scale_grid_outputentrysource)) * S ((dst_positive_code_grid_outputentrysource) + (dst_positive_scale_grid_outputentrysource)) + ((dst_positive_scale_grid_outputentrysource) + (dst_positive_scale_grid_outputentrysource))) + (((dst_negative_code_grid_outputentrysource) + (dst_negative_scale_grid_outputentrysource)) * S ((dst_negative_code_grid_outputentrysource) + (dst_negative_scale_grid_outputentrysource)) + ((dst_negative_scale_grid_outputentrysource) + (dst_negative_scale_grid_outputentrysource)))) + ((((dst_negative_code_grid_outputentrysource) + (dst_negative_scale_grid_outputentrysource)) * S ((dst_negative_code_grid_outputentrysource) + (dst_negative_scale_grid_outputentrysource)) + ((dst_negative_scale_grid_outputentrysource) + (dst_negative_scale_grid_outputentrysource))) + (((dst_negative_code_grid_outputentrysource) + (dst_negative_scale_grid_outputentrysource)) * S ((dst_negative_code_grid_outputentrysource) + (dst_negative_scale_grid_outputentrysource)) + ((dst_negative_scale_grid_outputentrysource) + (dst_negative_scale_grid_outputentrysource)))))) /\ (((((exists ff_h_pvs_grid_outputentrysourcepositive. ff_h_pvs_grid_outputentrysourcepositive + S (dst_positive_grid_outputentrysource) = S ((S (ssr_grid_row_grid_output)) * dst_positive_scale_grid_outputentrysource)) /\ exists ff_q_pvs_grid_outputentrysourcepositive. dst_positive_code_grid_outputentrysource = ff_q_pvs_grid_outputentrysourcepositive * S ((S (ssr_grid_row_grid_output)) * dst_positive_scale_grid_outputentrysource) + (dst_positive_grid_outputentrysource))) /\ (((((exists ff_h_pvs_grid_outputentrysourcenegative. ff_h_pvs_grid_outputentrysourcenegative + S (dst_negative_grid_outputentrysource) = S ((S (ssr_grid_row_grid_output)) * dst_negative_scale_grid_outputentrysource)) /\ exists ff_q_pvs_grid_outputentrysourcenegative. dst_negative_code_grid_outputentrysource = ff_q_pvs_grid_outputentrysourcenegative * S ((S (ssr_grid_row_grid_output)) * dst_negative_scale_grid_outputentrysource) + (dst_negative_grid_outputentrysource))) /\ (exists ge_balance_positive_grid_outputentrysourcevalue ge_balance_negative_grid_outputentrysourcevalue. (((((ssr_entry_value_grid_outputentry) = 2 * (ge_balance_positive_grid_outputentrysourcevalue) /\ (ge_balance_negative_grid_outputentrysourcevalue) = 0) \/ exists ge_signed_half_grid_outputentrysourcevaluedecode. (((ssr_entry_value_grid_outputentry) = 2 * ge_signed_half_grid_outputentrysourcevaluedecode + 1 /\ (ge_balance_positive_grid_outputentrysourcevalue) = 0) /\ (ge_balance_negative_grid_outputentrysourcevalue) = S ge_signed_half_grid_outputentrysourcevaluedecode))) /\ ((dst_positive_grid_outputentrysource) + ge_balance_negative_grid_outputentrysourcevalue = (dst_negative_grid_outputentrysource) + ge_balance_positive_grid_outputentrysourcevalue))))))))) /\ (((((exists ff_h_pvs_grid_outputentrymap. ff_h_pvs_grid_outputentrymap + S (ssr_entry_image_grid_outputentry) = S ((S (ssr_grid_row_grid_output)) * s)) /\ exists ff_q_pvs_grid_outputentrymap. r = ff_q_pvs_grid_outputentrymap * S ((S (ssr_grid_row_grid_output)) * s) + (ssr_entry_image_grid_outputentry))) /\ (((((ssr_grid_column_grid_output)=(ssr_entry_image_grid_outputentry)) /\ ((ssr_grid_value_grid_output)=(ssr_entry_value_grid_outputentry)))) \/ (((~((ssr_grid_column_grid_output)=(ssr_entry_image_grid_outputentry))) /\ ((ssr_grid_value_grid_output)=0)))))))))))))