DirichletInverse(N,F,G)

exists di_delta_dirichlet_inverse. ((((exists dst_positive_code_dirichlet_inversedeltatable dst_positive_scale_dirichlet_inversedeltatable dst_negative_code_dirichlet_inversedeltatable dst_negative_scale_dirichlet_inversedeltatable. (((di_delta_dirichlet_inverse) = (((((dst_positive_code_dirichlet_inversedeltatable) + (dst_positive_scale_dirichlet_inversedeltatable)) * S ((dst_positive_code_dirichlet_inversedeltatable) + (dst_positive_scale_dirichlet_inversedeltatable)) + ((dst_positive_scale_dirichlet_inversedeltatable) + (dst_positive_scale_dirichlet_inversedeltatable))) + (((dst_negative_code_dirichlet_inversedeltatable) + (dst_negative_scale_dirichlet_inversedeltatable)) * S ((dst_negative_code_dirichlet_inversedeltatable) + (dst_negative_scale_dirichlet_inversedeltatable)) + ((dst_negative_scale_dirichlet_inversedeltatable) + (dst_negative_scale_dirichlet_inversedeltatable)))) * S ((((dst_positive_code_dirichlet_inversedeltatable) + (dst_positive_scale_dirichlet_inversedeltatable)) * S ((dst_positive_code_dirichlet_inversedeltatable) + (dst_positive_scale_dirichlet_inversedeltatable)) + ((dst_positive_scale_dirichlet_inversedeltatable) + (dst_positive_scale_dirichlet_inversedeltatable))) + (((dst_negative_code_dirichlet_inversedeltatable) + (dst_negative_scale_dirichlet_inversedeltatable)) * S ((dst_negative_code_dirichlet_inversedeltatable) + (dst_negative_scale_dirichlet_inversedeltatable)) + ((dst_negative_scale_dirichlet_inversedeltatable) + (dst_negative_scale_dirichlet_inversedeltatable)))) + ((((dst_negative_code_dirichlet_inversedeltatable) + (dst_negative_scale_dirichlet_inversedeltatable)) * S ((dst_negative_code_dirichlet_inversedeltatable) + (dst_negative_scale_dirichlet_inversedeltatable)) + ((dst_negative_scale_dirichlet_inversedeltatable) + (dst_negative_scale_dirichlet_inversedeltatable))) + (((dst_negative_code_dirichlet_inversedeltatable) + (dst_negative_scale_dirichlet_inversedeltatable)) * S ((dst_negative_code_dirichlet_inversedeltatable) + (dst_negative_scale_dirichlet_inversedeltatable)) + ((dst_negative_scale_dirichlet_inversedeltatable) + (dst_negative_scale_dirichlet_inversedeltatable)))))) /\ (forall dst_index_dirichlet_inversedeltatable. (exists pvs_le_gap_dirichlet_inversedeltatabledomain. pvs_le_gap_dirichlet_inversedeltatabledomain + (dst_index_dirichlet_inversedeltatable) = ((N))) -> exists dst_positive_dirichlet_inversedeltatable dst_negative_dirichlet_inversedeltatable dst_value_dirichlet_inversedeltatable. ((((exists ff_h_pvs_dirichlet_inversedeltatableentrypositive. ff_h_pvs_dirichlet_inversedeltatableentrypositive + S (dst_positive_dirichlet_inversedeltatable) = S ((S (dst_index_dirichlet_inversedeltatable)) * dst_positive_scale_dirichlet_inversedeltatable)) /\ exists ff_q_pvs_dirichlet_inversedeltatableentrypositive. dst_positive_code_dirichlet_inversedeltatable = ff_q_pvs_dirichlet_inversedeltatableentrypositive * S ((S (dst_index_dirichlet_inversedeltatable)) * dst_positive_scale_dirichlet_inversedeltatable) + (dst_positive_dirichlet_inversedeltatable))) /\ (((((exists ff_h_pvs_dirichlet_inversedeltatableentrynegative. ff_h_pvs_dirichlet_inversedeltatableentrynegative + S (dst_negative_dirichlet_inversedeltatable) = S ((S (dst_index_dirichlet_inversedeltatable)) * dst_negative_scale_dirichlet_inversedeltatable)) /\ exists ff_q_pvs_dirichlet_inversedeltatableentrynegative. dst_negative_code_dirichlet_inversedeltatable = ff_q_pvs_dirichlet_inversedeltatableentrynegative * S ((S (dst_index_dirichlet_inversedeltatable)) * dst_negative_scale_dirichlet_inversedeltatable) + (dst_negative_dirichlet_inversedeltatable))) /\ (exists ge_balance_positive_dirichlet_inversedeltatableentryvalue ge_balance_negative_dirichlet_inversedeltatableentryvalue. (((((dst_value_dirichlet_inversedeltatable) = 2 * (ge_balance_positive_dirichlet_inversedeltatableentryvalue) /\ (ge_balance_negative_dirichlet_inversedeltatableentryvalue) = 0) \/ exists ge_signed_half_dirichlet_inversedeltatableentryvaluedecode. (((dst_value_dirichlet_inversedeltatable) = 2 * ge_signed_half_dirichlet_inversedeltatableentryvaluedecode + 1 /\ (ge_balance_positive_dirichlet_inversedeltatableentryvalue) = 0) /\ (ge_balance_negative_dirichlet_inversedeltatableentryvalue) = S ge_signed_half_dirichlet_inversedeltatableentryvaluedecode))) /\ ((dst_positive_dirichlet_inversedeltatable) + ge_balance_negative_dirichlet_inversedeltatableentryvalue = (dst_negative_dirichlet_inversedeltatable) + ge_balance_positive_dirichlet_inversedeltatableentryvalue))))))))) /\ (forall du_index_dirichlet_inversedelta du_value_dirichlet_inversedelta. ~(du_index_dirichlet_inversedelta=0) -> (exists pvs_le_gap_dirichlet_inversedeltabound. pvs_le_gap_dirichlet_inversedeltabound + (du_index_dirichlet_inversedelta) = ((N))) -> (exists dst_positive_code_dirichlet_inversedeltaentry dst_positive_scale_dirichlet_inversedeltaentry dst_negative_code_dirichlet_inversedeltaentry dst_negative_scale_dirichlet_inversedeltaentry dst_positive_dirichlet_inversedeltaentry dst_negative_dirichlet_inversedeltaentry. (((di_delta_dirichlet_inverse) = (((((dst_positive_code_dirichlet_inversedeltaentry) + (dst_positive_scale_dirichlet_inversedeltaentry)) * S ((dst_positive_code_dirichlet_inversedeltaentry) + (dst_positive_scale_dirichlet_inversedeltaentry)) + ((dst_positive_scale_dirichlet_inversedeltaentry) + (dst_positive_scale_dirichlet_inversedeltaentry))) + (((dst_negative_code_dirichlet_inversedeltaentry) + (dst_negative_scale_dirichlet_inversedeltaentry)) * S ((dst_negative_code_dirichlet_inversedeltaentry) + (dst_negative_scale_dirichlet_inversedeltaentry)) + ((dst_negative_scale_dirichlet_inversedeltaentry) + (dst_negative_scale_dirichlet_inversedeltaentry)))) * S ((((dst_positive_code_dirichlet_inversedeltaentry) + (dst_positive_scale_dirichlet_inversedeltaentry)) * S ((dst_positive_code_dirichlet_inversedeltaentry) + (dst_positive_scale_dirichlet_inversedeltaentry)) + ((dst_positive_scale_dirichlet_inversedeltaentry) + (dst_positive_scale_dirichlet_inversedeltaentry))) + (((dst_negative_code_dirichlet_inversedeltaentry) + (dst_negative_scale_dirichlet_inversedeltaentry)) * S ((dst_negative_code_dirichlet_inversedeltaentry) + (dst_negative_scale_dirichlet_inversedeltaentry)) + ((dst_negative_scale_dirichlet_inversedeltaentry) + (dst_negative_scale_dirichlet_inversedeltaentry)))) + ((((dst_negative_code_dirichlet_inversedeltaentry) + (dst_negative_scale_dirichlet_inversedeltaentry)) * S ((dst_negative_code_dirichlet_inversedeltaentry) + (dst_negative_scale_dirichlet_inversedeltaentry)) + ((dst_negative_scale_dirichlet_inversedeltaentry) + (dst_negative_scale_dirichlet_inversedeltaentry))) + (((dst_negative_code_dirichlet_inversedeltaentry) + (dst_negative_scale_dirichlet_inversedeltaentry)) * S ((dst_negative_code_dirichlet_inversedeltaentry) + (dst_negative_scale_dirichlet_inversedeltaentry)) + ((dst_negative_scale_dirichlet_inversedeltaentry) + (dst_negative_scale_dirichlet_inversedeltaentry)))))) /\ (((((exists ff_h_pvs_dirichlet_inversedeltaentrypositive. ff_h_pvs_dirichlet_inversedeltaentrypositive + S (dst_positive_dirichlet_inversedeltaentry) = S ((S (du_index_dirichlet_inversedelta)) * dst_positive_scale_dirichlet_inversedeltaentry)) /\ exists ff_q_pvs_dirichlet_inversedeltaentrypositive. dst_positive_code_dirichlet_inversedeltaentry = ff_q_pvs_dirichlet_inversedeltaentrypositive * S ((S (du_index_dirichlet_inversedelta)) * dst_positive_scale_dirichlet_inversedeltaentry) + (dst_positive_dirichlet_inversedeltaentry))) /\ (((((exists ff_h_pvs_dirichlet_inversedeltaentrynegative. ff_h_pvs_dirichlet_inversedeltaentrynegative + S (dst_negative_dirichlet_inversedeltaentry) = S ((S (du_index_dirichlet_inversedelta)) * dst_negative_scale_dirichlet_inversedeltaentry)) /\ exists ff_q_pvs_dirichlet_inversedeltaentrynegative. dst_negative_code_dirichlet_inversedeltaentry = ff_q_pvs_dirichlet_inversedeltaentrynegative * S ((S (du_index_dirichlet_inversedelta)) * dst_negative_scale_dirichlet_inversedeltaentry) + (dst_negative_dirichlet_inversedeltaentry))) /\ (exists ge_balance_positive_dirichlet_inversedeltaentryvalue ge_balance_negative_dirichlet_inversedeltaentryvalue. (((((du_value_dirichlet_inversedelta) = 2 * (ge_balance_positive_dirichlet_inversedeltaentryvalue) /\ (ge_balance_negative_dirichlet_inversedeltaentryvalue) = 0) \/ exists ge_signed_half_dirichlet_inversedeltaentryvaluedecode. (((du_value_dirichlet_inversedelta) = 2 * ge_signed_half_dirichlet_inversedeltaentryvaluedecode + 1 /\ (ge_balance_positive_dirichlet_inversedeltaentryvalue) = 0) /\ (ge_balance_negative_dirichlet_inversedeltaentryvalue) = S ge_signed_half_dirichlet_inversedeltaentryvaluedecode))) /\ ((dst_positive_dirichlet_inversedeltaentry) + ge_balance_negative_dirichlet_inversedeltaentryvalue = (dst_negative_dirichlet_inversedeltaentry) + ge_balance_positive_dirichlet_inversedeltaentryvalue))))))))) -> ((((du_index_dirichlet_inversedelta)=1 -> (du_value_dirichlet_inversedelta)=2) /\ (~((du_index_dirichlet_inversedelta)=1) -> (du_value_dirichlet_inversedelta)=0)))))) /\ (((((exists dst_positive_code_dirichlet_inverseleftleft dst_positive_scale_dirichlet_inverseleftleft dst_negative_code_dirichlet_inverseleftleft dst_negative_scale_dirichlet_inverseleftleft. ((((F)) = (((((dst_positive_code_dirichlet_inverseleftleft) + (dst_positive_scale_dirichlet_inverseleftleft)) * S ((dst_positive_code_dirichlet_inverseleftleft) + (dst_positive_scale_dirichlet_inverseleftleft)) + ((dst_positive_scale_dirichlet_inverseleftleft) + (dst_positive_scale_dirichlet_inverseleftleft))) + (((dst_negative_code_dirichlet_inverseleftleft) + (dst_negative_scale_dirichlet_inverseleftleft)) * S ((dst_negative_code_dirichlet_inverseleftleft) + (dst_negative_scale_dirichlet_inverseleftleft)) + ((dst_negative_scale_dirichlet_inverseleftleft) + (dst_negative_scale_dirichlet_inverseleftleft)))) * S ((((dst_positive_code_dirichlet_inverseleftleft) + (dst_positive_scale_dirichlet_inverseleftleft)) * S ((dst_positive_code_dirichlet_inverseleftleft) + (dst_positive_scale_dirichlet_inverseleftleft)) + ((dst_positive_scale_dirichlet_inverseleftleft) + (dst_positive_scale_dirichlet_inverseleftleft))) + (((dst_negative_code_dirichlet_inverseleftleft) + (dst_negative_scale_dirichlet_inverseleftleft)) * S ((dst_negative_code_dirichlet_inverseleftleft) + (dst_negative_scale_dirichlet_inverseleftleft)) + ((dst_negative_scale_dirichlet_inverseleftleft) + (dst_negative_scale_dirichlet_inverseleftleft)))) + ((((dst_negative_code_dirichlet_inverseleftleft) + (dst_negative_scale_dirichlet_inverseleftleft)) * S ((dst_negative_code_dirichlet_inverseleftleft) + (dst_negative_scale_dirichlet_inverseleftleft)) + ((dst_negative_scale_dirichlet_inverseleftleft) + (dst_negative_scale_dirichlet_inverseleftleft))) + (((dst_negative_code_dirichlet_inverseleftleft) + (dst_negative_scale_dirichlet_inverseleftleft)) * S ((dst_negative_code_dirichlet_inverseleftleft) + (dst_negative_scale_dirichlet_inverseleftleft)) + ((dst_negative_scale_dirichlet_inverseleftleft) + (dst_negative_scale_dirichlet_inverseleftleft)))))) /\ (forall dst_index_dirichlet_inverseleftleft. (exists pvs_le_gap_dirichlet_inverseleftleftdomain. pvs_le_gap_dirichlet_inverseleftleftdomain + (dst_index_dirichlet_inverseleftleft) = ((N))) -> exists dst_positive_dirichlet_inverseleftleft dst_negative_dirichlet_inverseleftleft dst_value_dirichlet_inverseleftleft. ((((exists ff_h_pvs_dirichlet_inverseleftleftentrypositive. ff_h_pvs_dirichlet_inverseleftleftentrypositive + S (dst_positive_dirichlet_inverseleftleft) = S ((S (dst_index_dirichlet_inverseleftleft)) * dst_positive_scale_dirichlet_inverseleftleft)) /\ exists ff_q_pvs_dirichlet_inverseleftleftentrypositive. dst_positive_code_dirichlet_inverseleftleft = ff_q_pvs_dirichlet_inverseleftleftentrypositive * S ((S (dst_index_dirichlet_inverseleftleft)) * dst_positive_scale_dirichlet_inverseleftleft) + (dst_positive_dirichlet_inverseleftleft))) /\ (((((exists ff_h_pvs_dirichlet_inverseleftleftentrynegative. ff_h_pvs_dirichlet_inverseleftleftentrynegative + S (dst_negative_dirichlet_inverseleftleft) = S ((S (dst_index_dirichlet_inverseleftleft)) * dst_negative_scale_dirichlet_inverseleftleft)) /\ exists ff_q_pvs_dirichlet_inverseleftleftentrynegative. dst_negative_code_dirichlet_inverseleftleft = ff_q_pvs_dirichlet_inverseleftleftentrynegative * S ((S (dst_index_dirichlet_inverseleftleft)) * dst_negative_scale_dirichlet_inverseleftleft) + (dst_negative_dirichlet_inverseleftleft))) /\ (exists ge_balance_positive_dirichlet_inverseleftleftentryvalue ge_balance_negative_dirichlet_inverseleftleftentryvalue. (((((dst_value_dirichlet_inverseleftleft) = 2 * (ge_balance_positive_dirichlet_inverseleftleftentryvalue) /\ (ge_balance_negative_dirichlet_inverseleftleftentryvalue) = 0) \/ exists ge_signed_half_dirichlet_inverseleftleftentryvaluedecode. (((dst_value_dirichlet_inverseleftleft) = 2 * ge_signed_half_dirichlet_inverseleftleftentryvaluedecode + 1 /\ (ge_balance_positive_dirichlet_inverseleftleftentryvalue) = 0) /\ (ge_balance_negative_dirichlet_inverseleftleftentryvalue) = S ge_signed_half_dirichlet_inverseleftleftentryvaluedecode))) /\ ((dst_positive_dirichlet_inverseleftleft) + ge_balance_negative_dirichlet_inverseleftleftentryvalue = (dst_negative_dirichlet_inverseleftleft) + ge_balance_positive_dirichlet_inverseleftleftentryvalue))))))))) /\ (((exists dst_positive_code_dirichlet_inverseleftright dst_positive_scale_dirichlet_inverseleftright dst_negative_code_dirichlet_inverseleftright dst_negative_scale_dirichlet_inverseleftright. ((((G)) = (((((dst_positive_code_dirichlet_inverseleftright) + (dst_positive_scale_dirichlet_inverseleftright)) * S ((dst_positive_code_dirichlet_inverseleftright) + (dst_positive_scale_dirichlet_inverseleftright)) + ((dst_positive_scale_dirichlet_inverseleftright) + (dst_positive_scale_dirichlet_inverseleftright))) + (((dst_negative_code_dirichlet_inverseleftright) + (dst_negative_scale_dirichlet_inverseleftright)) * S ((dst_negative_code_dirichlet_inverseleftright) + (dst_negative_scale_dirichlet_inverseleftright)) + ((dst_negative_scale_dirichlet_inverseleftright) + (dst_negative_scale_dirichlet_inverseleftright)))) * S ((((dst_positive_code_dirichlet_inverseleftright) + (dst_positive_scale_dirichlet_inverseleftright)) * S ((dst_positive_code_dirichlet_inverseleftright) + (dst_positive_scale_dirichlet_inverseleftright)) + ((dst_positive_scale_dirichlet_inverseleftright) + (dst_positive_scale_dirichlet_inverseleftright))) + (((dst_negative_code_dirichlet_inverseleftright) + (dst_negative_scale_dirichlet_inverseleftright)) * S ((dst_negative_code_dirichlet_inverseleftright) + (dst_negative_scale_dirichlet_inverseleftright)) + ((dst_negative_scale_dirichlet_inverseleftright) + (dst_negative_scale_dirichlet_inverseleftright)))) + ((((dst_negative_code_dirichlet_inverseleftright) + (dst_negative_scale_dirichlet_inverseleftright)) * S ((dst_negative_code_dirichlet_inverseleftright) + (dst_negative_scale_dirichlet_inverseleftright)) + ((dst_negative_scale_dirichlet_inverseleftright) + (dst_negative_scale_dirichlet_inverseleftright))) + (((dst_negative_code_dirichlet_inverseleftright) + (dst_negative_scale_dirichlet_inverseleftright)) * S ((dst_negative_code_dirichlet_inverseleftright) + (dst_negative_scale_dirichlet_inverseleftright)) + ((dst_negative_scale_dirichlet_inverseleftright) + (dst_negative_scale_dirichlet_inverseleftright)))))) /\ (forall dst_index_dirichlet_inverseleftright. (exists pvs_le_gap_dirichlet_inverseleftrightdomain. pvs_le_gap_dirichlet_inverseleftrightdomain + (dst_index_dirichlet_inverseleftright) = ((N))) -> exists dst_positive_dirichlet_inverseleftright dst_negative_dirichlet_inverseleftright dst_value_dirichlet_inverseleftright. ((((exists ff_h_pvs_dirichlet_inverseleftrightentrypositive. ff_h_pvs_dirichlet_inverseleftrightentrypositive + S (dst_positive_dirichlet_inverseleftright) = S ((S (dst_index_dirichlet_inverseleftright)) * dst_positive_scale_dirichlet_inverseleftright)) /\ exists ff_q_pvs_dirichlet_inverseleftrightentrypositive. dst_positive_code_dirichlet_inverseleftright = ff_q_pvs_dirichlet_inverseleftrightentrypositive * S ((S (dst_index_dirichlet_inverseleftright)) * dst_positive_scale_dirichlet_inverseleftright) + (dst_positive_dirichlet_inverseleftright))) /\ (((((exists ff_h_pvs_dirichlet_inverseleftrightentrynegative. ff_h_pvs_dirichlet_inverseleftrightentrynegative + S (dst_negative_dirichlet_inverseleftright) = S ((S (dst_index_dirichlet_inverseleftright)) * dst_negative_scale_dirichlet_inverseleftright)) /\ exists ff_q_pvs_dirichlet_inverseleftrightentrynegative. dst_negative_code_dirichlet_inverseleftright = ff_q_pvs_dirichlet_inverseleftrightentrynegative * S ((S (dst_index_dirichlet_inverseleftright)) * dst_negative_scale_dirichlet_inverseleftright) + (dst_negative_dirichlet_inverseleftright))) /\ (exists ge_balance_positive_dirichlet_inverseleftrightentryvalue ge_balance_negative_dirichlet_inverseleftrightentryvalue. (((((dst_value_dirichlet_inverseleftright) = 2 * (ge_balance_positive_dirichlet_inverseleftrightentryvalue) /\ (ge_balance_negative_dirichlet_inverseleftrightentryvalue) = 0) \/ exists ge_signed_half_dirichlet_inverseleftrightentryvaluedecode. (((dst_value_dirichlet_inverseleftright) = 2 * ge_signed_half_dirichlet_inverseleftrightentryvaluedecode + 1 /\ (ge_balance_positive_dirichlet_inverseleftrightentryvalue) = 0) /\ (ge_balance_negative_dirichlet_inverseleftrightentryvalue) = S ge_signed_half_dirichlet_inverseleftrightentryvaluedecode))) /\ ((dst_positive_dirichlet_inverseleftright) + ge_balance_negative_dirichlet_inverseleftrightentryvalue = (dst_negative_dirichlet_inverseleftright) + ge_balance_positive_dirichlet_inverseleftrightentryvalue))))))))) /\ (((exists dst_positive_code_dirichlet_inverselefttable dst_positive_scale_dirichlet_inverselefttable dst_negative_code_dirichlet_inverselefttable dst_negative_scale_dirichlet_inverselefttable. (((di_delta_dirichlet_inverse) = (((((dst_positive_code_dirichlet_inverselefttable) + (dst_positive_scale_dirichlet_inverselefttable)) * S ((dst_positive_code_dirichlet_inverselefttable) + (dst_positive_scale_dirichlet_inverselefttable)) + ((dst_positive_scale_dirichlet_inverselefttable) + (dst_positive_scale_dirichlet_inverselefttable))) + (((dst_negative_code_dirichlet_inverselefttable) + (dst_negative_scale_dirichlet_inverselefttable)) * S ((dst_negative_code_dirichlet_inverselefttable) + (dst_negative_scale_dirichlet_inverselefttable)) + ((dst_negative_scale_dirichlet_inverselefttable) + (dst_negative_scale_dirichlet_inverselefttable)))) * S ((((dst_positive_code_dirichlet_inverselefttable) + (dst_positive_scale_dirichlet_inverselefttable)) * S ((dst_positive_code_dirichlet_inverselefttable) + (dst_positive_scale_dirichlet_inverselefttable)) + ((dst_positive_scale_dirichlet_inverselefttable) + (dst_positive_scale_dirichlet_inverselefttable))) + (((dst_negative_code_dirichlet_inverselefttable) + (dst_negative_scale_dirichlet_inverselefttable)) * S ((dst_negative_code_dirichlet_inverselefttable) + (dst_negative_scale_dirichlet_inverselefttable)) + ((dst_negative_scale_dirichlet_inverselefttable) + (dst_negative_scale_dirichlet_inverselefttable)))) + ((((dst_negative_code_dirichlet_inverselefttable) + (dst_negative_scale_dirichlet_inverselefttable)) * S ((dst_negative_code_dirichlet_inverselefttable) + (dst_negative_scale_dirichlet_inverselefttable)) + ((dst_negative_scale_dirichlet_inverselefttable) + (dst_negative_scale_dirichlet_inverselefttable))) + (((dst_negative_code_dirichlet_inverselefttable) + (dst_negative_scale_dirichlet_inverselefttable)) * S ((dst_negative_code_dirichlet_inverselefttable) + (dst_negative_scale_dirichlet_inverselefttable)) + ((dst_negative_scale_dirichlet_inverselefttable) + (dst_negative_scale_dirichlet_inverselefttable)))))) /\ (forall dst_index_dirichlet_inverselefttable. (exists pvs_le_gap_dirichlet_inverselefttabledomain. pvs_le_gap_dirichlet_inverselefttabledomain + (dst_index_dirichlet_inverselefttable) = ((N))) -> exists dst_positive_dirichlet_inverselefttable dst_negative_dirichlet_inverselefttable dst_value_dirichlet_inverselefttable. ((((exists ff_h_pvs_dirichlet_inverselefttableentrypositive. ff_h_pvs_dirichlet_inverselefttableentrypositive + S (dst_positive_dirichlet_inverselefttable) = S ((S (dst_index_dirichlet_inverselefttable)) * dst_positive_scale_dirichlet_inverselefttable)) /\ exists ff_q_pvs_dirichlet_inverselefttableentrypositive. dst_positive_code_dirichlet_inverselefttable = ff_q_pvs_dirichlet_inverselefttableentrypositive * S ((S (dst_index_dirichlet_inverselefttable)) * dst_positive_scale_dirichlet_inverselefttable) + (dst_positive_dirichlet_inverselefttable))) /\ (((((exists ff_h_pvs_dirichlet_inverselefttableentrynegative. ff_h_pvs_dirichlet_inverselefttableentrynegative + S (dst_negative_dirichlet_inverselefttable) = S ((S (dst_index_dirichlet_inverselefttable)) * dst_negative_scale_dirichlet_inverselefttable)) /\ exists ff_q_pvs_dirichlet_inverselefttableentrynegative. dst_negative_code_dirichlet_inverselefttable = ff_q_pvs_dirichlet_inverselefttableentrynegative * S ((S (dst_index_dirichlet_inverselefttable)) * dst_negative_scale_dirichlet_inverselefttable) + (dst_negative_dirichlet_inverselefttable))) /\ (exists ge_balance_positive_dirichlet_inverselefttableentryvalue ge_balance_negative_dirichlet_inverselefttableentryvalue. (((((dst_value_dirichlet_inverselefttable) = 2 * (ge_balance_positive_dirichlet_inverselefttableentryvalue) /\ (ge_balance_negative_dirichlet_inverselefttableentryvalue) = 0) \/ exists ge_signed_half_dirichlet_inverselefttableentryvaluedecode. (((dst_value_dirichlet_inverselefttable) = 2 * ge_signed_half_dirichlet_inverselefttableentryvaluedecode + 1 /\ (ge_balance_positive_dirichlet_inverselefttableentryvalue) = 0) /\ (ge_balance_negative_dirichlet_inverselefttableentryvalue) = S ge_signed_half_dirichlet_inverselefttableentryvaluedecode))) /\ ((dst_positive_dirichlet_inverselefttable) + ge_balance_negative_dirichlet_inverselefttableentryvalue = (dst_negative_dirichlet_inverselefttable) + ge_balance_positive_dirichlet_inverselefttableentryvalue))))))))) /\ (forall dc_input_dirichlet_inverseleft dc_output_dirichlet_inverseleft. ~(dc_input_dirichlet_inverseleft=0) -> (exists pvs_le_gap_dirichlet_inverseleftdomain. pvs_le_gap_dirichlet_inverseleftdomain + (dc_input_dirichlet_inverseleft) = ((N))) -> (exists dst_positive_code_dirichlet_inverseleftlookup dst_positive_scale_dirichlet_inverseleftlookup dst_negative_code_dirichlet_inverseleftlookup dst_negative_scale_dirichlet_inverseleftlookup dst_positive_dirichlet_inverseleftlookup dst_negative_dirichlet_inverseleftlookup. (((di_delta_dirichlet_inverse) = (((((dst_positive_code_dirichlet_inverseleftlookup) + (dst_positive_scale_dirichlet_inverseleftlookup)) * S ((dst_positive_code_dirichlet_inverseleftlookup) + (dst_positive_scale_dirichlet_inverseleftlookup)) + ((dst_positive_scale_dirichlet_inverseleftlookup) + (dst_positive_scale_dirichlet_inverseleftlookup))) + (((dst_negative_code_dirichlet_inverseleftlookup) + (dst_negative_scale_dirichlet_inverseleftlookup)) * S ((dst_negative_code_dirichlet_inverseleftlookup) + (dst_negative_scale_dirichlet_inverseleftlookup)) + ((dst_negative_scale_dirichlet_inverseleftlookup) + (dst_negative_scale_dirichlet_inverseleftlookup)))) * S ((((dst_positive_code_dirichlet_inverseleftlookup) + (dst_positive_scale_dirichlet_inverseleftlookup)) * S ((dst_positive_code_dirichlet_inverseleftlookup) + (dst_positive_scale_dirichlet_inverseleftlookup)) + ((dst_positive_scale_dirichlet_inverseleftlookup) + (dst_positive_scale_dirichlet_inverseleftlookup))) + (((dst_negative_code_dirichlet_inverseleftlookup) + (dst_negative_scale_dirichlet_inverseleftlookup)) * S ((dst_negative_code_dirichlet_inverseleftlookup) + (dst_negative_scale_dirichlet_inverseleftlookup)) + ((dst_negative_scale_dirichlet_inverseleftlookup) + (dst_negative_scale_dirichlet_inverseleftlookup)))) + ((((dst_negative_code_dirichlet_inverseleftlookup) + (dst_negative_scale_dirichlet_inverseleftlookup)) * S ((dst_negative_code_dirichlet_inverseleftlookup) + (dst_negative_scale_dirichlet_inverseleftlookup)) + ((dst_negative_scale_dirichlet_inverseleftlookup) + (dst_negative_scale_dirichlet_inverseleftlookup))) + (((dst_negative_code_dirichlet_inverseleftlookup) + (dst_negative_scale_dirichlet_inverseleftlookup)) * S ((dst_negative_code_dirichlet_inverseleftlookup) + (dst_negative_scale_dirichlet_inverseleftlookup)) + ((dst_negative_scale_dirichlet_inverseleftlookup) + (dst_negative_scale_dirichlet_inverseleftlookup)))))) /\ (((((exists ff_h_pvs_dirichlet_inverseleftlookuppositive. ff_h_pvs_dirichlet_inverseleftlookuppositive + S (dst_positive_dirichlet_inverseleftlookup) = S ((S (dc_input_dirichlet_inverseleft)) * dst_positive_scale_dirichlet_inverseleftlookup)) /\ exists ff_q_pvs_dirichlet_inverseleftlookuppositive. dst_positive_code_dirichlet_inverseleftlookup = ff_q_pvs_dirichlet_inverseleftlookuppositive * S ((S (dc_input_dirichlet_inverseleft)) * dst_positive_scale_dirichlet_inverseleftlookup) + (dst_positive_dirichlet_inverseleftlookup))) /\ (((((exists ff_h_pvs_dirichlet_inverseleftlookupnegative. ff_h_pvs_dirichlet_inverseleftlookupnegative + S (dst_negative_dirichlet_inverseleftlookup) = S ((S (dc_input_dirichlet_inverseleft)) * dst_negative_scale_dirichlet_inverseleftlookup)) /\ exists ff_q_pvs_dirichlet_inverseleftlookupnegative. dst_negative_code_dirichlet_inverseleftlookup = ff_q_pvs_dirichlet_inverseleftlookupnegative * S ((S (dc_input_dirichlet_inverseleft)) * dst_negative_scale_dirichlet_inverseleftlookup) + (dst_negative_dirichlet_inverseleftlookup))) /\ (exists ge_balance_positive_dirichlet_inverseleftlookupvalue ge_balance_negative_dirichlet_inverseleftlookupvalue. (((((dc_output_dirichlet_inverseleft) = 2 * (ge_balance_positive_dirichlet_inverseleftlookupvalue) /\ (ge_balance_negative_dirichlet_inverseleftlookupvalue) = 0) \/ exists ge_signed_half_dirichlet_inverseleftlookupvaluedecode. (((dc_output_dirichlet_inverseleft) = 2 * ge_signed_half_dirichlet_inverseleftlookupvaluedecode + 1 /\ (ge_balance_positive_dirichlet_inverseleftlookupvalue) = 0) /\ (ge_balance_negative_dirichlet_inverseleftlookupvalue) = S ge_signed_half_dirichlet_inverseleftlookupvaluedecode))) /\ ((dst_positive_dirichlet_inverseleftlookup) + ge_balance_negative_dirichlet_inverseleftlookupvalue = (dst_negative_dirichlet_inverseleftlookup) + ge_balance_positive_dirichlet_inverseleftlookupvalue))))))))) -> (((~((dc_input_dirichlet_inverseleft)=0)) /\ (exists dc_mask_dirichlet_inverseleftvalue. ((((exists dst_positive_code_dirichlet_inverseleftvaluemasktable dst_positive_scale_dirichlet_inverseleftvaluemasktable dst_negative_code_dirichlet_inverseleftvaluemasktable dst_negative_scale_dirichlet_inverseleftvaluemasktable. (((dc_mask_dirichlet_inverseleftvalue) = (((((dst_positive_code_dirichlet_inverseleftvaluemasktable) + (dst_positive_scale_dirichlet_inverseleftvaluemasktable)) * S ((dst_positive_code_dirichlet_inverseleftvaluemasktable) + (dst_positive_scale_dirichlet_inverseleftvaluemasktable)) + ((dst_positive_scale_dirichlet_inverseleftvaluemasktable) + (dst_positive_scale_dirichlet_inverseleftvaluemasktable))) + (((dst_negative_code_dirichlet_inverseleftvaluemasktable) + (dst_negative_scale_dirichlet_inverseleftvaluemasktable)) * S ((dst_negative_code_dirichlet_inverseleftvaluemasktable) + (dst_negative_scale_dirichlet_inverseleftvaluemasktable)) + ((dst_negative_scale_dirichlet_inverseleftvaluemasktable) + (dst_negative_scale_dirichlet_inverseleftvaluemasktable)))) * S ((((dst_positive_code_dirichlet_inverseleftvaluemasktable) + (dst_positive_scale_dirichlet_inverseleftvaluemasktable)) * S ((dst_positive_code_dirichlet_inverseleftvaluemasktable) + (dst_positive_scale_dirichlet_inverseleftvaluemasktable)) + ((dst_positive_scale_dirichlet_inverseleftvaluemasktable) + (dst_positive_scale_dirichlet_inverseleftvaluemasktable))) + (((dst_negative_code_dirichlet_inverseleftvaluemasktable) + (dst_negative_scale_dirichlet_inverseleftvaluemasktable)) * S ((dst_negative_code_dirichlet_inverseleftvaluemasktable) + (dst_negative_scale_dirichlet_inverseleftvaluemasktable)) + ((dst_negative_scale_dirichlet_inverseleftvaluemasktable) + (dst_negative_scale_dirichlet_inverseleftvaluemasktable)))) + ((((dst_negative_code_dirichlet_inverseleftvaluemasktable) + (dst_negative_scale_dirichlet_inverseleftvaluemasktable)) * S ((dst_negative_code_dirichlet_inverseleftvaluemasktable) + (dst_negative_scale_dirichlet_inverseleftvaluemasktable)) + ((dst_negative_scale_dirichlet_inverseleftvaluemasktable) + (dst_negative_scale_dirichlet_inverseleftvaluemasktable))) + (((dst_negative_code_dirichlet_inverseleftvaluemasktable) + (dst_negative_scale_dirichlet_inverseleftvaluemasktable)) * S ((dst_negative_code_dirichlet_inverseleftvaluemasktable) + (dst_negative_scale_dirichlet_inverseleftvaluemasktable)) + ((dst_negative_scale_dirichlet_inverseleftvaluemasktable) + (dst_negative_scale_dirichlet_inverseleftvaluemasktable)))))) /\ (forall dst_index_dirichlet_inverseleftvaluemasktable. (exists pvs_le_gap_dirichlet_inverseleftvaluemasktabledomain. pvs_le_gap_dirichlet_inverseleftvaluemasktabledomain + (dst_index_dirichlet_inverseleftvaluemasktable) = (dc_input_dirichlet_inverseleft)) -> exists dst_positive_dirichlet_inverseleftvaluemasktable dst_negative_dirichlet_inverseleftvaluemasktable dst_value_dirichlet_inverseleftvaluemasktable. ((((exists ff_h_pvs_dirichlet_inverseleftvaluemasktableentrypositive. ff_h_pvs_dirichlet_inverseleftvaluemasktableentrypositive + S (dst_positive_dirichlet_inverseleftvaluemasktable) = S ((S (dst_index_dirichlet_inverseleftvaluemasktable)) * dst_positive_scale_dirichlet_inverseleftvaluemasktable)) /\ exists ff_q_pvs_dirichlet_inverseleftvaluemasktableentrypositive. dst_positive_code_dirichlet_inverseleftvaluemasktable = ff_q_pvs_dirichlet_inverseleftvaluemasktableentrypositive * S ((S (dst_index_dirichlet_inverseleftvaluemasktable)) * dst_positive_scale_dirichlet_inverseleftvaluemasktable) + (dst_positive_dirichlet_inverseleftvaluemasktable))) /\ (((((exists ff_h_pvs_dirichlet_inverseleftvaluemasktableentrynegative. ff_h_pvs_dirichlet_inverseleftvaluemasktableentrynegative + S (dst_negative_dirichlet_inverseleftvaluemasktable) = S ((S (dst_index_dirichlet_inverseleftvaluemasktable)) * dst_negative_scale_dirichlet_inverseleftvaluemasktable)) /\ exists ff_q_pvs_dirichlet_inverseleftvaluemasktableentrynegative. dst_negative_code_dirichlet_inverseleftvaluemasktable = ff_q_pvs_dirichlet_inverseleftvaluemasktableentrynegative * S ((S (dst_index_dirichlet_inverseleftvaluemasktable)) * dst_negative_scale_dirichlet_inverseleftvaluemasktable) + (dst_negative_dirichlet_inverseleftvaluemasktable))) /\ (exists ge_balance_positive_dirichlet_inverseleftvaluemasktableentryvalue ge_balance_negative_dirichlet_inverseleftvaluemasktableentryvalue. (((((dst_value_dirichlet_inverseleftvaluemasktable) = 2 * (ge_balance_positive_dirichlet_inverseleftvaluemasktableentryvalue) /\ (ge_balance_negative_dirichlet_inverseleftvaluemasktableentryvalue) = 0) \/ exists ge_signed_half_dirichlet_inverseleftvaluemasktableentryvaluedecode. (((dst_value_dirichlet_inverseleftvaluemasktable) = 2 * ge_signed_half_dirichlet_inverseleftvaluemasktableentryvaluedecode + 1 /\ (ge_balance_positive_dirichlet_inverseleftvaluemasktableentryvalue) = 0) /\ (ge_balance_negative_dirichlet_inverseleftvaluemasktableentryvalue) = S ge_signed_half_dirichlet_inverseleftvaluemasktableentryvaluedecode))) /\ ((dst_positive_dirichlet_inverseleftvaluemasktable) + ge_balance_negative_dirichlet_inverseleftvaluemasktableentryvalue = (dst_negative_dirichlet_inverseleftvaluemasktable) + ge_balance_positive_dirichlet_inverseleftvaluemasktableentryvalue))))))))) /\ (forall dc_index_dirichlet_inverseleftvaluemask dc_value_dirichlet_inverseleftvaluemask. (exists pvs_le_gap_dirichlet_inverseleftvaluemaskdomain. pvs_le_gap_dirichlet_inverseleftvaluemaskdomain + (dc_index_dirichlet_inverseleftvaluemask) = (dc_input_dirichlet_inverseleft)) -> (exists dst_positive_code_dirichlet_inverseleftvaluemasklookup dst_positive_scale_dirichlet_inverseleftvaluemasklookup dst_negative_code_dirichlet_inverseleftvaluemasklookup dst_negative_scale_dirichlet_inverseleftvaluemasklookup dst_positive_dirichlet_inverseleftvaluemasklookup dst_negative_dirichlet_inverseleftvaluemasklookup. (((dc_mask_dirichlet_inverseleftvalue) = (((((dst_positive_code_dirichlet_inverseleftvaluemasklookup) + (dst_positive_scale_dirichlet_inverseleftvaluemasklookup)) * S ((dst_positive_code_dirichlet_inverseleftvaluemasklookup) + (dst_positive_scale_dirichlet_inverseleftvaluemasklookup)) + ((dst_positive_scale_dirichlet_inverseleftvaluemasklookup) + (dst_positive_scale_dirichlet_inverseleftvaluemasklookup))) + (((dst_negative_code_dirichlet_inverseleftvaluemasklookup) + (dst_negative_scale_dirichlet_inverseleftvaluemasklookup)) * S ((dst_negative_code_dirichlet_inverseleftvaluemasklookup) + (dst_negative_scale_dirichlet_inverseleftvaluemasklookup)) + ((dst_negative_scale_dirichlet_inverseleftvaluemasklookup) + (dst_negative_scale_dirichlet_inverseleftvaluemasklookup)))) * S ((((dst_positive_code_dirichlet_inverseleftvaluemasklookup) + (dst_positive_scale_dirichlet_inverseleftvaluemasklookup)) * S ((dst_positive_code_dirichlet_inverseleftvaluemasklookup) + (dst_positive_scale_dirichlet_inverseleftvaluemasklookup)) + ((dst_positive_scale_dirichlet_inverseleftvaluemasklookup) + (dst_positive_scale_dirichlet_inverseleftvaluemasklookup))) + (((dst_negative_code_dirichlet_inverseleftvaluemasklookup) + (dst_negative_scale_dirichlet_inverseleftvaluemasklookup)) * S ((dst_negative_code_dirichlet_inverseleftvaluemasklookup) + (dst_negative_scale_dirichlet_inverseleftvaluemasklookup)) + ((dst_negative_scale_dirichlet_inverseleftvaluemasklookup) + (dst_negative_scale_dirichlet_inverseleftvaluemasklookup)))) + ((((dst_negative_code_dirichlet_inverseleftvaluemasklookup) + (dst_negative_scale_dirichlet_inverseleftvaluemasklookup)) * S ((dst_negative_code_dirichlet_inverseleftvaluemasklookup) + (dst_negative_scale_dirichlet_inverseleftvaluemasklookup)) + ((dst_negative_scale_dirichlet_inverseleftvaluemasklookup) + (dst_negative_scale_dirichlet_inverseleftvaluemasklookup))) + (((dst_negative_code_dirichlet_inverseleftvaluemasklookup) + (dst_negative_scale_dirichlet_inverseleftvaluemasklookup)) * S ((dst_negative_code_dirichlet_inverseleftvaluemasklookup) + (dst_negative_scale_dirichlet_inverseleftvaluemasklookup)) + ((dst_negative_scale_dirichlet_inverseleftvaluemasklookup) + (dst_negative_scale_dirichlet_inverseleftvaluemasklookup)))))) /\ (((((exists ff_h_pvs_dirichlet_inverseleftvaluemasklookuppositive. ff_h_pvs_dirichlet_inverseleftvaluemasklookuppositive + S (dst_positive_dirichlet_inverseleftvaluemasklookup) = S ((S (dc_index_dirichlet_inverseleftvaluemask)) * dst_positive_scale_dirichlet_inverseleftvaluemasklookup)) /\ exists ff_q_pvs_dirichlet_inverseleftvaluemasklookuppositive. dst_positive_code_dirichlet_inverseleftvaluemasklookup = ff_q_pvs_dirichlet_inverseleftvaluemasklookuppositive * S ((S (dc_index_dirichlet_inverseleftvaluemask)) * dst_positive_scale_dirichlet_inverseleftvaluemasklookup) + (dst_positive_dirichlet_inverseleftvaluemasklookup))) /\ (((((exists ff_h_pvs_dirichlet_inverseleftvaluemasklookupnegative. ff_h_pvs_dirichlet_inverseleftvaluemasklookupnegative + S (dst_negative_dirichlet_inverseleftvaluemasklookup) = S ((S (dc_index_dirichlet_inverseleftvaluemask)) * dst_negative_scale_dirichlet_inverseleftvaluemasklookup)) /\ exists ff_q_pvs_dirichlet_inverseleftvaluemasklookupnegative. dst_negative_code_dirichlet_inverseleftvaluemasklookup = ff_q_pvs_dirichlet_inverseleftvaluemasklookupnegative * S ((S (dc_index_dirichlet_inverseleftvaluemask)) * dst_negative_scale_dirichlet_inverseleftvaluemasklookup) + (dst_negative_dirichlet_inverseleftvaluemasklookup))) /\ (exists ge_balance_positive_dirichlet_inverseleftvaluemasklookupvalue ge_balance_negative_dirichlet_inverseleftvaluemasklookupvalue. (((((dc_value_dirichlet_inverseleftvaluemask) = 2 * (ge_balance_positive_dirichlet_inverseleftvaluemasklookupvalue) /\ (ge_balance_negative_dirichlet_inverseleftvaluemasklookupvalue) = 0) \/ exists ge_signed_half_dirichlet_inverseleftvaluemasklookupvaluedecode. (((dc_value_dirichlet_inverseleftvaluemask) = 2 * ge_signed_half_dirichlet_inverseleftvaluemasklookupvaluedecode + 1 /\ (ge_balance_positive_dirichlet_inverseleftvaluemasklookupvalue) = 0) /\ (ge_balance_negative_dirichlet_inverseleftvaluemasklookupvalue) = S ge_signed_half_dirichlet_inverseleftvaluemasklookupvaluedecode))) /\ ((dst_positive_dirichlet_inverseleftvaluemasklookup) + ge_balance_negative_dirichlet_inverseleftvaluemasklookupvalue = (dst_negative_dirichlet_inverseleftvaluemasklookup) + ge_balance_positive_dirichlet_inverseleftvaluemasklookupvalue))))))))) -> ((((~((dc_index_dirichlet_inverseleftvaluemask)=0)) /\ (exists dc_quotient_dirichlet_inverseleftvaluemaskentry dc_left_dirichlet_inverseleftvaluemaskentry dc_right_dirichlet_inverseleftvaluemaskentry. (((dc_input_dirichlet_inverseleft)=(dc_index_dirichlet_inverseleftvaluemask)*dc_quotient_dirichlet_inverseleftvaluemaskentry) /\ (((exists dst_positive_code_dirichlet_inverseleftvaluemaskentryleft dst_positive_scale_dirichlet_inverseleftvaluemaskentryleft dst_negative_code_dirichlet_inverseleftvaluemaskentryleft dst_negative_scale_dirichlet_inverseleftvaluemaskentryleft dst_positive_dirichlet_inverseleftvaluemaskentryleft dst_negative_dirichlet_inverseleftvaluemaskentryleft. ((((F)) = (((((dst_positive_code_dirichlet_inverseleftvaluemaskentryleft) + (dst_positive_scale_dirichlet_inverseleftvaluemaskentryleft)) * S ((dst_positive_code_dirichlet_inverseleftvaluemaskentryleft) + (dst_positive_scale_dirichlet_inverseleftvaluemaskentryleft)) + ((dst_positive_scale_dirichlet_inverseleftvaluemaskentryleft) + (dst_positive_scale_dirichlet_inverseleftvaluemaskentryleft))) + (((dst_negative_code_dirichlet_inverseleftvaluemaskentryleft) + (dst_negative_scale_dirichlet_inverseleftvaluemaskentryleft)) * S ((dst_negative_code_dirichlet_inverseleftvaluemaskentryleft) + (dst_negative_scale_dirichlet_inverseleftvaluemaskentryleft)) + ((dst_negative_scale_dirichlet_inverseleftvaluemaskentryleft) + (dst_negative_scale_dirichlet_inverseleftvaluemaskentryleft)))) * S ((((dst_positive_code_dirichlet_inverseleftvaluemaskentryleft) + (dst_positive_scale_dirichlet_inverseleftvaluemaskentryleft)) * S ((dst_positive_code_dirichlet_inverseleftvaluemaskentryleft) + (dst_positive_scale_dirichlet_inverseleftvaluemaskentryleft)) + ((dst_positive_scale_dirichlet_inverseleftvaluemaskentryleft) + (dst_positive_scale_dirichlet_inverseleftvaluemaskentryleft))) + (((dst_negative_code_dirichlet_inverseleftvaluemaskentryleft) + (dst_negative_scale_dirichlet_inverseleftvaluemaskentryleft)) * S ((dst_negative_code_dirichlet_inverseleftvaluemaskentryleft) + (dst_negative_scale_dirichlet_inverseleftvaluemaskentryleft)) + ((dst_negative_scale_dirichlet_inverseleftvaluemaskentryleft) + (dst_negative_scale_dirichlet_inverseleftvaluemaskentryleft)))) + ((((dst_negative_code_dirichlet_inverseleftvaluemaskentryleft) + (dst_negative_scale_dirichlet_inverseleftvaluemaskentryleft)) * S ((dst_negative_code_dirichlet_inverseleftvaluemaskentryleft) + (dst_negative_scale_dirichlet_inverseleftvaluemaskentryleft)) + ((dst_negative_scale_dirichlet_inverseleftvaluemaskentryleft) + (dst_negative_scale_dirichlet_inverseleftvaluemaskentryleft))) + (((dst_negative_code_dirichlet_inverseleftvaluemaskentryleft) + (dst_negative_scale_dirichlet_inverseleftvaluemaskentryleft)) * S ((dst_negative_code_dirichlet_inverseleftvaluemaskentryleft) + (dst_negative_scale_dirichlet_inverseleftvaluemaskentryleft)) + ((dst_negative_scale_dirichlet_inverseleftvaluemaskentryleft) + (dst_negative_scale_dirichlet_inverseleftvaluemaskentryleft)))))) /\ (((((exists ff_h_pvs_dirichlet_inverseleftvaluemaskentryleftpositive. ff_h_pvs_dirichlet_inverseleftvaluemaskentryleftpositive + S (dst_positive_dirichlet_inverseleftvaluemaskentryleft) = S ((S (dc_index_dirichlet_inverseleftvaluemask)) * dst_positive_scale_dirichlet_inverseleftvaluemaskentryleft)) /\ exists ff_q_pvs_dirichlet_inverseleftvaluemaskentryleftpositive. dst_positive_code_dirichlet_inverseleftvaluemaskentryleft = ff_q_pvs_dirichlet_inverseleftvaluemaskentryleftpositive * S ((S (dc_index_dirichlet_inverseleftvaluemask)) * dst_positive_scale_dirichlet_inverseleftvaluemaskentryleft) + (dst_positive_dirichlet_inverseleftvaluemaskentryleft))) /\ (((((exists ff_h_pvs_dirichlet_inverseleftvaluemaskentryleftnegative. ff_h_pvs_dirichlet_inverseleftvaluemaskentryleftnegative + S (dst_negative_dirichlet_inverseleftvaluemaskentryleft) = S ((S (dc_index_dirichlet_inverseleftvaluemask)) * dst_negative_scale_dirichlet_inverseleftvaluemaskentryleft)) /\ exists ff_q_pvs_dirichlet_inverseleftvaluemaskentryleftnegative. dst_negative_code_dirichlet_inverseleftvaluemaskentryleft = ff_q_pvs_dirichlet_inverseleftvaluemaskentryleftnegative * S ((S (dc_index_dirichlet_inverseleftvaluemask)) * dst_negative_scale_dirichlet_inverseleftvaluemaskentryleft) + (dst_negative_dirichlet_inverseleftvaluemaskentryleft))) /\ (exists ge_balance_positive_dirichlet_inverseleftvaluemaskentryleftvalue ge_balance_negative_dirichlet_inverseleftvaluemaskentryleftvalue. (((((dc_left_dirichlet_inverseleftvaluemaskentry) = 2 * (ge_balance_positive_dirichlet_inverseleftvaluemaskentryleftvalue) /\ (ge_balance_negative_dirichlet_inverseleftvaluemaskentryleftvalue) = 0) \/ exists ge_signed_half_dirichlet_inverseleftvaluemaskentryleftvaluedecode. (((dc_left_dirichlet_inverseleftvaluemaskentry) = 2 * ge_signed_half_dirichlet_inverseleftvaluemaskentryleftvaluedecode + 1 /\ (ge_balance_positive_dirichlet_inverseleftvaluemaskentryleftvalue) = 0) /\ (ge_balance_negative_dirichlet_inverseleftvaluemaskentryleftvalue) = S ge_signed_half_dirichlet_inverseleftvaluemaskentryleftvaluedecode))) /\ ((dst_positive_dirichlet_inverseleftvaluemaskentryleft) + ge_balance_negative_dirichlet_inverseleftvaluemaskentryleftvalue = (dst_negative_dirichlet_inverseleftvaluemaskentryleft) + ge_balance_positive_dirichlet_inverseleftvaluemaskentryleftvalue))))))))) /\ (((exists dst_positive_code_dirichlet_inverseleftvaluemaskentryright dst_positive_scale_dirichlet_inverseleftvaluemaskentryright dst_negative_code_dirichlet_inverseleftvaluemaskentryright dst_negative_scale_dirichlet_inverseleftvaluemaskentryright dst_positive_dirichlet_inverseleftvaluemaskentryright dst_negative_dirichlet_inverseleftvaluemaskentryright. ((((G)) = (((((dst_positive_code_dirichlet_inverseleftvaluemaskentryright) + (dst_positive_scale_dirichlet_inverseleftvaluemaskentryright)) * S ((dst_positive_code_dirichlet_inverseleftvaluemaskentryright) + (dst_positive_scale_dirichlet_inverseleftvaluemaskentryright)) + ((dst_positive_scale_dirichlet_inverseleftvaluemaskentryright) + (dst_positive_scale_dirichlet_inverseleftvaluemaskentryright))) + (((dst_negative_code_dirichlet_inverseleftvaluemaskentryright) + (dst_negative_scale_dirichlet_inverseleftvaluemaskentryright)) * S ((dst_negative_code_dirichlet_inverseleftvaluemaskentryright) + (dst_negative_scale_dirichlet_inverseleftvaluemaskentryright)) + ((dst_negative_scale_dirichlet_inverseleftvaluemaskentryright) + (dst_negative_scale_dirichlet_inverseleftvaluemaskentryright)))) * S ((((dst_positive_code_dirichlet_inverseleftvaluemaskentryright) + (dst_positive_scale_dirichlet_inverseleftvaluemaskentryright)) * S ((dst_positive_code_dirichlet_inverseleftvaluemaskentryright) + (dst_positive_scale_dirichlet_inverseleftvaluemaskentryright)) + ((dst_positive_scale_dirichlet_inverseleftvaluemaskentryright) + (dst_positive_scale_dirichlet_inverseleftvaluemaskentryright))) + (((dst_negative_code_dirichlet_inverseleftvaluemaskentryright) + (dst_negative_scale_dirichlet_inverseleftvaluemaskentryright)) * S ((dst_negative_code_dirichlet_inverseleftvaluemaskentryright) + (dst_negative_scale_dirichlet_inverseleftvaluemaskentryright)) + ((dst_negative_scale_dirichlet_inverseleftvaluemaskentryright) + (dst_negative_scale_dirichlet_inverseleftvaluemaskentryright)))) + ((((dst_negative_code_dirichlet_inverseleftvaluemaskentryright) + (dst_negative_scale_dirichlet_inverseleftvaluemaskentryright)) * S ((dst_negative_code_dirichlet_inverseleftvaluemaskentryright) + (dst_negative_scale_dirichlet_inverseleftvaluemaskentryright)) + ((dst_negative_scale_dirichlet_inverseleftvaluemaskentryright) + (dst_negative_scale_dirichlet_inverseleftvaluemaskentryright))) + (((dst_negative_code_dirichlet_inverseleftvaluemaskentryright) + (dst_negative_scale_dirichlet_inverseleftvaluemaskentryright)) * S ((dst_negative_code_dirichlet_inverseleftvaluemaskentryright) + (dst_negative_scale_dirichlet_inverseleftvaluemaskentryright)) + ((dst_negative_scale_dirichlet_inverseleftvaluemaskentryright) + (dst_negative_scale_dirichlet_inverseleftvaluemaskentryright)))))) /\ (((((exists ff_h_pvs_dirichlet_inverseleftvaluemaskentryrightpositive. ff_h_pvs_dirichlet_inverseleftvaluemaskentryrightpositive + S (dst_positive_dirichlet_inverseleftvaluemaskentryright) = S ((S (dc_quotient_dirichlet_inverseleftvaluemaskentry)) * dst_positive_scale_dirichlet_inverseleftvaluemaskentryright)) /\ exists ff_q_pvs_dirichlet_inverseleftvaluemaskentryrightpositive. dst_positive_code_dirichlet_inverseleftvaluemaskentryright = ff_q_pvs_dirichlet_inverseleftvaluemaskentryrightpositive * S ((S (dc_quotient_dirichlet_inverseleftvaluemaskentry)) * dst_positive_scale_dirichlet_inverseleftvaluemaskentryright) + (dst_positive_dirichlet_inverseleftvaluemaskentryright))) /\ (((((exists ff_h_pvs_dirichlet_inverseleftvaluemaskentryrightnegative. ff_h_pvs_dirichlet_inverseleftvaluemaskentryrightnegative + S (dst_negative_dirichlet_inverseleftvaluemaskentryright) = S ((S (dc_quotient_dirichlet_inverseleftvaluemaskentry)) * dst_negative_scale_dirichlet_inverseleftvaluemaskentryright)) /\ exists ff_q_pvs_dirichlet_inverseleftvaluemaskentryrightnegative. dst_negative_code_dirichlet_inverseleftvaluemaskentryright = ff_q_pvs_dirichlet_inverseleftvaluemaskentryrightnegative * S ((S (dc_quotient_dirichlet_inverseleftvaluemaskentry)) * dst_negative_scale_dirichlet_inverseleftvaluemaskentryright) + (dst_negative_dirichlet_inverseleftvaluemaskentryright))) /\ (exists ge_balance_positive_dirichlet_inverseleftvaluemaskentryrightvalue ge_balance_negative_dirichlet_inverseleftvaluemaskentryrightvalue. (((((dc_right_dirichlet_inverseleftvaluemaskentry) = 2 * (ge_balance_positive_dirichlet_inverseleftvaluemaskentryrightvalue) /\ (ge_balance_negative_dirichlet_inverseleftvaluemaskentryrightvalue) = 0) \/ exists ge_signed_half_dirichlet_inverseleftvaluemaskentryrightvaluedecode. (((dc_right_dirichlet_inverseleftvaluemaskentry) = 2 * ge_signed_half_dirichlet_inverseleftvaluemaskentryrightvaluedecode + 1 /\ (ge_balance_positive_dirichlet_inverseleftvaluemaskentryrightvalue) = 0) /\ (ge_balance_negative_dirichlet_inverseleftvaluemaskentryrightvalue) = S ge_signed_half_dirichlet_inverseleftvaluemaskentryrightvaluedecode))) /\ ((dst_positive_dirichlet_inverseleftvaluemaskentryright) + ge_balance_negative_dirichlet_inverseleftvaluemaskentryrightvalue = (dst_negative_dirichlet_inverseleftvaluemaskentryright) + ge_balance_positive_dirichlet_inverseleftvaluemaskentryrightvalue))))))))) /\ (exists sto_ap_dirichlet_inverseleftvaluemaskentryproduct sto_an_dirichlet_inverseleftvaluemaskentryproduct sto_bp_dirichlet_inverseleftvaluemaskentryproduct sto_bn_dirichlet_inverseleftvaluemaskentryproduct sto_cp_dirichlet_inverseleftvaluemaskentryproduct sto_cn_dirichlet_inverseleftvaluemaskentryproduct. (((((dc_left_dirichlet_inverseleftvaluemaskentry) = 2 * (sto_ap_dirichlet_inverseleftvaluemaskentryproduct) /\ (sto_an_dirichlet_inverseleftvaluemaskentryproduct) = 0) \/ exists ge_signed_half_dirichlet_inverseleftvaluemaskentryproductleft. (((dc_left_dirichlet_inverseleftvaluemaskentry) = 2 * ge_signed_half_dirichlet_inverseleftvaluemaskentryproductleft + 1 /\ (sto_ap_dirichlet_inverseleftvaluemaskentryproduct) = 0) /\ (sto_an_dirichlet_inverseleftvaluemaskentryproduct) = S ge_signed_half_dirichlet_inverseleftvaluemaskentryproductleft))) /\ ((((((dc_right_dirichlet_inverseleftvaluemaskentry) = 2 * (sto_bp_dirichlet_inverseleftvaluemaskentryproduct) /\ (sto_bn_dirichlet_inverseleftvaluemaskentryproduct) = 0) \/ exists ge_signed_half_dirichlet_inverseleftvaluemaskentryproductright. (((dc_right_dirichlet_inverseleftvaluemaskentry) = 2 * ge_signed_half_dirichlet_inverseleftvaluemaskentryproductright + 1 /\ (sto_bp_dirichlet_inverseleftvaluemaskentryproduct) = 0) /\ (sto_bn_dirichlet_inverseleftvaluemaskentryproduct) = S ge_signed_half_dirichlet_inverseleftvaluemaskentryproductright))) /\ ((((((dc_value_dirichlet_inverseleftvaluemask) = 2 * (sto_cp_dirichlet_inverseleftvaluemaskentryproduct) /\ (sto_cn_dirichlet_inverseleftvaluemaskentryproduct) = 0) \/ exists ge_signed_half_dirichlet_inverseleftvaluemaskentryproductoutput. (((dc_value_dirichlet_inverseleftvaluemask) = 2 * ge_signed_half_dirichlet_inverseleftvaluemaskentryproductoutput + 1 /\ (sto_cp_dirichlet_inverseleftvaluemaskentryproduct) = 0) /\ (sto_cn_dirichlet_inverseleftvaluemaskentryproduct) = S ge_signed_half_dirichlet_inverseleftvaluemaskentryproductoutput))) /\ ((sto_ap_dirichlet_inverseleftvaluemaskentryproduct * sto_bp_dirichlet_inverseleftvaluemaskentryproduct + sto_an_dirichlet_inverseleftvaluemaskentryproduct * sto_bn_dirichlet_inverseleftvaluemaskentryproduct) + sto_cn_dirichlet_inverseleftvaluemaskentryproduct = (sto_ap_dirichlet_inverseleftvaluemaskentryproduct * sto_bn_dirichlet_inverseleftvaluemaskentryproduct + sto_an_dirichlet_inverseleftvaluemaskentryproduct * sto_bp_dirichlet_inverseleftvaluemaskentryproduct) + sto_cp_dirichlet_inverseleftvaluemaskentryproduct))))))))))))))) \/ ((((dc_index_dirichlet_inverseleftvaluemask)=0 \/ ~(exists pvs_factor_dirichlet_inverseleftvaluemaskentrynondivisor. (dc_input_dirichlet_inverseleft) = (dc_index_dirichlet_inverseleftvaluemask) * pvs_factor_dirichlet_inverseleftvaluemaskentrynondivisor)) /\ ((dc_value_dirichlet_inverseleftvaluemask)=0))))))) /\ (exists dst_positive_code_dirichlet_inverseleftvaluefold dst_positive_scale_dirichlet_inverseleftvaluefold dst_negative_code_dirichlet_inverseleftvaluefold dst_negative_scale_dirichlet_inverseleftvaluefold dst_positive_sum_dirichlet_inverseleftvaluefold dst_negative_sum_dirichlet_inverseleftvaluefold. (((dc_mask_dirichlet_inverseleftvalue) = (((((dst_positive_code_dirichlet_inverseleftvaluefold) + (dst_positive_scale_dirichlet_inverseleftvaluefold)) * S ((dst_positive_code_dirichlet_inverseleftvaluefold) + (dst_positive_scale_dirichlet_inverseleftvaluefold)) + ((dst_positive_scale_dirichlet_inverseleftvaluefold) + (dst_positive_scale_dirichlet_inverseleftvaluefold))) + (((dst_negative_code_dirichlet_inverseleftvaluefold) + (dst_negative_scale_dirichlet_inverseleftvaluefold)) * S ((dst_negative_code_dirichlet_inverseleftvaluefold) + (dst_negative_scale_dirichlet_inverseleftvaluefold)) + ((dst_negative_scale_dirichlet_inverseleftvaluefold) + (dst_negative_scale_dirichlet_inverseleftvaluefold)))) * S ((((dst_positive_code_dirichlet_inverseleftvaluefold) + (dst_positive_scale_dirichlet_inverseleftvaluefold)) * S ((dst_positive_code_dirichlet_inverseleftvaluefold) + (dst_positive_scale_dirichlet_inverseleftvaluefold)) + ((dst_positive_scale_dirichlet_inverseleftvaluefold) + (dst_positive_scale_dirichlet_inverseleftvaluefold))) + (((dst_negative_code_dirichlet_inverseleftvaluefold) + (dst_negative_scale_dirichlet_inverseleftvaluefold)) * S ((dst_negative_code_dirichlet_inverseleftvaluefold) + (dst_negative_scale_dirichlet_inverseleftvaluefold)) + ((dst_negative_scale_dirichlet_inverseleftvaluefold) + (dst_negative_scale_dirichlet_inverseleftvaluefold)))) + ((((dst_negative_code_dirichlet_inverseleftvaluefold) + (dst_negative_scale_dirichlet_inverseleftvaluefold)) * S ((dst_negative_code_dirichlet_inverseleftvaluefold) + (dst_negative_scale_dirichlet_inverseleftvaluefold)) + ((dst_negative_scale_dirichlet_inverseleftvaluefold) + (dst_negative_scale_dirichlet_inverseleftvaluefold))) + (((dst_negative_code_dirichlet_inverseleftvaluefold) + (dst_negative_scale_dirichlet_inverseleftvaluefold)) * S ((dst_negative_code_dirichlet_inverseleftvaluefold) + (dst_negative_scale_dirichlet_inverseleftvaluefold)) + ((dst_negative_scale_dirichlet_inverseleftvaluefold) + (dst_negative_scale_dirichlet_inverseleftvaluefold)))))) /\ (((exists fs_u_dst_dirichlet_inverseleftvaluefoldpositive fs_v_dst_dirichlet_inverseleftvaluefoldpositive. ((((exists fs_h_dst_dirichlet_inverseleftvaluefoldpositive_body_start. fs_h_dst_dirichlet_inverseleftvaluefoldpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_dirichlet_inverseleftvaluefoldpositive)) /\ exists fs_q_dst_dirichlet_inverseleftvaluefoldpositive_body_start. fs_u_dst_dirichlet_inverseleftvaluefoldpositive = fs_q_dst_dirichlet_inverseleftvaluefoldpositive_body_start * S ((S (0)) * fs_v_dst_dirichlet_inverseleftvaluefoldpositive) + (0))) /\ ((((exists fs_h_dst_dirichlet_inverseleftvaluefoldpositive_body_terminal. fs_h_dst_dirichlet_inverseleftvaluefoldpositive_body_terminal + S (dst_positive_sum_dirichlet_inverseleftvaluefold) = S ((S (S (dc_input_dirichlet_inverseleft))) * fs_v_dst_dirichlet_inverseleftvaluefoldpositive)) /\ exists fs_q_dst_dirichlet_inverseleftvaluefoldpositive_body_terminal. fs_u_dst_dirichlet_inverseleftvaluefoldpositive = fs_q_dst_dirichlet_inverseleftvaluefoldpositive_body_terminal * S ((S (S (dc_input_dirichlet_inverseleft))) * fs_v_dst_dirichlet_inverseleftvaluefoldpositive) + (dst_positive_sum_dirichlet_inverseleftvaluefold))) /\ forall fs_i_dst_dirichlet_inverseleftvaluefoldpositive_body_steps. (exists fs_lt_dst_dirichlet_inverseleftvaluefoldpositive_body_steps_bound. fs_lt_dst_dirichlet_inverseleftvaluefoldpositive_body_steps_bound + S fs_i_dst_dirichlet_inverseleftvaluefoldpositive_body_steps = S (dc_input_dirichlet_inverseleft)) -> exists fs_a_dst_dirichlet_inverseleftvaluefoldpositive_body_steps fs_r_dst_dirichlet_inverseleftvaluefoldpositive_body_steps fs_s_dst_dirichlet_inverseleftvaluefoldpositive_body_steps. ((((exists fs_h_dst_dirichlet_inverseleftvaluefoldpositive_body_steps_summand. fs_h_dst_dirichlet_inverseleftvaluefoldpositive_body_steps_summand + S (fs_a_dst_dirichlet_inverseleftvaluefoldpositive_body_steps) = S ((S (fs_i_dst_dirichlet_inverseleftvaluefoldpositive_body_steps)) * dst_positive_scale_dirichlet_inverseleftvaluefold)) /\ exists fs_q_dst_dirichlet_inverseleftvaluefoldpositive_body_steps_summand. dst_positive_code_dirichlet_inverseleftvaluefold = fs_q_dst_dirichlet_inverseleftvaluefoldpositive_body_steps_summand * S ((S (fs_i_dst_dirichlet_inverseleftvaluefoldpositive_body_steps)) * dst_positive_scale_dirichlet_inverseleftvaluefold) + (fs_a_dst_dirichlet_inverseleftvaluefoldpositive_body_steps))) /\ ((((exists fs_h_dst_dirichlet_inverseleftvaluefoldpositive_body_steps_partial. fs_h_dst_dirichlet_inverseleftvaluefoldpositive_body_steps_partial + S (fs_r_dst_dirichlet_inverseleftvaluefoldpositive_body_steps) = S ((S (fs_i_dst_dirichlet_inverseleftvaluefoldpositive_body_steps)) * fs_v_dst_dirichlet_inverseleftvaluefoldpositive)) /\ exists fs_q_dst_dirichlet_inverseleftvaluefoldpositive_body_steps_partial. fs_u_dst_dirichlet_inverseleftvaluefoldpositive = fs_q_dst_dirichlet_inverseleftvaluefoldpositive_body_steps_partial * S ((S (fs_i_dst_dirichlet_inverseleftvaluefoldpositive_body_steps)) * fs_v_dst_dirichlet_inverseleftvaluefoldpositive) + (fs_r_dst_dirichlet_inverseleftvaluefoldpositive_body_steps))) /\ ((((exists fs_h_dst_dirichlet_inverseleftvaluefoldpositive_body_steps_successor. fs_h_dst_dirichlet_inverseleftvaluefoldpositive_body_steps_successor + S (fs_s_dst_dirichlet_inverseleftvaluefoldpositive_body_steps) = S ((S (S fs_i_dst_dirichlet_inverseleftvaluefoldpositive_body_steps)) * fs_v_dst_dirichlet_inverseleftvaluefoldpositive)) /\ exists fs_q_dst_dirichlet_inverseleftvaluefoldpositive_body_steps_successor. fs_u_dst_dirichlet_inverseleftvaluefoldpositive = fs_q_dst_dirichlet_inverseleftvaluefoldpositive_body_steps_successor * S ((S (S fs_i_dst_dirichlet_inverseleftvaluefoldpositive_body_steps)) * fs_v_dst_dirichlet_inverseleftvaluefoldpositive) + (fs_s_dst_dirichlet_inverseleftvaluefoldpositive_body_steps))) /\ fs_s_dst_dirichlet_inverseleftvaluefoldpositive_body_steps = fs_r_dst_dirichlet_inverseleftvaluefoldpositive_body_steps + fs_a_dst_dirichlet_inverseleftvaluefoldpositive_body_steps)))))) /\ (((exists fs_u_dst_dirichlet_inverseleftvaluefoldnegative fs_v_dst_dirichlet_inverseleftvaluefoldnegative. ((((exists fs_h_dst_dirichlet_inverseleftvaluefoldnegative_body_start. fs_h_dst_dirichlet_inverseleftvaluefoldnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_dirichlet_inverseleftvaluefoldnegative)) /\ exists fs_q_dst_dirichlet_inverseleftvaluefoldnegative_body_start. fs_u_dst_dirichlet_inverseleftvaluefoldnegative = fs_q_dst_dirichlet_inverseleftvaluefoldnegative_body_start * S ((S (0)) * fs_v_dst_dirichlet_inverseleftvaluefoldnegative) + (0))) /\ ((((exists fs_h_dst_dirichlet_inverseleftvaluefoldnegative_body_terminal. fs_h_dst_dirichlet_inverseleftvaluefoldnegative_body_terminal + S (dst_negative_sum_dirichlet_inverseleftvaluefold) = S ((S (S (dc_input_dirichlet_inverseleft))) * fs_v_dst_dirichlet_inverseleftvaluefoldnegative)) /\ exists fs_q_dst_dirichlet_inverseleftvaluefoldnegative_body_terminal. fs_u_dst_dirichlet_inverseleftvaluefoldnegative = fs_q_dst_dirichlet_inverseleftvaluefoldnegative_body_terminal * S ((S (S (dc_input_dirichlet_inverseleft))) * fs_v_dst_dirichlet_inverseleftvaluefoldnegative) + (dst_negative_sum_dirichlet_inverseleftvaluefold))) /\ forall fs_i_dst_dirichlet_inverseleftvaluefoldnegative_body_steps. (exists fs_lt_dst_dirichlet_inverseleftvaluefoldnegative_body_steps_bound. fs_lt_dst_dirichlet_inverseleftvaluefoldnegative_body_steps_bound + S fs_i_dst_dirichlet_inverseleftvaluefoldnegative_body_steps = S (dc_input_dirichlet_inverseleft)) -> exists fs_a_dst_dirichlet_inverseleftvaluefoldnegative_body_steps fs_r_dst_dirichlet_inverseleftvaluefoldnegative_body_steps fs_s_dst_dirichlet_inverseleftvaluefoldnegative_body_steps. ((((exists fs_h_dst_dirichlet_inverseleftvaluefoldnegative_body_steps_summand. fs_h_dst_dirichlet_inverseleftvaluefoldnegative_body_steps_summand + S (fs_a_dst_dirichlet_inverseleftvaluefoldnegative_body_steps) = S ((S (fs_i_dst_dirichlet_inverseleftvaluefoldnegative_body_steps)) * dst_negative_scale_dirichlet_inverseleftvaluefold)) /\ exists fs_q_dst_dirichlet_inverseleftvaluefoldnegative_body_steps_summand. dst_negative_code_dirichlet_inverseleftvaluefold = fs_q_dst_dirichlet_inverseleftvaluefoldnegative_body_steps_summand * S ((S (fs_i_dst_dirichlet_inverseleftvaluefoldnegative_body_steps)) * dst_negative_scale_dirichlet_inverseleftvaluefold) + (fs_a_dst_dirichlet_inverseleftvaluefoldnegative_body_steps))) /\ ((((exists fs_h_dst_dirichlet_inverseleftvaluefoldnegative_body_steps_partial. fs_h_dst_dirichlet_inverseleftvaluefoldnegative_body_steps_partial + S (fs_r_dst_dirichlet_inverseleftvaluefoldnegative_body_steps) = S ((S (fs_i_dst_dirichlet_inverseleftvaluefoldnegative_body_steps)) * fs_v_dst_dirichlet_inverseleftvaluefoldnegative)) /\ exists fs_q_dst_dirichlet_inverseleftvaluefoldnegative_body_steps_partial. fs_u_dst_dirichlet_inverseleftvaluefoldnegative = fs_q_dst_dirichlet_inverseleftvaluefoldnegative_body_steps_partial * S ((S (fs_i_dst_dirichlet_inverseleftvaluefoldnegative_body_steps)) * fs_v_dst_dirichlet_inverseleftvaluefoldnegative) + (fs_r_dst_dirichlet_inverseleftvaluefoldnegative_body_steps))) /\ ((((exists fs_h_dst_dirichlet_inverseleftvaluefoldnegative_body_steps_successor. fs_h_dst_dirichlet_inverseleftvaluefoldnegative_body_steps_successor + S (fs_s_dst_dirichlet_inverseleftvaluefoldnegative_body_steps) = S ((S (S fs_i_dst_dirichlet_inverseleftvaluefoldnegative_body_steps)) * fs_v_dst_dirichlet_inverseleftvaluefoldnegative)) /\ exists fs_q_dst_dirichlet_inverseleftvaluefoldnegative_body_steps_successor. fs_u_dst_dirichlet_inverseleftvaluefoldnegative = fs_q_dst_dirichlet_inverseleftvaluefoldnegative_body_steps_successor * S ((S (S fs_i_dst_dirichlet_inverseleftvaluefoldnegative_body_steps)) * fs_v_dst_dirichlet_inverseleftvaluefoldnegative) + (fs_s_dst_dirichlet_inverseleftvaluefoldnegative_body_steps))) /\ fs_s_dst_dirichlet_inverseleftvaluefoldnegative_body_steps = fs_r_dst_dirichlet_inverseleftvaluefoldnegative_body_steps + fs_a_dst_dirichlet_inverseleftvaluefoldnegative_body_steps)))))) /\ (exists ge_balance_positive_dirichlet_inverseleftvaluefoldresult ge_balance_negative_dirichlet_inverseleftvaluefoldresult. (((((dc_output_dirichlet_inverseleft) = 2 * (ge_balance_positive_dirichlet_inverseleftvaluefoldresult) /\ (ge_balance_negative_dirichlet_inverseleftvaluefoldresult) = 0) \/ exists ge_signed_half_dirichlet_inverseleftvaluefoldresultdecode. (((dc_output_dirichlet_inverseleft) = 2 * ge_signed_half_dirichlet_inverseleftvaluefoldresultdecode + 1 /\ (ge_balance_positive_dirichlet_inverseleftvaluefoldresult) = 0) /\ (ge_balance_negative_dirichlet_inverseleftvaluefoldresult) = S ge_signed_half_dirichlet_inverseleftvaluefoldresultdecode))) /\ ((dst_positive_sum_dirichlet_inverseleftvaluefold) + ge_balance_negative_dirichlet_inverseleftvaluefoldresult = (dst_negative_sum_dirichlet_inverseleftvaluefold) + ge_balance_positive_dirichlet_inverseleftvaluefoldresult)))))))))))))))))))) /\ (((exists dst_positive_code_dirichlet_inverserightleft dst_positive_scale_dirichlet_inverserightleft dst_negative_code_dirichlet_inverserightleft dst_negative_scale_dirichlet_inverserightleft. ((((G)) = (((((dst_positive_code_dirichlet_inverserightleft) + (dst_positive_scale_dirichlet_inverserightleft)) * S ((dst_positive_code_dirichlet_inverserightleft) + (dst_positive_scale_dirichlet_inverserightleft)) + ((dst_positive_scale_dirichlet_inverserightleft) + (dst_positive_scale_dirichlet_inverserightleft))) + (((dst_negative_code_dirichlet_inverserightleft) + (dst_negative_scale_dirichlet_inverserightleft)) * S ((dst_negative_code_dirichlet_inverserightleft) + (dst_negative_scale_dirichlet_inverserightleft)) + ((dst_negative_scale_dirichlet_inverserightleft) + (dst_negative_scale_dirichlet_inverserightleft)))) * S ((((dst_positive_code_dirichlet_inverserightleft) + (dst_positive_scale_dirichlet_inverserightleft)) * S ((dst_positive_code_dirichlet_inverserightleft) + (dst_positive_scale_dirichlet_inverserightleft)) + ((dst_positive_scale_dirichlet_inverserightleft) + (dst_positive_scale_dirichlet_inverserightleft))) + (((dst_negative_code_dirichlet_inverserightleft) + (dst_negative_scale_dirichlet_inverserightleft)) * S ((dst_negative_code_dirichlet_inverserightleft) + (dst_negative_scale_dirichlet_inverserightleft)) + ((dst_negative_scale_dirichlet_inverserightleft) + (dst_negative_scale_dirichlet_inverserightleft)))) + ((((dst_negative_code_dirichlet_inverserightleft) + (dst_negative_scale_dirichlet_inverserightleft)) * S ((dst_negative_code_dirichlet_inverserightleft) + (dst_negative_scale_dirichlet_inverserightleft)) + ((dst_negative_scale_dirichlet_inverserightleft) + (dst_negative_scale_dirichlet_inverserightleft))) + (((dst_negative_code_dirichlet_inverserightleft) + (dst_negative_scale_dirichlet_inverserightleft)) * S ((dst_negative_code_dirichlet_inverserightleft) + (dst_negative_scale_dirichlet_inverserightleft)) + ((dst_negative_scale_dirichlet_inverserightleft) + (dst_negative_scale_dirichlet_inverserightleft)))))) /\ (forall dst_index_dirichlet_inverserightleft. (exists pvs_le_gap_dirichlet_inverserightleftdomain. pvs_le_gap_dirichlet_inverserightleftdomain + (dst_index_dirichlet_inverserightleft) = ((N))) -> exists dst_positive_dirichlet_inverserightleft dst_negative_dirichlet_inverserightleft dst_value_dirichlet_inverserightleft. ((((exists ff_h_pvs_dirichlet_inverserightleftentrypositive. ff_h_pvs_dirichlet_inverserightleftentrypositive + S (dst_positive_dirichlet_inverserightleft) = S ((S (dst_index_dirichlet_inverserightleft)) * dst_positive_scale_dirichlet_inverserightleft)) /\ exists ff_q_pvs_dirichlet_inverserightleftentrypositive. dst_positive_code_dirichlet_inverserightleft = ff_q_pvs_dirichlet_inverserightleftentrypositive * S ((S (dst_index_dirichlet_inverserightleft)) * dst_positive_scale_dirichlet_inverserightleft) + (dst_positive_dirichlet_inverserightleft))) /\ (((((exists ff_h_pvs_dirichlet_inverserightleftentrynegative. ff_h_pvs_dirichlet_inverserightleftentrynegative + S (dst_negative_dirichlet_inverserightleft) = S ((S (dst_index_dirichlet_inverserightleft)) * dst_negative_scale_dirichlet_inverserightleft)) /\ exists ff_q_pvs_dirichlet_inverserightleftentrynegative. dst_negative_code_dirichlet_inverserightleft = ff_q_pvs_dirichlet_inverserightleftentrynegative * S ((S (dst_index_dirichlet_inverserightleft)) * dst_negative_scale_dirichlet_inverserightleft) + (dst_negative_dirichlet_inverserightleft))) /\ (exists ge_balance_positive_dirichlet_inverserightleftentryvalue ge_balance_negative_dirichlet_inverserightleftentryvalue. (((((dst_value_dirichlet_inverserightleft) = 2 * (ge_balance_positive_dirichlet_inverserightleftentryvalue) /\ (ge_balance_negative_dirichlet_inverserightleftentryvalue) = 0) \/ exists ge_signed_half_dirichlet_inverserightleftentryvaluedecode. (((dst_value_dirichlet_inverserightleft) = 2 * ge_signed_half_dirichlet_inverserightleftentryvaluedecode + 1 /\ (ge_balance_positive_dirichlet_inverserightleftentryvalue) = 0) /\ (ge_balance_negative_dirichlet_inverserightleftentryvalue) = S ge_signed_half_dirichlet_inverserightleftentryvaluedecode))) /\ ((dst_positive_dirichlet_inverserightleft) + ge_balance_negative_dirichlet_inverserightleftentryvalue = (dst_negative_dirichlet_inverserightleft) + ge_balance_positive_dirichlet_inverserightleftentryvalue))))))))) /\ (((exists dst_positive_code_dirichlet_inverserightright dst_positive_scale_dirichlet_inverserightright dst_negative_code_dirichlet_inverserightright dst_negative_scale_dirichlet_inverserightright. ((((F)) = (((((dst_positive_code_dirichlet_inverserightright) + (dst_positive_scale_dirichlet_inverserightright)) * S ((dst_positive_code_dirichlet_inverserightright) + (dst_positive_scale_dirichlet_inverserightright)) + ((dst_positive_scale_dirichlet_inverserightright) + (dst_positive_scale_dirichlet_inverserightright))) + (((dst_negative_code_dirichlet_inverserightright) + (dst_negative_scale_dirichlet_inverserightright)) * S ((dst_negative_code_dirichlet_inverserightright) + (dst_negative_scale_dirichlet_inverserightright)) + ((dst_negative_scale_dirichlet_inverserightright) + (dst_negative_scale_dirichlet_inverserightright)))) * S ((((dst_positive_code_dirichlet_inverserightright) + (dst_positive_scale_dirichlet_inverserightright)) * S ((dst_positive_code_dirichlet_inverserightright) + (dst_positive_scale_dirichlet_inverserightright)) + ((dst_positive_scale_dirichlet_inverserightright) + (dst_positive_scale_dirichlet_inverserightright))) + (((dst_negative_code_dirichlet_inverserightright) + (dst_negative_scale_dirichlet_inverserightright)) * S ((dst_negative_code_dirichlet_inverserightright) + (dst_negative_scale_dirichlet_inverserightright)) + ((dst_negative_scale_dirichlet_inverserightright) + (dst_negative_scale_dirichlet_inverserightright)))) + ((((dst_negative_code_dirichlet_inverserightright) + (dst_negative_scale_dirichlet_inverserightright)) * S ((dst_negative_code_dirichlet_inverserightright) + (dst_negative_scale_dirichlet_inverserightright)) + ((dst_negative_scale_dirichlet_inverserightright) + (dst_negative_scale_dirichlet_inverserightright))) + (((dst_negative_code_dirichlet_inverserightright) + (dst_negative_scale_dirichlet_inverserightright)) * S ((dst_negative_code_dirichlet_inverserightright) + (dst_negative_scale_dirichlet_inverserightright)) + ((dst_negative_scale_dirichlet_inverserightright) + (dst_negative_scale_dirichlet_inverserightright)))))) /\ (forall dst_index_dirichlet_inverserightright. (exists pvs_le_gap_dirichlet_inverserightrightdomain. pvs_le_gap_dirichlet_inverserightrightdomain + (dst_index_dirichlet_inverserightright) = ((N))) -> exists dst_positive_dirichlet_inverserightright dst_negative_dirichlet_inverserightright dst_value_dirichlet_inverserightright. ((((exists ff_h_pvs_dirichlet_inverserightrightentrypositive. ff_h_pvs_dirichlet_inverserightrightentrypositive + S (dst_positive_dirichlet_inverserightright) = S ((S (dst_index_dirichlet_inverserightright)) * dst_positive_scale_dirichlet_inverserightright)) /\ exists ff_q_pvs_dirichlet_inverserightrightentrypositive. dst_positive_code_dirichlet_inverserightright = ff_q_pvs_dirichlet_inverserightrightentrypositive * S ((S (dst_index_dirichlet_inverserightright)) * dst_positive_scale_dirichlet_inverserightright) + (dst_positive_dirichlet_inverserightright))) /\ (((((exists ff_h_pvs_dirichlet_inverserightrightentrynegative. ff_h_pvs_dirichlet_inverserightrightentrynegative + S (dst_negative_dirichlet_inverserightright) = S ((S (dst_index_dirichlet_inverserightright)) * dst_negative_scale_dirichlet_inverserightright)) /\ exists ff_q_pvs_dirichlet_inverserightrightentrynegative. dst_negative_code_dirichlet_inverserightright = ff_q_pvs_dirichlet_inverserightrightentrynegative * S ((S (dst_index_dirichlet_inverserightright)) * dst_negative_scale_dirichlet_inverserightright) + (dst_negative_dirichlet_inverserightright))) /\ (exists ge_balance_positive_dirichlet_inverserightrightentryvalue ge_balance_negative_dirichlet_inverserightrightentryvalue. (((((dst_value_dirichlet_inverserightright) = 2 * (ge_balance_positive_dirichlet_inverserightrightentryvalue) /\ (ge_balance_negative_dirichlet_inverserightrightentryvalue) = 0) \/ exists ge_signed_half_dirichlet_inverserightrightentryvaluedecode. (((dst_value_dirichlet_inverserightright) = 2 * ge_signed_half_dirichlet_inverserightrightentryvaluedecode + 1 /\ (ge_balance_positive_dirichlet_inverserightrightentryvalue) = 0) /\ (ge_balance_negative_dirichlet_inverserightrightentryvalue) = S ge_signed_half_dirichlet_inverserightrightentryvaluedecode))) /\ ((dst_positive_dirichlet_inverserightright) + ge_balance_negative_dirichlet_inverserightrightentryvalue = (dst_negative_dirichlet_inverserightright) + ge_balance_positive_dirichlet_inverserightrightentryvalue))))))))) /\ (((exists dst_positive_code_dirichlet_inverserighttable dst_positive_scale_dirichlet_inverserighttable dst_negative_code_dirichlet_inverserighttable dst_negative_scale_dirichlet_inverserighttable. (((di_delta_dirichlet_inverse) = (((((dst_positive_code_dirichlet_inverserighttable) + (dst_positive_scale_dirichlet_inverserighttable)) * S ((dst_positive_code_dirichlet_inverserighttable) + (dst_positive_scale_dirichlet_inverserighttable)) + ((dst_positive_scale_dirichlet_inverserighttable) + (dst_positive_scale_dirichlet_inverserighttable))) + (((dst_negative_code_dirichlet_inverserighttable) + (dst_negative_scale_dirichlet_inverserighttable)) * S ((dst_negative_code_dirichlet_inverserighttable) + (dst_negative_scale_dirichlet_inverserighttable)) + ((dst_negative_scale_dirichlet_inverserighttable) + (dst_negative_scale_dirichlet_inverserighttable)))) * S ((((dst_positive_code_dirichlet_inverserighttable) + (dst_positive_scale_dirichlet_inverserighttable)) * S ((dst_positive_code_dirichlet_inverserighttable) + (dst_positive_scale_dirichlet_inverserighttable)) + ((dst_positive_scale_dirichlet_inverserighttable) + (dst_positive_scale_dirichlet_inverserighttable))) + (((dst_negative_code_dirichlet_inverserighttable) + (dst_negative_scale_dirichlet_inverserighttable)) * S ((dst_negative_code_dirichlet_inverserighttable) + (dst_negative_scale_dirichlet_inverserighttable)) + ((dst_negative_scale_dirichlet_inverserighttable) + (dst_negative_scale_dirichlet_inverserighttable)))) + ((((dst_negative_code_dirichlet_inverserighttable) + (dst_negative_scale_dirichlet_inverserighttable)) * S ((dst_negative_code_dirichlet_inverserighttable) + (dst_negative_scale_dirichlet_inverserighttable)) + ((dst_negative_scale_dirichlet_inverserighttable) + (dst_negative_scale_dirichlet_inverserighttable))) + (((dst_negative_code_dirichlet_inverserighttable) + (dst_negative_scale_dirichlet_inverserighttable)) * S ((dst_negative_code_dirichlet_inverserighttable) + (dst_negative_scale_dirichlet_inverserighttable)) + ((dst_negative_scale_dirichlet_inverserighttable) + (dst_negative_scale_dirichlet_inverserighttable)))))) /\ (forall dst_index_dirichlet_inverserighttable. (exists pvs_le_gap_dirichlet_inverserighttabledomain. pvs_le_gap_dirichlet_inverserighttabledomain + (dst_index_dirichlet_inverserighttable) = ((N))) -> exists dst_positive_dirichlet_inverserighttable dst_negative_dirichlet_inverserighttable dst_value_dirichlet_inverserighttable. ((((exists ff_h_pvs_dirichlet_inverserighttableentrypositive. ff_h_pvs_dirichlet_inverserighttableentrypositive + S (dst_positive_dirichlet_inverserighttable) = S ((S (dst_index_dirichlet_inverserighttable)) * dst_positive_scale_dirichlet_inverserighttable)) /\ exists ff_q_pvs_dirichlet_inverserighttableentrypositive. dst_positive_code_dirichlet_inverserighttable = ff_q_pvs_dirichlet_inverserighttableentrypositive * S ((S (dst_index_dirichlet_inverserighttable)) * dst_positive_scale_dirichlet_inverserighttable) + (dst_positive_dirichlet_inverserighttable))) /\ (((((exists ff_h_pvs_dirichlet_inverserighttableentrynegative. ff_h_pvs_dirichlet_inverserighttableentrynegative + S (dst_negative_dirichlet_inverserighttable) = S ((S (dst_index_dirichlet_inverserighttable)) * dst_negative_scale_dirichlet_inverserighttable)) /\ exists ff_q_pvs_dirichlet_inverserighttableentrynegative. dst_negative_code_dirichlet_inverserighttable = ff_q_pvs_dirichlet_inverserighttableentrynegative * S ((S (dst_index_dirichlet_inverserighttable)) * dst_negative_scale_dirichlet_inverserighttable) + (dst_negative_dirichlet_inverserighttable))) /\ (exists ge_balance_positive_dirichlet_inverserighttableentryvalue ge_balance_negative_dirichlet_inverserighttableentryvalue. (((((dst_value_dirichlet_inverserighttable) = 2 * (ge_balance_positive_dirichlet_inverserighttableentryvalue) /\ (ge_balance_negative_dirichlet_inverserighttableentryvalue) = 0) \/ exists ge_signed_half_dirichlet_inverserighttableentryvaluedecode. (((dst_value_dirichlet_inverserighttable) = 2 * ge_signed_half_dirichlet_inverserighttableentryvaluedecode + 1 /\ (ge_balance_positive_dirichlet_inverserighttableentryvalue) = 0) /\ (ge_balance_negative_dirichlet_inverserighttableentryvalue) = S ge_signed_half_dirichlet_inverserighttableentryvaluedecode))) /\ ((dst_positive_dirichlet_inverserighttable) + ge_balance_negative_dirichlet_inverserighttableentryvalue = (dst_negative_dirichlet_inverserighttable) + ge_balance_positive_dirichlet_inverserighttableentryvalue))))))))) /\ (forall dc_input_dirichlet_inverseright dc_output_dirichlet_inverseright. ~(dc_input_dirichlet_inverseright=0) -> (exists pvs_le_gap_dirichlet_inverserightdomain. pvs_le_gap_dirichlet_inverserightdomain + (dc_input_dirichlet_inverseright) = ((N))) -> (exists dst_positive_code_dirichlet_inverserightlookup dst_positive_scale_dirichlet_inverserightlookup dst_negative_code_dirichlet_inverserightlookup dst_negative_scale_dirichlet_inverserightlookup dst_positive_dirichlet_inverserightlookup dst_negative_dirichlet_inverserightlookup. (((di_delta_dirichlet_inverse) = (((((dst_positive_code_dirichlet_inverserightlookup) + (dst_positive_scale_dirichlet_inverserightlookup)) * S ((dst_positive_code_dirichlet_inverserightlookup) + (dst_positive_scale_dirichlet_inverserightlookup)) + ((dst_positive_scale_dirichlet_inverserightlookup) + (dst_positive_scale_dirichlet_inverserightlookup))) + (((dst_negative_code_dirichlet_inverserightlookup) + (dst_negative_scale_dirichlet_inverserightlookup)) * S ((dst_negative_code_dirichlet_inverserightlookup) + (dst_negative_scale_dirichlet_inverserightlookup)) + ((dst_negative_scale_dirichlet_inverserightlookup) + (dst_negative_scale_dirichlet_inverserightlookup)))) * S ((((dst_positive_code_dirichlet_inverserightlookup) + (dst_positive_scale_dirichlet_inverserightlookup)) * S ((dst_positive_code_dirichlet_inverserightlookup) + (dst_positive_scale_dirichlet_inverserightlookup)) + ((dst_positive_scale_dirichlet_inverserightlookup) + (dst_positive_scale_dirichlet_inverserightlookup))) + (((dst_negative_code_dirichlet_inverserightlookup) + (dst_negative_scale_dirichlet_inverserightlookup)) * S ((dst_negative_code_dirichlet_inverserightlookup) + (dst_negative_scale_dirichlet_inverserightlookup)) + ((dst_negative_scale_dirichlet_inverserightlookup) + (dst_negative_scale_dirichlet_inverserightlookup)))) + ((((dst_negative_code_dirichlet_inverserightlookup) + (dst_negative_scale_dirichlet_inverserightlookup)) * S ((dst_negative_code_dirichlet_inverserightlookup) + (dst_negative_scale_dirichlet_inverserightlookup)) + ((dst_negative_scale_dirichlet_inverserightlookup) + (dst_negative_scale_dirichlet_inverserightlookup))) + (((dst_negative_code_dirichlet_inverserightlookup) + (dst_negative_scale_dirichlet_inverserightlookup)) * S ((dst_negative_code_dirichlet_inverserightlookup) + (dst_negative_scale_dirichlet_inverserightlookup)) + ((dst_negative_scale_dirichlet_inverserightlookup) + (dst_negative_scale_dirichlet_inverserightlookup)))))) /\ (((((exists ff_h_pvs_dirichlet_inverserightlookuppositive. ff_h_pvs_dirichlet_inverserightlookuppositive + S (dst_positive_dirichlet_inverserightlookup) = S ((S (dc_input_dirichlet_inverseright)) * dst_positive_scale_dirichlet_inverserightlookup)) /\ exists ff_q_pvs_dirichlet_inverserightlookuppositive. dst_positive_code_dirichlet_inverserightlookup = ff_q_pvs_dirichlet_inverserightlookuppositive * S ((S (dc_input_dirichlet_inverseright)) * dst_positive_scale_dirichlet_inverserightlookup) + (dst_positive_dirichlet_inverserightlookup))) /\ (((((exists ff_h_pvs_dirichlet_inverserightlookupnegative. ff_h_pvs_dirichlet_inverserightlookupnegative + S (dst_negative_dirichlet_inverserightlookup) = S ((S (dc_input_dirichlet_inverseright)) * dst_negative_scale_dirichlet_inverserightlookup)) /\ exists ff_q_pvs_dirichlet_inverserightlookupnegative. dst_negative_code_dirichlet_inverserightlookup = ff_q_pvs_dirichlet_inverserightlookupnegative * S ((S (dc_input_dirichlet_inverseright)) * dst_negative_scale_dirichlet_inverserightlookup) + (dst_negative_dirichlet_inverserightlookup))) /\ (exists ge_balance_positive_dirichlet_inverserightlookupvalue ge_balance_negative_dirichlet_inverserightlookupvalue. (((((dc_output_dirichlet_inverseright) = 2 * (ge_balance_positive_dirichlet_inverserightlookupvalue) /\ (ge_balance_negative_dirichlet_inverserightlookupvalue) = 0) \/ exists ge_signed_half_dirichlet_inverserightlookupvaluedecode. (((dc_output_dirichlet_inverseright) = 2 * ge_signed_half_dirichlet_inverserightlookupvaluedecode + 1 /\ (ge_balance_positive_dirichlet_inverserightlookupvalue) = 0) /\ (ge_balance_negative_dirichlet_inverserightlookupvalue) = S ge_signed_half_dirichlet_inverserightlookupvaluedecode))) /\ ((dst_positive_dirichlet_inverserightlookup) + ge_balance_negative_dirichlet_inverserightlookupvalue = (dst_negative_dirichlet_inverserightlookup) + ge_balance_positive_dirichlet_inverserightlookupvalue))))))))) -> (((~((dc_input_dirichlet_inverseright)=0)) /\ (exists dc_mask_dirichlet_inverserightvalue. ((((exists dst_positive_code_dirichlet_inverserightvaluemasktable dst_positive_scale_dirichlet_inverserightvaluemasktable dst_negative_code_dirichlet_inverserightvaluemasktable dst_negative_scale_dirichlet_inverserightvaluemasktable. (((dc_mask_dirichlet_inverserightvalue) = (((((dst_positive_code_dirichlet_inverserightvaluemasktable) + (dst_positive_scale_dirichlet_inverserightvaluemasktable)) * S ((dst_positive_code_dirichlet_inverserightvaluemasktable) + (dst_positive_scale_dirichlet_inverserightvaluemasktable)) + ((dst_positive_scale_dirichlet_inverserightvaluemasktable) + (dst_positive_scale_dirichlet_inverserightvaluemasktable))) + (((dst_negative_code_dirichlet_inverserightvaluemasktable) + (dst_negative_scale_dirichlet_inverserightvaluemasktable)) * S ((dst_negative_code_dirichlet_inverserightvaluemasktable) + (dst_negative_scale_dirichlet_inverserightvaluemasktable)) + ((dst_negative_scale_dirichlet_inverserightvaluemasktable) + (dst_negative_scale_dirichlet_inverserightvaluemasktable)))) * S ((((dst_positive_code_dirichlet_inverserightvaluemasktable) + (dst_positive_scale_dirichlet_inverserightvaluemasktable)) * S ((dst_positive_code_dirichlet_inverserightvaluemasktable) + (dst_positive_scale_dirichlet_inverserightvaluemasktable)) + ((dst_positive_scale_dirichlet_inverserightvaluemasktable) + (dst_positive_scale_dirichlet_inverserightvaluemasktable))) + (((dst_negative_code_dirichlet_inverserightvaluemasktable) + (dst_negative_scale_dirichlet_inverserightvaluemasktable)) * S ((dst_negative_code_dirichlet_inverserightvaluemasktable) + (dst_negative_scale_dirichlet_inverserightvaluemasktable)) + ((dst_negative_scale_dirichlet_inverserightvaluemasktable) + (dst_negative_scale_dirichlet_inverserightvaluemasktable)))) + ((((dst_negative_code_dirichlet_inverserightvaluemasktable) + (dst_negative_scale_dirichlet_inverserightvaluemasktable)) * S ((dst_negative_code_dirichlet_inverserightvaluemasktable) + (dst_negative_scale_dirichlet_inverserightvaluemasktable)) + ((dst_negative_scale_dirichlet_inverserightvaluemasktable) + (dst_negative_scale_dirichlet_inverserightvaluemasktable))) + (((dst_negative_code_dirichlet_inverserightvaluemasktable) + (dst_negative_scale_dirichlet_inverserightvaluemasktable)) * S ((dst_negative_code_dirichlet_inverserightvaluemasktable) + (dst_negative_scale_dirichlet_inverserightvaluemasktable)) + ((dst_negative_scale_dirichlet_inverserightvaluemasktable) + (dst_negative_scale_dirichlet_inverserightvaluemasktable)))))) /\ (forall dst_index_dirichlet_inverserightvaluemasktable. (exists pvs_le_gap_dirichlet_inverserightvaluemasktabledomain. pvs_le_gap_dirichlet_inverserightvaluemasktabledomain + (dst_index_dirichlet_inverserightvaluemasktable) = (dc_input_dirichlet_inverseright)) -> exists dst_positive_dirichlet_inverserightvaluemasktable dst_negative_dirichlet_inverserightvaluemasktable dst_value_dirichlet_inverserightvaluemasktable. ((((exists ff_h_pvs_dirichlet_inverserightvaluemasktableentrypositive. ff_h_pvs_dirichlet_inverserightvaluemasktableentrypositive + S (dst_positive_dirichlet_inverserightvaluemasktable) = S ((S (dst_index_dirichlet_inverserightvaluemasktable)) * dst_positive_scale_dirichlet_inverserightvaluemasktable)) /\ exists ff_q_pvs_dirichlet_inverserightvaluemasktableentrypositive. dst_positive_code_dirichlet_inverserightvaluemasktable = ff_q_pvs_dirichlet_inverserightvaluemasktableentrypositive * S ((S (dst_index_dirichlet_inverserightvaluemasktable)) * dst_positive_scale_dirichlet_inverserightvaluemasktable) + (dst_positive_dirichlet_inverserightvaluemasktable))) /\ (((((exists ff_h_pvs_dirichlet_inverserightvaluemasktableentrynegative. ff_h_pvs_dirichlet_inverserightvaluemasktableentrynegative + S (dst_negative_dirichlet_inverserightvaluemasktable) = S ((S (dst_index_dirichlet_inverserightvaluemasktable)) * dst_negative_scale_dirichlet_inverserightvaluemasktable)) /\ exists ff_q_pvs_dirichlet_inverserightvaluemasktableentrynegative. dst_negative_code_dirichlet_inverserightvaluemasktable = ff_q_pvs_dirichlet_inverserightvaluemasktableentrynegative * S ((S (dst_index_dirichlet_inverserightvaluemasktable)) * dst_negative_scale_dirichlet_inverserightvaluemasktable) + (dst_negative_dirichlet_inverserightvaluemasktable))) /\ (exists ge_balance_positive_dirichlet_inverserightvaluemasktableentryvalue ge_balance_negative_dirichlet_inverserightvaluemasktableentryvalue. (((((dst_value_dirichlet_inverserightvaluemasktable) = 2 * (ge_balance_positive_dirichlet_inverserightvaluemasktableentryvalue) /\ (ge_balance_negative_dirichlet_inverserightvaluemasktableentryvalue) = 0) \/ exists ge_signed_half_dirichlet_inverserightvaluemasktableentryvaluedecode. (((dst_value_dirichlet_inverserightvaluemasktable) = 2 * ge_signed_half_dirichlet_inverserightvaluemasktableentryvaluedecode + 1 /\ (ge_balance_positive_dirichlet_inverserightvaluemasktableentryvalue) = 0) /\ (ge_balance_negative_dirichlet_inverserightvaluemasktableentryvalue) = S ge_signed_half_dirichlet_inverserightvaluemasktableentryvaluedecode))) /\ ((dst_positive_dirichlet_inverserightvaluemasktable) + ge_balance_negative_dirichlet_inverserightvaluemasktableentryvalue = (dst_negative_dirichlet_inverserightvaluemasktable) + ge_balance_positive_dirichlet_inverserightvaluemasktableentryvalue))))))))) /\ (forall dc_index_dirichlet_inverserightvaluemask dc_value_dirichlet_inverserightvaluemask. (exists pvs_le_gap_dirichlet_inverserightvaluemaskdomain. pvs_le_gap_dirichlet_inverserightvaluemaskdomain + (dc_index_dirichlet_inverserightvaluemask) = (dc_input_dirichlet_inverseright)) -> (exists dst_positive_code_dirichlet_inverserightvaluemasklookup dst_positive_scale_dirichlet_inverserightvaluemasklookup dst_negative_code_dirichlet_inverserightvaluemasklookup dst_negative_scale_dirichlet_inverserightvaluemasklookup dst_positive_dirichlet_inverserightvaluemasklookup dst_negative_dirichlet_inverserightvaluemasklookup. (((dc_mask_dirichlet_inverserightvalue) = (((((dst_positive_code_dirichlet_inverserightvaluemasklookup) + (dst_positive_scale_dirichlet_inverserightvaluemasklookup)) * S ((dst_positive_code_dirichlet_inverserightvaluemasklookup) + (dst_positive_scale_dirichlet_inverserightvaluemasklookup)) + ((dst_positive_scale_dirichlet_inverserightvaluemasklookup) + (dst_positive_scale_dirichlet_inverserightvaluemasklookup))) + (((dst_negative_code_dirichlet_inverserightvaluemasklookup) + (dst_negative_scale_dirichlet_inverserightvaluemasklookup)) * S ((dst_negative_code_dirichlet_inverserightvaluemasklookup) + (dst_negative_scale_dirichlet_inverserightvaluemasklookup)) + ((dst_negative_scale_dirichlet_inverserightvaluemasklookup) + (dst_negative_scale_dirichlet_inverserightvaluemasklookup)))) * S ((((dst_positive_code_dirichlet_inverserightvaluemasklookup) + (dst_positive_scale_dirichlet_inverserightvaluemasklookup)) * S ((dst_positive_code_dirichlet_inverserightvaluemasklookup) + (dst_positive_scale_dirichlet_inverserightvaluemasklookup)) + ((dst_positive_scale_dirichlet_inverserightvaluemasklookup) + (dst_positive_scale_dirichlet_inverserightvaluemasklookup))) + (((dst_negative_code_dirichlet_inverserightvaluemasklookup) + (dst_negative_scale_dirichlet_inverserightvaluemasklookup)) * S ((dst_negative_code_dirichlet_inverserightvaluemasklookup) + (dst_negative_scale_dirichlet_inverserightvaluemasklookup)) + ((dst_negative_scale_dirichlet_inverserightvaluemasklookup) + (dst_negative_scale_dirichlet_inverserightvaluemasklookup)))) + ((((dst_negative_code_dirichlet_inverserightvaluemasklookup) + (dst_negative_scale_dirichlet_inverserightvaluemasklookup)) * S ((dst_negative_code_dirichlet_inverserightvaluemasklookup) + (dst_negative_scale_dirichlet_inverserightvaluemasklookup)) + ((dst_negative_scale_dirichlet_inverserightvaluemasklookup) + (dst_negative_scale_dirichlet_inverserightvaluemasklookup))) + (((dst_negative_code_dirichlet_inverserightvaluemasklookup) + (dst_negative_scale_dirichlet_inverserightvaluemasklookup)) * S ((dst_negative_code_dirichlet_inverserightvaluemasklookup) + (dst_negative_scale_dirichlet_inverserightvaluemasklookup)) + ((dst_negative_scale_dirichlet_inverserightvaluemasklookup) + (dst_negative_scale_dirichlet_inverserightvaluemasklookup)))))) /\ (((((exists ff_h_pvs_dirichlet_inverserightvaluemasklookuppositive. ff_h_pvs_dirichlet_inverserightvaluemasklookuppositive + S (dst_positive_dirichlet_inverserightvaluemasklookup) = S ((S (dc_index_dirichlet_inverserightvaluemask)) * dst_positive_scale_dirichlet_inverserightvaluemasklookup)) /\ exists ff_q_pvs_dirichlet_inverserightvaluemasklookuppositive. dst_positive_code_dirichlet_inverserightvaluemasklookup = ff_q_pvs_dirichlet_inverserightvaluemasklookuppositive * S ((S (dc_index_dirichlet_inverserightvaluemask)) * dst_positive_scale_dirichlet_inverserightvaluemasklookup) + (dst_positive_dirichlet_inverserightvaluemasklookup))) /\ (((((exists ff_h_pvs_dirichlet_inverserightvaluemasklookupnegative. ff_h_pvs_dirichlet_inverserightvaluemasklookupnegative + S (dst_negative_dirichlet_inverserightvaluemasklookup) = S ((S (dc_index_dirichlet_inverserightvaluemask)) * dst_negative_scale_dirichlet_inverserightvaluemasklookup)) /\ exists ff_q_pvs_dirichlet_inverserightvaluemasklookupnegative. dst_negative_code_dirichlet_inverserightvaluemasklookup = ff_q_pvs_dirichlet_inverserightvaluemasklookupnegative * S ((S (dc_index_dirichlet_inverserightvaluemask)) * dst_negative_scale_dirichlet_inverserightvaluemasklookup) + (dst_negative_dirichlet_inverserightvaluemasklookup))) /\ (exists ge_balance_positive_dirichlet_inverserightvaluemasklookupvalue ge_balance_negative_dirichlet_inverserightvaluemasklookupvalue. (((((dc_value_dirichlet_inverserightvaluemask) = 2 * (ge_balance_positive_dirichlet_inverserightvaluemasklookupvalue) /\ (ge_balance_negative_dirichlet_inverserightvaluemasklookupvalue) = 0) \/ exists ge_signed_half_dirichlet_inverserightvaluemasklookupvaluedecode. (((dc_value_dirichlet_inverserightvaluemask) = 2 * ge_signed_half_dirichlet_inverserightvaluemasklookupvaluedecode + 1 /\ (ge_balance_positive_dirichlet_inverserightvaluemasklookupvalue) = 0) /\ (ge_balance_negative_dirichlet_inverserightvaluemasklookupvalue) = S ge_signed_half_dirichlet_inverserightvaluemasklookupvaluedecode))) /\ ((dst_positive_dirichlet_inverserightvaluemasklookup) + ge_balance_negative_dirichlet_inverserightvaluemasklookupvalue = (dst_negative_dirichlet_inverserightvaluemasklookup) + ge_balance_positive_dirichlet_inverserightvaluemasklookupvalue))))))))) -> ((((~((dc_index_dirichlet_inverserightvaluemask)=0)) /\ (exists dc_quotient_dirichlet_inverserightvaluemaskentry dc_left_dirichlet_inverserightvaluemaskentry dc_right_dirichlet_inverserightvaluemaskentry. (((dc_input_dirichlet_inverseright)=(dc_index_dirichlet_inverserightvaluemask)*dc_quotient_dirichlet_inverserightvaluemaskentry) /\ (((exists dst_positive_code_dirichlet_inverserightvaluemaskentryleft dst_positive_scale_dirichlet_inverserightvaluemaskentryleft dst_negative_code_dirichlet_inverserightvaluemaskentryleft dst_negative_scale_dirichlet_inverserightvaluemaskentryleft dst_positive_dirichlet_inverserightvaluemaskentryleft dst_negative_dirichlet_inverserightvaluemaskentryleft. ((((G)) = (((((dst_positive_code_dirichlet_inverserightvaluemaskentryleft) + (dst_positive_scale_dirichlet_inverserightvaluemaskentryleft)) * S ((dst_positive_code_dirichlet_inverserightvaluemaskentryleft) + (dst_positive_scale_dirichlet_inverserightvaluemaskentryleft)) + ((dst_positive_scale_dirichlet_inverserightvaluemaskentryleft) + (dst_positive_scale_dirichlet_inverserightvaluemaskentryleft))) + (((dst_negative_code_dirichlet_inverserightvaluemaskentryleft) + (dst_negative_scale_dirichlet_inverserightvaluemaskentryleft)) * S ((dst_negative_code_dirichlet_inverserightvaluemaskentryleft) + (dst_negative_scale_dirichlet_inverserightvaluemaskentryleft)) + ((dst_negative_scale_dirichlet_inverserightvaluemaskentryleft) + (dst_negative_scale_dirichlet_inverserightvaluemaskentryleft)))) * S ((((dst_positive_code_dirichlet_inverserightvaluemaskentryleft) + (dst_positive_scale_dirichlet_inverserightvaluemaskentryleft)) * S ((dst_positive_code_dirichlet_inverserightvaluemaskentryleft) + (dst_positive_scale_dirichlet_inverserightvaluemaskentryleft)) + ((dst_positive_scale_dirichlet_inverserightvaluemaskentryleft) + (dst_positive_scale_dirichlet_inverserightvaluemaskentryleft))) + (((dst_negative_code_dirichlet_inverserightvaluemaskentryleft) + (dst_negative_scale_dirichlet_inverserightvaluemaskentryleft)) * S ((dst_negative_code_dirichlet_inverserightvaluemaskentryleft) + (dst_negative_scale_dirichlet_inverserightvaluemaskentryleft)) + ((dst_negative_scale_dirichlet_inverserightvaluemaskentryleft) + (dst_negative_scale_dirichlet_inverserightvaluemaskentryleft)))) + ((((dst_negative_code_dirichlet_inverserightvaluemaskentryleft) + (dst_negative_scale_dirichlet_inverserightvaluemaskentryleft)) * S ((dst_negative_code_dirichlet_inverserightvaluemaskentryleft) + (dst_negative_scale_dirichlet_inverserightvaluemaskentryleft)) + ((dst_negative_scale_dirichlet_inverserightvaluemaskentryleft) + (dst_negative_scale_dirichlet_inverserightvaluemaskentryleft))) + (((dst_negative_code_dirichlet_inverserightvaluemaskentryleft) + (dst_negative_scale_dirichlet_inverserightvaluemaskentryleft)) * S ((dst_negative_code_dirichlet_inverserightvaluemaskentryleft) + (dst_negative_scale_dirichlet_inverserightvaluemaskentryleft)) + ((dst_negative_scale_dirichlet_inverserightvaluemaskentryleft) + (dst_negative_scale_dirichlet_inverserightvaluemaskentryleft)))))) /\ (((((exists ff_h_pvs_dirichlet_inverserightvaluemaskentryleftpositive. ff_h_pvs_dirichlet_inverserightvaluemaskentryleftpositive + S (dst_positive_dirichlet_inverserightvaluemaskentryleft) = S ((S (dc_index_dirichlet_inverserightvaluemask)) * dst_positive_scale_dirichlet_inverserightvaluemaskentryleft)) /\ exists ff_q_pvs_dirichlet_inverserightvaluemaskentryleftpositive. dst_positive_code_dirichlet_inverserightvaluemaskentryleft = ff_q_pvs_dirichlet_inverserightvaluemaskentryleftpositive * S ((S (dc_index_dirichlet_inverserightvaluemask)) * dst_positive_scale_dirichlet_inverserightvaluemaskentryleft) + (dst_positive_dirichlet_inverserightvaluemaskentryleft))) /\ (((((exists ff_h_pvs_dirichlet_inverserightvaluemaskentryleftnegative. ff_h_pvs_dirichlet_inverserightvaluemaskentryleftnegative + S (dst_negative_dirichlet_inverserightvaluemaskentryleft) = S ((S (dc_index_dirichlet_inverserightvaluemask)) * dst_negative_scale_dirichlet_inverserightvaluemaskentryleft)) /\ exists ff_q_pvs_dirichlet_inverserightvaluemaskentryleftnegative. dst_negative_code_dirichlet_inverserightvaluemaskentryleft = ff_q_pvs_dirichlet_inverserightvaluemaskentryleftnegative * S ((S (dc_index_dirichlet_inverserightvaluemask)) * dst_negative_scale_dirichlet_inverserightvaluemaskentryleft) + (dst_negative_dirichlet_inverserightvaluemaskentryleft))) /\ (exists ge_balance_positive_dirichlet_inverserightvaluemaskentryleftvalue ge_balance_negative_dirichlet_inverserightvaluemaskentryleftvalue. (((((dc_left_dirichlet_inverserightvaluemaskentry) = 2 * (ge_balance_positive_dirichlet_inverserightvaluemaskentryleftvalue) /\ (ge_balance_negative_dirichlet_inverserightvaluemaskentryleftvalue) = 0) \/ exists ge_signed_half_dirichlet_inverserightvaluemaskentryleftvaluedecode. (((dc_left_dirichlet_inverserightvaluemaskentry) = 2 * ge_signed_half_dirichlet_inverserightvaluemaskentryleftvaluedecode + 1 /\ (ge_balance_positive_dirichlet_inverserightvaluemaskentryleftvalue) = 0) /\ (ge_balance_negative_dirichlet_inverserightvaluemaskentryleftvalue) = S ge_signed_half_dirichlet_inverserightvaluemaskentryleftvaluedecode))) /\ ((dst_positive_dirichlet_inverserightvaluemaskentryleft) + ge_balance_negative_dirichlet_inverserightvaluemaskentryleftvalue = (dst_negative_dirichlet_inverserightvaluemaskentryleft) + ge_balance_positive_dirichlet_inverserightvaluemaskentryleftvalue))))))))) /\ (((exists dst_positive_code_dirichlet_inverserightvaluemaskentryright dst_positive_scale_dirichlet_inverserightvaluemaskentryright dst_negative_code_dirichlet_inverserightvaluemaskentryright dst_negative_scale_dirichlet_inverserightvaluemaskentryright dst_positive_dirichlet_inverserightvaluemaskentryright dst_negative_dirichlet_inverserightvaluemaskentryright. ((((F)) = (((((dst_positive_code_dirichlet_inverserightvaluemaskentryright) + (dst_positive_scale_dirichlet_inverserightvaluemaskentryright)) * S ((dst_positive_code_dirichlet_inverserightvaluemaskentryright) + (dst_positive_scale_dirichlet_inverserightvaluemaskentryright)) + ((dst_positive_scale_dirichlet_inverserightvaluemaskentryright) + (dst_positive_scale_dirichlet_inverserightvaluemaskentryright))) + (((dst_negative_code_dirichlet_inverserightvaluemaskentryright) + (dst_negative_scale_dirichlet_inverserightvaluemaskentryright)) * S ((dst_negative_code_dirichlet_inverserightvaluemaskentryright) + (dst_negative_scale_dirichlet_inverserightvaluemaskentryright)) + ((dst_negative_scale_dirichlet_inverserightvaluemaskentryright) + (dst_negative_scale_dirichlet_inverserightvaluemaskentryright)))) * S ((((dst_positive_code_dirichlet_inverserightvaluemaskentryright) + (dst_positive_scale_dirichlet_inverserightvaluemaskentryright)) * S ((dst_positive_code_dirichlet_inverserightvaluemaskentryright) + (dst_positive_scale_dirichlet_inverserightvaluemaskentryright)) + ((dst_positive_scale_dirichlet_inverserightvaluemaskentryright) + (dst_positive_scale_dirichlet_inverserightvaluemaskentryright))) + (((dst_negative_code_dirichlet_inverserightvaluemaskentryright) + (dst_negative_scale_dirichlet_inverserightvaluemaskentryright)) * S ((dst_negative_code_dirichlet_inverserightvaluemaskentryright) + (dst_negative_scale_dirichlet_inverserightvaluemaskentryright)) + ((dst_negative_scale_dirichlet_inverserightvaluemaskentryright) + (dst_negative_scale_dirichlet_inverserightvaluemaskentryright)))) + ((((dst_negative_code_dirichlet_inverserightvaluemaskentryright) + (dst_negative_scale_dirichlet_inverserightvaluemaskentryright)) * S ((dst_negative_code_dirichlet_inverserightvaluemaskentryright) + (dst_negative_scale_dirichlet_inverserightvaluemaskentryright)) + ((dst_negative_scale_dirichlet_inverserightvaluemaskentryright) + (dst_negative_scale_dirichlet_inverserightvaluemaskentryright))) + (((dst_negative_code_dirichlet_inverserightvaluemaskentryright) + (dst_negative_scale_dirichlet_inverserightvaluemaskentryright)) * S ((dst_negative_code_dirichlet_inverserightvaluemaskentryright) + (dst_negative_scale_dirichlet_inverserightvaluemaskentryright)) + ((dst_negative_scale_dirichlet_inverserightvaluemaskentryright) + (dst_negative_scale_dirichlet_inverserightvaluemaskentryright)))))) /\ (((((exists ff_h_pvs_dirichlet_inverserightvaluemaskentryrightpositive. ff_h_pvs_dirichlet_inverserightvaluemaskentryrightpositive + S (dst_positive_dirichlet_inverserightvaluemaskentryright) = S ((S (dc_quotient_dirichlet_inverserightvaluemaskentry)) * dst_positive_scale_dirichlet_inverserightvaluemaskentryright)) /\ exists ff_q_pvs_dirichlet_inverserightvaluemaskentryrightpositive. dst_positive_code_dirichlet_inverserightvaluemaskentryright = ff_q_pvs_dirichlet_inverserightvaluemaskentryrightpositive * S ((S (dc_quotient_dirichlet_inverserightvaluemaskentry)) * dst_positive_scale_dirichlet_inverserightvaluemaskentryright) + (dst_positive_dirichlet_inverserightvaluemaskentryright))) /\ (((((exists ff_h_pvs_dirichlet_inverserightvaluemaskentryrightnegative. ff_h_pvs_dirichlet_inverserightvaluemaskentryrightnegative + S (dst_negative_dirichlet_inverserightvaluemaskentryright) = S ((S (dc_quotient_dirichlet_inverserightvaluemaskentry)) * dst_negative_scale_dirichlet_inverserightvaluemaskentryright)) /\ exists ff_q_pvs_dirichlet_inverserightvaluemaskentryrightnegative. dst_negative_code_dirichlet_inverserightvaluemaskentryright = ff_q_pvs_dirichlet_inverserightvaluemaskentryrightnegative * S ((S (dc_quotient_dirichlet_inverserightvaluemaskentry)) * dst_negative_scale_dirichlet_inverserightvaluemaskentryright) + (dst_negative_dirichlet_inverserightvaluemaskentryright))) /\ (exists ge_balance_positive_dirichlet_inverserightvaluemaskentryrightvalue ge_balance_negative_dirichlet_inverserightvaluemaskentryrightvalue. (((((dc_right_dirichlet_inverserightvaluemaskentry) = 2 * (ge_balance_positive_dirichlet_inverserightvaluemaskentryrightvalue) /\ (ge_balance_negative_dirichlet_inverserightvaluemaskentryrightvalue) = 0) \/ exists ge_signed_half_dirichlet_inverserightvaluemaskentryrightvaluedecode. (((dc_right_dirichlet_inverserightvaluemaskentry) = 2 * ge_signed_half_dirichlet_inverserightvaluemaskentryrightvaluedecode + 1 /\ (ge_balance_positive_dirichlet_inverserightvaluemaskentryrightvalue) = 0) /\ (ge_balance_negative_dirichlet_inverserightvaluemaskentryrightvalue) = S ge_signed_half_dirichlet_inverserightvaluemaskentryrightvaluedecode))) /\ ((dst_positive_dirichlet_inverserightvaluemaskentryright) + ge_balance_negative_dirichlet_inverserightvaluemaskentryrightvalue = (dst_negative_dirichlet_inverserightvaluemaskentryright) + ge_balance_positive_dirichlet_inverserightvaluemaskentryrightvalue))))))))) /\ (exists sto_ap_dirichlet_inverserightvaluemaskentryproduct sto_an_dirichlet_inverserightvaluemaskentryproduct sto_bp_dirichlet_inverserightvaluemaskentryproduct sto_bn_dirichlet_inverserightvaluemaskentryproduct sto_cp_dirichlet_inverserightvaluemaskentryproduct sto_cn_dirichlet_inverserightvaluemaskentryproduct. (((((dc_left_dirichlet_inverserightvaluemaskentry) = 2 * (sto_ap_dirichlet_inverserightvaluemaskentryproduct) /\ (sto_an_dirichlet_inverserightvaluemaskentryproduct) = 0) \/ exists ge_signed_half_dirichlet_inverserightvaluemaskentryproductleft. (((dc_left_dirichlet_inverserightvaluemaskentry) = 2 * ge_signed_half_dirichlet_inverserightvaluemaskentryproductleft + 1 /\ (sto_ap_dirichlet_inverserightvaluemaskentryproduct) = 0) /\ (sto_an_dirichlet_inverserightvaluemaskentryproduct) = S ge_signed_half_dirichlet_inverserightvaluemaskentryproductleft))) /\ ((((((dc_right_dirichlet_inverserightvaluemaskentry) = 2 * (sto_bp_dirichlet_inverserightvaluemaskentryproduct) /\ (sto_bn_dirichlet_inverserightvaluemaskentryproduct) = 0) \/ exists ge_signed_half_dirichlet_inverserightvaluemaskentryproductright. (((dc_right_dirichlet_inverserightvaluemaskentry) = 2 * ge_signed_half_dirichlet_inverserightvaluemaskentryproductright + 1 /\ (sto_bp_dirichlet_inverserightvaluemaskentryproduct) = 0) /\ (sto_bn_dirichlet_inverserightvaluemaskentryproduct) = S ge_signed_half_dirichlet_inverserightvaluemaskentryproductright))) /\ ((((((dc_value_dirichlet_inverserightvaluemask) = 2 * (sto_cp_dirichlet_inverserightvaluemaskentryproduct) /\ (sto_cn_dirichlet_inverserightvaluemaskentryproduct) = 0) \/ exists ge_signed_half_dirichlet_inverserightvaluemaskentryproductoutput. (((dc_value_dirichlet_inverserightvaluemask) = 2 * ge_signed_half_dirichlet_inverserightvaluemaskentryproductoutput + 1 /\ (sto_cp_dirichlet_inverserightvaluemaskentryproduct) = 0) /\ (sto_cn_dirichlet_inverserightvaluemaskentryproduct) = S ge_signed_half_dirichlet_inverserightvaluemaskentryproductoutput))) /\ ((sto_ap_dirichlet_inverserightvaluemaskentryproduct * sto_bp_dirichlet_inverserightvaluemaskentryproduct + sto_an_dirichlet_inverserightvaluemaskentryproduct * sto_bn_dirichlet_inverserightvaluemaskentryproduct) + sto_cn_dirichlet_inverserightvaluemaskentryproduct = (sto_ap_dirichlet_inverserightvaluemaskentryproduct * sto_bn_dirichlet_inverserightvaluemaskentryproduct + sto_an_dirichlet_inverserightvaluemaskentryproduct * sto_bp_dirichlet_inverserightvaluemaskentryproduct) + sto_cp_dirichlet_inverserightvaluemaskentryproduct))))))))))))))) \/ ((((dc_index_dirichlet_inverserightvaluemask)=0 \/ ~(exists pvs_factor_dirichlet_inverserightvaluemaskentrynondivisor. (dc_input_dirichlet_inverseright) = (dc_index_dirichlet_inverserightvaluemask) * pvs_factor_dirichlet_inverserightvaluemaskentrynondivisor)) /\ ((dc_value_dirichlet_inverserightvaluemask)=0))))))) /\ (exists dst_positive_code_dirichlet_inverserightvaluefold dst_positive_scale_dirichlet_inverserightvaluefold dst_negative_code_dirichlet_inverserightvaluefold dst_negative_scale_dirichlet_inverserightvaluefold dst_positive_sum_dirichlet_inverserightvaluefold dst_negative_sum_dirichlet_inverserightvaluefold. (((dc_mask_dirichlet_inverserightvalue) = (((((dst_positive_code_dirichlet_inverserightvaluefold) + (dst_positive_scale_dirichlet_inverserightvaluefold)) * S ((dst_positive_code_dirichlet_inverserightvaluefold) + (dst_positive_scale_dirichlet_inverserightvaluefold)) + ((dst_positive_scale_dirichlet_inverserightvaluefold) + (dst_positive_scale_dirichlet_inverserightvaluefold))) + (((dst_negative_code_dirichlet_inverserightvaluefold) + (dst_negative_scale_dirichlet_inverserightvaluefold)) * S ((dst_negative_code_dirichlet_inverserightvaluefold) + (dst_negative_scale_dirichlet_inverserightvaluefold)) + ((dst_negative_scale_dirichlet_inverserightvaluefold) + (dst_negative_scale_dirichlet_inverserightvaluefold)))) * S ((((dst_positive_code_dirichlet_inverserightvaluefold) + (dst_positive_scale_dirichlet_inverserightvaluefold)) * S ((dst_positive_code_dirichlet_inverserightvaluefold) + (dst_positive_scale_dirichlet_inverserightvaluefold)) + ((dst_positive_scale_dirichlet_inverserightvaluefold) + (dst_positive_scale_dirichlet_inverserightvaluefold))) + (((dst_negative_code_dirichlet_inverserightvaluefold) + (dst_negative_scale_dirichlet_inverserightvaluefold)) * S ((dst_negative_code_dirichlet_inverserightvaluefold) + (dst_negative_scale_dirichlet_inverserightvaluefold)) + ((dst_negative_scale_dirichlet_inverserightvaluefold) + (dst_negative_scale_dirichlet_inverserightvaluefold)))) + ((((dst_negative_code_dirichlet_inverserightvaluefold) + (dst_negative_scale_dirichlet_inverserightvaluefold)) * S ((dst_negative_code_dirichlet_inverserightvaluefold) + (dst_negative_scale_dirichlet_inverserightvaluefold)) + ((dst_negative_scale_dirichlet_inverserightvaluefold) + (dst_negative_scale_dirichlet_inverserightvaluefold))) + (((dst_negative_code_dirichlet_inverserightvaluefold) + (dst_negative_scale_dirichlet_inverserightvaluefold)) * S ((dst_negative_code_dirichlet_inverserightvaluefold) + (dst_negative_scale_dirichlet_inverserightvaluefold)) + ((dst_negative_scale_dirichlet_inverserightvaluefold) + (dst_negative_scale_dirichlet_inverserightvaluefold)))))) /\ (((exists fs_u_dst_dirichlet_inverserightvaluefoldpositive fs_v_dst_dirichlet_inverserightvaluefoldpositive. ((((exists fs_h_dst_dirichlet_inverserightvaluefoldpositive_body_start. fs_h_dst_dirichlet_inverserightvaluefoldpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_dirichlet_inverserightvaluefoldpositive)) /\ exists fs_q_dst_dirichlet_inverserightvaluefoldpositive_body_start. fs_u_dst_dirichlet_inverserightvaluefoldpositive = fs_q_dst_dirichlet_inverserightvaluefoldpositive_body_start * S ((S (0)) * fs_v_dst_dirichlet_inverserightvaluefoldpositive) + (0))) /\ ((((exists fs_h_dst_dirichlet_inverserightvaluefoldpositive_body_terminal. fs_h_dst_dirichlet_inverserightvaluefoldpositive_body_terminal + S (dst_positive_sum_dirichlet_inverserightvaluefold) = S ((S (S (dc_input_dirichlet_inverseright))) * fs_v_dst_dirichlet_inverserightvaluefoldpositive)) /\ exists fs_q_dst_dirichlet_inverserightvaluefoldpositive_body_terminal. fs_u_dst_dirichlet_inverserightvaluefoldpositive = fs_q_dst_dirichlet_inverserightvaluefoldpositive_body_terminal * S ((S (S (dc_input_dirichlet_inverseright))) * fs_v_dst_dirichlet_inverserightvaluefoldpositive) + (dst_positive_sum_dirichlet_inverserightvaluefold))) /\ forall fs_i_dst_dirichlet_inverserightvaluefoldpositive_body_steps. (exists fs_lt_dst_dirichlet_inverserightvaluefoldpositive_body_steps_bound. fs_lt_dst_dirichlet_inverserightvaluefoldpositive_body_steps_bound + S fs_i_dst_dirichlet_inverserightvaluefoldpositive_body_steps = S (dc_input_dirichlet_inverseright)) -> exists fs_a_dst_dirichlet_inverserightvaluefoldpositive_body_steps fs_r_dst_dirichlet_inverserightvaluefoldpositive_body_steps fs_s_dst_dirichlet_inverserightvaluefoldpositive_body_steps. ((((exists fs_h_dst_dirichlet_inverserightvaluefoldpositive_body_steps_summand. fs_h_dst_dirichlet_inverserightvaluefoldpositive_body_steps_summand + S (fs_a_dst_dirichlet_inverserightvaluefoldpositive_body_steps) = S ((S (fs_i_dst_dirichlet_inverserightvaluefoldpositive_body_steps)) * dst_positive_scale_dirichlet_inverserightvaluefold)) /\ exists fs_q_dst_dirichlet_inverserightvaluefoldpositive_body_steps_summand. dst_positive_code_dirichlet_inverserightvaluefold = fs_q_dst_dirichlet_inverserightvaluefoldpositive_body_steps_summand * S ((S (fs_i_dst_dirichlet_inverserightvaluefoldpositive_body_steps)) * dst_positive_scale_dirichlet_inverserightvaluefold) + (fs_a_dst_dirichlet_inverserightvaluefoldpositive_body_steps))) /\ ((((exists fs_h_dst_dirichlet_inverserightvaluefoldpositive_body_steps_partial. fs_h_dst_dirichlet_inverserightvaluefoldpositive_body_steps_partial + S (fs_r_dst_dirichlet_inverserightvaluefoldpositive_body_steps) = S ((S (fs_i_dst_dirichlet_inverserightvaluefoldpositive_body_steps)) * fs_v_dst_dirichlet_inverserightvaluefoldpositive)) /\ exists fs_q_dst_dirichlet_inverserightvaluefoldpositive_body_steps_partial. fs_u_dst_dirichlet_inverserightvaluefoldpositive = fs_q_dst_dirichlet_inverserightvaluefoldpositive_body_steps_partial * S ((S (fs_i_dst_dirichlet_inverserightvaluefoldpositive_body_steps)) * fs_v_dst_dirichlet_inverserightvaluefoldpositive) + (fs_r_dst_dirichlet_inverserightvaluefoldpositive_body_steps))) /\ ((((exists fs_h_dst_dirichlet_inverserightvaluefoldpositive_body_steps_successor. fs_h_dst_dirichlet_inverserightvaluefoldpositive_body_steps_successor + S (fs_s_dst_dirichlet_inverserightvaluefoldpositive_body_steps) = S ((S (S fs_i_dst_dirichlet_inverserightvaluefoldpositive_body_steps)) * fs_v_dst_dirichlet_inverserightvaluefoldpositive)) /\ exists fs_q_dst_dirichlet_inverserightvaluefoldpositive_body_steps_successor. fs_u_dst_dirichlet_inverserightvaluefoldpositive = fs_q_dst_dirichlet_inverserightvaluefoldpositive_body_steps_successor * S ((S (S fs_i_dst_dirichlet_inverserightvaluefoldpositive_body_steps)) * fs_v_dst_dirichlet_inverserightvaluefoldpositive) + (fs_s_dst_dirichlet_inverserightvaluefoldpositive_body_steps))) /\ fs_s_dst_dirichlet_inverserightvaluefoldpositive_body_steps = fs_r_dst_dirichlet_inverserightvaluefoldpositive_body_steps + fs_a_dst_dirichlet_inverserightvaluefoldpositive_body_steps)))))) /\ (((exists fs_u_dst_dirichlet_inverserightvaluefoldnegative fs_v_dst_dirichlet_inverserightvaluefoldnegative. ((((exists fs_h_dst_dirichlet_inverserightvaluefoldnegative_body_start. fs_h_dst_dirichlet_inverserightvaluefoldnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_dirichlet_inverserightvaluefoldnegative)) /\ exists fs_q_dst_dirichlet_inverserightvaluefoldnegative_body_start. fs_u_dst_dirichlet_inverserightvaluefoldnegative = fs_q_dst_dirichlet_inverserightvaluefoldnegative_body_start * S ((S (0)) * fs_v_dst_dirichlet_inverserightvaluefoldnegative) + (0))) /\ ((((exists fs_h_dst_dirichlet_inverserightvaluefoldnegative_body_terminal. fs_h_dst_dirichlet_inverserightvaluefoldnegative_body_terminal + S (dst_negative_sum_dirichlet_inverserightvaluefold) = S ((S (S (dc_input_dirichlet_inverseright))) * fs_v_dst_dirichlet_inverserightvaluefoldnegative)) /\ exists fs_q_dst_dirichlet_inverserightvaluefoldnegative_body_terminal. fs_u_dst_dirichlet_inverserightvaluefoldnegative = fs_q_dst_dirichlet_inverserightvaluefoldnegative_body_terminal * S ((S (S (dc_input_dirichlet_inverseright))) * fs_v_dst_dirichlet_inverserightvaluefoldnegative) + (dst_negative_sum_dirichlet_inverserightvaluefold))) /\ forall fs_i_dst_dirichlet_inverserightvaluefoldnegative_body_steps. (exists fs_lt_dst_dirichlet_inverserightvaluefoldnegative_body_steps_bound. fs_lt_dst_dirichlet_inverserightvaluefoldnegative_body_steps_bound + S fs_i_dst_dirichlet_inverserightvaluefoldnegative_body_steps = S (dc_input_dirichlet_inverseright)) -> exists fs_a_dst_dirichlet_inverserightvaluefoldnegative_body_steps fs_r_dst_dirichlet_inverserightvaluefoldnegative_body_steps fs_s_dst_dirichlet_inverserightvaluefoldnegative_body_steps. ((((exists fs_h_dst_dirichlet_inverserightvaluefoldnegative_body_steps_summand. fs_h_dst_dirichlet_inverserightvaluefoldnegative_body_steps_summand + S (fs_a_dst_dirichlet_inverserightvaluefoldnegative_body_steps) = S ((S (fs_i_dst_dirichlet_inverserightvaluefoldnegative_body_steps)) * dst_negative_scale_dirichlet_inverserightvaluefold)) /\ exists fs_q_dst_dirichlet_inverserightvaluefoldnegative_body_steps_summand. dst_negative_code_dirichlet_inverserightvaluefold = fs_q_dst_dirichlet_inverserightvaluefoldnegative_body_steps_summand * S ((S (fs_i_dst_dirichlet_inverserightvaluefoldnegative_body_steps)) * dst_negative_scale_dirichlet_inverserightvaluefold) + (fs_a_dst_dirichlet_inverserightvaluefoldnegative_body_steps))) /\ ((((exists fs_h_dst_dirichlet_inverserightvaluefoldnegative_body_steps_partial. fs_h_dst_dirichlet_inverserightvaluefoldnegative_body_steps_partial + S (fs_r_dst_dirichlet_inverserightvaluefoldnegative_body_steps) = S ((S (fs_i_dst_dirichlet_inverserightvaluefoldnegative_body_steps)) * fs_v_dst_dirichlet_inverserightvaluefoldnegative)) /\ exists fs_q_dst_dirichlet_inverserightvaluefoldnegative_body_steps_partial. fs_u_dst_dirichlet_inverserightvaluefoldnegative = fs_q_dst_dirichlet_inverserightvaluefoldnegative_body_steps_partial * S ((S (fs_i_dst_dirichlet_inverserightvaluefoldnegative_body_steps)) * fs_v_dst_dirichlet_inverserightvaluefoldnegative) + (fs_r_dst_dirichlet_inverserightvaluefoldnegative_body_steps))) /\ ((((exists fs_h_dst_dirichlet_inverserightvaluefoldnegative_body_steps_successor. fs_h_dst_dirichlet_inverserightvaluefoldnegative_body_steps_successor + S (fs_s_dst_dirichlet_inverserightvaluefoldnegative_body_steps) = S ((S (S fs_i_dst_dirichlet_inverserightvaluefoldnegative_body_steps)) * fs_v_dst_dirichlet_inverserightvaluefoldnegative)) /\ exists fs_q_dst_dirichlet_inverserightvaluefoldnegative_body_steps_successor. fs_u_dst_dirichlet_inverserightvaluefoldnegative = fs_q_dst_dirichlet_inverserightvaluefoldnegative_body_steps_successor * S ((S (S fs_i_dst_dirichlet_inverserightvaluefoldnegative_body_steps)) * fs_v_dst_dirichlet_inverserightvaluefoldnegative) + (fs_s_dst_dirichlet_inverserightvaluefoldnegative_body_steps))) /\ fs_s_dst_dirichlet_inverserightvaluefoldnegative_body_steps = fs_r_dst_dirichlet_inverserightvaluefoldnegative_body_steps + fs_a_dst_dirichlet_inverserightvaluefoldnegative_body_steps)))))) /\ (exists ge_balance_positive_dirichlet_inverserightvaluefoldresult ge_balance_negative_dirichlet_inverserightvaluefoldresult. (((((dc_output_dirichlet_inverseright) = 2 * (ge_balance_positive_dirichlet_inverserightvaluefoldresult) /\ (ge_balance_negative_dirichlet_inverserightvaluefoldresult) = 0) \/ exists ge_signed_half_dirichlet_inverserightvaluefoldresultdecode. (((dc_output_dirichlet_inverseright) = 2 * ge_signed_half_dirichlet_inverserightvaluefoldresultdecode + 1 /\ (ge_balance_positive_dirichlet_inverserightvaluefoldresult) = 0) /\ (ge_balance_negative_dirichlet_inverserightvaluefoldresult) = S ge_signed_half_dirichlet_inverserightvaluefoldresultdecode))) /\ ((dst_positive_sum_dirichlet_inverserightvaluefold) + ge_balance_negative_dirichlet_inverserightvaluefoldresult = (dst_negative_sum_dirichlet_inverserightvaluefold) + ge_balance_positive_dirichlet_inverserightvaluefoldresult)))))))))))))))))))))))

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