SignedCartesianProduct(F,G,T,m,n)

((exists dst_positive_code_g009_definitionF dst_positive_scale_g009_definitionF dst_negative_code_g009_definitionF dst_negative_scale_g009_definitionF. ((((F)) = (((((dst_positive_code_g009_definitionF) + (dst_positive_scale_g009_definitionF)) * S ((dst_positive_code_g009_definitionF) + (dst_positive_scale_g009_definitionF)) + ((dst_positive_scale_g009_definitionF) + (dst_positive_scale_g009_definitionF))) + (((dst_negative_code_g009_definitionF) + (dst_negative_scale_g009_definitionF)) * S ((dst_negative_code_g009_definitionF) + (dst_negative_scale_g009_definitionF)) + ((dst_negative_scale_g009_definitionF) + (dst_negative_scale_g009_definitionF)))) * S ((((dst_positive_code_g009_definitionF) + (dst_positive_scale_g009_definitionF)) * S ((dst_positive_code_g009_definitionF) + (dst_positive_scale_g009_definitionF)) + ((dst_positive_scale_g009_definitionF) + (dst_positive_scale_g009_definitionF))) + (((dst_negative_code_g009_definitionF) + (dst_negative_scale_g009_definitionF)) * S ((dst_negative_code_g009_definitionF) + (dst_negative_scale_g009_definitionF)) + ((dst_negative_scale_g009_definitionF) + (dst_negative_scale_g009_definitionF)))) + ((((dst_negative_code_g009_definitionF) + (dst_negative_scale_g009_definitionF)) * S ((dst_negative_code_g009_definitionF) + (dst_negative_scale_g009_definitionF)) + ((dst_negative_scale_g009_definitionF) + (dst_negative_scale_g009_definitionF))) + (((dst_negative_code_g009_definitionF) + (dst_negative_scale_g009_definitionF)) * S ((dst_negative_code_g009_definitionF) + (dst_negative_scale_g009_definitionF)) + ((dst_negative_scale_g009_definitionF) + (dst_negative_scale_g009_definitionF)))))) /\ (forall dst_index_g009_definitionF. (exists pvs_le_gap_g009_definitionFdomain. pvs_le_gap_g009_definitionFdomain + (dst_index_g009_definitionF) = (0)) -> exists dst_positive_g009_definitionF dst_negative_g009_definitionF dst_value_g009_definitionF. ((((exists ff_h_pvs_g009_definitionFentrypositive. ff_h_pvs_g009_definitionFentrypositive + S (dst_positive_g009_definitionF) = S ((S (dst_index_g009_definitionF)) * dst_positive_scale_g009_definitionF)) /\ exists ff_q_pvs_g009_definitionFentrypositive. dst_positive_code_g009_definitionF = ff_q_pvs_g009_definitionFentrypositive * S ((S (dst_index_g009_definitionF)) * dst_positive_scale_g009_definitionF) + (dst_positive_g009_definitionF))) /\ (((((exists ff_h_pvs_g009_definitionFentrynegative. ff_h_pvs_g009_definitionFentrynegative + S (dst_negative_g009_definitionF) = S ((S (dst_index_g009_definitionF)) * dst_negative_scale_g009_definitionF)) /\ exists ff_q_pvs_g009_definitionFentrynegative. dst_negative_code_g009_definitionF = ff_q_pvs_g009_definitionFentrynegative * S ((S (dst_index_g009_definitionF)) * dst_negative_scale_g009_definitionF) + (dst_negative_g009_definitionF))) /\ (exists ge_balance_positive_g009_definitionFentryvalue ge_balance_negative_g009_definitionFentryvalue. (((((dst_value_g009_definitionF) = 2 * (ge_balance_positive_g009_definitionFentryvalue) /\ (ge_balance_negative_g009_definitionFentryvalue) = 0) \/ exists ge_signed_half_g009_definitionFentryvaluedecode. (((dst_value_g009_definitionF) = 2 * ge_signed_half_g009_definitionFentryvaluedecode + 1 /\ (ge_balance_positive_g009_definitionFentryvalue) = 0) /\ (ge_balance_negative_g009_definitionFentryvalue) = S ge_signed_half_g009_definitionFentryvaluedecode))) /\ ((dst_positive_g009_definitionF) + ge_balance_negative_g009_definitionFentryvalue = (dst_negative_g009_definitionF) + ge_balance_positive_g009_definitionFentryvalue))))))))) /\ (((exists dst_positive_code_g009_definitionG dst_positive_scale_g009_definitionG dst_negative_code_g009_definitionG dst_negative_scale_g009_definitionG. ((((G)) = (((((dst_positive_code_g009_definitionG) + (dst_positive_scale_g009_definitionG)) * S ((dst_positive_code_g009_definitionG) + (dst_positive_scale_g009_definitionG)) + ((dst_positive_scale_g009_definitionG) + (dst_positive_scale_g009_definitionG))) + (((dst_negative_code_g009_definitionG) + (dst_negative_scale_g009_definitionG)) * S ((dst_negative_code_g009_definitionG) + (dst_negative_scale_g009_definitionG)) + ((dst_negative_scale_g009_definitionG) + (dst_negative_scale_g009_definitionG)))) * S ((((dst_positive_code_g009_definitionG) + (dst_positive_scale_g009_definitionG)) * S ((dst_positive_code_g009_definitionG) + (dst_positive_scale_g009_definitionG)) + ((dst_positive_scale_g009_definitionG) + (dst_positive_scale_g009_definitionG))) + (((dst_negative_code_g009_definitionG) + (dst_negative_scale_g009_definitionG)) * S ((dst_negative_code_g009_definitionG) + (dst_negative_scale_g009_definitionG)) + ((dst_negative_scale_g009_definitionG) + (dst_negative_scale_g009_definitionG)))) + ((((dst_negative_code_g009_definitionG) + (dst_negative_scale_g009_definitionG)) * S ((dst_negative_code_g009_definitionG) + (dst_negative_scale_g009_definitionG)) + ((dst_negative_scale_g009_definitionG) + (dst_negative_scale_g009_definitionG))) + (((dst_negative_code_g009_definitionG) + (dst_negative_scale_g009_definitionG)) * S ((dst_negative_code_g009_definitionG) + (dst_negative_scale_g009_definitionG)) + ((dst_negative_scale_g009_definitionG) + (dst_negative_scale_g009_definitionG)))))) /\ (forall dst_index_g009_definitionG. (exists pvs_le_gap_g009_definitionGdomain. pvs_le_gap_g009_definitionGdomain + (dst_index_g009_definitionG) = (0)) -> exists dst_positive_g009_definitionG dst_negative_g009_definitionG dst_value_g009_definitionG. ((((exists ff_h_pvs_g009_definitionGentrypositive. ff_h_pvs_g009_definitionGentrypositive + S (dst_positive_g009_definitionG) = S ((S (dst_index_g009_definitionG)) * dst_positive_scale_g009_definitionG)) /\ exists ff_q_pvs_g009_definitionGentrypositive. dst_positive_code_g009_definitionG = ff_q_pvs_g009_definitionGentrypositive * S ((S (dst_index_g009_definitionG)) * dst_positive_scale_g009_definitionG) + (dst_positive_g009_definitionG))) /\ (((((exists ff_h_pvs_g009_definitionGentrynegative. ff_h_pvs_g009_definitionGentrynegative + S (dst_negative_g009_definitionG) = S ((S (dst_index_g009_definitionG)) * dst_negative_scale_g009_definitionG)) /\ exists ff_q_pvs_g009_definitionGentrynegative. dst_negative_code_g009_definitionG = ff_q_pvs_g009_definitionGentrynegative * S ((S (dst_index_g009_definitionG)) * dst_negative_scale_g009_definitionG) + (dst_negative_g009_definitionG))) /\ (exists ge_balance_positive_g009_definitionGentryvalue ge_balance_negative_g009_definitionGentryvalue. (((((dst_value_g009_definitionG) = 2 * (ge_balance_positive_g009_definitionGentryvalue) /\ (ge_balance_negative_g009_definitionGentryvalue) = 0) \/ exists ge_signed_half_g009_definitionGentryvaluedecode. (((dst_value_g009_definitionG) = 2 * ge_signed_half_g009_definitionGentryvaluedecode + 1 /\ (ge_balance_positive_g009_definitionGentryvalue) = 0) /\ (ge_balance_negative_g009_definitionGentryvalue) = S ge_signed_half_g009_definitionGentryvaluedecode))) /\ ((dst_positive_g009_definitionG) + ge_balance_negative_g009_definitionGentryvalue = (dst_negative_g009_definitionG) + ge_balance_positive_g009_definitionGentryvalue))))))))) /\ (((exists dst_positive_code_g009_definitionT dst_positive_scale_g009_definitionT dst_negative_code_g009_definitionT dst_negative_scale_g009_definitionT. ((((T)) = (((((dst_positive_code_g009_definitionT) + (dst_positive_scale_g009_definitionT)) * S ((dst_positive_code_g009_definitionT) + (dst_positive_scale_g009_definitionT)) + ((dst_positive_scale_g009_definitionT) + (dst_positive_scale_g009_definitionT))) + (((dst_negative_code_g009_definitionT) + (dst_negative_scale_g009_definitionT)) * S ((dst_negative_code_g009_definitionT) + (dst_negative_scale_g009_definitionT)) + ((dst_negative_scale_g009_definitionT) + (dst_negative_scale_g009_definitionT)))) * S ((((dst_positive_code_g009_definitionT) + (dst_positive_scale_g009_definitionT)) * S ((dst_positive_code_g009_definitionT) + (dst_positive_scale_g009_definitionT)) + ((dst_positive_scale_g009_definitionT) + (dst_positive_scale_g009_definitionT))) + (((dst_negative_code_g009_definitionT) + (dst_negative_scale_g009_definitionT)) * S ((dst_negative_code_g009_definitionT) + (dst_negative_scale_g009_definitionT)) + ((dst_negative_scale_g009_definitionT) + (dst_negative_scale_g009_definitionT)))) + ((((dst_negative_code_g009_definitionT) + (dst_negative_scale_g009_definitionT)) * S ((dst_negative_code_g009_definitionT) + (dst_negative_scale_g009_definitionT)) + ((dst_negative_scale_g009_definitionT) + (dst_negative_scale_g009_definitionT))) + (((dst_negative_code_g009_definitionT) + (dst_negative_scale_g009_definitionT)) * S ((dst_negative_code_g009_definitionT) + (dst_negative_scale_g009_definitionT)) + ((dst_negative_scale_g009_definitionT) + (dst_negative_scale_g009_definitionT)))))) /\ (forall dst_index_g009_definitionT. (exists pvs_le_gap_g009_definitionTdomain. pvs_le_gap_g009_definitionTdomain + (dst_index_g009_definitionT) = (((m))*((n)))) -> exists dst_positive_g009_definitionT dst_negative_g009_definitionT dst_value_g009_definitionT. ((((exists ff_h_pvs_g009_definitionTentrypositive. ff_h_pvs_g009_definitionTentrypositive + S (dst_positive_g009_definitionT) = S ((S (dst_index_g009_definitionT)) * dst_positive_scale_g009_definitionT)) /\ exists ff_q_pvs_g009_definitionTentrypositive. dst_positive_code_g009_definitionT = ff_q_pvs_g009_definitionTentrypositive * S ((S (dst_index_g009_definitionT)) * dst_positive_scale_g009_definitionT) + (dst_positive_g009_definitionT))) /\ (((((exists ff_h_pvs_g009_definitionTentrynegative. ff_h_pvs_g009_definitionTentrynegative + S (dst_negative_g009_definitionT) = S ((S (dst_index_g009_definitionT)) * dst_negative_scale_g009_definitionT)) /\ exists ff_q_pvs_g009_definitionTentrynegative. dst_negative_code_g009_definitionT = ff_q_pvs_g009_definitionTentrynegative * S ((S (dst_index_g009_definitionT)) * dst_negative_scale_g009_definitionT) + (dst_negative_g009_definitionT))) /\ (exists ge_balance_positive_g009_definitionTentryvalue ge_balance_negative_g009_definitionTentryvalue. (((((dst_value_g009_definitionT) = 2 * (ge_balance_positive_g009_definitionTentryvalue) /\ (ge_balance_negative_g009_definitionTentryvalue) = 0) \/ exists ge_signed_half_g009_definitionTentryvaluedecode. (((dst_value_g009_definitionT) = 2 * ge_signed_half_g009_definitionTentryvaluedecode + 1 /\ (ge_balance_positive_g009_definitionTentryvalue) = 0) /\ (ge_balance_negative_g009_definitionTentryvalue) = S ge_signed_half_g009_definitionTentryvaluedecode))) /\ ((dst_positive_g009_definitionT) + ge_balance_negative_g009_definitionTentryvalue = (dst_negative_g009_definitionT) + ge_balance_positive_g009_definitionTentryvalue))))))))) /\ (forall scp_row_g009_definition scp_column_g009_definition scp_first_g009_definition scp_second_g009_definition scp_value_g009_definition. (exists pvs_gap_g009_definitionrows. pvs_gap_g009_definitionrows + S (scp_row_g009_definition) = ((m))) -> (exists pvs_gap_g009_definitioncolumns. pvs_gap_g009_definitioncolumns + S (scp_column_g009_definition) = ((n))) -> (exists dst_positive_code_g009_definitionfirst dst_positive_scale_g009_definitionfirst dst_negative_code_g009_definitionfirst dst_negative_scale_g009_definitionfirst dst_positive_g009_definitionfirst dst_negative_g009_definitionfirst. ((((F)) = (((((dst_positive_code_g009_definitionfirst) + (dst_positive_scale_g009_definitionfirst)) * S ((dst_positive_code_g009_definitionfirst) + (dst_positive_scale_g009_definitionfirst)) + ((dst_positive_scale_g009_definitionfirst) + (dst_positive_scale_g009_definitionfirst))) + (((dst_negative_code_g009_definitionfirst) + (dst_negative_scale_g009_definitionfirst)) * S ((dst_negative_code_g009_definitionfirst) + (dst_negative_scale_g009_definitionfirst)) + ((dst_negative_scale_g009_definitionfirst) + (dst_negative_scale_g009_definitionfirst)))) * S ((((dst_positive_code_g009_definitionfirst) + (dst_positive_scale_g009_definitionfirst)) * S ((dst_positive_code_g009_definitionfirst) + (dst_positive_scale_g009_definitionfirst)) + ((dst_positive_scale_g009_definitionfirst) + (dst_positive_scale_g009_definitionfirst))) + (((dst_negative_code_g009_definitionfirst) + (dst_negative_scale_g009_definitionfirst)) * S ((dst_negative_code_g009_definitionfirst) + (dst_negative_scale_g009_definitionfirst)) + ((dst_negative_scale_g009_definitionfirst) + (dst_negative_scale_g009_definitionfirst)))) + ((((dst_negative_code_g009_definitionfirst) + (dst_negative_scale_g009_definitionfirst)) * S ((dst_negative_code_g009_definitionfirst) + (dst_negative_scale_g009_definitionfirst)) + ((dst_negative_scale_g009_definitionfirst) + (dst_negative_scale_g009_definitionfirst))) + (((dst_negative_code_g009_definitionfirst) + (dst_negative_scale_g009_definitionfirst)) * S ((dst_negative_code_g009_definitionfirst) + (dst_negative_scale_g009_definitionfirst)) + ((dst_negative_scale_g009_definitionfirst) + (dst_negative_scale_g009_definitionfirst)))))) /\ (((((exists ff_h_pvs_g009_definitionfirstpositive. ff_h_pvs_g009_definitionfirstpositive + S (dst_positive_g009_definitionfirst) = S ((S (scp_row_g009_definition)) * dst_positive_scale_g009_definitionfirst)) /\ exists ff_q_pvs_g009_definitionfirstpositive. dst_positive_code_g009_definitionfirst = ff_q_pvs_g009_definitionfirstpositive * S ((S (scp_row_g009_definition)) * dst_positive_scale_g009_definitionfirst) + (dst_positive_g009_definitionfirst))) /\ (((((exists ff_h_pvs_g009_definitionfirstnegative. ff_h_pvs_g009_definitionfirstnegative + S (dst_negative_g009_definitionfirst) = S ((S (scp_row_g009_definition)) * dst_negative_scale_g009_definitionfirst)) /\ exists ff_q_pvs_g009_definitionfirstnegative. dst_negative_code_g009_definitionfirst = ff_q_pvs_g009_definitionfirstnegative * S ((S (scp_row_g009_definition)) * dst_negative_scale_g009_definitionfirst) + (dst_negative_g009_definitionfirst))) /\ (exists ge_balance_positive_g009_definitionfirstvalue ge_balance_negative_g009_definitionfirstvalue. (((((scp_first_g009_definition) = 2 * (ge_balance_positive_g009_definitionfirstvalue) /\ (ge_balance_negative_g009_definitionfirstvalue) = 0) \/ exists ge_signed_half_g009_definitionfirstvaluedecode. (((scp_first_g009_definition) = 2 * ge_signed_half_g009_definitionfirstvaluedecode + 1 /\ (ge_balance_positive_g009_definitionfirstvalue) = 0) /\ (ge_balance_negative_g009_definitionfirstvalue) = S ge_signed_half_g009_definitionfirstvaluedecode))) /\ ((dst_positive_g009_definitionfirst) + ge_balance_negative_g009_definitionfirstvalue = (dst_negative_g009_definitionfirst) + ge_balance_positive_g009_definitionfirstvalue))))))))) -> (exists dst_positive_code_g009_definitionsecond dst_positive_scale_g009_definitionsecond dst_negative_code_g009_definitionsecond dst_negative_scale_g009_definitionsecond dst_positive_g009_definitionsecond dst_negative_g009_definitionsecond. ((((G)) = (((((dst_positive_code_g009_definitionsecond) + (dst_positive_scale_g009_definitionsecond)) * S ((dst_positive_code_g009_definitionsecond) + (dst_positive_scale_g009_definitionsecond)) + ((dst_positive_scale_g009_definitionsecond) + (dst_positive_scale_g009_definitionsecond))) + (((dst_negative_code_g009_definitionsecond) + (dst_negative_scale_g009_definitionsecond)) * S ((dst_negative_code_g009_definitionsecond) + (dst_negative_scale_g009_definitionsecond)) + ((dst_negative_scale_g009_definitionsecond) + (dst_negative_scale_g009_definitionsecond)))) * S ((((dst_positive_code_g009_definitionsecond) + (dst_positive_scale_g009_definitionsecond)) * S ((dst_positive_code_g009_definitionsecond) + (dst_positive_scale_g009_definitionsecond)) + ((dst_positive_scale_g009_definitionsecond) + (dst_positive_scale_g009_definitionsecond))) + (((dst_negative_code_g009_definitionsecond) + (dst_negative_scale_g009_definitionsecond)) * S ((dst_negative_code_g009_definitionsecond) + (dst_negative_scale_g009_definitionsecond)) + ((dst_negative_scale_g009_definitionsecond) + (dst_negative_scale_g009_definitionsecond)))) + ((((dst_negative_code_g009_definitionsecond) + (dst_negative_scale_g009_definitionsecond)) * S ((dst_negative_code_g009_definitionsecond) + (dst_negative_scale_g009_definitionsecond)) + ((dst_negative_scale_g009_definitionsecond) + (dst_negative_scale_g009_definitionsecond))) + (((dst_negative_code_g009_definitionsecond) + (dst_negative_scale_g009_definitionsecond)) * S ((dst_negative_code_g009_definitionsecond) + (dst_negative_scale_g009_definitionsecond)) + ((dst_negative_scale_g009_definitionsecond) + (dst_negative_scale_g009_definitionsecond)))))) /\ (((((exists ff_h_pvs_g009_definitionsecondpositive. ff_h_pvs_g009_definitionsecondpositive + S (dst_positive_g009_definitionsecond) = S ((S (scp_column_g009_definition)) * dst_positive_scale_g009_definitionsecond)) /\ exists ff_q_pvs_g009_definitionsecondpositive. dst_positive_code_g009_definitionsecond = ff_q_pvs_g009_definitionsecondpositive * S ((S (scp_column_g009_definition)) * dst_positive_scale_g009_definitionsecond) + (dst_positive_g009_definitionsecond))) /\ (((((exists ff_h_pvs_g009_definitionsecondnegative. ff_h_pvs_g009_definitionsecondnegative + S (dst_negative_g009_definitionsecond) = S ((S (scp_column_g009_definition)) * dst_negative_scale_g009_definitionsecond)) /\ exists ff_q_pvs_g009_definitionsecondnegative. dst_negative_code_g009_definitionsecond = ff_q_pvs_g009_definitionsecondnegative * S ((S (scp_column_g009_definition)) * dst_negative_scale_g009_definitionsecond) + (dst_negative_g009_definitionsecond))) /\ (exists ge_balance_positive_g009_definitionsecondvalue ge_balance_negative_g009_definitionsecondvalue. (((((scp_second_g009_definition) = 2 * (ge_balance_positive_g009_definitionsecondvalue) /\ (ge_balance_negative_g009_definitionsecondvalue) = 0) \/ exists ge_signed_half_g009_definitionsecondvaluedecode. (((scp_second_g009_definition) = 2 * ge_signed_half_g009_definitionsecondvaluedecode + 1 /\ (ge_balance_positive_g009_definitionsecondvalue) = 0) /\ (ge_balance_negative_g009_definitionsecondvalue) = S ge_signed_half_g009_definitionsecondvaluedecode))) /\ ((dst_positive_g009_definitionsecond) + ge_balance_negative_g009_definitionsecondvalue = (dst_negative_g009_definitionsecond) + ge_balance_positive_g009_definitionsecondvalue))))))))) -> (exists dst_positive_code_g009_definitionentry dst_positive_scale_g009_definitionentry dst_negative_code_g009_definitionentry dst_negative_scale_g009_definitionentry dst_positive_g009_definitionentry dst_negative_g009_definitionentry. ((((T)) = (((((dst_positive_code_g009_definitionentry) + (dst_positive_scale_g009_definitionentry)) * S ((dst_positive_code_g009_definitionentry) + (dst_positive_scale_g009_definitionentry)) + ((dst_positive_scale_g009_definitionentry) + (dst_positive_scale_g009_definitionentry))) + (((dst_negative_code_g009_definitionentry) + (dst_negative_scale_g009_definitionentry)) * S ((dst_negative_code_g009_definitionentry) + (dst_negative_scale_g009_definitionentry)) + ((dst_negative_scale_g009_definitionentry) + (dst_negative_scale_g009_definitionentry)))) * S ((((dst_positive_code_g009_definitionentry) + (dst_positive_scale_g009_definitionentry)) * S ((dst_positive_code_g009_definitionentry) + (dst_positive_scale_g009_definitionentry)) + ((dst_positive_scale_g009_definitionentry) + (dst_positive_scale_g009_definitionentry))) + (((dst_negative_code_g009_definitionentry) + (dst_negative_scale_g009_definitionentry)) * S ((dst_negative_code_g009_definitionentry) + (dst_negative_scale_g009_definitionentry)) + ((dst_negative_scale_g009_definitionentry) + (dst_negative_scale_g009_definitionentry)))) + ((((dst_negative_code_g009_definitionentry) + (dst_negative_scale_g009_definitionentry)) * S ((dst_negative_code_g009_definitionentry) + (dst_negative_scale_g009_definitionentry)) + ((dst_negative_scale_g009_definitionentry) + (dst_negative_scale_g009_definitionentry))) + (((dst_negative_code_g009_definitionentry) + (dst_negative_scale_g009_definitionentry)) * S ((dst_negative_code_g009_definitionentry) + (dst_negative_scale_g009_definitionentry)) + ((dst_negative_scale_g009_definitionentry) + (dst_negative_scale_g009_definitionentry)))))) /\ (((((exists ff_h_pvs_g009_definitionentrypositive. ff_h_pvs_g009_definitionentrypositive + S (dst_positive_g009_definitionentry) = S ((S ((((n))*(scp_row_g009_definition)+(scp_column_g009_definition)))) * dst_positive_scale_g009_definitionentry)) /\ exists ff_q_pvs_g009_definitionentrypositive. dst_positive_code_g009_definitionentry = ff_q_pvs_g009_definitionentrypositive * S ((S ((((n))*(scp_row_g009_definition)+(scp_column_g009_definition)))) * dst_positive_scale_g009_definitionentry) + (dst_positive_g009_definitionentry))) /\ (((((exists ff_h_pvs_g009_definitionentrynegative. ff_h_pvs_g009_definitionentrynegative + S (dst_negative_g009_definitionentry) = S ((S ((((n))*(scp_row_g009_definition)+(scp_column_g009_definition)))) * dst_negative_scale_g009_definitionentry)) /\ exists ff_q_pvs_g009_definitionentrynegative. dst_negative_code_g009_definitionentry = ff_q_pvs_g009_definitionentrynegative * S ((S ((((n))*(scp_row_g009_definition)+(scp_column_g009_definition)))) * dst_negative_scale_g009_definitionentry) + (dst_negative_g009_definitionentry))) /\ (exists ge_balance_positive_g009_definitionentryvalue ge_balance_negative_g009_definitionentryvalue. (((((scp_value_g009_definition) = 2 * (ge_balance_positive_g009_definitionentryvalue) /\ (ge_balance_negative_g009_definitionentryvalue) = 0) \/ exists ge_signed_half_g009_definitionentryvaluedecode. (((scp_value_g009_definition) = 2 * ge_signed_half_g009_definitionentryvaluedecode + 1 /\ (ge_balance_positive_g009_definitionentryvalue) = 0) /\ (ge_balance_negative_g009_definitionentryvalue) = S ge_signed_half_g009_definitionentryvaluedecode))) /\ ((dst_positive_g009_definitionentry) + ge_balance_negative_g009_definitionentryvalue = (dst_negative_g009_definitionentry) + ge_balance_positive_g009_definitionentryvalue))))))))) -> (exists sto_ap_g009_definitionmultiply sto_an_g009_definitionmultiply sto_bp_g009_definitionmultiply sto_bn_g009_definitionmultiply sto_cp_g009_definitionmultiply sto_cn_g009_definitionmultiply. (((((scp_first_g009_definition) = 2 * (sto_ap_g009_definitionmultiply) /\ (sto_an_g009_definitionmultiply) = 0) \/ exists ge_signed_half_g009_definitionmultiplyleft. (((scp_first_g009_definition) = 2 * ge_signed_half_g009_definitionmultiplyleft + 1 /\ (sto_ap_g009_definitionmultiply) = 0) /\ (sto_an_g009_definitionmultiply) = S ge_signed_half_g009_definitionmultiplyleft))) /\ ((((((scp_second_g009_definition) = 2 * (sto_bp_g009_definitionmultiply) /\ (sto_bn_g009_definitionmultiply) = 0) \/ exists ge_signed_half_g009_definitionmultiplyright. (((scp_second_g009_definition) = 2 * ge_signed_half_g009_definitionmultiplyright + 1 /\ (sto_bp_g009_definitionmultiply) = 0) /\ (sto_bn_g009_definitionmultiply) = S ge_signed_half_g009_definitionmultiplyright))) /\ ((((((scp_value_g009_definition) = 2 * (sto_cp_g009_definitionmultiply) /\ (sto_cn_g009_definitionmultiply) = 0) \/ exists ge_signed_half_g009_definitionmultiplyoutput. (((scp_value_g009_definition) = 2 * ge_signed_half_g009_definitionmultiplyoutput + 1 /\ (sto_cp_g009_definitionmultiply) = 0) /\ (sto_cn_g009_definitionmultiply) = S ge_signed_half_g009_definitionmultiplyoutput))) /\ ((sto_ap_g009_definitionmultiply * sto_bp_g009_definitionmultiply + sto_an_g009_definitionmultiply * sto_bn_g009_definitionmultiply) + sto_cn_g009_definitionmultiply = (sto_ap_g009_definitionmultiply * sto_bn_g009_definitionmultiply + sto_an_g009_definitionmultiply * sto_bp_g009_definitionmultiply) + sto_cp_g009_definitionmultiply)))))))))))))

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