signed_support_incidence_flat_prefix_zero

Exact expanded first-order arithmetic statement

forall A r s M T z. (exists dst_positive_code_prefix_zero_table dst_positive_scale_prefix_zero_table dst_negative_code_prefix_zero_table dst_negative_scale_prefix_zero_table. (((T) = (((((dst_positive_code_prefix_zero_table) + (dst_positive_scale_prefix_zero_table)) * S ((dst_positive_code_prefix_zero_table) + (dst_positive_scale_prefix_zero_table)) + ((dst_positive_scale_prefix_zero_table) + (dst_positive_scale_prefix_zero_table))) + (((dst_negative_code_prefix_zero_table) + (dst_negative_scale_prefix_zero_table)) * S ((dst_negative_code_prefix_zero_table) + (dst_negative_scale_prefix_zero_table)) + ((dst_negative_scale_prefix_zero_table) + (dst_negative_scale_prefix_zero_table)))) * S ((((dst_positive_code_prefix_zero_table) + (dst_positive_scale_prefix_zero_table)) * S ((dst_positive_code_prefix_zero_table) + (dst_positive_scale_prefix_zero_table)) + ((dst_positive_scale_prefix_zero_table) + (dst_positive_scale_prefix_zero_table))) + (((dst_negative_code_prefix_zero_table) + (dst_negative_scale_prefix_zero_table)) * S ((dst_negative_code_prefix_zero_table) + (dst_negative_scale_prefix_zero_table)) + ((dst_negative_scale_prefix_zero_table) + (dst_negative_scale_prefix_zero_table)))) + ((((dst_negative_code_prefix_zero_table) + (dst_negative_scale_prefix_zero_table)) * S ((dst_negative_code_prefix_zero_table) + (dst_negative_scale_prefix_zero_table)) + ((dst_negative_scale_prefix_zero_table) + (dst_negative_scale_prefix_zero_table))) + (((dst_negative_code_prefix_zero_table) + (dst_negative_scale_prefix_zero_table)) * S ((dst_negative_code_prefix_zero_table) + (dst_negative_scale_prefix_zero_table)) + ((dst_negative_scale_prefix_zero_table) + (dst_negative_scale_prefix_zero_table)))))) /\ (forall dst_index_prefix_zero_table. (exists pvs_le_gap_prefix_zero_tabledomain. pvs_le_gap_prefix_zero_tabledomain + (dst_index_prefix_zero_table) = (0)) -> exists dst_positive_prefix_zero_table dst_negative_prefix_zero_table dst_value_prefix_zero_table. ((((exists ff_h_pvs_prefix_zero_tableentrypositive. ff_h_pvs_prefix_zero_tableentrypositive + S (dst_positive_prefix_zero_table) = S ((S (dst_index_prefix_zero_table)) * dst_positive_scale_prefix_zero_table)) /\ exists ff_q_pvs_prefix_zero_tableentrypositive. dst_positive_code_prefix_zero_table = ff_q_pvs_prefix_zero_tableentrypositive * S ((S (dst_index_prefix_zero_table)) * dst_positive_scale_prefix_zero_table) + (dst_positive_prefix_zero_table))) /\ (((((exists ff_h_pvs_prefix_zero_tableentrynegative. ff_h_pvs_prefix_zero_tableentrynegative + S (dst_negative_prefix_zero_table) = S ((S (dst_index_prefix_zero_table)) * dst_negative_scale_prefix_zero_table)) /\ exists ff_q_pvs_prefix_zero_tableentrynegative. dst_negative_code_prefix_zero_table = ff_q_pvs_prefix_zero_tableentrynegative * S ((S (dst_index_prefix_zero_table)) * dst_negative_scale_prefix_zero_table) + (dst_negative_prefix_zero_table))) /\ (exists ge_balance_positive_prefix_zero_tableentryvalue ge_balance_negative_prefix_zero_tableentryvalue. (((((dst_value_prefix_zero_table) = 2 * (ge_balance_positive_prefix_zero_tableentryvalue) /\ (ge_balance_negative_prefix_zero_tableentryvalue) = 0) \/ exists ge_signed_half_prefix_zero_tableentryvaluedecode. (((dst_value_prefix_zero_table) = 2 * ge_signed_half_prefix_zero_tableentryvaluedecode + 1 /\ (ge_balance_positive_prefix_zero_tableentryvalue) = 0) /\ (ge_balance_negative_prefix_zero_tableentryvalue) = S ge_signed_half_prefix_zero_tableentryvaluedecode))) /\ ((dst_positive_prefix_zero_table) + ge_balance_negative_prefix_zero_tableentryvalue = (dst_negative_prefix_zero_table) + ge_balance_positive_prefix_zero_tableentryvalue))))))))) -> (exists dst_positive_code_prefix_zero_lookup dst_positive_scale_prefix_zero_lookup dst_negative_code_prefix_zero_lookup dst_negative_scale_prefix_zero_lookup dst_positive_prefix_zero_lookup dst_negative_prefix_zero_lookup. (((T) = (((((dst_positive_code_prefix_zero_lookup) + (dst_positive_scale_prefix_zero_lookup)) * S ((dst_positive_code_prefix_zero_lookup) + (dst_positive_scale_prefix_zero_lookup)) + ((dst_positive_scale_prefix_zero_lookup) + (dst_positive_scale_prefix_zero_lookup))) + (((dst_negative_code_prefix_zero_lookup) + (dst_negative_scale_prefix_zero_lookup)) * S ((dst_negative_code_prefix_zero_lookup) + (dst_negative_scale_prefix_zero_lookup)) + ((dst_negative_scale_prefix_zero_lookup) + (dst_negative_scale_prefix_zero_lookup)))) * S ((((dst_positive_code_prefix_zero_lookup) + (dst_positive_scale_prefix_zero_lookup)) * S ((dst_positive_code_prefix_zero_lookup) + (dst_positive_scale_prefix_zero_lookup)) + ((dst_positive_scale_prefix_zero_lookup) + (dst_positive_scale_prefix_zero_lookup))) + (((dst_negative_code_prefix_zero_lookup) + (dst_negative_scale_prefix_zero_lookup)) * S ((dst_negative_code_prefix_zero_lookup) + (dst_negative_scale_prefix_zero_lookup)) + ((dst_negative_scale_prefix_zero_lookup) + (dst_negative_scale_prefix_zero_lookup)))) + ((((dst_negative_code_prefix_zero_lookup) + (dst_negative_scale_prefix_zero_lookup)) * S ((dst_negative_code_prefix_zero_lookup) + (dst_negative_scale_prefix_zero_lookup)) + ((dst_negative_scale_prefix_zero_lookup) + (dst_negative_scale_prefix_zero_lookup))) + (((dst_negative_code_prefix_zero_lookup) + (dst_negative_scale_prefix_zero_lookup)) * S ((dst_negative_code_prefix_zero_lookup) + (dst_negative_scale_prefix_zero_lookup)) + ((dst_negative_scale_prefix_zero_lookup) + (dst_negative_scale_prefix_zero_lookup)))))) /\ (((((exists ff_h_pvs_prefix_zero_lookuppositive. ff_h_pvs_prefix_zero_lookuppositive + S (dst_positive_prefix_zero_lookup) = S ((S (0)) * dst_positive_scale_prefix_zero_lookup)) /\ exists ff_q_pvs_prefix_zero_lookuppositive. dst_positive_code_prefix_zero_lookup = ff_q_pvs_prefix_zero_lookuppositive * S ((S (0)) * dst_positive_scale_prefix_zero_lookup) + (dst_positive_prefix_zero_lookup))) /\ (((((exists ff_h_pvs_prefix_zero_lookupnegative. ff_h_pvs_prefix_zero_lookupnegative + S (dst_negative_prefix_zero_lookup) = S ((S (0)) * dst_negative_scale_prefix_zero_lookup)) /\ exists ff_q_pvs_prefix_zero_lookupnegative. dst_negative_code_prefix_zero_lookup = ff_q_pvs_prefix_zero_lookupnegative * S ((S (0)) * dst_negative_scale_prefix_zero_lookup) + (dst_negative_prefix_zero_lookup))) /\ (exists ge_balance_positive_prefix_zero_lookupvalue ge_balance_negative_prefix_zero_lookupvalue. (((((z) = 2 * (ge_balance_positive_prefix_zero_lookupvalue) /\ (ge_balance_negative_prefix_zero_lookupvalue) = 0) \/ exists ge_signed_half_prefix_zero_lookupvaluedecode. (((z) = 2 * ge_signed_half_prefix_zero_lookupvaluedecode + 1 /\ (ge_balance_positive_prefix_zero_lookupvalue) = 0) /\ (ge_balance_negative_prefix_zero_lookupvalue) = S ge_signed_half_prefix_zero_lookupvaluedecode))) /\ ((dst_positive_prefix_zero_lookup) + ge_balance_negative_prefix_zero_lookupvalue = (dst_negative_prefix_zero_lookup) + ge_balance_positive_prefix_zero_lookupvalue))))))))) -> (exists ssr_flat_row_prefix_zero_value ssr_flat_column_prefix_zero_value. (((0)=(((S (M))*(ssr_flat_row_prefix_zero_value)+(ssr_flat_column_prefix_zero_value)))) /\ (((exists pvs_gap_prefix_zero_valueremainder. pvs_gap_prefix_zero_valueremainder + S (ssr_flat_column_prefix_zero_value) = (S (M))) /\ (exists ssr_entry_value_prefix_zero_valueentry ssr_entry_image_prefix_zero_valueentry. ((exists dst_positive_code_prefix_zero_valueentrysource dst_positive_scale_prefix_zero_valueentrysource dst_negative_code_prefix_zero_valueentrysource dst_negative_scale_prefix_zero_valueentrysource dst_positive_prefix_zero_valueentrysource dst_negative_prefix_zero_valueentrysource. (((A) = (((((dst_positive_code_prefix_zero_valueentrysource) + (dst_positive_scale_prefix_zero_valueentrysource)) * S ((dst_positive_code_prefix_zero_valueentrysource) + (dst_positive_scale_prefix_zero_valueentrysource)) + ((dst_positive_scale_prefix_zero_valueentrysource) + (dst_positive_scale_prefix_zero_valueentrysource))) + (((dst_negative_code_prefix_zero_valueentrysource) + (dst_negative_scale_prefix_zero_valueentrysource)) * S ((dst_negative_code_prefix_zero_valueentrysource) + (dst_negative_scale_prefix_zero_valueentrysource)) + ((dst_negative_scale_prefix_zero_valueentrysource) + (dst_negative_scale_prefix_zero_valueentrysource)))) * S ((((dst_positive_code_prefix_zero_valueentrysource) + (dst_positive_scale_prefix_zero_valueentrysource)) * S ((dst_positive_code_prefix_zero_valueentrysource) + (dst_positive_scale_prefix_zero_valueentrysource)) + ((dst_positive_scale_prefix_zero_valueentrysource) + (dst_positive_scale_prefix_zero_valueentrysource))) + (((dst_negative_code_prefix_zero_valueentrysource) + (dst_negative_scale_prefix_zero_valueentrysource)) * S ((dst_negative_code_prefix_zero_valueentrysource) + (dst_negative_scale_prefix_zero_valueentrysource)) + ((dst_negative_scale_prefix_zero_valueentrysource) + (dst_negative_scale_prefix_zero_valueentrysource)))) + ((((dst_negative_code_prefix_zero_valueentrysource) + (dst_negative_scale_prefix_zero_valueentrysource)) * S ((dst_negative_code_prefix_zero_valueentrysource) + (dst_negative_scale_prefix_zero_valueentrysource)) + ((dst_negative_scale_prefix_zero_valueentrysource) + (dst_negative_scale_prefix_zero_valueentrysource))) + (((dst_negative_code_prefix_zero_valueentrysource) + (dst_negative_scale_prefix_zero_valueentrysource)) * S ((dst_negative_code_prefix_zero_valueentrysource) + (dst_negative_scale_prefix_zero_valueentrysource)) + ((dst_negative_scale_prefix_zero_valueentrysource) + (dst_negative_scale_prefix_zero_valueentrysource)))))) /\ (((((exists ff_h_pvs_prefix_zero_valueentrysourcepositive. ff_h_pvs_prefix_zero_valueentrysourcepositive + S (dst_positive_prefix_zero_valueentrysource) = S ((S (ssr_flat_row_prefix_zero_value)) * dst_positive_scale_prefix_zero_valueentrysource)) /\ exists ff_q_pvs_prefix_zero_valueentrysourcepositive. dst_positive_code_prefix_zero_valueentrysource = ff_q_pvs_prefix_zero_valueentrysourcepositive * S ((S (ssr_flat_row_prefix_zero_value)) * dst_positive_scale_prefix_zero_valueentrysource) + (dst_positive_prefix_zero_valueentrysource))) /\ (((((exists ff_h_pvs_prefix_zero_valueentrysourcenegative. ff_h_pvs_prefix_zero_valueentrysourcenegative + S (dst_negative_prefix_zero_valueentrysource) = S ((S (ssr_flat_row_prefix_zero_value)) * dst_negative_scale_prefix_zero_valueentrysource)) /\ exists ff_q_pvs_prefix_zero_valueentrysourcenegative. dst_negative_code_prefix_zero_valueentrysource = ff_q_pvs_prefix_zero_valueentrysourcenegative * S ((S (ssr_flat_row_prefix_zero_value)) * dst_negative_scale_prefix_zero_valueentrysource) + (dst_negative_prefix_zero_valueentrysource))) /\ (exists ge_balance_positive_prefix_zero_valueentrysourcevalue ge_balance_negative_prefix_zero_valueentrysourcevalue. (((((ssr_entry_value_prefix_zero_valueentry) = 2 * (ge_balance_positive_prefix_zero_valueentrysourcevalue) /\ (ge_balance_negative_prefix_zero_valueentrysourcevalue) = 0) \/ exists ge_signed_half_prefix_zero_valueentrysourcevaluedecode. (((ssr_entry_value_prefix_zero_valueentry) = 2 * ge_signed_half_prefix_zero_valueentrysourcevaluedecode + 1 /\ (ge_balance_positive_prefix_zero_valueentrysourcevalue) = 0) /\ (ge_balance_negative_prefix_zero_valueentrysourcevalue) = S ge_signed_half_prefix_zero_valueentrysourcevaluedecode))) /\ ((dst_positive_prefix_zero_valueentrysource) + ge_balance_negative_prefix_zero_valueentrysourcevalue = (dst_negative_prefix_zero_valueentrysource) + ge_balance_positive_prefix_zero_valueentrysourcevalue))))))))) /\ (((((exists ff_h_pvs_prefix_zero_valueentrymap. ff_h_pvs_prefix_zero_valueentrymap + S (ssr_entry_image_prefix_zero_valueentry) = S ((S (ssr_flat_row_prefix_zero_value)) * s)) /\ exists ff_q_pvs_prefix_zero_valueentrymap. r = ff_q_pvs_prefix_zero_valueentrymap * S ((S (ssr_flat_row_prefix_zero_value)) * s) + (ssr_entry_image_prefix_zero_valueentry))) /\ (((((ssr_flat_column_prefix_zero_value)=(ssr_entry_image_prefix_zero_valueentry)) /\ ((z)=(ssr_entry_value_prefix_zero_valueentry)))) \/ (((~((ssr_flat_column_prefix_zero_value)=(ssr_entry_image_prefix_zero_valueentry))) /\ ((z)=0)))))))))))) -> (((exists dst_positive_code_prefix_zerotable dst_positive_scale_prefix_zerotable dst_negative_code_prefix_zerotable dst_negative_scale_prefix_zerotable. (((T) = (((((dst_positive_code_prefix_zerotable) + (dst_positive_scale_prefix_zerotable)) * S ((dst_positive_code_prefix_zerotable) + (dst_positive_scale_prefix_zerotable)) + ((dst_positive_scale_prefix_zerotable) + (dst_positive_scale_prefix_zerotable))) + (((dst_negative_code_prefix_zerotable) + (dst_negative_scale_prefix_zerotable)) * S ((dst_negative_code_prefix_zerotable) + (dst_negative_scale_prefix_zerotable)) + ((dst_negative_scale_prefix_zerotable) + (dst_negative_scale_prefix_zerotable)))) * S ((((dst_positive_code_prefix_zerotable) + (dst_positive_scale_prefix_zerotable)) * S ((dst_positive_code_prefix_zerotable) + (dst_positive_scale_prefix_zerotable)) + ((dst_positive_scale_prefix_zerotable) + (dst_positive_scale_prefix_zerotable))) + (((dst_negative_code_prefix_zerotable) + (dst_negative_scale_prefix_zerotable)) * S ((dst_negative_code_prefix_zerotable) + (dst_negative_scale_prefix_zerotable)) + ((dst_negative_scale_prefix_zerotable) + (dst_negative_scale_prefix_zerotable)))) + ((((dst_negative_code_prefix_zerotable) + (dst_negative_scale_prefix_zerotable)) * S ((dst_negative_code_prefix_zerotable) + (dst_negative_scale_prefix_zerotable)) + ((dst_negative_scale_prefix_zerotable) + (dst_negative_scale_prefix_zerotable))) + (((dst_negative_code_prefix_zerotable) + (dst_negative_scale_prefix_zerotable)) * S ((dst_negative_code_prefix_zerotable) + (dst_negative_scale_prefix_zerotable)) + ((dst_negative_scale_prefix_zerotable) + (dst_negative_scale_prefix_zerotable)))))) /\ (forall dst_index_prefix_zerotable. (exists pvs_le_gap_prefix_zerotabledomain. pvs_le_gap_prefix_zerotabledomain + (dst_index_prefix_zerotable) = (0)) -> exists dst_positive_prefix_zerotable dst_negative_prefix_zerotable dst_value_prefix_zerotable. ((((exists ff_h_pvs_prefix_zerotableentrypositive. ff_h_pvs_prefix_zerotableentrypositive + S (dst_positive_prefix_zerotable) = S ((S (dst_index_prefix_zerotable)) * dst_positive_scale_prefix_zerotable)) /\ exists ff_q_pvs_prefix_zerotableentrypositive. dst_positive_code_prefix_zerotable = ff_q_pvs_prefix_zerotableentrypositive * S ((S (dst_index_prefix_zerotable)) * dst_positive_scale_prefix_zerotable) + (dst_positive_prefix_zerotable))) /\ (((((exists ff_h_pvs_prefix_zerotableentrynegative. ff_h_pvs_prefix_zerotableentrynegative + S (dst_negative_prefix_zerotable) = S ((S (dst_index_prefix_zerotable)) * dst_negative_scale_prefix_zerotable)) /\ exists ff_q_pvs_prefix_zerotableentrynegative. dst_negative_code_prefix_zerotable = ff_q_pvs_prefix_zerotableentrynegative * S ((S (dst_index_prefix_zerotable)) * dst_negative_scale_prefix_zerotable) + (dst_negative_prefix_zerotable))) /\ (exists ge_balance_positive_prefix_zerotableentryvalue ge_balance_negative_prefix_zerotableentryvalue. (((((dst_value_prefix_zerotable) = 2 * (ge_balance_positive_prefix_zerotableentryvalue) /\ (ge_balance_negative_prefix_zerotableentryvalue) = 0) \/ exists ge_signed_half_prefix_zerotableentryvaluedecode. (((dst_value_prefix_zerotable) = 2 * ge_signed_half_prefix_zerotableentryvaluedecode + 1 /\ (ge_balance_positive_prefix_zerotableentryvalue) = 0) /\ (ge_balance_negative_prefix_zerotableentryvalue) = S ge_signed_half_prefix_zerotableentryvaluedecode))) /\ ((dst_positive_prefix_zerotable) + ge_balance_negative_prefix_zerotableentryvalue = (dst_negative_prefix_zerotable) + ge_balance_positive_prefix_zerotableentryvalue))))))))) /\ (forall ssr_prefix_index_prefix_zero ssr_prefix_value_prefix_zero. (exists pvs_le_gap_prefix_zerobound. pvs_le_gap_prefix_zerobound + (ssr_prefix_index_prefix_zero) = (0)) -> (exists dst_positive_code_prefix_zerolookup dst_positive_scale_prefix_zerolookup dst_negative_code_prefix_zerolookup dst_negative_scale_prefix_zerolookup dst_positive_prefix_zerolookup dst_negative_prefix_zerolookup. (((T) = (((((dst_positive_code_prefix_zerolookup) + (dst_positive_scale_prefix_zerolookup)) * S ((dst_positive_code_prefix_zerolookup) + (dst_positive_scale_prefix_zerolookup)) + ((dst_positive_scale_prefix_zerolookup) + (dst_positive_scale_prefix_zerolookup))) + (((dst_negative_code_prefix_zerolookup) + (dst_negative_scale_prefix_zerolookup)) * S ((dst_negative_code_prefix_zerolookup) + (dst_negative_scale_prefix_zerolookup)) + ((dst_negative_scale_prefix_zerolookup) + (dst_negative_scale_prefix_zerolookup)))) * S ((((dst_positive_code_prefix_zerolookup) + (dst_positive_scale_prefix_zerolookup)) * S ((dst_positive_code_prefix_zerolookup) + (dst_positive_scale_prefix_zerolookup)) + ((dst_positive_scale_prefix_zerolookup) + (dst_positive_scale_prefix_zerolookup))) + (((dst_negative_code_prefix_zerolookup) + (dst_negative_scale_prefix_zerolookup)) * S ((dst_negative_code_prefix_zerolookup) + (dst_negative_scale_prefix_zerolookup)) + ((dst_negative_scale_prefix_zerolookup) + (dst_negative_scale_prefix_zerolookup)))) + ((((dst_negative_code_prefix_zerolookup) + (dst_negative_scale_prefix_zerolookup)) * S ((dst_negative_code_prefix_zerolookup) + (dst_negative_scale_prefix_zerolookup)) + ((dst_negative_scale_prefix_zerolookup) + (dst_negative_scale_prefix_zerolookup))) + (((dst_negative_code_prefix_zerolookup) + (dst_negative_scale_prefix_zerolookup)) * S ((dst_negative_code_prefix_zerolookup) + (dst_negative_scale_prefix_zerolookup)) + ((dst_negative_scale_prefix_zerolookup) + (dst_negative_scale_prefix_zerolookup)))))) /\ (((((exists ff_h_pvs_prefix_zerolookuppositive. ff_h_pvs_prefix_zerolookuppositive + S (dst_positive_prefix_zerolookup) = S ((S (ssr_prefix_index_prefix_zero)) * dst_positive_scale_prefix_zerolookup)) /\ exists ff_q_pvs_prefix_zerolookuppositive. dst_positive_code_prefix_zerolookup = ff_q_pvs_prefix_zerolookuppositive * S ((S (ssr_prefix_index_prefix_zero)) * dst_positive_scale_prefix_zerolookup) + (dst_positive_prefix_zerolookup))) /\ (((((exists ff_h_pvs_prefix_zerolookupnegative. ff_h_pvs_prefix_zerolookupnegative + S (dst_negative_prefix_zerolookup) = S ((S (ssr_prefix_index_prefix_zero)) * dst_negative_scale_prefix_zerolookup)) /\ exists ff_q_pvs_prefix_zerolookupnegative. dst_negative_code_prefix_zerolookup = ff_q_pvs_prefix_zerolookupnegative * S ((S (ssr_prefix_index_prefix_zero)) * dst_negative_scale_prefix_zerolookup) + (dst_negative_prefix_zerolookup))) /\ (exists ge_balance_positive_prefix_zerolookupvalue ge_balance_negative_prefix_zerolookupvalue. (((((ssr_prefix_value_prefix_zero) = 2 * (ge_balance_positive_prefix_zerolookupvalue) /\ (ge_balance_negative_prefix_zerolookupvalue) = 0) \/ exists ge_signed_half_prefix_zerolookupvaluedecode. (((ssr_prefix_value_prefix_zero) = 2 * ge_signed_half_prefix_zerolookupvaluedecode + 1 /\ (ge_balance_positive_prefix_zerolookupvalue) = 0) /\ (ge_balance_negative_prefix_zerolookupvalue) = S ge_signed_half_prefix_zerolookupvaluedecode))) /\ ((dst_positive_prefix_zerolookup) + ge_balance_negative_prefix_zerolookupvalue = (dst_negative_prefix_zerolookup) + ge_balance_positive_prefix_zerolookupvalue))))))))) -> (exists ssr_flat_row_prefix_zeroentry ssr_flat_column_prefix_zeroentry. (((ssr_prefix_index_prefix_zero)=(((S (M))*(ssr_flat_row_prefix_zeroentry)+(ssr_flat_column_prefix_zeroentry)))) /\ (((exists pvs_gap_prefix_zeroentryremainder. pvs_gap_prefix_zeroentryremainder + S (ssr_flat_column_prefix_zeroentry) = (S (M))) /\ (exists ssr_entry_value_prefix_zeroentryentry ssr_entry_image_prefix_zeroentryentry. ((exists dst_positive_code_prefix_zeroentryentrysource dst_positive_scale_prefix_zeroentryentrysource dst_negative_code_prefix_zeroentryentrysource dst_negative_scale_prefix_zeroentryentrysource dst_positive_prefix_zeroentryentrysource dst_negative_prefix_zeroentryentrysource. (((A) = (((((dst_positive_code_prefix_zeroentryentrysource) + (dst_positive_scale_prefix_zeroentryentrysource)) * S ((dst_positive_code_prefix_zeroentryentrysource) + (dst_positive_scale_prefix_zeroentryentrysource)) + ((dst_positive_scale_prefix_zeroentryentrysource) + (dst_positive_scale_prefix_zeroentryentrysource))) + (((dst_negative_code_prefix_zeroentryentrysource) + (dst_negative_scale_prefix_zeroentryentrysource)) * S ((dst_negative_code_prefix_zeroentryentrysource) + (dst_negative_scale_prefix_zeroentryentrysource)) + ((dst_negative_scale_prefix_zeroentryentrysource) + (dst_negative_scale_prefix_zeroentryentrysource)))) * S ((((dst_positive_code_prefix_zeroentryentrysource) + (dst_positive_scale_prefix_zeroentryentrysource)) * S ((dst_positive_code_prefix_zeroentryentrysource) + (dst_positive_scale_prefix_zeroentryentrysource)) + ((dst_positive_scale_prefix_zeroentryentrysource) + (dst_positive_scale_prefix_zeroentryentrysource))) + (((dst_negative_code_prefix_zeroentryentrysource) + (dst_negative_scale_prefix_zeroentryentrysource)) * S ((dst_negative_code_prefix_zeroentryentrysource) + (dst_negative_scale_prefix_zeroentryentrysource)) + ((dst_negative_scale_prefix_zeroentryentrysource) + (dst_negative_scale_prefix_zeroentryentrysource)))) + ((((dst_negative_code_prefix_zeroentryentrysource) + (dst_negative_scale_prefix_zeroentryentrysource)) * S ((dst_negative_code_prefix_zeroentryentrysource) + (dst_negative_scale_prefix_zeroentryentrysource)) + ((dst_negative_scale_prefix_zeroentryentrysource) + (dst_negative_scale_prefix_zeroentryentrysource))) + (((dst_negative_code_prefix_zeroentryentrysource) + (dst_negative_scale_prefix_zeroentryentrysource)) * S ((dst_negative_code_prefix_zeroentryentrysource) + (dst_negative_scale_prefix_zeroentryentrysource)) + ((dst_negative_scale_prefix_zeroentryentrysource) + (dst_negative_scale_prefix_zeroentryentrysource)))))) /\ (((((exists ff_h_pvs_prefix_zeroentryentrysourcepositive. ff_h_pvs_prefix_zeroentryentrysourcepositive + S (dst_positive_prefix_zeroentryentrysource) = S ((S (ssr_flat_row_prefix_zeroentry)) * dst_positive_scale_prefix_zeroentryentrysource)) /\ exists ff_q_pvs_prefix_zeroentryentrysourcepositive. dst_positive_code_prefix_zeroentryentrysource = ff_q_pvs_prefix_zeroentryentrysourcepositive * S ((S (ssr_flat_row_prefix_zeroentry)) * dst_positive_scale_prefix_zeroentryentrysource) + (dst_positive_prefix_zeroentryentrysource))) /\ (((((exists ff_h_pvs_prefix_zeroentryentrysourcenegative. ff_h_pvs_prefix_zeroentryentrysourcenegative + S (dst_negative_prefix_zeroentryentrysource) = S ((S (ssr_flat_row_prefix_zeroentry)) * dst_negative_scale_prefix_zeroentryentrysource)) /\ exists ff_q_pvs_prefix_zeroentryentrysourcenegative. dst_negative_code_prefix_zeroentryentrysource = ff_q_pvs_prefix_zeroentryentrysourcenegative * S ((S (ssr_flat_row_prefix_zeroentry)) * dst_negative_scale_prefix_zeroentryentrysource) + (dst_negative_prefix_zeroentryentrysource))) /\ (exists ge_balance_positive_prefix_zeroentryentrysourcevalue ge_balance_negative_prefix_zeroentryentrysourcevalue. (((((ssr_entry_value_prefix_zeroentryentry) = 2 * (ge_balance_positive_prefix_zeroentryentrysourcevalue) /\ (ge_balance_negative_prefix_zeroentryentrysourcevalue) = 0) \/ exists ge_signed_half_prefix_zeroentryentrysourcevaluedecode. (((ssr_entry_value_prefix_zeroentryentry) = 2 * ge_signed_half_prefix_zeroentryentrysourcevaluedecode + 1 /\ (ge_balance_positive_prefix_zeroentryentrysourcevalue) = 0) /\ (ge_balance_negative_prefix_zeroentryentrysourcevalue) = S ge_signed_half_prefix_zeroentryentrysourcevaluedecode))) /\ ((dst_positive_prefix_zeroentryentrysource) + ge_balance_negative_prefix_zeroentryentrysourcevalue = (dst_negative_prefix_zeroentryentrysource) + ge_balance_positive_prefix_zeroentryentrysourcevalue))))))))) /\ (((((exists ff_h_pvs_prefix_zeroentryentrymap. ff_h_pvs_prefix_zeroentryentrymap + S (ssr_entry_image_prefix_zeroentryentry) = S ((S (ssr_flat_row_prefix_zeroentry)) * s)) /\ exists ff_q_pvs_prefix_zeroentryentrymap. r = ff_q_pvs_prefix_zeroentryentrymap * S ((S (ssr_flat_row_prefix_zeroentry)) * s) + (ssr_entry_image_prefix_zeroentryentry))) /\ (((((ssr_flat_column_prefix_zeroentry)=(ssr_entry_image_prefix_zeroentryentry)) /\ ((ssr_prefix_value_prefix_zero)=(ssr_entry_value_prefix_zeroentryentry)))) \/ (((~((ssr_flat_column_prefix_zeroentry)=(ssr_entry_image_prefix_zeroentryentry))) /\ ((ssr_prefix_value_prefix_zero)=0)))))))))))))))