DirichletDivisorGridWitness(F,G,m,n,i,z,d,e,a,b)

((((i))=((S ((n)))*((d))+((e)))) /\ (((exists pvs_gap_g009_definitionrow. pvs_gap_g009_definitionrow + S ((d)) = (S ((m)))) /\ (((exists pvs_gap_g009_definitioncolumn. pvs_gap_g009_definitioncolumn + S ((e)) = (S ((n)))) /\ (((((~(((d))=0)) /\ (((~(((e))=0)) /\ (((exists pvs_factor_g009_definitionpairleft. ((m)) = ((d)) * pvs_factor_g009_definitionpairleft) /\ (((exists pvs_factor_g009_definitionpairright. ((n)) = ((e)) * pvs_factor_g009_definitionpairright) /\ ((((d))*((e)))=((d))*((e))))))))))) /\ ((((((~(((d))=0)) /\ (exists dc_quotient_g009_definitionleft dc_left_g009_definitionleft dc_right_g009_definitionleft. ((((m))=((d))*dc_quotient_g009_definitionleft) /\ (((exists dst_positive_code_g009_definitionleftleft dst_positive_scale_g009_definitionleftleft dst_negative_code_g009_definitionleftleft dst_negative_scale_g009_definitionleftleft dst_positive_g009_definitionleftleft dst_negative_g009_definitionleftleft. ((((F)) = (((((dst_positive_code_g009_definitionleftleft) + (dst_positive_scale_g009_definitionleftleft)) * S ((dst_positive_code_g009_definitionleftleft) + (dst_positive_scale_g009_definitionleftleft)) + ((dst_positive_scale_g009_definitionleftleft) + (dst_positive_scale_g009_definitionleftleft))) + (((dst_negative_code_g009_definitionleftleft) + (dst_negative_scale_g009_definitionleftleft)) * S ((dst_negative_code_g009_definitionleftleft) + (dst_negative_scale_g009_definitionleftleft)) + ((dst_negative_scale_g009_definitionleftleft) + (dst_negative_scale_g009_definitionleftleft)))) * S ((((dst_positive_code_g009_definitionleftleft) + (dst_positive_scale_g009_definitionleftleft)) * S ((dst_positive_code_g009_definitionleftleft) + (dst_positive_scale_g009_definitionleftleft)) + ((dst_positive_scale_g009_definitionleftleft) + (dst_positive_scale_g009_definitionleftleft))) + (((dst_negative_code_g009_definitionleftleft) + (dst_negative_scale_g009_definitionleftleft)) * S ((dst_negative_code_g009_definitionleftleft) + (dst_negative_scale_g009_definitionleftleft)) + ((dst_negative_scale_g009_definitionleftleft) + (dst_negative_scale_g009_definitionleftleft)))) + ((((dst_negative_code_g009_definitionleftleft) + (dst_negative_scale_g009_definitionleftleft)) * S ((dst_negative_code_g009_definitionleftleft) + (dst_negative_scale_g009_definitionleftleft)) + ((dst_negative_scale_g009_definitionleftleft) + (dst_negative_scale_g009_definitionleftleft))) + (((dst_negative_code_g009_definitionleftleft) + (dst_negative_scale_g009_definitionleftleft)) * S ((dst_negative_code_g009_definitionleftleft) + (dst_negative_scale_g009_definitionleftleft)) + ((dst_negative_scale_g009_definitionleftleft) + (dst_negative_scale_g009_definitionleftleft)))))) /\ (((((exists ff_h_pvs_g009_definitionleftleftpositive. ff_h_pvs_g009_definitionleftleftpositive + S (dst_positive_g009_definitionleftleft) = S ((S ((d))) * dst_positive_scale_g009_definitionleftleft)) /\ exists ff_q_pvs_g009_definitionleftleftpositive. dst_positive_code_g009_definitionleftleft = ff_q_pvs_g009_definitionleftleftpositive * S ((S ((d))) * dst_positive_scale_g009_definitionleftleft) + (dst_positive_g009_definitionleftleft))) /\ (((((exists ff_h_pvs_g009_definitionleftleftnegative. ff_h_pvs_g009_definitionleftleftnegative + S (dst_negative_g009_definitionleftleft) = S ((S ((d))) * dst_negative_scale_g009_definitionleftleft)) /\ exists ff_q_pvs_g009_definitionleftleftnegative. dst_negative_code_g009_definitionleftleft = ff_q_pvs_g009_definitionleftleftnegative * S ((S ((d))) * dst_negative_scale_g009_definitionleftleft) + (dst_negative_g009_definitionleftleft))) /\ (exists ge_balance_positive_g009_definitionleftleftvalue ge_balance_negative_g009_definitionleftleftvalue. (((((dc_left_g009_definitionleft) = 2 * (ge_balance_positive_g009_definitionleftleftvalue) /\ (ge_balance_negative_g009_definitionleftleftvalue) = 0) \/ exists ge_signed_half_g009_definitionleftleftvaluedecode. (((dc_left_g009_definitionleft) = 2 * ge_signed_half_g009_definitionleftleftvaluedecode + 1 /\ (ge_balance_positive_g009_definitionleftleftvalue) = 0) /\ (ge_balance_negative_g009_definitionleftleftvalue) = S ge_signed_half_g009_definitionleftleftvaluedecode))) /\ ((dst_positive_g009_definitionleftleft) + ge_balance_negative_g009_definitionleftleftvalue = (dst_negative_g009_definitionleftleft) + ge_balance_positive_g009_definitionleftleftvalue))))))))) /\ (((exists dst_positive_code_g009_definitionleftright dst_positive_scale_g009_definitionleftright dst_negative_code_g009_definitionleftright dst_negative_scale_g009_definitionleftright dst_positive_g009_definitionleftright dst_negative_g009_definitionleftright. ((((G)) = (((((dst_positive_code_g009_definitionleftright) + (dst_positive_scale_g009_definitionleftright)) * S ((dst_positive_code_g009_definitionleftright) + (dst_positive_scale_g009_definitionleftright)) + ((dst_positive_scale_g009_definitionleftright) + (dst_positive_scale_g009_definitionleftright))) + (((dst_negative_code_g009_definitionleftright) + (dst_negative_scale_g009_definitionleftright)) * S ((dst_negative_code_g009_definitionleftright) + (dst_negative_scale_g009_definitionleftright)) + ((dst_negative_scale_g009_definitionleftright) + (dst_negative_scale_g009_definitionleftright)))) * S ((((dst_positive_code_g009_definitionleftright) + (dst_positive_scale_g009_definitionleftright)) * S ((dst_positive_code_g009_definitionleftright) + (dst_positive_scale_g009_definitionleftright)) + ((dst_positive_scale_g009_definitionleftright) + (dst_positive_scale_g009_definitionleftright))) + (((dst_negative_code_g009_definitionleftright) + (dst_negative_scale_g009_definitionleftright)) * S ((dst_negative_code_g009_definitionleftright) + (dst_negative_scale_g009_definitionleftright)) + ((dst_negative_scale_g009_definitionleftright) + (dst_negative_scale_g009_definitionleftright)))) + ((((dst_negative_code_g009_definitionleftright) + (dst_negative_scale_g009_definitionleftright)) * S ((dst_negative_code_g009_definitionleftright) + (dst_negative_scale_g009_definitionleftright)) + ((dst_negative_scale_g009_definitionleftright) + (dst_negative_scale_g009_definitionleftright))) + (((dst_negative_code_g009_definitionleftright) + (dst_negative_scale_g009_definitionleftright)) * S ((dst_negative_code_g009_definitionleftright) + (dst_negative_scale_g009_definitionleftright)) + ((dst_negative_scale_g009_definitionleftright) + (dst_negative_scale_g009_definitionleftright)))))) /\ (((((exists ff_h_pvs_g009_definitionleftrightpositive. ff_h_pvs_g009_definitionleftrightpositive + S (dst_positive_g009_definitionleftright) = S ((S (dc_quotient_g009_definitionleft)) * dst_positive_scale_g009_definitionleftright)) /\ exists ff_q_pvs_g009_definitionleftrightpositive. dst_positive_code_g009_definitionleftright = ff_q_pvs_g009_definitionleftrightpositive * S ((S (dc_quotient_g009_definitionleft)) * dst_positive_scale_g009_definitionleftright) + (dst_positive_g009_definitionleftright))) /\ (((((exists ff_h_pvs_g009_definitionleftrightnegative. ff_h_pvs_g009_definitionleftrightnegative + S (dst_negative_g009_definitionleftright) = S ((S (dc_quotient_g009_definitionleft)) * dst_negative_scale_g009_definitionleftright)) /\ exists ff_q_pvs_g009_definitionleftrightnegative. dst_negative_code_g009_definitionleftright = ff_q_pvs_g009_definitionleftrightnegative * S ((S (dc_quotient_g009_definitionleft)) * dst_negative_scale_g009_definitionleftright) + (dst_negative_g009_definitionleftright))) /\ (exists ge_balance_positive_g009_definitionleftrightvalue ge_balance_negative_g009_definitionleftrightvalue. (((((dc_right_g009_definitionleft) = 2 * (ge_balance_positive_g009_definitionleftrightvalue) /\ (ge_balance_negative_g009_definitionleftrightvalue) = 0) \/ exists ge_signed_half_g009_definitionleftrightvaluedecode. (((dc_right_g009_definitionleft) = 2 * ge_signed_half_g009_definitionleftrightvaluedecode + 1 /\ (ge_balance_positive_g009_definitionleftrightvalue) = 0) /\ (ge_balance_negative_g009_definitionleftrightvalue) = S ge_signed_half_g009_definitionleftrightvaluedecode))) /\ ((dst_positive_g009_definitionleftright) + ge_balance_negative_g009_definitionleftrightvalue = (dst_negative_g009_definitionleftright) + ge_balance_positive_g009_definitionleftrightvalue))))))))) /\ (exists sto_ap_g009_definitionleftproduct sto_an_g009_definitionleftproduct sto_bp_g009_definitionleftproduct sto_bn_g009_definitionleftproduct sto_cp_g009_definitionleftproduct sto_cn_g009_definitionleftproduct. (((((dc_left_g009_definitionleft) = 2 * (sto_ap_g009_definitionleftproduct) /\ (sto_an_g009_definitionleftproduct) = 0) \/ exists ge_signed_half_g009_definitionleftproductleft. (((dc_left_g009_definitionleft) = 2 * ge_signed_half_g009_definitionleftproductleft + 1 /\ (sto_ap_g009_definitionleftproduct) = 0) /\ (sto_an_g009_definitionleftproduct) = S ge_signed_half_g009_definitionleftproductleft))) /\ ((((((dc_right_g009_definitionleft) = 2 * (sto_bp_g009_definitionleftproduct) /\ (sto_bn_g009_definitionleftproduct) = 0) \/ exists ge_signed_half_g009_definitionleftproductright. (((dc_right_g009_definitionleft) = 2 * ge_signed_half_g009_definitionleftproductright + 1 /\ (sto_bp_g009_definitionleftproduct) = 0) /\ (sto_bn_g009_definitionleftproduct) = S ge_signed_half_g009_definitionleftproductright))) /\ (((((((a)) = 2 * (sto_cp_g009_definitionleftproduct) /\ (sto_cn_g009_definitionleftproduct) = 0) \/ exists ge_signed_half_g009_definitionleftproductoutput. ((((a)) = 2 * ge_signed_half_g009_definitionleftproductoutput + 1 /\ (sto_cp_g009_definitionleftproduct) = 0) /\ (sto_cn_g009_definitionleftproduct) = S ge_signed_half_g009_definitionleftproductoutput))) /\ ((sto_ap_g009_definitionleftproduct * sto_bp_g009_definitionleftproduct + sto_an_g009_definitionleftproduct * sto_bn_g009_definitionleftproduct) + sto_cn_g009_definitionleftproduct = (sto_ap_g009_definitionleftproduct * sto_bn_g009_definitionleftproduct + sto_an_g009_definitionleftproduct * sto_bp_g009_definitionleftproduct) + sto_cp_g009_definitionleftproduct))))))))))))))) \/ (((((d))=0 \/ ~(exists pvs_factor_g009_definitionleftnondivisor. ((m)) = ((d)) * pvs_factor_g009_definitionleftnondivisor)) /\ (((a))=0)))) /\ ((((((~(((e))=0)) /\ (exists dc_quotient_g009_definitionright dc_left_g009_definitionright dc_right_g009_definitionright. ((((n))=((e))*dc_quotient_g009_definitionright) /\ (((exists dst_positive_code_g009_definitionrightleft dst_positive_scale_g009_definitionrightleft dst_negative_code_g009_definitionrightleft dst_negative_scale_g009_definitionrightleft dst_positive_g009_definitionrightleft dst_negative_g009_definitionrightleft. ((((F)) = (((((dst_positive_code_g009_definitionrightleft) + (dst_positive_scale_g009_definitionrightleft)) * S ((dst_positive_code_g009_definitionrightleft) + (dst_positive_scale_g009_definitionrightleft)) + ((dst_positive_scale_g009_definitionrightleft) + (dst_positive_scale_g009_definitionrightleft))) + (((dst_negative_code_g009_definitionrightleft) + (dst_negative_scale_g009_definitionrightleft)) * S ((dst_negative_code_g009_definitionrightleft) + (dst_negative_scale_g009_definitionrightleft)) + ((dst_negative_scale_g009_definitionrightleft) + (dst_negative_scale_g009_definitionrightleft)))) * S ((((dst_positive_code_g009_definitionrightleft) + (dst_positive_scale_g009_definitionrightleft)) * S ((dst_positive_code_g009_definitionrightleft) + (dst_positive_scale_g009_definitionrightleft)) + ((dst_positive_scale_g009_definitionrightleft) + (dst_positive_scale_g009_definitionrightleft))) + (((dst_negative_code_g009_definitionrightleft) + (dst_negative_scale_g009_definitionrightleft)) * S ((dst_negative_code_g009_definitionrightleft) + (dst_negative_scale_g009_definitionrightleft)) + ((dst_negative_scale_g009_definitionrightleft) + (dst_negative_scale_g009_definitionrightleft)))) + ((((dst_negative_code_g009_definitionrightleft) + (dst_negative_scale_g009_definitionrightleft)) * S ((dst_negative_code_g009_definitionrightleft) + (dst_negative_scale_g009_definitionrightleft)) + ((dst_negative_scale_g009_definitionrightleft) + (dst_negative_scale_g009_definitionrightleft))) + (((dst_negative_code_g009_definitionrightleft) + (dst_negative_scale_g009_definitionrightleft)) * S ((dst_negative_code_g009_definitionrightleft) + (dst_negative_scale_g009_definitionrightleft)) + ((dst_negative_scale_g009_definitionrightleft) + (dst_negative_scale_g009_definitionrightleft)))))) /\ (((((exists ff_h_pvs_g009_definitionrightleftpositive. ff_h_pvs_g009_definitionrightleftpositive + S (dst_positive_g009_definitionrightleft) = S ((S ((e))) * dst_positive_scale_g009_definitionrightleft)) /\ exists ff_q_pvs_g009_definitionrightleftpositive. dst_positive_code_g009_definitionrightleft = ff_q_pvs_g009_definitionrightleftpositive * S ((S ((e))) * dst_positive_scale_g009_definitionrightleft) + (dst_positive_g009_definitionrightleft))) /\ (((((exists ff_h_pvs_g009_definitionrightleftnegative. ff_h_pvs_g009_definitionrightleftnegative + S (dst_negative_g009_definitionrightleft) = S ((S ((e))) * dst_negative_scale_g009_definitionrightleft)) /\ exists ff_q_pvs_g009_definitionrightleftnegative. dst_negative_code_g009_definitionrightleft = ff_q_pvs_g009_definitionrightleftnegative * S ((S ((e))) * dst_negative_scale_g009_definitionrightleft) + (dst_negative_g009_definitionrightleft))) /\ (exists ge_balance_positive_g009_definitionrightleftvalue ge_balance_negative_g009_definitionrightleftvalue. (((((dc_left_g009_definitionright) = 2 * (ge_balance_positive_g009_definitionrightleftvalue) /\ (ge_balance_negative_g009_definitionrightleftvalue) = 0) \/ exists ge_signed_half_g009_definitionrightleftvaluedecode. (((dc_left_g009_definitionright) = 2 * ge_signed_half_g009_definitionrightleftvaluedecode + 1 /\ (ge_balance_positive_g009_definitionrightleftvalue) = 0) /\ (ge_balance_negative_g009_definitionrightleftvalue) = S ge_signed_half_g009_definitionrightleftvaluedecode))) /\ ((dst_positive_g009_definitionrightleft) + ge_balance_negative_g009_definitionrightleftvalue = (dst_negative_g009_definitionrightleft) + ge_balance_positive_g009_definitionrightleftvalue))))))))) /\ (((exists dst_positive_code_g009_definitionrightright dst_positive_scale_g009_definitionrightright dst_negative_code_g009_definitionrightright dst_negative_scale_g009_definitionrightright dst_positive_g009_definitionrightright dst_negative_g009_definitionrightright. ((((G)) = (((((dst_positive_code_g009_definitionrightright) + (dst_positive_scale_g009_definitionrightright)) * S ((dst_positive_code_g009_definitionrightright) + (dst_positive_scale_g009_definitionrightright)) + ((dst_positive_scale_g009_definitionrightright) + (dst_positive_scale_g009_definitionrightright))) + (((dst_negative_code_g009_definitionrightright) + (dst_negative_scale_g009_definitionrightright)) * S ((dst_negative_code_g009_definitionrightright) + (dst_negative_scale_g009_definitionrightright)) + ((dst_negative_scale_g009_definitionrightright) + (dst_negative_scale_g009_definitionrightright)))) * S ((((dst_positive_code_g009_definitionrightright) + (dst_positive_scale_g009_definitionrightright)) * S ((dst_positive_code_g009_definitionrightright) + (dst_positive_scale_g009_definitionrightright)) + ((dst_positive_scale_g009_definitionrightright) + (dst_positive_scale_g009_definitionrightright))) + (((dst_negative_code_g009_definitionrightright) + (dst_negative_scale_g009_definitionrightright)) * S ((dst_negative_code_g009_definitionrightright) + (dst_negative_scale_g009_definitionrightright)) + ((dst_negative_scale_g009_definitionrightright) + (dst_negative_scale_g009_definitionrightright)))) + ((((dst_negative_code_g009_definitionrightright) + (dst_negative_scale_g009_definitionrightright)) * S ((dst_negative_code_g009_definitionrightright) + (dst_negative_scale_g009_definitionrightright)) + ((dst_negative_scale_g009_definitionrightright) + (dst_negative_scale_g009_definitionrightright))) + (((dst_negative_code_g009_definitionrightright) + (dst_negative_scale_g009_definitionrightright)) * S ((dst_negative_code_g009_definitionrightright) + (dst_negative_scale_g009_definitionrightright)) + ((dst_negative_scale_g009_definitionrightright) + (dst_negative_scale_g009_definitionrightright)))))) /\ (((((exists ff_h_pvs_g009_definitionrightrightpositive. ff_h_pvs_g009_definitionrightrightpositive + S (dst_positive_g009_definitionrightright) = S ((S (dc_quotient_g009_definitionright)) * dst_positive_scale_g009_definitionrightright)) /\ exists ff_q_pvs_g009_definitionrightrightpositive. dst_positive_code_g009_definitionrightright = ff_q_pvs_g009_definitionrightrightpositive * S ((S (dc_quotient_g009_definitionright)) * dst_positive_scale_g009_definitionrightright) + (dst_positive_g009_definitionrightright))) /\ (((((exists ff_h_pvs_g009_definitionrightrightnegative. ff_h_pvs_g009_definitionrightrightnegative + S (dst_negative_g009_definitionrightright) = S ((S (dc_quotient_g009_definitionright)) * dst_negative_scale_g009_definitionrightright)) /\ exists ff_q_pvs_g009_definitionrightrightnegative. dst_negative_code_g009_definitionrightright = ff_q_pvs_g009_definitionrightrightnegative * S ((S (dc_quotient_g009_definitionright)) * dst_negative_scale_g009_definitionrightright) + (dst_negative_g009_definitionrightright))) /\ (exists ge_balance_positive_g009_definitionrightrightvalue ge_balance_negative_g009_definitionrightrightvalue. (((((dc_right_g009_definitionright) = 2 * (ge_balance_positive_g009_definitionrightrightvalue) /\ (ge_balance_negative_g009_definitionrightrightvalue) = 0) \/ exists ge_signed_half_g009_definitionrightrightvaluedecode. (((dc_right_g009_definitionright) = 2 * ge_signed_half_g009_definitionrightrightvaluedecode + 1 /\ (ge_balance_positive_g009_definitionrightrightvalue) = 0) /\ (ge_balance_negative_g009_definitionrightrightvalue) = S ge_signed_half_g009_definitionrightrightvaluedecode))) /\ ((dst_positive_g009_definitionrightright) + ge_balance_negative_g009_definitionrightrightvalue = (dst_negative_g009_definitionrightright) + ge_balance_positive_g009_definitionrightrightvalue))))))))) /\ (exists sto_ap_g009_definitionrightproduct sto_an_g009_definitionrightproduct sto_bp_g009_definitionrightproduct sto_bn_g009_definitionrightproduct sto_cp_g009_definitionrightproduct sto_cn_g009_definitionrightproduct. (((((dc_left_g009_definitionright) = 2 * (sto_ap_g009_definitionrightproduct) /\ (sto_an_g009_definitionrightproduct) = 0) \/ exists ge_signed_half_g009_definitionrightproductleft. (((dc_left_g009_definitionright) = 2 * ge_signed_half_g009_definitionrightproductleft + 1 /\ (sto_ap_g009_definitionrightproduct) = 0) /\ (sto_an_g009_definitionrightproduct) = S ge_signed_half_g009_definitionrightproductleft))) /\ ((((((dc_right_g009_definitionright) = 2 * (sto_bp_g009_definitionrightproduct) /\ (sto_bn_g009_definitionrightproduct) = 0) \/ exists ge_signed_half_g009_definitionrightproductright. (((dc_right_g009_definitionright) = 2 * ge_signed_half_g009_definitionrightproductright + 1 /\ (sto_bp_g009_definitionrightproduct) = 0) /\ (sto_bn_g009_definitionrightproduct) = S ge_signed_half_g009_definitionrightproductright))) /\ (((((((b)) = 2 * (sto_cp_g009_definitionrightproduct) /\ (sto_cn_g009_definitionrightproduct) = 0) \/ exists ge_signed_half_g009_definitionrightproductoutput. ((((b)) = 2 * ge_signed_half_g009_definitionrightproductoutput + 1 /\ (sto_cp_g009_definitionrightproduct) = 0) /\ (sto_cn_g009_definitionrightproduct) = S ge_signed_half_g009_definitionrightproductoutput))) /\ ((sto_ap_g009_definitionrightproduct * sto_bp_g009_definitionrightproduct + sto_an_g009_definitionrightproduct * sto_bn_g009_definitionrightproduct) + sto_cn_g009_definitionrightproduct = (sto_ap_g009_definitionrightproduct * sto_bn_g009_definitionrightproduct + sto_an_g009_definitionrightproduct * sto_bp_g009_definitionrightproduct) + sto_cp_g009_definitionrightproduct))))))))))))))) \/ (((((e))=0 \/ ~(exists pvs_factor_g009_definitionrightnondivisor. ((n)) = ((e)) * pvs_factor_g009_definitionrightnondivisor)) /\ (((b))=0)))) /\ (exists sto_ap_g009_definitionproduct sto_an_g009_definitionproduct sto_bp_g009_definitionproduct sto_bn_g009_definitionproduct sto_cp_g009_definitionproduct sto_cn_g009_definitionproduct. ((((((a)) = 2 * (sto_ap_g009_definitionproduct) /\ (sto_an_g009_definitionproduct) = 0) \/ exists ge_signed_half_g009_definitionproductleft. ((((a)) = 2 * ge_signed_half_g009_definitionproductleft + 1 /\ (sto_ap_g009_definitionproduct) = 0) /\ (sto_an_g009_definitionproduct) = S ge_signed_half_g009_definitionproductleft))) /\ (((((((b)) = 2 * (sto_bp_g009_definitionproduct) /\ (sto_bn_g009_definitionproduct) = 0) \/ exists ge_signed_half_g009_definitionproductright. ((((b)) = 2 * ge_signed_half_g009_definitionproductright + 1 /\ (sto_bp_g009_definitionproduct) = 0) /\ (sto_bn_g009_definitionproduct) = S ge_signed_half_g009_definitionproductright))) /\ (((((((z)) = 2 * (sto_cp_g009_definitionproduct) /\ (sto_cn_g009_definitionproduct) = 0) \/ exists ge_signed_half_g009_definitionproductoutput. ((((z)) = 2 * ge_signed_half_g009_definitionproductoutput + 1 /\ (sto_cp_g009_definitionproduct) = 0) /\ (sto_cn_g009_definitionproduct) = S ge_signed_half_g009_definitionproductoutput))) /\ ((sto_ap_g009_definitionproduct * sto_bp_g009_definitionproduct + sto_an_g009_definitionproduct * sto_bn_g009_definitionproduct) + sto_cn_g009_definitionproduct = (sto_ap_g009_definitionproduct * sto_bn_g009_definitionproduct + sto_an_g009_definitionproduct * sto_bp_g009_definitionproduct) + sto_cp_g009_definitionproduct))))))))))))))))))

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