SignedSupportIncidence(A,r,s,L,M,T)

((exists dst_positive_code_g009_definitionsource dst_positive_scale_g009_definitionsource dst_negative_code_g009_definitionsource dst_negative_scale_g009_definitionsource. ((((A)) = (((((dst_positive_code_g009_definitionsource) + (dst_positive_scale_g009_definitionsource)) * S ((dst_positive_code_g009_definitionsource) + (dst_positive_scale_g009_definitionsource)) + ((dst_positive_scale_g009_definitionsource) + (dst_positive_scale_g009_definitionsource))) + (((dst_negative_code_g009_definitionsource) + (dst_negative_scale_g009_definitionsource)) * S ((dst_negative_code_g009_definitionsource) + (dst_negative_scale_g009_definitionsource)) + ((dst_negative_scale_g009_definitionsource) + (dst_negative_scale_g009_definitionsource)))) * S ((((dst_positive_code_g009_definitionsource) + (dst_positive_scale_g009_definitionsource)) * S ((dst_positive_code_g009_definitionsource) + (dst_positive_scale_g009_definitionsource)) + ((dst_positive_scale_g009_definitionsource) + (dst_positive_scale_g009_definitionsource))) + (((dst_negative_code_g009_definitionsource) + (dst_negative_scale_g009_definitionsource)) * S ((dst_negative_code_g009_definitionsource) + (dst_negative_scale_g009_definitionsource)) + ((dst_negative_scale_g009_definitionsource) + (dst_negative_scale_g009_definitionsource)))) + ((((dst_negative_code_g009_definitionsource) + (dst_negative_scale_g009_definitionsource)) * S ((dst_negative_code_g009_definitionsource) + (dst_negative_scale_g009_definitionsource)) + ((dst_negative_scale_g009_definitionsource) + (dst_negative_scale_g009_definitionsource))) + (((dst_negative_code_g009_definitionsource) + (dst_negative_scale_g009_definitionsource)) * S ((dst_negative_code_g009_definitionsource) + (dst_negative_scale_g009_definitionsource)) + ((dst_negative_scale_g009_definitionsource) + (dst_negative_scale_g009_definitionsource)))))) /\ (forall dst_index_g009_definitionsource. (exists pvs_le_gap_g009_definitionsourcedomain. pvs_le_gap_g009_definitionsourcedomain + (dst_index_g009_definitionsource) = (0)) -> exists dst_positive_g009_definitionsource dst_negative_g009_definitionsource dst_value_g009_definitionsource. ((((exists ff_h_pvs_g009_definitionsourceentrypositive. ff_h_pvs_g009_definitionsourceentrypositive + S (dst_positive_g009_definitionsource) = S ((S (dst_index_g009_definitionsource)) * dst_positive_scale_g009_definitionsource)) /\ exists ff_q_pvs_g009_definitionsourceentrypositive. dst_positive_code_g009_definitionsource = ff_q_pvs_g009_definitionsourceentrypositive * S ((S (dst_index_g009_definitionsource)) * dst_positive_scale_g009_definitionsource) + (dst_positive_g009_definitionsource))) /\ (((((exists ff_h_pvs_g009_definitionsourceentrynegative. ff_h_pvs_g009_definitionsourceentrynegative + S (dst_negative_g009_definitionsource) = S ((S (dst_index_g009_definitionsource)) * dst_negative_scale_g009_definitionsource)) /\ exists ff_q_pvs_g009_definitionsourceentrynegative. dst_negative_code_g009_definitionsource = ff_q_pvs_g009_definitionsourceentrynegative * S ((S (dst_index_g009_definitionsource)) * dst_negative_scale_g009_definitionsource) + (dst_negative_g009_definitionsource))) /\ (exists ge_balance_positive_g009_definitionsourceentryvalue ge_balance_negative_g009_definitionsourceentryvalue. (((((dst_value_g009_definitionsource) = 2 * (ge_balance_positive_g009_definitionsourceentryvalue) /\ (ge_balance_negative_g009_definitionsourceentryvalue) = 0) \/ exists ge_signed_half_g009_definitionsourceentryvaluedecode. (((dst_value_g009_definitionsource) = 2 * ge_signed_half_g009_definitionsourceentryvaluedecode + 1 /\ (ge_balance_positive_g009_definitionsourceentryvalue) = 0) /\ (ge_balance_negative_g009_definitionsourceentryvalue) = S ge_signed_half_g009_definitionsourceentryvaluedecode))) /\ ((dst_positive_g009_definitionsource) + ge_balance_negative_g009_definitionsourceentryvalue = (dst_negative_g009_definitionsource) + ge_balance_positive_g009_definitionsourceentryvalue))))))))) /\ (((exists dst_positive_code_g009_definitiontable dst_positive_scale_g009_definitiontable dst_negative_code_g009_definitiontable dst_negative_scale_g009_definitiontable. ((((T)) = (((((dst_positive_code_g009_definitiontable) + (dst_positive_scale_g009_definitiontable)) * S ((dst_positive_code_g009_definitiontable) + (dst_positive_scale_g009_definitiontable)) + ((dst_positive_scale_g009_definitiontable) + (dst_positive_scale_g009_definitiontable))) + (((dst_negative_code_g009_definitiontable) + (dst_negative_scale_g009_definitiontable)) * S ((dst_negative_code_g009_definitiontable) + (dst_negative_scale_g009_definitiontable)) + ((dst_negative_scale_g009_definitiontable) + (dst_negative_scale_g009_definitiontable)))) * S ((((dst_positive_code_g009_definitiontable) + (dst_positive_scale_g009_definitiontable)) * S ((dst_positive_code_g009_definitiontable) + (dst_positive_scale_g009_definitiontable)) + ((dst_positive_scale_g009_definitiontable) + (dst_positive_scale_g009_definitiontable))) + (((dst_negative_code_g009_definitiontable) + (dst_negative_scale_g009_definitiontable)) * S ((dst_negative_code_g009_definitiontable) + (dst_negative_scale_g009_definitiontable)) + ((dst_negative_scale_g009_definitiontable) + (dst_negative_scale_g009_definitiontable)))) + ((((dst_negative_code_g009_definitiontable) + (dst_negative_scale_g009_definitiontable)) * S ((dst_negative_code_g009_definitiontable) + (dst_negative_scale_g009_definitiontable)) + ((dst_negative_scale_g009_definitiontable) + (dst_negative_scale_g009_definitiontable))) + (((dst_negative_code_g009_definitiontable) + (dst_negative_scale_g009_definitiontable)) * S ((dst_negative_code_g009_definitiontable) + (dst_negative_scale_g009_definitiontable)) + ((dst_negative_scale_g009_definitiontable) + (dst_negative_scale_g009_definitiontable)))))) /\ (forall dst_index_g009_definitiontable. (exists pvs_le_gap_g009_definitiontabledomain. pvs_le_gap_g009_definitiontabledomain + (dst_index_g009_definitiontable) = (((L))*(S ((M))))) -> exists dst_positive_g009_definitiontable dst_negative_g009_definitiontable dst_value_g009_definitiontable. ((((exists ff_h_pvs_g009_definitiontableentrypositive. ff_h_pvs_g009_definitiontableentrypositive + S (dst_positive_g009_definitiontable) = S ((S (dst_index_g009_definitiontable)) * dst_positive_scale_g009_definitiontable)) /\ exists ff_q_pvs_g009_definitiontableentrypositive. dst_positive_code_g009_definitiontable = ff_q_pvs_g009_definitiontableentrypositive * S ((S (dst_index_g009_definitiontable)) * dst_positive_scale_g009_definitiontable) + (dst_positive_g009_definitiontable))) /\ (((((exists ff_h_pvs_g009_definitiontableentrynegative. ff_h_pvs_g009_definitiontableentrynegative + S (dst_negative_g009_definitiontable) = S ((S (dst_index_g009_definitiontable)) * dst_negative_scale_g009_definitiontable)) /\ exists ff_q_pvs_g009_definitiontableentrynegative. dst_negative_code_g009_definitiontable = ff_q_pvs_g009_definitiontableentrynegative * S ((S (dst_index_g009_definitiontable)) * dst_negative_scale_g009_definitiontable) + (dst_negative_g009_definitiontable))) /\ (exists ge_balance_positive_g009_definitiontableentryvalue ge_balance_negative_g009_definitiontableentryvalue. (((((dst_value_g009_definitiontable) = 2 * (ge_balance_positive_g009_definitiontableentryvalue) /\ (ge_balance_negative_g009_definitiontableentryvalue) = 0) \/ exists ge_signed_half_g009_definitiontableentryvaluedecode. (((dst_value_g009_definitiontable) = 2 * ge_signed_half_g009_definitiontableentryvaluedecode + 1 /\ (ge_balance_positive_g009_definitiontableentryvalue) = 0) /\ (ge_balance_negative_g009_definitiontableentryvalue) = S ge_signed_half_g009_definitiontableentryvaluedecode))) /\ ((dst_positive_g009_definitiontable) + ge_balance_negative_g009_definitiontableentryvalue = (dst_negative_g009_definitiontable) + ge_balance_positive_g009_definitiontableentryvalue))))))))) /\ (forall ssr_grid_row_g009_definition ssr_grid_column_g009_definition ssr_grid_value_g009_definition. (exists pvs_gap_g009_definitionrow_bound. pvs_gap_g009_definitionrow_bound + S (ssr_grid_row_g009_definition) = ((L))) -> (exists pvs_gap_g009_definitioncolumn_bound. pvs_gap_g009_definitioncolumn_bound + S (ssr_grid_column_g009_definition) = ((M))) -> (exists dst_positive_code_g009_definitionlookup dst_positive_scale_g009_definitionlookup dst_negative_code_g009_definitionlookup dst_negative_scale_g009_definitionlookup dst_positive_g009_definitionlookup dst_negative_g009_definitionlookup. ((((T)) = (((((dst_positive_code_g009_definitionlookup) + (dst_positive_scale_g009_definitionlookup)) * S ((dst_positive_code_g009_definitionlookup) + (dst_positive_scale_g009_definitionlookup)) + ((dst_positive_scale_g009_definitionlookup) + (dst_positive_scale_g009_definitionlookup))) + (((dst_negative_code_g009_definitionlookup) + (dst_negative_scale_g009_definitionlookup)) * S ((dst_negative_code_g009_definitionlookup) + (dst_negative_scale_g009_definitionlookup)) + ((dst_negative_scale_g009_definitionlookup) + (dst_negative_scale_g009_definitionlookup)))) * S ((((dst_positive_code_g009_definitionlookup) + (dst_positive_scale_g009_definitionlookup)) * S ((dst_positive_code_g009_definitionlookup) + (dst_positive_scale_g009_definitionlookup)) + ((dst_positive_scale_g009_definitionlookup) + (dst_positive_scale_g009_definitionlookup))) + (((dst_negative_code_g009_definitionlookup) + (dst_negative_scale_g009_definitionlookup)) * S ((dst_negative_code_g009_definitionlookup) + (dst_negative_scale_g009_definitionlookup)) + ((dst_negative_scale_g009_definitionlookup) + (dst_negative_scale_g009_definitionlookup)))) + ((((dst_negative_code_g009_definitionlookup) + (dst_negative_scale_g009_definitionlookup)) * S ((dst_negative_code_g009_definitionlookup) + (dst_negative_scale_g009_definitionlookup)) + ((dst_negative_scale_g009_definitionlookup) + (dst_negative_scale_g009_definitionlookup))) + (((dst_negative_code_g009_definitionlookup) + (dst_negative_scale_g009_definitionlookup)) * S ((dst_negative_code_g009_definitionlookup) + (dst_negative_scale_g009_definitionlookup)) + ((dst_negative_scale_g009_definitionlookup) + (dst_negative_scale_g009_definitionlookup)))))) /\ (((((exists ff_h_pvs_g009_definitionlookuppositive. ff_h_pvs_g009_definitionlookuppositive + S (dst_positive_g009_definitionlookup) = S ((S (((S ((M)))*(ssr_grid_row_g009_definition)+(ssr_grid_column_g009_definition)))) * dst_positive_scale_g009_definitionlookup)) /\ exists ff_q_pvs_g009_definitionlookuppositive. dst_positive_code_g009_definitionlookup = ff_q_pvs_g009_definitionlookuppositive * S ((S (((S ((M)))*(ssr_grid_row_g009_definition)+(ssr_grid_column_g009_definition)))) * dst_positive_scale_g009_definitionlookup) + (dst_positive_g009_definitionlookup))) /\ (((((exists ff_h_pvs_g009_definitionlookupnegative. ff_h_pvs_g009_definitionlookupnegative + S (dst_negative_g009_definitionlookup) = S ((S (((S ((M)))*(ssr_grid_row_g009_definition)+(ssr_grid_column_g009_definition)))) * dst_negative_scale_g009_definitionlookup)) /\ exists ff_q_pvs_g009_definitionlookupnegative. dst_negative_code_g009_definitionlookup = ff_q_pvs_g009_definitionlookupnegative * S ((S (((S ((M)))*(ssr_grid_row_g009_definition)+(ssr_grid_column_g009_definition)))) * dst_negative_scale_g009_definitionlookup) + (dst_negative_g009_definitionlookup))) /\ (exists ge_balance_positive_g009_definitionlookupvalue ge_balance_negative_g009_definitionlookupvalue. (((((ssr_grid_value_g009_definition) = 2 * (ge_balance_positive_g009_definitionlookupvalue) /\ (ge_balance_negative_g009_definitionlookupvalue) = 0) \/ exists ge_signed_half_g009_definitionlookupvaluedecode. (((ssr_grid_value_g009_definition) = 2 * ge_signed_half_g009_definitionlookupvaluedecode + 1 /\ (ge_balance_positive_g009_definitionlookupvalue) = 0) /\ (ge_balance_negative_g009_definitionlookupvalue) = S ge_signed_half_g009_definitionlookupvaluedecode))) /\ ((dst_positive_g009_definitionlookup) + ge_balance_negative_g009_definitionlookupvalue = (dst_negative_g009_definitionlookup) + ge_balance_positive_g009_definitionlookupvalue))))))))) -> (exists ssr_entry_value_g009_definitionentry ssr_entry_image_g009_definitionentry. ((exists dst_positive_code_g009_definitionentrysource dst_positive_scale_g009_definitionentrysource dst_negative_code_g009_definitionentrysource dst_negative_scale_g009_definitionentrysource dst_positive_g009_definitionentrysource dst_negative_g009_definitionentrysource. ((((A)) = (((((dst_positive_code_g009_definitionentrysource) + (dst_positive_scale_g009_definitionentrysource)) * S ((dst_positive_code_g009_definitionentrysource) + (dst_positive_scale_g009_definitionentrysource)) + ((dst_positive_scale_g009_definitionentrysource) + (dst_positive_scale_g009_definitionentrysource))) + (((dst_negative_code_g009_definitionentrysource) + (dst_negative_scale_g009_definitionentrysource)) * S ((dst_negative_code_g009_definitionentrysource) + (dst_negative_scale_g009_definitionentrysource)) + ((dst_negative_scale_g009_definitionentrysource) + (dst_negative_scale_g009_definitionentrysource)))) * S ((((dst_positive_code_g009_definitionentrysource) + (dst_positive_scale_g009_definitionentrysource)) * S ((dst_positive_code_g009_definitionentrysource) + (dst_positive_scale_g009_definitionentrysource)) + ((dst_positive_scale_g009_definitionentrysource) + (dst_positive_scale_g009_definitionentrysource))) + (((dst_negative_code_g009_definitionentrysource) + (dst_negative_scale_g009_definitionentrysource)) * S ((dst_negative_code_g009_definitionentrysource) + (dst_negative_scale_g009_definitionentrysource)) + ((dst_negative_scale_g009_definitionentrysource) + (dst_negative_scale_g009_definitionentrysource)))) + ((((dst_negative_code_g009_definitionentrysource) + (dst_negative_scale_g009_definitionentrysource)) * S ((dst_negative_code_g009_definitionentrysource) + (dst_negative_scale_g009_definitionentrysource)) + ((dst_negative_scale_g009_definitionentrysource) + (dst_negative_scale_g009_definitionentrysource))) + (((dst_negative_code_g009_definitionentrysource) + (dst_negative_scale_g009_definitionentrysource)) * S ((dst_negative_code_g009_definitionentrysource) + (dst_negative_scale_g009_definitionentrysource)) + ((dst_negative_scale_g009_definitionentrysource) + (dst_negative_scale_g009_definitionentrysource)))))) /\ (((((exists ff_h_pvs_g009_definitionentrysourcepositive. ff_h_pvs_g009_definitionentrysourcepositive + S (dst_positive_g009_definitionentrysource) = S ((S (ssr_grid_row_g009_definition)) * dst_positive_scale_g009_definitionentrysource)) /\ exists ff_q_pvs_g009_definitionentrysourcepositive. dst_positive_code_g009_definitionentrysource = ff_q_pvs_g009_definitionentrysourcepositive * S ((S (ssr_grid_row_g009_definition)) * dst_positive_scale_g009_definitionentrysource) + (dst_positive_g009_definitionentrysource))) /\ (((((exists ff_h_pvs_g009_definitionentrysourcenegative. ff_h_pvs_g009_definitionentrysourcenegative + S (dst_negative_g009_definitionentrysource) = S ((S (ssr_grid_row_g009_definition)) * dst_negative_scale_g009_definitionentrysource)) /\ exists ff_q_pvs_g009_definitionentrysourcenegative. dst_negative_code_g009_definitionentrysource = ff_q_pvs_g009_definitionentrysourcenegative * S ((S (ssr_grid_row_g009_definition)) * dst_negative_scale_g009_definitionentrysource) + (dst_negative_g009_definitionentrysource))) /\ (exists ge_balance_positive_g009_definitionentrysourcevalue ge_balance_negative_g009_definitionentrysourcevalue. (((((ssr_entry_value_g009_definitionentry) = 2 * (ge_balance_positive_g009_definitionentrysourcevalue) /\ (ge_balance_negative_g009_definitionentrysourcevalue) = 0) \/ exists ge_signed_half_g009_definitionentrysourcevaluedecode. (((ssr_entry_value_g009_definitionentry) = 2 * ge_signed_half_g009_definitionentrysourcevaluedecode + 1 /\ (ge_balance_positive_g009_definitionentrysourcevalue) = 0) /\ (ge_balance_negative_g009_definitionentrysourcevalue) = S ge_signed_half_g009_definitionentrysourcevaluedecode))) /\ ((dst_positive_g009_definitionentrysource) + ge_balance_negative_g009_definitionentrysourcevalue = (dst_negative_g009_definitionentrysource) + ge_balance_positive_g009_definitionentrysourcevalue))))))))) /\ (((((exists ff_h_pvs_g009_definitionentrymap. ff_h_pvs_g009_definitionentrymap + S (ssr_entry_image_g009_definitionentry) = S ((S (ssr_grid_row_g009_definition)) * (s))) /\ exists ff_q_pvs_g009_definitionentrymap. (r) = ff_q_pvs_g009_definitionentrymap * S ((S (ssr_grid_row_g009_definition)) * (s)) + (ssr_entry_image_g009_definitionentry))) /\ (((((ssr_grid_column_g009_definition)=(ssr_entry_image_g009_definitionentry)) /\ ((ssr_grid_value_g009_definition)=(ssr_entry_value_g009_definitionentry)))) \/ (((~((ssr_grid_column_g009_definition)=(ssr_entry_image_g009_definitionentry))) /\ ((ssr_grid_value_g009_definition)=0))))))))))))

The unchanged native kernel never receives this surface symbol. Binder-safe expansion produces only its existing first-order syntax.