DirichletFlatPrefix(F,G,H,n,l,T)

((exists dst_positive_code_dirichlettable dst_positive_scale_dirichlettable dst_negative_code_dirichlettable dst_negative_scale_dirichlettable. ((((T)) = (((((dst_positive_code_dirichlettable) + (dst_positive_scale_dirichlettable)) * S ((dst_positive_code_dirichlettable) + (dst_positive_scale_dirichlettable)) + ((dst_positive_scale_dirichlettable) + (dst_positive_scale_dirichlettable))) + (((dst_negative_code_dirichlettable) + (dst_negative_scale_dirichlettable)) * S ((dst_negative_code_dirichlettable) + (dst_negative_scale_dirichlettable)) + ((dst_negative_scale_dirichlettable) + (dst_negative_scale_dirichlettable)))) * S ((((dst_positive_code_dirichlettable) + (dst_positive_scale_dirichlettable)) * S ((dst_positive_code_dirichlettable) + (dst_positive_scale_dirichlettable)) + ((dst_positive_scale_dirichlettable) + (dst_positive_scale_dirichlettable))) + (((dst_negative_code_dirichlettable) + (dst_negative_scale_dirichlettable)) * S ((dst_negative_code_dirichlettable) + (dst_negative_scale_dirichlettable)) + ((dst_negative_scale_dirichlettable) + (dst_negative_scale_dirichlettable)))) + ((((dst_negative_code_dirichlettable) + (dst_negative_scale_dirichlettable)) * S ((dst_negative_code_dirichlettable) + (dst_negative_scale_dirichlettable)) + ((dst_negative_scale_dirichlettable) + (dst_negative_scale_dirichlettable))) + (((dst_negative_code_dirichlettable) + (dst_negative_scale_dirichlettable)) * S ((dst_negative_code_dirichlettable) + (dst_negative_scale_dirichlettable)) + ((dst_negative_scale_dirichlettable) + (dst_negative_scale_dirichlettable)))))) /\ (forall dst_index_dirichlettable. (exists pvs_le_gap_dirichlettabledomain. pvs_le_gap_dirichlettabledomain + (dst_index_dirichlettable) = ((l))) -> exists dst_positive_dirichlettable dst_negative_dirichlettable dst_value_dirichlettable. ((((exists ff_h_pvs_dirichlettableentrypositive. ff_h_pvs_dirichlettableentrypositive + S (dst_positive_dirichlettable) = S ((S (dst_index_dirichlettable)) * dst_positive_scale_dirichlettable)) /\ exists ff_q_pvs_dirichlettableentrypositive. dst_positive_code_dirichlettable = ff_q_pvs_dirichlettableentrypositive * S ((S (dst_index_dirichlettable)) * dst_positive_scale_dirichlettable) + (dst_positive_dirichlettable))) /\ (((((exists ff_h_pvs_dirichlettableentrynegative. ff_h_pvs_dirichlettableentrynegative + S (dst_negative_dirichlettable) = S ((S (dst_index_dirichlettable)) * dst_negative_scale_dirichlettable)) /\ exists ff_q_pvs_dirichlettableentrynegative. dst_negative_code_dirichlettable = ff_q_pvs_dirichlettableentrynegative * S ((S (dst_index_dirichlettable)) * dst_negative_scale_dirichlettable) + (dst_negative_dirichlettable))) /\ (exists ge_balance_positive_dirichlettableentryvalue ge_balance_negative_dirichlettableentryvalue. (((((dst_value_dirichlettable) = 2 * (ge_balance_positive_dirichlettableentryvalue) /\ (ge_balance_negative_dirichlettableentryvalue) = 0) \/ exists ge_signed_half_dirichlettableentryvaluedecode. (((dst_value_dirichlettable) = 2 * ge_signed_half_dirichlettableentryvaluedecode + 1 /\ (ge_balance_positive_dirichlettableentryvalue) = 0) /\ (ge_balance_negative_dirichlettableentryvalue) = S ge_signed_half_dirichlettableentryvaluedecode))) /\ ((dst_positive_dirichlettable) + ge_balance_negative_dirichlettableentryvalue = (dst_negative_dirichlettable) + ge_balance_positive_dirichlettableentryvalue))))))))) /\ (forall dfg_flat_index_dirichlet dfg_flat_value_dirichlet. (exists pvs_le_gap_dirichletbound. pvs_le_gap_dirichletbound + (dfg_flat_index_dirichlet) = ((l))) -> (exists dst_positive_code_dirichletlookup dst_positive_scale_dirichletlookup dst_negative_code_dirichletlookup dst_negative_scale_dirichletlookup dst_positive_dirichletlookup dst_negative_dirichletlookup. ((((T)) = (((((dst_positive_code_dirichletlookup) + (dst_positive_scale_dirichletlookup)) * S ((dst_positive_code_dirichletlookup) + (dst_positive_scale_dirichletlookup)) + ((dst_positive_scale_dirichletlookup) + (dst_positive_scale_dirichletlookup))) + (((dst_negative_code_dirichletlookup) + (dst_negative_scale_dirichletlookup)) * S ((dst_negative_code_dirichletlookup) + (dst_negative_scale_dirichletlookup)) + ((dst_negative_scale_dirichletlookup) + (dst_negative_scale_dirichletlookup)))) * S ((((dst_positive_code_dirichletlookup) + (dst_positive_scale_dirichletlookup)) * S ((dst_positive_code_dirichletlookup) + (dst_positive_scale_dirichletlookup)) + ((dst_positive_scale_dirichletlookup) + (dst_positive_scale_dirichletlookup))) + (((dst_negative_code_dirichletlookup) + (dst_negative_scale_dirichletlookup)) * S ((dst_negative_code_dirichletlookup) + (dst_negative_scale_dirichletlookup)) + ((dst_negative_scale_dirichletlookup) + (dst_negative_scale_dirichletlookup)))) + ((((dst_negative_code_dirichletlookup) + (dst_negative_scale_dirichletlookup)) * S ((dst_negative_code_dirichletlookup) + (dst_negative_scale_dirichletlookup)) + ((dst_negative_scale_dirichletlookup) + (dst_negative_scale_dirichletlookup))) + (((dst_negative_code_dirichletlookup) + (dst_negative_scale_dirichletlookup)) * S ((dst_negative_code_dirichletlookup) + (dst_negative_scale_dirichletlookup)) + ((dst_negative_scale_dirichletlookup) + (dst_negative_scale_dirichletlookup)))))) /\ (((((exists ff_h_pvs_dirichletlookuppositive. ff_h_pvs_dirichletlookuppositive + S (dst_positive_dirichletlookup) = S ((S (dfg_flat_index_dirichlet)) * dst_positive_scale_dirichletlookup)) /\ exists ff_q_pvs_dirichletlookuppositive. dst_positive_code_dirichletlookup = ff_q_pvs_dirichletlookuppositive * S ((S (dfg_flat_index_dirichlet)) * dst_positive_scale_dirichletlookup) + (dst_positive_dirichletlookup))) /\ (((((exists ff_h_pvs_dirichletlookupnegative. ff_h_pvs_dirichletlookupnegative + S (dst_negative_dirichletlookup) = S ((S (dfg_flat_index_dirichlet)) * dst_negative_scale_dirichletlookup)) /\ exists ff_q_pvs_dirichletlookupnegative. dst_negative_code_dirichletlookup = ff_q_pvs_dirichletlookupnegative * S ((S (dfg_flat_index_dirichlet)) * dst_negative_scale_dirichletlookup) + (dst_negative_dirichletlookup))) /\ (exists ge_balance_positive_dirichletlookupvalue ge_balance_negative_dirichletlookupvalue. (((((dfg_flat_value_dirichlet) = 2 * (ge_balance_positive_dirichletlookupvalue) /\ (ge_balance_negative_dirichletlookupvalue) = 0) \/ exists ge_signed_half_dirichletlookupvaluedecode. (((dfg_flat_value_dirichlet) = 2 * ge_signed_half_dirichletlookupvaluedecode + 1 /\ (ge_balance_positive_dirichletlookupvalue) = 0) /\ (ge_balance_negative_dirichletlookupvalue) = S ge_signed_half_dirichletlookupvaluedecode))) /\ ((dst_positive_dirichletlookup) + ge_balance_negative_dirichletlookupvalue = (dst_negative_dirichletlookup) + ge_balance_positive_dirichletlookupvalue))))))))) -> (exists dfg_flat_row_dirichletentry dfg_flat_column_dirichletentry. (((dfg_flat_index_dirichlet)=((S ((n)))*(dfg_flat_row_dirichletentry)+(dfg_flat_column_dirichletentry))) /\ (((exists pvs_gap_dirichletentryremainder. pvs_gap_dirichletentryremainder + S (dfg_flat_column_dirichletentry) = (S ((n)))) /\ ((((~((dfg_flat_row_dirichletentry)=0)) /\ (((~((dfg_flat_column_dirichletentry)=0)) /\ (exists dfg_middle_dirichletentrycell dfg_first_dirichletentrycell dfg_last_dirichletentrycell dfg_value_dirichletentrycell. ((((n))=((dfg_flat_row_dirichletentry)*(dfg_flat_column_dirichletentry))*dfg_middle_dirichletentrycell) /\ (((exists dst_positive_code_dirichletentrycellfirst dst_positive_scale_dirichletentrycellfirst dst_negative_code_dirichletentrycellfirst dst_negative_scale_dirichletentrycellfirst dst_positive_dirichletentrycellfirst dst_negative_dirichletentrycellfirst. ((((F)) = (((((dst_positive_code_dirichletentrycellfirst) + (dst_positive_scale_dirichletentrycellfirst)) * S ((dst_positive_code_dirichletentrycellfirst) + (dst_positive_scale_dirichletentrycellfirst)) + ((dst_positive_scale_dirichletentrycellfirst) + (dst_positive_scale_dirichletentrycellfirst))) + (((dst_negative_code_dirichletentrycellfirst) + (dst_negative_scale_dirichletentrycellfirst)) * S ((dst_negative_code_dirichletentrycellfirst) + (dst_negative_scale_dirichletentrycellfirst)) + ((dst_negative_scale_dirichletentrycellfirst) + (dst_negative_scale_dirichletentrycellfirst)))) * S ((((dst_positive_code_dirichletentrycellfirst) + (dst_positive_scale_dirichletentrycellfirst)) * S ((dst_positive_code_dirichletentrycellfirst) + (dst_positive_scale_dirichletentrycellfirst)) + ((dst_positive_scale_dirichletentrycellfirst) + (dst_positive_scale_dirichletentrycellfirst))) + (((dst_negative_code_dirichletentrycellfirst) + (dst_negative_scale_dirichletentrycellfirst)) * S ((dst_negative_code_dirichletentrycellfirst) + (dst_negative_scale_dirichletentrycellfirst)) + ((dst_negative_scale_dirichletentrycellfirst) + (dst_negative_scale_dirichletentrycellfirst)))) + ((((dst_negative_code_dirichletentrycellfirst) + (dst_negative_scale_dirichletentrycellfirst)) * S ((dst_negative_code_dirichletentrycellfirst) + (dst_negative_scale_dirichletentrycellfirst)) + ((dst_negative_scale_dirichletentrycellfirst) + (dst_negative_scale_dirichletentrycellfirst))) + (((dst_negative_code_dirichletentrycellfirst) + (dst_negative_scale_dirichletentrycellfirst)) * S ((dst_negative_code_dirichletentrycellfirst) + (dst_negative_scale_dirichletentrycellfirst)) + ((dst_negative_scale_dirichletentrycellfirst) + (dst_negative_scale_dirichletentrycellfirst)))))) /\ (((((exists ff_h_pvs_dirichletentrycellfirstpositive. ff_h_pvs_dirichletentrycellfirstpositive + S (dst_positive_dirichletentrycellfirst) = S ((S (dfg_flat_row_dirichletentry)) * dst_positive_scale_dirichletentrycellfirst)) /\ exists ff_q_pvs_dirichletentrycellfirstpositive. dst_positive_code_dirichletentrycellfirst = ff_q_pvs_dirichletentrycellfirstpositive * S ((S (dfg_flat_row_dirichletentry)) * dst_positive_scale_dirichletentrycellfirst) + (dst_positive_dirichletentrycellfirst))) /\ (((((exists ff_h_pvs_dirichletentrycellfirstnegative. ff_h_pvs_dirichletentrycellfirstnegative + S (dst_negative_dirichletentrycellfirst) = S ((S (dfg_flat_row_dirichletentry)) * dst_negative_scale_dirichletentrycellfirst)) /\ exists ff_q_pvs_dirichletentrycellfirstnegative. dst_negative_code_dirichletentrycellfirst = ff_q_pvs_dirichletentrycellfirstnegative * S ((S (dfg_flat_row_dirichletentry)) * dst_negative_scale_dirichletentrycellfirst) + (dst_negative_dirichletentrycellfirst))) /\ (exists ge_balance_positive_dirichletentrycellfirstvalue ge_balance_negative_dirichletentrycellfirstvalue. (((((dfg_first_dirichletentrycell) = 2 * (ge_balance_positive_dirichletentrycellfirstvalue) /\ (ge_balance_negative_dirichletentrycellfirstvalue) = 0) \/ exists ge_signed_half_dirichletentrycellfirstvaluedecode. (((dfg_first_dirichletentrycell) = 2 * ge_signed_half_dirichletentrycellfirstvaluedecode + 1 /\ (ge_balance_positive_dirichletentrycellfirstvalue) = 0) /\ (ge_balance_negative_dirichletentrycellfirstvalue) = S ge_signed_half_dirichletentrycellfirstvaluedecode))) /\ ((dst_positive_dirichletentrycellfirst) + ge_balance_negative_dirichletentrycellfirstvalue = (dst_negative_dirichletentrycellfirst) + ge_balance_positive_dirichletentrycellfirstvalue))))))))) /\ (((exists dst_positive_code_dirichletentrycelllast dst_positive_scale_dirichletentrycelllast dst_negative_code_dirichletentrycelllast dst_negative_scale_dirichletentrycelllast dst_positive_dirichletentrycelllast dst_negative_dirichletentrycelllast. ((((H)) = (((((dst_positive_code_dirichletentrycelllast) + (dst_positive_scale_dirichletentrycelllast)) * S ((dst_positive_code_dirichletentrycelllast) + (dst_positive_scale_dirichletentrycelllast)) + ((dst_positive_scale_dirichletentrycelllast) + (dst_positive_scale_dirichletentrycelllast))) + (((dst_negative_code_dirichletentrycelllast) + (dst_negative_scale_dirichletentrycelllast)) * S ((dst_negative_code_dirichletentrycelllast) + (dst_negative_scale_dirichletentrycelllast)) + ((dst_negative_scale_dirichletentrycelllast) + (dst_negative_scale_dirichletentrycelllast)))) * S ((((dst_positive_code_dirichletentrycelllast) + (dst_positive_scale_dirichletentrycelllast)) * S ((dst_positive_code_dirichletentrycelllast) + (dst_positive_scale_dirichletentrycelllast)) + ((dst_positive_scale_dirichletentrycelllast) + (dst_positive_scale_dirichletentrycelllast))) + (((dst_negative_code_dirichletentrycelllast) + (dst_negative_scale_dirichletentrycelllast)) * S ((dst_negative_code_dirichletentrycelllast) + (dst_negative_scale_dirichletentrycelllast)) + ((dst_negative_scale_dirichletentrycelllast) + (dst_negative_scale_dirichletentrycelllast)))) + ((((dst_negative_code_dirichletentrycelllast) + (dst_negative_scale_dirichletentrycelllast)) * S ((dst_negative_code_dirichletentrycelllast) + (dst_negative_scale_dirichletentrycelllast)) + ((dst_negative_scale_dirichletentrycelllast) + (dst_negative_scale_dirichletentrycelllast))) + (((dst_negative_code_dirichletentrycelllast) + (dst_negative_scale_dirichletentrycelllast)) * S ((dst_negative_code_dirichletentrycelllast) + (dst_negative_scale_dirichletentrycelllast)) + ((dst_negative_scale_dirichletentrycelllast) + (dst_negative_scale_dirichletentrycelllast)))))) /\ (((((exists ff_h_pvs_dirichletentrycelllastpositive. ff_h_pvs_dirichletentrycelllastpositive + S (dst_positive_dirichletentrycelllast) = S ((S (dfg_flat_column_dirichletentry)) * dst_positive_scale_dirichletentrycelllast)) /\ exists ff_q_pvs_dirichletentrycelllastpositive. dst_positive_code_dirichletentrycelllast = ff_q_pvs_dirichletentrycelllastpositive * S ((S (dfg_flat_column_dirichletentry)) * dst_positive_scale_dirichletentrycelllast) + (dst_positive_dirichletentrycelllast))) /\ (((((exists ff_h_pvs_dirichletentrycelllastnegative. ff_h_pvs_dirichletentrycelllastnegative + S (dst_negative_dirichletentrycelllast) = S ((S (dfg_flat_column_dirichletentry)) * dst_negative_scale_dirichletentrycelllast)) /\ exists ff_q_pvs_dirichletentrycelllastnegative. dst_negative_code_dirichletentrycelllast = ff_q_pvs_dirichletentrycelllastnegative * S ((S (dfg_flat_column_dirichletentry)) * dst_negative_scale_dirichletentrycelllast) + (dst_negative_dirichletentrycelllast))) /\ (exists ge_balance_positive_dirichletentrycelllastvalue ge_balance_negative_dirichletentrycelllastvalue. (((((dfg_last_dirichletentrycell) = 2 * (ge_balance_positive_dirichletentrycelllastvalue) /\ (ge_balance_negative_dirichletentrycelllastvalue) = 0) \/ exists ge_signed_half_dirichletentrycelllastvaluedecode. (((dfg_last_dirichletentrycell) = 2 * ge_signed_half_dirichletentrycelllastvaluedecode + 1 /\ (ge_balance_positive_dirichletentrycelllastvalue) = 0) /\ (ge_balance_negative_dirichletentrycelllastvalue) = S ge_signed_half_dirichletentrycelllastvaluedecode))) /\ ((dst_positive_dirichletentrycelllast) + ge_balance_negative_dirichletentrycelllastvalue = (dst_negative_dirichletentrycelllast) + ge_balance_positive_dirichletentrycelllastvalue))))))))) /\ (((exists dst_positive_code_dirichletentrycellmiddle dst_positive_scale_dirichletentrycellmiddle dst_negative_code_dirichletentrycellmiddle dst_negative_scale_dirichletentrycellmiddle dst_positive_dirichletentrycellmiddle dst_negative_dirichletentrycellmiddle. ((((G)) = (((((dst_positive_code_dirichletentrycellmiddle) + (dst_positive_scale_dirichletentrycellmiddle)) * S ((dst_positive_code_dirichletentrycellmiddle) + (dst_positive_scale_dirichletentrycellmiddle)) + ((dst_positive_scale_dirichletentrycellmiddle) + (dst_positive_scale_dirichletentrycellmiddle))) + (((dst_negative_code_dirichletentrycellmiddle) + (dst_negative_scale_dirichletentrycellmiddle)) * S ((dst_negative_code_dirichletentrycellmiddle) + (dst_negative_scale_dirichletentrycellmiddle)) + ((dst_negative_scale_dirichletentrycellmiddle) + (dst_negative_scale_dirichletentrycellmiddle)))) * S ((((dst_positive_code_dirichletentrycellmiddle) + (dst_positive_scale_dirichletentrycellmiddle)) * S ((dst_positive_code_dirichletentrycellmiddle) + (dst_positive_scale_dirichletentrycellmiddle)) + ((dst_positive_scale_dirichletentrycellmiddle) + (dst_positive_scale_dirichletentrycellmiddle))) + (((dst_negative_code_dirichletentrycellmiddle) + (dst_negative_scale_dirichletentrycellmiddle)) * S ((dst_negative_code_dirichletentrycellmiddle) + (dst_negative_scale_dirichletentrycellmiddle)) + ((dst_negative_scale_dirichletentrycellmiddle) + (dst_negative_scale_dirichletentrycellmiddle)))) + ((((dst_negative_code_dirichletentrycellmiddle) + (dst_negative_scale_dirichletentrycellmiddle)) * S ((dst_negative_code_dirichletentrycellmiddle) + (dst_negative_scale_dirichletentrycellmiddle)) + ((dst_negative_scale_dirichletentrycellmiddle) + (dst_negative_scale_dirichletentrycellmiddle))) + (((dst_negative_code_dirichletentrycellmiddle) + (dst_negative_scale_dirichletentrycellmiddle)) * S ((dst_negative_code_dirichletentrycellmiddle) + (dst_negative_scale_dirichletentrycellmiddle)) + ((dst_negative_scale_dirichletentrycellmiddle) + (dst_negative_scale_dirichletentrycellmiddle)))))) /\ (((((exists ff_h_pvs_dirichletentrycellmiddlepositive. ff_h_pvs_dirichletentrycellmiddlepositive + S (dst_positive_dirichletentrycellmiddle) = S ((S (dfg_middle_dirichletentrycell)) * dst_positive_scale_dirichletentrycellmiddle)) /\ exists ff_q_pvs_dirichletentrycellmiddlepositive. dst_positive_code_dirichletentrycellmiddle = ff_q_pvs_dirichletentrycellmiddlepositive * S ((S (dfg_middle_dirichletentrycell)) * dst_positive_scale_dirichletentrycellmiddle) + (dst_positive_dirichletentrycellmiddle))) /\ (((((exists ff_h_pvs_dirichletentrycellmiddlenegative. ff_h_pvs_dirichletentrycellmiddlenegative + S (dst_negative_dirichletentrycellmiddle) = S ((S (dfg_middle_dirichletentrycell)) * dst_negative_scale_dirichletentrycellmiddle)) /\ exists ff_q_pvs_dirichletentrycellmiddlenegative. dst_negative_code_dirichletentrycellmiddle = ff_q_pvs_dirichletentrycellmiddlenegative * S ((S (dfg_middle_dirichletentrycell)) * dst_negative_scale_dirichletentrycellmiddle) + (dst_negative_dirichletentrycellmiddle))) /\ (exists ge_balance_positive_dirichletentrycellmiddlevalue ge_balance_negative_dirichletentrycellmiddlevalue. (((((dfg_value_dirichletentrycell) = 2 * (ge_balance_positive_dirichletentrycellmiddlevalue) /\ (ge_balance_negative_dirichletentrycellmiddlevalue) = 0) \/ exists ge_signed_half_dirichletentrycellmiddlevaluedecode. (((dfg_value_dirichletentrycell) = 2 * ge_signed_half_dirichletentrycellmiddlevaluedecode + 1 /\ (ge_balance_positive_dirichletentrycellmiddlevalue) = 0) /\ (ge_balance_negative_dirichletentrycellmiddlevalue) = S ge_signed_half_dirichletentrycellmiddlevaluedecode))) /\ ((dst_positive_dirichletentrycellmiddle) + ge_balance_negative_dirichletentrycellmiddlevalue = (dst_negative_dirichletentrycellmiddle) + ge_balance_positive_dirichletentrycellmiddlevalue))))))))) /\ (exists dfg_inner_dirichletentrycellproduct. ((exists sto_ap_dirichletentrycellproductinner sto_an_dirichletentrycellproductinner sto_bp_dirichletentrycellproductinner sto_bn_dirichletentrycellproductinner sto_cp_dirichletentrycellproductinner sto_cn_dirichletentrycellproductinner. (((((dfg_last_dirichletentrycell) = 2 * (sto_ap_dirichletentrycellproductinner) /\ (sto_an_dirichletentrycellproductinner) = 0) \/ exists ge_signed_half_dirichletentrycellproductinnerleft. (((dfg_last_dirichletentrycell) = 2 * ge_signed_half_dirichletentrycellproductinnerleft + 1 /\ (sto_ap_dirichletentrycellproductinner) = 0) /\ (sto_an_dirichletentrycellproductinner) = S ge_signed_half_dirichletentrycellproductinnerleft))) /\ ((((((dfg_value_dirichletentrycell) = 2 * (sto_bp_dirichletentrycellproductinner) /\ (sto_bn_dirichletentrycellproductinner) = 0) \/ exists ge_signed_half_dirichletentrycellproductinnerright. (((dfg_value_dirichletentrycell) = 2 * ge_signed_half_dirichletentrycellproductinnerright + 1 /\ (sto_bp_dirichletentrycellproductinner) = 0) /\ (sto_bn_dirichletentrycellproductinner) = S ge_signed_half_dirichletentrycellproductinnerright))) /\ ((((((dfg_inner_dirichletentrycellproduct) = 2 * (sto_cp_dirichletentrycellproductinner) /\ (sto_cn_dirichletentrycellproductinner) = 0) \/ exists ge_signed_half_dirichletentrycellproductinneroutput. (((dfg_inner_dirichletentrycellproduct) = 2 * ge_signed_half_dirichletentrycellproductinneroutput + 1 /\ (sto_cp_dirichletentrycellproductinner) = 0) /\ (sto_cn_dirichletentrycellproductinner) = S ge_signed_half_dirichletentrycellproductinneroutput))) /\ ((sto_ap_dirichletentrycellproductinner * sto_bp_dirichletentrycellproductinner + sto_an_dirichletentrycellproductinner * sto_bn_dirichletentrycellproductinner) + sto_cn_dirichletentrycellproductinner = (sto_ap_dirichletentrycellproductinner * sto_bn_dirichletentrycellproductinner + sto_an_dirichletentrycellproductinner * sto_bp_dirichletentrycellproductinner) + sto_cp_dirichletentrycellproductinner))))))) /\ (exists sto_ap_dirichletentrycellproductouter sto_an_dirichletentrycellproductouter sto_bp_dirichletentrycellproductouter sto_bn_dirichletentrycellproductouter sto_cp_dirichletentrycellproductouter sto_cn_dirichletentrycellproductouter. (((((dfg_first_dirichletentrycell) = 2 * (sto_ap_dirichletentrycellproductouter) /\ (sto_an_dirichletentrycellproductouter) = 0) \/ exists ge_signed_half_dirichletentrycellproductouterleft. (((dfg_first_dirichletentrycell) = 2 * ge_signed_half_dirichletentrycellproductouterleft + 1 /\ (sto_ap_dirichletentrycellproductouter) = 0) /\ (sto_an_dirichletentrycellproductouter) = S ge_signed_half_dirichletentrycellproductouterleft))) /\ ((((((dfg_inner_dirichletentrycellproduct) = 2 * (sto_bp_dirichletentrycellproductouter) /\ (sto_bn_dirichletentrycellproductouter) = 0) \/ exists ge_signed_half_dirichletentrycellproductouterright. (((dfg_inner_dirichletentrycellproduct) = 2 * ge_signed_half_dirichletentrycellproductouterright + 1 /\ (sto_bp_dirichletentrycellproductouter) = 0) /\ (sto_bn_dirichletentrycellproductouter) = S ge_signed_half_dirichletentrycellproductouterright))) /\ ((((((dfg_flat_value_dirichlet) = 2 * (sto_cp_dirichletentrycellproductouter) /\ (sto_cn_dirichletentrycellproductouter) = 0) \/ exists ge_signed_half_dirichletentrycellproductouteroutput. (((dfg_flat_value_dirichlet) = 2 * ge_signed_half_dirichletentrycellproductouteroutput + 1 /\ (sto_cp_dirichletentrycellproductouter) = 0) /\ (sto_cn_dirichletentrycellproductouter) = S ge_signed_half_dirichletentrycellproductouteroutput))) /\ ((sto_ap_dirichletentrycellproductouter * sto_bp_dirichletentrycellproductouter + sto_an_dirichletentrycellproductouter * sto_bn_dirichletentrycellproductouter) + sto_cn_dirichletentrycellproductouter = (sto_ap_dirichletentrycellproductouter * sto_bn_dirichletentrycellproductouter + sto_an_dirichletentrycellproductouter * sto_bp_dirichletentrycellproductouter) + sto_cp_dirichletentrycellproductouter))))))))))))))))))))) \/ ((((dfg_flat_row_dirichletentry)=0 \/ ((dfg_flat_column_dirichletentry)=0 \/ ~(exists pvs_factor_dirichletentrycellomittednondivisor. ((n)) = ((dfg_flat_row_dirichletentry)*(dfg_flat_column_dirichletentry)) * pvs_factor_dirichletentrycellomittednondivisor))) /\ ((dfg_flat_value_dirichlet)=0))))))))))

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